Abstract Interpretation for PLONKish Circuits
Fatemeh Heidari Soureshjani, Jan Gorzny · 2024
Zero-knowledge proof systems are becoming powerful tools in domains like blockchain networks. In this work, we improve abstract interpretation methods to sanity check PLONKish arithmetizations of computation, such as those used in the Halo2 zero-knowledge proof system. Our work aims to improve the accuracy of checks for unused gates, assigned but unconstrained values, and possibly under-constrained circuits, all of which may indicate a bug in the circuits. We show how copy constraints and arbitrary lookup functions can be used in abstract interpretation based analysis of these circuits. We are motivated to revisit this topic as these circuits, through their use in general purpose blockchain networks, may be responsible for the security of millions of dollars in cryptocurrency.