Skip to content

Commit 6bf777f

Browse files
arthurpaulinoarthurpaulino
committed
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).
1 parent 5aa84bd commit 6bf777f

3 files changed

Lines changed: 34 additions & 27 deletions

File tree

‎Ix/IxVM/Kernel/Primitive.lean‎

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1267,16 +1267,23 @@ def primitive := ⟦
12671267
}
12681268
}
12691269

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

‎Tests/Ix/IxVM.lean‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -120,36 +120,36 @@ private def kernelCheckEntries : List (String × Nat) := [
120120
("Eq.rec", 2_575_090),
121121
("Nat", 1_857_572),
122122
("Nat.add", 12_973_039),
123-
("Nat.add_comm", 54_350_107),
123+
("Nat.add_comm", 54_350_110),
124124
("Nat.decEq", 68_538_632),
125-
("Nat.decLe", 191_354_790),
126-
("Nat.sub_le_of_le_add", 515_033_220),
125+
("Nat.decLe", 191_354_793),
126+
("Nat.sub_le_of_le_add", 515_056_158),
127127
-- Newly-unlocked targets (level_leq Géran normalize).
128128
("Trans.mk", 2_863_374),
129-
("Array.append_assoc", 2_588_113_566),
130-
("Vector.append", 2_661_200_807),
129+
("Array.append_assoc", 2_588_157_538),
130+
("Vector.append", 2_661_244_845),
131131
-- Primitive reduction theorems (`IxVMPrim`)
132132
("IxVMPrim.nat_add_lit", 28_083_713),
133133
("IxVMPrim.nat_sub_lit", 33_755_207),
134134
("IxVMPrim.nat_mul_lit", 24_642_249),
135135
("IxVMPrim.nat_mul_big", 24_116_975),
136-
("IxVMPrim.nat_div_lit", 367_240_783),
137-
("IxVMPrim.nat_mod_lit", 375_936_541),
136+
("IxVMPrim.nat_div_lit", 367_262_654),
137+
("IxVMPrim.nat_mod_lit", 375_958_446),
138138
("IxVMPrim.nat_succ_lit", 7_307_039),
139139
("IxVMPrim.nat_pred_lit", 14_682_236),
140-
("IxVMPrim.nat_gcd_lit", 605_481_967),
141-
("IxVMPrim.nat_land_lit", 1_019_712_405),
142-
("IxVMPrim.nat_lor_lit", 1_020_941_332),
143-
("IxVMPrim.nat_xor_lit", 1_029_773_064),
140+
("IxVMPrim.nat_gcd_lit", 605_512_664),
141+
("IxVMPrim.nat_land_lit", 1_019_743_752),
142+
("IxVMPrim.nat_lor_lit", 1_020_972_680),
143+
("IxVMPrim.nat_xor_lit", 1_029_804_417),
144144
("IxVMPrim.nat_shl_lit", 34_843_370),
145-
("IxVMPrim.nat_shr_lit", 372_704_905),
145+
("IxVMPrim.nat_shr_lit", 372_726_784),
146146
("IxVMPrim.nat_beq_lit", 24_108_404),
147147
("IxVMPrim.nat_ble_lit", 22_469_243),
148-
("IxVMPrim.nat_dec_le", 198_104_577),
149-
("IxVMPrim.nat_dec_lt", 202_076_476),
148+
("IxVMPrim.nat_dec_le", 198_104_580),
149+
("IxVMPrim.nat_dec_lt", 202_076_479),
150150
("IxVMPrim.nat_dec_eq", 82_352_518),
151-
("IxVMPrim.str_size_lit", 733_871_761),
152-
("IxVMPrim.bv_to_nat_lit", 577_337_315),
151+
("IxVMPrim.str_size_lit", 733_902_817),
152+
("IxVMPrim.bv_to_nat_lit", 577_368_072),
153153
-- Mutual block + multi-member recursors
154154
("IxVMInd.Even", 25_965_406),
155155
("IxVMInd.Odd", 25_728_543),
@@ -159,8 +159,8 @@ private def kernelCheckEntries : List (String × Nat) := [
159159
("IxVMInd.Tree", 2_634_462),
160160
("IxVMInd.Tree.rec", 4_870_642),
161161
-- Edge cases from prelude
162-
("String.Internal.append", 725_384_432),
163-
("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_091_321_972),
162+
("String.Internal.append", 725_415_461),
163+
("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_091_354_031),
164164
]
165165

166166
private def nameOfString (str : String) : Lean.Name :=

‎src/aiur/bytecode.rs‎

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

0 commit comments

Comments
 (0)