Skip to content

chore: Update multi stark - #588

Draft
samuelburnham wants to merge 4 commits into
mainfrom
update-multi-stark
Draft

chore: Update multi stark#588
samuelburnham wants to merge 4 commits into
mainfrom
update-multi-stark

Conversation

@samuelburnham

@samuelburnham samuelburnham commented Aug 22, 2026

Copy link
Copy Markdown
Member

@samuelburnham
samuelburnham force-pushed the update-multi-stark branch 2 times, most recently from 7a91539 to 10d1cda Compare August 24, 2026 20:57
@samuelburnham
Bump Rust toolchain to 1.98
9ed7db5 
- rust-toolchain.toml channel: 1.92 → 1.98, with the matching fenix
  toolchain hash in flake.nix. The pinned fenix already carries the 1.98
  release manifest, so flake.lock needs no change (fenix's nixpkgs stays
  pinned via its lean4-nix follows, so the Lean toolchain is untouched).
- Drop clippy::from_iter_instead_of_collect from the workspace lints:
  removed in clippy 1.98 and now warns as unknown.
- Fix the warnings new clippy 1.98 lints surface across the workspace:
  chunks_exact(N) → as_chunks::<N>() where the chunk size is constant,
  descending sort_by → sort_by_key(Reverse(..)), iteration over map
  values via .values(), map().unwrap_or() → map_or(), a checked
  division, an unwrap-after-is_some restructured into if-let, and
  assorted redundant-reference/pattern cleanups (mostly cargo clippy
  --fix). The two byte-gadget files keep their chunks_exact warnings
  until the next commit, which rewrites those regions anyway.

CI derives its Rust version from rust-toolchain.toml, so no workflow
changes are needed.
@samuelburnham
Bump multi-stark: width-binding policy, height bound, P3 v0.6.0
2e4e7fe 
Companion to multi-stark's update-p3 branch (c72d321 → 249b740), which
carries four soundness/robustness fixes and the Plonky3 v0.6.0 bump
(pruned FRI Merkle multiproofs: ~2x faster verification, 40-70% smaller
proofs; canonical Goldilocks serde removes proof-byte malleability).
Proofs and verifying keys are not compatible with the previous pin.

Integration:

- Lookup gained max_multiplicity, a declared per-row bound on the
  multiplicity's integer magnitude feeding the newly enforced logUp
  height bound Σ wᵢ·hᵢ + |claims| < p. Function-circuit slots accumulate
  mutually-exclusive branch selectors, so they declare 1; committed
  count columns (function return slots, the memory circuit, the byte
  gadget tables) declare the new COUNT_COLUMN_BUDGET (2^32 queries per
  entry).
- The VK wire format carries the bound: u64 LE max_multiplicity per
  lookup, between the multiplicity node id and the arg count. The
  in-circuit VK deserializer (Ix/MultiStark/SystemDeserialize.lean)
  parses past it; the value is bound through the vk digest but the
  height bound itself is not yet enforced in-circuit (the native
  verifier enforces it).
- Message fingerprints are width-bound by default upstream (the slot
  width seeds the Horner fold), which is incompatible with aiur's
  branch-shared lookup slots: mutually exclusive branches superpose
  messages of different natural widths into one slot at the maximum
  width, so a narrow call is sent zero-padded to a width its callee's
  return slot never provides, and proving fails with
  UnbalancedChannel (pinned as the prove_verify_mismatched_call_widths
  regression). Aiur instead declares WidthBinding::ByConstruction —
  the plain Horner fold, restoring zero-padding transparency — and
  takes on the prefix-freeness contract that makes it sound: every
  message's natural width is a function of its constant-constrained
  leading prefix (channel tag plus discriminator: fun_idx fixes
  2+in+out, the memory size coordinate fixes 3+size, each gadget tag
  fixes its table width), so zero-extension can only equate a padded
  message with its own natural form. The contract is documented at the
  channel constants in lib.rs; the declaration is applied in
  AiurSystem::build and mirrored in the vk_codec decoder so decoded
  VKs replay the same transcript. ByConstruction is also exactly the
  fold the in-circuit verifier's logup_fingerprint already computes,
  so the recursive verifier needs no fingerprint change.
- The policy is Fiat-Shamir-bound as the first observe_shape word; the
  in-circuit transcript replay prepends the matching limb.
- aiur_multi_stark.rs regenerated (ix codegen) for the deserializer
  and transcript changes.

- P3 v0.6.0 ships FRI query openings as pruned Merkle multiproofs,
  while the in-circuit verifier consumes one authentication path per
  query (its per-query control flow is a far smaller circuit than the
  amortized multiproof walk). Rather than porting the walk into the
  DSL, the proof advice stays in the per-query transport: multi-stark's
  new advice module re-encodes a natively-verified proof by running
  p3's own verification with a recording compression function and
  reading each query's path back out of the recorded digest map. The
  advice bytes are untrusted verifier input, never digest-bound —
  the transcript binds the commitments and every expanded sibling is
  authenticated against them per query — so pruning vs expansion is
  pure transport and the encoding choice is sound. AiurSystem gains
  proof_to_advice_bytes (FFI: AiurSystem.proofToAdviceBytes); the
  recursive-verifier test feeds it instead of Proof.toBytes, whose
  native wire format is still round-tripped separately. The Lean-side
  proof grammar and the codegen'd verifier are byte-identical to
  before — no in-circuit changes.

Claim layout, the VK wire format above and aiur's public semantics are
otherwise unchanged; the policy adds no prover or verifier work over
the previous pin.

Still open, native-verifier-only: the logUp height bound is parsed
past but not yet enforced in-circuit (a wide-arithmetic check, tracked
separately).
@samuelburnham
Bump Blake3.lean and lean-ffi for Rust 1.98
74f9809 
The Lean v4.33.1 update pinned both dependencies at revisions that
predate their Rust 1.98 bumps; their heads now carry those bumps, which
this workspace needs since rust-toolchain.toml moved to 1.98. Both
revisions stay on leanprover/lean4:v4.33.1.

- Blake3.lean 1b0fbd2 → e6e908b (Rust 1.98, plus a case-insensitive
  source-directory fix), updated in lakefile.lean, lake-manifest.json
  and the blake3-lean flake input. The revision keeps the
  `blake3_rs_shared` target the `ix_native_decide_dynlib` pin requires.
  The inherited entry in Benchmarks/Compile/lake-manifest.json was still
  on the pre-4.33.1 revision and now tracks the root pin.
- lean-ffi 2a9c91e → 93c7e52 (Rust 1.98). Only bignat reaches the sp1
  and zisk workspaces, so their lock files move that one package.
@samuelburnham

samuelburnham commented Aug 24, 2026

Copy link
Copy Markdown
Member Author

!benchmark

@argument-ci-bot

argument-ci-bot Bot commented Aug 24, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

!benchmark — main vs 74f9809

backends: aiur=prove · envs: InitStd

aiur · InitStd · prove — main from: base run @ 68a50d3 (not on bencher)

7 constants · 0 with regressions · 7 with improvements (|Δ| > 3.0% on any metric).

IxVM on FRI (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 9.014 s 9.125 s +1.2% 30.764 s 29.486 s -4.2% 🟢 90.200 94.110 +4.3% 🟢 70.68 GiB 72.32 GiB +2.3% 11.33 MiB 11.07 MiB -2.3% 69.0 ms 64.1 ms -7.1% (1.08× faster) 🟢 134.35B 134.35B +0.0%
Char.ofOrdinal_le_of_le 6.963 s 6.853 s -1.6% 26.602 s 24.797 s -6.8% (1.07× faster) 🟢 103.860 111.420 +7.3% (1.07× faster) 🟢 63.85 GiB 65.39 GiB +2.4% 11.33 MiB 11.07 MiB -2.3% 79.9 ms 66.8 ms -16.4% (1.20× faster) 🟢 102.60B 102.60B +0.0%
Array.extract_append 6.631 s 6.685 s +0.8% 23.297 s 22.392 s -3.9% 🟢 68.940 71.720 +4.0% 🟢 52.00 GiB 52.76 GiB +1.5% 11.24 MiB 10.99 MiB -2.2% 74.5 ms 65.2 ms -12.5% (1.14× faster) 🟢 97.08B 97.08B +0.0%
Std.HashMap 4.057 s 4.083 s +0.6% 16.120 s 14.987 s -7.0% (1.08× faster) 🟢 126.680 136.250 +7.6% (1.08× faster) 🟢 36.28 GiB 37.04 GiB +2.1% 11.26 MiB 11.01 MiB -2.1% 76.5 ms 62.5 ms -18.2% (1.22× faster) 🟢 61.88B 61.88B +0.0%
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 3.618 s 3.612 s -0.2% 14.534 s 13.846 s -4.7% 🟢 128.460 134.840 +5.0% 🟢 33.93 GiB 34.72 GiB +2.3% 11.26 MiB 11.01 MiB -2.2% 70.9 ms 62.7 ms -11.5% (1.13× faster) 🟢 55.68B 55.68B +0.0%
String.append 433.8 ms 426.8 ms -1.6% 2.285 s 2.127 s -6.9% (1.07× faster) 🟢 143.100 153.740 +7.4% (1.07× faster) 🟢 4.88 GiB 4.92 GiB +0.8% 9.94 MiB 9.73 MiB -2.1% 63.4 ms 51.1 ms -19.5% (1.24× faster) 🟢 3.37B 3.37B +0.0%
Nat.add_comm 262.5 ms 260.5 ms -0.8% 1.061 s 999.5 ms -5.8% (1.06× faster) 🟢 43.360 46.030 +6.2% (1.06× faster) 🟢 4.61 GiB 4.57 GiB -1.0% 9.09 MiB 8.91 MiB -2.0% 54.7 ms 45.3 ms -17.1% (1.21× faster) 🟢 308.40M 308.40M +0.0%
FRI verifier on FRI (7 constants)
constant execute-time (main) execute-time (PR) Δ% prove-time (main) prove-time (PR) Δ% throughput (const/s) (main) throughput (const/s) (PR) Δ% peak-ram (main) peak-ram (PR) Δ% proof-size (main) proof-size (PR) Δ% verify-time (main) verify-time (PR) Δ% fft-cost (main) fft-cost (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 5.646 s n/a n/a 31.929 s n/a n/a 86.910 n/a n/a 100.08 GiB n/a n/a 3.97 MiB n/a n/a 26.1 ms n/a n/a 210.23B n/a n/a
Char.ofOrdinal_le_of_le 5.466 s n/a n/a 32.052 s n/a n/a 86.200 n/a n/a 99.25 GiB n/a n/a 3.97 MiB n/a n/a 25.0 ms n/a n/a 207.18B n/a n/a
Array.extract_append 5.297 s n/a n/a 30.552 s n/a n/a 52.570 n/a n/a 94.65 GiB n/a n/a 3.97 MiB n/a n/a 24.7 ms n/a n/a 200.65B n/a n/a
Std.HashMap 5.326 s n/a n/a 30.546 s n/a n/a 66.850 n/a n/a 94.70 GiB n/a n/a 3.97 MiB n/a n/a 24.6 ms n/a n/a 203.35B n/a n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 5.427 s n/a n/a 31.479 s n/a n/a 59.310 n/a n/a 98.48 GiB n/a n/a 3.97 MiB n/a n/a 25.3 ms n/a n/a 205.59B n/a n/a
String.append 4.426 s n/a n/a 27.931 s n/a n/a 11.710 n/a n/a 87.81 GiB n/a n/a 3.97 MiB n/a n/a 24.5 ms n/a n/a 168.67B n/a n/a
Nat.add_comm 3.559 s n/a n/a 18.907 s n/a n/a 2.430 n/a n/a 58.66 GiB n/a n/a 3.97 MiB n/a n/a 24.7 ms n/a n/a 130.84B n/a n/a
Pipeline total (7 constants)
constant total-time (main) total-time (PR) Δ% pipeline-throughput (const/s) (main) pipeline-throughput (const/s) (PR) Δ% pipeline-peak-ram (main) pipeline-peak-ram (PR) Δ%
ByteArray.utf8DecodeChar?_utf8EncodeChar_append 1m 2.7s n/a n/a 44.260 n/a n/a 100.08 GiB n/a n/a
Char.ofOrdinal_le_of_le 58.654 s n/a n/a 47.110 n/a n/a 99.25 GiB n/a n/a
Array.extract_append 53.850 s n/a n/a 29.820 n/a n/a 94.65 GiB n/a n/a
Std.HashMap 46.666 s n/a n/a 43.760 n/a n/a 94.70 GiB n/a n/a
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq 46.013 s n/a n/a 40.580 n/a n/a 98.48 GiB n/a n/a
String.append 30.216 s n/a n/a 10.820 n/a n/a 87.81 GiB n/a n/a
Nat.add_comm 19.967 s n/a n/a 2.300 n/a n/a 58.66 GiB n/a n/a

Workflow logs

@samuelburnham
bench: feed the recursive phase advice bytes, fix RecursionDebug's claim
bef1a81 
The !benchmark recursive phase reported n/a for every fri-verifier
metric: Benchmarks/Typecheck.lean still fed Proof.toBytes — the pruned
multiproof wire format — to executeMultiStark/proveMultiStark, so the
in-circuit verifier rejected on parse and the harness (correctly) left
the recursive fields absent rather than emit a fake datum. The
in-circuit verifier consumes the per-query advice transport
(AiurSystem.proofToAdviceBytes); proofBytes stays the reported
proof-size metric.

bench-recursion-debug had the same advice-format gap plus a stale
claim recipe: it still built the public input as 32 raw digest bytes,
predating the ClaimHarness.packedDigestKey packing bench-typecheck
uses (its own out-of-circuit sanity check failed with
InvalidPowWitness — a wrong claim diverges every challenge — and the
advice re-encoder refused the proof for the same reason). Both aligned
with the typecheck flow.

Validated end-to-end at production parameters (numQueries 100,
query PoW 20, blowup 2) on Nat.add_comm: inner prove, advice
re-encoding, and the codegen'd in-circuit verifier accepting.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@samuelburnham