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
- Components:
src/ir
- IR term definition
term/bv.rs
: bit-vec literalsterm/field.rs
: prime-field literalsterm/ty.rs
: type-checkingterm/extras.rs
: algorithms: substitutions, etc.
- Optimization
opt/cfold.rs
: constant foldingopt/flat.rs
: n-ary flatteningopt/inline.rs
: inliningopt/sha.rs
: replacements for SHA's CH and MAJ operationsopt/tuple.rs
: eliminating tuplesopt/mem/obliv.rs
: oblivious array eliminationopt/mem/lin.rs
: linear-scan array eliminationopt/mem/visit.rs
: utility for visiting (and replacing?) all array-related terms
- IR term definition
src/target
- R1CS backend
- lowering from IR
- optimization
- connection to bellman
- SMT backend
- based on rsmt2
- R1CS backend
src/circify
- Machinery for recursive imports
mem
: the stack memory modulemod
: 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
- A once-queue (each item appears at most once)
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
).