UTF-8 typechecking unblocked (#451)

* IxVM kernel: native unconstrained_big_uint_div_mod Aiur op + small wins

* Aiur op `unconstrained_big_uint_div_mod(a: KLimbs, b: KLimbs) -> (KLimbs, KLimbs)`:
  runtime computes (q, r) via `num_bigint::BigUint::div_rem` and inserts
  both result lists into `memory[10]` content-addressed with
  multiplicity 0; no constraints emitted. Wired through
  bytecode/execute/constraints/trace + FFI decoder +
  Source/Typed/Simple/Concrete/Bytecode stages + Meta syntax +
  Compiler/{Check, Concretize, Simple, Match, Lower, Layout}. Lean
  reference evaluators (Interpret/SourceEval/BytecodeEval) are stubbed
  with TODOs; src/aiur/execute.rs is the authoritative impl.

* Primitive.lean: `klimbs_div_mod` now reads (q, r) from the op then
  verifies `klimbs_normalize(klimbs_add(klimbs_mul(q, b), r)) == klimbs_normalize(a)`
  and `klimbs_lt(r, b) == 1` when `b != 0`. Drops recursive
  `klimbs_div_mod_go`: its 2^24-step memo growth on (2^32, 256) was the
  klimbs OOM driver.

* Core.lean: route list_lookup through list_drop so sublist ptrs dedup
  via Aiur's content-addressed store.

* Infer.lean: collapse App-spine inference into one helper that peels
  the head's Forall telescope arg-by-arg using a single expr_inst_many
  per step on the ORIGINAL dom (with a growing innermost-first subs
  list) instead of N consecutive expr_inst1 rewalks of a residual cod.

* Tests/Ix/IxVM.lean: re-pin 37 FFT costs.

lake exe check Nat.add_comm: 55_504_714 -> 54_350_107 FFT (-2.1%).
lake exe check '_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.helper₃':
previously OOM (~1.2 GB single allocation inside klimbs_div_mod_go);
now passes at 37_793_684_978 FFT.

* IxVM kernel: fix klimbs_to_ctor_form to single-step expansion

`klimbs_to_ctor_form` recursively unfolded a Nat literal `n` into the
full ctor chain `Nat.succ^n(Nat.zero)`. For large `n` the recursion
created O(n) memo entries (one per `klimbs_dec`, one per
`klimbs_normalize`, one per the recursive `klimbs_to_ctor_form` call)
and OOM'd the per-fn function_queries before completing.

Rust's `nat_to_constructor` (src/ix/kernel/whnf.rs:1664-1687) does the
right thing: produce `Nat.succ(Lit(n-1))` — a single ctor wrap whose
predecessor stays a `Lit(Nat)`. Subsequent iota reductions re-trigger
expansion only as needed. Mirror that semantics in Aiur.

`lake exe check '_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.<bomb>'`
with `ulimit -v 20000000`:
* assemble₂._proof_1:                 OOM → 11_936_582_540 FFT
* assemble₃._proof_3:                 OOM → 11_934_210_486 FFT
* assemble₃._proof_4:                 OOM → 11_968_289_150 FFT
* assemble₄_eq_some_iff_..._proof_1_13: OOM → 8_510_124_580 FFT
* helper₃:                  37_793_684_978 → 16_870_284_540 FFT (-55.4%)

`lake exe check 'ByteArray.utf8DecodeChar?_utf8EncodeChar_append'` with
`ulimit -v 22000000`: passes at 43_544_984_712 FFT (the full theorem,
which was the original UTF-8 blocker).

Tests/Ix/IxVM.lean: 18 small FFT pin increases — every const whose
WHNF path now eagerly synthesizes a `Lit(n-1)` predecessor (one extra
`mk_nat_lit` per ctor-form coercion instead of zero in the old
recursive body that walked the whole chain anyway).

Author: arthurpaulino

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)