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 all 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 @@
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.
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 @@
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 @@
}

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

Ok(())
}

Expand Down Expand Up @@ -514,7 +576,7 @@
/// Returns the quotient and remainder such that lhs = rhs * quotient + remainder
/// and |remainder| < |rhs|
/// and remainder has the same sign than lhs
/// Note that this is not the euclidian division, where we have instead remainder < |rhs|

Check warning on line 579 in crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs

View workflow job for this annotation

GitHub Actions / Spellcheck / Spellcheck

Unknown word (euclidian)
fn signed_division_var(
&mut self,
lhs: AcirVar,
Expand Down Expand Up @@ -599,7 +661,7 @@
}

/// Returns an `AcirVar` which will be constrained to be lhs mod 2^{rhs}
/// In order to do this, we simply perform euclidian division of lhs by 2^{rhs}

Check warning on line 664 in crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs

View workflow job for this annotation

GitHub Actions / Spellcheck / Spellcheck

Unknown word (euclidian)
/// The remainder of the division is then lhs mod 2^{rhs}
pub(crate) fn truncate_var(
&mut self,
Expand Down Expand Up @@ -933,7 +995,7 @@
}

/// Recursively create acir values for returned arrays. This is necessary because a brillig returned array can have nested arrays as elements.
/// A singular array of witnesses is collected for a top level array, by deflattening the assigned witnesses at each level.

Check warning on line 998 in crates/noirc_evaluator/src/ssa/acir_gen/acir_ir/acir_variable.rs

View workflow job for this annotation

GitHub Actions / Spellcheck / Spellcheck

Unknown word (deflattening)
fn brillig_array_output(
&mut self,
element_types: &[AcirType],
Expand Down