Cryptology ePrint Archive: Report 2020/1586

Unifying Compilers for SNARKs, SMT, and More

Alex Ozdemir and Fraser Brown and Riad S. Wahby

Abstract: The programming languages community, the cryptography community, and others rely on translating programs in high-level source languages (e.g., C) to logical constraint representations. Unfortunately, building compilers for this task is difficult and time consuming. In this work, we show that all of these communities can build upon a shared compiler infrastructure, because they all share a common abstraction: stateless, non-deterministic computations that we call existentially quantified circuits, or EQCs.

To make our approach concrete we create CirC, an infrastructure for building compilers to EQCs. CirC makes it easy to add support for new EQCs: we build support for two, one used by the PL community and one used by the cryptography community, in $\approx$2000 LOC. It’s also easy to extend CirC to support new source languages: we build a feature complete compiler for a cryptographic language in one week and $\approx$700 LOC, whereas the reference compiler for the same language took years to write, comprises $\approx$24000 LOC, and produces worse-performing output than our compiler. Finally, CirC enables novel applications that combine multiple EQCs. For example, we build the first pipeline that (1) automatically identifies bugs in programs, then (2) automatically constructs cryptographic proofs of the bugs' existence.

Category / Keywords: implementation / zero knowledge, implementation

Date: received 18 Dec 2020, last revised 18 Feb 2021

Contact author: aozdemir at cs stanford edu

Available format(s): PDF | BibTeX Citation

Note: Update boolector citation.

Version: 20210218:183528 (All versions of this report)

Short URL: ia.cr/2020/1586