CoBBL: Dynamic Constraint Generation for SNARKs

General-purpose probabilistic proof systems operate on programs expressed as systems of arithmetic constraints-an unfriendly representation. There are two broad approaches in the literature to turning friendlier, high-level programs into constraints suitable for proof systems: direct translation and CPU emulation. Direct translators compile a program into highly optimized constraints; unfortunately, this process requires expressing all possible paths through the program, which results in compile times that scale with the program's runtime rather than its size. In addition, the prover must pay the cost of every possible program path, even those untaken by a given input. In contrast, CPU emulators don't compile programs to constraints; instead, they “execute” those programs, expressed as CPU instructions, on a CPU emulator that is itself expressed as constraints. As a result, this approach can't perform powerful, program-specific optimizations, and may require thousands of constraints where direct translation could use a clever handful. Worse, CPU emulators inherit an impractically expensive program state representation from the CPUs they emulate. This paper presents a compiler and proof system, CoBBL, that combines the benefits of CPU emulation and direct translation: it takes advantage of program-specific optimizations, but doesn't pay for an unnecessary state representation or unexecuted computation. CoBBL outperforms CirC, a state-of-the-art direct translator, by 1-30× on compile time and 26–350 ×on prover time, and outperforms Jolt, a state-of-the-art CPU emulator, on prover time by 1.1-1.8× on Jolt-friendly benchmarks, and up to 100× on other benchmarks.