multi-stark bump - #522
Draft
gabriel-barrett wants to merge 8 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.
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).
gabriel-barrett
force-pushed
the
multi-stark-overhaul
branch
from
July 28, 2026 20:48
3f98f62 to
ad3cffa
Compare
Adopt the direct-logup multi-stark rev: the logUp constraints are no
longer compiled into the constraint graph, so the vk stops carrying
them — measured on the IxVM kernel system, the vk drops from 5.91 MB
to 1.54 MB (-74%; the synthesized logUp machinery was 91% of the
compiled nodes). The recursive verifier's in-circuit cost at toy scale
drops ~12% (less vk hashing and node reading).
- Cargo.toml: TEMPORARY [patch] to the local multi-stark checkout
(branch direct-logup, b76e43b); swap to the pushed rev before merge.
- vk_codec.rs: the per-circuit header's num_publics slot (a constant,
derived on decode) now carries constraint_count (user roots +
(L+3)*D, the observe_shape value), and max_constraint_degree is the
combined user + analytic-logUp value; the decoder fills the new
Circuit fields and recomputes the graph's own user-roots max degree.
- SystemDeserialize.lean: the compiled lookups (multiplicity + arg
NodeIds) are now parsed instead of skipped — they drive the direct
evaluation; the constraint-count shape limb comes from the header
(zero_count is no longer observed); record framing asserted.
- Verifier.lean: ood_composition folds the directly-evaluated logUp
values after the user roots, mirroring Rust's
lookup::logup_constraint_values: per lookup the two coordinates of
(beta + fingerprint(gamma, args)) * inv - 1 (fingerprint via
head-first Horner through the memoized eval_at, so lookup-expression
evaluation shares the user-constraint cache), then the first-row,
transition, and last-row accumulator constraints. Coordinate pairs
multiply in X^2 = 7 with Ext coefficients (pair_mul).
- aiur_multi_stark.rs regenerated (lake exe ix codegen).
lake test -- --ignored {multi-stark, recursive-verifier, aiur} all
pass (honest accepted, codegen matches interpreter, tampered proof and
claim rejected); cargo test -p aiur 5/5 incl. the vk codec round-trip;
workspace clippy/fmt clean.
The residual size gap to the old symbolic-tree vk was pure encoding
width: preorder trees pay zero bytes for structure while the graph
paid two u32 child ids per binary node. Close it by sizing the wire
fields to the actual value ranges:
- node ids, zeros, and lookup references are u16 (per-circuit graphs
are far below 65k nodes; the encoder asserts),
- Var packs (source, offset) into the tag byte (10 + 2*source +
offset) with a u16 column index: 7 bytes -> 3,
- constants split small (u16) / big (u64): most are selector weights
and small literals, 9 bytes -> 3,
- Public index is u8 (num_publics = 8),
- Add/Sub/Mul: 9 bytes -> 5.
Mirrored in SystemDeserialize.lean (tags 10..15 map straight to Var
source/offset constants; u16 reads); aiur_multi_stark.rs regenerated.
IxVM kernel vk progression: 5.91 MB (compiled logUp) -> 1.54 MB
(direct logUp) -> 819 KB dense — 28% below the old symbolic-tree
format (1.13 MB) and 7.2x below where this branch started, with the
same 4.3x hash-consing advantage now paying only ~2x pointer overhead.
lake test -- --ignored {multi-stark, recursive-verifier, aiur} all
pass (honest accepted, codegen matches interpreter, tampers rejected);
cargo test -p aiur 5/5 incl. codec round-trip; clippy/fmt clean.
gabriel-barrett
force-pushed
the
multi-stark-overhaul
branch
from
July 29, 2026 16:30
f2e025e to
58682f2
Compare
Nothing in the vk is now redundant — every byte is content the
verifier consumes (nodes, zeros, lookups, widths, degree):
- constraint_count and stage_2_width are no longer serialized: both
derive from the zero/lookup counts (zeros + (L+3)*D and (1+L)*D).
The Lean reader builds their Fiat-Shamir observation limbs with one
gl_to_bytes each — cheaper in-circuit than hashing the extra bytes.
- lookup_prefix_len dropped: the Lean verifier never used it, and the
Rust decoder derives it as 1 + the max node id reachable from the
lookup expressions (children always precede parents).
- The per-record u32 length prefix dropped: it existed to skip the
lookups section, which is now fully parsed; records decode from a
single shared cursor, guarded by the full-consumption check
(truncated and padded vks are rejected — test updated).
- Counts and widths sized to their ranges: node/zero/lookup counts,
main/preprocessed widths, and max_constraint_degree are u16
(preprocessed_height stays u32: the Bytes2 table is exactly 65536).
IxVM kernel vk: 819,329 -> 796,593 bytes. Full progression vs the
5.91 MB this line of work started from: direct logUp 1.54 MB, dense
nodes 819 KB, derivables dropped 797 KB — 30% below main's 1.13 MB
symbolic-tree format.
lake test -- --ignored {multi-stark, recursive-verifier, aiur} all
pass; cargo test -p aiur 5/5; clippy/fmt clean; codegen regenerated.
…t path) No API or protocol change — the rev only speeds up the prover's quotient constraint evaluation (~20% faster than the old compiled-logUp path on a lookup-heavy benchmark). cargo test -p aiur 5/5.
Member
Author
|
!benchmark aiur fresh |
Member
Author
|
!benchmark aiur-recursive 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 |
49.277 s | 46.373 s | -5.9% (1.06× faster) 🟢 | 34.620 | 36.790 | +6.3% (1.06× faster) 🟢 | 96.30 GiB | 96.39 GiB | +0.1% | 10.378 s | 10.351 s | -0.3% | 168.0 ms | 168.2 ms | +0.1% | 25.88 MiB | 25.88 MiB | +0.0% | 36.21B | 36.21B | +0.0% |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
50.414 s | 45.957 s | -8.8% (1.10× faster) 🟢 | 57.330 | 62.880 | +9.7% (1.10× faster) 🟢 | 102.06 GiB | 102.05 GiB | -0.0% | 9.454 s | 9.280 s | -1.8% | 162.9 ms | 221.2 ms | +35.8% (1.36× slower) |
25.96 MiB | 25.96 MiB | +0.0% | 38.11B | 38.11B | +0.0% |
Char.ofOrdinal_le_of_le |
38.262 s | 36.238 s | -5.3% (1.06× faster) 🟢 | 74.800 | 78.980 | +5.6% (1.06× faster) 🟢 | 79.83 GiB | 79.86 GiB | +0.0% | 6.805 s | 6.753 s | -0.8% | 162.6 ms | 199.9 ms | +23.0% (1.23× slower) |
25.90 MiB | 25.90 MiB | +0.0% | 29.15B | 29.15B | +0.0% |
Vector.extract_append._proof_2 |
28.725 s | 26.639 s | -7.3% (1.08× faster) 🟢 | 50.170 | 54.090 | +7.8% (1.08× faster) 🟢 | 53.16 GiB | 53.15 GiB | -0.0% | 5.678 s | 5.842 s | +2.9% | 166.4 ms | 165.9 ms | -0.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.427 s | 22.719 s | -3.0% 🟢 | 84.220 | 86.840 | +3.1% 🟢 | 50.09 GiB | 50.11 GiB | +0.0% | 3.472 s | 3.536 s | +1.8% | 174.6 ms | 163.6 ms | -6.3% (1.07× faster) 🟢 | 25.72 MiB | 25.72 MiB | +0.0% | 15.71B | 15.71B | +0.0% |
String.split |
22.690 s | 21.195 s | -6.6% (1.07× faster) 🟢 | 85.900 | 91.960 | +7.1% (1.07× faster) 🟢 | 48.06 GiB | 48.06 GiB | +0.0% | 3.139 s | 3.131 s | -0.3% | 171.9 ms | 165.2 ms | -3.9% 🟢 | 25.92 MiB | 25.92 MiB | +0.0% | 14.22B | 14.22B | +0.0% |
List.mergeSort |
15.556 s | 14.812 s | -4.8% (1.05× faster) 🟢 | 102.720 | 107.880 | +5.0% (1.05× faster) 🟢 | 31.73 GiB | 31.71 GiB | -0.1% | 2.263 s | 2.285 s | +1.0% | 161.1 ms | 180.1 ms | +11.8% (1.12× slower) |
25.77 MiB | 25.77 MiB | +0.0% | 10.46B | 10.46B | +0.0% |
Vector.append |
5.139 s | 4.921 s | -4.2% 🟢 | 110.140 | 115.010 | +4.4% 🟢 | 8.51 GiB | 8.36 GiB | -1.8% | 603.8 ms | 595.8 ms | -1.3% | 150.7 ms | 146.8 ms | -2.6% | 24.38 MiB | 24.38 MiB | +0.0% | 2.21B | 2.21B | +0.0% |
Nat.gcd_comm |
4.337 s | 4.132 s | -4.7% 🟢 | 95.680 | 100.430 | +5.0% 🟢 | 7.57 GiB | 7.54 GiB | -0.3% | 473.0 ms | 466.5 ms | -1.4% | 147.0 ms | 145.8 ms | -0.8% | 23.99 MiB | 23.99 MiB | +0.0% | 1.56B | 1.56B | +0.0% |
String.append |
3.172 s | 3.181 s | +0.3% | 111.290 | 110.970 | -0.3% | 6.49 GiB | 4.93 GiB | -24.1% (1.32× smaller) 🟢 | 355.5 ms | 365.6 ms | +2.8% | 151.0 ms | 139.2 ms | -7.8% (1.08× faster) 🟢 | 23.30 MiB | 23.30 MiB | +0.0% | 869.46M | 869.46M | +0.0% |
Int.gcd |
2.552 s | 2.548 s | -0.2% | 89.730 | 89.880 | +0.2% | 4.85 GiB | 5.53 GiB | +13.8% (1.14× larger) |
289.9 ms | 294.9 ms | +1.7% | 139.4 ms | 135.2 ms | -3.0% | 22.92 MiB | 22.92 MiB | +0.0% | 539.56M | 539.56M | +0.0% |
Nat.sub_le_of_le_add |
2.440 s | 2.391 s | -2.0% | 77.860 | 79.460 | +2.1% | 4.88 GiB | 4.85 GiB | -0.5% | 281.2 ms | 285.5 ms | +1.5% | 150.4 ms | 147.8 ms | -1.7% | 23.39 MiB | 23.39 MiB | +0.0% | 451.92M | 451.92M | +0.0% |
Nat.add_comm |
1.298 s | 1.311 s | +1.0% | 39.290 | 38.900 | -1.0% | 4.17 GiB | 3.92 GiB | -6.1% (1.06× smaller) 🟢 | 198.3 ms | 195.0 ms | -1.6% | 138.8 ms | 127.3 ms | -8.3% (1.09× faster) 🟢 | 21.85 MiB | 21.85 MiB | +0.0% | 48.99M | 48.99M | +0.0% |
13 constants · 4 with regressions · 11 with improvements (|Δ| > 3.0% on any metric).
|
| 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 |
5.126 s | 4.569 s | -10.9% (1.12× faster) 🟢 | 14.61 GiB | 14.62 GiB | +0.1% | 10.91 MiB | 10.88 MiB | -0.3% | 76.7 ms | 68.8 ms | -10.3% (1.12× faster) 🟢 | 462.7 ms | 442.0 ms | -4.5% 🟢 | 3.94B | 3.84B | -2.7% | 99.5 ms | 100.6 ms | +1.2% | 846.23 KiB | 846.23 KiB | +0.0% | 6.9 ms | 6.5 ms | -4.8% (1.05× faster) 🟢 | 355.63 MiB | 364.95 MiB | +2.6% |
square-q100-b1 |
3.506 s | 3.708 s | +5.8% (1.06× slower) |
9.66 GiB | 9.63 GiB | -0.3% | 10.84 MiB | 10.81 MiB | -0.3% | 76.5 ms | 70.4 ms | -8.0% (1.09× faster) 🟢 | 401.7 ms | 408.5 ms | +1.7% | 3.39B | 3.41B | +0.6% | 71.0 ms | 101.1 ms | +42.3% (1.42× slower) |
779.67 KiB | 779.67 KiB | +0.0% | 6.1 ms | 6.2 ms | +0.4% | 253.34 MiB | 270.73 MiB | +6.9% (1.07× larger) |
2 proofs · 1 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).
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.