Quantstamp: Linting Halo2 Circuits

Various tools (Ecne, Picus) exist for sanity checking various ZK proof system circuits. However, this work is limited to R1CS analysis and is therefore not suitable for use with proof systems with Plonkish arithmetic. We describe a modification to the Halo2 proof codebase that enables constraints for Halo2 gates to be sanity checked. We outline a proof of concept where real (erroneous) circuits are found to be under-constrained in the sense that they have two satisfying assignments. These satisfying assignments are found via an SMT solver connected directly to the Halo2 codebase. This is the first work we are aware of that applies lightweight formal methods to the Halo2 codebase. We conclude by outlining future directions for the project. with Jan Gorzny Fatemeh Heidari Mohsen Ahmadvand Mohammad Jahanara Jeffrey Kam Matthias Hall-Andersen