Aiur test pipeline: proving/execution split, unconstrained-op typing, full cross-engine coverage

.github/workflows/ci.yml

@@ -81,7 +81,11 @@ jobs:
       - name: Test Ix CLI
         run: lake test --wfail -- cli
       - name: Aiur tests
-        run: lake test --wfail -- --ignored aiur 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

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,17 +810,18 @@ 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`).
+    -- 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')

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

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))
@@ -489,7 +562,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)