From 480d199a442520a6f7dea46cadcaba5c597f302e Mon Sep 17 00:00:00 2001 From: Arthur Paulino Date: Mon, 13 Jul 2026 13:58:49 +0000 Subject: [PATCH] aiur: correct memory circuit width in statistics Mirrors crates/aiur/src/memory.rs (`Memory::width`): multiplicity + selector + pointer + size value columns, plus the single lookup's `G.extensionDegree * (1 + 1)` stage-2 columns as in `FunctionLayout.totalWidth`. The old size + 11 over-counted every memory circuit by 4. `G.extensionDegree` moves to Goldilocks.lean. Re-pin all 56 kernel-check FFT costs from a full `lake test -- --ignored ixvm` run (all green); every pin drops since the reported memory-circuit cost deflates. Actual proving cost is unchanged. --- Ix/Aiur/Goldilocks.lean | 2 + Ix/Aiur/Stages/Bytecode.lean | 4 +- Ix/Aiur/Statistics.lean | 6 +- Tests/Ix/IxVM.lean | 112 +++++++++++++++++------------------ 4 files changed, 64 insertions(+), 60 deletions(-) diff --git a/Ix/Aiur/Goldilocks.lean b/Ix/Aiur/Goldilocks.lean index 8b431ad8..a1e00a5f 100644 --- a/Ix/Aiur/Goldilocks.lean +++ b/Ix/Aiur/Goldilocks.lean @@ -7,6 +7,8 @@ namespace Aiur abbrev gSize : UInt64 := 1 - 2 ^ 32 abbrev G := { u : UInt64 // u < gSize } +abbrev G.extensionDegree : Nat := 2 + def G.ofNat (n : Nat) : G := let n := n.toUInt64 if h : n < gSize then ⟨n, h⟩ diff --git a/Ix/Aiur/Stages/Bytecode.lean b/Ix/Aiur/Stages/Bytecode.lean index 8950db99..9de3ffe3 100644 --- a/Ix/Aiur/Stages/Bytecode.lean +++ b/Ix/Aiur/Stages/Bytecode.lean @@ -88,10 +88,8 @@ structure FunctionLayout where def FunctionLayout.width (l : FunctionLayout) : Nat := l.inputSize + l.selectors + l.auxiliaries -abbrev goldilocksExtensionDegree : Nat := 2 - def FunctionLayout.totalWidth (l : FunctionLayout) : Nat := - l.width + goldilocksExtensionDegree * (1 + l.lookups) + l.width + G.extensionDegree * (1 + l.lookups) structure Function where body : Block diff --git a/Ix/Aiur/Statistics.lean b/Ix/Aiur/Statistics.lean index ddcf082b..90800f6a 100644 --- a/Ix/Aiur/Statistics.lean +++ b/Ix/Aiur/Statistics.lean @@ -58,7 +58,11 @@ def computeStats (compiled : CompiledToplevel) (queryCounts : Array QueryCount) acc := acc.push { name, width := w, height := h, cacheHits := hits, fftCost := fftCost w h : CircuitStats } acc let memoryCircuits := t.memorySizes.mapIdx fun i size => - let w := size + 11 + -- Mirrors `crates/aiur/src/memory.rs` (`Memory::width`): multiplicity + + -- selector + pointer + `size` value columns; the single lookup adds + -- `G.extensionDegree * (1 + 1)` stage-2 columns, as in + -- `FunctionLayout.totalWidth`. + let w := 3 + size + G.extensionDegree * (1 + 1) let qc := queryCounts[nAllFuns + i]! let h := qc.uniqueRows let hits := qc.totalHits - qc.uniqueRows diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index 0594adeb..64a2f3c0 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -143,62 +143,62 @@ public def kernelCheck (name : Lean.Name) (env : Lean.Environment) : observed cost in the message so it can be pasted back. -/ private def kernelCheckEntries : List (String × Nat) := [ -- Stdlib - ("HEq", 1_707_330), - ("HEq.rec", 2_674_401), - ("Eq.rec", 2_568_796), - ("Nat", 1_848_963), - ("Nat.add", 12_862_667), - ("Nat.add_comm", 53_748_034), - ("Nat.decEq", 67_465_767), - ("Nat.decLe", 188_267_204), - ("Nat.sub_le_of_le_add", 509_275_238), + ("HEq", 1_572_665), + ("HEq.rec", 2_513_705), + ("Eq.rec", 2_411_743), + ("Nat", 1_713_632), + ("Nat.add", 12_452_644), + ("Nat.add_comm", 52_433_121), + ("Nat.decEq", 65_867_624), + ("Nat.decLe", 184_262_009), + ("Nat.sub_le_of_le_add", 498_805_880), -- Newly-unlocked targets (level_leq Géran normalize). - ("Trans.mk", 2_837_043), - ("Array.append_assoc", 2_516_757_878), - ("Vector.append", 2_584_871_352), + ("Trans.mk", 2_675_624), + ("Array.append_assoc", 2_470_936_809), + ("Vector.append", 2_537_672_911), -- Primitive reduction theorems (`IxVMPrim`) - ("IxVMPrim.nat_add_lit", 27_531_135), - ("IxVMPrim.nat_sub_lit", 33_267_046), - ("IxVMPrim.nat_mul_lit", 24_330_411), - ("IxVMPrim.nat_mul_big", 23_774_792), - ("IxVMPrim.nat_div_lit", 362_408_942), - ("IxVMPrim.nat_mod_lit", 370_619_545), - ("IxVMPrim.nat_succ_lit", 7_194_844), - ("IxVMPrim.nat_pred_lit", 14_467_396), - ("IxVMPrim.nat_gcd_lit", 596_843_893), - ("IxVMPrim.nat_land_lit", 1_004_836_787), - ("IxVMPrim.nat_lor_lit", 1_005_550_176), - ("IxVMPrim.nat_xor_lit", 1_013_521_624), - ("IxVMPrim.nat_shl_lit", 34_288_792), - ("IxVMPrim.nat_shr_lit", 367_333_879), - ("IxVMPrim.nat_pow_big", 71_103_729), - ("IxVMPrim.nat_beq_lit", 23_785_738), - ("IxVMPrim.nat_ble_lit", 22_079_774), - ("IxVMPrim.nat_dec_le", 194_603_173), - ("IxVMPrim.nat_dec_lt", 198_521_364), - ("IxVMPrim.nat_dec_eq", 80_906_449), - ("IxVMPrim.str_size_lit", 709_617_199), - ("IxVMPrim.bv_to_nat_lit", 568_367_655), + ("IxVMPrim.nat_add_lit", 26_814_053), + ("IxVMPrim.nat_sub_lit", 32_412_442), + ("IxVMPrim.nat_mul_lit", 23_666_696), + ("IxVMPrim.nat_mul_big", 23_122_538), + ("IxVMPrim.nat_div_lit", 354_910_499), + ("IxVMPrim.nat_mod_lit", 362_947_228), + ("IxVMPrim.nat_succ_lit", 6_926_628), + ("IxVMPrim.nat_pred_lit", 14_034_229), + ("IxVMPrim.nat_gcd_lit", 584_563_967), + ("IxVMPrim.nat_land_lit", 984_261_593), + ("IxVMPrim.nat_lor_lit", 984_965_002), + ("IxVMPrim.nat_xor_lit", 992_808_202), + ("IxVMPrim.nat_shl_lit", 33_405_700), + ("IxVMPrim.nat_shr_lit", 359_726_163), + ("IxVMPrim.nat_pow_big", 69_814_320), + ("IxVMPrim.nat_beq_lit", 23_148_690), + ("IxVMPrim.nat_ble_lit", 21_477_337), + ("IxVMPrim.nat_dec_le", 190_477_852), + ("IxVMPrim.nat_dec_lt", 194_312_399), + ("IxVMPrim.nat_dec_eq", 79_028_929), + ("IxVMPrim.str_size_lit", 695_223_900), + ("IxVMPrim.bv_to_nat_lit", 556_768_718), -- Mutual block + multi-member recursors - ("IxVMInd.Even", 25_516_962), - ("IxVMInd.Odd", 25_269_345), - ("IxVMInd.Even.rec", 31_116_602), - ("IxVMInd.Odd.rec", 31_114_086), + ("IxVMInd.Even", 24_844_615), + ("IxVMInd.Odd", 24_601_448), + ("IxVMInd.Even.rec", 30_317_596), + ("IxVMInd.Odd.rec", 30_314_820), -- Nested inductive + aux recursor (Tree.mk : List Tree → Tree) - ("IxVMInd.Tree", 2_607_720), - ("IxVMInd.Tree.rec", 4_849_613), + ("IxVMInd.Tree", 2_452_264), + ("IxVMInd.Tree.rec", 4_636_084), -- Aux dedup: distinct spec_params on one external inductive (3 motives). - ("IxVMInd.DedupM", 4_721_332), - ("IxVMInd.DedupM.rec", 7_890_218), + ("IxVMInd.DedupM", 4_522_010), + ("IxVMInd.DedupM.rec", 7_613_209), -- Aux dedup de-lift guard: equal spec_params at field depths 0 and 2. - ("IxVMInd.DepthM", 3_555_297), - ("IxVMInd.DepthM.rec", 6_263_860), + ("IxVMInd.DepthM", 3_380_600), + ("IxVMInd.DepthM.rec", 6_022_611), -- Edge cases from prelude - ("String.Internal.append", 701_785_005), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_054_962_285), + ("String.Internal.append", 687_579_884), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 1_033_641_289), -- Aux recursor with transitively-nested inductives (Syntax → Array Syntax -- → List Syntax); shard 53 regression driver. - ("Lean.Syntax.rec", 727_050_101), + ("Lean.Syntax.rec", 712_428_223), -- Evaporated-aux canonicalization (Tests/Ix/Compile/Mutual.lean AuxDedup*): -- SCC splitting strands `rec_N` auxes whose spec-param inductives moved to -- other SCCs; their claims alias the external inductive's recursor @@ -206,15 +206,15 @@ private def kernelCheckEntries : List (String × Nat) := [ -- whose claims are literally the same `List.rec` closure. AuxDedupMixed -- mixes one genuine canonical aux (`M.rec_1`, over `List M`) with one -- evaporated alias (`M.rec_2`, over `List B`). - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 3_498_075), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 4_390_037), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 3_087_145), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 3_087_145), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 3_087_145), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 3_531_908), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 6_150_929), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 6_152_908), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 3_087_145), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 3_322_301), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 4_189_674), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 2_916_533), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 2_916_533), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 2_916_533), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 3_356_051), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 5_908_162), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 5_910_162), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 2_916_533), ] private def nameOfString (str : String) : Lean.Name :=