perf: Switch Aiur from Keccak to Blake3 hashing

Benchmarks/Aiur.lean

@@ -86,9 +86,9 @@ def main : IO Unit := do
     countInE2E
     let compiled ← benchStepE "compile" Aiur.Source.Toplevel.compile toplevel
     let system ← benchStep "build AiurSystem"
-        (Aiur.AiurSystem.build compiled.bytecode) commitmentParameters
+        (Aiur.AiurSystem.build compiled.bytecode commitmentParameters) friParameters
     let funIdx := compiled.getFuncIdx `main |>.get!
     let (claim, proof, _) ← benchStep "prove fib 10"
-        (Aiur.AiurSystem.prove system friParameters funIdx #[10]) default (oneShot := true)
+        (Aiur.AiurSystem.prove system funIdx #[10]) default (oneShot := true)
     let _ ← benchStepE "verify fib 10"
-        (Aiur.AiurSystem.verify system friParameters claim) proof
+        (Aiur.AiurSystem.verify system claim) proof

Benchmarks/Blake3.lean

@@ -34,7 +34,7 @@ def blake3Bench : IO $ Array BenchReport := do
     | throw (IO.userError "Compilation failed")
   let some funIdx := compiled.getFuncIdx `blake3_bench
     | throw (IO.userError "Aiur function not found")
-  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
+  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters
   bgroup "prove blake3" { oneShot := true, avgThroughput := true, report := true } do
     for dataSize in dataSizes do
       for numHashes in numHashesPerProof do
@@ -47,7 +47,7 @@ def blake3Bench : IO $ Array BenchReport := do
             ioBuffer.extend 0 #[.ofNat idx] data
         throughput (.ElementsAndBytes numHashes.toUInt64 (dataSize * numHashes).toUInt64 "hashes")
         bench s!"dataSize={dataSize} numHashes={numHashes}"
-          (aiurSystem.prove friParameters funIdx #[Aiur.G.ofNat numHashes]) ioBuffer
+          (aiurSystem.prove funIdx #[Aiur.G.ofNat numHashes]) ioBuffer
 
 def main : IO Unit := do
   let _ ← blake3Bench

Benchmarks/IxVM.lean

@@ -26,7 +26,7 @@ def main : IO Unit := do
     | throw (IO.userError "Compilation failed")
   let some funIdx := compiled.getFuncIdx `ixon_serde_blake3_bench
     | throw (IO.userError "Aiur function not found")
-  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
+  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters
 
   let env ← get_env!
   let ixonEnv ← IxVM.ClaimHarness.loadIxonEnv ``Nat.add_comm env
@@ -37,6 +37,6 @@ def main : IO Unit := do
     -- IxVM-native prove: routes execution through the codegen'd Rust
     -- kernel (`execute_generated`) instead of the bytecode interpreter.
     bench "serde/blake3 Nat.add_comm"
-      (aiurSystem.proveIxVM friParameters funIdx #[.ofNat n])
+      (aiurSystem.proveIxVM funIdx #[.ofNat n])
       ioBuffer
   return

Benchmarks/RecursiveVerifier.lean

@@ -18,11 +18,13 @@ of `Tests/MultiStark.lean::endToEndSuite`, but measures cost instead of
 asserting accept/reject.
 
 ```
-lake exe bench-recursive-verifier                 # factorial(5), q=3, blowup 2
+lake exe bench-recursive-verifier                 # factorial(5), q=100 (soundness level — heavy)
+lake exe bench-recursive-verifier --queries 3     # cheap local run (toy soundness)
 lake exe bench-recursive-verifier --execute-only  # skip the outer prove (FFT/exec only)
 
   --trivial        square(5) instead of factorial(5) — the per-statement floor
-  --queries N      FRI query count        (default 3)
+  --queries N      FRI query count (default 100 = soundness level; pass a
+                   small value for a cheap local run)
   --blowup N       log2 blowup            (default 2)
   --pow N          commit PoW bits        (default 20)
   --json <path>    write a benchmark results row (Ix.Benchmark.Results); the
@@ -82,7 +84,7 @@ def recCommitParams (args : List String) : Aiur.CommitmentParameters :=
   { logBlowup := argNat args "--blowup" 2, capHeight := 0 }
 def innerFri (args : List String) : Aiur.FriParameters :=
   { logFinalPolyLen := argNat args "--final-poly" 0, maxLogArity := 1,
-    numQueries := argNat args "--queries" 3,
+    numQueries := argNat args "--queries" 100,
     commitProofOfWorkBits := argNat args "--pow" 20, queryProofOfWorkBits := 0 }
 
 def secs (t0 t1 : Nat) : Float := (Float.ofNat (t1 - t0)) / 1e9
@@ -116,15 +118,15 @@ def main (args : List String) : IO UInt32 := do
   let facCompiled ← match program.compile with
     | .ok c => pure c
     | .error e => IO.eprintln s!"inner compile failed: {e}"; return 1
-  let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams
+  let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams innerFri
   let facIdx := facCompiled.getFuncIdx entry |>.get!
   IO.println s!"proving inner {entry}(5)…"
   TracingTexray.resetPeakTreeRss
   let it0 ← IO.monoNanosNow
-  let (claim, proof, _) := facSystem.prove innerFri facIdx #[Aiur.G.ofNat 5] default
+  let (claim, proof, _) := facSystem.prove facIdx #[Aiur.G.ofNat 5] default
   let proofBytes := proof.toBytes
   let it1 ← IO.monoNanosNow
-  let innerOk := facSystem.verify innerFri claim proof matches .ok _
+  let innerOk := facSystem.verify claim proof matches .ok _
   let it2 ← IO.monoNanosNow
   let innerPeak ← TracingTexray.peakTreeRssBytes
   IO.println s!"inner PROVE: {secs it0 it1} s, \
@@ -134,7 +136,7 @@ def main (args : List String) : IO UInt32 := do
     IO.eprintln "inner proof failed to verify"
     return 1
   -- Proof (advice, channel 0), vk (channel 1), claims (channel 2), plus the
-  -- Keccak-bound vk/claims digests and FRI params as public input.
+  -- Blake3-bound vk/claims digests and FRI params as public input.
   let claimBytes := MultiStark.serializeClaims #[claim]
   let (pubInput, io) := MultiStark.verifierInput proofBytes facSystem.vkBytes
     claimBytes recCommitParams innerFri
@@ -173,14 +175,14 @@ def main (args : List String) : IO UInt32 := do
       return 0
     -- PROVE the verifier execution (multi-stark): the recursion step itself.
     IO.println "\n=== PROVING the verifier (multi-stark) ==="
-    let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams
+    let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams innerFri
     TracingTexray.resetPeakTreeRss
     let t0 ← IO.monoNanosNow
-    let (vclaim, vproof, _) := vSystem.prove innerFri vIdx pubInput io
+    let (vclaim, vproof, _) := vSystem.prove vIdx pubInput io
     let nbytes := vproof.toBytes.size  -- force the (lazy, pure) prove to run
     let t1 ← IO.monoNanosNow
     let outerPeak ← TracingTexray.peakTreeRssBytes
-    let outerOk := vSystem.verify innerFri vclaim vproof matches .ok _
+    let outerOk := vSystem.verify vclaim vproof matches .ok _
     let t2 ← IO.monoNanosNow
     IO.println s!"verifier PROVE time: {secs t0 t1} s, proof {nbytes} bytes"
     IO.println s!"verifier proof VERIFY time: \

Benchmarks/Sha256.lean

@@ -34,7 +34,7 @@ def sha256Bench : IO $ Array BenchReport := do
     | throw (IO.userError "Compilation failed")
   let some funIdx := compiled.getFuncIdx `sha256_bench
     | throw (IO.userError "Aiur function not found")
-  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters
+  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters
   bgroup "prove sha256" { oneShot := true, avgThroughput := true, report := true } do
     for dataSize in dataSizes do
       for numHashes in numHashesPerProof do
@@ -47,7 +47,7 @@ def sha256Bench : IO $ Array BenchReport := do
             ioBuffer.extend 0 #[.ofNat idx] data
         throughput (.ElementsAndBytes numHashes.toUInt64 (dataSize * numHashes).toUInt64 "hashes")
         bench s!"dataSize={dataSize} numHashes={numHashes}"
-          (aiurSystem.prove friParameters funIdx #[Aiur.G.ofNat numHashes]) ioBuffer
+          (aiurSystem.prove funIdx #[Aiur.G.ofNat numHashes]) ioBuffer
 
 def main : IO Unit := do
   let _ ← sha256Bench

Benchmarks/Typecheck.lean

@@ -125,15 +125,17 @@ def recursiveCommitmentParameters : Aiur.CommitmentParameters := {
   capHeight := 0
 }
 
-/-- Recursion-tuned FRI parameters: the in-circuit verifier's cost scales with
-    the inner proof's query count, so the recursion configuration trades
-    queries (3, not 100) for blowup and commit proof-of-work. `--recursive`
-    runs the WHOLE system — the inner prove included — under these, so its
-    rows are not comparable to the standard `prove` cell's. -/
+/-- Recursion FRI parameters for `--recursive`. The query count IS the
+    soundness level, so a real (secure) recursive proof needs the full query
+    count, not a toy handful. The in-circuit verifier's cost scales with that
+    count, so at IxVM scale the cell is expected to exceed even a 128 GB host —
+    an OOM row here documents the gap between secure recursion and what fits
+    today. `--recursive` runs the WHOLE system, inner prove included, under
+    these, so its rows are not comparable to the standard `prove` cell's. -/
 def recursiveFriParameters : Aiur.FriParameters := {
   logFinalPolyLen := 0
   maxLogArity := 1
-  numQueries := 3
+  numQueries := 100
   commitProofOfWorkBits := 20
   queryProofOfWorkBits := 0
 }
@@ -325,7 +327,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
   let (commitParams, friParams) :=
     if recursive then (recursiveCommitmentParameters, recursiveFriParameters)
     else (commitmentParameters, friParameters)
-  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitParams
+  let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitParams friParams
   -- The recursive-verifier context, compiled and built ONCE: the verifier
   -- toplevel is constant-independent, and its prover system (same recursion
   -- parameters) is reused for every constant's outer prove.
@@ -338,7 +340,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
       let some vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof
         | throw (IO.userError "verify_multi_stark_proof entrypoint missing")
       pure (some (vCompiled, vIdx,
-        Aiur.AiurSystem.build vCompiled.bytecode commitParams))
+        Aiur.AiurSystem.build vCompiled.bytecode commitParams friParams))
 
   -- Load the serialized env lazily (the `ix check --ixe` path, #445): byte-window
   -- constants over the backing buffer, so only the checked closure is ever
@@ -452,11 +454,11 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
         if skipDeps then
           let witness := IxVM.ClaimHarness.buildVerifyConst ixonEnv addr
           let (claim, proof, ioBuf) :=
-            aiurSystem.proveIxVM friParams funIdx witness.input witness.inputIOBuffer
+            aiurSystem.proveIxVM funIdx witness.input witness.inputIOBuffer
           (.ok (claim, proof, ioBuf) :
             Except String (Array Aiur.G × Aiur.Proof × Aiur.IOBuffer))
         else
-          match aiurSystem.proveAddrWithEnv friParams funIdx envHandle addr.hash with
+          match aiurSystem.proveAddrWithEnv funIdx envHandle addr.hash with
           | .error e => .error e
           | .ok (claimBytes, proof, ioBuf) =>
             -- The envHandle path returns the SERIALIZED `Ix.Claim`; rebuild
@@ -474,7 +476,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
         let peak ← TracingTexray.peakTreeRssBytes
         let proofBytes := Aiur.Proof.toBytes proof
         let (verifyRes, verifySec) ← timed fun _ =>
-          aiurSystem.verify friParams claim proof
+          aiurSystem.verify claim proof
         let verifySec? ← match verifyRes with
           | .ok () => pure (some verifySec)
           | .error e =>
@@ -519,11 +521,11 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
             (← IO.getStdout).flush
             TracingTexray.resetPeakTreeRss
             let ((rvClaim, rvProof, _), rvProveSec) ← timed fun _ =>
-              vSystem.prove friParams vIdx pubInput io
+              vSystem.prove vIdx pubInput io
             let rvPeak ← TracingTexray.peakTreeRssBytes
             let rvProofBytes := Aiur.Proof.toBytes rvProof
             let (rvVerifyRes, rvVerifySec) ← timed fun _ =>
-              vSystem.verify friParams rvClaim rvProof
+              vSystem.verify rvClaim rvProof
             let rvVerifySec? ← match rvVerifyRes with
               | .ok () => pure (some rvVerifySec)
               | .error e =>

Cargo.toml

@@ -50,7 +50,7 @@ itertools = "0.14.0"
 log = "0.4"
 memmap2 = "0.9"
 mimalloc = { version = "0.1", default-features = false }
-multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "9ecab51d553445c0cc7b571af00a76b8a83a6f8c" }
+multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "2c019220cb43ce946efec6b9caf507f5a6bccd1c" }
 num-bigint = "0.4.6"
 quickcheck = "1.0.3"
 quickcheck_macros = "1.0.0"

Ix/Aiur/Protocol.lean

@@ -45,14 +45,14 @@ instance : Nonempty AiurSystem := AiurSystemNonempty.property
 namespace AiurSystem
 
 @[extern "rs_aiur_system_build"]
-opaque build : @&Bytecode.Toplevel → @&CommitmentParameters → AiurSystem
+opaque build : @&Bytecode.Toplevel → @&CommitmentParameters → @&FriParameters → AiurSystem
 
 /-- Serialize the verifying key (`System<AiurCircuit>`) to bytes. -/
 @[extern "rs_aiur_system_vk_bytes"]
 opaque vkBytes : @& AiurSystem → ByteArray
 
 @[extern "rs_aiur_system_prove"]
-private opaque prove' : @& AiurSystem → @& FriParameters →
+private opaque prove' : @& AiurSystem →
   @& Bytecode.FunIdx → @& Array G →
   (ioData : @& Array (G × Array G)) →
   (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
@@ -62,19 +62,19 @@ private opaque prove' : @& AiurSystem → @& FriParameters →
 then generates a proof of the computation. Returns the claim
 (`#[functionChannel, funIdx] ++ args ++ output`), the `Proof`, and the
 updated `IOBuffer`. -/
-def prove (system : @& AiurSystem) (friParameters : @& FriParameters)
+def prove (system : @& AiurSystem)
   (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
     Array G × Proof × IOBuffer :=
   let ioData := ioBuffer.data.toArray
   let ioMap := ioBuffer.map.toArray
-  let (claim, proof, ioData, ioMap) := prove' system friParameters funIdx args
+  let (claim, proof, ioData, ioMap) := prove' system funIdx args
     ioData ioMap
   let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
   let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
   (claim, proof, ⟨ioData, ioMap⟩)
 
 @[extern "rs_aiur_system_prove_ixvm"]
-private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
+private opaque proveIxVM' : @& AiurSystem →
   @& Bytecode.FunIdx → @& Array G →
   (ioData : @& Array (G × Array G)) →
   (ioMap : @& Array ((G × Array G) × IOKeyInfo)) →
@@ -85,19 +85,19 @@ private opaque proveIxVM' : @& AiurSystem → @& FriParameters →
     of the bytecode interpreter. The resulting `Proof` is
     verification-compatible with one from `prove`. Only valid when
     `system.toplevel` is the IxVM kernel's bytecode. -/
-def proveIxVM (system : @& AiurSystem) (friParameters : @& FriParameters)
+def proveIxVM (system : @& AiurSystem)
   (funIdx : @& Bytecode.FunIdx) (args : @& Array G) (ioBuffer : IOBuffer) :
     Array G × Proof × IOBuffer :=
   let ioData := ioBuffer.data.toArray
   let ioMap := ioBuffer.map.toArray
-  let (claim, proof, ioData, ioMap) := proveIxVM' system friParameters funIdx args
+  let (claim, proof, ioData, ioMap) := proveIxVM' system funIdx args
     ioData ioMap
   let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
   let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
   (claim, proof, ⟨ioData, ioMap⟩)
 
 @[extern "rs_aiur_system_prove_addr_with_env"]
-private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
+private opaque proveAddrWithEnv' : @& AiurSystem →
   @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
     Except String (ByteArray × Proof ×
       Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))
@@ -106,35 +106,35 @@ private opaque proveAddrWithEnv' : @& AiurSystem → @& FriParameters →
     `(claimBytes, proof, ioBuffer)` — Rust serializes the
     reconstructed `Ix.Claim` via `ixon::Claim::put` so Lean can
     deserialize directly without re-running the closure walk. -/
-def proveAddrWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
+def proveAddrWithEnv (system : @& AiurSystem)
   (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (addrBytes : ByteArray) :
     Except String (ByteArray × Proof × IOBuffer) :=
-  match proveAddrWithEnv' system friParameters funIdx envHandle addrBytes with
+  match proveAddrWithEnv' system funIdx envHandle addrBytes with
   | .error e => .error e
   | .ok (claimBytes, proof, ioData, ioMap) =>
     let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
     let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
     .ok (claimBytes, proof, ⟨ioData, ioMap⟩)
 
 @[extern "rs_aiur_system_shard_prove_with_env"]
-private opaque shardProveWithEnv' : @& AiurSystem → @& FriParameters →
+private opaque shardProveWithEnv' : @& AiurSystem →
   @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →
     Except String (ByteArray × Proof ×
       Array (G × Array G) × Array ((G × Array G) × IOKeyInfo))
 
 /-- Per-shard prove against a Rust-owned `EnvHandle`. -/
-def shardProveWithEnv (system : @& AiurSystem) (friParameters : @& FriParameters)
+def shardProveWithEnv (system : @& AiurSystem)
   (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle) (ownedBlob : ByteArray) :
     Except String (ByteArray × Proof × IOBuffer) :=
-  match shardProveWithEnv' system friParameters funIdx envHandle ownedBlob with
+  match shardProveWithEnv' system funIdx envHandle ownedBlob with
   | .error e => .error e
   | .ok (claimBytes, proof, ioData, ioMap) =>
     let ioData := ioData.foldl (fun acc (k, v) => acc.insert k v) ∅
     let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
     .ok (claimBytes, proof, ⟨ioData, ioMap⟩)
 
 @[extern "rs_aiur_system_verify"]
-opaque verify : @& AiurSystem → @& FriParameters →
+opaque verify : @& AiurSystem →
   @& Array G → @& Proof → Except String Unit
 
 end AiurSystem