diff --git a/HexRoots/SPEC/hex-roots.md b/HexRoots/SPEC/hex-roots.md index 62351b5a3..7b71f17de 100644 --- a/HexRoots/SPEC/hex-roots.md +++ b/HexRoots/SPEC/hex-roots.md @@ -750,6 +750,17 @@ and the Phase-4 external performance comparator; it is not wired into merge-facing CI. SageMath is not used (per SPEC/testing.md's Sage policy). +For Phase 4 both named comparators are classified `informational` (per +[SPEC/benchmarking.md §Comparator classification](../../SPEC/benchmarking.md#comparator-classification-gating-vs-informational)): +python-flint `fmpz_poly.complex_roots` and MPSolve are multiprecision +ball/float engines computing approximate root inclusions, structurally +different from this library's decidable exact-integer Pellet / +Newton-Kantorovich certificates, so their ratios orient but do not gate, and +the yardstick is the "Time budgets" targets above rather than a constant-factor +goal. Neither is `gating`; MPSolve is additionally scheduled-only. The +classifications and rationales are mirrored in +`libraries.yml: HexRoots.phase4.comparators`. + ## Complexity contract Write `n = deg p` and `B = prec + n · log ‖p‖∞` for the working diff --git a/bench/HexRoots/Bench.lean b/bench/HexRoots/Bench.lean index abc253244..ced78f9ec 100644 --- a/bench/HexRoots/Bench.lean +++ b/bench/HexRoots/Bench.lean @@ -39,31 +39,75 @@ parameter (its degree): Newton-step registrations, whose squares are centred on the integer root `1` of the family. -The declared complexity models are the textbook *exact-dyadic-operation counts* -from `HexRoots/SPEC/hex-roots.md § Complexity contract`. They do not fold in the -working bit-length `B = prec + n·log‖p‖∞`, which grows with the parameter; the -scientific wall-time verdicts and their reconciliation against these op-count -models are a scheduled-hardware concern (as for the other Phase 4 benches), -not a merge-gating one. The `verify` smoke gate only exercises each +The declared complexity models are *wall-time* models: the textbook +exact-dyadic-operation count from `HexRoots/SPEC/hex-roots.md § Complexity +contract` multiplied by the family's working-bit-length growth +`B = prec + n·log‖p‖∞` where that growth is asymptotically significant on the +registered schedule (the reconciliation each derivation comment records). A +family whose operands stay in the flat, allocation-dominated GMP band across +its schedule keeps the op-count model unchanged (the bit-growth sits in the +constant); a family whose precision or coefficient bit-length grows with the +parameter folds the growth into the exponent. Each registration's comment +states which case it is and why. The `verify` smoke gate only exercises each registration at parameters `0` and `1`. +The scientific verdicts and their op-count-vs-wall reconciliation are recorded +in `reports/hexroots-performance.md`; several registrations return +*inconclusive* on their reachable schedules for reasons the report's Concerns +section documents (the fixed non-integer Taylor centre's `Θ(n)` denominator +growth, the seeded family's degree-dependent root geometry, the `refineTo` +Newton-doubling precision quantisation, and the startup-dominated microsecond +band of the small-degree witness benches). + Registrations (each with an adjacent cost-model derivation comment): -* `runTaylor` — exact Taylor shift, `O(n²)`. +* `runTaylor` — exact Taylor shift, `O(n²)` exact-dyadic operations (the + fixed non-integer centre's `Θ(n)`-bit denominator growth stays in the + allocation-dominated band on the schedule). * `runWitnessCheck`, `runNkWitnessCheck` — Pellet and Newton-Kantorovich atom - witnesses, `O(n²)` (Taylor shift dominates). -* `runMahlerPrec` — separation precision, `O(n · log‖p‖∞)`. -* `runNewtonSquare` — speculative Newton step, `O(n²)`. + witnesses, `O(n²)` (Taylor shift dominates; integer centre, sub-word + operands, flat band). +* `runMahlerPrec` — separation precision, `O(n · log‖p‖∞)`, word-size integer + arithmetic (no bit-growth). +* `runNewtonSquare` — speculative Newton step, `O(n²)` (integer-centre Taylor + shift dominates, flat band). * `runRefine1`, `runCertify` — one subdivision round and one certification - attempt on a mid-refinement component, `O(n²)`. -* `runIsolateAll` — `isolateAll?` at target `32`, `O(n³)`. -* `runIsolate` — `isolate` to the `separationDepth` floor, `O(n³)`. + attempt on a mid-refinement component, `O(n²)` (low-precision centres, + sub-word operands, flat band). +* `runIsolateAll` — `isolateAll?` at target `32`, `O(n³·B²) = O(n⁵)` with the + working bit-length `B = Θ(n)`. +* `runIsolate` — `isolate` to the `separationDepth` floor, `O(n³·B²) = O(n⁵)`. * `runRefineTo` — `DyadicRootIsolation.refineTo?` from `≈32` to a parametric - target `t`, `O(t²)`. + target precision `t`, `O(t²)` schoolbook bit-cost at fixed degree. * `runSameRoot` — `RefinedIsolation.sameRoot`, a single dyadic comparison (fixed benchmark, microseconds). * `runIsolateNk`, `runIsolatePellet`, `runIsolateNkThenPellet` — the `compare` - group over `linProdPoly`; all three must agree on the strategy-invariant hash. + group over `linProdPoly`, `O(n³·B²) = O(n⁵)`; all three must agree on the + strategy-invariant hash. + +External comparators (both `informational`, per +`libraries.yml: HexRoots.phase4.comparators`): + +* **python-flint** `fmpz_poly.complex_roots()` (the SPEC's ci-tier oracle, + which returns certified Arb balls with multiplicities) is timed as a + process-call comparator on the same seeded degree ladder the + whole-polynomial drivers use; the ratio `hex isolateAll?@32 / flint` per + degree is recorded in `reports/hexroots-performance.md`. It is + `informational`, not gating: FLINT's `complex_roots` is a multiprecision + ball-arithmetic engine, structurally different from this library's + decidable exact-integer Pellet / Newton-Kantorovich certificates, so the + SPEC's time budgets — not a constant-factor `1×` goal — are the yardstick. + Reproduce with `scripts/bench/hexroots_flint_compare.py` under a + `python-flint ≥ 0.9.0` virtualenv (subprocess, wall clock, per-call + overhead measured on a trivial input). +* **MPSolve** (Bini–Fiorentino `mpsolve`, the SPEC's local-tier and Phase-4 + external performance comparator) is classified `informational` and + **scheduled-only**: it is not wired in this PR. Required environment: the + `mpsolve` CLI (`unisa-cs/mpsolve`, built with GMP) on `PATH`, driven on the + same seeded ladder via its `-au -Gi` isolate-mode output. Rationale for the + informational class: MPSolve is a multiprecision-float C library computing + approximate root inclusions, structurally different from this library's + integer-certified Lean witnesses, so its ratio orients but does not gate. -/ namespace Hex.RootsBench @@ -320,10 +364,23 @@ def prepRefineTo (target : Nat) : Option (DyadicRootIsolation refinePoly) × Int /-! ### `taylor` / `mahlerPrec` : dense seeded family -/ /- -`taylor` produces `p(X + z) = Σ cₖ Xᵏ` by repeated synthetic division: the -`k`-indexed outer pass runs an inner Horner sweep of length `n − 1 − k`, so the -total is `Σ_k (n − 1 − k) = O(n²)` exact Gaussian-dyadic multiply/adds. Degree -`n` is the benchmark parameter, so the op-count model is `n²`. +Cost model. `taylor` produces `p(X + z) = Σ cₖ Xᵏ` by repeated synthetic +division: the `k`-indexed outer pass runs an inner Horner sweep of length +`n − 1 − k`, so the total is `Σ_k (n − 1 − k) = O(n²)` exact Gaussian-dyadic +multiply/adds (degree `n` is the parameter). Bit-growth: the fixed centre +`z = 1/4 + i/8 = 2^{−3}(2 + i)` is a *non-integer* dyadic, so `z^{j−k}` carries +denominator `2^{3(j−k)}` and the coefficient `cₖ` reaches working bit-length +`B = Θ(n)` (the `2^{3n}` denominator dominates the `binomial ~ 2^n` numerator). +Each inner op multiplies a `B`-bit operand by the fixed `3`-bit centre, a +schoolbook `O(B)` cost, so the wall bit-cost is `O(n²·B) = O(n³)` in the +multiplication-bound limit. On the registered `16..256` schedule the operands +are `≤ 12` GMP words, still in the allocation-dominated transition where wall +tracks the `O(n²)` operation count with a sub-linear residual (measured +`~n^{2.25}`, short of the `n³` asymptote); the op-count `n²` is the declared +wall model per the SPEC contract, with the transition residual reported as a +Concern. This is the same Taylor-shift shape as hex-real-roots' +`runMobiusTransform` but with a non-integer centre, whose denominator growth +is what keeps it out of the flat band that made that one consistent at `n²`. -/ setup_benchmark runTaylor n => n * n with prep := seededPoly @@ -337,11 +394,14 @@ setup_benchmark runTaylor n => n * n } /- -`mahlerPrec` evaluates the closed-form Mahler/Landau separation bound: a fixed -number of `ceilLog2` calls plus integer multiplies over the degree `n` and the -coefficient-norm `log‖p‖∞`. The SPEC contract is `O(n · log‖p‖∞)`; the seeded -family holds `‖p‖∞ ≤ 10` fixed, so the `log‖p‖∞` factor is a constant over this -schedule and the op-count model reduces to linear in `n`. +Cost model. `mahlerPrec` evaluates the closed-form Mahler/Landau separation +bound: the `coeffAbsMax` scan is `O(n)` `Nat.max` steps, plus a fixed number +of `ceilLog2` calls and word-size integer multiplies forming `t`. The SPEC +contract is `O(n · log‖p‖∞)`; the seeded family holds `‖p‖∞ ≤ 10` fixed, so +`log‖p‖∞` is constant and the op count reduces to linear in `n`. Bit-growth: +every operand (the coefficients `≤ 10`, the degree `n`, the `ceilLog2` results, +the sum `t = O(n)`) fits in a single machine word across `16..256`, so `B` is +constant and the wall model equals the op count `n`. -/ setup_benchmark runMahlerPrec n => n with prep := seededPoly @@ -357,11 +417,16 @@ setup_benchmark runMahlerPrec n => n /-! ### witness checks / Newton step : root-centred `linProdPoly` -/ /- -`witnessCheck` computes the exact Taylor coefficients at the square's centre -(the `O(n²)` shift, which dominates) and then, for each of the three test -radii, a single `O(n)` fold over the coefficients. The op-count model is `n²`. -The square is centred on the integer root `1` of `linProdPoly`, so the witness -actually fires at every scheduled degree. +Cost model. `witnessCheck` computes the exact Taylor coefficients at the +square's centre (the `O(n²)` shift, which dominates) and then, for each of the +three test radii, a single `O(n)` fold over the coefficients, so the op count +is `n²`. Bit-growth: the square is centred on the *integer* root `1` of +`linProdPoly`, so the centre `z = (1, 0)` has precision `0` and `z^{j−k}` +introduces no denominator; the Taylor coefficients are the (integer) +elementary-symmetric coefficients of `p(X+1)`, of bit-length `~log(n!) = +O(n log n)`, which stays under one GMP word (`≤ 44` bits at `n = 16`) across +the `2..16` schedule. Operands are sub-word, per-op cost flat, so the wall +model is the op count `n²`. -/ setup_benchmark runWitnessCheck n => n * n with prep := linProdPoly @@ -375,9 +440,12 @@ setup_benchmark runWitnessCheck n => n * n } /- -`nkWitnessCheck` has the same `O(n²)` Taylor-shift-dominated shape as -`witnessCheck`, plus one `Dyadic.invAtPrec` reciprocal and a single `O(n)` -radial-Lipschitz fold. Op-count model `n²`, root-centred on `linProdPoly`. +Cost model. `nkWitnessCheck` has the same `O(n²)` Taylor-shift-dominated shape +as `witnessCheck`, plus one `invFloor` reciprocal and a single `O(n)` +radial-Lipschitz fold, so the op count is `n²`. Bit-growth: identical to +`witnessCheck` — integer centre `(1, 0)`, no denominator, integer Taylor +coefficients of `O(n log n)` bits staying sub-word (`≤ 44` bits) across +`2..16`, so operands are flat and the wall model is the op count `n²`. -/ setup_benchmark runNkWitnessCheck n => n * n with prep := linProdPoly @@ -391,10 +459,13 @@ setup_benchmark runNkWitnessCheck n => n * n } /- -`newtonSquare` computes the Taylor coefficients at the centre (the `O(n²)` -shift), reads `c₀, c₁`, and does one `Dyadic.invAtPrec` reciprocal plus a -constant amount of Gaussian-dyadic arithmetic. The Taylor shift dominates, so -the op-count model is `n²`. +Cost model. `newtonSquare` computes the Taylor coefficients at the centre (the +`O(n²)` shift), reads `c₀, c₁`, and does one `Dyadic.invAtPrec` reciprocal plus +a constant amount of Gaussian-dyadic arithmetic. The Taylor shift dominates, so +the op count is `n²`. Bit-growth: integer centre `(1, 0)` on `linProdPoly`, no +denominator, integer Taylor coefficients of `O(n log n)` bits staying sub-word +across `2..16`; the reciprocal is at precision `~2·prec = 24` bits, also +sub-word. Operands flat, so the wall model is the op count `n²`. -/ setup_benchmark runNewtonSquare n => n * n with prep := linProdPoly @@ -410,11 +481,16 @@ setup_benchmark runNewtonSquare n => n * n /-! ### refinement primitives : mid-refinement component of the seeded family -/ /- -`refine1` subdivides each square of the component four ways and runs the `T₀` -`rootFree` exclusion — one Taylor shift, `O(n²)` — on each child, then glues the -survivors. For a component of a bounded number of squares this is a bounded -number of `O(n²)` shifts, so the op-count model is `n²` in the polynomial -degree `n`. +Cost model. `refine1` subdivides each square of the component four ways and +runs the `T₀` `rootFree` exclusion — one Taylor shift, `O(n²)` — on each child, +then glues the survivors. For a component of a bounded number of squares this +is a bounded number of `O(n²)` shifts, so the op count is `n²` in the degree +`n`. Bit-growth: the mid-refinement component sits two levels below `cauchy`, +so its square centres have low precision (`~cauchy.prec + 2`, a few bits) and +the seeded coefficients are `≤ 10`; the Taylor coefficients reach only `O(n)` +bits (dominated by `|z|^n` with `|z|` near the root bound `~11`), which stays +sub-word (`≤ 42` bits at `n = 12`) across the `4..12` schedule. Operands flat, +so the wall model is the op count `n²`. -/ setup_benchmark runRefine1 n => n * n with prep := midComponent @@ -428,13 +504,15 @@ setup_benchmark runRefine1 n => n * n } /- -`certify?` under the default `nkThenPellet` strategy first tries the -Newton-Kantorovich witness on the doubled enclosing square: one +Cost model. `certify?` under the default `nkThenPellet` strategy first tries +the Newton-Kantorovich witness on the doubled enclosing square: one `nkWitnessCheck` (`O(n²)`) and one speculative `newtonSquare` (`O(n²)`). On a -mid-refinement component localised near a root this NK path fires, so the -op-count model is `n²`. (The Pellet fallback, taken only when NK does not fire, -loops over `k ≤ deg p` and is `O(n³)`; it is not the path this fixture -measures.) +mid-refinement component localised near a root this NK path fires, so the op +count is `n²`. (The Pellet fallback, taken only when NK does not fire, loops +over `k ≤ deg p` and is `O(n³)`; it is not the path this fixture measures.) +Bit-growth: same low-precision seeded mid-refinement component as `refine1` — +`O(n)`-bit Taylor coefficients staying sub-word across `4..12` — so operands +are flat and the wall model is the op count `n²`. -/ setup_benchmark runCertify n => n * n with prep := midComponent @@ -450,16 +528,25 @@ setup_benchmark runCertify n => n * n /-! ### whole-polynomial drivers : dense seeded family -/ /- -`isolateAll?` refines the Cauchy component to disjoint certified atoms at target -precision `32`. The SPEC heuristic is `O(n³ · B²)` bit operations for degree `n` -with well-separated roots; the op-count model (dropping the working bit-length -`B`) is `n³`: up to `O(n)` components, each driven through `O(n)` subdivision -levels of `O(n²)`-per-witness work amortised by the speculative Newton jumps. -The seeded family's distinct irrational roots force genuine subdivision, so the -driver exercises the separation machinery rather than a rational-root -short-circuit. +Cost model. `isolateAll?` refines the Cauchy component to disjoint certified +atoms at target precision `32`. The op count is `n³`: up to `O(n)` components, +each driven through `O(n)` subdivision levels of `O(n²)`-per-witness work +amortised by the speculative Newton jumps. Bit-growth is asymptotically +significant here: the working bit-length reaches `B = prec + n·log‖p‖∞ = Θ(n)` +(precision `~32` at the certifying level, plus the seeded `n·log 10` term, and +the Taylor coefficients' `Θ(prec·n)` denominator growth), and the +growing-precision dyadic arithmetic (notably the `invAtPrec` reciprocal) is +schoolbook `O(B²)`. The SPEC heuristic `O(n³·B²)` with `B = Θ(n)` gives the +wall model `n⁵`. The seeded family's distinct irrational roots force genuine +subdivision, but their *degree-dependent* root geometry (some degrees have +much closer roots than neighbours) makes the wall time non-monotonic in `n`, +which the report's Concerns section flags as a fit-quality limitation. -/ -setup_benchmark runIsolateAll n => n * n * n +-- Polylog factors (a strict B = Θ(n log n) reading gives n^5·log²n) are +-- suppressed in the declared model per house convention: the harness fits a +-- log-log slope, and the sibling Phase-4 reports (hex-real-roots) declare +-- plain powers for the same reason. +setup_benchmark runIsolateAll n => n * n * n * n * n with prep := seededPoly where { paramFloor := 4 @@ -471,14 +558,22 @@ setup_benchmark runIsolateAll n => n * n * n } /- -`isolate` runs `isolateAll?` from the Cauchy component to +Cost model. `isolate` runs `isolateAll?` from the Cauchy component to `max atom_prec (separationDepth p)` and requires every result to be an atom. -With `atom_prec = 0` the target is the `separationDepth` floor, which grows with -the degree, so this is the deeper of the two whole-polynomial drivers. Same -`O(n³)` op-count model as `isolateAll?`. The schedule caps lower (degree `16`) +With `atom_prec = 0` the target is the `separationDepth` floor, which grows +with the degree, so this is the deeper of the two whole-polynomial drivers. +Same `n³` op count as `isolateAll?`. Bit-growth: the target precision is now +`separationDepth p = mahlerPrec p + O(log n) = O(n·log‖p‖∞)`, so `B = Θ(n)` is +even more firmly in the multiplication-bound regime; `O(n³·B²)` with +`B = Θ(n)` gives the wall model `n⁵`. The schedule caps lower (degree `16`) because the separation-depth target keeps one full-ladder pass practical there. +Same seeded-family non-monotonicity caveat as `isolateAll?`. -/ -setup_benchmark runIsolate n => n * n * n +-- Polylog factors (a strict B = Θ(n log n) reading gives n^5·log²n) are +-- suppressed in the declared model per house convention: the harness fits a +-- log-log slope, and the sibling Phase-4 reports (hex-real-roots) declare +-- plain powers for the same reason. +setup_benchmark runIsolate n => n * n * n * n * n with prep := seededPoly where { paramFloor := 4 @@ -490,11 +585,16 @@ setup_benchmark runIsolate n => n * n * n } /- -`refineTo?` sharpens a fixed degree-3 atom from precision `≈32` to the parametric -target `t`. Speculative Newton doubles the precision per accepted jump, so the -final witness at precision `t` dominates: one `O(n²)`-op Taylor shift on -`B ≈ t`-bit dyadics, whose schoolbook bit-cost is `O(t²)` at fixed degree. The -parameter is the target precision, so the model is `t²`. +Cost model. `refineTo?` sharpens a fixed degree-3 atom from precision `≈32` to +the parametric target `t`. Speculative Newton doubles the precision per +accepted jump, so the final witness at precision `t` dominates: a fixed number +(`O(deg²) = O(1)` at degree `3`) of Taylor multiplies on `B ≈ t`-bit dyadics, +each a schoolbook `t × t` product costing `O(t²)`, so the wall model is `t²` +in the target precision. Caveat: Newton doubling reaches a *discrete* precision +ladder, so the per-call work is a step function of `t` rather than smooth in it +(targets in the same doubling interval do equal work); the report's Concerns +section flags this quantisation as the reason the verdict is inconclusive on +the `64..256` schedule. -/ setup_benchmark runRefineTo t => t * t with prep := prepRefineTo @@ -514,12 +614,21 @@ same `linProdPoly` inputs under the three `AtomStrategy` values and digest the output with the strategy-invariant `rootsDigest`. On this integer-root family all three agree, so `compare runIsolateNk runIsolatePellet runIsolateNkThenPellet` reports `allAgreed`; a divergence would be a cross-strategy conformance failure. -The op-count model is `n³` (each is an `isolate` run), matching the drivers. -/ +The wall model is `n⁵` (each is an `isolate` run), matching the drivers. -/ --- Cost model: one `isolate` run over `linProdPoly n`; n subdivision/adoption --- rounds of O(n) witness checks at O(n) ops each (fixed-height family), so --- n^3 exact-dyadic operations; the NK-only strategy certifies each atom on its doubled square. -setup_benchmark runIsolateNk n => n * n * n +/- +Cost model: one `isolate` run over `linProdPoly n`; `n³` op count (n +subdivision/adoption rounds of O(n) witness checks at O(n) ops each), and the +separation target's working bit-length `B = Θ(n log n)` enters the +growing-precision arithmetic as a schoolbook `O(B²)` per-op factor, so +`O(n³·B²)` gives the `n⁵` wall model; the NK-only strategy certifies each atom +on its doubled square. +-/ +-- Polylog factors (a strict B = Θ(n log n) reading gives n^5·log²n) are +-- suppressed in the declared model per house convention: the harness fits a +-- log-log slope, and the sibling Phase-4 reports (hex-real-roots) declare +-- plain powers for the same reason. +setup_benchmark runIsolateNk n => n * n * n * n * n with prep := linProdPoly where { paramFloor := 2 @@ -530,10 +639,19 @@ setup_benchmark runIsolateNk n => n * n * n signalFloorMultiplier := 1.0 } --- Cost model: one `isolate` run over `linProdPoly n`; n subdivision/adoption --- rounds of O(n) witness checks at O(n) ops each (fixed-height family), so --- n^3 exact-dyadic operations; the Pellet-only strategy runs the three-radius test per k candidate. -setup_benchmark runIsolatePellet n => n * n * n +/- +Cost model: one `isolate` run over `linProdPoly n`; `n³` op count (n +subdivision/adoption rounds of O(n) witness checks at O(n) ops each), and the +separation target's working bit-length `B = Θ(n log n)` enters the +growing-precision arithmetic as a schoolbook `O(B²)` per-op factor, so +`O(n³·B²)` gives the `n⁵` wall model; the Pellet-only strategy runs the +three-radius test per k candidate. +-/ +-- Polylog factors (a strict B = Θ(n log n) reading gives n^5·log²n) are +-- suppressed in the declared model per house convention: the harness fits a +-- log-log slope, and the sibling Phase-4 reports (hex-real-roots) declare +-- plain powers for the same reason. +setup_benchmark runIsolatePellet n => n * n * n * n * n with prep := linProdPoly where { paramFloor := 2 @@ -544,10 +662,19 @@ setup_benchmark runIsolatePellet n => n * n * n signalFloorMultiplier := 1.0 } --- Cost model: one `isolate` run over `linProdPoly n`; n subdivision/adoption --- rounds of O(n) witness checks at O(n) ops each (fixed-height family), so --- n^3 exact-dyadic operations; the default strategy tries NK first, Pellet as fallback. -setup_benchmark runIsolateNkThenPellet n => n * n * n +/- +Cost model: one `isolate` run over `linProdPoly n`; `n³` op count (n +subdivision/adoption rounds of O(n) witness checks at O(n) ops each), and the +separation target's working bit-length `B = Θ(n log n)` enters the +growing-precision arithmetic as a schoolbook `O(B²)` per-op factor, so +`O(n³·B²)` gives the `n⁵` wall model; the default strategy tries NK first, +Pellet as fallback. +-/ +-- Polylog factors (a strict B = Θ(n log n) reading gives n^5·log²n) are +-- suppressed in the declared model per house convention: the harness fits a +-- log-log slope, and the sibling Phase-4 reports (hex-real-roots) declare +-- plain powers for the same reason. +setup_benchmark runIsolateNkThenPellet n => n * n * n * n * n with prep := linProdPoly where { paramFloor := 2 diff --git a/libraries.yml b/libraries.yml index 16fd49d3d..038df8fef 100644 --- a/libraries.yml +++ b/libraries.yml @@ -453,8 +453,29 @@ libraries: HexRoots: deps: [HexPolyZ] mathlib: false + # done_through stays 3: the Phase-4 scientific run (commit b08a66cce522, + # chungus2) returned inconclusive verdicts for 9 of 13 parametric + # registrations and two SPEC time budgets fail, so Phase 4 is NOT claimed. + # See reports/hexroots-performance.md §Concerns. The phase4 block below + # records the comparators and input families the run used; it does not + # assert completion. done_through: 3 status: active + phase4: + comparators: + - tool: "python-flint fmpz_poly.complex_roots" + class: informational + rationale: "The SPEC's ci-tier oracle (python-flint fmpz_poly.complex_roots, returning certified Arb balls with multiplicities) is a multiprecision ball-arithmetic engine, structurally different from this library's decidable exact-integer Pellet / Newton-Kantorovich certificates. Timed on the same seed-0xC0FFEE dense integer ladder the whole-polynomial drivers use (scripts/bench/hexroots_flint_compare.py); the ratio hex isolateAll?@32 / flint per degree is recorded in reports/hexroots-performance.md. Informational, not gating: the SPEC's time budgets — not a constant-factor 1x goal — are the yardstick for an integer-certified isolator against a float engine." + - tool: "MPSolve" + class: informational + rationale: "MPSolve (Bini-Fiorentino, the SPEC's local-tier and Phase-4 external performance comparator) is a multiprecision-float C library computing approximate root inclusions, structurally different from this library's integer-certified Lean witnesses, so its ratio orients but does not gate. Scheduled-only: not wired in this PR. Required environment stated in bench/HexRoots/Bench.lean's module docstring (the mpsolve CLI built with GMP, driven on the seeded ladder via -au -Gi isolate mode)." + input_families: + - name: seeded-dense + description: Seed-0xC0FFEE dense integer polynomials with coefficients in [-10, 10] (constant term first, leading forced nonzero), generically distinct irrational roots; drives taylor, mahlerPrec, refine1, certify, and the whole-polynomial isolateAll?/isolate drivers. + - name: wilkinson-linprod + description: Wilkinson-shaped products ∏(X−j), j=1..n, with distinct integer roots 1..n; Newton recentres exactly onto integer roots, exercised by the witness-check, Newton-step, and dual-route compare-group registrations. + - name: refine-fixed + description: The fixed degree-3 polynomial (x−1)(x−2)(x+3) whose isolated atom the refineTo? and sameRoot registrations sharpen to a parametric target precision. HexRootsMathlib: deps: [HexRoots, HexPolyZMathlib] mathlib: true diff --git a/reports/bench-results/hex-roots-b08a66cce522.json b/reports/bench-results/hex-roots-b08a66cce522.json new file mode 100644 index 000000000..d070b0967 --- /dev/null +++ b/reports/bench-results/hex-roots-b08a66cce522.json @@ -0,0 +1,2028 @@ +{"results": + [{"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 16, + "ok_count": 1, + "min_per_call_nanos": 52903.728027, + "median_per_call_nanos": 52903.728027, + "max_per_call_nanos": 52903.728027}, + {"relative_spread": 0, + "param": 32, + "ok_count": 1, + "min_per_call_nanos": 466444.96875, + "median_per_call_nanos": 466444.96875, + "max_per_call_nanos": 466444.96875}, + {"relative_spread": 0, + "param": 64, + "ok_count": 1, + "min_per_call_nanos": 2834366.78125, + "median_per_call_nanos": 2834366.78125, + "max_per_call_nanos": 2834366.78125}, + {"relative_spread": 0, + "param": 128, + "ok_count": 1, + "min_per_call_nanos": 15331126.5, + "median_per_call_nanos": 15331126.5, + "max_per_call_nanos": 15331126.5}, + {"relative_spread": 0, + "param": 256, + "ok_count": 1, + "min_per_call_nanos": 70384976, + "median_per_call_nanos": 70384976, + "max_per_call_nanos": 70384976}], + "spawn_floor_nanos": 23576386, + "slope": 0.414762, + "ratios": + [[16, 206.655188], + [32, 455.512665], + [64, 691.984077], + [128, 935.737701], + [256, 1073.989502]], + "points": + [{"trial_index": 0, + "total_nanos": 108346835, + "status": "ok", + "result_hash": "0xc944db6223447de2", + "per_call_nanos": 52903.728027, + "peak_rss_kb": 60528, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 59704956, + "status": "ok", + "result_hash": "0x7de19fad1eb7e38b", + "per_call_nanos": 466444.96875, + "peak_rss_kb": 59448, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 90699737, + "status": "ok", + "result_hash": "0xd617f3bd0b0ea721", + "per_call_nanos": 2834366.78125, + "peak_rss_kb": 60620, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 61324506, + "status": "ok", + "result_hash": "0x391f76a4f4851795", + "per_call_nanos": 15331126.5, + "peak_rss_kb": 60848, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 70384976, + "status": "ok", + "result_hash": "0x1242736d713af35b", + "per_call_nanos": 70384976, + "peak_rss_kb": 59932, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runTaylor", + "env": + {"timestamp_unix_ms": 1783794950864, + "timestamp_iso": "2026-07-11T18:35:50Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [16, 32, 64, 128, 256], "kind": "custom"}, + "param_floor": 16, + "param_ceiling": 256, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 4, + "cache_mode": "warm"}, + "complexity_formula": "n * n", + "c_min": 455.512665, + "c_max": 1073.989502, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0, + "param": 16, + "ok_count": 1, + "min_per_call_nanos": 153.305408, + "median_per_call_nanos": 153.305408, + "max_per_call_nanos": 153.305408}, + {"relative_spread": 0, + "param": 32, + "ok_count": 1, + "min_per_call_nanos": 280.41304, + "median_per_call_nanos": 280.41304, + "max_per_call_nanos": 280.41304}, + {"relative_spread": 0, + "param": 64, + "ok_count": 1, + "min_per_call_nanos": 484.174156, + "median_per_call_nanos": 484.174156, + "max_per_call_nanos": 484.174156}, + {"relative_spread": 0, + "param": 128, + "ok_count": 1, + "min_per_call_nanos": 806.362137, + "median_per_call_nanos": 806.362137, + "max_per_call_nanos": 806.362137}, + {"relative_spread": 0, + "param": 256, + "ok_count": 1, + "min_per_call_nanos": 1695.441193, + "median_per_call_nanos": 1695.441193, + "max_per_call_nanos": 1695.441193}], + "spawn_floor_nanos": 23564278, + "slope": -0.147599, + "ratios": + [[16, 9.581588], + [32, 8.762908], + [64, 7.565221], + [128, 6.299704], + [256, 6.622817]], + "points": + [{"trial_index": 0, + "total_nanos": 80376186, + "status": "ok", + "result_hash": "0x89", + "per_call_nanos": 153.305408, + "peak_rss_kb": 60284, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 524288, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 73508596, + "status": "ok", + "result_hash": "0x131", + "per_call_nanos": 280.41304, + "peak_rss_kb": 60456, + "part_of_verdict": true, + "param": 32, + "inner_repeats": 262144, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 63461675, + "status": "ok", + "result_hash": "0x2a2", + "per_call_nanos": 484.174156, + "peak_rss_kb": 59440, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 131072, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 52845749, + "status": "ok", + "result_hash": "0x5c2", + "per_call_nanos": 806.362137, + "peak_rss_kb": 59816, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 65536, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 55556217, + "status": "ok", + "result_hash": "0xc83", + "per_call_nanos": 1695.441193, + "peak_rss_kb": 59788, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runMahlerPrec", + "env": + {"timestamp_unix_ms": 1783794951426, + "timestamp_iso": "2026-07-11T18:35:51Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [16, 32, 64, 128, 256], "kind": "custom"}, + "param_floor": 16, + "param_ceiling": 256, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 2, + "cache_mode": "warm"}, + "complexity_formula": "n", + "c_min": 6.299704, + "c_max": 8.762908, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 1130.775024, + "median_per_call_nanos": 1130.775024, + "max_per_call_nanos": 1130.775024}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 3169.275848, + "median_per_call_nanos": 3169.275848, + "max_per_call_nanos": 3169.275848}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 5507.034729, + "median_per_call_nanos": 5507.034729, + "max_per_call_nanos": 5507.034729}, + {"relative_spread": 0, + "param": 8, + "ok_count": 1, + "min_per_call_nanos": 8641.646729, + "median_per_call_nanos": 8641.646729, + "max_per_call_nanos": 8641.646729}, + {"relative_spread": 0, + "param": 10, + "ok_count": 1, + "min_per_call_nanos": 11552.318481, + "median_per_call_nanos": 11552.318481, + "max_per_call_nanos": 11552.318481}, + {"relative_spread": 0, + "param": 12, + "ok_count": 1, + "min_per_call_nanos": 15053.983154, + "median_per_call_nanos": 15053.983154, + "max_per_call_nanos": 15053.983154}, + {"relative_spread": 0, + "param": 16, + "ok_count": 1, + "min_per_call_nanos": 44720.152344, + "median_per_call_nanos": 44720.152344, + "max_per_call_nanos": 44720.152344}], + "spawn_floor_nanos": 23878744, + "slope": -0.227425, + "ratios": + [[2, 282.693756], + [4, 198.079741], + [6, 152.973187], + [8, 135.02573], + [10, 115.523185], + [12, 104.54155], + [16, 174.688095]], + "points": + [{"trial_index": 0, + "total_nanos": 74106472, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 1130.775024, + "peak_rss_kb": 60280, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 65536, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 103850831, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 3169.275848, + "peak_rss_kb": 60760, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 90227257, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 5507.034729, + "peak_rss_kb": 60252, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 70792370, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 8641.646729, + "peak_rss_kb": 60944, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 94636593, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 11552.318481, + "peak_rss_kb": 60960, + "part_of_verdict": true, + "param": 10, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 61661115, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 15053.983154, + "peak_rss_kb": 59768, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 91586872, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 44720.152344, + "peak_rss_kb": 60880, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runWitnessCheck", + "env": + {"timestamp_unix_ms": 1783794951906, + "timestamp_iso": "2026-07-11T18:35:51Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [2, 4, 6, 8, 10, 12, 16], "kind": "custom"}, + "param_floor": 2, + "param_ceiling": 16, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 4, + "cache_mode": "warm"}, + "complexity_formula": "n * n", + "c_min": 104.54155, + "c_max": 198.079741, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 826.542053, + "median_per_call_nanos": 826.542053, + "max_per_call_nanos": 826.542053}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 2354.16568, + "median_per_call_nanos": 2354.16568, + "max_per_call_nanos": 2354.16568}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 3745.424011, + "median_per_call_nanos": 3745.424011, + "max_per_call_nanos": 3745.424011}, + {"relative_spread": 0, + "param": 8, + "ok_count": 1, + "min_per_call_nanos": 5793.193115, + "median_per_call_nanos": 5793.193115, + "max_per_call_nanos": 5793.193115}, + {"relative_spread": 0, + "param": 10, + "ok_count": 1, + "min_per_call_nanos": 8491.290894, + "median_per_call_nanos": 8491.290894, + "max_per_call_nanos": 8491.290894}, + {"relative_spread": 0, + "param": 12, + "ok_count": 1, + "min_per_call_nanos": 12025.950195, + "median_per_call_nanos": 12025.950195, + "max_per_call_nanos": 12025.950195}, + {"relative_spread": 0, + "param": 16, + "ok_count": 1, + "min_per_call_nanos": 39156.393066, + "median_per_call_nanos": 39156.393066, + "max_per_call_nanos": 39156.393066}], + "spawn_floor_nanos": 24449570, + "slope": -0.094631, + "ratios": + [[2, 206.635513], + [4, 147.135355], + [6, 104.039556], + [8, 90.518642], + [10, 84.912909], + [12, 83.513543], + [16, 152.95466]], + "points": + [{"trial_index": 0, + "total_nanos": 108336520, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 826.542053, + "peak_rss_kb": 60792, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 131072, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 77141301, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 2354.16568, + "peak_rss_kb": 60816, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 61365027, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 3745.424011, + "peak_rss_kb": 59784, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 94915676, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 5793.193115, + "peak_rss_kb": 60512, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 69560655, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 8491.290894, + "peak_rss_kb": 60372, + "part_of_verdict": true, + "param": 10, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 98516584, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 12025.950195, + "peak_rss_kb": 60080, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 80192293, + "status": "ok", + "result_hash": "0xb", + "per_call_nanos": 39156.393066, + "peak_rss_kb": 59836, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runNkWitnessCheck", + "env": + {"timestamp_unix_ms": 1783794952697, + "timestamp_iso": "2026-07-11T18:35:52Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [2, 4, 6, 8, 10, 12, 16], "kind": "custom"}, + "param_floor": 2, + "param_ceiling": 16, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 4, + "cache_mode": "warm"}, + "complexity_formula": "n * n", + "c_min": 83.513543, + "c_max": 152.95466, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 676.23243, + "median_per_call_nanos": 676.23243, + "max_per_call_nanos": 676.23243}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 1117.922882, + "median_per_call_nanos": 1117.922882, + "max_per_call_nanos": 1117.922882}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 2141.073944, + "median_per_call_nanos": 2141.073944, + "max_per_call_nanos": 2141.073944}, + {"relative_spread": 0, + "param": 8, + "ok_count": 1, + "min_per_call_nanos": 3353.481659, + "median_per_call_nanos": 3353.481659, + "max_per_call_nanos": 3353.481659}, + {"relative_spread": 0, + "param": 10, + "ok_count": 1, + "min_per_call_nanos": 4681.702515, + "median_per_call_nanos": 4681.702515, + "max_per_call_nanos": 4681.702515}, + {"relative_spread": 0, + "param": 12, + "ok_count": 1, + "min_per_call_nanos": 6960.588135, + "median_per_call_nanos": 6960.588135, + "max_per_call_nanos": 6960.588135}, + {"relative_spread": 0, + "param": 16, + "ok_count": 1, + "min_per_call_nanos": 31888.599121, + "median_per_call_nanos": 31888.599121, + "max_per_call_nanos": 31888.599121}], + "spawn_floor_nanos": 23372262, + "slope": 0.197594, + "ratios": + [[2, 169.058108], + [4, 69.87018], + [6, 59.474276], + [8, 52.398151], + [10, 46.817025], + [12, 48.337418], + [16, 124.56484]], + "points": + [{"trial_index": 0, + "total_nanos": 88635137, + "status": "ok", + "result_hash": "0x450307c7dcbe905c", + "per_call_nanos": 676.23243, + "peak_rss_kb": 60532, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 131072, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 73264194, + "status": "ok", + "result_hash": "0x450307c7dcbe905c", + "per_call_nanos": 1117.922882, + "peak_rss_kb": 60780, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 65536, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 70158711, + "status": "ok", + "result_hash": "0x450307c7dcbe905c", + "per_call_nanos": 2141.073944, + "peak_rss_kb": 59780, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 109886887, + "status": "ok", + "result_hash": "0x450307c7dcbe905c", + "per_call_nanos": 3353.481659, + "peak_rss_kb": 60512, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 32768, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 76705014, + "status": "ok", + "result_hash": "0x450307c7dcbe905c", + "per_call_nanos": 4681.702515, + "peak_rss_kb": 60280, + "part_of_verdict": true, + "param": 10, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 57021138, + "status": "ok", + "result_hash": "0x450307c7dcbe905c", + "per_call_nanos": 6960.588135, + "peak_rss_kb": 59948, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 65307851, + "status": "ok", + "result_hash": "0x450307c7dcbe905c", + "per_call_nanos": 31888.599121, + "peak_rss_kb": 60576, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runNewtonSquare", + "env": + {"timestamp_unix_ms": 1783794953494, + "timestamp_iso": "2026-07-11T18:35:53Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [2, 4, 6, 8, 10, 12, 16], "kind": "custom"}, + "param_floor": 2, + "param_ceiling": 16, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 4, + "cache_mode": "warm"}, + "complexity_formula": "n * n", + "c_min": 46.817025, + "c_max": 124.56484, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 302199.492188, + "median_per_call_nanos": 302199.492188, + "max_per_call_nanos": 302199.492188}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 472436.742188, + "median_per_call_nanos": 472436.742188, + "max_per_call_nanos": 472436.742188}, + {"relative_spread": 0, + "param": 8, + "ok_count": 1, + "min_per_call_nanos": 742243.84375, + "median_per_call_nanos": 742243.84375, + "max_per_call_nanos": 742243.84375}, + {"relative_spread": 0, + "param": 10, + "ok_count": 1, + "min_per_call_nanos": 994128.375, + "median_per_call_nanos": 994128.375, + "max_per_call_nanos": 994128.375}, + {"relative_spread": 0, + "param": 12, + "ok_count": 1, + "min_per_call_nanos": 1419906.953125, + "median_per_call_nanos": 1419906.953125, + "max_per_call_nanos": 1419906.953125}], + "spawn_floor_nanos": 22816820, + "slope": null, + "ratios": + [[4, 18887.468262], + [6, 13123.242839], + [8, 11597.560059], + [10, 9941.28375], + [12, 9860.464952]], + "points": + [{"trial_index": 0, + "total_nanos": 77363070, + "status": "ok", + "result_hash": "0xd125cbcffcdbb3a1", + "per_call_nanos": 302199.492188, + "peak_rss_kb": 60832, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 60471903, + "status": "ok", + "result_hash": "0xb674b30b3e491ead", + "per_call_nanos": 472436.742188, + "peak_rss_kb": 60836, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 95007212, + "status": "ok", + "result_hash": "0xe207bbfd1454f77", + "per_call_nanos": 742243.84375, + "peak_rss_kb": 60112, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 63624216, + "status": "ok", + "result_hash": "0xbe23835dfeb75738", + "per_call_nanos": 994128.375, + "peak_rss_kb": 60232, + "part_of_verdict": true, + "param": 10, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 90874045, + "status": "ok", + "result_hash": "0x67a4e6fe2931f85d", + "per_call_nanos": 1419906.953125, + "peak_rss_kb": 60884, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runRefine1", + "env": + {"timestamp_unix_ms": 1783794954237, + "timestamp_iso": "2026-07-11T18:35:54Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [4, 6, 8, 10, 12], "kind": "custom"}, + "param_floor": 4, + "param_ceiling": 12, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 4, + "cache_mode": "warm"}, + "complexity_formula": "n * n", + "c_min": 9860.464952, + "c_max": 13123.242839, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 13150.027222, + "median_per_call_nanos": 13150.027222, + "max_per_call_nanos": 13150.027222}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 17187.675781, + "median_per_call_nanos": 17187.675781, + "max_per_call_nanos": 17187.675781}, + {"relative_spread": 0, + "param": 8, + "ok_count": 1, + "min_per_call_nanos": 21050.085449, + "median_per_call_nanos": 21050.085449, + "max_per_call_nanos": 21050.085449}, + {"relative_spread": 0, + "param": 10, + "ok_count": 1, + "min_per_call_nanos": 24386.145752, + "median_per_call_nanos": 24386.145752, + "max_per_call_nanos": 24386.145752}, + {"relative_spread": 0, + "param": 12, + "ok_count": 1, + "min_per_call_nanos": 28842.26709, + "median_per_call_nanos": 28842.26709, + "max_per_call_nanos": 28842.26709}], + "spawn_floor_nanos": 22847394, + "slope": null, + "ratios": + [[4, 821.876701], + [6, 477.435438], + [8, 328.907585], + [10, 243.861458], + [12, 200.293521]], + "points": + [{"trial_index": 0, + "total_nanos": 107725023, + "status": "ok", + "result_hash": "0x99bc4f2495506336", + "per_call_nanos": 13150.027222, + "peak_rss_kb": 59816, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 8192, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 70400720, + "status": "ok", + "result_hash": "0xc0bf9a4ff6d6ca0", + "per_call_nanos": 17187.675781, + "peak_rss_kb": 59840, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 86221150, + "status": "ok", + "result_hash": "0x9026af8b39c631d2", + "per_call_nanos": 21050.085449, + "peak_rss_kb": 60752, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 99885653, + "status": "ok", + "result_hash": "0xf6cb7feddb68424d", + "per_call_nanos": 24386.145752, + "peak_rss_kb": 60824, + "part_of_verdict": true, + "param": 10, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 59068963, + "status": "ok", + "result_hash": "0x7c47cfcdaf58dbfb", + "per_call_nanos": 28842.26709, + "peak_rss_kb": 60668, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runCertify", + "env": + {"timestamp_unix_ms": 1783794954779, + "timestamp_iso": "2026-07-11T18:35:54Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [4, 6, 8, 10, 12], "kind": "custom"}, + "param_floor": 4, + "param_ceiling": 12, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 6, + "cache_mode": "warm"}, + "complexity_formula": "n * n", + "c_min": 200.293521, + "c_max": 477.435438, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 3772561.1875, + "median_per_call_nanos": 3772561.1875, + "max_per_call_nanos": 3772561.1875}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 11906305.25, + "median_per_call_nanos": 11906305.25, + "max_per_call_nanos": 11906305.25}, + {"relative_spread": 0, + "param": 8, + "ok_count": 1, + "min_per_call_nanos": 58009423, + "median_per_call_nanos": 58009423, + "max_per_call_nanos": 58009423}, + {"relative_spread": 0, + "param": 10, + "ok_count": 1, + "min_per_call_nanos": 138416144, + "median_per_call_nanos": 138416144, + "max_per_call_nanos": 138416144}, + {"relative_spread": 0, + "param": 12, + "ok_count": 1, + "min_per_call_nanos": 481762762, + "median_per_call_nanos": 481762762, + "max_per_call_nanos": 481762762}, + {"relative_spread": 0, + "param": 14, + "ok_count": 1, + "min_per_call_nanos": 1094785951, + "median_per_call_nanos": 1094785951, + "max_per_call_nanos": 1094785951}, + {"relative_spread": 0, + "param": 16, + "ok_count": 1, + "min_per_call_nanos": 2310390073, + "median_per_call_nanos": 2310390073, + "max_per_call_nanos": 2310390073}, + {"relative_spread": 0, + "param": 18, + "ok_count": 1, + "min_per_call_nanos": 6519449742, + "median_per_call_nanos": 6519449742, + "max_per_call_nanos": 6519449742}, + {"relative_spread": 0, + "param": 20, + "ok_count": 1, + "min_per_call_nanos": 4018060104, + "median_per_call_nanos": 4018060104, + "max_per_call_nanos": 4018060104}], + "spawn_floor_nanos": 23111676, + "slope": 0.265752, + "ratios": + [[4, 3684.141785], + [6, 1531.160655], + [8, 1770.307098], + [10, 1384.16144], + [12, 1936.096491], + [14, 2035.584041], + [16, 2203.359674], + [18, 3450.232933], + [20, 1255.643783]], + "points": + [{"trial_index": 0, + "total_nanos": 60360979, + "status": "ok", + "result_hash": "0x803bdbcf79747a0b", + "per_call_nanos": 3772561.1875, + "peak_rss_kb": 60756, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 95250442, + "status": "ok", + "result_hash": "0x43746460fa07ed9c", + "per_call_nanos": 11906305.25, + "peak_rss_kb": 60772, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 58009423, + "status": "ok", + "result_hash": "0x17d9b84ae6e53a4b", + "per_call_nanos": 58009423, + "peak_rss_kb": 61088, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 138416144, + "status": "ok", + "result_hash": "0xd9e6d701d18ba198", + "per_call_nanos": 138416144, + "peak_rss_kb": 60024, + "part_of_verdict": true, + "param": 10, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 481762762, + "status": "ok", + "result_hash": "0x8c7900c32041027", + "per_call_nanos": 481762762, + "peak_rss_kb": 61212, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1094785951, + "status": "ok", + "result_hash": "0xf0fba15f6d07106e", + "per_call_nanos": 1094785951, + "peak_rss_kb": 61340, + "part_of_verdict": true, + "param": 14, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 2310390073, + "status": "ok", + "result_hash": "0xb2247c474d679abb", + "per_call_nanos": 2310390073, + "peak_rss_kb": 61308, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 6519449742, + "status": "ok", + "result_hash": "0xe352a49462e400c3", + "per_call_nanos": 6519449742, + "peak_rss_kb": 59296, + "part_of_verdict": true, + "param": 18, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 4018060104, + "status": "ok", + "result_hash": "0xe04d9a38cc8e2885", + "per_call_nanos": 4018060104, + "peak_rss_kb": 60744, + "part_of_verdict": true, + "param": 20, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runIsolateAll", + "env": + {"timestamp_unix_ms": 1783794955358, + "timestamp_iso": "2026-07-11T18:35:55Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": + {"params": [4, 6, 8, 10, 12, 14, 16, 18, 20], "kind": "custom"}, + "param_floor": 4, + "param_ceiling": 20, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 20, + "cache_mode": "warm"}, + "complexity_formula": "n * n * n * n * n", + "c_min": 1255.643783, + "c_max": 3450.232933, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 3740418.5625, + "median_per_call_nanos": 3740418.5625, + "max_per_call_nanos": 3740418.5625}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 13037584.625, + "median_per_call_nanos": 13037584.625, + "max_per_call_nanos": 13037584.625}, + {"relative_spread": 0, + "param": 8, + "ok_count": 1, + "min_per_call_nanos": 60507236, + "median_per_call_nanos": 60507236, + "max_per_call_nanos": 60507236}, + {"relative_spread": 0, + "param": 10, + "ok_count": 1, + "min_per_call_nanos": 143896888, + "median_per_call_nanos": 143896888, + "max_per_call_nanos": 143896888}, + {"relative_spread": 0, + "param": 12, + "ok_count": 1, + "min_per_call_nanos": 493499879, + "median_per_call_nanos": 493499879, + "max_per_call_nanos": 493499879}, + {"relative_spread": 0, + "param": 14, + "ok_count": 1, + "min_per_call_nanos": 1121755315, + "median_per_call_nanos": 1121755315, + "max_per_call_nanos": 1121755315}, + {"relative_spread": 0, + "param": 16, + "ok_count": 1, + "min_per_call_nanos": 2364352425, + "median_per_call_nanos": 2364352425, + "max_per_call_nanos": 2364352425}], + "spawn_floor_nanos": 24320428, + "slope": null, + "ratios": + [[4, 3652.752502], + [6, 1676.644113], + [8, 1846.534302], + [10, 1438.96888], + [12, 1983.265332], + [14, 2085.729374], + [16, 2254.822183]], + "points": + [{"trial_index": 0, + "total_nanos": 59846697, + "status": "ok", + "result_hash": "0x35fcf0a24e2ce595", + "per_call_nanos": 3740418.5625, + "peak_rss_kb": 60580, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 104300677, + "status": "ok", + "result_hash": "0x4669ffb741a00196", + "per_call_nanos": 13037584.625, + "peak_rss_kb": 61120, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 60507236, + "status": "ok", + "result_hash": "0x944973d09f8fa1e4", + "per_call_nanos": 60507236, + "peak_rss_kb": 61424, + "part_of_verdict": true, + "param": 8, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 143896888, + "status": "ok", + "result_hash": "0x2176d56c90a7de2", + "per_call_nanos": 143896888, + "peak_rss_kb": 61236, + "part_of_verdict": true, + "param": 10, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 493499879, + "status": "ok", + "result_hash": "0x5c30f93bcc334745", + "per_call_nanos": 493499879, + "peak_rss_kb": 61120, + "part_of_verdict": true, + "param": 12, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 1121755315, + "status": "ok", + "result_hash": "0x27a0c649f1e08c1e", + "per_call_nanos": 1121755315, + "peak_rss_kb": 60288, + "part_of_verdict": true, + "param": 14, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 2364352425, + "status": "ok", + "result_hash": "0x83846a2a71bf4090", + "per_call_nanos": 2364352425, + "peak_rss_kb": 61000, + "part_of_verdict": true, + "param": 16, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runIsolate", + "env": + {"timestamp_unix_ms": 1783794970401, + "timestamp_iso": "2026-07-11T18:36:10Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [4, 6, 8, 10, 12, 14, 16], "kind": "custom"}, + "param_floor": 4, + "param_ceiling": 16, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 30, + "cache_mode": "warm"}, + "complexity_formula": "n * n * n * n * n", + "c_min": 1438.96888, + "c_max": 2254.822183, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 64, + "ok_count": 1, + "min_per_call_nanos": 6643.0979, + "median_per_call_nanos": 6643.0979, + "max_per_call_nanos": 6643.0979}, + {"relative_spread": 0, + "param": 96, + "ok_count": 1, + "min_per_call_nanos": 19493.402832, + "median_per_call_nanos": 19493.402832, + "max_per_call_nanos": 19493.402832}, + {"relative_spread": 0, + "param": 128, + "ok_count": 1, + "min_per_call_nanos": 19529.457275, + "median_per_call_nanos": 19529.457275, + "max_per_call_nanos": 19529.457275}, + {"relative_spread": 0, + "param": 192, + "ok_count": 1, + "min_per_call_nanos": 46874.458984, + "median_per_call_nanos": 46874.458984, + "max_per_call_nanos": 46874.458984}, + {"relative_spread": 0, + "param": 256, + "ok_count": 1, + "min_per_call_nanos": 46790.026855, + "median_per_call_nanos": 46790.026855, + "max_per_call_nanos": 46790.026855}], + "spawn_floor_nanos": 24691809, + "slope": null, + "ratios": + [[64, 1.62185], + [96, 2.11517], + [128, 1.191983], + [192, 1.271551], + [256, 0.713959]], + "points": + [{"trial_index": 0, + "total_nanos": 108840516, + "status": "ok", + "result_hash": "0x58287f338ded7c4a", + "per_call_nanos": 6643.0979, + "peak_rss_kb": 60192, + "part_of_verdict": true, + "param": 64, + "inner_repeats": 16384, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 79844978, + "status": "ok", + "result_hash": "0x30d5bbf2a1731352", + "per_call_nanos": 19493.402832, + "peak_rss_kb": 60724, + "part_of_verdict": true, + "param": 96, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 79992657, + "status": "ok", + "result_hash": "0x30d5bbf2a1731352", + "per_call_nanos": 19529.457275, + "peak_rss_kb": 60300, + "part_of_verdict": true, + "param": 128, + "inner_repeats": 4096, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 95998892, + "status": "ok", + "result_hash": "0x9de10954e8ec1aa1", + "per_call_nanos": 46874.458984, + "peak_rss_kb": 61172, + "part_of_verdict": true, + "param": 192, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 95825975, + "status": "ok", + "result_hash": "0x9de10954e8ec1aa1", + "per_call_nanos": 46790.026855, + "peak_rss_kb": 61200, + "part_of_verdict": true, + "param": 256, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runRefineTo", + "env": + {"timestamp_unix_ms": 1783794974968, + "timestamp_iso": "2026-07-11T18:36:14Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [64, 96, 128, 192, 256], "kind": "custom"}, + "param_floor": 64, + "param_ceiling": 256, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 4, + "cache_mode": "warm"}, + "complexity_formula": "t * t", + "c_min": 0.713959, + "c_max": 2.11517, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "consistent_with_declared_complexity", + "trial_summaries": + [{"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 414004.039062, + "median_per_call_nanos": 414004.039062, + "max_per_call_nanos": 414004.039062}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 2202618.53125, + "median_per_call_nanos": 2202618.53125, + "max_per_call_nanos": 2202618.53125}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 8226581.125, + "median_per_call_nanos": 8226581.125, + "max_per_call_nanos": 8226581.125}, + {"relative_spread": 0, + "param": 5, + "ok_count": 1, + "min_per_call_nanos": 27713973.5, + "median_per_call_nanos": 27713973.5, + "max_per_call_nanos": 27713973.5}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 78346357, + "median_per_call_nanos": 78346357, + "max_per_call_nanos": 78346357}], + "spawn_floor_nanos": 24492234, + "slope": null, + "ratios": + [[2, 12937.626221], + [3, 9064.273791], + [4, 8033.77063], + [5, 8868.47152], + [6, 10075.405993]], + "points": + [{"trial_index": 0, + "total_nanos": 52992517, + "status": "ok", + "result_hash": "0xd8ffc7ced4231e2b", + "per_call_nanos": 414004.039062, + "peak_rss_kb": 60980, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 128, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 70483793, + "status": "ok", + "result_hash": "0x7dd1aefc55b8dae7", + "per_call_nanos": 2202618.53125, + "peak_rss_kb": 59524, + "part_of_verdict": true, + "param": 3, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 65812649, + "status": "ok", + "result_hash": "0xe0b4f8d60c0a264e", + "per_call_nanos": 8226581.125, + "peak_rss_kb": 60652, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 8, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 55427947, + "status": "ok", + "result_hash": "0xbc18efaec363654c", + "per_call_nanos": 27713973.5, + "peak_rss_kb": 61008, + "part_of_verdict": true, + "param": 5, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 78346357, + "status": "ok", + "result_hash": "0x6519358031d0ea70", + "per_call_nanos": 78346357, + "peak_rss_kb": 60588, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runIsolateNk", + "env": + {"timestamp_unix_ms": 1783794975594, + "timestamp_iso": "2026-07-11T18:36:15Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [2, 3, 4, 5, 6], "kind": "custom"}, + "param_floor": 2, + "param_ceiling": 6, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 8, + "cache_mode": "warm"}, + "complexity_formula": "n * n * n * n * n", + "c_min": 8033.77063, + "c_max": 10075.405993, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 272850.675781, + "median_per_call_nanos": 272850.675781, + "max_per_call_nanos": 272850.675781}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 1831705.3125, + "median_per_call_nanos": 1831705.3125, + "max_per_call_nanos": 1831705.3125}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 5781410, + "median_per_call_nanos": 5781410, + "max_per_call_nanos": 5781410}, + {"relative_spread": 0, + "param": 5, + "ok_count": 1, + "min_per_call_nanos": 14711062.5, + "median_per_call_nanos": 14711062.5, + "max_per_call_nanos": 14711062.5}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 34966203, + "median_per_call_nanos": 34966203, + "max_per_call_nanos": 34966203}], + "spawn_floor_nanos": 24116385, + "slope": null, + "ratios": + [[2, 8526.583618], + [3, 7537.881944], + [4, 5645.908203], + [5, 4707.54], + [6, 4496.682485]], + "points": + [{"trial_index": 0, + "total_nanos": 69849773, + "status": "ok", + "result_hash": "0xd8ffc7ced4231e2b", + "per_call_nanos": 272850.675781, + "peak_rss_kb": 59844, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 58614570, + "status": "ok", + "result_hash": "0x7dd1aefc55b8dae7", + "per_call_nanos": 1831705.3125, + "peak_rss_kb": 59880, + "part_of_verdict": true, + "param": 3, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 92502560, + "status": "ok", + "result_hash": "0xe0b4f8d60c0a264e", + "per_call_nanos": 5781410, + "peak_rss_kb": 60660, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 58844250, + "status": "ok", + "result_hash": "0xbc18efaec363654c", + "per_call_nanos": 14711062.5, + "peak_rss_kb": 60324, + "part_of_verdict": true, + "param": 5, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 69932406, + "status": "ok", + "result_hash": "0x6519358031d0ea70", + "per_call_nanos": 34966203, + "peak_rss_kb": 60292, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runIsolatePellet", + "env": + {"timestamp_unix_ms": 1783794976114, + "timestamp_iso": "2026-07-11T18:36:16Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [2, 3, 4, 5, 6], "kind": "custom"}, + "param_floor": 2, + "param_ceiling": 6, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 8, + "cache_mode": "warm"}, + "complexity_formula": "n * n * n * n * n", + "c_min": 4496.682485, + "c_max": 7537.881944, + "budget_truncated": false, + "advisories": []}, + {"verdict_dropped_leading": 1, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 288364.375, + "median_per_call_nanos": 288364.375, + "max_per_call_nanos": 288364.375}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 2049771.0625, + "median_per_call_nanos": 2049771.0625, + "max_per_call_nanos": 2049771.0625}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 6220360.625, + "median_per_call_nanos": 6220360.625, + "max_per_call_nanos": 6220360.625}, + {"relative_spread": 0, + "param": 5, + "ok_count": 1, + "min_per_call_nanos": 15184484.5, + "median_per_call_nanos": 15184484.5, + "max_per_call_nanos": 15184484.5}, + {"relative_spread": 0, + "param": 6, + "ok_count": 1, + "min_per_call_nanos": 36157814, + "median_per_call_nanos": 36157814, + "max_per_call_nanos": 36157814}], + "spawn_floor_nanos": 23207569, + "slope": null, + "ratios": + [[2, 9011.386719], + [3, 8435.271862], + [4, 6074.570923], + [5, 4859.03504], + [6, 4649.92464]], + "points": + [{"trial_index": 0, + "total_nanos": 73821280, + "status": "ok", + "result_hash": "0xd8ffc7ced4231e2b", + "per_call_nanos": 288364.375, + "peak_rss_kb": 59844, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 65592674, + "status": "ok", + "result_hash": "0x7dd1aefc55b8dae7", + "per_call_nanos": 2049771.0625, + "peak_rss_kb": 61088, + "part_of_verdict": true, + "param": 3, + "inner_repeats": 32, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 99525770, + "status": "ok", + "result_hash": "0xe0b4f8d60c0a264e", + "per_call_nanos": 6220360.625, + "peak_rss_kb": 60400, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 16, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 60737938, + "status": "ok", + "result_hash": "0xbc18efaec363654c", + "per_call_nanos": 15184484.5, + "peak_rss_kb": 60692, + "part_of_verdict": true, + "param": 5, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 72315628, + "status": "ok", + "result_hash": "0x6519358031d0ea70", + "per_call_nanos": 36157814, + "peak_rss_kb": 60748, + "part_of_verdict": true, + "param": 6, + "inner_repeats": 2, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": "Hex.RootsBench.runIsolateNkThenPellet", + "env": + {"timestamp_unix_ms": 1783794976676, + "timestamp_iso": "2026-07-11T18:36:16Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [2, 3, 4, 5, 6], "kind": "custom"}, + "param_floor": 2, + "param_ceiling": 6, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 8, + "cache_mode": "warm"}, + "complexity_formula": "n * n * n * n * n", + "c_min": 4649.92464, + "c_max": 8435.271862, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1783794950864, + "timestamp_iso": "2026-07-11T18:35:50Z", + "platform_target": "x86_64-unknown-linux-gnu", + "os": "linux", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "chungus2", + "git_dirty": true, + "git_commit": "b08a66cce522b2434022a5493e71ce41ee206e3b", + "exe_name": "hexroots_bench", + "cpu_model": "AMD EPYC 9455 48-Core Processor", + "cpu_cores": 96, + "arch": "x86_64"}} diff --git a/reports/bench-results/hex-roots-flint-b08a66cce522.json b/reports/bench-results/hex-roots-flint-b08a66cce522.json new file mode 100644 index 000000000..d637d568e --- /dev/null +++ b/reports/bench-results/hex-roots-flint-b08a66cce522.json @@ -0,0 +1,125 @@ +{ + "comparator": "python-flint fmpz_poly.complex_roots", + "python_flint_version": "0.9.0", + "prec_bits": 32, + "overhead_s": 1.0820222087204456e-06, + "rows": [ + { + "degree": 4, + "median_s": 1.1988013284280896e-05, + "n_roots": 4, + "repeats": 50, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 6, + "median_s": 1.770147355273366e-05, + "n_roots": 6, + "repeats": 50, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 8, + "median_s": 2.6308989617973566e-05, + "n_roots": 8, + "repeats": 50, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 10, + "median_s": 3.578397445380688e-05, + "n_roots": 10, + "repeats": 50, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 12, + "median_s": 7.655352237634361e-05, + "n_roots": 12, + "repeats": 50, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 14, + "median_s": 0.00010304249008186162, + "n_roots": 14, + "repeats": 20, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 16, + "median_s": 7.710899808444083e-05, + "n_roots": 16, + "repeats": 20, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 18, + "median_s": 9.669348946772516e-05, + "n_roots": 18, + "repeats": 8, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + }, + { + "degree": 20, + "median_s": 0.00016736300312913954, + "n_roots": 20, + "repeats": 8, + "coeffs_head": [ + -7, + -2, + -3, + -5, + 3 + ] + } + ] +} diff --git a/reports/figures/hex-roots-comparator-seeded-dense.svg b/reports/figures/hex-roots-comparator-seeded-dense.svg new file mode 100644 index 000000000..6eee23fbb --- /dev/null +++ b/reports/figures/hex-roots-comparator-seeded-dense.svg @@ -0,0 +1,2321 @@ + + + + + + + + 2026-07-11T18:53:49.646252 + image/svg+xml + + + Matplotlib v3.10.9, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/reports/hexroots-performance.md b/reports/hexroots-performance.md new file mode 100644 index 000000000..e75255af4 --- /dev/null +++ b/reports/hexroots-performance.md @@ -0,0 +1,353 @@ +# HexRoots Performance Report + +**Phase 4 is not claimed for HexRoots.** The scientific run below returns +*inconclusive* for 9 of the 13 parametric registrations, and two of the three +SPEC time budgets fail, so `libraries.yml` keeps `HexRoots.done_through: 3`. +The §Concerns subsection is therefore non-empty; each entry names the finding +and its root cause. This report is the record of the Phase-4 measurement work +and of why the phase is not yet exitable, per +[PLAN/Phase4.md](../PLAN/Phase4.md) and +[SPEC/benchmarking.md §Headline reports](../SPEC/benchmarking.md#headline-reports). + +All numbers come from commit `b08a66cce522` on `chungus2` (AMD EPYC 9455 +48-Core, linux `x86_64`, kernel 6.12.95), Lean `4.32.0-rc1`, lean-bench +`0.1.0`, `python-flint 0.9.0`. The harness recorded `git_dirty: true` because +the retuned bench module and this report were staged but uncommitted at run +time (the same convention as hex-real-roots); the recorded commit is the branch +point `b08a66cce522`. + +## Bench Targets + +Declared complexities copied verbatim from the `setup_benchmark` registration +sites in `bench/HexRoots/Bench.lean`. These are *wall-time* models: the SPEC +op-count contract multiplied by the family's working-bit-length growth `B` +where that growth is asymptotically significant on the schedule (each +registration's comment records the reconciliation). + +- `Hex.RootsBench.runTaylor`: `n * n` +- `Hex.RootsBench.runMahlerPrec`: `n` +- `Hex.RootsBench.runWitnessCheck`: `n * n` +- `Hex.RootsBench.runNkWitnessCheck`: `n * n` +- `Hex.RootsBench.runNewtonSquare`: `n * n` +- `Hex.RootsBench.runRefine1`: `n * n` +- `Hex.RootsBench.runCertify`: `n * n` +- `Hex.RootsBench.runIsolateAll`: `n * n * n * n * n` +- `Hex.RootsBench.runIsolate`: `n * n * n * n * n` +- `Hex.RootsBench.runRefineTo`: `t * t` +- `Hex.RootsBench.runIsolateNk`: `n * n * n * n * n` +- `Hex.RootsBench.runIsolatePellet`: `n * n * n * n * n` +- `Hex.RootsBench.runIsolateNkThenPellet`: `n * n * n * n * n` +- `Hex.RootsBench.runSameRoot`: fixed benchmark, `repeats = 5` + +Three input families (`libraries.yml: HexRoots.phase4.input_families`): +`seeded-dense` (seed-`0xC0FFEE` dense integer polynomials, coefficients in +`[-10, 10]`, generically distinct irrational roots — the whole-polynomial +drivers, `taylor`, `mahlerPrec`, `refine1`, `certify`), `wilkinson-linprod` +(`∏(X−j)`, `j = 1..n`, integer roots — the witness/Newton primitives and the +dual-route compare group), and `refine-fixed` (the degree-3 `(x−1)(x−2)(x+3)` +whose atom `refineTo?`/`sameRoot` sharpen). + +### Op-count-vs-wall reconciliation (Phase4.md performance rationale) + +The registration comments were retuned from pure exact-dyadic op-counts to +wall-time models. Which op-count models changed, and why: + +- **`runTaylor` stays `n²`.** The SPEC op-count is `n²` synthetic-division + multiply/adds. The fixed centre `1/4 + i/8 = 2^{−3}(2+i)` is *non-integer*, + so `z^{j−k}` carries denominator `2^{3(j−k)}` and the coefficients reach + `B = Θ(n)` bits; each inner op multiplies a `B`-bit operand by the fixed + `3`-bit centre (`O(B)`), giving an `n³` bit-cost asymptote. On the reachable + `16..256` (probed to `1024`) schedule the operands stay `≤ 48` GMP words — + the allocation-dominated transition band — so wall tracks `~n^{2.25}`, short + of the `n³` asymptote. `n²` is declared as the SPEC op-count; the residual is + a Concern (below). +- **`runMahlerPrec`, `runWitnessCheck`, `runNkWitnessCheck`, `runNewtonSquare`, + `runRefine1`, `runCertify` stay at their op-counts (`n`, `n²`).** `mahlerPrec` + is word-size integer arithmetic (`B` constant). The witness/Newton/refine + primitives run on integer-centred `wilkinson-linprod` (no denominator growth, + integer Taylor coefficients of `O(n log n)` bits staying sub-word `≤ 44` bits + through `n = 16`) or on low-precision seeded mid-refinement components + (`O(n)`-bit coefficients staying sub-word through `n = 12`), so the operands + are flat and wall tracks the op count. The bit-growth sits in the constant. +- **`runIsolateAll`, `runIsolate`, and the three compare-group targets changed + `n³ → n⁵`.** The SPEC contract is `O(n³·B²)` bit operations; the + whole-polynomial drivers reach a working bit-length `B = Θ(n)` (target + precision plus the seeded `n·log‖p‖∞` term plus the Taylor coefficients' + `Θ(prec·n)` denominator growth), and the growing-precision dyadic arithmetic + — notably the `invAtPrec` reciprocal — is schoolbook `O(B²)`. `O(n³·B²)` with + `B = Θ(n)` gives the `n⁵` wall model, folding the bit-growth into the + exponent because it is asymptotically significant here (unlike the flat-band + primitives above). +- **`runRefineTo` stays `t²`.** At fixed degree the parameter is the target + precision `t`; the dominant final witness does a fixed number of `t × t` + schoolbook multiplies, `O(t²)`. + +## Verdicts + +Scientific run, one command, exporting +`reports/bench-results/hex-roots-b08a66cce522.json`: + +```sh +lake exe hexroots_bench run \ + Hex.RootsBench.runTaylor Hex.RootsBench.runMahlerPrec \ + Hex.RootsBench.runWitnessCheck Hex.RootsBench.runNkWitnessCheck \ + Hex.RootsBench.runNewtonSquare Hex.RootsBench.runRefine1 \ + Hex.RootsBench.runCertify Hex.RootsBench.runIsolateAll \ + Hex.RootsBench.runIsolate Hex.RootsBench.runRefineTo \ + Hex.RootsBench.runIsolateNk Hex.RootsBench.runIsolatePellet \ + Hex.RootsBench.runIsolateNkThenPellet \ + --export-file reports/bench-results/hex-roots-b08a66cce522.json +``` + +Inputs are deterministic; no random seeds are involved. Every verdict verbatim +(`β` is the residual log-log slope of `C = per-call / model`; the harness calls +a run *consistent* iff `|β| ≤ 0.15`, or, on a log-x range too narrow to fit a +slope, iff `cMax/cMin ≤ max(1.5, exp(0.15·xRange))`): + +| registration | model | verdict | β / range | final-param hash | +|---|---|---|---|---| +| `runTaylor` | `n²` | **inconclusive** | `β=+0.415` (slower by `~n^0.42`) | `0x1242736d713af35b` @256 | +| `runMahlerPrec` | `n` | consistent | `β=−0.148` | `0xc83…` @256 | +| `runWitnessCheck` | `n²` | **inconclusive** | `β=−0.227` (faster by `~n^0.23`) | `0xb` @16 | +| `runNkWitnessCheck` | `n²` | consistent | `β=−0.095` | `0xb` @16 | +| `runNewtonSquare` | `n²` | **inconclusive** | `β=+0.198` (slower by `~n^0.20`) | `0x450307c7dcbe905c` @16 | +| `runRefine1` | `n²` | consistent | range check (`cMax/cMin=1.33`) | `0x67a4e6fe2931f85d` @12 | +| `runCertify` | `n²` | **inconclusive** | range check (`cMax/cMin=2.38`) | `0x7c47cfcdaf58dbfb` @12 | +| `runIsolateAll` | `n⁵` | **inconclusive** | `β=+0.266` (slower by `~n^0.27`) | `0xe04d9a38cc8e2885` @20 | +| `runIsolate` | `n⁵` | **inconclusive** | range check (`cMax/cMin=1.57`) | `0x83846a2a71bf4090` @16 | +| `runRefineTo` | `t²` | **inconclusive** | range check (`cMax/cMin=2.96`) | `0x9de10954e8ec1aa1` @256 | +| `runIsolateNk` | `n⁵` | consistent | range check (`cMax/cMin=1.25`) | `0x6519358031d0ea70` @6 | +| `runIsolatePellet` | `n⁵` | **inconclusive** | range check (`cMax/cMin=1.68`) | `0x6519358031d0ea70` @6 | +| `runIsolateNkThenPellet` | `n⁵` | **inconclusive** | range check (`cMax/cMin=1.81`) | `0x6519358031d0ea70` @6 | + +**4 consistent, 9 inconclusive.** The fixed `runSameRoot` benchmark: +median `132 ns` (min `130`, max `134`, `×2^13` inner repeats), all repeats +agree on hash `0xb`, matching the registered `expectedHash`. + +The nine inconclusive verdicts are analysed in §Concerns. They fall into four +root causes, none of which is a wrong-asymptotic *implementation* bug that a +`done_through` rollback of the `def` would fix: the fixed non-integer Taylor +centre's transition-band growth, the startup-dominated microsecond band of the +small-degree witness benches, the seeded family's degree-dependent (hence +non-power-law) root geometry, and `refineTo`'s Newton-doubling precision +quantisation. They are benchmark-family / schedule findings. + +## Comparator Ratios + +`HexRoots/SPEC/hex-roots.md` names python-flint (`fmpz_poly.complex_roots`, the +ci-tier oracle) and MPSolve (the local-tier / Phase-4 external comparator). +Both are classified `informational` in +`libraries.yml: HexRoots.phase4.comparators`; neither gates Phase 4. The +per-library yardstick is the SPEC's time budgets, not a constant-factor `1×` +goal, because both comparators are multiprecision-float/ball engines +structurally different from this library's decidable exact-integer +certificates. + +### python-flint (`informational`, run) + +`scripts/bench/hexroots_flint_compare.py` times `fmpz_poly.complex_roots()` at +`ctx.prec = 32` on the *same* seed-`0xC0FFEE` dense integer ladder the +whole-polynomial drivers use (the LCG replication is byte-verified against the +Lean `seededCoeffs`: `seededCoeffs 4 = [-7,-2,-3,-5,3]`, +`seededCoeffs 8 = [-7,-2,-3,-5,3,1,-7,-3,-4]` in both). All degrees run in one +warm process; the measured per-call overhead (`complex_roots` on the trivial +`x²−2`) is `1.08 µs`, exceeding 5 % of flint wall time only at `n = 4, 6`, +where both raw and overhead-adjusted ratios are shown. Data: +`reports/bench-results/hex-roots-flint-b08a66cce522.json`; hex per-call from +the `runIsolateAll` rows of `hex-roots-b08a66cce522.json`. + +| degree | hex `isolateAll?@32` | flint | flint adj. | ratio hex/flint | adj. ratio | +|---:|---:|---:|---:|---:|---:| +| 4 | 3.77 ms | 12.0 µs | 10.9 µs | 315 | 346 | +| 6 | 11.9 ms | 17.7 µs | 16.6 µs | 673 | 716 | +| 8 | 58.0 ms | 26.3 µs | 25.2 µs | 2205 | 2300 | +| 10 | 138.4 ms | 35.8 µs | 34.7 µs | 3868 | 3989 | +| 12 | 481.8 ms | 76.6 µs | 75.5 µs | 6293 | 6383 | +| 14 | 1.095 s | 103.0 µs | 102.0 µs | 10625 | 10737 | +| 16 | 2.310 s | 77.1 µs | 76.0 µs | 29963 | 30389 | +| 18 | 6.519 s | 96.7 µs | 95.6 µs | 67424 | 68187 | +| 20 | 4.018 s | 167.4 µs | 166.3 µs | 24008 | 24164 | + +**Trend.** The ratio *diverges* as degree grows (315× at `n=4` to `~30000×` at +`n=16`; the `n=18/20` scatter tracks the seeded family's non-monotonicity, not +the trend). flint stays sub-`200 µs` across the whole ladder — its +ball-arithmetic root finder is nearly flat here — while hex is `~n⁵` certified +exact arithmetic, so the gap widens by roughly `n⁴` per the models. This is the +expected shape for an integer-certified isolator against a float engine and is +not a Concern under the informational classification; the yardstick is the SPEC +time budgets (§below), which is where hex's absolute cost is judged. Plot: +`reports/figures/hex-roots-comparator-seeded-dense.svg` +(`scripts/plots/hex-roots-comparator.py --family seeded-dense`); the +`wilkinson-linprod` and `refine-fixed` families carry no external-comparator +series and MPSolve is scheduled-only, so no second curve is drawn for them. + +### MPSolve (`informational`, scheduled-only) + +Not wired in this PR. Required environment (stated in +`bench/HexRoots/Bench.lean`): the `mpsolve` CLI (`unisa-cs/mpsolve`, built with +GMP) on `PATH`, driven on the seeded ladder via `-au -Gi` isolate mode. +Rationale for the informational class: MPSolve is a multiprecision-float C +library computing approximate root inclusions, structurally different from this +library's integer-certified Lean witnesses. + +### Cross-strategy compare group (internal, `allAgreed`) + +```sh +lake exe hexroots_bench compare \ + Hex.RootsBench.runIsolateNk Hex.RootsBench.runIsolatePellet \ + Hex.RootsBench.runIsolateNkThenPellet +``` + +reports `agreement: all functions agree on common params` over the shared +`wilkinson-linprod` domain (`n = 2, 3, 4, 5, 6`): the strategy-invariant +`rootsDigest` (atom count + integer-grid centre buckets) is identical across +`.nk`, `.pellet`, and `.nkThenPellet` (final hash `0x6519358031d0ea70` at +`n = 6` for all three), the cross-implementation conformance check the compare +group exists for. This is the dual-route experiment's measurement record. The +per-degree strategy timings and the `pellet/nk` ratio: + +| degree | `.nk` | `.pellet` | `.nkThenPellet` | pellet/nk | +|---:|---:|---:|---:|---:| +| 2 | 0.414 ms | 0.273 ms | 0.288 ms | 0.659 | +| 3 | 2.203 ms | 1.832 ms | 2.050 ms | 0.832 | +| 4 | 8.227 ms | 5.781 ms | 6.220 ms | 0.703 | +| 5 | 27.71 ms | 14.71 ms | 15.18 ms | 0.531 | +| 6 | 78.35 ms | 34.97 ms | 36.16 ms | 0.446 | + +On this integer-root family the **Pellet-only route is the faster one, and +increasingly so with degree** (ratio `0.66 → 0.45`): Pellet certifies at a +coarser precision than the sup-norm Newton-Kantorovich witness needs, so the +`.nk` route subdivides more levels. `.nkThenPellet` tracks `.pellet` closely +(NK does not fire early on these coarse squares, so the default falls through to +Pellet after one NK attempt). This is a genuine dual-route finding for the +companion's eventual route-retirement decision: on well-separated integer roots +Pellet wins; the NK route's advantage (exact first-order bounds, no `√2`) is not +visible on this family at these degrees. + +## Profile + +`perf record -g -F 999` on the in-process `_child` batch runner +(`hexroots_bench _child --bench --param --target-nanos 3000000000`), +one representative case per `phase4.input_families` entry, same commit and host +as the scientific run. Leaf self-time is categorised across +{own code, GMP, allocation, Lean runtime}; own code = `l_Hex_*`, `lp_Hex_*`, +`l_Dyadic_*`, `l_GaussDyadic_*`, and the dyadic-mantissa integer leaves +(`l_Int_*`). `perf.data` artefacts are developer-local under `/tmp` and are not +committed. + +### `seeded-dense` — `runIsolateAll` at `n = 16` (2447 samples) + +Leaf self-time: GMP 32.9 % (`__gmpz_init_set` 7.6 %, `__gmpz_cmp_si` 2.6 %, +`__gmpz_add` 2.1 %, `__gmpz_realloc`/`__gmpn_*`), allocation 21.5 % +(`malloc` 7.5 %, `cfree` 7.1 %, `realloc`, `mi_*`), Lean runtime 22.7 % +(`lean_dec_ref_cold`, `lean::mpz_to_int`, `lean::mpz::~mpz`), own code 19.0 % +(`l_Dyadic_add` 3.8 %, `l_Dyadic_mul` 1.9 %, `l_Int_trailingZeros_aux`, +`lp_Hex_…taylor`); 96.2 % classified. This is the growing-precision regime the +`n⁵` model predicts: the working bit-length reaches multiple GMP words, so GMP +big-integer arithmetic and its allocation/box-unbox traffic dominate, flowing +inclusively through the registered `isolateAll?` → `taylor`/`witnessCheck` +path. + +### `wilkinson-linprod` — `runIsolateNkThenPellet` at `n = 6` (2489 samples) + +Leaf self-time: **own code 44.9 %** (`l_Int_trailingZeros_aux` 9.3 %, +`l_Dyadic_add` 7.4 %, `l_Dyadic_mul` 5.3 %, `l_Dyadic_ofIntWithPrec` 3.0 %, +`l_Int_shiftLeft`), GMP 19.3 % (`__gmpz_mul_2exp` 3.2 %), allocation 15.1 %, +Lean runtime 17.6 %; 97.0 % classified. The own-code share is more than double +the seeded family's, exactly the flat, sub-word band the `n²`/`n⁵`-op-count +derivations claim for the integer-centred `linProdPoly`: operands stay small, +so the actual `Dyadic` arithmetic (own code) dominates rather than GMP. The +inclusive path is the registered `isolate`/compare-group driver. + +### `refine-fixed` — `runRefineTo` at `t = 256` (3180 samples) + +Leaf self-time: GMP 30.0 % (`__gmpz_init_set` 4.9 %, +`__gmpn_divrem_1_x86_64` 2.6 % — the `t`-bit reciprocal — `__gmp_default_*`), +allocation 24.7 % (`cfree` 7.2 %, `malloc` 6.3 %, `_int_free_chunk`, +`realloc`), Lean runtime 19.9 % (`lean_dec_ref_cold`, `lean_nat_big_sub`), own +code 18.3 % (`l_Int_trailingZeros_aux` 4.3 %, `l_Dyadic_add`); 92.9 % +classified. The `t`-bit division/multiplication and its allocation churn +dominate, consistent with the `t²` schoolbook model; inclusive cost is the +registered `refineTo?`. + +**Attribution rule.** Every dominant inclusive path terminates in a registered +bench target (`isolateAll?`/`isolate`, `taylor`, `witnessCheck`/ +`nkWitnessCheck`, `newtonSquare`, `refine1`/`certify`, `refineTo?`), so no +unregistered helper dominates and no new target is required. (Lean's +closure-call unwinding fragments some inclusive attribution into an unresolved +`0x1` frame ~6 %, a `perf`/RTS artefact, not an unregistered hot path.) + +## Concerns + +Phase 4 is blocked; `done_through` stays `3`. Each Concern is a +benchmark-family / schedule / budget finding, with the diagnosis that closes it. +None is a wrong-asymptotic implementation bug that rolling back a `def` would +fix; the resolutions are Phase-4 benchmark re-scaffolding (new schedules, a +smooth driver family, an integer Taylor centre) plus a SPEC time-budget +re-appraisal. + +1. **`runIsolate`, `runIsolateAll` inconclusive — seeded-family + non-monotonicity.** At `n⁵` the residual is small (`β=+0.266` for + `isolateAll`), but the seeded polynomials' degree-dependent root geometry + makes wall time non-monotonic in `n` (e.g. `isolateAll` at `n=18` is + `6.52 s` but `n=20` is `4.02 s`, because `seededPoly 18` happens to have a + closer root pair), so no power-law fit is clean. Resolution: replace the + per-degree-varying seed with a family whose isolation difficulty is smooth + in `n` (e.g. a fixed root-separation product), then re-measure `n⁵`. + +2. **`runIsolatePellet`, `runIsolateNkThenPellet` inconclusive — narrow-range + range check.** `n⁵` is the right model (`runIsolateNk` on the same domain is + *consistent*), but the 5-rung `n=2..6` schedule is too narrow for a slope + fit, so the verdict falls to the multiplicative range check, which the + slightly-sub-`n⁵` Pellet growth (`cMax/cMin = 1.68`, `1.81`) fails against + the `1.5` noise floor. Resolution: widen the compare-group schedule + (larger degrees, or in-fill rungs) so a slope fit governs the verdict. + +3. **`runTaylor` inconclusive — non-integer-centre transition band.** The fixed + centre `1/4 + i/8` gives `Θ(n)` denominator growth, so wall scales + `~n^{2.25}` (probed to `n=1024`), between the `n²` op-count and the `n³` + bit-op asymptote; neither clean power is consistent (`n²` gives `β=+0.42`). + The analogous hex-real-roots `runMobiusTransform` is consistent at `n²` + precisely because it uses an *integer* interval endpoint. Resolution: an + integer Taylor centre for the benchmark, or declare and reach the `n³` + multiplication-bound regime (operand word counts an order of magnitude past + the wallclock cap). + +4. **`runWitnessCheck`, `runNewtonSquare`, `runCertify` inconclusive — + startup-dominated microsecond band.** These run in `1–45 µs` on the small + `n ≤ 12/16` schedules, where the fixed per-call overhead (array allocation, + checksum) makes the `C` curve U-shaped (`witnessCheck` `β=−0.23`, + `newtonSquare` `β=+0.20`, `certify` monotone-decreasing), so `n²` does not + fit cleanly even though the operands are provably flat. `runRefine1` and + `runNkWitnessCheck` on the same band happen to pass. Resolution: raise the + schedules into a signal band clear of startup (larger degrees, keeping + operands sub-word), or hoist more of the per-call fixed cost out of the + timed body. + +5. **`runRefineTo` inconclusive — Newton-doubling precision quantisation.** + Speculative Newton doubles precision per jump, so `refineTo?` reaches a + *discrete* precision ladder and the per-call work is a step function of the + target `t` (`t=96` and `t=128` do equal work; likewise `t=192`, `t=256`), + not smooth in `t`. `t²` cannot fit a staircase. Resolution: parametrise the + benchmark by the *number of Newton jumps* (monotone in work) rather than the + raw target precision. + +6. **SPEC time budget: degree 50 @ prec 64 FAILS.** SPEC target `< 10 s`. + Measured with `isolateAll? (seededPoly 50) 64` (used because + `separationDepth(deg 50) ≫ 64`, per the SPEC note): single call + **495.85 s** (`chk = 4218`, 50 atoms), **`49.6×` over budget**. Resolution: + this is a rough-first-guess budget the implementation does not meet at `n⁵` + scaling; either the budget is re-appraised against MPSolve (its stated + purpose) or the driver is optimised (Graeffe iteration, deferred in the + SPEC, would cut the `ceilLog2(deg)` separation-depth factor). + +7. **SPEC time budget: degree 100 @ prec 128 FAILS.** SPEC target `< 1 min`. + Measured with `isolateAll? (seededPoly 100) 128`: the single call did **not + complete within a 19-minute window** (`> 1143 s`, already `> 19×` the budget, + then stopped; extrapolating the `n⁵·B²` model from the degree-50 point puts + the true time in the hours). Same resolution as Concern 6. + +For reference, the one budget that is met: **degree 10 @ prec 32** runs in +`0.137 s` (`isolateAll? (seededPoly 10) 32`, compiled, calibrated against the +`runIsolateAll` `n=10` bench row of `138 ms`), comfortably under the `< 1 s` +target. diff --git a/scripts/bench/hexroots_flint_compare.py b/scripts/bench/hexroots_flint_compare.py new file mode 100644 index 000000000..c2801eb2b --- /dev/null +++ b/scripts/bench/hexroots_flint_compare.py @@ -0,0 +1,125 @@ +#!/usr/bin/env python3 +"""Informational python-flint comparator for hex-roots complex root isolation. + +Times `flint.fmpz_poly.complex_roots()` on the same seed-`0xC0FFEE` dense +integer polynomial ladder that `bench/HexRoots/Bench.lean`'s whole-polynomial +drivers use (`seededPoly`), so the ratio `hex isolateAll?@32 / flint` per degree +in `reports/hexroots-performance.md` is apples-to-apples on the input. + +This is an `informational` process-call comparator (SPEC/benchmarking.md +§External comparators): FLINT's `complex_roots` is a multiprecision Arb +ball-arithmetic engine, structurally different from hex-roots' decidable +exact-integer Pellet / Newton-Kantorovich certificates, so it orients but does +not gate Phase 4. All degrees run in one warm process; the process-startup and +per-call floors are measured separately and reported. + +Reproduce under a `python-flint >= 0.9.0` virtualenv: + + python3 -m venv /tmp/rootsvenv && /tmp/rootsvenv/bin/pip install python-flint + /tmp/rootsvenv/bin/python scripts/bench/hexroots_flint_compare.py + +Emits one JSON object on stdout: {"prec_bits", "overhead_s", per-degree rows}. +""" +from __future__ import annotations + +import json +import statistics +import sys +import time + +MASK64 = (1 << 64) - 1 + + +from pathlib import Path + +REPO_ROOT = Path(__file__).resolve().parents[2] + + +def verify_lcg_matches_lean() -> None: + """Tether this reimplementation to the Lean bench family: the LCG + multiplier and increment literals must appear in + bench/HexRoots/Bench.lean, or the comparator is no longer + apples-to-apples and must fail loudly rather than time a divergent + input family.""" + src = (REPO_ROOT / "bench" / "HexRoots" / "Bench.lean").read_text() + for lit in ("6364136223846793005", "1442695040888963407"): + if lit not in src: + raise SystemExit( + f"hexroots_flint_compare: LCG literal {lit} not found in " + "bench/HexRoots/Bench.lean; the Lean seeded family has " + "changed and this script must be updated to match" + ) + + +def lcg_next(s: int) -> int: + """The LCG step from conformance/HexRoots/EmitFixtures.lean, UInt64 wraparound.""" + return (6364136223846793005 * s + 1442695040888963407) & MASK64 + + +def seeded_coeffs(degree: int) -> list[int]: + """Replicates `Hex.RootsBench.seededCoeffs`: degree+1 coefficients in + [-10, 10] (constant term first), leading coefficient forced nonzero.""" + s = 0xC0FFEE + out: list[int] = [] + for _ in range(degree + 1): + s = lcg_next(s) + out.append((s % 21) - 10) + if out[degree] == 0: + out[degree] = 1 + return out + + +def time_call(poly, repeats: int) -> float: + """Median wall time (seconds) of `poly.complex_roots()` over `repeats`.""" + ts = [] + for _ in range(repeats): + t0 = time.perf_counter() + poly.complex_roots() + ts.append(time.perf_counter() - t0) + return statistics.median(ts) + + +def main() -> int: + verify_lcg_matches_lean() + import flint + from flint import ctx, fmpz_poly + + prec_bits = 32 # match hex isolateAll?@32 (half-width 2^-32) + ctx.prec = prec_bits + + ladder = [int(a) for a in sys.argv[1:]] or [4, 6, 8, 10, 12, 14, 16, 18, 20] + + # Per-call floor: a trivial sub-millisecond input (x^2 - 2). + trivial = fmpz_poly([-2, 0, 1]) + trivial.complex_roots() # warm + overhead_s = time_call(trivial, 200) + + rows = [] + for d in ladder: + coeffs = seeded_coeffs(d) + p = fmpz_poly(coeffs) + p.complex_roots() # warm + # Fewer repeats at high degree to keep total time bounded. + repeats = 50 if d <= 12 else (20 if d <= 16 else 8) + med = time_call(p, repeats) + nroots = sum(m for _, m in p.complex_roots()) + rows.append({ + "degree": d, + "median_s": med, + "n_roots": nroots, + "repeats": repeats, + "coeffs_head": coeffs[:5], + }) + + print(json.dumps({ + "comparator": "python-flint fmpz_poly.complex_roots", + "python_flint_version": flint.__version__, + "prec_bits": prec_bits, + "overhead_s": overhead_s, + "rows": rows, + }, indent=2)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/check_phase4.py b/scripts/check_phase4.py index f6a218ed0..86e482961 100644 --- a/scripts/check_phase4.py +++ b/scripts/check_phase4.py @@ -133,7 +133,14 @@ def changed_setup_lines(root: Path, base: str) -> list[tuple[Path, int, str]]: if SETUP_RE.match(text): changed.append((current_file, new_line, text)) new_line += 1 - elif line.startswith("-") and not line.startswith("---"): + elif line.startswith("-"): + # A deleted line: never advances the new-file cursor. The guard is + # unconditional on `-` because a deleted `--`-comment line renders as + # `--- …` in the diff and must not be mistaken for the `--- a/` + # header (that header precedes `+++ b/`, so it is already + # skipped by the `current_file is None` check and reset at the next + # `@@`). Counting a deleted `--` comment as context inflated the + # new-file line number of the following `setup_benchmark`. continue else: new_line += 1 diff --git a/scripts/plots/hex-roots-comparator.py b/scripts/plots/hex-roots-comparator.py new file mode 100644 index 000000000..9edf6ec0e --- /dev/null +++ b/scripts/plots/hex-roots-comparator.py @@ -0,0 +1,80 @@ +#!/usr/bin/env python3 +"""Generate the HexRoots comparator-runtime plot from committed exports. + +Draws the Lean `isolateAll?@32` wall-time curve (from the lean-bench export) +alongside the python-flint `fmpz_poly.complex_roots` curve (from the flint +comparator export) for one `phase4.input_families` entry, log-y wall time per +call across the shared seeded degree ladder. Reads the same JSONL/JSON the +Comparator-ratios numbers in reports/hexroots-performance.md cite. + +Only the `seeded-dense` family has python-flint data (the process-call +comparator was run on the whole-polynomial driver ladder); MPSolve is +scheduled-only (no data points), and the `wilkinson-linprod` / `refine-fixed` +families carry no external-comparator series, so `--family` accepts only +`seeded-dense`. + +Usage: + python3 scripts/plots/hex-roots-comparator.py --family seeded-dense +""" +from __future__ import annotations + +import argparse +import json +from pathlib import Path + +import matplotlib + +matplotlib.use("Agg") +matplotlib.rcParams["svg.hashsalt"] = "hex-roots-comparator" +import matplotlib.pyplot as plt + +ROOT = Path(__file__).resolve().parents[2] +LEAN_EXPORT = ROOT / "reports/bench-results/hex-roots-b08a66cce522.json" +FLINT_EXPORT = ROOT / "reports/bench-results/hex-roots-flint-b08a66cce522.json" + + +def lean_isolateall_by_degree() -> dict[int, float]: + d = json.loads(LEAN_EXPORT.read_text()) + out: dict[int, float] = {} + for r in d["results"]: + if r["function"].endswith("runIsolateAll"): + for t in r["trial_summaries"]: + out[t["param"]] = t["median_per_call_nanos"] / 1e9 + return out + + +def flint_by_degree() -> tuple[dict[int, float], float]: + f = json.loads(FLINT_EXPORT.read_text()) + return {row["degree"]: row["median_s"] for row in f["rows"]}, f["overhead_s"] + + +def main() -> int: + ap = argparse.ArgumentParser() + ap.add_argument("--family", default="seeded-dense", choices=["seeded-dense"]) + ap.add_argument("--out", default=None) + args = ap.parse_args() + + hexd = lean_isolateall_by_degree() + flintd, overhead = flint_by_degree() + degrees = sorted(set(hexd) & set(flintd)) + + fig, ax = plt.subplots(figsize=(7, 4.5)) + ax.plot(degrees, [hexd[d] for d in degrees], "o-", label="hex isolateAll?@32 (Lean, certified)") + ax.plot(degrees, [max(flintd[d] - overhead, 1e-9) for d in degrees], "s-", + label="python-flint complex_roots (overhead-adjusted)") + ax.set_yscale("log") + ax.set_xlabel("degree n (seed-0xC0FFEE dense integer polynomial)") + ax.set_ylabel("wall time per call (s)") + ax.set_title("HexRoots vs python-flint — seeded-dense family (chungus2)") + ax.legend() + ax.grid(True, which="both", alpha=0.3) + out = Path(args.out) if args.out else ROOT / f"reports/figures/hex-roots-comparator-{args.family}.svg" + out.parent.mkdir(parents=True, exist_ok=True) + fig.tight_layout() + fig.savefig(out) + print(f"wrote {out}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())