50b97f6acb
This PR does two things: - Fixes some scoping issues in Z# having to do with the context in which function and struct definitions are interpreted. - Improves speed and reduces TermTable memory consumption by 2x (by keying on Arc<TermData> rather than TermData) - Improves speed for Z# array handling with a BTreeMap -> HashMap swap - Adds intrinsic widening casts in Z#. These were previously handled by bit-splitting, which is wasteful. On array-heavy Z# programs, this PR improves speed by about 5x and memory consumption by roughly the same. --- * zsharp::term::ir_array should use HashMap (faster, less memory) * perf improvements constant folding: get rid of redundant clones bitvector: impl arith for refs TermTable: don't store redundant term as key * EMBED widening casts * generic inf: need to push fn defn context onto filestack * canonicalize path in err msg * need struct defn on filestack, too * no need to warn about U32 indexing in zsharp * fix warning
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/frontzokrates: 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).