multi-stark bump - #522
Draft
gabriel-barrett wants to merge 4 commits into
Draft
Conversation
Bump multi-stark to the constraint-IR rev (1c6ef62) and adapt Aiur to the
new API, which replaces the AIR/builder machinery with data. Net removal:
Aiur no longer defines AIRs — it builds CircuitInputs (Expr constraints +
Lookups) directly.
- constraints.rs: SymbolicExpression -> multi_stark::expr::Expr; delete the
Constraints Air/BaseAir impls; materialize the per-selector boolean
constraints (formerly emitted in eval) into the constraint vector; keep
the degree-tracking auxiliary-column allocation.
- synthesis.rs: System<SC, AiurCircuit> -> System<SC>; delete the
AiurCircuit AIR enum; build each circuit as CircuitInputs; retain
per-circuit lookup slot widths for the witness layout (the old
circuits[i].air.lookups path is gone). prove/verify logic unchanged.
- memory.rs / gadgets{,bytes1,bytes2}.rs: lookups over Expr (pull = negated
multiplicity), delete Air/BaseAir, re-express memory transition rules as
explicit Expr constraints (IsTransition / main_next); keep tables,
execution, and witness generation.
- vk_codec.rs: serialize the new compiled circuit (flat node graph + roots
+ widths) instead of the symbolic AIR. NOTE: the vk wire format changed;
the Lean mirror Ix/MultiStark/SystemDeserialize.lean must be updated to
match (not done here).
Adds a Rust end-to-end prove/verify test (f(a,b)=a*b) exercising an
auxiliary column and the function-channel lookup: honest proof verifies,
tampered claim rejected. cargo check/test/clippy/fmt clean across the
workspace.
Adds prove_verify_call_and_memory_roundtrip: f(a,b) = g(a)*b with b routed through a size-1 memory (Call + Store + Load + Mul). Exercises the cross-circuit function-channel lookup (f pushes, g's return pulls) and the memory-channel lookup + the migrated Memory transition constraints. Honest proof verifies; tampered claim rejected. Test-only; 5 aiur tests pass.
Rewrite the Aiur-DSL recursive STARK verifier to match the new constraint-IR multi-stark (vk v3 = flat compiled node graph). - SystemDeserialize.lean: parse per-circuit 8xu32 header + tagged SysNode stream (children by NodeId) + zeros roots (compiled lookups skipped via the record length prefix; lookup constraints are compiled into zeros). Drop SymExpr/SysEntry/SysAir/SysLookupAir and the symbolic reader. - Verifier.lean: replace the symbolic-tree interpreter + LookupAir replay (eval_sym/fingerprint_ext/fold_zeros/fold_sel_bools/fold_lookups/ ood_comp_tail) with a forward node sweep: sweep_nodes builds a per-node value buffer, eval_node reads leaves (Var by 2*source+offset from the opened rows, Public from the beta/gamma/acc/next_acc coord vector, selectors from Lagrange evals), fold_roots Horner-folds zeros with alpha. Stage-2 opened rows fed as base columns directly (no from_ext_basis); quotient recombination unchanged. - Regenerate crates/ixvm-codegen/src/aiur_multi_stark.rs (lake exe ix codegen); aiur_ixvm.rs byte-identical. lake test: multi-stark self-tests 12/12, recursive-verifier e2e 6/6 (honest proof accepted, codegen verifier matches interpreter, tamper rejected), aiur prove/verify 5/5 programs.
Member
Author
|
!benchmark aiur fresh |
|
| constant | prove-time (main) | prove-time (PR) | Δ% | throughput (const/s) (main) | throughput (const/s) (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% | execute-time (main) | execute-time (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | fft-cost (main) | fft-cost (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Array.extract_append |
48.575 s | 46.693 s | -3.9% 🟢 | 35.120 | 36.540 | +4.0% 🟢 | 96.36 GiB | 96.27 GiB | -0.1% | 10.548 s | 10.569 s | +0.2% | 167.5 ms | 167.1 ms | -0.2% | 25.88 MiB | 25.88 MiB | +0.0% | 36.21B | 36.21B | +0.0% |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
47.937 s | 46.092 s | -3.9% 🟢 | 60.290 | 62.700 | +4.0% 🟢 | 102.03 GiB | 102.10 GiB | +0.1% | 9.078 s | 9.112 s | +0.4% | 179.6 ms | 191.9 ms | +6.9% (1.07× slower) |
25.96 MiB | 25.96 MiB | +0.0% | 38.11B | 38.11B | +0.0% |
Char.ofOrdinal_le_of_le |
37.956 s | 36.577 s | -3.6% 🟢 | 75.400 | 78.250 | +3.8% 🟢 | 79.82 GiB | 79.92 GiB | +0.1% | 6.793 s | 6.573 s | -3.2% 🟢 | 198.3 ms | 179.3 ms | -9.6% (1.11× faster) 🟢 | 25.90 MiB | 25.90 MiB | +0.0% | 29.15B | 29.15B | +0.0% |
Vector.extract_append._proof_2 |
27.943 s | 26.779 s | -4.2% 🟢 | 51.570 | 53.810 | +4.3% 🟢 | 53.13 GiB | 53.15 GiB | +0.0% | 5.626 s | 5.842 s | +3.8% |
161.3 ms | 157.6 ms | -2.3% | 25.55 MiB | 25.55 MiB | +0.0% | 21.18B | 21.18B | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
23.479 s | 22.482 s | -4.2% 🟢 | 84.030 | 87.760 | +4.4% 🟢 | 50.08 GiB | 50.07 GiB | -0.0% | 3.440 s | 3.457 s | +0.5% | 161.2 ms | 172.5 ms | +7.0% (1.07× slower) |
25.72 MiB | 25.72 MiB | +0.0% | 15.71B | 15.71B | +0.0% |
String.split |
22.145 s | 21.371 s | -3.5% 🟢 | 88.010 | 91.200 | +3.6% 🟢 | 48.06 GiB | 48.04 GiB | -0.1% | 3.142 s | 3.139 s | -0.1% | 178.6 ms | 159.1 ms | -10.9% (1.12× faster) 🟢 | 25.92 MiB | 25.92 MiB | +0.0% | 14.22B | 14.22B | +0.0% |
List.mergeSort |
15.381 s | 14.885 s | -3.2% 🟢 | 103.900 | 107.360 | +3.3% 🟢 | 31.72 GiB | 31.77 GiB | +0.2% | 2.247 s | 2.236 s | -0.5% | 172.5 ms | 156.0 ms | -9.6% (1.11× faster) 🟢 | 25.77 MiB | 25.77 MiB | +0.0% | 10.46B | 10.46B | +0.0% |
Vector.append |
5.095 s | 4.984 s | -2.2% | 111.090 | 113.570 | +2.2% | 8.35 GiB | 8.33 GiB | -0.2% | 604.5 ms | 612.9 ms | +1.4% | 161.5 ms | 151.8 ms | -6.0% (1.06× faster) 🟢 | 24.38 MiB | 24.38 MiB | +0.0% | 2.21B | 2.21B | +0.0% |
Nat.gcd_comm |
4.247 s | 4.149 s | -2.3% | 97.720 | 100.030 | +2.4% | 7.88 GiB | 7.51 GiB | -4.6% 🟢 | 475.0 ms | 473.2 ms | -0.4% | 147.7 ms | 154.1 ms | +4.3% |
23.99 MiB | 23.99 MiB | +0.0% | 1.56B | 1.56B | +0.0% |
String.append |
3.149 s | 3.050 s | -3.1% 🟢 | 112.110 | 115.730 | +3.2% 🟢 | 6.63 GiB | 6.55 GiB | -1.3% | 357.4 ms | 352.8 ms | -1.3% | 148.6 ms | 142.1 ms | -4.4% 🟢 | 23.30 MiB | 23.30 MiB | +0.0% | 869.46M | 869.46M | +0.0% |
Int.gcd |
2.564 s | 2.551 s | -0.5% | 89.320 | 89.780 | +0.5% | 4.85 GiB | 4.84 GiB | -0.1% | 289.6 ms | 290.0 ms | +0.2% | 139.3 ms | 132.7 ms | -4.7% 🟢 | 22.92 MiB | 22.92 MiB | +0.0% | 539.56M | 539.56M | +0.0% |
Nat.sub_le_of_le_add |
2.360 s | 2.398 s | +1.6% | 80.530 | 79.230 | -1.6% | 4.92 GiB | 4.88 GiB | -0.9% | 285.0 ms | 284.3 ms | -0.2% | 157.3 ms | 147.4 ms | -6.3% (1.07× faster) 🟢 | 23.39 MiB | 23.39 MiB | +0.0% | 451.92M | 451.92M | +0.0% |
Nat.add_comm |
1.284 s | 1.337 s | +4.1% |
39.710 | 38.150 | -3.9% |
3.96 GiB | 4.62 GiB | +16.6% (1.17× larger) |
197.4 ms | 197.3 ms | -0.1% | 129.2 ms | 125.8 ms | -2.6% | 21.85 MiB | 21.85 MiB | +0.0% | 48.99M | 48.99M | +0.0% |
13 constants · 5 with regressions · 12 with improvements (|Δ| > 3.0% on any metric).
The OOD composition check evaluated the constraint graph with a forward sweep mirroring the Rust evaluator, appending each node's value to a List<Ext> buffer via list_concat and reading children back with list_lookup. In Aiur that buffer is O(n^2): every append rebuilds the list, and the temporaries dominated the verifier's list traffic (list_concat.G_2 alone was 16% of total FFT cost). eval_at interprets the graph directly instead: evaluate node i by recursing into its children. Aiur memoizes calls by argument pointers, so each node is computed at most once per opening context and every further reference (DAG sharing, later constraint roots) is a cache hit; node fetches share list_drop's cached drop-chain over the single nodes list. fold_roots evaluates each constraint root through the same cache. Dead nodes unreachable from the roots are never evaluated at all. bench-recursive-verifier --execute-only --queries 3 (factorial(5)): total in-circuit FFT cost 341.4M -> 222.9M (-35%); the sweep-buffer circuits (sweep_nodes/buf_child and the list_concat.G_2 + memory[4] traffic) drop out of the profile, leaving Blake3 hashing at ~80% of verifier cost. aiur_multi_stark.rs regenerated (lake exe ix codegen). lake test -- --ignored recursive-verifier: 6/6 (codegen'd verifier matches interpreter; tampered proof and claim still rejected).
Member
Author
|
!benchmark aiur-recursive fresh |
|
| proof | recursive-prove-time (main) | recursive-prove-time (PR) | Δ% | recursive-peak-ram (main) | recursive-peak-ram (PR) | Δ% | recursive-proof-size (main) | recursive-proof-size (PR) | Δ% | recursive-verify-time (main) | recursive-verify-time (PR) | Δ% | recursive-execute-time (main) | recursive-execute-time (PR) | Δ% | recursive-fft-cost (main) | recursive-fft-cost (PR) | Δ% | prove-time (main) | prove-time (PR) | Δ% | proof-size (main) | proof-size (PR) | Δ% | verify-time (main) | verify-time (PR) | Δ% | peak-ram (main) | peak-ram (PR) | Δ% |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
factorial-q100-b2 |
4.544 s | 4.540 s | -0.1% | 14.64 GiB | 14.63 GiB | -0.1% | 10.91 MiB | 10.57 MiB | -3.2% 🟢 | 70.3 ms | 67.2 ms | -4.5% 🟢 | 448.5 ms | 448.2 ms | -0.1% | 3.94B | 3.97B | +0.6% | 87.8 ms | 98.9 ms | +12.6% (1.13× slower) |
846.23 KiB | 846.23 KiB | +0.0% | 6.3 ms | 6.6 ms | +5.1% (1.05× slower) |
361.79 MiB | 370.93 MiB | +2.5% |
square-q100-b1 |
3.424 s | 3.480 s | +1.6% | 9.62 GiB | 9.67 GiB | +0.5% | 10.84 MiB | 10.50 MiB | -3.2% 🟢 | 73.4 ms | 67.6 ms | -8.0% (1.09× faster) 🟢 | 398.8 ms | 400.1 ms | +0.3% | 3.39B | 3.30B | -2.5% | 71.0 ms | 74.8 ms | +5.3% (1.05× slower) |
779.67 KiB | 779.67 KiB | +0.0% | 6.1 ms | 6.2 ms | +1.3% | 255.14 MiB | 262.51 MiB | +2.9% |
2 proofs · 2 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).
gabriel-barrett
force-pushed
the
multi-stark-overhaul
branch
from
July 28, 2026 20:48
3f98f62 to
ad3cffa
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Aiur on constraint-IR multi-stark + in-circuit verifier port
Adopts the multi-stark constraint restructure
(argumentcomputer/multi-stark#
multi-stark-overhaul,rev
1c6ef62), where circuits are data instead ofAirtrait impls:frontend
Exprtrees compile to a flat, hash-consed node graph(
graph::ConstraintGraph) that the prover, verifier, and witnessgenerator evaluate with a dense forward sweep. Three commits, each
building and passing tests on its own:
1.
aiur: migrate to constraint-IR multi-starkAiur no longer defines AIRs — it builds
CircuitInputs(Exprconstraints + lookups) directly.
SymbolicExpression→multi_stark::expr::Expr;the
ConstraintsAir/BaseAirimpls are deleted; the per-selectorboolean constraints formerly emitted in
evalare materialized intothe constraint vector; degree-tracking auxiliary-column allocation is
kept.
System<SC, AiurCircuit>→System<SC>; theAiurCircuitAIR enum is gone; each circuit becomes aCircuitInputs. Prove/verify logic unchanged.Expr(pull = negatedmultiplicity); memory transition rules re-expressed as explicit
constraints via
IsTransition/ next-row columns.graph (tagged node stream, constraint roots, layout widths) instead
of the symbolic AIR. Node degrees are derived on decode, not stored.
column and the function-channel lookup: honest proof verifies,
tampered claim rejected.
2.
aiur: broaden e2e prove/verify test to call + memoryExtends the e2e test to cover function calls and store/load, so the
function and memory lookup channels are exercised through real proofs.
3.
MultiStark: port in-circuit recursive verifier to constraint-IRThe Aiur-DSL recursive STARK verifier now consumes vk v3.
node stream + constraint roots. The symbolic reader
(
SymExpr/SysAir/SysLookupAir) is deleted — lookup constraintsarrive pre-compiled into the roots.
LookupAirreplayis replaced by a forward node sweep mirroring the Rust evaluator:
one value buffer slot per node, leaves read from the opened rows /
lookup publics / Lagrange selector evals, roots Horner-folded with α.
Stage-2 openings are consumed as base columns directly (no
from_ext_basisexcept for the quotient). Quotient recombinationunchanged.
crates/ixvm-codegen/src/aiur_multi_stark.rsregenerated(
lake exe ix codegen).Testing
cargo test -p aiur --release: 5/5 e2e prove/verify programs;workspace
check/clippy/fmtclean.lake test -- --ignored multi-stark: non-native Goldilocks /ExtGoldilocks arithmetic + reduced-opening fold vs reference, 12/12.
lake test -- --ignored recursive-verifier: honest proof accepted(vk digest + OOD + FRI), codegen'd verifier matches the interpreter,
tampered proof advice and tampered claim both rejected, 6/6.
lake test -- --ignored aiur: execute/interpret/claim/prove/verifyacross the test programs.