Home

Awesome

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, Circom} 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.

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.

Architecture

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).