* windowed mul
* Working
* Window of 4 bits
* Fix
* Comments
* Unroll loop
* Unroll loop
* remove global
* Minor
* Minor
* Implement `CALLVALUE, CALLDATALOAD, CALLDATASIZE, CALLDATACOPY` in interpreter
* Minor
* Doesn't work
* Minor
* Minor
* wnaf msm
* Working hardcoded values: 28657 opcodes
* Working wnaf
* Small wnaf optim
* Precompute works
* Working together
* Bump to 129 bits
* Working glv decomposition
* Working MSM with GLV
* Almost working
* Working
* ECC test folder
* Working with real sig data
* Fix tests + Clippy
* Minor
* Cleaning
* Comments
* Cleaning
* Smaller glv test file
* Print opcode count at the end of interpreter run
* More constants
* Add z3 proof that the GLV scalars are 129-bit or less
* Minor change to z3 proof
* Move files and renaming fns
* Testing
* Fix BN GLV
* BN precompute table
* Working precompute
* Working bn tests
* Working
* Minor
* Minor
* Use MULFP254
* Minor
* Merge conflicts
* Remove unused asm file
* ECC fns renaming (#874)
* PR feedback
* Unify handling of ADD, SUB, LT, GT under the formula x+y=z+cy*2^256.
* Rename general column ranges to "registers" instead of "inputs".
* Rename 'compare' module to 'addcc'.
* Update comments.
* Enforce length equality in iteration.
* Address William's PR comments.
* windowed mul
* Working
* Window of 4 bits
* Fix
* Comments
* Unroll loop
* Unroll loop
* remove global
* Minor
* Minor
* Implement `CALLVALUE, CALLDATALOAD, CALLDATASIZE, CALLDATACOPY` in interpreter
* Minor
* Doesn't work
* Minor
* Minor
* wnaf msm
* Working hardcoded values: 28657 opcodes
* Working wnaf
* Small wnaf optim
* Precompute works
* Working together
* Bump to 129 bits
* Working glv decomposition
* Working MSM with GLV
* Almost working
* Working
* ECC test folder
* Working with real sig data
* Fix tests + Clippy
* Minor
* Cleaning
* Comments
* Cleaning
* Smaller glv test file
* Print opcode count at the end of interpreter run
* More constants
* Add z3 proof that the GLV scalars are 129-bit or less
* Minor change to z3 proof
* Minor
* Hamish's suggestion
* Working
* Cleaning
* Clippy
* PR feedback
* Minor PR feedback
* Simplify loop and remove clippy.
* Offset auxiliary coefficients so they're always positive.
* Split mul aux input into lo/hi parts.
* Rename register.
* Combine `QUO_INPUT_{LO,HI}`; rearrange some columns.
* Split `MODULAR_AUX_INPUT` into high and low pieces.
* Remove range_check_error debug output.
* First draft of generating the range checks.
* Remove opcodes for operations that were defined elsewhere.
* Clean up interface to build arithmetic trace.
* Fix "degree too high" bug in DIV by zero.
* Fix constraint_transition usage in recursive compare.
* Fix variable name; use named constant.
* Fix comment values.
* Fix bug in recursive MUL circuit.
* Superficial improvements; remove unnecessary genericity.
* Fix bug in recursive MULMOD circuit.
* Remove debugging noise; expand test.
* Minor comment.
* Enforce assumption in assert.
* Make DIV its own operation.
* Make MOD it's own operation; rename structs; refactor.
* Expand basic test.
* Remove comment.
* Put Stark operations in their own file.
* Test long traces.
* Minor comment.
* Address William's comments.
* Use `const_assert!` instead of `debug_assert!` because Clippy.
* New implementation of InterpolationGate
* Use CosetInterpolationGate in recursive verifier
* Minimize the degree of interpolation gate
Minimize the degree if it doesn't increase the number of wires or constraints. This allows for more efficiency with selectors.
* Include tests for number of wires and constraints
* Run rustfmt
* Run cargo fmt
* Fix documentation typo
Co-authored-by: wborgeaud <williamborgeaud@gmail.com>
* Fix clippy issue
Co-authored-by: wborgeaud <williamborgeaud@gmail.com>
Which can be used to compress two proofs into one. Each inner proof can be either
- an "EVM root" proof (which typically proves one transaction, though it could be 0 or more)
- another aggregation proof
Reverts the degree adjustment part of #436. As @jimpo pointed out, the adjustment complicates security by allowing rational functions of the form `poly(x) / x`.
A tight degree bound shouldn't be necessary. Ultimately we want to check that some witness function `f(x)` exists satisfying (simplified) `c(f(x)) = Z_H(x) q(x)`. We only need `f(x)` to be low-degree because that allows us to use polynomial identity testing. With PIT we don't care about exact degree bounds; a negligible degree change will have a negligible effect on PIT soundness.
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
