From df4c275b3c91c6f46d3bcd773b81bee9a265b824 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Fri, 31 Jul 2026 15:56:41 -0300 Subject: [PATCH 1/4] aiur: circuit-level function grouping (no source pragma) Several functions can now be proven by ONE circuit: the members are walked like branches of a single function - auxiliary columns and lookup slots are shared across members (the same save/restore sharing match arms already use), selector columns are laid out consecutively per member, and every member folds its selector-gated return message (carrying its own function index) into the shared lookup slot 0 against a single shared multiplicity column. One extra constraint enforces cross-member exclusivity: the sum of the members' top-block selectors must be boolean. Callers are untouched - calls still target function indices on the function channel - so grouping is invisible to execution, the query record, and the interpreter. Grouping is a CIRCUIT-level choice, not a property of the function library, so there is no source annotation: Source.Toplevel.compile builds the default singleton partition (Bytecode.Toplevel.circuits, one circuit per constrained function - behavior-identical to before), and CompiledToplevel.groupFunctions optionally regroups it by function NAME (validated: known, constrained, non-entry, no duplicates). The merged layout is max inputs, summed selectors, max auxiliaries, max lookups - so grouping fits rarely-called functions of similar shape: each (rare) row pays the group's selector count while the system sheds one circuit (vk entry, commitment matrix, verifier work) per absorbed member. Rust consumes the partition directly (bytecode Circuit via FFI; constraints/trace/synthesis iterate circuits, witness rows concatenate the members' queried rows in member order). The stage-2 lookup group size and the branchless raw-argument rule now key on the CIRCUIT layout: multi-member circuits are branching by construction, so their arguments are selector-superposed exactly like match arms. Tests: the aiur suite proves the same toplevel twice - ungrouped and with a 3-member test group (different arities, matches, cross-member call, recursion) - plus structural checks on the partition (members, merge-rule layout, every constrained function in exactly one circuit). All suites pass unchanged (ixvm FFT pins identical - the default partition is behavior-neutral); codegen is unaffected (execution ignores the partition). --- Ix/Aiur/Compiler.lean | 81 ++++++++++++++++++++++++++- Ix/Aiur/Compiler/Lower.lean | 2 +- Ix/Aiur/Stages/Bytecode.lean | 24 ++++++++ Ix/Aiur/Statistics.lean | 41 ++++++-------- Tests/Aiur/Aiur.lean | 79 ++++++++++++++++++++++++++ Tests/Aiur/Common.lean | 5 +- Tests/Main.lean | 12 +++- crates/aiur/src/bytecode.rs | 17 ++++++ crates/aiur/src/constraints.rs | 98 +++++++++++++++++++++------------ crates/aiur/src/synthesis.rs | 47 ++++++++++------ crates/aiur/src/trace.rs | 84 +++++++++++++++++++++------- crates/ffi/src/aiur/toplevel.rs | 18 +++++- crates/ffi/src/lean.rs | 3 +- 13 files changed, 406 insertions(+), 105 deletions(-) diff --git a/Ix/Aiur/Compiler.lean b/Ix/Aiur/Compiler.lean index cef51cdae..e8e8ccfae 100644 --- a/Ix/Aiur/Compiler.lean +++ b/Ix/Aiur/Compiler.lean @@ -42,6 +42,68 @@ def CompiledToplevel.getFuncIdx (ct : CompiledToplevel) (name : Lean.Name) : Option Bytecode.FunIdx := ct.nameMap[Global.mk name]? +/-- Regroup the circuit partition: each `(name, members)` in `groups` becomes +ONE circuit proving all the listed functions (branching on the member; see +`Bytecode.Circuit`), positioned where its first member's singleton circuit +was; every other constrained function keeps its singleton circuit. Grouping +is a circuit-level choice — the function "library", its bytecode, execution, +and the query record are untouched, and callers still target function +indices on the function channel. + +Grouping is favorable for RARELY-CALLED functions of similar shape: the +merged circuit sums the members' selector columns but takes the max of their +auxiliary columns, so each (rare) row pays the group's selector count, while +the system sheds one circuit (vk entry, commitment matrix, verifier work) +per absorbed member. + +Errors if a name is unknown, unconstrained (it has no circuit to group), an +entry function, listed twice, or if a group is empty. -/ +def CompiledToplevel.groupFunctions (ct : CompiledToplevel) + (groups : Array (String × Array Lean.Name)) : + Except String CompiledToplevel := do + let t := ct.bytecode + -- Resolve and validate the groups into member-index arrays. + let mut grouped : Std.HashMap Bytecode.FunIdx Nat := {} + let mut resolved : Array (String × Array Bytecode.FunIdx) := #[] + for (gname, names) in groups do + if names.isEmpty then + throw s!"group {gname} is empty" + let mut members := #[] + for name in names do + let some i := ct.getFuncIdx name + | throw s!"group {gname}: unknown function {name}" + let f := t.functions[i]! + unless f.constrained do + throw s!"group {gname}: {name} is unconstrained (it has no circuit)" + if f.entry then + throw s!"group {gname}: {name} is an entry function" + if grouped.contains i then + throw s!"group {gname}: {name} is already grouped" + grouped := grouped.insert i resolved.size + members := members.push i + resolved := resolved.push (gname, members) + -- Rebuild the partition in first-occurrence order over the existing + -- (singleton-ordered) circuits. + let mut circuits : Array Bytecode.Circuit := #[] + let mut placed : Array Bool := .replicate resolved.size false + for c in t.circuits do + let members := c.members + if h : members.size = 1 then + let i := members[0] + match grouped[i]? with + | none => circuits := circuits.push c + | some g => + unless placed[g]! do + placed := placed.set! g true + let (gname, ms) := resolved[g]! + let layout := ms.foldl (init := t.functions[ms[0]!]!.layout) + fun acc m => if m == ms[0]! then acc + else acc.merge t.functions[m]!.layout + circuits := circuits.push { name := gname, members := ms, layout } + else + throw "groupFunctions: partition already grouped; group from a freshly compiled toplevel" + pure { ct with bytecode := { t with circuits } } + /-- Termination helper for the `Block`/`Ctrl` traversal below. -/ private theorem Bytecode.Block.sizeOf_ctrl_lt'' (b : Bytecode.Block) : sizeOf b.ctrl < sizeOf b := by @@ -90,6 +152,18 @@ decreasing_by | (apply Prod.Lex.left; exact Bytecode.Block.sizeOf_ctrl_lt'' _) end +/-- The default circuit partition: one singleton circuit per constrained +function, in function-index order, named by `nameOf`. -/ +def Bytecode.Toplevel.singletonCircuits (t : Bytecode.Toplevel) + (nameOf : Bytecode.FunIdx → String) : Array Bytecode.Circuit := Id.run do + let mut circuits : Array Bytecode.Circuit := #[] + for h : i in [:t.functions.size] do + let f := t.functions[i] + if f.constrained then + circuits := circuits.push + { name := nameOf i, members := #[i], layout := f.layout } + pure circuits + /-- Compute which functions need a circuit. A function needs a circuit iff it is reachable from an entry point through a chain of constrained call edges. -/ def Bytecode.Toplevel.needsCircuit (t : Bytecode.Toplevel) : Array Bool := Id.run do @@ -118,11 +192,16 @@ def Source.Toplevel.compile (t : Source.Toplevel) : Except String CompiledToplev let (bytecodeRaw, preNameMap) ← concDecls.toBytecode let (bytecodeDedup, remap) := bytecodeRaw.deduplicate let needs := bytecodeDedup.needsCircuit - let bytecode := { bytecodeDedup with + let bytecode : Bytecode.Toplevel := { bytecodeDedup with functions := bytecodeDedup.functions.mapIdx fun i f => { f with constrained := needs[i]! } } let nameMap := preNameMap.fold (init := (∅ : Std.HashMap Global Bytecode.FunIdx)) fun acc name idx => acc.insert name (remap idx) + -- Singleton circuits are labeled with (one of) the function's source names. + let reverseMap := nameMap.fold (init := (∅ : Std.HashMap Bytecode.FunIdx String)) + fun acc global idx => if acc.contains idx then acc else acc.insert idx (toString global) + let bytecode := { bytecode with + circuits := bytecode.singletonCircuits fun i => reverseMap[i]?.getD s!"" } pure (CompiledToplevel.mk t bytecode nameMap) /-- Progress helper: given success of the three `Except`-returning stages, diff --git a/Ix/Aiur/Compiler/Lower.lean b/Ix/Aiur/Compiler/Lower.lean index c125514ea..039eb7dcc 100644 --- a/Ix/Aiur/Compiler/Lower.lean +++ b/Ix/Aiur/Compiler/Lower.lean @@ -633,7 +633,7 @@ def Concrete.Decls.toBytecode (decls : Concrete.Decls) : let memSizes := layoutMState.memSizes.foldl (·.insert ·) memSizes pure (functions.push function, memSizes, nameMap) | _ => pure acc - pure (⟨functions, memSizes.toArray⟩, nameMap) + pure (⟨functions, memSizes.toArray, #[]⟩, nameMap) end Aiur diff --git a/Ix/Aiur/Stages/Bytecode.lean b/Ix/Aiur/Stages/Bytecode.lean index acd8e2579..21c52fd66 100644 --- a/Ix/Aiur/Stages/Bytecode.lean +++ b/Ix/Aiur/Stages/Bytecode.lean @@ -122,9 +122,33 @@ structure Function where constrained : Bool deriving Inhabited, Repr +/-- A circuit of the proving system, backing one or more functions. By +default every constrained function gets a singleton circuit named after it; +`CompiledToplevel.groupFunctions` can regroup several functions into one +circuit whose branching selects the member function. `layout` is the merged +layout: max `inputSize`, sum of `selectors`, max `auxiliaries` (which +includes the single shared multiplicity column), max `lookups` (slot 0 is +the shared return lookup). -/ +structure Circuit where + name : String + members : Array FunIdx + layout : FunctionLayout + deriving Inhabited, Repr + +/-- Merged layout of a group of functions (see `Circuit`). -/ +def FunctionLayout.merge (a b : FunctionLayout) : FunctionLayout where + inputSize := a.inputSize.max b.inputSize + selectors := a.selectors + b.selectors + auxiliaries := a.auxiliaries.max b.auxiliaries + lookups := a.lookups.max b.lookups + structure Toplevel where functions : Array Function memorySizes : Array Nat + /-- Circuit partition of the constrained functions, in first-occurrence + order. Built by `Source.Toplevel.compile` (singletons by default; see + `CompiledToplevel.groupFunctions`); empty on a freshly lowered toplevel. -/ + circuits : Array Circuit := #[] deriving Repr end Bytecode diff --git a/Ix/Aiur/Statistics.lean b/Ix/Aiur/Statistics.lean index aa91de166..095a1d2d8 100644 --- a/Ix/Aiur/Statistics.lean +++ b/Ix/Aiur/Statistics.lean @@ -81,44 +81,37 @@ def computeStats (compiled : CompiledToplevel) (queryCounts : Array QueryCount) (logBlowup : Nat := defaultCommitmentParameters.logBlowup) : ExecutionStats := let t := compiled.bytecode - -- Invert nameMap to get FunIdx → String - let reverseMap := compiled.nameMap.fold (init := (∅ : Std.HashMap Bytecode.FunIdx String)) - fun acc global idx => if !acc.contains idx then acc.insert idx (toString global) else acc let nAllFuns := t.functions.size - let nConstrained := t.functions.foldl (fun n f => if f.constrained then n + 1 else n) 0 - -- Shapes arrive in canonical system order: constrained functions - -- (ascending index), memories, `Bytes1`, `Bytes2`. A mismatch means the - -- shapes were built from a different toplevel; misindexing would silently - -- attribute costs to the wrong circuits. - if shapes.size != nConstrained + t.memorySizes.size + 2 then + -- Shapes arrive in canonical system order: function circuits (grouped; + -- singletons for ungrouped functions, in ascending member index), + -- memories, `Bytes1`, `Bytes2`. A mismatch means the shapes were built + -- from a different toplevel; misindexing would silently attribute costs + -- to the wrong circuits. + if shapes.size != t.circuits.size + t.memorySizes.size + 2 then panic! s!"computeStats: {shapes.size} circuit shapes for \ - {nConstrained} constrained functions + {t.memorySizes.size} memories + 2 gadgets" + {t.circuits.size} function circuits + {t.memorySizes.size} memories + 2 gadgets" else let mkStats (name : String) (shape : CircuitShape) (h hits : Nat) : CircuitStats := { name, width := shape.committedWidth, height := h, cacheHits := hits, fftCost := fftCost shape h logBlowup, uncachedFftCost := fftCost shape (h + hits) logBlowup } - let functionCircuits := Id.run do - let mut acc := #[] - let mut shapeIdx := 0 - for i in [:nAllFuns] do - if t.functions[i]!.constrained then - let shape := shapes[shapeIdx]! - shapeIdx := shapeIdx + 1 - let qc := queryCounts[i]! - let name := reverseMap[i]?.getD s!"" - acc := acc.push - (mkStats name shape qc.uniqueRows (qc.totalHits - qc.uniqueRows)) - acc + -- One row per function circuit: heights and cache hits are summed over + -- the circuit's member functions (singletons sum over one). + let functionCircuits := t.circuits.mapIdx fun cIdx c => + let shape := shapes[cIdx]! + let (h, hits) := c.members.foldl (init := (0, 0)) fun (h, hits) i => + let qc := queryCounts[i]! + (h + qc.uniqueRows, hits + (qc.totalHits - qc.uniqueRows)) + mkStats c.name shape h hits let memoryCircuits := t.memorySizes.mapIdx fun i size => - let shape := shapes[nConstrained + i]! + let shape := shapes[t.circuits.size + i]! let qc := queryCounts[nAllFuns + i]! mkStats s!"memory[{size}]" shape qc.uniqueRows (qc.totalHits - qc.uniqueRows) -- The byte gadgets commit full-table traces in every proof: their height -- is the (fixed) preprocessed height, independent of the query set, so -- they carry no cache-hit counterfactual. let gadgetCircuits := #["Bytes1", "Bytes2"].mapIdx fun i name => - let shape := shapes[nConstrained + t.memorySizes.size + i]! + let shape := shapes[t.circuits.size + t.memorySizes.size + i]! mkStats name shape shape.preprocessedHeight 0 let circuits := (functionCircuits ++ memoryCircuits ++ gadgetCircuits).qsort (·.fftCost > ·.fftCost) diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean index 833aa509d..0230ad1f1 100644 --- a/Tests/Aiur/Aiur.lean +++ b/Tests/Aiur/Aiur.lean @@ -738,6 +738,38 @@ def toplevel := ⟦ let s5 = c[4] + c[0]; -- 255 s1 + s2 + 10 * s3 + s4 + s5 -- 1309 } + + --------------------------------------------------------------------------- + -- Grouped circuits (`CompiledToplevel.groupFunctions`): the test runner + -- groups these three into one circuit whose branching selects the member. + -- Grouping is a circuit-level choice, so there is NO source annotation: + -- the same functions also run ungrouped in the plain suite. Members + -- differ in arity, output and branch count, call each other (through the + -- shared circuit) and recurse. + --------------------------------------------------------------------------- + fn grouped_double(x: G) -> G { + x + x + } + + -- Different arity, a match (two selectors), calls a fellow group member. + fn grouped_pick(t: G, a: G, b: G) -> G { + match t { + 0 => grouped_double(a), + _ => b, + } + } + + -- Recursive group member: self-calls route through the shared circuit. + fn grouped_sum_range(n: G) -> G { + match n { + 0 => 0, + _ => n + grouped_sum_range(n - 1), + } + } + + pub fn calls_grouped(t: G, a: G, b: G) -> G { + grouped_pick(t, a, b) + grouped_sum_range(a) + } ⟧ /-- The PROVING suite: every case runs the full prove+verify pipeline @@ -866,6 +898,53 @@ def aiurTestCases : List AiurTestCase := [ -- Unconstrained g_to_bytes / g_inverse hints: all cases in one proof .prove `hint_test #[] #[1309], + + -- Grouped-circuit member functions, run UNGROUPED here (the grouped + -- variant runs in the grouped env; see `testGroups`). + -- t=0 → grouped_double(5) + Σ1..5 = 10 + 15 = 25; t≠0 → 9 + Σ1..3 = 15. + .prove `calls_grouped #[0, 5, 9] #[25] + (label := "calls_grouped(0,5,9)"), + .prove `calls_grouped #[1, 3, 9] #[15] + (label := "calls_grouped(1,3,9)"), ] +/-- The grouping the `aiur` runner applies for the grouped environment. -/ +def testGroups : Array (String × Array Lean.Name) := + #[("test_group", #[`grouped_double, `grouped_pick, `grouped_sum_range])] + +def groupedTestCases : List AiurTestCase := [ + .prove `calls_grouped #[0, 5, 9] #[25] + (label := "calls_grouped(0,5,9) [grouped]"), + .prove `calls_grouped #[1, 3, 9] #[15] + (label := "calls_grouped(1,3,9) [grouped]"), +] + +/-- Structural checks on the grouped partition: the grouped circuit exists, +holds exactly its members, its layout follows the merge rule (max inputs, +summed selectors, max auxiliaries, max lookups), and every constrained +function lands in exactly one circuit. -/ +def groupingStructureChecks (compiled : Aiur.CompiledToplevel) : TestSeq := + let t := compiled.bytecode + let memberOf := fun (name : Lean.Name) => compiled.getFuncIdx name |>.get! + let expectedMembers := + #[`grouped_double, `grouped_pick, `grouped_sum_range].map memberOf + match t.circuits.find? (·.name == "test_group") with + | none => test "test_group circuit exists" false + | some c => + let layouts := c.members.map (t.functions[·]!.layout) + let expected := layouts.foldl (init := (⟨0, 0, 0, 0⟩ : Aiur.Bytecode.FunctionLayout)) + Aiur.Bytecode.FunctionLayout.merge + let allCircuitMembers := t.circuits.flatMap (·.members) + let constrained := (Array.range t.functions.size).filter + (t.functions[·]!.constrained) + test "test_group circuit exists" true ++ + test "test_group members" (c.members == expectedMembers) ++ + test "test_group layout follows the merge rule" + (c.layout.inputSize == expected.inputSize && + c.layout.selectors == expected.selectors && + c.layout.auxiliaries == expected.auxiliaries && + c.layout.lookups == expected.lookups) ++ + test "every constrained function is in exactly one circuit" + (allCircuitMembers.qsort (· < ·) == constrained) + end diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean index f16bbc739..89b8b2c2b 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -72,10 +72,13 @@ structure AiurTestEnv where aiurSystem : Aiur.AiurSystem shapes : Array Aiur.CircuitShape -def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) : +def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) + (groups : Array (String × Array Lean.Name) := #[]) : Except String AiurTestEnv := do let toplevel ← toplevelFn.mapError toString let compiled ← toplevel.compile + let compiled ← if groups.isEmpty then pure compiled + else compiled.groupFunctions groups let decls ← toplevel.mkDecls.mapError toString let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters return ⟨compiled, decls, aiurSystem, aiurSystem.circuitShapes⟩ diff --git a/Tests/Main.lean b/Tests/Main.lean index 94fc62a94..19cb2b078 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -166,7 +166,17 @@ def primaryRunners : List (String × IO UInt32) := [ IO.println "aiur-prove" match AiurTestEnv.build (pure toplevel) with | .error e => IO.eprintln s!"Aiur setup failed: {e}"; return 1 - | .ok env => LSpec.lspecEachIO aiurTestCases fun tc => pure (env.runTestCase tc)), + | .ok env => do + let r1 ← LSpec.lspecEachIO aiurTestCases fun tc => pure (env.runTestCase tc) + -- The same toplevel with `testGroups` applied: the members share one + -- circuit, and the whole suite of grouped cases proves through it. + match AiurTestEnv.build (pure toplevel) testGroups with + | .error e => IO.eprintln s!"Aiur grouped setup failed: {e}"; return 1 + | .ok genv => do + let r2 ← LSpec.lspecEachIO groupedTestCases fun tc => pure (genv.runTestCase tc) + let r3 ← LSpec.lspecIO + (.ofList [("aiur-grouping", [groupingStructureChecks genv.compiled])]) [] + return if r1 == 0 && r2 == 0 && r3 == 0 then 0 else 1), ("aiur-hashes", do IO.println "aiur-hashes" let .ok blake3Env := AiurTestEnv.build (do diff --git a/crates/aiur/src/bytecode.rs b/crates/aiur/src/bytecode.rs index 57e426e82..3349906ff 100644 --- a/crates/aiur/src/bytecode.rs +++ b/crates/aiur/src/bytecode.rs @@ -5,6 +5,23 @@ use super::G; pub struct Toplevel { pub functions: Vec, pub memory_sizes: Vec, + /// Circuit partition of the constrained functions, in first-occurrence + /// order. Computed by the Lean compiler (singletons by default; + /// `CompiledToplevel.groupFunctions` regroups); every constrained + /// function appears in exactly one circuit. + pub circuits: Vec, +} + +/// A circuit of the proving system, backing one or more functions. Ungrouped +/// functions get a singleton circuit; grouped functions share one circuit +/// whose branching selects the member function. +/// +/// `layout` is the merged layout: max `input_size`, sum of `selectors`, max +/// `auxiliaries` (which includes the single shared multiplicity column), max +/// `lookups` (slot 0 is the shared return lookup). +pub struct Circuit { + pub members: Vec, + pub layout: FunctionLayout, } pub struct Function { diff --git a/crates/aiur/src/constraints.rs b/crates/aiur/src/constraints.rs index 26488ce50..8691198b2 100644 --- a/crates/aiur/src/constraints.rs +++ b/crates/aiur/src/constraints.rs @@ -6,7 +6,7 @@ use std::{array, ops::Range, sync::LazyLock}; use crate::{ FxIndexMap, G, - bytecode::{Block, Ctrl, Function, FunctionLayout, Op, Toplevel, ValIdx}, + bytecode::{Block, Ctrl, Op, Toplevel, ValIdx}, function_channel, gadgets::{ AiurGadget, @@ -65,11 +65,18 @@ pub struct Constraints { } struct ConstraintState { + /// Index of the circuit member currently being walked. function_index: G, - /// Exactly one selector: the function has a single leaf block (no - /// matches), so every lookup slot is written by exactly one branch. + /// Exactly one selector: the circuit backs a single function with a + /// single leaf block (no matches), so every lookup slot is written by + /// exactly one branch. branchless: bool, - layout: FunctionLayout, + /// Input size of the current member (inputs live in columns + /// `0..input_size` for every member; the circuit reserves the max). + input_size: usize, + /// Column of the current member's first selector: the circuit's input + /// block plus the selector counts of the members walked before it. + sel_base: usize, column: usize, lookup: usize, lookups: Vec>, @@ -88,7 +95,7 @@ struct SharedState { impl ConstraintState { fn selector_index(&self, sel: usize) -> usize { - sel + self.layout.input_size + sel + self.sel_base } /// Selector-gate a lookup argument. Lookup slots shared across branches @@ -131,34 +138,75 @@ impl ConstraintState { } impl Toplevel { + /// Build the constraints of one circuit. The circuit's members are walked + /// like branches of a single function: each walk restarts the auxiliary + /// column / lookup-slot counters (so members share those, like match arms + /// do), while selector columns are laid out consecutively per member. All + /// members fold their return message into the shared lookup slot 0, gated + /// by their own selectors and carrying their own function index, against + /// the single shared multiplicity column. pub fn build_constraints( &self, - function_index: usize, + circuit_index: usize, ) -> (Constraints, Vec>) { - let function = &self.functions[function_index]; + let circuit = &self.circuits[circuit_index]; + let layout = circuit.layout; let constraints = Constraints { zeros: vec![], - selectors: 0..0, - width: function.layout.width(), + selectors: layout.input_size..layout.input_size + layout.selectors, + width: layout.width(), }; let mut state = ConstraintState { - function_index: G::from_usize(function_index), - branchless: function.layout.selectors == 1, - layout: function.layout, + function_index: G::ZERO, + branchless: layout.selectors == 1, + input_size: 0, + sel_base: 0, column: 0, lookup: 0, map: vec![], - lookups: vec![empty_lookup(); function.layout.lookups], + lookups: vec![empty_lookup(); layout.lookups], constraints, yield_info: vec![], }; - function.build_constraints(&mut state); + // The shared multiplicity column: first auxiliary, right after the + // selectors. The return lookup occupies the first lookup slot. + let multiplicity = var(layout.input_size + layout.selectors); + state.lookups[0].multiplicity = -multiplicity; + let aux_start = layout.input_size + layout.selectors + 1; + let mut sel_base = layout.input_size; + let mut circuit_sel = Expr::from(G::ZERO); + for &member in &circuit.members { + let function = &self.functions[member]; + state.function_index = G::from_usize(member); + state.input_size = function.layout.input_size; + state.sel_base = sel_base; + state.column = aux_start; + state.lookup = 1; + state.map.clear(); + (0..function.layout.input_size).for_each(|i| state.map.push((var(i), 1))); + let body_sel = function.body.get_block_selector(&state); + circuit_sel = circuit_sel + body_sel.clone(); + function.body.collect_constraints(body_sel, &mut state); + debug_assert!(state.yield_info.is_empty()); + sel_base += function.layout.selectors; + } // The old `Air::eval` asserted each selector column boolean; the new // system compiles a constraint vector, so materialize those explicitly. for sel in state.constraints.selectors.clone() { let s = var(sel); state.constraints.zeros.push(s.clone() * (s - konst(G::ONE))); } + // Cross-member exclusivity: the circuit-level selector (the sum of the + // members' top-block selectors) must be boolean, so at most one member + // is active per row and the shared return lookup emits a single + // member's message. A singleton circuit already gets this from its top + // block's own boolean constraint. + if circuit.members.len() > 1 { + state + .constraints + .zeros + .push(circuit_sel.clone() * (Expr::from(G::ONE) - circuit_sel)); + } (state.constraints, state.lookups) } } @@ -167,26 +215,6 @@ fn empty_lookup() -> Lookup { Lookup { multiplicity: konst(G::ZERO), args: vec![] } } -impl Function { - fn build_constraints(&self, state: &mut ConstraintState) { - // the first columns are occupied by the input, which is also mapped - state.column += self.layout.input_size; - (0..self.layout.input_size).for_each(|i| state.map.push((var(i), 1))); - // then comes the selectors, which are not mapped - let init_sel = state.column; - let final_sel = state.column + self.layout.selectors; - state.constraints.selectors = init_sel..final_sel; - state.column = final_sel; - // the multiplicity occupies another column - let multiplicity = var(state.column); - state.column += 1; - // the return lookup occupies the first lookup slot - state.lookups[0].multiplicity = -multiplicity.clone(); - state.lookup += 1; - self.body.collect_constraints(self.body.get_block_selector(state), state); - } -} - impl Block { fn collect_constraints(&self, sel: Expr, state: &mut ConstraintState) { // Boolean constraint for this block's selector @@ -277,7 +305,7 @@ impl Ctrl { ]; // input args.extend( - (0..state.layout.input_size) + (0..state.input_size) .map(|arg| state.gate(&sel, state.map[arg].0.clone())), ); // output diff --git a/crates/aiur/src/synthesis.rs b/crates/aiur/src/synthesis.rs index f0be342ba..ae7e2ac89 100644 --- a/crates/aiur/src/synthesis.rs +++ b/crates/aiur/src/synthesis.rs @@ -154,20 +154,17 @@ impl AiurSystem { }); }; - // Constrained functions (ascending index). - for i in 0..toplevel.functions.len() { - if !toplevel.functions[i].constrained { - continue; - } + // Function circuits, in partition order (singletons unless grouped). + for i in 0..toplevel.circuits.len() { let (constraints, lookups) = toplevel.build_constraints(i); - // A branchless function's lookup arguments are sent raw (degree 1; + // A branchless circuit's lookup arguments are sent raw (degree 1; // see `ConstraintState::gate`), so two lookups fit in one chained // accumulator step at degree 3 — within the degree the selector-gated - // constraints already pay for. Branching functions keep k = 1: their + // constraints already pay for. Branching circuits keep k = 1: their // superposed arguments are degree 2, and grouping would push the // logUp constraints past the quotient budget. let group_size = - if toplevel.functions[i].layout.selectors == 1 && lookups.len() >= 2 { + if toplevel.circuits[i].layout.selectors == 1 && lookups.len() >= 2 { 2 } else { 1 @@ -221,11 +218,8 @@ impl AiurSystem { /// order the circuits were chained in [`AiurSystem::build`], so index `i` /// of the returned `Vec` corresponds to `self.system.circuits[i]`. fn circuit_types(&self) -> Vec { - let functions = (0..self.toplevel.functions.len()).filter_map(|idx| { - self.toplevel.functions[idx] - .constrained - .then_some(CircuitType::Function { idx }) - }); + let functions = (0..self.toplevel.circuits.len()) + .map(|idx| CircuitType::Function { idx }); let memories = self .toplevel .memory_sizes @@ -648,6 +642,25 @@ mod tests { /// fresh auxiliary column pinned by `sel * (col - a*b)`. /// - `lookups = 1`: the function-provide (return) lookup in slot 0, which /// pulls the claim `[function_channel, fun_idx, a, b, a*b]`. + /// + /// Test-side singleton partition (production circuits come pre-built from + /// the Lean compiler). + fn with_singleton_circuits( + functions: Vec, + memory_sizes: Vec, + ) -> Toplevel { + let circuits = functions + .iter() + .enumerate() + .filter(|(_, f)| f.constrained) + .map(|(i, f)| crate::bytecode::Circuit { + members: vec![i], + layout: f.layout, + }) + .collect(); + Toplevel { functions, memory_sizes, circuits } + } + fn mul_toplevel() -> Toplevel { let body = Block { ops: vec![Op::Mul(0, 1)], ctrl: Ctrl::Return(0, vec![2]) }; @@ -662,7 +675,7 @@ mod tests { entry: true, constrained: true, }; - Toplevel { functions: vec![function], memory_sizes: vec![] } + with_singleton_circuits(vec![function], vec![]) } fn xor_splits_toplevel() -> Toplevel { @@ -681,7 +694,7 @@ mod tests { entry: true, constrained: true, }; - Toplevel { functions: vec![function], memory_sizes: vec![] } + with_singleton_circuits(vec![function], vec![]) } #[test] @@ -787,7 +800,7 @@ mod tests { constrained: true, }; - Toplevel { functions: vec![f, g], memory_sizes: vec![1] } + with_singleton_circuits(vec![f, g], vec![1]) } #[test] @@ -881,7 +894,7 @@ mod tests { constrained: true, }; - Toplevel { functions: vec![f, g, h], memory_sizes: vec![] } + with_singleton_circuits(vec![f, g, h], vec![]) } #[test] diff --git a/crates/aiur/src/trace.rs b/crates/aiur/src/trace.rs index e87dfe151..66e88cf92 100644 --- a/crates/aiur/src/trace.rs +++ b/crates/aiur/src/trace.rs @@ -12,7 +12,7 @@ use rayon::{ use crate::{ FxIndexMap, G, - bytecode::{Block, Ctrl, Function, Op, Toplevel}, + bytecode::{Block, Ctrl, Function, FunctionLayout, Op, Toplevel}, execute::{ IOBuffer, IOKeyInfo, QueryRecord, find_unconstrained_big_uint_div_mod, g_inverse_value, @@ -20,6 +20,7 @@ use crate::{ function_channel, gadgets::{bytes1::Bytes1, bytes2::Bytes2}, memory::Memory, + querymap::QueryRef, u8_add_channel, u8_and_channel, u8_bit_decomposition_channel, u8_less_than_channel, u8_mul_channel, u8_or_channel, u8_range_check_channel, u8_shift_left_channel, u8_shift_right_channel, u8_sub_channel, @@ -55,15 +56,23 @@ fn u32_sum(values: &[u64]) -> ([G; 4], G) { } impl<'a, 'b> ColumnMutSlice<'a, 'b> { + /// Slice a circuit row into the regions of one member function: the + /// member's inputs are a prefix of the circuit's input block, its + /// selectors a sub-range of the circuit's selector block at `sel_offset`, + /// and the auxiliary block is shared by all members. fn from_slice( function: &Function, + circuit_layout: &FunctionLayout, + sel_offset: usize, slice: &'a mut [G], lookups: &'a mut LookupRowMut<'b, G>, ) -> Self { - let (inputs, slice) = slice.split_at_mut(function.layout.input_size); - let (selectors, slice) = slice.split_at_mut(function.layout.selectors); - let (auxiliaries, slice) = slice.split_at_mut(function.layout.auxiliaries); - assert!(slice.is_empty()); + let (inputs, slice) = slice.split_at_mut(circuit_layout.input_size); + let (selectors, auxiliaries) = slice.split_at_mut(circuit_layout.selectors); + assert_eq!(auxiliaries.len(), circuit_layout.auxiliaries); + let inputs = &mut inputs[..function.layout.input_size]; + let selectors = + &mut selectors[sel_offset..sel_offset + function.layout.selectors]; Self { inputs, selectors, auxiliaries, lookups } } @@ -92,22 +101,49 @@ struct TraceContext<'a> { query_record: &'a QueryRecord, } +/// One row of a circuit trace: the member function it belongs to, the +/// member's selector offset within the circuit, its function index, and the +/// recorded query. +struct RowMeta<'a> { + function: &'a Function, + sel_offset: usize, + function_index: G, + inputs: &'a [G], + result: QueryRef<'a>, +} + impl Toplevel { pub fn witness_data( &self, - function_index: usize, + circuit_index: usize, query_record: &QueryRecord, io_buffer: &IOBuffer, slot_arg_widths: &[usize], ) -> (RowMajorMatrix, LookupValues) { - let func = &self.functions[function_index]; - let width = func.width(); - let unfiltered_queries = &query_record.function_queries[function_index]; - let queries = unfiltered_queries - .iter() - .filter(|(_, res)| !res.multiplicity.is_zero()) - .collect::>(); - let height_no_padding = queries.len(); + let circuit = &self.circuits[circuit_index]; + let layout = &circuit.layout; + let width = layout.width(); + // Concatenate the members' queried rows, in member order. + let mut rows_meta = Vec::new(); + let mut sel_offset = 0; + for &member in &circuit.members { + let function = &self.functions[member]; + let function_index = G::from_usize(member); + rows_meta.extend( + query_record.function_queries[member] + .iter() + .filter(|(_, res)| !res.multiplicity.is_zero()) + .map(|(inputs, result)| RowMeta { + function, + sel_offset, + function_index, + inputs, + result, + }), + ); + sel_offset += function.layout.selectors; + } + let height_no_padding = rows_meta.len(); // An unqueried circuit yields an EMPTY trace (not a padded height-1 one): // the prover deactivates it, so it is neither committed nor opened. let height = if height_no_padding == 0 { @@ -126,21 +162,27 @@ impl Toplevel { .zip(row_writers[..height_no_padding].par_iter_mut()) .enumerate() .for_each(|(i, (row, lookups))| { - let (inputs, result) = queries[i]; + let meta = &rows_meta[i]; let index = &mut ColumnIndex { auxiliary: 0, // we skip the first lookup, which is reserved for return lookup: 1, }; - let slice = &mut ColumnMutSlice::from_slice(func, row, lookups); + let slice = &mut ColumnMutSlice::from_slice( + meta.function, + layout, + meta.sel_offset, + row, + lookups, + ); let context = TraceContext { - function_index: G::from_usize(function_index), - inputs, - multiplicity: result.multiplicity, - output: result.output, + function_index: meta.function_index, + inputs: meta.inputs, + multiplicity: meta.result.multiplicity, + output: meta.result.output, query_record, }; - func.populate_row(index, slice, context, io_buffer); + meta.function.populate_row(index, slice, context, io_buffer); }); drop(row_writers); let trace = RowMajorMatrix::new(rows, width); diff --git a/crates/ffi/src/aiur/toplevel.rs b/crates/ffi/src/aiur/toplevel.rs index 4b88cdacd..fbead94f7 100644 --- a/crates/ffi/src/aiur/toplevel.rs +++ b/crates/ffi/src/aiur/toplevel.rs @@ -2,12 +2,15 @@ use multi_stark::p3_field::PrimeCharacteristicRing; use lean_ffi::object::{LeanBorrowed, LeanCtor, LeanRef}; +use crate::lean::LeanAiurCircuit; use crate::lean::LeanAiurFunction; use crate::lean::LeanAiurToplevel; use aiur::{ FxIndexMap, G, - bytecode::{Block, Ctrl, Function, FunctionLayout, Op, Toplevel, ValIdx}, + bytecode::{ + Block, Circuit, Ctrl, Function, FunctionLayout, Op, Toplevel, ValIdx, + }, }; use crate::aiur::{lean_unbox_g, lean_unbox_nat_as_usize}; @@ -294,14 +297,23 @@ fn decode_function(ctor: LeanCtor>) -> Function { Function { body, layout, entry, constrained } } +fn decode_circuit(ctor: LeanCtor>) -> Circuit { + let ctor = LeanAiurCircuit::from_ctor(ctor); + // Object field 0 is the circuit's display name (`String`), unused here. + let members = ctor.get_obj(1).as_array().map(|x| lean_unbox_nat_as_usize(&x)); + let layout = decode_function_layout(ctor.get_obj(2).as_ctor()); + Circuit { members, layout } +} + pub(crate) fn decode_toplevel( obj: &LeanAiurToplevel, ) -> Toplevel { let ctor = obj.as_ctor(); - let [functions_obj, memory_sizes_obj] = ctor.objs::<2>(); + let [functions_obj, memory_sizes_obj, circuits_obj] = ctor.objs::<3>(); let functions = functions_obj.as_array().map(|o| decode_function(o.as_ctor())); let memory_sizes = memory_sizes_obj.as_array().map(|x| lean_unbox_nat_as_usize(&x)); - Toplevel { functions, memory_sizes } + let circuits = circuits_obj.as_array().map(|o| decode_circuit(o.as_ctor())); + Toplevel { functions, memory_sizes, circuits } } diff --git a/crates/ffi/src/lean.rs b/crates/ffi/src/lean.rs index 4c57a4b2c..cf4ab2645 100644 --- a/crates/ffi/src/lean.rs +++ b/crates/ffi/src/lean.rs @@ -275,8 +275,9 @@ lean_ffi::lean_inductive! { // --- Aiur types --- - LeanAiurToplevel [ { num_obj: 2 } ]; + LeanAiurToplevel [ { num_obj: 3 } ]; LeanAiurFunction [ { num_obj: 2, num_8: 2 } ]; + LeanAiurCircuit [ { num_obj: 3 } ]; // Aiur FFI result structures (`Ix/Aiur/Semantics/BytecodeFfi.lean`, // `Ix/Aiur/Protocol.lean`). `IOBuffer` hashmaps cross the boundary as From 78801022663b87f7bf9bb401e9fa68ab1807f2c8 Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Mon, 3 Aug 2026 11:36:37 -0300 Subject: [PATCH 2/4] aiur: wire optional function-grouping application points (empty groupings) Route every site that compiles a production toplevel for proving or verifying through `compileWithGroups` with a per-toplevel grouping datum: `IxVM.functionGroups` for the kernel (CLI check/prove/verify/refine/ aggregate, the batch checker, the ixvm test runner, the benches), `Aggr.functionGroups` for the `ix_aggr` recursion system (aggregate prove/verify, the aggregation tests and benches), and `MultiStark.verifierFunctionGroups` for the standalone Multi-STARK verifier (its end-to-end tests, recursion-debug, bench-typecheck). `groupFunctions` resolves members by STRING name (the exact `toString` of the Global, the inverse of what statistics print, so measured groupings feed back verbatim). All three groupings start EMPTY, i.e. singleton circuits - behavior-identical to before; the data files are the single knob later commits turn. --- Benchmarks/AggregatePolicy.lean | 9 +++++---- Benchmarks/RecursionDebug.lean | 6 +++--- Benchmarks/Typecheck.lean | 6 +++--- Ix/Aggr.lean | 1 + Ix/Aggr/FunctionGroups.lean | 20 ++++++++++++++++++++ Ix/Aiur/Compiler.lean | 15 +++++++++++++-- Ix/Cli/AggregateCmd.lean | 16 +++++++++------- Ix/Cli/CheckCmd.lean | 9 +++++---- Ix/Cli/ProveCmd.lean | 2 +- Ix/Cli/RefineCmd.lean | 2 +- Ix/Cli/VerifyCmd.lean | 6 +++--- Ix/IxVM.lean | 1 + Ix/IxVM/FunctionGroups.lean | 20 ++++++++++++++++++++ Ix/MultiStark.lean | 1 + Ix/MultiStark/VerifierFunctionGroups.lean | 20 ++++++++++++++++++++ Tests/Aggr.lean | 2 +- Tests/AggrActivation.lean | 2 +- Tests/Aiur/Aiur.lean | 4 ++-- Tests/Aiur/Common.lean | 2 +- Tests/Main.lean | 2 +- Tests/MultiStark.lean | 4 ++-- 21 files changed, 114 insertions(+), 36 deletions(-) create mode 100644 Ix/Aggr/FunctionGroups.lean create mode 100644 Ix/IxVM/FunctionGroups.lean create mode 100644 Ix/MultiStark/VerifierFunctionGroups.lean diff --git a/Benchmarks/AggregatePolicy.lean b/Benchmarks/AggregatePolicy.lean index b04281df0..659828d99 100644 --- a/Benchmarks/AggregatePolicy.lean +++ b/Benchmarks/AggregatePolicy.lean @@ -83,11 +83,12 @@ def parseShardIds (value : String) : Except String (Array Nat) := do pure ids def compileToplevel (label : String) - (source : Except Aiur.Global Aiur.Source.Toplevel) : + (source : Except Aiur.Global Aiur.Source.Toplevel) + (groups : Array (String × Array String)) : IO (Except String Aiur.CompiledToplevel) := do match source with | .error error => pure (.error s!"{label} toplevel merge failed: {error}") - | .ok top => match top.compile with + | .ok top => match top.compileWithGroups groups with | .error error => pure (.error s!"{label} compilation failed: {error}") | .ok compiled => pure (.ok compiled) @@ -604,13 +605,13 @@ def main (args : List String) : IO UInt32 := do writeReport jsonPath? metadata0 rows #[] "preparing" TracingTexray.startSampler 25 IO.println "[aggregate-policy] compiling IxVM and ixAggr systems" - let ixvmCompiled ← match ← compileToplevel "IxVM" IxVM.ixVM with + let ixvmCompiled ← match ← compileToplevel "IxVM" IxVM.ixVM IxVM.functionGroups with | .error error => writeReport jsonPath? metadata0 rows #[] "error" (error? := some error) IO.eprintln error return 1 | .ok compiled => pure compiled - let aggrCompiled ← match ← compileToplevel "ixAggr recursion" Aggr.ixAggr with + let aggrCompiled ← match ← compileToplevel "ixAggr recursion" Aggr.ixAggr Aggr.functionGroups with | .error error => writeReport jsonPath? metadata0 rows #[] "error" (error? := some error) IO.eprintln error diff --git a/Benchmarks/RecursionDebug.lean b/Benchmarks/RecursionDebug.lean index 679d2c99c..84550e901 100644 --- a/Benchmarks/RecursionDebug.lean +++ b/Benchmarks/RecursionDebug.lean @@ -74,7 +74,7 @@ def proveConst (ixePath constName : String) (skipDeps : Bool) -- production toplevel no longer carries. let .ok toplevel := (if skipDeps then IxVM.ixVMFull else IxVM.ixVM) | IO.eprintln "IxVM toplevel merge failed"; return none - let .ok compiled := toplevel.compile + let .ok compiled := toplevel.compileWithGroups IxVM.functionGroups | IO.eprintln "IxVM compile failed"; return none let entrypoint := if skipDeps then `verify_const else `verify_claim let some funIdx := compiled.getFuncIdx entrypoint @@ -165,7 +165,7 @@ def main (args : List String) : IO UInt32 := do -- `--list-funcs`: dump the compiled verifier's funIdx → name table (for -- decoding fun_idx stacks printed by the Rust bytecode interpreter). if args.contains "--list-funcs" then - let .ok vCompiled := vTop.compile + let .ok vCompiled := vTop.compileWithGroups MultiStark.verifierFunctionGroups | IO.eprintln "multi-stark verifier compile failed"; return 1 let entries := vCompiled.nameMap.toArray.qsort (·.2 < ·.2) for (g, i) in entries do @@ -199,7 +199,7 @@ def main (args : List String) : IO UInt32 := do IO.println s!"ACCEPTED in {secs t0 t1} s: {Aiur.Value.ppDeref s.store depth v}" return 0 else - let .ok vCompiled := vTop.compile + let .ok vCompiled := vTop.compileWithGroups MultiStark.verifierFunctionGroups | IO.eprintln "multi-stark verifier compile failed"; return 1 let some vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof | IO.eprintln "verify_multi_stark_proof entrypoint missing"; return 1 diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 0672405aa..e25db3f50 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -450,7 +450,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do -- claim run, which is the honest reading of those numbers. let .ok toplevel := (if skipDeps then IxVM.ixVMFull else IxVM.ixVM) | throw (IO.userError "Merging IxVM kernel failed") - let .ok compiled := toplevel.compile + let .ok compiled := toplevel.compileWithGroups IxVM.functionGroups | throw (IO.userError "Compilation of IxVM kernel failed") let entrypoint := if skipDeps then `verify_const else `verify_claim let some funIdx := compiled.getFuncIdx entrypoint @@ -479,7 +479,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do if !recursive then pure none else do let .ok vTop := MultiStark.multiStark | throw (IO.userError "Merging multi-stark verifier failed") - let .ok vCompiled := vTop.compile + let .ok vCompiled := vTop.compileWithGroups MultiStark.verifierFunctionGroups | throw (IO.userError "Compilation of multi-stark verifier failed") let some vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof | throw (IO.userError "verify_multi_stark_proof entrypoint missing") @@ -493,7 +493,7 @@ def runTypecheckCmd (p : Cli.Parsed) : IO UInt32 := do if !join then pure none else do let .ok aggrTop := Aggr.ixAggr | throw (IO.userError "Merging ix_aggr failed") - let .ok aggrCompiled := aggrTop.compile + let .ok aggrCompiled := aggrTop.compileWithGroups Aggr.functionGroups | throw (IO.userError "Compilation of ix_aggr failed") let some aggrIdx := aggrCompiled.getFuncIdx `ix_aggr | throw (IO.userError "ix_aggr entrypoint missing") diff --git a/Ix/Aggr.lean b/Ix/Aggr.lean index d787bd71c..be5abacf1 100644 --- a/Ix/Aggr.lean +++ b/Ix/Aggr.lean @@ -1,6 +1,7 @@ module public import Blake3.Rust public import Ix.Aggr.Circuit +public import Ix.Aggr.FunctionGroups public import Ix.Aggr.Host public import Ix.AssumptionTree public import Ix.MultiStark diff --git a/Ix/Aggr/FunctionGroups.lean b/Ix/Aggr/FunctionGroups.lean new file mode 100644 index 000000000..24c594e7a --- /dev/null +++ b/Ix/Aggr/FunctionGroups.lean @@ -0,0 +1,20 @@ +module + +/-! +Function-grouping data for the production aggregation toplevel +(`Aggr.ixAggr`), applied wherever it is compiled for proving or verifying +(see `CompiledToplevel.groupFunctions`). Empty = no grouping: every +constrained function keeps its singleton circuit. Fill from measured +workload statistics; a stale grouping stays sound (grouping never affects +semantics), only less efficient. +-/ + +public section + +namespace Aggr + +def functionGroups : Array (String × Array String) := #[] + +end Aggr + +end diff --git a/Ix/Aiur/Compiler.lean b/Ix/Aiur/Compiler.lean index e8e8ccfae..39fe13956 100644 --- a/Ix/Aiur/Compiler.lean +++ b/Ix/Aiur/Compiler.lean @@ -59,9 +59,14 @@ per absorbed member. Errors if a name is unknown, unconstrained (it has no circuit to group), an entry function, listed twice, or if a group is empty. -/ def CompiledToplevel.groupFunctions (ct : CompiledToplevel) - (groups : Array (String × Array Lean.Name)) : + (groups : Array (String × Array String)) : Except String CompiledToplevel := do let t := ct.bytecode + -- Function names as printed (`toString` of the `Global`), the exact + -- inverse of what statistics reports — so measured groupings can be fed + -- back verbatim. + let byName : Std.HashMap String Bytecode.FunIdx := + ct.nameMap.fold (init := {}) fun acc g i => acc.insert (toString g) i -- Resolve and validate the groups into member-index arrays. let mut grouped : Std.HashMap Bytecode.FunIdx Nat := {} let mut resolved : Array (String × Array Bytecode.FunIdx) := #[] @@ -70,7 +75,7 @@ def CompiledToplevel.groupFunctions (ct : CompiledToplevel) throw s!"group {gname} is empty" let mut members := #[] for name in names do - let some i := ct.getFuncIdx name + let some i := byName[name]? | throw s!"group {gname}: unknown function {name}" let f := t.functions[i]! unless f.constrained do @@ -204,6 +209,12 @@ def Source.Toplevel.compile (t : Source.Toplevel) : Except String CompiledToplev circuits := bytecode.singletonCircuits fun i => reverseMap[i]?.getD s!"" } pure (CompiledToplevel.mk t bytecode nameMap) +/-- `compile`, then apply a function grouping (see +`CompiledToplevel.groupFunctions`). -/ +def Source.Toplevel.compileWithGroups (t : Source.Toplevel) + (groups : Array (String × Array String)) : Except String CompiledToplevel := do + (← t.compile).groupFunctions groups + /-- Progress helper: given success of the three `Except`-returning stages, `compile` as a whole returns `.ok` (the remaining stages — `deduplicate`, `needsCircuit`, the field-setter `mapIdx`, the name-map `fold`, and the diff --git a/Ix/Cli/AggregateCmd.lean b/Ix/Cli/AggregateCmd.lean index ccca0c707..1b19531e5 100644 --- a/Ix/Cli/AggregateCmd.lean +++ b/Ix/Cli/AggregateCmd.lean @@ -483,11 +483,12 @@ def prepareShards (env : Ixon.Env) (shards : Array (Array Address)) pure prepared private def compileToplevel (label : String) - (source : Except Aiur.Global Aiur.Source.Toplevel) : + (source : Except Aiur.Global Aiur.Source.Toplevel) + (groups : Array (String × Array String)) : IO (Except String Aiur.CompiledToplevel) := do match source with | .error e => return Except.error s!"{label} toplevel merge failed: {e}" - | .ok top => match top.compile with + | .ok top => match top.compileWithGroups groups with | .error e => return Except.error s!"{label} compilation failed: {e}" | .ok compiled => return Except.ok compiled @@ -502,10 +503,11 @@ pipeline together lets the independent IxVM and recursion backends build in parallel instead of serializing their Rust setup on the controller thread. -/ private def buildAggregateBackend (label : String) (source : Unit → Except Aiur.Global Aiur.Source.Toplevel) + (groups : Array (String × Array String)) (commitment : Aiur.CommitmentParameters) (fri : Aiur.FriParameters) : IO (Except String AggregateBackend) := do let source ← IO.lazyPure source - let compiled ← match ← compileToplevel label source with + let compiled ← match ← compileToplevel label source groups with | .error e => return .error e | .ok compiled => pure compiled let system := Aiur.AiurSystem.build compiled.bytecode commitment fri @@ -943,11 +945,11 @@ private def runAggregateCmdNativeWith let envTask ← IO.asTask (prio := .dedicated) do timed (IO.lazyPure fun _ => Aiur.EnvHandle.fromIxe ixePath) let ixvmBackendTask ← IO.asTask (prio := .dedicated) do - timed (buildAggregateBackend "IxVM" (fun _ => IxVM.ixVM) + timed (buildAggregateBackend "IxVM" (fun _ => IxVM.ixVM) IxVM.functionGroups Aiur.defaultCommitmentParameters Aiur.defaultFriParameters) let aggrBackendTask ← IO.asTask (prio := .dedicated) do timed (buildAggregateBackend "ixAggr recursion" (fun _ => Aggr.ixAggr) - recursionParameters.commitment recursionParameters.fri) + Aggr.functionGroups recursionParameters.commitment recursionParameters.fri) -- Join every setup branch before selecting an error, so a failed branch -- cannot orphan compilation work in the process. @@ -1052,11 +1054,11 @@ private def runAggregateCmdLeanReferenceWith let proofsTask ← IO.asTask (prio := .dedicated) do timed (loadShardProofs proofHexes) let ixvmBackendTask ← IO.asTask (prio := .dedicated) do - timed (buildAggregateBackend "IxVM" (fun _ => IxVM.ixVM) + timed (buildAggregateBackend "IxVM" (fun _ => IxVM.ixVM) IxVM.functionGroups Aiur.defaultCommitmentParameters Aiur.defaultFriParameters) let aggrBackendTask ← IO.asTask (prio := .dedicated) do timed (buildAggregateBackend "ixAggr recursion" (fun _ => Aggr.ixAggr) - recursionParameters.commitment recursionParameters.fri) + Aggr.functionGroups recursionParameters.commitment recursionParameters.fri) let prepareOutcome := prepareTask.get let proofsOutcome := proofsTask.get diff --git a/Ix/Cli/CheckCmd.lean b/Ix/Cli/CheckCmd.lean index c88f3b0b2..9de6950fc 100644 --- a/Ix/Cli/CheckCmd.lean +++ b/Ix/Cli/CheckCmd.lean @@ -141,7 +141,8 @@ inductive Target where and resolve to labels here. -/ def runBatchCheck (ixePath : String) (names : List String) (jobs : Nat) (toplevel : Aiur.Source.Toplevel) (useBytecode : Bool) : IO UInt32 := do - let compiled : Aiur.CompiledToplevel ← match toplevel.compile with + let compiled : Aiur.CompiledToplevel ← + match toplevel.compileWithGroups IxVM.functionGroups with | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c let envHandle ← match Aiur.EnvHandle.fromIxe ixePath with @@ -1383,7 +1384,7 @@ def runCheckCmd (p : Cli.Parsed) : IO UInt32 := do pure 1 pure go else do - let compiled ← match toplevel.compile with + let compiled ← match toplevel.compileWithGroups IxVM.functionGroups with | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c let go (_ : Ix.Claim) (envHandle? : Option Aiur.EnvHandle) (target : Target) @@ -1396,7 +1397,7 @@ def runCheckCmd (p : Cli.Parsed) : IO UInt32 := do return (← runShardCheckManifest manifest ixe k (fun c w l => runOne c none (.leanW w) l)) else do - let compiled ← match toplevel.compile with + let compiled ← match toplevel.compileWithGroups IxVM.functionGroups with | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c return (← runShardCheckManifestNative manifest ixe k compiled printStats statsOut useBytecode) @@ -1405,7 +1406,7 @@ def runCheckCmd (p : Cli.Parsed) : IO UInt32 := do return (← runShardCheckAll manifest ixe ((p.flag? "jobs").map (·.as! Nat)) (fun c w l => runOne c none (.leanW w) l)) else do - let compiled ← match toplevel.compile with + let compiled ← match toplevel.compileWithGroups IxVM.functionGroups with | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c let json? := (p.flag? "json").map fun f => diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index 010a19b2f..6e5e52b9b 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -273,7 +273,7 @@ def runProveCmd (p : Cli.Parsed) : IO UInt32 := do let toplevel ← match IxVM.ixVM with | .error e => IO.eprintln s!"toplevel merging failed: {e}"; return 1 | .ok t => pure t - let compiled ← match toplevel.compile with + let compiled ← match toplevel.compileWithGroups IxVM.functionGroups with | .error e => IO.eprintln s!"compilation failed: {e}"; return 1 | .ok c => pure c let aiurSystem := Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters diff --git a/Ix/Cli/RefineCmd.lean b/Ix/Cli/RefineCmd.lean index abec477e2..73ec02f66 100644 --- a/Ix/Cli/RefineCmd.lean +++ b/Ix/Cli/RefineCmd.lean @@ -62,7 +62,7 @@ def runShardRefineCmd (p : Cli.Parsed) : IO UInt32 := do let toplevel ← match IxVM.ixVM with | .error e => IO.eprintln s!"toplevel merging failed: {e}"; return 1 | .ok t => pure t - let compiled ← match toplevel.compile with + let compiled ← match toplevel.compileWithGroups IxVM.functionGroups with | .error e => IO.eprintln s!"compilation failed: {e}"; return 1 | .ok c => pure c -- The proven-leaf guard: a selected leaf whose claim already has a diff --git a/Ix/Cli/VerifyCmd.lean b/Ix/Cli/VerifyCmd.lean index 1b6bc5fe4..2f03bb565 100644 --- a/Ix/Cli/VerifyCmd.lean +++ b/Ix/Cli/VerifyCmd.lean @@ -82,7 +82,7 @@ def verifyOneProof (aiurSystem : Aiur.AiurSystem) (compiled : Aiur.CompiledTople def buildBackend : IO (Except String (Aiur.AiurSystem × Aiur.CompiledToplevel)) := do match IxVM.ixVM with | .error e => return .error s!"toplevel merging failed: {e}" - | .ok toplevel => match toplevel.compile with + | .ok toplevel => match toplevel.compileWithGroups IxVM.functionGroups with | .error e => return .error s!"compilation failed: {e}" | .ok compiled => return .ok (Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters, compiled) @@ -154,12 +154,12 @@ private def buildAggregateBackend IO (Except String AggregateBackend) := do let ixvmCompiled ← match IxVM.ixVM with | .error e => return .error s!"IxVM toplevel merging failed: {e}" - | .ok top => match top.compile with + | .ok top => match top.compileWithGroups IxVM.functionGroups with | .error e => return .error s!"IxVM compilation failed: {e}" | .ok compiled => pure compiled let aggrCompiled ← match Aggr.ixAggr with | .error e => return .error s!"recursion toplevel merging failed: {e}" - | .ok top => match top.compile with + | .ok top => match top.compileWithGroups Aggr.functionGroups with | .error e => return .error s!"recursion compilation failed: {e}" | .ok compiled => pure compiled let verifyIdx := ixvmCompiled.getFuncIdx `verify_claim |>.get! diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean index 45c6b898d..c04615004 100644 --- a/Ix/IxVM.lean +++ b/Ix/IxVM.lean @@ -1,6 +1,7 @@ module public import Ix.Aiur.Meta public import Ix.IxVM.Core +public import Ix.IxVM.FunctionGroups public import Ix.IxVM.ByteStream public import Ix.IxVM.Blake3 public import Ix.IxVM.RBTreeMap diff --git a/Ix/IxVM/FunctionGroups.lean b/Ix/IxVM/FunctionGroups.lean new file mode 100644 index 000000000..f37a56d09 --- /dev/null +++ b/Ix/IxVM/FunctionGroups.lean @@ -0,0 +1,20 @@ +module + +/-! +Function-grouping data for the IxVM kernel toplevel, applied wherever the +kernel is compiled for proving or verifying (see +`CompiledToplevel.groupFunctions`). Empty = no grouping: every constrained +function keeps its singleton circuit. Fill from measured workload +statistics; a stale grouping stays sound (grouping never affects +semantics), only less efficient. +-/ + +public section + +namespace IxVM + +def functionGroups : Array (String × Array String) := #[] + +end IxVM + +end diff --git a/Ix/MultiStark.lean b/Ix/MultiStark.lean index ac60c7739..beb3f64c6 100644 --- a/Ix/MultiStark.lean +++ b/Ix/MultiStark.lean @@ -14,6 +14,7 @@ public import Ix.MultiStark.Keccak public import Ix.MultiStark.Pcs public import Ix.MultiStark.SystemDeserialize public import Ix.MultiStark.Verifier +public import Ix.MultiStark.VerifierFunctionGroups public import Ix.MultiStark.Tests /-! diff --git a/Ix/MultiStark/VerifierFunctionGroups.lean b/Ix/MultiStark/VerifierFunctionGroups.lean new file mode 100644 index 000000000..5c9c8501a --- /dev/null +++ b/Ix/MultiStark/VerifierFunctionGroups.lean @@ -0,0 +1,20 @@ +module + +/-! +Function-grouping data for the standalone Multi-STARK verifier toplevel +(`MultiStark.multiStark`), applied wherever it is compiled for proving or +verifying (see `CompiledToplevel.groupFunctions`). Empty = no grouping: +every constrained function keeps its singleton circuit. Fill from measured +workload statistics; a stale grouping stays sound (grouping never affects +semantics), only less efficient. +-/ + +public section + +namespace MultiStark + +def verifierFunctionGroups : Array (String × Array String) := #[] + +end MultiStark + +end diff --git a/Tests/Aggr.lean b/Tests/Aggr.lean index 7ac7b35aa..eceb1146f 100644 --- a/Tests/Aggr.lean +++ b/Tests/Aggr.lean @@ -107,7 +107,7 @@ def smokeSuite : IO UInt32 := do let aggrTop ← match Aggr.ixAggr with | .error e => IO.eprintln s!"ixAggr toplevel merge failed: {e}"; return 1 | .ok t => pure t - let aggrCompiled ← match aggrTop.compile with + let aggrCompiled ← match aggrTop.compileWithGroups Aggr.functionGroups with | .error e => IO.eprintln s!"ixAggr compilation failed: {e}"; return 1 | .ok c => pure c let some ixAggrIdx := aggrCompiled.getFuncIdx `ix_aggr diff --git a/Tests/AggrActivation.lean b/Tests/AggrActivation.lean index adc843fed..205f6cef9 100644 --- a/Tests/AggrActivation.lean +++ b/Tests/AggrActivation.lean @@ -514,7 +514,7 @@ def run : IO UInt32 := do let top ← match Aggr.ixAggr with | .error e => IO.eprintln s!"activation toplevel merge failed: {e}"; return 1 | .ok top => pure top - let compiled ← match top.compile with + let compiled ← match top.compileWithGroups Aggr.functionGroups with | .error e => IO.eprintln s!"activation toplevel compilation failed: {e}"; return 1 | .ok compiled => pure compiled let some ixAggrIdx := compiled.getFuncIdx `ix_aggr | do diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean index 0230ad1f1..cf1a890bf 100644 --- a/Tests/Aiur/Aiur.lean +++ b/Tests/Aiur/Aiur.lean @@ -909,8 +909,8 @@ def aiurTestCases : List AiurTestCase := [ ] /-- The grouping the `aiur` runner applies for the grouped environment. -/ -def testGroups : Array (String × Array Lean.Name) := - #[("test_group", #[`grouped_double, `grouped_pick, `grouped_sum_range])] +def testGroups : Array (String × Array String) := + #[("test_group", #["grouped_double", "grouped_pick", "grouped_sum_range"])] def groupedTestCases : List AiurTestCase := [ .prove `calls_grouped #[0, 5, 9] #[25] diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean index 89b8b2c2b..afd13803d 100644 --- a/Tests/Aiur/Common.lean +++ b/Tests/Aiur/Common.lean @@ -73,7 +73,7 @@ structure AiurTestEnv where shapes : Array Aiur.CircuitShape def AiurTestEnv.build (toplevelFn : Except Aiur.Global Aiur.Source.Toplevel) - (groups : Array (String × Array Lean.Name) := #[]) : + (groups : Array (String × Array String) := #[]) : Except String AiurTestEnv := do let toplevel ← toplevelFn.mapError toString let compiled ← toplevel.compile diff --git a/Tests/Main.lean b/Tests/Main.lean index 19cb2b078..b22bc92e1 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -225,7 +225,7 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ -- committed kernel system). let kernelUnitTests := .exec `kernel_unit_tests let serdeTest ← serdeNatAddComm env - match AiurTestEnv.build IxVM.ixVM, AiurTestEnv.build IxVM.ixVMFull with + match AiurTestEnv.build IxVM.ixVM IxVM.functionGroups, AiurTestEnv.build IxVM.ixVMFull with | .error e, _ | _, .error e => IO.eprintln s!"IxVM env build failed: {e}"; return 1 | .ok v2Env, .ok v2FullEnv => diff --git a/Tests/MultiStark.lean b/Tests/MultiStark.lean index 0e0f92425..d55f537a0 100644 --- a/Tests/MultiStark.lean +++ b/Tests/MultiStark.lean @@ -188,7 +188,7 @@ def endToEndSuite : IO UInt32 := do let vTop ← match MultiStark.multiStark with | .error e => IO.eprintln s!"verifier toplevel merge failed: {e}"; return 1 | .ok t => pure t - let vCompiled ← match vTop.compile with + let vCompiled ← match vTop.compileWithGroups MultiStark.verifierFunctionGroups with | .error e => IO.eprintln s!"verifier compilation failed: {e}"; return 1 | .ok c => pure c let vIdx ← match vCompiled.getFuncIdx `verify_multi_stark_proof with @@ -579,7 +579,7 @@ def joinSmokeSuite : IO UInt32 := do let top ← match MultiStark.multiStark with | .error e => IO.eprintln s!"aggregate toplevel merge failed: {e}"; return 1 | .ok t => pure t - let compiled ← match top.compile with + let compiled ← match top.compileWithGroups MultiStark.verifierFunctionGroups with | .error e => IO.eprintln s!"aggregate compilation failed: {e}"; return 1 | .ok c => pure c let joinIdx := compiled.getFuncIdx `join_two |>.get! From d25f4594f0622db902700c5f17e5e2ac15bfff1a Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 8 Sep 2026 16:30:31 +0000 Subject: [PATCH 3/4] ixvm: populate the function grouping by cost-aware greedy merging (744 -> 171) Built from fresh execute-only kernel-check profiles of the current circuits (String.split, Array.extract_append, and a 2^16384 big-nat reduction whose hot circuit is cold in every typechecking workload), with a partitioner that ranks merges by the ACTIVE committed width they save - what a proof actually opens, at every FRI query - per unit of modelled prover cost (the FFT model of Ix/Aiur/Statistics.lean plus a constraint-evaluation term, relative to each workload), within an average 2% (max 4%) cost increase per workload, <= 16 members and <= 40 selectors per group. The width/FFT model reproduces the measured statistics to the column, so the emitted grouping is exactly what the prover builds. 83 groups over 656 of 743 groupable circuits: 744 -> 171 circuits, total committed width 33,693 -> 12,729 (-62%), active width on kernel checks -50% to -58% (three held-out constants included) at +1.0% to +2.0% measured FFT cost. End to end, proofs of Nat.sub_le_of_le_add / Lean.Syntax.rec / String.split shrink from 19.8 / 20.2 / 22.5 MB to 9.4 / 10.3 / 9.9 MB, proving is slightly faster (fewer per-circuit fixed costs than extra columns) and verification takes half the time. Kernel FFT pins re-measured (median +1.7%, max +3.8%; shard pipeline +1.3%). --- Ix/IxVM/FunctionGroups.lean | 832 +++++++++++++++++++++++++++++++++++- Tests/Ix/IxVM.lean | 158 +++---- Tests/Main.lean | 4 +- 3 files changed, 912 insertions(+), 82 deletions(-) diff --git a/Ix/IxVM/FunctionGroups.lean b/Ix/IxVM/FunctionGroups.lean index f37a56d09..27820e1fb 100644 --- a/Ix/IxVM/FunctionGroups.lean +++ b/Ix/IxVM/FunctionGroups.lean @@ -13,7 +13,837 @@ public section namespace IxVM -def functionGroups : Array (String × Array String) := #[] +-- Cost-aware greedy grouping over the String.split / Array.extract_append +-- kernel-check profiles and a 2^16384 big-nat reduction: merges are ranked +-- by active committed width saved (proof size) per unit of modelled prover +-- cost (FFT model plus a constraint-evaluation term, relative to each +-- workload), capped at 16 members and 40 selectors per group, within an +-- average 2% (max 4%) cost increase per workload. 83 groups over 656 of +-- 743 groupable circuits: 744 -> 171 circuits. +def functionGroups : Array (String × Array String) := #[ + ("ixvm_group_00", #[ + "memo_u32_less_than", + "lbr_max", + "lbr_min", + "delta_unfold" + ]), + ("ixvm_group_01", #[ + "address_eq_tail", + "get_recursor", + "count_ctors", + "ctor_at", + "load_verified_blob", + "get_ci", + "check_canonical_block", + "peer_agree_walk", + "ind_is_solo", + "flat_originals_walk", + "find_peer_recursor_with_spec" + ]), + ("ixvm_group_02", #[ + "u64_eq", + "relaxed_u64_succ", + "quot_kind_tag", + "klimbs_mod", + "system_platform_get_num_bits_addr", + "str_addr", + "convert_axiom", + "convert_quotient", + "quot_ctor_addr", + "quot_lift_addr_iota", + "quot_ind_addr", + "quot_type_addr" + ]), + ("ixvm_group_03", #[ + "u64_add", + "is_str_prim_addr", + "is_dec_prim_addr", + "check_const" + ]), + ("ixvm_group_04", #[ + "relaxed_u64_pred", + "flatten_u64" + ]), + ("ixvm_group_05", #[ + "verify_bytes_against", + "put_constructor_proj", + "get_expr_let", + "build_succ_chain", + "bytes_to_u64_limb", + "io_peel_field_loop", + "assert_occ_param_bvars", + "populate_rules", + "build_minor_doms", + "peel_leading_foralls_acc", + "flat_find_matching", + "const_idxs_rules" + ]), + ("ixvm_group_06", #[ + "bytes_to_addr", + "get_constructor", + "get_mut_const", + "is_unit_like_type", + "canon_muts_has_kind", + "is_muts_block", + "muts_indc_count_is_one", + "const_idxs_ctors" + ]), + ("ixvm_group_07", #[ + "blake3_next_layer", + "get_ci_iprj", + "get_ci_cprj", + "muts_member_at", + "projection_addr", + "build_flat_block", + "run_claim" + ]), + ("ixvm_group_08", #[ + "blake3_compress_layer", + "blake3_finish", + "get_constant" + ]), + ("ixvm_group_09", #[ + "put_expr", + "get_ci_rprj", + "first_recr_parent_block", + "load_assumption_tree", + "env_walk", + "get_mut_entry", + "get_mut_entry_list_inner", + "check_opt_addr", + "check_muts_components", + "list_length_u64.MutConst", + "list_lookup_u64.Constructor" + ]), + ("ixvm_group_10", #[ + "put_u64_le", + "check_native_nat", + "utf8_last_go", + "char_lit_codepoint", + "mk_nat_binop_stuck", + "canon_cmp_krec_rule_ctx", + "canon_kind_ord", + "canon_ctor_ctx_entries", + "canon_refine_one", + "canon_ins_sort", + "canon_flatten", + "canon_all_singleton", + "extract_aux_spec_params_from_rec", + "check_opt_u64", + "list_concat.Tup.Ptr.U8_32.G", + "rbtree_map_insert.G" + ]), + ("ixvm_group_11", #[ + "put_tag0", + "put_tag4", + "put_definition_proj", + "convert_definition", + "level_reduce", + "compare_struct_fields", + "try_unfold_head", + "k_infer_lit", + "list_any_mentions_block", + "check_inductive_shape", + "list_reverse.G" + ]), + ("ixvm_group_12", #[ + "put_tag2", + "univ_succ_base", + "put_recursor_rule", + "put_mut_const", + "u64_or", + "u64_xor_kbits", + "defn_member_recur_addrs", + "canon_cmp_member_ctx", + "canon_sort_loop", + "aux_already_in", + "spec_params_dom_prefix_match", + "addr_set_build", + "env_walk_refs", + "env_walk_leaves", + "expr_addr", + "rbtree_map_balance.G" + ]), + ("ixvm_group_13", #[ + "put_u64_list", + "put_recursor_rule_list", + "canon_g_list_eq", + "canon_ctx_class_idx", + "canon_cmp_kexpr_ctx", + "canon_member_ci", + "canon_member_num_ctors", + "canon_refine_classes", + "canon_group_consec", + "level_list_struct_eq", + "spec_params_ptr_eq", + "flat_find_pos", + "get_opt_rule_list_masked", + "get_opt_ctor_entry_list_masked", + "list_length.U8_8" + ]), + ("ixvm_group_14", #[ + "put_quot_kind", + "pack_def_kind_safety", + "mk_nat_literal_64", + "mk_nat_one", + "char_of_nat_addr", + "char_type_addr", + "byte_array_empty_addr", + "utf8_last_codepoint", + "utf8_cont", + "canon_ord_then", + "canon_sord_then", + "def_safety_tag", + "check_opt_bool", + "check_opt_recr_rules", + "check_opt_ctor_entries", + "run_contains" + ]), + ("ixvm_group_15", #[ + "put_all_mode", + "klimbs_shl", + "np_whnf_inner_bv", + "canon_addr_chunk", + "canon_cmp_kliteral", + "leaf_hash", + "node_hash", + "addr_set_member", + "get_opt_u64_masked", + "get_opt_addr_masked", + "get_opt_bool_masked", + "get_opt_def_kind_masked", + "get_opt_quot_kind_masked", + "check_opt_def_kind", + "check_opt_def_safety", + "check_opt_quot_kind" + ]), + ("ixvm_group_16", #[ + "app_telescope_count", + "lam_telescope_count", + "all_telescope_count", + "put_app_telescope", + "put_lam_telescope", + "put_all_telescope", + "put_definition", + "put_constructor", + "put_inductive", + "str_lit_delta_step", + "canon_cmp_ctor_range_ctx", + "canon_group_walk", + "get_reveal_rule_list_inner", + "check_recr_rules", + "rbtree_map_lookup_or_default.G", + "rbtree_map_ins.G" + ]), + ("ixvm_group_17", #[ + "put_address", + "u64_mul", + "try_reduce_decide_bitvec_lt", + "try_nat_binop_addr", + "build_rec_type_from", + "check_recursor_canonical_full" + ]), + ("ixvm_group_18", #[ + "univ_succ_count", + "put_univ", + "put_axiom", + "put_quotient", + "put_constructor_list", + "put_mut_const_list", + "klimbs_lor", + "klimbs_xor_op", + "canon_cmp_klimbs_tail", + "extract_aux_occ_us", + "detect_aux_from_recrs_ex", + "get_ctor_entry", + "check_ctor_entries", + "list_length_u64.U8_8", + "list_length_u64.Constructor", + "list_length_u64.RecursorRule" + ]), + ("ixvm_group_19", #[ + "put_expr_list", + "get_recursor_rule_list", + "get_inductive", + "canon_indc_positions", + "check_block_peer_param_agreement", + "flat_find_pos_kind", + "build_rec_type", + "build_flat_own_params", + "build_all_minors_walk", + "build_all_motives_walk", + "const_idxs_muts", + "list_length_u64.Ptr.U8_32" + ]), + ("ixvm_group_20", #[ + "put_univ_list", + "put_address_list", + "put_sharing", + "klimbs_dec", + "mk_nat_offset_stuck", + "idx_to_u64", + "nlvars_eq", + "se_scan_fields", + "se_addr_in", + "compute_iprj_addr", + "flat_member_at", + "collect_index_doms", + "collect_n_doms_whnf", + "wrap_lams", + "is_rec_field_peel" + ]), + ("ixvm_group_21", #[ + "put_recursor", + "klimbs_scalar_value", + "str_dec_eq_build", + "canon_addr_cmp", + "canon_cmp_member_same_kind_ctx", + "canon_cmp_ctor_pair_ctx", + "get_reveal_ctor_info", + "get_ctor_entry_list_inner", + "check_opt_expr_addr", + "check_ctor_entry", + "check_mut_const", + "run_reveal" + ]), + ("ixvm_group_22", #[ + "put_constant_info", + "put_constant", + "convert_inductive", + "convert_constructor", + "convert_recursor", + "const_idxs_of", + "check_muts_member_at" + ]), + ("ixvm_group_23", #[ + "put_refs", + "put_univs", + "klimbs_le", + "check_no_dep_data_field_if_prop", + "assert_return_head_is_parent", + "caddr_is_peer", + "rec_to_parent_addr", + "peel_motive_params_subst", + "list_lift_indices", + "build_peer_recs", + "list_lift_each", + "check_rec_major_spine", + "get_opt_addr", + "list_length.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode" + ]), + ("ixvm_group_24", #[ + "read_byte", + "klimbs_mul", + "expr_inst1_bvar", + "unfold_b_and_loop", + "peel_n_foralls" + ]), + ("ixvm_group_25", #[ + "get_tag2", + "get_constructor_proj", + "level_max", + "whnf_iota_major", + "collect_spine_of_ctor" + ]), + ("ixvm_group_26", #[ + "get_lam_telescope", + "get_all_telescope" + ]), + ("ixvm_group_27", #[ + "get_univ", + "klimbs_sub_borrow", + "try_same_proj_head_app" + ]), + ("ixvm_group_28", #[ + "get_univ_list", + "level_max_offsets", + "projection_definition_info", + "whnf_struct_core_proj", + "slow2_eager_fallback", + "lazy_delta_a_const_b_proj", + "lazy_delta_b_const_a_proj" + ]), + ("ixvm_group_29", #[ + "get_address_list", + "list_snoc.U8_8" + ]), + ("ixvm_group_30", #[ + "unpack_def_kind_safety", + "assert_wire_bool", + "defn_is_unsafe_ci", + "lbr_dec", + "delta_rank", + "is_defn_or_thm", + "is_unsafe_ci", + "check_parent_inductive_shape", + "build_all_motives", + "build_all_minors", + "build_ctor_app_params" + ]), + ("ixvm_group_31", #[ + "get_definition", + "cleanup_nat_offset_major", + "convert_univ_idxs", + "k_is_def_eq_slow2" + ]), + ("ixvm_group_32", #[ + "get_axiom", + "get_quotient", + "bv_to_nat_via", + "bitvec_of_nat_args_direct", + "mk_int_prim", + "klimbs_eq", + "bitvec_prep_spine", + "quot_extract_arg", + "struct_block_member_addrs", + "try_eta_expand", + "check_eq_type" + ]), + ("ixvm_group_33", #[ + "get_constructor_list", + "get_mut_const_list", + "load_verified_constant", + "build_recur_addrs_walk", + "check_muts_all" + ]), + ("ixvm_group_34", #[ + "get_inductive_proj", + "klimbs_is_zero", + "k_is_def_eq_struct_safe", + "try_eta_swap", + "run_check" + ]), + ("ixvm_group_35", #[ + "get_constant_info_by_variant", + "run_check_transitive" + ]), + ("ixvm_group_36", #[ + "klimbs_succ", + "is_nat_succ_ih_step", + "bytes_to_limbs", + "convert_rec_rules", + "nl_eq", + "nlvars_dominates", + "dec_dispatch_le_eq", + "ctors_before_pos", + "projection_addr_ctor" + ]), + ("ixvm_group_37", #[ + "u64_sub_with_borrow", + "try_nat_offset_dispatch", + "nl_covers_const", + "normalize_int_dec_rebuild", + "check_valid_ind_app", + "is_large_eliminator", + "compute_k_target", + "build_motive_type_flat", + "canonical_rules_at_pos", + "build_rule_rhs", + "check_recursor_member" + ]), + ("ixvm_group_38", #[ + "glimbs_to_klimbs", + "try_match_nat_add", + "level_normalize", + "level_max_go", + "ctx_close_cut", + "nat_lit_to_ctor_or_self" + ]), + ("ixvm_group_39", #[ + "klimbs_sub", + "skip_bytes", + "level_explicit_val", + "expr_has_bvar_at_let", + "build_param_lvls_range", + "build_major_params", + "build_apply_xs", + "apply_indices_in_conclusion", + "count_foralls_body", + "peel_leading_foralls", + "build_rec_lvls_list", + "check_rec_rules_wellscoped", + "list_lookup_or_default.Ptr.U8_32" + ]), + ("ixvm_group_40", #[ + "klimbs_div_mod", + "klimbs_pow", + "try_nat_linear_rec", + "check_ctor_return_type", + "check_inductive_shape_ctors", + "peel_ctor_params_subst", + "walk_fields_classify" + ]), + ("ixvm_group_41", #[ + "klimbs_div", + "klimbs_gcd", + "klimbs_shr", + "mk_bool", + "try_quot_iota", + "se_parent_addr", + "struct_is_rec", + "struct_scan_ctors", + "intern_int_lit", + "all_bvars_in_args", + "args_contain_bvar" + ]), + ("ixvm_group_42", #[ + "u64_and", + "klimbs_land", + "try_reduce_subtype_val", + "try_str_to_byte_array", + "try_int_prim_second", + "try_quot_lift", + "k_synth_gate", + "dec_finish", + "canon_cprj_addr" + ]), + ("ixvm_group_43", #[ + "nat_zero_addr", + "nat_succ_addr_iota", + "nat_pred_addr", + "nat_sub_addr", + "nat_xor_addr", + "nat_shift_right_addr", + "punit_size_of_1_addr", + "reduce_bool_addr", + "reduce_nat_addr", + "string_utf8_byte_size_addr", + "string_append_addr", + "string_of_list_addr", + "string_back_addr", + "string_legacy_back_addr", + "string_to_byte_array_addr", + "string_dec_eq_addr" + ]), + ("ixvm_group_44", #[ + "int_of_nat_addr", + "int_neg_succ_addr_dec", + "bool_true_addr", + "bool_false_addr", + "bit_vec_of_nat_addr", + "bit_vec_addr", + "lt_lt_addr", + "decidable_rec_addr", + "decidable_is_true_addr_dec", + "decidable_is_false_addr_dec", + "nat_le_of_ble_eq_true_addr_dec", + "nat_eq_of_beq_eq_true_addr_dec", + "nat_ne_of_beq_eq_false_addr_dec", + "bool_type_addr_dec", + "eq_refl_addr_dec", + "eq_type_addr" + ]), + ("ixvm_group_45", #[ + "int_add_addr", + "int_mul_addr", + "int_neg_addr", + "int_emod_addr", + "int_ediv_addr", + "int_bmod_addr", + "int_bdiv_addr", + "int_nat_abs_addr", + "int_pow_addr", + "bit_vec_to_nat_addr", + "bit_vec_ult_addr", + "decidable_decide_addr", + "fin_addr", + "int_dec_eq_addr_dec", + "int_dec_le_addr_dec", + "int_dec_lt_addr_dec" + ]), + ("ixvm_group_46", #[ + "int_sub_addr", + "nat_add_addr", + "nat_mul_addr", + "nat_pow_addr", + "nat_gcd_addr", + "nat_mod_addr", + "nat_div_addr", + "nat_land_addr", + "nat_lor_addr", + "nat_shift_left_addr", + "nat_beq_addr", + "nat_ble_addr", + "nat_addr_io", + "nat_dec_le_addr_dec", + "nat_dec_eq_addr_dec", + "nat_dec_lt_addr_dec" + ]), + ("ixvm_group_47", #[ + "system_platform_num_bits_addr", + "subtype_val_addr", + "mk_nat_lit", + "build_recur_addrs", + "level_eq", + "nl_add_const", + "check_prop_field_if_prop", + "validate_univ_params_list", + "check_param_agreement", + "expr_mentions_block", + "build_motive_apps", + "is_rec_field" + ]), + ("ixvm_group_48", #[ + "is_native_prim_addr", + "nl_add_var", + "expr_lbr_let", + "expr_lift_bvar", + "validate_univ_params_seen" + ]), + ("ixvm_group_49", #[ + "try_native_dispatch", + "try_str_dispatch", + "str_lit_to_ctor", + "nlvars_add", + "nlvars_subsume" + ]), + ("ixvm_group_50", #[ + "check_native_bool", + "bitvec_prep_spine_ult", + "build_char_list", + "char_lit_codepoint_syn", + "int_ediv_prim", + "int_bmod_prim", + "nlvars_max_offset", + "nlvars_any_offset_geq", + "canon_ord_cmp_g", + "canon_cmp_krec_rule_list_ctx", + "run_check_env" + ]), + ("ixvm_group_51", #[ + "is_bitvec_prim_addr", + "try_extract_nat_app", + "nl_skip_empty", + "whnf_get_ctor_or_none", + "is_prop_type", + "get_result_sort_level" + ]), + ("ixvm_group_52", #[ + "try_reduce_bit_vec_ult", + "try_str_back", + "walk_char_list_bytes", + "int_bdiv_prim", + "try_quot_ind", + "try_str_dec_eq", + "canon_cmp_u64_lex", + "canon_build_ctx_members", + "canon_insert_sorted" + ]), + ("ixvm_group_53", #[ + "try_bitvec_dispatch", + "try_nat_binop_dispatch", + "glist_cmp", + "nl_add_const_go", + "try_normalize_int_decidable", + "try_dec_dispatch" + ]), + ("ixvm_group_54", #[ + "list_nil_addr", + "list_cons_addr", + "nat_not_le_of_not_ble_eq_true_addr_dec", + "canon_sord_lt_strong", + "canon_sord_eq_strong", + "canon_sord_gt_strong", + "canon_sord_of_g" + ]), + ("ixvm_group_55", #[ + "utf8_validate", + "try_extract_nat", + "glist_eq_len", + "normalize_aux", + "assert_lvls_are_params", + "check_field_universes", + "addr_list_contains", + "wrap_foralls", + "list_reverse_acc.G" + ]), + ("ixvm_group_56", #[ + "utf8_decode_one", + "is_int_prim_addr", + "try_int_prim_dispatch", + "glist_ordered_insert", + "try_iota", + "check_positivity_aug" + ]), + ("ixvm_group_57", #[ + "str_lit_to_ctor_app_or_self", + "level_offset_of", + "ctx_next_cut" + ]), + ("ixvm_group_58", #[ + "klimbs_from_g", + "canon_cmp_kuniv_list", + "canon_cmp_bytes", + "kexpr_struct_eq", + "parse_atree_body" + ]), + ("ixvm_group_59", #[ + "utf8_encode_prepend", + "get_ci_dprj", + "aux_from_recrs_walk_ex", + "find_peer_rec_spec_walk", + "get_reveal_mut_const_info", + "get_reveal_info", + "list_lookup_u64.MutConst" + ]), + ("ixvm_group_60", #[ + "try_extract_int_prim", + "literal_eq", + "is_int_dec_prim_addr", + "try_extract_int", + "check_quot", + "check_nested_ctors_positivity", + "check_large_walk_fields", + "subst_param_for", + "ctor_subst_param_for" + ]), + ("ixvm_group_61", #[ + "int_add_prim", + "normalize_imax_dispatch", + "has_bvar_in_range_let", + "expr_lift_let", + "apply_n_projs", + "se_peel_tol", + "se_mentions", + "count_foralls_at_least", + "check_large_prop_ctor" + ]), + ("ixvm_group_62", #[ + "int_emod_prim", + "canon_ctx_cmp_addr", + "canon_cmp_kuniv", + "canon_cmp_klimbs", + "canon_build_ctx_classes", + "canon_classes_eq", + "extract_aux_spec_params", + "spec_params_lower", + "apply_spec_params_lifted", + "list_snoc.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode" + ]), + ("ixvm_group_63", #[ + "build_succ_offset", + "try_k_synth_iota", + "lazy_delta_step_const_const", + "try_lazy_delta_app", + "dec_rewrite_lt_to_le", + "dec_build_proof", + "compare_rules", + "apply_ihs_full", + "build_minor_at_depth", + "build_ih_doms" + ]), + ("ixvm_group_64", #[ + "convert_univ", + "nl_le_vars", + "level_imax", + "expr_glb_let", + "replace_spine_major", + "k_is_def_eq_slow_nd_after_core", + "check_param_agreement_go", + "check_field_universes_inner" + ]), + ("ixvm_group_65", #[ + "level_is_not_zero", + "nl_subsumption_walk", + "level_inst_params", + "whnf_spine", + "try_proof_irrel" + ]), + ("ixvm_group_66", #[ + "glist_subset", + "nl_subsume_entry", + "try_nat_dispatch_prewhnf", + "try_struct_eta_iota", + "k_infer_proj" + ]), + ("ixvm_group_67", #[ + "nl_covers_var", + "nl_le", + "level_leq", + "find_rule", + "ensure_sort_only", + "level_list_eq", + "unfold_both_and_loop", + "is_inductive_prop", + "peel_field_loop", + "peel_n_lams_collect", + "list_length.KRecRule" + ]), + ("ixvm_group_68", #[ + "level_equal", + "expr_inst1_let", + "expr_inst_many_let", + "k_is_def_eq_struct_go", + "check_positivity_fields", + "check_positivity", + "build_apply_field_bvars" + ]), + ("ixvm_group_69", #[ + "level_struct_eq", + "peel_params_subst", + "k_is_def_eq_structure_tree_app", + "peel_n_alls_whnf" + ]), + ("ixvm_group_70", #[ + "level_max_subsumes", + "k_is_def_eq_slow", + "k_is_def_eq_structure_tree" + ]), + ("ixvm_group_71", #[ + "level_list_inst", + "k_is_def_eq_slow_nd", + "try_unit_like" + ]), + ("ixvm_group_72", #[ + "has_bvar_in_range_binder", + "k_is_def_eq_struct", + "assert_safety" + ]), + ("ixvm_group_73", #[ + "ctx_seek_cut", + "try_unfold_proj_app" + ]), + ("ixvm_group_74", #[ + "ctx_trim", + "try_reduce_projection_definition" + ]), + ("ixvm_group_75", #[ + "expr_has_bvar_at_binder", + "k_is_def_eq_ordered" + ]), + ("ixvm_group_76", #[ + "whnf_proj_head", + "whnf_nd_proj_head" + ]), + ("ixvm_group_77", #[ + "try_reduce_fin_val_decidable_rec", + "prim_family" + ]), + ("ixvm_group_78", #[ + "whnf_struct_core_const", + "k_is_def_eq_struct_spend" + ]), + ("ixvm_group_79", #[ + "const_num_lvls", + "const_type_of" + ]), + ("ixvm_group_80", #[ + "k_infer_only", + "try_eta_struct" + ]), + ("ixvm_group_81", #[ + "k_is_def_eq_core", + "try_def_eq_nat" + ]), + ("ixvm_group_82", #[ + "slow2_after_delta", + "unfold_a_and_loop", + "lazy_delta_both_proj", + "assert_first_args_are_param_bvars", + "check_field_universes_skip_params", + "peel_n_foralls_with_types" + ]) +] end IxVM diff --git a/Tests/Ix/IxVM.lean b/Tests/Ix/IxVM.lean index bfc2b84d4..5beb15798 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -352,85 +352,85 @@ private def nameOfString (str : String) : Lean.Name := listed constant fails the suite, so a regression cannot land quietly and an improvement has to be acknowledged by re-pinning. -/ private def kernelCheckEntries : List (String × Nat) := [ - ("HEq", 129_415_470), - ("HEq.rec", 133_223_427), - ("Eq.rec", 132_596_931), - ("Nat", 129_436_540), - ("Nat.add", 167_868_233), - ("Nat.add_comm", 314_331_886), - ("Nat.decEq", 370_795_262), - ("Nat.decLe", 798_081_474), - ("Nat.sub_le_of_le_add", 1_948_253_617), - ("Nat.shiftRight_succ", 1_439_153_606), - ("Trans.mk", 135_466_677), - ("Array.append_assoc", 9_267_286_835), - ("Vector.append", 9_471_352_620), - ("IxVMPrim.nat_add_lit", 208_274_268), - ("IxVMPrim.nat_sub_lit", 222_435_032), - ("IxVMPrim.nat_mul_lit", 199_841_394), - ("IxVMPrim.nat_mul_big", 198_352_348), - ("IxVMPrim.nat_div_lit", 1_404_697_950), - ("IxVMPrim.nat_mod_lit", 1_431_576_563), - ("IxVMPrim.nat_succ_lit", 143_185_821), - ("IxVMPrim.nat_pred_lit", 163_830_878), - ("IxVMPrim.nat_gcd_lit", 2_210_628_026), - ("IxVMPrim.nat_land_lit", 3_653_494_999), - ("IxVMPrim.nat_lor_lit", 3_655_573_141), - ("IxVMPrim.nat_xor_lit", 3_674_449_748), - ("IxVMPrim.nat_shl_lit", 228_041_403), - ("IxVMPrim.nat_shr_lit", 1_419_823_703), - ("IxVMPrim.nat_pow_big", 391_618_075), - ("IxVMPrim.nat_beq_lit", 197_314_462), - ("IxVMPrim.nat_ble_lit", 192_799_735), - ("IxVMPrim.nat_cases_big", 163_937_210), - ("IxVMPrim.nat_dec_le", 815_683_083), - ("IxVMPrim.nat_dec_lt", 826_672_702), - ("IxVMPrim.nat_dec_eq", 408_940_371), - ("IxVMPrim.str_size_lit", 2_531_391_753), - ("IxVMPrim.bv_to_nat_lit", 2_107_059_382), - ("IxVMInd.Even", 202_133_976), - ("IxVMInd.Odd", 202_138_603), - ("IxVMInd.Even.rec", 219_913_382), - ("IxVMInd.Odd.rec", 219_912_453), - ("IxVMInd.IdxTeleN.rec", 158_099_596), - ("IxVMInd.IdxTeleB.rec", 158_097_905), - ("IxVMInd.SoloA.rec", 153_633_594), - ("IxVMInd.SoloB.rec", 153_632_757), - ("IxVMInd.UnsafeSquash", 131_133_753), - ("IxVMInd.Tree", 130_813_148), - ("IxVMInd.Tree.rec", 140_400_054), - ("IxVMInd.DedupM", 133_854_318), - ("IxVMInd.DedupM.rec", 146_734_266), - ("IxVMInd.DepthM", 132_406_572), - ("IxVMInd.DepthM.rec", 142_909_654), - ("String.Internal.append", 2_501_652_777), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 3_730_569_331), - ("Lean.Syntax.rec", 2_558_942_599), - ("IxVMInd.AuxTie", 315_323_114), - ("IxVMInd.AuxTie.rec", 357_605_752), - ("IxVMInd.HiddenIdx", 130_343_481), - ("IxVMInd.HiddenIdx.rec", 133_347_150), - ("IxVMInd.thmMajorUse", 511_421_317), - ("IxVMInd.partialKRec", 148_742_691), - ("IxVMInd.deepRebase", 216_591_459), - ("String.Slice.Pattern.Model.NoPrefixPatternModel.rec", 3_485_771_407), - ("Lean.Widget.TaggedText.rec", 2_531_498_592), - ("Lean.Doc.Part.rec", 2_572_953_643), - ("Lean.Doc.Block.rec", 2_805_884_331), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 132_004_150), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 135_241_018), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 134_322_394), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 134_322_394), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 134_322_394), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 132_255_319), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 143_018_650), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 143_017_067), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 134_322_394), - ("strOfListFoldSize", 2_813_850_907), - ("strOfListFoldSizeAscii", 2_814_672_191), - ("IxVMPrim.lazy_ble_offset", 229_149_821), - ("IxVMPrim.lazy_unit_cast", 546_072_520), - ("IxVMPrim.sizeof_unit", 158_832_181), + ("HEq", 129_564_490), + ("HEq.rec", 133_835_821), + ("Eq.rec", 133_138_390), + ("Nat", 129_621_511), + ("Nat.add", 170_281_370), + ("Nat.add_comm", 321_324_560), + ("Nat.decEq", 378_272_240), + ("Nat.decLe", 815_724_966), + ("Nat.sub_le_of_le_add", 1_978_749_695), + ("Nat.shiftRight_succ", 1_465_492_882), + ("Trans.mk", 137_285_211), + ("Array.append_assoc", 9_392_514_200), + ("Vector.append", 9_599_238_332), + ("IxVMPrim.nat_add_lit", 212_940_808), + ("IxVMPrim.nat_sub_lit", 227_419_004), + ("IxVMPrim.nat_mul_lit", 203_336_609), + ("IxVMPrim.nat_mul_big", 201_846_122), + ("IxVMPrim.nat_div_lit", 1_429_722_214), + ("IxVMPrim.nat_mod_lit", 1_457_032_266), + ("IxVMPrim.nat_succ_lit", 144_205_846), + ("IxVMPrim.nat_pred_lit", 165_895_387), + ("IxVMPrim.nat_gcd_lit", 2_246_460_709), + ("IxVMPrim.nat_land_lit", 3_702_449_683), + ("IxVMPrim.nat_lor_lit", 3_704_556_317), + ("IxVMPrim.nat_xor_lit", 3_723_893_052), + ("IxVMPrim.nat_shl_lit", 233_004_581), + ("IxVMPrim.nat_shr_lit", 1_445_101_184), + ("IxVMPrim.nat_pow_big", 399_051_503), + ("IxVMPrim.nat_beq_lit", 201_055_250), + ("IxVMPrim.nat_ble_lit", 196_415_590), + ("IxVMPrim.nat_cases_big", 166_089_142), + ("IxVMPrim.nat_dec_le", 833_697_241), + ("IxVMPrim.nat_dec_lt", 845_266_268), + ("IxVMPrim.nat_dec_eq", 417_837_609), + ("IxVMPrim.str_size_lit", 2_577_695_936), + ("IxVMPrim.bv_to_nat_lit", 2_145_356_704), + ("IxVMInd.Even", 206_790_322), + ("IxVMInd.Odd", 206_794_948), + ("IxVMInd.Even.rec", 225_871_765), + ("IxVMInd.Odd.rec", 225_870_836), + ("IxVMInd.IdxTeleN.rec", 160_998_572), + ("IxVMInd.IdxTeleB.rec", 160_996_881), + ("IxVMInd.SoloA.rec", 156_111_821), + ("IxVMInd.SoloB.rec", 156_110_984), + ("IxVMInd.UnsafeSquash", 131_444_123), + ("IxVMInd.Tree", 131_234_444), + ("IxVMInd.Tree.rec", 142_073_111), + ("IxVMInd.DedupM", 134_569_673), + ("IxVMInd.DedupM.rec", 149_126_381), + ("IxVMInd.DepthM", 132_969_322), + ("IxVMInd.DepthM.rec", 144_766_356), + ("String.Internal.append", 2_547_985_001), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 3_792_209_247), + ("Lean.Syntax.rec", 2_610_636_692), + ("IxVMInd.AuxTie", 324_670_938), + ("IxVMInd.AuxTie.rec", 371_234_512), + ("IxVMInd.HiddenIdx", 130_537_130), + ("IxVMInd.HiddenIdx.rec", 133_953_988), + ("IxVMInd.thmMajorUse", 524_278_831), + ("IxVMInd.partialKRec", 150_274_713), + ("IxVMInd.deepRebase", 221_419_382), + ("String.Slice.Pattern.Model.NoPrefixPatternModel.rec", 3_543_958_284), + ("Lean.Widget.TaggedText.rec", 2_580_667_020), + ("Lean.Doc.Part.rec", 2_627_121_877), + ("Lean.Doc.Block.rec", 2_873_716_428), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 132_540_159), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 136_184_734), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 135_211_941), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 135_211_941), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 135_211_941), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 132_835_418), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 144_932_554), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 144_930_972), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 135_211_941), + ("strOfListFoldSize", 2_863_685_734), + ("strOfListFoldSizeAscii", 2_864_527_734), + ("IxVMPrim.lazy_ble_offset", 234_266_803), + ("IxVMPrim.lazy_unit_cast", 558_018_744), + ("IxVMPrim.sizeof_unit", 160_837_922), ] /-- Variant of `kernelChecks`, pinned to the baseline diff --git a/Tests/Main.lean b/Tests/Main.lean index b22bc92e1..fb6d83d8b 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -276,8 +276,8 @@ def ignoredRunners (env : Lean.Environment) : List (String × IO UInt32) := [ let actual := (Aiur.computeStats v2Env.compiled qc v2Env.shapes).totalFftCost.round.toUInt64.toNat pure (LSpec.test - s!"Shard pipeline FFT matches: expected 6_859_583_032, got {actual}" - (actual = 6_859_583_032)) + s!"Shard pipeline FFT matches: expected 6_946_001_069, got {actual}" + (actual = 6_946_001_069)) LSpec.lspecIO (.ofList [("ixvm", [fullSeq, aiurSeq, arenaSeq, exploitSeq, paritySeq, shardSeq])]) []), From c5c900c4f850faba4c692b6d29aa1cddc7d2bccb Mon Sep 17 00:00:00 2001 From: Gabriel Barreto Date: Tue, 8 Sep 2026 18:29:06 +0000 Subject: [PATCH 4/4] aiur: IX_NO_FUNCTION_GROUPS switches function grouping off process-wide For testing and measurement against the ungrouped systems without editing the data files: when the variable is set to anything but `0` or the empty string, `compileWithGroups` ignores its grouping and compiles the singleton partition, at every site that applies one (kernel, ix_aggr, standalone verifier). Read once per process through an `implemented_by` opaque, so the pure compile path stays pure. The prover and the verifier must see the same setting - grouping changes the verifying key. --- Ix/Aiur/Compiler.lean | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/Ix/Aiur/Compiler.lean b/Ix/Aiur/Compiler.lean index 39fe13956..5eb558e18 100644 --- a/Ix/Aiur/Compiler.lean +++ b/Ix/Aiur/Compiler.lean @@ -209,11 +209,33 @@ def Source.Toplevel.compile (t : Source.Toplevel) : Except String CompiledToplev circuits := bytecode.singletonCircuits fun i => reverseMap[i]?.getD s!"" } pure (CompiledToplevel.mk t bytecode nameMap) +/-- Name of the environment variable that switches function grouping OFF +process-wide: when it is set to anything but `0` or the empty string, +`compileWithGroups` ignores its grouping and compiles the singleton +partition. For testing and measurement only - the prover and the verifier +must see the same setting, since grouping changes the verifying key. -/ +def noFunctionGroupsEnvVar : String := "IX_NO_FUNCTION_GROUPS" + +unsafe def functionGroupsDisabledUnsafe (_ : Unit) : Bool := + match unsafeBaseIO (IO.getEnv noFunctionGroupsEnvVar) with + | some v => v != "0" && v != "" + | none => false + +@[implemented_by functionGroupsDisabledUnsafe] +opaque functionGroupsDisabledImpl (_ : Unit) : Bool := false + +/-- Whether `IX_NO_FUNCTION_GROUPS` disables function grouping in this +process (see `noFunctionGroupsEnvVar`). -/ +def functionGroupsDisabled : Bool := functionGroupsDisabledImpl () + /-- `compile`, then apply a function grouping (see -`CompiledToplevel.groupFunctions`). -/ +`CompiledToplevel.groupFunctions`) - unless `IX_NO_FUNCTION_GROUPS` is set +(see `noFunctionGroupsEnvVar`), in which case the grouping is ignored and +every constrained function keeps its singleton circuit. -/ def Source.Toplevel.compileWithGroups (t : Source.Toplevel) (groups : Array (String × Array String)) : Except String CompiledToplevel := do - (← t.compile).groupFunctions groups + let compiled ← t.compile + if functionGroupsDisabled then pure compiled else compiled.groupFunctions groups /-- Progress helper: given success of the three `Except`-returning stages, `compile` as a whole returns `.ok` (the remaining stages — `deduplicate`,