Alex Ozdemir
February 11, 2021 at 11:00 AM on Zoom / Soda Hall
CirC: Unifying Compilers for SNARKs, SMT, and More
Abstract: We present CirC (“SIR-see”): a compiler infrastructure that aims to supportzero-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 * ... This is joint work with Fraser Brown and Riad S. Wahby.
Bio: Alex Ozdemir is a Phd student at Stanford, studying cryptography and formalmethods. Lately, he’s been investigating how cryptographic proof systems can be made more useful, sometimes by using techniques from formal methods and programming languages.