Paper 2023/778

Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)

Alex Ozdemir, Stanford University
Riad S. Wahby, Carnegie Mellon University
Fraser Brown, Carnegie Mellon University
Clark Barrett, Stanford University

Zero Knowledge Proofs (ZKPs) are cryptographic protocols by which a prover convinces a verifier of the truth of a statement with- out revealing any other information. Typically, statements are expressed in a high-level language and then compiled to a low-level representation on which the ZKP operates. Thus, a bug in a ZKP compiler can com- promise the statement that the ZK proof is supposed to establish. This paper takes a step towards ZKP compiler correctness by partially veri- fying a field-blasting compiler pass, a pass that translates Boolean and bit-vector logic into equivalent operations in a finite field. First, we define correctness for field-blasters and ZKP compilers more generally. Next, we describe the specific field-blaster using a set of encoding rules and de- fine verification conditions for individual rules. Finally, we connect the rules and the correctness definition by showing that if our verification conditions hold, the field-blaster is correct. We have implemented our approach in the CirC ZKP compiler and have proved bounded versions of the corresponding verification conditions. We show that our partially verified field-blaster does not hurt the performance of the compiler or its output; we also report on four bugs uncovered during verification.

Available format(s)
Publication info
Published elsewhere. CAV'23
zero knowledgecompilersverificationfinite fields
Contact author(s)
aozdemir @ cs stanford edu
2023-05-30: revised
2023-05-27: received
See all versions
Short URL
Creative Commons Attribution


      author = {Alex Ozdemir and Riad S. Wahby and Fraser Brown and Clark Barrett},
      title = {Bounded Verification for Finite-Field-Blasting (In a Compiler for Zero Knowledge Proofs)},
      howpublished = {Cryptology ePrint Archive, Paper 2023/778},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.