CirC: The Circuit Compiler

CirC is a compiler infrastructure which supports compilation from high-level (stateful, uniform) languages to (state-free, non-uniform, existentially quantified) circuits.

It's been used to compile {C, ZoKrates} to {SMT, ILP, R1CS, MPC}, but it probably also applies to any statically type high-level language and constant-time/FHE.

If you want to learn more about CirC, see our paper or slides.

This is the second implementation of CirC. The first was done in Haskell and can be found here.

Requirements

Developing CirC requires the CVC4 SMT solver, which is used in some tests. Its binary must be on your path. On Arch Linux and Ubuntu you can install the cvc4 package from official repositories.

You'll also need the COIN-OR CBC solver. On Arch linux, this is coin-or-cbc. On Ubuntu coinor-cbc and coinor-libcbc-dev.

You'll also need a stable Rust compiler.

Quickstart

For an example of doing ZKP compilation, look here.

Architecture

• Components:
  • src/ir
    • IR term definition
      • term/bv.rs: bit-vec literals
      • term/field.rs: prime-field literals
      • term/ty.rs: type-checking
      • term/extras.rs: algorithms: substitutions, etc.
    • Optimization
      • opt/cfold.rs: constant folding
      • opt/flat.rs: n-ary flattening
      • opt/inline.rs: inlining
      • opt/sha.rs: replacements for SHA's CH and MAJ operations
      • opt/tuple.rs: eliminating tuples
      • opt/mem/obliv.rs: oblivious array elimination
      • opt/mem/lin.rs: linear-scan array elimination
      • opt/mem/visit.rs: utility for visiting (and replacing?) all array-related terms
  • src/target
    • R1CS backend
      • lowering from IR
      • optimization
      • connection to bellman
    • SMT backend
      • based on rsmt2
  • src/circify
    • Machinery for recursive imports
    • mem: the stack memory module
    • mod: the main Circify interface
  • src/front
    • zokrates: the ZoKrates front-end
  • src/util
    • A once-queue (each item appears at most once)
      • Implemented by combining a set with a queue
    • hash-consing machinery
  • examples/circ.rs
    • This is the entry point to the zokrates copiler

Backends

SMT

The SMT backend can be changed between CVC4 and cvc5 by setting the RSMT2_CVC4_CMD environmental variable to the SMT solver's invocation command (cvc4 or cvc5).