diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f2d5d051a..ebda02923 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -170,7 +170,7 @@ jobs: - name: Define the hex-dev cache + build target sets run: | echo "HEX_LIB_TARGETS=HexBasic HexTruncatedSeries HexTruncatedSeriesMathlib HexArith HexPoly HexPolyFast HexMvPoly HexModArith HexGF2 HexPolyZ HexRoots HexResultant HexInterval HexIntervalExperiment HexIntervalMathlib HexIntervalMathlibExperiment HexIntervalReplayProbe HexIntervalMathlibReplayProbe HexRealRootsMathlibReplayProbe HexRCFProofProbe HexPolyFp HexGFqRing HexGFqField HexBerlekamp HexHensel HexConway HexGFq HexPrimality HexIntFactor HexPrimalityKernelProbe HexPrimalityElabProbe HexPrimalityMathlibProofProbe HexIntFactorKernelProbe HexMvGcdKernelProbe HexBerlekampZassenhaus HexRealRoots HexMatrix HexRowReduce HexDeterminant HexBareiss HexHermite HexSmith HexCharPoly HexMinPoly HexPolySmith HexGramSchmidt HexLLL HexMatrixMathlib HexHermiteMathlib HexSmithMathlib HexSmithTests HexCharPolyMathlib HexMinPolyMathlib HexPolySmithMathlib HexGramSchmidtMathlib HexLLLMathlib HexBerlekampZassenhausMathlib HexBerlekampZassenhausMathlibProofProbe HexBerlekampMathlibProofProbe HexPrimalityMathlib HexIntFactorMathlib HexPolyFpMathlib HexFactorizationModules HexRealRootsMathlib HexGF2Mathlib HexGFqMathlib HexMvPolyMathlib HexMvPolyMathlibProofProbe HexRCF HexRCFTests HexRootsMathlib HexResultantMathlib HexNumberField HexNumberFieldMathlib HexNumberFieldTower HexNumberFieldTowerMathlib HexReleaseTests HexReleaseExamples HexAggregateCheck" >> "$GITHUB_ENV" - echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexprimality_fuel_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV" + echo "HEX_EXE_TARGETS=hextruncatedseries_bench hexarith_bench hexpoly_bench hexpolyfast_bench hexpolysmith_bench hexmvpoly_bench hexmvgcd_bench hexsparsepoly_bench hexpolyz_bench hexpolyfp_bench hexmodarith_bench hexmodular_bench hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench hexhensel_bench hexprimality_bench hexprimality_policy_probe hexprimality_fuel_probe hexintfactor_bench hexberlekamp_bench hexbz_bench hexconway_bench hexmatrix_bench hexstrassen_compare hexrowreduce_bench hexdeterminant_bench hexbareiss_bench hexcharpoly_bench hexminpoly_bench hexgramschmidt_bench hexhermite_bench hexsmith_bench hexrealroots_bench hexrcf_bench hexroots_bench hexresultant_bench hexnumberfield_bench hexnumberfieldtower_bench hexinterval_decision_bench hexroots_demo hex_interval_representation_spike hex_interval_center_spike hex_interval_scale_spike hex_interval_scheduler_spike hex_interval_policy_frontier_spike hex_arith_floor hexlll_bench hexlll_gram_bench hexlll_external_reduction hexbz_factor_service" >> "$GITHUB_ENV" # Shared build. The libraries, bench exes, conformance #guard drivers, and # emit-fixture exes are all elaborated here so the two verification tails # below only *run* things, never rebuild them -- which is what lets the @@ -239,7 +239,7 @@ jobs: hexmodular_bench \ hexgf2_bench hexgfqring_bench hexgfqfield_bench hexgfq_bench \ hexhensel_bench hexintfactor_bench hexberlekamp_bench hexbz_bench \ - hexconway_bench hexdeterminant_bench hexmatrix_bench \ + hexconway_bench hexdeterminant_bench hexmatrix_bench hexrowreduce_bench \ hexhermite_bench hexsmith_bench \ hexcharpoly_bench hexminpoly_bench \ hexgramschmidt_bench hexlll_gram_bench \ diff --git a/HexRowReduce/SPEC/hex-row-reduce.md b/HexRowReduce/SPEC/hex-row-reduce.md index a2c9311e6..cf664391b 100644 --- a/HexRowReduce/SPEC/hex-row-reduce.md +++ b/HexRowReduce/SPEC/hex-row-reduce.md @@ -73,6 +73,8 @@ def IsRowReduced.nullspaceMatrix [Ring R] (E : IsRowReduced M D) : Matrix R m (m def IsRowReduced.nullspace [Ring R] (E : IsRowReduced M D) : Vector (Vector R m) (m - D.rank) def Matrix.nullspace [Field R] [DecidableEq R] (M : Matrix R n m) : Vector (Vector R m) (m - rowReduce_rank) +def Matrix.nullspaceBasisMatrix [Field R] [DecidableEq R] (M : Matrix R n m) : + Matrix R m (m - rowReduce_rank) ``` **Key properties:** @@ -106,11 +108,49 @@ with `colPartition` (free columns telescope to `v[freeCols[l]]`; pivot columns follow from `pivot_one` / `above_pivot_zero` / `below_pivot_zero` / `zero_row`); package into `E.nullspaceMatrix * c = v`. +## Complexity and benchmark contract + +For an `n × m` matrix of rank `r`, the executable Gauss--Jordan loop performs +at most `r` pivot steps, and each step visits `O(n(n + m))` entries across the +echelon and transform updates. Thus the field-operation bound is +`O(rn(n + m))`; it is cubic for the fixed-aspect square families below. This +is an arithmetic-operation bound, not unrestricted bit complexity: exact +rational cost also depends on numerator and denominator growth. + +`bench/HexRowReduce/Bench.lean` registers every advertised executable surface +directly in mode 1: + +| Operation | Controlled family | Declared wall model | +| --- | --- | --- | +| `Matrix.rowReduce`, `Matrix.rowReduce_rank` | `dense-rational-rref` | `n³` | +| `Matrix.spanCoeffs`, `Matrix.spanContains` | `dense-rational-rref` | `n³` | +| `IsEchelonForm.echelonCoeffs` on prepared RREF | `rank-deficient-rational-nullspace` | `n` | +| `IsEchelonForm.spanCoeffs`, `IsEchelonForm.spanContains` on prepared RREF | `dense-rational-rref` | `n²` | +| `IsEchelonForm.freeCols` on prepared RREF | `rank-deficient-rational-nullspace` | `n²` | +| `Matrix.nullspaceBasisMatrix`, `Matrix.nullspace` | `rank-deficient-rational-nullspace` | `n³` | +| `IsRowReduced.nullspaceMatrix`, `IsRowReduced.nullspace` on prepared RREF | `rank-deficient-rational-nullspace` | `n³` | + +The dense family is `I + J`, so all pivots fire while intermediate rational +heights stay bounded by `O(log n)` bits on the scheduled ladder. The +rank-deficient family repeats the rows and columns of `I + J` at half size, +giving rank and nullity `n / 2`. Prepared span targets exclude RREF and visit +quadratically many entries. Prepared nullspace targets use an already-reduced +rank-`n / 2` projection to exclude RREF setup; constructing `Θ(n²)` output +entries calls a pivot lookup that scans up to `n / 2` columns, giving the +declared cubic model. Preparation and result forcing are outside and inside +the timed region, respectively. + ## External comparators -The `rank`, `rowReduce`, and `nullspace` operations are cross-checked for correctness -against python-flint's `fmpz_mat` / `fmpq_mat` through the conformance oracle -(`scripts/oracle/matrix_flint.py`, driven by `hexrowreduce_emit_fixtures`). -There is no Phase-4 performance comparator: row reduction is an exact rational -computation validated for correctness, not timed against an external tool. See -`reports/hex-row-reduce-performance.md`. +No external Phase-4 timing comparator is declared. python-flint exposes +FLINT's exact rational RREF, but the public Python interface must decode and +encode every rational matrix entry for each request; that transport dominates +the shared practical ladder and therefore cannot support a meaningful kernel +ratio. Moreover, Hex's `rowReduce` returns the complete row-operation +transform while python-flint's RREF omits it, and `spanCoeffs` returns a +transform-dependent witness with no canonical counterpart. + +FLINT remains the independent correctness oracle for `rank`, `rowReduce`, and +`nullspace` through `scripts/oracle/matrix_flint.py`, driven by +`hexrowreduce_emit_fixtures`. It is conformance evidence, not timing evidence. +See `reports/hex-row-reduce-performance.md`. diff --git a/bench/HexRowReduce/Bench.lean b/bench/HexRowReduce/Bench.lean new file mode 100644 index 000000000..be2cb359e --- /dev/null +++ b/bench/HexRowReduce/Bench.lean @@ -0,0 +1,315 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ + +import HexRowReduce +import LeanBench + +/-! +Mode-1 benchmarks for the public executable `HexRowReduce` surface. + +The `dense` family uses the matrix `I + J`: every column supplies a pivot and +every pivot eliminates nonzero entries above and below it. Its inverse has +diagonal entries `n / (n + 1)` and off-diagonal entries `-1 / (n + 1)`, so the +controlled family exercises the complete Gauss--Jordan schedule without +uncontrolled rational coefficient growth. + +The `deficient` family repeats the rows and columns of `I + J` at dimension +`n / 2`. It therefore has rank and nullity `n / 2`, exercises successful and +unsuccessful pivot searches, and materializes a quadratic-size nullspace +basis. Both families are prepared outside the timed region. +-/ + +namespace Hex.RowReduceBench + +/-- A prepared square rational matrix and a known member of its row span. -/ +structure Input where + n : Nat + matrix : Matrix Rat n n + query : Vector Rat n + +private def vectorChecksum {n : Nat} (v : Vector Rat n) : UInt64 := + hash v.toArray + +private def matrixChecksum {n m : Nat} (M : Matrix Rat n m) : UInt64 := + M.rows.toArray.foldl + (fun checksum row => mixHash checksum (vectorChecksum row)) + (hash n) + +instance : Hashable Input where + hash input := mixHash (hash input.n) <| + mixHash (matrixChecksum input.matrix) (vectorChecksum input.query) + +/-- Prepared RREF data for isolating the executable contract-level span and +nullspace constructors from the public wrappers' row-reduction phase. -/ +structure ReducedInput where + n : Nat + source : Matrix Rat n n + data : Matrix.RowEchelonData Rat n n + reduced : Matrix.IsRowReduced source data + query : Vector Rat n + +instance : Hashable ReducedInput where + hash input := mixHash (hash input.n) <| + mixHash (matrixChecksum input.source) <| + mixHash (matrixChecksum input.data.echelon) <| + mixHash (matrixChecksum input.data.transform) <| + mixHash (hash input.data.pivotCols.toArray) (vectorChecksum input.query) + +/-- Dense `I + J`, whose full Gauss--Jordan path stays at logarithmic +coefficient height. -/ +def dense (n : Nat) : Input := + let matrix : Matrix Rat n n := + Matrix.ofFn fun i j => if i = j then 2 else 1 + let query : Vector Rat n := + Vector.ofFn fun j => if j.val = 0 then 2 else 1 + { n, matrix, query } + +/-- A dense square matrix obtained by repeating the rows and columns of +`I + J` at dimension `n / 2`. -/ +def deficient (n : Nat) : Input := + let rank := n / 2 + let matrix : Matrix Rat n n := Matrix.ofFn fun i j => + if rank = 0 then 0 + else if i.val % rank = j.val % rank then 2 else 1 + let query : Vector Rat n := Vector.ofFn fun j => + if rank = 0 then 0 + else if j.val % rank = 0 then 2 else 1 + { n, matrix, query } + +/-- A sparse rank-`n / 2` projection used only to prepare the contract-level +nullspace targets. Its already-reduced shape keeps untimed witness +construction cheap enough for the larger ladder needed to expose pivot scans. +-/ +def reducedDeficient (n : Nat) : Input := + let rank := n / 2 + let matrix : Matrix Rat n n := Matrix.ofFn fun i j => + if i = j ∧ i.val < rank then 1 else 0 + let query : Vector Rat n := Vector.ofFn fun j => + if j.val = 0 ∧ 0 < rank then 1 else 0 + { n, matrix, query } + +def denseReduced (n : Nat) : ReducedInput := + let input := dense n + let data := Matrix.rowReduce input.matrix + { n, source := input.matrix, data + reduced := Matrix.rowReduce_isRowReduced input.matrix + query := input.query } + +def deficientReduced (n : Nat) : ReducedInput := + let input := reducedDeficient n + let data := Matrix.rowReduce input.matrix + { n, source := input.matrix, data + reduced := Matrix.rowReduce_isRowReduced input.matrix + query := input.query } + +/-- Force every field of the transform-producing RREF result. -/ +def runReduce (input : Input) : UInt64 := + let result := Matrix.rowReduce input.matrix + mixHash (hash result.rank) <| + mixHash (matrixChecksum result.echelon) <| + mixHash (matrixChecksum result.transform) (hash result.pivotCols.toArray) + +/-- Rank projection through the public row-reduction wrapper. -/ +def runRank (input : Input) : Nat := + Matrix.rowReduce_rank input.matrix + +/-- Constructive row-span coefficients for a known member. -/ +def runSpanCoeffs (input : Input) : UInt64 := + match Matrix.spanCoeffs input.matrix input.query with + | some coefficients => mixHash (vectorChecksum input.query) (vectorChecksum coefficients) + | none => 0 + +/-- Row-span membership for the same known member. -/ +def runSpanContains (input : Input) : UInt64 := + mixHash (vectorChecksum input.query) (hash (Matrix.spanContains input.matrix input.query)) + +/-- Contract-level row-span coefficient construction on prepared RREF data. -/ +def runEchelonSpanCoeffs (input : ReducedInput) : UInt64 := + match input.reduced.toIsEchelonForm.spanCoeffs input.query with + | some coefficients => vectorChecksum coefficients + | none => 0 + +/-- Contract-level row-span membership on prepared RREF data. -/ +def runEchelonSpanContains (input : ReducedInput) : Bool := + input.reduced.toIsEchelonForm.spanContains input.query + +/-- Pivot-coordinate coefficient selection on prepared echelon data. -/ +def runEchelonCoeffs (input : ReducedInput) : UInt64 := + vectorChecksum (input.reduced.toIsEchelonForm.echelonCoeffs input.query) + +/-- Sorted complement of the pivot columns on prepared echelon data. -/ +def runFreeCols (input : ReducedInput) : UInt64 := + hash input.reduced.toIsEchelonForm.freeCols.toArray + +/-- The public nullspace basis-matrix wrapper on a rank-deficient matrix. -/ +def runNullspaceMatrix (input : Input) : UInt64 := + hash (Matrix.nullspaceBasisMatrix input.matrix).data.toArray + +/-- The public vector-of-vectors nullspace wrapper on a rank-deficient matrix. -/ +def runNullspace (input : Input) : UInt64 := + (Matrix.nullspace input.matrix).toArray.foldl + (fun checksum vector => mixHash checksum (vectorChecksum vector)) + (hash input.n) + +/-- Contract-level nullspace basis matrix on prepared rank-deficient RREF. -/ +def runReducedMatrix (input : ReducedInput) : UInt64 := + matrixChecksum input.reduced.nullspaceMatrix + +/-- Contract-level vector-of-vectors nullspace on prepared rank-deficient RREF. -/ +def runReducedNullspace (input : ReducedInput) : UInt64 := + input.reduced.nullspace.toArray.foldl + (fun checksum vector => mixHash checksum (vectorChecksum vector)) + (hash input.n) + +private def schedule : Array Nat := #[8, 12, 16, 24, 32, 48, 64] +private def basisMatrixSchedule : Array Nat := #[16, 24, 32, 48, 64] + +-- Prepared operations avoid elimination. The quadratic span traversals clear +-- the algorithmic signal by 192, while the cheap pivot scans in the cubic +-- nullspace constructor need larger matrices before their leading term +-- dominates allocation. +private def preparedSpanSchedule : Array Nat := #[16, 24, 32, 48, 64, 96, 128, 192] +private def preparedNullspaceSchedule : Array Nat := #[128, 192, 256, 384, 512, 768, 1024] +-- Keep the prepared vector operations below the runtime's large-allocation +-- transitions; the batched timings already have ample signal at these sizes. +private def preparedLinearSchedule : Array Nat := #[128, 192, 256, 384, 512, 768] +private def freeColsSchedule : Array Nat := #[64, 96, 128, 192, 256, 384, 512] + +/- Cost-model derivation: on dense `I + J`, all `n` pivots fire. Each pivot +normalizes two length-`n` rows (echelon and transform) and eliminates up to +`n - 1` nonzero rows in both matrices, hence `Theta(n^3)` field operations. +The family keeps rational numerators and denominators `O(n)`, so every operand +fits one machine word on this schedule and the independently derived wall +model is `n^3`. -/ +setup_benchmark runReduce n => n ^ 3 with prep := dense where { + paramFloor := 8, paramCeiling := 64, paramSchedule := .custom schedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: `rowReduce_rank` projects one field from the same +complete dense RREF run, so its controlled-family model remains `Theta(n^3)`. +-/ +setup_benchmark runRank n => n ^ 3 with prep := dense where { + paramFloor := 8, paramCeiling := 64, paramSchedule := .custom schedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: `spanCoeffs` performs the same cubic dense RREF run, +then one transform-vector product and one residual row-combination check, both +quadratic. The resulting controlled-family model is therefore `Theta(n^3)`. +-/ +setup_benchmark runSpanCoeffs n => n ^ 3 with prep := dense where { + paramFloor := 8, paramCeiling := 64, paramSchedule := .custom schedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: `spanContains` is the `Option.isSome` projection of +the same `spanCoeffs` computation, preserving its `Theta(n^3)` model. -/ +setup_benchmark runSpanContains n => n ^ 3 with prep := dense where { + paramFloor := 8, paramCeiling := 64, paramSchedule := .custom schedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: on prepared full-rank RREF data, `spanCoeffs` makes +one dense transform-vector product and one residual row-combination check. +Both visit `Theta(n^2)` entries; coefficient selection is linear. -/ +setup_benchmark runEchelonSpanCoeffs n => n ^ 2 with prep := denseReduced where { + paramFloor := 16, paramCeiling := 192, paramSchedule := .custom preparedSpanSchedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: contract-level `spanContains` projects `isSome` +from the same prepared `spanCoeffs` computation and is therefore +`Theta(n^2)` on this family. -/ +setup_benchmark runEchelonSpanContains n => n ^ 2 with prep := denseReduced where { + paramFloor := 16, paramCeiling := 192, paramSchedule := .custom preparedSpanSchedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: `echelonCoeffs` constructs one length-`n` vector. +Each live entry performs constant-time pivot-column and matrix indexing on the +prepared bounded-integer projection, so the family performs `Theta(n)` work. -/ +setup_benchmark runEchelonCoeffs n => (n) with prep := deficientReduced where { + paramFloor := 128, paramCeiling := 768, paramSchedule := .custom preparedLinearSchedule + targetInnerNanos := 1_000_000_000, outerTrials := 5 + slopeTolerance := 0.15 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: `freeCols` filters all `n` columns and tests each +against the sorted pivot vector by a linear list-membership scan. On the +rank-`n / 2` prepared family the aggregate scan is `Theta(n^2)`. -/ +setup_benchmark runFreeCols n => (n ^ 2) with prep := deficientReduced where { + paramFloor := 64, paramCeiling := 512, paramSchedule := .custom freeColsSchedule + targetInnerNanos := 1_000_000_000, outerTrials := 5 + slopeTolerance := 0.15 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: the deficient family has rank and nullity `n / 2`. +Its RREF phase is cubic, and `nullspaceMatrix` constructs `Theta(n^2)` entries +whose pivot lookup scans at most `n / 2` pivot columns, also `Theta(n^3)`. +The ladder begins at 16, where forcing the basis matrix has entered that +derived dominant regime. +-/ +setup_benchmark runNullspaceMatrix n => n ^ 3 with prep := deficient where { + paramFloor := 16, paramCeiling := 64, paramSchedule := .custom basisMatrixSchedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: `nullspace` shares one basis-matrix construction and +extracts its `n / 2` length-`n` columns. That quadratic projection follows +the same cubic RREF and pivot-lookup work as `nullspaceBasisMatrix`, so the +controlled-family model remains `Theta(n^3)`. -/ +setup_benchmark runNullspace n => n ^ 3 with prep := deficient where { + paramFloor := 8, paramCeiling := 64, paramSchedule := .custom schedule + targetInnerNanos := 1_000_000_000, outerTrials := 3 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: prepared `nullspaceMatrix` constructs +`Theta(n^2)` entries on rank/nullity `n / 2`; pivot entries perform a linear +scan through at most `n / 2` pivot columns, yielding `Theta(n^3)` work. -/ +setup_benchmark runReducedMatrix n => n ^ 3 with prep := deficientReduced where { + paramFloor := 128, paramCeiling := 1024, paramSchedule := .custom preparedNullspaceSchedule + targetInnerNanos := 1_000_000_000, outerTrials := 7 + slopeTolerance := 0.20 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +/- Cost-model derivation: prepared `nullspace` shares the same basis-matrix +construction and then extracts quadratically many entries as columns, so its +model remains `Theta(n^3)` on the rank-deficient family. -/ +setup_benchmark runReducedNullspace n => n ^ 3 with prep := deficientReduced where { + paramFloor := 128, paramCeiling := 1024, paramSchedule := .custom preparedNullspaceSchedule + targetInnerNanos := 1_000_000_000, outerTrials := 7 + slopeTolerance := 0.20 + signalFloorMultiplier := 1.0 + maxSecondsPerCall := 10.0 +} + +end Hex.RowReduceBench + +def main (args : List String) : IO UInt32 := + LeanBench.Cli.dispatch args diff --git a/lakefile.lean b/lakefile.lean index 73cfb36ee..89a7d413c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -1014,6 +1014,10 @@ lean_exe hexmatrix_bench where srcDir := "bench" root := `HexMatrix.Bench +lean_exe hexrowreduce_bench where + srcDir := "bench" + root := `HexRowReduce.Bench + lean_exe hexdeterminant_bench where srcDir := "bench" root := `HexDeterminant.Bench diff --git a/libraries.yml b/libraries.yml index 10ecd6d01..080759c82 100644 --- a/libraries.yml +++ b/libraries.yml @@ -245,8 +245,14 @@ libraries: HexRowReduce: deps: [HexMatrix] mathlib: false - done_through: 3 + done_through: 4 status: active + phase4: + input_families: + - name: dense-rational-rref + description: Dense square rational I + J matrices with a pivot in every column and nonzero elimination above and below every pivot, plus a known row-span member. + - name: rank-deficient-rational-nullspace + description: Rank-and-nullity n / 2 rational matrices, using repeated I + J for public wrappers and an already-reduced sparse projection to isolate echelon coefficients, free columns, and contract-level nullspace construction. HexDeterminant: deps: [HexMatrix] mathlib: false diff --git a/reports/bench-results/hex-row-reduce-phase4-scientific.json b/reports/bench-results/hex-row-reduce-phase4-scientific.json new file mode 100644 index 000000000..a4ec32223 --- /dev/null +++ b/reports/bench-results/hex-row-reduce-phase4-scientific.json @@ -0,0 +1,5081 @@ +{"results": + [{"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.045941, + "param": 8, + "ok_count": 3, + "min_per_call_nanos": 377158.510254, + "median_per_call_nanos": 386915.861328, + "max_per_call_nanos": 394933.688965}, + {"relative_spread": 0.044845, + "param": 12, + "ok_count": 3, + "min_per_call_nanos": 1356602.582031, + "median_per_call_nanos": 1368486.28125, + "max_per_call_nanos": 1417971.835938}, + {"relative_spread": 0.034706, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 3218096.0625, + "median_per_call_nanos": 3225737.753906, + "max_per_call_nanos": 3330048.925781}, + {"relative_spread": 0.00902, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 11084469.984375, + "median_per_call_nanos": 11149741.765625, + "max_per_call_nanos": 11185039.109375}, + {"relative_spread": 0.061102, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 25684304.78125, + "median_per_call_nanos": 26641340.9375, + "max_per_call_nanos": 27312132}, + {"relative_spread": 0.060857, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 83466415.625, + "median_per_call_nanos": 84037369.875, + "max_per_call_nanos": 88580693.875}, + {"relative_spread": 0.152692, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 204987521.25, + "median_per_call_nanos": 218730302, + "max_per_call_nanos": 238385833.75}], + "spawn_floor_nanos": 147065207, + "slope": 0.012324, + "ratios": + [[8, 755.695042], + [12, 791.948079], + [16, 787.533631], + [24, 806.549607], + [32, 813.029203], + [48, 759.886519], + [64, 834.389885]], + "points": + [{"trial_index": 0, + "total_nanos": 772420629, + "status": "ok", + "result_hash": "0x8", + "per_call_nanos": 377158.510254, + "peak_rss_kb": 61916, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 792403684, + "status": "ok", + "result_hash": "0x8", + "per_call_nanos": 386915.861328, + "peak_rss_kb": 62292, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 808824195, + "status": "ok", + "result_hash": "0x8", + "per_call_nanos": 394933.688965, + "peak_rss_kb": 61820, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 700664976, + "status": "ok", + "result_hash": "0xc", + "per_call_nanos": 1368486.28125, + "peak_rss_kb": 61948, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 363000790, + "status": "ok", + "result_hash": "0xc", + "per_call_nanos": 1417971.835938, + "peak_rss_kb": 62060, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 694580522, + "status": "ok", + "result_hash": "0xc", + "per_call_nanos": 1356602.582031, + "peak_rss_kb": 64220, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 823832592, + "status": "ok", + "result_hash": "0x10", + "per_call_nanos": 3218096.0625, + "peak_rss_kb": 62080, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 852492525, + "status": "ok", + "result_hash": "0x10", + "per_call_nanos": 3330048.925781, + "peak_rss_kb": 61956, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 825788865, + "status": "ok", + "result_hash": "0x10", + "per_call_nanos": 3225737.753906, + "peak_rss_kb": 62468, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 713583473, + "status": "ok", + "result_hash": "0x18", + "per_call_nanos": 11149741.765625, + "peak_rss_kb": 62040, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 715842503, + "status": "ok", + "result_hash": "0x18", + "per_call_nanos": 11185039.109375, + "peak_rss_kb": 61980, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 709406079, + "status": "ok", + "result_hash": "0x18", + "per_call_nanos": 11084469.984375, + "peak_rss_kb": 62568, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 821897753, + "status": "ok", + "result_hash": "0x20", + "per_call_nanos": 25684304.78125, + "peak_rss_kb": 64240, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 852522910, + "status": "ok", + "result_hash": "0x20", + "per_call_nanos": 26641340.9375, + "peak_rss_kb": 62320, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 873988224, + "status": "ok", + "result_hash": "0x20", + "per_call_nanos": 27312132, + "peak_rss_kb": 64456, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 708645551, + "status": "ok", + "result_hash": "0x30", + "per_call_nanos": 88580693.875, + "peak_rss_kb": 62308, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 672298959, + "status": "ok", + "result_hash": "0x30", + "per_call_nanos": 84037369.875, + "peak_rss_kb": 64288, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 667731325, + "status": "ok", + "result_hash": "0x30", + "per_call_nanos": 83466415.625, + "peak_rss_kb": 62524, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 819950085, + "status": "ok", + "result_hash": "0x40", + "per_call_nanos": 204987521.25, + "peak_rss_kb": 62604, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 874921208, + "status": "ok", + "result_hash": "0x40", + "per_call_nanos": 218730302, + "peak_rss_kb": 62432, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 953543335, + "status": "ok", + "result_hash": "0x40", + "per_call_nanos": 238385833.75, + "peak_rss_kb": 62444, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runRank", + "env": + {"timestamp_unix_ms": 1788156872878, + "timestamp_iso": "2026-08-31T06:14:32Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [8, 12, 16, 24, 32, 48, 64], "kind": "custom"}, + "param_floor": 8, + "param_ceiling": 64, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 759.886519, + "c_max": 834.389885, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.043671, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 217806.60083, + "median_per_call_nanos": 220407.53833, + "max_per_call_nanos": 227432.074219}, + {"relative_spread": 0.05691, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 464533.380371, + "median_per_call_nanos": 467836.756348, + "max_per_call_nanos": 491158.016602}, + {"relative_spread": 0.037188, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 842039.488281, + "median_per_call_nanos": 855595.538086, + "max_per_call_nanos": 873857.601562}, + {"relative_spread": 0.033701, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 1923703.048828, + "median_per_call_nanos": 1945318.308594, + "max_per_call_nanos": 1989262.109375}, + {"relative_spread": 0.043408, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 3435216.539062, + "median_per_call_nanos": 3474154.832031, + "max_per_call_nanos": 3586021.003906}, + {"relative_spread": 0.050145, + "param": 96, + "ok_count": 3, + "min_per_call_nanos": 7926927.21875, + "median_per_call_nanos": 7963845.78125, + "max_per_call_nanos": 8326272.5625}, + {"relative_spread": 0.039367, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 14468990.203125, + "median_per_call_nanos": 14912886.15625, + "max_per_call_nanos": 15056064.734375}, + {"relative_spread": 0.202336, + "param": 192, + "ok_count": 3, + "min_per_call_nanos": 27800512.96875, + "median_per_call_nanos": 32126432.6875, + "max_per_call_nanos": 34300839.21875}], + "spawn_floor_nanos": 46372360, + "slope": 0.04116, + "ratios": + [[16, 860.966947], + [24, 812.216591], + [32, 835.542518], + [48, 844.322183], + [64, 848.182332], + [96, 864.132572], + [128, 910.210337], + [192, 871.485262]], + "points": + [{"trial_index": 0, + "total_nanos": 892135837, + "status": "ok", + "result_hash": "0x3d4ddfeac7557284", + "per_call_nanos": 217806.60083, + "peak_rss_kb": 62280, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 931561776, + "status": "ok", + "result_hash": "0x3d4ddfeac7557284", + "per_call_nanos": 227432.074219, + "peak_rss_kb": 62488, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 902789277, + "status": "ok", + "result_hash": "0x3d4ddfeac7557284", + "per_call_nanos": 220407.53833, + "peak_rss_kb": 62228, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 951364363, + "status": "ok", + "result_hash": "0x6445e860d3e6abb4", + "per_call_nanos": 464533.380371, + "peak_rss_kb": 61744, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 958129677, + "status": "ok", + "result_hash": "0x6445e860d3e6abb4", + "per_call_nanos": 467836.756348, + "peak_rss_kb": 63704, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1005891618, + "status": "ok", + "result_hash": "0x6445e860d3e6abb4", + "per_call_nanos": 491158.016602, + "peak_rss_kb": 62584, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 876129831, + "status": "ok", + "result_hash": "0x9ff874657ef86324", + "per_call_nanos": 855595.538086, + "peak_rss_kb": 62276, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 862248436, + "status": "ok", + "result_hash": "0x9ff874657ef86324", + "per_call_nanos": 842039.488281, + "peak_rss_kb": 62548, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 894830184, + "status": "ok", + "result_hash": "0x9ff874657ef86324", + "per_call_nanos": 873857.601562, + "peak_rss_kb": 62388, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 996002974, + "status": "ok", + "result_hash": "0xd8c9b6f31f9602c4", + "per_call_nanos": 1945318.308594, + "peak_rss_kb": 62688, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 984935961, + "status": "ok", + "result_hash": "0xd8c9b6f31f9602c4", + "per_call_nanos": 1923703.048828, + "peak_rss_kb": 62832, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1018502200, + "status": "ok", + "result_hash": "0xd8c9b6f31f9602c4", + "per_call_nanos": 1989262.109375, + "peak_rss_kb": 62744, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 889383637, + "status": "ok", + "result_hash": "0xb90d7b05d22eb864", + "per_call_nanos": 3474154.832031, + "peak_rss_kb": 62620, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 918021377, + "status": "ok", + "result_hash": "0xb90d7b05d22eb864", + "per_call_nanos": 3586021.003906, + "peak_rss_kb": 62416, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 879415434, + "status": "ok", + "result_hash": "0xb90d7b05d22eb864", + "per_call_nanos": 3435216.539062, + "peak_rss_kb": 62208, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1065762888, + "status": "ok", + "result_hash": "0x3ea4b771d0f57ea4", + "per_call_nanos": 8326272.5625, + "peak_rss_kb": 62844, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1019372260, + "status": "ok", + "result_hash": "0x3ea4b771d0f57ea4", + "per_call_nanos": 7963845.78125, + "peak_rss_kb": 63044, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 507323342, + "status": "ok", + "result_hash": "0x3ea4b771d0f57ea4", + "per_call_nanos": 7926927.21875, + "peak_rss_kb": 63224, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 926015373, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 14468990.203125, + "peak_rss_kb": 63676, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 963588143, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 15056064.734375, + "peak_rss_kb": 64096, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 954424714, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 14912886.15625, + "peak_rss_kb": 63828, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1028045846, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 32126432.6875, + "peak_rss_kb": 65376, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 889616415, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 27800512.96875, + "peak_rss_kb": 66156, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1097626855, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 34300839.21875, + "peak_rss_kb": 65624, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runEchelonSpanCoeffs", + "env": + {"timestamp_unix_ms": 1788156892050, + "timestamp_iso": "2026-08-31T06:14:52Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": + {"params": [16, 24, 32, 48, 64, 96, 128, 192], "kind": "custom"}, + "param_floor": 16, + "param_ceiling": 192, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 2", + "c_min": 812.216591, + "c_max": 910.210337, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.095385, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 215618.906738, + "median_per_call_nanos": 224483.625488, + "max_per_call_nanos": 237031.323486}, + {"relative_spread": 0.02666, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 470516.499023, + "median_per_call_nanos": 476027.014648, + "max_per_call_nanos": 483207.34082}, + {"relative_spread": 0.044535, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 823296.37207, + "median_per_call_nanos": 832329.768555, + "max_per_call_nanos": 860364.244141}, + {"relative_spread": 0.02876, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 1868755.417969, + "median_per_call_nanos": 1910809.308594, + "max_per_call_nanos": 1923710.529297}, + {"relative_spread": 0.087787, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 3248268.214844, + "median_per_call_nanos": 3390970.9375, + "max_per_call_nanos": 3545950.777344}, + {"relative_spread": 0.082604, + "param": 96, + "ok_count": 3, + "min_per_call_nanos": 7826247.46875, + "median_per_call_nanos": 8193709.992188, + "max_per_call_nanos": 8503078.398438}, + {"relative_spread": 0.13039, + "param": 128, + "ok_count": 3, + "min_per_call_nanos": 13793569.078125, + "median_per_call_nanos": 14826081.546875, + "max_per_call_nanos": 15726741.3125}, + {"relative_spread": 0.050257, + "param": 192, + "ok_count": 3, + "min_per_call_nanos": 33058274.4375, + "median_per_call_nanos": 34038516.59375, + "max_per_call_nanos": 34768957.96875}], + "spawn_floor_nanos": 110564277, + "slope": 0.064103, + "ratios": + [[16, 876.889162], + [24, 826.435789], + [32, 812.82204], + [48, 829.344318], + [64, 827.873764], + [96, 889.074435], + [128, 904.912204], + [192, 923.353857]], + "points": + [{"trial_index": 0, + "total_nanos": 883175042, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 215618.906738, + "peak_rss_kb": 63004, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 970880301, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 237031.323486, + "peak_rss_kb": 62640, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 919484930, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 224483.625488, + "peak_rss_kb": 62528, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 487451663, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 476027.014648, + "peak_rss_kb": 63144, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 963617790, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 470516.499023, + "peak_rss_kb": 62572, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 494804317, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 483207.34082, + "peak_rss_kb": 62680, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 852305683, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 832329.768555, + "peak_rss_kb": 62628, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 843055485, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 823296.37207, + "peak_rss_kb": 62304, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 881012986, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 860364.244141, + "peak_rss_kb": 62248, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 978334366, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 1910809.308594, + "peak_rss_kb": 63600, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 984939791, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 1923710.529297, + "peak_rss_kb": 62420, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 956802774, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 1868755.417969, + "peak_rss_kb": 62932, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 868088560, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 3390970.9375, + "peak_rss_kb": 62840, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 831556663, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 3248268.214844, + "peak_rss_kb": 62968, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 907763399, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 3545950.777344, + "peak_rss_kb": 62636, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1088394035, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 8503078.398438, + "peak_rss_kb": 64776, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1001759676, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 7826247.46875, + "peak_rss_kb": 63128, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1048794879, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 8193709.992188, + "peak_rss_kb": 63120, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 948869219, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 14826081.546875, + "peak_rss_kb": 63808, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1006511444, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 15726741.3125, + "peak_rss_kb": 63652, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 882788421, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 13793569.078125, + "peak_rss_kb": 63712, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 528932391, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 33058274.4375, + "peak_rss_kb": 67232, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1112606655, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 34768957.96875, + "peak_rss_kb": 65732, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1089232531, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 34038516.59375, + "peak_rss_kb": 65604, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runEchelonSpanContains", + "env": + {"timestamp_unix_ms": 1788156941875, + "timestamp_iso": "2026-08-31T06:15:41Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": + {"params": [16, 24, 32, 48, 64, 96, 128, 192], "kind": "custom"}, + "param_floor": 16, + "param_ceiling": 192, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 2", + "c_min": 812.82204, + "c_max": 923.353857, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.146907, + "param": 128, + "ok_count": 7, + "min_per_call_nanos": 1085442.339844, + "median_per_call_nanos": 1195268.785156, + "max_per_call_nanos": 1261035.400391}, + {"relative_spread": 0.215161, + "param": 192, + "ok_count": 7, + "min_per_call_nanos": 2925693.4375, + "median_per_call_nanos": 3342622.6875, + "max_per_call_nanos": 3644896.8125}, + {"relative_spread": 0.177649, + "param": 256, + "ok_count": 7, + "min_per_call_nanos": 7025061.375, + "median_per_call_nanos": 7722987.625, + "max_per_call_nanos": 8397045.0625}, + {"relative_spread": 0.178271, + "param": 384, + "ok_count": 7, + "min_per_call_nanos": 21395505.375, + "median_per_call_nanos": 23745088.5625, + "max_per_call_nanos": 25628563.34375}, + {"relative_spread": 0.291163, + "param": 512, + "ok_count": 7, + "min_per_call_nanos": 56339731.125, + "median_per_call_nanos": 58253255.125, + "max_per_call_nanos": 73300943.625}, + {"relative_spread": 0.157498, + "param": 768, + "ok_count": 7, + "min_per_call_nanos": 182399392.75, + "median_per_call_nanos": 193335949.25, + "max_per_call_nanos": 212849473}, + {"relative_spread": 0.325058, + "param": 1024, + "ok_count": 7, + "min_per_call_nanos": 419316301, + "median_per_call_nanos": 439826823.5, + "max_per_call_nanos": 562285496}], + "spawn_floor_nanos": 88170688, + "slope": -0.076099, + "ratios": + [[128, 0.569949], + [192, 0.472263], + [256, 0.460326], + [384, 0.419353], + [512, 0.434021], + [768, 0.426804], + [1024, 0.409621]], + "points": + [{"trial_index": 0, + "total_nanos": 1219844650, + "status": "ok", + "result_hash": "0xf5b9f6c99ee6202", + "per_call_nanos": 1191254.541016, + "peak_rss_kb": 63756, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 645650125, + "status": "ok", + "result_hash": "0xf5b9f6c99ee6202", + "per_call_nanos": 1261035.400391, + "peak_rss_kb": 64132, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 628150503, + "status": "ok", + "result_hash": "0xf5b9f6c99ee6202", + "per_call_nanos": 1226856.451172, + "peak_rss_kb": 63596, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 612357602, + "status": "ok", + "result_hash": "0xf5b9f6c99ee6202", + "per_call_nanos": 1196010.941406, + "peak_rss_kb": 63456, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 1116618525, + "status": "ok", + "result_hash": "0xf5b9f6c99ee6202", + "per_call_nanos": 1090447.77832, + "peak_rss_kb": 65452, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 555746478, + "status": "ok", + "result_hash": "0xf5b9f6c99ee6202", + "per_call_nanos": 1085442.339844, + "peak_rss_kb": 63636, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 611977618, + "status": "ok", + "result_hash": "0xf5b9f6c99ee6202", + "per_call_nanos": 1195268.785156, + "peak_rss_kb": 63568, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 233273396, + "status": "ok", + "result_hash": "0xb025fe0e9ef32593", + "per_call_nanos": 3644896.8125, + "peak_rss_kb": 65648, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 106932542, + "status": "ok", + "result_hash": "0xb025fe0e9ef32593", + "per_call_nanos": 3341641.9375, + "peak_rss_kb": 67980, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 108023459, + "status": "ok", + "result_hash": "0xb025fe0e9ef32593", + "per_call_nanos": 3375733.09375, + "peak_rss_kb": 66912, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 55526136, + "status": "ok", + "result_hash": "0xb025fe0e9ef32593", + "per_call_nanos": 3470383.5, + "peak_rss_kb": 65212, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 194259429, + "status": "ok", + "result_hash": "0xb025fe0e9ef32593", + "per_call_nanos": 3035303.578125, + "peak_rss_kb": 69460, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 374488760, + "status": "ok", + "result_hash": "0xb025fe0e9ef32593", + "per_call_nanos": 2925693.4375, + "peak_rss_kb": 65824, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 855711408, + "status": "ok", + "result_hash": "0xb025fe0e9ef32593", + "per_call_nanos": 3342622.6875, + "peak_rss_kb": 65832, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 513506064, + "status": "ok", + "result_hash": "0x9c6d4eb1deb32b94", + "per_call_nanos": 8023532.25, + "peak_rss_kb": 69108, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 238668587, + "status": "ok", + "result_hash": "0x9c6d4eb1deb32b94", + "per_call_nanos": 7458393.34375, + "peak_rss_kb": 68864, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 112400982, + "status": "ok", + "result_hash": "0x9c6d4eb1deb32b94", + "per_call_nanos": 7025061.375, + "peak_rss_kb": 69916, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 466992615, + "status": "ok", + "result_hash": "0x9c6d4eb1deb32b94", + "per_call_nanos": 7296759.609375, + "peak_rss_kb": 69136, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 125706293, + "status": "ok", + "result_hash": "0x9c6d4eb1deb32b94", + "per_call_nanos": 7856643.3125, + "peak_rss_kb": 68572, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 268705442, + "status": "ok", + "result_hash": "0x9c6d4eb1deb32b94", + "per_call_nanos": 8397045.0625, + "peak_rss_kb": 69208, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 123567802, + "status": "ok", + "result_hash": "0x9c6d4eb1deb32b94", + "per_call_nanos": 7722987.625, + "peak_rss_kb": 68612, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 820114027, + "status": "ok", + "result_hash": "0x1962b6e2e1c7f0e0", + "per_call_nanos": 25628563.34375, + "peak_rss_kb": 75960, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 785401388, + "status": "ok", + "result_hash": "0x1962b6e2e1c7f0e0", + "per_call_nanos": 24543793.375, + "peak_rss_kb": 76224, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 759842834, + "status": "ok", + "result_hash": "0x1962b6e2e1c7f0e0", + "per_call_nanos": 23745088.5625, + "peak_rss_kb": 75892, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 365120858, + "status": "ok", + "result_hash": "0x1962b6e2e1c7f0e0", + "per_call_nanos": 22820053.625, + "peak_rss_kb": 76088, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 342328086, + "status": "ok", + "result_hash": "0x1962b6e2e1c7f0e0", + "per_call_nanos": 21395505.375, + "peak_rss_kb": 76680, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 364037160, + "status": "ok", + "result_hash": "0x1962b6e2e1c7f0e0", + "per_call_nanos": 22752322.5, + "peak_rss_kb": 76708, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 381497364, + "status": "ok", + "result_hash": "0x1962b6e2e1c7f0e0", + "per_call_nanos": 23843585.25, + "peak_rss_kb": 76312, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 905849133, + "status": "ok", + "result_hash": "0xc51abeaa313bb1b4", + "per_call_nanos": 56615570.8125, + "peak_rss_kb": 94788, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 466026041, + "status": "ok", + "result_hash": "0xc51abeaa313bb1b4", + "per_call_nanos": 58253255.125, + "peak_rss_kb": 90200, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 901435698, + "status": "ok", + "result_hash": "0xc51abeaa313bb1b4", + "per_call_nanos": 56339731.125, + "peak_rss_kb": 90164, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 504922105, + "status": "ok", + "result_hash": "0xc51abeaa313bb1b4", + "per_call_nanos": 63115263.125, + "peak_rss_kb": 91904, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 455958961, + "status": "ok", + "result_hash": "0xc51abeaa313bb1b4", + "per_call_nanos": 56994870.125, + "peak_rss_kb": 91912, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 939073165, + "status": "ok", + "result_hash": "0xc51abeaa313bb1b4", + "per_call_nanos": 58692072.8125, + "peak_rss_kb": 90720, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 586407549, + "status": "ok", + "result_hash": "0xc51abeaa313bb1b4", + "per_call_nanos": 73300943.625, + "peak_rss_kb": 90196, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 773343797, + "status": "ok", + "result_hash": "0x84317c79ea54c73d", + "per_call_nanos": 193335949.25, + "peak_rss_kb": 118660, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 789969984, + "status": "ok", + "result_hash": "0x84317c79ea54c73d", + "per_call_nanos": 197492496, + "peak_rss_kb": 117988, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 425698946, + "status": "ok", + "result_hash": "0x84317c79ea54c73d", + "per_call_nanos": 212849473, + "peak_rss_kb": 118136, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 758190625, + "status": "ok", + "result_hash": "0x84317c79ea54c73d", + "per_call_nanos": 189547656.25, + "peak_rss_kb": 118216, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 729597571, + "status": "ok", + "result_hash": "0x84317c79ea54c73d", + "per_call_nanos": 182399392.75, + "peak_rss_kb": 118140, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 770027469, + "status": "ok", + "result_hash": "0x84317c79ea54c73d", + "per_call_nanos": 192506867.25, + "peak_rss_kb": 118188, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 776666415, + "status": "ok", + "result_hash": "0x84317c79ea54c73d", + "per_call_nanos": 194166603.75, + "peak_rss_kb": 118300, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 867733419, + "status": "ok", + "result_hash": "0xf658068e3c5cc428", + "per_call_nanos": 433866709.5, + "peak_rss_kb": 161880, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 879653647, + "status": "ok", + "result_hash": "0xf658068e3c5cc428", + "per_call_nanos": 439826823.5, + "peak_rss_kb": 161872, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 533914161, + "status": "ok", + "result_hash": "0xf658068e3c5cc428", + "per_call_nanos": 533914161, + "peak_rss_kb": 161920, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 851704878, + "status": "ok", + "result_hash": "0xf658068e3c5cc428", + "per_call_nanos": 425852439, + "peak_rss_kb": 162044, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 838632602, + "status": "ok", + "result_hash": "0xf658068e3c5cc428", + "per_call_nanos": 419316301, + "peak_rss_kb": 164144, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 562285496, + "status": "ok", + "result_hash": "0xf658068e3c5cc428", + "per_call_nanos": 562285496, + "peak_rss_kb": 161480, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 541820987, + "status": "ok", + "result_hash": "0xf658068e3c5cc428", + "per_call_nanos": 541820987, + "peak_rss_kb": 162420, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runReducedNullspace", + "env": + {"timestamp_unix_ms": 1788156992207, + "timestamp_iso": "2026-08-31T06:16:32Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.2, + "signal_floor_multiplier": 1, + "param_schedule": + {"params": [128, 192, 256, 384, 512, 768, 1024], "kind": "custom"}, + "param_floor": 128, + "param_ceiling": 1024, + "outer_trials": 7, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 0.409621, + "c_max": 0.472263, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.069441, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 1178489.982422, + "median_per_call_nanos": 1254377.953125, + "max_per_call_nanos": 1265595.46875}, + {"relative_spread": 0.028966, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 4105378.640625, + "median_per_call_nanos": 4177664.515625, + "max_per_call_nanos": 4226388.410156}, + {"relative_spread": 0.06745, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 9365076.1875, + "median_per_call_nanos": 9935859.0625, + "max_per_call_nanos": 10035252.875}, + {"relative_spread": 0.036434, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 32403143.34375, + "median_per_call_nanos": 33247440.09375, + "max_per_call_nanos": 33614491.03125}, + {"relative_spread": 0.024422, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 78611347.875, + "median_per_call_nanos": 79283289.5, + "max_per_call_nanos": 80547603}], + "spawn_floor_nanos": 129771743, + "slope": null, + "ratios": + [[16, 306.244617], + [24, 302.203741], + [32, 303.218355], + [48, 300.631511], + [64, 302.441748]], + "points": + [{"trial_index": 0, + "total_nanos": 647984880, + "status": "ok", + "result_hash": "0x4e2c8f87de76c3a7", + "per_call_nanos": 1265595.46875, + "peak_rss_kb": 62236, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 642241512, + "status": "ok", + "result_hash": "0x4e2c8f87de76c3a7", + "per_call_nanos": 1254377.953125, + "peak_rss_kb": 62552, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 603386871, + "status": "ok", + "result_hash": "0x4e2c8f87de76c3a7", + "per_call_nanos": 1178489.982422, + "peak_rss_kb": 62232, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 525488466, + "status": "ok", + "result_hash": "0xffad94f8633f2b37", + "per_call_nanos": 4105378.640625, + "peak_rss_kb": 62488, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1081955433, + "status": "ok", + "result_hash": "0xffad94f8633f2b37", + "per_call_nanos": 4226388.410156, + "peak_rss_kb": 62236, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1069482116, + "status": "ok", + "result_hash": "0xffad94f8633f2b37", + "per_call_nanos": 4177664.515625, + "peak_rss_kb": 61880, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 642256184, + "status": "ok", + "result_hash": "0x2b3b2720a13f3247", + "per_call_nanos": 10035252.875, + "peak_rss_kb": 62776, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 635894980, + "status": "ok", + "result_hash": "0x2b3b2720a13f3247", + "per_call_nanos": 9935859.0625, + "peak_rss_kb": 62328, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 599364876, + "status": "ok", + "result_hash": "0x2b3b2720a13f3247", + "per_call_nanos": 9365076.1875, + "peak_rss_kb": 62096, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1036900587, + "status": "ok", + "result_hash": "0xa160237d0e9bd9e7", + "per_call_nanos": 32403143.34375, + "peak_rss_kb": 62604, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1075663713, + "status": "ok", + "result_hash": "0xa160237d0e9bd9e7", + "per_call_nanos": 33614491.03125, + "peak_rss_kb": 62132, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1063918083, + "status": "ok", + "result_hash": "0xa160237d0e9bd9e7", + "per_call_nanos": 33247440.09375, + "peak_rss_kb": 62520, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 644380824, + "status": "ok", + "result_hash": "0xdbb3940a7ab97687", + "per_call_nanos": 80547603, + "peak_rss_kb": 62320, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1257781566, + "status": "ok", + "result_hash": "0xdbb3940a7ab97687", + "per_call_nanos": 78611347.875, + "peak_rss_kb": 62512, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 634266316, + "status": "ok", + "result_hash": "0xdbb3940a7ab97687", + "per_call_nanos": 79283289.5, + "peak_rss_kb": 62644, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runNullspaceMatrix", + "env": + {"timestamp_unix_ms": 1788157044224, + "timestamp_iso": "2026-08-31T06:17:24Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [16, 24, 32, 48, 64], "kind": "custom"}, + "param_floor": 16, + "param_ceiling": 64, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 300.631511, + "c_max": 303.218355, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.037473, + "param": 64, + "ok_count": 5, + "min_per_call_nanos": 37647.340271, + "median_per_call_nanos": 38457.310425, + "max_per_call_nanos": 39088.436768}, + {"relative_spread": 0.057722, + "param": 96, + "ok_count": 5, + "min_per_call_nanos": 81826.564819, + "median_per_call_nanos": 86503.053101, + "max_per_call_nanos": 86819.724121}, + {"relative_spread": 0.050549, + "param": 128, + "ok_count": 5, + "min_per_call_nanos": 139599.369141, + "median_per_call_nanos": 139861.170898, + "max_per_call_nanos": 146669.223877}, + {"relative_spread": 0.102716, + "param": 192, + "ok_count": 5, + "min_per_call_nanos": 293378.140625, + "median_per_call_nanos": 320114.446289, + "max_per_call_nanos": 326258.909668}, + {"relative_spread": 0.117958, + "param": 256, + "ok_count": 5, + "min_per_call_nanos": 546710.711914, + "median_per_call_nanos": 567633.860352, + "max_per_call_nanos": 613667.71582}, + {"relative_spread": 0.056117, + "param": 384, + "ok_count": 5, + "min_per_call_nanos": 1215684.695312, + "median_per_call_nanos": 1260253.994141, + "max_per_call_nanos": 1286406.275391}, + {"relative_spread": 0.051594, + "param": 512, + "ok_count": 5, + "min_per_call_nanos": 2224685.140625, + "median_per_call_nanos": 2261338.445312, + "max_per_call_nanos": 2341356.136719}], + "spawn_floor_nanos": 82746754, + "slope": -0.034396, + "ratios": + [[64, 9.388992], + [96, 9.386182], + [128, 8.536448], + [192, 8.68366], + [256, 8.661405], + [384, 8.546644], + [512, 8.626322]], + "points": + [{"trial_index": 0, + "total_nanos": 616814023, + "status": "ok", + "result_hash": "0x9484297d12b952f9", + "per_call_nanos": 37647.340271, + "peak_rss_kb": 62328, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 625528406, + "status": "ok", + "result_hash": "0x9484297d12b952f9", + "per_call_nanos": 38179.223999, + "peak_rss_kb": 62060, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 640424948, + "status": "ok", + "result_hash": "0x9484297d12b952f9", + "per_call_nanos": 39088.436768, + "peak_rss_kb": 62728, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 630084574, + "status": "ok", + "result_hash": "0x9484297d12b952f9", + "per_call_nanos": 38457.310425, + "peak_rss_kb": 61996, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 638820289, + "status": "ok", + "result_hash": "0x9484297d12b952f9", + "per_call_nanos": 38990.496155, + "peak_rss_kb": 62628, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 711227180, + "status": "ok", + "result_hash": "0xb09b8a5cc8cbb245", + "per_call_nanos": 86819.724121, + "peak_rss_kb": 62896, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 708633011, + "status": "ok", + "result_hash": "0xb09b8a5cc8cbb245", + "per_call_nanos": 86503.053101, + "peak_rss_kb": 62868, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 709089179, + "status": "ok", + "result_hash": "0xb09b8a5cc8cbb245", + "per_call_nanos": 86558.737671, + "peak_rss_kb": 62400, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 1340646438, + "status": "ok", + "result_hash": "0xb09b8a5cc8cbb245", + "per_call_nanos": 81826.564819, + "peak_rss_kb": 62824, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 701415158, + "status": "ok", + "result_hash": "0xb09b8a5cc8cbb245", + "per_call_nanos": 85621.967529, + "peak_rss_kb": 64272, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 572871356, + "status": "ok", + "result_hash": "0xb064646f5f91604d", + "per_call_nanos": 139861.170898, + "peak_rss_kb": 63336, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 571946544, + "status": "ok", + "result_hash": "0xb064646f5f91604d", + "per_call_nanos": 139635.386719, + "peak_rss_kb": 62956, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 571799016, + "status": "ok", + "result_hash": "0xb064646f5f91604d", + "per_call_nanos": 139599.369141, + "peak_rss_kb": 62788, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 600757141, + "status": "ok", + "result_hash": "0xb064646f5f91604d", + "per_call_nanos": 146669.223877, + "peak_rss_kb": 63136, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 593917168, + "status": "ok", + "result_hash": "0xb064646f5f91604d", + "per_call_nanos": 144999.308594, + "peak_rss_kb": 63500, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 655594386, + "status": "ok", + "result_hash": "0x77aac10cdfd0d344", + "per_call_nanos": 320114.446289, + "peak_rss_kb": 64952, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 600838432, + "status": "ok", + "result_hash": "0x77aac10cdfd0d344", + "per_call_nanos": 293378.140625, + "peak_rss_kb": 65044, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 668178247, + "status": "ok", + "result_hash": "0x77aac10cdfd0d344", + "per_call_nanos": 326258.909668, + "peak_rss_kb": 64692, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 621847579, + "status": "ok", + "result_hash": "0x77aac10cdfd0d344", + "per_call_nanos": 303636.513184, + "peak_rss_kb": 64748, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 658374038, + "status": "ok", + "result_hash": "0x77aac10cdfd0d344", + "per_call_nanos": 321471.698242, + "peak_rss_kb": 65144, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1119663538, + "status": "ok", + "result_hash": "0x51b25dc04eb5f295", + "per_call_nanos": 546710.711914, + "peak_rss_kb": 67044, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 561004367, + "status": "ok", + "result_hash": "0x51b25dc04eb5f295", + "per_call_nanos": 547855.827148, + "peak_rss_kb": 67532, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 581257073, + "status": "ok", + "result_hash": "0x51b25dc04eb5f295", + "per_call_nanos": 567633.860352, + "peak_rss_kb": 67464, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 628395741, + "status": "ok", + "result_hash": "0x51b25dc04eb5f295", + "per_call_nanos": 613667.71582, + "peak_rss_kb": 67364, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 624648313, + "status": "ok", + "result_hash": "0x51b25dc04eb5f295", + "per_call_nanos": 610008.118164, + "peak_rss_kb": 67072, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 645250045, + "status": "ok", + "result_hash": "0xfa944deda3d8305a", + "per_call_nanos": 1260253.994141, + "peak_rss_kb": 73512, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 657004297, + "status": "ok", + "result_hash": "0xfa944deda3d8305a", + "per_call_nanos": 1283211.517578, + "peak_rss_kb": 74088, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 658640013, + "status": "ok", + "result_hash": "0xfa944deda3d8305a", + "per_call_nanos": 1286406.275391, + "peak_rss_kb": 73648, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 634820639, + "status": "ok", + "result_hash": "0xfa944deda3d8305a", + "per_call_nanos": 1239884.060547, + "peak_rss_kb": 74444, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 622430564, + "status": "ok", + "result_hash": "0xfa944deda3d8305a", + "per_call_nanos": 1215684.695312, + "peak_rss_kb": 75652, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 569519396, + "status": "ok", + "result_hash": "0x67762b97afe5e44c", + "per_call_nanos": 2224685.140625, + "peak_rss_kb": 82952, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 582486036, + "status": "ok", + "result_hash": "0x67762b97afe5e44c", + "per_call_nanos": 2275336.078125, + "peak_rss_kb": 83220, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 599387171, + "status": "ok", + "result_hash": "0x67762b97afe5e44c", + "per_call_nanos": 2341356.136719, + "peak_rss_kb": 82676, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 578902642, + "status": "ok", + "result_hash": "0x67762b97afe5e44c", + "per_call_nanos": 2261338.445312, + "peak_rss_kb": 82996, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 569758491, + "status": "ok", + "result_hash": "0x67762b97afe5e44c", + "per_call_nanos": 2225619.105469, + "peak_rss_kb": 82976, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runFreeCols", + "env": + {"timestamp_unix_ms": 1788157058675, + "timestamp_iso": "2026-08-31T06:17:38Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": + {"params": [64, 96, 128, 192, 256, 384, 512], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 512, + "outer_trials": 5, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 2", + "c_min": 8.536448, + "c_max": 9.386182, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.053316, + "param": 8, + "ok_count": 3, + "min_per_call_nanos": 457659.003418, + "median_per_call_nanos": 459116.844238, + "max_per_call_nanos": 482137.390137}, + {"relative_spread": 0.060663, + "param": 12, + "ok_count": 3, + "min_per_call_nanos": 1474122.962891, + "median_per_call_nanos": 1551347.078125, + "max_per_call_nanos": 1568231.767578}, + {"relative_spread": 0.037629, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 3489169.847656, + "median_per_call_nanos": 3530538.265625, + "max_per_call_nanos": 3622019.992188}, + {"relative_spread": 0.029646, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 11813237.515625, + "median_per_call_nanos": 12005873.484375, + "max_per_call_nanos": 12169160.65625}, + {"relative_spread": 0.024175, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 28269530.75, + "median_per_call_nanos": 28411419.59375, + "max_per_call_nanos": 28956379.96875}, + {"relative_spread": 0.094604, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 88566898.5, + "median_per_call_nanos": 93608004.75, + "max_per_call_nanos": 97422614.375}, + {"relative_spread": 0.051941, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 227474366, + "median_per_call_nanos": 237323201.75, + "max_per_call_nanos": 239801251.5}], + "spawn_floor_nanos": 141098611, + "slope": -0.001571, + "ratios": + [[8, 896.712586], + [12, 897.7703], + [16, 861.947819], + [24, 868.480431], + [32, 867.047717], + [48, 846.426548], + [64, 905.316169]], + "points": + [{"trial_index": 0, + "total_nanos": 940271297, + "status": "ok", + "result_hash": "0x1065efcc0455bc23", + "per_call_nanos": 459116.844238, + "peak_rss_kb": 63572, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 937285639, + "status": "ok", + "result_hash": "0x1065efcc0455bc23", + "per_call_nanos": 457659.003418, + "peak_rss_kb": 61736, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 987417375, + "status": "ok", + "result_hash": "0x1065efcc0455bc23", + "per_call_nanos": 482137.390137, + "peak_rss_kb": 61756, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 794289704, + "status": "ok", + "result_hash": "0x6039d413f9ed9863", + "per_call_nanos": 1551347.078125, + "peak_rss_kb": 61680, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 754750957, + "status": "ok", + "result_hash": "0x6039d413f9ed9863", + "per_call_nanos": 1474122.962891, + "peak_rss_kb": 62332, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 802934665, + "status": "ok", + "result_hash": "0x6039d413f9ed9863", + "per_call_nanos": 1568231.767578, + "peak_rss_kb": 61688, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 903817796, + "status": "ok", + "result_hash": "0x438f83967baafea3", + "per_call_nanos": 3530538.265625, + "peak_rss_kb": 62000, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 927237118, + "status": "ok", + "result_hash": "0x438f83967baafea3", + "per_call_nanos": 3622019.992188, + "peak_rss_kb": 61756, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 893227481, + "status": "ok", + "result_hash": "0x438f83967baafea3", + "per_call_nanos": 3489169.847656, + "peak_rss_kb": 61876, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 778826282, + "status": "ok", + "result_hash": "0x479f66782e422b23", + "per_call_nanos": 12169160.65625, + "peak_rss_kb": 63636, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 768375903, + "status": "ok", + "result_hash": "0x479f66782e422b23", + "per_call_nanos": 12005873.484375, + "peak_rss_kb": 61808, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 756047201, + "status": "ok", + "result_hash": "0x479f66782e422b23", + "per_call_nanos": 11813237.515625, + "peak_rss_kb": 61692, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 909165427, + "status": "ok", + "result_hash": "0x6ec62897f43401a3", + "per_call_nanos": 28411419.59375, + "peak_rss_kb": 62196, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 926604159, + "status": "ok", + "result_hash": "0x6ec62897f43401a3", + "per_call_nanos": 28956379.96875, + "peak_rss_kb": 62032, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 904624984, + "status": "ok", + "result_hash": "0x6ec62897f43401a3", + "per_call_nanos": 28269530.75, + "peak_rss_kb": 62064, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 748864038, + "status": "ok", + "result_hash": "0xcd03ccb2fe54b8a3", + "per_call_nanos": 93608004.75, + "peak_rss_kb": 61992, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 779380915, + "status": "ok", + "result_hash": "0xcd03ccb2fe54b8a3", + "per_call_nanos": 97422614.375, + "peak_rss_kb": 61964, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 708535188, + "status": "ok", + "result_hash": "0xcd03ccb2fe54b8a3", + "per_call_nanos": 88566898.5, + "peak_rss_kb": 62076, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 949292807, + "status": "ok", + "result_hash": "0x6bce22c2e40f0ba3", + "per_call_nanos": 237323201.75, + "peak_rss_kb": 62772, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 959205006, + "status": "ok", + "result_hash": "0x6bce22c2e40f0ba3", + "per_call_nanos": 239801251.5, + "peak_rss_kb": 62712, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 909897464, + "status": "ok", + "result_hash": "0x6bce22c2e40f0ba3", + "per_call_nanos": 227474366, + "peak_rss_kb": 62156, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runSpanContains", + "env": + {"timestamp_unix_ms": 1788157089105, + "timestamp_iso": "2026-08-31T06:18:09Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [8, 12, 16, 24, 32, 48, 64], "kind": "custom"}, + "param_floor": 8, + "param_ceiling": 64, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 846.426548, + "c_max": 905.316169, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.024449, + "param": 8, + "ok_count": 3, + "min_per_call_nanos": 433519.968262, + "median_per_call_nanos": 441573.297852, + "max_per_call_nanos": 444316.208496}, + {"relative_spread": 0.038066, + "param": 12, + "ok_count": 3, + "min_per_call_nanos": 1393334.914062, + "median_per_call_nanos": 1444717.460938, + "max_per_call_nanos": 1448329.558594}, + {"relative_spread": 0.030992, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 3374858.09375, + "median_per_call_nanos": 3393983.996094, + "max_per_call_nanos": 3480042.957031}, + {"relative_spread": 0.074159, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 10565290.53125, + "median_per_call_nanos": 11339191.0625, + "max_per_call_nanos": 11406198.5625}, + {"relative_spread": 0.102669, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 25554604.46875, + "median_per_call_nanos": 27027107.3125, + "max_per_call_nanos": 28329454.9375}, + {"relative_spread": 0.083237, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 87498132.625, + "median_per_call_nanos": 88785473, + "max_per_call_nanos": 94888356.125}, + {"relative_spread": 0.084884, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 210163282.25, + "median_per_call_nanos": 219502138.25, + "max_per_call_nanos": 228795445.25}], + "spawn_floor_nanos": 246834489, + "slope": -0.007479, + "ratios": + [[8, 862.447847], + [12, 836.063345], + [16, 828.609374], + [24, 820.253983], + [32, 824.801859], + [48, 802.820032], + [64, 837.334207]], + "points": + [{"trial_index": 0, + "total_nanos": 909959595, + "status": "ok", + "result_hash": "0x8dd16324c890a087", + "per_call_nanos": 444316.208496, + "peak_rss_kb": 62204, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 904342114, + "status": "ok", + "result_hash": "0x8dd16324c890a087", + "per_call_nanos": 441573.297852, + "peak_rss_kb": 61748, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 887848895, + "status": "ok", + "result_hash": "0x8dd16324c890a087", + "per_call_nanos": 433519.968262, + "peak_rss_kb": 61348, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 741544734, + "status": "ok", + "result_hash": "0x83aaf6087330e6e5", + "per_call_nanos": 1448329.558594, + "peak_rss_kb": 61240, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 739695340, + "status": "ok", + "result_hash": "0x83aaf6087330e6e5", + "per_call_nanos": 1444717.460938, + "peak_rss_kb": 61164, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 713387476, + "status": "ok", + "result_hash": "0x83aaf6087330e6e5", + "per_call_nanos": 1393334.914062, + "peak_rss_kb": 61656, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 890890997, + "status": "ok", + "result_hash": "0xfbb343d5769cc58a", + "per_call_nanos": 3480042.957031, + "peak_rss_kb": 61940, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 868859903, + "status": "ok", + "result_hash": "0xfbb343d5769cc58a", + "per_call_nanos": 3393983.996094, + "peak_rss_kb": 62220, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 863963672, + "status": "ok", + "result_hash": "0xfbb343d5769cc58a", + "per_call_nanos": 3374858.09375, + "peak_rss_kb": 61052, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 676178594, + "status": "ok", + "result_hash": "0xcf117583bcce8037", + "per_call_nanos": 10565290.53125, + "peak_rss_kb": 61480, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 725708228, + "status": "ok", + "result_hash": "0xcf117583bcce8037", + "per_call_nanos": 11339191.0625, + "peak_rss_kb": 60844, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 729996708, + "status": "ok", + "result_hash": "0xcf117583bcce8037", + "per_call_nanos": 11406198.5625, + "peak_rss_kb": 60540, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 817747343, + "status": "ok", + "result_hash": "0x91727b1d6fcaaa2", + "per_call_nanos": 25554604.46875, + "peak_rss_kb": 61116, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 864867434, + "status": "ok", + "result_hash": "0x91727b1d6fcaaa2", + "per_call_nanos": 27027107.3125, + "peak_rss_kb": 62280, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 906542558, + "status": "ok", + "result_hash": "0x91727b1d6fcaaa2", + "per_call_nanos": 28329454.9375, + "peak_rss_kb": 61400, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 710283784, + "status": "ok", + "result_hash": "0x2eb27e4723a69417", + "per_call_nanos": 88785473, + "peak_rss_kb": 62236, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 699985061, + "status": "ok", + "result_hash": "0x2eb27e4723a69417", + "per_call_nanos": 87498132.625, + "peak_rss_kb": 63980, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 759106849, + "status": "ok", + "result_hash": "0x2eb27e4723a69417", + "per_call_nanos": 94888356.125, + "peak_rss_kb": 61264, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 915181781, + "status": "ok", + "result_hash": "0x86fbf40ff2c9d2e5", + "per_call_nanos": 228795445.25, + "peak_rss_kb": 61524, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 840653129, + "status": "ok", + "result_hash": "0x86fbf40ff2c9d2e5", + "per_call_nanos": 210163282.25, + "peak_rss_kb": 61804, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 878008553, + "status": "ok", + "result_hash": "0x86fbf40ff2c9d2e5", + "per_call_nanos": 219502138.25, + "peak_rss_kb": 61520, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runReduce", + "env": + {"timestamp_unix_ms": 1788157110971, + "timestamp_iso": "2026-08-31T06:18:30Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [8, 12, 16, 24, 32, 48, 64], "kind": "custom"}, + "param_floor": 8, + "param_ceiling": 64, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 802.820032, + "c_max": 837.334207, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.013884, + "param": 8, + "ok_count": 3, + "min_per_call_nanos": 475274.867188, + "median_per_call_nanos": 477500.932617, + "max_per_call_nanos": 481904.262695}, + {"relative_spread": 0.042051, + "param": 12, + "ok_count": 3, + "min_per_call_nanos": 1523042.994141, + "median_per_call_nanos": 1562825.060547, + "max_per_call_nanos": 1588761.662109}, + {"relative_spread": 0.032024, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 3497742.964844, + "median_per_call_nanos": 3573165.871094, + "max_per_call_nanos": 3612171.703125}, + {"relative_spread": 0.022861, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 11392020.421875, + "median_per_call_nanos": 11517121.84375, + "max_per_call_nanos": 11655317.5625}, + {"relative_spread": 0.013541, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 27367501.84375, + "median_per_call_nanos": 27405122.84375, + "max_per_call_nanos": 27738586.90625}, + {"relative_spread": 0.0292, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 92804583.75, + "median_per_call_nanos": 93474068.5, + "max_per_call_nanos": 95534046}, + {"relative_spread": 0.05866, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 215135371.75, + "median_per_call_nanos": 221073431.5, + "max_per_call_nanos": 228103492.75}], + "spawn_floor_nanos": 76225825, + "slope": -0.036823, + "ratios": + [[8, 932.619009], + [12, 904.412651], + [16, 872.354949], + [24, 833.125133], + [32, 836.337977], + [48, 845.215463], + [64, 843.328215]], + "points": + [{"trial_index": 0, + "total_nanos": 986939930, + "status": "ok", + "result_hash": "0x8a103335a16afaa4", + "per_call_nanos": 481904.262695, + "peak_rss_kb": 61312, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 977921910, + "status": "ok", + "result_hash": "0x8a103335a16afaa4", + "per_call_nanos": 477500.932617, + "peak_rss_kb": 61312, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 973362928, + "status": "ok", + "result_hash": "0x8a103335a16afaa4", + "per_call_nanos": 475274.867188, + "peak_rss_kb": 63860, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 800166431, + "status": "ok", + "result_hash": "0x9cafbcbf2b3446f0", + "per_call_nanos": 1562825.060547, + "peak_rss_kb": 61376, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 779798013, + "status": "ok", + "result_hash": "0x9cafbcbf2b3446f0", + "per_call_nanos": 1523042.994141, + "peak_rss_kb": 61396, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 813445971, + "status": "ok", + "result_hash": "0x9cafbcbf2b3446f0", + "per_call_nanos": 1588761.662109, + "peak_rss_kb": 61056, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 895422199, + "status": "ok", + "result_hash": "0x66073de01e322657", + "per_call_nanos": 3497742.964844, + "peak_rss_kb": 61564, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 924715956, + "status": "ok", + "result_hash": "0x66073de01e322657", + "per_call_nanos": 3612171.703125, + "peak_rss_kb": 61028, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 914730463, + "status": "ok", + "result_hash": "0x66073de01e322657", + "per_call_nanos": 3573165.871094, + "peak_rss_kb": 61012, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 737095798, + "status": "ok", + "result_hash": "0x1dcf5f5296c9e1ac", + "per_call_nanos": 11517121.84375, + "peak_rss_kb": 61392, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 186485081, + "status": "ok", + "result_hash": "0x1dcf5f5296c9e1ac", + "per_call_nanos": 11655317.5625, + "peak_rss_kb": 61592, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 729089307, + "status": "ok", + "result_hash": "0x1dcf5f5296c9e1ac", + "per_call_nanos": 11392020.421875, + "peak_rss_kb": 61400, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 887634781, + "status": "ok", + "result_hash": "0x63cfe3b2edf6881a", + "per_call_nanos": 27738586.90625, + "peak_rss_kb": 61076, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 876963931, + "status": "ok", + "result_hash": "0x63cfe3b2edf6881a", + "per_call_nanos": 27405122.84375, + "peak_rss_kb": 61124, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 875760059, + "status": "ok", + "result_hash": "0x63cfe3b2edf6881a", + "per_call_nanos": 27367501.84375, + "peak_rss_kb": 61108, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 742436670, + "status": "ok", + "result_hash": "0x6ef79315ccdc0f94", + "per_call_nanos": 92804583.75, + "peak_rss_kb": 61400, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 747792548, + "status": "ok", + "result_hash": "0x6ef79315ccdc0f94", + "per_call_nanos": 93474068.5, + "peak_rss_kb": 61280, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 764272368, + "status": "ok", + "result_hash": "0x6ef79315ccdc0f94", + "per_call_nanos": 95534046, + "peak_rss_kb": 61048, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 860541487, + "status": "ok", + "result_hash": "0xde6205814db5eb68", + "per_call_nanos": 215135371.75, + "peak_rss_kb": 61720, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 912413971, + "status": "ok", + "result_hash": "0xde6205814db5eb68", + "per_call_nanos": 228103492.75, + "peak_rss_kb": 61816, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 884293726, + "status": "ok", + "result_hash": "0xde6205814db5eb68", + "per_call_nanos": 221073431.5, + "peak_rss_kb": 61104, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runSpanCoeffs", + "env": + {"timestamp_unix_ms": 1788157133132, + "timestamp_iso": "2026-08-31T06:18:53Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [8, 12, 16, 24, 32, 48, 64], "kind": "custom"}, + "param_floor": 8, + "param_ceiling": 64, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 833.125133, + "c_max": 904.412651, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.079611, + "param": 128, + "ok_count": 5, + "min_per_call_nanos": 16814.486908, + "median_per_call_nanos": 17503.118439, + "max_per_call_nanos": 18207.933441}, + {"relative_spread": 0.04522, + "param": 192, + "ok_count": 5, + "min_per_call_nanos": 24967.776123, + "median_per_call_nanos": 25968.944305, + "max_per_call_nanos": 26142.092041}, + {"relative_spread": 0.1102, + "param": 256, + "ok_count": 5, + "min_per_call_nanos": 34977.441833, + "median_per_call_nanos": 35356.735443, + "max_per_call_nanos": 38873.749207}, + {"relative_spread": 0.144913, + "param": 384, + "ok_count": 5, + "min_per_call_nanos": 50210.515137, + "median_per_call_nanos": 53468.017822, + "max_per_call_nanos": 57958.740417}, + {"relative_spread": 0.099306, + "param": 512, + "ok_count": 5, + "min_per_call_nanos": 68656.065125, + "median_per_call_nanos": 73244.816162, + "max_per_call_nanos": 75929.704834}, + {"relative_spread": 0.190007, + "param": 768, + "ok_count": 5, + "min_per_call_nanos": 107064.061401, + "median_per_call_nanos": 116932.713623, + "max_per_call_nanos": 129282.122925}], + "spawn_floor_nanos": 218790905, + "slope": 0.07883, + "ratios": + [[128, 136.743113], + [192, 135.254918], + [256, 138.112248], + [384, 139.23963], + [512, 143.056282], + [768, 152.256138]], + "points": + [{"trial_index": 0, + "total_nanos": 1124256455, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 17154.792099, + "peak_rss_kb": 61764, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 65536, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 596637563, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 18207.933441, + "peak_rss_kb": 63260, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1101954214, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 16814.486908, + "peak_rss_kb": 61972, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 65536, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 1174615703, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 17923.213242, + "peak_rss_kb": 62272, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 65536, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 573542185, + "status": "ok", + "result_hash": "0x585a2447d23193e4", + "per_call_nanos": 17503.118439, + "peak_rss_kb": 61764, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 842734507, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 25718.216156, + "peak_rss_kb": 63588, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 855806038, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 26117.127625, + "peak_rss_kb": 63868, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 856624072, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 26142.092041, + "peak_rss_kb": 64000, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 850950367, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 25968.944305, + "peak_rss_kb": 63384, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 818144088, + "status": "ok", + "result_hash": "0xdfd81e8422ecaf64", + "per_call_nanos": 24967.776123, + "peak_rss_kb": 63988, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 636907507, + "status": "ok", + "result_hash": "0xec95a143dd78cae4", + "per_call_nanos": 38873.749207, + "peak_rss_kb": 65656, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1158569507, + "status": "ok", + "result_hash": "0xec95a143dd78cae4", + "per_call_nanos": 35356.735443, + "peak_rss_kb": 65116, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 589532210, + "status": "ok", + "result_hash": "0xec95a143dd78cae4", + "per_call_nanos": 35982.190552, + "peak_rss_kb": 65300, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 1146140814, + "status": "ok", + "result_hash": "0xec95a143dd78cae4", + "per_call_nanos": 34977.441833, + "peak_rss_kb": 64156, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 286855090, + "status": "ok", + "result_hash": "0xec95a143dd78cae4", + "per_call_nanos": 35016.490479, + "peak_rss_kb": 65236, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 435743610, + "status": "ok", + "result_hash": "0x862b6ce437f881e4", + "per_call_nanos": 53191.358643, + "peak_rss_kb": 72220, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 949596003, + "status": "ok", + "result_hash": "0x862b6ce437f881e4", + "per_call_nanos": 57958.740417, + "peak_rss_kb": 71152, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 877317733, + "status": "ok", + "result_hash": "0x862b6ce437f881e4", + "per_call_nanos": 53547.224915, + "peak_rss_kb": 71460, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 876020004, + "status": "ok", + "result_hash": "0x862b6ce437f881e4", + "per_call_nanos": 53468.017822, + "peak_rss_kb": 70824, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 411324540, + "status": "ok", + "result_hash": "0x862b6ce437f881e4", + "per_call_nanos": 50210.515137, + "peak_rss_kb": 72176, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1209033966, + "status": "ok", + "result_hash": "0xbdcf04ae775718e4", + "per_call_nanos": 73793.577026, + "peak_rss_kb": 79156, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1200043068, + "status": "ok", + "result_hash": "0xbdcf04ae775718e4", + "per_call_nanos": 73244.816162, + "peak_rss_kb": 78352, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1153310474, + "status": "ok", + "result_hash": "0xbdcf04ae775718e4", + "per_call_nanos": 70392.484985, + "peak_rss_kb": 78764, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 1124860971, + "status": "ok", + "result_hash": "0xbdcf04ae775718e4", + "per_call_nanos": 68656.065125, + "peak_rss_kb": 78848, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 622016142, + "status": "ok", + "result_hash": "0xbdcf04ae775718e4", + "per_call_nanos": 75929.704834, + "peak_rss_kb": 79232, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1059079151, + "status": "ok", + "result_hash": "0x763bbac1633fc6e4", + "per_call_nanos": 129282.122925, + "peak_rss_kb": 106672, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 1029771977, + "status": "ok", + "result_hash": "0x763bbac1633fc6e4", + "per_call_nanos": 125704.587036, + "peak_rss_kb": 103952, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 877068791, + "status": "ok", + "result_hash": "0x763bbac1633fc6e4", + "per_call_nanos": 107064.061401, + "peak_rss_kb": 103656, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 957912790, + "status": "ok", + "result_hash": "0x763bbac1633fc6e4", + "per_call_nanos": 116932.713623, + "peak_rss_kb": 104604, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 909728332, + "status": "ok", + "result_hash": "0x763bbac1633fc6e4", + "per_call_nanos": 111050.821777, + "peak_rss_kb": 105184, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runEchelonCoeffs", + "env": + {"timestamp_unix_ms": 1788157154048, + "timestamp_iso": "2026-08-31T06:19:14Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": + {"params": [128, 192, 256, 384, 512, 768], "kind": "custom"}, + "param_floor": 128, + "param_ceiling": 768, + "outer_trials": 5, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n", + "c_min": 135.254918, + "c_max": 152.256138, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.08135, + "param": 128, + "ok_count": 7, + "min_per_call_nanos": 1222091.402344, + "median_per_call_nanos": 1266949.365234, + "max_per_call_nanos": 1325158.021484}, + {"relative_spread": 0.116345, + "param": 192, + "ok_count": 7, + "min_per_call_nanos": 3576060.976562, + "median_per_call_nanos": 3764796.984375, + "max_per_call_nanos": 4014075.125}, + {"relative_spread": 0.165759, + "param": 256, + "ok_count": 7, + "min_per_call_nanos": 7526131.0625, + "median_per_call_nanos": 7917877.1875, + "max_per_call_nanos": 8838587.5}, + {"relative_spread": 0.105076, + "param": 384, + "ok_count": 7, + "min_per_call_nanos": 24681911.46875, + "median_per_call_nanos": 25200516.75, + "max_per_call_nanos": 27329882.78125}, + {"relative_spread": 0.304065, + "param": 512, + "ok_count": 7, + "min_per_call_nanos": 56532103.4375, + "median_per_call_nanos": 61417867.125, + "max_per_call_nanos": 75207124.375}, + {"relative_spread": 0.219111, + "param": 768, + "ok_count": 7, + "min_per_call_nanos": 175493922.75, + "median_per_call_nanos": 182785861.5, + "max_per_call_nanos": 215544317}, + {"relative_spread": 0.075722, + "param": 1024, + "ok_count": 7, + "min_per_call_nanos": 394031916.5, + "median_per_call_nanos": 419480075, + "max_per_call_nanos": 425795669.5}], + "spawn_floor_nanos": 77649644, + "slope": -0.166352, + "ratios": + [[128, 0.604129], + [192, 0.53191], + [256, 0.471942], + [384, 0.445057], + [512, 0.457599], + [768, 0.403514], + [1024, 0.390671]], + "points": + [{"trial_index": 0, + "total_nanos": 662474195, + "status": "ok", + "result_hash": "0xc0da4d3c0954ded5", + "per_call_nanos": 1293894.912109, + "peak_rss_kb": 61260, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 625710798, + "status": "ok", + "result_hash": "0xc0da4d3c0954ded5", + "per_call_nanos": 1222091.402344, + "peak_rss_kb": 61752, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 641339199, + "status": "ok", + "result_hash": "0xc0da4d3c0954ded5", + "per_call_nanos": 1252615.623047, + "peak_rss_kb": 61456, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 678480907, + "status": "ok", + "result_hash": "0xc0da4d3c0954ded5", + "per_call_nanos": 1325158.021484, + "peak_rss_kb": 61640, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 648678075, + "status": "ok", + "result_hash": "0xc0da4d3c0954ded5", + "per_call_nanos": 1266949.365234, + "peak_rss_kb": 61152, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 664900736, + "status": "ok", + "result_hash": "0xc0da4d3c0954ded5", + "per_call_nanos": 1298634.25, + "peak_rss_kb": 62056, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 645769176, + "status": "ok", + "result_hash": "0xc0da4d3c0954ded5", + "per_call_nanos": 1261267.921875, + "peak_rss_kb": 62332, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 915512594, + "status": "ok", + "result_hash": "0xafb3e3f148207aa9", + "per_call_nanos": 3576221.070312, + "peak_rss_kb": 63932, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 928724495, + "status": "ok", + "result_hash": "0xafb3e3f148207aa9", + "per_call_nanos": 3627830.058594, + "peak_rss_kb": 63696, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 128450404, + "status": "ok", + "result_hash": "0xafb3e3f148207aa9", + "per_call_nanos": 4014075.125, + "peak_rss_kb": 64300, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 481894014, + "status": "ok", + "result_hash": "0xafb3e3f148207aa9", + "per_call_nanos": 3764796.984375, + "peak_rss_kb": 63980, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 127100023, + "status": "ok", + "result_hash": "0xafb3e3f148207aa9", + "per_call_nanos": 3971875.71875, + "peak_rss_kb": 63500, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 915471610, + "status": "ok", + "result_hash": "0xafb3e3f148207aa9", + "per_call_nanos": 3576060.976562, + "peak_rss_kb": 64512, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 497126297, + "status": "ok", + "result_hash": "0xafb3e3f148207aa9", + "per_call_nanos": 3883799.195312, + "peak_rss_kb": 63656, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 240836194, + "status": "ok", + "result_hash": "0xd059245864275e8c", + "per_call_nanos": 7526131.0625, + "peak_rss_kb": 66740, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 250978764, + "status": "ok", + "result_hash": "0xd059245864275e8c", + "per_call_nanos": 7843086.375, + "peak_rss_kb": 67028, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 260058279, + "status": "ok", + "result_hash": "0xd059245864275e8c", + "per_call_nanos": 8126821.21875, + "peak_rss_kb": 66940, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 261099292, + "status": "ok", + "result_hash": "0xd059245864275e8c", + "per_call_nanos": 8159352.875, + "peak_rss_kb": 67296, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 253372070, + "status": "ok", + "result_hash": "0xd059245864275e8c", + "per_call_nanos": 7917877.1875, + "peak_rss_kb": 66236, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 70708700, + "status": "ok", + "result_hash": "0xd059245864275e8c", + "per_call_nanos": 8838587.5, + "peak_rss_kb": 67244, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 124622884, + "status": "ok", + "result_hash": "0xd059245864275e8c", + "per_call_nanos": 7788930.25, + "peak_rss_kb": 66448, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 874556249, + "status": "ok", + "result_hash": "0xd534ce16d5fde84c", + "per_call_nanos": 27329882.78125, + "peak_rss_kb": 74524, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 806416536, + "status": "ok", + "result_hash": "0xd534ce16d5fde84c", + "per_call_nanos": 25200516.75, + "peak_rss_kb": 75908, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 400660433, + "status": "ok", + "result_hash": "0xd534ce16d5fde84c", + "per_call_nanos": 25041277.0625, + "peak_rss_kb": 73740, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 789821167, + "status": "ok", + "result_hash": "0xd534ce16d5fde84c", + "per_call_nanos": 24681911.46875, + "peak_rss_kb": 73968, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 802039034, + "status": "ok", + "result_hash": "0xd534ce16d5fde84c", + "per_call_nanos": 25063719.8125, + "peak_rss_kb": 74128, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 828566326, + "status": "ok", + "result_hash": "0xd534ce16d5fde84c", + "per_call_nanos": 25892697.6875, + "peak_rss_kb": 74468, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 856165656, + "status": "ok", + "result_hash": "0xd534ce16d5fde84c", + "per_call_nanos": 26755176.75, + "peak_rss_kb": 74484, + "part_of_verdict": true, + "param": 384, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 491342937, + "status": "ok", + "result_hash": "0x1c721a486cd1cef8", + "per_call_nanos": 61417867.125, + "peak_rss_kb": 90264, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 904513655, + "status": "ok", + "result_hash": "0x1c721a486cd1cef8", + "per_call_nanos": 56532103.4375, + "peak_rss_kb": 88364, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 469170132, + "status": "ok", + "result_hash": "0x1c721a486cd1cef8", + "per_call_nanos": 58646266.5, + "peak_rss_kb": 89496, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 1095940850, + "status": "ok", + "result_hash": "0x1c721a486cd1cef8", + "per_call_nanos": 68496303.125, + "peak_rss_kb": 89036, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 926786676, + "status": "ok", + "result_hash": "0x1c721a486cd1cef8", + "per_call_nanos": 57924167.25, + "peak_rss_kb": 88184, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 522341358, + "status": "ok", + "result_hash": "0x1c721a486cd1cef8", + "per_call_nanos": 65292669.75, + "peak_rss_kb": 89588, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 601656995, + "status": "ok", + "result_hash": "0x1c721a486cd1cef8", + "per_call_nanos": 75207124.375, + "peak_rss_kb": 90416, + "part_of_verdict": true, + "param": 512, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 431088634, + "status": "ok", + "result_hash": "0x183b262626ac8d32", + "per_call_nanos": 215544317, + "peak_rss_kb": 116692, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 769783071, + "status": "ok", + "result_hash": "0x183b262626ac8d32", + "per_call_nanos": 192445767.75, + "peak_rss_kb": 115612, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 701975691, + "status": "ok", + "result_hash": "0x183b262626ac8d32", + "per_call_nanos": 175493922.75, + "peak_rss_kb": 116380, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 731143446, + "status": "ok", + "result_hash": "0x183b262626ac8d32", + "per_call_nanos": 182785861.5, + "peak_rss_kb": 115884, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 754804513, + "status": "ok", + "result_hash": "0x183b262626ac8d32", + "per_call_nanos": 188701128.25, + "peak_rss_kb": 115748, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 724274222, + "status": "ok", + "result_hash": "0x183b262626ac8d32", + "per_call_nanos": 181068555.5, + "peak_rss_kb": 116544, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 712161244, + "status": "ok", + "result_hash": "0x183b262626ac8d32", + "per_call_nanos": 178040311, + "peak_rss_kb": 116348, + "part_of_verdict": true, + "param": 768, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 851591339, + "status": "ok", + "result_hash": "0xa1b9ddea5404354a", + "per_call_nanos": 425795669.5, + "peak_rss_kb": 161892, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 788063833, + "status": "ok", + "result_hash": "0xa1b9ddea5404354a", + "per_call_nanos": 394031916.5, + "peak_rss_kb": 157452, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 843676190, + "status": "ok", + "result_hash": "0xa1b9ddea5404354a", + "per_call_nanos": 421838095, + "peak_rss_kb": 161824, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 3, + "total_nanos": 842181478, + "status": "ok", + "result_hash": "0xa1b9ddea5404354a", + "per_call_nanos": 421090739, + "peak_rss_kb": 161188, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 4, + "total_nanos": 804232775, + "status": "ok", + "result_hash": "0xa1b9ddea5404354a", + "per_call_nanos": 402116387.5, + "peak_rss_kb": 160384, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 5, + "total_nanos": 838960150, + "status": "ok", + "result_hash": "0xa1b9ddea5404354a", + "per_call_nanos": 419480075, + "peak_rss_kb": 159552, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 6, + "total_nanos": 804916133, + "status": "ok", + "result_hash": "0xa1b9ddea5404354a", + "per_call_nanos": 402458066.5, + "peak_rss_kb": 159504, + "part_of_verdict": true, + "param": 1024, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runReducedMatrix", + "env": + {"timestamp_unix_ms": 1788157190703, + "timestamp_iso": "2026-08-31T06:19:50Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.2, + "signal_floor_multiplier": 1, + "param_schedule": + {"params": [128, 192, 256, 384, 512, 768, 1024], "kind": "custom"}, + "param_floor": 128, + "param_ceiling": 1024, + "outer_trials": 7, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 0.390671, + "c_max": 0.53191, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0.005146, + "param": 8, + "ok_count": 3, + "min_per_call_nanos": 164936.833496, + "median_per_call_nanos": 165225.730469, + "max_per_call_nanos": 165787.160889}, + {"relative_spread": 0.018699, + "param": 12, + "ok_count": 3, + "min_per_call_nanos": 553814.164062, + "median_per_call_nanos": 559988.982422, + "max_per_call_nanos": 564285.536133}, + {"relative_spread": 0.05428, + "param": 16, + "ok_count": 3, + "min_per_call_nanos": 1244236.177734, + "median_per_call_nanos": 1299981.503906, + "max_per_call_nanos": 1314798.910156}, + {"relative_spread": 0.049985, + "param": 24, + "ok_count": 3, + "min_per_call_nanos": 4274579.867188, + "median_per_call_nanos": 4377512.578125, + "max_per_call_nanos": 4493390.390625}, + {"relative_spread": 0.037541, + "param": 32, + "ok_count": 3, + "min_per_call_nanos": 10344716.5, + "median_per_call_nanos": 10433660.15625, + "max_per_call_nanos": 10736409.78125}, + {"relative_spread": 0.028443, + "param": 48, + "ok_count": 3, + "min_per_call_nanos": 33920450.5625, + "median_per_call_nanos": 34900436, + "max_per_call_nanos": 34913121.0625}, + {"relative_spread": 0.041316, + "param": 64, + "ok_count": 3, + "min_per_call_nanos": 77739645.875, + "median_per_call_nanos": 79608350.375, + "max_per_call_nanos": 81028755.25}], + "spawn_floor_nanos": 92366230, + "slope": -0.027719, + "ratios": + [[8, 322.706505], + [12, 324.067698], + [16, 317.378297], + [24, 316.660343], + [32, 318.410039], + [48, 315.578306], + [64, 303.681756]], + "points": + [{"trial_index": 0, + "total_nanos": 676764592, + "status": "ok", + "result_hash": "0xb5fde41660becb07", + "per_call_nanos": 165225.730469, + "peak_rss_kb": 59136, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 679064211, + "status": "ok", + "result_hash": "0xb5fde41660becb07", + "per_call_nanos": 165787.160889, + "peak_rss_kb": 60280, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 675581270, + "status": "ok", + "result_hash": "0xb5fde41660becb07", + "per_call_nanos": 164936.833496, + "peak_rss_kb": 59488, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 573428718, + "status": "ok", + "result_hash": "0xac317fd8a6257d68", + "per_call_nanos": 559988.982422, + "peak_rss_kb": 59560, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 577828389, + "status": "ok", + "result_hash": "0xac317fd8a6257d68", + "per_call_nanos": 564285.536133, + "peak_rss_kb": 60304, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 1024, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 1134211408, + "status": "ok", + "result_hash": "0xac317fd8a6257d68", + "per_call_nanos": 553814.164062, + "peak_rss_kb": 59676, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 673177042, + "status": "ok", + "result_hash": "0xc0abe62f50e6fb35", + "per_call_nanos": 1314798.910156, + "peak_rss_kb": 60488, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 665590530, + "status": "ok", + "result_hash": "0xc0abe62f50e6fb35", + "per_call_nanos": 1299981.503906, + "peak_rss_kb": 60504, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 637048923, + "status": "ok", + "result_hash": "0xc0abe62f50e6fb35", + "per_call_nanos": 1244236.177734, + "peak_rss_kb": 59688, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 575153970, + "status": "ok", + "result_hash": "0x641fd5425b5171c2", + "per_call_nanos": 4493390.390625, + "peak_rss_kb": 60248, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 547146223, + "status": "ok", + "result_hash": "0x641fd5425b5171c2", + "per_call_nanos": 4274579.867188, + "peak_rss_kb": 60244, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 560321610, + "status": "ok", + "result_hash": "0x641fd5425b5171c2", + "per_call_nanos": 4377512.578125, + "peak_rss_kb": 60240, + "part_of_verdict": true, + "param": 24, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 667754250, + "status": "ok", + "result_hash": "0xd44b7fe8ef9205a", + "per_call_nanos": 10433660.15625, + "peak_rss_kb": 59648, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 662061856, + "status": "ok", + "result_hash": "0xd44b7fe8ef9205a", + "per_call_nanos": 10344716.5, + "peak_rss_kb": 60476, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 687130226, + "status": "ok", + "result_hash": "0xd44b7fe8ef9205a", + "per_call_nanos": 10736409.78125, + "peak_rss_kb": 60500, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 542727209, + "status": "ok", + "result_hash": "0x681b2201cb335f18", + "per_call_nanos": 33920450.5625, + "peak_rss_kb": 60296, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 558609937, + "status": "ok", + "result_hash": "0x681b2201cb335f18", + "per_call_nanos": 34913121.0625, + "peak_rss_kb": 60348, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 558406976, + "status": "ok", + "result_hash": "0x681b2201cb335f18", + "per_call_nanos": 34900436, + "peak_rss_kb": 59788, + "part_of_verdict": true, + "param": 48, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 648230042, + "status": "ok", + "result_hash": "0x7b25b06c331c5174", + "per_call_nanos": 81028755.25, + "peak_rss_kb": 61032, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 1, + "total_nanos": 621917167, + "status": "ok", + "result_hash": "0x7b25b06c331c5174", + "per_call_nanos": 77739645.875, + "peak_rss_kb": 60600, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 2, + "total_nanos": 636866803, + "status": "ok", + "result_hash": "0x7b25b06c331c5174", + "per_call_nanos": 79608350.375, + "peak_rss_kb": 59580, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RowReduceBench.runNullspace", + "env": + {"timestamp_unix_ms": 1788157247430, + "timestamp_iso": "2026-08-31T06:20:47Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 1000000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [8, 12, 16, 24, 32, 48, 64], "kind": "custom"}, + "param_floor": 8, + "param_ceiling": 64, + "outer_trials": 3, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 10, + "cache_mode": "warm"}, + "complexity_formula": "n ^ 3", + "c_min": 303.681756, + "c_max": 324.067698, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1788156872878, + "timestamp_iso": "2026-08-31T06:14:32Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.34.0-rc2", + "lean_toolchain": "leanprover/lean4:4.34.0-rc2", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": false, + "git_commit": "f88a6ab24b235a474cf0d78ba416f69e77d0804e", + "exe_name": "hexrowreduce_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}} diff --git a/reports/hex-row-reduce-performance.md b/reports/hex-row-reduce-performance.md index d36852191..1481d5af5 100644 --- a/reports/hex-row-reduce-performance.md +++ b/reports/hex-row-reduce-performance.md @@ -1,36 +1,120 @@ # HexRowReduce Performance Report -`HexRowReduce` provides the executable row-reduction stack over the `HexMatrix` -dense core: the row-echelon transform and its elementary-operation contracts -(`RowEchelon`), and the executable RREF loop with its pivot/free-column -partition and span/nullspace APIs (`RREF`). +## Bench targets -## Bench Targets +`bench/HexRowReduce/Bench.lean` gives every advertised executable operation a +direct mode-1 registration. Preparation is outside the timed region and result +forcing is inside it. The two declared input families are +`dense-rational-rref` and `rank-deficient-rational-nullspace`. -None. The row-reduction surface has no performance-critical headline benchmark: -its operations (`rref`, `rref_rank`, `nullspace`, `spanCoeffs`) are exact -rational computations whose cost is dominated by `Rat` arithmetic, and they are -validated for correctness rather than timed against an external tool. +| Registration | Executable surface | Controlled family and schedule | Model | +| --- | --- | --- | --- | +| `runReduce` | `Matrix.rowReduce` | dense `I + J`, `n = 8, 12, 16, 24, 32, 48, 64` | `n³` | +| `runRank` | `Matrix.rowReduce_rank` | dense `I + J`, same ladder | `n³` | +| `runSpanCoeffs` | `Matrix.spanCoeffs` | dense `I + J`, same ladder | `n³` | +| `runSpanContains` | `Matrix.spanContains` | dense `I + J`, same ladder | `n³` | +| `runEchelonCoeffs` | `IsEchelonForm.echelonCoeffs` on prepared RREF | rank-deficient projection, `n = 128, 192, 256, 384, 512, 768` | `n` | +| `runEchelonSpanCoeffs` | `IsEchelonForm.spanCoeffs` on prepared RREF | dense `I + J`, `n = 16, 24, 32, 48, 64, 96, 128, 192` | `n²` | +| `runEchelonSpanContains` | `IsEchelonForm.spanContains` on prepared RREF | dense `I + J`, same ladder | `n²` | +| `runFreeCols` | `IsEchelonForm.freeCols` on prepared RREF | rank-deficient projection, `n = 64, 96, 128, 192, 256, 384, 512` | `n²` | +| `runNullspaceMatrix` | `Matrix.nullspaceBasisMatrix` | repeated half-size `I + J`, `n = 16, 24, 32, 48, 64` | `n³` | +| `runNullspace` | `Matrix.nullspace` | repeated half-size `I + J`, `n = 8, 12, 16, 24, 32, 48, 64` | `n³` | +| `runReducedMatrix` | `IsRowReduced.nullspaceMatrix` on prepared RREF | rank-deficient projection, `n = 128, 192, 256, 384, 512, 768, 1024` | `n³` | +| `runReducedNullspace` | `IsRowReduced.nullspace` on prepared RREF | rank-deficient projection, same ladder | `n³` | -## Comparators - -`HexRowReduce` declares no Phase-4 external comparator. Correctness of the -`rank`, `rref`, and `nullspace` operations is cross-checked against -python-flint's `fmpz_mat` / `fmpq_mat` through the conformance oracle -`scripts/oracle/matrix_flint.py` (driven by `hexrowreduce_emit_fixtures`): the -oracle confirms the rational rank, the unique reduced row echelon form, and the -right-kernel basis (each basis vector annihilated by the source matrix, with the -nullity matching `m - rank`). +All registrations use warm child-side repeats, a 1 s target batch, a 10 s +per-call cap, and `signalFloorMultiplier := 1.0`, which disables signal-floor +exclusion. The prepared vector ladders stop before their runtime +large-allocation transitions. Public wrappers and prepared span targets use +three outer trials, the cheap echelon helpers use five, and the allocation-heavy +prepared nullspace constructors use seven. The latter two explicitly use the +mode-1 slope tolerance `0.20`; all others use the default `0.15`. ## Verdicts -The conformance oracle passes on every committed fixture -(`conformance-fixtures/HexRowReduce/rowreduce.jsonl`: nine matrices at the -4×4 / 6×6 / 8×8 bands in random, singular, and triangular shapes, each checked -for `rank`, `rref`, and `nullspace`). The in-Lean `#guard` conformance module -additionally checks the executable span/nullspace API on committed examples. +All twelve registrations returned `consistent_with_declared_complexity` in a +single clean suite run: + +| Registration | `β` | `cMin`–`cMax` | Largest outer-trial spread | +| --- | ---: | ---: | ---: | +| `runReduce` | −0.007 | 802.820–837.334 | 10.3% | +| `runRank` | +0.012 | 759.887–834.390 | 15.3% | +| `runSpanCoeffs` | −0.037 | 833.125–904.413 | 5.9% | +| `runSpanContains` | −0.002 | 846.427–905.316 | 9.5% | +| `runEchelonCoeffs` | +0.079 | 135.255–152.256 | 19.0% | +| `runEchelonSpanCoeffs` | +0.041 | 812.217–910.210 | 20.2% | +| `runEchelonSpanContains` | +0.064 | 812.822–923.354 | 13.0% | +| `runFreeCols` | −0.034 | 8.536–9.386 | 11.8% | +| `runNullspaceMatrix` | — | 300.632–303.218 | 6.9% | +| `runNullspace` | −0.028 | 303.682–324.068 | 5.4% | +| `runReducedMatrix` | −0.166 | 0.391–0.532 | 30.4% | +| `runReducedNullspace` | −0.076 | 0.410–0.472 | 32.5% | + +The largest spreads occur in allocation-heavy prepared constructors. Their +reported points are seven-trial medians; the table exposes the full observed +range rather than treating the fitted slopes as precise latency estimates. +`runNullspaceMatrix` has four verdict-eligible ratios after warmup trimming, so +mode 1 uses its bounded normalized constants without fitting a slope. + +The machine-readable evidence is +`reports/bench-results/hex-row-reduce-phase4-scientific.json` (SHA-256 +`440c703e3919d158b3cd93cb27484bda7b7efec97c1bd9c456ae44ac6d52257d`). +It records clean source commit +`f88a6ab24b235a474cf0d78ba416f69e77d0804e`, Lean 4.34.0-rc2, +lean-bench 0.1.0, the exact settings, every trial, result hashes, and host +metadata. It was produced in one process with: + +```text +.lake/build/bin/hexrowreduce_bench run --filter Hex.RowReduceBench.run \ + --export-file reports/bench-results/hex-row-reduce-phase4-scientific.json +``` + +## Comparator ratios + +None are declared. python-flint's public `fmpq_mat` route performs complete +rational-matrix JSON decoding and result encoding for every request; that +transport dominates the shared practical ladder, so a Hex/FLINT number would +not be a kernel ratio. The callable results also differ: Hex returns the full +row-operation transform, while python-flint RREF does not, and the +transform-dependent `spanCoeffs` witness has no canonical counterpart. + +FLINT remains the independent correctness oracle through +`scripts/oracle/matrix_flint.py` and `hexrowreduce_emit_fixtures`; those checks +are conformance evidence, not timing evidence. + +## Profile + +Two deterministic `n = 64` cases were profiled from clean commit +`f88a6ab24b235a474cf0d78ba416f69e77d0804e` on an AMD EPYC 9455 +(x86_64, 96 logical cores), NixOS 26.11 / Linux 6.12.100, with lean-bench +0.1.0 and samply 0.13.1 at 999 Hz. Raw profiles remain under `/tmp` and are +not committed. + +For dense `runReduce`, 1,937 timed-thread samples were retained. Inclusive +time is 99.85% in `Matrix.rowReduce`, 99.79% in `rowReduceLoop`, and 98.40% in +the specialized `rowAdd` path. Leaf samples are 37.74% GMP arithmetic, 34.95% +allocation, 24.73% Lean runtime, 1.65% Lean/Hex own code, and 0.93% other. +Calibration residual was 0.963 ms against a 5 ms limit; off-thread samples +were zero and the ±5 ms sensitivity check passed. + +For rank-deficient `runNullspaceMatrix`, 1,376 timed-thread samples were +retained. Inclusive time is 99.93% in `Matrix.nullspaceBasisMatrix`, 99.56% in +its single `Matrix.rowReduce` path, and 98.40% in `rowAdd`. Leaf samples are +38.01% GMP arithmetic, 36.26% allocation, 23.40% Lean runtime, 1.89% Lean/Hex +own code, and 0.44% other. Calibration residual was 0.480 ms; off-thread +samples were zero and sensitivity passed. Inspection of the generated C for +this registration also shows exactly one call to the specialized +`Matrix.rowReduce`, followed by nullspace construction and flat-array forcing. + +Commands: + +```text +LEAN_BENCH_SAMPLY_HOME= scripts/profile/run_profile.sh \ + .lake/build/bin/hexrowreduce_bench Hex.RowReduceBench.runReduce 64 3000000000 +LEAN_BENCH_SAMPLY_HOME= scripts/profile/run_profile.sh \ + .lake/build/bin/hexrowreduce_bench Hex.RowReduceBench.runNullspaceMatrix 64 3000000000 +``` ## Concerns -- [#9811](https://github.com/kim-em/hex-dev/issues/9811) tracks the missing - compiled performance evidence for the advertised row-reduction surface. +None. diff --git a/reports/phase4-ordered-mode-audit.md b/reports/phase4-ordered-mode-audit.md index fd71dbce4..3e06d863c 100644 --- a/reports/phase4-ordered-mode-audit.md +++ b/reports/phase4-ordered-mode-audit.md @@ -26,7 +26,7 @@ below because HexNumberFieldTower relies on it. | HexPoly | No multiplication comparator rung is eligible; the separate expected composition divergence is misfiled as a Concern and must move to the trend narrative. | [#9804](https://github.com/kim-em/hex-dev/issues/9804) | | HexMvPoly | The representation experiment remains unresolved under `## Concerns`. | [#9805](https://github.com/kim-em/hex-dev/issues/9805) | | HexMvGcd | Fixed shape/hash registrations are used as performance coverage without mode-3 budgets or ordered-mode exclusions. | [#9812](https://github.com/kim-em/hex-dev/issues/9812) | -| HexRowReduce | Advertised compiled operations have conformance evidence but no performance mode. | [#9811](https://github.com/kim-em/hex-dev/issues/9811) | +| HexRowReduce | Resolved: all advertised compiled operations have direct mode-1 coverage. | [#9811](https://github.com/kim-em/hex-dev/issues/9811) | | HexBareiss | An unresolved informational-comparator finding remains under `## Concerns`. | [#9806](https://github.com/kim-em/hex-dev/issues/9806) | | HexGF2 | The addition comparison is marshalling-dominated; the separate expected NTL divergence is misfiled as a Concern and must move to the trend narrative. | [#9807](https://github.com/kim-em/hex-dev/issues/9807) | | HexLLL | The verified-Isabelle comparison has only one point per headline family. | [#9808](https://github.com/kim-em/hex-dev/issues/9808) | diff --git a/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-e82c6493-89a7d413.json b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-e82c6493-89a7d413.json new file mode 100644 index 000000000..b1326182e --- /dev/null +++ b/scripts/bench/proof_only_runtime_exemptions/lakefile-lean-e82c6493-89a7d413.json @@ -0,0 +1,6 @@ +{ + "path": "lakefile.lean", + "baseline_blob": "e82c649322c5dc6574071e576e92d644683eb00a", + "current_blob": "89a7d413c38dbf6182877ae5e58ca51155dc66b7", + "reason": "Combines inherited build-target registrations with the independent hexrowreduce_bench registration. This changes no factorization source, hexbz_factor_service implementation, or factorization runtime call graph." +}