diff --git a/research/e8-root-swap-fast-inner/PROOF.md b/research/e8-root-swap-fast-inner/PROOF.md new file mode 100644 index 0000000000..c4f5340289 --- /dev/null +++ b/research/e8-root-swap-fast-inner/PROOF.md @@ -0,0 +1,49 @@ +# Exact substitution and retained checks + +This contribution was produced by Nick Petalas. Apache-2.0. + +For the default scientific command pinned in SOURCES.json, replacing +`verify.dot` and `extension_check.dot` by `replay.dot8` preserves the full +result and every rejection predicate. This is implementation equivalence, +not independent acceptance of the predecessor's mathematical conclusions. + +The two source dot functions receive eight-coordinate integer or rational +vectors. In the primary these are roots, normals, simple vectors and rows of +an eight-dimensional rational inverse. In the extension they are the same +doubled coordinate vectors, inverse rows and explicit eight-coordinate +fixtures. Frozen constructors and dimension checks fix this domain. Floating +point and overloaded scalar protocols are excluded. + +Put s_0=0 and s_(j+1)=s_j+a_j*b_j for j=0,...,7. The original generator/sum +computes s_8. The new expression has the same eight terms and left-associated +additions, starting with zero. Exact integer/Fraction arithmetic proves equality +by induction on j. The new length check succeeds on the admitted calls. +Substituting an equal pure function preserves callers' values, branches and +checks by induction over execution. No memoization, pruning, approximation or +fixture-dependent answer is introduced. The Cartan and Gaussian algebra +implementations are unchanged. + +The adapter authenticates all ten scientific inputs before compiling the four +original source modules at their original file locations. Compilation bypasses +adjacent bytecode caches. Import order is geometry, algebra, extension, primary. +The original default main executes, including the original full RESULT.json +comparison, and must return zero. Existing module objects, path and argument +lists are restored on exit. Stable files during execution are assumed, as in +the original source-hash check. Lean source bytes are authenticated because +they occur in that receipt, but Lean is not executed. + +Checked mode compares old and new results at all 5,096,623 substituted calls +in one complete execution. A separate 576-case set includes all 64 ordered +basis pairs and both orientations of 256 signed rational fixtures. Six wrong +lengths and one invalid mode reject. Ten physical source-byte mutations and +one missing file reject before compilation. A wrong-dot integration control +reaches the original root-norm failure and rejects the complete command. +These are nineteen controls. Module sentinels check namespace restoration. +Explicit exceptions retain checks under optimized Python. + +Performance is a local observation. Five alternating fresh-process pairs time +the original default CLI and new default CLI, including startup and output +capture. Every run must return zero, print the original success line and have +empty stderr. Input authentication before and after timing checks stability. +The generated report records every command, time and failure. It is not a +portable runtime bound, mathematical theorem or CI performance threshold. diff --git a/research/e8-root-swap-fast-inner/README.md b/research/e8-root-swap-fast-inner/README.md new file mode 100644 index 0000000000..d97cd70ee7 --- /dev/null +++ b/research/e8-root-swap-fast-inner/README.md @@ -0,0 +1,120 @@ +# Faster complete E8 root-swap replay + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +The new exact eight-coordinate dot product reduces the complete retained +[PR3166](https://github.com/CrocSwap/integer-mult-bounds/pull/3166) replay's +local median wall time by **13.95%**, from **6.131 s to 5.275 s**. Five +alternating fresh-process pairs execute the full scientific command on both +sides. All ten runs succeed with identical stdout and no stderr. Every +candidate run is faster than every baseline run in this sample. + +Claim type: scoped implementation-equivalence proof, exact finite conformance, +and local performance evidence. The decoder mathematics and its certificates +remain conorholds's contribution. No new kappa or scientific audit is claimed. + +`replay.py` authenticates ten scientific files, compiles the four original +modules from their authenticated bytes, replaces only the primary and +extension dot products, and calls the original main. The separate Cartan +implementation, Gaussian algebra, geometry, rejection controls, source hashes +and complete RESULT.json comparison remain active. Frozen files are unchanged. +[PROOF.md](PROOF.md) gives the substitution argument and scope. + +## Measured complete consumer + +CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs. Initial shared-host load +averages were 2.27, 2.58, 1.99. No other replay from this contribution ran during +timing; other contributors could use the machine. Both commands use +`-I -W error -B`, including startup, imports, every check and output capture. + +| Pair | Original, seconds | Specialized, seconds | +|---|---:|---:| +| 1 | 6.333281 | 5.110564 | +| 2 | 6.083976 | 5.607583 | +| 3 | 6.376638 | 5.199241 | +| 4 | 6.130820 | 5.275435 | +| 5 | 6.124533 | 5.409365 | +| Median | 6.130820 | 5.275435 | +| Range | 6.083976 to 6.376638 | 5.110564 to 5.607583 | + +The percentage uses nanosecond medians 6,130,819,750 and 5,275,434,583. +A separate baseline profile attributes 3.718 s of its 17.878 s instrumented +run to the two replaced dot functions. The measured saving is below that +20.8% share. Generator/sum overhead is the changed cost; the other checks +limit the saving. Profile seconds are not estimates of uninstrumented time. +This local result implies no runtime bound on another host or input. + +`benchmark.py` generates stdout evidence containing every command, elapsed +nanosecond count, return code, stdout digest and failure count. The table +transcribes that report. No timing receipt is hand-written. CI runs +conformance, not a performance threshold. + +## Reproduce + +From the repository root with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e8-root-swap-fast-inner/replay.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e8-root-swap-fast-inner/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/e8-root-swap-fast-inner/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/e8-root-swap-fast-inner/benchmark.py --pairs 5 +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-root-swap-fast-inner +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-root-swap-fast-inner --check-source-history +``` + +Another CPython 3.12 executable may replace the absolute path. Set `TMPDIR` +to a private external directory for temporary custody controls. The fast +command prints the unchanged source success line. The new verifier emits a +generated JSON receipt with `PASS_E8_ROOT_SWAP_FAST_INNER`, 5,096,623 exact +old/new dot comparisons, 576 scalar fixtures, nineteen controls and hashes of +all eight package files. Source mathematical check counts are inherited +coverage. Each registered normal/optimized command has a 120-second limit. +Benchmarking is optional and excluded from CI. + +## Sources and limits + +Canonical base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priorities revision 8. +The selected record resolves to PR6030, kappa .003125804. The card's first +binding control passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; this is +orientation only. TASK.json refines replay-runtime to this complete command. +SOURCES.json pins ten live scientific inputs and historical provenance. + +Credit conorholds / PR3166 for the original replay, proofs, checks and +certificates, and DreamingOfClouds / PR2816, PR2826, PR2862 and PR3154 with +their retained E8 lineage. Their files and notices are unchanged. Fixed-product +unrolling is standard. This contribution supplies its source-bound adaptation, +preservation argument and measured complete consumer. Nick Petalas / PR6164 +optimized publication-byte preflight using this package as a fixture; it did +not accelerate this scientific command. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370259) +states this scope. Main, merged and live PRs, recent account work, handoffs and +local reservations were checked. The overlap cache covered 506 open PRs and +6,501 Discussion records; sparse local-note coverage was incomplete. Arbitrary +historical diffs, unpublished work and literature priority remain outside coverage. + +Equivalence covers the pinned default command and exact integer/rational +eight-coordinate arguments. Arbitrary overloaded scalar types, receipt-emission +CLI options, arbitrary module-cache states and future source changes are +excluded. Lean source bytes are authenticated; Lean is not run. No native or +physical caller, precision, tape, stock, compiler, outer or selected cold replay, +new supplier or complete multiplication theorem is supplied. All five selected +framework assumptions and the selected frontier remain unchanged. + +New functions stay below sixty lines and have bounded fixture/module/input +loops and no recursion. Managed allocation is a Power of Ten rule 3 deviation +for this fixed workload and ten inputs capped at 1 MiB each. Authenticated +compilation of four unchanged modules is a rule 8 deviation; it generates no +new source. The two substitutions, comparison closure and source main are +fixed rule 9 dispatch targets. Frozen predecessor loop/function constraints +are retained. Warning-strict normal/optimized replay supplies the available +diagnostics; no separate static analyzer or real-time guarantee is claimed. + +## Open next questions + +1. Integrate into one maintained replay entry while retaining the checkers' + intended arithmetic independence. First identify the active consumer and + measure its full command. This adapter targets a historical fixture. +2. Profile that consumer's remaining bottleneck before another optimization. + The first verified improvement ends this contribution; no follow-up is reserved. diff --git a/research/e8-root-swap-fast-inner/SOURCES.json b/research/e8-root-swap-fast-inner/SOURCES.json new file mode 100644 index 0000000000..6cfa00d5d1 --- /dev/null +++ b/research/e8-root-swap-fast-inner/SOURCES.json @@ -0,0 +1,78 @@ +{ + "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/e8-d0-root-swaps/EXTENSION.md", + "usage": "input", + "git_blob": "99dc1c21b72e90e7669386d77506334900992286", + "sha256": "47f86fca33843bb2bc2b5ddbc07b91d846fe04952b8c133ff02dcbb9637b6357" + }, + { + "path": "research/e8-d0-root-swaps/PROOF.md", + "usage": "input", + "git_blob": "79051f9f431863259dd7d714e096ce9e865b151b", + "sha256": "531b1dcb0de5f652fa2ca8dca97174c4973face53c877bd919cf584afa632953" + }, + { + "path": "research/e8-d0-root-swaps/RESULT.json", + "usage": "input", + "git_blob": "e1a89572dc2e18b745655a562bbb8e9bece54a93", + "sha256": "d894b32076290b688d9838e9889989d837bacd378ba6b9654d25658a44661403" + }, + { + "path": "research/e8-d0-root-swaps/algebra_check.py", + "usage": "input", + "git_blob": "b108bbd226f895f4291002ec06613ed4b3e7faa4", + "sha256": "45dad6b59a4fad6d2ccf6c6d7f726e5f9813f03e9ff1f33e84107797ca7bc040" + }, + { + "path": "research/e8-d0-root-swaps/extension_check.py", + "usage": "input", + "git_blob": "659edb7f09a73ab417997e43344306d2882f71fc", + "sha256": "a246c10ab650b46c13ec86ddc814306338ac84c65a93e2c6cda45c2fcf8c5b70" + }, + { + "path": "research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean", + "usage": "input", + "git_blob": "4351c589eca198ff65af72a671dc6268dde89fd2", + "sha256": "9205ffe7c3ee68e7ade608631378ebb9e8d8f3e28d6c873de9cbdd7b1becf9b2" + }, + { + "path": "research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean", + "usage": "input", + "git_blob": "2041473a4640aa1adf17284bf73eb99b6bfcddbc", + "sha256": "7c506e82ccef28ec502eb7bcf214450c23b9decbd38c94d9b5b1fe66b81834a9" + }, + { + "path": "research/e8-d0-root-swaps/formal/RootSwapQuartet.lean", + "usage": "input", + "git_blob": "d7aecfd2f356956dadd136ac0f53a7b80643e529", + "sha256": "43edf0c90eba5ba805b691cd0b36b8b1e8abc5f80519a5ee1e5cc163bfd8a3e6" + }, + { + "path": "research/e8-d0-root-swaps/geometry_audit.py", + "usage": "input", + "git_blob": "3084be53d349da489e947d1e5a1c689eeb5148bc", + "sha256": "dc6c51d1a9376498d35dd35f8f24eb33c2c461656b249a76bf6c41ec3cac91ad" + }, + { + "path": "research/e8-d0-root-swaps/verify.py", + "usage": "input", + "git_blob": "7be154af0f4fba335addd9acd6404c82b44142d9", + "sha256": "ff2e84dd385490434435b871216044700bc949d00c7ea351fe91af5b07bb0217" + } + ] +} diff --git a/research/e8-root-swap-fast-inner/TASK.json b/research/e8-root-swap-fast-inner/TASK.json new file mode 100644 index 0000000000..d359142763 --- /dev/null +++ b/research/e8-root-swap-fast-inner/TASK.json @@ -0,0 +1,67 @@ +{ + "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": "Source-bound exact dot-product specialization reducing complete default PR3166 scientific replay runtime with all original checks retained.", + "scope_change_reason": "Narrow the runtime card to one pinned complete command; predecessor theorems are not audited or claimed anew.", + "bottleneck_link": "Reduce exact arithmetic overhead in a complete research replay without dropping checks; this historical component does not alter the selected supplier invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified complete replay speedup; one candidate is retained.", + "outcome": "completed", + "evidence": "PROOF.md gives exact substitution. verify.py compares 5096623 actual dots, 576 scalar fixtures and nineteen controls. README.md records five alternating pairs, zero failures and 13.9522152319 percent less median wall time.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the specialization be integrated into one maintained replay entry while preserving intended arithmetic independence?", + "why_it_matters": "The adapter accelerates a historical fixture rather than current supplier cold replay.", + "first_step": "Identify one active consumer, preserve all comparisons and controls, and measure its full command.", + "blocked_by": "No maintained consumer integration is supplied." + }, + { + "question": "Which remaining bottleneck matters in that consumer?", + "why_it_matters": "Unmodified work limits further speedup.", + "first_step": "Profile that complete consumer after integration.", + "blocked_by": "The first improvement ends this contribution; no further optimization is reserved." + } + ] +} diff --git a/research/e8-root-swap-fast-inner/VERIFY.json b/research/e8-root-swap-fast-inner/VERIFY.json new file mode 100644 index 0000000000..9d06da7c7a --- /dev/null +++ b/research/e8-root-swap-fast-inner/VERIFY.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-d0-root-swaps/EXTENSION.md", + "research/e8-d0-root-swaps/PROOF.md", + "research/e8-d0-root-swaps/RESULT.json", + "research/e8-d0-root-swaps/algebra_check.py", + "research/e8-d0-root-swaps/extension_check.py", + "research/e8-d0-root-swaps/formal/RootSwapConnectedCover.lean", + "research/e8-d0-root-swaps/formal/RootSwapOneExceptional.lean", + "research/e8-d0-root-swaps/formal/RootSwapQuartet.lean", + "research/e8-d0-root-swaps/geometry_audit.py", + "research/e8-d0-root-swaps/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 5096623 actual specialized/original dots, complete original scientific command and receipt, 576 scalar fixtures, nineteen custody/domain/integration controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete conformance and rejection coverage with optimized Python." + } + ] +} diff --git a/research/e8-root-swap-fast-inner/benchmark.py b/research/e8-root-swap-fast-inner/benchmark.py new file mode 100644 index 0000000000..07b93807c4 --- /dev/null +++ b/research/e8-root-swap-fast-inner/benchmark.py @@ -0,0 +1,76 @@ +"""Time complete fresh-process commands; write the generated evidence to stdout. + +Produced by Nick Petalas. Apache-2.0. Timings are local observations only. +""" + +from __future__ import annotations + +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +from time import perf_counter_ns + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import replay + + +def measure(argv, root): + start = perf_counter_ns() + process = subprocess.run(argv, cwd=root, capture_output=True, timeout=120, + check=False) + elapsed = perf_counter_ns() - start + correct = (process.returncode == 0 and process.stderr == b"" + and process.stdout == replay.EXPECTED.encode()) + return {"elapsed_ns": elapsed, "returncode": process.returncode, + "correct": correct, "stdout_sha256": sha256(process.stdout).hexdigest(), + "stderr": process.stderr.decode("utf-8", errors="replace")} + + +def benchmark(pairs): + replay.require(5 <= pairs <= 15, "pairs must be between five and fifteen") + root = replay.PACKAGE.parents[1] + before = replay.authenticated_inputs(root) + flags = [sys.executable, "-I", "-W", "error", "-B"] + commands = { + "baseline": flags + [str(root / replay.SOURCE / "verify.py")], + "fast": flags + [str(replay.PACKAGE / "replay.py")], + } + rows = [] + for pair in range(pairs): + for side in ("baseline", "fast"): + rows.append({"pair": pair + 1, "side": side, + **measure(commands[side], root)}) + replay.require(replay.authenticated_inputs(root) == before, + "scientific inputs changed during measurement") + failures = sum(not row["correct"] for row in rows) + summary = {} + for side in commands: + values = [row["elapsed_ns"] for row in rows if row["side"] == side] + summary[side] = {"median_ns": statistics.median(values), + "min_ns": min(values), "max_ns": max(values)} + return {"schema_version": 1, "python": sys.version, + "platform": platform.platform(), "cpu_count": os.cpu_count(), + "load_average": list(os.getloadavg()), "commands": commands, + "pairs": pairs, "complete_replays": len(rows), "failures": failures, + "summary": summary, "runs": rows, + "fraction_less_wall_time": 1 - summary["fast"]["median_ns"] + / summary["baseline"]["median_ns"]} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--pairs", type=int, default=5) + args = parser.parse_args() + result = benchmark(args.pairs) + print(json.dumps(result, indent=2, sort_keys=True)) + return int(result["failures"] != 0) + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/e8-root-swap-fast-inner/replay.py b/research/e8-root-swap-fast-inner/replay.py new file mode 100644 index 0000000000..8602938982 --- /dev/null +++ b/research/e8-root-swap-fast-inner/replay.py @@ -0,0 +1,115 @@ +"""Exact dot-product specialization for the complete retained E8 replay. + +Produced by Nick Petalas. Apache-2.0. The authenticated source programs, +mathematics, checks and notices remain conorholds's PR3166 contribution. +""" + +from __future__ import annotations + +from contextlib import contextmanager +from hashlib import sha256 +import json +from pathlib import Path +import sys +from types import ModuleType + + +PACKAGE = Path(__file__).resolve().parent +SOURCE = Path("research/e8-d0-root-swaps") +MODULES = ("geometry_audit", "algebra_check", "extension_check", "verify") +EXPECTED = ( + "PASS_E8_D0_ROOT_SWAPS geometry=two-exact-methods normal_families=5 " + "root_remainders=120 parabolics=256 extension_models=2 f1_support=24 " + "frame_plane_cases=57120\n" +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot8(a, b): + """The source's left-associated exact sum on its eight-coordinate domain.""" + if len(a) != 8 or len(b) != 8: + raise ValueError("dot8 requires eight coordinates") + return (0 + a[0] * b[0] + a[1] * b[1] + a[2] * b[2] + + a[3] * b[3] + a[4] * b[4] + a[5] * b[5] + + a[6] * b[6] + a[7] * b[7]) + + +def authenticated_inputs(root): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + rows = [row for row in manifest["files"] if row["usage"] == "input"] + require(len(rows) == 10, "expected ten scientific inputs") + result = {} + for row in rows: + path = row["path"] + require(Path(path).parent in (SOURCE, SOURCE / "formal"), "input scope") + raw = (root / path).read_bytes() + require(len(raw) <= 2**20, "scientific input capacity") + require(sha256(raw).hexdigest() == row["sha256"], "changed source: " + path) + require(path not in result, "duplicate scientific input") + result[path] = raw + require(all(str(SOURCE / (name + ".py")) in result for name in MODULES), + "missing scientific module") + return result + + +def checked_dot(original, stats): + def compare(a, b): + actual = dot8(a, b) + require(actual == original(a, b), "dot specialization disagrees") + stats["calls"] += 1 + return actual + return compare + + +@contextmanager +def source_modules(root, raw): + """Compile only the four hash-authenticated modules, bypassing .pyc reads.""" + names = ("geometry_audit", "algebra_check", "extension_check", "e8_bound_source") + previous = {name: sys.modules.get(name) for name in names} + old_path, old_argv = sys.path[:], sys.argv[:] + loaded = {} + try: + for filename, name in zip(MODULES, names): + path = root / SOURCE / (filename + ".py") + module = ModuleType(name) + module.__file__ = str(path) + sys.modules[name] = module + exec(compile(raw[str(SOURCE / (filename + ".py"))], str(path), "exec"), + module.__dict__) + loaded[filename] = module + yield loaded + finally: + sys.path[:] = old_path + sys.argv[:] = old_argv + for name in names: + if previous[name] is None: + sys.modules.pop(name, None) + else: + sys.modules[name] = previous[name] + + +def run_replay(mode="fast", root=None): + require(mode in ("baseline", "fast", "checked"), "replay mode") + root = PACKAGE.parents[1] if root is None else Path(root) + raw = authenticated_inputs(root) + stats = {"calls": 0} + with source_modules(root, raw) as modules: + for name in ("verify", "extension_check"): + module = modules[name] + if mode == "fast": + module.dot = dot8 + elif mode == "checked": + module.dot = checked_dot(module.dot, stats) + sys.argv[:] = [str(root / SOURCE / "verify.py")] + result = modules["verify"].main() + require(result == 0, "complete scientific replay failed") + return stats + + +if __name__ == "__main__": + require(len(sys.argv) in (1, 2), "usage: replay.py [baseline|fast|checked]") + run_replay(sys.argv[1] if len(sys.argv) == 2 else "fast") diff --git a/research/e8-root-swap-fast-inner/verify.py b/research/e8-root-swap-fast-inner/verify.py new file mode 100644 index 0000000000..2d81ee3ad1 --- /dev/null +++ b/research/e8-root-swap-fast-inner/verify.py @@ -0,0 +1,126 @@ +"""Check the new implementation contract, custody and full source integration. + +Produced by Nick Petalas. Apache-2.0. This preserves predecessor coverage; +it does not claim independent acceptance of the predecessor mathematics. +""" + +from contextlib import redirect_stderr, redirect_stdout +from fractions import Fraction +from hashlib import sha256 +from io import StringIO +from itertools import product +import json +from pathlib import Path +import sys +from tempfile import TemporaryDirectory +from types import ModuleType + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import replay + + +def rejected(call, message): + try: + call() + except (ValueError, OSError) as error: + replay.require(message in str(error), "unexpected rejection: " + str(error)) + return + raise ValueError("missing rejection: " + message) + + +def dot_cases(): + basis = [tuple(int(i == j) for i in range(8)) for j in range(8)] + cases = [(a, b) for a in basis for b in basis] + for signs in product((-1, 1), repeat=8): + a = tuple(signs[i] * (i + 1) for i in range(8)) + b = tuple(Fraction(signs[7 - i] * (3 * i - 11), i + 2) for i in range(8)) + cases.extend(((a, b), (b, a))) + for a, b in cases: + replay.require(replay.dot8(a, b) == sum(x * y for x, y in zip(a, b)), + "exact scalar case") + for left, right in ((0, 8), (7, 8), (9, 8), (8, 0), (8, 7), (8, 9)): + rejected(lambda: replay.dot8([0] * left, [0] * right), "eight coordinates") + rejected(lambda: replay.run_replay("unknown"), "replay mode") + return len(cases), 7 + + +def custody_controls(): + originals = replay.authenticated_inputs(replay.PACKAGE.parents[1]) + with TemporaryDirectory(prefix="e8-dot-custody-") as name: + root = Path(name) + for path, raw in originals.items(): + target = root / path + target.parent.mkdir(parents=True, exist_ok=True) + replay.require(target.write_bytes(raw) == len(raw), "fixture write") + for path, raw in originals.items(): + target = root / path + replay.require(target.write_bytes(raw + b"\n") == len(raw) + 1, + "mutation write") + rejected(lambda: replay.authenticated_inputs(root), "changed source") + replay.require(target.write_bytes(raw) == len(raw), "fixture restore") + path = next(iter(originals)) + (root / path).unlink() + rejected(lambda: replay.authenticated_inputs(root), "No such file") + return len(originals) + 1 + + +def complete_conformance(): + names = ("geometry_audit", "algebra_check", "extension_check", "e8_bound_source") + previous = {name: sys.modules.get(name) for name in names} + sentinels = {name: ModuleType(name) for name in names} + old_path, old_argv = sys.path[:], sys.argv[:] + output = StringIO() + try: + sys.modules.update(sentinels) + with redirect_stdout(output): + stats = replay.run_replay("checked") + replay.require(output.getvalue() == replay.EXPECTED, "complete source stdout") + replay.require(stats == {"calls": 5096623}, "complete replacement coverage") + replay.require(all(sys.modules[name] is sentinels[name] for name in names), + "module restoration") + replay.require(sys.path == old_path and sys.argv == old_argv, + "process-state restoration") + finally: + for name in names: + if previous[name] is None: + sys.modules.pop(name, None) + else: + sys.modules[name] = previous[name] + return stats + + +def kernel_fault_control(): + original = replay.dot8 + def damaged(a, b): + return original(a, b) - a[7] * b[7] + replay.dot8 = damaged + error = StringIO() + try: + with redirect_stdout(StringIO()), redirect_stderr(error): + rejected(lambda: replay.run_replay("fast"), "complete scientific replay failed") + replay.require("root norm is not two" in error.getvalue(), + "source did not detect the changed dot product") + finally: + replay.dot8 = original + return 1 + + +def main(): + replay.require(len(sys.argv) == 1, "verify.py takes no arguments") + scalar_cases, controls = dot_cases() + controls += custody_controls() + stats = complete_conformance() + controls += kernel_fault_control() + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "replay.py", "benchmark.py", "verify.py") + hashes = {name: sha256((replay.PACKAGE / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps({"status": "PASS_E8_ROOT_SWAP_FAST_INNER", + "scalar_cases": scalar_cases, "controls": controls, + "complete_dot_comparisons": stats["calls"], + "source_stdout_sha256": sha256(replay.EXPECTED.encode()).hexdigest(), + "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()