Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: Use equivalence information from equality assertions to simplify circuit #2378

Merged
merged 3 commits into from
Aug 22, 2023
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view

Large diffs are not rendered by default.

Binary file not shown.
Original file line number Diff line number Diff line change
@@ -1 +1 @@
H4sIAAAAAAAA/+2debRXUxvHn9s8z/NERESc3526lygRESkiIurWjYiIiEglIiIiIhqIiBQRESkiokRESjLP8zy9++v+Wm/ned//znP2Ot/VOWs9q76stfvu/Zz92Xv/zjl7b8kR6VdB/r3cX6Vc9s8q2+lySpdXuoLSFZWupHRlpasoXVXpakpXV7qG0jWVrqV0baXrKF1X6XpK11e6gdINlW6kdGOlmyjdVOlmSjdXuoXSLZVupfROSu+c1cibZLVION8Vsv+/0nb5q5rNTfVsDmpm27p2tk3rZtuufraNGmbbonG2zk2zdWuerUPLrNedsh62/futs3/fpndRelel2yi9m9K7K91W6T2U3lPpdkrvpfTeSrdXeh+l91U6UDqjdK7SeUrnK12gdKHSHZQuUrpY6f2U3l/pjkofoPSBSndSurPSByndRemDlT5E6a5KH6r0YUp3U/pwpY9QurvSRyp9lNI9lD5a6Z5K91L6GKWPVbq30scpfbzSfZQ+QekTle6r9ElKn6x0P6VPUfpUpfsrPUDpEqUHKj1I6VKlByt9mtKnKz1E6TOUPlPpoUqfpfTZSg9T+hylz1V6uNLnKX2+0iOUvkDpC5UeqfRFSl+s9CilL1H6UqVHK32Z0mOUHqv0OKUvV3q80lcofaXSE5S+SumrlZ6o9DVKX6v0JKWvU/p6pScrfYPSNyo9RemblL5Z6alK36L0rUpPU/o2pW9XerrSdyh9p9IzlJ6p9CylZyt9l9J3Kz1H6XuUvlfpuUrfp/T9Ss9T+gGlH1R6vtIPKb1A6YVKP6z0I0ovUvpRpR9TerHSjyv9hNJLlH5S6aeUXqr000o/o/QypZ9VernSK5R+TunnlV6p9AtKv6j0KqVfUvplpVcr/YrSryq9Rum1Sr+m9DqlX1f6DaXXK/2m0m8pvUHpt5V+R+mNSr+r9CalNyv9ntJblH5f6a1Kf6D0h0p/pPTHSn+i9KdKf6b050p/ofSXSn+l9NdKf6P0t0p/p/T3Sv+g9I9K/6T0z0r/ovSvSv+m9O9K/6H0n0r/pfTfSv+jNP6yvc5RupzS5ZWuoHRFpSspXVnpKkpXVbqa0tWVrqF0TaVrKV1b6TpK11W6ntL1lW6gdEOlGyndWOkmSjdVupnSzZVuoXRLpVtldcXsf8P9gKu1lK3tsZ7HGh7rdqzVsT7HmhzrcKy9sd7GGhvraqylsX7GmhnrZKyNsR7GGhjrXqx1sb7FmhbrWKxdsV7FGhXrUqxFsf7sLGXrzC5Stp7EGhLrRqwVsT7EmhDrQKz9sN7DGg/rOqzlsH7Dmg3rNKzNsB7DGgzrLqy1sL7CmgrrKKydsF7CGgnrIqyFsP7pL2XrnBIpW89gDYN1C9YqWJ9gTYJ1CNYeWG9gjYF1BdYSWD9gzYB1AtYGWA9gDYB5P+b6mN9jTo95PObumK9jjo55OebimH+PkbJ59jgpm09jDo15M+bKmB9jTox5MOa+mO9ijot5LeaymL9izop5KuammI9iDop5J+aamF9iTol5JOaOmC9ijoh5IeaCmP/NlLJ53mwpm89hDod5G+ZqmJ9hToZ5GOZemG9hjoV5FeZSmD9hzoR5EuZGmA9hDoR5D+Y6mN9gToN5DOYumK9gjoJ5CeYimH8sk7J5xnIpm09gDoF5A+YKmB9gToB5AMZ+jPcY4zGuYyzH+I0xG+M0xmaMxxiDMe5irMX4ijEV4yjGToyXGCMxLmIsxPi3RcrGua1SNp5hDMO4hbEK4xPGJIxDGHsw3mCMwbiCsQTjB8YMjBMYGzAeYAwA98F68B1MB8fBbvAajAaX0ffA33+Zm1PGVvAUDAU3wUrwEUwEB8E+8A6MA9fAMvALzAKnwCbwCAwCd8Aa8AVMAUfADvACjAAXwILtr3LZPztn/8wLCvPzSzvklmbyMgOC3OKSooIgv6CksChTlCkoKhiUW5SXV1qUX9ShuKS4Q1Ccyc8rzQwuKM4bHJRdOYZl7ZTz37KCSFdeUL6syf/nylH1D6JdGTvPZW257dp5O1FB5Q5X+eyflWKok6h/R7djrf/z30z/8TiStHOOfbmtc+xu/rjq3TrHPEeBbHclvU23XdbgK2dY1i5mECnM9wU+O89h8O2ags82SbvGAL42CQcf6t2GDHxtSMBX3rCs3cwgkl/qC3x2nsPg2z0Fn22Sdo8BfG0TDj7Uuy0Z+NqSgK+CYVl7mEGkQ64v8Nl5DoNvzxR8tknaMwbwtUs4+FDvdmTga0cCvoqGZe1lBpHSjC/w2XkOg2/vFHy2Sdo7BvC1Tzj4UO/2ZOBrTwK+SoZl7WP3cMMb+Ow8h8G3bwo+2yTtGwP4goSDD/UOyMAXkICvsmFZGTOIDPD2VNfOcxh8uSn4bJOUGwP48hIOPtQ7jwx8eSTgq2JYVr4ZRHKLfYHPznMYfAUp+GyTVBAD+AoTDj7Uu5AMfIUk4KtqWFYHM4iUFPkCn53nMPiKUvDZJqkoBvAVJxx8qHcxGfiKScBXzbCs/cwgUuBtqWvnOQy+/VPw2SZp/xjA1zHh4EO9O5KBryMJ+KoblnWAGUTyC3yBz85zGHwHpuCzTdKBMYCvU8LBh3p3IgNfJxLw1TAsq7PdUrfQF/jsPIfBd1AKPtskHRQD+LokHHyodxcy8HUhAV9Nw7IONoNIkbfXWew8h8F3SAo+2yQdEgP4uiYcfKh3VzLwdSUBXy3Dsg4lBJ+d5zD4DkvBZ5ukw2IAX7eEgw/17kYGvm4k4KttWNbhdg83vD3VtfMcBt8RKfhsk3REDODrnnDwod7dycDXnQR8dQzLOtIOfIN8gc/Ocxh8R6Xgs03SUTGAr0fCwYd69yADXw8S8NU1LOtoM4jkepvx2XkOg69nCj7bJPWMAXy9Eg4+1LsXGfh6kYCvnmFZx5hBJC/PF/jsPIfBd2wKPtskHRsD+HonHHyod28y8PUmAV99w7KOM4NIqbcZn53nMPiOT8Fnm6TjYwBfn4SDD/XuQwa+PiTga2BY1glmEMn3Bj47z2HwnZiCzzZJJ8YAvr4JBx/q3ZcMfH1JwNfQsKyTzCDSwdsmBXaew+A7OQWfbZJOjgF8/RIOPtS7Hxn4+pGAr5FhWaeYQaTEG/jsPIfBd2oKPtsknRoD+PonHHyod38y8PUnAV9jw7IG2M34vG1SYOc5DL6SFHy2SSqJAXwDEw4+1HsgGfgGkoCviWFZg8wgUuztyw07z2Hwlabgs01SaQzgG5xw8KHeg8nAN5gEfE0NyzrN7uGGt9dZ7DyHwXd6Cj7bJJ0eA/iGJBx8qPcQMvANIQFfM8OyzjCDiL/Dhuw8h8F3Zgo+2ySdGQP4hiYcfKj3UDLwDSUBX3PDss4yg8hgb/vx2XkOg+/sFHy2STo7BvANSzj4UO9hZOAbRgK+FoZlnWP3G5+3pa6d5zD4zk3BZ5ukc2MA3/CEgw/1Hk4GvuEk4GtpWNZ5djM+b0917TyHwXd+Cj7bJJ0fA/hGJBx8qPcIMvCNIAFfK8OyLjCEiC/wXRAT+C5MwWebpAtjAN/IhIMP9R5JBr6RJODbybCsiwjBd1FM4Ls4BZ9tki6OAXyjEg4+1HsUGfhGkYBvZ8OyLrGDiLenupfEBL5LU/DZJunSGMA3OuHgQ71Hk4Fv9A4IvssIwXdZTOAbk4LPNkljYgDf2ISDD/UeSwa+sSTgs1zqjiNc6o6LCXyXp+CzTdLlMYBvfMLBh3qPJwPfeBLwWT7cuIIQfFfEBL4rU/DZJunKGMA3IeHgQ70nkIFvAgn4LF9nucoMIv5eZ7HzHAbf1Sn4bJN0dQzgm5hw8KHeE8nAN5EEfJYvMF9jBhF/LzDbeQ6D79oUfLZJujYG8E1KOPhQ70lk4JtEAj7LT9aus5vxeftkzc5zGHzXp+CzTdL1MYBvcsLBh3pPJgPfZBLwWW5ScIMZRPxtUmDnOQy+G1Pw2SbpxhjANyXh4EO9p5CBbwoJ+Cy3pbrJDCL+tqWy8xwG380p+GyTdHMM4JuacPCh3lPJwDeVBHyWG5HeYvcbn7cZn53nMPhuTcFnm6RbYwDftISDD/WeRga+aSTgs9x6/jYziPjbet7Ocxh8t6fgs03S7TGAb3rCwYd6TycD33QS8FkeNnSHGUT8HTZk5zkMvjtT8Nkm6c4YwDcj4eBDvWeQgW8GCfgsj5ecaTfj8wY+O89h8M1KwWebpFkxgG92wsGHes8mA99sEvBZHih+l93DDW8Hitt5DoPv7hR8tkm6OwbwzUk4+FDvOWTgm0MCvvqGZd1jBpFSb+Cz8xwG370p+GyTdG8M4JubcPCh3nPJwDeXBHz1DMu6zwwied5eZ7HzHAbf/Sn4bJN0fwzgm5dw8KHe88jAN48EfHUNy3rADCK53mZ8dp7D4HswBZ9tkh6MAXzzEw4+1Hs+Gfjmk4CvjmFZD5lBpGCQL/DZeQ6Db0EKPtskLYgBfAsTDj7UeyEZ+BaSgK+2YVkP24HP24zPznMYfI+k4LNN0iMxgG9RwsGHei8iA98iEvDVMizrUTOIFHn7csPOcxh8j6Xgs03SYzGAb3HCwYd6LyYD32IS8NU0LOtxQvDZeQ6D74kUfLZJeiIG8C1JOPhQ7yVk4FtCAr4ahmU9aQaRkkJf4LPzHAbfUyn4bJP0VAzgW5pw8KHeS8nAt5QEfNUNy3raDCL53vbjs/McBt8zKfhsk/RMDOBblnDwod7LyMC3jAR81QzLetbu4Ya3TQrsPIfBtzwFn22SlscAvhUJBx/qvYIMfCtIwFfVsKzn7Ja63p7q2nkOg+/5FHy2SXo+BvCtTDj4UO+VZOBbSQK+KoZlvWAGkVxvmxTYeQ6D78UUfLZJejEG8K1KOPhQ71Vk4FtFAr7KhmW9ZAaRAd6Wunaew+B7OQWfbZJejgF8qxMOPtR7NRn4VpOAr5JhWa+YQSTP2+ssdp7D4Hs1BZ9tkl6NAXxrEg4+1HsNGfjWkICvomFZa80g4u+wITvPYfC9loLPNkmvxQC+dQkHH+q9jgx860jAV8GwrNfNINIh1xf47DyHwfdGCj7bJL0RA/jWJxx8qPd6MvCtJwFfecOy3jSDSH6pL/DZeQ6D760UfLZJeisG8G1IOPhQ7w1k4NtAAr5yhmW9bQaRwnxf4LPzHAbfOyn4bJP0Tgzg25hw8KHeG8nAt5EEfDmGZb1r93DD21NdO89h8G1KwWebpE0xgG9zwsGHem8mA9/mmMBn7bO1cPjcxZPPqGXvKn7uz6g+25D43I3E5+4kPtsKBz/3EA4u7SkcXGonHPfnXiT3594keW9Pkvd9SHzuS3J/BiT3Z4Yk77kkec8TjnEzn8RngXD0o0Lh6EcdhKMfFZHcn8UkPvcTjn60v3D0o47C0Y8OIMn7gSTt2Uk4+ntnEp8HkdyfXYSDSweT+DyExGdX4eDSocLRjw4jyXs3krwfLhycP4Lk/uwuHPfnkSQ+jxKOftRDOPrR0cLRj3oKR957kbTnMcLR348l8dmbxOdxJD6PJ/HZh8TnCcLBzxOFg599SdrzJJL2PFk4+lE/kryf4invQbQrcyrJ/dlfOPI+gCTvJSQ+B5Lcn4OEg5+lJD4Hk/g8TTi4dLpw9KMhJO15Bkl7nikc/Wgoic+zSHyeTeJzmHD093OEo7+fS5L34SQ+zyO5P88nuT9HkLTnBZ7aM4h2ZS4kyftI4cj7RSR5v5gk76OEI++XkOT9UpK8jxaOvF9G0p5jhGO+NJbE5zgSn5eT+BxP4vMK4eDSlcIxHk0QDn5eJRz359UkPieS+LyGxOe1JD4nCQc/rxMOLl1P0p6TSdrzBpL2vNFTewbRrswUkrzfJBz8vJnE51QSn7cIR3+/VTj60TSS9rxNOPh5O4nP6ST35x3CcX/eSdKeM4SD8zNJ8j6LJO+zSdrzLpL2vFs4+tEcEp/3kPi8l8TnXOHo7/eJn/4eRLsy9wsHl+YJx/35AMn9+SDJ/TmfxOdDJD4XkPhcKBxcelg4+vsjJO25SDg4/yiJz8dIfC4Wjn70uHD0oydI8r6EJO9PkuT9KZK8LyXx+TSJz2eEox8tEz/9KIh2ZZ4l8bmcxOcK4eDnc8LR358Xjv6+kuT+fIHk/nxROPK+iiTvL5H4fJnk/lwtHPx8RTj60askeV9D0p5rhaO/v0bicx3J/fm6cHDpDRKf60l8vikcXHpLOPrRBpK8v02S93dI8r6RJO/vkvjcRHJ/bia5P98jac8tJO35vnD0o60kPj8g8fmhcPSjj8RPPwqiXZmPSXx+QuLzUxKfnwkH5z8XDi59QeLzSxKfXwkH578Wjv7+DYnPb0l8fkfi83vh4PwPwtHffyRpz59I2vNn4ehHv5Dk/VfhGN9/I7k/fyfJ+x8kef+TJO9/CQeX/ibx+Q+JTxTI4DOHxGe5HA5+ls/h4GcFEp8VSXxWIvFZmcRnFRKfVUl8ViPxWZ3EZw0SnzVJfNYi8VmbxGcdEp91SXzWI/FZn8RnAxKfDUl8NiLx2ZjEZxMSn01JfDYj8dmcxGcLEp8tPfkMol2ZViS/g/nyyZL3HaUfsXCJhfMs4ybLPIRlXscyT2ZZd7Cs41jWxSy/M7D8bsPyOxjL74osv9Oy/O7N8hyB5bkMy3MulueGLM9hWZ5rs7wnwPLeBct7LL7eCwqiXd7eswqiXTTvrbG8B8jyXiXLe6q+3vtleY+a5b30INpF856/r+8mWL5DCaJd3r7rCaJd3r6T2lG+O2P5jo/lu0hf35kG0S6a73a/JfHJ8l25r+/0WfY92FH2kWDZl8PXPidBtMvbvjFBtItmHx6WfY1Y9onyte8Wyz5mO8q+cFtJfL4vHJzfIhz9iGVfTZZ9Sn3t+xrVJ8s+ur72JQ6iXTT7PPvaNzuqT1/7kAfRLpp93X3tkx/VJ8u5AyznOPg6FyOIdnk7ZySIdtGc27JWOLjEcq4QyzlNvs69iurT1zliQbTL27lsQbSL5pw7X+cGRi2b5RxGX+daBtEub+eERi3b17mrUX36Osc2iHZ5Oxc4iHbRnLP8LInPZcLR332dqx7VJ8s59UtJfD4lHPx8Ujj60RKSvD9BkvfHSfK+mCTvj5H4fJTE5yLh6EePCEc/epikPRd6as8g2pVZQOLzIRKf80l8Pigc/f0B4eD8POHg0v0k9+d9JPfnXOG4P+8l8XkPic85JD7vFg4u3SUc/X02SXvOImnPmcLRj2aQ5P1OkrzfQdKe0z21ZxDtytxO4vM2kvtzmnDcn7eStOctwsH5qSQ+bybxeZNw9KMpwsHPG4Wjv98gHHmfTNKe15O053Uk7TlJOPh5LYnPa0h8TiTxeTWJz6uEg0sTxA+XgmhX5krh4OcVwnF/jifxeTmJz3EkPseS+BwjHPy8TDi4NJqkPS8VjvHoEpK8jxKOvF9MkveLSPI+UjjyfiFJ3i8gyfsI4cj7+STteZ5wzJeGk/g8l+T+PIfk/hxGkvezSXyeReJzKInPM4Wjv58hHP19CEl7nk7SnqcJRz8aTOKzlMTnIOHoRwPFTz8Kol2ZEhKfA4SDS/2F4/48lSTvp5DkvZ9w8PNkkvvzJJK89yVpzxNJ2vME4ehHfUh8Hk/i8zgSn71JfB5L4vMY4eBnL+HgZ0+S9jzaU3sG0a5MD5K8HyUc/f1IEp/dhaMfHSEc/ehw4ehH3YTj/jyM5P48lCTvXUnyfgiJz4NJfHYRjn50kHBwvjOJz07CwaUDheP+PICkPTsKB5f2J8n7fsLR34tJfBYJRz/qIBz9qFA4+lEByf2ZT+IzTzj6Ua5w9KOMcPSjgCTv+5LkfR8Sn+1J7s+9Se7PvUjy3o4k73sKx7i5B8n92VY47s/dSXzuRuKzDYnPXYWDS7sIB5daCweX3suxqvPg0lY5//VYzkV5FxVcVHRRyUVlF1VcVHVRzUV1FzVc1HRRy0VtF3Vc1HVRz0V9Fw1cNHTRyEVjF01cNHXRzEVzFy1ctHTRysVOLnZ2gbbHfYJ7Gv0PrADXwGCMFxjbMA5jzoD5DeZimDdijovGxtoB6xysybB+xFoX63L8hoDfO/DbDH5Hwm9e+H0OvyXid89tv9Hit2/8To9nCnj+gWc1eK6EZ2B4Xodni3gOime2eL6MZ+F4bo93DHq6wLsbeM8E78Tg/R28a4T3ovAOF943w7txeI8P7xzi/Ui8y4n3TvGObH8XA1yUuMA73Xj/HO/K471+fIOA7yXwbQe+Q8E3M/i+B98i4bspfON1jgt8O4fv/PBNIr6fxLee+C4V39Die198m4zvqPHNN75Px7f0+O4fexSMcTHWxTgX2FMD+39grxLsq4I9YLBfDfbWwT5A2LMI+ythLyjsW4U9tia7wN5l2GcNe8Jh/zrstYd9AbGHIfZbxN6Q2McSe25if1DsZYp9V7FH7EwXs1zMdoE9jbH/MvaKxr7W2IMb+4Vjb3Psw44947G/Pfbix7kBOONggQucHYFzLnAmB84PwVknOJcFZ8jgvBuczYNzhHDmEc5nwllSOPcKZ3Qtc/Gsi+UucKYczr/DWX04VxBnIOK8RpwtiXMwcWYnzhfFWag4txVnzK51gbN7cc4wzkTG+c04axrnYuMMb5w3jrPRcY47zpx/18UmF5tdvOdii4v3XWx18YGLD1185OJjF5+4+NTFZy4+d/GFiy9dfOXiaxffuPjWxXcuvnfxg4sfXfzk4mcXv7j41cVvLn538YeLP1385eJvF/+4QOfPcVHORXkXFVxUdFHJRWUXVVxUdVHNRXUXNVzUdFHLRW0XdVzUdVHPRX0XDVw0dNHIRWMXTVw0ddHMRXMXLVy0dLGNPVkL/15g238AmDD9ZWCnAgA=
H4sIAAAAAAAA/+2debRP5RrH32Oe53kWEZHf78wnMkVEREREOJwTEZF5nkVERESmKBERpZSIiIgoEZHcxntv89wd32/nZ2U/9/53nnev/V3t31rP4ltrvb7vfvb+7OfZw7svxhnzS07z+8/+1eSI/ZnvCp1D6JxC5xI6t9B5hM4rdD6h8wtdQOiCQhcSurDQRYQuKnQxoYsLXULokkKXErq00GWELit0OaHLC11B6IpCVxK6stBVhK4qdLWYRt5MTBvjzXeu2P/Pc0X+8sdyUzCWg8KxbV00tk2Lx7Zdydg2Kh3bFmVjcy4fm1vF2Bwqx7xWjXm4/O9Xj/39sr5K6BpC1xT6aqFrCV1b6GuEriN0XaGvFbqe0PWFvk7oBkJHhI4KHS90gtCJQicJnSx0itCpQqcJfb3QDYVuJPQNQjcWuonQTYVuJnRzoW8UuoXQLYW+SehWQrcW+mah2wjdVuhbhG4ndHuhbxW6g9Adhb5N6E5Cdxb6dqG7CN1V6DuE7iZ0d6HvFLqH0D2FvkvoXkL3FrqP0OlC9xW6n9AZQmcKfbfQ/YUeIPQ9Qg8UepDQ9wo9WOghQt8n9FChhwl9v9DDhR4h9EihRwk9WugxQo8VepzQ44WeIPREoScJPVnoKUJPFXqa0NOFniH0TKFnCf2A0LOFniP0g0LPFXqe0A8JPV/oBUI/LPRCoRcJ/YjQi4VeIvSjQi8VepnQjwm9XOgVQj8u9EqhVwm9Wug1Qq8V+gmh1wm9XugnhX5K6A1CPy30RqE3Cf2M0JuF3iL0s0JvFXqb0M8JvV3oHUI/L/QLQu8U+kWhXxJ6l9AvC/2K0LuFflXoPULvFfo1ofcJvV/o14U+IPRBod8Q+pDQh4V+U+gjQh8V+i2hjwl9XOi3hT4h9Emh3xH6XaFPCf2e0KeFPiP0+0KfFfqc0B8IfV7oC0J/KPRFoT8S+pLQfxH6Y6E/EfpToT8T+nOhvxD6r0L/Tei/C/2l0F8J/bXQ3wj9rdDfCf290D8I/aPQPwn9s9C/CP2r0L8J/Q+h/yn0v4T+t9D/ERp/uVLHCZ1D6JxC5xI6t9B5hM4rdD6h8wtdQOiCQhcSurDQRYQuKnQxoYsLXULokkKXErq00GWELit0OaHLC11B6IpCVxK6stBVYjp37L9hf8Cvusnq7dHPo4dH345eHf05enL04ei90W+jx0ZfjV4a/TN6ZvTJ6I3RD6MHRt+LXhf9LXpa9LHoXdGvokdFX4peFP1nU5PVZzY3Wf0kekj0jegV0R+iJ0QfiN4P/R56PPR16OXQv6FnQ5+G3gz9GHow9F3otdBfoadCH4XeCf0SeiT0ReiF0P/0Nll9TrrJ6mfQw6BvQa+C/gQ9CfoQ9B7oN9BjoK9AL4H+AT0D+gT0BugH0AOg7ketj/oeNT3qeNTuqNdRo6MuRy2O+nuyyaqzp5qseho1NOpm1Mqoj1ETow5G7Yt6FzUu6lrUsqhfUbOiTkVtinoUNSjqTtSaqC9RU6KORO2IehE1IupC1IKo/1abrDpvrcmq51DDoW5DrYb6DDUZ6jDUXqi3UGOhrkIthfoJNRPqJNRGqIdQA6HuQa2D+gY1DeoY1C6oV1CjoC5BLYL6Y6/JqjP2max6AjUE6gbUCqgPUBOgDsC5H+d7nONxXse5HOdvnLNxnsa5GedjnINx3sW5FudXnFNxHsW5E+dLnCNxXsS5EOe/iybrPHfJZJ3PcA7DeQvnKpyfcE7CeQjnHpxvcI7BeQXnEpw/cM7AeQLnBpwPcA4A98F68B1MB8fBbvAajAaXceyBv78zNy6LreApGApugpXgI5gIDoJ94B0YB66BZeAXmAVOgU3gERgE7oA14AuYAo6AHeAFGAEugAVX/nLE/mwa+zMhkpyYmJESnxFNiPaJxKelpyZFEpPSk1OjqdGk1KR+8akJCRmpiakpaelpKZG0aGJCRjQzKS0hM5L1i1Mcq2rcH2NFsvVLiOTM2uT/84sT849k7xfV85y1LS//ql0hconc4Re7pfD79WLtORnx78jtWOT//DfVf9xFkqrF6Y9bPU5v53c17+px6jmKmCt+Qd+ml3/a4MuhONZVahBJTvQLfHqeveCrEYJPN0k1HICvZsDBh3nXJANfTRLw5VQc62o1iCRm+AU+Pc9e8NUKwaebpFoOwFc74ODDvGuTga82CfhyKY51jRpEUuL9Ap+eZy/46oTg001SHQfgqxtw8GHedcnAV5cEfLkVx7pWDSIZUb/Ap+fZC756Ifh0k1TPAfjqBxx8mHd9MvDVJwFfHsWxrtO7ueEb+PQ8e8HXIASfbpIaOABfJODgw7wjZOCLkIAvr+JYUTWI9PHtrq6eZy/44kPw6SYp3gH4EgIOPsw7gQx8CSTgy6c4VqIaROLT/AKfnmcv+JJC8OkmKckB+JIDDj7MO5kMfMkk4MuvOFaKGkTSU/0Cn55nL/hSQ/DpJinVAfjSAg4+zDuNDHxpJOAroDjW9WoQSfKt1dXz7AVfwxB8uklq6AB8jQIOPsy7ERn4GpGAr6DiWDeoQSQxyS/w6Xn2gq9xCD7dJDV2AL4mAQcf5t2EDHxNSMBXSHGspnqtbrJf4NPz7AVfsxB8uklq5gB8zQMOPsy7ORn4mpOAr7DiWDeqQSTVt8dZ9Dx7wdciBJ9uklo4AF/LgIMP825JBr6WJOArojjWTYTg0/PsBV+rEHy6SWrlAHytAw4+zLs1Gfhak4CvqOJYN+vd3PDtrq6eZy/42oTg001SGwfgaxtw8GHebcnA15YEfMUUx7pFD3z9/AKfnmcv+NqF4NNNUjsH4GsfcPBh3u3JwNeeBHzFFce6VQ0i8b5VfHqeveDrEIJPN0kdHICvY8DBh3l3JANfRxLwlVAc6zY1iCQk+AU+Pc9e8HUKwaebpE4OwNc54ODDvDuTga8zCfhKKo51uxpEMnyr+PQ8e8HXJQSfbpK6OABf14CDD/PuSga+riTgK6U41h1qEEn0DXx6nr3g6xaCTzdJ3RyAr3vAwYd5dycDX3cS8JVWHOtONYik+LZIgZ5nL/h6hODTTVIPB+DrGXDwYd49ycDXkwR8ZRTHuksNIum+gU/Psxd8vULw6SaplwPw9Q44+DDv3mTg600CvrKKY/XRq/h8W6RAz7MXfOkh+HSTlO4AfH0DDj7Muy8Z+PqSgK+c4lj91CCS5tubG3qeveDLCMGnm6QMB+DLDDj4MO9MMvBlkoCvvOJYd+vd3PDtcRY9z17w9Q/Bp5uk/g7ANyDg4MO8B5CBbwAJ+CoojnWPGkT8+9iQnmcv+AaG4NNN0kAH4BsUcPBh3oPIwDeIBHwVFce6Vw0imb6tx6fn2Qu+wSH4dJM02AH4hgQcfJj3EDLwDSEBXyXFse7Tu8bnW6ur59kLvqEh+HSTNNQB+IYFHHyY9zAy8A0jAV9lxbHu16v4fLurq+fZC77hIfh0kzTcAfhGBBx8mPcIMvCNIAFfFcWxRipCxC/wjXQEvlEh+HSTNMoB+EYHHHyY92gy8I0mAV9VxbHGEIJvjCPwjQ3Bp5uksQ7ANy7g4MO8x5GBbxwJ+KopjjVeDyK+3dUd7wh8E0Lw6SZpggPwTQw4+DDviWTgm/gnBN8kQvBNcgS+ySH4dJM02QH4pgQcfJj3FDLwTSEBn2arO5Ww1Z3qCHzTQvDpJmmaA/BNDzj4MO/pZOCbTgI+zZsbMwjBN8MR+GaG4NNN0kwH4JsVcPBh3rPIwDeLBHyaj7M8oAYR/x5n0fPsBd/sEHy6SZrtAHxzAg4+zHsOGfjmkIBP8wHmB9Ug4t8DzHqeveCbG4JPN0lzHYBvXsDBh3nPIwPfPBLwab6y9pBexefbK2t6nr3gmx+CTzdJ8x2Ab0HAwYd5LyAD3wIS8GkuUvCwGkT8W6RAz7MXfAtD8OkmaaED8C0KOPgw70Vk4FtEAj7NZakeUYOIf8tS6Xn2gm9xCD7dJC12AL4lAQcf5r2EDHxLSMCnuRDpo3rX+Hyr+PQ8e8G3NASfbpKWOgDfsoCDD/NeRga+ZSTg01x6/jE1iPi39LyeZy/4lofg003ScgfgWxFw8GHeK8jAt4IEfJofG3pcDSL+fWxIz7MXfCtD8OkmaaUD8K0KOPgw71Vk4FtFAj7Nz0uu1qv4fAOfnmcv+NaE4NNN0hoH4FsbcPBh3mvJwLeWBHyaHxR/Qu/mhm8fFNfz7AXfuhB8ukla5wB86wMOPsx7PRn41pOAr6TiWE+qQSTDN/DpefaC76kQfLpJesoB+DYEHHyY9wYy8G0gAV8JxbGeVoNIgm+Ps+h59oJvYwg+3SRtdAC+TQEHH+a9iQx8m0jAV1xxrGfUIBLvW8Wn59kLvs0h+HSTtNkB+LYEHHyY9xYy8G0hAV8xxbGeVYNIUj+/wKfn2Qu+rSH4dJO01QH4tgUcfJj3NjLwbSMBX1HFsZ7TA59vFZ+eZy/4tofg003Sdgfg2xFw8GHeO8jAt4MEfEUUx3peDSKpvr25oefZC74XQvDpJukFB+DbGXDwYd47ycC3kwR8hRXHepEQfHqeveB7KQSfbpJecgC+XQEHH+a9iwx8u0jAV0hxrJfVIJKe7Bf49Dx7wfdKCD7dJL3iAHy7Aw4+zHs3Gfh2k4CvoOJYr6pBJNG39fj0PHvBtycEn26S9jgA396Agw/z3ksGvr0k4CugONZrejc3fFukQM+zF3z7QvDpJmmfA/DtDzj4MO/9ZODbTwK+/Ipjva7X6vp2V1fPsxd8B0Lw6SbpgAPwHQw4+DDvg2TgO0gCvnyKY72hBpF43xYp0PPsBd+hEHy6STrkAHyHAw4+zPswGfgOk4Avr+JYb6pBpI9vra6eZy/4joTg003SEQfgOxpw8GHeR8nAd5QEfHkUx3pLDSIJvj3OoufZC75jIfh0k3TMAfiOBxx8mPdxMvAdJwFfbsWx3laDiH8fG9Lz7AXfiRB8ukk64QB8JwMOPsz7JBn4TpKAL5fiWO+oQSQl3i/w6Xn2gu/dEHy6SXrXAfhOBRx8mPcpMvCdIgFfTsWx3lODSGKGX+DT8+wF3+kQfLpJOu0AfGcCDj7M+wwZ+M6QgC+H4ljvq0EkOdEv8Ol59oLvbAg+3SSddQC+cwEHH+Z9jgx850jAF6c41gd6Nzd8u6ur59kLvvMh+HSTdN4B+C4EHHyY9wUy8F1wBD5tn9UNh8+rfPKZ3bFrGH/2z+z6rEni82oSn7VIfNY2HPy8xnBwqY7h4FJdw7F/Xkuyf9YjyXt9krxfR+KzAcn+GSHZP6MkeY8nyXuC4ThvJpL4TDIcx1Gy4TiOUgzHcZRKsn+mkfi83nAcRw0Nx3HUyHAcRzeQ5L0xyfZsYjiO96YkPpuR7J/NDQeXbiTx2YLEZ0vDwaWbDMdx1Iok761J8n6z4eB8G5L9s63h2D9vIfHZznAcR+0Nx3F0q+E4jjoYjrx3JNmetxmO470Tic/OJD5vJ/HZhcRnVxKfdxgOfnYzHPzsTrI97yTZnj0Mx3HUkyTvd/mU90j2ftFeJPtnb8OR9z4keU8n8dmXZP/sZzj4mUHiM5PE592Gg0v9DcdxNIBke95Dsj0HGo7jaBCJz3tJfA4m8TnEcBzv9xmO430oSd6Hkfi8n2T/HE6yf44g2Z4jfdqekez9oqNI8j7acOR9DEnex5LkfZzhyPt4krxPIMn7RMOR90kk23Oy4aiXppD4nEricxqJz+kkPmcYDi7NNBzno1mGg58PGI79czaJzzkkPh8k8TmXxOc8w8HPhwwHl+aTbM8FJNvzYZLtudCn7RnJ3i+6iCTvjxgOfi4m8bmExOejhuN4X2o4jqNlJNvzMcPBz+UkPleQ7J+PG479cyXJ9lxlODi/miTva0jyvpZkez5Bsj3XGY7jaD2JzydJfD5F4nOD4Tjenzb+HO+R7P2iGw0HlzYZjv3zGZL9czPJ/rmFxOezJD63kvjcZji49JzhON63k2zPHYaD88+T+HyBxOdOw3EcvWg4jqOXSPK+iyTvL5Pk/RWSvO8m8fkqic89huM42mv8OY4i2ftFXyPxuY/E537Dwc/XDcfxfsBwHO8HSfbPN0j2z0OGI++HSfL+JonPIyT751HDwc+3DMdxdIwk78dJtufbhuN4P0Hi8yTJ/vmO4eDSuyQ+T5H4fM9wcOm04TiOzpDk/X2SvJ8lyfs5krx/QOLzPMn+eYFk//yQZHteJNmeHxmO4+gSic+/kPj82HAcR58Yf46jSPZ+0U9JfH5G4vNzEp9fGA7O/9VwcOlvJD7/TuLzS8PB+a8Mx/H+NYnPb0h8fkvi8zvDwfnvDcfx/gPJ9vyRZHv+ZDiOo59J8v6L4Ti//0qyf/5Gkvd/kOT9nyR5/5fh4NK/SXz+h8QnBmTwGUfiM0ccBz9zxnHwMxeJz9wkPvOQ+MxL4jMfic/8JD4LkPgsSOKzEInPwiQ+i5D4LErisxiJz+IkPkuQ+CxJ4rMUic/SJD7LkPgsS+KzHInP8iQ+K5D4rEjisxKJz8o++Yxk7xetQnJ9qXK4f6r6ZDneWfjJcj5iOb+z1Ess9SdLPc/SH7H0myz9O8v1EJbrSyzX61iuf7JcT2a5Ps9yv4Pl/hHL/TiW+5ss94tZ7r+zPM/A8nwIy/M2fj2v+Gd5/vNXEp8sz1H/SOLzexKfX5L4ZHmPj+W9SJb3TD8m8cmynsAlEp8fkfj8kMTneRKfLOsFsay/9D6JT5Z1zN4j8cmyHiDL+oos61UeJ/H5FolPlvWTD5H4PEDik+W7A3tIfLJ8t4XlOzgs3xXaReKT5ftcO0l8snznjuW7gSzfYXyOxOczJD5ZvrO8gcQny3fVWb5Tv57E5zoSn2tJfK4m8bmKxOfjJD6Xkfh8lMTnEhKfi0l8PkLi82ESn/NJfM4j8TmXxOeDJD7nkPicTeLzARKfM0h8TifxOY3E51QSn1NIfE4m8TmRxOc4Ep+jSXyOIPF5P4nPYSQ+h5L4HELiczCJz3tJfA4i8TmQxOcAEp93k/jMJPGZQeKzH4nP3iQ+e5L47EHiszuJzztIfHYl8dmFxOftJD47k/jsROLzNhKfHUh8tiPxeQuJz7YkPluT+GxF4rMlic8WJD5vJPHZnMRnYxKfjUh8NiTxmULiM5nEZzyJzyiJzwYkPq8j8VmfxOe1JD7rkvisTeKzFonPq0l81iTxWYPE54dxWj4zM6rE/eExh42cNnLZyG0jj428NvLZyG+jgI2CNgrZKGyjiI2iNorZKG6jhI2SNkrZKG2jjI2yNsrZKG+jgo2KNirZqGyjio2qNqrZqG7jKhvIAfYX7Ns4DsGMa2zUsQHOgcn1bOAcgvMdzs3Y2KglUPck2Ei0kWQD9Rpqy1QbaTaut4GaGPX7DTbQbzSJ5aWZDfRJ6OnQf6JXvskGentch7jZRhsbuHaC6zy4JtXexq02cB2tow1c98M1SlxPxbVfXKfGNXVc/+9mA/cr7rSB+yu4F3SXjV42etvoYyPdRl8buO+Ge4S4n4l7r/1t4F7xPTZwbxv34fHMAJ5vwLMY99nAsyN4zgXP5Ay3gWeIRtoYZQPPPY2xMdYGntUab2OCDTxfNsnGZBtTbEy1gWci8fwmnjWdaWOWDTwfi2d58dwxnpHG89x49vwhG3hWfoENPNu/0MYiG3gfAe9O4D0PvJOy1AbeoXnMxnIbK2zg3Z+VNvCu0moba2ystfGEDby3hnfs8D4g3l3Ee5ZP29hoA++G4j3WzTa22HjWxlYb22zgPdztNvDeMN5xxvvYeHf8RRt41x3v5b9sA+sIYM0DrM+AtST22njNxj4b+21gHQys2XHQxhs2sM7IYRtv2jhiA+ujYC2XYzaw9szbNk7YOGkDa+ZgfR+sRYR1k07bwDpPWJPqrA2soYX1vrA22QUbWEvtoo2PbFyygTX1sP7fJzY+tfGZjc9tfGED6xdirUWsC4k1LL+y8bWNb2x8a+M7G1iD8wcbWDP0Jxs/28A6p1iT9TcbWEMW693i2/f4rjy+2Y6DH98ax3e8sWYv1hfGWshYtxlrTGM9bKzdjXXGsSY61m/HWvNYFx9r+ON7A/g2Ar7jgG9O4PsY+JYHvjuCb6Tgey749gy+k4Nv+uD7Q/hW0mX2xCz8/gPb/gsgcVZIGGUCAA==
62 changes: 62 additions & 0 deletions crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs
Original file line number Diff line number Diff line change
Expand Up @@ -153,6 +153,65 @@ impl AcirContext {
self.add_data(var_data)
}

fn mark_variables_equivalent(
&mut self,
lhs: AcirVar,
rhs: AcirVar,
) -> Result<(), InternalError> {
if lhs == rhs {
return Ok(());
}

let lhs_data = self.vars.remove(&lhs).ok_or_else(|| InternalError::UndeclaredAcirVar {
call_stack: self.get_call_stack(),
})?;
let rhs_data = self.vars.remove(&rhs).ok_or_else(|| InternalError::UndeclaredAcirVar {
call_stack: self.get_call_stack(),
})?;

let (new_lhs_data, new_rhs_data) = match (lhs_data, rhs_data) {
// Always prefer a constant variable.
(constant @ AcirVarData::Const(_), _) | (_, constant @ AcirVarData::Const(_)) => {
(constant.clone(), constant)
}

// Replace any expressions with witnesses.
(witness @ AcirVarData::Witness(_), AcirVarData::Expr(_))
| (AcirVarData::Expr(_), witness @ AcirVarData::Witness(_)) => {
(witness.clone(), witness)
}

// If both variables are witnesses then use the smaller of the two in future.
(AcirVarData::Witness(lhs_witness), AcirVarData::Witness(rhs_witness)) => {
let witness = AcirVarData::Witness(std::cmp::min(lhs_witness, rhs_witness));
(witness.clone(), witness)
}

(AcirVarData::Expr(lhs_expr), AcirVarData::Expr(rhs_expr)) => {
if lhs_expr.is_linear() && rhs_expr.is_linear() {
// If both expressions are linear, choose the one with the fewest terms
TomAFrench marked this conversation as resolved.
Show resolved Hide resolved
let expr = if lhs_expr.linear_combinations.len()
<= rhs_expr.linear_combinations.len()
{
lhs_expr
} else {
rhs_expr
};

let expr = AcirVarData::Expr(expr);
(expr.clone(), expr)
} else {
(AcirVarData::Expr(lhs_expr), AcirVarData::Expr(rhs_expr))
}
}
};

self.vars.insert(lhs, new_lhs_data);
self.vars.insert(rhs, new_rhs_data);

Ok(())
}

pub(crate) fn get_call_stack(&self) -> CallStack {
self.acir_ir.call_stack.clone()
}
Expand Down Expand Up @@ -345,6 +404,7 @@ impl AcirContext {
if diff_expr.is_const() {
if diff_expr.is_zero() {
// Constraint is always true - assertion is unnecessary.
self.mark_variables_equivalent(lhs, rhs)?;
return Ok(());
} else {
// Constraint is always false - this program is unprovable.
Expand All @@ -357,6 +417,8 @@ impl AcirContext {
}

self.acir_ir.assert_is_zero(diff_expr);
self.mark_variables_equivalent(lhs, rhs)?;

Ok(())
}

Expand Down