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 cef51cdae..5eb558e18 100644 --- a/Ix/Aiur/Compiler.lean +++ b/Ix/Aiur/Compiler.lean @@ -42,6 +42,73 @@ 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 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) := #[] + 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 := byName[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 +157,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,13 +197,46 @@ 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) +/-- 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`) - 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 + 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`, `needsCircuit`, the field-setter `mapIdx`, the name-map `fold`, and the 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/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..27820e1fb --- /dev/null +++ b/Ix/IxVM/FunctionGroups.lean @@ -0,0 +1,850 @@ +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 + +-- 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 + +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 833aa509d..cf1a890bf 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 String) := + #[("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..afd13803d 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 String) := #[]) : 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/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 94fc62a94..fb6d83d8b 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 @@ -215,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 => @@ -266,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])]) []), 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! 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