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