IxVM: cheaper shard checking via an addr-first kernel, plus soundness hardening

Benchmarks/IxVM.lean

@@ -1,5 +1,6 @@
 import Ix.Meta
 import Ix.IxVM
+import Ix.IxVM.Toplevel
 import Ix.Aiur.Protocol
 import Ix.Aiur.Compiler
 import Ix.Benchmark.Bench

Benchmarks/RecursionDebug.lean

@@ -1,4 +1,5 @@
 import Ix.IxVM
+import Ix.IxVM.Toplevel
 import Ix.IxVM.ClaimHarness
 import Ix.Aiur.Protocol
 import Ix.Aiur.Compiler
@@ -65,7 +66,9 @@ def secs (t0 t1 : Nat) : Float := (Float.ofNat (t1 - t0)) / 1e9
 /-- Prove `constName`'s typecheck and return `(proofBytes, vkBytes, claimBytes)`. -/
 def proveConst (ixePath constName : String) (skipDeps : Bool)
     (fri : Aiur.FriParameters) : IO (Option (ByteArray × ByteArray × ByteArray)) := do
-  let .ok toplevel := IxVM.ixVM
+  -- `--skip-deps` uses the subject-only `verify_const`, which the
+  -- production toplevel no longer carries.
+  let .ok toplevel := (if skipDeps then IxVM.ixVMFull else IxVM.ixVM)
     | IO.eprintln "IxVM toplevel merge failed"; return none
   let .ok compiled := toplevel.compile
     | IO.eprintln "IxVM compile failed"; return none

Benchmarks/Typecheck.lean

@@ -1,5 +1,6 @@
 import Cli
 import Ix.IxVM
+import Ix.IxVM.Toplevel
 import Ix.Aiur.Protocol
 import Ix.Aiur.Compiler
 import Ix.Aiur.Statistics
@@ -70,9 +71,11 @@ For each constant the harness STARK-checks `Ix.Claim.check addr none` (the full
 transitive typecheck) in two phases:
 
 1. **Execute** (every constant): run the bytecode out-of-circuit. Cheap and
-   deterministic, so we always record `constants` (closure size), `fft-cost`
-   (Σ width·height·log2(height) over circuits — the proving-cost proxy), and
-   `execute-time`.
+   deterministic, so we always record `constants` (the number of constants the
+   kernel actually typechecked: `check_const`'s unique query count — NOT the
+   shipped byte scope, which also carries primitive bytes the kernel may
+   never touch), `fft-cost` (Σ width·height·log2(height) over circuits — the
+   proving-cost proxy), and `execute-time`.
 2. **Prove** (cheap→expensive by measured fft-cost): the end-to-end STARK prove,
    recording `prove-time`, the serialized `proof-size` (bytes), and
    `verify-time` (verifying the fresh proof) — prover changes can trade speed
@@ -314,13 +317,21 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
   | _, _ => pure ()
 
   -- Compile the IxVM kernel once; build the prover system once.
-  let .ok toplevel := IxVM.ixVM
+  -- `--skip-deps` proves the subject-only `verify_const`, a debug
+  -- entrypoint absent from the production toplevel, so it needs the full
+  -- one — and is thereby measuring a DIFFERENT verifying key than a
+  -- claim run, which is the honest reading of those numbers.
+  let .ok toplevel := (if skipDeps then IxVM.ixVMFull else IxVM.ixVM)
     | throw (IO.userError "Merging IxVM kernel failed")
   let .ok compiled := toplevel.compile
     | throw (IO.userError "Compilation of IxVM kernel failed")
   let entrypoint := if skipDeps then `verify_const else `verify_claim
   let some funIdx := compiled.getFuncIdx entrypoint
     | throw (IO.userError s!"{entrypoint} entrypoint missing")
+  -- `check_const`'s unique query count is the `constants` metric below;
+  -- resolve it up front so a kernel rename fails the run, not the metric.
+  let some checkConstIdx := compiled.getFuncIdx `check_const
+    | throw (IO.userError "check_const missing from compiled kernel")
   -- Recursive mode runs the WHOLE system — the inner prove included — under
   -- the recursion-tuned parameters, so the verifier's query loop stays
   -- tractable (cost scales with numQueries).
@@ -398,7 +409,15 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
              failed := true }, addr)
       | .ok (_, _, queryCounts) =>
         let stats := Aiur.computeStats compiled queryCounts
-        let constants := (IxVM.ClaimHarness.closureFrom ixonEnv addr).size
+        -- Constants CHECKED, not shipped: `check_const` is memoized per
+        -- (ci, addr), so its unique query count is exactly the number of
+        -- constants the kernel typechecked. The shipped byte scope
+        -- (`closureFrom`) is a superset (primitive bytes seeded for
+        -- reduction), so counting it would inflate throughput.
+        let some qc := queryCounts[checkConstIdx]?
+          | throw (IO.userError s!"queryCounts has no entry for check_const \
+              (idx {checkConstIdx}, {queryCounts.size} entries)")
+        let constants := qc.uniqueRows
         -- Throughput via the shared benchmark framework; duration/RAM per
         -- phase stream from texray's `aiur/execute_ixvm` span line.
         let thrpt := (Throughput.Elements constants.toUInt64 "consts").formatRate
@@ -409,7 +428,14 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
           ({ name := label, constants, fftCost := stats.totalFftCost,
              executeSec := execSec, executePeakRss := some execPeak }, addr)
     catch e =>
+      -- Record the failure rather than dropping the constant. A silent
+      -- drop left `execed.any (·.failed)` clear, so a thrown constant —
+      -- including the `check_const`-missing throw above — yielded an
+      -- exit-0 run with one fewer row and no other trace.
       IO.eprintln s!"  execute {label} threw: {e}"
+      execed := execed.push
+        ({ name := label, constants := 0, fftCost := 0, executeSec := 0,
+           failed := true }, addr)
 
   -- Persist rows when `--json` was given, MERGING into the file (the shared
   -- results-row contract): rows land after each result, so a kill leaves the
@@ -477,10 +503,18 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do
         let proofBytes := Aiur.Proof.toBytes proof
         let (verifyRes, verifySec) ← timed fun _ =>
           aiurSystem.verify claim proof
+        -- A proof that does not verify is a correctness alarm, not a slow
+        -- row: mark the entry FAILED so `status` says so and the run
+        -- exits non-zero. Leaving `failed` clear emitted `"status":"ok"`
+        -- with prove-time and proof-size present, the only signal being
+        -- an absent `verify-time` key — invisible to anything keying on
+        -- status.
+        let mut r := r
         let verifySec? ← match verifyRes with
           | .ok () => pure (some verifySec)
           | .error e =>
             IO.eprintln s!"  verify {r.name} FAILED: {e}"
+            r := { r with failed := true }
             pure none
         IO.println s!"  {r.name}: prove={proveSec}s verify={verifySec}s \
           proof={proofBytes.size} bytes (cumulative {spent}s)"

Ix/Aiur/Compiler/Check.lean

@@ -847,11 +847,11 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
       let ret' ← inferTerm ret
       pure (Typed.Term.ioWrite ret'.typ ret'.escapes channel' data' ret')
     | typ' => throw $ .notAnArray typ'
-  | .assertEq a b ret => do
+  | .assertEq a b msg ret => do
     let a' ← inferNoEscape a
     let b' ← checkNoEscape b a'.typ
     let ret' ← inferTerm ret
-    pure (Typed.Term.assertEq ret'.typ ret'.escapes a' b' ret')
+    pure (Typed.Term.assertEq ret'.typ ret'.escapes a' b' msg ret')
   | .debug label term ret => do
     let term' ← match term with
       | none => pure none
@@ -958,8 +958,9 @@ def zonkTypedTerm (t : Typed.Term) : CheckM Typed.Term := match t with
   | .store τ e a => do pure (.store (← zonkTyp τ) e (← zonkTypedTerm a))
   | .load τ e a => do pure (.load (← zonkTyp τ) e (← zonkTypedTerm a))
   | .ptrVal τ e a => do pure (.ptrVal (← zonkTyp τ) e (← zonkTypedTerm a))
-  | .assertEq τ e a b r => do
-      pure (.assertEq (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b) (← zonkTypedTerm r))
+  | .assertEq τ e a b msg r => do
+      pure (.assertEq (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b)
+        msg (← zonkTypedTerm r))
   | .ioGetInfo τ e c k => do
       pure (.ioGetInfo (← zonkTyp τ) e (← zonkTypedTerm c) (← zonkTypedTerm k))
   | .ioSetInfo τ e c k i l r => do

Ix/Aiur/Compiler/Concretize.lean

@@ -306,9 +306,10 @@ def termToConcrete
   | .store τ e a => do pure (.store (← typToConcrete mono τ) e (← termToConcrete mono a))
   | .load τ e a => do pure (.load (← typToConcrete mono τ) e (← termToConcrete mono a))
   | .ptrVal τ e a => do pure (.ptrVal (← typToConcrete mono τ) e (← termToConcrete mono a))
-  | .assertEq τ e a b r => do
+  | .assertEq τ e a b msg r => do
       pure (.assertEq (← typToConcrete mono τ) e
-                      (← termToConcrete mono a) (← termToConcrete mono b) (← termToConcrete mono r))
+                      (← termToConcrete mono a) (← termToConcrete mono b)
+                      msg (← termToConcrete mono r))
   | .ioGetInfo τ e c k => do
       pure (.ioGetInfo (← typToConcrete mono τ) e
                        (← termToConcrete mono c) (← termToConcrete mono k))
@@ -530,10 +531,10 @@ def rewriteTypedTerm (decls : Typed.Decls)
   | .store τ e a => .store (rewriteTyp subst mono τ) e (rewriteTypedTerm decls subst mono a)
   | .load τ e a => .load (rewriteTyp subst mono τ) e (rewriteTypedTerm decls subst mono a)
   | .ptrVal τ e a => .ptrVal (rewriteTyp subst mono τ) e (rewriteTypedTerm decls subst mono a)
-  | .assertEq τ e a b r =>
+  | .assertEq τ e a b msg r =>
     .assertEq (rewriteTyp subst mono τ) e
               (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
-              (rewriteTypedTerm decls subst mono r)
+              msg (rewriteTypedTerm decls subst mono r)
   | .ioGetInfo τ e c k =>
     .ioGetInfo (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono c) (rewriteTypedTerm decls subst mono k)
@@ -669,7 +670,7 @@ def collectInTypedTerm (seen : Std.HashSet (Global × Array Typ)) :
   | .proj τ _ a _ | .get τ _ a _ | .slice τ _ a _ _ =>
     collectInTypedTerm (collectInTyp seen τ) a
   | .set τ _ a _ v => collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) v
-  | .assertEq τ _ a b r =>
+  | .assertEq τ _ a b _ r =>
     collectInTypedTerm
       (collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b) r
   | .ioSetInfo τ _ c k i l r =>
@@ -740,7 +741,7 @@ def collectCalls (decls : Typed.Decls)
     collectCalls decls (collectCalls decls seen c) k
   | .proj _ _ a _ | .get _ _ a _ | .slice _ _ a _ _ => collectCalls decls seen a
   | .set _ _ a _ v => collectCalls decls (collectCalls decls seen a) v
-  | .assertEq _ _ a b r =>
+  | .assertEq _ _ a b _ r =>
     collectCalls decls (collectCalls decls (collectCalls decls seen a) b) r
   | .ioSetInfo _ _ c k i l r =>
     collectCalls decls
@@ -803,9 +804,9 @@ def substInTypedTerm (subst : Global → Option Typ) : Typed.Term → Typed.Term
   | .store τ e a => .store (Typ.instantiate subst τ) e (substInTypedTerm subst a)
   | .load τ e a => .load (Typ.instantiate subst τ) e (substInTypedTerm subst a)
   | .ptrVal τ e a => .ptrVal (Typ.instantiate subst τ) e (substInTypedTerm subst a)
-  | .assertEq τ e a b r =>
+  | .assertEq τ e a b msg r =>
     .assertEq (Typ.instantiate subst τ) e (substInTypedTerm subst a)
-              (substInTypedTerm subst b) (substInTypedTerm subst r)
+              (substInTypedTerm subst b) msg (substInTypedTerm subst r)
   | .ioGetInfo τ e c k =>
     .ioGetInfo (Typ.instantiate subst τ) e
       (substInTypedTerm subst c) (substInTypedTerm subst k)

Ix/Aiur/Compiler/Lower.lean

@@ -267,10 +267,10 @@ def toIndex
     let ptr ← expectIdx layoutMap bindings ptr
     pushOp (.load size ptr) size
   | .ptrVal _ _ ptr => toIndex layoutMap bindings ptr
-  | .assertEq _ _ a b ret => do
+  | .assertEq _ _ a b msg ret => do
     let a ← toIndex layoutMap bindings a
     let b ← toIndex layoutMap bindings b
-    modify fun stt => { stt with ops := stt.ops.push (.assertEq a b) }
+    modify fun stt => { stt with ops := stt.ops.push (.assertEq a b msg) }
     toIndex layoutMap bindings ret
   | .ioGetInfo _ _ channel key => do
     let channel ← expectIdx layoutMap bindings channel
@@ -477,10 +477,10 @@ def Concrete.Term.compile
     let term ← term.mapM (toIndex layoutMap bindings)
     modify fun stt => { stt with ops := stt.ops.push (.debug label term) }
     ret.compile returnTyp layoutMap bindings yieldCtrl
-  | .assertEq _ _ a b ret => do
+  | .assertEq _ _ a b msg ret => do
     let a ← toIndex layoutMap bindings a
     let b ← toIndex layoutMap bindings b
-    modify fun stt => { stt with ops := stt.ops.push (.assertEq a b) }
+    modify fun stt => { stt with ops := stt.ops.push (.assertEq a b msg) }
     ret.compile returnTyp layoutMap bindings yieldCtrl
   | .ioSetInfo _ _ channel key idx len ret => do
     let channel ← toIndex layoutMap bindings channel

Ix/Aiur/Compiler/Match.lean

@@ -369,7 +369,8 @@ def typedToSimple : Term → Simple.Term
   | .store τ e a => .store τ e (typedToSimple a)
   | .load τ e a => .load τ e (typedToSimple a)
   | .ptrVal τ e a => .ptrVal τ e (typedToSimple a)
-  | .assertEq τ e a b r => .assertEq τ e (typedToSimple a) (typedToSimple b) (typedToSimple r)
+  | .assertEq τ e a b msg r =>
+    .assertEq τ e (typedToSimple a) (typedToSimple b) msg (typedToSimple r)
   | .ioGetInfo τ e c k => .ioGetInfo τ e (typedToSimple c) (typedToSimple k)
   | .ioSetInfo τ e c k i l r =>
     .ioSetInfo τ e (typedToSimple c) (typedToSimple k) (typedToSimple i)

Ix/Aiur/Compiler/Simple.lean

@@ -103,11 +103,11 @@ def simplifyTypedTerm (decls : Source.Decls) : Term → Except CheckError Term
         | some sub => do pure (some (← simplifyTypedTerm decls sub))
       let r' ← simplifyTypedTerm decls r
       pure (.debug τ e l t' r')
-  | .assertEq τ e a b r => do
+  | .assertEq τ e a b msg r => do
       let a' ← simplifyTypedTerm decls a
       let b' ← simplifyTypedTerm decls b
       let r' ← simplifyTypedTerm decls r
-      pure (.assertEq τ e a' b' r')
+      pure (.assertEq τ e a' b' msg r')
   | .ioSetInfo τ e c k i l r => do
       let c' ← simplifyTypedTerm decls c
       let k' ← simplifyTypedTerm decls k

Ix/Aiur/Interpret.lean

@@ -318,10 +318,13 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
       match ← interp decls bindings t with
       | .pointer _ n => return .field (G.ofNat n)
       | _            => throwErr "ptrVal: expected pointer"
-  | .assertEq t1 t2 ret => do
+  | .assertEq t1 t2 msg ret => do
       let v1 ← interp decls bindings t1
       let v2 ← interp decls bindings t2
-      if v1 != v2 then throwErr s!"assertEq: {v1} ≠ {v2}"
+      if v1 != v2 then
+        match msg with
+        | some m => throwErr s!"assertEq: {v1} ≠ {v2} ({m})"
+        | none   => throwErr s!"assertEq: {v1} ≠ {v2}"
       interp decls bindings ret
   | .u8BitDecomposition t => do
       match ← interp decls bindings t with

Ix/Aiur/Meta.lean

@@ -183,7 +183,7 @@ syntax "set" "(" aiur_trm ", " num ", " aiur_trm ")"                        : ai
 syntax "store" "(" aiur_trm ")"                                              : aiur_trm
 syntax "load" "(" aiur_trm ")"                                               : aiur_trm
 syntax "ptr_val" "(" aiur_trm ")"                                            : aiur_trm
-syntax "assert_eq!" "(" aiur_trm ", " aiur_trm ")" ";" (aiur_trm)?         : aiur_trm
+syntax "assert_eq!" "(" aiur_trm ", " aiur_trm (", " str)? ")" ";" (aiur_trm)? : aiur_trm
 syntax aiur_trm ": " aiur_typ                                               : aiur_trm
 syntax "io_get_info" "(" aiur_trm ", " aiur_trm ")"                          : aiur_trm
 syntax "io_set_info" "(" aiur_trm ", " aiur_trm ", " aiur_trm ", " aiur_trm ")" ";"
@@ -310,8 +310,11 @@ partial def elabTrm : ElabStxCat `aiur_trm
     mkAppM ``Source.Term.load #[← elabTrm a]
   | `(aiur_trm| ptr_val($a:aiur_trm)) => do
     mkAppM ``Source.Term.ptrVal #[← elabTrm a]
-  | `(aiur_trm| assert_eq!($a:aiur_trm, $b:aiur_trm); $[$ret:aiur_trm]?) => do
-    mkAppM ``Source.Term.assertEq #[← elabTrm a, ← elabTrm b, ← elabRet ret]
+  | `(aiur_trm| assert_eq!($a:aiur_trm, $b:aiur_trm $[, $msg:str]?); $[$ret:aiur_trm]?) => do
+    let msgExpr ← match msg with
+      | some m => mkAppM ``Option.some #[mkStrLit m.getString]
+      | none   => mkAppOptM ``Option.none #[Lean.mkConst ``String]
+    mkAppM ``Source.Term.assertEq #[← elabTrm a, ← elabTrm b, msgExpr, ← elabRet ret]
   | `(aiur_trm| $v:aiur_trm : $t:aiur_typ) => do
     mkAppM ``Source.Term.ann #[← elabTyp t, ← elabTrm v]
   | `(aiur_trm| io_get_info($ch:aiur_trm, $key:aiur_trm)) => do
@@ -500,11 +503,11 @@ where
     | `(aiur_trm| ptr_val($a:aiur_trm)) => do
       let a ← replaceToken old new a
       `(aiur_trm| ptr_val($a))
-    | `(aiur_trm| assert_eq!($a:aiur_trm, $b:aiur_trm); $[$ret:aiur_trm]?) => do
+    | `(aiur_trm| assert_eq!($a:aiur_trm, $b:aiur_trm $[, $msg:str]?); $[$ret:aiur_trm]?) => do
       let a ← replaceToken old new a
       let b ← replaceToken old new b
       let ret' ← ret.mapM $ replaceToken old new
-      `(aiur_trm| assert_eq!($a, $b); $[$ret']?)
+      `(aiur_trm| assert_eq!($a, $b $[, $msg]?); $[$ret']?)
     | `(aiur_trm| $v:aiur_trm : $t:aiur_typ) => do
       let v ← replaceToken old new v
       `(aiur_trm| $v : $t)

Ix/Aiur/Semantics/BytecodeEval.lean

@@ -197,7 +197,7 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
     let ptrG ← readIdx st ptr
     let vs ← memLoad st size ptrG.val.toNat
     pure (appendMap st vs)
-  | .assertEq as bs => do
+  | .assertEq as bs _ => do
     let aGs ← readIdxs st as
     let bGs ← readIdxs st bs
     if aGs == bGs then .ok st else .error .assertFailed

Ix/Aiur/Semantics/BytecodeFfi.lean

@@ -184,26 +184,26 @@ private opaque checkAddrWithEnv' : @& Bytecode.Toplevel →
   @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
     Except String ExecuteResult
 
-@[extern "rs_aiur_toplevel_shard_check_with_env"]
-private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
-  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
-    Except String ExecuteResult
-
 /-- Per-claim check against a Rust-owned `EnvHandle`. `useBytecode`
     selects the generic Aiur bytecode interpreter
     (`Bytecode.Toplevel.execute`) over the codegen'd IxVM kernel
     (`execute_ixvm`); useful for tight iteration loops on Lean-side
-    IxVM source where regenerating `crates/ixvm-codegen/src/aiur_ixvm.rs` and
-    recompiling Rust is too slow. -/
+    IxVM source where regenerating the Rust kernel is too slow. -/
 def checkAddrWithEnv (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
   (addrBytes : ByteArray) (useBytecode : Bool := false)
   : Except String (Array G × IOBuffer × Array QueryCount) :=
   (checkAddrWithEnv' toplevel funIdx envHandle addrBytes useBytecode).map
     fun r => (r.output, .ofArrays r.ioData r.ioMap, r.queryCounts)
 
-/-- Per-shard check against a Rust-owned `EnvHandle`. See
-    `checkAddrWithEnv` for `useBytecode` semantics. -/
+@[extern "rs_aiur_toplevel_shard_check_with_env"]
+private opaque shardCheckWithEnv' : @& Bytecode.Toplevel →
+  @& Bytecode.FunIdx → @& EnvHandle → @& ByteArray → Bool →
+    Except String ExecuteResult
+
+/-- Per-shard check with the witness shape (wrapper-augmented byte
+    scope for the kernel's kernel-side blake3'd projection addrs). Claim and
+    digest are identical to `shardCheckWithEnv`'s. -/
 def shardCheckWithEnv (toplevel : @& Bytecode.Toplevel)
   (funIdx : @& Bytecode.FunIdx) (envHandle : @& EnvHandle)
   (ownedBlob : ByteArray) (useBytecode : Bool := false)

Ix/Aiur/Semantics/SourceEval.lean

@@ -337,14 +337,17 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
         match v with
         | .pointer _ n => .ok (.field (G.ofNat n), st')
         | _            => .error (.typeMismatch "ptrVal")
-  | .assertEq t1 t2 ret =>
+  | .assertEq t1 t2 msg ret =>
       match interp decls fuel bindings t1 st with
       | .error e => .error e
       | .ok (v1, st1) =>
         match interp decls fuel bindings t2 st1 with
         | .error e => .error e
         | .ok (v2, st2) =>
-          if v1 != v2 then .error (.typeMismatch "assertEq")
+          if v1 != v2 then
+            .error (.typeMismatch (match msg with
+              | some m => s!"assertEq: {m}"
+              | none   => "assertEq"))
           else interp decls fuel bindings ret st2
   | .u8BitDecomposition t =>
       match interp decls fuel bindings t st with