perf: Switch Aiur from Keccak to Blake3 hashing

Benchmarks/RecursiveVerifier.lean

@@ -0,0 +1,118 @@
+import Ix.Aiur.Meta
+import Ix.Aiur.Protocol
+import Ix.Aiur.Compiler
+import Ix.Aiur.Statistics
+import Ix.MultiStark
+import Blake3.Rust
+import Ix.TracingTexray
+
+open Aiur
+
+/-!
+# Recursive-verifier cost benchmark
+
+Proves `factorial(5)` with the multi-stark backend, then runs the in-circuit
+recursive verifier (`verify_multi_stark_proof`) over that proof and reports its
+cost. Mirrors the setup of `Tests/MultiStark.lean::endToEndSuite`, but measures
+cost instead of asserting accept/reject.
+
+```
+lake exe bench-recursive-verifier                 # execute + FFT + PROVE (texray) — ~5 s / ~7 GB
+lake exe bench-recursive-verifier --execute-only  # skip the prove (FFT/exec only)
+```
+
+What it reports:
+* **In-circuit FFT cost** (`Σ width·height·log₂(height)`) — the prover-work / RAM
+  driver for proving the verifier. This is the headline recursion-cost metric.
+* By default, the **end-to-end STARK prove** of the verifier, with `tracing-texray`
+  emitting the per-stage timeline (`stage1_commit` / `quotient` / `fri_open`) and
+  RAM Δ/peak (~5 s, ~7 GB peak). Pass `--execute-only` to skip the prove on a
+  memory-constrained box.
+
+Determinism note: the multi-stark prover is **non-deterministic under `parallel`**
+(the same statement yields byte-different valid proofs run-to-run), so the
+verifier authenticates slightly different Merkle paths and its FFT drifts ~±15%.
+Aiur *execution* FFT is deterministic; pin the inner proof with
+`RAYON_NUM_THREADS=1` for exactly reproducible numbers.
+-/
+
+def factorialProgram : Source.Toplevel := ⟦
+  pub fn factorial(n: G) -> G {
+    match n {
+      0 => 1,
+      _ => n * factorial(n - 1),
+    }
+  }
+⟧
+
+def recCommitParams : Aiur.CommitmentParameters := { logBlowup := 2, capHeight := 0 }
+def innerFri : Aiur.FriParameters :=
+  { logFinalPolyLen := 0, maxLogArity := 1, numQueries := 3,
+    commitProofOfWorkBits := 20, queryProofOfWorkBits := 0 }
+
+def u64le (n : Nat) : Array UInt8 :=
+  (Array.range 8).map (fun i => UInt8.ofNat ((n >>> (8 * i)) % 256))
+
+/-- Serialize the public claims for the verifier's IO channel (matches the
+in-circuit `read_claims` wire format). -/
+def serializeClaims (claims : Array (Array Aiur.G)) : ByteArray := Id.run do
+  let mut out : Array UInt8 := u64le claims.size
+  for c in claims do
+    out := out ++ u64le c.size
+    for g in c do
+      out := out ++ u64le g.val.toNat
+  return ⟨out⟩
+
+def main (args : List String) : IO Unit := do
+  let doProve := !args.contains "--execute-only"
+  -- Inner proof: factorial(5) under the multi-stark backend.
+  let facCompiled ← match factorialProgram.compile with
+    | .ok c => pure c | .error e => IO.eprintln s!"factorial compile failed: {e}"; return
+  let facSystem := AiurSystem.build facCompiled.bytecode recCommitParams
+  let facIdx := facCompiled.getFuncIdx `factorial |>.get!
+  IO.println "proving inner factorial(5)…"
+  let (claim, proof, _) := facSystem.prove innerFri facIdx #[Aiur.G.ofNat 5] default
+  let proofBytes := proof.toBytes
+  -- Serialize proof (advice, channel 0), vk (channel 1), claims (channel 2), plus
+  -- the Blake3-bound vk/claims digests and FRI params as public input.
+  let proofGs : Array Aiur.G := proofBytes.data.map .ofUInt8
+  let vkBytes := facSystem.vkBytes
+  let sysDigestInput : Array Aiur.G := (Blake3.Rust.hash vkBytes).val.data.map .ofUInt8
+  let vkGs : Array Aiur.G := vkBytes.data.map .ofUInt8
+  let claimBytes := serializeClaims #[claim]
+  let claimsDigestInput : Array Aiur.G := (Blake3.Rust.hash claimBytes).val.data.map .ofUInt8
+  let claimGs : Array Aiur.G := claimBytes.data.map .ofUInt8
+  let friParamInput : Array Aiur.G :=
+    #[Aiur.G.ofNat innerFri.numQueries, Aiur.G.ofNat innerFri.commitProofOfWorkBits,
+      Aiur.G.ofNat recCommitParams.logBlowup]
+  let pubInput : Array Aiur.G := sysDigestInput ++ claimsDigestInput ++ friParamInput
+  let io := (((default : IOBuffer).extend 0 #[Aiur.G.ofNat 0] proofGs).extend
+      1 #[Aiur.G.ofNat 0] vkGs).extend 2 #[Aiur.G.ofNat 0] claimGs
+  IO.println s!"inner proof: {proofBytes.size} bytes"
+  -- Compile the verifier toplevel and run it over the proof.
+  let vTop ← match MultiStark.multiStark with
+    | .ok t => pure t | .error e => IO.eprintln s!"verifier merge failed: {e}"; return
+  let vCompiled ← match vTop.compile with
+    | .ok c => pure c | .error e => IO.eprintln s!"verifier compile failed: {e}"; return
+  let vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof |>.get!
+  IO.println "executing verify_multi_stark_proof…"
+  match vCompiled.bytecode.execute vIdx pubInput io with
+  | .error e => IO.eprintln s!"verifier execution failed: {e}"
+  | .ok (out, _, qc) =>
+    let stats := Aiur.computeStats vCompiled qc
+    IO.println s!"verifier output (1=accept): {out}"
+    IO.println s!"\n=== recursive verifier in-circuit cost ==="
+    IO.println s!"totalFftCost = {stats.totalFftCost}"
+    IO.println "\n=== per-circuit breakdown (top FFT contributors) ==="
+    Aiur.printStats stats
+    if doProve then
+      -- PROVE the verifier execution (multi-stark) with texray: per-stage timeline
+      -- + RAM Δ/peak (~7 GB).
+      IO.println "\n=== PROVING the verifier (multi-stark + texray) ==="
+      TracingTexray.init {}
+      let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams
+      let t0 ← IO.monoNanosNow
+      let (_, vproof, _) := vSystem.prove innerFri vIdx pubInput io
+      let nbytes := vproof.toBytes.size  -- force the (lazy, pure) prove to run
+      let t1 ← IO.monoNanosNow
+      IO.println s!"verifier PROVE time: {(Float.ofNat (t1 - t0)) / 1e9} s, proof {nbytes} bytes"

Benchmarks/Typecheck.lean

@@ -37,6 +37,7 @@ lake exe bench-typecheck --ixe <path> [names…] [flags]
   --texray       force the tracing-texray timeline + RAM breakdown on.
   --no-texray    force it off. Default: on iff `--json` was NOT given, so a
                  plain local run gets the breakdown while a JSON run stays quiet.
+  --execute-only stop after Phase 1 (FFT/exec metrics); skip the proving phase.
 ```
 
 For each constant the harness STARK-checks `Ix.Claim.check addr none` (the full
@@ -149,6 +150,8 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
   -- subject-only: check just the target (`verify_const`, trusting its deps)
   -- instead of re-checking the whole transitive closure (`verify_claim`).
   let subjectOnly := p.hasFlag "subject-only"
+  -- --execute-only: stop after Phase 1 (FFT/exec metrics), skip proving.
+  let executeOnly := p.hasFlag "execute-only"
   -- Default: trace iff we're not in JSON/bencher mode.
   let useTexray :=
     if p.hasFlag "texray" then true
@@ -216,6 +219,11 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
       IO.FS.writeFile path (Json.mkObj (results.map Result.toJsonEntry).toList).pretty
     | none => pure ()
 
+  if executeOnly then
+    writeJson (execed.map (·.1))
+    IO.println s!"── execute-only: skipped proving ({execed.size} constants) ──"
+    return 0
+
   -- Phase 2: prove cheap→expensive. Refine each entry with its prove-time as it
   -- lands. Install texray first so the prove spans (timeline + RAM Δ/peak) render.
   if useTexray then TracingTexray.init {}
@@ -252,6 +260,7 @@ def typecheckCmd : Cli.Cmd := `[Cli|
     "subject-only";       "Check only each target itself (verify_const, trusting its deps) instead of re-checking its whole transitive closure (verify_claim)."
     texray;               "Force the tracing-texray timeline + RAM breakdown on (per-prove spans on stderr)."
     "no-texray";          "Force the breakdown off. Default: on iff --json was not given."
+    "execute-only";       "Stop after Phase 1 (FFT/exec metrics); skip proving."
 
   ARGS:
     ...names : String;   "Fully-qualified constant name(s) to benchmark (e.g. `Nat.add_comm String.append`). Optional if `--manifest` is given."

Cargo.toml

@@ -46,7 +46,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 = "0b260d7b23f239c196a7d03bb8fef3a548669b73" }
 num-bigint = "0.4.6"
 quickcheck = "1.0.3"
 quickcheck_macros = "1.0.0"

Ix/MultiStark.lean

@@ -2,6 +2,7 @@ module
 public import Ix.Aiur.Meta
 public import Ix.IxVM.Core
 public import Ix.IxVM.ByteStream
+public import Ix.IxVM.Blake3
 public import Ix.MultiStark.Goldilocks
 public import Ix.MultiStark.Deserialize
 public import Ix.MultiStark.Keccak
@@ -15,12 +16,12 @@ public import Ix.MultiStark.Tests
 
 The recursive verifier. Its public statement is purely existential: *"there
 exists a valid multi-stark proof, under the FRI parameters given as public
-input, for the constraint system with this keccak-256 digest and these public
+input, for the constraint system with this Blake3 digest and these public
 claims."* The proof itself is **non-deterministic advice** (fed on IO channel 0,
 never hashed or otherwise bound as a public input): the Fiat-Shamir transcript
 replay plus the Merkle/OOD/FRI checks are exactly what make any accepted advice
 a valid proof — a hash binding of the proof bytes would add nothing to the
-statement, while costing one keccak-f per 136 bytes in-circuit.
+statement, while costing an extra in-circuit hash over those bytes.
 
 The verifying key and claims, by contrast, ARE digest-bound (`system_digest`,
 `claims_digest`): they determine *what was proven*.
@@ -35,8 +36,8 @@ public section
 namespace MultiStark
 
 def entrypoints := ⟦
-  -- Public inputs: the keccak-256 digests of the verifying key and the claims
-  -- (4 little-endian u64 lanes each) plus the variable FRI parameters. The
+  -- Public inputs: the Blake3 digests of the verifying key and the claims
+  -- (32 bytes = 4 little-endian u64 lanes each) plus the variable FRI parameters. The
   -- proof is pure non-deterministic advice on IO channel 0 — see the module
   -- docstring. One stream per channel (0 = proof, 1 = vk, 2 = claims), each
   -- registered under key `[0]` on its channel.
@@ -47,19 +48,19 @@ def entrypoints := ⟦
     let (proof, rest) = read_proof(bytes);
     assert_eq!(load(rest), ListNode.Nil);
     -- Verifying key (`System<AiurCircuit>`) from IO channel 1: bind the bytes
-    -- to the public keccak-256 `system_digest`, then reconstruct the system.
+    -- to the public Blake3 `system_digest`, then reconstruct the system.
     let (sidx, slen) = io_get_info(1, [0]);
     let sbytes = #read_byte_stream(1, sidx, slen);
-    assert_eq!(keccak256(sbytes), system_digest);
+    assert_eq!(b3_to_digest(blake3(sbytes)), system_digest);
     let (sys, srest) = read_system(sbytes);
     assert_eq!(load(srest), ListNode.Nil);
     -- Public claims (`&[&[Val]]`) from IO channel 2: bind the bytes to the
-    -- public keccak-256 `claims_digest`, then deserialize. Binding them as a
+    -- public Blake3 `claims_digest`, then deserialize. Binding them as a
     -- public input is what makes the lookup argument sound (a prover cannot
     -- choose claims adaptively).
     let (cidx, clen) = io_get_info(2, [0]);
     let cbytes = #read_byte_stream(2, cidx, clen);
-    assert_eq!(keccak256(cbytes), claims_digest);
+    assert_eq!(b3_to_digest(blake3(cbytes)), claims_digest);
     let (claims, crest) = read_claims(cbytes);
     assert_eq!(load(crest), ListNode.Nil);
     -- Structural + accumulator + PCS checks.
@@ -73,12 +74,12 @@ def entrypoints := ⟦
 
 /-- The standalone Multi-STARK verifier toplevel: `core` (lists/options) +
 `byteStream` (`U64`, `flatten_u64`, `read_byte_stream`, …) + the deserializer,
-the keccak-256 implementation, and the entrypoint. -/
+the Blake3 hash, and the entrypoint. -/
 def multiStark : Except Aiur.Global Aiur.Source.Toplevel := do
   let t ← IxVM.core.merge IxVM.byteStream
   let t ← t.merge MultiStark.goldilocks
   let t ← t.merge deserialize
-  let t ← t.merge keccak
+  let t ← t.merge IxVM.blake3
   let t ← t.merge systemDeserialize
   let t ← t.merge pcs
   let t ← t.merge verifier