From 88f72032e3b768ffa4a80d3c960b8a0e0b971cf0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 21:48:16 +1000 Subject: [PATCH 1/7] bench: Swinnerton-Dyer tier-crossover ladders (SD_k, SD_k pairs, SD4 blocks) Register the #8537 benchmark families as tracked lean-bench targets: the SD_k irreducible ladder (k = 1..5), the pair ladder SD_k(x)*SD_k(x+1) (k = 1..5, classical -> lattice crossover at k = 5), and the block ladder prod_{i --- bench/HexBerlekampZassenhaus/Bench.lean | 256 ++++++++++++++++++++++++ 1 file changed, 256 insertions(+) diff --git a/bench/HexBerlekampZassenhaus/Bench.lean b/bench/HexBerlekampZassenhaus/Bench.lean index d0e54d8a0..4bc8e3462 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 +558,38 @@ def prepAdvSwinnertonDyerSD3 (_ : Nat) : ZPoly := def prepAdvPhi15 (_ : Nat) : ZPoly := advPhi15 +/-- Prep for the Swinnerton-Dyer ladder: parameter `k` selects `SD_k`. -/ +def prepAdvSwinnertonDyerLadder (k : Nat) : ZPoly := + advSwinnertonDyerLadder.getD (k - 1) advSwinnertonDyerSD3 + +/-- Prep for the pair ladder: parameter `k` selects `SD_k(x) · SD_k(x+1)`. -/ +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 +1334,66 @@ 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): + +* `runFactorAdvSwinnertonDyerLadderChecksum k` — `SD_k`, `k = 1..5`: + irreducible worst cases; the classical tier certifies by enumerating + `2^(2^(k-1)-1)` candidates. +* `runFactorAdvSwinnertonDyerPairChecksum k` — `SD_k(x)·SD_k(x+1)`, + `k = 1..5`: classical answers `k ≤ 4`; `k = 5` declines at the level-aware + boundary (206368 candidates) and the CLD lattice tier answers. +* `runFactorAdvSwinnertonDyerSD4BlocksChecksum m` — `∏_{i 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] + } + +setup_benchmark runFactorAdvSwinnertonDyerPairChecksum k => 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] + } + +setup_benchmark runFactorAdvSwinnertonDyerSD4BlocksChecksum m => m + 1 + 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 +1654,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 From 7da4747e34da141d610ff7bcb6911bd38e5a4c21 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 21:53:25 +1000 Subject: [PATCH 2/7] bench: SD tier-crossover figure generators (hex/Isabelle/FLINT curves) Add scripts/plots/hex-berlekamp-zassenhaus-sd.py (three log-y wall-time figures from the committed lean-bench exports, with the Isabelle per-request baseline subtracted per the headline-report convention and missing comparator rungs annotated rather than dropped) and the companion hex-berlekamp-zassenhaus-sd-flint.py (informational python-flint curve, inputs cross-checked against the Lean #guard pins). Co-Authored-By: Claude Opus 4.8 --- .../hex-berlekamp-zassenhaus-sd-flint.py | 135 +++++++++++++ scripts/plots/hex-berlekamp-zassenhaus-sd.py | 190 ++++++++++++++++++ 2 files changed, 325 insertions(+) create mode 100755 scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py create mode 100755 scripts/plots/hex-berlekamp-zassenhaus-sd.py 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..d2759b61c --- /dev/null +++ b/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py @@ -0,0 +1,135 @@ +#!/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 (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..fd7f51f19 --- /dev/null +++ b/scripts/plots/hex-berlekamp-zassenhaus-sd.py @@ -0,0 +1,190 @@ +#!/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: + """Newest committed export matching the pattern (lexicographic on name).""" + matches = sorted(RESULTS.glob(pattern)) + if not matches: + raise SystemExit(f"no bench export matches {pattern} under {RESULTS}") + return matches[-1] + + +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 + median_s = max(result["median_nanos"] / 1e9 - baseline_s, 1e-9) + 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 + # The pair rung k = 4 and the block rung m = 2 share the input + # SD_4(x)·SD_4(x+1); reuse the measurement on the blocks curve. + 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(): + ax.annotate(f"Isabelle {note}", xy=(param, ax.get_ylim()[1]), + xytext=(param - 1.6, ax.get_ylim()[1] * 0.25), + fontsize=8, color="#d62728", + arrowprops=dict(arrowstyle="->", color="#d62728", lw=0.8)) + if spec["crossover"]: + param, note = spec["crossover"] + ax.axvline(param - 0.5, color="#2ca02c", linestyle=":", lw=1.2) + ax.text(param - 0.45, min(hex_curve.values()) * 1.5, note, + fontsize=8, color="#2ca02c", va="bottom") + 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()) From 3a18760f87299d0ad7d919559bb064d6c6a7c5cb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 21:57:25 +1000 Subject: [PATCH 3/7] bench: commit SD tier-crossover exports and figures (carica, 7da4747e) Clean-tree lean-bench exports for the three SD families and the verified-Isabelle rungs, the informational python-flint curve, and the three generated log-y scaling figures. Co-Authored-By: Claude Opus 4.8 --- ...erlekamp-zassenhaus-7da4747e-sd-flint.json | 106 + ...ekamp-zassenhaus-7da4747e-sd-isabelle.json | 539 ++++ ...rlekamp-zassenhaus-7da4747e-sd-ladder.json | 155 ++ ...berlekamp-zassenhaus-7da4747e-sd-pair.json | 155 ++ ...lekamp-zassenhaus-7da4747e-sd4-blocks.json | 133 + .../hex-berlekamp-zassenhaus-sd-ladder.svg | 2198 +++++++++++++++ .../hex-berlekamp-zassenhaus-sd-pair.svg | 2373 +++++++++++++++++ 7 files changed, 5659 insertions(+) create mode 100644 reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-flint.json create mode 100644 reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json create mode 100644 reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-ladder.json create mode 100644 reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-pair.json create mode 100644 reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd4-blocks.json create mode 100644 reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg create mode 100644 reports/figures/hex-berlekamp-zassenhaus-sd-pair.svg diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-flint.json b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-flint.json new file mode 100644 index 000000000..00ee053c0 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "timestamp_unix": 1782993351, + "results": [ + { + "family": "ladder", + "param": 1, + "degree": 2, + "median_seconds_per_call": 2.890912296216186e-07, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 2, + "degree": 4, + "median_seconds_per_call": 1.5690959941139226e-05, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 3, + "degree": 8, + "median_seconds_per_call": 6.942276002064318e-05, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 4, + "degree": 16, + "median_seconds_per_call": 0.0002965960898109188, + "factor_count_with_multiplicity": 1 + }, + { + "family": "ladder", + "param": 5, + "degree": 32, + "median_seconds_per_call": 0.0015310281560232397, + "factor_count_with_multiplicity": 1 + }, + { + "family": "pair", + "param": 1, + "degree": 4, + "median_seconds_per_call": 1.571265792676968e-05, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 2, + "degree": 8, + "median_seconds_per_call": 4.7605954478058266e-05, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 3, + "degree": 16, + "median_seconds_per_call": 0.00018833241779248056, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 4, + "degree": 32, + "median_seconds_per_call": 0.0013999522307130974, + "factor_count_with_multiplicity": 2 + }, + { + "family": "pair", + "param": 5, + "degree": 64, + "median_seconds_per_call": 0.008416277349169832, + "factor_count_with_multiplicity": 2 + }, + { + "family": "blocks", + "param": 1, + "degree": 16, + "median_seconds_per_call": 0.0002936237183348567, + "factor_count_with_multiplicity": 1 + }, + { + "family": "blocks", + "param": 2, + "degree": 32, + "median_seconds_per_call": 0.0014020831704328884, + "factor_count_with_multiplicity": 2 + }, + { + "family": "blocks", + "param": 3, + "degree": 48, + "median_seconds_per_call": 0.003597600749344565, + "factor_count_with_multiplicity": 3 + }, + { + "family": "blocks", + "param": 4, + "degree": 64, + "median_seconds_per_call": 0.007964288408402354, + "factor_count_with_multiplicity": 4 + } + ] +} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json new file mode 100644 index 000000000..89af0ab42 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json @@ -0,0 +1,539 @@ +{"results": + [{"points": + [{"total_nanos": 5457250, + "status": "ok", + "result_hash": "0xc2f2de73e00e63e3", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 7189542, + "status": "ok", + "result_hash": "0xc2f2de73e00e63e3", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 6399208, + "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": 5457250, + "median_nanos": 6399208, + "max_nanos": 7189542, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": "Hex.BerlekampZassenhausBench.runIsabelleFactorBaselineChecksum", + "expected_hash_check": {"status": "match"}, + "env": + {"timestamp_unix_ms": 1782993257811, + "timestamp_iso": "2026-07-02T11:54:17Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 9079458, + "status": "ok", + "result_hash": "0xfd5a821e013bc945", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 18453208, + "status": "ok", + "result_hash": "0xfd5a821e013bc945", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 12036583, + "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": 9079458, + "median_nanos": 12036583, + "max_nanos": 18453208, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD3Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993258024, + "timestamp_iso": "2026-07-02T11:54:18Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 10811417, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 10637250, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 9781083, + "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": 9781083, + "median_nanos": 10637250, + "max_nanos": 10811417, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993258236, + "timestamp_iso": "2026-07-02T11:54:18Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 41191292, + "status": "ok", + "result_hash": "0xd79637486bd0e8f1", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 41850708, + "status": "ok", + "result_hash": "0xd79637486bd0e8f1", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 41826875, + "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": 41191292, + "median_nanos": 41826875, + "max_nanos": 41850708, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD5Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993258431, + "timestamp_iso": "2026-07-02T11:54:18Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 11575917, + "status": "ok", + "result_hash": "0x91a910093667deb", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 10414292, + "status": "ok", + "result_hash": "0x91a910093667deb", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 9997500, + "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": 9997500, + "median_nanos": 10414292, + "max_nanos": 11575917, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK2Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993258752, + "timestamp_iso": "2026-07-02T11:54:18Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 11179959, + "status": "ok", + "result_hash": "0xe662c5d3f8bd82a4", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 11690250, + "status": "ok", + "result_hash": "0xe662c5d3f8bd82a4", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 12036000, + "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": 11179959, + "median_nanos": 11690250, + "max_nanos": 12036000, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK3Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993258953, + "timestamp_iso": "2026-07-02T11:54:18Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 23379875, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 22737750, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 24823500, + "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": 22737750, + "median_nanos": 23379875, + "max_nanos": 24823500, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK4Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993259156, + "timestamp_iso": "2026-07-02T11:54:19Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 399389833, + "status": "ok", + "result_hash": "0x6c60e1792f37236e", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 406025208, + "status": "ok", + "result_hash": "0x6c60e1792f37236e", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 411399083, + "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": 399389833, + "median_nanos": 406025208, + "max_nanos": 411399083, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4BlocksM3Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993259407, + "timestamp_iso": "2026-07-02T11:54:19Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 4540862708, + "status": "ok", + "result_hash": "0xbfade8ca2e42228c", + "repeat_index": 0, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 4852883625, + "status": "ok", + "result_hash": "0xbfade8ca2e42228c", + "repeat_index": 1, + "peak_rss_kb": null, + "inner_repeats": 1, + "error": null, + "alloc_bytes": null}, + {"total_nanos": 4609761542, + "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": 4540862708, + "median_nanos": 4609761542, + "max_nanos": 4852883625, + "kind": "fixed", + "hashes_agree": true, + "hashable": true, + "function": + "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4BlocksM4Checksum", + "expected_hash_check": {"status": "unset"}, + "env": + {"timestamp_unix_ms": 1782993261190, + "timestamp_iso": "2026-07-02T11:54:21Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": 1782993257811, + "timestamp_iso": "2026-07-02T11:54:17Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-ladder.json b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-ladder.json new file mode 100644 index 000000000..264c1da9e --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-ladder.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": 36752.421387, + "median_per_call_nanos": 36752.421387, + "max_per_call_nanos": 36752.421387}, + {"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 134775.146484, + "median_per_call_nanos": 134775.146484, + "max_per_call_nanos": 134775.146484}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 1616261.078125, + "median_per_call_nanos": 1616261.078125, + "max_per_call_nanos": 1616261.078125}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 17351416.5, + "median_per_call_nanos": 17351416.5, + "max_per_call_nanos": 17351416.5}, + {"relative_spread": 0, + "param": 5, + "ok_count": 1, + "min_per_call_nanos": 354438875, + "median_per_call_nanos": 354438875, + "max_per_call_nanos": 354438875}], + "spawn_floor_nanos": 34539666, + "slope": null, + "ratios": + [[2, 44925.048828], + [3, 404065.269531], + [4, 3470283.3], + [5, 59073145.833333]], + "points": + [{"trial_index": 0, + "total_nanos": 75268959, + "status": "ok", + "result_hash": "0x7a04d2ad549a6dd3", + "per_call_nanos": 36752.421387, + "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": 69004875, + "status": "ok", + "result_hash": "0x37ffee7fa6956231", + "per_call_nanos": 134775.146484, + "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": 103440709, + "status": "ok", + "result_hash": "0xfd5a821e013bc945", + "per_call_nanos": 1616261.078125, + "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": 69405666, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "per_call_nanos": 17351416.5, + "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": 354438875, + "status": "ok", + "result_hash": "0xd79637486bd0e8f1", + "per_call_nanos": 354438875, + "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": 1782993220961, + "timestamp_iso": "2026-07-02T11:53:40Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": "k + 1", + "c_min": 44925.048828, + "c_max": 59073145.833333, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1782993220961, + "timestamp_iso": "2026-07-02T11:53:40Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-pair.json b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-pair.json new file mode 100644 index 000000000..082b23a66 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-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": 226606.605469, + "median_per_call_nanos": 226606.605469, + "max_per_call_nanos": 226606.605469}, + {"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 1483320.3125, + "median_per_call_nanos": 1483320.3125, + "max_per_call_nanos": 1483320.3125}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 25741156.25, + "median_per_call_nanos": 25741156.25, + "max_per_call_nanos": 25741156.25}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 260786750, + "median_per_call_nanos": 260786750, + "max_per_call_nanos": 260786750}, + {"relative_spread": 0, + "param": 5, + "ok_count": 1, + "min_per_call_nanos": 16709169583, + "median_per_call_nanos": 16709169583, + "max_per_call_nanos": 16709169583}], + "spawn_floor_nanos": 41442208, + "slope": null, + "ratios": + [[2, 494440.104167], + [3, 6435289.0625], + [4, 52157350], + [5, 2784861597.166667]], + "points": + [{"trial_index": 0, + "total_nanos": 58011291, + "status": "ok", + "result_hash": "0xe0c054166fe7ff22", + "per_call_nanos": 226606.605469, + "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": 94932500, + "status": "ok", + "result_hash": "0x91a910093667deb", + "per_call_nanos": 1483320.3125, + "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": 102964625, + "status": "ok", + "result_hash": "0xe662c5d3f8bd82a4", + "per_call_nanos": 25741156.25, + "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": 260786750, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "per_call_nanos": 260786750, + "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": 16709169583, + "status": "ok", + "result_hash": "0x6a608009af52d72d", + "per_call_nanos": 16709169583, + "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": 1782993222227, + "timestamp_iso": "2026-07-02T11:53:42Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": "k + 1", + "c_min": 494440.104167, + "c_max": 2784861597.166667, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1782993222227, + "timestamp_iso": "2026-07-02T11:53:42Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "exe_name": "hexbz_bench", + "cpu_model": null, + "cpu_cores": null, + "arch": "arm64"}} diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd4-blocks.json b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd4-blocks.json new file mode 100644 index 000000000..10859e091 --- /dev/null +++ b/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-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": 17205302.25, + "median_per_call_nanos": 17205302.25, + "max_per_call_nanos": 17205302.25}, + {"relative_spread": 0, + "param": 2, + "ok_count": 1, + "min_per_call_nanos": 262806250, + "median_per_call_nanos": 262806250, + "max_per_call_nanos": 262806250}, + {"relative_spread": 0, + "param": 3, + "ok_count": 1, + "min_per_call_nanos": 3360426833, + "median_per_call_nanos": 3360426833, + "max_per_call_nanos": 3360426833}, + {"relative_spread": 0, + "param": 4, + "ok_count": 1, + "min_per_call_nanos": 14018191917, + "median_per_call_nanos": 14018191917, + "max_per_call_nanos": 14018191917}], + "spawn_floor_nanos": 31220541, + "slope": null, + "ratios": [[2, 87602083.333333], [3, 840106708.25], [4, 2803638383.4]], + "points": + [{"trial_index": 0, + "total_nanos": 68821209, + "status": "ok", + "result_hash": "0x36f82522fa530950", + "per_call_nanos": 17205302.25, + "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": 262806250, + "status": "ok", + "result_hash": "0x28afc4e530363597", + "per_call_nanos": 262806250, + "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": 3360426833, + "status": "ok", + "result_hash": "0x6c60e1792f37236e", + "per_call_nanos": 3360426833, + "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": 14018191917, + "status": "ok", + "result_hash": "0xbfade8ca2e42228c", + "per_call_nanos": 14018191917, + "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": 1782993239823, + "timestamp_iso": "2026-07-02T11:53:59Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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": "m + 1", + "c_min": 87602083.333333, + "c_max": 2803638383.4, + "budget_truncated": false, + "advisories": []}], + "lean_bench_version": "0.1.0", + "export_schema_version": 1, + "env": + {"timestamp_unix_ms": 1782993239823, + "timestamp_iso": "2026-07-02T11:53:59Z", + "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": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "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..368f5ed7b --- /dev/null +++ b/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg @@ -0,0 +1,2198 @@ + + + + + + + + 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..4092012ec --- /dev/null +++ b/reports/figures/hex-berlekamp-zassenhaus-sd-pair.svg @@ -0,0 +1,2373 @@ + + + + + + + + image/svg+xml + + + Matplotlib v3.10.9, https://matplotlib.org/ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + From 8bedd2780f6f9e2d5693e9a1b0b014d98a3895ee Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 21:59:52 +1000 Subject: [PATCH 4/7] doc: SD tier-crossover subsection in the BZ headline report Tables, figures, artefact SHA-256s, hex-vs-Isabelle multiset-agreement hashes for all nine shared rungs, and the trend narrative (including the hex-loses-ground-with-r observation on the certification ladder, flagged as an optimisation target). Co-Authored-By: Claude Opus 4.8 --- .../hex-berlekamp-zassenhaus-performance.md | 93 +++++++++++++++++++ 1 file changed, 93 insertions(+) diff --git a/reports/hex-berlekamp-zassenhaus-performance.md b/reports/hex-berlekamp-zassenhaus-performance.md index 0fff840e9..ba3eda830 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`: `k + 1` +- `Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerPairChecksum`: `k + 1` +- `Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerSD4BlocksChecksum`: `m + 1` ## Comparator Ratios @@ -483,6 +486,96 @@ 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`; declared `k + 1` models are placeholders in the +SD3-singleton style, 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 `7da4747e` (clean tree) on `carica` +(Apple M2 Ultra, macOS), recorded `2026-07-02T11:53:40Z`: + +```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 7da4747e +``` + +Export artefacts (`reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-*`), +SHA-256: + +| artefact | SHA-256 | +|---|---| +| `-sd-ladder.json` | `a7b643c1395299c195844a9610a4117585d8a36227afa040dc03ac8ffc403577` | +| `-sd-pair.json` | `36f2307d44af834d8707378f00b5afdd71edfe63a4dd5315bccbe2b1acc43469` | +| `-sd4-blocks.json` | `3e077ad5a3637400e1ddf1259a9cff18e39801219e13c05ee380939b2f30d377` | +| `-sd-isabelle.json` | `c373605068f2182ea3b800e6214d052c1ba7bba774973df9b7b35eeaf97f7e8d` | +| `-sd-flint.json` | `052d547c8dd7904a8d38192ec57919cd2e90fec4bcb8b8c3ff09e0aef052300e` | + +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 `6.399 ms` recorded in the same +export; FLINT informational): + +| family / rung | deg | hex `factor` | Isabelle (raw) | FLINT | tier | +|---|---:|---:|---:|---:|---| +| `SD_k` k=1 | 2 | 0.037 ms | — | 0.0003 ms | quadratic | +| `SD_k` k=2 | 4 | 0.135 ms | — | 0.016 ms | classical | +| `SD_k` k=3 | 8 | 1.616 ms | 12.04 ms | 0.071 ms | classical | +| `SD_k` k=4 | 16 | 17.35 ms | 10.64 ms | 0.300 ms | classical | +| `SD_k` k=5 | 32 | 354.4 ms | 41.83 ms | 1.541 ms | classical | +| pair k=1 | 4 | 0.227 ms | — | 0.016 ms | classical | +| pair k=2 | 8 | 1.483 ms | 10.41 ms | 0.048 ms | classical | +| pair k=3 | 16 | 25.74 ms | 11.69 ms | 0.192 ms | classical | +| pair k=4 | 32 | 260.8 ms | 23.38 ms | 1.439 ms | classical | +| pair k=5 | 64 | **16.71 s** | **> 120 s (killed)** | 8.575 ms | **lattice** | +| blocks m=1 | 16 | 17.21 ms | 10.64 ms | 0.299 ms | classical | +| blocks m=2 | 32 | 262.8 ms | 23.38 ms | 1.430 ms | classical | +| blocks m=3 | 48 | 3.360 s | 406.0 ms | 3.664 ms | lattice | +| blocks m=4 | 64 | 14.02 s | 4.610 s | 8.091 ms | lattice | + +Multiset agreement: on all nine rungs shared with an Isabelle +registration, the hex parametric `result_hash` equals the Isabelle +rung's `observed_hash` (canonical order-insensitive factor-multiset +checksum) — `0xfd5a821e013bc945` (SD3), `0x36f82522fa530950` (SD4), +`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 (hex/Isabelle ≈ 1.6 at SD4, ≈ 10 at SD5 and +blocks m=3, ≈ 3–4 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` From 6a7ce1e4755b08c8ddaced970ad1fc910b748357 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 22:08:22 +1000 Subject: [PATCH 5/7] fix: address bench-branch review findings Commit the sd4-blocks figure the earlier glob missed; map the SD4 measurement onto the blocks m=1 comparator point; make the plot script refuse to guess between multiple committed sweeps and drop (with a warning) baseline-limited Isabelle rungs instead of plotting artificial points; add degree asserts and a scope note to the FLINT cross-check; make the ladder preps panic loudly out of schedule instead of silently substituting SD3; state the eight-distinct-inputs/two-duplications structure of the agreement hashes explicitly in the report. Co-Authored-By: Claude Opus 4.8 --- bench/HexBerlekampZassenhaus/Bench.lean | 14 +- progress/20260702T120303Z_bench-sd-review.md | 20 + .../20260702T121500Z_bench-sd-families.md | 41 + .../hex-berlekamp-zassenhaus-sd4-blocks.svg | 2171 +++++++++++++++++ .../hex-berlekamp-zassenhaus-performance.md | 21 +- .../hex-berlekamp-zassenhaus-sd-flint.py | 11 + scripts/plots/hex-berlekamp-zassenhaus-sd.py | 42 +- 7 files changed, 2296 insertions(+), 24 deletions(-) create mode 100644 progress/20260702T120303Z_bench-sd-review.md create mode 100644 progress/20260702T121500Z_bench-sd-families.md create mode 100644 reports/figures/hex-berlekamp-zassenhaus-sd4-blocks.svg diff --git a/bench/HexBerlekampZassenhaus/Bench.lean b/bench/HexBerlekampZassenhaus/Bench.lean index 4bc8e3462..fa5d106ac 100644 --- a/bench/HexBerlekampZassenhaus/Bench.lean +++ b/bench/HexBerlekampZassenhaus/Bench.lean @@ -133,6 +133,9 @@ namespace BerlekampZassenhausBench open Lean (Json) +/-- Default for the ladder preps' loud out-of-range panics (`#[…][i]!`). -/ +local instance : Inhabited ZPoly := ⟨0⟩ + private instance benchBoundsThirtyOne : ZMod64.Bounds 31 := ⟨by decide, by decide⟩ instance : Hashable ZPoly where @@ -234,7 +237,7 @@ candidates, so classical declines at its level boundary and the CLD lattice tier answers. This is the family behind #8530/#8537. -/ def advSwinnertonDyerPair (k : Nat) : ZPoly := - let p := advSwinnertonDyerLadder.getD (k - 1) advSwinnertonDyerSD3 + let p := advSwinnertonDyerLadder[k - 1]! p * shiftArg p 1 -- Constant coefficients of the derived products, pinned against the sympy @@ -558,11 +561,14 @@ def prepAdvSwinnertonDyerSD3 (_ : Nat) : ZPoly := def prepAdvPhi15 (_ : Nat) : ZPoly := advPhi15 -/-- Prep for the Swinnerton-Dyer ladder: parameter `k` selects `SD_k`. -/ +/-- 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.getD (k - 1) advSwinnertonDyerSD3 + advSwinnertonDyerLadder[k - 1]! -/-- Prep for the pair ladder: parameter `k` selects `SD_k(x) · SD_k(x+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 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/figures/hex-berlekamp-zassenhaus-sd4-blocks.svg b/reports/figures/hex-berlekamp-zassenhaus-sd4-blocks.svg new file mode 100644 index 000000000..23d044563 --- /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 ba3eda830..db6476a27 100644 --- a/reports/hex-berlekamp-zassenhaus-performance.md +++ b/reports/hex-berlekamp-zassenhaus-performance.md @@ -550,15 +550,18 @@ export; FLINT informational): | blocks m=3 | 48 | 3.360 s | 406.0 ms | 3.664 ms | lattice | | blocks m=4 | 64 | 14.02 s | 4.610 s | 8.091 ms | lattice | -Multiset agreement: on all nine rungs shared with an Isabelle -registration, the hex parametric `result_hash` equals the Isabelle -rung's `observed_hash` (canonical order-insensitive factor-multiset -checksum) — `0xfd5a821e013bc945` (SD3), `0x36f82522fa530950` (SD4), -`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. +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 diff --git a/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py b/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py index d2759b61c..f80354739 100755 --- a/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py +++ b/scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py @@ -64,6 +64,17 @@ def build_families() -> dict[str, dict[int, list[int]]]: 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]) diff --git a/scripts/plots/hex-berlekamp-zassenhaus-sd.py b/scripts/plots/hex-berlekamp-zassenhaus-sd.py index fd7f51f19..0b2dacdcb 100755 --- a/scripts/plots/hex-berlekamp-zassenhaus-sd.py +++ b/scripts/plots/hex-berlekamp-zassenhaus-sd.py @@ -78,11 +78,19 @@ def newest(pattern: str) -> Path: - """Newest committed export matching the pattern (lexicographic on name).""" + """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}") - return matches[-1] + 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]: @@ -106,7 +114,13 @@ def load_isabelle_rungs(path: Path) -> dict[str, dict[int, float]]: m = ISABELLE_RUNG.search(result["function"]) if not m: continue - median_s = max(result["median_nanos"] / 1e9 - baseline_s, 1e-9) + 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"): @@ -114,8 +128,11 @@ def load_isabelle_rungs(path: Path) -> dict[str, dict[int, float]]: elif m.group("blocks"): k = int(m.group("blocks")) rungs["blocks"][k] = median_s - # The pair rung k = 4 and the block rung m = 2 share the input - # SD_4(x)·SD_4(x+1); reuse the measurement on the blocks curve. + # 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 @@ -143,15 +160,18 @@ def draw(family: str, spec: dict, hex_curve: dict[int, float], xs = sorted(curve) ax.plot(xs, [curve[x] for x in xs], label=label, **style) for param, note in missing.items(): - ax.annotate(f"Isabelle {note}", xy=(param, ax.get_ylim()[1]), - xytext=(param - 1.6, ax.get_ylim()[1] * 0.25), - fontsize=8, color="#d62728", - arrowprops=dict(arrowstyle="->", color="#d62728", lw=0.8)) + # 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.45, min(hex_curve.values()) * 1.5, note, - fontsize=8, color="#2ca02c", va="bottom") + 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"]) From 5ec8d8b57e5e0671351346dd9bf36b160b1b535b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 22:13:25 +1000 Subject: [PATCH 6/7] bench: cost-model derivations for the SD tier-crossover registrations Cost-model derivation, per family: SD_k splits into r = 2^(k-1) local factors mod every prime and classical certification enumerates the full head-forced subset powerset, so the candidate count 2^(2^(k-1)) dominates and is the declared complexity model for the ladder; the pair family is bounded by the same worst-case powerset shape through k = 4 and by the budget-constant decline plus the polynomial CLD lattice tier at k = 5; the block family's classical regime is the powerset bound 2^(8m - 1), declared 2^(8m), with the same polynomial lattice dominance past the m = 3 crossover. No single textbook exponent fits across a tier crossover, so the top-rung verdicts are expected inconclusive; the committed figures and per-rung canonical checksums carry the regression signal. Replaces the k + 1 placeholders that scripts/check_phase4.py rightly rejected as not being cost-model derivations. Co-Authored-By: Claude Opus 4.8 --- bench/HexBerlekampZassenhaus/Bench.lean | 50 +++++++++++++++---------- 1 file changed, 30 insertions(+), 20 deletions(-) diff --git a/bench/HexBerlekampZassenhaus/Bench.lean b/bench/HexBerlekampZassenhaus/Bench.lean index fa5d106ac..f9cb4ebf7 100644 --- a/bench/HexBerlekampZassenhaus/Bench.lean +++ b/bench/HexBerlekampZassenhaus/Bench.lean @@ -1345,26 +1345,21 @@ 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): - -* `runFactorAdvSwinnertonDyerLadderChecksum k` — `SD_k`, `k = 1..5`: - irreducible worst cases; the classical tier certifies by enumerating - `2^(2^(k-1)-1)` candidates. -* `runFactorAdvSwinnertonDyerPairChecksum k` — `SD_k(x)·SD_k(x+1)`, - `k = 1..5`: classical answers `k ≤ 4`; `k = 5` declines at the level-aware - boundary (206368 candidates) and the CLD lattice tier answers. -* `runFactorAdvSwinnertonDyerSD4BlocksChecksum m` — `∏_{i k + 1 + +-- 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 @@ -1376,7 +1371,15 @@ setup_benchmark runFactorAdvSwinnertonDyerLadderChecksum k => k + 1 tags := #[scheduledHardwareTag] } -setup_benchmark runFactorAdvSwinnertonDyerPairChecksum k => k + 1 +-- 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 @@ -1388,7 +1391,14 @@ setup_benchmark runFactorAdvSwinnertonDyerPairChecksum k => k + 1 tags := #[scheduledHardwareTag] } -setup_benchmark runFactorAdvSwinnertonDyerSD4BlocksChecksum m => m + 1 +-- 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 From 341c1384de05b1554dda7e7373db773617cd6d1a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 2 Jul 2026 22:18:19 +1000 Subject: [PATCH 7/7] bench: refresh SD exports, figures, and report at 5ec8d8b5 Re-sweep after the cost-model derivation commit so the committed artefacts, figures, and the headline report all cite one commit. All ten Isabelle-covered rows keep their canonical factor-multiset hashes (agreement unchanged); the trend-narrative ratios are now consistently overhead-adjusted (hex/Isabelle ~3.8 at SD4, ~9.5 at SD5 on the certification ladder). Co-Authored-By: Claude Opus 4.8 --- ...rlekamp-zassenhaus-5ec8d8b5-sd-flint.json} | 32 +- ...kamp-zassenhaus-5ec8d8b5-sd-isabelle.json} | 168 +++---- ...lekamp-zassenhaus-5ec8d8b5-sd-ladder.json} | 75 ++- ...erlekamp-zassenhaus-5ec8d8b5-sd-pair.json} | 78 +-- ...ekamp-zassenhaus-5ec8d8b5-sd4-blocks.json} | 62 +-- .../hex-berlekamp-zassenhaus-sd-ladder.svg | 434 ++++++++-------- .../hex-berlekamp-zassenhaus-sd-pair.svg | 472 +++++++++--------- .../hex-berlekamp-zassenhaus-sd4-blocks.svg | 330 ++++++------ .../hex-berlekamp-zassenhaus-performance.md | 73 +-- 9 files changed, 850 insertions(+), 874 deletions(-) rename reports/bench-results/{hex-berlekamp-zassenhaus-7da4747e-sd-flint.json => hex-berlekamp-zassenhaus-5ec8d8b5-sd-flint.json} (65%) rename reports/bench-results/{hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json => hex-berlekamp-zassenhaus-5ec8d8b5-sd-isabelle.json} (80%) rename reports/bench-results/{hex-berlekamp-zassenhaus-7da4747e-sd-ladder.json => hex-berlekamp-zassenhaus-5ec8d8b5-sd-ladder.json} (67%) rename reports/bench-results/{hex-berlekamp-zassenhaus-7da4747e-sd-pair.json => hex-berlekamp-zassenhaus-5ec8d8b5-sd-pair.json} (67%) rename reports/bench-results/{hex-berlekamp-zassenhaus-7da4747e-sd4-blocks.json => hex-berlekamp-zassenhaus-5ec8d8b5-sd4-blocks.json} (68%) diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-flint.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-flint.json similarity index 65% rename from reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-flint.json rename to reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-flint.json index 00ee053c0..e1234d498 100644 --- a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-flint.json +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-flint.json @@ -1,105 +1,105 @@ { "generator": "scripts/plots/hex-berlekamp-zassenhaus-sd-flint.py", "engine": "python-flint (fmpz_poly.factor), sympy 1.14.0 inputs", - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", - "timestamp_unix": 1782993351, + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", + "timestamp_unix": 1782994528, "results": [ { "family": "ladder", "param": 1, "degree": 2, - "median_seconds_per_call": 2.890912296216186e-07, + "median_seconds_per_call": 3.065994187423371e-07, "factor_count_with_multiplicity": 1 }, { "family": "ladder", "param": 2, "degree": 4, - "median_seconds_per_call": 1.5690959941139226e-05, + "median_seconds_per_call": 1.5654083256322338e-05, "factor_count_with_multiplicity": 1 }, { "family": "ladder", "param": 3, "degree": 8, - "median_seconds_per_call": 6.942276002064318e-05, + "median_seconds_per_call": 6.967456567963382e-05, "factor_count_with_multiplicity": 1 }, { "family": "ladder", "param": 4, "degree": 16, - "median_seconds_per_call": 0.0002965960898109188, + "median_seconds_per_call": 0.00029246276858430065, "factor_count_with_multiplicity": 1 }, { "family": "ladder", "param": 5, "degree": 32, - "median_seconds_per_call": 0.0015310281560232397, + "median_seconds_per_call": 0.001512591553364473, "factor_count_with_multiplicity": 1 }, { "family": "pair", "param": 1, "degree": 4, - "median_seconds_per_call": 1.571265792676968e-05, + "median_seconds_per_call": 1.5707024900279976e-05, "factor_count_with_multiplicity": 2 }, { "family": "pair", "param": 2, "degree": 8, - "median_seconds_per_call": 4.7605954478058266e-05, + "median_seconds_per_call": 4.80088170036197e-05, "factor_count_with_multiplicity": 2 }, { "family": "pair", "param": 3, "degree": 16, - "median_seconds_per_call": 0.00018833241779248056, + "median_seconds_per_call": 0.00018705276488617528, "factor_count_with_multiplicity": 2 }, { "family": "pair", "param": 4, "degree": 32, - "median_seconds_per_call": 0.0013999522307130974, + "median_seconds_per_call": 0.0014058453789402847, "factor_count_with_multiplicity": 2 }, { "family": "pair", "param": 5, "degree": 64, - "median_seconds_per_call": 0.008416277349169832, + "median_seconds_per_call": 0.008388305985135958, "factor_count_with_multiplicity": 2 }, { "family": "blocks", "param": 1, "degree": 16, - "median_seconds_per_call": 0.0002936237183348567, + "median_seconds_per_call": 0.00029293162015164853, "factor_count_with_multiplicity": 1 }, { "family": "blocks", "param": 2, "degree": 32, - "median_seconds_per_call": 0.0014020831704328884, + "median_seconds_per_call": 0.0014015908200235572, "factor_count_with_multiplicity": 2 }, { "family": "blocks", "param": 3, "degree": 48, - "median_seconds_per_call": 0.003597600749344565, + "median_seconds_per_call": 0.0035937760439992417, "factor_count_with_multiplicity": 3 }, { "family": "blocks", "param": 4, "degree": 64, - "median_seconds_per_call": 0.007964288408402354, + "median_seconds_per_call": 0.007978048175573349, "factor_count_with_multiplicity": 4 } ] diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-isabelle.json similarity index 80% rename from reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json rename to reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-isabelle.json index 89af0ab42..8f8f439ae 100644 --- a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-isabelle.json +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-isabelle.json @@ -1,6 +1,6 @@ {"results": [{"points": - [{"total_nanos": 5457250, + [{"total_nanos": 5324584, "status": "ok", "result_hash": "0xc2f2de73e00e63e3", "repeat_index": 0, @@ -8,7 +8,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 7189542, + {"total_nanos": 5612708, "status": "ok", "result_hash": "0xc2f2de73e00e63e3", "repeat_index": 1, @@ -16,7 +16,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 6399208, + {"total_nanos": 4978583, "status": "ok", "result_hash": "0xc2f2de73e00e63e3", "repeat_index": 2, @@ -25,17 +25,17 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0xc2f2de73e00e63e3", - "min_nanos": 5457250, - "median_nanos": 6399208, - "max_nanos": 7189542, + "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": 1782993257811, - "timestamp_iso": "2026-07-02T11:54:17Z", + {"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", @@ -43,7 +43,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -57,7 +57,7 @@ "expected_hash": "0xc2f2de73e00e63e3"}, "budget_truncated": false}, {"points": - [{"total_nanos": 9079458, + [{"total_nanos": 8674875, "status": "ok", "result_hash": "0xfd5a821e013bc945", "repeat_index": 0, @@ -65,7 +65,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 18453208, + {"total_nanos": 8739792, "status": "ok", "result_hash": "0xfd5a821e013bc945", "repeat_index": 1, @@ -73,7 +73,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 12036583, + {"total_nanos": 8818500, "status": "ok", "result_hash": "0xfd5a821e013bc945", "repeat_index": 2, @@ -82,9 +82,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0xfd5a821e013bc945", - "min_nanos": 9079458, - "median_nanos": 12036583, - "max_nanos": 18453208, + "min_nanos": 8674875, + "median_nanos": 8739792, + "max_nanos": 8818500, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -92,8 +92,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD3Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993258024, - "timestamp_iso": "2026-07-02T11:54:18Z", + {"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", @@ -101,7 +101,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -115,7 +115,7 @@ "expected_hash": null}, "budget_truncated": false}, {"points": - [{"total_nanos": 10811417, + [{"total_nanos": 9598292, "status": "ok", "result_hash": "0x36f82522fa530950", "repeat_index": 0, @@ -123,7 +123,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 10637250, + {"total_nanos": 9774750, "status": "ok", "result_hash": "0x36f82522fa530950", "repeat_index": 1, @@ -131,7 +131,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 9781083, + {"total_nanos": 9849167, "status": "ok", "result_hash": "0x36f82522fa530950", "repeat_index": 2, @@ -140,9 +140,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0x36f82522fa530950", - "min_nanos": 9781083, - "median_nanos": 10637250, - "max_nanos": 10811417, + "min_nanos": 9598292, + "median_nanos": 9774750, + "max_nanos": 9849167, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -150,8 +150,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993258236, - "timestamp_iso": "2026-07-02T11:54:18Z", + {"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", @@ -159,7 +159,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -173,7 +173,7 @@ "expected_hash": null}, "budget_truncated": false}, {"points": - [{"total_nanos": 41191292, + [{"total_nanos": 40211250, "status": "ok", "result_hash": "0xd79637486bd0e8f1", "repeat_index": 0, @@ -181,7 +181,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 41850708, + {"total_nanos": 39287792, "status": "ok", "result_hash": "0xd79637486bd0e8f1", "repeat_index": 1, @@ -189,7 +189,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 41826875, + {"total_nanos": 39726917, "status": "ok", "result_hash": "0xd79637486bd0e8f1", "repeat_index": 2, @@ -198,9 +198,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0xd79637486bd0e8f1", - "min_nanos": 41191292, - "median_nanos": 41826875, - "max_nanos": 41850708, + "min_nanos": 39287792, + "median_nanos": 39726917, + "max_nanos": 40211250, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -208,8 +208,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD5Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993258431, - "timestamp_iso": "2026-07-02T11:54:18Z", + {"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", @@ -217,7 +217,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -231,7 +231,7 @@ "expected_hash": null}, "budget_truncated": false}, {"points": - [{"total_nanos": 11575917, + [{"total_nanos": 8829417, "status": "ok", "result_hash": "0x91a910093667deb", "repeat_index": 0, @@ -239,7 +239,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 10414292, + {"total_nanos": 8487292, "status": "ok", "result_hash": "0x91a910093667deb", "repeat_index": 1, @@ -247,7 +247,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 9997500, + {"total_nanos": 8594209, "status": "ok", "result_hash": "0x91a910093667deb", "repeat_index": 2, @@ -256,9 +256,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0x91a910093667deb", - "min_nanos": 9997500, - "median_nanos": 10414292, - "max_nanos": 11575917, + "min_nanos": 8487292, + "median_nanos": 8594209, + "max_nanos": 8829417, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -266,8 +266,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK2Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993258752, - "timestamp_iso": "2026-07-02T11:54:18Z", + {"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", @@ -275,7 +275,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -289,7 +289,7 @@ "expected_hash": null}, "budget_truncated": false}, {"points": - [{"total_nanos": 11179959, + [{"total_nanos": 9823750, "status": "ok", "result_hash": "0xe662c5d3f8bd82a4", "repeat_index": 0, @@ -297,7 +297,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 11690250, + {"total_nanos": 9823875, "status": "ok", "result_hash": "0xe662c5d3f8bd82a4", "repeat_index": 1, @@ -305,7 +305,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 12036000, + {"total_nanos": 9904583, "status": "ok", "result_hash": "0xe662c5d3f8bd82a4", "repeat_index": 2, @@ -314,9 +314,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0xe662c5d3f8bd82a4", - "min_nanos": 11179959, - "median_nanos": 11690250, - "max_nanos": 12036000, + "min_nanos": 9823750, + "median_nanos": 9823875, + "max_nanos": 9904583, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -324,8 +324,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK3Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993258953, - "timestamp_iso": "2026-07-02T11:54:18Z", + {"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", @@ -333,7 +333,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -347,7 +347,7 @@ "expected_hash": null}, "budget_truncated": false}, {"points": - [{"total_nanos": 23379875, + [{"total_nanos": 21637083, "status": "ok", "result_hash": "0x28afc4e530363597", "repeat_index": 0, @@ -355,7 +355,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 22737750, + {"total_nanos": 21258458, "status": "ok", "result_hash": "0x28afc4e530363597", "repeat_index": 1, @@ -363,7 +363,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 24823500, + {"total_nanos": 21742042, "status": "ok", "result_hash": "0x28afc4e530363597", "repeat_index": 2, @@ -372,9 +372,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0x28afc4e530363597", - "min_nanos": 22737750, - "median_nanos": 23379875, - "max_nanos": 24823500, + "min_nanos": 21258458, + "median_nanos": 21637083, + "max_nanos": 21742042, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -382,8 +382,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerPairK4Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993259156, - "timestamp_iso": "2026-07-02T11:54:19Z", + {"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", @@ -391,7 +391,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -405,7 +405,7 @@ "expected_hash": null}, "budget_truncated": false}, {"points": - [{"total_nanos": 399389833, + [{"total_nanos": 418307917, "status": "ok", "result_hash": "0x6c60e1792f37236e", "repeat_index": 0, @@ -413,7 +413,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 406025208, + {"total_nanos": 385832042, "status": "ok", "result_hash": "0x6c60e1792f37236e", "repeat_index": 1, @@ -421,7 +421,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 411399083, + {"total_nanos": 384243292, "status": "ok", "result_hash": "0x6c60e1792f37236e", "repeat_index": 2, @@ -430,9 +430,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0x6c60e1792f37236e", - "min_nanos": 399389833, - "median_nanos": 406025208, - "max_nanos": 411399083, + "min_nanos": 384243292, + "median_nanos": 385832042, + "max_nanos": 418307917, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -440,8 +440,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4BlocksM3Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993259407, - "timestamp_iso": "2026-07-02T11:54:19Z", + {"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", @@ -449,7 +449,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -463,7 +463,7 @@ "expected_hash": null}, "budget_truncated": false}, {"points": - [{"total_nanos": 4540862708, + [{"total_nanos": 4336240416, "status": "ok", "result_hash": "0xbfade8ca2e42228c", "repeat_index": 0, @@ -471,7 +471,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 4852883625, + {"total_nanos": 4324568875, "status": "ok", "result_hash": "0xbfade8ca2e42228c", "repeat_index": 1, @@ -479,7 +479,7 @@ "inner_repeats": 1, "error": null, "alloc_bytes": null}, - {"total_nanos": 4609761542, + {"total_nanos": 4413780584, "status": "ok", "result_hash": "0xbfade8ca2e42228c", "repeat_index": 2, @@ -488,9 +488,9 @@ "error": null, "alloc_bytes": null}], "observed_hash": "0xbfade8ca2e42228c", - "min_nanos": 4540862708, - "median_nanos": 4609761542, - "max_nanos": 4852883625, + "min_nanos": 4324568875, + "median_nanos": 4336240416, + "max_nanos": 4413780584, "kind": "fixed", "hashes_agree": true, "hashable": true, @@ -498,8 +498,8 @@ "Hex.BerlekampZassenhausBench.runIsabelleAdvSwinnertonDyerSD4BlocksM4Checksum", "expected_hash_check": {"status": "unset"}, "env": - {"timestamp_unix_ms": 1782993261190, - "timestamp_iso": "2026-07-02T11:54:21Z", + {"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", @@ -507,7 +507,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -523,8 +523,8 @@ "lean_bench_version": "0.1.0", "export_schema_version": 1, "env": - {"timestamp_unix_ms": 1782993257811, - "timestamp_iso": "2026-07-02T11:54:17Z", + {"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", @@ -532,7 +532,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-ladder.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-ladder.json similarity index 67% rename from reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-ladder.json rename to reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-ladder.json index 264c1da9e..63680ad03 100644 --- a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-ladder.json +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-ladder.json @@ -5,46 +5,43 @@ [{"relative_spread": 0, "param": 1, "ok_count": 1, - "min_per_call_nanos": 36752.421387, - "median_per_call_nanos": 36752.421387, - "max_per_call_nanos": 36752.421387}, + "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": 134775.146484, - "median_per_call_nanos": 134775.146484, - "max_per_call_nanos": 134775.146484}, + "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": 1616261.078125, - "median_per_call_nanos": 1616261.078125, - "max_per_call_nanos": 1616261.078125}, + "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": 17351416.5, - "median_per_call_nanos": 17351416.5, - "max_per_call_nanos": 17351416.5}, + "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": 354438875, - "median_per_call_nanos": 354438875, - "max_per_call_nanos": 354438875}], - "spawn_floor_nanos": 34539666, + "min_per_call_nanos": 327059916, + "median_per_call_nanos": 327059916, + "max_per_call_nanos": 327059916}], + "spawn_floor_nanos": 29923958, "slope": null, "ratios": - [[2, 44925.048828], - [3, 404065.269531], - [4, 3470283.3], - [5, 59073145.833333]], + [[2, 33629.374024], [3, 100947.549805], [4, 66423.950195], [5, 4990.538269]], "points": [{"trial_index": 0, - "total_nanos": 75268959, + "total_nanos": 73926459, "status": "ok", "result_hash": "0x7a04d2ad549a6dd3", - "per_call_nanos": 36752.421387, + "per_call_nanos": 36096.903809, "peak_rss_kb": null, "part_of_verdict": true, "param": 1, @@ -53,10 +50,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 69004875, + "total_nanos": 68872958, "status": "ok", "result_hash": "0x37ffee7fa6956231", - "per_call_nanos": 134775.146484, + "per_call_nanos": 134517.496094, "peak_rss_kb": null, "part_of_verdict": true, "param": 2, @@ -65,10 +62,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 103440709, + "total_nanos": 103370291, "status": "ok", "result_hash": "0xfd5a821e013bc945", - "per_call_nanos": 1616261.078125, + "per_call_nanos": 1615160.796875, "peak_rss_kb": null, "part_of_verdict": true, "param": 3, @@ -77,10 +74,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 69405666, + "total_nanos": 68018125, "status": "ok", "result_hash": "0x36f82522fa530950", - "per_call_nanos": 17351416.5, + "per_call_nanos": 17004531.25, "peak_rss_kb": null, "part_of_verdict": true, "param": 4, @@ -89,10 +86,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 354438875, + "total_nanos": 327059916, "status": "ok", "result_hash": "0xd79637486bd0e8f1", - "per_call_nanos": 354438875, + "per_call_nanos": 327059916, "peak_rss_kb": null, "part_of_verdict": true, "param": 5, @@ -105,8 +102,8 @@ "function": "Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerLadderChecksum", "env": - {"timestamp_unix_ms": 1782993220961, - "timestamp_iso": "2026-07-02T11:53:40Z", + {"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", @@ -114,7 +111,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -131,16 +128,16 @@ "narrow_range_noise_floor": 1.5, "max_seconds_per_call": 30, "cache_mode": "warm"}, - "complexity_formula": "k + 1", - "c_min": 44925.048828, - "c_max": 59073145.833333, + "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": 1782993220961, - "timestamp_iso": "2026-07-02T11:53:40Z", + {"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", @@ -148,7 +145,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-pair.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-pair.json similarity index 67% rename from reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-pair.json rename to reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-pair.json index 082b23a66..223d7d009 100644 --- a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd-pair.json +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd-pair.json @@ -5,46 +5,46 @@ [{"relative_spread": 0, "param": 1, "ok_count": 1, - "min_per_call_nanos": 226606.605469, - "median_per_call_nanos": 226606.605469, - "max_per_call_nanos": 226606.605469}, + "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": 1483320.3125, - "median_per_call_nanos": 1483320.3125, - "max_per_call_nanos": 1483320.3125}, + "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": 25741156.25, - "median_per_call_nanos": 25741156.25, - "max_per_call_nanos": 25741156.25}, + "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": 260786750, - "median_per_call_nanos": 260786750, - "max_per_call_nanos": 260786750}, + "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": 16709169583, - "median_per_call_nanos": 16709169583, - "max_per_call_nanos": 16709169583}], - "spawn_floor_nanos": 41442208, + "min_per_call_nanos": 15924779834, + "median_per_call_nanos": 15924779834, + "max_per_call_nanos": 15924779834}], + "spawn_floor_nanos": 30197458, "slope": null, "ratios": - [[2, 494440.104167], - [3, 6435289.0625], - [4, 52157350], - [5, 2784861597.166667]], + [[2, 366599.121094], + [3, 1551577.46875], + [4, 994593.097656], + [5, 242992.856354]], "points": [{"trial_index": 0, - "total_nanos": 58011291, + "total_nanos": 52380667, "status": "ok", "result_hash": "0xe0c054166fe7ff22", - "per_call_nanos": 226606.605469, + "per_call_nanos": 204611.980469, "peak_rss_kb": null, "part_of_verdict": true, "param": 1, @@ -53,10 +53,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 94932500, + "total_nanos": 93849375, "status": "ok", "result_hash": "0x91a910093667deb", - "per_call_nanos": 1483320.3125, + "per_call_nanos": 1466396.484375, "peak_rss_kb": null, "part_of_verdict": true, "param": 2, @@ -65,10 +65,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 102964625, + "total_nanos": 99300958, "status": "ok", "result_hash": "0xe662c5d3f8bd82a4", - "per_call_nanos": 25741156.25, + "per_call_nanos": 24825239.5, "peak_rss_kb": null, "part_of_verdict": true, "param": 3, @@ -77,10 +77,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 260786750, + "total_nanos": 254615833, "status": "ok", "result_hash": "0x28afc4e530363597", - "per_call_nanos": 260786750, + "per_call_nanos": 254615833, "peak_rss_kb": null, "part_of_verdict": true, "param": 4, @@ -89,10 +89,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 16709169583, + "total_nanos": 15924779834, "status": "ok", "result_hash": "0x6a608009af52d72d", - "per_call_nanos": 16709169583, + "per_call_nanos": 15924779834, "peak_rss_kb": null, "part_of_verdict": true, "param": 5, @@ -105,8 +105,8 @@ "function": "Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerPairChecksum", "env": - {"timestamp_unix_ms": 1782993222227, - "timestamp_iso": "2026-07-02T11:53:42Z", + {"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", @@ -114,7 +114,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -131,16 +131,16 @@ "narrow_range_noise_floor": 1.5, "max_seconds_per_call": 60, "cache_mode": "warm"}, - "complexity_formula": "k + 1", - "c_min": 494440.104167, - "c_max": 2784861597.166667, + "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": 1782993222227, - "timestamp_iso": "2026-07-02T11:53:42Z", + {"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", @@ -148,7 +148,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, diff --git a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd4-blocks.json b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd4-blocks.json similarity index 68% rename from reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd4-blocks.json rename to reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd4-blocks.json index 10859e091..25bc3ae10 100644 --- a/reports/bench-results/hex-berlekamp-zassenhaus-7da4747e-sd4-blocks.json +++ b/reports/bench-results/hex-berlekamp-zassenhaus-5ec8d8b5-sd4-blocks.json @@ -5,36 +5,36 @@ [{"relative_spread": 0, "param": 1, "ok_count": 1, - "min_per_call_nanos": 17205302.25, - "median_per_call_nanos": 17205302.25, - "max_per_call_nanos": 17205302.25}, + "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": 262806250, - "median_per_call_nanos": 262806250, - "max_per_call_nanos": 262806250}, + "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": 3360426833, - "median_per_call_nanos": 3360426833, - "max_per_call_nanos": 3360426833}, + "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": 14018191917, - "median_per_call_nanos": 14018191917, - "max_per_call_nanos": 14018191917}], - "spawn_floor_nanos": 31220541, + "min_per_call_nanos": 13659442584, + "median_per_call_nanos": 13659442584, + "max_per_call_nanos": 13659442584}], + "spawn_floor_nanos": 30551459, "slope": null, - "ratios": [[2, 87602083.333333], [3, 840106708.25], [4, 2803638383.4]], + "ratios": [[2, 3872.496277], [3, 200.941655], [4, 3.180337]], "points": [{"trial_index": 0, - "total_nanos": 68821209, + "total_nanos": 68037500, "status": "ok", "result_hash": "0x36f82522fa530950", - "per_call_nanos": 17205302.25, + "per_call_nanos": 17009375, "peak_rss_kb": null, "part_of_verdict": true, "param": 1, @@ -43,10 +43,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 262806250, + "total_nanos": 253787916, "status": "ok", "result_hash": "0x28afc4e530363597", - "per_call_nanos": 262806250, + "per_call_nanos": 253787916, "peak_rss_kb": null, "part_of_verdict": true, "param": 2, @@ -55,10 +55,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 3360426833, + "total_nanos": 3371241542, "status": "ok", "result_hash": "0x6c60e1792f37236e", - "per_call_nanos": 3360426833, + "per_call_nanos": 3371241542, "peak_rss_kb": null, "part_of_verdict": true, "param": 3, @@ -67,10 +67,10 @@ "below_signal_floor": false, "alloc_bytes": null}, {"trial_index": 0, - "total_nanos": 14018191917, + "total_nanos": 13659442584, "status": "ok", "result_hash": "0xbfade8ca2e42228c", - "per_call_nanos": 14018191917, + "per_call_nanos": 13659442584, "peak_rss_kb": null, "part_of_verdict": true, "param": 4, @@ -83,8 +83,8 @@ "function": "Hex.BerlekampZassenhausBench.runFactorAdvSwinnertonDyerSD4BlocksChecksum", "env": - {"timestamp_unix_ms": 1782993239823, - "timestamp_iso": "2026-07-02T11:53:59Z", + {"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", @@ -92,7 +92,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, @@ -109,16 +109,16 @@ "narrow_range_noise_floor": 1.5, "max_seconds_per_call": 120, "cache_mode": "warm"}, - "complexity_formula": "m + 1", - "c_min": 87602083.333333, - "c_max": 2803638383.4, + "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": 1782993239823, - "timestamp_iso": "2026-07-02T11:53:59Z", + {"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", @@ -126,7 +126,7 @@ "lean_bench_version": "0.1.0", "hostname": "carica", "git_dirty": false, - "git_commit": "7da4747e34da141d610ff7bcb6911bd38e5a4c21", + "git_commit": "5ec8d8b57e5e0671351346dd9bf36b160b1b535b", "exe_name": "hexbz_bench", "cpu_model": null, "cpu_cores": null, diff --git a/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg b/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg index 368f5ed7b..553521ee7 100644 --- a/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg +++ b/reports/figures/hex-berlekamp-zassenhaus-sd-ladder.svg @@ -662,8 +662,8 @@ z - @@ -673,12 +673,12 @@ L -3.5 0 " style="stroke: #000000; stroke-width: 0.8"/> - + - + - - + - + @@ -762,18 +762,18 @@ L 450 192.554002 - - + - + @@ -783,18 +783,18 @@ L 450 158.422329 - - + - + @@ -804,18 +804,18 @@ L 450 124.290656 - - + - + @@ -825,18 +825,18 @@ L 450 90.158984 - - + - + @@ -846,8 +846,8 @@ L 450 56.027311 - @@ -857,643 +857,631 @@ L -2 0 " style="stroke: #000000; stroke-width: 0.6"/> - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - - - - - - - - - - + @@ -1638,11 +1626,11 @@ z - - + @@ -1659,17 +1647,17 @@ z " style="stroke: #1f77b4"/> - - - - + + + + - - + - - - + + + - + - - - - + + + + @@ -1912,7 +1900,7 @@ Q 60.015346 68.8275 61.615346 68.8275 z " style="fill: #ffffff; opacity: 0.8; stroke: #cccccc; stroke-linejoin: miter"/> - + - + - + - @@ -650,12 +650,12 @@ L -3.5 0 " style="stroke: #000000; stroke-width: 0.8"/> - + - + - - + - + @@ -709,18 +709,18 @@ L 450 218.738685 - - + - + @@ -730,18 +730,18 @@ L 450 185.976086 - - + - + @@ -751,18 +751,18 @@ L 450 153.213486 - - + - + @@ -772,18 +772,18 @@ L 450 120.450886 - - + - + @@ -792,18 +792,18 @@ L 450 87.688286 - - + - + @@ -812,8 +812,8 @@ L 450 54.925686 - @@ -823,667 +823,655 @@ L -2 0 " style="stroke: #000000; stroke-width: 0.6"/> - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - - - - - - - - - - - + @@ -1645,12 +1633,12 @@ z - - + - - - - - + + + + + - - + - - - + + + - + - - - - + + + + - - + - + @@ -1746,7 +1734,7 @@ L 450 26.664 - + - + @@ -1806,7 +1794,7 @@ z - + - + - + - + - + - @@ -743,12 +743,12 @@ L -3.5 0 " style="stroke: #000000; stroke-width: 0.8"/> - + - + - - + - + @@ -809,18 +809,18 @@ L 450 181.842727 - - + - + @@ -830,18 +830,18 @@ L 450 138.97145 - - + - + @@ -850,18 +850,18 @@ L 450 96.100173 - - + - + @@ -870,8 +870,8 @@ L 450 53.228896 - @@ -881,487 +881,487 @@ L -2 0 " style="stroke: #000000; stroke-width: 0.6"/> - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + - - + @@ -1464,9 +1464,9 @@ z - @@ -1483,17 +1483,17 @@ z " style="stroke: #1f77b4"/> - - - + + + - - - - - + + + + - - - + + + @@ -1557,7 +1557,7 @@ L 450 36.9105 - + - + 120 s (killed)** | 8.575 ms | **lattice** | -| blocks m=1 | 16 | 17.21 ms | 10.64 ms | 0.299 ms | classical | -| blocks m=2 | 32 | 262.8 ms | 23.38 ms | 1.430 ms | classical | -| blocks m=3 | 48 | 3.360 s | 406.0 ms | 3.664 ms | lattice | -| blocks m=4 | 64 | 14.02 s | 4.610 s | 8.091 ms | lattice | +| `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: @@ -565,13 +568,13 @@ 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 (hex/Isabelle ≈ 1.6 at SD4, ≈ 10 at SD5 and -blocks m=3, ≈ 3–4 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: +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