Skip to content

aiur: correct memory circuit width in statistics (size + 7) #501

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
arthurpaulino wants to merge 1 commit into
base: main
Choose a base branch
from
+64 −60
Open

aiur: correct memory circuit width in statistics (size + 7) #501

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Ix/Aiur/Goldilocks.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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⟩
Expand Down
4 changes: 1 addition & 3 deletions Ix/Aiur/Stages/Bytecode.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 5 additions & 1 deletion Ix/Aiur/Statistics.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
112 changes: 56 additions & 56 deletions Tests/Ix/IxVM.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,78 +143,78 @@ 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
-- (`List.rec`) — hence the identical pin on all four evaporated entries,
-- 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 :=
Expand Down
Loading