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/IxVM/Kernel/Primitive.lean

@@ -1249,16 +1249,23 @@ def primitive := ⟦
     }
   }
 
-  -- Convert a KLimbs n into a chain `App(Const(succ), App(Const(succ),
-  -- ... Const(zero)))` for n calls of succ. Used by nat-literal-to-ctor
-  -- coercion in iota.
+  -- Single-step Nat-literal → ctor coercion. Mirrors Rust
+  -- `nat_to_constructor` (src/ix/kernel/whnf.rs:1664-1687):
+  --   0   → `Const(Nat.zero)`
+  --   n+1 → `App(Const(Nat.succ), Lit(Nat(n-1)))`
+  -- The predecessor stays a `Lit`; the iota that asked for this expansion
+  -- only needs to see the head ctor. Subsequent matches re-trigger
+  -- expansion as needed. The previous body unfolded recursively into
+  -- `Nat.succ^n(Nat.zero)`, which OOM'd for large literals (the original
+  -- driver: per-step `klimbs_dec` memo growth, 4M+ entries seen on
+  -- `Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₂._proof_1`
+  -- before allocation failure).
   fn klimbs_to_ctor_form(n: KLimbs, zero_idx: G, succ_idx: G) -> KExpr {
     match load(n) {
       ListNode.Nil =>
         store(KExprNode.Const(zero_idx, store(ListNode.Nil))),
       ListNode.Cons(_, _) =>
-        let dec = klimbs_dec(n);
-        let pred = klimbs_to_ctor_form(dec, zero_idx, succ_idx);
+        let pred = mk_nat_lit(klimbs_normalize(klimbs_dec(n)));
         let succ_const = store(KExprNode.Const(succ_idx, store(ListNode.Nil)));
         store(KExprNode.App(succ_const, pred)),
     }

src/aiur/bytecode.rs

@@ -64,10 +64,10 @@ pub enum Op {
   /// Range-check two values into `[0, 256)` via the byte chip. Produces no new
   /// values: its `u8` results alias the two inputs (cf. `AssertEq`).
   U8RangeCheck(ValIdx, ValIdx),
-  /// Unconstrained LE byte-list division-modulo hint. Inputs are two pointers
-  /// to `ByteStream` (= `List<U8>`) values storing the dividend `a` and
-  /// divisor `b` as little-endian byte sequences. Outputs two new pointers to
-  /// `ByteStream` values for the quotient `q` and remainder `r` such that
+  /// Unconstrained `BigUint` division-modulo hint. Inputs are two pointers
+  /// to `KLimbs` (= `List<U64>`) values storing the dividend `a` and divisor
+  /// `b` as little-endian u64 limb chains. Outputs two new pointers to
+  /// `KLimbs` values for the quotient `q` and remainder `r` such that
   /// `q * b + r = a` with `0 ≤ r < b` (when `b > 0`). Computed natively by
   /// the runtime via `num_bigint::BigUint::div_rem`; no in-circuit recursion
   /// and no constraints generated. The caller is responsible for verifying