params: blowup 4 + 20-bit query grinding — proven soundness regime - #513
Merged
Conversation
Move the Aiur STARK parameters from (log_blowup = 1, commit_pow = 20, query_pow = 0) to (log_blowup = 2, commit_pow = 0, query_pow = 20), targeting the PROVEN FRI soundness bound within the unique decoding radius instead of the list-decoding-capacity conjecture. Why: at rate rho = 2^-log_blowup, FRI's per-query soundness is only proven up to the unique decoding radius delta = (1 - rho)/2, giving a per-query error of 1 - delta = (1 + rho)/2. At log_blowup = 1 that is 3/4 per query — 0.415 bits — so 100 queries yield only ~41 bits proven. At log_blowup = 2 the per-query error is 5/8 — 0.678 bits — so the same 100 queries yield ~68 bits, plus 20 bits of query grinding: ~88 bits of proven security (and 200+ bits, capped by the ~2^-100 field terms, under the capacity conjecture). Query grinding (2^20 work immediately before query sampling) adds its bits one-for-one to the query-phase error, which is the dominant term of the union bound; it costs the honest prover a one-off ~1M hashes. Commit grinding drops to 0: the commit-phase error terms (FRI folding challenges, constraint folding, lookup collisions) are bounded by the size of the degree-2 Goldilocks extension at roughly 2^-100 — orders of magnitude below the ~2^-88 query phase — so grinding them buys no measurable security and only slows honest proving. The doubled blowup also raises the supported constraint degree from 3 to 5, which the upcoming logup message-grouping change relies on. Benchmarks/RecursiveVerifier.lean and Tests/MultiStark.lean keep their old parameters: the Lean recursive verifier hardcodes query_pow = 0 (Ix/MultiStark.lean) and is ported separately.
Member
Author
|
!benchmark |
Member
|
!benchmark aiur-recursive |
Contributor
|
| 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 |
39.435 s | 48.544 s | +23.1% (1.23× slower) |
43.260 | 35.140 | -18.8% (1.23× slower) |
58.47 GiB | 96.66 GiB | +65.3% (1.65× larger) |
10.371 s | 10.384 s | +0.1% | 173.5 ms | 258.9 ms | +49.3% (1.49× slower) |
26.22 MiB | 26.30 MiB | +0.3% | 36.16B | 36.16B | +0.0% |
ByteArray.utf8DecodeChar?_utf8EncodeChar_append |
38.821 s | 48.388 s | +24.6% (1.25× slower) |
74.440 | 59.730 | -19.8% (1.25× slower) |
64.25 GiB | 102.38 GiB | +59.4% (1.59× larger) |
9.279 s | 9.176 s | -1.1% | 169.0 ms | 184.3 ms | +9.0% (1.09× slower) |
26.30 MiB | 26.39 MiB | +0.3% | 38.09B | 38.09B | +0.0% |
Char.ofOrdinal_le_of_le |
30.658 s | 38.552 s | +25.7% (1.26× slower) |
93.350 | 74.240 | -20.5% (1.26× slower) |
49.55 GiB | 80.19 GiB | +61.8% (1.62× larger) |
6.760 s | 6.724 s | -0.5% | 170.4 ms | 230.7 ms | +35.3% (1.35× slower) |
26.24 MiB | 26.32 MiB | +0.3% | 29.13B | 29.13B | +0.0% |
Vector.extract_append._proof_2 |
22.813 s | 27.991 s | +22.7% (1.23× slower) |
63.170 | 51.480 | -18.5% (1.23× slower) |
34.93 GiB | 53.23 GiB | +52.4% (1.52× larger) |
5.845 s | 5.792 s | -0.9% | 169.1 ms | 175.8 ms | +3.9% |
25.89 MiB | 25.97 MiB | +0.3% | 21.16B | 21.16B | +0.0% |
_private.Init.Data.Range.Polymorphic.SInt.0.Int64.instRxcHasSize_eq |
18.662 s | 23.858 s | +27.8% (1.28× slower) |
105.720 | 82.700 | -21.8% (1.28× slower) |
31.58 GiB | 50.26 GiB | +59.1% (1.59× larger) |
3.452 s | 3.470 s | +0.5% | 174.1 ms | 166.3 ms | -4.5% 🟢 | 26.06 MiB | 26.14 MiB | +0.3% | 15.70B | 15.70B | +0.0% |
String.split |
17.726 s | 22.275 s | +25.7% (1.26× slower) |
109.950 | 87.500 | -20.4% (1.26× slower) |
30.85 GiB | 48.22 GiB | +56.3% (1.56× larger) |
3.098 s | 3.167 s | +2.2% | 190.0 ms | 170.0 ms | -10.5% (1.12× faster) 🟢 | 26.22 MiB | 26.30 MiB | +0.3% | 14.21B | 14.21B | +0.0% |
List.mergeSort |
12.510 s | 15.487 s | +23.8% (1.24× slower) |
127.740 | 103.180 | -19.2% (1.24× slower) |
19.82 GiB | 31.80 GiB | +60.5% (1.60× larger) |
2.249 s | 2.279 s | +1.4% | 186.0 ms | 171.6 ms | -7.7% (1.08× faster) 🟢 | 26.11 MiB | 26.19 MiB | +0.3% | 10.45B | 10.45B | +0.0% |
Vector.append |
4.326 s | 5.187 s | +19.9% (1.20× slower) |
130.850 | 109.120 | -16.6% (1.20× slower) |
6.56 GiB | 8.36 GiB | +27.3% (1.27× larger) |
593.6 ms | 596.5 ms | +0.5% | 167.4 ms | 168.7 ms | +0.8% | 24.71 MiB | 24.78 MiB | +0.3% | 2.21B | 2.21B | +0.0% |
Nat.gcd_comm |
3.586 s | 4.392 s | +22.5% (1.22× slower) |
115.720 | 94.480 | -18.4% (1.22× slower) |
5.12 GiB | 7.57 GiB | +47.6% (1.48× larger) |
472.9 ms | 472.7 ms | -0.0% | 153.4 ms | 154.0 ms | +0.4% | 24.32 MiB | 24.39 MiB | +0.3% | 1.56B | 1.56B | +0.0% |
String.append |
2.740 s | 3.270 s | +19.3% (1.19× slower) |
128.810 | 107.960 | -16.2% (1.19× slower) |
6.11 GiB | 5.09 GiB | -16.6% (1.20× smaller) 🟢 | 357.4 ms | 353.4 ms | -1.1% | 147.7 ms | 165.7 ms | +12.2% (1.12× slower) |
23.57 MiB | 23.64 MiB | +0.3% | 868.67M | 868.67M | +0.0% |
Int.gcd |
2.268 s | 2.674 s | +17.9% (1.18× slower) |
100.950 | 85.650 | -15.2% (1.18× slower) |
4.79 GiB | 4.84 GiB | +1.0% | 292.1 ms | 291.1 ms | -0.3% | 147.6 ms | 151.3 ms | +2.5% | 23.22 MiB | 23.29 MiB | +0.3% | 539.07M | 539.07M | +0.0% |
Nat.sub_le_of_le_add |
2.137 s | 2.508 s | +17.4% (1.17× slower) |
88.930 | 75.750 | -14.8% (1.17× slower) |
4.88 GiB | 4.91 GiB | +0.6% | 282.8 ms | 278.0 ms | -1.7% | 148.5 ms | 153.3 ms | +3.2% |
23.70 MiB | 23.77 MiB | +0.3% | 451.52M | 451.52M | +0.0% |
Nat.add_comm |
1.173 s | 1.416 s | +20.7% (1.21× slower) |
43.480 | 36.010 | -17.2% (1.21× slower) |
5.06 GiB | 3.91 GiB | -22.7% (1.29× smaller) 🟢 | 195.5 ms | 194.5 ms | -0.5% | 151.2 ms | 136.9 ms | -9.4% (1.10× faster) 🟢 | 22.15 MiB | 22.21 MiB | +0.3% | 48.90M | 48.90M | +0.0% |
Std.Tactic.BVDecide.BVExpr.bitblast.goCache_Inv_of_Inv._mutual |
OOM | OOM | n/a | OOM | OOM | n/a | OOM | OOM | n/a | 54.726 s | 55.464 s | +1.3% | OOM | OOM | n/a | OOM | OOM | n/a | 205.13B | 205.13B | +0.0% |
14 constants · 13 with regressions · 5 with improvements (|Δ| > 3.0% on any metric).
Contributor
|
| 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.960 s | 4.867 s | -1.9% | 14.60 GiB | 14.57 GiB | -0.2% | 11.39 MiB | 11.39 MiB | +0.0% | 75.8 ms | 73.8 ms | -2.7% | 465.8 ms | 439.9 ms | -5.6% (1.06× faster) 🟢 | 3.94B | 3.81B | -3.2% 🟢 | 172.8 ms | 188.4 ms | +9.0% (1.09× slower) |
848.62 KiB | 848.62 KiB | +0.0% | 6.6 ms | 6.8 ms | +3.0% | 363.64 MiB | 364.89 MiB | +0.3% |
square-q100-b1 |
3.716 s | 3.781 s | +1.8% | 9.69 GiB | 9.64 GiB | -0.5% | 11.32 MiB | 11.32 MiB | +0.0% | 75.6 ms | 74.0 ms | -2.1% | 404.7 ms | 402.9 ms | -0.4% | 3.38B | 3.28B | -2.9% | 169.8 ms | 197.8 ms | +16.5% (1.16× slower) |
782.06 KiB | 782.06 KiB | +0.0% | 6.0 ms | 5.6 ms | -5.8% (1.06× faster) 🟢 | 271.71 MiB | 272.91 MiB | +0.4% |
2 proofs · 2 with regressions · 2 with improvements (|Δ| > 3.0% on any metric).
arthurpaulino
approved these changes
Jul 23, 2026
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
2 participants
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.
STARK parameters: blowup 4 + 20-bit query grinding — proven soundness regime
Moves the Aiur STARK parameters from
to
so that the security level is backed by the proven FRI soundness bound
within the unique decoding radius, instead of the list-decoding-capacity
conjecture.
Why
At rate
ρ = 2^-log_blowup, FRI's per-query soundness is only proven up tothe unique decoding radius
δ = (1 − ρ)/2, giving a per-query error of1 − δ = (1 + ρ)/2:log_blowup = 1(old)log_blowup = 2(new)Under the usual capacity conjecture the same parameters give 200+ bits,
capped by the ~2⁻¹⁰⁰ field-size terms of the union bound — so the change
costs nothing in the conjectured regime and buys a defensible proven number.
Query grinding (0 → 20 bits). Grinding immediately before query sampling
adds its bits one-for-one to the query-phase error — the dominant term of the
union bound. Honest-prover cost: a one-off ~2²⁰ hashes (milliseconds).
Commit grinding (20 → 0 bits). The commit-phase error terms (FRI folding
challenges, constraint folding α, lookup collisions) are Schwartz–Zippel
bounds against the degree-2 Goldilocks extension, sitting around 2⁻¹⁰⁰ —
orders of magnitude below the ~2⁻⁸⁸ query phase in every regime, proven or
conjectured. Grinding them adds no measurable security; it only slowed honest
proving (2²⁰ work per FRI fold round). Dropping it to 0 keeps the parameter
honest rather than decorative.
Costs and side effects
each Merkle path gains one hash. This is the price of the proven regime.
(
2^log_blowup + 1), headroom the upcoming logup message-grouping changerelies on.
conjectured) makes queries cheaper per bit, opening room to later trade
query count against grinding for smaller proofs.
Scope
Parameter definitions only:
Tests/Aiur/Common.lean,Ix/Cli/ProveCmd.lean,Ix/Cli/VerifyCmd.lean, and theBenchmarks/{Aiur,Blake3,IxVM,Sha256, Typecheck}.leanconfigs.Benchmarks/RecursiveVerifier.leanandTests/MultiStark.leanintentionallykeep the old parameters: the Lean recursive verifier hardcodes
query_pow = 0as a protocol assumption (Ix/MultiStark.lean) and is beingported separately.