Analysis of polynomial equality constraint systems for ZK-protocols

Abstract

Zero Knowledge (ZK) proofs are protocols with growing applications in fields such as cryptography. They can be particularly difficult to design and thus have multiple domain-specific languages (DSLs) to aid a programmer in their construction. Analysis methods for these protocols are then typically language-specific, greatly limiting their utility. Most languages compile user code into a midpoint polynomial-circuit called a rank one constraint system (R1CS). We provide tools to analyse these R1CS circuits which hence have much broader applicability than existing tools. Specifically, we design and implement a tool for equivalence up to renaming and scaling, useful to avoid repeating a laborious step of the ZK process. As implemented, the tool can handle circuits on the order of millions of constraints. Additionally, we provide methods to extract a directed acyclic hierarchical structure via clustering to guide an automated property prover with recursive proving. Such a structure typically exists in DSL code but is lost when compiled to R1CS and is required to make larger circuits feasible to pass to a property prover. The guidance given by our clustering methods to the property prover Civer gave comparable results to the guidance of the original structure present in the code and finished in faster time.