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