From c77192b930c5e40d876fcf74e7067a8d050f27d7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 11 Jul 2026 14:22:50 +0000 Subject: [PATCH] perf(hex-matrix): Submatrix views for the mulStrassen recursion MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add the Submatrix view type (Subarray-style: base matrix, row/col offsets, block dimensions; entry reads are offset arithmetic into the shared flat buffer) and rewire mulStrassen's internal recursion over views, so quadrants stop being materialized copies — generated C shows zero quadrant-copy allocations, with allocation remaining only for the operand sums, the seven products, padding, and leaf materialization for the unchanged baseMul signature. mulStrassen_eq_mul is re-proved via view-to-Matrix abstraction lemmas; the algorithm, its statement, and the three named correctness lemmas are untouched. The colAdd family moves from the materializing mapRows pass to flat per-entry column engines with unchanged public lemma statements. Cost model re-measured on the view recursion: cutoff sweep and scaling series within noise of the committed flat baseline (0.99-1.01x), so strassenDefault.cutoff stays at the measured 96; the committed exports and overlay figure record the outcome. Closes #8652. Co-Authored-By: Claude Fable 5 --- HexMatrix/Elementary.lean | 60 +- HexMatrix/SPEC/hex-matrix.md | 64 +- HexMatrix/Strassen.lean | 246 ++- HexMatrix/Submatrix.lean | 175 +++ ...matrix-mul-scaling-flat-view-chungus2.json | 532 +++++++ ...-matrix-strassen-cutoff-view-chungus2.json | 1320 +++++++++++++++++ reports/figures/hex-matrix-mul-scaling.svg | 310 ++-- 7 files changed, 2435 insertions(+), 272 deletions(-) create mode 100644 reports/bench-results/hex-matrix-mul-scaling-flat-view-chungus2.json create mode 100644 reports/bench-results/hex-matrix-strassen-cutoff-view-chungus2.json diff --git a/HexMatrix/Elementary.lean b/HexMatrix/Elementary.lean index 0cafd0de1..f8fdc8a7d 100644 --- a/HexMatrix/Elementary.lean +++ b/HexMatrix/Elementary.lean @@ -264,23 +264,29 @@ replaced by `M[dst][k] + c * M[src][k]`. -/ /-- Replace column `dst` by `col dst + c * col src`. -Each row is mapped to its update of the single `dst` entry. On the flat -backing `mapRows` materializes the rows and reflattens, so this is a -value-level pass over the matrix, not an in-place column write; a flat -per-entry column engine (like `setCol`/`modifyCol`) is follow-up work -alongside the `BlockView` recursion. -/ +The source column is read once into `csrc` (one contiguous copy, a borrowed read +taken before the write); the subsequent `modifyCol` then holds the only live +reference to the buffer and updates the `dst` column entry of each row in place — +one single-entry `Vector.modify` of the flat buffer per row (`O(n)` writes +total) — when the runtime sees it uniquely referenced, with no row +materialization. This replaces the former `mapRows` pass, which materialized and +reflattened every row. -/ @[expose] def colAdd [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) : Matrix R n m := - M.mapRows fun row => row.set dst (row[dst] + c * row[src]) + let csrc := M.col src + M.modifyCol dst fun i x => x + c * csrc[i] /-- Replace column `dst` by `col dst + col src * c`. -This is the right-scalar variant of `colAdd`. It is the column-add operation -whose right-multiplication wrapper is valid over a noncommutative ring. -/ +This is the right-scalar variant of `colAdd`, valid as a right-multiplication +wrapper over a noncommutative ring. Same flat per-entry column engine as +`colAdd`: read the source column once, then `modifyCol` the `dst` entries in +place. -/ @[expose] def colAddRight [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) : Matrix R n m := - M.mapRows fun row => row.set dst (row[dst] + row[src] * c) + let csrc := M.col src + M.modifyCol dst fun i x => x + csrc[i] * c /-- Read an entry of `colAdd M src dst c` by cases on the column index: column `dst` returns `M[i][dst] + c * M[i][src]`, any other column is @@ -289,9 +295,10 @@ theorem getElem_colAdd [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) (i : Fin n) (j : Fin m) : (colAdd M src dst c)[i][j] = if j = dst then M[i][j] + c * M[i][src] else M[i][j] := by - rw [colAdd, getElem_eq_getRow, getRow_mapRows] - simp only [Vector.getElem_set, getElem_eq_getRow, Fin.getElem_fin, Fin.ext_iff] - grind + rw [colAdd, getElem_modifyCol] + by_cases hj : j = dst + · rw [if_pos hj, if_pos hj, hj, getElem_col] + · rw [if_neg hj, if_neg hj] /-- Read an entry of `colAddRight M src dst c` by cases on the column index: column `dst` returns `M[i][dst] + M[i][src] * c`, any other column is @@ -300,9 +307,10 @@ theorem getElem_colAddRight [Mul R] [Add R] (M : Matrix R n m) (src dst : Fin m) (c : R) (i : Fin n) (j : Fin m) : (colAddRight M src dst c)[i][j] = if j = dst then M[i][j] + M[i][src] * c else M[i][j] := by - rw [colAddRight, getElem_eq_getRow, getRow_mapRows] - simp only [Vector.getElem_set, getElem_eq_getRow, Fin.getElem_fin, Fin.ext_iff] - grind + rw [colAddRight, getElem_modifyCol] + by_cases hj : j = dst + · rw [if_pos hj, if_pos hj, hj, getElem_col] + · rw [if_neg hj, if_neg hj] /-- Column `dst` of `colAdd M src dst c` is the pointwise column combination. -/ @[simp, grind =] theorem col_colAdd_dst [Mul R] [Add R] @@ -407,12 +415,16 @@ replaced by `M[i][dst] + M[i][src] * c`. -/ /-- Swap columns `i` and `j` in a dense matrix. -The swap is done row by row via `mapRows`: each row's `i` and `j` entries are -exchanged with `Vector.swap`, reusing the freed row slot when `M` is uniquely -referenced. The column mirror of `rowSwap`. -/ +Both columns are read once (two borrowed `O(n)` reads taken before the writes), +then written back with two `setCol` passes that update one flat-buffer entry per +row in place, reusing the backing store when `M` is uniquely referenced. This +replaces the former `mapRows` pass, which materialized and reflattened every row. +The column mirror of `rowSwap`. -/ @[expose] def colSwap (M : Matrix R n m) (i j : Fin m) : Matrix R n m := - M.mapRows fun row => row.swap i j + let ci := M.col i + let cj := M.col j + (M.setCol i fun r => cj[r]).setCol j fun r => ci[r] /-- Read an entry of `colSwap M i j` by cases on the column index: column `j` returns the original column `i`, column `i` returns the original column `j`, and @@ -420,9 +432,13 @@ any other column is unchanged. -/ @[grind =] theorem getElem_colSwap (M : Matrix R n m) (i j : Fin m) (r : Fin n) (c : Fin m) : (colSwap M i j)[r][c] = if c = j then M[r][i] else if c = i then M[r][j] else M[r][c] := by - rw [colSwap, getElem_eq_getRow, getRow_mapRows] - simp only [Vector.getElem_swap, getElem_eq_getRow, Fin.getElem_fin, Fin.ext_iff] - grind + rw [colSwap, getElem_setCol] + by_cases hcj : c = j + · rw [if_pos hcj, if_pos hcj, getElem_col] + · rw [if_neg hcj, if_neg hcj, getElem_setCol] + by_cases hci : c = i + · rw [if_pos hci, if_pos hci, getElem_col] + · rw [if_neg hci, if_neg hci] /-- Column `i` of `colSwap M i j` is the original column `j`. -/ @[simp, grind =] theorem col_colSwap_left (M : Matrix R n m) (i j : Fin m) : diff --git a/HexMatrix/SPEC/hex-matrix.md b/HexMatrix/SPEC/hex-matrix.md index 7f8b25130..720c1f7e7 100644 --- a/HexMatrix/SPEC/hex-matrix.md +++ b/HexMatrix/SPEC/hex-matrix.md @@ -69,12 +69,15 @@ rather than copying it. **Indexed row/column mutation.** `modifyRow` updates one row span in place; `setCol` and the per-entry `modifyCol` update one column entry per row through flat per-entry folds over the single buffer. The column *analogues* of the -elementary operations (`colAdd`, `colAddRight`, `colSwap`) currently go -through `mapRows`, which materializes the rows and reflattens — a value-level -pass, not an in-place column write; migrating them to the flat per-entry -engine is follow-up work alongside the `BlockView` recursion. -This replaces the former `ofFn`-rebuild form of `setCol`, which read and -reallocated every entry to change one column. +elementary operations (`colAdd`, `colAddRight`, `colSwap`) run the same flat +per-entry column engine: each reads the source column(s) once into a borrowed +`O(n)` vector, then writes the destination column entries in place through +`modifyCol` (`colAdd`/`colAddRight`) or two `setCol` passes (`colSwap`) — one +single-entry flat-buffer write per row, reusing the backing store when the +matrix is uniquely referenced, with no row materialization. This replaced the +former `mapRows` form, which materialized every row and reflattened, and the +former `ofFn`-rebuild form of `setCol`, which read and reallocated every entry +to change one column. **Key properties:** - identity matrices act as left and right multiplicative identities @@ -250,14 +253,22 @@ condition is config-independent. ### Avoiding sub-block copies -The four quadrants of `A`, `B`, and `C` are **views**, not freshly materialized -matrices: a view is a backing matrix together with a row offset, a column -offset, and the two block dimensions. Reading a quadrant entry adds the offset -and indexes the backing store. The recursive splitting therefore allocates -nothing for the quadrants themselves. The internal recursion is stated over this -view type, not over `Matrix`. Only when a block drops below the cutoff does the -recursion **materialize** that small view into a `Matrix` and hand it to -`cfg.baseMul`, which is why the public `baseMul` keeps the clean +The four quadrants of `A` and `B` are **views** (`Submatrix`, named in the +`Subarray`/`Substring` style), not freshly materialized matrices: a `Submatrix` +is a backing matrix together with a row offset, a column offset, the two block +dimensions (type indices), and the real-data extent (`rhi`/`chi`, one past the +last real row/column in backing coordinates). Reading a quadrant entry adds the +offset and indexes the shared backing store when the position holds real data +(`r0 + i < rhi ∧ c0 + j < chi`) and returns `0` in the zero-pad fringe otherwise. +The recursive splitting therefore allocates nothing for the quadrants themselves +— `Submatrix.toBlocks₁₁ … toBlocks₂₂` are pure offset/extent arithmetic. Because +the backing dims never change through the recursion, `r0 + i < rhi` is the exact +real-vs-pad test at every nesting depth, so widening a view to even dimensions +(`Submatrix.pad`) before a split is likewise a copy-free reshape. The internal +recursion `mulStrassenView` is stated over this view type, not over `Matrix`. +Only when a block drops below the cutoff does the recursion **materialize** that +small view into a `Matrix` (`Submatrix.toMatrix`) and hand it to `cfg.baseMul`, +which is why the public `baseMul` keeps the clean `Matrix R n m → Matrix R m k → Matrix R n k` type: views inside the recursion, a materialized `Matrix` at each leaf. @@ -277,12 +288,18 @@ bulk materialization of a leaf block for the base kernel, and a block view that is pure offset-and-stride arithmetic into one shared buffer (`backing[(r0 + i) * m + (c0 + j)]`). `Hex.Matrix` is deliberately an opaque one-field structure (design principle 10) precisely so that representation -switch stayed invisible to consumers when it landed. The current -implementation recurses over materialized `Matrix` quadrants (reusing the -existing matrix add and subtract) and pays the copies; the `BlockView` type -(backing matrix plus row/column offsets plus the block dimensions) and the -rewiring of the recursion over views is follow-up work on the same flat -backing. The recursion and the correctness proof are identical either way. +switch stayed invisible to consumers when it landed. The recursion runs over +the `Submatrix` view type (backing matrix plus row/column offsets plus block +dimensions plus real-data extent), so the only allocations are the fifteen +`Sᵢ`/`Tᵢ`/`Uᵢ` operand sums, the seven recursive products, the top-level +full-matrix view of each operand, and the leaf materialization for `cfg.baseMul` +— the per-level quadrant and pad copies are gone. Correctness reduces to the +same three lemmas: a view-to-matrix abstraction lemma (`toMatrix` of a quadrant +view equals `toBlocks` of the materialized parent, and `toMatrix` of a widened +view equals `Matrix.pad` of the materialized source) carries the view recursion +`mulStrassenView` down to the `mul`-level Winograd/block/padding decomposition, +so the recursion and the correctness proof are identical to the `Matrix`-level +form the migration first shipped. ### Correctness @@ -347,7 +364,7 @@ Strassen exponent is only a diagnostic, not an acceptance condition: near the cutoff the Strassen curve is in a crossover transient, and on the row-of-rows backing the locality overhead and the limited benched sizes bend the fit above `2.81`. The exponent approaches `log₂ 7` only once the sizes are large enough or -the `BlockView` recursion lands on the flat backing (see the representation +the `Submatrix` view recursion lands on the flat backing (see the representation note below). The point the figure must make is the visibly shallower Strassen slope: Strassen lowers the asymptotic order, not merely the constant factor. A speedup table @@ -363,9 +380,10 @@ across `64…1024`; identical checksums) with a small Bareiss elimination cost row-contiguous under row-of-rows, so parity is the expected reading; what the flat backing changes for Strassen is not these curves but the cost model of the *recursion's internals* — quadrant materialization and leaf handling — -which is why the crossover gets re-measured when the `BlockView`-based +which is why the crossover gets re-measured when the `Submatrix`-view recursion (see "Avoiding sub-block copies") replaces materialized quadrants, -not before. +not before. That re-measurement is recorded with the shipped +`strassenDefault.cutoff` in `HexMatrix/Strassen.lean`. ### A demonstration non-default config diff --git a/HexMatrix/Strassen.lean b/HexMatrix/Strassen.lean index 939f3c3d2..2b9d29131 100644 --- a/HexMatrix/Strassen.lean +++ b/HexMatrix/Strassen.lean @@ -48,6 +48,65 @@ namespace Matrix variable {R : Type u} {n m k : Nat} +/-! ### View-to-matrix abstraction + +The Strassen recursion runs over `Submatrix` views (`HexMatrix/Submatrix.lean`). +These lemmas relate a view's `toMatrix` materialization to the corresponding +`Matrix`-level `pad`/`toBlocks` operation, so the view recursion reduces to the +existing `mulStrassen_eq_mul` decomposition. -/ + +/-- Materializing a widened view is `Matrix.pad` of the materialized source. -/ +theorem toMatrix_pad_view [OfNat R 0] (A : Submatrix R n m) (n' m' : Nat) + (hn : n ≤ n') (hm : m ≤ m') : + (A.pad n' m' hn hm).toMatrix = pad A.toMatrix n' m' := by + apply ext_getElem + intro i j + rw [Submatrix.getElem_toMatrix, Submatrix.entry_pad, getElem_pad] + by_cases h : i.val < n ∧ j.val < m + · rw [dif_pos h, dif_pos h, getElem_pair_eq_nested, Submatrix.getElem_toMatrix] + · rw [dif_neg h, dif_neg h] + +/-- Materializing the top-left quadrant view is `Matrix.toBlocks₁₁` of the +materialized parent. -/ +theorem toMatrix_toBlocks₁₁ [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : + (Submatrix.toBlocks₁₁ A).toMatrix = toBlocks₁₁ A.toMatrix := by + apply ext_getElem + intro i j + rw [Submatrix.getElem_toMatrix, getElem_toBlocks₁₁, Submatrix.getElem_toMatrix, + Submatrix.entry, Submatrix.entry] + simp only [Submatrix.toBlocks₁₁, Fin.val_castAdd] + all_goals (have hi := i.isLt; have hj := j.isLt; split <;> split <;> (first | rfl | (exfalso; omega))) + +/-- Materializing the top-right quadrant view is `Matrix.toBlocks₁₂` of the parent. -/ +theorem toMatrix_toBlocks₁₂ [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : + (Submatrix.toBlocks₁₂ A).toMatrix = toBlocks₁₂ A.toMatrix := by + apply ext_getElem + intro i j + rw [Submatrix.getElem_toMatrix, getElem_toBlocks₁₂, Submatrix.getElem_toMatrix, + Submatrix.entry, Submatrix.entry] + simp only [Submatrix.toBlocks₁₂, Fin.val_castAdd, Fin.val_natAdd, Nat.add_assoc] + all_goals (have hi := i.isLt; have hj := j.isLt; split <;> split <;> (first | rfl | (exfalso; omega))) + +/-- Materializing the bottom-left quadrant view is `Matrix.toBlocks₂₁` of the parent. -/ +theorem toMatrix_toBlocks₂₁ [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : + (Submatrix.toBlocks₂₁ A).toMatrix = toBlocks₂₁ A.toMatrix := by + apply ext_getElem + intro i j + rw [Submatrix.getElem_toMatrix, getElem_toBlocks₂₁, Submatrix.getElem_toMatrix, + Submatrix.entry, Submatrix.entry] + simp only [Submatrix.toBlocks₂₁, Fin.val_castAdd, Fin.val_natAdd, Nat.add_assoc] + all_goals (have hi := i.isLt; have hj := j.isLt; split <;> split <;> (first | rfl | (exfalso; omega))) + +/-- Materializing the bottom-right quadrant view is `Matrix.toBlocks₂₂` of the parent. -/ +theorem toMatrix_toBlocks₂₂ [OfNat R 0] {h w : Nat} (A : Submatrix R (h + h) (w + w)) : + (Submatrix.toBlocks₂₂ A).toMatrix = toBlocks₂₂ A.toMatrix := by + apply ext_getElem + intro i j + rw [Submatrix.getElem_toMatrix, getElem_toBlocks₂₂, Submatrix.getElem_toMatrix, + Submatrix.entry, Submatrix.entry] + simp only [Submatrix.toBlocks₂₂, Fin.val_natAdd, Nat.add_assoc] + all_goals (have hi := i.isLt; have hj := j.isLt; split <;> split <;> (first | rfl | (exfalso; omega))) + /-- Configuration for `mulStrassen`: the recursion `cutoff` below which a block is handed to the base kernel, and the pluggable `baseMul` base kernel itself. Data only — `baseMul` is a bare function and the record carries no algebraic instances, @@ -73,19 +132,19 @@ cutoff of `96`. Measured by the Strassen bench driver (`bench/HexMatrix/Bench.lean`) on `Int` coefficients with GMP arithmetic, sweeping the cutoff `τ` against dimension `n` -on host `chungus2` (AMD EPYC 9455), Lean toolchain `4.32.0-rc1`, on the current -row-of-rows `Vector (Vector R m) n` backing. On that backing an extra Strassen -level below a `64×64` block loses to the naive base kernel (its coefficient- -multiplication saving is swamped by quadrant materialization and stride/cache -overhead), while a `128×128` block splits profitably (one Strassen level: -`≈ 90 ms` vs naive `≈ 97 ms`). Any cutoff in `(64, 128]` therefore recurses down -to a `64×64` naive leaf; that leaf class wins from the first splitting dimension -(`n = 128`) and stays within ~4% of the `128×128`-leaf class at `n = 512` (which -edges ahead there), so `96` is shipped as its representative, extending Strassen -to non-power-of-two blocks in `[96, 128)` as well. Per -`HexMatrix/SPEC/hex-matrix.md` § "Benchmarks" this crossover is representation- -dependent — the flat `Vector R (n*m)` backing (#8652) is expected to lower it and -will re-measure it against this same bench. -/ +on host `chungus2` (AMD EPYC 9455), Lean toolchain `4.32.0-rc1`. An extra +Strassen level below a `64×64` block loses to the naive base kernel, while a +`128×128` block splits profitably. Any cutoff in `(64, 128]` therefore recurses +down to a `64×64` naive leaf; that leaf class wins from the first splitting +dimension (`n = 128`) and stays within ~4% of the `128×128`-leaf class at +`n = 512` (which edges ahead there), so `96` is shipped as its representative, +extending Strassen to non-power-of-two blocks in `[96, 128)` as well. The value +has been re-measured twice per `HexMatrix/SPEC/hex-matrix.md` § "Benchmarks": +on the flat row-major backing with materialized quadrants and again on the +`Submatrix`-view recursion, both within noise of the original sweep (the +quadrant copies the views remove are `O(n²)` per level against the `O(n^2.81)` +multiply work, so they never dominated at benched sizes) — the crossover +stayed put and `96` stands. -/ @[expose] def strassenDefault [Mul R] [Add R] [OfNat R 0] : StrassenConfig R where cutoff := 96 @@ -99,54 +158,57 @@ theorem strassenDefault_valid [Mul R] [Add R] [OfNat R 0] : show mulImpl X Y = mul X Y rw [mul_eq_mulImpl] -/-- **Strassen-Winograd multiplication.** Recurses on the runtime dimensions, -following the Winograd schedule from `HexMatrix/SPEC/hex-matrix.md`. +/-- The internal Strassen-Winograd recursion over copy-free `Submatrix` **views**. +Recurses on the runtime dimensions following the Winograd schedule from +`HexMatrix/SPEC/hex-matrix.md`. Base case: when any of `n`, `m`, `k` is `≤ 1` or below `cfg.cutoff`, materialize -the current blocks and call `cfg.baseMul`. The `≤ 1` disjuncts are -config-independent, so `cutoff = 0` cannot defeat termination. - -Recursive step: pad each operand up to even dimensions (`h + h`, `w + w`, -`d + d` with `h := (n+1)/2` etc.), split into 2×2 blocks with no dimension cast, -run the fifteen-addition Winograd schedule with seven recursive products, assemble -with `fromBlocks`, and crop back to `n × k`. Termination is well-founded on -`n + m + k`: the recursion fires only when `n, m, k ≥ 2`, and each halved -dimension is then strictly smaller. -/ +the current view blocks (`toMatrix`) and call `cfg.baseMul` — the only leaf +allocation. The `≤ 1` disjuncts are config-independent, so `cutoff = 0` cannot +defeat termination. + +Recursive step: widen each operand view to even dimensions (`h + h`, `w + w`, +`d + d` with `h := (n+1)/2` etc.) — a zero-fill reshape with no copy — split into +2×2 quadrant **views** (offset arithmetic, no copy), materialize only the fifteen +`Sᵢ`/`Tᵢ`/`Uᵢ` operand sums and the seven recursive products, assemble with +`fromBlocks`, and crop back to `n × k`. Termination is well-founded on `n + m + k`: +the recursion fires only when `n, m, k ≥ 2`, and each halved dimension is then +strictly smaller. -/ @[expose] -def mulStrassen {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] - (cfg : StrassenConfig R) {n m k : Nat} (M : Matrix R n m) (N : Matrix R m k) : +def mulStrassenView {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] + (cfg : StrassenConfig R) {n m k : Nat} (A : Submatrix R n m) (B : Submatrix R m k) : Matrix R n k := if n ≤ 1 ∨ m ≤ 1 ∨ k ≤ 1 ∨ n < cfg.cutoff ∨ m < cfg.cutoff ∨ k < cfg.cutoff then - cfg.baseMul M N + cfg.baseMul A.toMatrix B.toMatrix else let h := (n + 1) / 2 let w := (m + 1) / 2 let d := (k + 1) / 2 - let Mp := pad M (h + h) (w + w) - let Np := pad N (w + w) (d + d) - let A₁₁ := toBlocks₁₁ Mp - let A₁₂ := toBlocks₁₂ Mp - let A₂₁ := toBlocks₂₁ Mp - let A₂₂ := toBlocks₂₂ Mp - let B₁₁ := toBlocks₁₁ Np - let B₁₂ := toBlocks₁₂ Np - let B₂₁ := toBlocks₂₁ Np - let B₂₂ := toBlocks₂₂ Np - let S₁ := A₂₁ + A₂₂ - let S₂ := S₁ - A₁₁ - let S₃ := A₁₁ - A₂₁ - let S₄ := A₁₂ - S₂ - let T₁ := B₁₂ - B₁₁ - let T₂ := B₂₂ - T₁ - let T₃ := B₂₂ - B₁₂ - let T₄ := T₂ - B₂₁ - let P₁ := mulStrassen cfg A₁₁ B₁₁ - let P₂ := mulStrassen cfg A₁₂ B₂₁ - let P₃ := mulStrassen cfg S₄ B₂₂ - let P₄ := mulStrassen cfg A₂₂ T₄ - let P₅ := mulStrassen cfg S₁ T₁ - let P₆ := mulStrassen cfg S₂ T₂ - let P₇ := mulStrassen cfg S₃ T₃ + let Ap := A.pad (h + h) (w + w) (by omega) (by omega) + let Bp := B.pad (w + w) (d + d) (by omega) (by omega) + let A₁₁ := Ap.toBlocks₁₁ + let A₁₂ := Ap.toBlocks₁₂ + let A₂₁ := Ap.toBlocks₂₁ + let A₂₂ := Ap.toBlocks₂₂ + let B₁₁ := Bp.toBlocks₁₁ + let B₁₂ := Bp.toBlocks₁₂ + let B₂₁ := Bp.toBlocks₂₁ + let B₂₂ := Bp.toBlocks₂₂ + let S₁ := A₂₁.add A₂₂ + let S₂ := S₁.sub A₁₁ + let S₃ := A₁₁.sub A₂₁ + let S₄ := A₁₂.sub S₂ + let T₁ := B₁₂.sub B₁₁ + let T₂ := B₂₂.sub T₁ + let T₃ := B₂₂.sub B₁₂ + let T₄ := T₂.sub B₂₁ + let P₁ := mulStrassenView cfg A₁₁ B₁₁ + let P₂ := mulStrassenView cfg A₁₂ B₂₁ + let P₃ := mulStrassenView cfg S₄ B₂₂ + let P₄ := mulStrassenView cfg A₂₂ T₄ + let P₅ := mulStrassenView cfg S₁ T₁ + let P₆ := mulStrassenView cfg S₂ T₂ + let P₇ := mulStrassenView cfg S₃ T₃ let U₁ := P₁ + P₂ let U₂ := P₁ + P₆ let U₃ := U₂ + P₇ @@ -158,36 +220,76 @@ def mulStrassen {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] termination_by n + m + k decreasing_by all_goals (simp_wf; omega) -/-- **Correctness of Strassen-Winograd multiplication.** For every valid -configuration, `mulStrassen` computes the same matrix as the reference `mul`. -/ -theorem mulStrassen_eq_mul [Lean.Grind.Ring R] +/-- **Strassen-Winograd multiplication.** The public entry point wraps the operands +as full-matrix `Submatrix` views and runs the copy-free view recursion +`mulStrassenView`; the quadrant splitting inside allocates nothing (see that +def and `HexMatrix/SPEC/hex-matrix.md` § "Avoiding sub-block copies"). -/ +@[expose] +def mulStrassen {R : Type u} [Mul R] [Add R] [Sub R] [OfNat R 0] + (cfg : StrassenConfig R) {n m k : Nat} (M : Matrix R n m) (N : Matrix R m k) : + Matrix R n k := + mulStrassenView cfg (Submatrix.ofMatrix M) (Submatrix.ofMatrix N) + +/-- The view recursion computes the same matrix as the reference `mul` of the +materialized operands, for every valid configuration. Proved by functional +induction over `mulStrassenView`, reducing each quadrant view to its `toBlocks` +materialization (`toMatrix_toBlocks…`, `toMatrix_pad_view`) and composing the +three wave-1 lemmas exactly as the `Matrix`-level recursion did. -/ +theorem mulStrassenView_eq_mul [Lean.Grind.Ring R] (cfg : StrassenConfig R) (hcfg : cfg.Valid) - (M : Matrix R n m) (N : Matrix R m k) : - mulStrassen cfg M N = mul M N := by - fun_induction mulStrassen cfg M N with - | case1 n m k M N hbase => exact hcfg M N - | case2 n m k M N hbase h w d Mp Np + (A : Submatrix R n m) (B : Submatrix R m k) : + mulStrassenView cfg A B = mul A.toMatrix B.toMatrix := by + fun_induction mulStrassenView cfg A B with + | case1 n m k A B hbase => exact hcfg A.toMatrix B.toMatrix + | case2 n m k A B hbase h w d Ap Bp A₁₁ A₁₂ A₂₁ A₂₂ B₁₁ B₁₂ B₂₁ B₂₂ S₁ S₂ S₃ S₄ T₁ T₂ T₃ T₄ P₁ P₂ P₃ P₄ P₅ P₆ P₇ U₁ U₂ U₃ U₄ U₅ U₆ U₇ hP₁ hP₂ hP₃ hP₄ hP₅ hP₆ hP₇ => - let win : Winograd A₁₁ A₁₂ A₂₁ A₂₂ B₁₁ B₁₂ B₂₁ B₂₂ := - { S₁, S₂, S₃, S₄, T₁, T₂, T₃, T₄, P₁, P₂, P₃, P₄, P₅, P₆, P₇, + let win : Winograd A₁₁.toMatrix A₁₂.toMatrix A₂₁.toMatrix A₂₂.toMatrix + B₁₁.toMatrix B₁₂.toMatrix B₂₁.toMatrix B₂₂.toMatrix := + { S₁ := S₁.toMatrix, S₂ := S₂.toMatrix, S₃ := S₃.toMatrix, S₄ := S₄.toMatrix, + T₁ := T₁.toMatrix, T₂ := T₂.toMatrix, T₃ := T₃.toMatrix, T₄ := T₄.toMatrix, + P₁, P₂, P₃, P₄, P₅, P₆, P₇, U₁, U₂, U₃, U₄, U₅, U₆, U₇, - hS₁ := rfl, hS₂ := rfl, hS₃ := rfl, hS₄ := rfl, - hT₁ := rfl, hT₂ := rfl, hT₃ := rfl, hT₄ := rfl, + hS₁ := Submatrix.toMatrix_add A₂₁ A₂₂, hS₂ := Submatrix.toMatrix_sub S₁ A₁₁, + hS₃ := Submatrix.toMatrix_sub A₁₁ A₂₁, hS₄ := Submatrix.toMatrix_sub A₁₂ S₂, + hT₁ := Submatrix.toMatrix_sub B₁₂ B₁₁, hT₂ := Submatrix.toMatrix_sub B₂₂ T₁, + hT₃ := Submatrix.toMatrix_sub B₂₂ B₁₂, hT₄ := Submatrix.toMatrix_sub T₂ B₂₁, hP₁, hP₂, hP₃, hP₄, hP₅, hP₆, hP₇, hU₁ := rfl, hU₂ := rfl, hU₃ := rfl, hU₄ := rfl, hU₅ := rfl, hU₆ := rfl, hU₇ := rfl } - have e11 : U₁ = A₁₁ * B₁₁ + A₁₂ * B₂₁ := win.c11 - have e12 : U₅ = A₁₁ * B₁₂ + A₁₂ * B₂₂ := win.c12 - have e21 : U₆ = A₂₁ * B₁₁ + A₂₂ * B₂₁ := win.c21 - have e22 : U₇ = A₂₁ * B₁₂ + A₂₂ * B₂₂ := win.c22 - have hAb : fromBlocks A₁₁ A₁₂ A₂₁ A₂₂ = Mp := fromBlocks_toBlocks Mp - have hBb : fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = Np := fromBlocks_toBlocks Np - rw [e11, e12, e21, e22, ← fromBlocks_mul_fromBlocks, hAb, hBb] - exact takeCols_takeRows_mul_pad M N (h + h) (w + w) (d + d) (by omega) (by omega) (by omega) + have e11 : U₁ = A₁₁.toMatrix * B₁₁.toMatrix + A₁₂.toMatrix * B₂₁.toMatrix := win.c11 + have e12 : U₅ = A₁₁.toMatrix * B₁₂.toMatrix + A₁₂.toMatrix * B₂₂.toMatrix := win.c12 + have e21 : U₆ = A₂₁.toMatrix * B₁₁.toMatrix + A₂₂.toMatrix * B₂₁.toMatrix := win.c21 + have e22 : U₇ = A₂₁.toMatrix * B₁₂.toMatrix + A₂₂.toMatrix * B₂₂.toMatrix := win.c22 + have hAb : fromBlocks A₁₁.toMatrix A₁₂.toMatrix A₂₁.toMatrix A₂₂.toMatrix = Ap.toMatrix := by + show fromBlocks (Ap.toBlocks₁₁).toMatrix (Ap.toBlocks₁₂).toMatrix + (Ap.toBlocks₂₁).toMatrix (Ap.toBlocks₂₂).toMatrix = Ap.toMatrix + rw [toMatrix_toBlocks₁₁, toMatrix_toBlocks₁₂, toMatrix_toBlocks₂₁, toMatrix_toBlocks₂₂, + fromBlocks_toBlocks] + have hBb : fromBlocks B₁₁.toMatrix B₁₂.toMatrix B₂₁.toMatrix B₂₂.toMatrix = Bp.toMatrix := by + show fromBlocks (Bp.toBlocks₁₁).toMatrix (Bp.toBlocks₁₂).toMatrix + (Bp.toBlocks₂₁).toMatrix (Bp.toBlocks₂₂).toMatrix = Bp.toMatrix + rw [toMatrix_toBlocks₁₁, toMatrix_toBlocks₁₂, toMatrix_toBlocks₂₁, toMatrix_toBlocks₂₂, + fromBlocks_toBlocks] + have hApM : Ap.toMatrix = pad A.toMatrix (h + h) (w + w) := + toMatrix_pad_view A (h + h) (w + w) (by omega) (by omega) + have hBpM : Bp.toMatrix = pad B.toMatrix (w + w) (d + d) := + toMatrix_pad_view B (w + w) (d + d) (by omega) (by omega) + rw [e11, e12, e21, e22, ← fromBlocks_mul_fromBlocks, hAb, hBb, hApM, hBpM] + exact takeCols_takeRows_mul_pad A.toMatrix B.toMatrix (h + h) (w + w) (d + d) + (by omega) (by omega) (by omega) + +/-- **Correctness of Strassen-Winograd multiplication.** For every valid +configuration, `mulStrassen` computes the same matrix as the reference `mul`. -/ +theorem mulStrassen_eq_mul [Lean.Grind.Ring R] + (cfg : StrassenConfig R) (hcfg : cfg.Valid) + (M : Matrix R n m) (N : Matrix R m k) : + mulStrassen cfg M N = mul M N := by + show mulStrassenView cfg (Submatrix.ofMatrix M) (Submatrix.ofMatrix N) = mul M N + rw [mulStrassenView_eq_mul cfg hcfg, Submatrix.toMatrix_ofMatrix, Submatrix.toMatrix_ofMatrix] end Matrix diff --git a/HexMatrix/Submatrix.lean b/HexMatrix/Submatrix.lean index 8fb5830a9..2e8e0c1ea 100644 --- a/HexMatrix/Submatrix.lean +++ b/HexMatrix/Submatrix.lean @@ -127,4 +127,179 @@ def takeCols (M : Matrix R n m) (k : Nat) (hk : k ≤ m) : Matrix R n k := end Matrix +/-! ### Copy-free submatrix views + +A `Submatrix R rows cols` is a **view** into a backing `Matrix R N M`: a row/column +offset plus the real-data extent, with the logical `rows × cols` shape carried as +type indices. Reading entry `(i, j)` is pure offset arithmetic into the shared flat +buffer (`base[(r0 + i, c0 + j)]`) when that position holds real data, and `0` +otherwise — the zero-fill lets a view stand for a matrix logically padded past its +data without copying. The backing dims `N, M` never change through a recursion, so +`r0 + i < rhi` (the real-row bound, a prefix of the logical rows) is the exact +real-vs-pad test at every nesting depth. Quadrant-of-a-view is a view (offset +arithmetic, no copy); this is the recursion surface `mulStrassen` runs over +(`HexMatrix/Strassen.lean`). See `HexMatrix/SPEC/hex-matrix.md` § "Avoiding +sub-block copies". -/ + +/-- A copy-free view of a `rows × cols` block, possibly zero-padded past its +real-data extent, into a shared backing `Matrix R N M`. Reading `(i, j)` returns +`base[(r0 + i, c0 + j)]` when `r0 + i < rhi ∧ c0 + j < chi` (real data) and `0` +otherwise (pad). The invariants pin `[r0, rhi) × [c0, chi)` inside the backing and +inside the logical block, so the real data is a prefix of each axis. -/ +structure Submatrix (R : Type u) (rows cols : Nat) where + /-- Backing row count. -/ N : Nat + /-- Backing column count. -/ M : Nat + /-- Shared backing buffer; sub-views alias it, never copy it. -/ base : Hex.Matrix R N M + /-- Row offset into the backing. -/ r0 : Nat + /-- Column offset into the backing. -/ c0 : Nat + /-- One past the last real-data row (backing coordinate). -/ rhi : Nat + /-- One past the last real-data column (backing coordinate). -/ chi : Nat + /-- Real rows stay inside the backing. -/ hrN : rhi ≤ N + /-- Real columns stay inside the backing. -/ hcM : chi ≤ M + /-- Real rows are a prefix of the logical rows. -/ hrR : rhi ≤ r0 + rows + /-- Real columns are a prefix of the logical columns. -/ hcC : chi ≤ c0 + cols + +namespace Submatrix + +variable {R : Type u} {rows cols : Nat} + +/-- Read entry `(i, j)` of a view: the flat backing read at `(r0 + i, c0 + j)` +inside the real-data window, `0` in the zero-pad fringe. -/ +@[expose] +def entry [OfNat R 0] (A : Submatrix R rows cols) (i : Fin rows) (j : Fin cols) : R := + if h : A.r0 + i.val < A.rhi ∧ A.c0 + j.val < A.chi then + A.base[(A.r0 + i.val, A.c0 + j.val)]'(by + obtain ⟨h1, h2⟩ := h; exact ⟨by have := A.hrN; omega, by have := A.hcM; omega⟩) + else 0 + +/-- Materialize a view into a genuine `Matrix` (a copy of the block, with the +zero-pad fringe filled in). This is the leaf/operand allocation the recursion +pays; interior quadrants stay views. -/ +@[expose] +def toMatrix [OfNat R 0] (A : Submatrix R rows cols) : Matrix R rows cols := + Matrix.ofFn fun i j => A.entry i j + +/-- Entry access of a materialized view is the view read. -/ +@[simp, grind =] theorem getElem_toMatrix [OfNat R 0] (A : Submatrix R rows cols) + (i : Fin rows) (j : Fin cols) : (A.toMatrix)[i][j] = A.entry i j := by + rw [toMatrix, Matrix.getElem_ofFn] + +/-- The full-matrix view of a `Matrix`: offset `0`, real extent the whole matrix. -/ +@[expose] +def ofMatrix (Mx : Matrix R n m) : Submatrix R n m where + N := n; M := m; base := Mx; r0 := 0; c0 := 0; rhi := n; chi := m + hrN := Nat.le_refl _ + hcM := Nat.le_refl _ + hrR := by omega + hcC := by omega + +/-- Reading the full-matrix view is reading the matrix. -/ +@[simp, grind =] theorem entry_ofMatrix [OfNat R 0] (Mx : Matrix R n m) (i : Fin n) (j : Fin m) : + (ofMatrix Mx).entry i j = Mx[i][j] := by + rw [entry, ofMatrix] + rw [dif_pos (⟨by omega, by omega⟩ : (0 : Nat) + i.val < n ∧ (0 : Nat) + j.val < m)] + simp [Matrix.getElem_pair_nat] + +/-- Materializing the full-matrix view returns the matrix. -/ +@[simp, grind =] theorem toMatrix_ofMatrix [OfNat R 0] (Mx : Matrix R n m) : + (ofMatrix Mx).toMatrix = Mx := by + apply Matrix.ext_getElem + intro i j + rw [getElem_toMatrix, entry_ofMatrix] + +/-- Widen a view's logical shape to `n' × m'` (`n ≤ n'`, `m ≤ m'`) without copying: +the real-data window is unchanged, so the new fringe reads `0`. This is the +zero-padding the Strassen recursion applies before splitting. -/ +@[expose] +def pad (A : Submatrix R n m) (n' m' : Nat) (hn : n ≤ n') (hm : m ≤ m') : Submatrix R n' m' where + N := A.N; M := A.M; base := A.base; r0 := A.r0; c0 := A.c0; rhi := A.rhi; chi := A.chi + hrN := A.hrN; hcM := A.hcM + hrR := by have := A.hrR; omega + hcC := by have := A.hcC; omega + +/-- Reading a widened view agrees with the source view inside the source shape. -/ +@[grind =] theorem entry_pad [OfNat R 0] (A : Submatrix R n m) (n' m' : Nat) + (hn : n ≤ n') (hm : m ≤ m') (i : Fin n') (j : Fin m') : + (A.pad n' m' hn hm).entry i j = + if h : i.val < n ∧ j.val < m then A.entry ⟨i.val, h.1⟩ ⟨j.val, h.2⟩ else 0 := by + by_cases hin : i.val < n ∧ j.val < m + · rw [dif_pos hin]; rfl + · rw [dif_neg hin, entry] + apply dif_neg + simp only [pad] + intro hd + have h1 := A.hrR + have h2 := A.hcC + omega + +/-- Top-left `h × w` quadrant of an `(h+h) × (w+w)` view: same offset, real extent +capped at the block boundary. No copy. -/ +@[expose] +def toBlocks₁₁ (A : Submatrix R (h + h) (w + w)) : Submatrix R h w where + N := A.N; M := A.M; base := A.base; r0 := A.r0; c0 := A.c0 + rhi := min A.rhi (A.r0 + h); chi := min A.chi (A.c0 + w) + hrN := by have := A.hrN; omega + hcM := by have := A.hcM; omega + hrR := by omega + hcC := by omega + +/-- Top-right `h × w` quadrant of an `(h+h) × (w+w)` view. No copy. -/ +@[expose] +def toBlocks₁₂ (A : Submatrix R (h + h) (w + w)) : Submatrix R h w where + N := A.N; M := A.M; base := A.base; r0 := A.r0; c0 := A.c0 + w + rhi := min A.rhi (A.r0 + h); chi := A.chi + hrN := by have := A.hrN; omega + hcM := A.hcM + hrR := by omega + hcC := by have := A.hcC; omega + +/-- Bottom-left `h × w` quadrant of an `(h+h) × (w+w)` view. No copy. -/ +@[expose] +def toBlocks₂₁ (A : Submatrix R (h + h) (w + w)) : Submatrix R h w where + N := A.N; M := A.M; base := A.base; r0 := A.r0 + h; c0 := A.c0 + rhi := A.rhi; chi := min A.chi (A.c0 + w) + hrN := A.hrN + hcM := by have := A.hcM; omega + hrR := by have := A.hrR; omega + hcC := by omega + +/-- Bottom-right `h × w` quadrant of an `(h+h) × (w+w)` view. No copy. -/ +@[expose] +def toBlocks₂₂ (A : Submatrix R (h + h) (w + w)) : Submatrix R h w where + N := A.N; M := A.M; base := A.base; r0 := A.r0 + h; c0 := A.c0 + w + rhi := A.rhi; chi := A.chi + hrN := A.hrN + hcM := A.hcM + hrR := by have := A.hrR; omega + hcC := by have := A.hcC; omega + +/-- Entrywise sum of two views, materialized into a fresh matrix (an operand-sum +allocation). -/ +@[expose] +def add [Add R] [OfNat R 0] (A B : Submatrix R rows cols) : Submatrix R rows cols := + ofMatrix (Matrix.ofFn fun i j => A.entry i j + B.entry i j) + +/-- Entrywise difference of two views, materialized into a fresh matrix. -/ +@[expose] +def sub [Sub R] [OfNat R 0] (A B : Submatrix R rows cols) : Submatrix R rows cols := + ofMatrix (Matrix.ofFn fun i j => A.entry i j - B.entry i j) + +/-- Materializing a view sum is the matrix sum of the materializations. -/ +@[simp, grind =] theorem toMatrix_add [Add R] [OfNat R 0] (A B : Submatrix R rows cols) : + (A.add B).toMatrix = A.toMatrix + B.toMatrix := by + apply Matrix.ext_getElem + intro i j + rw [add, toMatrix_ofMatrix, Matrix.getElem_add, Matrix.getElem_ofFn, getElem_toMatrix, + getElem_toMatrix] + +/-- Materializing a view difference is the matrix difference of the materializations. -/ +@[simp, grind =] theorem toMatrix_sub [Sub R] [OfNat R 0] (A B : Submatrix R rows cols) : + (A.sub B).toMatrix = A.toMatrix - B.toMatrix := by + apply Matrix.ext_getElem + intro i j + rw [sub, toMatrix_ofMatrix, Matrix.getElem_sub, Matrix.getElem_ofFn, getElem_toMatrix, + getElem_toMatrix] + +end Submatrix + end Hex diff --git a/reports/bench-results/hex-matrix-mul-scaling-flat-view-chungus2.json b/reports/bench-results/hex-matrix-mul-scaling-flat-view-chungus2.json new file mode 100644 index 000000000..10cb58625 --- /dev/null +++ b/reports/bench-results/hex-matrix-mul-scaling-flat-view-chungus2.json @@ -0,0 +1,532 @@ +{"results": + [{"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.029099, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 12242736.96875, + "median_per_call_nanos": 12377207.8125, + "max_per_call_nanos": 12602898.25}, + {"relative_spread": 0.007566, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 97149611.25, + "median_per_call_nanos": 97691499.5, + "max_per_call_nanos": 97888699.25}, + {"relative_spread": 0.013173, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 765938745, + "median_per_call_nanos": 775903394, + "max_per_call_nanos": 776160064}, + {"relative_spread": 0.01057, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 6170358413, + "median_per_call_nanos": 6210713334, + "max_per_call_nanos": 6236008114}, + {"relative_spread": 0.020267, + "param": 1024, + "ok_count": 3, + "min_per_call_nanos": 49441875848, + "median_per_call_nanos": 49879310689, + "max_per_call_nanos": 50452779161}], + "spawn_floor_nanos": 23376738, + "slope": -0.001121, + "ratios": + [[64, 47.215301], + [128, 46.582937], + [256, 46.247446], + [512, 46.27342], + [1024, 46.453728]], + "points": + [{"trial_index": 0, + "total_nanos": 403292744, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12602898.25, + "peak_rss_kb": 60816, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 391767583, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12242736.96875, + "peak_rss_kb": 61416, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 396070650, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12377207.8125, + "peak_rss_kb": 60440, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 390765998, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 97691499.5, + "peak_rss_kb": 62364, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 388598445, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 97149611.25, + "peak_rss_kb": 61660, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 391554797, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 97888699.25, + "peak_rss_kb": 61880, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 775903394, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 775903394, + "peak_rss_kb": 66948, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 765938745, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 765938745, + "peak_rss_kb": 67384, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 776160064, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 776160064, + "peak_rss_kb": 67744, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 6210713334, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6210713334, + "peak_rss_kb": 88972, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 6170358413, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6170358413, + "peak_rss_kb": 87528, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 6236008114, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6236008114, + "peak_rss_kb": 88248, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 49441875848, + "status": "ok", + "result_hash": "0x1ffbbcd11f386b8e", + "per_call_nanos": 49441875848, + "peak_rss_kb": 169472, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 50452779161, + "status": "ok", + "result_hash": "0x1ffbbcd11f386b8e", + "per_call_nanos": 50452779161, + "peak_rss_kb": 168708, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 49879310689, + "status": "ok", + "result_hash": "0x1ffbbcd11f386b8e", + "per_call_nanos": 49879310689, + "peak_rss_kb": 167952, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runSquareMulChecksum", + "env": + {"timestamp_unix_ms": 1783778603754, + "timestamp_iso": "2026-07-11T14:03:23Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512, 1024], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 1024, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 120, + "cache_mode": "warm"}, + "complexity_formula": "n * n * n", + "c_min": 46.247446, + "c_max": 46.582937, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.011384, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 12319641.875, + "median_per_call_nanos": 12363093.78125, + "max_per_call_nanos": 12460378.28125}, + {"relative_spread": 0.00582, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 90797466.75, + "median_per_call_nanos": 91225548.5, + "max_per_call_nanos": 91328423.5}, + {"relative_spread": 0.020965, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 614170834, + "median_per_call_nanos": 614767369, + "max_per_call_nanos": 627059556}, + {"relative_spread": 0.026659, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 4829547412, + "median_per_call_nanos": 4874164171, + "max_per_call_nanos": 4959487131}, + {"relative_spread": 0.057656, + "param": 1024, + "ok_count": 3, + "min_per_call_nanos": 40486007204, + "median_per_call_nanos": 41439722536, + "max_per_call_nanos": 42875240896}], + "spawn_floor_nanos": 22495971, + "slope": 0.139558, + "ratios": + [[64, 105.084563], + [128, 110.772053], + [256, 106.64156], + [512, 120.786332], + [1024, 146.702136]], + "points": + [{"trial_index": 0, + "total_nanos": 394228540, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12319641.875, + "peak_rss_kb": 61168, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 395619001, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12363093.78125, + "peak_rss_kb": 60540, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 398732105, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12460378.28125, + "peak_rss_kb": 61304, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 365313694, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 91328423.5, + "peak_rss_kb": 63372, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 364902194, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 91225548.5, + "peak_rss_kb": 63036, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 363189867, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 90797466.75, + "peak_rss_kb": 62828, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 627059556, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 627059556, + "peak_rss_kb": 71536, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 614767369, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 614767369, + "peak_rss_kb": 70628, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 614170834, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 614170834, + "peak_rss_kb": 70656, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 4829547412, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4829547412, + "peak_rss_kb": 105704, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 4959487131, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4959487131, + "peak_rss_kb": 103468, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 4874164171, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4874164171, + "peak_rss_kb": 102676, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 41439722536, + "status": "ok", + "result_hash": "0x1ffbbcd11f386b8e", + "per_call_nanos": 41439722536, + "peak_rss_kb": 221032, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 40486007204, + "status": "ok", + "result_hash": "0x1ffbbcd11f386b8e", + "per_call_nanos": 40486007204, + "peak_rss_kb": 220128, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 42875240896, + "status": "ok", + "result_hash": "0x1ffbbcd11f386b8e", + "per_call_nanos": 42875240896, + "peak_rss_kb": 222736, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runSquareMulStrassenChecksum", + "env": + {"timestamp_unix_ms": 1783778778090, + "timestamp_iso": "2026-07-11T14:06:18Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512, 1024], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 1024, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 120, + "cache_mode": "warm"}, + "complexity_formula": "7 ^ Nat.log2 n", + "c_min": 106.64156, + "c_max": 146.702136, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1783778603754, + "timestamp_iso": "2026-07-11T14:03:23Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}} diff --git a/reports/bench-results/hex-matrix-strassen-cutoff-view-chungus2.json b/reports/bench-results/hex-matrix-strassen-cutoff-view-chungus2.json new file mode 100644 index 000000000..c11c2e085 --- /dev/null +++ b/reports/bench-results/hex-matrix-strassen-cutoff-view-chungus2.json @@ -0,0 +1,1320 @@ +{"results": + [{"verdict_dropped_leading": 0, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.008343, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 12211633.90625, + "median_per_call_nanos": 12240226.5625, + "max_per_call_nanos": 12313758.34375}, + {"relative_spread": 0.005269, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 96732828.5, + "median_per_call_nanos": 96857515.75, + "max_per_call_nanos": 97243214.75}, + {"relative_spread": 0.029797, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 767184025, + "median_per_call_nanos": 775236745, + "max_per_call_nanos": 790283548}, + {"relative_spread": 0.055885, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 6217424643, + "median_per_call_nanos": 6246229530, + "max_per_call_nanos": 6566496293}], + "spawn_floor_nanos": 21501014, + "slope": -0.001366, + "ratios": + [[64, 46.692759], [128, 46.185263], [256, 46.207711], [512, 46.538037]], + "points": + [{"trial_index": 0, + "total_nanos": 390772285, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12211633.90625, + "peak_rss_kb": 60604, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 391687250, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12240226.5625, + "peak_rss_kb": 60540, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 394040267, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12313758.34375, + "peak_rss_kb": 61136, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 386931314, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 96732828.5, + "peak_rss_kb": 61348, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 388972859, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 97243214.75, + "peak_rss_kb": 61688, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 387430063, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 96857515.75, + "peak_rss_kb": 61664, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 775236745, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 775236745, + "peak_rss_kb": 67552, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 790283548, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 790283548, + "peak_rss_kb": 67452, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 767184025, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 767184025, + "peak_rss_kb": 67152, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 6217424643, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6217424643, + "peak_rss_kb": 88464, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 6566496293, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6566496293, + "peak_rss_kb": 88556, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 6246229530, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6246229530, + "peak_rss_kb": 88504, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 0, + "status": "killed_at_cap", + "result_hash": null, + "per_call_nanos": 0, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 0, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 0, + "status": "killed_at_cap", + "result_hash": null, + "per_call_nanos": 0, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 0, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 0, + "status": "killed_at_cap", + "result_hash": null, + "per_call_nanos": 0, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 0, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runSquareMulChecksum", + "env": + {"timestamp_unix_ms": 1783766382300, + "timestamp_iso": "2026-07-11T10:39:42Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512, 1024], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 1024, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 40, + "cache_mode": "warm"}, + "complexity_formula": "n * n * n", + "c_min": 46.185263, + "c_max": 46.692759, + "budget_truncated": false, + "advisories": ["truncated_at_cap"]}, + {"verdict_dropped_leading": 0, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.016624, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 13299042.375, + "median_per_call_nanos": 13339382.125, + "max_per_call_nanos": 13520794.96875}, + {"relative_spread": 0.061296, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 112196508.25, + "median_per_call_nanos": 112289628.75, + "max_per_call_nanos": 119079415.75}, + {"relative_spread": 0.006055, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 797147031, + "median_per_call_nanos": 801853133, + "max_per_call_nanos": 802002564}, + {"relative_spread": 0.014877, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 6080192471, + "median_per_call_nanos": 6108016868, + "max_per_call_nanos": 6171062817}], + "spawn_floor_nanos": 22246459, + "slope": 0.127917, + "ratios": + [[64, 113.382877], [128, 136.349442], [256, 139.094677], [512, 151.362352]], + "points": + [{"trial_index": 0, + "total_nanos": 425569356, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 13299042.375, + "peak_rss_kb": 61056, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 426860228, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 13339382.125, + "peak_rss_kb": 61296, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 432665439, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 13520794.96875, + "peak_rss_kb": 61932, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 449158515, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 112289628.75, + "peak_rss_kb": 62584, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 476317663, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 119079415.75, + "peak_rss_kb": 62812, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 448786033, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 112196508.25, + "peak_rss_kb": 63416, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 802002564, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 802002564, + "peak_rss_kb": 71084, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 801853133, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 801853133, + "peak_rss_kb": 71076, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 797147031, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 797147031, + "peak_rss_kb": 71124, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 6171062817, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6171062817, + "peak_rss_kb": 101976, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 6080192471, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6080192471, + "peak_rss_kb": 100420, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 6108016868, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 6108016868, + "peak_rss_kb": 101992, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runStrassenCut32", + "env": + {"timestamp_unix_ms": 1783766527377, + "timestamp_iso": "2026-07-11T10:42:07Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 512, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 40, + "cache_mode": "warm"}, + "complexity_formula": "7 ^ Nat.log2 n", + "c_min": 113.382877, + "c_max": 151.362352, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 0, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0.006654, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 11076333.09375, + "median_per_call_nanos": 11090464.03125, + "max_per_call_nanos": 11150126.78125}, + {"relative_spread": 0.002332, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 93230148.75, + "median_per_call_nanos": 93391149.75, + "max_per_call_nanos": 93447948.75}, + {"relative_spread": 0.002541, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 667370220, + "median_per_call_nanos": 667764845, + "max_per_call_nanos": 669066934}, + {"relative_spread": 0.021396, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 5276978651, + "median_per_call_nanos": 5357132497, + "max_per_call_nanos": 5391598814}], + "spawn_floor_nanos": 22368269, + "slope": 0.151243, + "ratios": + [[64, 94.267389], [128, 113.401668], [256, 115.834848], [512, 132.754737]], + "points": + [{"trial_index": 0, + "total_nanos": 356804057, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 11150126.78125, + "peak_rss_kb": 61420, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 354894849, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 11090464.03125, + "peak_rss_kb": 61140, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 354442659, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 11076333.09375, + "peak_rss_kb": 61308, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 373564599, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 93391149.75, + "peak_rss_kb": 63008, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 372920595, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 93230148.75, + "peak_rss_kb": 63944, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 373791795, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 93447948.75, + "peak_rss_kb": 63608, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 667764845, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 667764845, + "peak_rss_kb": 71156, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 669066934, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 669066934, + "peak_rss_kb": 70596, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 667370220, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 667370220, + "peak_rss_kb": 71352, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 5276978651, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 5276978651, + "peak_rss_kb": 104396, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 5357132497, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 5357132497, + "peak_rss_kb": 104876, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 5391598814, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 5391598814, + "peak_rss_kb": 105044, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runStrassenCut64", + "env": + {"timestamp_unix_ms": 1783766551645, + "timestamp_iso": "2026-07-11T10:42:31Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 512, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 40, + "cache_mode": "warm"}, + "complexity_formula": "7 ^ Nat.log2 n", + "c_min": 94.267389, + "c_max": 132.754737, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 0, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.009083, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 12318572.90625, + "median_per_call_nanos": 12393602.53125, + "max_per_call_nanos": 12431139.6875}, + {"relative_spread": 0.01031, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 90499533.5, + "median_per_call_nanos": 90676265.25, + "max_per_call_nanos": 91434375.75}, + {"relative_spread": 0.020882, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 608302709, + "median_per_call_nanos": 610388209, + "max_per_call_nanos": 621048773}, + {"relative_spread": 0.033101, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 4774352891, + "median_per_call_nanos": 4866363099, + "max_per_call_nanos": 4935432665}], + "spawn_floor_nanos": 22922892, + "slope": 0.052869, + "ratios": + [[64, 105.343883], [128, 110.105077], [256, 105.881922], [512, 120.593014]], + "points": + [{"trial_index": 0, + "total_nanos": 394194333, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12318572.90625, + "peak_rss_kb": 61096, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 396595281, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12393602.53125, + "peak_rss_kb": 61284, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 397796470, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12431139.6875, + "peak_rss_kb": 61256, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 362705061, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 90676265.25, + "peak_rss_kb": 63344, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 365737503, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 91434375.75, + "peak_rss_kb": 63180, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 361998134, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 90499533.5, + "peak_rss_kb": 63000, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 621048773, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 621048773, + "peak_rss_kb": 71520, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 608302709, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 608302709, + "peak_rss_kb": 71484, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 610388209, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 610388209, + "peak_rss_kb": 71672, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 4866363099, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4866363099, + "peak_rss_kb": 103828, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 4774352891, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4774352891, + "peak_rss_kb": 102968, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 4935432665, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4935432665, + "peak_rss_kb": 102548, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runStrassenCut96", + "env": + {"timestamp_unix_ms": 1783766572634, + "timestamp_iso": "2026-07-11T10:42:52Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 512, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 40, + "cache_mode": "warm"}, + "complexity_formula": "7 ^ Nat.log2 n", + "c_min": 105.343883, + "c_max": 120.593014, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 0, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.054409, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 12379979.25, + "median_per_call_nanos": 12424191.3125, + "max_per_call_nanos": 13055965.4375}, + {"relative_spread": 0.009968, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 91461801.75, + "median_per_call_nanos": 91705868.25, + "max_per_call_nanos": 92375921}, + {"relative_spread": 0.085349, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 608808890, + "median_per_call_nanos": 613664785, + "max_per_call_nanos": 661184669}, + {"relative_spread": 0.044937, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 4847035107, + "median_per_call_nanos": 4929966953, + "max_per_call_nanos": 5068575349}], + "spawn_floor_nanos": 23224328, + "slope": 0.056566, + "ratios": + [[64, 105.603884], [128, 111.355288], [256, 106.450298], [512, 122.169177]], + "points": + [{"trial_index": 0, + "total_nanos": 397574122, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12424191.3125, + "peak_rss_kb": 61136, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 417790894, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 13055965.4375, + "peak_rss_kb": 61336, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 396159336, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12379979.25, + "peak_rss_kb": 60292, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 369503684, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 92375921, + "peak_rss_kb": 63408, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 366823473, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 91705868.25, + "peak_rss_kb": 63284, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 365847207, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 91461801.75, + "peak_rss_kb": 62820, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 661184669, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 661184669, + "peak_rss_kb": 71628, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 608808890, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 608808890, + "peak_rss_kb": 70960, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 613664785, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 613664785, + "peak_rss_kb": 71280, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 5068575349, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 5068575349, + "peak_rss_kb": 104592, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 4929966953, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4929966953, + "peak_rss_kb": 101520, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 4847035107, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4847035107, + "peak_rss_kb": 101480, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runStrassenCut128", + "env": + {"timestamp_unix_ms": 1783766592092, + "timestamp_iso": "2026-07-11T10:43:12Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 512, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 40, + "cache_mode": "warm"}, + "complexity_formula": "7 ^ Nat.log2 n", + "c_min": 105.603884, + "c_max": 122.169177, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 0, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.012767, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 12331680.21875, + "median_per_call_nanos": 12355738.65625, + "max_per_call_nanos": 12489424.21875}, + {"relative_spread": 0.005428, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 97538041.75, + "median_per_call_nanos": 97639164, + "max_per_call_nanos": 98068057}, + {"relative_spread": 0.042641, + "param": 256, + "ok_count": 3, + "min_per_call_nanos": 607015004, + "median_per_call_nanos": 613425682, + "max_per_call_nanos": 633171816}, + {"relative_spread": 0.030259, + "param": 512, + "ok_count": 3, + "min_per_call_nanos": 4566110923, + "median_per_call_nanos": 4596441994, + "max_per_call_nanos": 4705196560}], + "spawn_floor_nanos": 22693091, + "slope": 0.019538, + "ratios": + [[64, 105.022046], [128, 118.559886], [256, 106.408822], [512, 113.904118]], + "points": + [{"trial_index": 0, + "total_nanos": 394613767, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12331680.21875, + "peak_rss_kb": 61096, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 395383637, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12355738.65625, + "peak_rss_kb": 60284, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 399661575, + "status": "ok", + "result_hash": "0x1fee7d7dcb68e", + "per_call_nanos": 12489424.21875, + "peak_rss_kb": 61148, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 392272228, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 98068057, + "peak_rss_kb": 62448, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 390152167, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 97538041.75, + "peak_rss_kb": 62416, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 390556656, + "status": "ok", + "result_hash": "0x100a3ae5f21088", + "per_call_nanos": 97639164, + "peak_rss_kb": 62348, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 613425682, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 613425682, + "peak_rss_kb": 71384, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 633171816, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 633171816, + "peak_rss_kb": 71616, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 607015004, + "status": "ok", + "result_hash": "0x800c4094b504ba", + "per_call_nanos": 607015004, + "peak_rss_kb": 70816, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 4566110923, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4566110923, + "peak_rss_kb": 103828, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 4705196560, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4705196560, + "peak_rss_kb": 103764, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 4596441994, + "status": "ok", + "result_hash": "0x3ff9d8390625168", + "per_call_nanos": 4596441994, + "peak_rss_kb": 103024, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.MatrixBench.runStrassenCut256", + "env": + {"timestamp_unix_ms": 1783766611915, + "timestamp_iso": "2026-07-11T10:43:31Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 500000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 10, + "param_schedule": {"params": [64, 128, 256, 512], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 512, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 40, + "cache_mode": "warm"}, + "complexity_formula": "7 ^ Nat.log2 n", + "c_min": 105.022046, + "c_max": 118.559886, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1783766382300, + "timestamp_iso": "2026-07-11T10:39:42Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "aed7d831896c3eddc8527b2133c31a7241d4a3ae", + "exe_name": "hexmatrix_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}} diff --git a/reports/figures/hex-matrix-mul-scaling.svg b/reports/figures/hex-matrix-mul-scaling.svg index 6cdd8ed95..ef798d17d 100644 --- a/reports/figures/hex-matrix-mul-scaling.svg +++ b/reports/figures/hex-matrix-mul-scaling.svg @@ -603,8 +603,8 @@ z - @@ -614,12 +614,12 @@ L -3.5 0 " style="stroke: #000000; stroke-width: 0.8"/> - + - + @@ -630,18 +630,18 @@ L -3.5 0 - - + - + @@ -653,18 +653,18 @@ L 507.6 225.039043 - - + - + - - + - + @@ -705,8 +705,8 @@ L 507.6 87.264905 - @@ -716,379 +716,379 @@ L -2 0 " style="stroke: #000000; stroke-width: 0.6"/> - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + @@ -1196,10 +1196,10 @@ z - @@ -1216,19 +1216,19 @@ z " style="stroke: #c1443c; stroke-opacity: 0.85"/> - - - - + + + + - - - - - - + + + + + - - - - - - + + + + + - - - - - - + + + + + - @@ -1334,7 +1334,7 @@ L 507.6 25.44 - + - +