Recursive verification of Ix proofs at kernel scale

Benchmarks/IxVM.lean

@@ -20,7 +20,11 @@ def friParameters : Aiur.FriParameters := {
 }
 
 def main : IO Unit := do
-  let .ok toplevel := IxVM.ixVM
+  -- `ixon_serde_blake3_bench` is a bench-only entrypoint, present only in
+  -- the FULL toplevel (production prunes it), so this prove goes through
+  -- the generic interpreter — the codegen'd kernel mirrors the pruned
+  -- toplevel and has no code (or index) for bench entries.
+  let .ok toplevel := IxVM.ixVMFull
     | throw (IO.userError "Merging failed")
   let .ok compiled := toplevel.compile
     | throw (IO.userError "Compilation failed")
@@ -34,9 +38,7 @@ def main : IO Unit := do
 
   let _ ← bgroup "IxVM benchmarks" { oneShot := true } do
     throughput (.Elements n.toUInt64 "consts")
-    -- 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 funIdx #[.ofNat n])
+      (aiurSystem.prove funIdx #[.ofNat n])
       ioBuffer
   return

Benchmarks/RecursiveVerifier.lean

@@ -136,10 +136,13 @@ 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
-  -- Blake3-bound vk/claims digests and FRI params as public input.
+  -- Blake3-bound vk/claims digests and FRI params as public input. The
+  -- advice buffer is built natively in Rust from the raw byte blobs
+  -- (`executeMultiStark` / `proveMultiStark`).
   let claimBytes := MultiStark.serializeClaims #[claim]
-  let (pubInput, io) := MultiStark.verifierInput proofBytes facSystem.vkBytes
-    claimBytes recCommitParams innerFri
+  let vkBytes := facSystem.vkBytes
+  let pubInput := MultiStark.verifierPubInput vkBytes claimBytes
+    recCommitParams innerFri
   -- Compile the verifier toplevel and run it over the proof.
   let vTop ← match MultiStark.multiStark with
     | .ok t => pure t
@@ -149,10 +152,17 @@ def main (args : List String) : IO UInt32 := do
     | .error e => IO.eprintln s!"verifier compile failed: {e}"; return 1
   let vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof |>.get!
   IO.println "executing verify_multi_stark_proof…"
+  -- `--use-bytecode`: route through the generic Aiur interpreter instead of
+  -- the codegen'd verifier (same escape hatch as `ix check --use-bytecode`;
+  -- useful for iterating on `Ix/MultiStark/*.lean` without regenerating
+  -- `crates/ixvm-codegen/src/aiur_multi_stark.rs`, and for measuring the
+  -- interpreter ↔ codegen gap).
+  let useBytecode := args.contains "--use-bytecode"
   let e0 ← IO.monoNanosNow
-  match vCompiled.bytecode.execute vIdx pubInput io with
+  match vCompiled.bytecode.executeMultiStark vIdx pubInput proofBytes vkBytes
+    claimBytes useBytecode with
   | .error e => IO.eprintln s!"verifier execution REJECTED: {e}"; return 1
-  | .ok (_, _, qc) =>
+  | .ok (_, qc) =>
     let e1 ← IO.monoNanosNow
     let stats := Aiur.computeStats vCompiled qc
     IO.println s!"verifier accepted, execute {secs e0 e1} s"
@@ -178,7 +188,8 @@ def main (args : List String) : IO UInt32 := do
     let vSystem := AiurSystem.build vCompiled.bytecode recCommitParams innerFri
     TracingTexray.resetPeakTreeRss
     let t0 ← IO.monoNanosNow
-    let (vclaim, vproof, _) := vSystem.prove vIdx pubInput io
+    let (vclaim, vproof) := vSystem.proveMultiStark vIdx pubInput proofBytes
+      vkBytes claimBytes
     let nbytes := vproof.toBytes.size  -- force the (lazy, pure) prove to run
     let t1 ← IO.monoNanosNow
     let outerPeak ← TracingTexray.peakTreeRssBytes

Benchmarks/Typecheck.lean

@@ -498,17 +498,25 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
           IO.println s!"  [{i + 1}/{ordered.size}] recursively verifying {r.name} …"
           (← IO.getStdout).flush
           let claimBytes := MultiStark.serializeClaims #[claim]
-          let (pubInput, io) := MultiStark.verifierInput proofBytes
-            aiurSystem.vkBytes claimBytes commitParams friParams
+          let vkBytes := aiurSystem.vkBytes
+          let pubInput := MultiStark.verifierPubInput vkBytes claimBytes
+            commitParams friParams
+          -- Native path: the advice buffer is built in Rust from the raw
+          -- byte blobs and execution routes through the codegen'd verifier.
           let (rvRes, rvSec) ← timed fun _ =>
-            vCompiled.bytecode.execute vIdx pubInput io
+            vCompiled.bytecode.executeMultiStark vIdx pubInput proofBytes
+              vkBytes claimBytes
           match rvRes with
           | .error e =>
             IO.eprintln s!"  ❌ recursive verifier REJECTED {r.name}'s proof: {e}"
-          | .ok (_, _, qc) =>
+          | .ok (_, qc) =>
             let rvStats := Aiur.computeStats vCompiled qc
             IO.println s!"  {r.name}: recursive={rvSec}s \
               recursive-fft-cost={rvStats.totalFftCost}"
+            -- The per-circuit breakdown names where the verifier's cost
+            -- lives (deserialization vs blake3 vs FRI); texray-gated like
+            -- the other detailed diagnostics.
+            if useTexray then Aiur.printStats rvStats
             let (row, _) := ordered[i]!
             ordered := ordered.set! i
               ({ row with recursiveExecuteSec := some rvSec
@@ -520,8 +528,9 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
             IO.println s!"  [{i + 1}/{ordered.size}] proving the verifier over {r.name} …"
             (← IO.getStdout).flush
             TracingTexray.resetPeakTreeRss
-            let ((rvClaim, rvProof, _), rvProveSec) ← timed fun _ =>
-              vSystem.prove vIdx pubInput io
+            let ((rvClaim, rvProof), rvProveSec) ← timed fun _ =>
+              vSystem.proveMultiStark vIdx pubInput proofBytes vkBytes
+                claimBytes
             let rvPeak ← TracingTexray.peakTreeRssBytes
             let rvProofBytes := Aiur.Proof.toBytes rvProof
             let (rvVerifyRes, rvVerifySec) ← timed fun _ =>

Cargo.toml

@@ -47,10 +47,11 @@ dashmap = "6.1.0"
 hashbrown = "0.15"
 indexmap = "2"
 itertools = "0.14.0"
+libc = "0.2"
 log = "0.4"
 memmap2 = "0.9"
 mimalloc = { version = "0.1", default-features = false }
-multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "2c019220cb43ce946efec6b9caf507f5a6bccd1c" }
+multi-stark = { git = "https://github.com/argumentcomputer/multi-stark.git", rev = "6382036e970ab508e69b2db2b8ae5ad64672e34b" }
 num-bigint = "0.4.6"
 quickcheck = "1.0.3"
 quickcheck_macros = "1.0.0"

Ix/Aiur/Compiler/Check.lean

@@ -801,6 +801,14 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
     let a' ← inferNoEscape a
     let b' ← checkNoEscape b a'.typ
     pure (Typed.Term.unconstrainedBigUintDivMod (.tuple #[a'.typ, a'.typ]) false a' b')
+  | .unconstrainedGToBytes a => do
+    -- The bytes are UNCONSTRAINED advice typed `u8`; the caller must
+    -- range-check them (see `Source.Term.unconstrainedGToBytes`).
+    let a' ← checkNoEscape a .field
+    pure (Typed.Term.unconstrainedGToBytes (.array .u8 8) false a')
+  | .unconstrainedGInverse a => do
+    let a' ← checkNoEscape a .field
+    pure (Typed.Term.unconstrainedGInverse .field false a')
   | .toField a => do
     let a' ← checkNoEscape a .u8
     pure (Typed.Term.toField .field false a')
@@ -981,6 +989,10 @@ def zonkTypedTerm (t : Typed.Term) : CheckM Typed.Term := match t with
       pure (.u8RangeCheck (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .unconstrainedBigUintDivMod τ e a b => do
       pure (.unconstrainedBigUintDivMod (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
+  | .unconstrainedGToBytes τ e a => do
+      pure (.unconstrainedGToBytes (← zonkTyp τ) e (← zonkTypedTerm a))
+  | .unconstrainedGInverse τ e a => do
+      pure (.unconstrainedGInverse (← zonkTyp τ) e (← zonkTypedTerm a))
   | .toField τ e a => do pure (.toField (← zonkTyp τ) e (← zonkTypedTerm a))
   | .u8FromFieldUnsafe τ e a => do
       pure (.u8FromFieldUnsafe (← zonkTyp τ) e (← zonkTypedTerm a))

Ix/Aiur/Compiler/Concretize.lean

@@ -366,6 +366,10 @@ def termToConcrete
   | .unconstrainedBigUintDivMod τ e a b => do
       pure (.unconstrainedBigUintDivMod (← typToConcrete mono τ) e
                                     (← termToConcrete mono a) (← termToConcrete mono b))
+  | .unconstrainedGToBytes τ e a => do
+      pure (.unconstrainedGToBytes (← typToConcrete mono τ) e (← termToConcrete mono a))
+  | .unconstrainedGInverse τ e a => do
+      pure (.unconstrainedGInverse (← typToConcrete mono τ) e (← termToConcrete mono a))
   -- `toField` / `u8FromFieldUnsafe` are erased coercions: `u8` and `field`
   -- share a representation, so we drop the wrapper and keep the inner term.
   | .toField _ _ a | .u8FromFieldUnsafe _ _ a => termToConcrete mono a
@@ -575,6 +579,10 @@ def rewriteTypedTerm (decls : Typed.Decls)
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
   | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
+  | .unconstrainedGToBytes τ e a => .unconstrainedGToBytes (rewriteTyp subst mono τ) e
+      (rewriteTypedTerm decls subst mono a)
+  | .unconstrainedGInverse τ e a => .unconstrainedGInverse (rewriteTyp subst mono τ) e
+      (rewriteTypedTerm decls subst mono a)
   | .toField τ e a => .toField (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a)
   | .u8FromFieldUnsafe τ e a => .u8FromFieldUnsafe (rewriteTyp subst mono τ) e
@@ -653,6 +661,7 @@ def collectInTypedTerm (seen : Std.HashSet (Global × Array Typ)) :
     collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b
   | .eqZero τ _ a | .store τ _ a | .load τ _ a | .ptrVal τ _ a | .toField τ _ a
   | .u8FromFieldUnsafe τ _ a
+  | .unconstrainedGToBytes τ _ a | .unconstrainedGInverse τ _ a
   | .u8BitDecomposition τ _ a | .u8ShiftLeft τ _ a | .u8ShiftRight τ _ a =>
     collectInTypedTerm (collectInTyp seen τ) a
   | .ioGetInfo τ _ c k =>
@@ -724,6 +733,7 @@ def collectCalls (decls : Typed.Decls)
     collectCalls decls (collectCalls decls seen a) b
   | .eqZero _ _ a | .store _ _ a | .load _ _ a | .ptrVal _ _ a | .toField _ _ a
   | .u8FromFieldUnsafe _ _ a
+  | .unconstrainedGToBytes _ _ a | .unconstrainedGInverse _ _ a
   | .u8BitDecomposition _ _ a | .u8ShiftLeft _ _ a | .u8ShiftRight _ _ a =>
     collectCalls decls seen a
   | .ioGetInfo _ _ c k =>
@@ -839,6 +849,10 @@ def substInTypedTerm (subst : Global → Option Typ) : Typed.Term → Typed.Term
       (substInTypedTerm subst a) (substInTypedTerm subst b)
   | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)
+  | .unconstrainedGToBytes τ e a =>
+    .unconstrainedGToBytes (Typ.instantiate subst τ) e (substInTypedTerm subst a)
+  | .unconstrainedGInverse τ e a =>
+    .unconstrainedGInverse (Typ.instantiate subst τ) e (substInTypedTerm subst a)
   | .toField τ e a => .toField (Typ.instantiate subst τ) e (substInTypedTerm subst a)
   | .u8FromFieldUnsafe τ e a =>
     .u8FromFieldUnsafe (Typ.instantiate subst τ) e (substInTypedTerm subst a)

Ix/Aiur/Compiler/Layout.lean

@@ -207,6 +207,10 @@ def opLayout : Bytecode.Op → LayoutM Unit
   -- No constraint relation, no lookup. Mirrors `IORead` (aux only) — the Rust
   -- `constraints.rs` pushes exactly 2 auxiliaries and emits no relation.
   | .unconstrainedBigUintDivMod .. => do pushDegrees #[1, 1]; bumpAuxiliaries 2
+  -- Unconstrained hints: fresh auxiliary witness columns only, no relation,
+  -- no lookup — same shape as `IORead`. The caller pins the values.
+  | .unconstrainedGToBytes _ => do pushDegrees $ .replicate 8 1; bumpAuxiliaries 8
+  | .unconstrainedGInverse _ => do pushDegree 1; bumpAuxiliaries
   | .debug .. => pure ()
 
 /-- Termination helper for blockLayout's Block/Ctrl traversal. -/

Ix/Aiur/Compiler/Lower.lean

@@ -333,6 +333,12 @@ def toIndex
     let a ← expectIdx layoutMap bindings a
     let b ← expectIdx layoutMap bindings b
     pushOp (.unconstrainedBigUintDivMod a b) 2
+  | .unconstrainedGToBytes _ _ a => do
+    let a ← expectIdx layoutMap bindings a
+    pushOp (.unconstrainedGToBytes a) 8
+  | .unconstrainedGInverse _ _ a => do
+    let a ← expectIdx layoutMap bindings a
+    pushOp (.unconstrainedGInverse a)
   | .debug _ _ label term ret => do
     let term ← match term with
       | none => pure none

Ix/Aiur/Compiler/Match.lean

@@ -391,6 +391,8 @@ def typedToSimple : Term → Simple.Term
   | .u32LessThan τ e a b => .u32LessThan τ e (typedToSimple a) (typedToSimple b)
   | .u8RangeCheck τ e a b => .u8RangeCheck τ e (typedToSimple a) (typedToSimple b)
   | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod τ e (typedToSimple a) (typedToSimple b)
+  | .unconstrainedGToBytes τ e a => .unconstrainedGToBytes τ e (typedToSimple a)
+  | .unconstrainedGInverse τ e a => .unconstrainedGInverse τ e (typedToSimple a)
   | .toField τ e a => .toField τ e (typedToSimple a)
   | .u8FromFieldUnsafe τ e a => .u8FromFieldUnsafe τ e (typedToSimple a)
   | .debug τ e l t r =>

Ix/Aiur/Compiler/Simple.lean

@@ -136,6 +136,12 @@ def simplifyTypedTerm (decls : Source.Decls) : Term → Except CheckError Term
       let a' ← simplifyTypedTerm decls a
       let b' ← simplifyTypedTerm decls b
       pure (.unconstrainedBigUintDivMod τ e a' b')
+  | .unconstrainedGToBytes τ e a => do
+      let a' ← simplifyTypedTerm decls a
+      pure (.unconstrainedGToBytes τ e a')
+  | .unconstrainedGInverse τ e a => do
+      let a' ← simplifyTypedTerm decls a
+      pure (.unconstrainedGInverse τ e a')
   | .toField τ e a => do
       let a' ← simplifyTypedTerm decls a
       pure (.toField τ e a')

Ix/Aiur/Goldilocks.lean

@@ -85,6 +85,27 @@ def G.u8BitDecomposition (a : G) : Fin 8 → G :=
 
 def G.u32LessThan (a b : G) : G := if a.n < b.n then 1 else 0
 
+/-- The 8 little-endian bytes of the canonical `u64` value. Semantic model of
+the `unconstrained_g_to_bytes` hint. -/
+def G.toLeBytes (a : G) : Fin 8 → G :=
+  fun i => G.ofUInt8 (a.val >>> (8 * i.val).toUInt64).toUInt8
+
+/-- Exponentiation by squaring. Fuel-structural (64 bits covers any `n < 2⁶⁴`
+exponent, in particular `p − 2`). -/
+def G.pow (x : G) (n : Nat) : G := go n 64 where
+  go (n fuel : Nat) : G := match fuel with
+    | 0 => 1
+    | fuel + 1 =>
+      if n == 0 then 1
+      else
+        let h := go (n / 2) fuel
+        let sq := h * h
+        if n % 2 == 0 then sq else sq * x
+
+/-- Fermat inverse `x^(p−2)`, with `0 ↦ 0`. Semantic model of the
+`unconstrained_g_inverse` hint. -/
+def G.inverse (x : G) : G := G.pow x (gSize.toNat - 2)
+
 theorem G.one_ne_zero : ¬(1 : G) = (0 : G) := by decide
 
 theorem G.add_comm (a b : G) : a + b = b + a := by

Ix/Aiur/Interpret.lean

@@ -417,6 +417,14 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
       let _ ← interp decls bindings t1
       let _ ← interp decls bindings t2
       throwErr "unconstrainedBigUintDivMod: not implemented in debug interpreter"
+  | .unconstrainedGToBytes t => do
+      match ← interp decls bindings t with
+      | .field g => return .array (Array.ofFn fun i => .field (g.toLeBytes i))
+      | _ => throwErr "unconstrainedGToBytes: expected field value"
+  | .unconstrainedGInverse t => do
+      match ← interp decls bindings t with
+      | .field g => return .field g.inverse
+      | _ => throwErr "unconstrainedGInverse: expected field value"
   -- `toField` / `u8FromFieldUnsafe` are erased coercions: value unchanged.
   | .toField t | .u8FromFieldUnsafe t => interp decls bindings t
   | .u8Lit n => return .field (G.ofNat n)

Ix/Aiur/Meta.lean

@@ -205,6 +205,8 @@ syntax "u8_less_than" "(" aiur_trm ", " aiur_trm ")"                        : ai
 syntax "u32_less_than" "(" aiur_trm ", " aiur_trm ")"                       : aiur_trm
 syntax "u8_range_check" "(" aiur_trm ", " aiur_trm ")"                      : aiur_trm
 syntax "unconstrained_big_uint_div_mod" "(" aiur_trm ", " aiur_trm ")"           : aiur_trm
+syntax "unconstrained_g_to_bytes" "(" aiur_trm ")"                          : aiur_trm
+syntax "unconstrained_g_inverse" "(" aiur_trm ")"                           : aiur_trm
 syntax "to_field" "(" aiur_trm ")"                                          : aiur_trm
 syntax "u8_from_field_unsafe" "(" aiur_trm ")"                              : aiur_trm
 syntax:max num "u8"                                                         : aiur_trm
@@ -351,6 +353,10 @@ partial def elabTrm : ElabStxCat `aiur_trm
     mkAppM ``Source.Term.u8RangeCheck #[← elabTrm i, ← elabTrm j]
   | `(aiur_trm| unconstrained_big_uint_div_mod($a:aiur_trm, $b:aiur_trm)) => do
     mkAppM ``Source.Term.unconstrainedBigUintDivMod #[← elabTrm a, ← elabTrm b]
+  | `(aiur_trm| unconstrained_g_to_bytes($a:aiur_trm)) => do
+    mkAppM ``Source.Term.unconstrainedGToBytes #[← elabTrm a]
+  | `(aiur_trm| unconstrained_g_inverse($a:aiur_trm)) => do
+    mkAppM ``Source.Term.unconstrainedGInverse #[← elabTrm a]
   | `(aiur_trm| to_field($a:aiur_trm)) => do
     mkAppM ``Source.Term.toField #[← elabTrm a]
   | `(aiur_trm| u8_from_field_unsafe($a:aiur_trm)) => do
@@ -579,6 +585,12 @@ where
       let a ← replaceToken old new a
       let b ← replaceToken old new b
       `(aiur_trm| unconstrained_big_uint_div_mod($a, $b))
+    | `(aiur_trm| unconstrained_g_to_bytes($a:aiur_trm)) => do
+      let a ← replaceToken old new a
+      `(aiur_trm| unconstrained_g_to_bytes($a))
+    | `(aiur_trm| unconstrained_g_inverse($a:aiur_trm)) => do
+      let a ← replaceToken old new a
+      `(aiur_trm| unconstrained_g_inverse($a))
     | `(aiur_trm| to_field($a:aiur_trm)) => do
       let a ← replaceToken old new a
       `(aiur_trm| to_field($a))

Ix/Aiur/Protocol.lean

@@ -96,6 +96,29 @@ def proveIxVM (system : @& AiurSystem)
   let ioMap := ioMap.foldl (fun acc (k, v) => acc.insert k v) ∅
   (claim, proof, ⟨ioData, ioMap⟩)
 
+@[extern "rs_aiur_multi_stark_prove"]
+private opaque proveMultiStark' : @& AiurSystem →
+  @& Bytecode.FunIdx → @& Array G →
+  (proofBytes : @& ByteArray) → (vkBytes : @& ByteArray) →
+  (claimBytes : @& ByteArray) → Bool →
+    Array G × Proof
+
+/-- Prove the MultiStark recursive verifier over raw proof/vk/claims
+    byte blobs. The IO advice buffer is built natively in Rust (see
+    `Bytecode.Toplevel.executeMultiStark`); the execute step inside
+    the prove routes through the codegen'd verifier
+    (`crates/ixvm-codegen/src/aiur_multi_stark.rs`) unless
+    `useBytecode` is set. Only valid when `system` was built from the
+    production `MultiStark.multiStark` bytecode. Returns the claim
+    (`#[functionChannel, funIdx] ++ pubInput ++ output`) and the
+    `Proof`; the final buffer is not returned. -/
+def proveMultiStark (system : @& AiurSystem)
+  (funIdx : @& Bytecode.FunIdx) (pubInput : @& Array G)
+  (proofBytes vkBytes claimBytes : @& ByteArray) (useBytecode : Bool := false) :
+    Array G × Proof :=
+  proveMultiStark' system funIdx pubInput proofBytes vkBytes claimBytes
+    useBytecode
+
 @[extern "rs_aiur_system_prove_addr_with_env"]
 private opaque proveAddrWithEnv' : @& AiurSystem →
   @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray →