Commit 2b27eaf
bench(hex-gfq): satisfy ordered constructor benchmark modes (#9859)
* bench(hex-gfq): promote constructor verdicts to mode 1
Cost model: fixed-modulus dense long division is linear in representative length; packed single-word reduction is constant, and the shared family is linear because the generic scan dominates.
* perf(hex-gfq): certify ordered benchmark modes
* bench(HexGFq): repair ordered verdict modes
Cost model: generic fixed-modulus dense reductions are linear in representative length. Packed GF2q 1 has at most n single-word leading-term eliminations and is therefore a mode-2 linear upper bound; packed GF2q 8 uses a fixed maximal-degree dense word after its honest linear ladder failed both mode 1 and mode 2.
* bench(HexGFq): retain final scientific evidence
Cost model: the temporary packed degree-eight audit varies exact input degree across the complete UInt64 range against the independently derived linear reduction bound.
* bench(HexGFq): select fixed packed degree-eight verdict
Cost model: the clean exact-degree audit is inconclusive with positive residual slope against n, so it fails both the two-sided mode-1 claim and the linear mode-2 upper-bound verdict; retain the maximal-degree fixed target and its 100 microsecond budget.
* docs(HexGFq): refresh ordered-mode evidence
* bench(HexGFq): model packed eliminations directly
Cost model: degree-one reduction performs exactly (n + 1) / 2 nonzero quotient eliminations for the dense input. Degree-eight inputs are prepared as the modulus times a dense quotient and perform exactly n - 7 eliminations. Both models add fixed packaging and projection stages. Generic fixtures are now prefix-nested across parameters.
* docs(HexGFq): record exact mode-one evidence
Replace the superseded packed fixed-budget and one-sided artifacts with the clean all-mode-one scientific export. Refresh profiler attribution from six clean profiles, including direct degree-eight packed and generic measurements.
* bench(HexGFq): make packed verdict observable
Cost model: adding a degree-below-eight remainder leaves the dense quotient and exact n - 7 elimination count unchanged while producing parameter-varying results. Remove a duplicate packed rung and start generic ladders where their linear fixed-width elimination model applies.
* docs(HexGFq): refresh observable mode-one evidence
Record the clean post-review scientific export and six profiles. Document registered and fitted ranges, parameter-varying packed degree-eight hashes, exact profile locations, and host OS traceability.
* bench(HexGFq): stabilize shared verdict ladder
Cost model: the packed half saturates at degree 63, so register the shared family where its fixed work is dominated by the generic degree-n scan. Diversify the degree-eight low residues while preserving its exact dense quotient and elimination count.
* docs(HexGFq): record stable post-review evidence
Refresh the clean scientific artifact and six profiles after stabilizing the shared ladder. Scope completeness to issue #9814 constructor/projection work, record the warmup fraction and spawn-floor conditions, and reflect HexConway's Phase-7 promotion.
* docs(HexGFq): state signal-floor evidence precisely
Report the harness flag recorded by the artifact without claiming every raw timed batch exceeds the separately measured spawn floor.
---------
Co-authored-by: Kim Morrison <kim@lean-fro.org>1 parent d3d4927 commit 2b27eaf
4 files changed
Lines changed: 2767 additions & 285 deletions
File tree
- bench/HexGFq
- reports
- bench-results
0 commit comments