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.
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)
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
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`.
* update TODO
* add quiet mode to zxc
* Drop and garbage collection
This commit adds Drop instances and related functionality that force
garbage collection at life cycle end of various structs that contain
Terms.
I didn't implement Drop for Computation because its Terms are generally
moved into a converter. This means that back-ends are responsible for
garbage collecting (see new functionality in ILP, R1cs, and ABY).
* collect the cfold table, too
* prevent double-panic as a result of garbage_collect()
* z# parser: zx is a default extension too
* update Cargo.lock
* strictness un-op #()
also added err messages for asserts and ?: ternary support from ZoK upstream
* for assignments, strict rhs => strict lhs
* zsharp: type definitions WIP
Still missing monomorphization.
* type defns: generic inference
* struct monomorphization for type aliased structs
* different approach: no monomorphization, just canonicalize aliases
* canonicalize struct names
* typedef tests
things work except that importing an alias and not its referent breaks typechecking
* add error message about needing to import referent structs
* update hashconsing pointer in Cargo.toml
* maybe_garbage_collect should also return early when panicking
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
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.
* macos deps script (broken on M1 for now)
* arch dep should be coin-or-cbc
* ZoK 0.7.6 support megat status-commit
- bring in ZoK 0.7.6 libraries
- port in diffs from old thirdparty
- first-cut const and literal support
- add toposort for includes so that we can resolve const values in next pass
- statement handling, include-walking fix
- type should cover u64 case, too
- structs: store for now
- const handling
- flatten import map up-front to make later derefs easier to handle
- stash note
- need array consts, too
- rough in const array support, I think
- error message
- small cleanups: change type of ZGen::constants and make comments more meaningful
- generics in fn calls
- small: better error message
- need to resolve exprs as const in const_type_
- wip simple typing pass
- ast visitor wip
- zokrates ast visitor 1st cut
- double check that we cover all product types
- const typing visitor ; visitor error handling
- reorg visit_files ; unification infra wip
- unification infra wip
- need to walk accesses for an assignment
- walk_accesses wip
- small q
- refactor: data structs should be Hash(Hash), not flat
- walk_accesses wip
- monomorphize structs on LHS of declarations
- check identifiers when monomorphizing structs
- unification wip
- unification wip
- inline struct members must declare all fields
- unification for array_initializer
- unify postfix
- unify fdef with call
- ZExpressionTyper wip
- ZExpressionTyper wip
- ZExpressionTyper first cut
- type equality first cut
- type equality improved
- update struct handling
- stash note
- zok_fe trivial
- error msg fix
- params in scope during stmt visiting
- stash note
- and_then rather than unwrap in flatten_import_map
- handle special names (e.g. EMBED) in toposort
- types for EMBED
- EMBED is now a valid file in stdlib
- rewriter should handle Types, too
- need to rewrite literals on LHS of def stmts
- iteration: fix type of iter var
- for now, allow indexing with both Field and u*
- add warning for indexing with Field
- impl pow
- don't add ITE when unconditionally assigning
- oops, Uint takes bv_lit not pf_lit
- simplify
- fix arg order to bv_lit, improve new_<integral> functions
- use constant folding for term::const_int
- EMBED rework wip
- EMBED rework wip
- EMBED rework wip
- EMBED rework wip
- EMBED rework wip
- prep for generic inf push
- generic inf wip
- generic inf wip
- generic inf wip
- struct generic inference
- struct array inference wip
- make const_expr_ return Result<> rather than blowing up
- finish first-cut generic inf for Array
- turn on fn generic inf
- rework struct monomorphization code
- add support for const asserts
- process declarations lexically
previously we'd processed all consts, then structs, then fns.
now we want to add const initialization via function call,
which is easiest to implement if we simply process declarations
in-order as they appear in the file and require that all uses
follow defs lexically.
This seems to rule out mutual recursion, so we may want to revisit.
- add const initialization via ternary
- const fn call wip
- ZGen interior mutability
this lets us call expr, const_expr_ without mut ref.
this seems to be the right way to go here.
- small touches after rebase
- reorganize zvisit code
- generic lookup: should go through whole stack! (and not panic if stack is empty)
- wip bugfixes
- const_identifier_ should consult generics ; generic_lookup shouldn't traverse the whole stack
- expr type inf for array accesses
- small
- const_stmt_ infra
- const_stmt_ most var infra in place
- cvar_assign handles AssigneeAccesses now
- split type_ and const_type_ using const generics
- cvar_assign: build up list of accesses before resolving them, so that we don't try to double-borrow cvars_stack
- interpreter intf
- zoki --- zok interpreter front-end
- const_expr direct access vs through term impl
- very quick zsharp readme
- feature gate ILP back-end
this makes it easier to build CirC on M1 macs (otherwise,
need to build coin-or from source, which is not hard but
is annoying)
- rename zokrates to zsharp
- heavy hitting stuff here
- update z# readme
- turn off ci for zsharp branch
- small
- add cfg to switch to bn254 curve
- zsharp readme quick
- struct consts
- handle literals on LHS of const decls
- typechecker: ! can take U*, too
- refactor typechecking in InlineStructExpression handling, const_eexpr_ (this is going to move, though)
- support inline structs in ZConstLiteralRewriter
- really turn of ci this time, don't just induce a failure
- don't build circ or opa_bench examples when 'lp' option is off ; fix example builds given renamed zokrates module
- unify_inline_array: respect array dims!
- better InlineArray len handling
- check fn return type
- small, plus a few tiny test cases
- redefinition is an error
- update thinking / status on uglinesses
- explicit generic literals are U32
- remove redundant typechecking in InlineStruct const expr handling
- array and struct equality
- generic-in-generic const test
- inline array and struct generic tests
- small
- sticky notes
- stash note
- small cleanup in zstmtwalker
- support ZSHARP_STDLIB_PATH envvar in ZStdLib
- get_field_size in EMBED ; field comparisons
- test runner
- hex literal fix
- inconsistent array test
- literals test
- TODO quick update
* generic inf refactor wip
* generic inf refactor
- keep plugging away at revamped generic inference
- generic inf refactor wip
- generic inf rework wip
- stash note about divrem
- generic inf wip
- build up one term rather than a vec; walk struct members; remove old crap
- small
- generic inf rework wip
- generic inf refactor wip
- partially hook up new generic inf
- zgenericinf: invoke solver, return result
- ZGenericInf hooked up
- stash a note
- find_unique_model function
- enable incremental mode for find_unique_model
- hook up find_unique_model in zgenericinf
* go over TODOs and small cleanup
* field %
- field to bv should use full width
- need to make sure MSB is 0 when lowering to R1CS\!
* update todos
* unify const and non-const code paths
- unify function_call and const_function_call
- unify stmt and const_stmt
- type_impl_ returns Result<>
- unify expr and const_expr
* update TODO
* rework after rebase
* fix circ example and clippies
* constant folding for array select and store
* cfold: Tuple and extend Eq
* more informative generic params error message in function call
* array accesses should be Field if not otherwise typed
* support Uxx array indexing (automatic type coercion) ; check array index and value for consistency
* tuple const folding
* stash note about array construction
* todos
* more todos
* IR tuple repr: use boxed slices rather than vecs
this enforces the invariant that tuple lengths cannot be changed
closes#39
* IR tuple typing checks
the value in a given tuple slot has a fixed type.
this invariant isn't fully captured right now---it's
up to front- and back-ends to enforce this.
[ EDIT: I think the above is wrong. `ir::term::ty::rec_check_raw`
appears to enforce this. ]
I've added a couple extra safety checks for this.
* todo update
* const fold bvconcat and booltobv
* IR array key_sort and bounds checks
* array oob todos / tests
* ZGenericInf early exit for monomorphized calls
* self.unwrap cleanup
* cache generic inference results
* small debug/assert
* array construction optimization
when constructing an array, push leaf terms directly into the array
rather than building up a huge term. This reduces memory pressure and
reduces constant folding cost in the (common) case of large const
arrays
* todos
* clippy
* bit order consistency fix / tests
to_bits and from_bits functions use msb0 ordering
(i.e., index 0 of the bool array is the MSB)
* clippy small
* update TODOs
* clippy for zsharp frontend
* cargo fmt ; pretty-printing T
* add span for error context in expr and stmt
* update TODOs
* add s_divisible and s_remainder in 'field' in stdlib
* comment on signed field fns
* superfluous front-end example
* zxi unused imports
* zxc first cut
* zxc: in count mode, dump out constraints
* sidestep stack blowup in ir::term::ty::check_raw
* add option to skip linearity reduction in zxc with -L
* debug messages... darn
* lru caching for cfold
* unbounded/bounded cache
unbounded during a single fold_cache call, bounded between
* rebase fixes
feature gate aby back-end with lp
changes in zxi/zxc, and some clippies
* don't check-in non-top-level Cargo.lock
* increase LRU cache size for cfold to avoid n^2 behavior
* heuristic term/type cache collector
* tidy
* fmt
* small bugfix
* small fixes ; move zx_tests
* re-enable ci
* fmt
* tentative obliv-fix
* more obliv-fix
* clippy (for tests)
* Polish the obliv fix a bit. Document
* Addressing my unsolicited comment
* fix build
* typo
* stash Alex's idea about modeling RAM transformations
* back to upstream hashconsing
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: Riad S. Wahby <rsw@jfet.org>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
The ZoKrates front-end now represents ZoK arrays as IR arrays, and ZoK structures as (type-tagged) IR tuples.
During this change, I discovered that IR support for eliminating tuples and arrays was not complete.
Thus the change list is:
The ZoK front-end uses IR arrays and tuples
Improve IR passes for array and tuple elimination
Enforce cargo fmt in CI
Bugfix: handle ZoK accessors in L-values in the correct order
Bugfix: add array evaluation to the IR
This PR does not:
implement an array flattening pass
implement permutation-based memory-checking
Benefits:
The ZoK->R1CS compiler is now ~5.88x faster (as defined by the time it takes to run the tests in master's scripts/zokrates_test.zsh script: this goes from 8.59s to 1.46s)
For benchmarks with multi-dimensional arrays, the ZoK->R1CS compiler can now compile them with reasonable speed. Before it it would time out on even tiny examples.
The ZoK->R1CS compiler will be able to benefit from future memory-checking improvements
IR support for arrays and tuples is complete now, making those parts of the IR more accessible to future front-ends.
alex-ozdemir added 21 commits 11 days ago
This PR makes compilation deterministic (by switching to fxhash) and improves the CLI.
Technically, the std-based hash tables cannot be guaranteed to have the deterministic iteration order that we need, regardless of what hash you use, so I've added some micro-tests for the property that we need. I'm not optimistic about getting better guarantees from std, but I'll try.
The CLI has also changed.
* OPA-by-ILP benchmark example
* Reverted unverified push to master branch
* Added conversion gates and integrated ABY lowering with SharingMap
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
