diff --git a/research/a2-e6-cached-contractions/PROOF.md b/research/a2-e6-cached-contractions/PROOF.md new file mode 100644 index 0000000000..fcfe25d7b1 --- /dev/null +++ b/research/a2-e6-cached-contractions/PROOF.md @@ -0,0 +1,96 @@ +# Exact contraction reuse in the PR2061 primary replay + +This scoped implementation-equivalence proof was produced by Nick Petalas. +New work is Apache-2.0. Independent human and formal proof-kernel review are +unclaimed. Adam Gall's COPY69 theorem is a cited predecessor result, not a +new mathematical claim of this package. + +## Contract and equality + +The pinned primary verifier checks each requested ordered pair by computing + +```text +sum_k rows[i][k] * (sum_s Q(E.LINES[j][s]) * frame.F[k][s]) / 4 + == 2 * E.G[i][j]. +``` + +Its actual domain has 112 live indices, nine normals and eight coordinates. +All contractions use exact rational arithmetic. During an identity invocation +the indices, normals, roots and Gram matrix are fixed. No callback or mutation +occurs inside a contraction. + +Define `C[j,k]` to be the parenthesized sum divided by four. Its inputs do not +depend on i. The adapter computes each C once, then uses +`sum_k rows[i][k] * C[j,k]` in the same i,j,k order. Each coefficient is exactly +the original coefficient, including rational conversion and division. Therefore +each entry comparison has exactly the same value. The first failing ordered +pair is unchanged, and success still requires every requested ordered pair. +Eagerly computing later coefficients adds no exceptional behavior on this +fixed finite rational domain. + +The cache is local to one call. It is discarded before the next invocation, +so changing normals, input rows, roots or Gram data cannot reuse stale values. +The adapter authenticates all nine live files before importing predecessor +code. The predecessor retains its own source checks as well. + +## Exact work reduction + +The original `run()` invokes the identity routine twice. Its positive witness +compares 12,544 entries. Its existing deliberately changed coefficient fails +on comparison 4,817. Both invocations and both outcomes remain present. + +For V visited pairs, the original executes 9V eight-coordinate contractions. +For each invocation the adapter executes 9*112=1,008 contractions. Hence + +```text +original: 9*(12544+4817) = 156249 contractions +cached: 2*9*112 = 2016 contractions +removed: 154233 contractions +removed rational products: 8*154233 = 1233864 +``` + +These are counts of explicit `Q(a) * b` operations in the inner contraction. +No claim counts the saved additions, conversions or divisions as further +multiplications. The outer nine-term entry sums are unchanged. The verifier +enumerates the visited pairs and checks these exact counts. + +## Complete workload and measurement + +Both benchmark modes invoke the unchanged complete `run()`. It still performs +the geometry checks, every character-compatibility and triple-compatibility +check, support and rank calculations, attaining identity, all existing +rejection controls and both rational interval budget screens. Both compare +the entire freshly computed result with the pinned `RESULT.json` and print +the same complete-primary success line. Only `exact_identity` is replaced. + +The complete primary CLI is the measurement boundary. Import, all source hash +checks, construction, scientific execution, certificate comparison and output +are inside the subprocess timer. It is not a whole four-command registered +workflow measurement. The independent checker and six-test driver remain +unchanged and are not claimed to be faster. + +Five alternating original/cached fresh processes each passed, with identical +stdout and no stderr. Median elapsed time was 2.354848833 seconds original +and 1.698670834 seconds cached, a 27.8649733% reduction. Original range was +2.331363334 to 2.602431125 seconds; cached range was 1.675971083 to 1.886004875. +The ten integer nanosecond samples are reproduced in README.md. +These are local macOS measurements, not a portable timing guarantee. + +A separate, untimed cProfile run attributed 2.769 of 4.770 profiled run-seconds +to the two original identity invocations. The measured saving is below that +profile share. Other exact rational work, especially the unchanged interval +budget calculation, limits the complete-CLI gain. Profiling overhead is not +included in the reported timings. + +## Scope and stopping point + +The proof applies to this fixed source-bound rational routine, not arbitrary +side-effecting or mutable input objects. The new finite controls compare the +original and cached routines on rational inputs, every single-entry mutation +of five bounded domains, changed normals and changed Gram data. Separate +source controls reject corruption of each live file and one missing file. + +The first verified improvement ended optimization. This package does not +re-establish the predecessor's optimum, change its decoder, lower a native +invoice or prove a multiplication bound. Complete supplier, physical, stock, +precision/tape, compiler and outer obligations retain their prior status. diff --git a/research/a2-e6-cached-contractions/README.md b/research/a2-e6-cached-contractions/README.md new file mode 100644 index 0000000000..6c10402fa3 --- /dev/null +++ b/research/a2-e6-cached-contractions/README.md @@ -0,0 +1,125 @@ +# Cached contractions in the complete A2+E6 primary replay + +The opt-in PR2061 adapter removes 154,233 repeated exact contractions and +1,233,864 rational multiplications. The complete primary CLI's local median +time falls by 27.86%, preserving its complete result and all original checks. +This is a scoped implementation-equivalence proof, exact operation-count +certificate and local performance result. It is not a new decoder theorem, +supplier admission or kappa. The contribution was produced by Nick Petalas. + +`replay.py` authenticates nine live source files, imports the unchanged primary +verifier and replaces only `exact_identity`. The new implementation computes +the fixed 112-by-9 root-normal contraction table once per call. It retains +every ordered entry comparison, the original early rejection and the complete +`RESULT.json` comparison. The cache never survives an invocation. +[PROOF.md](PROOF.md) proves exact equality and gives the counting argument. +No frozen predecessor file or selected record changes. + +## Measurements + +CPython 3.12.15, macOS 27.0.1 arm64, 18 logical CPUs, standard library only. +Five alternating original/cached fresh-process pairs passed with no errors, +identical stdout and empty stderr. The timer encloses the entire CLI, including +imports, source authentication and both rational budget screens. + +| Mode | Median seconds | Minimum | Maximum | +| --- | ---: | ---: | ---: | +| Original | 2.354848833 | 2.331363334 | 2.602431125 | +| Cached | 1.698670834 | 1.675971083 | 1.886004875 | + +The integer nanosecond samples, in alternating pair order, are: + +```text +original cached +2332376792 1886004875 +2602431125 1675971083 +2354848833 1841411000 +2331363334 1698670834 +2503531083 1684102000 +``` + +The one-minute load average rose from 3.00 to 4.41 during the run. Other work +could not be controlled; the sides were interleaved on the same machine. +A separate profile places about 58% of the original `run()` time in the two +identity invocations. The unchanged interval budget calculation is a remaining +limiter. Profiler runs are excluded from the timing sample. The measured gain +is below the original identity share; no isolated helper timing is substituted +for the complete CLI. This is not a whole four-command workflow speedup or a +guarantee on another machine. + +## 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/a2-e6-cached-contractions/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/a2-e6-cached-contractions/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a2-e6-cached-contractions +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a2-e6-cached-contractions --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a2-e6-cached-contractions/benchmark.py +``` + +Any CPython 3.12 path may replace the local absolute path. Put `TMPDIR` and +redirected receipts in an external scratch directory if retaining outputs. +The benchmark defaults to five alternating pairs and accepts at most nine. +It checks every exit status and exact stdout; a failed run aborts the report. +Registered verification runs normal and optimized Python and writes a generated +stdout receipt bound to every package-file hash. No receipt is handwritten. +Expected markers are `PASS_A2_E6_CACHED_CONTRACTIONS`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. + +The verifier retains the complete primary science, including 12,544 positive +identity comparisons and the coefficient mutation's rejection at comparison +4,817. It adds 37 rational control cases and ten real source-admission controls. +Each of the nine live dependencies is independently corrupted and rejected; +one missing input is rejected. The package exports with all declared inputs +and can replay without Git or network access. No source receipt is rewritten. + +## Scope and implementation constraints + +The first successful contraction change ended optimization. `independent.py` +and `test_verify.py` from PR2061 are unchanged, unoptimized and outside the timed +primary CLI. Their mathematical results are not this contribution. No selected +cold replay, Lean, Docker, native supplier or complete multiplication theorem +was run or proved. The selected conditional kappa 0.003125804 and its five +framework assumptions remain unchanged. Independent human and formal +proof-kernel review are unclaimed. + +The adapter has at most 120 indices, nine normals and eight coordinates from +the authenticated source. Its cache has at most 1,080 rational entries, 1,008 +on the actual fixture. New functions fit within 60 lines, use no recursion and +enforce bounded domains. Source-control copies are temporary and removed on +every exit. Each subprocess has a 60-second timeout; the benchmark has at most +18 subprocesses. CPython allocation and fixed-target dynamic module imports are +documented Power of Ten deviations. The legacy imported `run()` exceeds the +function-size target; it remains frozen to preserve the exact workload. +Warning-strict normal and optimized runs provide recurring diagnostics. + +## Open next questions + +Should this adapter be adopted by PR2061's registered workflow? Start with an +explicit successor source binding and the complete four-command Linux replay. +Default adoption and a whole-workflow measurement are still missing. They +cannot be inferred from the primary CLI measurement. [TASK.json](TASK.json) +records the same first step and blocker. No further optimization is reserved. + +## Credit and overlap + +Adam Gall's [PR2061](https://github.com/CrocSwap/integer-mult-bounds/pull/2061), +head `eed23989eddf7ec0b2c24d9e3794d0fca53f11ab`, supplies the complete scientific +workload, COPY69 result and rejection controls. Credit joaqcoo / PR1224 for the +normal family and geometry implementation; Philipp / mightyOil / PR1248, +commdata2338 / PR1304 and Hanson Sun / bbMisk / PR1612 for the deficiency method; +DreamingOfClouds, GamingPuzzled, themilkman216, woklerx, Sagar Thakrar and Douglas +Colkitt for the decoder, coverage and ceiling lineage retained in PR2061. +Their files and notices are unchanged. The new contribution is the contraction +adapter, equality proof, operation reduction and complete-CLI measurements. +Exact source pins are in [SOURCES.json](SOURCES.json). New work is Apache-2.0. + +Base canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371337). +Live open PRs, recent account PRs, handoffs and all-main README searches were +checked for this particular replay. The overlap helper had complete remote +pagination and incomplete sparse local-note coverage, supplemented by Git main +searches. These searches are bounded evidence, not proof of global novelty. +No related open PR studying this exact A2+E6 primary replay was found. diff --git a/research/a2-e6-cached-contractions/SOURCES.json b/research/a2-e6-cached-contractions/SOURCES.json new file mode 100644 index 0000000000..ce8f55367b --- /dev/null +++ b/research/a2-e6-cached-contractions/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/a2-e6-nine-normal-floor/RESULT.json", + "usage": "input", + "git_blob": "c87f58ee3d4394ee8a1d2bb4a1ad85cc184747b9", + "sha256": "d6712b33ad02b9c894b3e8253f75103297ad725c196e63b02af7fab2df62f0ca" + }, + { + "path": "research/a2-e6-nine-normal-floor/SOURCES.json", + "usage": "input", + "git_blob": "749c5e467b8cec6bfaf80657e41975c364c6ecb8", + "sha256": "47d3b549df431f199617ecc70be4a597ecd7d05443494c2517b1be3c12db59da" + }, + { + "path": "research/a2-e6-nine-normal-floor/verify.py", + "usage": "input", + "git_blob": "46113056d907077ad60c5542d4b8452a70dd36f3", + "sha256": "93f9d9293dbee222f926d9da003742959f6b55ff337abe3d7a8acd85f2a2f345" + }, + { + "path": "research/a8-one-pair-frame-floor/README.md", + "usage": "input", + "git_blob": "8f3748696ab69b1ba57a400e0e2070bf09b817d8", + "sha256": "bd0fa2ec318eb5b8ac21c69b5be3dbcabdb7a9e51d8cecdbc79e46bfe56ef94c" + }, + { + "path": "research/complex-local-word-ceiling/RESULT.json", + "usage": "input", + "git_blob": "77f55043a679dd722330f1e2499863e36376d9f9", + "sha256": "d91d6c46509875abf1f61de67c2609656d3dc685451299f83caa6f922493692d" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/PROOF.md", + "usage": "input", + "git_blob": "e510fd180a286445fd6fc484057001bfc60f8c9c", + "sha256": "0503e07f1764708e9e72c01be88d3dad1b213e73eb3c23397a603032791fd23a" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/e8lab.py", + "usage": "input", + "git_blob": "6aef95fc972f56e600b7c9699238e3a1ce7f7413", + "sha256": "772349edc9dff45fa3cac89fdbbe8bf1bab734e9776a245fcac8e8bd60d94634" + }, + { + "path": "research/nine-term-decoder-normal-form-seed42/verify.py", + "usage": "input", + "git_blob": "994e429042f292084546c8d1efe287dfb5930fd9", + "sha256": "248763cf5ff85f073766aa8a85187a1d314fcf3a716b2586ca8fc1197d4c6c4e" + }, + { + "path": "research/a2-e6-nine-normal-floor/README.md", + "usage": "provenance", + "git_blob": "188643388662d639b4d1e798ac70bdfdadd37a22", + "sha256": "be549abbe2b617e2868ab086b1602f711a11a2064174d41a9cd30a6cf2945827" + } + ] +} diff --git a/research/a2-e6-cached-contractions/TASK.json b/research/a2-e6-cached-contractions/TASK.json new file mode 100644 index 0000000000..11351e0721 --- /dev/null +++ b/research/a2-e6-cached-contractions/TASK.json @@ -0,0 +1,75 @@ +{ + "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 implementation equivalence, operation reduction and complete primary CLI timing for PR2061.", + "scope_change_reason": "Choose the complete PR2061 primary scientific CLI as one bounded replay; cache only its fixed exact contractions.", + "bottleneck_link": "Reduce repeated exact arithmetic in a complete retained geometry/decoder replay without losing its scientific checks.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified complete-CLI improvement; no second optimization.", + "outcome": "completed", + "evidence": "PROOF.md, replay.py and verify.py; benchmark.py generates exact per-run timings outside the checkout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Should the opt-in adapter be adopted by PR2061's registered workflow?", + "why_it_matters": "The measured primary-CLI saving does not change the predecessor's default replay.", + "first_step": "Arrange an explicit successor source binding and run its full four-command registered workflow on Linux.", + "blocked_by": "Production adoption and a whole-workflow measurement are outside this isolated contribution." + } + ], + "source_pr": 2061, + "source_author": "adamgall", + "source_head": "eed23989eddf7ec0b2c24d9e3794d0fca53f11ab", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371337", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS 27.0.1 arm64", + "dependencies": "standard library" + }, + "limitations": [ + "Complete primary CLI only; independent.py and test_verify.py are unchanged and not optimized.", + "No new decoder optimum, supplier admission, kappa or multiplication theorem.", + "All five selected framework assumptions remain; selected scientific replay, Lean and Docker were not run." + ] +} diff --git a/research/a2-e6-cached-contractions/VERIFY.json b/research/a2-e6-cached-contractions/VERIFY.json new file mode 100644 index 0000000000..17534b454b --- /dev/null +++ b/research/a2-e6-cached-contractions/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a2-e6-nine-normal-floor/RESULT.json", + "research/a2-e6-nine-normal-floor/SOURCES.json", + "research/a2-e6-nine-normal-floor/verify.py", + "research/a8-one-pair-frame-floor/README.md", + "research/complex-local-word-ceiling/RESULT.json", + "research/complex-local-word-ceiling/ceiling.py", + "research/nine-term-decoder-normal-form-seed42/PROOF.md", + "research/nine-term-decoder-normal-form-seed42/e8lab.py", + "research/nine-term-decoder-normal-form-seed42/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete primary scientific replay, full predecessor certificate equality, exact removed-operation counts, 37 rational controls and ten source-admission controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete scientific and adapter checks with assertions disabled." + } + ] +} diff --git a/research/a2-e6-cached-contractions/benchmark.py b/research/a2-e6-cached-contractions/benchmark.py new file mode 100644 index 0000000000..43d5cc47e2 --- /dev/null +++ b/research/a2-e6-cached-contractions/benchmark.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Time alternating fresh-process complete primary replays; write only stdout.""" + +import argparse +import hashlib +import json +import os +import platform +import statistics +import subprocess +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +EXPECTED = b"PASS_A2_E6_NINE_NORMAL_FLOOR copy=69 active=9 variable=17 fixed=52 entries=12544 controls=4\n" + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--pairs", type=int, choices=range(5, 10), default=5) + args = parser.parse_args() + rows = [] + env = dict(os.environ) + env.pop("PYTHONOPTIMIZE", None) + load_start = os.getloadavg() + for pair in range(args.pairs): + for mode in ("original", "cached"): + command = [sys.executable, "-I", "-W", "error", "-B", + str(HERE / "replay.py"), "--mode", mode] + started = time.perf_counter_ns() + run = subprocess.run(command, capture_output=True, timeout=60, env=env, check=False) + elapsed = time.perf_counter_ns() - started + if run.returncode or run.stdout != EXPECTED or run.stderr: + raise ValueError((mode, run.returncode, run.stdout, run.stderr)) + rows.append({"pair": pair, "mode": mode, "nanoseconds": elapsed, + "stdout_sha256": hashlib.sha256(run.stdout).hexdigest()}) + summary = {} + for mode in ("original", "cached"): + values = [row["nanoseconds"] for row in rows if row["mode"] == mode] + summary[mode] = {"median_ns": statistics.median(values), + "min_ns": min(values), "max_ns": max(values)} + fraction = 1 - summary["cached"]["median_ns"] / summary["original"]["median_ns"] + report = {"status": "PASS_A2_E6_COMPLETE_BENCHMARK", "errors": 0, + "python": sys.version, "executable": sys.executable, + "platform": platform.platform(), "machine": platform.machine(), + "cpu_count": os.cpu_count(), "load_start": load_start, + "load_end": os.getloadavg(), "runs": rows, "summary": summary, + "median_time_reduction": fraction, + "scope": "complete primary CLI; every run compares the full predecessor certificate"} + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/a2-e6-cached-contractions/replay.py b/research/a2-e6-cached-contractions/replay.py new file mode 100644 index 0000000000..127fb136ad --- /dev/null +++ b/research/a2-e6-cached-contractions/replay.py @@ -0,0 +1,93 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Complete PR2061 primary replay with invocation-local fixed contractions.""" + +import argparse +import hashlib +import importlib.util +import json +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = "research/a2-e6-nine-normal-floor" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(root=ROOT): + """Check every live dependency before the predecessor imports any code.""" + pins = json.loads((HERE / "SOURCES.json").read_text()) + live = [row for row in pins["files"] if row["usage"] == "input"] + require(len(live) == 9, "live dependency inventory") + for row in live: + path = root / row["path"] + require(path.is_file() and path.stat().st_size <= 2**20, "source size") + require(hashlib.sha256(path.read_bytes()).hexdigest() == row["sha256"], + "source mismatch: " + row["path"]) + + +def load_original(): + authenticate() + spec = importlib.util.spec_from_file_location("a2_e6_original", ROOT / SOURCE / "verify.py") + require(spec is not None and spec.loader is not None, "source loader") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def cached_identity(E, frame, indices, rows, counts=None): + """Factor the j,k-only contraction out of the all-pairs i,j test.""" + indices = tuple(indices) + require(len(indices) <= 120 and len(frame.F) == 9, "bounded identity domain") + coefficients = { + j: tuple(sum(Q(a) * b for a, b in zip(E.LINES[j], normal)) / 4 + for normal in frame.F) + for j in indices + } + visited = 0 + valid = True + for i in indices: + for j in indices: + visited += 1 + value = sum(rows[i][k] * coefficients[j][k] for k in range(9)) + if value != 2 * E.G[i][j]: + valid = False + break + if not valid: + break + if counts is not None: + counts.append({"entries": visited, + "original_contractions": 9 * visited, + "cached_contractions": 9 * len(indices), "valid": valid}) + return valid + + +def replay(mode): + require(mode in ("original", "cached"), "replay mode") + module = load_original() + counts = [] + if mode == "cached": + def identity(E, frame, indices, rows): + return cached_identity(E, frame, indices, rows, counts) + module.exact_identity = identity + result = json.loads(json.dumps(module.run())) + expected = json.loads((ROOT / SOURCE / "RESULT.json").read_text()) + require(result == expected, "complete predecessor certificate mismatch") + return result, counts + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--mode", choices=("original", "cached"), default="cached") + args = parser.parse_args() + replay(args.mode) + print("PASS_A2_E6_NINE_NORMAL_FLOOR copy=69 active=9 variable=17 fixed=52 entries=12544 controls=4") + + +if __name__ == "__main__": + main() diff --git a/research/a2-e6-cached-contractions/verify.py b/research/a2-e6-cached-contractions/verify.py new file mode 100644 index 0000000000..a7e0c975d4 --- /dev/null +++ b/research/a2-e6-cached-contractions/verify.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Verify the new contraction adapter and its complete retained workload.""" + +import hashlib +import json +import sys +import tempfile +from fractions import Fraction as Q +from pathlib import Path +from types import SimpleNamespace + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from replay import ROOT, authenticate, cached_identity, load_original, replay, require # noqa: E402 + + +def controls(): + original = load_original().exact_identity + E = SimpleNamespace(LINES=[(Q(i), Q(1 - i)) for i in range(4)]) + frame = SimpleNamespace(F=[(Q(k, 3), Q(2 - k, 5)) for k in range(9)]) + rows = {i: [Q((i + 1) * (k - 3), 7) for k in range(9)] for i in range(4)} + E.G = [[sum(rows[i][k] * sum(a * b for a, b in zip(E.LINES[j], frame.F[k])) / 8 + for k in range(9)) for j in range(4)] for i in range(4)] + cases = 0 + for length in range(5): + indices = list(range(length)) + require(original(E, frame, indices, rows) is True, "rational positive fixture") + require(cached_identity(E, frame, indices, rows) is True, "cached positive fixture") + cases += 1 + for i in indices: + for j in indices: + E.G[i][j] += Q(1, 11) + require(original(E, frame, indices, rows) is False, "original mutation") + require(cached_identity(E, frame, indices, rows) is False, "cached mutation") + E.G[i][j] -= Q(1, 11) + cases += 1 + # One fresh invocation must see changed source coefficients and Gram entries. + frame.F[0] = (Q(101), Q(-37)) + require(original(E, frame, list(range(4)), rows) is False, "changed normals original") + require(cached_identity(E, frame, list(range(4)), rows) is False, "no cross-call cache") + E.G[0][0] += 1 + require(cached_identity(E, frame, [0], rows) is False, "changed Gram matrix") + return cases + 2 + + +def source_controls(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + live = [row for row in pins["files"] if row["usage"] == "input"] + with tempfile.TemporaryDirectory(prefix="a2-e6-source-controls-") as name: + root = Path(name) + for row in live: + path = root / row["path"] + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes((ROOT / row["path"]).read_bytes()) + authenticate(root) + for row in live: + path = root / row["path"] + data = path.read_bytes() + path.write_bytes(data + b"\n") + try: + authenticate(root) + except ValueError as error: + require(str(error).startswith("source mismatch:"), "hash rejection reason") + else: + raise ValueError("source corruption accepted") + path.write_bytes(data) + path.unlink() + try: + authenticate(root) + except ValueError as error: + require(str(error) == "source size", "missing source rejection reason") + else: + raise ValueError("missing source accepted") + return len(live) + 1 + + +def main(): + control_count = controls() + source_count = source_controls() + result, counts = replay("cached") + require(len(counts) == 2, "both original identity invocations retained") + require(counts[0]["entries"] == 12544 and counts[0]["valid"], "all-pairs coverage") + require(counts[1]["entries"] == 4817 and not counts[1]["valid"], + "original changed-coefficient rejection") + original = sum(row["original_contractions"] for row in counts) + cached = sum(row["cached_contractions"] for row in counts) + require((original, cached) == (156249, 2016), "exact operation improvement") + files = sorted(path for path in HERE.iterdir() if path.is_file()) + require(len(files) <= 16 and all(p.stat().st_size <= 2**20 for p in files), "package bounds") + receipt = {"status": "PASS_A2_E6_CACHED_CONTRACTIONS", "controls": control_count, + "source_controls": source_count, + "calls": counts, "removed_contractions": original - cached, + "removed_rational_products": 8 * (original - cached), + "result_sha256": hashlib.sha256(json.dumps(result, sort_keys=True).encode()).hexdigest(), + "package_sha256": {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in files}} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()