From 04558e4c1196f1cd804e1324102cf7dc245759e3 Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Wed, 5 Aug 2026 08:37:02 -0700
Subject: [PATCH 1/5] tests(aiur): split proving from execution suites, fix
 early-return semantics

Restructure the Aiur test pipeline around what each mode actually checks:

- `aiur-prove` (renamed from `aiur`) is now the proving suite: 27
  cases, each pinning a distinct constraint, selector-gating, or
  lookup-argument configuration. The toplevel is pruned to functions
  reachable from these cases.
- `aiur-cross` is the compiler/interpreter suite: every case runs
  4-way agreement (Source.Eval, Interpret, Bytecode.Eval, native
  execute) on values and IOBuffer, plus negative-path agreement (all
  engines must reject) for assert / range-check / non-exhaustive-match
  / IO failures. Adds fold, gadget-op matches, and full inline_test
  parity; compiles the toplevel once. New CI step runs it on PRs (it
  previously never ran in CI).
- `aiur-hashes` proves only boundary sizes (blake3 0/1088, sha256
  0/65); other sizes execute against the Rust reference. The
  interpreter now also runs the smallest hash sizes and rbtree-map.
- Test FRI params drop proof-of-work grinding and use numQueries := 64,
  matching the Rust-side unit tests in crates/aiur.
- AiurTestCase: `.prove`/`.interp`/`.exec` constructors with a
  label param; `executionOnly` renamed to `withProof`.
- `ixvm`: the codegen parity gate reuses the `kernelChecks` cases
  (`runParityCase` ignores the FFT pins), removing the duplicated
  per-constant Ixon env load and witness construction (~5.6s of setup);
  the `parityCases` builder is gone.

The 4-way agreement immediately exposed three early-`return` bugs,
fixed here: Source.Eval evaluated `.ret` as a normal value (feeding
non-tail match continuations instead of exiting the function),
Bytecode.Eval treated Ctrl.return like Ctrl.yield (running
matchContinue continuations after a function-level return), and
Interpret.runFunction missed the `.ret` catch for the entry function.
All three now match the Rust executor's semantics.
---
 .github/workflows/ci.yml            |   4 +-
 Ix/Aiur/Interpret.lean              |   5 +-
 Ix/Aiur/Semantics/BytecodeEval.lean |  53 ++--
 Ix/Aiur/Semantics/SourceEval.lean   |  51 ++--
 Tests/Aiur/Aiur.lean                | 397 +++++-----------------------
 Tests/Aiur/Common.lean              |  40 ++-
 Tests/Aiur/Cross.lean               | 192 +++++++++++---
 Tests/Aiur/Hashes.lean              |  36 ++-
 Tests/Aiur/RBTreeMap.lean           |   9 +-
 Tests/Ix/IxVM.lean                  |  15 +-
 Tests/Main.lean                     |  19 +-
 11 files changed, 382 insertions(+), 439 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 952e4d274..9925992ee 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -80,8 +80,10 @@ jobs:
           use-github-cache: false
       - name: Test Ix CLI
         run: lake test --wfail -- cli
+      - name: Aiur compiler and interpreter tests
+        run: lake test --wfail -- aiur-cross
       - name: Aiur tests
-        run: lake test --wfail -- --ignored aiur aiur-hashes ixvm multi-stark recursive-verifier
+        run: lake test --wfail -- --ignored aiur-prove aiur-hashes ixvm multi-stark recursive-verifier
 
   rust-test:
     runs-on: ubuntu-latest
diff --git a/Ix/Aiur/Interpret.lean b/Ix/Aiur/Interpret.lean
index 7b6717367..975d812af 100644
--- a/Ix/Aiur/Interpret.lean
+++ b/Ix/Aiur/Interpret.lean
@@ -489,7 +489,10 @@ def runFunction (decls : Decls) (funcName : Global) (inputs : List Value)
                           expected {f.inputs.length}, got {inputs.length}" []), init)
       else
         let bindings := f.inputs.map (·.1) |>.zip inputs
-        StateT.run (ExceptT.run (interp decls bindings f.body)) init
+        -- `callSite` also catches a top-level early `return` from the entry
+        -- function itself, which otherwise escapes as a `.ret` interrupt.
+        StateT.run (ExceptT.run (callSite funcName inputs
+          (interp decls bindings f.body))) init
   | _ =>
       (.error (.error s!"Function not found: {funcName}" []), init)
 
diff --git a/Ix/Aiur/Semantics/BytecodeEval.lean b/Ix/Aiur/Semantics/BytecodeEval.lean
index 63b23c089..1c6a83aa1 100644
--- a/Ix/Aiur/Semantics/BytecodeEval.lean
+++ b/Ix/Aiur/Semantics/BytecodeEval.lean
@@ -26,7 +26,31 @@ namespace Aiur
 
 namespace Bytecode.Eval
 
-/-- Tagged errors — small enum, no messages, for proof statements. -/
+/-- Width-bucketed memory, matching Rust's `QueryRecord.memory_queries`.
+Outer key is the width; each bucket is an ordered map from flat-width arrays of
+field elements to unit (the index within the bucket is its insertion order). -/
+abbrev MemoryBuckets := IndexMap Nat (IndexMap (Array G) Unit)
+
+structure EvalState where
+  map      : Array G := #[]
+  memory   : MemoryBuckets := default
+  ioBuffer : IOBuffer
+  deriving Inhabited
+
+/-- Opaque `Repr` so `BytecodeError` (whose `earlyReturn` sentinel carries
+the state) can keep its derived instance; the state itself is not printable. -/
+instance : Repr EvalState := ⟨fun _ _ => .text "<EvalState>"⟩
+
+/-- Tagged errors — small enum, no messages, for proof statements.
+
+The `earlyReturn` case is NOT an error: it is the escape channel for
+`Ctrl.return`, which exits the enclosing FUNCTION — unwinding past any
+pending `matchContinue` continuations — while `Ctrl.yield` feeds the
+nearest continuation. It rides the `Except` error track so every
+intermediate frame propagates it for free, and is unwrapped back into a
+normal result at the function boundary (`evalOp .call` and
+`runFunction`) — mirroring the Rust executor's continuation-stack
+truncation on `Ctrl::Return`. -/
 inductive BytecodeError
   | outOfFuel
   | invalidValIdx (v : ValIdx)
@@ -41,19 +65,9 @@ inductive BytecodeError
   | unreachableAfterLayout
   | u8RangeCheckFailed
   | unconstrainedBigUintDivModUnsupported
+  | earlyReturn (outs : Array G) (st : EvalState)
   deriving Repr, Inhabited
 
-/-- Width-bucketed memory, matching Rust's `QueryRecord.memory_queries`.
-Outer key is the width; each bucket is an ordered map from flat-width arrays of
-field elements to unit (the index within the bucket is its insertion order). -/
-abbrev MemoryBuckets := IndexMap Nat (IndexMap (Array G) Unit)
-
-structure EvalState where
-  map      : Array G := #[]
-  memory   : MemoryBuckets := default
-  ioBuffer : IOBuffer
-  deriving Inhabited
-
 /-! ## ValIdx access -/
 
 def readIdx (st : EvalState) (v : ValIdx) : Except BytecodeError G :=
@@ -180,14 +194,16 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
         match fuel with
         | 0 => .error .outOfFuel
         | fuel+1 =>
+          -- Function boundary: an `earlyReturn` escaping the callee's body
+          -- is its normal return value.
           match evalBlock t fuel f.body innerSt with
-          | .error e => .error e
-          | .ok (outs, innerSt') =>
+          | .error (.earlyReturn outs innerSt') | .ok (outs, innerSt') =>
             if outs.size != outputSize then
               .error .callOutputSizeMismatch
             else
               pure (appendMap (setIoBuffer { st with memory := innerSt'.memory }
                                             innerSt'.ioBuffer) outs)
+          | .error e => .error e
     else .error (.invalidFunIdx fi)
   | .store vals => do
     let argGs ← readIdxs st vals
@@ -342,10 +358,15 @@ def evalCtrl (t : Bytecode.Toplevel) (fuel : Nat)
     (ctrl : Ctrl) (st : EvalState) : Except BytecodeError (Array G × EvalState) :=
   match ctrl with
   | .return _ outs =>
+    -- Function-level return: escape via the `earlyReturn` sentinel so a
+    -- pending `matchContinue` continuation is skipped (Rust truncates the
+    -- continuation stack here). Unwrapped at the function boundary.
     match readIdxs st outs with
     | .error e => .error e
-    | .ok gs   => .ok (gs, st)
+    | .ok gs   => .error (.earlyReturn gs st)
   | .yield _ outs =>
+    -- Continuation-level yield: normal result, consumed by the nearest
+    -- enclosing `matchContinue`.
     match readIdxs st outs with
     | .error e => .error e
     | .ok gs   => .ok (gs, st)
@@ -426,8 +447,8 @@ def runFunction (t : Bytecode.Toplevel) (funIdx : FunIdx) (args : Array G)
     else
       let st : EvalState := { map := args, ioBuffer }
       match evalBlock t fuel f.body st with
+      | .error (.earlyReturn outs st') | .ok (outs, st') => .ok (outs, st'.ioBuffer)
       | .error e => .error e
-      | .ok (outs, st') => .ok (outs, st'.ioBuffer)
   else .error (.invalidFunIdx funIdx)
 
 end Bytecode.Eval
diff --git a/Ix/Aiur/Semantics/SourceEval.lean b/Ix/Aiur/Semantics/SourceEval.lean
index 3e49839c5..57ab000ac 100644
--- a/Ix/Aiur/Semantics/SourceEval.lean
+++ b/Ix/Aiur/Semantics/SourceEval.lean
@@ -29,7 +29,31 @@ namespace Source.Eval
 
 open Source
 
-/-- Tagged errors — small enum, no messages, for use in proof statements. -/
+abbrev Bindings := List (Local × Value)
+/-- Memory store, width-bucketed to match Rust `src/aiur/execute.rs`
+`memory_queries: HashMap<size, IndexMap<Vec<G>, QueryResult>>`. Each width
+has its own `IndexMap`; `ptrVal` returns the local index within its width's
+bucket. Distinct-width pointers may share the same local index. -/
+abbrev Store    := Std.HashMap Nat (IndexMap (Array Value) Unit)
+
+structure EvalState where
+  store    : Store := {}
+  ioBuffer : IOBuffer
+  deriving Inhabited
+
+/-- Opaque `Repr` so `SourceError` (whose `earlyReturn` sentinel carries the
+state) can keep its derived instance; the state itself is not printable. -/
+instance : Repr EvalState := ⟨fun _ _ => .text "<EvalState>"⟩
+
+/-- Tagged errors — small enum, no messages, for use in proof statements.
+
+The `earlyReturn` case is NOT an error: it is the escape channel for an
+explicit `return` inside a function body (e.g. in a non-tail match arm).
+It rides the `Except` error track so that every intermediate combinator
+propagates it for free, and is unwrapped back into a normal result at the
+function-call boundary (`applyGlobal`) — mirroring the Rust executor,
+where `Ctrl::Return` unwinds the continuation stack and exits the
+function. It never escapes `runFunction`. -/
 inductive SourceError
   | outOfFuel
   | unboundVar (l : Local)
@@ -46,20 +70,9 @@ inductive SourceError
   | invalidPointer (n : Nat)
   | notCallable (g : Global)
   | notAFunctionValue
+  | earlyReturn (v : Value) (st : EvalState)
   deriving Repr, Inhabited
 
-abbrev Bindings := List (Local × Value)
-/-- Memory store, width-bucketed to match Rust `src/aiur/execute.rs`
-`memory_queries: HashMap<size, IndexMap<Vec<G>, QueryResult>>`. Each width
-has its own `IndexMap`; `ptrVal` returns the local index within its width's
-bucket. Distinct-width pointers may share the same local index. -/
-abbrev Store    := Std.HashMap Nat (IndexMap (Array Value) Unit)
-
-structure EvalState where
-  store    : Store := {}
-  ioBuffer : IOBuffer
-  deriving Inhabited
-
 /-- Result of evaluation: either a successful value+state pair, or an error. -/
 abbrev EvalResult := Except SourceError (Value × EvalState)
 
@@ -160,6 +173,7 @@ def applyGlobal (decls : Decls) (fuel : Nat) (g : Global) (args : List Value)
         else
           let bindings := f.inputs.map (·.1) |>.zip args
           match interp decls fuel bindings f.body st with
+          | .error (.earlyReturn v st') => .ok (v, st')
           | .error e => .error e
           | .ok (v, st') => .ok (v, st')
     | some (.constructor _ _) => .ok (.ctor g args.toArray, st)
@@ -205,10 +219,13 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
       | .ok (vs, st') => .ok (.array vs, st')
   | .ann _ t => interp decls fuel bindings t st
   | .ret sub =>
-      -- Explicit returns only appear inside function bodies; the body recursion
-      -- here returns normally (the surrounding caller treats the full body value
-      -- as the return value).
-      interp decls fuel bindings sub st
+      -- Escape to the enclosing function boundary via the `earlyReturn`
+      -- sentinel: a `return` inside a non-tail match arm (or any other
+      -- nested position) must NOT feed the surrounding continuation.
+      -- `applyGlobal`/`runFunction` unwrap it into a normal result.
+      match interp decls fuel bindings sub st with
+      | .error e => .error e
+      | .ok (v, st') => .error (.earlyReturn v st')
   | .let p t1 t2 =>
       match interp decls fuel bindings t1 st with
       | .error e => .error e
diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean
index a19ab7229..219113be7 100644
--- a/Tests/Aiur/Aiur.lean
+++ b/Tests/Aiur/Aiur.lean
@@ -7,27 +7,17 @@ public section
 
 open LSpec
 
+-- The PROVING corpus: only functions reachable from the proving cases in
+-- `aiurTestCases` below live here — every function compiles to a circuit
+-- that every proof commits (empty or not). Execution/interpreter coverage
+-- for frontend constructs (data-structure layout, templates, aliases,
+-- single-op wrappers, …) lives in `aiur-cross` (`Tests/Aiur/Cross.lean`).
 def toplevel := ⟦
+  -- Callee for match_lookup_ops and inline_test
   pub fn id(n: G) -> G {
     n
   }
 
-  pub fn proj1(a: G, _b: G) -> G {
-    a
-  }
-
-  pub fn sum(x: G, y: G) -> G {
-    x + y
-  }
-
-  pub fn prod(x: G, y: G) -> G {
-    x * y
-  }
-
-  pub fn sum_prod(x: G, y: G, z: G) -> G {
-    (x + y) * z
-  }
-
   ---------------------------------------------------------------------------
   -- Match coverage: active/inactive paths, inequality witnesses, nesting
   ---------------------------------------------------------------------------
@@ -136,13 +126,6 @@ def toplevel := ⟦
     [eq_zero(a), eq_zero(b), eq_zero(c), eq_zero(d)]
   }
 
-  ---------------------------------------------------------------------------
-  -- Memory: store/load
-  ---------------------------------------------------------------------------
-  pub fn store_and_load(x: G) -> G {
-    load(store(x))
-  }
-
   ---------------------------------------------------------------------------
   -- Enum with 2 constructors, pointer patterns, mutual recursion
   ---------------------------------------------------------------------------
@@ -151,14 +134,6 @@ def toplevel := ⟦
     Succ(&Nat)
   }
 
-  pub fn pointer_match() -> G {
-    let two = Nat.Succ(store(Nat.Succ(store(Nat.Zero))));
-    match two {
-      Nat.Succ(&Nat.Succ(&Nat.Zero)) => 1,
-      _ => 0,
-    }
-  }
-
   fn even(m: Nat) -> G {
     match m {
       Nat.Zero => 1,
@@ -173,26 +148,10 @@ def toplevel := ⟦
     }
   }
 
-  pub fn is_0_even() -> G {
-    even(Nat.Zero)
-  }
-
-  pub fn is_1_even() -> G {
-    even(Nat.Succ(store(Nat.Zero)))
-  }
-
   pub fn is_2_even() -> G {
     even(Nat.Succ(store(Nat.Succ(store(Nat.Zero)))))
   }
 
-  pub fn is_0_odd() -> G {
-    odd(Nat.Zero)
-  }
-
-  pub fn is_1_odd() -> G {
-    odd(Nat.Succ(store(Nat.Zero)))
-  }
-
   ---------------------------------------------------------------------------
   -- 3-constructor enum: tests tag dispatch with 3 cases, constructor field
   -- extraction at different offsets, and padding. Also an implicit
@@ -256,51 +215,6 @@ def toplevel := ⟦
     }
   }
 
-  ---------------------------------------------------------------------------
-  -- Data structure compilation: proj, get, slice, set, destructuring
-  ---------------------------------------------------------------------------
-  pub fn projections(as: (G, G, G, G, G)) -> (G, G) {
-    (proj(as, 1), proj(as, 3))
-  }
-
-  pub fn slice_and_get(as: [G; 5]) -> [G; 2] {
-    let left = as[0 .. 2];
-    let right = as[3 .. 5];
-    [left[1], right[0]]
-  }
-
-  pub fn deconstruct_tuple(as: (G, G, G, G, G)) -> (G, G) {
-    let (_, b, _, d, _) = as;
-    (b, d)
-  }
-
-  pub fn deconstruct_array(as: [G; 5]) -> [G; 2] {
-    let [_, b, _, d, _] = as;
-    [b, d]
-  }
-
-  pub fn array_set(arr: [(G, G); 3]) -> [(G, G); 3] {
-    set(arr, 1, (0, 0))
-  }
-
-  -- proj on mixed-size tuple: offset arithmetic with non-uniform element sizes
-  pub fn proj_mixed(t: (G, (G, G), G)) -> (G, G) {
-    proj(t, 1)
-  }
-
-  -- get at last index + set at first index with eltSize=2: boundary cases
-  pub fn array_get_set(arr: [(G, G); 3]) -> [(G, G); 3] {
-    let p = arr[2];
-    set(arr, 0, p)
-  }
-
-  ---------------------------------------------------------------------------
-  -- Assertion
-  ---------------------------------------------------------------------------
-  pub fn assert_eq_trivial() {
-    assert_eq!([1, 2, 3], [1, 2, 3]);
-  }
-
   ---------------------------------------------------------------------------
   -- IO
   ---------------------------------------------------------------------------
@@ -332,34 +246,6 @@ def toplevel := ⟦
     (u8_add(i_xor_j, i), u8_add(i_xor_j, j))
   }
 
-  pub fn u8_sub_function(i: U8, j: U8) -> (U8, U8) {
-    u8_sub(i, j)
-  }
-
-  pub fn u8_mul_function(i: U8, j: U8) -> (U8, U8) {
-    u8_mul(i, j)
-  }
-
-  pub fn u8_less_than_function(i: U8, j: U8) -> G {
-    u8_less_than(i, j)
-  }
-
-  pub fn u8_and_function(i: U8, j: U8) -> U8 {
-    u8_and(i, j)
-  }
-
-  pub fn u8_or_function(i: U8, j: U8) -> U8 {
-    u8_or(i, j)
-  }
-
-  pub fn u8_chain_rotr7_function(i: U8, j: U8) -> (U8, U8, U8) {
-    u8_chain_rotr7(i, j)
-  }
-
-  pub fn u8_chain_rotr4_function(i: U8, j: U8) -> (U8, U8, U8) {
-    u8_chain_rotr4(i, j)
-  }
-
   -- Full u32 right-rotation by 7, built by chaining the partial gadget over
   -- adjacent little-endian byte pairs (2 lookups + 2 free field adds).
   pub fn u32_rotr7(b: [U8; 4]) -> [U8; 4] {
@@ -380,40 +266,12 @@ def toplevel := ⟦
   }
 
   ---------------------------------------------------------------------------
-  -- u8 range-check / to_field / literal
+  -- u8 range-check / to_field
   ---------------------------------------------------------------------------
   pub fn range_check_id(a: G, b: G) -> (G, G) {
     let (x, y) = u8_range_check(a, b);
     (to_field(x), to_field(y))
   }
-  pub fn u8_lit_xor(a: G) -> G {
-    let (x, _) = u8_range_check(a, a);
-    to_field(u8_xor(x, 200u8))
-  }
-
-  ---------------------------------------------------------------------------
-  -- Fold/iteration
-  ---------------------------------------------------------------------------
-  pub fn fold_matrix_sum(m: [[G; 2]; 2]) -> G {
-    fold(0 .. 2, 0, |acc_outer, @i|
-      fold(0 .. 2, acc_outer, |acc_inner, @j|
-        acc_inner + m[@i][@j]
-      )
-    )
-  }
-
-  ---------------------------------------------------------------------------
-  -- Type aliases: basic, nested, in patterns
-  ---------------------------------------------------------------------------
-  -- `U8` is now a builtin type, not an alias.
-  type U16 = (U8, U8)
-  type U32 = (U16, U16)
-  type U64 = [U8; 8]
-  type Pair = (U8, U8)
-
-  pub fn alias_conversion(x: U64) -> U32 {
-    ((x[0], x[1]), (x[2], x[3]))
-  }
 
   ---------------------------------------------------------------------------
   -- EqZero degree-tracking regression: non-constant eq_zero followed by a
@@ -431,75 +289,6 @@ def toplevel := ⟦
     a + b + d
   }
 
-  ---------------------------------------------------------------------------
-  -- Templates: parametric datatypes and functions
-  ---------------------------------------------------------------------------
-  enum Wrapper‹A› {
-    Mk(A)
-  }
-
-  fn unwrap‹A›(w: Wrapper‹A›) -> A {
-    match w {
-      Wrapper.Mk(x) => x,
-    }
-  }
-
-  pub fn template_basic() -> G {
-    let w = Wrapper.Mk(42);
-    unwrap(w)
-  }
-
-  enum Option‹A› {
-    Some(A),
-    None
-  }
-
-  fn unwrap_or‹A›(opt: Option‹A›, default: A) -> A {
-    match opt {
-      Option.Some(x) => x,
-      Option.None => default,
-    }
-  }
-
-  pub fn template_unwrap_some() -> G {
-    let opt = Option.Some(42);
-    unwrap_or(opt, 0)
-  }
-
-  pub fn template_unwrap_none() -> G {
-    let opt = Option.None;
-    unwrap_or(opt, 99)
-  }
-
-  enum TPair‹A, B› {
-    Mk(A, B)
-  }
-
-  fn tpair_first‹A, B›(p: TPair‹A, B›) -> A {
-    match p {
-      TPair.Mk(a, _) => a,
-    }
-  }
-
-  fn tpair_second‹A, B›(p: TPair‹A, B›) -> B {
-    match p {
-      TPair.Mk(_, b) => b,
-    }
-  }
-
-  pub fn template_pair() -> (G, G) {
-    let p = TPair.Mk(10, 20);
-    (tpair_first(p), tpair_second(p))
-  }
-
-  -- Nested templates: Option‹TPair‹G, G››
-  pub fn template_nested() -> G {
-    let inner = TPair.Mk(3, 4);
-    let opt = Option.Some(inner);
-    let p = unwrap_or(opt, TPair.Mk(0, 0));
-    tpair_first(p) + tpair_second(p)
-  }
-
   ---------------------------------------------------------------------------
   -- Non-tail match: exercises basic, early return, sequential, and nested
   -- cases. All paths tested via a single entry point to minimise proof count.
@@ -857,104 +646,78 @@ def toplevel := ⟦
   }
 ⟧
 
+/-- The PROVING suite: every case runs the full prove+verify pipeline
+    (plus execute and interpret, which come for free in `runTestCase`).
+    A case belongs here only when it pins a distinct constraint,
+    selector-gating, or lookup-argument configuration — the things
+    execution never evaluates. Execution-semantics coverage (compiler,
+    evaluators, interpreter) lives in `aiur-cross`
+    (`Tests/Aiur/Cross.lean`). When several inputs of the same function
+    differ only in which path is active, only a minimal covering set of
+    proofs is kept — the other paths run in `aiur-cross`. -/
 def aiurTestCases : List AiurTestCase := [
-    -- Basic arithmetic
-    .noIO `id #[42] #[42],
-    .noIO `proj1 #[42, 64] #[42],
-    .noIO `sum #[3, 5] #[8],
-    .noIO `prod #[3, 5] #[15],
-    .noIO `sum_prod #[2, 3, 4] #[20],
-
-    -- Match: 1 explicit case + default, exercise both paths
-    { AiurTestCase.noIO `match_mul #[0] #[0] with label := "match_mul(0)" },
-    { AiurTestCase.noIO `match_mul #[2] #[8] with label := "match_mul(2)" },
-
-    -- Match: 3 explicit cases + default (3 inequality witnesses on default)
-    { AiurTestCase.noIO `multi_match #[0] #[100] with label := "multi_match(0)" },
-    { AiurTestCase.noIO `multi_match #[1] #[200] with label := "multi_match(1)" },
-    { AiurTestCase.noIO `multi_match #[2] #[300] with label := "multi_match(2)" },
-    { AiurTestCase.noIO `multi_match #[5] #[25] with label := "multi_match(5)" },
-
-    -- Nested match: 4 leaf selectors, witnesses at both nesting levels
-    { AiurTestCase.noIO `nested_match #[0, 0] #[10]
-        with label := "nested_match(0,0)" },
-    { AiurTestCase.noIO `nested_match #[0, 1] #[20]
-        with label := "nested_match(0,1)" },
-    { AiurTestCase.noIO `nested_match #[2, 0] #[30]
-        with label := "nested_match(2,0)" },
-    { AiurTestCase.noIO `nested_match #[2, 3] #[5]
-        with label := "nested_match(2,3)" },
+    -- Match: 1 explicit case + default, prove both paths (each side gates
+    -- the other's constraints)
+    .prove `match_mul #[0] #[0] (label := "match_mul(0)"),
+    .prove `match_mul #[2] #[8] (label := "match_mul(2)"),
+
+    -- Match: 3 explicit cases + default. Prove one explicit path and the
+    -- default path (3 inequality witnesses); the remaining explicit paths
+    -- exercise the same witness layout
+    .prove `multi_match #[0] #[100] (label := "multi_match(0)"),
+    .prove `multi_match #[5] #[25] (label := "multi_match(5)"),
+
+    -- Nested match: 4 leaf selectors. Prove one explicit-explicit and one
+    -- default-default leaf (witnesses at both nesting levels); the two
+    -- mixed leaves repeat those layouts
+    .prove `nested_match #[0, 0] #[10] (label := "nested_match(0,0)"),
+    .prove `nested_match #[2, 3] #[5] (label := "nested_match(2,3)"),
 
     -- Sel-gating: polynomial constraints (Mul, EqZero, AssertEq).
     -- Inactive branch has assert_eq!(0,1) (fails without sel=0),
     -- different Mul (aux mismatch), different EqZero (witness mismatch).
     -- x=0 chosen so inactive EqZero constraint `sel*(x+1)*x_result =
     -- sel*1*1 = sel` is nonzero without gating.
-    .noIO `match_poly_ops #[0] #[0, 1],
+    .prove `match_poly_ops #[0] #[0, 1],
 
     -- Sel-gating: function and memory lookup multiplicity
-    .noIO `match_lookup_ops #[42] #[42, 42],
+    .prove `match_lookup_ops #[42] #[42, 42],
 
     -- Sel-gating: gadget lookups (Bytes1, Bytes2) and U32LessThan polynomial
     -- constraints (swapped args on inactive path create decomposition mismatch)
-    .noIO `match_gadget_ops #[45, 131] #[22, 174, 1],
+    .prove `match_gadget_ops #[45, 131] #[22, 174, 1],
 
     -- Sel-gating: multi-output gadget lookups (Bytes2 output_size=2,
     -- Bytes1 output_size=8). Guards against partial fixes that only
     -- address output_size=1.
-    .noIO `match_gadget_ops_multi #[45, 131] #[176, 0, 1, 0, 1, 1, 0, 1, 0, 0],
+    .prove `match_gadget_ops_multi #[45, 131] #[176, 0, 1, 0, 1, 1, 0, 1, 0, 0],
 
     -- EqZero: constant path (c=0, d=101) and non-constant path (a=0, b=37)
-    .noIO `eq_zero_dummy #[0, 37] #[1, 0, 1, 0],
-
-    -- Memory
-    .noIO `store_and_load #[42] #[42],
-    .noIO `pointer_match #[] #[1],
+    .prove `eq_zero_dummy #[0, 37] #[1, 0, 1, 0],
 
-    -- Mutual recursion: depths 0–2 cover both branches of even/odd
-    .noIO `is_0_even #[] #[1],
-    .noIO `is_1_even #[] #[0],
-    .noIO `is_2_even #[] #[1],
-    .noIO `is_0_odd #[] #[0],
-    .noIO `is_1_odd #[] #[1],
+    -- Mutual recursion: prove only the deepest case (cross-circuit
+    -- lookups through both functions); shallower depths are sub-traces
+    .prove `is_2_even #[] #[1],
 
     -- 3-constructor enum: tag dispatch, field extraction at varying offsets,
     -- padding. Circle and Rect have degree-2 Mul in different branches with
     -- different operands sharing aux columns (implicit sel-gating test).
+    -- Circle and Rect are the degree-2 pair sharing aux columns (the
+    -- implicit sel-gating test): prove both. Tri (addition only) runs in
+    -- aiur-cross.
     -- Circle(5): [tag=0, r=5, pad, pad] → 5*5 = 25
-    { AiurTestCase.noIO `shape_area #[0, 5, 0, 0] #[25]
-        with label := "shape_area(Circle(5))" },
+    .prove `shape_area #[0, 5, 0, 0] #[25] (label := "shape_area(Circle(5))"),
     -- Rect(3,4): [tag=1, w=3, h=4, pad] → 3*4 = 12
-    { AiurTestCase.noIO `shape_area #[1, 3, 4, 0] #[12]
-        with label := "shape_area(Rect(3,4))" },
-    -- Tri(1,2,3): [tag=2, a=1, b=2, c=3] → 1+2+3 = 6
-    { AiurTestCase.noIO `shape_area #[2, 1, 2, 3] #[6]
-        with label := "shape_area(Tri(1,2,3))" },
+    .prove `shape_area #[1, 3, 4, 0] #[12] (label := "shape_area(Rect(3,4))"),
 
     -- Constrained recursion
-    { AiurTestCase.noIO `factorial #[5] #[120] with label := "factorial(5)" },
+    .prove `factorial #[5] #[120] (label := "factorial(5)"),
 
-    -- Fibonacci (left intact)
-    { AiurTestCase.noIO `fibonacci #[0] #[1] with label := "fibonacci(0)" },
-    { AiurTestCase.noIO `fibonacci #[1] #[1] with label := "fibonacci(1)" },
-    { AiurTestCase.noIO `fibonacci #[6] #[13] with label := "fibonacci(6)" },
+    -- Fibonacci: prove the deep case (call-lookup multiplicities > 1)
+    .prove `fibonacci #[6] #[13] (label := "fibonacci(6)"),
 
     -- Unconstrained recursion: mixed constrained/unconstrained calls
-    .noIO `unconstrained_fibonacci #[6] #[13],
-
-    -- Data structure compilation
-    .noIO `projections #[1, 2, 3, 4, 5] #[2, 4],
-    .noIO `slice_and_get #[1, 2, 3, 4, 5] #[2, 4],
-    .noIO `deconstruct_tuple #[1, 2, 3, 4, 5] #[2, 4],
-    .noIO `deconstruct_array #[1, 2, 3, 4, 5] #[2, 4],
-    .noIO `array_set #[1, 1, 2, 2, 3, 3] #[1, 1, 0, 0, 3, 3],
-    -- proj on (G, (G,G), G): tests offset arithmetic with mixed element sizes
-    .noIO `proj_mixed #[1, 2, 3, 4] #[2, 3],
-    -- get at last index + set at first index with eltSize=2: boundary cases
-    .noIO `array_get_set #[1, 1, 2, 2, 3, 3] #[3, 3, 2, 2, 3, 3],
-
-    -- Assertion
-    .noIO `assert_eq_trivial #[] #[],
+    .prove `unconstrained_fibonacci #[6] #[13],
 
     -- IO
     { functionName := `read_write_io
@@ -968,53 +731,33 @@ def aiurTestCases : List AiurTestCase := [
          .ofList [((0, #[0]), ⟨0, 4⟩), ((1, #[0]), ⟨0, 4⟩),
                   ((0, #[1]), ⟨0, 8⟩)]⟩ },
 
-    -- Byte operations
-    .noIO `shr_shr_shl_decompose #[87] #[0, 1, 0, 1, 0, 1, 0, 0],
-    .noIO `u8_add_xor #[45, 131] #[219, 0, 49, 1],
-    .noIO `u8_sub_function #[45, 131] #[170, 1],
-    .noIO `u8_mul_function #[45, 131] #[7, 23],
-    .noIO `u8_less_than_function #[45, 131] #[1],
-    .noIO `u8_and_function #[45, 131] #[1],
-    .noIO `u8_or_function #[45, 131] #[175],
-    .noIO `u8_chain_rotr7_function #[45, 131] #[6, 1, 90],
-    .noIO `u8_chain_rotr4_function #[45, 131] #[50, 8, 208],
-    .noIO `u32_rotr7 #[45, 131, 200, 17] #[6, 145, 35, 90],
-
-    -- u8 range-check / to_field / literal (exercises the U8RangeCheck circuit op)
-    .noIO `range_check_id #[45, 200] #[45, 200],
-    .noIO `range_check_id #[0, 255] #[0, 255],
-    .noIO `u8_lit_xor #[45] #[229],
-
-    -- u32 comparison: a < b, a > b, a = b
-    { AiurTestCase.noIO `u32_less_than_function #[300, 500] #[1]
-        with label := "u32_less_than(300,500)" },
-    { AiurTestCase.noIO `u32_less_than_function #[500, 300] #[0]
-        with label := "u32_less_than(500,300)" },
-    { AiurTestCase.noIO `u32_less_than_function #[500, 500] #[0]
-        with label := "u32_less_than(500,500)" },
-
-    -- Fold/iteration
-    .noIO `fold_matrix_sum #[1, 2, 3, 4] #[10],
-
-    -- Type aliases
-    { AiurTestCase.noIO `alias_conversion #[1, 2, 3, 4, 5, 6, 7, 8] #[1, 2, 3, 4]
-        with label := "alias_conversion (U64 = [U8; 8], U32 = (U16, U16))" },
+    -- Byte operations: the gadget LOOKUP ARGUMENT (Bytes1/Bytes2
+    -- multiplicities) is what proving checks; op results are table
+    -- content, verified by execution. Prove one Bytes1 chain, one
+    -- multi-output Bytes2 case, and the chain-gadget combination; the
+    -- single-op wrappers repeat the same lookup mechanics in aiur-cross.
+    .prove `shr_shr_shl_decompose #[87] #[0, 1, 0, 1, 0, 1, 0, 0],
+    .prove `u8_add_xor #[45, 131] #[219, 0, 49, 1],
+    .prove `u32_rotr7 #[45, 131, 200, 17] #[6, 145, 35, 90],
+
+    -- u8 range-check: prove the boundary case (U8RangeCheck circuit op)
+    .prove `range_check_id #[0, 255] #[0, 255],
+
+    -- u32 comparison: prove strict-less and the equality edge (distinct
+    -- carry-chain witnesses); a > b repeats the a = b carry layout
+    .prove `u32_less_than_function #[300, 500] #[1]
+      (label := "u32_less_than(300,500)"),
+    .prove `u32_less_than_function #[500, 500] #[0]
+      (label := "u32_less_than(500,500)"),
 
     -- EqZero degree-tracking regression (eq_zero(3)=0, 100, 3*3=9, 9*9=81, 0+100+81=181)
-    .noIO `eq_zero_degree_desync #[3] #[181],
-
-    -- Templates
-    .noIO `template_basic #[] #[42],
-    .noIO `template_unwrap_some #[] #[42],
-    .noIO `template_unwrap_none #[] #[99],
-    .noIO `template_pair #[] #[10, 20],
-    .noIO `template_nested #[] #[7],
+    .prove `eq_zero_degree_desync #[3] #[181],
 
     -- Non-tail match: all patterns in one proof (incl. function-call scrutinee)
-    .noIO `non_tail_match #[] #[2593],
+    .prove `non_tail_match #[] #[2593],
 
     -- Inlined function calls (`@fn(args)`): all scenarios in one proof
-    .noIO `inline_test #[] #[3182],
+    .prove `inline_test #[] #[3182],
   ]
 
 end
diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean
index b7fc720b3..182af0231 100644
--- a/Tests/Aiur/Common.lean
+++ b/Tests/Aiur/Common.lean
@@ -1,7 +1,6 @@
 module
 
 public import LSpec
-public import Tests.Gen.Basic
 public import Ix.Unsigned
 public import Ix.Aiur.Goldilocks
 public import Ix.Aiur.Protocol
@@ -11,8 +10,12 @@ public import Ix.Aiur.Statistics
 
 public section
 
-open LSpec SlimCheck Gen
+open LSpec
 
+/-- Every case executes; `interpret` and `withProof` independently add the
+    interpreter agreement check and the prove/verify pipeline. All three
+    used combinations have a constructor: `prove` (execute + interpret +
+    prove), `interp` (execute + interpret), `exec` (execute only). -/
 structure AiurTestCase where
   functionName : Lean.Name
   label : String := toString functionName
@@ -21,31 +24,46 @@ structure AiurTestCase where
   inputIOBuffer : Aiur.IOBuffer := default
   expectedIOBuffer : Aiur.IOBuffer := default
   interpret : Bool := true
-  executionOnly : Bool := false
+  withProof : Bool := true
   /-- When set, asserts the total FFT cost equals this value (rounded to
       `UInt64`). Pins per-circuit cost regressions: any kernel change that
       shifts FFT cost forces a manual update to the expected value. -/
   expectedFftCost : Option Nat := none
 
-def AiurTestCase.noIO (functionName : Lean.Name)
-    (input expectedOutput : Array Aiur.G) : AiurTestCase :=
-  { functionName, input, expectedOutput }
+/-- Full pipeline: execute + interpret + prove/verify. -/
+def AiurTestCase.prove (functionName : Lean.Name)
+    (input expectedOutput : Array Aiur.G)
+    (label : String := toString functionName) : AiurTestCase :=
+  { functionName, label, input, expectedOutput }
 
+/-- Execute + interpret, no proof. -/
+def AiurTestCase.interp (functionName : Lean.Name)
+    (input expectedOutput : Array Aiur.G)
+    (label : String := toString functionName) : AiurTestCase :=
+  { functionName, label, input, expectedOutput, withProof := false }
+
+/-- Execute only. -/
 def AiurTestCase.exec (functionName : Lean.Name)
-    (input : Array Aiur.G := #[]) (expectedOutput : Array Aiur.G := #[]) : AiurTestCase :=
-  { functionName, input, expectedOutput, interpret := false, executionOnly := true }
+    (input : Array Aiur.G := #[]) (expectedOutput : Array Aiur.G := #[])
+    (label : String := toString functionName) : AiurTestCase :=
+  { functionName, label, input, expectedOutput,
+    interpret := false, withProof := false }
 
 def commitmentParameters : Aiur.CommitmentParameters := {
   logBlowup := 2
   capHeight := 0
 }
 
+/-- Test-only FRI parameters: soundness margin is irrelevant here, so no
+    proof-of-work grinding (it adds a fixed 2^bits hashing cost to every
+    proof and tests nothing) and the same query count the Rust-side unit
+    tests use (`crates/aiur/src/synthesis.rs`). -/
 def friParameters : Aiur.FriParameters := {
   logFinalPolyLen := 0
   maxLogArity := 1
-  numQueries := 100
+  numQueries := 64
   commitProofOfWorkBits := 0
-  queryProofOfWorkBits := 20
+  queryProofOfWorkBits := 0
 }
 
 structure AiurTestEnv where
@@ -102,7 +120,7 @@ def AiurTestEnv.runTestCase (env : AiurTestEnv) (testCase : AiurTestCase) : Test
     let interpTest :=
       if testCase.interpret then env.interpTest testCase execOutput execIOBuffer
       else .done
-    if testCase.executionOnly then execTest ++ interpTest
+    if !testCase.withProof then execTest ++ interpTest
     else
       let (claim, proof, ioBuffer) := env.aiurSystem.prove
         funIdx testCase.input testCase.inputIOBuffer
diff --git a/Tests/Aiur/Cross.lean b/Tests/Aiur/Cross.lean
index fe9a3252d..03cacbcbd 100644
--- a/Tests/Aiur/Cross.lean
+++ b/Tests/Aiur/Cross.lean
@@ -5,14 +5,21 @@ public import Ix.Aiur
 public import Ix.Aiur.Meta
 
 /-!
-End-to-end pipeline cross-tests for `Ix/Aiur`.
+End-to-end pipeline cross-tests for `Ix/Aiur`: the compiler and
+interpreter suite.
 
 A single `toplevel` collects every Aiur surface-language program needed
 by the test corpus (datatypes, type aliases, mutually-recursive
 functions, etc.). The `runAgreement` helper evaluates one entry point
-through both the source-level reference evaluator (`Source.Eval`) and
-the lowered bytecode evaluator (`Bytecode.Eval`), asserting that the
-flat-encoded return value and the `IOBuffer` agree.
+through every execution-level engine — the source-level reference
+evaluator (`Source.Eval`), the source interpreter (`Aiur.Interpret`),
+the lowered bytecode evaluator (`Bytecode.Eval`) and the native
+bytecode executor — asserting that the flat-encoded return value and
+the `IOBuffer` agree across all of them.
+
+Proving lives elsewhere: the `aiur-prove` suite (`Tests/Aiur/Aiur.lean`)
+proves the constraint/lookup configurations, and this suite carries the
+execution-semantics coverage.
 -/
 
 public section
@@ -470,6 +477,32 @@ def toplevel : Source.Toplevel := ⟦
     }
   }
 
+  -- Gadget ops under a match: same shapes the `aiur-prove` suite proves for
+  -- sel-gating; here they pin the execution semantics of gadget calls
+  -- inside branches
+  pub fn match_gadget_ops(i: U8, j: U8) -> (U8, U8, G) {
+    match 0 {
+      0 => (u8_shift_right(i), u8_xor(i, j), u32_less_than(to_field(i), to_field(j))),
+      1 => (u8_shift_right(i), u8_xor(i, j), u32_less_than(to_field(j), to_field(i))),
+    }
+  }
+
+  pub fn match_gadget_ops_multi(i: U8, j: U8) -> ((U8, U8), [G; 8]) {
+    match 0 {
+      0 => (u8_add(i, j), u8_bit_decomposition(i)),
+      1 => (u8_add(i, j), u8_bit_decomposition(i)),
+    }
+  }
+
+  -- Fold/iteration: compile-time unrolling with `@`-indices
+  pub fn fold_matrix_sum(m: [[G; 2]; 2]) -> G {
+    fold(0 .. 2, 0, |acc_outer, @i|
+      fold(0 .. 2, acc_outer, |acc_inner, @j|
+        acc_inner + m[@i][@j]
+      )
+    )
+  }
+
   -- Nested type aliases (`U8` is now a builtin type, not an alias)
   type U16 = (U8, U8)
   type U32 = (U16, U16)
@@ -1073,14 +1106,23 @@ def toplevel : Source.Toplevel := ⟦
     + r11 + r12 + r13 + r14 + r15 + r16 + r17 + r18 + r19 + r20 + r21
   }
 
-  -- Inlined function calls (`@fn(args)`): both evaluators execute an
-  -- inlined call exactly like a normal one, so source/bytecode agreement
+  -- Inlined function calls (`@fn(args)`): the engines execute an
+  -- inlined call exactly like a normal one, so cross-engine agreement
   -- checks the splice (alpha-renaming, nesting, strict-position hoisting,
-  -- branching callees) preserved the semantics.
+  -- branching callees, multi-output and gadget callees) preserved the
+  -- semantics. Mirrors the `aiur-prove` suite's `inline_test` scenarios.
+  fn inl_double(x: G) -> G {
+    let t = x + x;
+    t
+  }
+
   fn inl_sq(x: G) -> G { x * x }
 
   fn inl_sq_plus(x: G, y: G) -> G { @inl_sq(x) + y }
 
+  -- Multi-output callee
+  fn inl_pair(x: G) -> (G, G) { (x + 1, x * 2) }
+
   fn inl_sign(x: G) -> G {
     match x {
       0 => 0,
@@ -1088,57 +1130,126 @@ def toplevel : Source.Toplevel := ⟦
     }
   }
 
+  -- Gadget lookup inside the callee
+  fn inl_add8(a: U8, b: U8) -> (U8, U8) { u8_add(a, b) }
+
   -- Single aggregate entry: every scenario in one agreement run.
   pub fn inline_test() -> G {
     -- Basic splice
-    let r1 = @inl_sq(5) + 1;                      -- 26
+    let r1 = @inl_double(21);                     -- 42
     -- Nested splice (callee @-inlines another helper)
     let r2 = @inl_sq_plus(3, 4);                  -- 13
-    -- Capture safety: caller local named like a callee binding, argument
-    -- mentions it
+    -- Capture safety: caller binds `t` (the callee's local name) and the
+    -- argument mentions it
     let t = 5;
-    let r3 = @inl_sq(t + 1) + t;                  -- 41
-    -- Strict positions: operator operands
-    let r4 = @inl_sq(3) + @inl_sq(4) * 100;       -- 1609
+    let r3 = @inl_double(t + 1) + t;              -- 17
+    -- Strict positions: array elements, operator operands, call argument
+    let arr = [@inl_double(3), @inl_sq(3)];       -- [6, 9]
+    let r4 = arr[0] + arr[1] * 100;               -- 906
+    let r5 = @inl_double(3) + @inl_sq(3);         -- 15
+    let r6 = id(@inl_double(7));                  -- 14
+    -- Multi-output callee
+    let (p1, p2) = @inl_pair(5);                  -- (6, 10)
+    let r7 = p1 + p2 * 100;                       -- 1006
     -- Branching callee in operand position, both paths (the spliced match
     -- gets bound to a fresh local before hoisting)
-    let r5 = @inl_sign(0) + @inl_sign(7) * 100;   -- 100
+    let r8 = @inl_sign(0) + @inl_sign(5) * 100;   -- 100
     -- Same callee inlined and normally called
-    let r6 = @inl_sq(3) + inl_sq(4);              -- 25
-    r1 + r2 + r3 + r4 + r5 + r6
+    let r9 = @inl_sq(3) + inl_sq(4);              -- 25
+    -- Gadget lookup in the callee
+    let (s, c) = @inl_add8(200u8, 100u8);         -- (44, 1)
+    let r10 = to_field(s) + to_field(c) * 1000;   -- 1044
+    r1 + r2 + r3 + r4 + r5 + r6 + r7 + r8 + r9 + r10
   }
 ⟧
 
-/-- Generic helper: run both evaluators on `entryName` with `inputs` as
-the source-level argument list, asserting that the flat-encoded return
-value and the `IOBuffer` agree. An optional `io` arg seeds both evaluators
-with a pre-populated `IOBuffer`. -/
+/-- Compiler outputs shared by every agreement case. Top-level closed
+defs are computed once at module initialization, so the toplevel is
+type-checked and compiled a single time instead of once per case. -/
+private def crossDecls : Except String Source.Decls :=
+  toplevel.mkDecls.mapError toString
+
+private def crossCompiled : Except String CompiledToplevel :=
+  toplevel.compile
+
+/-- Generic helper: run one entry point through all four engines — the
+source-level reference evaluator (`Source.Eval`), the source interpreter
+(`Aiur.Interpret`), the lowered bytecode evaluator (`Bytecode.Eval`) and
+the native bytecode executor — asserting that the flat-encoded return
+value and the `IOBuffer` of each engine agree with the reference
+evaluator. An optional `io` arg seeds every engine with a pre-populated
+`IOBuffer`. -/
 def runAgreement
     (label : String) (entryName : String)
     (inputs : List Value) (io : IOBuffer := default) (fuel : Nat := 1000) :
     TestSeq := Id.run do
   let globalName : Global := .init entryName
-  match toplevel.mkDecls with
-  | .error _ => pure (test s!"{label}: mkDecls" false)
+  match crossDecls with
+  | .error e => pure (test s!"{label}: mkDecls ({e})" false)
   | .ok decls =>
     match Source.Eval.runFunction decls globalName inputs io fuel with
     | .error e => pure (test s!"{label}: Source.Eval ({repr e})" false)
     | .ok (srcVal, srcIo) =>
-      match toplevel.compile with
+      match crossCompiled with
       | .error e => pure (test s!"{label}: Compile ({e})" false)
       | .ok ct =>
         let funIdx := ct.getFuncIdx (.mkSimple entryName) |>.getD 0
         let funcIdx := fun g => ct.nameMap[g]?
+        let srcFlat := flattenValue decls funcIdx srcVal
         let flatArgs : Array Aiur.G := inputs.foldl
           (fun acc v => acc ++ flattenValue decls funcIdx v) #[]
-        match Bytecode.Eval.runFunction ct.bytecode funIdx flatArgs io fuel with
-        | .error e => pure (test s!"{label}: Bytecode.Eval ({repr e})" false)
-        | .ok (bcOut, bcIo) =>
-          let srcFlat := flattenValue decls funcIdx srcVal
-          let valTest := test s!"{label}: values agree (src={srcFlat}, bc={bcOut})"
-            (srcFlat == bcOut)
-          let ioTest  := test s!"{label}: io agree" (srcIo == bcIo)
-          pure (valTest ++ ioTest)
+        let bcTests := match Bytecode.Eval.runFunction ct.bytecode funIdx flatArgs io fuel with
+          | .error e => test s!"{label}: Bytecode.Eval ({repr e})" false
+          | .ok (bcOut, bcIo) =>
+            test s!"{label}: Bytecode.Eval values agree (src={srcFlat}, bc={bcOut})"
+              (srcFlat == bcOut)
+            ++ test s!"{label}: Bytecode.Eval io agree" (srcIo == bcIo)
+        let interpTests := match Aiur.runFunction decls globalName inputs io with
+          | (.error e, _) => test s!"{label}: Interpret ({e})" false
+          | (.ok interpVal, state) =>
+            let interpFlat := flattenValue decls funcIdx interpVal
+            test s!"{label}: Interpret values agree (src={srcFlat}, interp={interpFlat})"
+              (srcFlat == interpFlat)
+            ++ test s!"{label}: Interpret io agree" (srcIo == state.ioBuffer)
+        let execTests := match ct.bytecode.execute funIdx flatArgs io with
+          | .error e => test s!"{label}: execute ({e})" false
+          | .ok (exOut, exIo, _) =>
+            test s!"{label}: execute values agree (src={srcFlat}, exec={exOut})"
+              (srcFlat == exOut)
+            ++ test s!"{label}: execute io agree" (srcIo == exIo)
+        pure (bcTests ++ interpTests ++ execTests)
+
+/-- Negative-path agreement: every engine must REJECT the run. A single
+engine accepting (or crashing differently) where the others error is a
+semantics divergence even though no success value exists to compare —
+the `return`-handling bugs hid exactly this way. Error *messages* are
+engine-specific, so only rejection itself is asserted. -/
+def runFailureAgreement
+    (label : String) (entryName : String)
+    (inputs : List Value) (io : IOBuffer := default) (fuel : Nat := 1000) :
+    TestSeq := Id.run do
+  let globalName : Global := .init entryName
+  match crossDecls, crossCompiled with
+  | .error e, _ => pure (test s!"{label}: mkDecls ({e})" false)
+  | _, .error e => pure (test s!"{label}: Compile ({e})" false)
+  | .ok decls, .ok ct =>
+    let funIdx := ct.getFuncIdx (.mkSimple entryName) |>.getD 0
+    let funcIdx := fun g => ct.nameMap[g]?
+    let flatArgs : Array Aiur.G := inputs.foldl
+      (fun acc v => acc ++ flattenValue decls funcIdx v) #[]
+    let srcRejects := match Source.Eval.runFunction decls globalName inputs io fuel with
+      | .error _ => true | .ok _ => false
+    let bcRejects := match Bytecode.Eval.runFunction ct.bytecode funIdx flatArgs io fuel with
+      | .error _ => true | .ok _ => false
+    let interpRejects := match Aiur.runFunction decls globalName inputs io with
+      | (.error _, _) => true | (.ok _, _) => false
+    let execRejects := match ct.bytecode.execute funIdx flatArgs io with
+      | .error _ => true | .ok _ => false
+    pure <|
+      test s!"{label}: Source.Eval rejects" (srcRejects = true)
+      ++ test s!"{label}: Bytecode.Eval rejects" (bcRejects = true)
+      ++ test s!"{label}: Interpret rejects" (interpRejects = true)
+      ++ test s!"{label}: execute rejects" (execRejects = true)
 
 private def myOpt (limb : String) : Global := Global.init "MyOpt" |>.pushNamespace limb
 private def myOpt2 (limb : String) : Global := Global.init "MyOpt2" |>.pushNamespace limb
@@ -1304,6 +1415,10 @@ def tests : TestSeq :=
   runAgreement "unconstrained_fibonacci(6)" "unconstrained_fibonacci" [6] ++
   runAgreement "match_poly_ops(42)" "match_poly_ops" [42] ++
   runAgreement "match_lookup_ops(42)" "match_lookup_ops" [42] ++
+  runAgreement "match_gadget_ops(45,131)" "match_gadget_ops" [45, 131] ++
+  runAgreement "match_gadget_ops_multi(45,131)" "match_gadget_ops_multi" [45, 131] ++
+  runAgreement "fold_matrix_sum([[1,2],[3,4]])" "fold_matrix_sum"
+    [.array #[.array #[1, 2], .array #[3, 4]]] ++
   runAgreement "alias_conversion[1..8]" "alias_conversion"
     [.array #[1, 2, 3, 4, 5, 6, 7, 8]] ++
   runAgreement "is_0_even" "is_0_even" [] ++
@@ -1366,7 +1481,20 @@ def tests : TestSeq :=
   runAgreement "ntm_recursive_test" "ntm_recursive_test" [] ++
   runAgreement "non_tail_match" "non_tail_match" [] ++
   -- Inlined function calls (`@fn(args)`): all scenarios in one entry
-  runAgreement "inline_test" "inline_test" []
+  runAgreement "inline_test" "inline_test" [] ++
+  -- ----- Negative paths: every engine must reject --------------------------
+  -- assert_eq! mismatch
+  runFailureAgreement "assert_same(7,8) rejects" "assert_same" [7, 8] ++
+  -- u8_range_check out of range
+  runFailureAgreement "range_check_id(300,1) rejects" "range_check_id" [300, 1] ++
+  -- Non-exhaustive match: 8 explicit branches, no default, scrutinee 9
+  runFailureAgreement "ntm_large(9) rejects" "ntm_large" [9] ++
+  -- io_get_info on a missing key (empty IO buffer)
+  runFailureAgreement "read_write_io missing key rejects" "read_write_io" [] ++
+  -- io_read past the arena end: key registered with len 4, arena holds 2
+  runFailureAgreement "read_write_io OOB read rejects" "read_write_io" []
+    (io := { data := .ofList [(0, #[1, 2]), (1, #[5, 6, 7, 8])],
+             map := .ofList [((0, #[0]), ⟨0, 4⟩), ((1, #[0]), ⟨0, 4⟩)] })
 
 end AiurTests.Cross
 
diff --git a/Tests/Aiur/Hashes.lean b/Tests/Aiur/Hashes.lean
index 817b6351d..cb4097229 100644
--- a/Tests/Aiur/Hashes.lean
+++ b/Tests/Aiur/Hashes.lean
@@ -7,7 +7,16 @@ public import Ix.IxVM.Sha256
 public import Tests.Sha256
 public import Blake3.Rust
 
-def mkBlake3HashTestCase (size : Nat) : AiurTestCase :=
+/-!
+The size sweeps exercise execution paths (padding, chunk/block
+boundaries, tree parents); correctness per size is checked against the
+Rust reference output by execution alone. Constraint and lookup coverage
+saturates with one small and one multi-chunk proof per hash, so only the
+`prove := true` sizes pay for prove+verify.
+-/
+
+def mkBlake3HashTestCase (size : Nat) (prove : Bool := false)
+    (interp : Bool := false) : AiurTestCase :=
   let inputBytes := Array.range size |>.map Nat.toUInt8
   let outputBytes := Blake3.Rust.hash ⟨inputBytes⟩ |>.val.data
   let input := inputBytes.map .ofUInt8
@@ -17,9 +26,10 @@ def mkBlake3HashTestCase (size : Nat) : AiurTestCase :=
     -- channel 0; key fixed as #[0]
   { functionName := `blake3_test, label := s!"blake3 (size={size})"
     expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer
-    interpret := false }
+    interpret := interp, withProof := prove }
 
-def mkSha256HashTestCase (size : Nat) : AiurTestCase :=
+def mkSha256HashTestCase (size : Nat) (prove : Bool := false)
+    (interp : Bool := false) : AiurTestCase :=
   let inputBytes := Array.range size |>.map Nat.toUInt8
   let outputBytes := Sha256.hash ⟨inputBytes⟩ |>.data
   let input := inputBytes.map .ofUInt8
@@ -29,16 +39,19 @@ def mkSha256HashTestCase (size : Nat) : AiurTestCase :=
     -- channel 0; key fixed as #[0]
   { functionName := `sha256_test, label := s!"sha256 (size={size})"
     expectedOutput := output, inputIOBuffer := buffer, expectedIOBuffer := buffer
-    interpret := false }
+    interpret := interp, withProof := prove }
 
 public def blake3TestCases : List AiurTestCase := [
-  mkBlake3HashTestCase 0,
-  mkBlake3HashTestCase 32,
+  -- prove: empty input (padding-only path) and a two-chunk input with a
+  -- parent node (chunk = 1024 bytes). interp: the two smallest sizes give
+  -- the interpreter real-program coverage at bounded cost.
+  mkBlake3HashTestCase 0 (prove := true) (interp := true),
+  mkBlake3HashTestCase 32 (interp := true),
   mkBlake3HashTestCase 64,
   mkBlake3HashTestCase 96,
   mkBlake3HashTestCase 1024,
   mkBlake3HashTestCase 1056,
-  mkBlake3HashTestCase 1088,
+  mkBlake3HashTestCase 1088 (prove := true),
   mkBlake3HashTestCase 1120,
   mkBlake3HashTestCase 2048,
   mkBlake3HashTestCase 2080,
@@ -51,8 +64,11 @@ public def blake3TestCases : List AiurTestCase := [
 ]
 
 public def sha256TestCases : List AiurTestCase := [
-  mkSha256HashTestCase 0,
-  mkSha256HashTestCase 1,
+  -- prove: empty input (padding-only path) and a two-block input whose
+  -- length spills past the first block (block = 64 bytes). interp: the two
+  -- smallest sizes give the interpreter real-program coverage at bounded cost.
+  mkSha256HashTestCase 0 (prove := true) (interp := true),
+  mkSha256HashTestCase 1 (interp := true),
   mkSha256HashTestCase 14,
   mkSha256HashTestCase 16,
   mkSha256HashTestCase 17,
@@ -61,7 +77,7 @@ public def sha256TestCases : List AiurTestCase := [
   mkSha256HashTestCase 33,
   mkSha256HashTestCase 63,
   mkSha256HashTestCase 64,
-  mkSha256HashTestCase 65,
+  mkSha256HashTestCase 65 (prove := true),
   mkSha256HashTestCase 120,
   mkSha256HashTestCase 1200,
 ]
diff --git a/Tests/Aiur/RBTreeMap.lean b/Tests/Aiur/RBTreeMap.lean
index 75c6ac67d..488b3fc77 100644
--- a/Tests/Aiur/RBTreeMap.lean
+++ b/Tests/Aiur/RBTreeMap.lean
@@ -6,14 +6,17 @@ public import Ix.IxVM.RBTreeMap
 public section
 
 public def rbTreeMapTestCases : List AiurTestCase := [
-  { AiurTestCase.noIO `rbtree_map_test #[] #[
+  -- Data-structure logic test: asserts insert/lookup outputs. The
+  -- constraint machinery it compiles to (match, load/store, compares) is
+  -- proven by the `aiur-prove` suite, so execute + interpret is the whole
+  -- signal here.
+  .interp `rbtree_map_test #[] #[
       42,
       50, 100, 200,
       999,
       10, 20, 30, 40, 50,
       10, 20, 30, 40, 50,
-      200, 300, 400, 500, 600, 700, 800]
-    with interpret := false },
+      200, 300, 400, 500, 600, 700, 800],
 ]
 
 end
diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean
index b0b9999d2..5967174cb 100644
--- a/Tests/Ix/IxVM.lean
+++ b/Tests/Ix/IxVM.lean
@@ -150,7 +150,7 @@ public def serdeNatAddComm (env : Lean.Environment) : IO AiurTestCase := do
   pure { functionName := `ixon_serde_test, label := "Ixon serde test"
          input := #[.ofNat n], inputIOBuffer := ioBuffer
          expectedIOBuffer := ioBuffer
-         interpret := false, executionOnly := true }
+         interpret := false, withProof := false }
 
 /-- kernel check with equivalent transitive typecheck semantic.
     Reshapes an `Ix.Claim.check target none` request as a `CheckEnv`
@@ -175,7 +175,7 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) :
   pure { functionName := witness.funcName, label := s!"Kernel check {name}"
          input := witness.input, inputIOBuffer := witness.inputIOBuffer
          expectedIOBuffer := witness.inputIOBuffer
-         interpret := false, executionOnly := true }
+         interpret := false, withProof := false }
 
 private def nameOfString (str : String) : Lean.Name :=
   str.splitOn "." |>.foldl (init := .anonymous) fun acc s =>
@@ -288,15 +288,6 @@ public def runParityCase (compiled : Aiur.CompiledToplevel)
           (bQC.zip cQC).all fun (b, c) =>
             b.uniqueRows == c.uniqueRows && b.totalHits == c.totalHits)
 
-/-- Codegen parity fixtures: run each check through both the Aiur
-    bytecode interpreter and the generated Rust kernel, and assert they
-    agree on output, IOBuffer, and QueryCount. This is the gate that keeps
-    `crates/ixvm-codegen` in step with the Lean kernel source — an Aiur
-    edit without a `ix codegen` regen fails here. -/
-public def parityCases (env : Lean.Environment) : IO (List AiurTestCase) := do
-  kernelCheckEntries.mapM fun (name, _) =>
-    kernelCheck (nameOfString name) env
-
 /-! ## Claim variant smoke tests
 
 Each builds an `AiurTestCase` exercising one of the non-`Check-None`
@@ -311,7 +302,7 @@ private def asTestCase (label : String) (witness : ClaimWitness) : AiurTestCase
   { functionName := witness.funcName, label
     input := witness.input, inputIOBuffer := witness.inputIOBuffer
     expectedIOBuffer := witness.inputIOBuffer
-    interpret := false, executionOnly := true }
+    interpret := false, withProof := false }
 
 /-- Locate the first constant in `env.consts` whose `ConstantInfo`
     satisfies `pred`, or fail with `IO.userError`. -/
diff --git a/Tests/Main.lean b/Tests/Main.lean
index 8525fa005..e41da7a7f 100644
--- a/Tests/Main.lean
+++ b/Tests/Main.lean
@@ -119,8 +119,8 @@ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [
 
 /-- Ignored test runners - expensive, deferred IO actions run only when explicitly requested -/
 def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
-  ("aiur", do
-    IO.println "aiur"
+  ("aiur-prove", do
+    IO.println "aiur-prove"
     match AiurTestEnv.build (pure toplevel) with
     | .error e => IO.eprintln s!"Aiur setup failed: {e}"; return 1
     | .ok env => LSpec.lspecEachIO aiurTestCases fun tc => pure (env.runTestCase tc)),
@@ -146,12 +146,6 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
     let revealExpr ← claimRevealDefnExpr claimEnv
     let revealCPrj ← claimRevealCPrj claimEnv
     let containsTc ← claimContains
-    -- Codegen parity gate: the generated Rust kernel is emitted from the
-    -- toplevel, so this runs the same witnesses through both engines and
-    -- asserts they agree. It is only meaningful against a CURRENT
-    -- `ix codegen` output — regenerate after any Aiur edit, or this gate
-    -- compares against a stale kernel.
-    let parityCases ← parityCases env
     -- Shared-infrastructure test entrypoints live only in the FULL
     -- toplevel (pruning drops them so test-only circuits never widen a
     -- committed kernel system).
@@ -176,7 +170,14 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
           [envFull, envFrontier, checkAsm,
            revealFields, revealExpr, revealCPrj, containsTc]).foldl
         (init := .done) fun s tc => s ++ v2Env.runTestCase tc
-      let paritySeq := parityCases.foldl (init := .done) fun s tc =>
+      -- Codegen parity gate: the generated Rust kernel is emitted from
+      -- the toplevel, so this runs the same witnesses through both
+      -- engines and asserts they agree. It is only meaningful against a
+      -- CURRENT `ix codegen` output — regenerate after any Aiur edit, or
+      -- this gate compares against a stale kernel. Reuses the
+      -- `kernelChecks` cases (`runParityCase` ignores the FFT pins), so
+      -- the per-constant witness setup runs once, not twice.
+      let paritySeq := kernelChecks.foldl (init := .done) fun s tc =>
         s ++ runParityCase v2Env.compiled tc
       let fullSeq := [kernelUnitTests, serdeTest].foldl (init := .done)
         fun s tc => s ++ v2FullEnv.runTestCase tc

From b732f51cdf4027b64a93053e5937a23a309aad36 Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Wed, 5 Aug 2026 10:51:09 -0700
Subject: [PATCH 2/5] aiur: fix unconstrained_big_uint_div_mod to return [G; 8]
 limbs
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The op returned its input type verbatim, so the kernel's div/mod hints
came back typed `KLimbs = List‹U64›` — prover advice claiming u8's
"known to be range-checked" contract with no check having run. The
kernel's manual `klimbs_range_check` upheld soundness by discipline
only; the type system was satisfied before it ran.

The checker now gives the op a fixed signature (see
`bigUintDivModResultTyp`): inputs must be a pointer to a list datatype
instantiated at `[U8; 8]`, and each result is the same datatype at
`[G; 8]`. Unconstrained limbs cannot pose as bytes; consumers are
obliged to range-check their way back. Non-conforming inputs fail with
`unconstrainedBigUintDivModType`.

Kernel side, `klimbs_range_check` (check-and-discard) becomes
`glimbs_to_klimbs`: it walks the `List‹[G; 8]›` hint, range-checks
every byte, and rebuilds the limbs from the checked outputs — the only
door from advice back into `KLimbs`. `klimbs_div_mod` converts
before normalizing.

Codegen regenerated. FFT pins re-measured via
`lake test -- --ignored ixvm`: the nine div/mod-dependent constants
and the shard pipeline all shifted marginally down (ppm-level layout
change from the circuit swap); the shard pin message now prints
expected/got like the per-constant pins.
---
 Ix/Aiur/Compiler/Check.lean          | 22 +++++++--
 Ix/IxVM/Kernel/Klimbs.lean           | 62 +++++++++++++------------
 Tests/Ix/IxVM.lean                   | 18 ++++----
 Tests/Main.lean                      |  5 +-
 crates/ixvm-codegen/src/aiur_ixvm.rs | 68 ++++++++++++++++------------
 5 files changed, 102 insertions(+), 73 deletions(-)

diff --git a/Ix/Aiur/Compiler/Check.lean b/Ix/Aiur/Compiler/Check.lean
index 13fb15712..6c365cf64 100644
--- a/Ix/Aiur/Compiler/Check.lean
+++ b/Ix/Aiur/Compiler/Check.lean
@@ -49,6 +49,7 @@ inductive CheckError
   | infiniteType : Nat → Typ → CheckError
   | unresolvedMVar : Nat → CheckError
   | u8LitOutOfRange : Nat → CheckError
+  | unconstrainedBigUintDivModType : Typ → CheckError
   | entryHasPointer : Global → CheckError
   deriving Repr
 
@@ -406,6 +407,20 @@ def zonkTyp (t : Typ) : CheckM Typ := do
   let s ← get
   zonkTypBound (s.nextMVar + 1) {} t
 
+/-- Fixed signature of `unconstrainedBigUintDivMod`: the inputs are lists
+of U64 limbs — a pointer to a list datatype instantiated at `[U8; 8]`
+(e.g. `KLimbs = List‹U64›`) — and each result is the SAME list datatype
+instantiated at `[G; 8]`. The result limbs are UNCONSTRAINED prover
+advice, so they must not type as range-checked bytes; consumers rebuild
+`u8` limbs via `u8_range_check` (see `glimbs_to_klimbs` in the IxVM
+kernel). The list's constructor shape is not verified here; the runtime
+BigUint::div_rem faults on a malformed chain. Takes the ZONKED input
+type. -/
+def bigUintDivModResultTyp : Typ → CheckM Typ
+  | .pointer (.app g #[.array .u8 8]) =>
+    pure (.pointer (.app g #[.array .field 8]))
+  | τ => throw $ .unconstrainedBigUintDivModType τ
+
 def instantiateParams (params : List String) : CheckM (Array Typ × (Global → Option Typ)) := do
   let mvars ← (params.toArray.mapM fun _ => freshMVar)
   pure (mvars, mkParamSubst params mvars)
@@ -795,12 +810,11 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
     let b' ← checkNoEscape b .field
     pure (Typed.Term.u8RangeCheck (.tuple #[.u8, .u8]) false a' b')
   | .unconstrainedBigUintDivMod a b => do
-    -- Both inputs must be the same type (expected `List<U64>` at runtime,
-    -- but the type-checker is generic: any container will type-check, and
-    -- the runtime BigUint::div_rem will fault on a malformed shape).
+    -- See `bigUintDivModResultTyp` for the op's fixed signature.
     let a' ← inferNoEscape a
     let b' ← checkNoEscape b a'.typ
-    pure (Typed.Term.unconstrainedBigUintDivMod (.tuple #[a'.typ, a'.typ]) false a' b')
+    let τ ← bigUintDivModResultTyp (← zonkTyp a'.typ)
+    pure (Typed.Term.unconstrainedBigUintDivMod (.tuple #[τ, τ]) false a' b')
   | .unconstrainedGToBytes a => do
     -- The bytes are UNCONSTRAINED advice typed `u8`; the caller must
     -- range-check them (see `Source.Term.unconstrainedGToBytes`).
diff --git a/Ix/IxVM/Kernel/Klimbs.lean b/Ix/IxVM/Kernel/Klimbs.lean
index 272070395..89dd9b890 100644
--- a/Ix/IxVM/Kernel/Klimbs.lean
+++ b/Ix/IxVM/Kernel/Klimbs.lean
@@ -190,8 +190,11 @@ def klimbs := ⟦
     }
   }
 
-  -- Strip trailing zero limbs (canonicalize `[k, 0, 0]` → `[k]`).
-  -- Force every limb byte of a prover-supplied `KLimbs` into [0, 256).
+  -- Convert a prover-supplied field-typed limb list into a checked
+  -- `KLimbs`: every byte is forced into [0, 256) and the CHECKED outputs
+  -- (typed `u8`) rebuild the limbs. This is the only door from
+  -- `unconstrained_big_uint_div_mod` advice (typed `List‹[G; 8]›` by the
+  -- checker precisely so it cannot pose as bytes) back into `KLimbs`.
   --
   -- `KLimbs` is canonical in two independent ways — no trailing zero
   -- limbs, and every byte in range — and `klimbs_normalize` only
@@ -200,16 +203,17 @@ def klimbs := ⟦
   -- unequal to its canonical form, so `Nat.beq` answers `false` where
   -- Lean answers `true`. `u8_range_check` takes a pair per lookup row,
   -- so eight bytes cost four.
-  fn klimbs_range_check(n: KLimbs) {
+  fn glimbs_to_klimbs(n: List‹[G; 8]›) -> KLimbs {
     match load(n) {
-      ListNode.Nil => (),
+      ListNode.Nil => store(ListNode.Nil),
       ListNode.Cons(limb, rest) =>
         let [b0, b1, b2, b3, b4, b5, b6, b7] = limb;
-        let (_, _) = u8_range_check(to_field(b0), to_field(b1));
-        let (_, _) = u8_range_check(to_field(b2), to_field(b3));
-        let (_, _) = u8_range_check(to_field(b4), to_field(b5));
-        let (_, _) = u8_range_check(to_field(b6), to_field(b7));
-        klimbs_range_check(rest),
+        let (c0, c1) = u8_range_check(b0, b1);
+        let (c2, c3) = u8_range_check(b2, b3);
+        let (c4, c5) = u8_range_check(b4, b5);
+        let (c6, c7) = u8_range_check(b6, b7);
+        store(ListNode.Cons([c0, c1, c2, c3, c4, c5, c6, c7],
+          glimbs_to_klimbs(rest))),
     }
   }
 
@@ -506,27 +510,29 @@ def klimbs := ⟦
   -- `r < b` when `b != 0`. For `b == 0` the op returns `(0, a)`; only the
   -- `q*b + r == a` equality is required (which holds: `0*0 + a == a`).
   --
-  -- Soundness on the prover-supplied bytes: pinned by the explicit
-  -- `klimbs_range_check`es below, NOT by the arithmetic. `u64_mul` was
-  -- rewritten to raw field products plus `#split_carry`, whose u8 checks
-  -- constrain the split OUTPUTS, not the input digits — and it
-  -- re-canonicalizes while multiplying, so a digit-wrong `q` still yields
-  -- a canonical `q*b` and sails through the equality below. That left the
-  -- quotient's VALUE pinned but its representation free, which is enough:
-  -- `klimbs_eq` compares limbs rather than values, so a digit-wrong
-  -- quotient makes `Nat.beq (Nat.div 300 1) 300` answer `false`.
-  -- Trailing junk limbs are caught by the post-normalize equality.
+  -- Soundness on the prover-supplied bytes: pinned by the range checks
+  -- inside `glimbs_to_klimbs` below, NOT by the arithmetic — and the
+  -- checker enforces the discipline by typing the hint `List‹[G; 8]›`,
+  -- so the limbs cannot reach a `u8` consumer without that conversion.
+  -- `u64_mul` was rewritten to raw field products plus `#split_carry`,
+  -- whose u8 checks constrain the split OUTPUTS, not the input digits —
+  -- and it re-canonicalizes while multiplying, so a digit-wrong `q`
+  -- still yields a canonical `q*b` and sails through the equality below.
+  -- That left the quotient's VALUE pinned but its representation free,
+  -- which is enough: `klimbs_eq` compares limbs rather than values, so a
+  -- digit-wrong quotient makes `Nat.beq (Nat.div 300 1) 300` answer
+  -- `false`. Trailing junk limbs are caught by the post-normalize
+  -- equality.
   fn klimbs_div_mod(a: KLimbs, b: KLimbs) -> (KLimbs, KLimbs) {
     let (q_hint, r_hint) = unconstrained_big_uint_div_mod(a, b);
-    -- Normalize the hint before anything reads it. The op is unconstrained,
-    -- so nothing stops the prover returning limb lists with trailing zeros,
-    -- and these values are returned to callers: `klimbs_gcd` feeds the
-    -- remainder straight back as the next DIVISOR, where a trailing zero
-    -- limb made the `r < b` test pass vacuously.
-    let q = klimbs_normalize(q_hint);
-    let r = klimbs_normalize(r_hint);
-    klimbs_range_check(q);
-    klimbs_range_check(r);
+    -- Convert (range-checking every byte), then normalize. The op is
+    -- unconstrained, so nothing stops the prover returning limb lists
+    -- with trailing zeros, and these values are returned to callers:
+    -- `klimbs_gcd` feeds the remainder straight back as the next
+    -- DIVISOR, where a trailing zero limb made the `r < b` test pass
+    -- vacuously.
+    let q = klimbs_normalize(glimbs_to_klimbs(q_hint));
+    let r = klimbs_normalize(glimbs_to_klimbs(r_hint));
     let qb = klimbs_mul(q, b);
     let lhs = klimbs_normalize(klimbs_add(qb, r));
     let rhs = klimbs_normalize(a);
diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean
index 5967174cb..6022954f2 100644
--- a/Tests/Ix/IxVM.lean
+++ b/Tests/Ix/IxVM.lean
@@ -205,17 +205,17 @@ private def kernelCheckEntries : List (String × Nat) := [
   ("IxVMPrim.nat_sub_lit",                                                25_877_844),
   ("IxVMPrim.nat_mul_lit",                                                19_003_829),
   ("IxVMPrim.nat_mul_big",                                                18_520_173),
-  ("IxVMPrim.nat_div_lit",                                                284_318_816),
-  ("IxVMPrim.nat_mod_lit",                                                290_903_621),
+  ("IxVMPrim.nat_div_lit",                                                284_318_446),
+  ("IxVMPrim.nat_mod_lit",                                                290_903_252),
   ("IxVMPrim.nat_succ_lit",                                               4_811_530),
   ("IxVMPrim.nat_pred_lit",                                               10_858_515),
-  ("IxVMPrim.nat_gcd_lit",                                                471_798_984),
+  ("IxVMPrim.nat_gcd_lit",                                                471_798_408),
   ("IxVMPrim.nat_land_lit",                                               799_156_568),
   ("IxVMPrim.nat_lor_lit",                                                799_831_190),
   ("IxVMPrim.nat_xor_lit",                                                805_615_928),
-  ("IxVMPrim.nat_shl_lit",                                                26_840_070),
-  ("IxVMPrim.nat_shr_lit",                                                288_363_702),
-  ("IxVMPrim.nat_pow_big",                                                57_847_192),
+  ("IxVMPrim.nat_shl_lit",                                                26_839_257),
+  ("IxVMPrim.nat_shr_lit",                                                288_362_941),
+  ("IxVMPrim.nat_pow_big",                                                57_840_233),
   ("IxVMPrim.nat_beq_lit",                                                18_232_986),
   ("IxVMPrim.nat_ble_lit",                                                16_851_217),
   ("IxVMPrim.nat_cases_big",                                              10_575_443),
@@ -223,7 +223,7 @@ private def kernelCheckEntries : List (String × Nat) := [
   ("IxVMPrim.nat_dec_lt",                                                 155_516_288),
   ("IxVMPrim.nat_dec_eq",                                                 63_259_938),
   ("IxVMPrim.str_size_lit",                                               555_223_250),
-  ("IxVMPrim.bv_to_nat_lit",                                              448_081_688),
+  ("IxVMPrim.bv_to_nat_lit",                                              448_080_398),
   ("IxVMInd.Even",                                                        19_814_542),
   ("IxVMInd.Odd",                                                         19_814_843),
   ("IxVMInd.Even.rec",                                                    24_361_340),
@@ -252,8 +252,8 @@ private def kernelCheckEntries : List (String × Nat) := [
   ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 4_188_001),
   ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 4_187_901),
   ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 1_706_482),
-  ("strOfListFoldSize",                                                   630_070_386),
-  ("strOfListFoldSizeAscii",                                              630_358_743),
+  ("strOfListFoldSize",                                                   630_069_070),
+  ("strOfListFoldSizeAscii",                                              630_357_426),
 ]
 
 /-- Variant of `kernelChecks`, pinned to the baseline
diff --git a/Tests/Main.lean b/Tests/Main.lean
index e41da7a7f..f96e9153a 100644
--- a/Tests/Main.lean
+++ b/Tests/Main.lean
@@ -201,8 +201,9 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
             -- explicit, reviewed bump.
             let actual :=
               (Aiur.computeStats v2Env.compiled qc).totalFftCost.round.toUInt64.toNat
-            pure (LSpec.test "Shard pipeline FFT matches"
-              (actual = 1_929_261_345))
+            pure (LSpec.test
+              s!"Shard pipeline FFT matches: expected 1929255084, got {actual}"
+              (actual = 1_929_255_084))
       LSpec.lspecIO
         (.ofList [("ixvm",
           [fullSeq, aiurSeq, arenaSeq, exploitSeq, paritySeq, shardSeq])]) []),
diff --git a/crates/ixvm-codegen/src/aiur_ixvm.rs b/crates/ixvm-codegen/src/aiur_ixvm.rs
index 7c431102a..d85cc23a4 100644
--- a/crates/ixvm-codegen/src/aiur_ixvm.rs
+++ b/crates/ixvm-codegen/src/aiur_ixvm.rs
@@ -13518,7 +13518,7 @@ fn aiur_fn_112(
 
 const INPUT_SIZE_113: usize = 1;
 const IN_113: usize = 1;
-const OUT_113: usize = 0;
+const OUT_113: usize = 1;
 fn aiur_fn_113(
   inp: [G; IN_113],
   record: &mut QueryRecord,
@@ -13540,7 +13540,10 @@ fn aiur_fn_113(
     let __v_10: G = __loaded[9];
     match __v_1.as_canonical_u64() {
       1u64 => {
-        let __ret: [G; OUT_113] = [];
+        let __v_11: G = G::from_u64(1);
+        let __v_12: G = G::from_u64(1);
+        let __v_13: G = { let __values: [G; 10] = [__v_11, __v_12, __v_12, __v_12, __v_12, __v_12, __v_12, __v_12, __v_12, __v_12]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } };
+        let __ret: [G; OUT_113] = [__v_13];
         record.function_queries[113].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained));
         return Ok(__ret);
       },
@@ -13549,8 +13552,11 @@ fn aiur_fn_113(
         if !unconstrained { let __vi = __v_4; let __vj = __v_5; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); };
         if !unconstrained { let __vi = __v_6; let __vj = __v_7; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); };
         if !unconstrained { let __vi = __v_8; let __vj = __v_9; let __bi = __vi.as_canonical_u64(); let __bj = __vj.as_canonical_u64(); if __bi >= 256 { return Err(ExecError::U8RangeCheckFailed(__bi)); } if __bj >= 256 { return Err(ExecError::U8RangeCheckFailed(__bj)); } record.bytes2_queries.bump_range_check(&__vi, &__vj); };
+        let __v_11: G = G::from_u64(0);
         let __r_arr: [G; OUT_113] = { let __args: [G; IN_113] = [__v_10]; let __cu = unconstrained; if let Some(result) = record.function_queries[113].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_113] = unsafe { *(result.output.as_ptr() as *const [G; OUT_113]) }; __ret } else { aiur_fn_113(__args, record, io_buffer, __cu)? } };
-        let __ret: [G; OUT_113] = [];
+        let __v_12: G = __r_arr[0];
+        let __v_13: G = { let __values: [G; 10] = [__v_11, __v_2, __v_3, __v_4, __v_5, __v_6, __v_7, __v_8, __v_9, __v_12]; let __mq = record.memory_queries.get_mut(&10).ok_or(ExecError::InvalidMemorySize(10))?; if let Some(result) = __mq.get_mut(&__values[..]) { if !unconstrained { *result.multiplicity += G::ONE; } result.output[0] } else { let __ptr = G::from_usize(__mq.len()); __mq.insert(&__values[..], &[__ptr], G::from_bool(!unconstrained)); __ptr } };
+        let __ret: [G; OUT_113] = [__v_13];
         record.function_queries[113].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained));
         return Ok(__ret);
       },
@@ -14622,52 +14628,54 @@ fn aiur_fn_126(
     let __bu_qr: (G, G) = unconstrained_big_uint_div_mod_helper(__v_0, __v_1, record)?;
     let __v_2: G = __bu_qr.0;
     let __v_3: G = __bu_qr.1;
-    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_2]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
+    let __r_arr: [G; OUT_113] = { let __args: [G; IN_113] = [__v_2]; let __cu = unconstrained; if let Some(result) = record.function_queries[113].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_113] = unsafe { *(result.output.as_ptr() as *const [G; OUT_113]) }; __ret } else { aiur_fn_113(__args, record, io_buffer, __cu)? } };
     let __v_4: G = __r_arr[0];
-    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_3]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
+    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_4]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
     let __v_5: G = __r_arr[0];
-    let __r_arr: [G; OUT_113] = { let __args: [G; IN_113] = [__v_4]; let __cu = unconstrained; if let Some(result) = record.function_queries[113].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_113] = unsafe { *(result.output.as_ptr() as *const [G; OUT_113]) }; __ret } else { aiur_fn_113(__args, record, io_buffer, __cu)? } };
-    let __r_arr: [G; OUT_113] = { let __args: [G; IN_113] = [__v_5]; let __cu = unconstrained; if let Some(result) = record.function_queries[113].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_113] = unsafe { *(result.output.as_ptr() as *const [G; OUT_113]) }; __ret } else { aiur_fn_113(__args, record, io_buffer, __cu)? } };
-    let __r_arr: [G; OUT_121] = { let __args: [G; IN_121] = [__v_4, __v_1]; let __cu = unconstrained; if let Some(result) = record.function_queries[121].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_121] = unsafe { *(result.output.as_ptr() as *const [G; OUT_121]) }; __ret } else { aiur_fn_121(__args, record, io_buffer, __cu)? } };
+    let __r_arr: [G; OUT_113] = { let __args: [G; IN_113] = [__v_3]; let __cu = unconstrained; if let Some(result) = record.function_queries[113].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_113] = unsafe { *(result.output.as_ptr() as *const [G; OUT_113]) }; __ret } else { aiur_fn_113(__args, record, io_buffer, __cu)? } };
     let __v_6: G = __r_arr[0];
-    let __r_arr: [G; OUT_110] = { let __args: [G; IN_110] = [__v_6, __v_5]; let __cu = unconstrained; if let Some(result) = record.function_queries[110].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_110] = unsafe { *(result.output.as_ptr() as *const [G; OUT_110]) }; __ret } else { aiur_fn_110(__args, record, io_buffer, __cu)? } };
+    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_6]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
     let __v_7: G = __r_arr[0];
-    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_7]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
+    let __r_arr: [G; OUT_121] = { let __args: [G; IN_121] = [__v_5, __v_1]; let __cu = unconstrained; if let Some(result) = record.function_queries[121].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_121] = unsafe { *(result.output.as_ptr() as *const [G; OUT_121]) }; __ret } else { aiur_fn_121(__args, record, io_buffer, __cu)? } };
     let __v_8: G = __r_arr[0];
-    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_0]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
+    let __r_arr: [G; OUT_110] = { let __args: [G; IN_110] = [__v_8, __v_7]; let __cu = unconstrained; if let Some(result) = record.function_queries[110].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_110] = unsafe { *(result.output.as_ptr() as *const [G; OUT_110]) }; __ret } else { aiur_fn_110(__args, record, io_buffer, __cu)? } };
     let __v_9: G = __r_arr[0];
-    if (__v_8 != __v_9) {
-      return Err(ExecError::AssertEqMismatch { lhs: __v_8.as_canonical_u64(), rhs: __v_9.as_canonical_u64(), msg: Some("div/mod hint: q*b + r != a".to_string()) });
+    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_9]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
+    let __v_10: G = __r_arr[0];
+    let __r_arr: [G; OUT_114] = { let __args: [G; IN_114] = [__v_0]; let __cu = unconstrained; if let Some(result) = record.function_queries[114].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_114] = unsafe { *(result.output.as_ptr() as *const [G; OUT_114]) }; __ret } else { aiur_fn_114(__args, record, io_buffer, __cu)? } };
+    let __v_11: G = __r_arr[0];
+    if (__v_10 != __v_11) {
+      return Err(ExecError::AssertEqMismatch { lhs: __v_10.as_canonical_u64(), rhs: __v_11.as_canonical_u64(), msg: Some("div/mod hint: q*b + r != a".to_string()) });
     }
     let __r_arr: [G; OUT_125] = { let __args: [G; IN_125] = [__v_1]; let __cu = unconstrained; if let Some(result) = record.function_queries[125].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_125] = unsafe { *(result.output.as_ptr() as *const [G; OUT_125]) }; __ret } else { aiur_fn_125(__args, record, io_buffer, __cu)? } };
-    let __v_10: G = __r_arr[0];
-    match __v_10.as_canonical_u64() {
+    let __v_12: G = __r_arr[0];
+    match __v_12.as_canonical_u64() {
       1u64 => {
-        let __r_arr: [G; OUT_125] = { let __args: [G; IN_125] = [__v_4]; let __cu = unconstrained; if let Some(result) = record.function_queries[125].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_125] = unsafe { *(result.output.as_ptr() as *const [G; OUT_125]) }; __ret } else { aiur_fn_125(__args, record, io_buffer, __cu)? } };
-        let __v_11: G = __r_arr[0];
-        let __v_12: G = G::from_u64(1);
-        if (__v_11 != __v_12) {
-          return Err(ExecError::AssertEqMismatch { lhs: __v_11.as_canonical_u64(), rhs: __v_12.as_canonical_u64(), msg: Some("div/mod hint: division by zero must yield a zero quotient".to_string()) });
+        let __r_arr: [G; OUT_125] = { let __args: [G; IN_125] = [__v_5]; let __cu = unconstrained; if let Some(result) = record.function_queries[125].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_125] = unsafe { *(result.output.as_ptr() as *const [G; OUT_125]) }; __ret } else { aiur_fn_125(__args, record, io_buffer, __cu)? } };
+        let __v_13: G = __r_arr[0];
+        let __v_14: G = G::from_u64(1);
+        if (__v_13 != __v_14) {
+          return Err(ExecError::AssertEqMismatch { lhs: __v_13.as_canonical_u64(), rhs: __v_14.as_canonical_u64(), msg: Some("div/mod hint: division by zero must yield a zero quotient".to_string()) });
         }
-        let __ret: [G; OUT_126] = [__v_4, __v_5];
+        let __ret: [G; OUT_126] = [__v_5, __v_7];
         record.function_queries[126].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained));
         return Ok(__ret);
       },
       0u64 => {
-        let __r_arr: [G; OUT_108] = { let __args: [G; IN_108] = [__v_5]; let __cu = unconstrained; if let Some(result) = record.function_queries[108].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_108] = unsafe { *(result.output.as_ptr() as *const [G; OUT_108]) }; __ret } else { aiur_fn_108(__args, record, io_buffer, __cu)? } };
-        let __v_11: G = __r_arr[0];
-        let __r_arr: [G; OUT_116] = { let __args: [G; IN_116] = [__v_11, __v_1]; let __cu = unconstrained; if let Some(result) = record.function_queries[116].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_116] = unsafe { *(result.output.as_ptr() as *const [G; OUT_116]) }; __ret } else { aiur_fn_116(__args, record, io_buffer, __cu)? } };
-        let __v_12: G = __r_arr[0];
-        let __v_13: G = G::from_u64(1);
-        if (__v_12 != __v_13) {
-          return Err(ExecError::AssertEqMismatch { lhs: __v_12.as_canonical_u64(), rhs: __v_13.as_canonical_u64(), msg: Some("div/mod hint: remainder is not less than the divisor".to_string()) });
+        let __r_arr: [G; OUT_108] = { let __args: [G; IN_108] = [__v_7]; let __cu = unconstrained; if let Some(result) = record.function_queries[108].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_108] = unsafe { *(result.output.as_ptr() as *const [G; OUT_108]) }; __ret } else { aiur_fn_108(__args, record, io_buffer, __cu)? } };
+        let __v_13: G = __r_arr[0];
+        let __r_arr: [G; OUT_116] = { let __args: [G; IN_116] = [__v_13, __v_1]; let __cu = unconstrained; if let Some(result) = record.function_queries[116].get_mut(&__args[..]) { if !unconstrained { *result.multiplicity += G::ONE; } let __ret: [G; OUT_116] = unsafe { *(result.output.as_ptr() as *const [G; OUT_116]) }; __ret } else { aiur_fn_116(__args, record, io_buffer, __cu)? } };
+        let __v_14: G = __r_arr[0];
+        let __v_15: G = G::from_u64(1);
+        if (__v_14 != __v_15) {
+          return Err(ExecError::AssertEqMismatch { lhs: __v_14.as_canonical_u64(), rhs: __v_15.as_canonical_u64(), msg: Some("div/mod hint: remainder is not less than the divisor".to_string()) });
         }
-        let __ret: [G; OUT_126] = [__v_4, __v_5];
+        let __ret: [G; OUT_126] = [__v_5, __v_7];
         record.function_queries[126].insert(&inp[..], &__ret[..], G::from_bool(!unconstrained));
         return Ok(__ret);
       },
       _ => {
-        return Err(ExecError::MatchNoCase(__v_10.as_canonical_u64()));
+        return Err(ExecError::MatchNoCase(__v_12.as_canonical_u64()));
       },
     }
   })

From 43e55e44e30d86f7ef060d0459659ca90db12f41 Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Wed, 5 Aug 2026 11:01:09 -0700
Subject: [PATCH 3/5] aiur: fix unconstrained_g_to_bytes to return [G; 8]

Same flaw and same fix as unconstrained_big_uint_div_mod (previous
commit): the op typed its advice `[U8; 8]`, granting u8's "known to
be range-checked" contract to unchecked prover bytes, upheld only by
caller discipline. The checker now types the result `[G; 8]`; the two
consumers (`idx_to_u64` in the IxVM ingress, `gl_to_bytes` in the
MultiStark verifier) mint their bytes from the u8_range_check outputs,
dropping the now-unnecessary to_field wrappers.

to_field is an erased coercion, so the compiled bytecode is unchanged:
`ix codegen` regenerates byte-identical kernels and every FFT pin
holds (verified via `lake test -- --ignored ixvm multi-stark`).
---
 Ix/Aiur/Compiler/Check.lean   |  8 +++++---
 Ix/Aiur/Stages/Source.lean    | 11 ++++++-----
 Ix/IxVM/Ingress.lean          |  8 ++++----
 Ix/MultiStark/Goldilocks.lean |  8 ++++----
 4 files changed, 19 insertions(+), 16 deletions(-)

diff --git a/Ix/Aiur/Compiler/Check.lean b/Ix/Aiur/Compiler/Check.lean
index 6c365cf64..fc2dc62ba 100644
--- a/Ix/Aiur/Compiler/Check.lean
+++ b/Ix/Aiur/Compiler/Check.lean
@@ -816,10 +816,12 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
     let τ ← bigUintDivModResultTyp (← zonkTyp a'.typ)
     pure (Typed.Term.unconstrainedBigUintDivMod (.tuple #[τ, τ]) false a' b')
   | .unconstrainedGToBytes a => do
-    -- The bytes are UNCONSTRAINED advice typed `u8`; the caller must
-    -- range-check them (see `Source.Term.unconstrainedGToBytes`).
+    -- The bytes are UNCONSTRAINED advice, so they come back as raw
+    -- `field`s — they must not type as range-checked bytes. Consumers
+    -- mint `u8`s from the `u8_range_check` outputs (see `gl_to_bytes`
+    -- and `idx_to_u64`).
     let a' ← checkNoEscape a .field
-    pure (Typed.Term.unconstrainedGToBytes (.array .u8 8) false a')
+    pure (Typed.Term.unconstrainedGToBytes (.array .field 8) false a')
   | .unconstrainedGInverse a => do
     let a' ← checkNoEscape a .field
     pure (Typed.Term.unconstrainedGInverse .field false a')
diff --git a/Ix/Aiur/Stages/Source.lean b/Ix/Aiur/Stages/Source.lean
index 7fcea876b..369636c1b 100644
--- a/Ix/Aiur/Stages/Source.lean
+++ b/Ix/Aiur/Stages/Source.lean
@@ -440,11 +440,12 @@ inductive Term
   caller must verify `q*b + r == a` and `r < b` in constrained code. -/
   | unconstrainedBigUintDivMod : (a : Term) → (b : Term) → Term
   /-- Unconstrained hint: the 8 little-endian bytes of a field element's
-  canonical `u64` value, as a `[U8; 8]`. Computed natively by the Aiur
-  runtime; no constraints generated — the bytes are advice. The caller must
-  range-check each byte, assert they recompose to the input
-  (`Σ bᵢ·256ⁱ == x`), and assert canonicality (`< p`) in constrained code;
-  together these pin the unique canonical decomposition. -/
+  canonical `u64` value, as a `[G; 8]` — advice must not type as
+  range-checked bytes. Computed natively by the Aiur runtime; no
+  constraints generated. The caller must range-check each byte (minting
+  the `u8`s from the check outputs), assert they recompose to the input
+  (`Σ bᵢ·256ⁱ == x`), and assert canonicality (`< p`) in constrained
+  code; together these pin the unique canonical decomposition. -/
   | unconstrainedGToBytes : Term → Term
   /-- Unconstrained hint: the field inverse of a field element (`0 ↦ 0`).
   Computed natively by the Aiur runtime; no constraints generated — the
diff --git a/Ix/IxVM/Ingress.lean b/Ix/IxVM/Ingress.lean
index c05f08c44..42e7984fc 100644
--- a/Ix/IxVM/Ingress.lean
+++ b/Ix/IxVM/Ingress.lean
@@ -348,10 +348,10 @@ let block_c = load_verified_constant(block_addr);
   -- constructor count.
   fn idx_to_u64(idx: G) -> U64 {
     let [h0, h1, h2, h3, h4, h5, h6, h7] = unconstrained_g_to_bytes(idx);
-    let (b0, b1) = u8_range_check(to_field(h0), to_field(h1));
-    let (b2, b3) = u8_range_check(to_field(h2), to_field(h3));
-    let (b4, b5) = u8_range_check(to_field(h4), to_field(h5));
-    let (b6, b7) = u8_range_check(to_field(h6), to_field(h7));
+    let (b0, b1) = u8_range_check(h0, h1);
+    let (b2, b3) = u8_range_check(h2, h3);
+    let (b4, b5) = u8_range_check(h4, h5);
+    let (b6, b7) = u8_range_check(h6, h7);
     let bytes = [b0, b1, b2, b3, b4, b5, b6, b7];
     -- `flatten_u64` contributes the top-byte-is-zero assert and the sum.
     -- It does NOT range-check its input and so is not injective on its
diff --git a/Ix/MultiStark/Goldilocks.lean b/Ix/MultiStark/Goldilocks.lean
index 2453d39c6..cd84c4386 100644
--- a/Ix/MultiStark/Goldilocks.lean
+++ b/Ix/MultiStark/Goldilocks.lean
@@ -76,10 +76,10 @@ def goldilocks := ⟦
   -- decomposition (two distinct byte strings < p have distinct field values).
   fn gl_to_bytes(v: G) -> [U8; 8] {
     let b = unconstrained_g_to_bytes(v);
-    let (c0, c1) = u8_range_check(to_field(b[0]), to_field(b[1]));
-    let (c2, c3) = u8_range_check(to_field(b[2]), to_field(b[3]));
-    let (c4, c5) = u8_range_check(to_field(b[4]), to_field(b[5]));
-    let (c6, c7) = u8_range_check(to_field(b[6]), to_field(b[7]));
+    let (c0, c1) = u8_range_check(b[0], b[1]);
+    let (c2, c3) = u8_range_check(b[2], b[3]);
+    let (c4, c5) = u8_range_check(b[4], b[5]);
+    let (c6, c7) = u8_range_check(b[6], b[7]);
     let r = [c0, c1, c2, c3, c4, c5, c6, c7];
     assert_eq!(gl_val(r), v);
     assert_eq!(gl_lt_p(r), 1);

From b3533c8c09b02d6b25866c87a5b3816423f2b18f Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Wed, 5 Aug 2026 11:24:08 -0700
Subject: [PATCH 4/5] aiur: implement unconstrained_big_uint_div_mod in the
 Lean evaluators
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The op was the last cross-engine blind spot: both Lean semantic
evaluators and the debug interpreter stubbed it with an error, so
nothing could cross-check the runtime's bignum hints. All three now
mirror crates/aiur/src/execute.rs exactly: walk the width-10 limb
chains (tag 0 = Cons, 1 = Nil, LE bytes, per-byte range check,
cycle-bounded), divide as Nat (which matches the runtime's
b = 0 -> (0, a) convention), and rebuild canonical chains in the Rust
builder's allocation order (Nil first, limbs reversed, content-deduped).
Shared limb codecs live in Goldilocks.lean with proven termination.
SourceEval's store/load arms are refactored onto shared
storeValue/loadValue so hint chains allocate identically to program
stores, and the Semantics files no longer use panicking accessors
(vs[0]!, set!) — this code is slated for formal verification.

Coverage: divmod_test (plain / unit divisor / zero divisor / two-limb
dividend) and hint_test (g_to_bytes recomposition + canonicality on
p - 1, g_inverse on 7 and 0) run 4-way agreement in aiur-cross and one
proof each in aiur-prove.

hint_test immediately exposed a long-standing bug in the Lean field
model: G.ofNat narrowed through toUInt64 BEFORE reducing mod p, so any
op whose intermediate exceeds 2^64 (Mul products, Add/Sub carries, the
pow chain behind G.inverse) wrapped mod 2^64 instead of mod p — all
three Lean evaluators agreed with each other and diverged only from the
native executor. Fixed by reducing in Nat before narrowing; probed
inv(7) * 7 = 1 directly.

Validated: aiur-cross and aiur-prove (29 proofs) fully green, plus
aiur-hashes and rbtree-map.
---
 Ix/Aiur/Goldilocks.lean             |  32 ++++++-
 Ix/Aiur/Interpret.lean              |  93 ++++++++++++++++--
 Ix/Aiur/Semantics/BytecodeEval.lean |  59 ++++++++++--
 Ix/Aiur/Semantics/SourceEval.lean   | 142 +++++++++++++++++++++++-----
 Tests/Aiur/Aiur.lean                |  81 ++++++++++++++++
 Tests/Aiur/Cross.lean               |  74 +++++++++++++++
 6 files changed, 437 insertions(+), 44 deletions(-)

diff --git a/Ix/Aiur/Goldilocks.lean b/Ix/Aiur/Goldilocks.lean
index 7960f9b38..dc6c485c8 100644
--- a/Ix/Aiur/Goldilocks.lean
+++ b/Ix/Aiur/Goldilocks.lean
@@ -10,7 +10,13 @@ abbrev G := { u : UInt64 // u < gSize }
 abbrev G.extensionDegree : Nat := 2
 
 def G.ofNat (n : Nat) : G :=
-  let n := n.toUInt64
+  -- Reduce in `Nat` BEFORE narrowing: `toUInt64` wraps mod 2^64, which is
+  -- NOT reduction mod p — narrowing first silently corrupts any value
+  -- ≥ 2^64 (e.g. products in `Mul`, sums in `Add`/`Sub`, the `pow` chain
+  -- behind `G.inverse`). After `% gSize.toNat` the value fits `UInt64`
+  -- exactly, so the branch below is always true; it is kept (rather than
+  -- proved) to avoid a proof obligation on the numeral.
+  let n := (n % gSize.toNat).toUInt64
   if h : n < gSize then ⟨n, h⟩
   else ⟨n % gSize, UInt64.mod_lt n (by decide)⟩
 
@@ -90,6 +96,30 @@ 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
 
+/-- Canonical little-endian u64 limbs of a natural number, each limb as its
+8 LE bytes (as field elements). Semantic model of the limb lists the
+`unconstrained_big_uint_div_mod` runtime builds (`biguint_to_klimbs_u64` in
+`crates/aiur/src/execute.rs`): zero is the empty list, no trailing zero
+limbs. -/
+def natToLimbsLE (n : Nat) : List (Array G) :=
+  if h : n = 0 then []
+  else
+    let limb := n % 2^64
+    let bytes := Array.ofFn fun (i : Fin 8) => G.ofNat ((limb >>> (8 * i.val)) % 256)
+    bytes :: natToLimbsLE (n / 2^64)
+termination_by n
+decreasing_by
+  exact Nat.div_lt_self (Nat.pos_of_ne_zero h) (by decide : (1 : Nat) < 2^64)
+
+/-- Value of one 8-LE-byte limb. Inverse direction of `natToLimbsLE`'s
+per-limb encoding; bytes are assumed already validated `< 256`. -/
+def limbBytesVal (bytes : Array G) : Nat :=
+  (bytes.toList.zipIdx.map fun (b, i) => b.val.toNat <<< (8 * i)).foldl (· + ·) 0
+
+/-- Value of a head-first (little-endian) u64 limb list. -/
+def limbsVal (limbs : List (Array G)) : Nat :=
+  limbs.foldr (fun limb acc => limbBytesVal limb + acc <<< 64) 0
+
 /-- 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
diff --git a/Ix/Aiur/Interpret.lean b/Ix/Aiur/Interpret.lean
index 975d812af..ff5625ac9 100644
--- a/Ix/Aiur/Interpret.lean
+++ b/Ix/Aiur/Interpret.lean
@@ -200,6 +200,72 @@ private def callSite (g : Global) (args : List Value) (m : InterpM Value) : Inte
     | .ret v           => pure v
     | .error msg stack => throw (.error msg ((g, args) :: stack))
 
+/-! ### `List<U64>` limb chains (`unconstrainedBigUintDivMod`)
+
+Value-level mirror of `read_klimbs_u64` / `build_klimbs_u64` in
+`crates/aiur/src/execute.rs`; see `Ix/Aiur/Semantics/SourceEval.lean` for
+the reference-evaluator twin. Constructor 0 = Cons(limb, rest),
+constructor 1 = Nil; limb bytes little-endian, limbs head-first. -/
+
+/-- Store a value content-deduped, returning its pointer (the `.store`
+semantics, callable from the divmod chain builder). -/
+private def storeValueI (v : Value) : InterpM Value := do
+  let store ← getStore
+  if let some idx := store.getIdxOf #[v] then
+    return .pointer 0 idx
+  let idx := store.size
+  modify fun s => { s with store := s.store.insert #[v] () }
+  return .pointer 0 idx
+
+/-- Walk a limb-chain pointer, returning the node datatype and the limbs
+head-first. `steps` bounds the walk so a malformed cycle terminates. -/
+private def readLimbChainI (decls : Decls) :
+    Nat → Value → InterpM (DataType × List (Array G))
+  | 0, _ => throwErr "unconstrainedBigUintDivMod: cyclic limb list"
+  | steps+1, ptrVal => do
+    match ptrVal with
+    | .pointer _ n =>
+      let store ← getStore
+      match store.getByIdx n with
+      | none => throwErr s!"unconstrainedBigUintDivMod: invalid pointer {n}"
+      | some (vs, _) =>
+        match (vs[0]? : Option Value) with
+        | some (.ctor g args) =>
+          match decls.getByKey g with
+          | some (.constructor dt ctor) =>
+            let tag := dt.constructors.findIdx? (· == ctor) |>.getD 0
+            if tag == 1 then pure (dt, [])
+            else if tag == 0 then
+              match args with
+              | #[.array byteVals, rest] =>
+                let bytes ← byteVals.mapM fun bv =>
+                  match bv with
+                  | .field b =>
+                    if b.val < 256 then pure b
+                    else throwErr
+                      "unconstrainedBigUintDivMod: limb byte out of range"
+                  | _ => throwErr
+                      "unconstrainedBigUintDivMod: limb byte not a field"
+                if bytes.size == 8 then do
+                  let (_, restLimbs) ← readLimbChainI decls steps rest
+                  pure (dt, bytes :: restLimbs)
+                else throwErr "unconstrainedBigUintDivMod: limb is not [U8; 8]"
+              | _ => throwErr "unconstrainedBigUintDivMod: malformed Cons node"
+            else
+              throwErr "unconstrainedBigUintDivMod: unexpected constructor tag"
+          | _ => throwErr s!"unconstrainedBigUintDivMod: unbound ctor {g}"
+        | _ => throwErr "unconstrainedBigUintDivMod: node is not a constructor"
+    | _ => throwErr "unconstrainedBigUintDivMod: input is not a pointer"
+
+/-- Build a limb chain from head-first `limbs` (Nil first, limbs in
+reverse — same allocation order as the Rust builder). -/
+private def buildLimbChainI (consG nilG : Global) :
+    List (Array G) → InterpM Value
+  | [] => storeValueI (.ctor nilG #[])
+  | limb :: rest => do
+    let restPtr ← buildLimbChainI consG nilG rest
+    storeValueI (.ctor consG #[.array (limb.map .field), restPtr])
+
 mutual
 
 private partial def applyGlobal (decls : Decls) (g : Global) (args : List Value) :
@@ -410,16 +476,23 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
           else throwErr "u8RangeCheck: value out of range [0, 256)"
       | _, _ => throwErr "u8RangeCheck: expected field values"
   | .unconstrainedBigUintDivMod t1 t2 => do
-      -- TODO(unconstrainedBigUintDivMod): walk both List<U64> pointer chains via the
-      -- store to extract Vec<u8> bytes (LE), interpret as BigUints, compute
-      -- div_rem natively, build two fresh ListNode chains for q and r, and
-      -- return `.tuple #[.pointer w q_ptr, .pointer w r_ptr]`. The Rust
-      -- runtime (execute.rs) already does this; the Lean debug interpreter
-      -- doesn't yet have BigUint or klimbs helpers, so we surface an explicit
-      -- error rather than silently returning a wrong value.
-      let _ ← interp decls bindings t1
-      let _ ← interp decls bindings t2
-      throwErr "unconstrainedBigUintDivMod: not implemented in debug interpreter"
+      let aPtr ← interp decls bindings t1
+      let bPtr ← interp decls bindings t2
+      let bound := (← getStore).size + 1
+      let (dt, aLimbs) ← readLimbChainI decls bound aPtr
+      let (_, bLimbs) ← readLimbChainI decls bound bPtr
+      match dt.constructors[0]?, dt.constructors[1]? with
+      | some cons, some nil =>
+        let consG := dt.name.pushNamespace cons.nameHead
+        let nilG := dt.name.pushNamespace nil.nameHead
+        let aVal := limbsVal aLimbs
+        let bVal := limbsVal bLimbs
+        -- `Nat` division matches the runtime's `b = 0 → (0, a)` convention.
+        let qPtr ← buildLimbChainI consG nilG (natToLimbsLE (aVal / bVal))
+        let rPtr ← buildLimbChainI consG nilG (natToLimbsLE (aVal % bVal))
+        return .tuple #[qPtr, rPtr]
+      | _, _ =>
+        throwErr "unconstrainedBigUintDivMod: datatype has fewer than two constructors"
   | .unconstrainedGToBytes t => do
       match ← interp decls bindings t with
       | .field g => return .array (Array.ofFn fun i => .field (g.toLeBytes i))
diff --git a/Ix/Aiur/Semantics/BytecodeEval.lean b/Ix/Aiur/Semantics/BytecodeEval.lean
index 1c6a83aa1..72e11a038 100644
--- a/Ix/Aiur/Semantics/BytecodeEval.lean
+++ b/Ix/Aiur/Semantics/BytecodeEval.lean
@@ -64,7 +64,7 @@ inductive BytecodeError
   | callOutputSizeMismatch
   | unreachableAfterLayout
   | u8RangeCheckFailed
-  | unconstrainedBigUintDivModUnsupported
+  | unconstrainedBigUintDivModFailed
   | earlyReturn (outs : Array G) (st : EvalState)
   deriving Repr, Inhabited
 
@@ -104,6 +104,43 @@ def memLoad (st : EvalState) (size : Nat) (ptr : Nat) :
     | some (vs, _) => .ok vs
     | none         => .error (.invalidPointer size ptr)
 
+/-! ## `List<U64>` limb chains (`unconstrainedBigUintDivMod`)
+
+Mirrors `read_klimbs_u64` / `build_klimbs_u64` in `crates/aiur/src/execute.rs`:
+nodes live in the width-10 memory bucket with the standard tagged-enum
+layout `[tag, byte0..byte7, next_ptr]` — tag 0 = Cons, tag 1 = Nil, bytes
+little-endian within the u64 limb. -/
+
+/-- Walk a limb chain from `ptr`, returning the limbs head-first. `steps`
+bounds the walk: a chain longer than the width-10 bucket must revisit a
+pointer, i.e. a malformed cycle. -/
+def readLimbChain (st : EvalState) : Nat → Nat →
+    Except BytecodeError (List (Array G))
+  | 0, _ => .error .unconstrainedBigUintDivModFailed
+  | steps+1, ptr => do
+    let vs ← memLoad st 10 ptr
+    match vs[0]?, vs[9]? with
+    | some tag, some next =>
+      if tag == 1 then pure []
+      else if tag == 0 then
+        let bytes := vs.extract 1 9
+        if bytes.size == 8 && bytes.all (·.val < 256) then do
+          let rest ← readLimbChain st steps next.val.toNat
+          pure (bytes :: rest)
+        else .error .unconstrainedBigUintDivModFailed
+      else .error .unconstrainedBigUintDivModFailed
+    | _, _ => .error .unconstrainedBigUintDivModFailed
+
+/-- Build a limb chain from head-first `limbs`, returning the head pointer.
+Same insertion order as the Rust builder (Nil first, then limbs in reverse),
+so freshly-created pointer indices agree; `memStore` content-dedups like
+`QueryMap` does. -/
+def buildLimbChain (st : EvalState) : List (Array G) → EvalState × Nat
+  | [] => memStore st (#[1] ++ Array.replicate 9 0)
+  | limb :: rest =>
+    let (st', restPtr) := buildLimbChain st rest
+    memStore st' (#[0] ++ limb ++ #[.ofNat restPtr])
+
 def pushMap (st : EvalState) (g : G) : EvalState :=
   { st with map := st.map.push g }
 
@@ -311,14 +348,18 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
     let x ← readIdx st a; let y ← readIdx st b
     if x.val < 256 && y.val < 256 then .ok st else .error .u8RangeCheckFailed
   | .unconstrainedBigUintDivMod a b => do
-    -- TODO(unconstrainedBigUintDivMod): walk the two pointer chains in `st.memory`
-    -- (List<U64> = ListNode of [U8;8]), extract LE bytes, compute BigUint
-    -- div_rem, build two fresh ListNode chains in `st.memory`, push their
-    -- pointer ValIdxs. The Rust runtime already does this end-to-end; the
-    -- reference evaluator doesn't yet have BigUint helpers, so we surface
-    -- an explicit error rather than silently producing wrong values.
-    let _ ← readIdx st a; let _ ← readIdx st b
-    .error .unconstrainedBigUintDivModUnsupported
+    let aPtr ← readIdx st a
+    let bPtr ← readIdx st b
+    -- Walk bound: the width-10 bucket size plus one (see `readLimbChain`).
+    let bound := (st.memory.getByKey 10 |>.map (·.size) |>.getD 0) + 1
+    let aLimbs ← readLimbChain st bound aPtr.val.toNat
+    let bLimbs ← readLimbChain st bound bPtr.val.toNat
+    let aVal := limbsVal aLimbs
+    let bVal := limbsVal bLimbs
+    -- `Nat` division matches the runtime's `b = 0 → (0, a)` convention.
+    let (st1, qPtr) := buildLimbChain st (natToLimbsLE (aVal / bVal))
+    let (st2, rPtr) := buildLimbChain st1 (natToLimbsLE (aVal % bVal))
+    pure (pushMap (pushMap st2 (.ofNat qPtr)) (.ofNat rPtr))
   | .unconstrainedGToBytes idx => do
     let g ← readIdx st idx
     pure (appendMap st (Array.ofFn g.toLeBytes))
diff --git a/Ix/Aiur/Semantics/SourceEval.lean b/Ix/Aiur/Semantics/SourceEval.lean
index 57ab000ac..7a60b6ef1 100644
--- a/Ix/Aiur/Semantics/SourceEval.lean
+++ b/Ix/Aiur/Semantics/SourceEval.lean
@@ -131,6 +131,116 @@ def tryLocalLookup (g : Global) (bindings : Bindings) : Option Value :=
   | .str .anonymous name => bindings.find? (·.1 == Local.str name) |>.map (·.2)
   | _                    => none
 
+/-- Store `v` in its width bucket (width = flat size), content-deduped;
+returns the pointer value. Shared by the `.store` arm and the
+`unconstrainedBigUintDivMod` chain builder, so hint chains allocate
+identically to program stores. -/
+def storeValue (decls : Decls) (st : EvalState) (v : Value) : Value × EvalState :=
+  let w := (flattenValue decls (fun _ => none) v).size
+  let inner := st.store[w]?.getD (default : IndexMap (Array Value) Unit)
+  if let some idx := inner.getIdxOf #[v] then
+    (.pointer w idx, st)
+  else
+    let idx := inner.size
+    let inner' := inner.insert #[v] ()
+    (.pointer w idx, { st with store := st.store.insert w inner' })
+
+/-- Dereference a `(width, index)` pointer. -/
+def loadValue (st : EvalState) (w n : Nat) : Except SourceError Value :=
+  match st.store[w]? with
+  | some inner =>
+    match inner.getByIdx n with
+    | some (vs, _) =>
+      match vs[0]? with
+      | some v => .ok v
+      | none   => .error (.invalidPointer n)
+    | none => .error (.invalidPointer n)
+  | none => .error (.invalidPointer n)
+
+/-! ### `List<U64>` limb chains (`unconstrainedBigUintDivMod`)
+
+Value-level mirror of `read_klimbs_u64` / `build_klimbs_u64` in
+`crates/aiur/src/execute.rs`: nodes are two-constructor list values —
+constructor 0 = Cons(limb, rest), constructor 1 = Nil — with `[U8; 8]`
+limb bytes, little-endian within the u64 and head-first across limbs. -/
+
+/-- Datatype and declaration-index (= runtime tag) of a constructor. -/
+def ctorInfo (decls : Decls) (g : Global) :
+    Except SourceError (DataType × Nat) :=
+  match decls.getByKey g with
+  | some (.constructor dt ctor) =>
+    .ok (dt, dt.constructors.findIdx? (· == ctor) |>.getD 0)
+  | _ => .error (.unboundGlobal g)
+
+/-- Walk a limb-chain pointer value, returning the node datatype and the
+limbs head-first. `steps` bounds the walk (a chain longer than the store
+must revisit a pointer, i.e. a malformed cycle). -/
+def readLimbChain (decls : Decls) (st : EvalState) :
+    Nat → Value → Except SourceError (DataType × List (Array G))
+  | 0, _ => .error (.typeMismatch "unconstrainedBigUintDivMod: cyclic limb list")
+  | steps+1, ptrVal => do
+    match ptrVal with
+    | .pointer w n =>
+      match ← loadValue st w n with
+      | .ctor g args =>
+        let (dt, tag) ← ctorInfo decls g
+        if tag == 1 then pure (dt, [])
+        else if tag == 0 then
+          match args with
+          | #[.array byteVals, rest] =>
+            let bytes ← byteVals.mapM fun bv =>
+              match bv with
+              | .field b =>
+                if b.val < 256 then pure b
+                else throw (.typeMismatch
+                  "unconstrainedBigUintDivMod: limb byte out of range")
+              | _ => throw (.typeMismatch
+                  "unconstrainedBigUintDivMod: limb byte not a field")
+            if bytes.size == 8 then do
+              let (_, restLimbs) ← readLimbChain decls st steps rest
+              pure (dt, bytes :: restLimbs)
+            else throw (.typeMismatch
+              "unconstrainedBigUintDivMod: limb is not [U8; 8]")
+          | _ => throw (.typeMismatch
+              "unconstrainedBigUintDivMod: malformed Cons node")
+        else throw (.typeMismatch
+          "unconstrainedBigUintDivMod: unexpected constructor tag")
+      | _ => throw (.typeMismatch
+          "unconstrainedBigUintDivMod: node is not a constructor")
+    | _ => throw (.typeMismatch
+        "unconstrainedBigUintDivMod: input is not a pointer")
+
+/-- Build a limb chain from head-first `limbs` using the given Cons/Nil
+constructor names; returns the head pointer value. Same order as the Rust
+builder (Nil first, then limbs in reverse). -/
+def buildLimbChain (decls : Decls) (consG nilG : Global) (st : EvalState) :
+    List (Array G) → Value × EvalState
+  | [] => storeValue decls st (.ctor nilG #[])
+  | limb :: rest =>
+    let (restPtr, st') := buildLimbChain decls consG nilG st rest
+    storeValue decls st' (.ctor consG #[.array (limb.map .field), restPtr])
+
+/-- Semantic model of `unconstrainedBigUintDivMod` on already-evaluated
+pointer values: walk both chains, divide as `Nat` (which matches the
+runtime's `b = 0 → (0, a)` convention), and rebuild canonical result
+chains with the input's own constructors. -/
+def bigUintDivModValue (decls : Decls) (aPtr bPtr : Value)
+    (st : EvalState) : EvalResult := do
+  let bound := st.store.fold (init := 1) fun acc _ inner => acc + inner.size
+  let (dt, aLimbs) ← readLimbChain decls st bound aPtr
+  let (_, bLimbs) ← readLimbChain decls st bound bPtr
+  match dt.constructors[0]?, dt.constructors[1]? with
+  | some cons, some nil =>
+    let consG := dt.name.pushNamespace cons.nameHead
+    let nilG := dt.name.pushNamespace nil.nameHead
+    let aVal := limbsVal aLimbs
+    let bVal := limbsVal bLimbs
+    let (qPtr, st1) := buildLimbChain decls consG nilG st (natToLimbsLE (aVal / bVal))
+    let (rPtr, st2) := buildLimbChain decls consG nilG st1 (natToLimbsLE (aVal % bVal))
+    pure (.tuple #[qPtr, rPtr], st2)
+  | _, _ => throw (.typeMismatch
+      "unconstrainedBigUintDivMod: datatype has fewer than two constructors")
+
 /-- Array's `sizeOf` strictly exceeds its `toList`'s `sizeOf`. Used in
 termination proofs that go from `interp .tuple ts` to `evalList ts.toList`. -/
 private theorem sizeOf_toList_lt {α : Type} [SizeOf α] (a : Array α) :
@@ -316,7 +426,7 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
         | .ok (arr, st2) =>
           match arr with
           | .array vs =>
-            if n < vs.size then .ok (.array (vs.set! n val), st2)
+            if h : n < vs.size then .ok (.array (vs.set n val), st2)
             else .error (.indexOoB n)
           | _ => .error (.typeMismatch "set")
   | .store t =>
@@ -325,27 +435,17 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
       | .ok (v, st') =>
         -- Width-bucketed store (matches Rust `src/aiur/execute.rs:173-191`).
         -- Width = flat size of the stored value (funcIdx-irrelevant for length).
-        let w := (flattenValue decls (fun _ => none) v).size
-        let inner := st'.store[w]?.getD (default : IndexMap (Array Value) Unit)
-        if let some idx := inner.getIdxOf #[v] then
-          .ok (.pointer w idx, st')
-        else
-          let idx := inner.size
-          let inner' := inner.insert #[v] ()
-          let st'' := { st' with store := st'.store.insert w inner' }
-          .ok (.pointer w idx, st'')
+        let (ptr, st'') := storeValue decls st' v
+        .ok (ptr, st'')
   | .load t =>
       match interp decls fuel bindings t st with
       | .error e => .error e
       | .ok (v, st') =>
         match v with
         | .pointer w n =>
-          match st'.store[w]? with
-          | some inner =>
-            match inner.getByIdx n with
-            | some (vs, _) => .ok (vs[0]!, st')
-            | none         => .error (.invalidPointer n)
-          | none => .error (.invalidPointer n)
+          match loadValue st' w n with
+          | .ok v'    => .ok (v', st')
+          | .error e  => .error e
         | _ => .error (.typeMismatch "load")
   | .ptrVal t =>
       match interp decls fuel bindings t st with
@@ -465,18 +565,12 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
             else .error (.typeMismatch "u8RangeCheck")
           | _, _ => .error (.typeMismatch "u8RangeCheck")
   | .unconstrainedBigUintDivMod t1 t2 =>
-      -- TODO(unconstrainedBigUintDivMod): walk both List<U64> pointer chains via the
-      -- store to extract Vec<u8> bytes (LE), compute BigUint div_rem, build two
-      -- fresh ListNode chains, and return `.tuple #[.pointer w q_ptr, .pointer w r_ptr]`.
-      -- The Rust runtime already does this; the reference semantics doesn't yet
-      -- have klimbs/BigUint helpers. Surfacing typeMismatch keeps the source
-      -- evaluator total without committing to a half-baked semantics.
       match interp decls fuel bindings t1 st with
       | .error e => .error e
-      | .ok (_, st1) =>
+      | .ok (aPtr, st1) =>
         match interp decls fuel bindings t2 st1 with
         | .error e => .error e
-        | .ok (_, _) => .error (.typeMismatch "unconstrainedBigUintDivMod")
+        | .ok (bPtr, st2) => bigUintDivModValue decls aPtr bPtr st2
   | .unconstrainedGToBytes t =>
       match interp decls fuel bindings t st with
       | .error e => .error e
diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean
index 219113be7..5a9688d32 100644
--- a/Tests/Aiur/Aiur.lean
+++ b/Tests/Aiur/Aiur.lean
@@ -644,6 +644,80 @@ def toplevel := ⟦
     let r10 = to_field(s) + to_field(c) * 1000;   -- 1044
     r1 + r2 + r3 + r4 + r5 + r6 + r7 + r8 + r9 + r10
   }
+
+  ---------------------------------------------------------------------------
+  -- Unconstrained big-uint div/mod: lists of [U8; 8] limbs in, the same
+  -- list datatype at [G; 8] out. The datatype must declare Cons FIRST
+  -- (runtime tag contract: 0 = Cons, 1 = Nil). Limbs are little-endian
+  -- u64s, head-first.
+  ---------------------------------------------------------------------------
+  enum BNode‹T› {
+    BCons(T, &BNode‹T›),
+    BNil
+  }
+
+  fn blist0() -> &BNode‹[U8; 8]› { store(BNode.BNil) }
+  fn blist1(l: [U8; 8]) -> &BNode‹[U8; 8]› { store(BNode.BCons(l, blist0())) }
+  fn blist2(l0: [U8; 8], l1: [U8; 8]) -> &BNode‹[U8; 8]› {
+    store(BNode.BCons(l0, blist1(l1)))
+  }
+
+  -- u64 value of the first result limb (fits in G for the cases below).
+  fn glimb_val(p: &BNode‹[G; 8]›) -> G {
+    match load(p) {
+      BNode.BCons(l, _) => l[0] + 256 * l[1] + 65536 * l[2] + 16777216 * l[3]
+        + 4294967296 * l[4] + 1099511627776 * l[5] + 281474976710656 * l[6]
+        + 72057594037927936 * l[7],
+      BNode.BNil => 0,
+    }
+  }
+
+  fn glist_is_nil(p: &BNode‹[G; 8]›) -> G {
+    match load(p) {
+      BNode.BNil => 1,
+      BNode.BCons(_, _) => 0,
+    }
+  }
+
+  -- Aggregate: plain divide (300/7), unit divisor (300/1), zero divisor
+  -- (300/0 → (Nil, 300) by convention), and a two-limb dividend with a
+  -- Nil remainder (2^64 / 2 → (2^63, Nil), canonical single-limb q).
+  pub fn divmod_test() -> G {
+    let a300 = blist1([44u8, 1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let b7 = blist1([7u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let (q1, r1) = unconstrained_big_uint_div_mod(a300, b7);
+    let s1 = glimb_val(q1) + 1000 * glimb_val(r1);          -- 42 + 6000
+    let b1 = blist1([1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let (q2, _r2) = unconstrained_big_uint_div_mod(a300, b1);
+    let s2 = glimb_val(q2);                                 -- 300
+    let (q3, r3) = unconstrained_big_uint_div_mod(a300, blist0());
+    let s3 = 1000000 * glist_is_nil(q3) + glimb_val(r3);    -- 1000300
+    let a64 = blist2([0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8],
+                     [1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let b2 = blist1([2u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let (q4, r4) = unconstrained_big_uint_div_mod(a64, b2);
+    let s4 = glimb_val(q4) + glist_is_nil(r4);              -- 2^63 + 1
+    s1 + s2 + s3 + s4
+  }
+
+  ---------------------------------------------------------------------------
+  -- Unconstrained field hints: `g_to_bytes` returns the 8 LE bytes of the
+  -- CANONICAL u64 value as raw [G; 8] advice; `g_inverse` the field
+  -- inverse with 0 ↦ 0.
+  ---------------------------------------------------------------------------
+  pub fn hint_test() -> G {
+    -- 300 = 0x012C → LE bytes [44, 1, 0, ...]
+    let b = unconstrained_g_to_bytes(300);
+    let s1 = b[0] + 1000 * b[1];                -- 1044
+    let s2 = b[7];                              -- 0
+    -- x * x⁻¹ = 1 for x ≠ 0; 0 ↦ 0
+    let s3 = unconstrained_g_inverse(7) * 7;    -- 1
+    let s4 = unconstrained_g_inverse(0);        -- 0
+    -- Canonicality: 0 - 1 wraps to p - 1 = 0xFFFFFFFF00000000
+    let c = unconstrained_g_to_bytes(0 - 1);
+    let s5 = c[4] + c[0];                       -- 255
+    s1 + s2 + 10 * s3 + s4 + s5                 -- 1309
+  }
 ⟧
 
 /-- The PROVING suite: every case runs the full prove+verify pipeline
@@ -758,6 +832,13 @@ def aiurTestCases : List AiurTestCase := [
 
     -- Inlined function calls (`@fn(args)`): all scenarios in one proof
     .prove `inline_test #[] #[3182],
+
+    -- Unconstrained big-uint div/mod: all cases in one proof
+    -- (6042 + 300 + 1000300 + 2^63 + 1)
+    .prove `divmod_test #[] #[9223372036855782451],
+
+    -- Unconstrained g_to_bytes / g_inverse hints: all cases in one proof
+    .prove `hint_test #[] #[1309],
   ]
 
 end
diff --git a/Tests/Aiur/Cross.lean b/Tests/Aiur/Cross.lean
index 03cacbcbd..0c30d5c21 100644
--- a/Tests/Aiur/Cross.lean
+++ b/Tests/Aiur/Cross.lean
@@ -1161,6 +1161,76 @@ def toplevel : Source.Toplevel := ⟦
     let r10 = to_field(s) + to_field(c) * 1000;   -- 1044
     r1 + r2 + r3 + r4 + r5 + r6 + r7 + r8 + r9 + r10
   }
+
+  -- Unconstrained big-uint div/mod: lists of [U8; 8] limbs in, the same
+  -- list datatype at [G; 8] out. The datatype must declare Cons FIRST
+  -- (runtime tag contract: 0 = Cons, 1 = Nil). Limbs are little-endian
+  -- u64s, head-first.
+  enum BNode‹T› {
+    BCons(T, &BNode‹T›),
+    BNil
+  }
+
+  fn blist0() -> &BNode‹[U8; 8]› { store(BNode.BNil) }
+  fn blist1(l: [U8; 8]) -> &BNode‹[U8; 8]› { store(BNode.BCons(l, blist0())) }
+  fn blist2(l0: [U8; 8], l1: [U8; 8]) -> &BNode‹[U8; 8]› {
+    store(BNode.BCons(l0, blist1(l1)))
+  }
+
+  -- u64 value of the first result limb (fits in G for the cases below).
+  fn glimb_val(p: &BNode‹[G; 8]›) -> G {
+    match load(p) {
+      BNode.BCons(l, _) => l[0] + 256 * l[1] + 65536 * l[2] + 16777216 * l[3]
+        + 4294967296 * l[4] + 1099511627776 * l[5] + 281474976710656 * l[6]
+        + 72057594037927936 * l[7],
+      BNode.BNil => 0,
+    }
+  }
+
+  fn glist_is_nil(p: &BNode‹[G; 8]›) -> G {
+    match load(p) {
+      BNode.BNil => 1,
+      BNode.BCons(_, _) => 0,
+    }
+  }
+
+  -- Aggregate: plain divide (300/7), unit divisor (300/1), zero divisor
+  -- (300/0 → (Nil, 300) by convention), and a two-limb dividend with a
+  -- Nil remainder (2^64 / 2 → (2^63, Nil), canonical single-limb q).
+  pub fn divmod_test() -> G {
+    let a300 = blist1([44u8, 1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let b7 = blist1([7u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let (q1, r1) = unconstrained_big_uint_div_mod(a300, b7);
+    let s1 = glimb_val(q1) + 1000 * glimb_val(r1);          -- 42 + 6000
+    let b1 = blist1([1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let (q2, _r2) = unconstrained_big_uint_div_mod(a300, b1);
+    let s2 = glimb_val(q2);                                 -- 300
+    let (q3, r3) = unconstrained_big_uint_div_mod(a300, blist0());
+    let s3 = 1000000 * glist_is_nil(q3) + glimb_val(r3);    -- 1000300
+    let a64 = blist2([0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8],
+                     [1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let b2 = blist1([2u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8]);
+    let (q4, r4) = unconstrained_big_uint_div_mod(a64, b2);
+    let s4 = glimb_val(q4) + glist_is_nil(r4);              -- 2^63 + 1
+    s1 + s2 + s3 + s4
+  }
+
+  -- Unconstrained field hints: `g_to_bytes` returns the 8 LE bytes of the
+  -- CANONICAL u64 value as raw [G; 8] advice; `g_inverse` the field
+  -- inverse with 0 ↦ 0.
+  pub fn hint_test() -> G {
+    -- 300 = 0x012C → LE bytes [44, 1, 0, ...]
+    let b = unconstrained_g_to_bytes(300);
+    let s1 = b[0] + 1000 * b[1];                -- 1044
+    let s2 = b[7];                              -- 0
+    -- x * x⁻¹ = 1 for x ≠ 0; 0 ↦ 0
+    let s3 = unconstrained_g_inverse(7) * 7;    -- 1
+    let s4 = unconstrained_g_inverse(0);        -- 0
+    -- Canonicality: 0 - 1 wraps to p - 1 = 0xFFFFFFFF00000000
+    let c = unconstrained_g_to_bytes(0 - 1);
+    let s5 = c[4] + c[0];                       -- 255
+    s1 + s2 + 10 * s3 + s4 + s5                 -- 1309
+  }
 ⟧
 
 /-- Compiler outputs shared by every agreement case. Top-level closed
@@ -1482,6 +1552,10 @@ def tests : TestSeq :=
   runAgreement "non_tail_match" "non_tail_match" [] ++
   -- Inlined function calls (`@fn(args)`): all scenarios in one entry
   runAgreement "inline_test" "inline_test" [] ++
+  -- Unconstrained big-uint div/mod: all cases in one entry
+  runAgreement "divmod_test" "divmod_test" [] ++
+  -- Unconstrained g_to_bytes / g_inverse hints: all cases in one entry
+  runAgreement "hint_test" "hint_test" [] ++
   -- ----- Negative paths: every engine must reject --------------------------
   -- assert_eq! mismatch
   runFailureAgreement "assert_same(7,8) rejects" "assert_same" [7, 8] ++

From 71e88ceca7557824f3a1d1145716bacae60d4832 Mon Sep 17 00:00:00 2001
From: Arthur Paulino <arthurleonardo.ap@gmail.com>
Date: Wed, 5 Aug 2026 11:32:22 -0700
Subject: [PATCH 5/5] tests: promote quick Aiur suites from ignored to primary
 runners
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

aiur-prove, aiur-hashes, rbtree-map, multi-stark and recursive-verifier
are all seconds-scale now (measured: ~11s, 4s, 2s, 2s, 3s), so they run
by default. They stay as deferred IO runners — a new `primaryRunners`
list — rather than becoming `TestSeq` values, so their setup (Aiur
system builds, STARK proofs) does not execute at module initialization
for unrelated invocations. The primary section gains the same
unknown-name guard the ignored section has, and runner names work as
filter args (`lake test -- aiur-prove`).

Only ixvm remains in the ignored Aiur set; CI's Aiur step drops
--ignored for the migrated suites and keeps a separate ignored ixvm
step. The recursive-verifier's "~1.5 min" comment was stale — the
pipeline runs in seconds.

Full default `lake test` (all primary suites + runners): ~11.5s wall.
---
 .github/workflows/ci.yml |  8 ++++---
 Tests/Main.lean          | 47 ++++++++++++++++++++++++++++++----------
 Tests/MultiStark.lean    |  6 ++---
 3 files changed, 43 insertions(+), 18 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 9925992ee..420b569e2 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -80,10 +80,12 @@ jobs:
           use-github-cache: false
       - name: Test Ix CLI
         run: lake test --wfail -- cli
-      - name: Aiur compiler and interpreter tests
-        run: lake test --wfail -- aiur-cross
       - name: Aiur tests
-        run: lake test --wfail -- --ignored aiur-prove aiur-hashes ixvm multi-stark recursive-verifier
+        run: >-
+          lake test --wfail -- aiur-cross aiur-prove aiur-hashes rbtree-map
+          multi-stark recursive-verifier
+      - name: IxVM kernel tests
+        run: lake test --wfail -- --ignored ixvm
 
   rust-test:
     runs-on: ubuntu-latest
diff --git a/Tests/Main.lean b/Tests/Main.lean
index f96e9153a..f89d12afa 100644
--- a/Tests/Main.lean
+++ b/Tests/Main.lean
@@ -117,8 +117,13 @@ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [
   ("tc-ingress-meta", Tests.Tc.IngressMeta.suite),
 ]
 
-/-- Ignored test runners - expensive, deferred IO actions run only when explicitly requested -/
-def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
+/-- Primary test runners — quick suites run by default alongside
+`primarySuites`, but kept as deferred `IO` actions (not `TestSeq`
+values) so their setup — Aiur system builds, STARK proofs — does not
+execute at module initialization for unrelated invocations. All are
+seconds-scale (measured 2026-08-05: aiur-prove ~11s, the rest 2-4s
+each). -/
+def primaryRunners : List (String × IO UInt32) := [
   ("aiur-prove", do
     IO.println "aiur-prove"
     match AiurTestEnv.build (pure toplevel) with
@@ -135,6 +140,20 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
       | IO.eprintln "SHA256 setup failed"; return 1
     let r2 ← LSpec.lspecEachIO sha256TestCases fun tc => pure (sha256Env.runTestCase tc)
     return if r1 == 0 && r2 == 0 then 0 else 1),
+  ("rbtree-map", do
+    IO.println "rbtree-map"
+    match AiurTestEnv.build (pure IxVM.rbTreeMap) with
+    | .error e => IO.eprintln s!"RBTreeMap setup failed: {e}"; return 1
+    | .ok env => LSpec.lspecEachIO rbTreeMapTestCases fun tc => pure (env.runTestCase tc)),
+  -- Multi-STARK recursive verifier: `multi-stark` runs the verifier's
+  -- primitive self-tests, `recursive-verifier` the full
+  -- factorial-prove → recursive-verify → reject-tampering pipeline.
+  ("multi-stark", Tests.MultiStark.selfTestSuite),
+  ("recursive-verifier", Tests.MultiStark.endToEndSuite),
+]
+
+/-- Ignored test runners - expensive, deferred IO actions run only when explicitly requested -/
+def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
   ("ixvm", do
     let kernelChecks ← kernelChecks env
     -- the kernel CheckEnv smokes .
@@ -207,16 +226,6 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [
       LSpec.lspecIO
         (.ofList [("ixvm",
           [fullSeq, aiurSeq, arenaSeq, exploitSeq, paritySeq, shardSeq])]) []),
-  ("rbtree-map", do
-    IO.println "rbtree-map"
-    match AiurTestEnv.build (pure IxVM.rbTreeMap) with
-    | .error e => IO.eprintln s!"RBTreeMap setup failed: {e}"; return 1
-    | .ok env => LSpec.lspecEachIO rbTreeMapTestCases fun tc => pure (env.runTestCase tc)),
-  -- Multi-STARK recursive verifier (formerly the `recursive-verifier` executable):
-  -- `multi-stark` runs the cheap primitive self-tests, `recursive-verifier` runs the
-  -- ~1.5 min factorial-prove → recursive-verify → reject-tampering pipeline.
-  ("multi-stark", Tests.MultiStark.selfTestSuite),
-  ("recursive-verifier", Tests.MultiStark.endToEndSuite),
   ("validate-aux", runCompileValidateAux env),
   -- Cross-compiler differential over the same fixture corpus: pure-Lean
   -- Ix.CompileM per-block vs Rust, root-cause classified (see
@@ -264,12 +273,26 @@ def main (args : List String) : IO UInt32 := do
   -- Run primary tests unless --ignored (without --include-ignored) is specified
   if !runIgnored || includeIgnored then
     let primaryArgs := if runIgnored || includeIgnored then [] else filterArgs
+    -- Same guard as the ignored section: a filter arg naming neither a
+    -- primary suite nor a primary runner must be an ERROR, not a silent
+    -- no-op reporting success having run nothing.
+    for arg in primaryArgs do
+      if !primarySuites.contains arg
+          && !(primaryRunners.any fun (key, _) => key == arg)
+          && arg != "getfileenv-body" then
+        IO.eprintln s!"error: no primary suite or runner named '{arg}'"
+        return 1
     let primaryResult ← LSpec.lspecIO primarySuites primaryArgs
     if primaryResult != 0 then return primaryResult
     -- getFileEnv body-inclusion regression guard (IO: loads a fixture file)
     let envBodySeq ← Tests.Ix.EnvBody.suite
     let envBodyResult ← LSpec.lspecIO (.ofList [("getfileenv-body", [envBodySeq])]) primaryArgs
     if envBodyResult != 0 then return envBodyResult
+    let runners := if primaryArgs.isEmpty then primaryRunners
+      else primaryRunners.filter fun (key, _) => primaryArgs.contains key
+    for (_, action) in runners do
+      let r ← action
+      if r != 0 then return r
 
   -- Run ignored tests when --ignored or --include-ignored is specified
   if runIgnored || includeIgnored then
diff --git a/Tests/MultiStark.lean b/Tests/MultiStark.lean
index 37b081ff0..d13b0dd84 100644
--- a/Tests/MultiStark.lean
+++ b/Tests/MultiStark.lean
@@ -11,7 +11,7 @@ public import Blake3.Rust
 # Tests for the Multi-STARK recursive verifier
 
 These exercise `Ix/MultiStark.lean` (the in-circuit verifier) the way the former
-standalone `RecursiveVerifier.lean` executable did, split into two ignored
+standalone `RecursiveVerifier.lean` executable did, split into two primary
 runners (registered in `Tests/Main.lean`, both wired into `ci.yml`):
 
 * **`multi-stark`** — `selfTestSuite`. Executes the verifier's primitive
@@ -22,8 +22,8 @@ runners (registered in `Tests/Main.lean`, both wired into `ci.yml`):
   bytecode execution, no proving. The in-circuit `assert_eq!`s do the checking;
   every entrypoint returns `1` on success.
 
-* **`recursive-verifier`** — `endToEndSuite`. The full pipeline (~1.5 min,
-  dominated by proving + the verifier executions):
+* **`recursive-verifier`** — `endToEndSuite`. The full pipeline (a few
+  seconds, dominated by proving + the verifier executions):
   1. prove `factorial(5) = 120` with the Multi-STARK backend,
   2. feed that proof as non-deterministic advice (IO channel 0; vk on 1, claims
      on 2) and run `verify_multi_stark_proof` over it — it must accept,