Change: The tuple elimination pass now represents its *tuple trees*
using nested persistent vectors of non-tuple terms, rather than standard
terms.
Rationale: When large oblivious arrays are transformed to tuples, said
tuples are large, and updates to them use the tuple update operator.
However, when we eliminate those tuples, we essentially replace the
update operator with an explicit tuple (tree). For a large number of
updates, this entails quadratic memory usage.
Of course, it doesn't *need* to: each update only modifies one spot in
the tuple.
Thus, in this patch, we change the representation of tuples in tuple
tree from a standard term---whose children are in a vector---such that
the children are now in a persistent vector from the `im` crate. This
allows for an "update" operation on the vector that takes log time and
log new space.
Effect: This reduces the compiler's memory usage on
`examples/C/mpc/benchmarks/2pc_biomatch_40x.c` from ~28GB to ~1GB. It
also makes the compiler substantially faster on that benchmark.
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.
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
* 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
