diff --git a/research/e8-bit-r420/MANIFEST.sha256 b/research/e8-bit-r420/MANIFEST.sha256 index 8117af93d3..5e50ac35c5 100644 --- a/research/e8-bit-r420/MANIFEST.sha256 +++ b/research/e8-bit-r420/MANIFEST.sha256 @@ -14,7 +14,7 @@ e2fd3429e2db4389ae8a5ab47dda89f551b0d0952c42fad5ac8d38a85d670594 code/mutants.p c0a687f61aed29455cea953d8a3e49a32136edb3cd4213c46880c146a6ca7fa3 code/planio.py aade757c1e4e2714207cbc80a9a60793d84b5f009de2cac79ee8d3239986fd2a code/provenance.py afdf2e53648b417fcc49cd05e9a18ee9fff9ae41e791a6ffa333130e30f35feb code/summary.py -5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424 code/xcheck.py +cd1d91b32831b4bd75290edf8b19f3a4378c5733bf4755ba59ed5161e2c468b9 code/xcheck.py 9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784 data/bitE8mut-r420.json.gz ec81d67d8a82d41859ee33a4e387679b71e5ced15de074a71195d08969dd308a data/complex-b.json 3f4be566309841e00e842d5686f7937a355ae1a6a2eaa3ccb07bdf8a9ca604fb data/complex/pr535/EXACT-ASSEMBLY-PR493.json diff --git a/research/e8-bit-r420/code/xcheck.py b/research/e8-bit-r420/code/xcheck.py index fbff8607e4..75fef5468a 100644 --- a/research/e8-bit-r420/code/xcheck.py +++ b/research/e8-bit-r420/code/xcheck.py @@ -29,13 +29,18 @@ J the source part of every target's W0 output is its own source (J = I); K the helper part of every target's W0 output equals the helper set D adds to it (D = -V^-1 K s over F2); Uinv C applied to the W0 outputs of the z registers restores every z register (C = U^-1). -Prepared by eumemic with substantial Anthropic Claude assistance; Apache-2.0.""" +Prepared by eumemic with substantial Anthropic Claude assistance; Apache-2.0. + +Production rref uses primitive-integer elimination (Aman PR367 / research/r420-rref-performance) +and returns the same rational basis rows and pivot columns as the historical Fraction RREF. +See research/r420-rref-production/ for equivalence evidence. No other checker stage changes.""" import gzip import json import math import sys from collections import Counter from fractions import Fraction +from math import gcd, lcm class Reject(Exception): @@ -48,26 +53,65 @@ def need(cond, msg): # ------------------------------------------------------------------ exact linear algebra over Q and Z -def rref(rows): - """reduced row echelon form over Q of integer rows; returns (basis rows, pivot columns)""" - m = [[Fraction(x) for x in r] for r in rows] - piv = [] - rk = 0 - ncol = len(m[0]) if m else 0 - for col in range(ncol): - p = next((i for i in range(rk, len(m)) if m[i][col] != 0), None) - if p is None: +def _primitive(row): + content = gcd(*row) if row else 0 + return [x // content for x in row] if content > 1 else row + + +def _integer_rows(matrix): + """Convert integer/Fraction rows to content-primitive integer rows; never mutate inputs.""" + rows = [] + for values in matrix: + row = list(values) + if all(isinstance(x, int) for x in row): + rows.append(_primitive(row)) + else: + values = [Fraction(x) for x in row] + denominator = lcm(*(x.denominator for x in values)) if values else 1 + rows.append(_primitive([x.numerator * (denominator // x.denominator) + for x in values])) + if rows and any(len(row) != len(rows[0]) for row in rows): + raise ValueError('matrix rows must have equal lengths') + return rows + + +def _eliminate(matrix, reduced=False): + """Fraction-free integer elimination; returns primitive rows and pivot columns.""" + rows = _integer_rows(matrix) + if not rows: + return rows, [] + pivots = [] + for column in range(len(rows[0])): + rank = len(pivots) + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: continue - m[rk], m[p] = m[p], m[rk] - inv = 1 / m[rk][col] - m[rk] = [a * inv for a in m[rk]] - for i in range(len(m)): - if i != rk and m[i][col] != 0: - f = m[i][col] - m[i] = [a - f * b for a, b in zip(m[i], m[rk])] - piv.append(col) - rk += 1 - return m[:rk], piv + rows[rank], rows[pivot] = rows[pivot], rows[rank] + base = rows[rank] + targets = range(len(rows)) if reduced else range(rank + 1, len(rows)) + for i in targets: + if i == rank or not rows[i][column]: + continue + row = rows[i] + divisor = gcd(base[column], row[column]) + a, b = base[column] // divisor, row[column] // divisor + rows[i] = _primitive([a * x - b * y for x, y in zip(row, base)]) + pivots.append(column) + if len(pivots) == len(rows): + break + return rows, pivots + + +def rref(rows): + """Reduced row echelon form over Q; returns (basis rows, pivot columns). + + Production form of research/r420-rref-performance/: primitive-integer elimination + followed by exact pivot scaling to Fractions. Identical rational row space and + pivot list to the historical per-entry Fraction RREF. + """ + matrix, pivots = _eliminate(rows, reduced=True) + return [[Fraction(x, row[column]) for x in row] + for row, column in zip(matrix, pivots)], pivots def nullspace_int(rows, ncol=8): diff --git a/research/r420-rref-production/NOTICE.md b/research/r420-rref-production/NOTICE.md new file mode 100644 index 0000000000..fe1dd89a81 --- /dev/null +++ b/research/r420-rref-production/NOTICE.md @@ -0,0 +1,20 @@ +# Attribution and license + +Prepared by Wentao Li ([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor), wentaol4@illinois.edu) with substantial +AI assistance for orientation, overlap search, profiling, production wiring, +packaging, benchmarking and writing. Not independent human peer review. +Apache-2.0; see the repository root `LICENSE`. + +The primitive-integer RREF algorithm wired into production was introduced by +**Aman** (PR367 / `research/frame-algebra-performance` lineage) and integrated as +an opt-in adapter by the authors of +`research/r420-rref-performance/` (merged tooling PR; prepared for @MrPink604 +with substantial AI assistance). That package's NOTICE.md and PROOF.md retain +the exactness argument. This package wires an equivalent `rref` into the +production `research/e8-bit-r420/code/xcheck.py` path used by +`research/e8-bit-r420/verify.sh` step 2 and `mutants.py`. + +The original R420 checker, mutation harness, word and interleaved +scalar-interface lemma are **eumemic**'s PR543, with substantial Anthropic Claude +assistance. Upstream material retains its own source notices and license. diff --git a/research/r420-rref-production/README.md b/research/r420-rref-production/README.md new file mode 100644 index 0000000000..89cb46b8cf --- /dev/null +++ b/research/r420-rref-production/README.md @@ -0,0 +1,90 @@ +# Production integer RREF for the R420 exact checker + +**Tooling improvement; no new kappa.** At base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, production +`research/e8-bit-r420/code/xcheck.py:rref` still paid a Fraction-per-entry +elimination on every frame. The opt-in adapter +`research/r420-rref-performance/` already proved an equivalent +primitive-integer RREF with identical receipts and explicitly deferred +production adoption. This package wires that equivalent check into the +**production** `rref` used by `research/e8-bit-r420/verify.sh` step 2 and +`mutants.py`. + +Only `research/e8-bit-r420/code/xcheck.py` and its +`research/e8-bit-r420/MANIFEST.sha256` digest line change outside this +directory. Label validation, HNF, determinant, F2 replay, H1–H5/dirty +restoration, and every mutation control remain the historical implementations. +Selected frontier untouched. Prior research packages that still pin the +Fraction `xcheck.py` digest (including `research/r420-rref-performance/SOURCES.json` +and other R420 follow-ons) are left as historical provenance, same pattern as +earlier production promotions. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/r420-rref-production/verify.py +python3.12 -I -O -B research/r420-rref-production/verify.py +python3.12 -B scripts/research_package.py --package research/r420-rref-production +python3.12 -I -B research/r420-rref-production/benchmark.py --rounds 5 --write-result +``` + +Expected: + +```text +PASS_R420_RREF_PRODUCTION frames=672 matrices=677 corruption=… certs=0 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/r420-rref-production outcome=completed +PASS_IDENTICAL_R420_RREF_PRODUCTION_RECEIPTS +``` + +Default verify is read-only. Timing is host-descriptive and is not a +correctness gate. On Linux / CPython 3.12.3 (this host), five alternating +fresh-process pairs gave: + +- check median **1.064 → 0.362 s (2.94×)** +- mutants harness median **11.090 → 3.457 s (3.21×)** +- stage-median sum **12.155 → 3.819 s (3.18×)** + +Retained samples are in [`RESULT.json`](RESULT.json). + +## Why the integer RREF is equivalent + +Aman’s primitive-integer elimination (`exact_rows._eliminate(..., reduced=True)`) +computes a content-primitive integer row echelon form with the same pivot +columns as the historical Fraction RREF. Scaling each pivot row by the +reciprocal of its pivot entry returns lists of `Fraction` equal to the +historical basis rows. The unchanged `nullspace_int` therefore emits the same +integer annihilators. Finite evidence compares all **672** shipped frames plus +five supplemental matrices, and byte-identical complete `xcheck` / +`mutants` stdout. This supports the scoped kernel argument; it is not a formal +proof of the multiplication theorem. + +## Overlap and credit + +Closest priors (different delivery): + +- `research/r420-rref-performance/` — opt-in integer RREF adapter; this package + is the production wiring. +- [CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756) + — identical-receipt tooling quality bar. +- Open leave-alone tooling on other objects (#1922 joint frames, #2054/#2150 + shared/mixed-point, #2100 ternary, #2117 DisjointTensor.frame_data, #2194 + production verify_factor, #2210 production leech_minor, #2231 production + sparse-fusion orbits, #2239 joint-dual replay, #2257 bit-frame + `frameopt.close`, #1861 parity-side, #1076 quadratic-affine) was not reopened. + +Credit **eumemic** (PR543 checker/harness/word), **Aman** (PR367 integer rows), +and the authors of `research/r420-rref-performance/`. Prepared by **Wentao Li** +with substantial AI assistance; see [NOTICE.md](NOTICE.md) and +[TASK.json](TASK.json). Apache-2.0. + +## Open next questions + +1. **Should `research/r420-rref-performance/` note that production now ships the + same integer `rref`?** Its `SOURCES.json` still pins the historical Fraction + `xcheck.py` bytes. First step: one-line status note and pin refresh or relax. + Blocked on: maintainer preference for touching incorporated packages. +2. **Should other packages that pin `research/e8-bit-r420/code/xcheck.py` refresh + that single digest?** Leaving old pins keeps this tooling change focused. + Blocked on: a dedicated provenance follow-up. diff --git a/research/r420-rref-production/RESULT.json b/research/r420-rref-production/RESULT.json new file mode 100644 index 0000000000..f4ece018b6 --- /dev/null +++ b/research/r420-rref-production/RESULT.json @@ -0,0 +1,163 @@ +{ + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "baseline_xcheck_sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "check_speedup": 2.939734938471416, + "controls_speedup": 3.207916313783938, + "interpreter": "CPython 3.12.3", + "machine": "x86_64", + "no_new_kappa": true, + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "production_xcheck_sha256": "cd1d91b32831b4bd75290edf8b19f3a4378c5733bf4755ba59ed5161e2c468b9", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "rounds": 5, + "stage_median_sum_seconds": { + "baseline": 12.154546371000038, + "production": 3.8191861049999716 + }, + "stage_median_sum_speedup": 3.182496489261847, + "status": "PASS_IDENTICAL_R420_RREF_PRODUCTION_RECEIPTS", + "suite_median_seconds": { + "baseline": 6.077273185500019 + }, + "timing_scope": "fresh subprocess wall time including imports; warm OS caches, not flushed; host-descriptive only; not a correctness gate", + "workloads": { + "check": { + "median_seconds": { + "baseline": 1.0641992050000226, + "production": 0.36200515600000926 + }, + "records": [ + { + "engine": "baseline", + "pair": 0, + "seconds": 1.1395701070000541, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "production", + "pair": 0, + "seconds": 0.33981653799992273, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "production", + "pair": 1, + "seconds": 0.35975235000000794, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "baseline", + "pair": 1, + "seconds": 0.989689956999996, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "baseline", + "pair": 2, + "seconds": 1.0807330019999881, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "production", + "pair": 2, + "seconds": 0.3831915519999711, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "production", + "pair": 3, + "seconds": 0.4227107120000255, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "baseline", + "pair": 3, + "seconds": 1.0547227089999751, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "baseline", + "pair": 4, + "seconds": 1.0641992050000226, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + }, + { + "engine": "production", + "pair": 4, + "seconds": 0.36200515600000926, + "stdout_sha256": "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" + } + ], + "speedup": 2.939734938471416 + }, + "controls": { + "median_seconds": { + "baseline": 11.090347166000015, + "production": 3.4571809489999623 + }, + "records": [ + { + "engine": "baseline", + "pair": 0, + "seconds": 11.682598048000045, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "production", + "pair": 0, + "seconds": 3.4433927389999326, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "production", + "pair": 1, + "seconds": 3.5178037910000057, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "baseline", + "pair": 1, + "seconds": 11.325159448000022, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "baseline", + "pair": 2, + "seconds": 11.020422073999953, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "production", + "pair": 2, + "seconds": 3.348689057999991, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "production", + "pair": 3, + "seconds": 3.6446222680000346, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "baseline", + "pair": 3, + "seconds": 10.93502884999998, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "baseline", + "pair": 4, + "seconds": 11.090347166000015, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + }, + { + "engine": "production", + "pair": 4, + "seconds": 3.4571809489999623, + "stdout_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + } + ], + "speedup": 3.207916313783938 + } + } +} diff --git a/research/r420-rref-production/SOURCES.json b/research/r420-rref-production/SOURCES.json new file mode 100644 index 0000000000..af1e4925a4 --- /dev/null +++ b/research/r420-rref-production/SOURCES.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/e8-bit-r420/code/xcheck.py", + "usage": "provenance", + "git_blob": "fbff8607e4c61e18481f696b99dd38a32444e90d", + "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "note": "Base-commit Fraction RREF bytes retained as baseline.py; production working tree differs." + }, + { + "path": "research/e8-bit-r420/code/mutants.py", + "usage": "input", + "git_blob": "5b0fa1922076d2e91367b58483c96b33b7b08661", + "sha256": "e2fd3429e2db4389ae8a5ab47dda89f551b0d0952c42fad5ac8d38a85d670594" + }, + { + "path": "research/e8-bit-r420/data/bitE8mut-r420.json.gz", + "usage": "input", + "git_blob": "0c63ca62759dc63d302be6552aeeee1ede70350f", + "sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784" + }, + { + "path": "research/e8-bit-r420/verify.sh", + "usage": "input", + "git_blob": "fbad38c694a0ce4fcbf39110dc403c75017ece07", + "sha256": "3192dea51acd17addb2750834a9dc3fb5b991e8dc5970ba9d2ac54608d79cafa" + }, + { + "path": "research/r420-rref-performance/vendor/exact_rows.py", + "usage": "input", + "git_blob": "b35f2c0624a1e3b944e30c53e97be469d0d7cdb9", + "sha256": "56703c3f11a071a27794159028a980eeb36363569d12b179dd8f905d233471a5" + }, + { + "path": "research/r420-rref-performance/EXPECTED.json", + "usage": "input", + "git_blob": "00856e84e48521d60039fed424a66fd8bdef0f2f", + "sha256": "081bb0c48be0665a76f20282b9aff17ce6f6e2f87e7070b92ce39784442f4243" + }, + { + "path": "research/r420-rref-performance/README.md", + "usage": "provenance", + "git_blob": "e84e638ed2908cb05832d4c89d2b1a4633ee7f8c", + "sha256": "e921117e66d9e8f788b857ad06d95a01361344c4932a639a0ef0cc655403897e" + } + ] +} diff --git a/research/r420-rref-production/TASK.json b/research/r420-rref-production/TASK.json new file mode 100644 index 0000000000..927294b20d --- /dev/null +++ b/research/r420-rref-production/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_seed": "c4e19f8a2b7d6041e5a39c8d7f1b2a60", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Can the production PR543 R420 checker (research/e8-bit-r420/code/xcheck.py:rref, exercised by research/e8-bit-r420/verify.sh step 2 and mutants.py on the pinned bitE8mut-r420 word) adopt the exact primitive-integer RREF from research/r420-rref-performance/ so the shipped verify path is faster while every check stdout field, mutation-harness receipt, frame RREF/pivot list and integer annihilator stays identical?", + "scope_change_reason": "Expertise override selected verifier-engineering after profiling showed production xcheck.rref still paid a Fraction-per-entry elimination on every frame while the incorporated opt-in adapter research/r420-rref-performance/ already proved an identical-receipt integer accelerator and explicitly deferred production adoption. Leave-alone objects (joint frames, shared/mixed-point, ternary, parity-side, DisjointTensor.frame_data, verify_factor, leech_minor, sparse-fusion, joint-dual replay, bit-frame frameopt.close, quadratic-affine) and deferred micro-opts were not reopened.", + "bottleneck_link": "Side result on review throughput: the R420 independent exact replay is a retained historical interface lemma check. Faster identical rref does not change kappa or the binding complex supplier.", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, packaging, benchmarking and writing", + "outcome": "completed", + "evidence": "PASS_R420_RREF_PRODUCTION via research/r420-rref-production/verify.py (also under -O); PASS_IDENTICAL_R420_RREF_PRODUCTION_RECEIPTS via benchmark.py; MANIFEST.sha256 binds the production xcheck digest; identical check and mutants stdout digests.", + "author": "Wentao Li", + "email": "wentaol4@illinois.edu", + "github": "VictorLiwentao", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving production xcheck.rref change with frozen baseline, identical check/mutants receipts, temp-copy corruption rejection, registered replay and a measured before/after median. Do not invent kappa or reopen leave-alone objects.", + "open_questions": [ + { + "question": "Should research/r420-rref-performance/ note that production now ships the same integer rref?", + "why_it_matters": "That opt-in package's SOURCES.json pins the historical Fraction xcheck.py bytes and will fail source admission after this rewrite.", + "first_step": "Add a one-line status note and either refresh or relax that single pin without editing pinned mathematical evidence.", + "blocked_by": "Maintainer preference on touching incorporated historical packages." + }, + { + "question": "Should the ~30 other research/*/SOURCES.json pins of research/e8-bit-r420/code/xcheck.py be refreshed?", + "why_it_matters": "Those packages bind working-tree xcheck.py bytes as historical provenance; leaving the old pins keeps this tooling PR focused.", + "first_step": "Dedicated provenance follow-up that only rewrites those pin entries after confirming receipt identity.", + "blocked_by": "Pin repair outside this tooling change." + } + ] +} diff --git a/research/r420-rref-production/VERIFY.json b/research/r420-rref-production/VERIFY.json new file mode 100644 index 0000000000..6d4d0be7e0 --- /dev/null +++ b/research/r420-rref-production/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-r420/code/xcheck.py", + "research/e8-bit-r420/code/mutants.py", + "research/e8-bit-r420/data/bitE8mut-r420.json.gz", + "research/e8-bit-r420/MANIFEST.sha256", + "research/e8-bit-r420/verify.sh", + "research/r420-rref-performance/vendor/exact_rows.py", + "research/r420-rref-performance/EXPECTED.json" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Exact baseline copy of the base-commit xcheck.py; identical check and mutants stdout digests; all 672 frame RREF/nullspace comparisons; temp-copy sign-flip foil rejection; MANIFEST binds production digest; duplicate JSON-key check; read-only default." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Same package require() gates under -O; xcheck/mutants children still launch assertion-enabled via -I -B without PYTHONOPTIMIZE." + } + ] +} diff --git a/research/r420-rref-production/baseline.py b/research/r420-rref-production/baseline.py new file mode 100644 index 0000000000..fbff8607e4 --- /dev/null +++ b/research/r420-rref-production/baseline.py @@ -0,0 +1,375 @@ +"""Independent exact replay and interface audit of a bitE8/1 word whose source and helper registers may be gate +destinations in phase A and in phase B (interleaved with target reads). No producer, generator or hub code is +imported; only the word file is read. +usage: xcheck.py WORD.json.gz [--json OUT] + +Part L (labels): the 120 labels are integer vectors with = dot/2; every label has norm 2, distinct labels have +|| <= 1, and the lattice they generate (Hermite normal form over Z) has Gram determinant 1 and rank 8. An even +unimodular positive definite lattice of rank 8 is E8, so the labels are its 120 root lines. Every listed frame is +closed (the listed lines are exactly the root lines in its span). + +Part F (frames and exact F2 semantics): every register starts at its start frame (sources at their own line, targets +and helpers at frame 0); before each gate every operand climbs to the gate's frame, and a climb must be nested with a +strict increase of dimension. Targets stay at frame 0 until the scatter. Values are replayed symbolically: register +r starts as the column e_r (x columns, y columns, helper-dirt columns), so the replay covers every input at once, with +arbitrary helper contents. Required at the end: every source holds e_s, every helper holds e_h, every target holds +e_{y_t} + e_{x_t}; final frames: sources and helpers at the full frame, target t at t-perp. + +Part I (interface): the hypotheses of the interleaved scalar-interface lemma (README, "Review point"), each evaluated +separately: + H1 no gate anywhere whose destination is a z register (source or helper) reads a target; + H2 D: every gate is at frame 0, writes a target and reads only helpers (all of them at frame 0 when D runs); + H3 A writes only z registers; the scatter reads only retained helper registers and writes only targets; every B gate + either writes a z register from z registers only, or writes a target; + H4 C is exactly the literal reverse of the z-destination gates of A and B (in order A then B), each at the full + frame; final frames of all z registers are the full frame, so C needs no descent; + H5 V = I: the target-to-target part of the raw word A, scatter, B is the identity. +and the lemma's conclusion decomposed on the raw word W0 = (A, scatter, B): + U every z register's W0 output has no target column (z' = U z); + J the source part of every target's W0 output is its own source (J = I); + K the helper part of every target's W0 output equals the helper set D adds to it (D = -V^-1 K s over F2); + Uinv C applied to the W0 outputs of the z registers restores every z register (C = U^-1). +Prepared by eumemic with substantial Anthropic Claude assistance; Apache-2.0.""" +import gzip +import json +import math +import sys +from collections import Counter +from fractions import Fraction + + +class Reject(Exception): + pass + + +def need(cond, msg): + if not cond: + raise Reject(msg) + + +# ------------------------------------------------------------------ exact linear algebra over Q and Z +def rref(rows): + """reduced row echelon form over Q of integer rows; returns (basis rows, pivot columns)""" + m = [[Fraction(x) for x in r] for r in rows] + piv = [] + rk = 0 + ncol = len(m[0]) if m else 0 + for col in range(ncol): + p = next((i for i in range(rk, len(m)) if m[i][col] != 0), None) + if p is None: + continue + m[rk], m[p] = m[p], m[rk] + inv = 1 / m[rk][col] + m[rk] = [a * inv for a in m[rk]] + for i in range(len(m)): + if i != rk and m[i][col] != 0: + f = m[i][col] + m[i] = [a - f * b for a, b in zip(m[i], m[rk])] + piv.append(col) + rk += 1 + return m[:rk], piv + + +def nullspace_int(rows, ncol=8): + """integer basis of {n : r.n = 0 for every row r} (dot product)""" + if not rows: + return [[int(i == j) for j in range(ncol)] for i in range(ncol)] + basis, piv = rref(rows) + free = [c for c in range(ncol) if c not in piv] + out = [] + for f in free: + vec = [Fraction(0)] * ncol + vec[f] = Fraction(1) + for r, pc in zip(basis, piv): + vec[pc] = -r[f] + den = 1 + for x in vec: + den = den * x.denominator // math.gcd(den, x.denominator) + out.append([int(x * den) for x in vec]) + return out + + +def hnf_basis(rows): + """Z-basis of the lattice generated by integer rows (row-style Hermite reduction)""" + m = [list(r) for r in rows if any(r)] + basis = [] + ncol = len(rows[0]) + for col in range(ncol): + m = [r for r in m if any(r)] + while True: + nz = [r for r in m if r[col] != 0] + if len(nz) <= 1: + break + nz.sort(key=lambda r: abs(r[col])) + p = nz[0] + for r in m: + if r is not p and r[col] != 0: + q = r[col] // p[col] + for j in range(ncol): + r[j] -= q * p[j] + nz = [r for r in m if r[col] != 0] + if nz: + basis.append(nz[0]) + m = [r for r in m if r is not nz[0]] + return basis + + +def det(M): + M = [[Fraction(x) for x in r] for r in M] + n = len(M) + d = Fraction(1) + for col in range(n): + p = next((i for i in range(col, n) if M[i][col] != 0), None) + if p is None: + return Fraction(0) + if p != col: + M[col], M[p] = M[p], M[col] + d = -d + d *= M[col][col] + for i in range(col + 1, n): + f = M[i][col] / M[col][col] + M[i] = [a - f * b for a, b in zip(M[i], M[col])] + return d + + +# ------------------------------------------------------------------ the checker +class Word: + def __init__(self, w): + self.w = w + self.v = v = w["v"] + self.R = w["R"] + self.n = 2 * v + self.R + need(w["h"] == 8 and v == 120 and w["form"] == "/2", "not an E8 bit word header") + self.lines = [tuple(int(a) for a in r) for r in w["lines"]] + fr = w["frames"] + self.fdim = [] + self.fperp = [] + for f in fr: + need(all(0 <= i < v for i in f), "frame line out of range") + rows = [self.lines[i] for i in f] + b, _ = rref(rows) if rows else ([], []) + self.fdim.append(len(b)) + self.fperp.append(nullspace_int(rows)) + self.FULL = [k for k, d in enumerate(self.fdim) if d == 8] + self.ZERO = [k for k, d in enumerate(self.fdim) if d == 0] + need(len(self.FULL) == 1 and len(self.ZERO) == 1, "need exactly one full frame and one zero frame id") + self.FULL, self.ZERO = self.FULL[0], self.ZERO[0] + self._nest = {} + + def ip(self, a, b): + s = sum(x * y for x, y in zip(a, b)) + need(s % 2 == 0, "form not integral") + return s // 2 + + def labels(self): + L = self.lines + need(len(L) == 120 and len(set(L)) == 120, "need 120 distinct labels") + need(all(self.ip(a, a) == 2 for a in L), "a label does not have norm 2") + for i in range(120): + for j in range(i + 1, 120): + need(abs(self.ip(L[i], L[j])) <= 1, "two labels on one line") + B = hnf_basis(L) + need(len(B) == 8, "labels do not span rank 8") + G = [[self.ip(a, b) for b in B] for a in B] + need(det(G) == 1, "lattice generated by the labels is not unimodular") + # closure of every frame: the listed lines are exactly the labels inside its span + for k, f in enumerate(self.w["frames"]): + inside = [i for i in range(120) if all(sum(x * y for x, y in zip(L[i], nv)) == 0 for nv in self.fperp[k])] + need(sorted(inside) == sorted(f), "frame %d is not closed" % k) + return dict(labels=120, lattice_rank=8, gram_det=1, frames=len(self.w["frames"])) + + def nested(self, a, b): + """span(frame a) inside span(frame b)""" + k = (a, b) + if k not in self._nest: + ok = all(all(sum(x * y for x, y in zip(self.lines[i], nv)) == 0 for nv in self.fperp[b]) + for i in self.w["frames"][a]) + self._nest[k] = ok + return self._nest[k] + + def replay(self, sections=("D", "A", "scatter", "B", "C"), values=None, frames_on=True): + w, v, n = self.w, self.v, self.n + cur = list(w["start"]) + val = list(values) if values is not None else [1 << r for r in range(n)] + stats = Counter() + + def climb(r, f): + if cur[r] == f: + return + need(self.nested(cur[r], f) and self.fdim[cur[r]] < self.fdim[f], + "climb not nested: register %d from frame %d (dim %d) to frame %d (dim %d)" % + (r, cur[r], self.fdim[cur[r]], f, self.fdim[f])) + cur[r] = f + + def run(name): + for k, g in enumerate(w[name]): + need(len(g) == 3, "malformed gate") + f, d, srcs = g + regs = [d] + list(srcs) + need(0 <= f < len(self.fdim), "frame id out of range") + need(all(0 <= r < n for r in regs) and len(set(regs)) == len(regs) and srcs, + "%s gate %d: bad operands" % (name, k)) + if frames_on: + for r in regs: + climb(r, f) + acc = 0 + for s in srcs: + acc ^= val[s] + val[d] ^= acc + stats[name] += 1 + + if frames_on: + for s in range(v): + need(self.fdim[cur[s]] == 1 and self.w["frames"][cur[s]] == [s], "source %d does not start at its line" % s) + for r in range(v, n): + need(self.fdim[cur[r]] == 0, "target/helper %d does not start at frame 0" % r) + for name in sections: + if name == "scatter": + need(len(w["scatter"]) == v, "scatter must have one row per target") + need(all(0 <= k < len(w["ret"]) for row in w["scatter"] for k in row), "scatter index out of range") + need(all(2 * v <= q < n for q in w["ret"]), "retained totals must be helpers") + if frames_on: + need(all(self.fdim[cur[v + t]] == 0 for t in range(v)), "a target left frame 0 before the scatter") + copies = [val[q] for q in w["ret"]] + for t, row in enumerate(w["scatter"]): + for k in row: + val[v + t] ^= copies[k] + stats["scatter_terms"] = sum(len(r) for r in w["scatter"]) + else: + run(name) + return val, cur, stats + + def full(self): + """the complete program: legality and exact F2 identity on all columns""" + w, v, n = self.w, self.v, self.n + val, cur, stats = self.replay() + for r in range(n): + f = w["final"][r] + if cur[r] != f: + need(self.nested(cur[r], f) and self.fdim[cur[r]] < self.fdim[f], "final climb of %d not nested" % r) + for s in range(v): + need(self.fdim[w["final"][s]] == 8, "source final frame is not full") + for r in range(2 * v, n): + need(self.fdim[w["final"][r]] == 8, "helper final frame is not full") + for t in range(v): + f = w["final"][v + t] + perp = [i for i in range(120) if self.ip(self.lines[i], self.lines[t]) == 0] + need(sorted(w["frames"][f]) == perp, "target %d final frame is not t-perp" % t) + bad_s = [s for s in range(v) if val[s] != 1 << s] + bad_h = [r for r in range(2 * v, n) if val[r] != 1 << r] + bad_t = [t for t in range(v) if val[v + t] != (1 << (v + t)) | (1 << t)] + need(not bad_s, "sources not restored: %s" % bad_s[:5]) + need(not bad_h, "helpers not restored: %s" % bad_h[:5]) + need(not bad_t, "targets not y + x: %s" % bad_t[:5]) + return dict(columns=n, gates={k: stats[k] for k in ("D", "A", "B", "C")}, scatter_terms=stats["scatter_terms"]) + + def interface(self): + """each hypothesis of the interleaved lemma separately, and the decomposition of its conclusion""" + w, v, n = self.w, self.v, self.n + is_y = lambda r: v <= r < 2 * v + is_z = lambda r: not is_y(r) + H = {} + H["H1_no_target_feeds_z"] = not any(is_z(g[1]) and any(is_y(s) for s in g[2]) + for sec in ("D", "A", "B", "C") for g in w[sec]) + H["H2_D_frame0_targets_from_helpers"] = all( + self.fdim[g[0]] == 0 and is_y(g[1]) and all(s >= 2 * v for s in g[2]) for g in w["D"]) and all( + self.fdim[w["start"][r]] == 0 for r in range(v, n)) + H["H3_A_z_only_scatter_targets_B_split"] = ( + all(is_z(g[1]) for g in w["A"]) and all(2 * v <= q < n for q in w["ret"]) and len(w["scatter"]) == v + and all(is_y(g[1]) or all(is_z(s) for s in g[2]) for g in w["B"])) + zg = [[self.FULL, g[1], list(g[2])] for sec in ("A", "B") for g in w[sec] if is_z(g[1])] + H["H4_C_literal_reverse_at_full"] = ([[g[0], g[1], list(g[2])] for g in w["C"]] == list(reversed(zg)) + and all(self.fdim[w["final"][r]] == 8 for r in range(n) if is_z(r))) + # raw word W0 = A, scatter, B (no D, no C), values only + raw, _, _ = self.replay(sections=("A", "scatter", "B"), frames_on=False) + ymask = ((1 << v) - 1) << v + xmask = (1 << v) - 1 + smask = ((1 << self.R) - 1) << (2 * v) + H["H5_V_identity"] = all(raw[v + t] & ymask == 1 << (v + t) for t in range(v)) + C = {} + C["U_block_form"] = all(raw[r] & ymask == 0 for r in range(n) if is_z(r)) + C["J_identity"] = all(raw[v + t] & xmask == 1 << t for t in range(v)) + N = [0] * v + for g in w["D"]: + if is_y(g[1]): + for s in g[2]: + N[g[1] - v] ^= 1 << s + C["K_equals_D"] = all(raw[v + t] & smask == N[t] for t in range(v)) + # C applied to the raw z outputs restores every z register (C = U^-1) + vals = list(raw) + ok = True + for f, d, srcs in w["C"]: + if is_y(d) or any(is_y(s) for s in srcs): + ok = False + break + acc = 0 + for s in srcs: + acc ^= vals[s] + vals[d] ^= acc + C["C_is_U_inverse"] = ok and all(vals[r] == 1 << r for r in range(n) if is_z(r)) + # interleaving statistics + readers = set() + zB = [g for g in w["B"] if is_z(g[1])] + war = 0 # B z-writes into a register some target has already read in B + raw_after = 0 # target reads, in B, of a register already rewritten in B + written = set() + for k, g in enumerate(w["B"]): + if is_z(g[1]): + if g[1] in readers: + war += 1 + written.add(g[1]) + else: + for s in g[2]: + if is_z(s): + if s in written: + raw_after += 1 + readers.add(s) + info = dict(z_gates_A=sum(1 for g in w["A"] if is_z(g[1])), + source_writes_A=sum(1 for g in w["A"] if g[1] < v), + z_gates_B=len(zB), source_writes_B=sum(1 for g in zB if g[1] < v), + helper_writes_B=sum(1 for g in zB if g[1] >= 2 * v), + sources_rewritten_B=len({g[1] for g in zB if g[1] < v}), + B_z_write_frame_dims=dict(sorted(Counter(self.fdim[g[0]] for g in zB).items())), + B_z_operand_kinds=dict(sorted(Counter("%s<-%s" % ("source" if g[1] < v else "helper", "+".join( + sorted({"source" if s < v else "helper" for s in g[2]}))) for g in zB).items())), + B_z_operand_kinds_by_dim=dict(sorted(Counter("dim%d:%s<-%s" % (self.fdim[g[0]], "source" if g[1] < v + else "helper", "+".join(sorted({"source" if s < v else "helper" for s in g[2]}))) + for g in zB).items())), + B_z_writes_after_a_target_read_of_the_same_register=war, + B_target_reads_of_registers_rewritten_earlier_in_B=raw_after, + target_reads_of_targets=sum(1 for g in w["B"] if is_y(g[1]) and any(is_y(s) for s in g[2])), + cleanup_gates=len(w["C"])) + return H, C, info + + +def check(w): + """returns a dict; raises Reject on the first legality or F2 failure""" + W = Word(w) + lab = W.labels() + fl = W.full() + H, C, info = W.interface() + return W, lab, fl, H, C, info + + +if __name__ == "__main__": + w = json.load(gzip.open(sys.argv[1], "rt")) + try: + W, lab, fl, H, C, info = check(w) + except Reject as e: + print("REJECT", e) + sys.exit(1) + print("labels: 120 E8 root lines (even unimodular lattice of rank 8, Gram det 1); %d frames, every one closed" % + lab["frames"]) + print("legality and exact F2 replay on all %d columns (sources, targets, %d dirty helpers as symbolic inputs): " + "PASS; gates D/A/B/C = %s" % (fl["columns"], W.R, "/".join(str(fl["gates"][k]) for k in "DABC"))) + for k, x in list(H.items()) + list(C.items()): + print(" %-40s %s" % (k, "holds" if x else "FAILS")) + print(" " + json.dumps(info)) + ok = all(H.values()) and all(C.values()) + print("PASS interleaved interface lemma: hypotheses H1-H5 hold and the conclusion decomposes as U, J = I, D = K," + " C = U^-1" if ok else "REJECT interface") + if "--json" in sys.argv: + json.dump(dict(status="PASS_EXACT_REPLAY_AND_INTERLEAVED_INTERFACE" if ok else "REJECT", hypotheses=H, + conclusion=C, interleaving=info, gates=fl["gates"], columns=fl["columns"]), + open(sys.argv[sys.argv.index("--json") + 1], "w"), indent=1) + sys.exit(0 if ok else 1) diff --git a/research/r420-rref-production/benchmark.py b/research/r420-rref-production/benchmark.py new file mode 100644 index 0000000000..5cd0a25398 --- /dev/null +++ b/research/r420-rref-production/benchmark.py @@ -0,0 +1,182 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process before/after timings for production integer RREF. + +Timing is descriptive evidence for RESULT.json. Equivalence is enforced by +verify.py; this script fails only on unequal receipts or subprocess errors. +""" +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 +import time + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +WORD = ROOT / "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +MUTANTS = ROOT / "research/e8-bit-r420/code/mutants.py" +BASELINE = PACKAGE / "baseline.py" +PRODUCTION = ROOT / "research/e8-bit-r420/code/xcheck.py" + +CHECK_STDOUT_SHA256 = "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" +MUTANTS_STDOUT_SHA256 = "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + + +def clean_env(): + env = {k: v for k, v in os.environ.items() if k != "PYTHONOPTIMIZE"} + env["PYTHONDONTWRITEBYTECODE"] = "1" + return env + + +def run_workload(engine: str, suite: str) -> dict: + script = BASELINE if engine == "baseline" else PRODUCTION + if suite == "check": + cmd = [sys.executable, "-I", "-B", str(script), str(WORD)] + expected = CHECK_STDOUT_SHA256 + elif suite == "controls": + cmd = [sys.executable, "-I", "-B", str(MUTANTS), str(script), str(WORD)] + expected = MUTANTS_STDOUT_SHA256 + else: + raise SystemExit(f"unknown suite {suite}") + start = time.perf_counter() + proc = subprocess.run(cmd, cwd=ROOT, env=clean_env(), capture_output=True) + elapsed = time.perf_counter() - start + if proc.returncode != 0: + raise SystemExit(f"{engine}/{suite} failed\n{proc.stderr.decode()}\n{proc.stdout.decode()}") + digest = sha256(proc.stdout).hexdigest() + if digest != expected: + raise SystemExit(f"{engine}/{suite} stdout digest {digest} != {expected}") + return {"elapsed": elapsed, "stdout_sha256": digest, "stdout_bytes": len(proc.stdout)} + + +def unique_object(pairs): + out = {} + for key, value in pairs: + if key in out: + raise SystemExit(f"duplicate JSON key: {key}") + out[key] = value + return out + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument( + "--write-result", + action="store_true", + help="write RESULT.json (default prints only; use explicitly to refresh the artifact)", + ) + args = parser.parse_args(argv) + if args.rounds < 3: + raise SystemExit("Use at least three alternating rounds") + + workloads = {} + for suite in ("check", "controls"): + records = [] + for pair in range(args.rounds): + order = ("baseline", "production") if pair % 2 == 0 else ("production", "baseline") + outputs = {} + for engine in order: + row = run_workload(engine, suite) + records.append( + { + "pair": pair, + "engine": engine, + "seconds": row["elapsed"], + "stdout_sha256": row["stdout_sha256"], + } + ) + outputs[engine] = row["stdout_sha256"] + if outputs["baseline"] != outputs["production"]: + raise SystemExit(f"pair {pair} suite {suite} receipts differ") + medians = { + engine: statistics.median(r["seconds"] for r in records if r["engine"] == engine) + for engine in ("baseline", "production") + } + workloads[suite] = { + "records": records, + "median_seconds": medians, + "speedup": medians["baseline"] / medians["production"], + } + + result = { + "status": "PASS_IDENTICAL_R420_RREF_PRODUCTION_RECEIPTS", + "no_new_kappa": True, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "python": sys.version, + "platform": platform.platform(), + "machine": platform.machine(), + "interpreter": f"CPython {platform.python_version()}", + "rounds": args.rounds, + "timing_scope": ( + "fresh subprocess wall time including imports; warm OS caches, not flushed; " + "host-descriptive only; not a correctness gate" + ), + "workloads": workloads, + "suite_median_seconds": { + "baseline": statistics.median( + [ + workloads["check"]["median_seconds"]["baseline"], + workloads["controls"]["median_seconds"]["baseline"], + ] + ), + # Not a combined suite wall; retained for readability alongside per-workload medians. + }, + "check_speedup": workloads["check"]["speedup"], + "controls_speedup": workloads["controls"]["speedup"], + "production_xcheck_sha256": sha256(PRODUCTION.read_bytes()).hexdigest(), + "baseline_xcheck_sha256": sha256(BASELINE.read_bytes()).hexdigest(), + } + + # Combined alternating wall for check+controls in one process pair is not claimed; + # report the product of the two medians only as a descriptive sum of stage medians. + result["stage_median_sum_seconds"] = { + "baseline": ( + workloads["check"]["median_seconds"]["baseline"] + + workloads["controls"]["median_seconds"]["baseline"] + ), + "production": ( + workloads["check"]["median_seconds"]["production"] + + workloads["controls"]["median_seconds"]["production"] + ), + } + result["stage_median_sum_speedup"] = ( + result["stage_median_sum_seconds"]["baseline"] + / result["stage_median_sum_seconds"]["production"] + ) + + text = json.dumps(result, indent=2, sort_keys=True) + "\n" + # Reject duplicate keys if re-parsed. + json.loads(text, object_pairs_hook=unique_object) + if args.write_result: + (PACKAGE / "RESULT.json").write_text(text, encoding="utf-8") + print(result["status"]) + print( + "check", + workloads["check"]["median_seconds"], + "speedup", + round(workloads["check"]["speedup"], 3), + ) + print( + "controls", + workloads["controls"]["median_seconds"], + "speedup", + round(workloads["controls"]["speedup"], 3), + ) + print( + "stage_median_sum", + result["stage_median_sum_seconds"], + "speedup", + round(result["stage_median_sum_speedup"], 3), + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/r420-rref-production/verify.py b/research/r420-rref-production/verify.py new file mode 100644 index 0000000000..6508300853 --- /dev/null +++ b/research/r420-rref-production/verify.py @@ -0,0 +1,266 @@ +#!/usr/bin/env python3 +"""Equivalence, rejection and receipt controls for production integer RREF. + +Read-only by default. Timing is not a pass gate; see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +import copy +import gzip +import hashlib +from hashlib import sha256 +import importlib.util +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +from fractions import Fraction + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +PRODUCTION = ROOT / "research/e8-bit-r420/code/xcheck.py" +BASELINE = PACKAGE / "baseline.py" +WORD = ROOT / "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +MUTANTS = ROOT / "research/e8-bit-r420/code/mutants.py" +MANIFEST = ROOT / "research/e8-bit-r420/MANIFEST.sha256" + +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ORIGINAL_BLOB = "fbff8607e4c61e18481f696b99dd38a32444e90d" +ORIGINAL_SHA256 = "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" +OPTIMIZED_SHA256 = "cd1d91b32831b4bd75290edf8b19f3a4378c5733bf4755ba59ed5161e2c468b9" +CHECK_STDOUT_SHA256 = "e4637c1fe38b10fb82e0e4f710a28821e980f629ad3e22b51c1e75b3cdf40acd" +MUTANTS_STDOUT_SHA256 = "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8" + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def unique_object(pairs): + out = {} + for key, value in pairs: + require(key not in out, f"duplicate JSON key: {key}") + out[key] = value + return out + + +def load_json_unique(path: Path): + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_object) + + +def load_module(path: Path, name: str): + spec = importlib.util.spec_from_file_location(name, path) + require(spec is not None and spec.loader is not None, f"missing module {path}") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def clean_env(): + env = {k: v for k, v in os.environ.items() if k != "PYTHONOPTIMIZE"} + env["PYTHONDONTWRITEBYTECODE"] = "1" + return env + + +def run_xcheck(script: Path) -> bytes: + proc = subprocess.run( + [sys.executable, "-I", "-B", str(script), str(WORD)], + cwd=ROOT, + env=clean_env(), + capture_output=True, + ) + require(proc.returncode == 0, f"{script.name} failed\n{proc.stderr.decode()}\n{proc.stdout.decode()}") + return proc.stdout + + +def run_mutants(script: Path) -> bytes: + proc = subprocess.run( + [sys.executable, "-I", "-B", str(MUTANTS), str(script), str(WORD)], + cwd=ROOT, + env=clean_env(), + capture_output=True, + ) + require( + proc.returncode == 0, + f"mutants against {script.name} failed\n{proc.stderr.decode()}\n{proc.stdout.decode()}", + ) + return proc.stdout + + +def check_baseline_bytes() -> None: + original = subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:research/e8-bit-r420/code/xcheck.py"], + cwd=ROOT, + ) + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base xcheck.py sha256 drift") + blob = ( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:research/e8-bit-r420/code/xcheck.py"], + cwd=ROOT, + ) + .decode() + .strip() + ) + require(blob == ORIGINAL_BLOB, "base xcheck.py blob drift") + require(BASELINE.read_bytes() == original, "baseline.py must equal the base-commit xcheck.py") + require( + digest_file(PRODUCTION) == OPTIMIZED_SHA256, + "production xcheck.py does not match the claimed optimized digest", + ) + require(PRODUCTION.read_bytes() != original, "production must differ from the Fraction baseline") + + +def check_manifest_binds_production() -> None: + listed = {} + for line in MANIFEST.read_text(encoding="utf-8").splitlines(): + digest, path = line.split(" ", 1) + require(path not in listed, f"duplicate MANIFEST path: {path}") + listed[path] = digest + require(listed.get("code/xcheck.py") == OPTIMIZED_SHA256, "MANIFEST.sha256 must bind production xcheck.py") + actual = digest_file(ROOT / "research/e8-bit-r420" / "code/xcheck.py") + require(actual == OPTIMIZED_SHA256, "live xcheck.py drifted from OPTIMIZED_SHA256") + + +def check_frame_rref_equivalence(baseline, production) -> dict: + with gzip.open(WORD, "rt", encoding="utf-8") as handle: + # gzip JSON is a single object without duplicate keys in this fixture. + word = json.load(handle) + frames = word["frames"] + lines = word["lines"] + compared = 0 + for frame in frames: + rows = [lines[i] for i in frame] + before = copy.deepcopy(rows) + left = baseline.rref(rows) + right = production.rref(rows) + require(left == right, "frame RREF/pivot mismatch") + require(rows == before, "rref mutated its input rows") + require(all(isinstance(x, Fraction) for row in right[0] for x in row), "RREF type changed") + ns_l = baseline.nullspace_int(rows) + ns_r = production.nullspace_int(rows) + require(ns_l == ns_r, "integer annihilator basis changed") + require(len(ns_r) == 8 - len(right[1]), "rank/nullity mismatch") + require( + all(sum(x * y for x, y in zip(row, n)) == 0 for row in rows for n in ns_r), + "annihilator dot product is not zero", + ) + compared += 1 + # Supplemental rational / empty / dependent cases (same spirit as the opt-in adapter). + extras = [ + [], + [[0, -2, 3], [0, 4, -6]], + [[0, 0, 1], [0, -3, 2]], + [[2, 1, 1], [0, 3, 1]], + [[Fraction(1, 3), Fraction(2, 7)], [Fraction(2, 3), Fraction(4, 7)]], + ] + for rows in extras: + before = copy.deepcopy(rows) + left = baseline.rref(rows) + right = production.rref(rows) + require(left == right and rows == before, "supplemental RREF mismatch or mutation") + compared += 1 + return {"frames": len(frames), "matrices_compared": compared} + + +def check_stdout_equivalence() -> dict: + base_check = run_xcheck(BASELINE) + prod_check = run_xcheck(PRODUCTION) + require(base_check == prod_check, "complete check stdout differs") + require(sha256(prod_check).hexdigest() == CHECK_STDOUT_SHA256, "check stdout digest drift") + base_mut = run_mutants(BASELINE) + prod_mut = run_mutants(PRODUCTION) + require(base_mut == prod_mut, "mutation-harness stdout differs") + require(sha256(prod_mut).hexdigest() == MUTANTS_STDOUT_SHA256, "mutants stdout digest drift") + require(b"PASS interleaved interface lemma" in prod_check, "missing interface lemma marker") + require(b"PASS mutation controls: 9/9" in prod_mut, "missing mutation control marker") + return { + "check_stdout_sha256": CHECK_STDOUT_SHA256, + "mutants_stdout_sha256": MUTANTS_STDOUT_SHA256, + "check_bytes": len(prod_check), + "mutants_bytes": len(prod_mut), + } + + +def check_temp_corruption_rejection() -> dict: + """On-disk foil that flips the elimination sign must diverge from the honest RREF.""" + production = load_module(PRODUCTION, "xcheck_production_live") + with gzip.open(WORD, "rt", encoding="utf-8") as handle: + word = json.load(handle) + # Frame 127 needs reduced cleanup; sign-flip also breaks simpler frames. + sample = [word["lines"][i] for i in word["frames"][127]] + honest = production.rref(sample) + with tempfile.TemporaryDirectory(prefix="r420-rref-prod-") as tmp: + mutant_path = Path(tmp) / "xcheck.py" + text = PRODUCTION.read_text(encoding="utf-8") + needle = "rows[i] = _primitive([a * x - b * y for x, y in zip(row, base)])" + require(needle in text, "elimination update line missing for corruption control") + foil = "rows[i] = _primitive([a * x + b * y for x, y in zip(row, base)]) # foil: wrong sign" + mutant_path.write_text(text.replace(needle, foil, 1), encoding="utf-8") + require(mutant_path.read_bytes() != PRODUCTION.read_bytes(), "mutant must differ on disk") + mutant = load_module(mutant_path, "xcheck_production_mutant") + bad = mutant.rref(sample) + require(bad != honest, "sign-flip foil must change the sample RREF") + # Complete checker against the foil must either reject or print a different receipt. + try: + foil_out = run_xcheck(mutant_path) + honest_out = run_xcheck(PRODUCTION) + require(foil_out != honest_out, "foil accepted with identical complete stdout") + return {"rejected": True, "mode": "stdout_divergence"} + except AssertionError as exc: + return {"rejected": True, "mode": "subprocess_failure", "detail": str(exc)[:240]} + + +def check_o_policy_children() -> None: + """Package require() gates still launch assertion-enabled children under -O.""" + # The production/baseline checkers themselves may use assertions in mutants.py; + # children are always launched with -I -B and without PYTHONOPTIMIZE. + out = run_xcheck(PRODUCTION) + require(sha256(out).hexdigest() == CHECK_STDOUT_SHA256, "-O parent still gets assertion-enabled child") + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write-result", + action="store_true", + help="unused placeholder; default verify is read-only and never writes certificates", + ) + args = parser.parse_args(argv) + require(not args.write_result, "default verify is read-only; do not pass --write-result") + + check_baseline_bytes() + check_manifest_binds_production() + baseline = load_module(BASELINE, "xcheck_baseline") + production = load_module(PRODUCTION, "xcheck_production") + algebra = check_frame_rref_equivalence(baseline, production) + receipts = check_stdout_equivalence() + corruption = check_temp_corruption_rejection() + check_o_policy_children() + + # Duplicate-key guard on RESULT.json when present (read-only). + result_path = PACKAGE / "RESULT.json" + if result_path.exists(): + load_json_unique(result_path) + + print( + "PASS_R420_RREF_PRODUCTION " + f"frames={algebra['frames']} " + f"matrices={algebra['matrices_compared']} " + f"corruption={corruption['mode']} " + f"check_sha={receipts['check_stdout_sha256'][:12]} " + "certs=0 no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/r420-triple-bases-seed01/README.md b/research/r420-triple-bases-seed01/README.md index 7bd8f135b3..209597c890 100644 --- a/research/r420-triple-bases-seed01/README.md +++ b/research/r420-triple-bases-seed01/README.md @@ -185,3 +185,5 @@ Prepared for **Sagar Thakrar (@thakrarsagar)** with substantial **OpenAI Codex assistance** in research, proof, implementation, verification and writing. One agent; separate implementations are not independent human review. New work is Apache-2.0, preserving predecessor licenses and attribution. + +After production promotion of `xcheck.rref` (`research/r420-rref-production/`), the historical Fraction-era `research/e8-bit-r420/code/xcheck.py` digest is pinned as **provenance** only and is no longer a live VERIFY input. diff --git a/research/r420-triple-bases-seed01/SOURCES.json b/research/r420-triple-bases-seed01/SOURCES.json index 98496793a5..cf5f711372 100644 --- a/research/r420-triple-bases-seed01/SOURCES.json +++ b/research/r420-triple-bases-seed01/SOURCES.json @@ -28,7 +28,7 @@ }, { "path": "research/e8-bit-r420/code/xcheck.py", - "usage": "input", + "usage": "provenance", "git_blob": "fbff8607e4c61e18481f696b99dd38a32444e90d", "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" }, diff --git a/research/r420-triple-bases-seed01/VERIFY.json b/research/r420-triple-bases-seed01/VERIFY.json index 75b97e6709..221c7058b2 100644 --- a/research/r420-triple-bases-seed01/VERIFY.json +++ b/research/r420-triple-bases-seed01/VERIFY.json @@ -6,7 +6,6 @@ "inputs": [ "research/e8-bit-carrier-skeleton/code/bit/export_records.py", "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", - "research/e8-bit-r420/code/xcheck.py", "research/e8-bit-r420/data/bitE8mut-r420.json.gz", "research/r420-decoder-sharing/audit.py", "research/r420-decoder-sharing/verify.py"