From 5c87056e228fb83c1ea496fce97633532b7d428c Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Thu, 23 Jul 2026 12:53:46 -0300 Subject: [PATCH] =?UTF-8?q?params:=20blowup=204=20+=2020-bit=20query=20gri?= =?UTF-8?q?nding=20=E2=80=94=20proven=20soundness=20regime?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- Benchmarks/Aiur.lean | 6 +++--- Benchmarks/Blake3.lean | 6 +++--- Benchmarks/IxVM.lean | 6 +++--- Benchmarks/Sha256.lean | 6 +++--- Benchmarks/Typecheck.lean | 10 +++++----- Ix/Cli/ProveCmd.lean | 6 +++--- Ix/Cli/VerifyCmd.lean | 6 +++--- Tests/Aiur/Common.lean | 6 +++--- 8 files changed, 26 insertions(+), 26 deletions(-) diff --git a/Benchmarks/Aiur.lean b/Benchmarks/Aiur.lean index adda1d460..931d855a6 100644 --- a/Benchmarks/Aiur.lean +++ b/Benchmarks/Aiur.lean @@ -52,7 +52,7 @@ def toplevel := ⟦ ⟧ def commitmentParameters : Aiur.CommitmentParameters := { - logBlowup := 1 + logBlowup := 2 capHeight := 0 } @@ -60,8 +60,8 @@ def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } -- Stages the e2e proving pipeline through `benchStep`: each call times a stage diff --git a/Benchmarks/Blake3.lean b/Benchmarks/Blake3.lean index d8d047724..ebf23c739 100644 --- a/Benchmarks/Blake3.lean +++ b/Benchmarks/Blake3.lean @@ -11,7 +11,7 @@ abbrev dataSizes := #[64, 128, 256, 512, 1024, 2048] abbrev numHashesPerProof := #[1, 2, 4, 8, 16, 32] def commitmentParameters : Aiur.CommitmentParameters := { - logBlowup := 1 + logBlowup := 2 capHeight := 0 } @@ -19,8 +19,8 @@ def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } def mergedToplevel : Except Aiur.Global Aiur.Source.Toplevel := do diff --git a/Benchmarks/IxVM.lean b/Benchmarks/IxVM.lean index d288aa6ee..ffb463369 100644 --- a/Benchmarks/IxVM.lean +++ b/Benchmarks/IxVM.lean @@ -7,7 +7,7 @@ import Ix.Benchmark.Bench open BgroupM def commitmentParameters : Aiur.CommitmentParameters := { - logBlowup := 1 + logBlowup := 2 capHeight := 0 } @@ -15,8 +15,8 @@ def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } def main : IO Unit := do diff --git a/Benchmarks/Sha256.lean b/Benchmarks/Sha256.lean index 96c780d4d..86e08a28c 100644 --- a/Benchmarks/Sha256.lean +++ b/Benchmarks/Sha256.lean @@ -11,7 +11,7 @@ abbrev dataSizes := #[64, 128, 256, 512, 1024, 2048] abbrev numHashesPerProof := #[1, 2, 4, 8, 16, 32] def commitmentParameters : Aiur.CommitmentParameters := { - logBlowup := 1 + logBlowup := 2 capHeight := 0 } @@ -19,8 +19,8 @@ def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } def mergedToplevel : Except Aiur.Global Aiur.Source.Toplevel := do diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 1462fa601..3fa65bfc4 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -106,7 +106,7 @@ bencher-specific reshaping is the caller's job (see open Lean (Json Name) def commitmentParameters : Aiur.CommitmentParameters := { - logBlowup := 1 + logBlowup := 2 capHeight := 0 } @@ -114,8 +114,8 @@ def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } /-- Recursion-tuned commitment parameters for `--recursive`, matching @@ -136,8 +136,8 @@ def recursiveFriParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index 183b39209..6319c362f 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -48,14 +48,14 @@ namespace Ix.Cli.ProveCmd proof header, they MUST stay in sync between `prove` and `verify`. -/ private def commitmentParameters : Aiur.CommitmentParameters := - { logBlowup := 1, capHeight := 0 } + { logBlowup := 2, capHeight := 0 } private def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } def proveOne (aiurSystem : Aiur.AiurSystem) diff --git a/Ix/Cli/VerifyCmd.lean b/Ix/Cli/VerifyCmd.lean index 634028410..f24bcb623 100644 --- a/Ix/Cli/VerifyCmd.lean +++ b/Ix/Cli/VerifyCmd.lean @@ -37,14 +37,14 @@ private def addrOfHex! (label : String) (s : String) : IO Address := do silently with no useful diagnostic, so these MUST match the proving side until they migrate into the proof header. -/ private def commitmentParameters : Aiur.CommitmentParameters := - { logBlowup := 1, capHeight := 0 } + { logBlowup := 2, capHeight := 0 } private def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } /-- Verify one persisted `Ixon.Proof` wrapper (by store address) against its diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean index 8f17b28fb..b7fc720b3 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -36,7 +36,7 @@ def AiurTestCase.exec (functionName : Lean.Name) { functionName, input, expectedOutput, interpret := false, executionOnly := true } def commitmentParameters : Aiur.CommitmentParameters := { - logBlowup := 1 + logBlowup := 2 capHeight := 0 } @@ -44,8 +44,8 @@ def friParameters : Aiur.FriParameters := { logFinalPolyLen := 0 maxLogArity := 1 numQueries := 100 - commitProofOfWorkBits := 20 - queryProofOfWorkBits := 0 + commitProofOfWorkBits := 0 + queryProofOfWorkBits := 20 } structure AiurTestEnv where