chore: Update multi stark - #588
Conversation
10d1cda to
74f9809
Compare
|
!benchmark |
|
| 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 |
- 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.
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).
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.
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.
Advance Aiur to the companion multi-stark branch that retains the Plonky3 v0.6 protocol updates while improving the CUDA prover's memory envelope and resident Merkle gathering. Refresh Cargo.lock to the same exact revision. Keep the Rust 1.98 warnings-denied build clean by replacing two map(...).unwrap_or(0) expressions with the equivalent Result::map_or form. The q50 Vector.extract_append workload measures 3.70 s for inner STARK proving and 6.79 s for outer STARK proving on the RTX PRO 6000 Blackwell (10.49 s combined), versus approximately 71.6-71.9 s for the CPU proving-only baseline, or roughly 6.85x. The full recursive phases measure 13.01 s inner and 15.85 s outer; proof sizes remain 11,553,785 and 3,921,721 bytes. Validated with the release CPU and CUDA workspace tests, release CPU and CUDA clippy with warnings denied, rustfmt, and diff checks.
bef1a81 to
3fd0a58
Compare
|
!benchmark fresh |
|
|
!benchmark fresh |
|
Fresh PR comparisons rebuild the base checkout, but the benchmark job only provisions Lean before Lake invokes Cargo. Install the Rust channel pinned by the base checkout when its binaries are not cached. PR benchmarks dispatch trusted workflow YAML from the default branch, so a workflow-only fix cannot repair the PR that carries it. Bootstrap the same toolchain from the PR-local CPU provenance action that the trusted workflow already invokes before the base build; it becomes a no-op once the explicit workflow step lands.
f2eb4a8 to
d6e5085
Compare
|
!benchmark aiur fresh |
|
| 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 |
8.738 s | 💥 CRASH | n/a | 44.110 s | 💥 CRASH | n/a | 62.910 | 💥 CRASH | n/a | 70.77 GiB | 💥 CRASH | n/a | 11.33 MiB | 💥 CRASH | n/a | 76.7 ms | 💥 CRASH | n/a | 134.35B | 💥 CRASH | n/a |
Char.ofOrdinal_le_of_le |
6.534 s | 💥 CRASH | n/a | 38.173 s | 💥 CRASH | n/a | 72.380 | 💥 CRASH | n/a | 63.77 GiB | 💥 CRASH | n/a | 11.33 MiB | 💥 CRASH | n/a | 76.7 ms | 💥 CRASH | n/a | 102.60B | 💥 CRASH | n/a |
Array.extract_append |
6.374 s | 💥 CRASH | n/a | 33.133 s | 💥 CRASH | n/a | 48.470 | 💥 CRASH | n/a | 51.96 GiB | 💥 CRASH | n/a | 11.24 MiB | 💥 CRASH | n/a | 85.1 ms | 💥 CRASH | n/a | 97.08B | 💥 CRASH | n/a |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
3.710 s | 💥 CRASH | n/a | 20.768 s | 💥 CRASH | n/a | 89.900 | 💥 CRASH | n/a | 33.93 GiB | 💥 CRASH | n/a | 11.26 MiB | 💥 CRASH | n/a | 79.5 ms | 💥 CRASH | n/a | 55.68B | 💥 CRASH | n/a |
Std.HashMap |
4.043 s | 💥 CRASH | n/a | 22.523 s | 💥 CRASH | n/a | 90.660 | 💥 CRASH | n/a | 36.29 GiB | 💥 CRASH | n/a | 11.26 MiB | 💥 CRASH | n/a | 89.6 ms | 💥 CRASH | n/a | 61.88B | 💥 CRASH | n/a |
String.append |
711.7 ms | 💥 CRASH | n/a | 2.891 s | 💥 CRASH | n/a | 113.100 | 💥 CRASH | n/a | 4.90 GiB | 💥 CRASH | n/a | 9.94 MiB | 💥 CRASH | n/a | 70.2 ms | 💥 CRASH | n/a | 3.37B | 💥 CRASH | n/a |
Nat.add_comm |
503.2 ms | 💥 CRASH | n/a | 1.349 s | 💥 CRASH | n/a | 34.100 | 💥 CRASH | n/a | 4.58 GiB | 💥 CRASH | n/a | 9.09 MiB | 💥 CRASH | n/a | 58.2 ms | 💥 CRASH | n/a | 308.40M | 💥 CRASH | n/a |
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 |
6.765 s | 💥 CRASH | n/a | 54.295 s | 💥 CRASH | n/a | 51.110 | 💥 CRASH | n/a | 100.92 GiB | 💥 CRASH | n/a | 3.97 MiB | 💥 CRASH | n/a | 47.5 ms | 💥 CRASH | n/a | 210.23B | 💥 CRASH | n/a |
Char.ofOrdinal_le_of_le |
6.615 s | 💥 CRASH | n/a | 53.190 s | 💥 CRASH | n/a | 51.950 | 💥 CRASH | n/a | 100.17 GiB | 💥 CRASH | n/a | 3.97 MiB | 💥 CRASH | n/a | 41.2 ms | 💥 CRASH | n/a | 207.18B | 💥 CRASH | n/a |
Array.extract_append |
6.412 s | 💥 CRASH | n/a | 50.993 s | 💥 CRASH | n/a | 31.490 | 💥 CRASH | n/a | 94.89 GiB | 💥 CRASH | n/a | 3.97 MiB | 💥 CRASH | n/a | 47.9 ms | 💥 CRASH | n/a | 200.65B | 💥 CRASH | n/a |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
6.429 s | 💥 CRASH | n/a | 53.021 s | 💥 CRASH | n/a | 35.210 | 💥 CRASH | n/a | 98.71 GiB | 💥 CRASH | n/a | 3.97 MiB | 💥 CRASH | n/a | 34.5 ms | 💥 CRASH | n/a | 205.59B | 💥 CRASH | n/a |
Std.HashMap |
6.503 s | 💥 CRASH | n/a | 51.063 s | 💥 CRASH | n/a | 39.990 | 💥 CRASH | n/a | 95.25 GiB | 💥 CRASH | n/a | 3.97 MiB | 💥 CRASH | n/a | 49.3 ms | 💥 CRASH | n/a | 203.35B | 💥 CRASH | n/a |
String.append |
5.477 s | 💥 CRASH | n/a | 47.468 s | 💥 CRASH | n/a | 6.890 | 💥 CRASH | n/a | 87.84 GiB | 💥 CRASH | n/a | 3.97 MiB | 💥 CRASH | n/a | 32.6 ms | 💥 CRASH | n/a | 168.67B | 💥 CRASH | n/a |
Nat.add_comm |
4.257 s | 💥 CRASH | n/a | 31.155 s | 💥 CRASH | n/a | 1.480 | 💥 CRASH | n/a | 58.71 GiB | 💥 CRASH | n/a | 3.97 MiB | 💥 CRASH | n/a | 28.0 ms | 💥 CRASH | n/a | 130.84B | 💥 CRASH | 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 38.4s | 💥 CRASH | n/a | 28.200 | 💥 CRASH | n/a | 100.92 GiB | 💥 CRASH | n/a |
Char.ofOrdinal_le_of_le |
1m 31.4s | 💥 CRASH | n/a | 30.240 | 💥 CRASH | n/a | 100.17 GiB | 💥 CRASH | n/a |
Array.extract_append |
1m 24.1s | 💥 CRASH | n/a | 19.090 | 💥 CRASH | n/a | 94.89 GiB | 💥 CRASH | n/a |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
1m 13.8s | 💥 CRASH | n/a | 25.300 | 💥 CRASH | n/a | 98.71 GiB | 💥 CRASH | n/a |
Std.HashMap |
1m 13.6s | 💥 CRASH | n/a | 27.750 | 💥 CRASH | n/a | 95.25 GiB | 💥 CRASH | n/a |
String.append |
50.360 s | 💥 CRASH | n/a | 6.490 | 💥 CRASH | n/a | 87.84 GiB | 💥 CRASH | n/a |
Nat.add_comm |
32.504 s | 💥 CRASH | n/a | 1.420 | 💥 CRASH | n/a | 58.71 GiB | 💥 CRASH | n/a |
Companion PR for argumentcomputer/multi-stark#74