Skip to content

Commit 07712ff

Browse files
arthurpaulinoarthurpaulino
committed
Tests: re-pin IxVM FFT costs after Tier 1d + Nat-layer optimizations
Updates 41 pinned FFT costs in `Tests/Ix/IxVM.lean::kernelCheckEntries` to match the new kernel's output. All pins moved DOWN — every constant got cheaper, none regressed. Largest reductions (% change): Vector.append: 4_023_268_168 → 3_160_970_390 (-21.4%) Array.append_assoc: 3_938_574_533 → 3_079_334_815 (-21.8%) String.Internal.append: 793_580_333 → 775_968_134 ( -2.2%) bv_to_nat_lit: 635_780_327 → 619_870_154 ( -2.5%) nat_gcd_lit: 665_518_356 → 649_859_784 ( -2.4%) Nat.sub_le_of_le_add: 567_575_653 → 557_867_526 ( -1.7%) IxVMPrim.nat_mod_lit: 414_695_549 → 407_517_834 ( -1.7%) IxVMPrim.nat_div_lit: 405_607_545 → 398_641_590 ( -1.7%) IxVMPrim.nat_shr_lit: 411_128_901 → 404_158_486 ( -1.7%) Nat.decLe: 209_641_496 → 206_196_563 ( -1.6%) Nat.add_comm: 56_084_908 → 55_504_714 ( -1.0%) `lake test -- --ignored ixvm` passes with 0 FFT mismatches.
1 parent ae242e9 commit 07712ff

1 file changed

Lines changed: 41 additions & 41 deletions

File tree

‎Tests/Ix/IxVM.lean‎

Lines changed: 41 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -115,52 +115,52 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) :
115115
observed cost in the message so it can be pasted back. -/
116116
private def kernelCheckEntries : List (String × Nat) := [
117117
-- Stdlib
118-
("HEq", 1_716_582),
119-
("HEq.rec", 2_692_988),
120-
("Eq.rec", 2_575_400),
121-
("Nat", 1_857_523),
122-
("Nat.add", 13_343_000),
123-
("Nat.add_comm", 56_084_908),
124-
("Nat.decEq", 71_921_625),
125-
("Nat.decLe", 209_641_496),
126-
("Nat.sub_le_of_le_add", 567_575_653),
118+
("HEq", 1_716_231),
119+
("HEq.rec", 2_689_147),
120+
("Eq.rec", 2_573_006),
121+
("Nat", 1_857_475),
122+
("Nat.add", 13_174_565),
123+
("Nat.add_comm", 55_504_714),
124+
("Nat.decEq", 70_617_453),
125+
("Nat.decLe", 206_196_563),
126+
("Nat.sub_le_of_le_add", 557_867_526),
127127
-- Newly-unlocked targets (level_leq Géran normalize).
128-
("Trans.mk", 2_911_629),
129-
("Array.append_assoc", 3_938_574_533),
130-
("Vector.append", 4_023_268_168),
128+
("Trans.mk", 2_902_315),
129+
("Array.append_assoc", 3_079_334_815),
130+
("Vector.append", 3_160_970_390),
131131
-- Primitive reduction theorems (`IxVMPrim`)
132-
("IxVMPrim.nat_add_lit", 28_639_807),
133-
("IxVMPrim.nat_sub_lit", 34_436_244),
134-
("IxVMPrim.nat_mul_lit", 25_101_067),
135-
("IxVMPrim.nat_mul_big", 24_580_879),
136-
("IxVMPrim.nat_div_lit", 405_607_545),
137-
("IxVMPrim.nat_mod_lit", 414_695_549),
138-
("IxVMPrim.nat_succ_lit", 7_330_826),
139-
("IxVMPrim.nat_pred_lit", 14_804_098),
140-
("IxVMPrim.nat_gcd_lit", 665_518_356),
141-
("IxVMPrim.nat_land_lit", 1_138_665_214),
142-
("IxVMPrim.nat_lor_lit", 1_139_887_801),
143-
("IxVMPrim.nat_xor_lit", 1_149_371_965),
144-
("IxVMPrim.nat_shl_lit", 35_417_490),
145-
("IxVMPrim.nat_shr_lit", 411_128_901),
146-
("IxVMPrim.nat_beq_lit", 24_752_029),
147-
("IxVMPrim.nat_ble_lit", 23_016_526),
148-
("IxVMPrim.nat_dec_le", 216_661_883),
149-
("IxVMPrim.nat_dec_lt", 220_751_034),
150-
("IxVMPrim.nat_dec_eq", 86_118_842),
151-
("IxVMPrim.str_size_lit", 802_563_877),
152-
("IxVMPrim.bv_to_nat_lit", 635_780_327),
132+
("IxVMPrim.nat_add_lit", 28_456_739),
133+
("IxVMPrim.nat_sub_lit", 34_198_852),
134+
("IxVMPrim.nat_mul_lit", 24_891_009),
135+
("IxVMPrim.nat_mul_big", 24_371_642),
136+
("IxVMPrim.nat_div_lit", 398_641_590),
137+
("IxVMPrim.nat_mod_lit", 407_517_834),
138+
("IxVMPrim.nat_succ_lit", 7_328_956),
139+
("IxVMPrim.nat_pred_lit", 14_758_385),
140+
("IxVMPrim.nat_gcd_lit", 649_859_784),
141+
("IxVMPrim.nat_land_lit", 1_116_700_968),
142+
("IxVMPrim.nat_lor_lit", 1_117_922_443),
143+
("IxVMPrim.nat_xor_lit", 1_127_404_404),
144+
("IxVMPrim.nat_shl_lit", 35_193_480),
145+
("IxVMPrim.nat_shr_lit", 404_158_486),
146+
("IxVMPrim.nat_beq_lit", 24_527_554),
147+
("IxVMPrim.nat_ble_lit", 22_813_110),
148+
("IxVMPrim.nat_dec_le", 213_176_101),
149+
("IxVMPrim.nat_dec_lt", 217_273_299),
150+
("IxVMPrim.nat_dec_eq", 84_744_092),
151+
("IxVMPrim.str_size_lit", 784_847_922),
152+
("IxVMPrim.bv_to_nat_lit", 619_870_154),
153153
-- Mutual block + multi-member recursors
154-
("IxVMInd.Even", 26_482_492),
155-
("IxVMInd.Odd", 26_245_849),
156-
("IxVMInd.Even.rec", 32_164_273),
157-
("IxVMInd.Odd.rec", 32_163_380),
154+
("IxVMInd.Even", 26_296_709),
155+
("IxVMInd.Odd", 26_060_068),
156+
("IxVMInd.Even.rec", 31_974_039),
157+
("IxVMInd.Odd.rec", 31_973_146),
158158
-- Nested inductive + aux recursor (Tree.mk : List Tree → Tree)
159-
("IxVMInd.Tree", 2_633_415),
160-
("IxVMInd.Tree.rec", 4_858_321),
159+
("IxVMInd.Tree", 2_632_931),
160+
("IxVMInd.Tree.rec", 4_855_972),
161161
-- Edge cases from prelude
162-
("String.Internal.append", 793_580_333),
163-
("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_197_925_029),
162+
("String.Internal.append", 775_968_134),
163+
("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_173_017_464),
164164
]
165165

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

0 commit comments

Comments
 (0)