Skip to content

params: blowup 4 + 20-bit query grinding — proven soundness regime #513

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gabriel-barrett merged 1 commit into from
Jul 23, 2026
Merged

params: blowup 4 + 20-bit query grinding — proven soundness regime #513

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Benchmarks/Aiur.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,16 +52,16 @@ def toplevel := ⟦
⟧

def commitmentParameters : Aiur.CommitmentParameters := {
logBlowup := 1
logBlowup := 2
capHeight := 0
}

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
Expand Down
6 changes: 3 additions & 3 deletions Benchmarks/Blake3.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,16 +11,16 @@ 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
}

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
Expand Down
6 changes: 3 additions & 3 deletions Benchmarks/IxVM.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,16 @@ import Ix.Benchmark.Bench
open BgroupM

def commitmentParameters : Aiur.CommitmentParameters := {
logBlowup := 1
logBlowup := 2
capHeight := 0
}

def friParameters : Aiur.FriParameters := {
logFinalPolyLen := 0
maxLogArity := 1
numQueries := 100
commitProofOfWorkBits := 20
queryProofOfWorkBits := 0
commitProofOfWorkBits := 0
queryProofOfWorkBits := 20
}

def main : IO Unit := do
Expand Down
6 changes: 3 additions & 3 deletions Benchmarks/Sha256.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,16 +11,16 @@ 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
}

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
Expand Down
10 changes: 5 additions & 5 deletions Benchmarks/Typecheck.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,16 +106,16 @@ bencher-specific reshaping is the caller's job (see
open Lean (Json Name)

def commitmentParameters : Aiur.CommitmentParameters := {
logBlowup := 1
logBlowup := 2
capHeight := 0
}

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
Expand All @@ -136,8 +136,8 @@ def recursiveFriParameters : Aiur.FriParameters := {
logFinalPolyLen := 0
maxLogArity := 1
numQueries := 100
commitProofOfWorkBits := 20
queryProofOfWorkBits := 0
commitProofOfWorkBits := 0
queryProofOfWorkBits := 20
}


Expand Down
6 changes: 3 additions & 3 deletions Ix/Cli/ProveCmd.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
6 changes: 3 additions & 3 deletions Ix/Cli/VerifyCmd.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions Tests/Aiur/Common.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,16 +36,16 @@ def AiurTestCase.exec (functionName : Lean.Name)
{ functionName, input, expectedOutput, interpret := false, executionOnly := true }

def commitmentParameters : Aiur.CommitmentParameters := {
logBlowup := 1
logBlowup := 2
capHeight := 0
}

def friParameters : Aiur.FriParameters := {
logFinalPolyLen := 0
maxLogArity := 1
numQueries := 100
commitProofOfWorkBits := 20
queryProofOfWorkBits := 0
commitProofOfWorkBits := 0
queryProofOfWorkBits := 20
}

structure AiurTestEnv where
Expand Down