0b42f26089
In *non-recursive* type-checking, perhaps better called *type computing* we perform a minimal traversal in order to compute the type of a term, without recursively type-checking it. Informally, we assume it is well typed, and do the minimal amount of work needed to compute its type. Two improvements: 1. No longer implemented with recursion. 2. Caches all intermediate results. Implementation: * `check_dependencies(Term) -> Vec<Term>`: maps a terms to the immediate children of it whose types are needed to compute its type. * `check_raw_step(Term, TypeTable) -> Sort`: assumes those children have their types in the table, and computes this term's type. * `check_raw`: glues the two above functions together into a suitable traversal. Similar to `rec_check_raw`, but the traversal isn't total. Significance: Previously, we had a non-recursive implementation for array stores that *didn't cache intermediate results* which could cause quadratic type-checking time (if the type-check callee was doing a top-down traversal). Edward sent me a benchmark that was experiencing this, resulting in 74.1% of total compilation time being spent type-checking. Now it's down to 0.4% of total compilation time.
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).