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

#### Speaker

Alex Ozdemir

#### Host

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

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