IxVM kernel: unblock ByteArray.utf8DecodeChar?_utf8EncodeChar_append

Ix/Aiur/Compiler/Check.lean

@@ -787,6 +787,13 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
     let a' ← checkNoEscape a .field
     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).
+    let a' ← inferNoEscape a
+    let b' ← checkNoEscape b a'.typ
+    pure (Typed.Term.unconstrainedBigUintDivMod (.tuple #[a'.typ, a'.typ]) false a' b')
   | .toField a => do
     let a' ← checkNoEscape a .u8
     pure (Typed.Term.toField .field false a')
@@ -965,6 +972,8 @@ def zonkTypedTerm (t : Typed.Term) : CheckM Typed.Term := match t with
       pure (.u32LessThan (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .u8RangeCheck τ e a b => do
       pure (.u8RangeCheck (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
+  | .unconstrainedBigUintDivMod τ e a b => do
+      pure (.unconstrainedBigUintDivMod (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b))
   | .toField τ e a => do pure (.toField (← zonkTyp τ) e (← zonkTypedTerm a))
   | .u8FromFieldUnsafe τ e a => do
       pure (.u8FromFieldUnsafe (← zonkTyp τ) e (← zonkTypedTerm a))

Ix/Aiur/Compiler/Concretize.lean

@@ -363,6 +363,9 @@ def termToConcrete
   | .u8RangeCheck τ e a b => do
       pure (.u8RangeCheck (← typToConcrete mono τ) e
                           (← termToConcrete mono a) (← termToConcrete mono b))
+  | .unconstrainedBigUintDivMod τ e a b => do
+      pure (.unconstrainedBigUintDivMod (← typToConcrete mono τ) e
+                                    (← termToConcrete mono a) (← termToConcrete mono b))
   -- `toField` / `u8FromFieldUnsafe` are erased coercions: `u8` and `field`
   -- share a representation, so we drop the wrapper and keep the inner term.
   | .toField _ _ a | .u8FromFieldUnsafe _ _ a => termToConcrete mono a
@@ -570,6 +573,8 @@ def rewriteTypedTerm (decls : Typed.Decls)
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
   | .u8RangeCheck τ e a b => .u8RangeCheck (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
+  | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod (rewriteTyp subst mono τ) e
+      (rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
   | .toField τ e a => .toField (rewriteTyp subst mono τ) e
       (rewriteTypedTerm decls subst mono a)
   | .u8FromFieldUnsafe τ e a => .u8FromFieldUnsafe (rewriteTyp subst mono τ) e
@@ -642,6 +647,7 @@ def collectInTypedTerm (seen : Std.HashSet (Global × Array Typ)) :
   | .add τ _ a b | .sub τ _ a b | .mul τ _ a b
   | .u8Xor τ _ a b | .u8Add τ _ a b | .u8Mul τ _ a b | .u8Sub τ _ a b
   | .u8ChainRotr7 τ _ a b | .u8ChainRotr4 τ _ a b | .u8RangeCheck τ _ a b
+  | .unconstrainedBigUintDivMod τ _ a b
   | .u8And τ _ a b | .u8Or τ _ a b
   | .u8LessThan τ _ a b | .u32LessThan τ _ a b =>
     collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b
@@ -712,6 +718,7 @@ def collectCalls (decls : Typed.Decls)
   | .add _ _ a b | .sub _ _ a b | .mul _ _ a b
   | .u8Xor _ _ a b | .u8Add _ _ a b | .u8Mul _ _ a b | .u8Sub _ _ a b
   | .u8ChainRotr7 _ _ a b | .u8ChainRotr4 _ _ a b | .u8RangeCheck _ _ a b
+  | .unconstrainedBigUintDivMod _ _ a b
   | .u8And _ _ a b | .u8Or _ _ a b
   | .u8LessThan _ _ a b | .u32LessThan _ _ a b =>
     collectCalls decls (collectCalls decls seen a) b
@@ -830,6 +837,8 @@ def substInTypedTerm (subst : Global → Option Typ) : Typed.Term → Typed.Term
       (substInTypedTerm subst a) (substInTypedTerm subst b)
   | .u8RangeCheck τ e a b => .u8RangeCheck (Typ.instantiate subst τ) e
       (substInTypedTerm subst a) (substInTypedTerm subst b)
+  | .unconstrainedBigUintDivMod τ e a b => .unconstrainedBigUintDivMod (Typ.instantiate subst τ) e
+      (substInTypedTerm subst a) (substInTypedTerm subst b)
   | .toField τ e a => .toField (Typ.instantiate subst τ) e (substInTypedTerm subst a)
   | .u8FromFieldUnsafe τ e a =>
     .u8FromFieldUnsafe (Typ.instantiate subst τ) e (substInTypedTerm subst a)

Ix/Aiur/Compiler/Layout.lean

@@ -203,6 +203,10 @@ def opLayout : Bytecode.Op → LayoutM Unit
   | .u32LessThan .. => do pushDegree 1; bumpAuxiliaries 12; bumpLookups 6
   -- Pure range-check lookup: no output columns/degrees, just one lookup.
   | .u8RangeCheck .. => bumpLookups
+  -- Unconstrained hint: two fresh auxiliary witness columns (q_ptr, r_ptr).
+  -- No constraint relation, no lookup. Mirrors `IORead` (aux only) — the Rust
+  -- `constraints.rs` pushes exactly 2 auxiliaries and emits no relation.
+  | .unconstrainedBigUintDivMod .. => do pushDegrees #[1, 1]; bumpAuxiliaries 2
   | .debug .. => pure ()
 
 /-- Termination helper for blockLayout's Block/Ctrl traversal. -/

Ix/Aiur/Compiler/Lower.lean

@@ -326,6 +326,13 @@ def toIndex
     let j ← expectIdx layoutMap bindings j
     modify fun stt => { stt with ops := stt.ops.push (.u8RangeCheck i j) }
     pure #[i, j]
+  | .unconstrainedBigUintDivMod _ _ a b => do
+    -- Unconstrained hint: runtime computes q,r via BigUint::div_rem and writes
+    -- two fresh pointers (q_ptr, r_ptr) into the witness columns. No constraint
+    -- relation is emitted; caller verifies `q*b + r == a` and `r < b` separately.
+    let a ← expectIdx layoutMap bindings a
+    let b ← expectIdx layoutMap bindings b
+    pushOp (.unconstrainedBigUintDivMod a b) 2
   | .debug _ _ label term ret => do
     let term ← match term with
       | none => pure none

Ix/Aiur/Compiler/Match.lean

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

Ix/Aiur/Compiler/Simple.lean

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

Ix/Aiur/Interpret.lean

@@ -406,6 +406,17 @@ partial def interp (decls : Decls) (bindings : Bindings) : Term → InterpM Valu
           if a.val < 256 && b.val < 256 then return .tuple #[.field a, .field b]
           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"
   -- `toField` / `u8FromFieldUnsafe` are erased coercions: value unchanged.
   | .toField t | .u8FromFieldUnsafe t => interp decls bindings t
   | .u8Lit n => return .field (G.ofNat n)

Ix/Aiur/Meta.lean

@@ -188,6 +188,7 @@ syntax "u8_or" "(" aiur_trm ", " aiur_trm ")"                               : ai
 syntax "u8_less_than" "(" aiur_trm ", " aiur_trm ")"                        : aiur_trm
 syntax "u32_less_than" "(" aiur_trm ", " aiur_trm ")"                       : aiur_trm
 syntax "u8_range_check" "(" aiur_trm ", " aiur_trm ")"                      : aiur_trm
+syntax "unconstrained_big_uint_div_mod" "(" aiur_trm ", " aiur_trm ")"           : aiur_trm
 syntax "to_field" "(" aiur_trm ")"                                          : aiur_trm
 syntax "u8_from_field_unsafe" "(" aiur_trm ")"                              : aiur_trm
 syntax:max num "u8"                                                         : aiur_trm
@@ -323,6 +324,8 @@ partial def elabTrm : ElabStxCat `aiur_trm
     mkAppM ``Source.Term.u32LessThan #[← elabTrm i, ← elabTrm j]
   | `(aiur_trm| u8_range_check($i:aiur_trm, $j:aiur_trm)) => do
     mkAppM ``Source.Term.u8RangeCheck #[← elabTrm i, ← elabTrm j]
+  | `(aiur_trm| unconstrained_big_uint_div_mod($a:aiur_trm, $b:aiur_trm)) => do
+    mkAppM ``Source.Term.unconstrainedBigUintDivMod #[← elabTrm a, ← elabTrm b]
   | `(aiur_trm| to_field($a:aiur_trm)) => do
     mkAppM ``Source.Term.toField #[← elabTrm a]
   | `(aiur_trm| u8_from_field_unsafe($a:aiur_trm)) => do
@@ -547,6 +550,10 @@ where
       let i ← replaceToken old new i
       let j ← replaceToken old new j
       `(aiur_trm| u8_range_check($i, $j))
+    | `(aiur_trm| unconstrained_big_uint_div_mod($a:aiur_trm, $b:aiur_trm)) => do
+      let a ← replaceToken old new a
+      let b ← replaceToken old new b
+      `(aiur_trm| unconstrained_big_uint_div_mod($a, $b))
     | `(aiur_trm| to_field($a:aiur_trm)) => do
       let a ← replaceToken old new a
       `(aiur_trm| to_field($a))

Ix/Aiur/Semantics/BytecodeEval.lean

@@ -40,6 +40,7 @@ inductive BytecodeError
   | callOutputSizeMismatch
   | unreachableAfterLayout
   | u8RangeCheckFailed
+  | unconstrainedBigUintDivModUnsupported
   deriving Repr, Inhabited
 
 /-- Width-bucketed memory, matching Rust's `QueryRecord.memory_queries`.
@@ -293,6 +294,15 @@ def evalOp (t : Bytecode.Toplevel) (fuel : Nat) (op : Op) (st : EvalState) :
     -- outside `[0, 256)` (exactly what the byte-chip lookup enforces).
     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
   | .debug _ _ => .ok st
 termination_by (fuel, sizeOf op, 0)
 decreasing_by all_goals first | decreasing_tactic | omega

Ix/Aiur/Semantics/SourceEval.lean

@@ -444,6 +444,19 @@ def interp (decls : Decls) (fuel : Nat) (bindings : Bindings)
               .ok (.tuple #[.field a, .field b], st2)
             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) =>
+        match interp decls fuel bindings t2 st1 with
+        | .error e => .error e
+        | .ok (_, _) => .error (.typeMismatch "unconstrainedBigUintDivMod")
   -- `toField` / `u8FromFieldUnsafe` are erased coercions: value unchanged.
   | .toField t | .u8FromFieldUnsafe t => interp decls fuel bindings t st
   | .u8Lit n => .ok (.field (G.ofNat n), st)

Ix/Aiur/Stages/Bytecode.lean

@@ -50,6 +50,12 @@ inductive Op
   new values: it is a pure side-effect (lookup), and its `u8` results alias the
   two inputs. Kept last so its FFI tag (27) doesn't shift the others. -/
   | u8RangeCheck : ValIdx → ValIdx → Op
+  /-- Unconstrained LE byte-list division-modulo hint. Inputs are pointers to
+  two `List<U64>` (klimbs) values. Produces 2 fresh pointer values
+  `(q_ptr, r_ptr)` to newly-built `List<U64>` values such that `q*b + r = a`
+  and `0 ≤ r < b` (when `b > 0`). No constraint relation emitted; caller
+  must verify in constrained code. -/
+  | unconstrainedBigUintDivMod : ValIdx → ValIdx → Op
   deriving Repr, BEq, Hashable
 
 mutual

Ix/Aiur/Stages/Concrete.lean

@@ -87,6 +87,7 @@ inductive Term : Type where
   | u8ChainRotr7 (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | u8ChainRotr4 (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | u8RangeCheck (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
+  | unconstrainedBigUintDivMod (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | debug (typ : Typ) (escapes : Bool) (label : String) (t : Option Term) (r : Term) : Term
   deriving Repr, Inhabited
 
@@ -105,6 +106,7 @@ def Term.typ : Term → Typ
   | .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Mul t _ _ _ | .u8Sub t _ _ _
   | .u8And t _ _ _ | .u8Or t _ _ _ | .u8LessThan t _ _ _ | .u32LessThan t _ _ _
   | .u8ChainRotr7 t _ _ _ | .u8ChainRotr4 t _ _ _ | .u8RangeCheck t _ _ _
+  | .unconstrainedBigUintDivMod t _ _ _
   | .debug t _ _ _ _ => t
 
 /-- Get the escapes flag of a Concrete.Term. -/
@@ -122,6 +124,7 @@ def Term.escapes : Term → Bool
   | .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Mul _ e _ _ | .u8Sub _ e _ _
   | .u8And _ e _ _ | .u8Or _ e _ _ | .u8LessThan _ e _ _ | .u32LessThan _ e _ _
   | .u8ChainRotr7 _ e _ _ | .u8ChainRotr4 _ e _ _ | .u8RangeCheck _ e _ _
+  | .unconstrainedBigUintDivMod _ e _ _
   | .debug _ e _ _ _ => e
 
 structure Constructor where

Ix/Aiur/Stages/Simple.lean

@@ -83,6 +83,7 @@ inductive Term : Type where
   | u8ChainRotr7 (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | u8ChainRotr4 (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | u8RangeCheck (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
+  | unconstrainedBigUintDivMod (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | toField (typ : Typ) (escapes : Bool) (a : Term) : Term
   | u8FromFieldUnsafe (typ : Typ) (escapes : Bool) (a : Term) : Term
   | debug (typ : Typ) (escapes : Bool) (label : String) (t : Option Term) (r : Term) : Term
@@ -102,6 +103,7 @@ def Term.typ : Term → Typ
   | .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Mul t _ _ _ | .u8Sub t _ _ _
   | .u8And t _ _ _ | .u8Or t _ _ _ | .u8LessThan t _ _ _ | .u32LessThan t _ _ _
   | .u8ChainRotr7 t _ _ _ | .u8ChainRotr4 t _ _ _ | .u8RangeCheck t _ _ _
+  | .unconstrainedBigUintDivMod t _ _ _
   | .toField t _ _ | .u8FromFieldUnsafe t _ _
   | .debug t _ _ _ _ => t
 
@@ -119,6 +121,7 @@ def Term.escapes : Term → Bool
   | .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Mul _ e _ _ | .u8Sub _ e _ _
   | .u8And _ e _ _ | .u8Or _ e _ _ | .u8LessThan _ e _ _ | .u32LessThan _ e _ _
   | .u8ChainRotr7 _ e _ _ | .u8ChainRotr4 _ e _ _ | .u8RangeCheck _ e _ _
+  | .unconstrainedBigUintDivMod _ e _ _
   | .toField _ e _ | .u8FromFieldUnsafe _ e _
   | .debug _ e _ _ _ => e
 

Ix/Aiur/Stages/Source.lean

@@ -417,6 +417,13 @@ inductive Term
   | u32LessThan : Term → Term → Term
   | u8ChainRotr7 : Term → Term → Term
   | u8ChainRotr4 : Term → Term → Term
+  /-- Unconstrained LE byte-list division-modulo hint. Inputs are two
+  `List<U64>` (klimbs) values (LE limb order). Output is a tuple of two
+  fresh `List<U64>` values `(q, r)` with `q*b + r = a` and `0 ≤ r < b`
+  (when `b > 0`). Computed natively by the Aiur runtime via BigUint
+  div_rem; no constraints generated and no per-step memo growth. The
+  caller must verify `q*b + r == a` and `r < b` in constrained code. -/
+  | unconstrainedBigUintDivMod : (a : Term) → (b : Term) → Term
   /-- A `U8` literal in `[0, 256)`. Lowered to a plain field constant of type
   `u8` (no range-check lookup, since the value is statically in range). -/
   | u8Lit : Nat → Term

Ix/Aiur/Stages/Typed.lean

@@ -59,6 +59,7 @@ inductive Term : Type where
   | u8ChainRotr7 (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | u8ChainRotr4 (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | u8RangeCheck (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
+  | unconstrainedBigUintDivMod (typ : Typ) (escapes : Bool) (a : Term) (b : Term) : Term
   | toField (typ : Typ) (escapes : Bool) (a : Term) : Term
   | u8FromFieldUnsafe (typ : Typ) (escapes : Bool) (a : Term) : Term
   | debug (typ : Typ) (escapes : Bool) (label : String) (t : Option Term) (r : Term) : Term
@@ -78,6 +79,7 @@ def Term.typ : Term → Typ
   | .u8Xor t _ _ _ | .u8Add t _ _ _ | .u8Mul t _ _ _ | .u8Sub t _ _ _
   | .u8And t _ _ _ | .u8Or t _ _ _ | .u8LessThan t _ _ _ | .u32LessThan t _ _ _
   | .u8ChainRotr7 t _ _ _ | .u8ChainRotr4 t _ _ _ | .u8RangeCheck t _ _ _
+  | .unconstrainedBigUintDivMod t _ _ _
   | .toField t _ _ | .u8FromFieldUnsafe t _ _
   | .debug t _ _ _ _ => t
 
@@ -95,6 +97,7 @@ def Term.escapes : Term → Bool
   | .u8Xor _ e _ _ | .u8Add _ e _ _ | .u8Mul _ e _ _ | .u8Sub _ e _ _
   | .u8And _ e _ _ | .u8Or _ e _ _ | .u8LessThan _ e _ _ | .u32LessThan _ e _ _
   | .u8ChainRotr7 _ e _ _ | .u8ChainRotr4 _ e _ _ | .u8RangeCheck _ e _ _
+  | .unconstrainedBigUintDivMod _ e _ _
   | .toField _ e _ | .u8FromFieldUnsafe _ e _
   | .debug _ e _ _ _ => e
 

Ix/IxVM/Core.lean

@@ -52,11 +52,8 @@ def core := ⟦
   }
 
   fn list_lookup‹T›(list: List‹T›, idx: G) -> T {
-    let ListNode.Cons(v, rest) = load(list);
-    match idx {
-      0 => v,
-      _ => list_lookup(rest, idx - 1),
-    }
+    let ListNode.Cons(v, _) = load(list_drop(list, idx));
+    v
   }
 
   fn list_lookup_u64‹T›(list: List‹T›, idx: U64) -> T {