diff --git a/research/paired26-integer-dot-replay/README.md b/research/paired26-integer-dot-replay/README.md new file mode 100644 index 0000000000..8d3f6c5a9a --- /dev/null +++ b/research/paired26-integer-dot-replay/README.md @@ -0,0 +1,177 @@ +# Faster complete paired26 replay with integer dot products + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped implementation-equivalence proof, exact finite conformance +and local performance evidence. The complete primary command from +[Andrey Mas / an664's PR1624](https://github.com/CrocSwap/integer-mult-bounds/pull/1624) +takes **33.77% less median wall time locally**, from 0.628150 s to 0.415995 s. +Nine fresh-process pairs alternate their execution order. All eighteen commands +succeed with identical complete stdout and zero failures. Discovery stopped at +the first verified improvement. This is new implementation work. The predecessor's +decoder minimum and classification are cited results, not audit deliverables. + +## Exact change and proof + +The frozen source and certificate remain unchanged. `replay.py` authenticates +both SHA256 pins before executing the exact source bytes, then replaces only +its eight-coordinate rational `dot`. It runs the original default entry point, +including every mathematical check and rejection control. The accelerated +command accepts no arguments and cannot select the certificate-writing option. +It imports no predecessor bytecode. + +For an integer/Fraction row v, let q(v) be the positive least common multiple +of its reduced denominators, and put +n(v)[i] = numerator(v[i]) q(v) / denominator(v[i]). Then + +```text +sum_i v[i] w[i] = sum_i n(v)[i] n(w)[i] / (q(v) q(w)). +``` + +Python integer arithmetic is exact. One final Fraction reduction replaces the +repeated rational products and additions. Integer-only inputs return an integer, +matching the original type. Other widths/types use the original function, +including its shape-error behavior. + +Row conversion is reused only for the identical container with all eight scalar +objects identical to its saved snapshot. Built-in integers and Fractions are +immutable. Mutating a row therefore causes conversion again, including a change +from an integer to an equal Fraction. Cached entries retain their owners, so +object IDs cannot be recycled while cached. At most 1,024 rows are cached; +capacity clearing changes only conversion work. No dot-product result is cached. +Every call still computes all eight products and their sum. + +## Conformance evidence + +The new verifier compares all **189,904 reached dot values and exact types** +with the original throughout the complete primary computation. Both complete +computed certificates agree and pass the original strict comparison against the +saved certificate. Its canonical computed-certificate SHA256 is +`f975a374d2d0ce6346ae4eaf053dfd049185fdf2dfe731f1b175de77e99e5fc1`. +The new route performs 12,369 conversions, 367,439 row-cache hits and twelve +capacity clears, with zero reached fallbacks. Both routes retain the fourteen +original rejection controls and two additional complex controls. + +Additional conformance covers 65,536 rational vector pairs, ten fallback widths, +three fallback types, five in-place mutations and 2,049 capacity inputs. Eight +rejecting controls cover two bad shapes, both source pins, a wrong denominator, +wrong integer numerators, an oversized source and the writer option. Explicit +exceptions remain active under `-O`. +The unchanged default workload still includes all 511 functional records, +1,716 subsets, four decoder examples, full all-pairs identities, actual support +ranks and complete saved-certificate comparison. The separate predecessor +`audit.py` is unchanged and outside this optimization. + +## Local timing evidence + +CPython 3.12.15, macOS 27.0.1 arm64, eighteen logical CPUs. The load average +near the run was 1.76, 2.16, 2.11. Other applications remained active. Runs were +serial and alternating. Both commands use `-I -W error -B`, identical source and +certificate bytes and the same interpreter. Every timed region includes fresh +process startup and the complete default replay/certificate comparison. The new +route also includes authentication and cache initialization. + +| Pair | Original seconds | Integer seconds | +|---:|---:|---:| +| 1 | 0.620465667 | 0.415328333 | +| 2 | 0.634360125 | 0.568668250 | +| 3 | 0.621159000 | 0.418008917 | +| 4 | 0.627842541 | 0.415584500 | +| 5 | 0.630763416 | 0.418947291 | +| 6 | 0.624511541 | 0.412711708 | +| 7 | 0.634765208 | 0.415995042 | +| 8 | 0.631476833 | 0.416269375 | +| 9 | 0.628149917 | 0.415403291 | + +The ranges are 0.620465667 to 0.634765208 s and 0.412711708 to 0.568668250 s. +Every pair improves, including the slower second candidate run. Complete stdout +SHA256 is +`81d9b07342fe4de43ffa4acc83a5a33afedefd11939410d2d3d7be07edd8f10b`. +These are local observations, not a portable speed guarantee or CI timing claim. + +An untimed discovery profile places 2.015 of 2.474 profiled seconds in `dot`, +with Fraction multiplication/addition dominating. The saving is below that +81.45% share. An untimed candidate profile leaves 0.817 of 1.357 profiled seconds +in the replacement dot, including 0.487 s in row conversion/snapshot checking. +Profiles are excluded from wall-time reporting. Final Fraction construction and +all unchanged certificate work remain. There is no cached certificate or early +acceptance. + +## Reproduction + +From the repository root, standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/paired26-integer-dot-replay/replay.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/paired26-integer-dot-replay/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/paired26-integer-dot-replay/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/paired26-integer-dot-replay +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/paired26-integer-dot-replay --check-source-history +``` + +Any CPython 3.12 executable can replace the displayed path. Expected markers +are the unchanged `PASS_FIXED_PAIRED26_MINIMUM_62`, `PASS_PAIRED26_INTEGER_DOT`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +For timings, run `benchmark.py --pairs 9 --output /absolute/fresh/outside.json` +with that interpreter and flags. `verify.py --receipt /absolute/fresh/outside.json` +generates a hash-bound receipt. Default replay writes no artifacts. + +## Sources, scope and limitations + +Base main is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +[TASK.json](TASK.json) refines replay-runtime to one complete default command. +[SOURCES.json](SOURCES.json) pins exact inputs and provenance. Both input files +are declared in [VERIFY.json](VERIFY.json) for CI invalidation; any byte change +fails the adapter's hash boundary before source execution. + +Credit Andrey Mas / an664 / PR1624 for the original proof, program and +certificate; woklerx / PR1020 and PR1077 for the puncture, first pair and prior +decoder; Hanson Sun / bbMisk / PR1521 for the completion question; +themilkman216 / PR968 and DreamingOfClouds / PR717 for the geometry/billing model; +and the retained E8 lineage. Josie Elliston's PR1663 is a separate mathematical +audit, cited as prior work rather than replayed here. Common-denominator +arithmetic and caching are standard. The new result is the source-bound adapter, +equivalence contract and measured complete-command saving. + +Earlier exact-arithmetic implementations include Ali Romman's +[PR5002](https://github.com/CrocSwap/integer-mult-bounds/pull/5002) and Nick +Petalas's [PR6272](https://github.com/CrocSwap/integer-mult-bounds/pull/6272) +and [PR6281](https://github.com/CrocSwap/integer-mult-bounds/pull/6281). +They already use denominator clearing on other complete commands. This adapter's +specific contract reuses scalar-row normalization across calls while detecting +in-place mutations, and preserves the complete scalar value and return type. +Those earlier product implementations are not imported or extended here. + +No new decoder optimum, physical supplier, kappa, selected-frontier change, +complete multiplication theorem, independent human review or formal proof-kernel +acceptance is claimed. All five inherited framework assumptions remain. +No Lean, Docker, selected cold replay or separate predecessor audit was run. + +Local registered normal and optimized conformance commands passed in 1.870 s +and 1.953 s respectively, below their sixty-second timeouts. The package +metadata/registered replay passed. Publication-byte/source-history and exported +standalone checks are recorded in the PR body after the publication commit. +Hosted CI is pending at initial publication. + +Power of Ten inspection bounds numerical loops by eight coordinates, 1,024 +cached rows, the fixed test corpus, at most fifteen timing pairs and a 30-second +subprocess timeout. Functions stay below sixty lines. Source reads are capped +at 1 MiB. Source pins, arithmetic equality, capacity and full fixture coverage +are checked with exceptions. Python integer/Fraction allocation is a managed +runtime deviation from fixed allocation. Live cached collections are bounded; +allocator internals and arbitrary external scalar bit lengths are not measured. +Executing authenticated source and replacing its `dot` callable are explicit +deviations from static dispatch/metaprogramming restrictions, constrained to +one SHA256-pinned module and one function. The inherited verifier stays frozen. +A native fixed-allocation implementation and separate static analyzer are not +supplied. Warning-strict normal/optimized execution and AST inspection are used. + +## Open next questions + +Can the same representation improve another named complete rational replay? +Profile that command first, then authenticate its sources and check all reached +widths, scalar types, mutation behavior and output. Different denominators and +mutation patterns require new evidence. Neither the percentage nor this +conformance certificate transfers automatically. This follow-on is unclaimed. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371170). diff --git a/research/paired26-integer-dot-replay/SOURCES.json b/research/paired26-integer-dot-replay/SOURCES.json new file mode 100644 index 0000000000..ca46de3f16 --- /dev/null +++ b/research/paired26-integer-dot-replay/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/complex-paired26-completion/certificate.json", + "usage": "input", + "git_blob": "5d6d2095b6536595ffd2999124636a9f45c90192", + "sha256": "18103be5548d9558dfc49cc90bc9308aab13e48e7f99d30a45fd90cec7c2776d" + }, + { + "path": "research/complex-paired26-completion/verify.py", + "usage": "input", + "git_blob": "f59630a3261c914b65af6ed9e2d19a43ac9ba522", + "sha256": "34f20844f5184a66f2217b481c0cc82ed6a9eb85e97d3ec53eec36b641d2b07d" + }, + { + "path": "research/complex-paired26-completion/README.md", + "usage": "provenance", + "git_blob": "6712df1150d88a8b5ecc51871e8919fac93766e3", + "sha256": "ba2ebeb515190b7279ee490cd2ed450c9a48e91a22602ac7e384b9840367c0bc" + }, + { + "path": "research/complex-paired26-completion/ATTRIBUTION.md", + "usage": "provenance", + "git_blob": "bcac7c7d87574e88a3b2b1884964d8235606a415", + "sha256": "30c8dfdf13e5b3026e26ecb36288546eebe21f89a3075dc39c236baa09d7307d" + }, + { + "path": "research/complex-paired26-completion/proof.md", + "usage": "provenance", + "git_blob": "4a89efa74126836857c73fddc48147b0446ec4d7", + "sha256": "0305c955d39a0b11b9e3a3b58606882ceb85daac765050583645765c7a35fad3" + }, + { + "path": "research/complex-paired26-completion/audit.py", + "usage": "provenance", + "git_blob": "80c5269ed29c9f73d1e0b8819e612d907e3b211b", + "sha256": "5e39772867f69faaf95c4a9b429129485c462f1daedc1ce5b311dd542a5cb535" + }, + { + "path": "research/complex-paired26-completion/LICENSE", + "usage": "provenance", + "git_blob": "d645695673349e3947e8e5ae42332d0ac3164cd7", + "sha256": "cfc7749b96f63bd31c3c42b5c471bf756814053e847c10f3eb003417bc523d30" + } + ] +} diff --git a/research/paired26-integer-dot-replay/TASK.json b/research/paired26-integer-dot-replay/TASK.json new file mode 100644 index 0000000000..bf6c298b4f --- /dev/null +++ b/research/paired26-integer-dot-replay/TASK.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Accelerate the complete default primary command of PR1624 by exact common-denominator integer dot products, preserving every reached dot value/type, complete certificate and original rejection control.", + "scope_change_reason": "One source-bound fixture and one measured arithmetic bottleneck refine the replay-runtime card. This is implementation work, not a mathematical audit of PR1624.", + "bottleneck_link": "Faster complete exact replays reduce the cost of checking construction candidates; no kappa or supplier improvement is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified end-to-end improvement. At most two implementation candidates; no expansion of the predecessor theorem.", + "outcome": "completed", + "evidence": "Nine alternating fresh-process pairs: medians 0.628149917 s and 0.415995042 s, 33.774561% less wall time. Complete stdout equal with zero failures. Full conformance compares 189904 reached dot values/types and both complete certificates; 65536 rational cases, mutation/capacity/fallback controls and eight rejecting controls pass.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the same integer-row representation improve another named complete rational replay?", + "why_it_matters": "Exact arithmetic replay can dominate the cost of screening new constructions.", + "first_step": "Profile that complete command and enumerate its reached widths/types before choosing a bounded adapter.", + "blocked_by": "Different mutation patterns, denominator growth and output contracts need new source-bound conformance and timing evidence." + } + ] +} diff --git a/research/paired26-integer-dot-replay/VERIFY.json b/research/paired26-integer-dot-replay/VERIFY.json new file mode 100644 index 0000000000..830e309b14 --- /dev/null +++ b/research/paired26-integer-dot-replay/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-paired26-completion/certificate.json", + "research/complex-paired26-completion/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Compare all 189904 reached dot values and types, both complete certificates and the stored certificate; retain 14 original plus 2 complex controls; 65536 rational pairs, mutation/capacity/fallback and eight rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Compare all 189904 reached dot values and types, both complete certificates and the stored certificate; retain 14 original plus 2 complex controls; 65536 rational pairs, mutation/capacity/fallback and eight rejecting controls." + } + ] +} diff --git a/research/paired26-integer-dot-replay/benchmark.py b/research/paired26-integer-dot-replay/benchmark.py new file mode 100644 index 0000000000..bbe7c376bc --- /dev/null +++ b/research/paired26-integer-dot-replay/benchmark.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Alternate complete fresh-process commands; timings are local evidence.""" +from __future__ import annotations + +import argparse +import hashlib +import json +import platform +import statistics +import subprocess +import sys +import time +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def timed(script: Path) -> tuple[float, bytes]: + command = [sys.executable, "-I", "-W", "error", "-B", str(script)] + started = time.perf_counter_ns() + process = subprocess.run(command, cwd=ROOT, capture_output=True, timeout=30) + elapsed = (time.perf_counter_ns() - started) / 1_000_000_000 + if process.returncode or process.stderr: + raise RuntimeError("failed benchmark command: " + repr(process)) + if not process.stdout.startswith(b"PASS_FIXED_PAIRED26_MINIMUM_62\n"): + raise RuntimeError("complete success output absent") + return elapsed, process.stdout + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--pairs", type=int, default=9, choices=range(5, 16)) + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + if args.output.resolve().is_relative_to(ROOT): + raise ValueError("benchmark output must be outside checkout") + scripts = {"original": ROOT / "research/complex-paired26-completion/verify.py", + "integer": PACKAGE / "replay.py"} + rows, expected = [], None + for pair in range(args.pairs): + order = ("original", "integer") if pair % 2 == 0 else ("integer", "original") + row = {} + for engine in order: + elapsed, output = timed(scripts[engine]) + if expected is None: + expected = output + if output != expected: + raise RuntimeError("complete stdout disagreement") + row[engine] = elapsed + rows.append(row) + medians = {name: statistics.median(row[name] for row in rows) for name in scripts} + report = {"python": sys.version, "platform": platform.platform(), + "executable": sys.executable, "pairs": rows, "medians": medians, + "ranges": {name: [min(r[name] for r in rows), max(r[name] for r in rows)] + for name in scripts}, "failures": 0, + "stdout_sha256": hashlib.sha256(expected).hexdigest(), + "reduction_percent": 100 * (1 - medians["integer"] / medians["original"])} + inputs = [*scripts.values(), ROOT / "research/complex-paired26-completion/certificate.json"] + report["sha256"] = {str(path.relative_to(ROOT)): hashlib.sha256(path.read_bytes()).hexdigest() + for path in inputs} + with args.output.open("x", encoding="utf-8") as stream: + json.dump(report, stream, indent=2, sort_keys=True) + stream.write("\n") + print(json.dumps(report, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/paired26-integer-dot-replay/replay.py b/research/paired26-integer-dot-replay/replay.py new file mode 100644 index 0000000000..b2875eead4 --- /dev/null +++ b/research/paired26-integer-dot-replay/replay.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Run the frozen paired26 primary replay with exact integer dot products. + +Produced by Nick Petalas. The loaded verifier and its result retain Andrey +Mas's and the predecessor authors' credit. Only ``dot`` is replaced. +""" +from __future__ import annotations + +import hashlib +import sys +from dataclasses import dataclass +from fractions import Fraction +from math import lcm +from pathlib import Path +from types import ModuleType +from typing import Callable, Sequence + +SOURCE_DIRECTORY = Path("research/complex-paired26-completion") +SOURCE_HASHES = { + "verify.py": "34f20844f5184a66f2217b481c0cc82ed6a9eb85e97d3ec53eec36b641d2b07d", + "certificate.json": "18103be5548d9558dfc49cc90bc9308aab13e48e7f99d30a45fd90cec7c2776d", +} +MAX_INPUT_BYTES = 1 << 20 +MAX_CACHE_ROWS = 1024 +Scalar = int | Fraction + + +@dataclass(frozen=True) +class IntegerRow: + owner: Sequence[Scalar] + snapshot: tuple[Scalar, ...] + numerators: tuple[int, ...] + denominator: int + fractional: bool + + +class IntegerDot: + """Cache immutable scalar identities, never a dot-product result.""" + + def __init__(self, original: Callable): + self.original = original + self.rows: dict[int, IntegerRow] = {} + self.calls = 0 + self.hits = 0 + self.misses = 0 + self.clears = 0 + self.fallbacks = 0 + + def row(self, values: Sequence[Scalar]) -> IntegerRow | None: + saved = self.rows.get(id(values)) + if (saved is not None and saved.owner is values + and all(x is y for x, y in zip(values, saved.snapshot))): + self.hits += 1 + return saved + if any(type(x) not in (int, Fraction) for x in values): + return None + denominator = lcm(*(x.denominator for x in values)) + numerators = tuple(x.numerator * (denominator // x.denominator) + for x in values) + saved = IntegerRow(values, tuple(values), numerators, denominator, + any(type(x) is Fraction for x in values)) + if len(self.rows) == MAX_CACHE_ROWS: + self.rows.clear() + self.clears += 1 + self.rows[id(values)] = saved + self.misses += 1 + return saved + + def __call__(self, a: Sequence[Scalar], b: Sequence[Scalar]) -> Scalar: + self.calls += 1 + if len(a) != 8 or len(b) != 8: + self.fallbacks += 1 + return self.original(a, b) + left, right = self.row(a), self.row(b) + if left is None or right is None: + self.fallbacks += 1 + return self.original(a, b) + numerator = sum(x * y for x, y in zip(left.numerators, right.numerators)) + if left.fractional or right.fractional: + return Fraction(numerator, left.denominator * right.denominator) + return numerator + + +def checked_bytes(directory: Path, filename: str, expected: str) -> bytes: + path = directory / filename + with path.open("rb") as stream: + raw = stream.read(MAX_INPUT_BYTES + 1) + if len(raw) > MAX_INPUT_BYTES: + raise ValueError("source size limit: " + filename) + if hashlib.sha256(raw).hexdigest() != expected: + raise ValueError("source hash mismatch: " + filename) + return raw + + +def load_source(directory: Path | None = None) -> ModuleType: + if directory is None: + directory = Path(__file__).resolve().parents[2] / SOURCE_DIRECTORY + raw = {name: checked_bytes(directory, name, digest) + for name, digest in SOURCE_HASHES.items()} + module = ModuleType("paired26_frozen_primary") + module.__file__ = str(directory / "verify.py") + # Execute the bytes just authenticated, without importing any cached pyc. + exec(compile(raw["verify.py"], module.__file__, "exec"), module.__dict__) + return module + + +def main() -> int: + if len(sys.argv) != 1: + raise ValueError("accelerated replay accepts no arguments") + module = load_source() + module.dot = IntegerDot(module.dot) + return module.main([]) + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/paired26-integer-dot-replay/verify.py b/research/paired26-integer-dot-replay/verify.py new file mode 100644 index 0000000000..7cb870eb98 --- /dev/null +++ b/research/paired26-integer-dot-replay/verify.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check the new adapter, not the predecessor's universal decoder theorem.""" +from __future__ import annotations + +import argparse +import hashlib +import json +import sys +from dataclasses import replace +from fractions import Fraction as Q +from itertools import product +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +import replay as adapter +from replay import IntegerDot, MAX_CACHE_ROWS, SOURCE_HASHES, load_source + + +def need(ok: bool, message: str) -> None: + if not ok: + raise RuntimeError(message) + + +def equal_call(candidate, original, a, b) -> None: + expected = original(a, b) + actual = candidate(a, b) + need(actual == expected and type(actual) is type(expected), "dot mismatch") + + +def arithmetic_controls(original) -> dict: + candidate = IntegerDot(original) + values = (-1, 0, Q(1, 2), Q(2, 3)) + vectors = [list(row) + [0, 1, -1, Q(3, 5)] + for row in product(values, repeat=4)] + cases = 0 + for a in vectors: + for b in vectors: + equal_call(candidate, original, a, b) + cases += 1 + for width in range(10): + equal_call(candidate, original, [Q(1, 7)] * width, [3] * width) + for scalar in (True, 0.25, 2 + 3j): + equal_call(candidate, original, [scalar] * 8, [1] * 8) + return {"rational_pairs": cases, "fallback_widths": 10, + "fallback_types": 3} + + +def cache_controls(original) -> dict: + candidate = IntegerDot(original) + a, b = [1] * 8, [2] * 8 + for changed in (9, Q(9), Q(1, 7), -3, 1): + equal_call(candidate, original, a, b) + a[0] = changed + equal_call(candidate, original, a, b) + for value in range(2 * MAX_CACHE_ROWS + 1): + equal_call(candidate, original, [value] + [0] * 7, b) + need(len(candidate.rows) <= MAX_CACHE_ROWS, "cache capacity") + need(candidate.clears >= 2, "capacity control did not clear cache") + before = candidate.calls + equal_call(candidate, original, a, b) + equal_call(candidate, original, a, b) + need(candidate.calls == before + 2, "dot result was cached") + return {"mutations": 5, "capacity_inputs": 2 * MAX_CACHE_ROWS + 1, + "clears": candidate.clears} + + +def rejection_controls(original) -> int: + rejected = 0 + candidate = IntegerDot(original) + for a, b in (([1], [1, 2]), ([1] * 8, [1] * 7)): + try: + candidate(a, b) + except RuntimeError as exc: + need(str(exc) == "dot-product shape mismatch", "shape error changed") + rejected += 1 + else: + raise RuntimeError("bad shape accepted") + for filename in SOURCE_HASHES: + previous = SOURCE_HASHES[filename] + try: + SOURCE_HASHES[filename] = "0" * 64 + try: + load_source() + except ValueError as exc: + need(str(exc) == "source hash mismatch: " + filename, + "wrong source rejection") + rejected += 1 + else: + raise RuntimeError("bad source pin accepted") + finally: + SOURCE_HASHES[filename] = previous + a, b = [Q(1, 3)] * 8, [Q(2, 5)] * 8 + for field, bad in (("denominator", 1), ("numerators", (0,) * 8)): + candidate = IntegerDot(original) + candidate(a, b) + candidate.rows[id(a)] = replace(candidate.rows[id(a)], **{field: bad}) + try: + equal_call(candidate, original, a, b) + except RuntimeError as exc: + need(str(exc) == "dot mismatch", "wrong mutant rejection") + rejected += 1 + else: + raise RuntimeError("incorrect arithmetic accepted") + return rejected + boundary_controls() + + +def boundary_controls() -> int: + previous_limit, previous_argv = adapter.MAX_INPUT_BYTES, sys.argv + rejected = 0 + try: + adapter.MAX_INPUT_BYTES = 8 + try: + load_source() + except ValueError as exc: + need(str(exc) == "source size limit: verify.py", "size boundary changed") + rejected += 1 + else: + raise RuntimeError("oversized source accepted") + sys.argv = ["replay.py", "--write-certificate"] + try: + adapter.main() + except ValueError as exc: + need(str(exc) == "accelerated replay accepts no arguments", "CLI boundary changed") + rejected += 1 + else: + raise RuntimeError("writer option accepted") + finally: + adapter.MAX_INPUT_BYTES, sys.argv = previous_limit, previous_argv + return rejected + + +def full_conformance() -> dict: + baseline = load_source() + expected = baseline.compute_certificate() + candidate = load_source() + original = candidate.dot + integer_dot = IntegerDot(original) + checked = 0 + + def compare(a, b): + nonlocal checked + want, got = original(a, b), integer_dot(a, b) + need(want == got and type(want) is type(got), "reached dot mismatch") + checked += 1 + return got + + candidate.dot = compare + actual = candidate.compute_certificate() + need(actual == expected, "complete computed certificate differs") + saved = json.loads(Path(candidate.__file__).with_name("certificate.json").read_text()) + candidate.compare_certificate(saved, actual) + baseline.compare_certificate(saved, expected) + need(checked == integer_dot.calls == 189904, "reached dot coverage changed") + need(integer_dot.fallbacks == 0, "unexpected reached fallback") + encoded = json.dumps(actual, sort_keys=True, separators=(",", ":")).encode() + return {"checked_dot_calls": checked, "cache_hits": integer_dot.hits, + "row_conversions": integer_dot.misses, "cache_clears": integer_dot.clears, + "certificate_sha256": hashlib.sha256(encoded).hexdigest(), + "inherited_controls": len(actual["negative_controls"]["rejected"]), + "inherited_complex_controls": len(actual["negative_controls"] + ["additional_complex_controls"])} + + +def receipt(result: dict, destination: Path) -> None: + root = PACKAGE.parents[1] + if destination.resolve().is_relative_to(root): + raise ValueError("receipt must be outside the checkout") + paths = [PACKAGE / name for name in ("README.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "replay.py", "verify.py", + "benchmark.py")] + paths += [root / "research/complex-paired26-completion" / name + for name in sorted(SOURCE_HASHES)] + hashes = {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in paths} + with destination.open("x", encoding="utf-8") as stream: + json.dump({"result": result, "sha256": hashes}, stream, indent=2, sort_keys=True) + stream.write("\n") + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + original = load_source().dot + result = {"arithmetic": arithmetic_controls(original), + "cache": cache_controls(original), + "rejecting_controls": rejection_controls(original), + "full_conformance": full_conformance()} + if args.receipt is not None: + receipt(result, args.receipt) + print("PASS_PAIRED26_INTEGER_DOT " + json.dumps(result, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())