diff --git a/Benchmarks/RecursionDebug.lean b/Benchmarks/RecursionDebug.lean index 8bc20302..847c91ab 100644 --- a/Benchmarks/RecursionDebug.lean +++ b/Benchmarks/RecursionDebug.lean @@ -70,7 +70,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.coldGroups | IO.eprintln "IxVM compile failed"; return none let entrypoint := if skipDeps then `verify_const else `verify_claim let some funIdx := compiled.getFuncIdx entrypoint @@ -153,7 +153,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.verifierColdGroups | IO.eprintln "multi-stark verifier compile failed"; return 1 let entries := vCompiled.nameMap.toArray.qsort (·.2 < ·.2) for (g, i) in entries do @@ -187,7 +187,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.verifierColdGroups | 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/RecursiveVerifier.lean b/Benchmarks/RecursiveVerifier.lean index e99d1f61..ed4ab5e3 100644 --- a/Benchmarks/RecursiveVerifier.lean +++ b/Benchmarks/RecursiveVerifier.lean @@ -147,7 +147,7 @@ def main (args : List String) : IO UInt32 := do let vTop ← match MultiStark.multiStark with | .ok t => pure t | .error e => IO.eprintln s!"verifier merge failed: {e}"; return 1 - let vCompiled ← match vTop.compile with + let vCompiled ← match vTop.compileWithGroups MultiStark.verifierColdGroups with | .ok c => pure c | .error e => IO.eprintln s!"verifier compile failed: {e}"; return 1 let vIdx := vCompiled.getFuncIdx `verify_multi_stark_proof |>.get! diff --git a/Benchmarks/Typecheck.lean b/Benchmarks/Typecheck.lean index 5d3e6ede..bebde57a 100644 --- a/Benchmarks/Typecheck.lean +++ b/Benchmarks/Typecheck.lean @@ -329,7 +329,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.coldGroups | throw (IO.userError "Compilation of IxVM kernel failed") let entrypoint := if skipDeps then `verify_const else `verify_claim let some funIdx := compiled.getFuncIdx entrypoint @@ -358,7 +358,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.verifierColdGroups | 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") diff --git a/Ix/Aiur/Compiler.lean b/Ix/Aiur/Compiler.lean index d8526663..0fe32a89 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,24 @@ 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) +/-- `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/Aiur/Compiler/Lower.lean b/Ix/Aiur/Compiler/Lower.lean index 4cc3dc33..136df82e 100644 --- a/Ix/Aiur/Compiler/Lower.lean +++ b/Ix/Aiur/Compiler/Lower.lean @@ -631,7 +631,7 @@ def Concrete.Decls.toBytecode (decls : Concrete.Decls) : let memSizes := layoutMState.memSizes.fold (·.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 acd8e257..21c52fd6 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 aa91de16..05603516 100644 --- a/Ix/Aiur/Statistics.lean +++ b/Ix/Aiur/Statistics.lean @@ -45,6 +45,13 @@ structure CircuitStats where /-- FFT cost at the uncached height `height + cacheHits` (fixed-height gadget circuits keep their normal cost). Feeds `totalUncachedFftCost`. -/ uncachedFftCost : Float + -- TEMP (grouping instrumentation, revert with this commit): the circuit + -- layout shape, for picking group members — merging is cheapest between + -- circuits whose auxiliaries and lookups are CLOSE (both merge by max; + -- selectors sum). Zero for memory/gadget circuits (no function layout). + selectors : Nat := 0 + auxiliaries : Nat := 0 + lookups : Nat := 0 structure ExecutionStats where circuits : Array CircuitStats @@ -81,44 +88,39 @@ 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 with + selectors := c.layout.selectors, auxiliaries := c.layout.auxiliaries, + lookups := c.layout.lookups } 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) @@ -169,9 +171,14 @@ def printStats (stats : ExecutionStats) : IO Unit := do let n := f.round.toUInt64.toNat toString n let wFftCost := stats.circuits.foldl (fun m cs => Nat.max m (formatSci cs.fftCost).length) 8 + -- TEMP (grouping instrumentation, revert with this commit) + let wSel := stats.circuits.foldl (fun m cs => Nat.max m (toString cs.selectors).length) 3 + let wAux := stats.circuits.foldl (fun m cs => Nat.max m (toString cs.auxiliaries).length) 3 + let wLkp := stats.circuits.foldl (fun m cs => Nat.max m (toString cs.lookups).length) 3 let wPct := 7 let wCum := 7 - let totalW := wName + 1 + wWidth + 1 + wHeight + 1 + wHits + 1 + wFftCost + 1 + wPct + 1 + wCum + let totalW := wName + 1 + wWidth + 1 + wSel + 1 + wAux + 1 + wLkp + 1 + + wHeight + 1 + wHits + 1 + wFftCost + 1 + wPct + 1 + wCum let totalWidth := stats.circuits.foldl (· + ·.width) 0 let savedPct := if stats.totalUncachedFftCost == 0.0 then "0.00%" @@ -184,14 +191,14 @@ def printStats (stats : ExecutionStats) : IO Unit := do IO.println s!"Total cache hits: {stats.totalCacheHits}" IO.println s!"Total saved cost: {savedPct}" IO.println sep - IO.println s!"{padRight "Name" wName} {padLeft "Width" wWidth} {padLeft "Height" wHeight} {padLeft "Hits" wHits} {padLeft "FFT cost" wFftCost} {padLeft "%" wPct} {padLeft "%++" wCum}" + IO.println s!"{padRight "Name" wName} {padLeft "Width" wWidth} {padLeft "Sel" wSel} {padLeft "Aux" wAux} {padLeft "Lkp" wLkp} {padLeft "Height" wHeight} {padLeft "Hits" wHits} {padLeft "FFT cost" wFftCost} {padLeft "%" wPct} {padLeft "%++" wCum}" IO.println sep let mut cumFftCost : Float := 0.0 for cs in stats.circuits do cumFftCost := cumFftCost + cs.fftCost let pct := formatPercent cs.fftCost stats.totalFftCost let cum := formatPercent cumFftCost stats.totalFftCost - IO.println s!"{padRight cs.name wName} {padLeft (toString cs.width) wWidth} {padLeft (toString cs.height) wHeight} {padLeft (toString cs.cacheHits) wHits} {padLeft (formatSci cs.fftCost) wFftCost} {padLeft pct wPct} {padLeft cum wCum}" + IO.println s!"{padRight cs.name wName} {padLeft (toString cs.width) wWidth} {padLeft (toString cs.selectors) wSel} {padLeft (toString cs.auxiliaries) wAux} {padLeft (toString cs.lookups) wLkp} {padLeft (toString cs.height) wHeight} {padLeft (toString cs.cacheHits) wHits} {padLeft (formatSci cs.fftCost) wFftCost} {padLeft pct wPct} {padLeft cum wCum}" end Aiur diff --git a/Ix/Cli/CheckCmd.lean b/Ix/Cli/CheckCmd.lean index 56553878..ef647116 100644 --- a/Ix/Cli/CheckCmd.lean +++ b/Ix/Cli/CheckCmd.lean @@ -656,7 +656,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.coldGroups 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) @@ -669,7 +669,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.coldGroups with | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c return (← runShardCheckManifestNative manifest ixe k compiled printStats statsOut useBytecode) @@ -678,7 +678,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.coldGroups with | .error e => IO.eprintln s!"Compilation failed: {e}"; return 1 | .ok c => pure c return (← runShardManifestAllNative manifest ixe diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean index a35609d9..787853b3 100644 --- a/Ix/Cli/ProveCmd.lean +++ b/Ix/Cli/ProveCmd.lean @@ -146,7 +146,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.coldGroups 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/VerifyCmd.lean b/Ix/Cli/VerifyCmd.lean index 38135257..c2262b0d 100644 --- a/Ix/Cli/VerifyCmd.lean +++ b/Ix/Cli/VerifyCmd.lean @@ -73,7 +73,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.coldGroups with | .error e => return .error s!"compilation failed: {e}" | .ok compiled => return .ok (Aiur.AiurSystem.build compiled.bytecode commitmentParameters friParameters, compiled) diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean index 45c6b898..0add2290 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.ColdGroups public import Ix.IxVM.ByteStream public import Ix.IxVM.Blake3 public import Ix.IxVM.RBTreeMap diff --git a/Ix/IxVM/ColdGroups.lean b/Ix/IxVM/ColdGroups.lean new file mode 100644 index 00000000..236c3c6d --- /dev/null +++ b/Ix/IxVM/ColdGroups.lean @@ -0,0 +1,826 @@ +module + +/-! +Circuit-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 + +-- Shape-proximity bands over cold circuits (max FFT share < 0.5% on the +-- String.split / Array.extract_append kernel-check workloads; aux within +-- 1.6x, lookups within max(2x, +4), summed selectors <= 40; verify_claim +-- excluded as the entry). 85 bands over 630 of 709 function circuits: +-- 730 -> 185 circuits. See cold-groups/kernel-shape-grouping2.md. +def coldGroups : Array (String × Array String) := #[ + ("k_shape_00", #[ + "canon_kind_ord", + "canon_sord_eq_strong", + "canon_sord_gt_strong", + "canon_sord_lt_strong", + "canon_sord_of_g", + "check_opt_bool", + "check_opt_u64", + "const_num_lvls", + "const_type_of", + "def_safety_tag", + "flatten_u64" + ]), + ("k_shape_01", #[ + "pack_def_kind_safety", + "quot_kind_tag", + "unpack_def_kind_safety", + "check_opt_ctor_entries", + "check_opt_recr_rules" + ]), + ("k_shape_02", #[ + "canon_ord_then", + "canon_sord_then", + "defn_is_unsafe_ci", + "delta_rank", + "is_unsafe_ci", + "lbr_dec", + "relaxed_u64_pred", + "relaxed_u64_succ" + ]), + ("k_shape_03", #[ + "u64_eq", + "u64_is_zero", + "addr_set_member", + "assert_wire_bool", + "bit_vec_addr", + "bit_vec_of_nat_addr", + "bit_vec_to_nat_addr", + "bit_vec_ult_addr", + "bool_false_addr", + "bool_true_addr", + "bool_type_addr_dec", + "build_all_minors", + "build_all_motives", + "build_recur_addrs", + "byte_array_empty_addr", + "canon_addr_chunk", + "canon_cmp_kliteral", + "char_of_nat_addr", + "char_type_addr", + "check_parent_inductive_shape" + ]), + ("k_shape_04", #[ + "decidable_decide_addr", + "decidable_is_false_addr_dec", + "decidable_is_true_addr_dec", + "decidable_rec_addr", + "eq_refl_addr_dec", + "fin_addr", + "int_dec_eq_addr_dec", + "int_dec_le_addr_dec", + "int_dec_lt_addr_dec", + "int_neg_succ_addr_dec", + "int_of_nat_addr_dec", + "k_is_def_eq_struct", + "klimbs_add", + "list_cons_addr", + "list_nil_addr", + "literal_eq", + "lt_lt_addr", + "mk_nat_lit", + "nat_add_addr", + "nat_addr_io", + "nat_beq_addr", + "nat_ble_addr", + "nat_dec_eq_addr_dec", + "nat_dec_le_addr_dec", + "nat_dec_lt_addr_dec", + "nat_div_addr", + "nat_eq_of_beq_eq_true_addr_dec", + "nat_gcd_addr", + "nat_land_addr", + "nat_le_of_ble_eq_true_addr_dec", + "nat_lor_addr", + "nat_mod_addr", + "nat_mul_addr", + "nat_ne_of_beq_eq_false_addr_dec", + "nat_not_le_of_not_ble_eq_true_addr_dec", + "nat_pow_addr", + "nat_pred_addr" + ]), + ("k_shape_05", #[ + "nat_shift_left_addr", + "nat_shift_right_addr", + "nat_sub_addr", + "nat_succ_addr_iota", + "nat_xor_addr", + "nat_zero_addr", + "punit_addr", + "punit_size_of_1_addr", + "put_constant_info", + "put_quot_kind", + "quot_ctor_addr", + "quot_ind_addr", + "quot_lift_addr_iota", + "quot_type_addr", + "reduce_bool_addr", + "reduce_nat_addr", + "size_of_size_of_addr", + "str_addr", + "string_append_addr", + "string_back_addr", + "string_dec_eq_addr", + "string_legacy_back_addr", + "string_of_list_addr", + "string_to_byte_array_addr", + "string_utf8_byte_size_addr", + "subtype_val_addr", + "system_platform_get_num_bits_addr", + "system_platform_num_bits_addr", + "unit_addr", + "utf8_last_codepoint" + ]), + ("k_shape_06", #[ + "check_param_agreement", + "is_defn_or_thm", + "assert_safety", + "build_ctor_app_params", + "extract_aux_spec_params_from_rec", + "is_rec_field", + "klimbs_div", + "klimbs_mod", + "check_opt_def_kind", + "check_opt_def_safety", + "check_opt_quot_kind", + "convert_axiom", + "convert_quotient", + "has_bvar_in_range_binder", + "k_check", + "klimbs_mul", + "list_reverse.G", + "put_definition_proj", + "put_mut_const", + "run_contains", + "utf8_cont", + "check_inductive_shape" + ]), + ("k_shape_07", #[ + "get_opt_addr_masked", + "get_opt_bool_masked", + "get_opt_def_kind_masked", + "get_opt_quot_kind_masked", + "list_is_empty.U8", + "defn_member_recur_addrs", + "expr_inst1_bvar", + "k_is_def_eq_ordered", + "klimbs_shl_limbs", + "klimbs_sub", + "pad_block", + "put_u64_le", + "try_unfold_head", + "env_walk_leaves", + "expr_glb_binder" + ]), + ("k_shape_08", #[ + "has_bvar_in_range_let", + "k_infer", + "k_infer_lit", + "klimbs_dec", + "klimbs_gcd", + "mk_nat_literal_64", + "mk_nat_one", + "put_constructor_proj", + "validate_univ_params_list", + "get_opt_addr", + "list_lookup_or_default.Ptr.U8_32", + "nl_add_const", + "read_byte", + "apply_indices_in_conclusion", + "apply_n_projs", + "build_apply_field_bvars", + "build_apply_xs", + "build_major_params", + "build_motive_apps", + "build_param_lvls_range", + "build_rec_lvls_list" + ]), + ("k_shape_09", #[ + "canon_ctor_ctx_entries", + "check_prop_field_if_prop", + "mk_bool", + "np_whnf_inner_bv", + "peel_leading_foralls", + "unfold_a_and_loop", + "unfold_b_and_loop", + "check_positivity", + "expr_inst1_let", + "expr_inst_many_let", + "expr_lift_let", + "klimbs_shl", + "klimbs_shr", + "leaf_hash", + "level_equal", + "count_foralls_body", + "expr_inst_levels", + "level_offset_of", + "skip_bytes", + "canon_all_singleton", + "canon_flatten", + "canon_ins_sort", + "canon_refine_one" + ]), + ("k_shape_10", #[ + "check_field_universes", + "check_rec_rules_wellscoped", + "convert_definition", + "ctx_next_cut", + "level_max_subsumes", + "list_reverse_acc.G", + "put_address_list", + "utf8_validate", + "wrap_foralls", + "wrap_lams", + "check_positivity_fields", + "check_quot", + "env_walk_refs", + "put_tag0", + "put_tag2" + ]), + ("k_shape_11", #[ + "put_tag4", + "try_proof_irrel", + "walk_refs_transitive", + "convert_constructor", + "convert_inductive", + "expr_glb_let", + "node_hash", + "rbtree_map_insert.G", + "check_native_nat", + "count_foralls_at_least", + "level_explicit_val", + "list_length.KRecRule", + "peel_n_foralls", + "rbtree_map_balance.G", + "se_peel_tol", + "addr_list_contains", + "all_bvars_in_args" + ]), + ("k_shape_12", #[ + "char_lit_codepoint", + "check_field_universes_skip_params", + "is_large_eliminator", + "is_nat_zero", + "k_ensure_sort", + "k_is_def_eq_slow", + "level_is_not_zero", + "list_any_mentions_block", + "list_concat.Tup.Ptr.U8_32.G", + "list_take.Ptr.KExprNode", + "se_addr_in", + "str_lit_to_ctor_app_or_self" + ]), + ("k_shape_13", #[ + "utf8_last_go", + "apply_spec_params_lifted", + "canon_cmp_member_ctx", + "canon_group_consec", + "canon_refine_classes", + "check_no_dep_data_field_if_prop", + "compare_struct_fields", + "const_idxs_exprs", + "level_inst_params", + "level_list_inst", + "level_reduce", + "list_lift_each", + "list_lift_indices", + "nl_subsumption_walk", + "whnf_spine" + ]), + ("k_shape_14", #[ + "const_idxs_of", + "k_is_def_eq", + "try_unit_like", + "canon_cmp_klimbs", + "expr_lbr_let", + "mk_nat_binop_stuck", + "replace_spine_major" + ]), + ("k_shape_15", #[ + "list_length.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode", + "assert_lvls_are_params", + "canon_ctx_class_idx", + "canon_g_list_eq", + "check_large_prop_ctor", + "glist_eq_len", + "peel_leading_foralls_acc", + "se_scan_fields", + "canon_build_ctx_classes", + "canon_cmp_krec_rule_ctx", + "get_expr_let", + "nl_le_vars", + "normalize_aux" + ]), + ("k_shape_16", #[ + "try_string_lit_one", + "canon_ctx_cmp_addr", + "canon_sort_loop", + "check_field_universes_inner", + "intern_int_lit", + "spec_params_lower", + "try_quot_iota", + "unfold_both_and_loop", + "convert_recursor", + "assert_first_args_are_param_bvars", + "assert_occ_param_bvars", + "head_addr", + "list_snoc.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode", + "peel_n_foralls_with_types", + "check_rec_major_spine", + "get_result_sort_level" + ]), + ("k_shape_17", #[ + "io_peel_field_loop", + "level_list_struct_eq", + "peel_motive_params_subst", + "peel_n_alls_whnf", + "spec_params_ptr_eq", + "try_extract_nat", + "whnf_get_ctor_or_none", + "expr_inst_levels_walk", + "is_inductive_prop", + "k_is_def_eq_slow_nd" + ]), + ("k_shape_18", #[ + "level_leq", + "peel_field_loop", + "level_normalize", + "u64_and", + "u64_or", + "u64_xor_kbits" + ]), + ("k_shape_19", #[ + "find_rule", + "args_contain_bvar", + "peel_n_lams_collect", + "build_peer_recs", + "canon_classes_eq", + "de_args", + "expr_mentions_block" + ]), + ("k_shape_20", #[ + "lazy_delta_loop", + "level_eq", + "level_list_eq", + "canon_cmp_bytes" + ]), + ("k_shape_21", #[ + "canon_cmp_kuniv", + "canon_cmp_kuniv_list", + "extract_aux_spec_params", + "idx_to_u64", + "normalize_imax_dispatch", + "spec_params_dom_prefix_match", + "check_native_bool" + ]), + ("k_shape_22", #[ + "is_bitvec_prim_addr", + "is_int_dec_prim_addr", + "lazy_delta_both_proj", + "whnf_nd_apply_beta", + "canonical_rules_at_pos", + "mk_nat_offset_stuck" + ]), + ("k_shape_23", #[ + "get_opt_u64_masked", + "flat_find_pos", + "put_refs", + "put_sharing", + "put_univs", + "try_eta_swap", + "aux_already_in", + "is_prop_type", + "level_struct_eq", + "nl_skip_empty", + "peel_params_subst" + ]), + ("k_shape_24", #[ + "se_mentions", + "whnf_nd_with_spine", + "nl_covers_var", + "parse_atree_body", + "try_extract_nat_app", + "try_unfold_proj_app", + "klimbs_from_g", + "get_inductive_proj", + "list_length.U8_8", + "canon_cmp_kexpr_ctx", + "ensure_sort_only" + ]), + ("k_shape_25", #[ + "flat_member_at", + "rec_to_parent_addr", + "check_param_agreement_go", + "k_is_def_eq_struct_safe", + "nl_le", + "nlvars_eq" + ]), + ("k_shape_26", #[ + "build_char_list", + "build_motive_type_flat", + "k_def_eq_rebase", + "klimbs_pow" + ]), + ("k_shape_27", #[ + "get_opt_ctor_entry_list_masked", + "get_opt_rule_list_masked", + "klimbs_is_zero", + "klimbs_le", + "list_snoc.U8_8", + "put_u64_list", + "convert_univ", + "se_parent_addr" + ]), + ("k_shape_28", #[ + "kexpr_struct_eq", + "level_imax", + "lbr_max", + "lbr_min" + ]), + ("k_shape_29", #[ + "level_max_go", + "memo_u32_less_than", + "bitvec_of_nat_args_direct", + "glimbs_to_klimbs", + "quot_extract_arg", + "bv_to_nat_via", + "nl_add_var", + "check_ctor_return_type" + ]), + ("k_shape_30", #[ + "canon_member_num_ctors", + "put_recursor_rule_list", + "run_check", + "get_axiom", + "extract_aux_occ_us", + "whnf", + "whnf_nd" + ]), + ("k_shape_31", #[ + "canon_ord_cmp_g", + "put_constant", + "walk_fields_classify", + "check_large_walk_fields", + "expr_lift_bvar", + "dec_dispatch_le_eq", + "nat_lit_to_ctor_or_self", + "try_eta_expand", + "klimbs_div_mod", + "dec_rewrite_lt_to_le" + ]), + ("k_shape_32", #[ + "assert_return_head_is_parent", + "caddr_is_peer", + "canon_member_ci", + "check_eq_type", + "check_muts_member_at", + "const_idxs_rules", + "flat_find_matching", + "get_quotient", + "put_univ_list", + "get_address_list", + "get_all_telescope", + "get_expr_list", + "get_lam_telescope", + "collect_index_doms", + "compute_iprj_addr", + "k_is_def_eq_core" + ]), + ("k_shape_33", #[ + "bitvec_prep_spine", + "build_rule_rhs" + ]), + ("k_shape_34", #[ + "addr_set_build", + "struct_is_rec", + "convert_rec_rules", + "run_check_env", + "collect_n_doms_whnf", + "convert_univ_idxs", + "is_rec_field_peel", + "klimbs_mul_outer", + "try_def_eq_nat", + "peel_ctor_params_subst", + "validate_univ_params_seen" + ]), + ("k_shape_35", #[ + "bitvec_prep_spine_ult", + "ctx_seek_cut", + "normalize_int_dec_rebuild", + "canon_cmp_u64_lex", + "u64_add", + "u64_sub_with_borrow" + ]), + ("k_shape_36", #[ + "flat_find_pos_kind", + "canon_cmp_krec_rule_list_ctx", + "check_valid_ind_app", + "level_max", + "subst_param_for", + "try_match_nat_add", + "check_inductive_shape_ctors", + "ctor_subst_param_for", + "ctx_close_cut" + ]), + ("k_shape_37", #[ + "get_definition", + "populate_rules", + "char_lit_codepoint_syn", + "try_def_eq_app", + "level_max_offsets", + "nl_eq", + "try_k_synth_iota" + ]), + ("k_shape_38", #[ + "univ_succ_base", + "struct_scan_ctors", + "build_minor_doms" + ]), + ("k_shape_39", #[ + "cleanup_nat_offset_major", + "nlvars_any_offset_geq", + "nlvars_dominates", + "nlvars_max_offset", + "ctx_trim", + "is_dec_prim_addr", + "is_native_prim_addr", + "try_nat_offset_dispatch" + ]), + ("k_shape_40", #[ + "bytes_to_u64_limb", + "list_length_u64.Ptr.Univ", + "build_rec_type", + "build_succ_chain" + ]), + ("k_shape_41", #[ + "check_nested_ctors_positivity", + "try_extract_int", + "k_is_def_eq_slow2", + "check_const" + ]), + ("k_shape_42", #[ + "get_constructor_proj", + "put_recursor_rule" + ]), + ("k_shape_43", #[ + "expr_addr", + "put_axiom", + "put_quotient", + "get_u64_list", + "put_univ", + "delta_unfold" + ]), + ("k_shape_44", #[ + "nl_add_const_go", + "try_quot_ind", + "try_quot_lift", + "walk_char_list_bytes", + "is_str_prim_addr" + ]), + ("k_shape_45", #[ + "get_tag0", + "get_tag2", + "klimbs_eq", + "klimbs_succ", + "collect_spine_of_ctor", + "whnf_nd_const_head", + "compute_k_target", + "canon_cprj_addr" + ]), + ("k_shape_46", #[ + "nat_offset_of", + "projection_addr_ctor", + "projection_definition_info", + "canon_cmp_ctor_pair_ctx", + "try_bitvec_dispatch" + ]), + ("k_shape_47", #[ + "ctors_before_pos", + "put_expr_list", + "build_flat_own_params", + "canon_cmp_klimbs_tail", + "get_recursor_rule_list", + "get_univ_list", + "build_all_minors_walk", + "build_all_motives_walk", + "lazy_delta_a_const_b_proj", + "lazy_delta_b_const_a_proj", + "whnf_iota_major" + ]), + ("k_shape_48", #[ + "nl_covers_const", + "canon_build_ctx_members", + "check_recursor_member", + "try_nat_binop_dispatch", + "try_reduce_bit_vec_ult", + "build_ih_doms" + ]), + ("k_shape_49", #[ + "klimbs_normalize", + "put_constructor" + ]), + ("k_shape_50", #[ + "is_nat_succ_ih_step", + "try_normalize_int_decidable", + "try_reduce_subtype_val", + "try_str_to_byte_array", + "try_dec_dispatch" + ]), + ("k_shape_51", #[ + "try_nat_linear_rec", + "try_str_back" + ]), + ("k_shape_52", #[ + "rbtree_map_lookup_or_default.G", + "whnf_nd_proj_head", + "whnf_proj_head", + "bytes_to_limbs", + "has_bvar_in_range", + "try_str_dec_eq", + "try_reduce_size_of_unit" + ]), + ("k_shape_53", #[ + "build_rec_type_from", + "k_synth_gate", + "dec_build_proof", + "apply_ihs_full" + ]), + ("k_shape_54", #[ + "klimbs_land", + "klimbs_lor", + "klimbs_xor_op" + ]), + ("k_shape_55", #[ + "str_lit_delta_step", + "glist_ordered_insert", + "try_nat_dispatch_prewhnf" + ]), + ("k_shape_56", #[ + "glist_cmp", + "glist_subset", + "utf8_decode_one", + "dec_finish" + ]), + ("k_shape_57", #[ + "verify_bytes_against", + "get_univ" + ]), + ("k_shape_58", #[ + "canon_insert_sorted", + "bytes_to_addr", + "is_unit_like_type" + ]), + ("k_shape_59", #[ + "canon_cmp_ctor_range_ctx", + "put_inductive" + ]), + ("k_shape_60", #[ + "all_telescope_count", + "app_telescope_count", + "lam_telescope_count", + "check_ctor_entry" + ]), + ("k_shape_61", #[ + "canon_group_walk", + "check_positivity_aug" + ]), + ("k_shape_62", #[ + "put_recursor", + "canon_cmp_member_same_kind_ctx", + "try_native_dispatch" + ]), + ("k_shape_63", #[ + "count_ctors", + "put_constructor_list", + "put_all_telescope", + "put_app_telescope", + "put_lam_telescope", + "check_recr_rules" + ]), + ("k_shape_64", #[ + "try_lazy_delta_app", + "rbtree_map_ins.G", + "k_infer_proj", + "try_struct_eta_iota" + ]), + ("k_shape_65", #[ + "klimbs_add_carry", + "get_constructor", + "klimbs_sub_borrow", + "put_definition" + ]), + ("k_shape_66", #[ + "str_dec_eq_build", + "nlvars_add", + "try_nat_binop_addr" + ]), + ("k_shape_67", #[ + "get_mut_const", + "check_muts_all", + "get_constructor_list" + ]), + ("k_shape_68", #[ + "try_eta_struct", + "run_reveal" + ]), + ("k_shape_69", #[ + "is_muts_block", + "detect_aux_from_recrs_ex", + "find_peer_recursor_with_spec", + "muts_indc_count_is_one", + "canon_indc_positions", + "put_mut_const_list" + ]), + ("k_shape_70", #[ + "canon_muts_has_kind", + "get_ctor_entry", + "check_ctor_entries", + "build_recur_addrs_walk" + ]), + ("k_shape_71", #[ + "check_block_peer_param_agreement", + "ind_is_solo", + "struct_block_member_addrs", + "list_length_u64.Constructor", + "const_idxs_muts" + ]), + ("k_shape_72", #[ + "run_check_transitive", + "env_walk" + ]), + ("k_shape_73", #[ + "get_mut_const_list", + "put_expr" + ]), + ("k_shape_74", #[ + "prim_family", + "lazy_delta_step_const_const" + ]), + ("k_shape_75", #[ + "check_opt_addr", + "get_mut_entry" + ]), + ("k_shape_76", #[ + "address_eq_tail", + "address_eq", + "check_opt_expr_addr", + "get_ci" + ]), + ("k_shape_77", #[ + "flat_originals_walk", + "get_recursor", + "peer_agree_walk", + "run_claim" + ]), + ("k_shape_78", #[ + "try_reduce_decide_bitvec_lt", + "check_canonical_block" + ]), + ("k_shape_79", #[ + "get_mut_entry_list_inner", + "first_recr_parent_block", + "list_lookup_u64.Constructor" + ]), + ("k_shape_80", #[ + "load_assumption_tree", + "find_peer_rec_spec_walk" + ]), + ("k_shape_81", #[ + "aux_from_recrs_walk_ex", + "get_reveal_info", + "get_reveal_mut_const_info" + ]), + ("k_shape_82", #[ + "get_address", + "utf8_encode_prepend" + ]), + ("k_shape_83", #[ + "list_lookup_u64.MutConst", + "projection_addr", + "get_ci_iprj", + "get_ci_rprj", + "get_ci_dprj", + "check_muts_components" + ]), + ("k_shape_84", #[ + "blake3_next_layer", + "get_constant", + "get_ci_cprj", + "blake3_finish" + ]) +] + +end IxVM + +end diff --git a/Ix/MultiStark.lean b/Ix/MultiStark.lean index c9911442..6881ad13 100644 --- a/Ix/MultiStark.lean +++ b/Ix/MultiStark.lean @@ -11,6 +11,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.VerifierColdGroups public import Ix.MultiStark.Tests /-! diff --git a/Ix/MultiStark/VerifierColdGroups.lean b/Ix/MultiStark/VerifierColdGroups.lean new file mode 100644 index 00000000..58359883 --- /dev/null +++ b/Ix/MultiStark/VerifierColdGroups.lean @@ -0,0 +1,20 @@ +module + +/-! +Circuit-grouping data for the recursive-verifier toplevel, 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 verifierColdGroups : Array (String × Array String) := #[] + +end MultiStark + +end diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean index d78fa2f6..d62f0d04 100644 --- a/Tests/Aiur/Aiur.lean +++ b/Tests/Aiur/Aiur.lean @@ -719,6 +719,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 @@ -843,6 +875,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 f90e64f6..39ffb930 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 1f430c5e..a2a586c9 100644 --- a/Tests/Ix/IxVM.lean +++ b/Tests/Ix/IxVM.lean @@ -276,77 +276,77 @@ 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_239_352), - ("HEq.rec", 132_223_727), - ("Eq.rec", 131_796_529), - ("Nat", 129_236_482), - ("Nat.add", 159_622_648), - ("Nat.add_comm", 268_281_415), - ("Nat.decEq", 314_555_983), - ("Nat.decLe", 652_460_137), - ("Nat.sub_le_of_le_add", 1_577_107_099), - ("Nat.shiftRight_succ", 1_172_558_269), - ("Trans.mk", 134_045_879), - ("Array.append_assoc", 7_717_816_042), - ("Vector.append", 7_895_919_380), - ("IxVMPrim.nat_add_lit", 193_045_591), - ("IxVMPrim.nat_sub_lit", 206_429_542), - ("IxVMPrim.nat_mul_lit", 185_748_803), - ("IxVMPrim.nat_mul_big", 184_484_961), - ("IxVMPrim.nat_div_lit", 1_145_177_643), - ("IxVMPrim.nat_mod_lit", 1_166_515_024), - ("IxVMPrim.nat_succ_lit", 140_893_385), - ("IxVMPrim.nat_pred_lit", 158_099_686), - ("IxVMPrim.nat_gcd_lit", 1_819_307_333), - ("IxVMPrim.nat_land_lit", 2_945_733_257), - ("IxVMPrim.nat_lor_lit", 2_947_607_339), - ("IxVMPrim.nat_xor_lit", 2_963_279_952), - ("IxVMPrim.nat_shl_lit", 208_443_817), - ("IxVMPrim.nat_shr_lit", 1_157_079_133), - ("IxVMPrim.nat_pow_big", 361_995_186), - ("IxVMPrim.nat_beq_lit", 184_481_296), - ("IxVMPrim.nat_ble_lit", 180_137_392), - ("IxVMPrim.nat_cases_big", 157_983_733), - ("IxVMPrim.nat_dec_le", 667_624_988), - ("IxVMPrim.nat_dec_lt", 676_831_686), - ("IxVMPrim.nat_dec_eq", 346_845_775), - ("IxVMPrim.str_size_lit", 2_070_772_915), - ("IxVMPrim.bv_to_nat_lit", 1_729_888_453), - ("IxVMInd.Even", 187_829_482), - ("IxVMInd.Odd", 187_832_098), - ("IxVMInd.Even.rec", 202_546_550), - ("IxVMInd.Odd.rec", 202_547_473), - ("IxVMInd.Tree", 130_412_124), - ("IxVMInd.Tree.rec", 137_998_975), - ("IxVMInd.DedupM", 132_977_133), - ("IxVMInd.DedupM.rec", 143_220_708), - ("IxVMInd.DepthM", 131_760_815), - ("IxVMInd.DepthM.rec", 140_372_714), - ("String.Internal.append", 2_047_628_926), - ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 3_025_111_266), - ("Lean.Syntax.rec", 2_092_588_961), - ("IxVMInd.AuxTie", 280_526_725), - ("IxVMInd.AuxTie.rec", 313_017_899), - ("IxVMInd.HiddenIdx", 129_716_432), - ("IxVMInd.HiddenIdx.rec", 131_861_631), - ("IxVMInd.thmMajorUse", 441_019_720), - ("IxVMInd.partialKRec", 146_209_750), - ("IxVMInd.deepRebase", 195_377_539), - ("String.Slice.Pattern.Model.NoPrefixForwardPatternModel.rec", 2_880_537_174), - ("Lean.Widget.TaggedText.rec", 2_068_700_986), - ("Lean.Doc.Part.rec", 2_103_559_929), - ("Lean.Doc.Block.rec", 2_240_484_783), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 131_437_903), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 133_877_688), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 133_270_605), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 133_270_605), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 133_270_605), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 131_636_225), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 140_194_821), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 140_194_035), - ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 133_270_605), - ("strOfListFoldSize", 2_311_060_373), - ("strOfListFoldSizeAscii", 2_311_728_414), + ("HEq", 129_614_923), + ("HEq.rec", 133_914_548), + ("Eq.rec", 133_287_562), + ("Nat", 129_643_485), + ("Nat.add", 169_363_427), + ("Nat.add_comm", 303_687_588), + ("Nat.decEq", 360_291_029), + ("Nat.decLe", 772_303_497), + ("Nat.sub_le_of_le_add", 1_865_369_752), + ("Nat.shiftRight_succ", 1_391_216_093), + ("Trans.mk", 137_122_504), + ("Array.append_assoc", 9_257_829_977), + ("Vector.append", 9_461_542_378), + ("IxVMPrim.nat_add_lit", 212_154_642), + ("IxVMPrim.nat_sub_lit", 228_370_490), + ("IxVMPrim.nat_mul_lit", 201_572_207), + ("IxVMPrim.nat_mul_big", 199_985_590), + ("IxVMPrim.nat_div_lit", 1_359_001_478), + ("IxVMPrim.nat_mod_lit", 1_385_093_889), + ("IxVMPrim.nat_succ_lit", 144_532_764), + ("IxVMPrim.nat_pred_lit", 166_410_934), + ("IxVMPrim.nat_gcd_lit", 2_158_398_292), + ("IxVMPrim.nat_land_lit", 3_465_948_228), + ("IxVMPrim.nat_lor_lit", 3_468_268_358), + ("IxVMPrim.nat_xor_lit", 3_486_676_627), + ("IxVMPrim.nat_shl_lit", 230_041_921), + ("IxVMPrim.nat_shr_lit", 1_372_349_954), + ("IxVMPrim.nat_pow_big", 670_938_925), + ("IxVMPrim.nat_beq_lit", 200_595_377), + ("IxVMPrim.nat_ble_lit", 195_070_476), + ("IxVMPrim.nat_cases_big", 166_601_715), + ("IxVMPrim.nat_dec_le", 790_338_932), + ("IxVMPrim.nat_dec_lt", 801_732_216), + ("IxVMPrim.nat_dec_eq", 400_264_786), + ("IxVMPrim.str_size_lit", 2_464_292_178), + ("IxVMPrim.bv_to_nat_lit", 2_053_889_911), + ("IxVMInd.Even", 205_517_524), + ("IxVMInd.Odd", 205_520_140), + ("IxVMInd.Even.rec", 224_253_719), + ("IxVMInd.Odd.rec", 224_254_642), + ("IxVMInd.Tree", 131_263_253), + ("IxVMInd.Tree.rec", 141_469_958), + ("IxVMInd.DedupM", 134_598_603), + ("IxVMInd.DedupM.rec", 148_314_151), + ("IxVMInd.DepthM", 133_020_132), + ("IxVMInd.DepthM.rec", 144_540_776), + ("String.Internal.append", 2_437_496_123), + ("_private.Init.Prelude.0.Lean.extractMainModule._unsafe_rec", 3_603_333_119), + ("Lean.Syntax.rec", 2_494_596_914), + ("IxVMInd.AuxTie", 317_887_617), + ("IxVMInd.AuxTie.rec", 359_918_326), + ("IxVMInd.HiddenIdx", 130_237_418), + ("IxVMInd.HiddenIdx.rec", 133_293_032), + ("IxVMInd.thmMajorUse", 516_694_356), + ("IxVMInd.partialKRec", 151_787_477), + ("IxVMInd.deepRebase", 214_499_375), + ("String.Slice.Pattern.Model.NoPrefixForwardPatternModel.rec", 3_406_333_179), + ("Lean.Widget.TaggedText.rec", 2_464_786_293), + ("Lean.Doc.Part.rec", 2_511_025_214), + ("Lean.Doc.Block.rec", 2_679_871_677), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A", 132_590_814), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec", 135_858_714), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_1", 135_294_446), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup1.A.rec_2", 135_294_446), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedup2.A.rec_1", 135_294_446), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M", 132_891_055), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec", 144_357_365), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_1", 144_356_578), + ("_private.Tests.Ix.Compile.Mutual.0.Tests.Ix.Compile.Mutual.AuxDedupMixed.M.rec_2", 135_294_446), + ("strOfListFoldSize", 2_744_873_304), + ("strOfListFoldSizeAscii", 2_745_829_220), ] /-- Variant of `kernelChecks`, pinned to the baseline diff --git a/Tests/Main.lean b/Tests/Main.lean index 59203355..6846b0dc 100644 --- a/Tests/Main.lean +++ b/Tests/Main.lean @@ -130,7 +130,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 @@ -172,7 +182,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.coldGroups, AiurTestEnv.build IxVM.ixVMFull with | .error e, _ | _, .error e => IO.eprintln s!"IxVM env build failed: {e}"; return 1 | .ok v2Env, .ok v2FullEnv => @@ -223,8 +233,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 6079191308, got {actual}" - (actual = 6_079_191_308)) + s!"Shard pipeline FFT matches: expected 6634534730, got {actual}" + (actual = 6_634_534_730)) LSpec.lspecIO (.ofList [("ixvm", [fullSeq, aiurSeq, arenaSeq, exploitSeq, paritySeq, shardSeq])]) []), diff --git a/Tests/MultiStark.lean b/Tests/MultiStark.lean index c46b9477..f59ded1e 100644 --- a/Tests/MultiStark.lean +++ b/Tests/MultiStark.lean @@ -177,7 +177,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.verifierColdGroups 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 diff --git a/cold-groups/kernel-bands2.json b/cold-groups/kernel-bands2.json new file mode 100644 index 00000000..44c16afc --- /dev/null +++ b/cold-groups/kernel-bands2.json @@ -0,0 +1 @@ +[["canon_kind_ord", "canon_sord_eq_strong", "canon_sord_gt_strong", "canon_sord_lt_strong", "canon_sord_of_g", "check_opt_bool", "check_opt_u64", "const_num_lvls", "const_type_of", "def_safety_tag", "flatten_u64"], ["pack_def_kind_safety", "quot_kind_tag", "unpack_def_kind_safety", "check_opt_ctor_entries", "check_opt_recr_rules"], ["canon_ord_then", "canon_sord_then", "defn_is_unsafe_ci", "delta_rank", "is_unsafe_ci", "lbr_dec", "relaxed_u64_pred", "relaxed_u64_succ"], ["u64_eq", "u64_is_zero", "addr_set_member", "assert_wire_bool", "bit_vec_addr", "bit_vec_of_nat_addr", "bit_vec_to_nat_addr", "bit_vec_ult_addr", "bool_false_addr", "bool_true_addr", "bool_type_addr_dec", "build_all_minors", "build_all_motives", "build_recur_addrs", "byte_array_empty_addr", "canon_addr_chunk", "canon_cmp_kliteral", "char_of_nat_addr", "char_type_addr", "check_parent_inductive_shape"], ["decidable_decide_addr", "decidable_is_false_addr_dec", "decidable_is_true_addr_dec", "decidable_rec_addr", "eq_refl_addr_dec", "fin_addr", "int_dec_eq_addr_dec", "int_dec_le_addr_dec", "int_dec_lt_addr_dec", "int_neg_succ_addr_dec", "int_of_nat_addr_dec", "k_is_def_eq_struct", "klimbs_add", "list_cons_addr", "list_nil_addr", "literal_eq", "lt_lt_addr", "mk_nat_lit", "nat_add_addr", "nat_addr_io", "nat_beq_addr", "nat_ble_addr", "nat_dec_eq_addr_dec", "nat_dec_le_addr_dec", "nat_dec_lt_addr_dec", "nat_div_addr", "nat_eq_of_beq_eq_true_addr_dec", "nat_gcd_addr", "nat_land_addr", "nat_le_of_ble_eq_true_addr_dec", "nat_lor_addr", "nat_mod_addr", "nat_mul_addr", "nat_ne_of_beq_eq_false_addr_dec", "nat_not_le_of_not_ble_eq_true_addr_dec", "nat_pow_addr", "nat_pred_addr"], ["nat_shift_left_addr", "nat_shift_right_addr", "nat_sub_addr", "nat_succ_addr_iota", "nat_xor_addr", "nat_zero_addr", "punit_addr", "punit_size_of_1_addr", "put_constant_info", "put_quot_kind", "quot_ctor_addr", "quot_ind_addr", "quot_lift_addr_iota", "quot_type_addr", "reduce_bool_addr", "reduce_nat_addr", "size_of_size_of_addr", "str_addr", "string_append_addr", "string_back_addr", "string_dec_eq_addr", "string_legacy_back_addr", "string_of_list_addr", "string_to_byte_array_addr", "string_utf8_byte_size_addr", "subtype_val_addr", "system_platform_get_num_bits_addr", "system_platform_num_bits_addr", "unit_addr", "utf8_last_codepoint"], ["check_param_agreement", "is_defn_or_thm", "assert_safety", "build_ctor_app_params", "extract_aux_spec_params_from_rec", "is_rec_field", "klimbs_div", "klimbs_mod", "check_opt_def_kind", "check_opt_def_safety", "check_opt_quot_kind", "convert_axiom", "convert_quotient", "has_bvar_in_range_binder", "k_check", "klimbs_mul", "list_reverse.G", "put_definition_proj", "put_mut_const", "run_contains", "utf8_cont", "check_inductive_shape"], ["get_opt_addr_masked", "get_opt_bool_masked", "get_opt_def_kind_masked", "get_opt_quot_kind_masked", "list_is_empty.U8", "defn_member_recur_addrs", "expr_inst1_bvar", "k_is_def_eq_ordered", "klimbs_shl_limbs", "klimbs_sub", "pad_block", "put_u64_le", "try_unfold_head", "env_walk_leaves", "expr_glb_binder"], ["has_bvar_in_range_let", "k_infer", "k_infer_lit", "klimbs_dec", "klimbs_gcd", "mk_nat_literal_64", "mk_nat_one", "put_constructor_proj", "validate_univ_params_list", "get_opt_addr", "list_lookup_or_default.Ptr.U8_32", "nl_add_const", "read_byte", "apply_indices_in_conclusion", "apply_n_projs", "build_apply_field_bvars", "build_apply_xs", "build_major_params", "build_motive_apps", "build_param_lvls_range", "build_rec_lvls_list"], ["canon_ctor_ctx_entries", "check_prop_field_if_prop", "mk_bool", "np_whnf_inner_bv", "peel_leading_foralls", "unfold_a_and_loop", "unfold_b_and_loop", "check_positivity", "expr_inst1_let", "expr_inst_many_let", "expr_lift_let", "klimbs_shl", "klimbs_shr", "leaf_hash", "level_equal", "count_foralls_body", "expr_inst_levels", "level_offset_of", "skip_bytes", "canon_all_singleton", "canon_flatten", "canon_ins_sort", "canon_refine_one"], ["check_field_universes", "check_rec_rules_wellscoped", "convert_definition", "ctx_next_cut", "level_max_subsumes", "list_reverse_acc.G", "put_address_list", "utf8_validate", "wrap_foralls", "wrap_lams", "check_positivity_fields", "check_quot", "env_walk_refs", "put_tag0", "put_tag2"], ["put_tag4", "try_proof_irrel", "walk_refs_transitive", "convert_constructor", "convert_inductive", "expr_glb_let", "node_hash", "rbtree_map_insert.G", "check_native_nat", "count_foralls_at_least", "level_explicit_val", "list_length.KRecRule", "peel_n_foralls", "rbtree_map_balance.G", "se_peel_tol", "addr_list_contains", "all_bvars_in_args"], ["char_lit_codepoint", "check_field_universes_skip_params", "is_large_eliminator", "is_nat_zero", "k_ensure_sort", "k_is_def_eq_slow", "level_is_not_zero", "list_any_mentions_block", "list_concat.Tup.Ptr.U8_32.G", "list_take.Ptr.KExprNode", "se_addr_in", "str_lit_to_ctor_app_or_self"], ["utf8_last_go", "apply_spec_params_lifted", "canon_cmp_member_ctx", "canon_group_consec", "canon_refine_classes", "check_no_dep_data_field_if_prop", "compare_struct_fields", "const_idxs_exprs", "level_inst_params", "level_list_inst", "level_reduce", "list_lift_each", "list_lift_indices", "nl_subsumption_walk", "whnf_spine"], ["const_idxs_of", "k_is_def_eq", "try_unit_like", "canon_cmp_klimbs", "expr_lbr_let", "mk_nat_binop_stuck", "replace_spine_major"], ["list_length.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode", "assert_lvls_are_params", "canon_ctx_class_idx", "canon_g_list_eq", "check_large_prop_ctor", "glist_eq_len", "peel_leading_foralls_acc", "se_scan_fields", "canon_build_ctx_classes", "canon_cmp_krec_rule_ctx", "get_expr_let", "nl_le_vars", "normalize_aux"], ["try_string_lit_one", "canon_ctx_cmp_addr", "canon_sort_loop", "check_field_universes_inner", "intern_int_lit", "spec_params_lower", "try_quot_iota", "unfold_both_and_loop", "convert_recursor", "assert_first_args_are_param_bvars", "assert_occ_param_bvars", "head_addr", "list_snoc.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode", "peel_n_foralls_with_types", "check_rec_major_spine", "get_result_sort_level"], ["io_peel_field_loop", "level_list_struct_eq", "peel_motive_params_subst", "peel_n_alls_whnf", "spec_params_ptr_eq", "try_extract_nat", "whnf_get_ctor_or_none", "expr_inst_levels_walk", "is_inductive_prop", "k_is_def_eq_slow_nd"], ["level_leq", "peel_field_loop", "level_normalize", "u64_and", "u64_or", "u64_xor_kbits"], ["find_rule", "args_contain_bvar", "peel_n_lams_collect", "build_peer_recs", "canon_classes_eq", "de_args", "expr_mentions_block"], ["lazy_delta_loop", "level_eq", "level_list_eq", "canon_cmp_bytes"], ["canon_cmp_kuniv", "canon_cmp_kuniv_list", "extract_aux_spec_params", "idx_to_u64", "normalize_imax_dispatch", "spec_params_dom_prefix_match", "check_native_bool"], ["is_bitvec_prim_addr", "is_int_dec_prim_addr", "lazy_delta_both_proj", "whnf_nd_apply_beta", "canonical_rules_at_pos", "mk_nat_offset_stuck"], ["get_opt_u64_masked", "flat_find_pos", "put_refs", "put_sharing", "put_univs", "try_eta_swap", "aux_already_in", "is_prop_type", "level_struct_eq", "nl_skip_empty", "peel_params_subst"], ["se_mentions", "whnf_nd_with_spine", "nl_covers_var", "parse_atree_body", "try_extract_nat_app", "try_unfold_proj_app", "klimbs_from_g", "get_inductive_proj", "list_length.U8_8", "canon_cmp_kexpr_ctx", "ensure_sort_only"], ["flat_member_at", "rec_to_parent_addr", "check_param_agreement_go", "k_is_def_eq_struct_safe", "nl_le", "nlvars_eq"], ["build_char_list", "build_motive_type_flat", "k_def_eq_rebase", "klimbs_pow"], ["get_opt_ctor_entry_list_masked", "get_opt_rule_list_masked", "klimbs_is_zero", "klimbs_le", "list_snoc.U8_8", "put_u64_list", "convert_univ", "se_parent_addr"], ["kexpr_struct_eq", "level_imax", "lbr_max", "lbr_min"], ["level_max_go", "memo_u32_less_than", "bitvec_of_nat_args_direct", "glimbs_to_klimbs", "quot_extract_arg", "bv_to_nat_via", "nl_add_var", "check_ctor_return_type"], ["canon_member_num_ctors", "put_recursor_rule_list", "run_check", "get_axiom", "extract_aux_occ_us", "whnf", "whnf_nd"], ["canon_ord_cmp_g", "put_constant", "walk_fields_classify", "check_large_walk_fields", "expr_lift_bvar", "dec_dispatch_le_eq", "nat_lit_to_ctor_or_self", "try_eta_expand", "klimbs_div_mod", "dec_rewrite_lt_to_le"], ["assert_return_head_is_parent", "caddr_is_peer", "canon_member_ci", "check_eq_type", "check_muts_member_at", "const_idxs_rules", "flat_find_matching", "get_quotient", "put_univ_list", "get_address_list", "get_all_telescope", "get_expr_list", "get_lam_telescope", "collect_index_doms", "compute_iprj_addr", "k_is_def_eq_core"], ["bitvec_prep_spine", "build_rule_rhs"], ["addr_set_build", "struct_is_rec", "convert_rec_rules", "run_check_env", "collect_n_doms_whnf", "convert_univ_idxs", "is_rec_field_peel", "klimbs_mul_outer", "try_def_eq_nat", "peel_ctor_params_subst", "validate_univ_params_seen"], ["bitvec_prep_spine_ult", "ctx_seek_cut", "normalize_int_dec_rebuild", "canon_cmp_u64_lex", "u64_add", "u64_sub_with_borrow"], ["flat_find_pos_kind", "canon_cmp_krec_rule_list_ctx", "check_valid_ind_app", "level_max", "subst_param_for", "try_match_nat_add", "check_inductive_shape_ctors", "ctor_subst_param_for", "ctx_close_cut"], ["get_definition", "populate_rules", "char_lit_codepoint_syn", "try_def_eq_app", "level_max_offsets", "nl_eq", "try_k_synth_iota"], ["univ_succ_base", "struct_scan_ctors", "build_minor_doms"], ["cleanup_nat_offset_major", "nlvars_any_offset_geq", "nlvars_dominates", "nlvars_max_offset", "ctx_trim", "is_dec_prim_addr", "is_native_prim_addr", "try_nat_offset_dispatch"], ["bytes_to_u64_limb", "list_length_u64.Ptr.Univ", "build_rec_type", "build_succ_chain"], ["check_nested_ctors_positivity", "try_extract_int", "k_is_def_eq_slow2", "check_const"], ["get_constructor_proj", "put_recursor_rule"], ["expr_addr", "put_axiom", "put_quotient", "get_u64_list", "put_univ", "delta_unfold"], ["nl_add_const_go", "try_quot_ind", "try_quot_lift", "walk_char_list_bytes", "is_str_prim_addr"], ["get_tag0", "get_tag2", "klimbs_eq", "klimbs_succ", "collect_spine_of_ctor", "whnf_nd_const_head", "compute_k_target", "canon_cprj_addr"], ["nat_offset_of", "projection_addr_ctor", "projection_definition_info", "canon_cmp_ctor_pair_ctx", "try_bitvec_dispatch"], ["ctors_before_pos", "put_expr_list", "build_flat_own_params", "canon_cmp_klimbs_tail", "get_recursor_rule_list", "get_univ_list", "build_all_minors_walk", "build_all_motives_walk", "lazy_delta_a_const_b_proj", "lazy_delta_b_const_a_proj", "whnf_iota_major"], ["nl_covers_const", "canon_build_ctx_members", "check_recursor_member", "try_nat_binop_dispatch", "try_reduce_bit_vec_ult", "build_ih_doms"], ["klimbs_normalize", "put_constructor"], ["is_nat_succ_ih_step", "try_normalize_int_decidable", "try_reduce_subtype_val", "try_str_to_byte_array", "try_dec_dispatch"], ["try_nat_linear_rec", "try_str_back"], ["rbtree_map_lookup_or_default.G", "whnf_nd_proj_head", "whnf_proj_head", "bytes_to_limbs", "has_bvar_in_range", "try_str_dec_eq", "try_reduce_size_of_unit"], ["build_rec_type_from", "k_synth_gate", "dec_build_proof", "apply_ihs_full"], ["klimbs_land", "klimbs_lor", "klimbs_xor_op"], ["str_lit_delta_step", "glist_ordered_insert", "try_nat_dispatch_prewhnf"], ["glist_cmp", "glist_subset", "utf8_decode_one", "dec_finish"], ["verify_bytes_against", "get_univ"], ["canon_insert_sorted", "bytes_to_addr", "is_unit_like_type"], ["canon_cmp_ctor_range_ctx", "put_inductive"], ["all_telescope_count", "app_telescope_count", "lam_telescope_count", "check_ctor_entry"], ["canon_group_walk", "check_positivity_aug"], ["put_recursor", "canon_cmp_member_same_kind_ctx", "try_native_dispatch"], ["count_ctors", "put_constructor_list", "put_all_telescope", "put_app_telescope", "put_lam_telescope", "check_recr_rules"], ["try_lazy_delta_app", "rbtree_map_ins.G", "k_infer_proj", "try_struct_eta_iota"], ["klimbs_add_carry", "get_constructor", "klimbs_sub_borrow", "put_definition"], ["str_dec_eq_build", "nlvars_add", "try_nat_binop_addr"], ["get_mut_const", "check_muts_all", "get_constructor_list"], ["try_eta_struct", "run_reveal"], ["is_muts_block", "detect_aux_from_recrs_ex", "find_peer_recursor_with_spec", "muts_indc_count_is_one", "canon_indc_positions", "put_mut_const_list"], ["canon_muts_has_kind", "get_ctor_entry", "check_ctor_entries", "build_recur_addrs_walk"], ["check_block_peer_param_agreement", "ind_is_solo", "struct_block_member_addrs", "list_length_u64.Constructor", "const_idxs_muts"], ["run_check_transitive", "env_walk"], ["get_mut_const_list", "put_expr"], ["prim_family", "lazy_delta_step_const_const"], ["check_opt_addr", "get_mut_entry"], ["address_eq_tail", "address_eq", "check_opt_expr_addr", "get_ci"], ["flat_originals_walk", "get_recursor", "peer_agree_walk", "run_claim"], ["try_reduce_decide_bitvec_lt", "check_canonical_block"], ["get_mut_entry_list_inner", "first_recr_parent_block", "list_lookup_u64.Constructor"], ["load_assumption_tree", "find_peer_rec_spec_walk"], ["aux_from_recrs_walk_ex", "get_reveal_info", "get_reveal_mut_const_info"], ["get_address", "utf8_encode_prepend"], ["list_lookup_u64.MutConst", "projection_addr", "get_ci_iprj", "get_ci_rprj", "get_ci_dprj", "check_muts_components"], ["blake3_next_layer", "get_constant", "get_ci_cprj", "blake3_finish"]] \ No newline at end of file diff --git a/cold-groups/kernel-shape-grouping2.md b/cold-groups/kernel-shape-grouping2.md new file mode 100644 index 00000000..fd9454bf --- /dev/null +++ b/cold-groups/kernel-shape-grouping2.md @@ -0,0 +1,27 @@ +# Kernel cold-circuit grouping by layout shape (2026-08-14, post xor-split rebase) + +Rebuilt from scratch after rebasing group-functions onto main @ 97aa19e8 +(perf/virtual xor split #558) — the old groupings predated the fused +xor-rotation circuits and were discarded. Workloads: execute-only +`ix check --ixe InitStd.ixe` over String.split and Array.extract_append, +with the TEMP Sel/Aux/Lkp stats columns +(cold-groups/kstats2-{String.split,Array.extract_append}.txt; grouped runs +in kstats2-grouped-*.txt). + +## Heuristic (same conservative rule as the pre-rebase baseline) +Cold = max FFT share < 0.5% across the two workloads (668 of 709 function +circuits). Cluster cold circuits by SHAPE PROXIMITY: a band admits a member +while max(aux) <= 1.6 * min(aux), max(lkp) <= max(2 * min(lkp), min + 4), +and summed selectors stay <= 40 (selectors sum under the merge rule; aux and +lookups merge by max, so shape mismatch is pure per-row waste). +verify_claim is excluded (entry functions cannot group). + +## Result: 85 bands over 630 circuits +- circuits 730 -> 185, total committed width 33,331 -> 15,763 (-53%) +- measured FFT cost: String.split 4.951e10 -> 5.622e10 (+13.6%), + Array.extract_append 1.352e11 -> 1.471e11 (+8.8%) +- hot circuits left ungrouped (top max-share): blake3_compress_inner_j, + expr_inst_many_walk, expr_inst_many, blake3_compress_chunks, list_snoc.G, + peel_beta, list_drop.Ptr.Expr, blake3_compress +- band membership: cold-groups/kernel-bands2.json; applied grouping: + Ix/IxVM/ColdGroups.lean diff --git a/cold-groups/kstats2-Array.extract_append.txt b/cold-groups/kstats2-Array.extract_append.txt new file mode 100644 index 00000000..e9e06fa1 --- /dev/null +++ b/cold-groups/kstats2-Array.extract_append.txt @@ -0,0 +1,739 @@ +=== Circuit Statistics === +Circuits: 730 +Total width: 33331 +Total FFT cost: 135187270227 (1.35e11) +Total cache hits: 72393508 +Total saved cost: 57.23% +---------------------------------------------------------------------------------------------------------------------------------------------- +Name Width Sel Aux Lkp Height Hits FFT cost % %++ +---------------------------------------------------------------------------------------------------------------------------------------------- +expr_inst_many_walk 34 9 8 5 5471753 0 2.10e10 15.55% 15.55% +expr_inst_many 21 2 4 4 6975351 1584350 1.69e10 12.50% 28.05% +blake3_compress_inner_j 696 1 369 193 151585 0 9.08e9 6.72% 34.77% +memory[3] 12 0 0 0 6181533 17946311 8.59e9 6.35% 41.12% +list_snoc.G 22 2 6 4 2593801 881702 6.17e9 4.57% 45.69% +peel_beta 32 3 12 5 1637758 10634 5.47e9 4.05% 49.73% +list_drop.Ptr.Expr 20 2 6 3 2151895 1151414 4.60e9 3.41% 53.14% +blake3_compress_chunks 29 3 7 4 1288914 0 3.84e9 2.84% 55.98% +whnf_with_spine 34 6 11 5 1108779 14944 3.82e9 2.83% 58.81% +expr_inst_many_bvar 24 2 5 5 1528825 0 3.82e9 2.83% 61.64% +list_concat.Ptr.KExprNode 22 2 6 4 1505977 731709 3.45e9 2.55% 64.19% +expr_lbr 35 9 9 6 870475 9468745 3.04e9 2.25% 66.44% +collect_spine 23 2 8 4 1199012 836589 2.83e9 2.09% 68.53% +k_infer_app_spine_loop 59 8 21 11 470161 506 2.63e9 1.95% 70.48% +memory[4] 13 0 0 0 1735873 17182092 2.40e9 1.78% 72.25% +list_lookup.Ptr.KLevelNode 16 1 5 3 1364948 403575 2.27e9 1.68% 73.94% +list_length.Ptr.KExprNode 18 2 5 3 1166659 2680089 2.16e9 1.60% 75.53% +get_expr 50 12 23 5 391929 17 1.83e9 1.36% 76.89% +whnf_const_head 77 16 32 10 246268 0 1.71e9 1.26% 78.15% +blake3_compress 1080 1 929 40 21655 14 1.68e9 1.25% 79.40% +convert_expr 60 12 25 7 292994 154982 1.61e9 1.19% 80.59% +get_tag4 37 2 22 4 393551 0 1.37e9 1.01% 81.60% +apply_spine_expr 22 2 6 4 618392 83404 1.33e9 0.98% 82.58% +get_u64_le 28 2 14 3 422899 22 1.12e9 0.83% 83.41% +whnf_apply_beta 34 3 10 7 339939 0 1.07e9 0.79% 84.21% +get_app_telescope 43 2 15 6 264610 0 1.03e9 0.77% 84.97% +expr_inst1_walk 34 9 8 5 326314 0 1.03e9 0.76% 85.73% +expr_glb_walk 34 10 8 5 295964 0 9.25e8 0.68% 86.42% +g_list_has 21 3 6 3 413484 3025 8.25e8 0.61% 87.03% +validate_expr_well_scoped 52 9 20 8 176535 152144 8.06e8 0.60% 87.62% +expr_inst1 21 2 4 4 400830 220687 7.98e8 0.59% 88.21% +expr_lift 23 3 5 4 359613 1596071 7.76e8 0.57% 88.79% +try_reduce_projection_definition 59 3 24 13 151416 11396 7.74e8 0.57% 89.36% +const_idxs_expr 52 7 26 7 160015 209196 7.25e8 0.54% 89.90% +k_infer_core 53 9 22 8 156068 76251 7.19e8 0.53% 90.43% +expr_lift_walk 34 9 8 5 232640 0 7.13e8 0.53% 90.96% +try_prim_dispatch 30 6 8 4 254764 16347 6.95e8 0.51% 91.47% +list_take.Ptr.KExprNode 23 2 7 4 311258 46370 6.64e8 0.49% 91.96% +expr_lower_walk 53 10 18 9 141436 0 6.46e8 0.48% 92.44% +expr_glb 21 2 5 4 307017 351230 5.99e8 0.44% 92.88% +try_iota 108 5 39 25 66939 2106 5.82e8 0.43% 93.31% +whnf 38 6 14 6 157482 59630 5.22e8 0.39% 93.70% +safe_refs_only 43 9 19 5 140151 138582 5.20e8 0.38% 94.09% +try_nat_linear_rec 75 5 27 17 66603 305 4.03e8 0.30% 94.38% +bytes_to_block 265 1 193 65 20371 601 3.87e8 0.29% 94.67% +memory[18] 27 0 0 0 160015 742479 3.79e8 0.28% 94.95% +expr_lower 23 3 5 4 159506 145656 3.23e8 0.24% 95.19% +k_infer 15 1 4 4 232319 67885 3.19e8 0.24% 95.42% +whnf_nd_with_spine 34 6 11 5 108049 5848 3.11e8 0.23% 95.65% +k_is_def_eq 29 3 7 6 124776 117155 3.11e8 0.23% 95.88% +get_expr_list 42 2 15 6 88735 268 3.09e8 0.23% 96.11% +blake3_compress_block 211 2 169 15 19287 0 2.90e8 0.21% 96.33% +whnf_proj_head 61 4 28 10 47524 0 2.27e8 0.17% 96.50% +k_check 15 1 3 3 159446 212233 2.12e8 0.16% 96.65% +ctx_trim 52 3 19 12 48396 403673 1.98e8 0.15% 96.80% +try_def_eq_app 49 6 18 9 50776 2516 1.96e8 0.15% 96.94% +de_args 32 5 10 5 67744 21012 1.76e8 0.13% 97.08% +const_idxs_exprs 24 2 7 5 86624 1620 1.74e8 0.13% 97.20% +get_u64_list 49 2 22 6 44676 0 1.71e8 0.13% 97.33% +get_tag0 40 2 23 5 50253 2087 1.59e8 0.12% 97.45% +get_address 138 1 98 34 15781 90 1.52e8 0.11% 97.56% +whnf_nd 38 6 14 6 49692 10756 1.49e8 0.11% 97.67% +try_reduce_fin_val_decidable_rec 149 9 58 37 14010 42719 1.44e8 0.11% 97.78% +cleanup_nat_offset_major 45 5 19 8 37490 96326 1.30e8 0.10% 97.87% +Bytes2 24 0 0 0 65536 0 1.28e8 0.09% 97.97% +k_def_eq_rebase 44 2 12 11 36566 0 1.23e8 0.09% 98.06% +whnf_iota_major 51 3 24 9 30949 36035 1.19e8 0.09% 98.15% +k_is_def_eq_core 40 2 15 8 37176 11532 1.14e8 0.08% 98.23% +address_eq 82 2 66 4 19339 105521 1.14e8 0.08% 98.32% +whnf_nd_const_head 55 9 23 7 24843 0 1.01e8 0.07% 98.39% +try_string_lit_one 28 3 8 5 45390 0 9.99e7 0.07% 98.46% +ctx_seek_cut 44 2 16 10 28518 2605 9.39e7 0.07% 98.53% +try_match_nat_add 47 6 17 9 24711 0 8.56e7 0.06% 98.60% +try_eta_struct 91 8 48 14 12585 1295 7.84e7 0.06% 98.65% +expr_glb_binder 16 1 4 4 56426 179 7.33e7 0.05% 98.71% +expr_inst_levels_walk 36 9 9 6 26401 0 7.08e7 0.05% 98.76% +get_lam_telescope 42 2 15 6 22282 1 6.84e7 0.05% 98.81% +pad_block 18 2 4 3 46924 203 6.72e7 0.05% 98.86% +try_extract_nat 30 6 9 5 28819 38736 6.51e7 0.05% 98.91% +collect_spine_of_ctor 45 3 23 7 18694 48214 6.04e7 0.04% 98.95% +memory[32] 41 0 0 0 20282 85992 6.02e7 0.04% 99.00% +nat_lit_to_ctor_or_self 43 4 14 10 18695 48216 5.77e7 0.04% 99.04% +try_extract_nat_app 33 4 11 6 22971 0 5.57e7 0.04% 99.08% +k_is_def_eq_ordered 19 2 4 3 36613 563 5.40e7 0.04% 99.12% +k_is_def_eq_slow_nd 32 4 9 6 22695 0 5.34e7 0.04% 99.16% +try_struct_eta_iota 93 9 39 16 8529 0 5.21e7 0.04% 99.20% +k_is_def_eq_struct_safe 40 9 12 6 17527 45 5.00e7 0.04% 99.24% +whnf_nd_apply_beta 34 3 10 7 20065 0 4.95e7 0.04% 99.27% +get_address_list 42 2 15 6 15776 1546 4.68e7 0.03% 99.31% +k_infer_only 93 12 45 15 7639 13614 4.61e7 0.03% 99.34% +expr_inst1_bvar 20 3 4 3 29243 0 4.44e7 0.03% 99.38% +k_is_def_eq_slow 26 4 7 4 22695 0 4.35e7 0.03% 99.41% +expr_inst_levels 20 2 6 3 27486 203854 4.15e7 0.03% 99.44% +get_all_telescope 42 2 15 6 13871 8 4.06e7 0.03% 99.47% +whnf_nd_proj_head 61 4 28 10 9205 0 3.73e7 0.03% 99.50% +walk_refs_transitive 27 4 6 5 19062 467 3.73e7 0.03% 99.52% +nat_offset_of 58 12 23 9 9203 3526 3.55e7 0.03% 99.55% +ctx_close_cut 46 3 17 10 11155 3972 3.49e7 0.03% 99.58% +u64_is_zero 25 9 2 1 18991 574396 3.44e7 0.03% 99.60% +relaxed_u64_pred 25 9 2 1 18983 276989 3.44e7 0.03% 99.63% +k_is_def_eq_slow2 58 9 20 11 8692 0 3.33e7 0.02% 99.65% +k_ensure_sort 18 1 7 4 23106 11234 3.10e7 0.02% 99.67% +str_lit_to_ctor_app_or_self 24 3 7 4 15628 41101 2.67e7 0.02% 99.69% +blake3_compress_layer 223 3 170 6 2064 0 2.54e7 0.02% 99.71% +list_is_empty.U8 15 2 4 2 19025 18852 2.10e7 0.02% 99.73% +flatten_u64 14 1 1 1 18983 99858 1.92e7 0.01% 99.74% +blake3_finish 190 11 151 9 1707 0 1.75e7 0.01% 99.76% +blake3_next_layer 221 4 136 5 1464 0 1.71e7 0.01% 99.77% +try_def_eq_nat 41 4 16 7 6316 478 1.66e7 0.01% 99.78% +is_nat_zero 24 4 7 4 9134 3498 1.47e7 0.01% 99.79% +head_addr 24 2 9 4 9059 3989 1.46e7 0.01% 99.80% +ctx_next_cut 16 1 6 4 12668 23715 1.43e7 0.01% 99.81% +lazy_delta_loop 35 7 10 5 6269 470 1.41e7 0.01% 99.82% +get_constant 162 3 136 9 1621 0 1.41e7 0.01% 99.83% +replace_spine_major 23 1 7 7 8498 163 1.31e7 0.01% 99.84% +try_unit_like 28 2 7 6 6443 643 1.16e7 0.01% 99.85% +try_proof_irrel 25 2 6 5 6483 643 1.05e7 0.01% 99.86% +load_verified_constant 100 1 88 5 1621 2066 8.70e6 0.01% 99.87% +get_ci 97 10 68 7 1542 348070 7.98e6 0.01% 99.87% +blake3 86 1 72 8 1707 114 7.94e6 0.01% 99.88% +try_nat_dispatch_prewhnf 86 8 31 20 1550 0 7.12e6 0.01% 99.88% +memory[34] 43 0 0 0 2815 7298 7.04e6 0.01% 99.89% +run_check_transitive 79 7 55 6 1621 15636 6.89e6 0.01% 99.89% +verify_bytes_against 73 1 33 2 1707 0 6.75e6 0.00% 99.90% +const_idxs_of 77 6 7 6 1621 0 6.71e6 0.00% 99.90% +check_const 75 8 20 15 1542 79 6.18e6 0.00% 99.91% +expr_lift_bvar 39 2 14 8 2657 0 5.99e6 0.00% 99.91% +get_constant_info_by_variant 64 8 46 2 1542 0 5.28e6 0.00% 99.92% +prim_family 161 23 59 37 510 254254 3.71e6 0.00% 99.92% +whnf_spine 25 2 7 5 2502 1358 3.62e6 0.00% 99.92% +projection_definition_info 54 5 23 10 1196 151095 3.34e6 0.00% 99.92% +lbr_max 35 2 13 7 1593 890375 3.02e6 0.00% 99.93% +lbr_min 35 2 13 7 1545 388016 2.92e6 0.00% 99.93% +convert_definition 40 5 6 4 1341 0 2.83e6 0.00% 99.93% +memo_u32_less_than 28 1 13 7 1612 9659746 2.46e6 0.00% 99.93% +expr_mentions_block 40 14 10 5 1175 574 2.44e6 0.00% 99.93% +assert_safety 15 2 3 2 2730 153 2.44e6 0.00% 99.94% +is_unsafe_ci 29 9 2 1 1542 1977 2.42e6 0.00% 99.94% +const_type_of 27 8 1 1 1541 976 2.26e6 0.00% 99.94% +const_num_lvls 27 8 1 1 1541 11939 2.26e6 0.00% 99.94% +peel_params_subst 30 2 11 5 1376 290 2.20e6 0.00% 99.94% +get_definition 30 1 18 6 1341 0 2.14e6 0.00% 99.94% +run_check 24 1 14 4 1542 0 2.02e6 0.00% 99.95% +try_dec_dispatch 70 4 26 16 613 0 2.01e6 0.00% 99.95% +k_infer_proj 62 1 39 13 647 0 1.90e6 0.00% 99.95% +peel_n_alls_whnf 29 3 9 5 1215 0 1.85e6 0.00% 99.95% +is_prop_type 30 3 11 5 1141 5347 1.78e6 0.00% 99.95% +memory[12] 21 0 0 0 1548 416435 1.78e6 0.00% 99.95% +k_is_def_eq_struct_go 58 26 13 6 625 0 1.71e6 0.00% 99.95% +read_byte 18 2 5 3 1628 0 1.62e6 0.00% 99.96% +peel_field_loop 34 2 9 6 923 0 1.58e6 0.00% 99.96% +level_struct_eq 39 12 11 5 810 522 1.56e6 0.00% 99.96% +nl_subsume_entry 121 13 54 24 297 59 1.49e6 0.00% 99.96% +is_str_prim_addr 65 8 22 15 497 0 1.46e6 0.00% 99.96% +try_nat_binop_dispatch 65 6 24 14 476 790 1.39e6 0.00% 99.96% +is_nat_succ_ih_step 58 7 26 10 493 530 1.30e6 0.00% 99.96% +try_reduce_decide_bitvec_lt 165 8 72 40 202 15 1.28e6 0.00% 99.96% +is_native_prim_addr 57 7 19 13 495 0 1.28e6 0.00% 99.96% +is_dec_prim_addr 57 7 19 13 494 0 1.28e6 0.00% 99.96% +level_imax 37 6 13 6 653 7954 1.15e6 0.00% 99.97% +convert_univ_idxs 38 2 16 7 634 17502 1.14e6 0.00% 99.97% +level_inst_params 28 5 7 5 798 914 1.11e6 0.00% 99.97% +level_list_inst 25 2 7 5 870 1878 1.09e6 0.00% 99.97% +dec_build_proof 95 8 30 22 268 0 1.04e6 0.00% 99.97% +lazy_delta_step_const_const 120 6 60 22 214 0 1.00e6 0.00% 99.97% +dec_finish 90 4 32 22 267 0 9.78e5 0.00% 99.97% +get_univ 55 5 33 6 397 44 9.57e5 0.00% 99.97% +level_eq 36 10 10 5 545 133 9.11e5 0.00% 99.97% +try_eta_swap 30 4 11 4 626 59 8.95e5 0.00% 99.97% +is_bitvec_prim_addr 33 4 10 7 497 0 7.52e5 0.00% 99.97% +try_lazy_delta_app 72 6 39 10 255 0 7.43e5 0.00% 99.97% +try_normalize_int_decidable 64 4 26 13 277 0 7.29e5 0.00% 99.97% +try_unfold_proj_app 31 3 11 6 499 234 7.11e5 0.00% 99.97% +get_tag2 40 2 23 5 397 0 7.00e5 0.00% 99.97% +utf8_decode_one 76 4 32 17 228 0 6.87e5 0.00% 99.98% +peel_n_foralls 21 2 7 3 662 62 6.75e5 0.00% 99.98% +address_eq_tail 84 6 66 3 204 0 6.65e5 0.00% 99.98% +check_prop_field_if_prop 22 2 5 4 616 31 6.50e5 0.00% 99.98% +dec_dispatch_le_eq 47 5 14 9 321 0 6.40e5 0.00% 99.98% +peer_agree_walk 107 5 69 11 158 0 6.23e5 0.00% 99.98% +lazy_delta_both_proj 39 7 10 7 365 0 6.19e5 0.00% 99.98% +compare_struct_fields 31 3 7 5 416 0 5.76e5 0.00% 99.98% +try_bitvec_dispatch 66 6 23 15 219 0 5.70e5 0.00% 99.98% +normalize_int_dec_rebuild 53 3 16 12 258 0 5.57e5 0.00% 99.98% +level_max 45 4 17 9 295 110 5.55e5 0.00% 99.98% +level_is_not_zero 27 7 7 4 431 679 5.25e5 0.00% 99.98% +try_unfold_head 33 5 4 3 359 66 5.16e5 0.00% 99.98% +get_ci_cprj 158 1 142 7 96 1019 5.03e5 0.00% 99.98% +level_max_subsumes 23 3 6 4 474 44 5.02e5 0.00% 99.98% +level_max_go 39 6 13 7 289 0 4.71e5 0.00% 99.98% +expr_lbr_let 23 1 7 7 443 0 4.64e5 0.00% 99.98% +get_mut_const_list 86 2 59 6 146 12 4.57e5 0.00% 99.98% +get_constructor_list 75 2 48 6 163 12 4.55e5 0.00% 99.98% +is_inductive_prop 24 1 9 6 414 233 4.47e5 0.00% 99.98% +level_max_offsets 47 3 18 10 235 0 4.43e5 0.00% 99.98% +check_canonical_block 123 3 75 20 105 0 4.37e5 0.00% 99.98% +is_unit_like_type 60 7 34 7 189 6254 4.36e5 0.00% 99.98% +build_recur_addrs_walk 71 2 51 5 158 0 4.15e5 0.00% 99.98% +check_positivity_aug 78 5 35 15 145 4 4.11e5 0.00% 99.98% +ensure_sort_only 30 2 12 5 315 111 4.03e5 0.00% 99.98% +canon_muts_has_kind 69 6 51 3 155 80 3.95e5 0.00% 99.99% +get_univ_list 53 2 24 7 192 1620 3.93e5 0.00% 99.99% +check_muts_all 66 2 48 4 158 0 3.87e5 0.00% 99.99% +k_synth_gate 71 4 30 14 144 5 3.72e5 0.00% 99.99% +k_is_def_eq_struct 12 1 2 2 622 59 3.69e5 0.00% 99.99% +normalize_aux 33 7 8 5 268 95 3.66e5 0.00% 99.99% +put_constant 90 9 14 7 114 19 3.55e5 0.00% 99.99% +glist_subset 75 5 32 16 131 267 3.50e5 0.00% 99.99% +ctor_at 86 2 72 3 117 2 3.50e5 0.00% 99.99% +check_inductive_shape_ctors 52 2 17 10 175 0 3.45e5 0.00% 99.99% +projection_addr 134 4 105 9 79 105 3.37e5 0.00% 99.99% +try_k_synth_iota 59 4 18 12 149 0 3.23e5 0.00% 99.99% +check_no_dep_data_field_if_prop 28 3 7 5 269 7 3.14e5 0.00% 99.99% +nl_add_var 43 4 13 9 185 33 3.06e5 0.00% 99.99% +get_ci_iprj 121 1 108 6 79 9496 3.04e5 0.00% 99.99% +wrap_foralls 22 2 6 4 314 49 2.98e5 0.00% 99.99% +check_param_agreement_go 34 2 12 6 207 0 2.78e5 0.00% 99.99% +put_address 106 1 65 34 79 35 2.67e5 0.00% 99.99% +muts_member_at 108 2 94 3 77 177 2.63e5 0.00% 99.99% +check_positivity_fields 26 2 6 5 244 0 2.60e5 0.00% 99.99% +put_constant_info 64 8 2 2 114 0 2.53e5 0.00% 99.99% +peel_ctor_params_subst 46 3 16 8 146 2 2.47e5 0.00% 99.99% +try_nat_offset_dispatch 59 4 19 14 119 0 2.46e5 0.00% 99.99% +expr_inst1_let 21 1 5 5 268 0 2.37e5 0.00% 99.99% +peel_n_lams_collect 29 3 10 4 205 0 2.36e5 0.00% 99.99% +walk_fields_classify 42 3 14 7 149 2 2.31e5 0.00% 99.99% +peel_n_foralls_with_types 27 3 9 4 207 3 2.22e5 0.00% 99.99% +get_expr_let 28 1 8 5 191 0 2.09e5 0.00% 99.99% +delta_unfold 45 4 22 7 128 108 2.06e5 0.00% 99.99% +check_block_peer_param_agreement 81 4 52 4 79 0 2.05e5 0.00% 99.99% +bytes_to_u64_limb 50 10 20 3 116 0 2.03e5 0.00% 99.99% +utf8_validate 21 2 6 4 229 61 1.97e5 0.00% 99.99% +expr_inst_many_let 21 1 5 5 229 0 1.97e5 0.00% 99.99% +caddr_is_peer 31 2 15 4 164 13 1.93e5 0.00% 99.99% +const_idxs_muts 76 4 53 7 78 78 1.89e5 0.00% 99.99% +check_muts_member_at 74 1 15 5 79 0 1.87e5 0.00% 99.99% +convert_constructor 57 1 6 6 96 0 1.84e5 0.00% 99.99% +const_idxs_ctors 57 2 40 5 95 76 1.81e5 0.00% 99.99% +get_constructor 55 1 41 8 96 0 1.77e5 0.00% 99.99% +bytes_to_addr 44 1 34 3 114 19 1.75e5 0.00% 99.99% +get_inductive 67 1 51 9 79 0 1.70e5 0.00% 99.99% +canon_indc_positions 67 3 50 4 78 78 1.67e5 0.00% 99.99% +level_offset_of 20 2 6 3 207 288 1.67e5 0.00% 99.99% +check_field_universes_inner 29 2 8 6 153 0 1.67e5 0.00% 99.99% +compare_rules 89 4 40 16 61 0 1.63e5 0.00% 99.99% +count_ctors 51 2 38 3 95 78 1.63e5 0.00% 99.99% +try_extract_int 49 6 20 9 98 611 1.62e5 0.00% 99.99% +validate_univ_params_list 20 2 4 4 202 10956 1.62e5 0.00% 99.99% +get_mut_const 62 3 48 3 79 0 1.57e5 0.00% 99.99% +glist_cmp 76 6 32 16 67 189 1.57e5 0.00% 99.99% +build_motive_apps 23 2 5 4 172 0 1.53e5 0.00% 99.99% +flat_originals_walk 100 5 68 9 52 0 1.50e5 0.00% 99.99% +memory[10] 19 0 0 0 195 108527 1.48e5 0.00% 99.99% +put_tag0 32 3 6 5 127 25 1.47e5 0.00% 99.99% +memory[36] 45 0 0 0 95 375 1.44e5 0.00% 99.99% +relaxed_u64_succ 25 9 2 1 150 547 1.41e5 0.00% 99.99% +memory[47] 56 0 0 0 78 1009 1.40e5 0.00% 99.99% +try_nat_binop_addr 128 15 44 31 40 2 1.38e5 0.00% 99.99% +put_tag4 33 3 6 5 114 0 1.33e5 0.00% 100.00% +load_verified_blob 46 1 36 3 85 739 1.28e5 0.00% 100.00% +convert_inductive 50 1 6 6 79 0 1.27e5 0.00% 100.00% +Bytes1 11 0 0 0 256 0 1.22e5 0.00% 100.00% +check_ctor_return_type 37 1 13 12 94 92 1.17e5 0.00% 100.00% +is_rec_field_peel 40 3 16 7 87 0 1.15e5 0.00% 100.00% +validate_univ_params_seen 43 5 16 8 81 521 1.13e5 0.00% 100.00% +apply_ihs_full 100 2 30 26 41 0 1.11e5 0.00% 100.00% +whnf_get_ctor_or_none 26 2 9 5 119 56302 1.11e5 0.00% 100.00% +addr_list_contains 24 3 7 4 126 41 1.10e5 0.00% 100.00% +check_field_universes_skip_params 25 2 7 4 120 0 1.08e5 0.00% 100.00% +get_result_sort_level 28 2 9 5 105 187 1.02e5 0.00% 100.00% +io_peel_field_loop 30 2 9 5 98 18 1.01e5 0.00% 100.00% +build_minor_doms 54 2 19 7 61 0 9.99e4 0.00% 100.00% +memory[8] 17 0 0 0 151 44897 9.83e4 0.00% 100.00% +build_flat_block 159 7 121 12 26 0 9.81e4 0.00% 100.00% +get_recursor_rule_list 53 2 24 7 61 0 9.81e4 0.00% 100.00% +mk_nat_offset_stuck 37 2 10 9 81 0 9.79e4 0.00% 100.00% +nl_subsumption_walk 25 2 7 5 110 41 9.72e4 0.00% 100.00% +populate_rules 52 3 18 6 61 0 9.63e4 0.00% 100.00% +get_constructor_proj 31 1 21 4 90 0 9.38e4 0.00% 100.00% +is_muts_block 61 2 50 2 52 78 9.23e4 0.00% 100.00% +nl_eq 51 7 18 10 58 51 8.87e4 0.00% 100.00% +flat_find_matching 39 5 15 5 70 8 8.62e4 0.00% 100.00% +bytes_to_limbs 57 5 29 9 51 711 8.43e4 0.00% 100.00% +build_all_minors_walk 55 3 24 8 52 0 8.34e4 0.00% 100.00% +list_any_mentions_block 24 3 7 4 95 24 7.83e4 0.00% 100.00% +check_recursor_canonical_full 125 9 50 18 26 0 7.73e4 0.00% 100.00% +list_reverse_acc.G 22 2 6 4 99 0 7.58e4 0.00% 100.00% +convert_rec_rules 40 2 16 6 61 0 7.46e4 0.00% 100.00% +build_apply_field_bvars 23 2 5 4 94 28 7.42e4 0.00% 100.00% +check_field_universes 23 2 6 4 94 92 7.42e4 0.00% 100.00% +assert_first_args_are_param_bvars 27 2 9 4 81 65 7.22e4 0.00% 100.00% +assert_return_head_is_parent 27 1 15 4 78 16 6.90e4 0.00% 100.00% +level_list_eq 31 5 10 5 69 21987 6.78e4 0.00% 100.00% +check_positivity 20 1 5 5 94 92 6.50e4 0.00% 100.00% +level_equal 23 2 5 5 83 1315 6.38e4 0.00% 100.00% +build_ih_doms 78 2 24 20 32 9 6.36e4 0.00% 100.00% +k_infer_lit 20 2 4 4 88 0 6.00e4 0.00% 100.00% +u64_sub_with_borrow 53 1 16 16 41 1 5.97e4 0.00% 100.00% +build_minor_at_depth 65 1 25 21 35 0 5.96e4 0.00% 100.00% +klimbs_mul_single 86 3 47 7 28 0 5.89e4 0.00% 100.00% +build_rec_type_from 93 3 29 23 26 0 5.78e4 0.00% 100.00% +get_inductive_proj 22 1 12 3 79 0 5.76e4 0.00% 100.00% +put_definition_proj 22 1 3 3 79 0 5.76e4 0.00% 100.00% +nl_covers_var 35 4 11 6 54 1 5.63e4 0.00% 100.00% +level_normalize 25 1 9 9 68 94 5.42e4 0.00% 100.00% +get_recursor 87 1 69 11 26 0 5.41e4 0.00% 100.00% +u64_mul 222 1 155 46 13 0 5.39e4 0.00% 100.00% +lazy_delta_b_const_a_proj 55 6 24 8 36 0 5.25e4 0.00% 100.00% +check_inductive_shape 19 1 3 4 79 26 5.02e4 0.00% 100.00% +level_reduce 27 5 7 5 57 214 4.69e4 0.00% 100.00% +skip_bytes 21 3 6 3 69 47 4.67e4 0.00% 100.00% +check_param_agreement 14 1 2 3 94 92 4.65e4 0.00% 100.00% +nl_skip_empty 30 4 11 5 52 69 4.63e4 0.00% 100.00% +build_apply_xs 22 2 5 4 66 17 4.63e4 0.00% 100.00% +count_foralls_body 20 2 6 3 71 4 4.62e4 0.00% 100.00% +klimbs_sub_borrow 69 6 42 7 27 20 4.53e4 0.00% 100.00% +check_recursor_member 72 3 24 14 26 0 4.49e4 0.00% 100.00% +build_peer_recs 29 2 10 5 52 0 4.49e4 0.00% 100.00% +convert_recursor 71 1 8 8 26 0 4.43e4 0.00% 100.00% +convert_univ 33 5 13 5 46 1994 4.36e4 0.00% 100.00% +u64_add 53 1 16 16 32 28 4.36e4 0.00% 100.00% +muts_indc_count_is_one 66 4 50 3 27 25 4.33e4 0.00% 100.00% +ind_is_solo 69 3 52 4 26 0 4.31e4 0.00% 100.00% +build_succ_offset 57 2 17 16 30 0 4.30e4 0.00% 100.00% +expr_glb_let 21 1 6 6 64 0 4.26e4 0.00% 100.00% +level_explicit_val 22 4 7 3 61 274 4.20e4 0.00% 100.00% +build_all_motives_walk 51 3 24 8 32 20 4.20e4 0.00% 100.00% +klimbs_add_carry 67 5 41 7 26 9 4.19e4 0.00% 100.00% +find_peer_recursor_with_spec 67 2 50 3 26 0 4.19e4 0.00% 100.00% +build_rule_rhs 45 1 15 12 35 0 4.17e4 0.00% 100.00% +nlvars_subsume 111 6 49 25 17 3 3.92e4 0.00% 100.00% +compute_k_target 62 6 23 8 26 0 3.88e4 0.00% 100.00% +build_major_params 23 2 5 4 55 0 3.85e4 0.00% 100.00% +collect_n_doms_whnf 40 4 16 7 36 15 3.85e4 0.00% 100.00% +projection_addr_ctor 41 1 23 9 35 0 3.81e4 0.00% 100.00% +nl_add_const 22 4 5 3 53 49 3.53e4 0.00% 100.00% +is_rec_field 13 1 3 2 79 2 3.52e4 0.00% 100.00% +normalize_imax_dispatch 39 8 10 6 34 5 3.50e4 0.00% 100.00% +nl_add_const_go 58 5 22 12 25 0 3.46e4 0.00% 100.00% +nl_le 36 6 12 6 35 6 3.36e4 0.00% 100.00% +peel_motive_params_subst 31 2 9 5 39 12 3.34e4 0.00% 100.00% +klimbs_mul_outer 40 2 16 7 32 1 3.32e4 0.00% 100.00% +se_mentions 39 12 11 5 32 6 3.24e4 0.00% 100.00% +nl_le_vars 28 3 8 5 41 4 3.22e4 0.00% 100.00% +const_idxs_rules 32 2 15 5 36 25 3.11e4 0.00% 100.00% +check_rec_rules_wellscoped 23 2 6 4 46 15 3.09e4 0.00% 100.00% +build_motive_type_flat 48 3 12 10 26 0 3.03e4 0.00% 100.00% +build_recur_addrs 11 1 2 2 79 105 3.02e4 0.00% 100.00% +glist_eq_len 26 4 8 4 41 116 3.00e4 0.00% 100.00% +build_flat_own_params 45 4 24 6 27 25 2.99e4 0.00% 100.00% +put_constructor_proj 31 1 4 4 35 0 2.91e4 0.00% 100.00% +ctors_before_pos 46 5 24 5 26 0 2.90e4 0.00% 100.00% +build_rec_type 45 2 20 5 26 0 2.84e4 0.00% 100.00% +flat_find_pos_kind 43 7 17 5 26 0 2.72e4 0.00% 100.00% +nlvars_dominates 50 4 19 10 23 16 2.68e4 0.00% 100.00% +canonical_rules_at_pos 41 1 10 8 26 0 2.60e4 0.00% 100.00% +klimbs_normalize 48 4 25 7 23 316 2.58e4 0.00% 100.00% +memory[9] 18 0 0 0 46 304 2.45e4 0.00% 100.00% +glist_ordered_insert 73 4 31 16 16 73 2.39e4 0.00% 100.00% +lbr_dec 11 2 2 1 63 150172 2.30e4 0.00% 100.00% +lazy_delta_a_const_b_proj 55 6 24 8 19 0 2.29e4 0.00% 100.00% +memory[11] 20 0 0 0 36 122 1.99e4 0.00% 100.00% +list_length.KRecRule 20 2 7 3 36 25 1.99e4 0.00% 100.00% +flat_member_at 31 3 12 5 26 52 1.99e4 0.00% 100.00% +nlvars_add 102 5 44 23 11 12 1.98e4 0.00% 100.00% +expr_lift_let 21 1 5 5 33 0 1.87e4 0.00% 100.00% +build_ctor_app_params 19 2 3 2 35 0 1.83e4 0.00% 100.00% +rec_to_parent_addr 28 1 12 5 26 69045 1.80e4 0.00% 100.00% +struct_scan_ctors 45 4 19 6 18 0 1.75e4 0.00% 100.00% +is_large_eliminator 41 7 7 4 19 7 1.72e4 0.00% 100.00% +check_rec_major_spine 26 1 9 5 26 0 1.68e4 0.00% 100.00% +check_parent_inductive_shape 24 2 2 2 26 0 1.56e4 0.00% 100.00% +find_rule 25 3 10 3 25 58228 1.54e4 0.00% 100.00% +dec_rewrite_lt_to_le 49 2 14 13 15 0 1.49e4 0.00% 100.00% +klimbs_succ 41 3 23 5 17 107 1.49e4 0.00% 100.00% +build_succ_chain 53 2 20 5 14 141 1.46e4 0.00% 100.00% +list_length.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode 21 2 8 3 27 25 1.45e4 0.00% 100.00% +memory[5] 14 0 0 0 36 17400 1.43e4 0.00% 100.00% +is_defn_or_thm 24 3 3 1 24 459 1.41e4 0.00% 100.00% +list_reverse.G 13 1 3 3 37 180 1.39e4 0.00% 100.00% +se_scan_fields 25 3 8 4 23 0 1.38e4 0.00% 100.00% +level_leq 30 3 9 6 20 70 1.37e4 0.00% 100.00% +check_large_walk_fields 44 5 14 8 15 0 1.34e4 0.00% 100.00% +klimbs_sub 18 2 4 3 26 38 1.19e4 0.00% 100.00% +compute_iprj_addr 30 1 15 8 18 12181 1.19e4 0.00% 100.00% +memory[6] 15 0 0 0 27 337 1.06e4 0.00% 100.00% +se_parent_addr 34 5 13 5 15 151 1.05e4 0.00% 100.00% +klimbs_is_zero 26 2 13 3 18 406 1.04e4 0.00% 100.00% +se_peel_tol 22 3 7 3 20 0 1.02e4 0.00% 100.00% +struct_block_member_addrs 68 2 52 4 9 0 1.00e4 0.00% 100.00% +collect_index_doms 39 4 15 7 13 47 9.85e3 0.00% 100.00% +build_all_minors 14 1 2 2 26 0 9.49e3 0.00% 100.00% +assert_lvls_are_params 25 2 8 4 17 96 9.30e3 0.00% 100.00% +check_large_prop_ctor 27 3 8 4 15 0 8.45e3 0.00% 100.00% +build_all_motives 12 1 2 2 26 0 8.27e3 0.00% 100.00% +list_lift_indices 26 2 7 5 15 19 8.16e3 0.00% 100.00% +assert_occ_param_bvars 27 2 9 4 14 1 7.70e3 0.00% 100.00% +klimbs_add 11 1 2 2 26 16 7.66e3 0.00% 100.00% +peel_leading_foralls_acc 24 2 8 4 15 0 7.57e3 0.00% 100.00% +ctor_subst_param_for 49 3 17 10 9 69 7.31e3 0.00% 100.00% +list_snoc.U8_8 36 2 13 4 11 4 7.25e3 0.00% 100.00% +nlvars_eq 36 6 12 6 11 40 7.25e3 0.00% 100.00% +se_addr_in 24 3 7 4 14 0 6.90e3 0.00% 100.00% +apply_n_projs 24 2 5 4 14 0 6.90e3 0.00% 100.00% +klimbs_div_mod 46 2 14 12 9 0 6.89e3 0.00% 100.00% +list_lift_each 26 2 7 5 13 33 6.72e3 0.00% 100.00% +count_foralls_at_least 23 3 7 3 14 0 6.63e3 0.00% 100.00% +u64_byte_count 150 128 8 1 4 237 6.14e3 0.00% 100.00% +klimbs_mul 14 1 3 3 18 4 5.90e3 0.00% 100.00% +apply_indices_in_conclusion 22 2 5 4 13 19 5.76e3 0.00% 100.00% +klimbs_pow 43 3 12 11 8 0 5.45e3 0.00% 100.00% +klimbs_dec 14 1 4 4 16 120 5.06e3 0.00% 100.00% +struct_is_rec 33 2 16 5 9 160 5.03e3 0.00% 100.00% +mk_nat_lit 10 1 2 2 19 118 4.72e3 0.00% 100.00% +try_eta_expand 45 3 14 10 7 3 4.67e3 0.00% 100.00% +klimbs_eq 44 5 23 5 7 316 4.58e3 0.00% 100.00% +args_contain_bvar 28 4 10 4 9 1 4.32e3 0.00% 100.00% +klimbs_le 27 2 13 3 9 10 4.18e3 0.00% 100.00% +build_rec_lvls_list 21 2 5 4 10 22 3.85e3 0.00% 100.00% +klimbs_shl_limbs 18 2 4 3 11 4 3.82e3 0.00% 100.00% +check_valid_ind_app 35 1 17 8 7 0 3.69e3 0.00% 100.00% +build_param_lvls_range 22 2 5 4 9 47 3.46e3 0.00% 100.00% +peel_leading_foralls 15 1 5 4 11 1 3.25e3 0.00% 100.00% +list_lookup_or_default.Ptr.U8_32 20 2 5 3 9 21 3.18e3 0.00% 100.00% +check_nested_ctors_positivity 51 2 20 9 5 0 3.14e3 0.00% 100.00% +glimbs_to_klimbs 36 2 13 8 6 17 3.01e3 0.00% 100.00% +wrap_lams 22 2 6 4 8 0 2.93e3 0.00% 100.00% +memory[2] 11 0 0 0 12 96 2.80e3 0.00% 100.00% +is_int_dec_prim_addr 33 4 10 7 6 607 2.78e3 0.00% 100.00% +all_bvars_in_args 24 3 7 4 7 0 2.61e3 0.00% 100.00% +nl_covers_const 61 6 24 12 4 2 2.58e3 0.00% 100.00% +intern_int_lit 29 3 8 6 6 300 2.46e3 0.00% 100.00% +try_quot_iota 30 3 8 6 4 0 1.34e3 0.00% 100.00% +subst_param_for 46 3 17 9 3 22 1.20e3 0.00% 100.00% +unfold_b_and_loop 23 2 5 4 4 0 1.06e3 0.00% 100.00% +try_native_dispatch 98 8 37 23 2 0 1.05e3 0.00% 100.00% +klimbs_gcd 20 2 4 4 4 2 9.44e2 0.00% 100.00% +u64_eq 33 9 2 1 3 0 8.93e2 0.00% 100.00% +check_quot 29 5 6 5 3 0 7.97e2 0.00% 100.00% +get_quotient 27 1 15 5 3 0 7.50e2 0.00% 100.00% +convert_quotient 26 1 3 3 3 0 7.26e2 0.00% 100.00% +get_axiom 26 1 14 5 3 0 7.26e2 0.00% 100.00% +convert_axiom 26 1 3 3 3 0 7.26e2 0.00% 100.00% +try_reduce_subtype_val 63 4 26 14 2 0 7.02e2 0.00% 100.00% +try_quot_lift 59 3 22 14 2 0 6.62e2 0.00% 100.00% +run_claim 128 5 71 8 1 0 6.56e2 0.00% 100.00% +klimbs_land 52 3 31 6 2 0 5.92e2 0.00% 100.00% +unpack_def_kind_safety 17 9 1 1 3 1338 5.12e2 0.00% 100.00% +bitvec_prep_spine 44 3 15 10 2 0 5.12e2 0.00% 100.00% +bv_to_nat_via 41 4 13 9 2 0 4.82e2 0.00% 100.00% +defn_is_unsafe_ci 15 5 2 1 3 1338 4.65e2 0.00% 100.00% +quot_extract_arg 39 4 13 8 2 0 4.62e2 0.00% 100.00% +bitvec_of_nat_args_direct 38 4 13 8 2 0 4.52e2 0.00% 100.00% +quot_kind_tag 12 4 1 1 3 0 3.93e2 0.00% 100.00% +idx_to_u64 22 1 10 6 2 167 2.92e2 0.00% 100.00% +mk_bool 20 2 5 4 2 3 2.72e2 0.00% 100.00% +put_expr_list 42 2 24 5 1 0 2.26e2 0.00% 100.00% +canon_cprj_addr 41 1 23 9 1 143 2.21e2 0.00% 100.00% +verify_claim 40 1 1 2 1 0 2.16e2 0.00% 100.00% +u64_and 40 1 9 9 1 0 2.16e2 0.00% 100.00% +klimbs_mod 12 1 3 2 2 0 1.92e2 0.00% 100.00% +list_length_u64.Ptr.Univ 35 2 20 4 1 2 1.91e2 0.00% 100.00% +put_univ_list 33 2 15 5 1 0 1.81e2 0.00% 100.00% +unfold_both_and_loop 31 3 8 6 1 0 1.71e2 0.00% 100.00% +check_eq_type 24 1 15 4 1 0 1.36e2 0.00% 100.00% +mk_nat_binop_stuck 24 1 7 7 1 0 1.36e2 0.00% 100.00% +put_refs 22 1 11 4 1 113 1.26e2 0.00% 100.00% +put_sharing 22 1 11 4 1 113 1.26e2 0.00% 100.00% +put_address_list 22 2 6 4 1 0 1.26e2 0.00% 100.00% +put_univs 22 1 11 4 1 113 1.26e2 0.00% 100.00% +delta_rank 22 2 2 1 1 1 1.26e2 0.00% 100.00% +klimbs_shr 18 1 5 5 1 0 1.06e2 0.00% 100.00% +get_opt_addr 18 2 5 3 1 0 1.06e2 0.00% 100.00% +klimbs_div 12 1 3 2 1 0 7.60e1 0.00% 100.00% +assert_wire_bool 10 1 2 2 1 98 6.60e1 0.00% 100.00% +string_append_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +bool_true_addr 9 1 2 2 1 144 6.10e1 0.00% 100.00% +size_of_size_of_addr 9 1 2 2 1 493 6.10e1 0.00% 100.00% +quot_type_addr 9 1 2 2 1 0 6.10e1 0.00% 100.00% +string_back_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +string_legacy_back_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +string_to_byte_array_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +string_dec_eq_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +str_addr 9 1 2 2 1 34 6.10e1 0.00% 100.00% +nat_zero_addr 9 1 2 2 1 22 6.10e1 0.00% 100.00% +nat_succ_addr_iota 9 1 2 2 1 4454 6.10e1 0.00% 100.00% +nat_pred_addr 9 1 2 2 1 2058 6.10e1 0.00% 100.00% +nat_add_addr 9 1 2 2 1 25720 6.10e1 0.00% 100.00% +nat_sub_addr 9 1 2 2 1 533 6.10e1 0.00% 100.00% +nat_mul_addr 9 1 2 2 1 523 6.10e1 0.00% 100.00% +nat_pow_addr 9 1 2 2 1 510 6.10e1 0.00% 100.00% +nat_gcd_addr 9 1 2 2 1 513 6.10e1 0.00% 100.00% +nat_mod_addr 9 1 2 2 1 634 6.10e1 0.00% 100.00% +fin_addr 9 1 2 2 1 14009 6.10e1 0.00% 100.00% +decidable_rec_addr 9 1 2 2 1 2 6.10e1 0.00% 100.00% +nat_addr_io 9 1 2 2 1 54 6.10e1 0.00% 100.00% +quot_ctor_addr 9 1 2 2 1 2 6.10e1 0.00% 100.00% +quot_lift_addr_iota 9 1 2 2 1 4 6.10e1 0.00% 100.00% +quot_ind_addr 9 1 2 2 1 1 6.10e1 0.00% 100.00% +nat_div_addr 9 1 2 2 1 635 6.10e1 0.00% 100.00% +nat_land_addr 9 1 2 2 1 505 6.10e1 0.00% 100.00% +nat_lor_addr 9 1 2 2 1 503 6.10e1 0.00% 100.00% +nat_xor_addr 9 1 2 2 1 503 6.10e1 0.00% 100.00% +nat_shift_left_addr 9 1 2 2 1 503 6.10e1 0.00% 100.00% +nat_shift_right_addr 9 1 2 2 1 503 6.10e1 0.00% 100.00% +nat_beq_addr 9 1 2 2 1 505 6.10e1 0.00% 100.00% +nat_ble_addr 9 1 2 2 1 501 6.10e1 0.00% 100.00% +int_dec_lt_addr_dec 9 1 2 2 1 492 6.10e1 0.00% 100.00% +bool_false_addr 9 1 2 2 1 123 6.10e1 0.00% 100.00% +system_platform_num_bits_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +nat_dec_le_addr_dec 9 1 2 2 1 842 6.10e1 0.00% 100.00% +nat_dec_eq_addr_dec 9 1 2 2 1 828 6.10e1 0.00% 100.00% +nat_dec_lt_addr_dec 9 1 2 2 1 827 6.10e1 0.00% 100.00% +decidable_is_true_addr_dec 9 1 2 2 1 143 6.10e1 0.00% 100.00% +decidable_is_false_addr_dec 9 1 2 2 1 122 6.10e1 0.00% 100.00% +nat_le_of_ble_eq_true_addr_dec 9 1 2 2 1 6 6.10e1 0.00% 100.00% +nat_eq_of_beq_eq_true_addr_dec 9 1 2 2 1 136 6.10e1 0.00% 100.00% +nat_ne_of_beq_eq_false_addr_dec 9 1 2 2 1 122 6.10e1 0.00% 100.00% +bool_type_addr_dec 9 1 2 2 1 266 6.10e1 0.00% 100.00% +eq_refl_addr_dec 9 1 2 2 1 266 6.10e1 0.00% 100.00% +int_dec_eq_addr_dec 9 1 2 2 1 494 6.10e1 0.00% 100.00% +int_dec_le_addr_dec 9 1 2 2 1 496 6.10e1 0.00% 100.00% +string_of_list_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +int_of_nat_addr_dec 9 1 2 2 1 13 6.10e1 0.00% 100.00% +int_neg_succ_addr_dec 9 1 2 2 1 11 6.10e1 0.00% 100.00% +punit_size_of_1_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +bit_vec_to_nat_addr 9 1 2 2 1 715 6.10e1 0.00% 100.00% +bit_vec_of_nat_addr 9 1 2 2 1 1 6.10e1 0.00% 100.00% +bit_vec_addr 9 1 2 2 1 97 6.10e1 0.00% 100.00% +reduce_bool_addr 9 1 2 2 1 494 6.10e1 0.00% 100.00% +lt_lt_addr 9 1 2 2 1 199 6.10e1 0.00% 100.00% +reduce_nat_addr 9 1 2 2 1 494 6.10e1 0.00% 100.00% +bit_vec_ult_addr 9 1 2 2 1 712 6.10e1 0.00% 100.00% +decidable_decide_addr 9 1 2 2 1 712 6.10e1 0.00% 100.00% +system_platform_get_num_bits_addr 9 1 2 2 1 0 6.10e1 0.00% 100.00% +subtype_val_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +string_utf8_byte_size_addr 9 1 2 2 1 496 6.10e1 0.00% 100.00% +canon_cmp_klimbs 29 2 7 7 0 0 0 0.00% 100.00% +put_axiom 44 1 22 5 0 0 0 0.00% 100.00% +nlvars_max_offset 47 3 19 10 0 0 0 0.00% 100.00% +put_quotient 44 1 22 5 0 0 0 0.00% 100.00% +put_u64_list 29 2 13 4 0 0 0 0.00% 100.00% +app_telescope_count 67 2 35 4 0 0 0 0.00% 100.00% +lam_telescope_count 67 2 35 4 0 0 0 0.00% 100.00% +canon_cmp_krec_rule_ctx 26 1 8 5 0 0 0 0.00% 100.00% +canon_cmp_krec_rule_list_ctx 40 4 17 6 0 0 0 0.00% 100.00% +all_telescope_count 67 2 35 4 0 0 0 0.00% 100.00% +put_univ 53 5 22 6 0 0 0 0.00% 100.00% +put_app_telescope 74 2 39 5 0 0 0 0.00% 100.00% +try_str_dispatch 128 18 47 28 0 0 0 0.00% 100.00% +try_str_back 70 4 27 17 0 0 0 0.00% 100.00% +u64_or 40 1 9 9 0 0 0 0.00% 100.00% +u64_xor_kbits 40 1 9 9 0 0 0 0.00% 100.00% +try_str_to_byte_array 64 5 26 14 0 0 0 0.00% 100.00% +klimbs_lor 52 3 31 6 0 0 0 0.00% 100.00% +extract_aux_occ_us 46 4 14 6 0 0 0 0.00% 100.00% +extract_aux_spec_params 27 1 10 6 0 0 0 0.00% 100.00% +spec_params_lower 28 2 8 6 0 0 0 0.00% 100.00% +klimbs_xor_op 52 3 31 6 0 0 0 0.00% 100.00% +klimbs_shl 18 1 5 5 0 0 0 0.00% 100.00% +aux_already_in 33 5 11 5 0 0 0 0.00% 100.00% +kexpr_struct_eq 59 28 13 6 0 0 0 0.00% 100.00% +level_list_struct_eq 30 5 9 5 0 0 0 0.00% 100.00% +spec_params_ptr_eq 30 5 9 5 0 0 0 0.00% 100.00% +extract_aux_spec_params_from_rec 26 2 3 2 0 0 0 0.00% 100.00% +first_recr_parent_block 107 5 77 8 0 0 0 0.00% 100.00% +put_mut_const_list 66 2 50 4 0 0 0 0.00% 100.00% +detect_aux_from_recrs_ex 66 2 50 3 0 0 0 0.00% 100.00% +aux_from_recrs_walk_ex 138 9 90 14 0 0 0 0.00% 100.00% +flat_find_pos 29 3 11 4 0 0 0 0.00% 100.00% +canon_kind_ord 27 8 1 1 0 0 0 0.00% 100.00% +canon_cmp_member_ctx 48 2 7 5 0 0 0 0.00% 100.00% +put_constructor 73 1 25 8 0 0 0 0.00% 100.00% +put_constructor_list 55 2 39 4 0 0 0 0.00% 100.00% +canon_cmp_member_same_kind_ctx 118 8 37 22 0 0 0 0.00% 100.00% +canon_cmp_ctor_range_ctx 63 2 34 8 0 0 0 0.00% 100.00% +apply_spec_params_lifted 26 2 7 5 0 0 0 0.00% 100.00% +put_inductive 77 1 34 10 0 0 0 0.00% 100.00% +canon_cmp_ctor_pair_ctx 83 3 23 14 0 0 0 0.00% 100.00% +nlvars_any_offset_geq 48 3 19 10 0 0 0 0.00% 100.00% +put_lam_telescope 74 2 39 5 0 0 0 0.00% 100.00% +char_of_nat_addr 9 1 2 2 0 0 0 0.00% 100.00% +canon_member_ci 26 1 15 4 0 0 0 0.00% 100.00% +canon_member_num_ctors 26 2 14 2 0 0 0 0.00% 100.00% +utf8_last_codepoint 10 1 2 2 0 0 0 0.00% 100.00% +canon_build_ctx_classes 29 2 8 5 0 0 0 0.00% 100.00% +unfold_a_and_loop 23 2 5 4 0 0 0 0.00% 100.00% +canon_build_ctx_members 64 3 24 14 0 0 0 0.00% 100.00% +canon_ctor_ctx_entries 24 2 5 4 0 0 0 0.00% 100.00% +canon_sort_loop 31 3 8 6 0 0 0 0.00% 100.00% +canon_refine_classes 26 2 7 5 0 0 0 0.00% 100.00% +canon_refine_one 24 3 6 4 0 0 0 0.00% 100.00% +canon_ins_sort 23 2 6 4 0 0 0 0.00% 100.00% +canon_insert_sorted 58 3 33 7 0 0 0 0.00% 100.00% +utf8_last_go 23 2 7 4 0 0 0 0.00% 100.00% +canon_group_consec 26 2 7 5 0 0 0 0.00% 100.00% +canon_group_walk 65 3 35 9 0 0 0 0.00% 100.00% +find_peer_rec_spec_walk 131 10 85 12 0 0 0 0.00% 100.00% +utf8_cont 13 1 3 3 0 0 0 0.00% 100.00% +canon_classes_eq 31 5 10 5 0 0 0 0.00% 100.00% +canon_flatten 21 2 6 4 0 0 0 0.00% 100.00% +canon_all_singleton 22 3 6 4 0 0 0 0.00% 100.00% +list_nil_addr 9 1 2 2 0 0 0 0.00% 100.00% +str_lit_to_ctor 49 1 21 21 0 0 0 0.00% 100.00% +put_all_telescope 74 2 39 5 0 0 0 0.00% 100.00% +build_char_list 40 2 12 9 0 0 0 0.00% 100.00% +str_lit_delta_step 62 5 31 10 0 0 0 0.00% 100.00% +char_lit_codepoint 23 2 7 4 0 0 0 0.00% 100.00% +get_ci_dprj 130 1 109 6 0 0 0 0.00% 100.00% +canon_cmp_klimbs_tail 44 2 24 6 0 0 0 0.00% 100.00% +punit_addr 9 1 2 2 0 0 0 0.00% 100.00% +unit_addr 9 1 2 2 0 0 0 0.00% 100.00% +char_lit_codepoint_syn 43 6 18 7 0 0 0 0.00% 100.00% +klimbs_scalar_value 117 7 63 21 0 0 0 0.00% 100.00% +pack_def_kind_safety 18 9 1 1 0 0 0 0.00% 100.00% +canon_cmp_u64_lex 53 1 16 16 0 0 0 0.00% 100.00% +spec_params_dom_prefix_match 33 4 10 6 0 0 0 0.00% 100.00% +get_ci_rprj 121 1 108 6 0 0 0 0.00% 100.00% +nat_not_le_of_not_ble_eq_true_addr_dec 9 1 2 2 0 0 0 0.00% 100.00% +utf8_encode_prepend 212 4 100 51 0 0 0 0.00% 100.00% +char_type_addr 9 1 2 2 0 0 0 0.00% 100.00% +mk_nat_literal_64 13 1 4 4 0 0 0 0.00% 100.00% +put_quot_kind 16 4 2 2 0 0 0 0.00% 100.00% +canon_cmp_bytes 32 4 10 6 0 0 0 0.00% 100.00% +canon_g_list_eq 27 5 8 4 0 0 0 0.00% 100.00% +literal_eq 18 4 2 2 0 0 0 0.00% 100.00% +try_reduce_size_of_unit 71 5 29 16 0 0 0 0.00% 100.00% +check_native_bool 32 3 10 7 0 0 0 0.00% 100.00% +put_definition 68 1 42 8 0 0 0 0.00% 100.00% +canon_cmp_kexpr_ctx 29 2 12 4 0 0 0 0.00% 100.00% +put_mut_const 62 3 3 3 0 0 0 0.00% 100.00% +check_native_nat 21 3 7 3 0 0 0 0.00% 100.00% +put_recursor_rule 40 1 21 4 0 0 0 0.00% 100.00% +canon_cmp_kexpr_node_ctx 79 40 12 7 0 0 0 0.00% 100.00% +put_recursor_rule_list 30 2 14 4 0 0 0 0.00% 100.00% +list_cons_addr 9 1 2 2 0 0 0 0.00% 100.00% +klimbs_from_g 25 1 11 7 0 0 0 0.00% 100.00% +leaf_hash 17 1 5 5 0 0 0 0.00% 100.00% +node_hash 19 1 6 6 0 0 0 0.00% 100.00% +parse_atree_body 31 3 11 6 0 0 0 0.00% 100.00% +load_assumption_tree 96 1 84 6 0 0 0 0.00% 100.00% +addr_set_build 37 2 16 4 0 0 0 0.00% 100.00% +addr_set_member 16 1 2 2 0 0 0 0.00% 100.00% +env_walk 102 10 58 8 0 0 0 0.00% 100.00% +env_walk_refs 40 4 6 5 0 0 0 0.00% 100.00% +env_walk_leaves 31 2 4 4 0 0 0 0.00% 100.00% +run_check_env 38 3 16 6 0 0 0 0.00% 100.00% +walk_char_list_bytes 64 8 22 14 0 0 0 0.00% 100.00% +get_opt_u64_masked 23 2 11 2 0 0 0 0.00% 100.00% +get_opt_addr_masked 16 2 4 2 0 0 0 0.00% 100.00% +get_opt_bool_masked 16 2 4 2 0 0 0 0.00% 100.00% +get_opt_def_kind_masked 18 4 4 2 0 0 0 0.00% 100.00% +get_opt_quot_kind_masked 19 5 4 2 0 0 0 0.00% 100.00% +get_reveal_rule_list_inner 59 2 32 6 0 0 0 0.00% 100.00% +get_opt_rule_list_masked 27 2 13 3 0 0 0 0.00% 100.00% +get_reveal_ctor_info 80 1 64 9 0 0 0 0.00% 100.00% +get_ctor_entry 61 1 51 3 0 0 0 0.00% 100.00% +get_ctor_entry_list_inner 90 2 63 6 0 0 0 0.00% 100.00% +get_opt_ctor_entry_list_masked 27 2 13 3 0 0 0 0.00% 100.00% +get_reveal_mut_const_info 126 3 90 14 0 0 0 0.00% 100.00% +get_mut_entry 75 1 65 3 0 0 0 0.00% 100.00% +get_mut_entry_list_inner 104 2 77 6 0 0 0 0.00% 100.00% +get_reveal_info 134 11 90 14 0 0 0 0.00% 100.00% +expr_addr 34 1 22 5 0 0 0 0.00% 100.00% +def_safety_tag 11 3 1 1 0 0 0 0.00% 100.00% +check_opt_def_kind 18 2 3 3 0 0 0 0.00% 100.00% +check_opt_def_safety 18 2 3 3 0 0 0 0.00% 100.00% +check_opt_quot_kind 18 2 3 3 0 0 0 0.00% 100.00% +check_opt_bool 12 2 1 1 0 0 0 0.00% 100.00% +check_opt_u64 26 2 1 1 0 0 0 0.00% 100.00% +check_opt_addr 80 2 65 3 0 0 0 0.00% 100.00% +check_opt_expr_addr 83 2 66 4 0 0 0 0.00% 100.00% +check_recr_rules 67 2 39 6 0 0 0 0.00% 100.00% +check_opt_recr_rules 14 2 1 2 0 0 0 0.00% 100.00% +check_ctor_entry 97 1 35 8 0 0 0 0.00% 100.00% +check_ctor_entries 67 2 51 4 0 0 0 0.00% 100.00% +check_opt_ctor_entries 14 2 1 2 0 0 0 0.00% 100.00% +check_mut_const 127 3 1 10 0 0 0 0.00% 100.00% +check_muts_components 128 2 110 5 0 0 0 0.00% 100.00% +run_reveal 139 9 49 11 0 0 0 0.00% 100.00% +run_contains 14 1 3 3 0 0 0 0.00% 100.00% +has_bvar_in_range 75 11 29 14 0 0 0 0.00% 100.00% +has_bvar_in_range_binder 19 2 3 3 0 0 0 0.00% 100.00% +mk_nat_one 13 1 4 4 0 0 0 0.00% 100.00% +has_bvar_in_range_let 24 3 4 4 0 0 0 0.00% 100.00% +list_length_u64.U8_8 42 2 27 4 0 0 0 0.00% 100.00% +list_concat.Tup.Ptr.U8_32.G 23 2 7 4 0 0 0 0.00% 100.00% +try_quot_ind 59 3 22 14 0 0 0 0.00% 100.00% +rbtree_map_lookup_or_default.G 64 4 28 10 0 0 0 0.00% 100.00% +defn_member_recur_addrs 30 2 4 3 0 0 0 0.00% 100.00% +put_expr 110 12 59 8 0 0 0 0.00% 100.00% +put_u64_le 26 2 4 3 0 0 0 0.00% 100.00% +list_length_u64.Constructor 68 2 53 4 0 0 0 0.00% 100.00% +univ_succ_count 49 2 26 4 0 0 0 0.00% 100.00% +list_length.U8_8 25 2 12 3 0 0 0 0.00% 100.00% +list_lookup_u64.MutConst 127 2 102 5 0 0 0 0.00% 100.00% +list_length_u64.MutConst 79 2 64 4 0 0 0 0.00% 100.00% +list_length_u64.RecursorRule 43 2 28 4 0 0 0 0.00% 100.00% +list_lookup_u64.Constructor 105 2 80 5 0 0 0 0.00% 100.00% +byte_array_empty_addr 9 1 2 2 0 0 0 0.00% 100.00% +list_snoc.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode 28 2 9 4 0 0 0 0.00% 100.00% +try_str_dec_eq 71 7 29 14 0 0 0 0.00% 100.00% +try_reduce_bit_vec_ult 63 4 24 15 0 0 0 0.00% 100.00% +str_dec_eq_build 123 2 43 35 0 0 0 0.00% 100.00% +rbtree_map_insert.G 22 1 7 2 0 0 0 0.00% 100.00% +put_tag2 33 3 6 5 0 0 0 0.00% 100.00% +canon_ord_cmp_g 37 3 14 7 0 0 0 0.00% 100.00% +canon_ord_then 12 2 2 1 0 0 0 0.00% 100.00% +rbtree_map_ins.G 77 4 39 11 0 0 0 0.00% 100.00% +rbtree_map_balance.G 34 2 7 3 0 0 0 0.00% 100.00% +rbtree_map_balance_fix.G 122 57 31 8 0 0 0 0.00% 100.00% +canon_sord_lt_strong 6 1 1 1 0 0 0 0.00% 100.00% +univ_succ_base 40 2 19 3 0 0 0 0.00% 100.00% +canon_sord_eq_strong 6 1 1 1 0 0 0 0.00% 100.00% +canon_sord_gt_strong 6 1 1 1 0 0 0 0.00% 100.00% +canon_sord_then 14 2 2 1 0 0 0 0.00% 100.00% +canon_sord_of_g 7 1 1 1 0 0 0 0.00% 100.00% +canon_addr_cmp 105 1 80 18 0 0 0 0.00% 100.00% +canon_addr_chunk 17 1 2 2 0 0 0 0.00% 100.00% +canon_ctx_class_idx 25 3 8 4 0 0 0 0.00% 100.00% +canon_ctx_cmp_addr 32 5 8 6 0 0 0 0.00% 100.00% +bitvec_prep_spine_ult 46 4 16 10 0 0 0 0.00% 100.00% +memory[19] 28 0 0 0 0 0 0 0.00% 100.00% +np_whnf_inner_bv 16 1 5 4 0 0 0 0.00% 100.00% +put_recursor 98 1 36 12 0 0 0 0.00% 100.00% +canon_cmp_kuniv 44 16 10 6 0 0 0 0.00% 100.00% +canon_cmp_kuniv_list 32 4 10 6 0 0 0 0.00% 100.00% +memory[50] 59 0 0 0 0 0 0 0.00% 100.00% +memory[64] 73 0 0 0 0 0 0 0.00% 100.00% +canon_cmp_kliteral 18 4 2 2 0 0 0 0.00% 100.00% diff --git a/cold-groups/kstats2-String.split.txt b/cold-groups/kstats2-String.split.txt new file mode 100644 index 00000000..7b769e52 --- /dev/null +++ b/cold-groups/kstats2-String.split.txt @@ -0,0 +1,739 @@ +=== Circuit Statistics === +Circuits: 730 +Total width: 33331 +Total FFT cost: 49507530863 (4.95e10) +Total cache hits: 22638136 +Total saved cost: 51.38% +--------------------------------------------------------------------------------------------------------------------------------------------- +Name Width Sel Aux Lkp Height Hits FFT cost % %++ +--------------------------------------------------------------------------------------------------------------------------------------------- +blake3_compress_inner_j 696 1 369 193 136626 0 8.12e9 16.39% 16.39% +memory[3] 12 0 0 0 2947763 6323771 3.91e9 7.89% 24.29% +blake3_compress_chunks 29 3 7 4 1157705 0 3.42e9 6.91% 31.20% +expr_inst_many_walk 34 9 8 5 915195 0 3.11e9 6.29% 37.49% +expr_inst_many 21 2 4 4 1199626 299856 2.59e9 5.23% 42.72% +blake3_compress 1080 1 929 40 19518 15 1.50e9 3.04% 45.75% +get_expr 50 12 23 5 309599 20 1.42e9 2.87% 48.63% +convert_expr 60 12 25 7 240901 122716 1.30e9 2.63% 51.25% +k_infer_app_spine_loop 59 8 21 11 241267 677 1.28e9 2.59% 53.84% +list_drop.Ptr.Expr 20 2 6 3 592814 270333 1.16e9 2.34% 56.18% +expr_lbr 35 9 9 6 350993 2611613 1.14e9 2.31% 58.49% +list_snoc.G 22 2 6 4 521574 184967 1.11e9 2.24% 60.73% +get_tag4 37 2 22 4 311460 0 1.06e9 2.15% 62.88% +g_list_has 21 3 6 3 396339 3419 7.88e8 1.59% 64.47% +get_app_telescope 43 2 15 6 204828 0 7.84e8 1.58% 66.05% +expr_glb_walk 34 10 8 5 231083 0 7.08e8 1.43% 67.48% +validate_expr_well_scoped 52 9 20 8 144351 118355 6.48e8 1.31% 68.79% +peel_beta 32 3 12 5 221723 3113 6.38e8 1.29% 70.08% +memory[4] 13 0 0 0 497573 4533682 6.30e8 1.27% 71.35% +expr_inst_many_bvar 24 2 5 5 278974 0 6.16e8 1.24% 72.60% +expr_inst1_walk 34 9 8 5 202168 0 6.13e8 1.24% 73.84% +get_u64_le 28 2 14 3 240867 22 6.12e8 1.24% 75.07% +collect_spine 23 2 8 4 281491 197009 5.96e8 1.20% 76.28% +list_concat.Ptr.KExprNode 22 2 6 4 278551 242297 5.64e8 1.14% 77.42% +whnf_with_spine 34 6 11 5 175764 4941 5.27e8 1.06% 78.48% +expr_lower_walk 53 10 18 9 115078 0 5.17e8 1.04% 79.52% +k_infer_core 53 9 22 8 112780 54815 5.06e8 1.02% 80.54% +expr_inst1 21 2 4 4 261823 104786 5.04e8 1.02% 81.56% +const_idxs_expr 52 7 26 7 110757 166346 4.87e8 0.98% 82.55% +expr_glb 21 2 5 4 240811 257285 4.61e8 0.93% 83.48% +list_lookup.Ptr.KLevelNode 16 1 5 3 294825 71690 4.39e8 0.89% 84.36% +list_length.Ptr.KExprNode 18 2 5 3 249239 712085 4.11e8 0.83% 85.19% +expr_lift_walk 34 9 8 5 139072 0 4.09e8 0.83% 86.02% +safe_refs_only 43 9 19 5 111679 109780 4.07e8 0.82% 86.84% +expr_lift 23 3 5 4 182612 389282 3.74e8 0.75% 87.60% +bytes_to_block 265 1 193 65 18371 661 3.45e8 0.70% 88.29% +whnf_const_head 77 16 32 10 44889 0 2.69e8 0.54% 88.84% +expr_lower 23 3 5 4 130790 108524 2.60e8 0.53% 89.36% +memory[18] 27 0 0 0 110757 606238 2.55e8 0.51% 89.88% +blake3_compress_block 211 2 169 15 17109 0 2.54e8 0.51% 90.39% +k_infer 15 1 4 4 167595 29463 2.24e8 0.45% 90.84% +get_expr_list 42 2 15 6 63218 309 2.14e8 0.43% 91.28% +k_is_def_eq 29 3 7 6 83990 46963 2.02e8 0.41% 91.68% +ctx_trim 52 3 19 12 48098 190084 1.96e8 0.40% 92.08% +apply_spine_expr 22 2 6 4 104043 16635 1.94e8 0.39% 92.47% +get_u64_list 49 2 22 6 46876 0 1.80e8 0.36% 92.84% +get_address 138 1 98 34 17795 109 1.74e8 0.35% 93.19% +get_tag0 40 2 23 5 53295 2412 1.69e8 0.34% 93.53% +whnf 38 6 14 6 47030 19542 1.40e8 0.28% 93.81% +address_eq 82 2 66 4 22618 19841 1.35e8 0.27% 94.09% +try_reduce_projection_definition 59 3 24 13 29751 4863 1.31e8 0.27% 94.35% +whnf_apply_beta 34 3 10 7 48959 0 1.31e8 0.27% 94.62% +Bytes2 24 0 0 0 65536 0 1.28e8 0.26% 94.88% +k_check 15 1 3 3 99155 88585 1.27e8 0.26% 95.13% +const_idxs_exprs 24 2 7 5 60784 1859 1.18e8 0.24% 95.37% +try_prim_dispatch 30 6 8 4 48652 4883 1.15e8 0.23% 95.60% +list_take.Ptr.KExprNode 23 2 7 4 57432 26941 1.06e8 0.22% 95.82% +whnf_nd_with_spine 34 6 11 5 38656 4799 1.02e8 0.21% 96.02% +ctx_seek_cut 44 2 16 10 27929 2587 9.18e7 0.19% 96.21% +expr_inst_levels_walk 36 9 9 6 31303 0 8.53e7 0.17% 96.38% +whnf_nd 38 6 14 6 29812 3465 8.53e7 0.17% 96.55% +pad_block 18 2 4 3 53030 230 7.68e7 0.16% 96.71% +try_def_eq_app 49 6 18 9 21499 1644 7.66e7 0.15% 96.86% +get_lam_telescope 42 2 15 6 23359 1 7.20e7 0.15% 97.01% +expr_glb_binder 16 1 4 4 53542 191 6.92e7 0.14% 97.15% +try_iota 108 5 39 25 9346 388 6.69e7 0.14% 97.28% +k_def_eq_rebase 44 2 12 11 19680 0 6.25e7 0.13% 97.41% +try_string_lit_one 28 3 8 5 28280 0 5.96e7 0.12% 97.53% +k_is_def_eq_core 40 2 15 8 19045 7010 5.48e7 0.11% 97.64% +memory[32] 41 0 0 0 18539 87446 5.46e7 0.11% 97.75% +get_address_list 42 2 15 6 17784 1775 5.34e7 0.11% 97.86% +expr_inst_levels 20 2 6 3 32535 56169 4.99e7 0.10% 97.96% +get_all_telescope 42 2 15 6 15506 8 4.59e7 0.09% 98.05% +try_nat_linear_rec 75 5 27 17 9011 306 4.47e7 0.09% 98.14% +de_args 32 5 10 5 19108 5106 4.42e7 0.09% 98.23% +walk_refs_transitive 27 4 6 5 21264 546 4.20e7 0.08% 98.32% +expr_inst1_bvar 20 3 4 3 26224 0 3.94e7 0.08% 98.40% +whnf_proj_head 61 4 28 10 9276 0 3.76e7 0.08% 98.47% +ctx_close_cut 46 3 17 10 11451 3941 3.59e7 0.07% 98.55% +k_ensure_sort 18 1 7 4 24483 12547 3.30e7 0.07% 98.61% +k_is_def_eq_slow_nd 32 4 9 6 14140 0 3.17e7 0.06% 98.68% +whnf_nd_const_head 55 9 23 7 8646 0 3.14e7 0.06% 98.74% +blake3_compress_layer 223 3 170 6 2324 0 2.91e7 0.06% 98.80% +k_infer_only 93 12 45 15 4753 2955 2.72e7 0.05% 98.85% +k_is_def_eq_slow 26 4 7 4 14140 0 2.59e7 0.05% 98.91% +k_is_def_eq_ordered 19 2 4 3 18630 415 2.58e7 0.05% 98.96% +k_is_def_eq_struct_safe 40 9 12 6 9419 39 2.52e7 0.05% 99.01% +try_reduce_fin_val_decidable_rec 149 9 58 37 2472 9544 2.08e7 0.04% 99.05% +blake3_finish 190 11 151 9 1950 0 2.03e7 0.04% 99.09% +whnf_iota_major 51 3 24 9 5749 3630 1.85e7 0.04% 99.13% +list_is_empty.U8 15 2 4 2 16811 16906 1.83e7 0.04% 99.17% +cleanup_nat_offset_major 45 5 19 8 6158 12476 1.77e7 0.04% 99.20% +get_constant 162 3 136 9 1860 0 1.64e7 0.03% 99.24% +whnf_nd_apply_beta 34 3 10 7 7111 0 1.57e7 0.03% 99.27% +try_match_nat_add 47 6 17 9 5013 0 1.47e7 0.03% 99.30% +ctx_next_cut 16 1 6 4 12876 23232 1.45e7 0.03% 99.33% +try_eta_struct 91 8 48 14 2712 483 1.42e7 0.03% 99.36% +blake3_next_layer 221 4 136 5 1074 0 1.20e7 0.02% 99.38% +try_struct_eta_iota 93 9 39 16 2179 0 1.13e7 0.02% 99.40% +k_is_def_eq_slow2 58 9 20 11 3064 0 1.04e7 0.02% 99.42% +load_verified_constant 100 1 88 5 1860 2402 1.02e7 0.02% 99.44% +whnf_nd_proj_head 61 4 28 10 2740 0 9.64e6 0.02% 99.46% +get_ci 97 10 68 7 1765 82225 9.30e6 0.02% 99.48% +blake3 86 1 72 8 1950 140 9.23e6 0.02% 99.50% +try_extract_nat 30 6 9 5 4611 5517 8.58e6 0.02% 99.52% +try_extract_nat_app 33 4 11 6 4219 0 8.54e6 0.02% 99.54% +run_check_transitive 79 7 55 6 1860 17498 8.05e6 0.02% 99.55% +verify_bytes_against 73 1 33 2 1950 0 7.85e6 0.02% 99.57% +const_idxs_of 77 6 7 6 1860 0 7.84e6 0.02% 99.58% +check_const 75 8 20 15 1765 95 7.20e6 0.01% 99.60% +collect_spine_of_ctor 45 3 23 7 2757 6560 7.19e6 0.01% 99.61% +nat_offset_of 58 12 23 9 2153 692 6.99e6 0.01% 99.63% +nat_lit_to_ctor_or_self 43 4 14 10 2758 6563 6.88e6 0.01% 99.64% +memory[34] 43 0 0 0 2651 7671 6.58e6 0.01% 99.65% +str_lit_to_ctor_app_or_self 24 3 7 4 4185 7831 6.19e6 0.01% 99.67% +get_constant_info_by_variant 64 8 46 2 1765 0 6.16e6 0.01% 99.68% +expr_lift_bvar 39 2 14 8 2721 0 6.15e6 0.01% 99.69% +u64_is_zero 25 9 2 1 3017 482566 4.47e6 0.01% 99.70% +relaxed_u64_pred 25 9 2 1 3008 241141 4.45e6 0.01% 99.71% +prim_family 161 23 59 37 595 48057 4.44e6 0.01% 99.72% +try_nat_dispatch_prewhnf 86 8 31 20 972 0 4.18e6 0.01% 99.73% +projection_definition_info 54 5 23 10 1440 29368 4.13e6 0.01% 99.73% +convert_definition 40 5 6 4 1523 0 3.28e6 0.01% 99.74% +lbr_max 35 2 13 7 1601 369274 3.04e6 0.01% 99.75% +try_def_eq_nat 41 4 16 7 1374 185 2.99e6 0.01% 99.75% +lbr_min 35 2 13 7 1544 292203 2.92e6 0.01% 99.76% +expr_mentions_block 40 14 10 5 1354 607 2.87e6 0.01% 99.77% +is_nat_zero 24 4 7 4 2084 664 2.83e6 0.01% 99.77% +assert_safety 15 2 3 2 3122 166 2.83e6 0.01% 99.78% +is_unsafe_ci 29 9 2 1 1765 2323 2.82e6 0.01% 99.78% +replace_spine_major 23 1 7 7 2124 164 2.78e6 0.01% 99.79% +head_addr 24 2 9 4 2009 1093 2.72e6 0.01% 99.79% +const_num_lvls 27 8 1 1 1764 13102 2.63e6 0.01% 99.80% +const_type_of 27 8 1 1 1764 1101 2.63e6 0.01% 99.80% +flatten_u64 14 1 1 1 3008 93860 2.48e6 0.01% 99.81% +get_definition 30 1 18 6 1523 0 2.47e6 0.00% 99.81% +memo_u32_less_than 28 1 13 7 1612 2290680 2.46e6 0.00% 99.82% +lazy_delta_loop 35 7 10 5 1326 178 2.45e6 0.00% 99.82% +run_check 24 1 14 4 1765 0 2.35e6 0.00% 99.83% +peel_params_subst 30 2 11 5 1420 297 2.28e6 0.00% 99.83% +try_unit_like 28 2 7 6 1428 208 2.15e6 0.00% 99.84% +level_struct_eq 39 12 11 5 1070 750 2.14e6 0.00% 99.84% +memory[12] 21 0 0 0 1772 97658 2.07e6 0.00% 99.85% +try_proof_irrel 25 2 6 5 1460 208 1.97e6 0.00% 99.85% +k_infer_proj 62 1 39 13 665 0 1.96e6 0.00% 99.85% +whnf_spine 25 2 7 5 1440 780 1.94e6 0.00% 99.86% +read_byte 18 2 5 3 1868 0 1.89e6 0.00% 99.86% +peel_n_alls_whnf 29 3 9 5 1235 0 1.88e6 0.00% 99.87% +is_str_prim_addr 65 8 22 15 582 0 1.76e6 0.00% 99.87% +k_is_def_eq_struct_go 58 26 13 6 623 0 1.70e6 0.00% 99.87% +peel_field_loop 34 2 9 6 956 0 1.64e6 0.00% 99.88% +nl_subsume_entry 121 13 54 24 311 63 1.57e6 0.00% 99.88% +is_native_prim_addr 57 7 19 13 578 0 1.53e6 0.00% 99.88% +is_dec_prim_addr 57 7 19 13 577 0 1.53e6 0.00% 99.89% +level_imax 37 6 13 6 816 8708 1.49e6 0.00% 99.89% +try_nat_binop_dispatch 65 6 24 14 467 232 1.36e6 0.00% 99.89% +convert_univ_idxs 38 2 16 7 728 19588 1.34e6 0.00% 99.89% +level_list_inst 25 2 7 5 1035 2276 1.33e6 0.00% 99.90% +level_inst_params 28 5 7 5 935 1077 1.33e6 0.00% 99.90% +try_reduce_decide_bitvec_lt 165 8 72 40 194 15 1.22e6 0.00% 99.90% +get_univ 55 5 33 6 464 53 1.15e6 0.00% 99.90% +level_eq 36 10 10 5 653 177 1.12e6 0.00% 99.91% +is_prop_type 30 3 11 5 692 774 1.00e6 0.00% 99.91% +utf8_decode_one 76 4 32 17 306 0 9.71e5 0.00% 99.91% +peel_n_foralls 21 2 7 3 854 75 9.04e5 0.00% 99.91% +is_bitvec_prim_addr 33 4 10 7 580 0 8.99e5 0.00% 99.91% +try_eta_swap 30 4 11 4 625 49 8.93e5 0.00% 99.92% +lazy_delta_step_const_const 120 6 60 22 188 0 8.59e5 0.00% 99.92% +get_tag2 40 2 23 5 464 0 8.39e5 0.00% 99.92% +address_eq_tail 84 6 66 3 237 0 7.94e5 0.00% 99.92% +peer_agree_walk 107 5 69 11 190 0 7.76e5 0.00% 99.92% +try_unfold_proj_app 31 3 11 6 535 248 7.71e5 0.00% 99.92% +try_dec_dispatch 70 4 26 16 269 0 7.70e5 0.00% 99.93% +level_max 45 4 17 9 382 123 7.51e5 0.00% 99.93% +level_is_not_zero 27 7 7 4 553 877 7.00e5 0.00% 99.93% +level_max_subsumes 23 3 6 4 622 54 6.86e5 0.00% 99.93% +check_prop_field_if_prop 22 2 5 4 632 33 6.70e5 0.00% 99.93% +lazy_delta_both_proj 39 7 10 7 390 0 6.69e5 0.00% 99.93% +try_lazy_delta_app 72 6 39 10 225 0 6.41e5 0.00% 99.93% +level_max_go 39 6 13 7 375 0 6.39e5 0.00% 99.93% +get_ci_cprj 158 1 142 7 116 1097 6.33e5 0.00% 99.94% +level_max_offsets 47 3 18 10 306 0 6.05e5 0.00% 99.94% +get_mut_const_list 86 2 59 6 177 13 5.75e5 0.00% 99.94% +get_constructor_list 75 2 48 6 198 13 5.74e5 0.00% 99.94% +check_canonical_block 123 3 75 20 127 0 5.50e5 0.00% 99.94% +try_bitvec_dispatch 66 6 23 15 211 0 5.45e5 0.00% 99.94% +build_recur_addrs_walk 71 2 51 5 190 0 5.17e5 0.00% 99.94% +check_positivity_aug 78 5 35 15 175 5 5.15e5 0.00% 99.94% +canon_muts_has_kind 69 6 51 3 185 97 4.87e5 0.00% 99.94% +check_muts_all 66 2 48 4 190 0 4.81e5 0.00% 99.95% +get_univ_list 53 2 24 7 227 1859 4.79e5 0.00% 99.95% +expr_lbr_let 23 1 7 7 448 0 4.70e5 0.00% 99.95% +is_unit_like_type 60 7 34 7 197 1231 4.58e5 0.00% 99.95% +is_inductive_prop 24 1 9 6 421 244 4.56e5 0.00% 99.95% +put_constant 90 9 14 7 140 23 4.54e5 0.00% 99.95% +try_unfold_head 33 5 4 3 315 58 4.43e5 0.00% 99.95% +ctor_at 86 2 72 3 141 3 4.38e5 0.00% 99.95% +check_inductive_shape_ctors 52 2 17 10 211 0 4.31e5 0.00% 99.95% +projection_addr 134 4 105 9 95 127 4.22e5 0.00% 99.95% +ensure_sort_only 30 2 12 5 326 104 4.20e5 0.00% 99.95% +normalize_aux 33 7 8 5 288 104 3.99e5 0.00% 99.96% +check_param_agreement_go 34 2 12 6 272 0 3.84e5 0.00% 99.96% +wrap_foralls 22 2 6 4 390 65 3.83e5 0.00% 99.96% +get_ci_iprj 121 1 108 6 95 1037 3.81e5 0.00% 99.96% +peel_ctor_params_subst 46 3 16 8 210 3 3.80e5 0.00% 99.96% +k_is_def_eq_struct 12 1 2 2 619 49 3.67e5 0.00% 99.96% +try_normalize_int_decidable 64 4 26 13 152 0 3.58e5 0.00% 99.96% +glist_subset 75 5 32 16 131 280 3.50e5 0.00% 99.96% +peel_n_lams_collect 29 3 10 4 281 0 3.42e5 0.00% 99.96% +put_address 106 1 65 34 95 45 3.34e5 0.00% 99.96% +check_no_dep_data_field_if_prop 28 3 7 5 280 11 3.29e5 0.00% 99.96% +muts_member_at 108 2 94 3 92 214 3.27e5 0.00% 99.96% +put_constant_info 64 8 2 2 140 0 3.24e5 0.00% 99.96% +check_positivity_fields 26 2 6 5 294 0 3.24e5 0.00% 99.97% +nl_add_var 43 4 13 9 192 36 3.20e5 0.00% 99.97% +walk_fields_classify 42 3 14 7 192 3 3.13e5 0.00% 99.97% +peel_n_foralls_with_types 27 3 9 4 272 3 3.07e5 0.00% 99.97% +k_synth_gate 71 4 30 14 117 4 2.90e5 0.00% 99.97% +utf8_validate 21 2 6 4 307 64 2.77e5 0.00% 99.97% +normalize_int_dec_rebuild 53 3 16 12 140 0 2.70e5 0.00% 99.97% +try_nat_offset_dispatch 59 4 19 14 126 0 2.64e5 0.00% 99.97% +check_block_peer_param_agreement 81 4 52 4 95 0 2.56e5 0.00% 99.97% +caddr_is_peer 31 2 15 4 208 13 2.56e5 0.00% 99.97% +try_k_synth_iota 59 4 18 12 121 0 2.51e5 0.00% 99.97% +expr_inst1_let 21 1 5 5 269 0 2.38e5 0.00% 99.97% +const_idxs_muts 76 4 53 7 93 94 2.34e5 0.00% 99.97% +check_muts_member_at 74 1 15 5 95 0 2.34e5 0.00% 99.97% +compare_struct_fields 31 3 7 5 192 0 2.33e5 0.00% 99.97% +convert_constructor 57 1 6 6 116 0 2.31e5 0.00% 99.97% +const_idxs_ctors 57 2 40 5 114 91 2.26e5 0.00% 99.97% +check_field_universes_inner 29 2 8 6 197 0 2.25e5 0.00% 99.97% +bytes_to_addr 44 1 34 3 140 23 2.25e5 0.00% 99.97% +delta_unfold 45 4 22 7 137 124 2.24e5 0.00% 99.97% +get_constructor 55 1 41 8 116 0 2.23e5 0.00% 99.98% +compare_rules 89 4 40 16 77 0 2.18e5 0.00% 99.98% +get_expr_let 28 1 8 5 197 0 2.17e5 0.00% 99.98% +level_offset_of 20 2 6 3 258 381 2.16e5 0.00% 99.98% +get_inductive 67 1 51 9 95 0 2.13e5 0.00% 99.98% +build_motive_apps 23 2 5 4 224 0 2.09e5 0.00% 99.98% +bytes_to_u64_limb 50 10 20 3 118 0 2.07e5 0.00% 99.98% +canon_indc_positions 67 3 50 4 93 94 2.07e5 0.00% 99.98% +count_ctors 51 2 38 3 114 94 2.03e5 0.00% 99.98% +get_mut_const 62 3 48 3 95 0 1.97e5 0.00% 99.98% +validate_univ_params_list 20 2 4 4 238 11994 1.96e5 0.00% 99.98% +flat_originals_walk 100 5 68 9 64 0 1.94e5 0.00% 99.98% +put_tag0 32 3 6 5 157 31 1.89e5 0.00% 99.98% +memory[36] 45 0 0 0 114 453 1.79e5 0.00% 99.98% +check_field_universes_skip_params 25 2 7 4 179 0 1.74e5 0.00% 99.98% +memory[47] 56 0 0 0 93 1214 1.74e5 0.00% 99.98% +put_tag4 33 3 6 5 140 0 1.70e5 0.00% 99.98% +dec_dispatch_le_eq 47 5 14 9 102 0 1.64e5 0.00% 99.98% +memory[10] 19 0 0 0 210 59730 1.61e5 0.00% 99.98% +dec_build_proof 95 8 30 22 57 0 1.60e5 0.00% 99.98% +glist_cmp 76 6 32 16 68 200 1.60e5 0.00% 99.98% +convert_inductive 50 1 6 6 95 0 1.59e5 0.00% 99.98% +get_result_sort_level 28 2 9 5 150 222 1.57e5 0.00% 99.98% +try_extract_int 49 6 20 9 92 251 1.50e5 0.00% 99.98% +is_rec_field_peel 40 3 16 7 108 0 1.50e5 0.00% 99.98% +dec_finish 90 4 32 22 56 0 1.48e5 0.00% 99.98% +check_ctor_return_type 37 1 13 12 113 112 1.47e5 0.00% 99.98% +apply_ihs_full 100 2 30 26 51 0 1.46e5 0.00% 99.99% +addr_list_contains 24 3 7 4 159 54 1.45e5 0.00% 99.99% +is_nat_succ_ih_step 58 7 26 10 78 39 1.45e5 0.00% 99.99% +whnf_get_ctor_or_none 26 2 9 5 143 11527 1.38e5 0.00% 99.99% +load_verified_blob 46 1 36 3 89 711 1.36e5 0.00% 99.99% +build_minor_doms 54 2 19 7 77 0 1.33e5 0.00% 99.99% +get_recursor_rule_list 53 2 24 7 77 0 1.31e5 0.00% 99.99% +build_flat_block 159 7 121 12 32 0 1.28e5 0.00% 99.99% +populate_rules 52 3 18 6 77 0 1.28e5 0.00% 99.99% +validate_univ_params_seen 43 5 16 8 87 585 1.24e5 0.00% 99.99% +Bytes1 11 0 0 0 256 0 1.22e5 0.00% 99.99% +is_muts_block 61 2 50 2 64 96 1.19e5 0.00% 99.99% +get_constructor_proj 31 1 21 4 109 0 1.18e5 0.00% 99.99% +flat_find_matching 39 5 15 5 88 10 1.14e5 0.00% 99.99% +mk_nat_offset_stuck 37 2 10 9 88 0 1.08e5 0.00% 99.99% +build_all_minors_walk 55 3 24 8 64 0 1.08e5 0.00% 99.99% +io_peel_field_loop 30 2 9 5 103 17 1.07e5 0.00% 99.99% +nl_subsumption_walk 25 2 7 5 117 46 1.05e5 0.00% 99.99% +build_apply_field_bvars 23 2 5 4 123 36 1.03e5 0.00% 99.99% +check_recursor_canonical_full 125 9 50 18 32 0 1.01e5 0.00% 99.99% +convert_rec_rules 40 2 16 6 77 0 9.93e4 0.00% 99.99% +assert_first_args_are_param_bvars 27 2 9 4 104 79 9.78e4 0.00% 99.99% +nl_eq 51 7 18 10 62 58 9.64e4 0.00% 99.99% +list_any_mentions_block 24 3 7 4 111 27 9.45e4 0.00% 99.99% +list_reverse_acc.G 22 2 6 4 118 0 9.36e4 0.00% 99.99% +check_field_universes 23 2 6 4 113 112 9.27e4 0.00% 99.99% +assert_return_head_is_parent 27 1 15 4 94 19 8.66e4 0.00% 99.99% +bytes_to_limbs 57 5 29 9 52 683 8.64e4 0.00% 99.99% +try_nat_binop_addr 128 15 44 31 27 2 8.31e4 0.00% 99.99% +build_minor_at_depth 65 1 25 21 45 0 8.19e4 0.00% 99.99% +build_ih_doms 78 2 24 20 39 12 8.18e4 0.00% 99.99% +check_positivity 20 1 5 5 113 112 8.11e4 0.00% 99.99% +build_rec_type_from 93 3 29 23 32 0 7.56e4 0.00% 99.99% +level_list_eq 31 5 10 5 75 6077 7.51e4 0.00% 99.99% +level_equal 23 2 5 5 94 1417 7.42e4 0.00% 99.99% +put_definition_proj 22 1 3 3 95 0 7.21e4 0.00% 99.99% +get_inductive_proj 22 1 12 3 95 0 7.21e4 0.00% 99.99% +get_recursor 87 1 69 11 32 0 7.08e4 0.00% 99.99% +k_infer_lit 20 2 4 4 92 0 6.33e4 0.00% 99.99% +check_inductive_shape 19 1 3 4 95 32 6.27e4 0.00% 99.99% +count_foralls_body 20 2 6 3 91 5 6.25e4 0.00% 99.99% +level_normalize 25 1 9 9 75 105 6.11e4 0.00% 99.99% +check_recursor_member 72 3 24 14 32 0 5.88e4 0.00% 99.99% +check_param_agreement 14 1 2 3 113 112 5.80e4 0.00% 99.99% +build_peer_recs 29 2 10 5 64 0 5.80e4 0.00% 99.99% +convert_recursor 71 1 8 8 32 0 5.80e4 0.00% 99.99% +build_rule_rhs 45 1 15 12 45 0 5.72e4 0.00% 99.99% +collect_n_doms_whnf 40 4 16 7 49 20 5.68e4 0.00% 99.99% +ind_is_solo 69 3 52 4 32 0 5.64e4 0.00% 99.99% +nl_covers_var 35 4 11 6 54 1 5.63e4 0.00% 99.99% +klimbs_mul_single 86 3 47 7 27 0 5.62e4 0.00% 99.99% +muts_indc_count_is_one 66 4 50 3 33 31 5.61e4 0.00% 99.99% +build_apply_xs 22 2 5 4 77 18 5.59e4 0.00% 99.99% +build_all_motives_walk 51 3 24 8 40 24 5.57e4 0.00% 99.99% +build_major_params 23 2 5 4 74 0 5.55e4 0.00% 99.99% +find_peer_recursor_with_spec 67 2 50 3 32 0 5.48e4 0.00% 100.00% +u64_mul 222 1 155 46 13 0 5.39e4 0.00% 100.00% +lazy_delta_b_const_a_proj 55 6 24 8 36 0 5.25e4 0.00% 100.00% +projection_addr_ctor 41 1 23 9 45 0 5.23e4 0.00% 100.00% +nl_skip_empty 30 4 11 5 57 73 5.19e4 0.00% 100.00% +peel_motive_params_subst 31 2 9 5 55 15 5.13e4 0.00% 100.00% +compute_k_target 62 6 23 8 32 0 5.08e4 0.00% 100.00% +level_reduce 27 5 7 5 60 232 5.00e4 0.00% 100.00% +expr_inst_many_let 21 1 5 5 70 0 4.76e4 0.00% 100.00% +skip_bytes 21 3 6 3 70 48 4.76e4 0.00% 100.00% +is_rec_field 13 1 3 2 100 5 4.68e4 0.00% 100.00% +level_explicit_val 22 4 7 3 66 357 4.63e4 0.00% 100.00% +convert_univ 33 5 13 5 48 2312 4.60e4 0.00% 100.00% +build_succ_offset 57 2 17 16 30 0 4.30e4 0.00% 100.00% +const_idxs_rules 32 2 15 5 46 31 4.23e4 0.00% 100.00% +check_rec_rules_wellscoped 23 2 6 4 59 18 4.20e4 0.00% 100.00% +expr_glb_let 21 1 6 6 63 0 4.18e4 0.00% 100.00% +ctor_subst_param_for 49 3 17 10 32 91 4.04e4 0.00% 100.00% +put_constructor_proj 31 1 4 4 45 0 3.99e4 0.00% 100.00% +build_motive_type_flat 48 3 12 10 32 0 3.96e4 0.00% 100.00% +nlvars_subsume 111 6 49 25 17 3 3.92e4 0.00% 100.00% +se_mentions 39 12 11 5 37 6 3.89e4 0.00% 100.00% +build_flat_own_params 45 4 24 6 33 31 3.86e4 0.00% 100.00% +nl_add_const_go 58 5 22 12 27 0 3.82e4 0.00% 100.00% +ctors_before_pos 46 5 24 5 32 0 3.80e4 0.00% 100.00% +build_recur_addrs 11 1 2 2 95 128 3.77e4 0.00% 100.00% +build_rec_type 45 2 20 5 32 0 3.72e4 0.00% 100.00% +nl_add_const 22 4 5 3 55 53 3.70e4 0.00% 100.00% +flat_find_pos_kind 43 7 17 5 32 0 3.56e4 0.00% 100.00% +normalize_imax_dispatch 39 8 10 6 34 5 3.50e4 0.00% 100.00% +canonical_rules_at_pos 41 1 10 8 32 0 3.40e4 0.00% 100.00% +nl_le 36 6 12 6 35 7 3.36e4 0.00% 100.00% +nl_le_vars 28 3 8 5 41 4 3.22e4 0.00% 100.00% +klimbs_mul_outer 40 2 16 7 31 0 3.18e4 0.00% 100.00% +klimbs_add_carry 67 5 41 7 21 4 3.17e4 0.00% 100.00% +glist_eq_len 26 4 8 4 41 124 3.00e4 0.00% 100.00% +memory[11] 20 0 0 0 46 154 2.71e4 0.00% 100.00% +list_length.KRecRule 20 2 7 3 46 31 2.71e4 0.00% 100.00% +nlvars_dominates 50 4 19 10 23 16 2.68e4 0.00% 100.00% +flat_member_at 31 3 12 5 32 64 2.60e4 0.00% 100.00% +memory[9] 18 0 0 0 48 351 2.59e4 0.00% 100.00% +struct_scan_ctors 45 4 19 6 24 0 2.56e4 0.00% 100.00% +u64_sub_with_borrow 53 1 16 16 21 1 2.52e4 0.00% 100.00% +build_ctor_app_params 19 2 3 2 45 0 2.51e4 0.00% 100.00% +glist_ordered_insert 73 4 31 16 16 78 2.39e4 0.00% 100.00% +rec_to_parent_addr 28 1 12 5 32 9734 2.36e4 0.00% 100.00% +lbr_dec 11 2 2 1 63 75506 2.30e4 0.00% 100.00% +lazy_delta_a_const_b_proj 55 6 24 8 19 0 2.29e4 0.00% 100.00% +find_rule 25 3 10 3 34 7005 2.28e4 0.00% 100.00% +is_large_eliminator 41 7 7 4 23 9 2.22e4 0.00% 100.00% +check_rec_major_spine 26 1 9 5 32 0 2.20e4 0.00% 100.00% +klimbs_sub_borrow 69 6 42 7 15 10 2.08e4 0.00% 100.00% +u64_add 53 1 16 16 18 22 2.05e4 0.00% 100.00% +check_parent_inductive_shape 24 2 2 2 32 0 2.04e4 0.00% 100.00% +nlvars_add 102 5 44 23 11 12 1.98e4 0.00% 100.00% +memory[5] 14 0 0 0 46 4726 1.94e4 0.00% 100.00% +expr_lift_let 21 1 5 5 33 0 1.87e4 0.00% 100.00% +list_length.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode 21 2 8 3 33 31 1.87e4 0.00% 100.00% +se_scan_fields 25 3 8 4 29 0 1.87e4 0.00% 100.00% +relaxed_u64_succ 25 9 2 1 28 473 1.78e4 0.00% 100.00% +list_reverse.G 13 1 3 3 44 230 1.72e4 0.00% 100.00% +level_leq 30 3 9 6 23 94 1.64e4 0.00% 100.00% +is_defn_or_thm 24 3 3 1 27 404 1.64e4 0.00% 100.00% +se_peel_tol 22 3 7 3 28 0 1.58e4 0.00% 100.00% +compute_iprj_addr 30 1 15 8 22 1590 1.55e4 0.00% 100.00% +struct_block_member_addrs 68 2 52 4 12 0 1.51e4 0.00% 100.00% +dec_rewrite_lt_to_le 49 2 14 13 15 0 1.49e4 0.00% 100.00% +build_succ_chain 53 2 20 5 14 170 1.46e4 0.00% 100.00% +memory[6] 15 0 0 0 33 417 1.37e4 0.00% 100.00% +check_large_walk_fields 44 5 14 8 15 0 1.34e4 0.00% 100.00% +klimbs_normalize 48 4 25 7 14 279 1.33e4 0.00% 100.00% +memory[8] 17 0 0 0 29 40990 1.30e4 0.00% 100.00% +build_all_minors 14 1 2 2 32 0 1.24e4 0.00% 100.00% +collect_index_doms 39 4 15 7 14 58 1.09e4 0.00% 100.00% +build_all_motives 12 1 2 2 32 0 1.08e4 0.00% 100.00% +se_addr_in 24 3 7 4 18 0 9.66e3 0.00% 100.00% +se_parent_addr 34 5 13 5 14 124 9.57e3 0.00% 100.00% +assert_lvls_are_params 25 2 8 4 17 115 9.30e3 0.00% 100.00% +subst_param_for 46 3 17 9 11 27 9.15e3 0.00% 100.00% +list_lift_indices 26 2 7 5 16 24 8.90e3 0.00% 100.00% +u64_byte_count 150 128 8 1 5 292 8.89e3 0.00% 100.00% +check_large_prop_ctor 27 3 8 4 15 0 8.45e3 0.00% 100.00% +apply_n_projs 24 2 5 4 16 0 8.26e3 0.00% 100.00% +nlvars_eq 36 6 12 6 12 43 8.18e3 0.00% 100.00% +assert_occ_param_bvars 27 2 9 4 14 1 7.70e3 0.00% 100.00% +peel_leading_foralls_acc 24 2 8 4 15 0 7.57e3 0.00% 100.00% +struct_is_rec 33 2 16 5 12 82 7.53e3 0.00% 100.00% +list_snoc.U8_8 36 2 13 4 11 4 7.25e3 0.00% 100.00% +klimbs_div_mod 46 2 14 12 9 0 6.89e3 0.00% 100.00% +try_eta_expand 45 3 14 10 9 3 6.74e3 0.00% 100.00% +list_lift_each 26 2 7 5 13 43 6.72e3 0.00% 100.00% +count_foralls_at_least 23 3 7 3 14 0 6.63e3 0.00% 100.00% +apply_indices_in_conclusion 22 2 5 4 14 24 6.37e3 0.00% 100.00% +klimbs_add 11 1 2 2 21 14 5.83e3 0.00% 100.00% +klimbs_mul 14 1 3 3 17 2 5.48e3 0.00% 100.00% +klimbs_pow 43 3 12 11 8 0 5.45e3 0.00% 100.00% +klimbs_sub 18 2 4 3 14 36 5.30e3 0.00% 100.00% +args_contain_bvar 28 4 10 4 9 1 4.32e3 0.00% 100.00% +klimbs_succ 41 3 23 5 7 96 4.28e3 0.00% 100.00% +klimbs_le 27 2 13 3 9 10 4.18e3 0.00% 100.00% +klimbs_is_zero 26 2 13 3 9 427 4.03e3 0.00% 100.00% +build_rec_lvls_list 21 2 5 4 10 28 3.85e3 0.00% 100.00% +klimbs_shl_limbs 18 2 4 3 11 3 3.82e3 0.00% 100.00% +check_valid_ind_app 35 1 17 8 7 0 3.69e3 0.00% 100.00% +klimbs_eq 44 5 23 5 6 109 3.63e3 0.00% 100.00% +build_param_lvls_range 22 2 5 4 9 59 3.46e3 0.00% 100.00% +peel_leading_foralls 15 1 5 4 11 1 3.25e3 0.00% 100.00% +list_lookup_or_default.Ptr.U8_32 20 2 5 3 9 21 3.18e3 0.00% 100.00% +check_nested_ctors_positivity 51 2 20 9 5 0 3.14e3 0.00% 100.00% +memory[2] 11 0 0 0 13 99 3.11e3 0.00% 100.00% +glimbs_to_klimbs 36 2 13 8 6 17 3.01e3 0.00% 100.00% +wrap_lams 22 2 6 4 8 0 2.93e3 0.00% 100.00% +is_int_dec_prim_addr 33 4 10 7 6 263 2.78e3 0.00% 100.00% +all_bvars_in_args 24 3 7 4 7 0 2.61e3 0.00% 100.00% +nl_covers_const 61 6 24 12 4 2 2.58e3 0.00% 100.00% +try_native_dispatch 98 8 37 23 3 0 2.44e3 0.00% 100.00% +mk_nat_lit 10 1 2 2 9 105 1.75e3 0.00% 100.00% +try_reduce_subtype_val 63 4 26 14 3 0 1.61e3 0.00% 100.00% +try_str_dispatch 128 18 47 28 2 0 1.35e3 0.00% 100.00% +try_quot_iota 30 3 8 6 4 0 1.34e3 0.00% 100.00% +intern_int_lit 29 3 8 6 4 70 1.30e3 0.00% 100.00% +klimbs_dec 14 1 4 4 6 127 1.30e3 0.00% 100.00% +unfold_b_and_loop 23 2 5 4 4 0 1.06e3 0.00% 100.00% +klimbs_gcd 20 2 4 4 4 2 9.44e2 0.00% 100.00% +u64_eq 33 9 2 1 3 0 8.93e2 0.00% 100.00% +check_quot 29 5 6 5 3 0 7.97e2 0.00% 100.00% +get_quotient 27 1 15 5 3 0 7.50e2 0.00% 100.00% +convert_axiom 26 1 3 3 3 0 7.26e2 0.00% 100.00% +get_axiom 26 1 14 5 3 0 7.26e2 0.00% 100.00% +convert_quotient 26 1 3 3 3 0 7.26e2 0.00% 100.00% +try_quot_lift 59 3 22 14 2 0 6.62e2 0.00% 100.00% +run_claim 128 5 71 8 1 0 6.56e2 0.00% 100.00% +idx_to_u64 22 1 10 6 3 206 6.31e2 0.00% 100.00% +klimbs_land 52 3 31 6 2 0 5.92e2 0.00% 100.00% +unpack_def_kind_safety 17 9 1 1 3 1520 5.12e2 0.00% 100.00% +bitvec_prep_spine 44 3 15 10 2 0 5.12e2 0.00% 100.00% +bv_to_nat_via 41 4 13 9 2 0 4.82e2 0.00% 100.00% +defn_is_unsafe_ci 15 5 2 1 3 1520 4.65e2 0.00% 100.00% +quot_extract_arg 39 4 13 8 2 0 4.62e2 0.00% 100.00% +bitvec_of_nat_args_direct 38 4 13 8 2 0 4.52e2 0.00% 100.00% +quot_kind_tag 12 4 1 1 3 0 3.93e2 0.00% 100.00% +try_str_to_byte_array 64 5 26 14 1 0 3.36e2 0.00% 100.00% +mk_bool 20 2 5 4 2 3 2.72e2 0.00% 100.00% +put_expr_list 42 2 24 5 1 0 2.26e2 0.00% 100.00% +canon_cprj_addr 41 1 23 9 1 116 2.21e2 0.00% 100.00% +verify_claim 40 1 1 2 1 0 2.16e2 0.00% 100.00% +u64_and 40 1 9 9 1 0 2.16e2 0.00% 100.00% +klimbs_mod 12 1 3 2 2 0 1.92e2 0.00% 100.00% +list_length_u64.Ptr.Univ 35 2 20 4 1 2 1.91e2 0.00% 100.00% +put_univ_list 33 2 15 5 1 0 1.81e2 0.00% 100.00% +unfold_both_and_loop 31 3 8 6 1 0 1.71e2 0.00% 100.00% +mk_nat_binop_stuck 24 1 7 7 1 0 1.36e2 0.00% 100.00% +check_eq_type 24 1 15 4 1 0 1.36e2 0.00% 100.00% +put_refs 22 1 11 4 1 139 1.26e2 0.00% 100.00% +put_address_list 22 2 6 4 1 0 1.26e2 0.00% 100.00% +put_univs 22 1 11 4 1 139 1.26e2 0.00% 100.00% +put_sharing 22 1 11 4 1 139 1.26e2 0.00% 100.00% +delta_rank 22 2 2 1 1 1 1.26e2 0.00% 100.00% +klimbs_shr 18 1 5 5 1 0 1.06e2 0.00% 100.00% +get_opt_addr 18 2 5 3 1 0 1.06e2 0.00% 100.00% +literal_eq 18 4 2 2 1 0 1.06e2 0.00% 100.00% +klimbs_div 12 1 3 2 1 0 7.60e1 0.00% 100.00% +assert_wire_bool 10 1 2 2 1 118 6.60e1 0.00% 100.00% +nat_beq_addr 9 1 2 2 1 590 6.10e1 0.00% 100.00% +bool_type_addr_dec 9 1 2 2 1 55 6.10e1 0.00% 100.00% +eq_refl_addr_dec 9 1 2 2 1 55 6.10e1 0.00% 100.00% +int_dec_eq_addr_dec 9 1 2 2 1 577 6.10e1 0.00% 100.00% +int_dec_le_addr_dec 9 1 2 2 1 579 6.10e1 0.00% 100.00% +int_dec_lt_addr_dec 9 1 2 2 1 575 6.10e1 0.00% 100.00% +int_of_nat_addr_dec 9 1 2 2 1 8 6.10e1 0.00% 100.00% +int_neg_succ_addr_dec 9 1 2 2 1 8 6.10e1 0.00% 100.00% +bool_true_addr 9 1 2 2 1 35 6.10e1 0.00% 100.00% +str_addr 9 1 2 2 1 37 6.10e1 0.00% 100.00% +nat_ble_addr 9 1 2 2 1 586 6.10e1 0.00% 100.00% +nat_mul_addr 9 1 2 2 1 605 6.10e1 0.00% 100.00% +nat_pow_addr 9 1 2 2 1 595 6.10e1 0.00% 100.00% +nat_dec_le_addr_dec 9 1 2 2 1 706 6.10e1 0.00% 100.00% +nat_gcd_addr 9 1 2 2 1 598 6.10e1 0.00% 100.00% +nat_dec_eq_addr_dec 9 1 2 2 1 692 6.10e1 0.00% 100.00% +nat_succ_addr_iota 9 1 2 2 1 2576 6.10e1 0.00% 100.00% +nat_pred_addr 9 1 2 2 1 1565 6.10e1 0.00% 100.00% +string_append_addr 9 1 2 2 1 580 6.10e1 0.00% 100.00% +nat_dec_lt_addr_dec 9 1 2 2 1 691 6.10e1 0.00% 100.00% +decidable_is_true_addr_dec 9 1 2 2 1 34 6.10e1 0.00% 100.00% +decidable_is_false_addr_dec 9 1 2 2 1 20 6.10e1 0.00% 100.00% +bool_false_addr 9 1 2 2 1 21 6.10e1 0.00% 100.00% +system_platform_num_bits_addr 9 1 2 2 1 580 6.10e1 0.00% 100.00% +punit_size_of_1_addr 9 1 2 2 1 580 6.10e1 0.00% 100.00% +nat_zero_addr 9 1 2 2 1 22 6.10e1 0.00% 100.00% +system_platform_get_num_bits_addr 9 1 2 2 1 1 6.10e1 0.00% 100.00% +size_of_size_of_addr 9 1 2 2 1 576 6.10e1 0.00% 100.00% +string_back_addr 9 1 2 2 1 581 6.10e1 0.00% 100.00% +reduce_bool_addr 9 1 2 2 1 577 6.10e1 0.00% 100.00% +quot_type_addr 9 1 2 2 1 0 6.10e1 0.00% 100.00% +string_legacy_back_addr 9 1 2 2 1 581 6.10e1 0.00% 100.00% +nat_add_addr 9 1 2 2 1 6090 6.10e1 0.00% 100.00% +nat_mod_addr 9 1 2 2 1 726 6.10e1 0.00% 100.00% +nat_le_of_ble_eq_true_addr_dec 9 1 2 2 1 6 6.10e1 0.00% 100.00% +string_of_list_addr 9 1 2 2 1 582 6.10e1 0.00% 100.00% +nat_div_addr 9 1 2 2 1 727 6.10e1 0.00% 100.00% +nat_land_addr 9 1 2 2 1 590 6.10e1 0.00% 100.00% +nat_lor_addr 9 1 2 2 1 588 6.10e1 0.00% 100.00% +nat_sub_addr 9 1 2 2 1 611 6.10e1 0.00% 100.00% +reduce_nat_addr 9 1 2 2 1 577 6.10e1 0.00% 100.00% +bit_vec_to_nat_addr 9 1 2 2 1 790 6.10e1 0.00% 100.00% +bit_vec_of_nat_addr 9 1 2 2 1 1 6.10e1 0.00% 100.00% +bit_vec_addr 9 1 2 2 1 93 6.10e1 0.00% 100.00% +quot_lift_addr_iota 9 1 2 2 1 4 6.10e1 0.00% 100.00% +nat_xor_addr 9 1 2 2 1 588 6.10e1 0.00% 100.00% +string_utf8_byte_size_addr 9 1 2 2 1 583 6.10e1 0.00% 100.00% +fin_addr 9 1 2 2 1 2471 6.10e1 0.00% 100.00% +decidable_rec_addr 9 1 2 2 1 2 6.10e1 0.00% 100.00% +bit_vec_ult_addr 9 1 2 2 1 787 6.10e1 0.00% 100.00% +decidable_decide_addr 9 1 2 2 1 787 6.10e1 0.00% 100.00% +nat_addr_io 9 1 2 2 1 56 6.10e1 0.00% 100.00% +quot_ctor_addr 9 1 2 2 1 2 6.10e1 0.00% 100.00% +string_dec_eq_addr 9 1 2 2 1 579 6.10e1 0.00% 100.00% +quot_ind_addr 9 1 2 2 1 1 6.10e1 0.00% 100.00% +string_to_byte_array_addr 9 1 2 2 1 581 6.10e1 0.00% 100.00% +nat_eq_of_beq_eq_true_addr_dec 9 1 2 2 1 27 6.10e1 0.00% 100.00% +lt_lt_addr 9 1 2 2 1 191 6.10e1 0.00% 100.00% +nat_ne_of_beq_eq_false_addr_dec 9 1 2 2 1 20 6.10e1 0.00% 100.00% +nat_shift_left_addr 9 1 2 2 1 588 6.10e1 0.00% 100.00% +subtype_val_addr 9 1 2 2 1 580 6.10e1 0.00% 100.00% +nat_shift_right_addr 9 1 2 2 1 588 6.10e1 0.00% 100.00% +try_reduce_bit_vec_ult 63 4 24 15 0 0 0 0.00% 100.00% +put_inductive 77 1 34 10 0 0 0 0.00% 100.00% +utf8_encode_prepend 212 4 100 51 0 0 0 0.00% 100.00% +list_nil_addr 9 1 2 2 0 0 0 0.00% 100.00% +nat_not_le_of_not_ble_eq_true_addr_dec 9 1 2 2 0 0 0 0.00% 100.00% +defn_member_recur_addrs 30 2 4 3 0 0 0 0.00% 100.00% +put_quot_kind 16 4 2 2 0 0 0 0.00% 100.00% +get_ci_dprj 130 1 109 6 0 0 0 0.00% 100.00% +list_cons_addr 9 1 2 2 0 0 0 0.00% 100.00% +put_mut_const_list 66 2 50 4 0 0 0 0.00% 100.00% +put_definition 68 1 42 8 0 0 0 0.00% 100.00% +get_ci_rprj 121 1 108 6 0 0 0 0.00% 100.00% +put_univ 53 5 22 6 0 0 0 0.00% 100.00% +u64_or 40 1 9 9 0 0 0 0.00% 100.00% +u64_xor_kbits 40 1 9 9 0 0 0 0.00% 100.00% +extract_aux_occ_us 46 4 14 6 0 0 0 0.00% 100.00% +extract_aux_spec_params 27 1 10 6 0 0 0 0.00% 100.00% +spec_params_lower 28 2 8 6 0 0 0 0.00% 100.00% +univ_succ_base 40 2 19 3 0 0 0 0.00% 100.00% +put_recursor_rule 40 1 21 4 0 0 0 0.00% 100.00% +aux_already_in 33 5 11 5 0 0 0 0.00% 100.00% +kexpr_struct_eq 59 28 13 6 0 0 0 0.00% 100.00% +level_list_struct_eq 30 5 9 5 0 0 0 0.00% 100.00% +spec_params_ptr_eq 30 5 9 5 0 0 0 0.00% 100.00% +extract_aux_spec_params_from_rec 26 2 3 2 0 0 0 0.00% 100.00% +first_recr_parent_block 107 5 77 8 0 0 0 0.00% 100.00% +klimbs_lor 52 3 31 6 0 0 0 0.00% 100.00% +detect_aux_from_recrs_ex 66 2 50 3 0 0 0 0.00% 100.00% +aux_from_recrs_walk_ex 138 9 90 14 0 0 0 0.00% 100.00% +flat_find_pos 29 3 11 4 0 0 0 0.00% 100.00% +klimbs_xor_op 52 3 31 6 0 0 0 0.00% 100.00% +klimbs_shl 18 1 5 5 0 0 0 0.00% 100.00% +char_type_addr 9 1 2 2 0 0 0 0.00% 100.00% +put_recursor_rule_list 30 2 14 4 0 0 0 0.00% 100.00% +try_str_back 70 4 27 17 0 0 0 0.00% 100.00% +np_whnf_inner_bv 16 1 5 4 0 0 0 0.00% 100.00% +apply_spec_params_lifted 26 2 7 5 0 0 0 0.00% 100.00% +try_str_dec_eq 71 7 29 14 0 0 0 0.00% 100.00% +str_dec_eq_build 123 2 43 35 0 0 0 0.00% 100.00% +put_recursor 98 1 36 12 0 0 0 0.00% 100.00% +canon_ord_cmp_g 37 3 14 7 0 0 0 0.00% 100.00% +canon_ord_then 12 2 2 1 0 0 0 0.00% 100.00% +canon_sord_lt_strong 6 1 1 1 0 0 0 0.00% 100.00% +canon_sord_eq_strong 6 1 1 1 0 0 0 0.00% 100.00% +canon_sord_gt_strong 6 1 1 1 0 0 0 0.00% 100.00% +canon_sord_then 14 2 2 1 0 0 0 0.00% 100.00% +canon_sord_of_g 7 1 1 1 0 0 0 0.00% 100.00% +canon_addr_cmp 105 1 80 18 0 0 0 0.00% 100.00% +canon_addr_chunk 17 1 2 2 0 0 0 0.00% 100.00% +canon_ctx_class_idx 25 3 8 4 0 0 0 0.00% 100.00% +canon_ctx_cmp_addr 32 5 8 6 0 0 0 0.00% 100.00% +canon_cmp_kuniv 44 16 10 6 0 0 0 0.00% 100.00% +canon_cmp_kuniv_list 32 4 10 6 0 0 0 0.00% 100.00% +canon_cmp_kliteral 18 4 2 2 0 0 0 0.00% 100.00% +canon_cmp_klimbs 29 2 7 7 0 0 0 0.00% 100.00% +canon_cmp_klimbs_tail 44 2 24 6 0 0 0 0.00% 100.00% +canon_cmp_u64_lex 53 1 16 16 0 0 0 0.00% 100.00% +find_peer_rec_spec_walk 131 10 85 12 0 0 0 0.00% 100.00% +canon_cmp_bytes 32 4 10 6 0 0 0 0.00% 100.00% +canon_cmp_kexpr_ctx 29 2 12 4 0 0 0 0.00% 100.00% +canon_cmp_kexpr_node_ctx 79 40 12 7 0 0 0 0.00% 100.00% +canon_cmp_krec_rule_ctx 26 1 8 5 0 0 0 0.00% 100.00% +canon_cmp_krec_rule_list_ctx 40 4 17 6 0 0 0 0.00% 100.00% +canon_kind_ord 27 8 1 1 0 0 0 0.00% 100.00% +canon_cmp_member_ctx 48 2 7 5 0 0 0 0.00% 100.00% +canon_cmp_member_same_kind_ctx 118 8 37 22 0 0 0 0.00% 100.00% +canon_cmp_ctor_range_ctx 63 2 34 8 0 0 0 0.00% 100.00% +canon_cmp_ctor_pair_ctx 83 3 23 14 0 0 0 0.00% 100.00% +put_axiom 44 1 22 5 0 0 0 0.00% 100.00% +canon_member_ci 26 1 15 4 0 0 0 0.00% 100.00% +canon_member_num_ctors 26 2 14 2 0 0 0 0.00% 100.00% +canon_build_ctx_classes 29 2 8 5 0 0 0 0.00% 100.00% +canon_build_ctx_members 64 3 24 14 0 0 0 0.00% 100.00% +canon_ctor_ctx_entries 24 2 5 4 0 0 0 0.00% 100.00% +canon_sort_loop 31 3 8 6 0 0 0 0.00% 100.00% +canon_refine_classes 26 2 7 5 0 0 0 0.00% 100.00% +spec_params_dom_prefix_match 33 4 10 6 0 0 0 0.00% 100.00% +canon_refine_one 24 3 6 4 0 0 0 0.00% 100.00% +canon_ins_sort 23 2 6 4 0 0 0 0.00% 100.00% +canon_insert_sorted 58 3 33 7 0 0 0 0.00% 100.00% +canon_group_consec 26 2 7 5 0 0 0 0.00% 100.00% +canon_group_walk 65 3 35 9 0 0 0 0.00% 100.00% +canon_classes_eq 31 5 10 5 0 0 0 0.00% 100.00% +canon_flatten 21 2 6 4 0 0 0 0.00% 100.00% +canon_all_singleton 22 3 6 4 0 0 0 0.00% 100.00% +bitvec_prep_spine_ult 46 4 16 10 0 0 0 0.00% 100.00% +punit_addr 9 1 2 2 0 0 0 0.00% 100.00% +unit_addr 9 1 2 2 0 0 0 0.00% 100.00% +canon_g_list_eq 27 5 8 4 0 0 0 0.00% 100.00% +utf8_last_codepoint 10 1 2 2 0 0 0 0.00% 100.00% +try_quot_ind 59 3 22 14 0 0 0 0.00% 100.00% +pack_def_kind_safety 18 9 1 1 0 0 0 0.00% 100.00% +mk_nat_literal_64 13 1 4 4 0 0 0 0.00% 100.00% +mk_nat_one 13 1 4 4 0 0 0 0.00% 100.00% +utf8_last_go 23 2 7 4 0 0 0 0.00% 100.00% +utf8_cont 13 1 3 3 0 0 0 0.00% 100.00% +put_lam_telescope 74 2 39 5 0 0 0 0.00% 100.00% +leaf_hash 17 1 5 5 0 0 0 0.00% 100.00% +node_hash 19 1 6 6 0 0 0 0.00% 100.00% +parse_atree_body 31 3 11 6 0 0 0 0.00% 100.00% +load_assumption_tree 96 1 84 6 0 0 0 0.00% 100.00% +addr_set_build 37 2 16 4 0 0 0 0.00% 100.00% +addr_set_member 16 1 2 2 0 0 0 0.00% 100.00% +env_walk 102 10 58 8 0 0 0 0.00% 100.00% +env_walk_refs 40 4 6 5 0 0 0 0.00% 100.00% +env_walk_leaves 31 2 4 4 0 0 0 0.00% 100.00% +run_check_env 38 3 16 6 0 0 0 0.00% 100.00% +put_all_telescope 74 2 39 5 0 0 0 0.00% 100.00% +get_opt_u64_masked 23 2 11 2 0 0 0 0.00% 100.00% +get_opt_addr_masked 16 2 4 2 0 0 0 0.00% 100.00% +get_opt_bool_masked 16 2 4 2 0 0 0 0.00% 100.00% +get_opt_def_kind_masked 18 4 4 2 0 0 0 0.00% 100.00% +get_opt_quot_kind_masked 19 5 4 2 0 0 0 0.00% 100.00% +get_reveal_rule_list_inner 59 2 32 6 0 0 0 0.00% 100.00% +get_opt_rule_list_masked 27 2 13 3 0 0 0 0.00% 100.00% +get_reveal_ctor_info 80 1 64 9 0 0 0 0.00% 100.00% +get_ctor_entry 61 1 51 3 0 0 0 0.00% 100.00% +get_ctor_entry_list_inner 90 2 63 6 0 0 0 0.00% 100.00% +get_opt_ctor_entry_list_masked 27 2 13 3 0 0 0 0.00% 100.00% +get_reveal_mut_const_info 126 3 90 14 0 0 0 0.00% 100.00% +get_mut_entry 75 1 65 3 0 0 0 0.00% 100.00% +get_mut_entry_list_inner 104 2 77 6 0 0 0 0.00% 100.00% +get_reveal_info 134 11 90 14 0 0 0 0.00% 100.00% +expr_addr 34 1 22 5 0 0 0 0.00% 100.00% +def_safety_tag 11 3 1 1 0 0 0 0.00% 100.00% +check_opt_def_kind 18 2 3 3 0 0 0 0.00% 100.00% +check_opt_def_safety 18 2 3 3 0 0 0 0.00% 100.00% +check_opt_quot_kind 18 2 3 3 0 0 0 0.00% 100.00% +check_opt_bool 12 2 1 1 0 0 0 0.00% 100.00% +check_opt_u64 26 2 1 1 0 0 0 0.00% 100.00% +check_opt_addr 80 2 65 3 0 0 0 0.00% 100.00% +check_opt_expr_addr 83 2 66 4 0 0 0 0.00% 100.00% +check_recr_rules 67 2 39 6 0 0 0 0.00% 100.00% +check_opt_recr_rules 14 2 1 2 0 0 0 0.00% 100.00% +check_ctor_entry 97 1 35 8 0 0 0 0.00% 100.00% +check_ctor_entries 67 2 51 4 0 0 0 0.00% 100.00% +check_opt_ctor_entries 14 2 1 2 0 0 0 0.00% 100.00% +check_mut_const 127 3 1 10 0 0 0 0.00% 100.00% +check_muts_components 128 2 110 5 0 0 0 0.00% 100.00% +run_reveal 139 9 49 11 0 0 0 0.00% 100.00% +run_contains 14 1 3 3 0 0 0 0.00% 100.00% +char_of_nat_addr 9 1 2 2 0 0 0 0.00% 100.00% +unfold_a_and_loop 23 2 5 4 0 0 0 0.00% 100.00% +nlvars_max_offset 47 3 19 10 0 0 0 0.00% 100.00% +str_lit_to_ctor 49 1 21 21 0 0 0 0.00% 100.00% +list_length_u64.U8_8 42 2 27 4 0 0 0 0.00% 100.00% +list_concat.Tup.Ptr.U8_32.G 23 2 7 4 0 0 0 0.00% 100.00% +put_quotient 44 1 22 5 0 0 0 0.00% 100.00% +rbtree_map_lookup_or_default.G 64 4 28 10 0 0 0 0.00% 100.00% +has_bvar_in_range 75 11 29 14 0 0 0 0.00% 100.00% +try_reduce_size_of_unit 71 5 29 16 0 0 0 0.00% 100.00% +check_native_bool 32 3 10 7 0 0 0 0.00% 100.00% +list_length_u64.Constructor 68 2 53 4 0 0 0 0.00% 100.00% +check_native_nat 21 3 7 3 0 0 0 0.00% 100.00% +list_length.U8_8 25 2 12 3 0 0 0 0.00% 100.00% +list_lookup_u64.MutConst 127 2 102 5 0 0 0 0.00% 100.00% +list_length_u64.MutConst 79 2 64 4 0 0 0 0.00% 100.00% +list_length_u64.RecursorRule 43 2 28 4 0 0 0 0.00% 100.00% +list_lookup_u64.Constructor 105 2 80 5 0 0 0 0.00% 100.00% +has_bvar_in_range_binder 19 2 3 3 0 0 0 0.00% 100.00% +list_snoc.Tup.Ptr.U8_32.G.Ptr.ListNode.Ptr.KExprNode.Ptr.ListNode.Ptr.KLevelNode 28 2 9 4 0 0 0 0.00% 100.00% +has_bvar_in_range_let 24 3 4 4 0 0 0 0.00% 100.00% +put_constructor 73 1 25 8 0 0 0 0.00% 100.00% +put_expr 110 12 59 8 0 0 0 0.00% 100.00% +rbtree_map_insert.G 22 1 7 2 0 0 0 0.00% 100.00% +put_u64_le 26 2 4 3 0 0 0 0.00% 100.00% +put_constructor_list 55 2 39 4 0 0 0 0.00% 100.00% +put_tag2 33 3 6 5 0 0 0 0.00% 100.00% +rbtree_map_ins.G 77 4 39 11 0 0 0 0.00% 100.00% +rbtree_map_balance.G 34 2 7 3 0 0 0 0.00% 100.00% +rbtree_map_balance_fix.G 122 57 31 8 0 0 0 0.00% 100.00% +build_char_list 40 2 12 9 0 0 0 0.00% 100.00% +str_lit_delta_step 62 5 31 10 0 0 0 0.00% 100.00% +byte_array_empty_addr 9 1 2 2 0 0 0 0.00% 100.00% +put_mut_const 62 3 3 3 0 0 0 0.00% 100.00% +put_u64_list 29 2 13 4 0 0 0 0.00% 100.00% +app_telescope_count 67 2 35 4 0 0 0 0.00% 100.00% +klimbs_from_g 25 1 11 7 0 0 0 0.00% 100.00% +lam_telescope_count 67 2 35 4 0 0 0 0.00% 100.00% +walk_char_list_bytes 64 8 22 14 0 0 0 0.00% 100.00% +all_telescope_count 67 2 35 4 0 0 0 0.00% 100.00% +univ_succ_count 49 2 26 4 0 0 0 0.00% 100.00% +memory[19] 28 0 0 0 0 0 0 0.00% 100.00% +char_lit_codepoint 23 2 7 4 0 0 0 0.00% 100.00% +put_app_telescope 74 2 39 5 0 0 0 0.00% 100.00% +nlvars_any_offset_geq 48 3 19 10 0 0 0 0.00% 100.00% +char_lit_codepoint_syn 43 6 18 7 0 0 0 0.00% 100.00% +memory[50] 59 0 0 0 0 0 0 0.00% 100.00% +memory[64] 73 0 0 0 0 0 0 0.00% 100.00% +klimbs_scalar_value 117 7 63 21 0 0 0 0.00% 100.00% diff --git a/cold-groups/kstats2-grouped-Array.extract_append.txt b/cold-groups/kstats2-grouped-Array.extract_append.txt new file mode 100644 index 00000000..6edfd51f --- /dev/null +++ b/cold-groups/kstats2-grouped-Array.extract_append.txt @@ -0,0 +1,194 @@ +=== Circuit Statistics === +Circuits: 185 +Total width: 15763 +Total FFT cost: 147111354325 (1.47e11) +Total cache hits: 72393508 +Total saved cost: 63.21% +-------------------------------------------------------------------------------------------- +Name Width Sel Aux Lkp Height Hits FFT cost % %++ +-------------------------------------------------------------------------------------------- +expr_inst_many_walk 34 9 8 5 5471753 0 2.10e10 14.29% 14.29% +expr_inst_many 21 2 4 4 6975351 1584350 1.69e10 11.49% 25.78% +blake3_compress_inner_j 696 1 369 193 151585 0 9.08e9 6.17% 31.95% +memory[3] 12 0 0 0 6181533 17946311 8.59e9 5.84% 37.79% +list_snoc.G 22 2 6 4 2593801 881702 6.17e9 4.20% 41.99% +peel_beta 32 3 12 5 1637758 10634 5.47e9 3.72% 45.70% +list_drop.Ptr.Expr 20 2 6 3 2151895 1151414 4.60e9 3.13% 48.83% +blake3_compress_chunks 29 3 7 4 1288914 0 3.84e9 2.61% 51.44% +whnf_with_spine 34 6 11 5 1108779 14944 3.82e9 2.60% 54.04% +expr_inst_many_bvar 24 2 5 5 1528825 0 3.82e9 2.60% 56.64% +list_concat.Ptr.KExprNode 22 2 6 4 1505977 731709 3.45e9 2.35% 58.99% +expr_lbr 35 9 9 6 870475 9468745 3.04e9 2.06% 61.05% +collect_spine 23 2 8 4 1199012 836589 2.83e9 1.92% 62.98% +k_shape_12 74 40 7 4 382500 102913 2.64e9 1.79% 64.77% +k_infer_app_spine_loop 59 8 21 11 470161 506 2.63e9 1.79% 66.56% +memory[4] 13 0 0 0 1735873 17182092 2.40e9 1.63% 68.19% +list_lookup.Ptr.KLevelNode 16 1 5 3 1364948 403575 2.27e9 1.55% 69.74% +list_length.Ptr.KExprNode 18 2 5 3 1166659 2680089 2.16e9 1.47% 71.20% +get_expr 50 12 23 5 391929 17 1.83e9 1.25% 72.45% +k_shape_32 114 31 15 8 178303 25645 1.78e9 1.21% 73.66% +whnf_const_head 77 16 32 10 246268 0 1.71e9 1.16% 74.82% +blake3_compress 1080 1 929 40 21655 14 1.68e9 1.15% 75.97% +convert_expr 60 12 25 7 292994 154982 1.61e9 1.09% 77.06% +k_shape_08 75 40 5 4 234788 79166 1.58e9 1.07% 78.13% +get_tag4 37 2 22 4 393551 0 1.37e9 0.93% 79.06% +apply_spine_expr 22 2 6 4 618392 83404 1.33e9 0.90% 79.97% +k_shape_06 94 33 3 4 162630 213149 1.33e9 0.90% 80.87% +k_shape_30 64 22 14 6 208719 70386 1.19e9 0.81% 81.68% +k_shape_07 68 38 4 4 188627 19905 1.13e9 0.77% 82.45% +get_u64_le 28 2 14 3 422899 22 1.12e9 0.76% 83.21% +k_shape_14 89 16 7 7 141782 117961 1.08e9 0.74% 83.95% +whnf_apply_beta 34 3 10 7 339939 0 1.07e9 0.73% 84.68% +get_app_telescope 43 2 15 6 264610 0 1.03e9 0.70% 85.38% +expr_inst1_walk 34 9 8 5 326314 0 1.03e9 0.70% 86.08% +expr_glb_walk 34 10 8 5 295964 0 9.25e8 0.63% 86.71% +k_shape_24 74 40 12 7 131999 6200 8.36e8 0.57% 87.27% +g_list_has 21 3 6 3 413484 3025 8.25e8 0.56% 87.83% +validate_expr_well_scoped 52 9 20 8 176535 152144 8.06e8 0.55% 88.38% +expr_inst1 21 2 4 4 400830 220687 7.98e8 0.54% 88.93% +expr_lift 23 3 5 4 359613 1596071 7.76e8 0.53% 89.45% +try_reduce_projection_definition 59 3 24 13 151416 11396 7.74e8 0.53% 89.98% +const_idxs_expr 52 7 26 7 160015 209196 7.25e8 0.49% 90.47% +k_infer_core 53 9 22 8 156068 76251 7.19e8 0.49% 90.96% +expr_lift_walk 34 9 8 5 232640 0 7.13e8 0.48% 91.45% +k_shape_45 89 31 23 9 94238 50867 6.96e8 0.47% 91.92% +try_prim_dispatch 30 6 8 4 254764 16347 6.95e8 0.47% 92.39% +k_shape_39 91 36 19 14 87017 500015 6.53e8 0.44% 92.84% +expr_lower_walk 53 10 18 9 141436 0 6.46e8 0.44% 93.27% +k_shape_13 84 38 7 5 91674 6084 6.38e8 0.43% 93.71% +expr_glb 21 2 5 4 307017 351230 5.99e8 0.41% 94.12% +try_iota 108 5 39 25 66939 2106 5.82e8 0.40% 94.51% +safe_refs_only 43 9 19 5 140151 138582 5.20e8 0.35% 94.86% +k_shape_16 118 39 9 8 55072 4545 5.14e8 0.35% 95.21% +k_shape_52 113 40 29 16 56780 711 5.09e8 0.35% 95.56% +k_shape_17 70 39 9 6 79800 95301 4.58e8 0.31% 95.87% +k_shape_51 79 9 27 17 66603 305 4.24e8 0.29% 96.16% +bytes_to_block 265 1 193 65 20371 601 3.87e8 0.26% 96.42% +memory[18] 27 0 0 0 160015 742479 3.79e8 0.26% 96.68% +k_shape_37 91 30 18 12 52620 2567 3.77e8 0.26% 96.94% +k_shape_19 64 36 10 5 69210 79815 3.59e8 0.24% 97.18% +expr_lower 23 3 5 4 159506 145656 3.23e8 0.22% 97.40% +blake3_compress_block 211 2 169 15 19287 0 2.90e8 0.20% 97.60% +k_shape_82 213 5 100 51 15781 90 2.35e8 0.16% 97.76% +k_shape_36 83 33 17 10 36381 4173 2.30e8 0.16% 97.91% +k_shape_43 65 14 22 7 44804 108 2.27e8 0.15% 98.07% +k_shape_47 93 38 24 9 31395 37700 2.19e8 0.15% 98.22% +k_shape_31 131 38 14 13 21982 48240 2.08e8 0.14% 98.36% +k_shape_11 102 39 7 6 26824 1512 2.02e8 0.14% 98.50% +k_shape_35 80 12 16 16 28849 2634 1.72e8 0.12% 98.61% +k_shape_76 109 20 68 7 21085 453591 1.66e8 0.11% 98.72% +k_shape_26 57 10 12 11 36600 0 1.59e8 0.11% 98.83% +try_reduce_fin_val_decidable_rec 149 9 58 37 14010 42719 1.44e8 0.10% 98.93% +k_shape_09 65 40 6 5 29174 205635 1.42e8 0.10% 99.03% +k_shape_68 153 17 49 14 12585 1295 1.32e8 0.09% 99.12% +Bytes2 24 0 0 0 65536 0 1.28e8 0.09% 99.20% +k_shape_22 71 21 10 9 21040 607 1.08e8 0.07% 99.28% +k_shape_00 60 36 1 1 22065 112773 9.63e7 0.07% 99.34% +k_shape_03 66 40 2 2 19159 576657 9.06e7 0.06% 99.40% +k_shape_02 60 40 2 1 20742 431024 9.00e7 0.06% 99.47% +k_shape_10 77 40 6 5 15648 24001 8.45e7 0.06% 99.52% +k_shape_46 109 27 23 15 10653 154621 7.81e7 0.05% 99.58% +k_shape_84 259 19 151 9 4888 1019 7.77e7 0.05% 99.63% +k_shape_25 60 27 12 6 17832 69188 7.62e7 0.05% 99.68% +k_shape_64 104 20 39 16 9431 0 6.51e7 0.04% 99.73% +k_shape_41 92 25 20 15 10337 690 6.38e7 0.04% 99.77% +memory[32] 41 0 0 0 20282 85992 6.02e7 0.04% 99.81% +k_infer_only 93 12 45 15 7639 13614 4.61e7 0.03% 99.84% +k_shape_34 75 32 16 8 7402 18679 3.59e7 0.02% 99.87% +blake3_compress_layer 223 3 170 6 2064 0 2.54e7 0.02% 99.88% +k_shape_20 56 26 10 6 6883 22590 2.48e7 0.02% 99.90% +k_shape_28 71 38 13 7 3791 1286345 1.61e7 0.01% 99.91% +k_shape_23 66 38 11 5 4008 6626 1.60e7 0.01% 99.92% +k_shape_57 88 6 33 6 2104 44 1.03e7 0.01% 99.93% +k_shape_72 109 17 58 8 1621 15636 9.48e6 0.01% 99.93% +k_shape_29 74 26 13 12 2192 9659888 9.08e6 0.01% 99.94% +load_verified_constant 100 1 88 5 1621 2066 8.70e6 0.01% 99.95% +k_shape_55 95 17 31 20 1566 73 7.95e6 0.01% 99.95% +blake3 86 1 72 8 1707 114 7.94e6 0.01% 99.96% +memory[34] 43 0 0 0 2815 7298 7.04e6 0.00% 99.96% +k_shape_50 90 24 26 16 1385 530 6.55e6 0.00% 99.97% +k_shape_74 173 29 60 37 724 254254 5.98e6 0.00% 99.97% +get_constant_info_by_variant 64 8 46 2 1542 0 5.28e6 0.00% 99.97% +k_shape_56 105 19 32 22 693 456 3.46e6 0.00% 99.98% +k_shape_18 56 9 9 9 1012 164 2.87e6 0.00% 99.98% +k_shape_48 105 24 24 20 538 801 2.58e6 0.00% 99.98% +k_shape_53 115 17 30 26 479 5 2.47e6 0.00% 99.98% +k_shape_78 171 11 75 40 307 15 2.18e6 0.00% 99.98% +k_shape_15 69 38 8 5 638 336 2.07e6 0.00% 99.99% +k_shape_44 86 27 22 15 524 0 2.05e6 0.00% 99.99% +k_shape_04 54 40 2 2 697 52574 1.80e6 0.00% 99.99% +memory[12] 21 0 0 0 1548 416435 1.78e6 0.00% 99.99% +k_is_def_eq_struct_go 58 26 13 6 625 0 1.71e6 0.00% 99.99% +nl_subsume_entry 121 13 54 24 297 59 1.49e6 0.00% 99.99% +k_shape_67 80 7 48 6 400 12 1.40e6 0.00% 99.99% +k_shape_77 145 16 71 11 237 0 1.36e6 0.00% 99.99% +k_shape_70 80 11 51 5 313 80 1.05e6 0.00% 99.99% +k_shape_83 153 11 110 9 158 9601 8.88e5 0.00% 99.99% +k_shape_58 67 11 34 7 303 6273 8.48e5 0.00% 99.99% +k_shape_71 99 15 53 7 192 78 7.28e5 0.00% 100.00% +k_shape_73 112 14 59 8 146 12 5.93e5 0.00% 100.00% +k_shape_69 82 15 50 4 183 181 5.70e5 0.00% 100.00% +k_shape_05 96 40 2 2 139 13000 4.80e5 0.00% 100.00% +k_shape_65 88 13 42 8 149 29 4.79e5 0.00% 100.00% +k_shape_61 82 8 35 15 145 4 4.32e5 0.00% 100.00% +k_shape_40 67 16 20 5 157 143 3.89e5 0.00% 100.00% +ctor_at 86 2 72 3 117 2 3.50e5 0.00% 100.00% +k_shape_63 86 12 39 6 95 78 2.72e5 0.00% 100.00% +put_address 106 1 65 34 79 35 2.67e5 0.00% 100.00% +muts_member_at 108 2 94 3 77 177 2.63e5 0.00% 100.00% +k_shape_66 144 22 44 35 51 14 2.10e5 0.00% 100.00% +k_shape_27 58 22 13 5 99 2565 1.94e5 0.00% 100.00% +const_idxs_ctors 57 2 40 5 95 76 1.81e5 0.00% 100.00% +get_inductive 67 1 51 9 79 0 1.70e5 0.00% 100.00% +compare_rules 89 4 40 16 61 0 1.63e5 0.00% 100.00% +k_shape_38 60 8 19 7 79 0 1.52e5 0.00% 100.00% +memory[10] 19 0 0 0 195 108527 1.48e5 0.00% 100.00% +memory[36] 45 0 0 0 95 375 1.44e5 0.00% 100.00% +memory[47] 56 0 0 0 78 1009 1.40e5 0.00% 100.00% +k_shape_42 45 2 21 4 90 0 1.35e5 0.00% 100.00% +load_verified_blob 46 1 36 3 85 739 1.28e5 0.00% 100.00% +Bytes1 11 0 0 0 256 0 1.22e5 0.00% 100.00% +memory[8] 17 0 0 0 151 44897 9.83e4 0.00% 100.00% +build_flat_block 159 7 121 12 26 0 9.81e4 0.00% 100.00% +check_recursor_canonical_full 125 9 50 18 26 0 7.73e4 0.00% 100.00% +k_shape_21 71 37 10 7 36 172 6.74e4 0.00% 100.00% +build_minor_at_depth 65 1 25 21 35 0 5.96e4 0.00% 100.00% +k_shape_33 60 4 15 12 37 0 5.92e4 0.00% 100.00% +klimbs_mul_single 86 3 47 7 28 0 5.89e4 0.00% 100.00% +u64_mul 222 1 155 46 13 0 5.39e4 0.00% 100.00% +k_shape_49 85 5 25 8 23 316 4.50e4 0.00% 100.00% +build_succ_offset 57 2 17 16 30 0 4.30e4 0.00% 100.00% +nlvars_subsume 111 6 49 25 17 3 3.92e4 0.00% 100.00% +memory[9] 18 0 0 0 46 304 2.45e4 0.00% 100.00% +memory[11] 20 0 0 0 36 122 1.99e4 0.00% 100.00% +memory[5] 14 0 0 0 36 17400 1.43e4 0.00% 100.00% +memory[6] 15 0 0 0 27 337 1.06e4 0.00% 100.00% +u64_byte_count 150 128 8 1 4 237 6.14e3 0.00% 100.00% +k_shape_01 38 26 1 2 6 1338 3.16e3 0.00% 100.00% +memory[2] 11 0 0 0 12 96 2.80e3 0.00% 100.00% +k_shape_62 149 17 37 23 2 0 1.56e3 0.00% 100.00% +k_shape_54 58 9 31 6 2 0 6.52e2 0.00% 100.00% +verify_claim 40 1 1 2 1 0 2.16e2 0.00% 100.00% +klimbs_scalar_value 117 7 63 21 0 0 0 0.00% 100.00% +list_length_u64.RecursorRule 43 2 28 4 0 0 0 0.00% 100.00% +get_ctor_entry_list_inner 90 2 63 6 0 0 0 0.00% 100.00% +rbtree_map_balance_fix.G 122 57 31 8 0 0 0 0.00% 100.00% +k_shape_75 81 3 65 3 0 0 0 0.00% 100.00% +check_mut_const 127 3 1 10 0 0 0 0.00% 100.00% +k_shape_81 152 23 90 14 0 0 0 0.00% 100.00% +get_reveal_rule_list_inner 59 2 32 6 0 0 0 0.00% 100.00% +get_reveal_ctor_info 80 1 64 9 0 0 0 0.00% 100.00% +k_shape_60 111 7 35 8 0 0 0 0.00% 100.00% +list_length_u64.U8_8 42 2 27 4 0 0 0 0.00% 100.00% +k_shape_59 89 3 34 10 0 0 0 0.00% 100.00% +univ_succ_count 49 2 26 4 0 0 0 0.00% 100.00% +k_shape_80 132 11 85 12 0 0 0 0.00% 100.00% +str_lit_to_ctor 49 1 21 21 0 0 0 0.00% 100.00% +memory[19] 28 0 0 0 0 0 0 0.00% 100.00% +k_shape_79 118 9 80 8 0 0 0 0.00% 100.00% +canon_addr_cmp 105 1 80 18 0 0 0 0.00% 100.00% +list_length_u64.MutConst 79 2 64 4 0 0 0 0.00% 100.00% +canon_cmp_kexpr_node_ctx 79 40 12 7 0 0 0 0.00% 100.00% +memory[50] 59 0 0 0 0 0 0 0.00% 100.00% +memory[64] 73 0 0 0 0 0 0 0.00% 100.00% +try_str_dispatch 128 18 47 28 0 0 0 0.00% 100.00% diff --git a/cold-groups/kstats2-grouped-String.split.txt b/cold-groups/kstats2-grouped-String.split.txt new file mode 100644 index 00000000..1d271b2e --- /dev/null +++ b/cold-groups/kstats2-grouped-String.split.txt @@ -0,0 +1,194 @@ +=== Circuit Statistics === +Circuits: 185 +Total width: 15763 +Total FFT cost: 56219185748 (5.62e10) +Total cache hits: 22638136 +Total saved cost: 56.54% +------------------------------------------------------------------------------------------- +Name Width Sel Aux Lkp Height Hits FFT cost % %++ +------------------------------------------------------------------------------------------- +blake3_compress_inner_j 696 1 369 193 136626 0 8.12e9 14.44% 14.44% +memory[3] 12 0 0 0 2947763 6323771 3.91e9 6.95% 21.39% +blake3_compress_chunks 29 3 7 4 1157705 0 3.42e9 6.09% 27.48% +expr_inst_many_walk 34 9 8 5 915195 0 3.11e9 5.54% 33.01% +expr_inst_many 21 2 4 4 1199626 299856 2.59e9 4.60% 37.62% +blake3_compress 1080 1 929 40 19518 15 1.50e9 2.67% 40.29% +get_expr 50 12 23 5 309599 20 1.42e9 2.53% 42.82% +k_shape_32 114 31 15 8 139484 10824 1.36e9 2.43% 45.25% +convert_expr 60 12 25 7 240901 122716 1.30e9 2.31% 47.56% +k_infer_app_spine_loop 59 8 21 11 241267 677 1.28e9 2.28% 49.84% +list_drop.Ptr.Expr 20 2 6 3 592814 270333 1.16e9 2.06% 51.90% +expr_lbr 35 9 9 6 350993 2611613 1.14e9 2.04% 53.93% +k_shape_08 75 40 5 4 170460 41825 1.12e9 1.99% 55.92% +list_snoc.G 22 2 6 4 521574 184967 1.11e9 1.97% 57.89% +get_tag4 37 2 22 4 311460 0 1.06e9 1.89% 59.78% +k_shape_07 68 38 4 4 168577 17839 1.00e9 1.78% 61.56% +k_shape_06 94 33 3 4 102822 89536 8.08e8 1.44% 63.00% +g_list_has 21 3 6 3 396339 3419 7.88e8 1.40% 64.40% +get_app_telescope 43 2 15 6 204828 0 7.84e8 1.40% 65.80% +expr_glb_walk 34 10 8 5 231083 0 7.08e8 1.26% 67.06% +k_shape_14 89 16 7 7 89851 47335 6.61e8 1.18% 68.23% +validate_expr_well_scoped 52 9 20 8 144351 118355 6.48e8 1.15% 69.39% +k_shape_12 74 40 7 4 103208 48896 6.40e8 1.14% 70.53% +peel_beta 32 3 12 5 221723 3113 6.38e8 1.13% 71.66% +memory[4] 13 0 0 0 497573 4533682 6.30e8 1.12% 72.78% +expr_inst_many_bvar 24 2 5 5 278974 0 6.16e8 1.10% 73.88% +expr_inst1_walk 34 9 8 5 202168 0 6.13e8 1.09% 74.97% +get_u64_le 28 2 14 3 240867 22 6.12e8 1.09% 76.05% +collect_spine 23 2 8 4 281491 197009 5.96e8 1.06% 77.12% +list_concat.Ptr.KExprNode 22 2 6 4 278551 242297 5.64e8 1.00% 78.12% +whnf_with_spine 34 6 11 5 175764 4941 5.27e8 0.94% 79.06% +expr_lower_walk 53 10 18 9 115078 0 5.17e8 0.92% 79.98% +k_infer_core 53 9 22 8 112780 54815 5.06e8 0.90% 80.87% +expr_inst1 21 2 4 4 261823 104786 5.04e8 0.90% 81.77% +const_idxs_expr 52 7 26 7 110757 166346 4.87e8 0.87% 82.64% +k_shape_45 89 31 23 9 65208 9293 4.66e8 0.83% 83.47% +expr_glb 21 2 5 4 240811 257285 4.61e8 0.82% 84.29% +list_lookup.Ptr.KLevelNode 16 1 5 3 294825 71690 4.39e8 0.78% 85.07% +k_shape_13 84 38 7 5 64872 6348 4.38e8 0.78% 85.85% +k_shape_30 64 22 14 6 78610 23007 4.12e8 0.73% 86.58% +list_length.Ptr.KExprNode 18 2 5 3 249239 712085 4.11e8 0.73% 87.31% +expr_lift_walk 34 9 8 5 139072 0 4.09e8 0.73% 88.04% +safe_refs_only 43 9 19 5 111679 109780 4.07e8 0.72% 88.76% +k_shape_39 91 36 19 14 55560 202576 4.00e8 0.71% 89.47% +expr_lift 23 3 5 4 182612 389282 3.74e8 0.66% 90.14% +bytes_to_block 265 1 193 65 18371 661 3.45e8 0.61% 90.75% +k_shape_17 70 39 9 6 52011 17320 2.87e8 0.51% 91.26% +k_shape_16 118 39 9 8 31099 1468 2.75e8 0.49% 91.75% +whnf_const_head 77 16 32 10 44889 0 2.69e8 0.48% 92.23% +k_shape_82 213 5 100 51 17795 109 2.68e8 0.48% 92.71% +expr_lower 23 3 5 4 130790 108524 2.60e8 0.46% 93.17% +memory[18] 27 0 0 0 110757 606238 2.55e8 0.45% 93.62% +blake3_compress_block 211 2 169 15 17109 0 2.54e8 0.45% 94.08% +k_shape_24 74 40 12 7 43922 5158 2.52e8 0.45% 94.52% +k_shape_43 65 14 22 7 47013 124 2.39e8 0.42% 94.95% +k_shape_76 109 20 68 7 24620 102066 1.97e8 0.35% 95.30% +apply_spine_expr 22 2 6 4 104043 16635 1.94e8 0.35% 95.64% +k_shape_11 102 39 7 6 24312 1271 1.82e8 0.32% 95.97% +k_shape_09 65 40 6 5 34183 58169 1.69e8 0.30% 96.27% +k_shape_35 80 12 16 16 28108 2610 1.67e8 0.30% 96.56% +k_shape_37 91 30 18 12 23588 1702 1.57e8 0.28% 96.84% +try_reduce_projection_definition 59 3 24 13 29751 4863 1.31e8 0.23% 97.08% +whnf_apply_beta 34 3 10 7 48959 0 1.31e8 0.23% 97.31% +Bytes2 24 0 0 0 65536 0 1.28e8 0.23% 97.54% +try_prim_dispatch 30 6 8 4 48652 4883 1.15e8 0.21% 97.74% +k_shape_36 83 33 17 10 17139 4182 1.01e8 0.18% 97.92% +k_shape_19 64 36 10 5 20850 12719 9.65e7 0.17% 98.10% +k_shape_52 113 40 29 16 12068 683 9.29e7 0.17% 98.26% +k_shape_10 77 40 6 5 16471 23576 8.94e7 0.16% 98.42% +k_shape_26 57 10 12 11 19720 0 8.09e7 0.14% 98.56% +k_shape_84 259 19 151 9 5000 1097 7.97e7 0.14% 98.71% +try_iota 108 5 39 25 9346 388 6.69e7 0.12% 98.82% +memory[32] 41 0 0 0 18539 87446 5.46e7 0.10% 98.92% +k_shape_31 131 38 14 13 5961 6592 4.92e7 0.09% 99.01% +k_shape_51 79 9 27 17 9011 306 4.71e7 0.08% 99.09% +k_shape_25 60 27 12 6 9802 9887 3.93e7 0.07% 99.16% +k_shape_22 71 21 10 9 8207 263 3.82e7 0.07% 99.23% +k_shape_47 93 38 24 9 6278 5544 3.71e7 0.07% 99.30% +blake3_compress_layer 223 3 170 6 2324 0 2.91e7 0.05% 99.35% +k_shape_41 92 25 20 15 4926 346 2.80e7 0.05% 99.40% +k_infer_only 93 12 45 15 4753 2955 2.72e7 0.05% 99.45% +k_shape_46 109 27 23 15 3849 30060 2.51e7 0.04% 99.49% +k_shape_00 60 36 1 1 6536 108063 2.51e7 0.04% 99.54% +k_shape_68 153 17 49 14 2712 483 2.38e7 0.04% 99.58% +try_reduce_fin_val_decidable_rec 149 9 58 37 2472 9544 2.08e7 0.04% 99.61% +k_shape_64 104 20 39 16 3069 0 1.86e7 0.03% 99.65% +k_shape_02 60 40 2 1 4868 320964 1.81e7 0.03% 99.68% +k_shape_28 71 38 13 7 3961 670185 1.69e7 0.03% 99.71% +k_shape_23 66 38 11 5 3867 2360 1.53e7 0.03% 99.74% +k_shape_03 66 40 2 2 3219 484594 1.25e7 0.02% 99.76% +k_shape_57 88 6 33 6 2414 53 1.20e7 0.02% 99.78% +k_shape_34 75 32 16 8 2676 20463 1.15e7 0.02% 99.80% +k_shape_72 109 17 58 8 1860 17498 1.11e7 0.02% 99.82% +load_verified_constant 100 1 88 5 1860 2402 1.02e7 0.02% 99.84% +k_shape_29 74 26 13 12 2304 2290845 9.61e6 0.02% 99.86% +blake3 86 1 72 8 1950 140 9.23e6 0.02% 99.87% +memory[34] 43 0 0 0 2651 7671 6.58e6 0.01% 99.88% +k_shape_74 173 29 60 37 783 48057 6.54e6 0.01% 99.90% +k_shape_20 56 26 10 6 2054 6432 6.40e6 0.01% 99.91% +get_constant_info_by_variant 64 8 46 2 1765 0 6.16e6 0.01% 99.92% +k_shape_55 95 17 31 20 988 78 4.70e6 0.01% 99.93% +k_shape_18 56 9 9 9 1055 199 3.00e6 0.01% 99.93% +k_shape_56 105 19 32 22 561 480 2.71e6 0.00% 99.94% +k_shape_48 105 24 24 20 542 246 2.60e6 0.00% 99.94% +k_shape_44 86 27 22 15 611 0 2.45e6 0.00% 99.95% +k_shape_78 171 11 75 40 321 15 2.30e6 0.00% 99.95% +k_shape_15 69 38 8 5 676 378 2.22e6 0.00% 99.95% +memory[12] 21 0 0 0 1772 97658 2.07e6 0.00% 99.96% +k_shape_50 90 24 26 16 503 39 2.05e6 0.00% 99.96% +k_shape_04 54 40 2 2 680 20933 1.75e6 0.00% 99.96% +k_shape_67 80 7 48 6 483 13 1.74e6 0.00% 99.97% +k_shape_77 145 16 71 11 287 0 1.71e6 0.00% 99.97% +k_is_def_eq_struct_go 58 26 13 6 623 0 1.70e6 0.00% 99.97% +nl_subsume_entry 121 13 54 24 311 63 1.57e6 0.00% 99.98% +k_shape_70 80 11 51 5 375 97 1.30e6 0.00% 99.98% +k_shape_53 115 17 30 26 257 4 1.19e6 0.00% 99.98% +k_shape_83 153 11 110 9 190 1164 1.11e6 0.00% 99.98% +k_shape_58 67 11 34 7 337 1254 9.60e5 0.00% 99.98% +k_shape_71 99 15 53 7 232 94 9.11e5 0.00% 99.99% +k_shape_73 112 14 59 8 177 13 7.47e5 0.00% 99.99% +k_shape_69 82 15 50 4 222 221 7.17e5 0.00% 99.99% +k_shape_05 96 40 2 2 165 12555 5.89e5 0.00% 99.99% +k_shape_61 82 8 35 15 175 5 5.41e5 0.00% 99.99% +k_shape_65 88 13 42 8 152 14 4.90e5 0.00% 99.99% +ctor_at 86 2 72 3 141 3 4.38e5 0.00% 99.99% +k_shape_40 67 16 20 5 165 172 4.13e5 0.00% 99.99% +k_shape_63 86 12 39 6 114 94 3.39e5 0.00% 99.99% +put_address 106 1 65 34 95 45 3.34e5 0.00% 99.99% +muts_member_at 108 2 94 3 92 214 3.27e5 0.00% 99.99% +const_idxs_ctors 57 2 40 5 114 91 2.26e5 0.00% 100.00% +compare_rules 89 4 40 16 77 0 2.18e5 0.00% 100.00% +get_inductive 67 1 51 9 95 0 2.13e5 0.00% 100.00% +k_shape_38 60 8 19 7 101 0 2.05e5 0.00% 100.00% +memory[36] 45 0 0 0 114 453 1.79e5 0.00% 100.00% +k_shape_27 58 22 13 5 91 2877 1.75e5 0.00% 100.00% +memory[47] 56 0 0 0 93 1214 1.74e5 0.00% 100.00% +k_shape_42 45 2 21 4 109 0 1.70e5 0.00% 100.00% +memory[10] 19 0 0 0 210 59730 1.61e5 0.00% 100.00% +k_shape_66 144 22 44 35 38 14 1.45e5 0.00% 100.00% +load_verified_blob 46 1 36 3 89 711 1.36e5 0.00% 100.00% +build_flat_block 159 7 121 12 32 0 1.28e5 0.00% 100.00% +Bytes1 11 0 0 0 256 0 1.22e5 0.00% 100.00% +check_recursor_canonical_full 125 9 50 18 32 0 1.01e5 0.00% 100.00% +build_minor_at_depth 65 1 25 21 45 0 8.19e4 0.00% 100.00% +k_shape_33 60 4 15 12 47 0 8.00e4 0.00% 100.00% +k_shape_21 71 37 10 7 37 211 6.98e4 0.00% 100.00% +klimbs_mul_single 86 3 47 7 27 0 5.62e4 0.00% 100.00% +u64_mul 222 1 155 46 13 0 5.39e4 0.00% 100.00% +build_succ_offset 57 2 17 16 30 0 4.30e4 0.00% 100.00% +nlvars_subsume 111 6 49 25 17 3 3.92e4 0.00% 100.00% +memory[11] 20 0 0 0 46 154 2.71e4 0.00% 100.00% +memory[9] 18 0 0 0 48 351 2.59e4 0.00% 100.00% +k_shape_49 85 5 25 8 14 279 2.32e4 0.00% 100.00% +memory[5] 14 0 0 0 46 4726 1.94e4 0.00% 100.00% +memory[6] 15 0 0 0 33 417 1.37e4 0.00% 100.00% +memory[8] 17 0 0 0 29 40990 1.30e4 0.00% 100.00% +u64_byte_count 150 128 8 1 5 292 8.89e3 0.00% 100.00% +k_shape_62 149 17 37 23 3 0 3.65e3 0.00% 100.00% +k_shape_01 38 26 1 2 6 1520 3.16e3 0.00% 100.00% +memory[2] 11 0 0 0 13 99 3.11e3 0.00% 100.00% +try_str_dispatch 128 18 47 28 2 0 1.35e3 0.00% 100.00% +k_shape_54 58 9 31 6 2 0 6.52e2 0.00% 100.00% +verify_claim 40 1 1 2 1 0 2.16e2 0.00% 100.00% +list_length_u64.MutConst 79 2 64 4 0 0 0 0.00% 100.00% +get_reveal_rule_list_inner 59 2 32 6 0 0 0 0.00% 100.00% +rbtree_map_balance_fix.G 122 57 31 8 0 0 0 0.00% 100.00% +klimbs_scalar_value 117 7 63 21 0 0 0 0.00% 100.00% +get_reveal_ctor_info 80 1 64 9 0 0 0 0.00% 100.00% +get_ctor_entry_list_inner 90 2 63 6 0 0 0 0.00% 100.00% +k_shape_75 81 3 65 3 0 0 0 0.00% 100.00% +check_mut_const 127 3 1 10 0 0 0 0.00% 100.00% +list_length_u64.RecursorRule 43 2 28 4 0 0 0 0.00% 100.00% +k_shape_60 111 7 35 8 0 0 0 0.00% 100.00% +k_shape_79 118 9 80 8 0 0 0 0.00% 100.00% +list_length_u64.U8_8 42 2 27 4 0 0 0 0.00% 100.00% +univ_succ_count 49 2 26 4 0 0 0 0.00% 100.00% +k_shape_81 152 23 90 14 0 0 0 0.00% 100.00% +memory[19] 28 0 0 0 0 0 0 0.00% 100.00% +str_lit_to_ctor 49 1 21 21 0 0 0 0.00% 100.00% +k_shape_59 89 3 34 10 0 0 0 0.00% 100.00% +canon_addr_cmp 105 1 80 18 0 0 0 0.00% 100.00% +canon_cmp_kexpr_node_ctx 79 40 12 7 0 0 0 0.00% 100.00% +memory[50] 59 0 0 0 0 0 0 0.00% 100.00% +memory[64] 73 0 0 0 0 0 0 0.00% 100.00% +k_shape_80 132 11 85 12 0 0 0 0.00% 100.00% diff --git a/crates/aiur/src/bytecode.rs b/crates/aiur/src/bytecode.rs index 57e426e8..3349906f 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 26488ce5..8691198b 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 47d7ea37..6099213e 100644 --- a/crates/aiur/src/synthesis.rs +++ b/crates/aiur/src/synthesis.rs @@ -89,20 +89,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 @@ -156,11 +153,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 @@ -384,6 +378,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]) }; @@ -398,7 +411,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 { @@ -417,7 +430,7 @@ mod tests { entry: true, constrained: true, }; - Toplevel { functions: vec![function], memory_sizes: vec![] } + with_singleton_circuits(vec![function], vec![]) } #[test] @@ -523,7 +536,7 @@ mod tests { constrained: true, }; - Toplevel { functions: vec![f, g], memory_sizes: vec![1] } + with_singleton_circuits(vec![f, g], vec![1]) } #[test] diff --git a/crates/aiur/src/trace.rs b/crates/aiur/src/trace.rs index e87dfe15..66e88cf9 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 4b88cdac..fbead94f 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 e9040c66..0cd5b9ed 100644 --- a/crates/ffi/src/lean.rs +++ b/crates/ffi/src/lean.rs @@ -270,8 +270,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