From 805656edfa58a033c2d23aac929e94e5645d7e8a Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Tue, 23 Jun 2026 18:12:36 -0700 Subject: [PATCH] IxVM kernel: klimbs_pow via binary exponentiation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace `klimbs_mul(base, klimbs_pow(base, klimbs_dec(exp)))`'s O(exp) per-step memo growth with a binary-exponentiation recursion of depth O(log exp). Both `exp / 2` and `exp % 2` route through the native `unconstrained_big_uint_div_mod` op, so each level pays O(1) for the division — `log2(exp)` memo entries for `klimbs_pow` itself + the `klimbs_mul(base, base)` doublings. `lake test -- --ignored ixvm` on `IxVMPrim.nat_pow_big` (`(2 ^ 16384 : Nat) - 2 ^ 16384 = 0`, measured against the current `ap/utf8-mod-witness` baseline): 3_941_276_885 → 71_856_587 FFT (-98.2%). Tests/Ix/IxVM.lean: * new `IxVMPrim.nat_pow_big` synthetic — exercises `klimbs_pow` at a non-trivial exponent (`2 ^ 16384`) so future regressions in the body shift its FFT pin. * small pin shifts in `nat_shl_lit`, `nat_shr_lit`, `nat_div_lit`, `nat_mod_lit`, `nat_gcd_lit`, `bv_to_nat_lit` — all reduce via `klimbs_pow` / `klimbs_div_mod` and absorb the new cost shape. --- Ix/IxVM/Kernel/Primitive.lean | 19 ++++++++++++++++++- Tests/Ix/IxVM.lean | 14 +++++++++++--- 2 files changed, 29 insertions(+), 4 deletions(-) diff --git a/Ix/IxVM/Kernel/Primitive.lean b/Ix/IxVM/Kernel/Primitive.lean index 6462e3be..2254f08b 100644 --- a/Ix/IxVM/Kernel/Primitive.lean +++ b/Ix/IxVM/Kernel/Primitive.lean @@ -1152,10 +1152,27 @@ def primitive := ⟦ } } + -- Binary exponentiation. Replaces the old O(exp) recursive + -- `klimbs_mul(base, klimbs_pow(base, klimbs_dec(exp)))` body, which + -- created one per-fn memo row per exponent step and OOM'd for + -- non-trivial exponents. Recursion depth is `log2(exp)` — for + -- `exp = 2^32` that's 32 memo entries instead of 4 billion. + -- + -- Both `klimbs_div2` (= `klimbs_div(exp, 2)`) and `klimbs_is_odd` + -- (= `klimbs_mod(exp, 2) != 0`) route through `klimbs_div_mod`, which + -- is itself native (unconstrained_big_uint_div_mod) — so the + -- division per step is O(1) work. fn klimbs_pow(base: KLimbs, exp: KLimbs) -> KLimbs { match klimbs_is_zero(exp) { 1 => store(ListNode.Cons([1u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8], store(ListNode.Nil))), - 0 => klimbs_mul(base, klimbs_pow(base, klimbs_dec(exp))), + 0 => + let two = store(ListNode.Cons([2u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8, 0u8], store(ListNode.Nil))); + let (half, r) = klimbs_div_mod(exp, two); + let sq = klimbs_pow(klimbs_normalize(klimbs_mul(base, base)), klimbs_normalize(half)); + match klimbs_is_zero(r) { + 1 => sq, + 0 => klimbs_mul(base, sq), + }, } } diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 41c7ac42..d73e870d 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -44,6 +44,13 @@ public theorem nat_lor_lit : Nat.lor 0xf0 0x0f = 0xff := rfl public theorem nat_xor_lit : Nat.xor 0xff 0x0f = 0xf0 := rfl public theorem nat_shl_lit : Nat.shiftLeft 1 8 = 256 := rfl public theorem nat_shr_lit : Nat.shiftRight 256 4 = 16 := rfl +-- Synthetic: exercises `klimbs_pow` at a non-trivial exponent so the cost +-- of the current O(exp) recursive implementation shows up in the FFT pin. +-- Sized to terminate under typical caps with the current O(exp) body — a +-- proxy for the eventual binary-exponentiation rewrite. +set_option exponentiation.threshold 65536 in +set_option maxRecDepth 65536 in +public theorem nat_pow_big : (2 ^ 16384 : Nat) - (2 ^ 16384) = 0 := rfl -- Nat predicates (return Bool ctors) public theorem nat_beq_lit : Nat.beq 42 42 = true := rfl @@ -141,15 +148,16 @@ private def kernelCheckEntries : List (String × Nat) := [ ("IxVMPrim.nat_land_lit", 1_019_743_752), ("IxVMPrim.nat_lor_lit", 1_020_972_680), ("IxVMPrim.nat_xor_lit", 1_029_804_417), - ("IxVMPrim.nat_shl_lit", 34_843_370), - ("IxVMPrim.nat_shr_lit", 372_727_841), + ("IxVMPrim.nat_shl_lit", 34_836_668), + ("IxVMPrim.nat_shr_lit", 372_729_464), + ("IxVMPrim.nat_pow_big", 71_856_587), ("IxVMPrim.nat_beq_lit", 24_108_404), ("IxVMPrim.nat_ble_lit", 22_469_243), ("IxVMPrim.nat_dec_le", 198_104_580), ("IxVMPrim.nat_dec_lt", 202_076_479), ("IxVMPrim.nat_dec_eq", 82_352_518), ("IxVMPrim.str_size_lit", 733_902_817), - ("IxVMPrim.bv_to_nat_lit", 577_368_692), + ("IxVMPrim.bv_to_nat_lit", 577_322_203), -- Mutual block + multi-member recursors ("IxVMInd.Even", 25_965_406), ("IxVMInd.Odd", 25_728_543),