Skip to content
/ circ Public

(Cir)cuit (C)ompiler. Compiling high-level languages to circuits for SMT, zero-knowledge proofs, and more.

License

Unknown and 2 other licenses found

Licenses found

Unknown
COPYING
Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT
Notifications You must be signed in to change notification settings

circify/circ

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

About

(Cir)cuit (C)ompiler. Compiling high-level languages to circuits for SMT, zero-knowledge proofs, and more.

Resources

License

Unknown and 2 other licenses found

Licenses found

Unknown
COPYING
Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published