This allows folks to use the RAM machinery while sticking with (non-interactive) R1CS output.
We're going to need this anyway when we benchmark our new approach.
* Improve the oblivious RAM pass by killing the hack where we treat selects as arrays.
* Fix a bug where the volatile RAM pass would not place selects before stores against the same array
* Improve that volatile RAM pass by placing selects against the same array literal in the same RAM. Before, they would each end up in different RAMs, which sucks. This is especially bad for ROMs.
Previously, a GC call would scan the HC table, identifying dead nodes.
Now, whenever a Node is destroyed, if it's ready to be GC'd, it gets added to a list. That list is used at GC time instead of the scan.
This substantially decreases the cost of running GC many times (as the Z# FE does).
* r1cs: fix boolean majority
for m = majority(a,b,c),
we were lowering
(-ab + bc + ac - 2abc)
instead of
(ab + bc + ac - 2abc)
Whoops! This is a functional correctness bug: we were lowering
soundly and completely, for the wrong specification.
Credit to Anna for raising the issue!
* add test_sha256 (commented out b/c it is slow)
* fmt + lint
To reduce CI build time:
- Replaced ABY dependency with corresponding binary.
- Removed dependencies on KaHIP and KaHyPar for now because these dependencies aren't used upstream.
Minor updates:
- Updated ABY source to Public branch
Note:
- The aby_interpreter binary will only work on Linux. We can rebuild the binary from this repo.
A basic implementation of committed witnesses & volatile RAM extraction in the Z# front-end.
The passes in question are still a bit brittle, so I left them behind a flag.
- Upgraded ci pipeline to [v3](https://github.com/actions/cache/blob/main/README.md)
- Included installation and build scripts for KaHIP and kahypar in driver.py
- Used absolute paths for caching in ci pipeline (relative paths don't work).
Average ci time brought down from 15 minutes to 8 minutes!
Adds:
an implementation of the Mirage proof system
generalized to multiple round of interaction
a notion of rounds for variables
a notion of randomness for variables
to the R1CS layer:
committed witnesses
rounds
new witness computation machinery (to support multiple rounds)
Before, whenever we constructed a bit-wise encoding of a BV, we also
debitified it into a UINT encoding.
Now, we do the debitification on-demand. This saves ~10-15% of compilation
time.
While debitification is free from the perspective of R1CS, it is costly
for compilation time.
I measured compile time for the sha2 round function.
```terminal
Benchmark #1: ./circ-old third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs
Time (mean ± σ): 1.219 s ± 0.019 s [User: 1.145 s, System: 0.071 s]
Range (min … max): 1.180 s … 1.240 s 10 runs
Benchmark #2: ./circ-new third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs
Time (mean ± σ): 1.055 s ± 0.024 s [User: 987.1 ms, System: 65.9 ms]
Range (min … max): 1.026 s … 1.094 s 10 runs
Summary
'./circ-new third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs' ran
1.15 ± 0.03 times faster than './circ-old third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs'
```
I split the hash-consing implementation into its own crate and re-implemented it.
In the new implementation, the table is thread-local. Terms are not Send, but linear terms are.
Decreased used of atomics gives a non-trivial speed-up. I tested on Z#'s sha2 round function, with an exit after IR optimization:
Benchmark #1: ./circ-old third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs
Time (mean ± σ): 236.2 ms ± 16.1 ms [User: 223.3 ms, System: 12.4 ms]
Range (min … max): 221.1 ms … 264.1 ms 11 runs
Benchmark #2: ./circ-new third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs
Time (mean ± σ): 141.8 ms ± 13.1 ms [User: 131.3 ms, System: 10.0 ms]
Range (min … max): 125.4 ms … 160.4 ms 18 runs
Summary
'./circ-new third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs' ran
1.67 ± 0.19 times faster than './circ-old third_party/ZoKrates/zokrates_stdlib/stdlib/hashes/sha256/shaRound.zok r1cs'
The first bug is a disagreement between our bellman circuit and our bellman
verify function. The circuit omit unused variables (public or private). The
verify function includes unused public variables.
Now, the circuit includes unused public variables.
The second bug is related to large BV comparisons. The fix is to emit a
bitwise comparator. We could optimize further in the future.
closes#125
* Configuration system. Kill DFL_T
* add circ::cfg::CircCfg that holds cfg info
* it's constructible from circ_opt::CircOpt
* implements clap::Args, so you can set it from your compiler's
CLI/envvars
* defined in external crate to keep clap out of our main build
* organized by circ module, but not feature gated
* no point: the build wouldn't meaningfully change
* includes a way to set the default field
* added circ::cfg::set and circ::cfg::cfg
* also circ::cfg::set_default and circ::cfg::set_cfg
* access a sync::once_cell, static configuration
* killed DFL_T
* workflows
* unit-tested component probably need to not read circ::cfg::cfg.
* compilers need to call circ::cfg::set or circ::cfg::set_default.
* rm dead features
* WIP
* Alternate formatting machinery.
* fmt & lint
* rm Letified
* ilp
* Configuration system. Kill DFL_T
* add circ::cfg::CircCfg that holds cfg info
* it's constructible from circ_opt::CircOpt
* implements clap::Args, so you can set it from your compiler's
CLI/envvars
* defined in external crate to keep clap out of our main build
* organized by circ module, but not feature gated
* no point: the build wouldn't meaningfully change
* includes a way to set the default field
* added circ::cfg::set and circ::cfg::cfg
* also circ::cfg::set_default and circ::cfg::set_cfg
* access a sync::once_cell, static configuration
* killed DFL_T
* workflows
* unit-tested component probably need to not read circ::cfg::cfg.
* compilers need to call circ::cfg::set or circ::cfg::set_default.
* rm dead features
Fixes 4 bugs in R1CS lowering:
* division-by-zero in finite fields: previously, this always caused
incompleteness. Now, the behavior depends on the CIRC_RELAXATION
envvar:
* CIRC_RELAXATION=incomplete: divide-by-0 causes incompletenes
* CIRC_RELAXATION=nondet: divide-by-0 allows the output to take any value
* CIRC_RELAXATION=det: divide-by-0 forces the output to 0
* bit-vector overshift: previously, this cause incompleteness. Now,
we follow the semantics of SMT-LIB (the result saturates).
* bit-vector udiv-by-zero: previously, the output value was an
unconstrained bit-vector. Now, it is MAX (following SMT-LIB).
* bit-vector comparisons: previously, the prover could lie, claiming
that x < y when actually x >= y. All bit-vector comparisons are
affected, including those in udiv and urem.
* soundness bug!
* Better serde impl for bellman keys
Bellman keys (pk and vk) expose non-trait read and write functions for
interacting with `io::{Read,Write}`. They don't expose serde impls.
We need to serde them.
Previously, we used the io interface to convert from/to a `Vec<u8>`,
whose serde impl we used.
This was a bad idea b/c the serde impl for `Vec<u8>` is bad. It gets
stuck with the generic serde impl for `Vec`, rather than using
`(de)serialize_bytes`.
Now, we have serde-impl'd wrapper types for pk and vk that do the right
thing.
By my measurements, this decreases the cost of serializing a pk by about
84%.
* serde_bytes
* Slightly better serde implementation for Term
Also, for data-structures thereof.
Crediting Colin, b/c this is based on his PR.
Co-Authored-By: Collin Zhang <collinzrj@gmail.com>
The previous implementation for all 3 structures would separately serialize each term in a precomputation. This was very bad, because precomputations can be quite large, and the different terms typically share large numbers of sub-terms. This can be quadratic blowup.
Change list:
add input/output type metadata to PreComp (this makes the type of variables in a PreComp clear)
add textual serialization and parsing for PreComp (and include this in Computation)
add serde implementations for Computation and PreCop based on the text formats.
modify the R1cs serde derive so that the Vec<Term> is tuplized before serde
This reduces our prover-key size for verifyEddsa.zok from wildly large (>450GB) to 171MB.
Collin and Anna first observed this bug. Collin's PR #118 works around it (among other improvements).
Updated MPC unit tests to use function abstractions. Most of these updates are made to the C frontend and MPC lowering pass. Additional optimization and ILP solving passes need to be updated.
The assignment and cost model passes now need to factor in Array and Tuple semantics. This requires changes to the CostModel assignments. This also requires the the def-use-graph implementation for constant-index propagation.
Work-around:
- disabled HyCC benchmark tests
- disabled tests that use Op::Select / Op::Store
We received a benchmark from Lef which essentially checked the
following:
(cond ? A*B : A*C)[i] == v
where A, B, C are 4 by 4 matrices, cond is a bool, i is an index, and v
a value.
The expected number of constraints is n^3: order 64 , but compile time
and constraint count were in the thousands.
I investigated finding a number of things:
* the Z# front-end entered a conditional branch for the ternary, causing
the MM to happen in a conditional context
* while the MM has an oblivious access pattern, since `i` is variable,
the oblivious pass wasn't really helping
* there were some weird non-constant indices floating around like
(ite cond 0 0)
The three optimizations fix these problems:
* If the Z# frontend isn't in assertion isolation mode, don't enter a
conditional branch for an ITE
* Constant folding: add the rewrite (ite cond a a) -> a
* Linear-scan array eliminator: for each operation, check if the index
is constant. If so, skip the scan (for that access only)
Initial commit for support function abstractions.
`Computations` are maps of function names `str` to computation `Computation`.
Updates:
- Frontend `Gen` returns `Computations` with only a single main `Computation`.
- Optimizations take in `Computations` instead of a single `Computation`. Optimizations are applied to each `Computation`.
- Backends take in only the main `Computation`.
