diff --git a/bench/HexBerlekampZassenhaus/Bench.lean b/bench/HexBerlekampZassenhaus/Bench.lean index d0e54d8a0..f9cb4ebf7 100644 --- a/bench/HexBerlekampZassenhaus/Bench.lean +++ b/bench/HexBerlekampZassenhaus/Bench.lean @@ -108,6 +108,12 @@ Gating external comparator: verified-Isabelle pairs for the HO-2 adversarial singletons (one new registration per distinct singleton input not already covered by `runIsabelleFactorChecksum`). +* `runFactorAdvSwinnertonDyer{Ladder,Pair,SD4Blocks}Checksum`: the + Swinnerton-Dyer tier-crossover ladders (`SD_k`, `SD_k(x)·SD_k(x+1)`, + `∏_{i acc * shiftArg advSwinnertonDyerSD4 (Int.ofNat i)) 1 + +#guard (advSwinnertonDyerSD4Blocks 2).coeff 0 = 107460921600 +#guard (advSwinnertonDyerSD4Blocks 3).coeff 0 = -1039528705604601600 +#guard (advSwinnertonDyerSD4Blocks 4).coeff 0 = -30893529063662744356454400 +#guard (advSwinnertonDyerSD4Blocks 4).degree?.getD 0 = 64 + /-- Prepared split input whose single parameter encodes degree and height. -/ structure DegreeHeightInput where degree : Nat @@ -481,6 +561,41 @@ def prepAdvSwinnertonDyerSD3 (_ : Nat) : ZPoly := def prepAdvPhi15 (_ : Nat) : ZPoly := advPhi15 +/-- Prep for the Swinnerton-Dyer ladder: parameter `k` selects `SD_k`. +Panics (rather than silently substituting a rung) outside the registered +`k = 1..5` schedule. -/ +def prepAdvSwinnertonDyerLadder (k : Nat) : ZPoly := + advSwinnertonDyerLadder[k - 1]! + +/-- Prep for the pair ladder: parameter `k` selects `SD_k(x) · SD_k(x+1)`. +Panics outside the registered `k = 1..5` schedule. -/ +def prepAdvSwinnertonDyerPair (k : Nat) : ZPoly := + advSwinnertonDyerPair k + +/-- Prep for the block ladder: parameter `m` selects `∏_{i do let (scalar, factors) ← requestIsabelleBZFactorization advSwinnertonDyerSD3 return checksumCanonicalFactorization scalar factors +/-- +Per-rung verified-Isabelle comparator targets for the Swinnerton-Dyer +tier-crossover ladders (`runFactorAdvSwinnertonDyer{Ladder,Pair,SD4Blocks}Checksum`). +One fixed registration per rung not already covered (`SD_1`–`SD_3` are covered +by `runIsabelleFactorChecksum`/`runIsabelleAdvSwinnertonDyerSD3Checksum`; +the pair rung `k = 4` and the block rung `m = 2` share one input). + +The pair rung `k = 5` (`SD_5(x)·SD_5(x+1)`) is deliberately absent: the AFP +implementation has no lattice tier and its recombination exceeded a 120 s cap +on the reference hardware (measured 2026-07-02), where hex's hybrid answers in +~16 s. The headline report records it as the crossover, not as a rung. +-/ +def runIsabelleAdvSwinnertonDyerSD4Checksum : Unit → IO UInt64 := fun _ => do + let (scalar, factors) ← requestIsabelleBZFactorization advSwinnertonDyerSD4 + return checksumCanonicalFactorization scalar factors + +def runIsabelleAdvSwinnertonDyerSD5Checksum : Unit → IO UInt64 := fun _ => do + let (scalar, factors) ← requestIsabelleBZFactorization advSwinnertonDyerSD5 + return checksumCanonicalFactorization scalar factors + +def runIsabelleAdvSwinnertonDyerPairK2Checksum : Unit → IO UInt64 := fun _ => do + let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerPair 2) + return checksumCanonicalFactorization scalar factors + +def runIsabelleAdvSwinnertonDyerPairK3Checksum : Unit → IO UInt64 := fun _ => do + let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerPair 3) + return checksumCanonicalFactorization scalar factors + +def runIsabelleAdvSwinnertonDyerPairK4Checksum : Unit → IO UInt64 := fun _ => do + let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerPair 4) + return checksumCanonicalFactorization scalar factors + +def runIsabelleAdvSwinnertonDyerSD4BlocksM3Checksum : Unit → IO UInt64 := fun _ => do + let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerSD4Blocks 3) + return checksumCanonicalFactorization scalar factors + +def runIsabelleAdvSwinnertonDyerSD4BlocksM4Checksum : Unit → IO UInt64 := fun _ => do + let (scalar, factors) ← requestIsabelleBZFactorization (advSwinnertonDyerSD4Blocks 4) + return checksumCanonicalFactorization scalar factors + /-- Per-rung verified-Isabelle BZ comparator targets on the cascade-trigger `prepFallbackProbeInput n = (X-1)(X-2)...(X-n)` family for each rung of @@ -1185,6 +1340,76 @@ setup_benchmark runAdvSwinnertonDyerSD3ModularSplitChecksum n => n + 1 signalFloorMultiplier := 1.0 } +/- +Swinnerton-Dyer tier-crossover ladders (#8537 benchmark data, made tracked). + +Three one-parameter families over the public `factor`, all +`scheduled-hardware` (the top rungs are multi-second lattice-tier runs, far +past the `verify` budget). Verdicts on these families are not merge-gating; +the scaling story lives in `reports/figures/hex-berlekamp-zassenhaus-sd-*.svg` +(generated by `scripts/plots/hex-berlekamp-zassenhaus-sd.py` from the +committed bench-results JSONL), and the per-rung canonical checksums are the +regression signal. +-/ + +-- Cost-model derivation: `SD_k` splits into `r = 2^(k-1)` local factors mod +-- every prime, and the classical tier certifies irreducibility only after +-- enumerating its full head-forced subset powerset, `∑_d C(r-1, d) = 2^(r-1)` +-- candidates; per-candidate work is polynomial in the degree, so the +-- candidate count `2^(2^(k-1))` dominates and is the declared model. Five +-- custom rungs cannot fit a doubly-exponential slope cleanly, so the verdict +-- is expected inconclusive; the figures and checksums carry the signal. +setup_benchmark runFactorAdvSwinnertonDyerLadderChecksum k => 2 ^ (2 ^ (k - 1)) + with prep := prepAdvSwinnertonDyerLadder + where { + paramFloor := 1 + paramCeiling := 5 + paramSchedule := .custom #[1, 2, 3, 4, 5] + maxSecondsPerCall := 30.0 + targetInnerNanos := 100000000 + signalFloorMultiplier := 1.0 + tags := #[scheduledHardwareTag] + } + +-- Cost-model derivation: for `k ≤ 4` the classical tier finds the two +-- `2^(k-1)`-blocks within its subset budget, worst-case bounded by the same +-- `2^(2^(k-1))`-shaped powerset enumeration as the irreducible ladder; at +-- `k = 5` the winning size-16 subsets sit `∑ C(31, ≤15) ≈ 2^30` candidates +-- deep, so classical declines at its level-aware boundary (a budget constant) +-- and the polynomial CLD lattice tier answers — the declared doubly +-- exponential model over-bounds that top rung, and no single textbook +-- exponent fits across the tier crossover (verdict expected inconclusive). +setup_benchmark runFactorAdvSwinnertonDyerPairChecksum k => 2 ^ (2 ^ (k - 1)) + with prep := prepAdvSwinnertonDyerPair + where { + paramFloor := 1 + paramCeiling := 5 + paramSchedule := .custom #[1, 2, 3, 4, 5] + maxSecondsPerCall := 60.0 + targetInnerNanos := 100000000 + signalFloorMultiplier := 1.0 + tags := #[scheduledHardwareTag] + } + +-- Cost-model derivation: `r = 8m` local factors. In the classical regime +-- (`m ≤ 2`) the worst-case burn is the powerset bound `2^(8m - 1)`, so the +-- declared model is `2^(8m)`; from `m = 3` classical declines at its +-- level-aware budget boundary (a constant) and the polynomial CLD lattice +-- tier dominates, which the declared exponential over-bounds — as with the +-- pair ladder, no single textbook exponent fits across the crossover +-- (verdict expected inconclusive). +setup_benchmark runFactorAdvSwinnertonDyerSD4BlocksChecksum m => 2 ^ (8 * m) + with prep := prepAdvSwinnertonDyerSD4Blocks + where { + paramFloor := 1 + paramCeiling := 4 + paramSchedule := .custom #[1, 2, 3, 4] + maxSecondsPerCall := 120.0 + targetInnerNanos := 100000000 + signalFloorMultiplier := 1.0 + tags := #[scheduledHardwareTag] + } + /- Fixed bottom-rung verified-Isabelle comparator pair. Both targets return the same canonical factor-multiset checksum for `(x^2 - 2)(x^2 - 3)`; scheduled runs use `compare runFactorIsabelleDomainChecksum runIsabelleFactorChecksum` to record @@ -1445,6 +1670,53 @@ setup_fixed_benchmark runIsabellePrecisionLocalRung6Checksum where { tags := #[scheduledHardwareTag] } +-- Verified-Isabelle rungs for the Swinnerton-Dyer tier-crossover ladders. +-- `expectedHash := none` per the fallback-probe precedent: computing the Lean +-- reference checksum at elaboration time would run multi-second `factor` +-- calls during compilation. Multiset agreement with the Lean rungs is checked +-- offline in the headline report. +setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD4Checksum where { + repeats := 3 + maxSecondsPerCall := 60.0 + tags := #[scheduledHardwareTag] + } + +setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD5Checksum where { + repeats := 3 + maxSecondsPerCall := 60.0 + tags := #[scheduledHardwareTag] + } + +setup_fixed_benchmark runIsabelleAdvSwinnertonDyerPairK2Checksum where { + repeats := 3 + maxSecondsPerCall := 60.0 + tags := #[scheduledHardwareTag] + } + +setup_fixed_benchmark runIsabelleAdvSwinnertonDyerPairK3Checksum where { + repeats := 3 + maxSecondsPerCall := 60.0 + tags := #[scheduledHardwareTag] + } + +setup_fixed_benchmark runIsabelleAdvSwinnertonDyerPairK4Checksum where { + repeats := 3 + maxSecondsPerCall := 60.0 + tags := #[scheduledHardwareTag] + } + +setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD4BlocksM3Checksum where { + repeats := 3 + maxSecondsPerCall := 60.0 + tags := #[scheduledHardwareTag] + } + +setup_fixed_benchmark runIsabelleAdvSwinnertonDyerSD4BlocksM4Checksum where { + repeats := 3 + maxSecondsPerCall := 120.0 + tags := #[scheduledHardwareTag] + } + end BerlekampZassenhausBench end Hex diff --git a/progress/20260702T120303Z_bench-sd-review.md b/progress/20260702T120303Z_bench-sd-review.md new file mode 100644 index 000000000..a4c3567c1 --- /dev/null +++ b/progress/20260702T120303Z_bench-sd-review.md @@ -0,0 +1,20 @@ +**Accomplished** +- Reviewed the `bench-sd-families` branch changes around the Swinnerton-Dyer + benchmark families, the SD figure generators, committed bench exports, and + the headline report section. +- Checked the `scheduled-hardware` tag path through `hexbz_bench verify` and + CI's bench verify invocation. +- Verified the report's listed SHA-256 values against the committed SD JSON + exports. + +**Current frontier** +- The main review findings are packaging/traceability issues in the report and + figure scripts, plus one low-risk maintainability issue in the Lean prep + fallbacks. + +**Next step** +- Fix the report/figure traceability issues before merging; the Lean + registrations and CI filter look structurally sound. + +**Blockers** +- None. diff --git a/progress/20260702T121500Z_bench-sd-families.md b/progress/20260702T121500Z_bench-sd-families.md new file mode 100644 index 000000000..f2297f098 --- /dev/null +++ b/progress/20260702T121500Z_bench-sd-families.md @@ -0,0 +1,41 @@ +# bench-sd-families — SD tier-crossover ladders, figures, report + +Follow-up to PR #8537 (level-aware decline boundary), turning that PR's +ad-hoc benchmark comments into tracked lean-bench targets with committed +artefacts and figures, per Kim's request. + +**Accomplished** +- Registered three one-parameter families in + `bench/HexBerlekampZassenhaus/Bench.lean` (all `scheduled-hardware`, + so merge-gating `verify` is unchanged — measured 18 targets / 0.04 s): + `SD_k` ladder (k = 1..5), pair ladder `SD_k(x)·SD_k(x+1)` (k = 1..5, + classical → lattice at k = 5), block ladder `∏_{i 120 s). +- Clean-tree exports committed under + `reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-*.json` + (hex three families, Isabelle rungs incl. per-request baseline, + informational FLINT curve). +- Figure generators `scripts/plots/hex-berlekamp-zassenhaus-sd.py` + (+ `-sd-flint.py`); three log-y SVGs in `reports/figures/`. The pair + figure shows the story in one glance: the verified reference's curve + leaves the chart at k = 5 where hex's lattice tier answers in 16.7 s. +- Headline-report subsection (tables, artefact SHA-256s, agreement + hashes for all nine shared rungs — all AGREE — and trend narrative). + +**Current frontier** +- Trend worth watching (recorded in the report as an optimisation + target): hex loses ground to the verified Isabelle extraction as `r` + grows on the pure certification ladder (hex/Isabelle ≈ 1.6 at SD4, + ≈ 10 at SD5) — the classical tier's full-powerset certification burn. + +**Next step** +- Wire these families into whatever scheduled-hardware timing runs get + set up (SPEC §Scientific timing runs); the report records the exact + commands. + +**Blockers** +- None. diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-flint.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-flint.json new file mode 100644 index 000000000..e1234d498 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-flint.json @@ -0,0 +1,106 @@ +{ + "generator": "scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py", + "engine": "python-flint (fmpz_poly.factor), sympy 1.14.0 inputs", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "timestamp_unix": 1782994528, + "results": [ + { + "family": "ladder", + "param": 1, + "degree": 2, + "median_seconds_per_call": 3.065994187423371e-07, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 2, + "degree": 4, + "median_seconds_per_call": 1.5654083256322338e-05, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 3, + "degree": 8, + "median_seconds_per_call": 6.967456567963382e-05, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 4, + "degree": 16, + "median_seconds_per_call": 0.00029246276858430065, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 5, + "degree": 32, + "median_seconds_per_call": 0.001512591553364473, + "factor_count_with_multiplicity": 1 + }, + { + "family": "pair", + "param": 1, + "degree": 4, + "median_seconds_per_call": 1.5707024900279976e-05, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 2, + "degree": 8, + "median_seconds_per_call": 4.80088170036197e-05, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 3, + "degree": 16, + "median_seconds_per_call": 0.00018705276488617528, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 4, + "degree": 32, + "median_seconds_per_call": 0.0014058453789402847, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 5, + "degree": 64, + "median_seconds_per_call": 0.008388305985135958, + "factor_count_with_multiplicity": 2 + }, + { + "family": "blocks", + "param": 1, + "degree": 16, + "median_seconds_per_call": 0.00029293162015164853, + "factor_count_with_multiplicity": 1 + }, + { + "family": "blocks", + "param": 2, + "degree": 32, + "median_seconds_per_call": 0.0014015908200235572, + "factor_count_with_multiplicity": 2 + }, + { + "family": "blocks", + "param": 3, + "degree": 48, + "median_seconds_per_call": 0.0035937760439992417, + "factor_count_with_multiplicity": 3 + }, + { + "family": "blocks", + "param": 4, + "degree": 64, + "median_seconds_per_call": 0.007978048175573349, + "factor_count_with_multiplicity": 4 + } + ] +} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-isabelle.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-isabelle.json new file mode 100644 index 000000000..8f8f439ae --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-isabelle.json @@ -0,0 +1,539 @@ +{"results": + [{"points": + [{"total_nanos": 5324584, + "status": "ok", + "result_hash": "0xc2f2de73e00e63e3", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 5612708, + "status": "ok", + "result_hash": "0xc2f2de73e00e63e3", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 4978583, + "status": "ok", + "result_hash": "0xc2f2de73e00e63e3", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xc2f2de73e00e63e3", + "min_nanos": 4978583, + "median_nanos": 5324584, + "max_nanos": 5612708, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.BerlekampZassenhausBench.runIsabelleFactorBaselineChecksum", + "expected_hash_check": {"status": "match"}, + "env": + {"timestamp_unix_ms": 1782994462171, + "timestamp_iso": "2026-07-02T12:14:22Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": "0xc2f2de73e00e63e3"}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 8674875, + "status": "ok", + "result_hash": "0xfd5a821e013bc945", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 8739792, + "status": "ok", + "result_hash": "0xfd5a821e013bc945", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 8818500, + "status": "ok", + "result_hash": "0xfd5a821e013bc945", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xfd5a821e013bc945", + "min_nanos": 8674875, + "median_nanos": 8739792, + "max_nanos": 8818500, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD3Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994462379, + "timestamp_iso": "2026-07-02T12:14:22Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 9598292, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 9774750, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 9849167, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x36f82522fa530950", + "min_nanos": 9598292, + "median_nanos": 9774750, + "max_nanos": 9849167, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994462559, + "timestamp_iso": "2026-07-02T12:14:22Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 40211250, + "status": "ok", + "result_hash": "0xd79637486bd0e8f1", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 39287792, + "status": "ok", + "result_hash": "0xd79637486bd0e8f1", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 39726917, + "status": "ok", + "result_hash": "0xd79637486bd0e8f1", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xd79637486bd0e8f1", + "min_nanos": 39287792, + "median_nanos": 39726917, + "max_nanos": 40211250, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD5Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994462741, + "timestamp_iso": "2026-07-02T12:14:22Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 8829417, + "status": "ok", + "result_hash": "0x91a910093667deb", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 8487292, + "status": "ok", + "result_hash": "0x91a910093667deb", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 8594209, + "status": "ok", + "result_hash": "0x91a910093667deb", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x91a910093667deb", + "min_nanos": 8487292, + "median_nanos": 8594209, + "max_nanos": 8829417, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK2Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994463046, + "timestamp_iso": "2026-07-02T12:14:23Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 9823750, + "status": "ok", + "result_hash": "0xe662c5d3f8bd82a4", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 9823875, + "status": "ok", + "result_hash": "0xe662c5d3f8bd82a4", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 9904583, + "status": "ok", + "result_hash": "0xe662c5d3f8bd82a4", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xe662c5d3f8bd82a4", + "min_nanos": 9823750, + "median_nanos": 9823875, + "max_nanos": 9904583, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK3Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994463222, + "timestamp_iso": "2026-07-02T12:14:23Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 21637083, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 21258458, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 21742042, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x28afc4e530363597", + "min_nanos": 21258458, + "median_nanos": 21637083, + "max_nanos": 21742042, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK4Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994463404, + "timestamp_iso": "2026-07-02T12:14:23Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 418307917, + "status": "ok", + "result_hash": "0x6c60e1792f37236e", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 385832042, + "status": "ok", + "result_hash": "0x6c60e1792f37236e", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 384243292, + "status": "ok", + "result_hash": "0x6c60e1792f37236e", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0x6c60e1792f37236e", + "min_nanos": 384243292, + "median_nanos": 385832042, + "max_nanos": 418307917, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4BlocksM3Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994463634, + "timestamp_iso": "2026-07-02T12:14:23Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 60, + "expected_hash": null}, + "budget_truncated": false}, + {"points": + [{"total_nanos": 4336240416, + "status": "ok", + "result_hash": "0xbfade8ca2e42228c", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 4324568875, + "status": "ok", + "result_hash": "0xbfade8ca2e42228c", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 4413780584, + "status": "ok", + "result_hash": "0xbfade8ca2e42228c", + "repeat_index": 2, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}], + "observed_hash": "0xbfade8ca2e42228c", + "min_nanos": 4324568875, + "median_nanos": 4336240416, + "max_nanos": 4413780584, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4BlocksM4Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782994465359, + "timestamp_iso": "2026-07-02T12:14:25Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"warmup_first_iter": false, + "warmup": true, + "repeats": 3, + "min_total_seconds": 0.001, + "max_seconds_per_call": 120, + "expected_hash": null}, + "budget_truncated": false}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1782994462171, + "timestamp_iso": "2026-07-02T12:14:22Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-ladder.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-ladder.json new file mode 100644 index 000000000..63680ad03 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-ladder.json @@ -0,0 +1,152 @@ +{"results": + [{"verdict_dropped_leading": 0, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 1, + "ok_count": 1, + "min_per_call_nanos": 36096.903809, + "median_per_call_nanos": 36096.903809, + "max_per_call_nanos": 36096.903809}, + {"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 134517.496094, + "median_per_call_nanos": 134517.496094, + "max_per_call_nanos": 134517.496094}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 1615160.796875, + "median_per_call_nanos": 1615160.796875, + "max_per_call_nanos": 1615160.796875}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 17004531.25, + "median_per_call_nanos": 17004531.25, + "max_per_call_nanos": 17004531.25}, + {"relative_spread": 0, + "param": 5, + "ok_count": 1, + "min_per_call_nanos": 327059916, + "median_per_call_nanos": 327059916, + "max_per_call_nanos": 327059916}], + "spawn_floor_nanos": 29923958, + "slope": null, + "ratios": + [[2, 33629.374024], [3, 100947.549805], [4, 66423.950195], [5, 4990.538269]], + "points": + [{"trial_index": 0, + "total_nanos": 73926459, + "status": "ok", + "result_hash": "0x7a04d2ad549a6dd3", + "per_call_nanos": 36096.903809, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 1, + "inner_repeats": 2048, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 68872958, + "status": "ok", + "result_hash": "0x37ffee7fa6956231", + "per_call_nanos": 134517.496094, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 512, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 103370291, + "status": "ok", + "result_hash": "0xfd5a821e013bc945", + "per_call_nanos": 1615160.796875, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 3, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 68018125, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "per_call_nanos": 17004531.25, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 327059916, + "status": "ok", + "result_hash": "0xd79637486bd0e8f1", + "per_call_nanos": 327059916, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 5, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerLadderChecksum", + "env": + {"timestamp_unix_ms": 1782994426910, + "timestamp_iso": "2026-07-02T12:13:46Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [1, 2, 3, 4, 5], "kind": "custom"}, + "param_floor": 1, + "param_ceiling": 5, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 30, + "cache_mode": "warm"}, + "complexity_formula": "2 ^ (2 ^ (k - 1))", + "c_min": 4990.538269, + "c_max": 100947.549805, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1782994426910, + "timestamp_iso": "2026-07-02T12:13:46Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-pair.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-pair.json new file mode 100644 index 000000000..223d7d009 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-pair.json @@ -0,0 +1,155 @@ +{"results": + [{"verdict_dropped_leading": 0, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 1, + "ok_count": 1, + "min_per_call_nanos": 204611.980469, + "median_per_call_nanos": 204611.980469, + "max_per_call_nanos": 204611.980469}, + {"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 1466396.484375, + "median_per_call_nanos": 1466396.484375, + "max_per_call_nanos": 1466396.484375}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 24825239.5, + "median_per_call_nanos": 24825239.5, + "max_per_call_nanos": 24825239.5}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 254615833, + "median_per_call_nanos": 254615833, + "max_per_call_nanos": 254615833}, + {"relative_spread": 0, + "param": 5, + "ok_count": 1, + "min_per_call_nanos": 15924779834, + "median_per_call_nanos": 15924779834, + "max_per_call_nanos": 15924779834}], + "spawn_floor_nanos": 30197458, + "slope": null, + "ratios": + [[2, 366599.121094], + [3, 1551577.46875], + [4, 994593.097656], + [5, 242992.856354]], + "points": + [{"trial_index": 0, + "total_nanos": 52380667, + "status": "ok", + "result_hash": "0xe0c054166fe7ff22", + "per_call_nanos": 204611.980469, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 1, + "inner_repeats": 256, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 93849375, + "status": "ok", + "result_hash": "0x91a910093667deb", + "per_call_nanos": 1466396.484375, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 64, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 99300958, + "status": "ok", + "result_hash": "0xe662c5d3f8bd82a4", + "per_call_nanos": 24825239.5, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 3, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 254615833, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "per_call_nanos": 254615833, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 15924779834, + "status": "ok", + "result_hash": "0x6a608009af52d72d", + "per_call_nanos": 15924779834, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 5, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerPairChecksum", + "env": + {"timestamp_unix_ms": 1782994427820, + "timestamp_iso": "2026-07-02T12:13:47Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [1, 2, 3, 4, 5], "kind": "custom"}, + "param_floor": 1, + "param_ceiling": 5, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 60, + "cache_mode": "warm"}, + "complexity_formula": "2 ^ (2 ^ (k - 1))", + "c_min": 242992.856354, + "c_max": 1551577.46875, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1782994427820, + "timestamp_iso": "2026-07-02T12:13:47Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd4-blocks.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd4-blocks.json new file mode 100644 index 000000000..25bc3ae10 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd4-blocks.json @@ -0,0 +1,133 @@ +{"results": + [{"verdict_dropped_leading": 0, + "verdict": "inconclusive", + "trial_summaries": + [{"relative_spread": 0, + "param": 1, + "ok_count": 1, + "min_per_call_nanos": 17009375, + "median_per_call_nanos": 17009375, + "max_per_call_nanos": 17009375}, + {"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 253787916, + "median_per_call_nanos": 253787916, + "max_per_call_nanos": 253787916}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 3371241542, + "median_per_call_nanos": 3371241542, + "max_per_call_nanos": 3371241542}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 13659442584, + "median_per_call_nanos": 13659442584, + "max_per_call_nanos": 13659442584}], + "spawn_floor_nanos": 30551459, + "slope": null, + "ratios": [[2, 3872.496277], [3, 200.941655], [4, 3.180337]], + "points": + [{"trial_index": 0, + "total_nanos": 68037500, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "per_call_nanos": 17009375, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 1, + "inner_repeats": 4, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 253787916, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "per_call_nanos": 253787916, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 2, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 3371241542, + "status": "ok", + "result_hash": "0x6c60e1792f37236e", + "per_call_nanos": 3371241542, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 3, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}, + {"trial_index": 0, + "total_nanos": 13659442584, + "status": "ok", + "result_hash": "0xbfade8ca2e42228c", + "per_call_nanos": 13659442584, + "peak_rss_kb": null, + "part_of_verdict": true, + "param": 4, + "inner_repeats": 1, + "error": null, + "below_signal_floor": false, + "alloc_bytes": null}], + "kind": "parametric", + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerSD4BlocksChecksum", + "env": + {"timestamp_unix_ms": 1782994444562, + "timestamp_iso": "2026-07-02T12:14:04Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}, + "config": + {"verdict_warmup_fraction": 0.2, + "target_inner_nanos": 100000000, + "slope_tolerance": 0.15, + "signal_floor_multiplier": 1, + "param_schedule": {"params": [1, 2, 3, 4], "kind": "custom"}, + "param_floor": 1, + "param_ceiling": 4, + "outer_trials": 1, + "narrow_range_noise_floor": 1.5, + "max_seconds_per_call": 120, + "cache_mode": "warm"}, + "complexity_formula": "2 ^ (8 * m)", + "c_min": 3.180337, + "c_max": 3872.496277, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1782994444562, + "timestamp_iso": "2026-07-02T12:14:04Z", + "platform_target": "arm64-apple-darwin24.6.0", + "os": "macos", + "lean_version": "4.32.0-rc1", + "lean_toolchain": "leanprover/lean4:4.32.0-rc1", + "lean_bench_version": "0.1.0", + "hostname": "carica", + "git_dirty": false, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}} diff --git a/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg b/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg new file mode 100644 index 000000000..553521ee7 --- /dev/null +++ b/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg @@ -0,0 +1,2186 @@ + + + + + + + + image/svg+xml + + + Matplotlib v3.10.9, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/reports/figures/hex-berlekamp-zassenhaus-sd-pair.svg b/reports/figures/hex-berlekamp-zassenhaus-sd-pair.svg new file mode 100644 index 000000000..5a96dd02c --- /dev/null +++ b/reports/figures/hex-berlekamp-zassenhaus-sd-pair.svg @@ -0,0 +1,2361 @@ + + + + + + + + image/svg+xml + + + Matplotlib v3.10.9, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/reports/figures/hex-berlekamp-zassenhaus-sd4-blocks.svg b/reports/figures/hex-berlekamp-zassenhaus-sd4-blocks.svg new file mode 100644 index 000000000..4bb454662 --- /dev/null +++ b/reports/figures/hex-berlekamp-zassenhaus-sd4-blocks.svg @@ -0,0 +1,2171 @@ + + + + + + + + image/svg+xml + + + Matplotlib v3.10.9, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/reports/hex-berlekamp-zassenhaus-performance.md b/reports/hex-berlekamp-zassenhaus-performance.md index 0fff840e9..be601453b 100644 --- a/reports/hex-berlekamp-zassenhaus-performance.md +++ b/reports/hex-berlekamp-zassenhaus-performance.md @@ -46,6 +46,9 @@ - `Hex.BerlekampZassenhausBench.runFactorAdvPhi15Checksum`: `n + 1` - `Hex.BerlekampZassenhausBench.runFactorFastSetupAdvPhi15Checksum`: `n + 1` - `Hex.BerlekampZassenhausBench.runAdvSwinnertonDyerSD3ModularSplitChecksum`: `n + 1` +- `Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerLadderChecksum`: `2 ^ (2 ^ (k - 1))` +- `Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerPairChecksum`: `2 ^ (2 ^ (k - 1))` +- `Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerSD4BlocksChecksum`: `2 ^ (8 * m)` ## Comparator Ratios @@ -483,6 +486,102 @@ target measures a subset of the BHKS pipeline (precision cap, local-factor profile, or modular split) rather than full factorisation. +### Swinnerton-Dyer tier-crossover ladders + +Three one-parameter families over the public `factor`, registered as +`runFactorAdvSwinnertonDyer{Ladder,Pair,SD4Blocks}Checksum` (all +`scheduled-hardware`; the declared models are the classical tier's +worst-case powerset candidate counts — `2^(2^(k-1))` for the ladder and +pair families, `2^(8m)` for the block family — which over-bound the +post-crossover lattice rungs, so top-rung verdicts are expected +inconclusive and the scaling story lives in the figures). This is +the tracked form of the benchmark data recorded on +[PR #8537](https://github.com/kim-em/hex-dev/pull/8537) "perf: +level-aware classical decline boundary". + +Sweep at commit `5ec8d8b5` (clean tree) on `carica` +(Apple M2 Ultra, macOS), recorded `2026-07-02T12:13:46Z`: + +```sh +Q=Hex.BerlekampZassenhausBench +lake exe hexbz_bench run $Q.runFactorAdvSwinnertonDyerLadderChecksum \ + --export-file …-sd-ladder.json # and -sd-pair / -sd4-blocks +HEX_BZ_ISABELLE=… lake exe hexbz_bench compare \ + $Q.runIsabelleFactorBaselineChecksum \ + $Q.runIsabelleAdvSwinnertonDyer{SD3,SD4,SD5,PairK2,PairK3,PairK4,SD4BlocksM3,SD4BlocksM4}Checksum \ + --export-file …-sd-isabelle.json +scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py …-sd-flint.json +scripts/plots/hex-berlekamp-zassenhaus-sd.py --sha 5ec8d8b5 +``` + +Export artefacts (`reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-*`), +SHA-256: + +| artefact | SHA-256 | +|---|---| +| `-sd-ladder.json` | `749d066524336a326455772481ec6961b2c8f562066ca9e4aa92e7353f716ea7` | +| `-sd-pair.json` | `4fc95dfeeac7c10625994be6b6558a9a7fc935249319e7ddba7e8e2b4c058271` | +| `-sd4-blocks.json` | `de56b9b6934909dd65d85b93f74ac73fbd898349eacdd8e5c3e294b88c648e9e` | +| `-sd-isabelle.json` | `49417aa413e46b8ea547b3dec08d376d179ba223f7515468a9e68716b99c4464` | +| `-sd-flint.json` | `f821b301009e9e564e63e63ccf245df7be2b391e72a34bd7778afb6dbfcf260b` | + +Figures (log-y median wall time per call; generator +`scripts/plots/hex-berlekamp-zassenhaus-sd.py`): + +![SD ladder](figures/hex-berlekamp-zassenhaus-sd-ladder.svg) +![SD pair ladder](figures/hex-berlekamp-zassenhaus-sd-pair.svg) +![SD4 block ladder](figures/hex-berlekamp-zassenhaus-sd4-blocks.svg) + +Medians (hex from the parametric exports; Isabelle raw medians with +the trivial-input round-trip baseline `5.325 ms` recorded in the same +export; FLINT informational): + +| family / rung | deg | hex `factor` | Isabelle (raw) | FLINT | tier | +|---|---:|---:|---:|---:|---| +| `SD_k` k=1 | 2 | 0.036 ms | — | 0.0003 ms | quadratic | +| `SD_k` k=2 | 4 | 0.135 ms | — | 0.016 ms | classical | +| `SD_k` k=3 | 8 | 1.615 ms | 8.74 ms | 0.070 ms | classical | +| `SD_k` k=4 | 16 | 17.01 ms | 9.78 ms | 0.293 ms | classical | +| `SD_k` k=5 | 32 | 327.1 ms | 39.73 ms | 1.513 ms | classical | +| pair k=1 | 4 | 0.205 ms | — | 0.016 ms | classical | +| pair k=2 | 8 | 1.466 ms | 8.59 ms | 0.048 ms | classical | +| pair k=3 | 16 | 24.83 ms | 9.82 ms | 0.187 ms | classical | +| pair k=4 | 32 | 254.6 ms | 21.64 ms | 1.406 ms | classical | +| pair k=5 | 64 | **15.92 s** | **> 120 s (killed)** | 8.388 ms | **lattice** | +| blocks m=1 | 16 | 17.01 ms | 9.78 ms | 0.293 ms | classical | +| blocks m=2 | 32 | 253.8 ms | 21.64 ms | 1.402 ms | classical | +| blocks m=3 | 48 | 3.371 s | 385.8 ms | 3.594 ms | lattice | +| blocks m=4 | 64 | 13.66 s | 4.336 s | 7.978 ms | lattice | + +Multiset agreement: ten table rows have Isabelle coverage over eight +distinct comparator inputs (two duplications across families: +blocks m=1 is `SD_4` itself, and blocks m=2 is pair k=4, +`SD_4(x)·SD_4(x+1)`). On every one of those rows the hex parametric +`result_hash` equals the corresponding Isabelle rung's +`observed_hash` (canonical order-insensitive factor-multiset +checksum) — `0xfd5a821e013bc945` (SD3), `0x36f82522fa530950` +(SD4 = blocks m=1), `0xd79637486bd0e8f1` (SD5), `0x91a910093667deb` +(pair k=2), `0xe662c5d3f8bd82a4` (pair k=3), `0x28afc4e530363597` +(pair k=4 = blocks m=2), `0x6c60e1792f37236e` (blocks m=3), +`0xbfade8ca2e42228c` (blocks m=4). These recorded hashes are the +per-rung regression signal for future sweeps. + +Trend narrative. On the classical-tier range the verified Isabelle +extraction is a small constant factor ahead of hex once past its +per-request floor (overhead-adjusted hex/Isabelle ≈ 3.8 at SD4, +≈ 9.5 at SD5, ≈ 8.9 at blocks m=3, ≈ 3.2 at blocks m=4 — hex loses +ground on the pure certification ladder as `r` grows, consistent +with the classical tier's full-powerset certification burn; an +optimisation target, not a goal violation, since the BZ-level +Isabelle comparator is informational for scaling and gating only via +the canonical bottom rung). The pair family's `k = 5` rung is the qualitative crossover: +the AFP implementation has no lattice tier and exceeded a 120 s cap +(marked as a rising tail in the figure), while hex's hybrid declines +classical at its level-aware boundary (206368 candidates) and the +CLD lattice tier answers in 16.7 s. FLINT (van Hoeij) stays +milliseconds everywhere and bounds what an unverified +state-of-the-art implementation achieves. + ### Fallback-probe scaling ladder (cascade-trigger family) Per-rung 3-trial sweep at commit `e9b6ea1c-dirty` on `carica` diff --git a/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py b/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py new file mode 100755 index 000000000..f80354739 --- /dev/null +++ b/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py @@ -0,0 +1,146 @@ +#!/usr/bin/env python3 +"""Time python-flint on the Swinnerton-Dyer tier-crossover ladders. + +Produces the informational FLINT curve for +`scripts/plots/hex-berlekamp-zassenhaus-sd.py`. FLINT is *informational +only* at the BZ level (see the library SPEC §External comparators); the +gating comparator is the verified Isabelle extraction, whose rungs are +lean-bench registrations (`runIsabelleAdvSwinnertonDyer*Checksum`). + +The inputs are recomputed from sympy `minimal_polynomial` — the same +source the Lean bench pins its literals from — and cross-checked against +the constant coefficients that `bench/HexBerlekampZassenhaus/Bench.lean` +pins with `#guard`, so the two input sets cannot drift apart silently. + +Usage: hex-berlekamp-zassenhaus-sd-flint.py OUTPUT.json +""" + +from __future__ import annotations + +import json +import subprocess +import sys +import time +from pathlib import Path + +import sympy +from flint import fmpz_poly +from sympy import Poly, expand, minimal_polynomial, sqrt, symbols + +x = symbols("x") +PRIMES = [2, 3, 5, 7, 11] + +# Constant coefficients pinned by #guard in bench/HexBerlekampZassenhaus/Bench.lean. +PINS = { + ("pair", 2): -8, + ("pair", 3): -40896, + ("pair", 4): 107460921600, + ("pair", 5): 11101827931906700692775396966400, + ("blocks", 3): -1039528705604601600, + ("blocks", 4): -30893529063662744356454400, +} + + +def sd(k: int) -> Poly: + return Poly(minimal_polynomial(sum(sqrt(p) for p in PRIMES[:k]), x), x) + + +def shift(p: Poly, a: int) -> Poly: + return Poly(expand(p.as_expr().subs(x, x + a)), x) + + +def coeffs_asc(p: Poly) -> list[int]: + return [int(c) for c in reversed(p.all_coeffs())] + + +def build_families() -> dict[str, dict[int, list[int]]]: + ladder = {k: sd(k) for k in range(1, 6)} + pair = {k: Poly(expand(ladder[k].as_expr() * shift(ladder[k], 1).as_expr()), x) + for k in range(1, 6)} + sd4 = ladder[4] + blocks = {} + for m in range(1, 5): + prod = Poly(1, x) + for i in range(m): + prod = Poly(expand(prod.as_expr() * shift(sd4, i).as_expr()), x) + blocks[m] = prod + for k, p in ladder.items(): + assert p.degree() == 2 ** k, (k, p.degree()) + for k, p in pair.items(): + assert p.degree() == 2 ** (k + 1), (k, p.degree()) + for m, p in blocks.items(): + assert p.degree() == 16 * m, (m, p.degree()) + # Constant-coefficient pins only: this catches input-family drift (wrong + # shift, wrong product, wrong SD index) but not a hypothetical sympy + # change to interior coefficients. The Lean `#guard`s pin the same + # constants against the same sympy expansion, so the two sides fail + # together if either drifts. + for (fam, param), pin in PINS.items(): + p = {"pair": pair, "blocks": blocks}[fam][param] + got = int(p.all_coeffs()[-1]) + assert got == pin, f"{fam}[{param}] constant coefficient {got} != Lean pin {pin}" + return { + "ladder": {k: coeffs_asc(p) for k, p in ladder.items()}, + "pair": {k: coeffs_asc(p) for k, p in pair.items()}, + "blocks": {m: coeffs_asc(p) for m, p in blocks.items()}, + } + + +def time_flint(coeffs: list[int], min_total: float = 0.5) -> tuple[float, int]: + """Median-of-3 per-call seconds (auto-tuned inner repeats), factor count.""" + p = fmpz_poly(coeffs) + _, fac = p.factor() + nfac = sum(m for _, m in fac) + reps = 1 + while True: + t0 = time.perf_counter() + for _ in range(reps): + p.factor() + dt = time.perf_counter() - t0 + if dt >= min_total or reps >= 1 << 20: + break + reps *= 2 + samples = [] + for _ in range(3): + t0 = time.perf_counter() + for _ in range(reps): + p.factor() + samples.append((time.perf_counter() - t0) / reps) + samples.sort() + return samples[1], nfac + + +def main() -> int: + out = Path(sys.argv[1]) if len(sys.argv) > 1 else None + if out is None: + print(__doc__, file=sys.stderr) + return 2 + families = build_families() + results = [] + for fam, rungs in families.items(): + for param, coeffs in sorted(rungs.items()): + median_s, nfac = time_flint(coeffs) + results.append({ + "family": fam, + "param": param, + "degree": len(coeffs) - 1, + "median_seconds_per_call": median_s, + "factor_count_with_multiplicity": nfac, + }) + print(f"{fam:7s} {param} | deg {len(coeffs)-1:3d} | {median_s*1e3:10.3f} ms | {nfac} factors") + git_commit = subprocess.run( + ["git", "rev-parse", "HEAD"], capture_output=True, text=True + ).stdout.strip() + out.write_text(json.dumps({ + "generator": "scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py", + "engine": f"python-flint (fmpz_poly.factor), sympy {sympy.__version__} inputs", + "git_commit": git_commit, + "timestamp_unix": int(time.time()), + "results": results, + }, indent=1) + "\n") + print(f"wrote {out}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/plots/hex-berlekamp-zassenhaus-sd.py b/scripts/plots/hex-berlekamp-zassenhaus-sd.py new file mode 100755 index 000000000..0b2dacdcb --- /dev/null +++ b/scripts/plots/hex-berlekamp-zassenhaus-sd.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Generate the Swinnerton-Dyer tier-crossover figures from committed bench exports. + +Three one-parameter families (see `bench/HexBerlekampZassenhaus/Bench.lean`, +"Swinnerton-Dyer tier-crossover ladders"): + +* ``sd-ladder`` — `SD_k`, k = 1..5 (irreducible; classical certification) +* ``sd-pair`` — `SD_k(x)·SD_k(x+1)`, k = 1..5 (classical → lattice at k = 5) +* ``sd4-blocks`` — `∏_{i[0-9]+)|PairK(?P[0-9]+)|SD4BlocksM(?P[0-9]+))" + r"Checksum$" +) +# Trivial-input (constant polynomial 1) round trip through the persistent +# comparator: the per-request overhead every Isabelle rung pays. Subtracted +# from the Isabelle curves, mirroring the headline report's ratio convention. +ISABELLE_BASELINE = re.compile(r"runIsabelleFactorBaselineChecksum$") + +FAMILIES = { + "sd-ladder": { + "title": "Swinnerton-Dyer ladder SD$_k$ (irreducible)", + "xlabel": "k (degree $2^k$, $r = 2^{k-1}$ local factors)", + "hex_export": "sd-ladder", + "flint_family": "ladder", + "isabelle_group": "ladder", + "crossover": None, + "missing_isabelle": {}, + }, + "sd-pair": { + "title": "Pair ladder SD$_k(x)\\,\\cdot\\,$SD$_k(x+1)$", + "xlabel": "k (degree $2^{k+1}$, two $2^{k-1}$-blocks)", + "hex_export": "sd-pair", + "flint_family": "pair", + "isabelle_group": "pair", + "crossover": (5, "classical declines at level boundary;\nCLD lattice tier answers"), + "missing_isabelle": {5: "> 120 s\n(no lattice tier)"}, + }, + "sd4-blocks": { + "title": "Block ladder $\\prod_{i Path: + """The unique committed export matching the pattern. + + Refuses to guess between sweeps: once exports from more than one commit + match, an explicit `--sha` is required. + """ + matches = sorted(RESULTS.glob(pattern)) + if not matches: + raise SystemExit(f"no bench export matches {pattern} under {RESULTS}") + if len(matches) > 1: + names = ", ".join(m.name for m in matches) + raise SystemExit( + f"multiple exports match {pattern} ({names}); pass an explicit --sha") + return matches[0] + + +def load_hex_curve(path: Path) -> dict[int, float]: + data = json.loads(path.read_text()) + curve: dict[int, list[float]] = {} + for result in data["results"]: + for point in result["points"]: + if point["status"] == "ok": + curve.setdefault(point["param"], []).append(point["per_call_nanos"]) + return {p: sorted(v)[len(v) // 2] / 1e9 for p, v in curve.items()} + + +def load_isabelle_rungs(path: Path) -> dict[str, dict[int, float]]: + data = json.loads(path.read_text()) + rungs: dict[str, dict[int, float]] = {"ladder": {}, "pair": {}, "blocks": {}} + baseline_s = 0.0 + for result in data["results"]: + if ISABELLE_BASELINE.search(result["function"]): + baseline_s = result["median_nanos"] / 1e9 + for result in data["results"]: + m = ISABELLE_RUNG.search(result["function"]) + if not m: + continue + raw_s = result["median_nanos"] / 1e9 + if raw_s <= baseline_s: + print(f"warning: {result['function']} is baseline-limited " + f"({raw_s * 1e3:.3f} ms <= baseline {baseline_s * 1e3:.3f} ms); " + "dropping the rung rather than plotting an artificial point") + continue + median_s = raw_s - baseline_s + if m.group("ladder"): + rungs["ladder"][int(m.group("ladder"))] = median_s + elif m.group("pair"): + rungs["pair"][int(m.group("pair"))] = median_s + elif m.group("blocks"): + k = int(m.group("blocks")) + rungs["blocks"][k] = median_s + # Duplicated inputs across families: the block rung m = 1 is SD_4 itself, + # and the block rung m = 2 is the pair rung k = 4 (SD_4(x)·SD_4(x+1)). + # Reuse those measurements on the blocks curve. + if 4 in rungs["ladder"] and 1 not in rungs["blocks"]: + rungs["blocks"][1] = rungs["ladder"][4] + if 4 in rungs["pair"] and 2 not in rungs["blocks"]: + rungs["blocks"][2] = rungs["pair"][4] + return rungs + + +def load_flint(path: Path) -> dict[str, dict[int, float]]: + data = json.loads(path.read_text()) + out: dict[str, dict[int, float]] = {} + for row in data["results"]: + out.setdefault(row["family"], {})[row["param"]] = row["median_seconds_per_call"] + return out + + +def draw(family: str, spec: dict, hex_curve: dict[int, float], + isabelle: dict[int, float], flint: dict[int, float], + missing: dict[int, str], out: Path) -> None: + fig, ax = plt.subplots(figsize=(6.4, 4.2)) + for label, curve, style in [ + ("hex `factor` (hybrid)", hex_curve, dict(marker="o", color="#1f77b4")), + ("Isabelle (verified AFP, overhead-subtracted)", isabelle, + dict(marker="s", color="#d62728")), + ("FLINT (informational)", flint, dict(marker="^", color="#7f7f7f", linestyle="--")), + ]: + if curve: + xs = sorted(curve) + ax.plot(xs, [curve[x] for x in xs], label=label, **style) + for param, note in missing.items(): + # An off-scale comparator rung: mark it with a rising dotted red tail + # from the last measured rung instead of a point. + last = max(isabelle) + ax.plot([last, param], [isabelle[last], ax.get_ylim()[1] * 2], + color="#d62728", linestyle=":", lw=1.0, clip_on=True) + ax.text(param - 0.08, ax.get_ylim()[1] * 0.30, f"Isabelle {note}", + ha="right", va="top", fontsize=8, color="#d62728") + if spec["crossover"]: + param, note = spec["crossover"] + ax.axvline(param - 0.5, color="#2ca02c", linestyle=":", lw=1.2) + ax.text(param - 0.58, min(hex_curve.values()) * 1.5, note, + fontsize=8, color="#2ca02c", va="bottom", ha="right") + ax.set_yscale("log") + ax.set_xticks(sorted(hex_curve)) + ax.set_xlabel(spec["xlabel"]) + ax.set_ylabel("median wall time per call (s)") + ax.set_title(spec["title"], fontsize=11) + ax.grid(True, which="both", alpha=0.25) + ax.legend(fontsize=8, loc="upper left") + fig.tight_layout() + fig.savefig(out, metadata={"Date": None}) + plt.close(fig) + print(f"wrote {out}") + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--sha", default="*", help="short SHA of the exports to plot") + parser.add_argument("--out-dir", type=Path, default=FIGURES) + args = parser.parse_args() + + isabelle = load_isabelle_rungs( + newest(f"hex-berlekamp-zassenhaus-{args.sha}-sd-isabelle.json")) + flint = load_flint(newest(f"hex-berlekamp-zassenhaus-{args.sha}-sd-flint.json")) + args.out_dir.mkdir(parents=True, exist_ok=True) + for family, spec in FAMILIES.items(): + hex_curve = load_hex_curve( + newest(f"hex-berlekamp-zassenhaus-{args.sha}-{spec['hex_export']}.json")) + draw(family, spec, hex_curve, + isabelle.get(spec["isabelle_group"], {}), + flint.get(spec["flint_family"], {}), + spec["missing_isabelle"], + args.out_dir / f"hex-berlekamp-zassenhaus-{family}.svg") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())