Field Emulation Proofs

Check out the below repository! It contains Z3 proofs (i.e. formal, machine-checkable mathematical proofs) that ZK arithmetizations emulating cryptographically-sized finite field operations are sound. This means that, any solution to the constraints, corresponds to a valid “bigfield” operation.

https://github.com/VeridiseAuditing/field-emulation-proofs

I worked on this during an audit of Aztec bigfield circuits. These files have since been back-contributed to Aztec (see https://github.com/AztecProtocol/aztec-packages/pull/17152), although the Veridise repository is maintained separately in case there are any future additions.