CirC: Unifying Compilers for SNARKs, SMT, and More [Oakland'22]


Alex Ozdemir


Henry Corrigan-Gibbs
We present CirC ("SIR-see"): a compiler infrastructure that aims to support
zero-knowledge proof systems, multi-party computations, fully homomorphic
encryption, constraint solving, and optimization. We observe that these
seemingly disparate cryptosystems and verification problems share a common
model of computation. This model is characterized by being state-free,
non-uniform, and non-deterministic---we call it the *existentially quantified
circuit (EQC)*. The common model admits a shared compiler infrastructure
(CirC) for compiling different high-level languages to different circuit
representations used by these systems.

We show:
(1) CirC makes it easy to build new compilers for these systems
* e.g., we reproduce and improve on a 28k LOC compiler in 700 LOC.
(2) CirC's compilers perform well (by leveraging shared optimizations)
(3) CirC enables "cross-overs" in which different back-end systems are
combined in the service of a shared optimization
* SMT+ZKP = zero-knowledge bug bounties
* SMT+X = SMT assisted optimization