Skip to content

Commit 65ff3f5

Browse files
arthurpaulinoarthurpaulino
committed
Tests: re-pin IxVM FFT costs
Re-pin after a25e94e (unconstrained_big_uint_div_mod op), 1141f2d (k_infer App-spine fusion), 1c148db (list_lookup via list_drop), and 345999a (klimbs_to_ctor_form single-step). Lake test ixvm suite green.
1 parent 345999a commit 65ff3f5

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_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),
118+
("HEq", 1_715_513),
119+
("HEq.rec", 2_681_137),
120+
("Eq.rec", 2_575_090),
121+
("Nat", 1_857_572),
122+
("Nat.add", 12_973_039),
123+
("Nat.add_comm", 54_350_110),
124+
("Nat.decEq", 68_538_632),
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).
128-
("Trans.mk", 2_902_315),
129-
("Array.append_assoc", 3_079_334_815),
130-
("Vector.append", 3_160_970_390),
128+
("Trans.mk", 2_863_374),
129+
("Array.append_assoc", 2_588_157_538),
130+
("Vector.append", 2_661_244_845),
131131
-- Primitive reduction theorems (`IxVMPrim`)
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),
132+
("IxVMPrim.nat_add_lit", 28_083_713),
133+
("IxVMPrim.nat_sub_lit", 33_755_207),
134+
("IxVMPrim.nat_mul_lit", 24_642_249),
135+
("IxVMPrim.nat_mul_big", 24_116_975),
136+
("IxVMPrim.nat_div_lit", 367_262_842),
137+
("IxVMPrim.nat_mod_lit", 375_958_840),
138+
("IxVMPrim.nat_succ_lit", 7_307_039),
139+
("IxVMPrim.nat_pred_lit", 14_682_236),
140+
("IxVMPrim.nat_gcd_lit", 605_514_332),
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),
144+
("IxVMPrim.nat_shl_lit", 34_843_370),
145+
("IxVMPrim.nat_shr_lit", 372_727_841),
146+
("IxVMPrim.nat_beq_lit", 24_108_404),
147+
("IxVMPrim.nat_ble_lit", 22_469_243),
148+
("IxVMPrim.nat_dec_le", 198_104_580),
149+
("IxVMPrim.nat_dec_lt", 202_076_479),
150+
("IxVMPrim.nat_dec_eq", 82_352_518),
151+
("IxVMPrim.str_size_lit", 733_902_817),
152+
("IxVMPrim.bv_to_nat_lit", 577_368_692),
153153
-- Mutual block + multi-member recursors
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),
154+
("IxVMInd.Even", 25_965_406),
155+
("IxVMInd.Odd", 25_728_543),
156+
("IxVMInd.Even.rec", 31_629_158),
157+
("IxVMInd.Odd.rec", 31_628_265),
158158
-- Nested inductive + aux recursor (Tree.mk : List Tree → Tree)
159-
("IxVMInd.Tree", 2_632_931),
160-
("IxVMInd.Tree.rec", 4_855_972),
159+
("IxVMInd.Tree", 2_634_462),
160+
("IxVMInd.Tree.rec", 4_870_642),
161161
-- Edge cases from prelude
162-
("String.Internal.append", 775_968_134),
163-
("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_173_017_464),
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 :=

0 commit comments

Comments
 (0)