diff --git a/research/r420-geometry-cache/CLAIM.md b/research/r420-geometry-cache/CLAIM.md new file mode 100644 index 0000000000..864c57fbc4 --- /dev/null +++ b/research/r420-geometry-cache/CLAIM.md @@ -0,0 +1,47 @@ +# Verification-engineering claim: seed 91 + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`, freshly fetched main. +OS randomness `secrets.randbelow(100)` returned **91**, selecting verification +engineering. This is a second, independent contribution by @mtpsl with +substantial OpenAI Codex assistance; it does not depend on PR691. + +Three narrow candidates: + +0. Accelerate exact moment intervals. PR667/672 already address this area. +1. Cache repeated validated E8 geometry in PR543's mutation verifier. +2. Replace the repeated Fraction row reductions in one E8 frame initializer. + +Choose `91 mod 3 = 1`: a bounded in-process geometry cache, preserving the +original arithmetic and all per-word checks. The exact geometry/header input +must be part of the key; no persisted cache or unchecked old certificate. +Expected deliverable: an opt-in adapter, same-input A/B benchmark, exact receipt +comparison and cache invalidation/aliasing controls. No frontier change. + +Baseline observation: the original nine-negative/one-positive mutation suite, +including its initial valid word, took 8.120 seconds locally. The experiment +will rerun this same suite through each implementation and compare receipts. +Stop after one implementation and bounded targeted verification. Expected finish: +2026-10-13 12:55 Asia/Singapore; reserve the last quarter for verification/handoff. + +No pinned coordination issue exists (GitHub pinnedIssues query returned empty). +Open issues contain only the unrelated Discussions request #650. PRs checked +through #700. The review ledger marks PR452 (older PR358 prefix/arithmetic +adapters) unreviewed; it is not a dependency. PR662 concerns complex Clifford +helpers, not this E8 label/frame audit. PR661's frame-search negative result +does not concern verifier performance. PR667/672 address interval arithmetic. +The selected PR626 certificate, its actual PR543 supplier and review, and the +repository contribution instructions remain as established at the recorded base. + +Result: **completed tooling improvement**, submitted as +[PR709](https://github.com/CrocSwap/integer-mult-bounds/pull/709). +The same original mutation suite takes 8.239 s uncached and 1.273 s cached +(6.47x) in the recorded local pair. Complete diagnostics match byte for byte; +receipts, all ten original controls and twenty supplemental checks agree. +The adapter is optional, bounded and source-pinned. No existing verifier, +selected construction or upstream file changes; no new kappa. + +The pre-submission metadata refresh reached #704 with no overlapping PR543 +geometry-cache task. Main still equals the recorded base. Evidence, source pins, +reproduction command, dependency argument and limits are in this package. +This is the single result update to the local claim; no coordination thread +was available. diff --git a/research/r420-geometry-cache/README.md b/research/r420-geometry-cache/README.md new file mode 100644 index 0000000000..bd3989dd7d --- /dev/null +++ b/research/r420-geometry-cache/README.md @@ -0,0 +1,139 @@ +# Cache exact E8 geometry across PR543 mutation checks + +**Verification tooling; no mathematical construction or kappa change.** This +opt-in adapter speeds up the unmodified PR543 mutation harness by reusing a +previously validated E8 label/frame calculation for exactly matching inputs. +Every word still receives the predecessor's full scalar, frame-path, dirty +restoration and H1–H5/interface checks. + +On macOS arm64 / Python 3.12.3, one sequential, same-input A/B took +**8.239 seconds → 1.273 seconds (6.47× faster, 84.5% less wall time)**. +Both runs started separate processes with empty application caches. The original +and cached runs produced byte-identical diagnostics and equal complete JSON +receipts: all nine negative controls reject for the same reasons and the positive +control passes. OS caches were not flushed. This measures only this mutation +suite, not the full supplier pipeline; timings are diagnostic, not test thresholds. + +## Reproduce + +From the repository root, Python 3.10+ and its standard library: + +```sh +python3 -I -B research/r420-geometry-cache/verify.py +``` + +Expected first result line: + +```text +PASS_R420_GEOMETRY_CACHE original_controls=10 supplemental_checks=20 +``` + +The next line reports freshly measured A/B timings. The command runs one +original/cached pair on the exact same word and unchanged mutation harness, +compares receipts and full diagnostics, then checks twenty cache-specific cases. +`--output /absolute/new/directory` retains both logs, receipts and `RESULT.json`; +the directory must not already exist. Without it, scratch outputs are temporary. +The recorded run is in `evidence/RESULT.json` and the adjacent logs/receipts. + +Use the adapter directly with the existing harness: + +```sh +python3 -I -B research/e8-bit-r420/code/mutants.py \ + research/r420-geometry-cache/cached_xcheck.py \ + research/e8-bit-r420/data/bitE8mut-r420.json.gz +``` + +The adapter exposes the same `check(word)` and `Reject` API consumed by that +harness. It returns the predecessor's six-item result; as with the original API, +callers must inspect **all hypothesis and conclusion booleans**, not just absence +of an exception. It is an importable adapter, not a standalone verifier CLI. +`GeometryCache(capacity=2)` also permits an explicitly owned cache for a sequence +of checks. The default holds at most two geometry entries, in memory only. + +## What is reused, and why it is sound + +`cached_xcheck.py` checks the exact SHA-256 of the unchanged predecessor source +before importing it. It refuses source drift; a later checker must be reviewed +for changed data dependencies before changing this pin. + +For the pinned implementation, `Word.__init__` and `labels()` read only these +word fields: `h`, `v`, `R`, `form`, `lines`, `frames`. The cache key is their full +JSON serialization, preserving list order, duplicates and numeric representations. +It is **not a digest**, a filename, an object identity, a dimensions-only key or +an assumed E8 catalogue. Equal keys therefore have equal JSON input values for +every cached calculation. This adapter is scoped to ordinary finite JSON data, +as loaded from the word files, and sequential calls in one process. + +On a miss, the original exact constructor and label/frame-closure audit run. +Only successful geometry is retained. The cache stores immutable tuples of the +derived geometry and the label receipt. On every call, including a hit, it +creates a fresh original `Word`, supplies the current complete word, copies the +derived geometry into fresh mutable containers and clears per-word nesting +memoization. It then calls the unchanged `full()` and `interface()` methods. +No scalar execution result or successful whole-word verdict is cached. + +The label audit covers exact root norms, pair inner products, even-unimodular +lattice rank/determinant and closure of every listed frame. These obligations +have identical inputs on a hit. Every obligation that depends on the current +gates, starts, finals, retained totals or scatter is rerun. Geometry validated +for a word whose later scalar check fails may be retained: the scalar result is +not part of the cached evidence and cannot suppress the next word's replay. + +Returned `Word` objects and receipts share no mutable derived data with the +cache. Changing a caller-owned input is detected by the next key computation; +changing a previously returned result cannot poison the next check. Capacity +eviction causes full geometry validation on the next miss. There is no disk +cache, concurrent-call guarantee, approximate arithmetic or trusted old receipt. + +These statements are a code-dependency argument for this pinned finite checker, +not a formal proof of the integer-multiplication theorem. + +## Verification and boundaries + +The original suite checks its valid baseline plus nine negatives and one positive. +Additional checks compare exact outcomes and derived geometry against uncached +execution, including failure reasons: + +- Eight cache-hit corruptions: start, final, A, B, C, D, retained totals, scatter. +- Six geometry changes: h, v, R, form, a label, and an unclosed full frame. +- Repeated failed geometry, a valid reflected E8 geometry, returned-result + mutation, in-place input mutation, capacity-one eviction and source-pin drift. + +The two successful geometry variants also compare the full derived geometry and +all predecessor receipts. Source drift is tested by relocating the unchanged +adapter beside altered predecessor bytes; it must refuse to import. +`make selected-record-check` and staged whitespace validation pass. + +Only this new research package changes. No existing verifier, manifest, selected +certificate or `upstream/` byte is edited. The complete repository suite, selected +cold replay, hosted invoices, moment engines, Lean and remote CI were not run; +this is an isolated, optional acceleration of one existing finite check. +The inherited all-size, compiler, physical/common-label, hosting, precision, +tape and analytic assumptions remain untouched. No new kappa or end-to-end +supplier speedup is claimed. + +## Provenance and credit + +Base main: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +PR543 supplier: `2065fe4f72a914d907f1046603f5a36f17018535`. +`SOURCES.json` pins the exact three execution inputs by SHA-256 and Git blob. +The selected PR626 composition still uses conditional +`kappa=51110230636731/31250000000000000`. + +**Eumemic** supplied PR543's `xcheck.py`, mutation suite and R420 word, with +substantial Anthropic Claude assistance. The original geometry, construction, +dirty interface and mutation coverage are theirs. Credit also remains with +PR493, Dylan Crow's E8 checker/decoder work, Jacob Sussman's E8 unit, Zhihao +Chen's scalar interface, DreamingOfClouds' supplier/pricing work, and the complete +lineage in [`research/e8-bit-r420/NOTICE.md`](../e8-bit-r420/NOTICE.md). + +PR452 (Aman) studies older PR358 prefix and arithmetic reuse; PR662 accelerates +complex Clifford helper checks; PR667/672 concern interval arithmetic. Those +distinct performance contributions are not imported or independently reviewed +here. PR691 is our separate circuit contribution and is not a dependency. +The seed-91 claim and overlap checks are recorded in `CLAIM.md`. + +Prepared for **@mtpsl with substantial OpenAI Codex assistance** in implementing +the cache, analyzing dependencies, testing and packaging. No independent human +review is claimed. New files are Apache-2.0 under the repository's LICENSE; +predecessor attribution and files are preserved unchanged. diff --git a/research/r420-geometry-cache/SOURCES.json b/research/r420-geometry-cache/SOURCES.json new file mode 100644 index 0000000000..615227700a --- /dev/null +++ b/research/r420-geometry-cache/SOURCES.json @@ -0,0 +1,18 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source_pr543_commit": "2065fe4f72a914d907f1046603f5a36f17018535", + "execution_inputs": { + "research/e8-bit-r420/code/xcheck.py": { + "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "git_blob": "fbff8607e4c61e18481f696b99dd38a32444e90d" + }, + "research/e8-bit-r420/code/mutants.py": { + "sha256": "e2fd3429e2db4389ae8a5ab47dda89f551b0d0952c42fad5ac8d38a85d670594", + "git_blob": "5b0fa1922076d2e91367b58483c96b33b7b08661" + }, + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": { + "sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "git_blob": "0c63ca62759dc63d302be6552aeeee1ede70350f" + } + } +} diff --git a/research/r420-geometry-cache/VALIDATION.json b/research/r420-geometry-cache/VALIDATION.json new file mode 100644 index 0000000000..7a5e3dddd2 --- /dev/null +++ b/research/r420-geometry-cache/VALIDATION.json @@ -0,0 +1,35 @@ +{ + "status": "PASS_SCOPED_CACHE_TOOLING", + "platform": { + "machine": "arm64", + "platform": "Darwin", + "python": "3.12.3" + }, + "paired_run": { + "command": "python3 -I -B research/r420-geometry-cache/verify.py --output ../geometry-cache-validation", + "result": "PASS_R420_GEOMETRY_CACHE original_controls=10 supplemental_checks=20", + "benchmark": { + "cached_seconds": 1.2731981249526143, + "method": "one original-then-cached pair, separate cold processes, identical harness/input; OS caches not flushed", + "original_seconds": 8.238810583017766, + "speedup": 6.470957207327333 + } + }, + "additional_checks": [ + "make selected-record-check: PASS", + "direct adapter CLI refuses to masquerade as verification: PASS", + "staged git diff --check: PASS" + ], + "notes": [ + "Final direct-CLI guard added after the paired run; targeted CLI guard check passes. Imported cache implementation is unchanged.", + "Original and cached mutation diagnostics match byte for byte; complete JSON receipts match.", + "No source or mathematical files outside this new package changed." + ], + "not_run": [ + "full repository suite", + "selected cold replay", + "hosted invoices and moment engines", + "Lean", + "remote CI" + ] +} diff --git a/research/r420-geometry-cache/cached_xcheck.py b/research/r420-geometry-cache/cached_xcheck.py new file mode 100644 index 0000000000..dfeee952ef --- /dev/null +++ b/research/r420-geometry-cache/cached_xcheck.py @@ -0,0 +1,94 @@ +"""Opt-in, bounded geometry reuse for the pinned PR543 exact checker. + +Only Word.__init__ and labels() results are reused. full() and interface() +always run on a fresh Word instance. No persistent cache or approximate math. +Prepared for mtpsl with substantial OpenAI Codex assistance; Apache-2.0. +""" +from collections import OrderedDict +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/e8-bit-r420/code/xcheck.py" +PIN = "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" +if hashlib.sha256(SOURCE.read_bytes()).hexdigest() != PIN: + raise RuntimeError("pinned xcheck source changed; review cache dependencies before use") +spec = importlib.util.spec_from_file_location("r420_original_xcheck", SOURCE) +original = importlib.util.module_from_spec(spec) +spec.loader.exec_module(original) +Reject = original.Reject + +# Complete data dependencies of the pinned Word.__init__ and labels methods. +GEOMETRY_FIELDS = ("h", "v", "R", "form", "lines", "frames") + + +class GeometryCache: + def __init__(self, capacity=2): + if type(capacity) is not int or capacity < 1: + raise ValueError("capacity must be a positive integer") + self.capacity = capacity + self._entries = OrderedDict() + self.hits = 0 + self.misses = 0 + + def check(self, word): + # The full serialization, not its hash, is the equality key. Preserve + # array order, duplicate entries and raw numeric types. No normalization + # of labels or frames may hide invalid input from the original checker. + key = json.dumps({field: word[field] for field in GEOMETRY_FIELDS}, + sort_keys=True, separators=(",", ":"), allow_nan=False) + if key in self._entries: + self.hits += 1 + snapshot = self._entries.pop(key) + self._entries[key] = snapshot + else: + self.misses += 1 + checked = original.Word(word) + labels = checked.labels() # Failures never populate the cache. + snapshot = ( + checked.v, checked.R, checked.n, tuple(checked.lines), + tuple(checked.fdim), + tuple(tuple(tuple(row) for row in frame) for frame in checked.fperp), + checked.FULL, checked.ZERO, tuple(labels.items()), + ) + self._entries[key] = snapshot + if len(self._entries) > self.capacity: + self._entries.popitem(last=False) + + # Never return the cached mutable Word or share mutable derived data + # with it. In particular, caller mutation of a previous result cannot + # poison a later geometry hit. Per-word nesting memoization starts empty. + obj = original.Word.__new__(original.Word) + obj.w = word + obj.v, obj.R, obj.n = snapshot[:3] + obj.lines = list(snapshot[3]) + obj.fdim = list(snapshot[4]) + obj.fperp = [[list(row) for row in frame] for frame in snapshot[5]] + obj.FULL, obj.ZERO = snapshot[6:8] + obj._nest = {} + labels = dict(snapshot[8]) + full = obj.full() + hypotheses, conclusion, info = obj.interface() + return obj, labels, full, hypotheses, conclusion, info + + +_cache = GeometryCache() + + +def check(word): + """Drop-in check/Reject API for PR543's unchanged mutants.py harness.""" + return _cache.check(word) + + +def cache_info(): + return {"hits": _cache.hits, "misses": _cache.misses, + "entries": len(_cache._entries), "capacity": _cache.capacity} + + +if __name__ == "__main__": + raise SystemExit("This is a check/Reject adapter, not a verifier CLI. Run the package's verify.py or pass this file to PR543 mutants.py.") diff --git a/research/r420-geometry-cache/evidence/RESULT.json b/research/r420-geometry-cache/evidence/RESULT.json new file mode 100644 index 0000000000..f684cc0c77 --- /dev/null +++ b/research/r420-geometry-cache/evidence/RESULT.json @@ -0,0 +1,188 @@ +{ + "baseline_signature_sha256": "1a7b6a226622abe3c71ae8cf1cc43786d74342d66de9f9a2ea30c1a45f7d4a47", + "benchmark": { + "cached_seconds": 1.2731981249526143, + "method": "one original-then-cached pair, separate cold processes, identical harness/input; OS caches not flushed", + "original_seconds": 8.238810583017766, + "speedup": 6.470957207327333 + }, + "environment": { + "machine": "arm64", + "platform": "Darwin", + "python": "3.12.3" + }, + "mutation_diagnostics_sha256": "8c2738b3258e207370597b60c2ebd318e740fc0feaca04cb8b0e3a26089258d8", + "mutation_receipt_sha256": "cc18428af7bcb22e6088f3fc88de7206146050d9f3a09f1e367fcb8178d6e703", + "source_pins": { + "research/e8-bit-r420/code/mutants.py": { + "git_blob": "5b0fa1922076d2e91367b58483c96b33b7b08661", + "sha256": "e2fd3429e2db4389ae8a5ab47dda89f551b0d0952c42fad5ac8d38a85d670594" + }, + "research/e8-bit-r420/code/xcheck.py": { + "git_blob": "fbff8607e4c61e18481f696b99dd38a32444e90d", + "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" + }, + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": { + "git_blob": "0c63ca62759dc63d302be6552aeeee1ede70350f", + "sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784" + } + }, + "status": "PASS_R420_GEOMETRY_CACHE", + "supplemental_checks": [ + { + "accepted": false, + "cache_miss": false, + "case": "start frame", + "outcome": { + "accepted": false, + "exception": "target/helper 240 does not start at frame 0" + } + }, + { + "accepted": false, + "cache_miss": false, + "case": "final frame", + "outcome": { + "accepted": false, + "exception": "final climb of 240 not nested" + } + }, + { + "accepted": false, + "cache_miss": false, + "case": "A gate", + "outcome": { + "accepted": false, + "exception": "helpers not restored: [240]" + } + }, + { + "accepted": false, + "cache_miss": false, + "case": "B gate", + "outcome": { + "accepted": false, + "exception": "targets not y + x: [0]" + } + }, + { + "accepted": false, + "cache_miss": false, + "case": "C cleanup", + "outcome": { + "accepted": false, + "exception": "sources not restored: [11, 41, 44, 83, 86]" + } + }, + { + "accepted": false, + "cache_miss": false, + "case": "D compensation", + "outcome": { + "accepted": false, + "exception": "targets not y + x: [0]" + } + }, + { + "accepted": false, + "cache_miss": false, + "case": "retained totals", + "outcome": { + "accepted": false, + "exception": "targets not y + x: [1, 2, 4, 7, 8]" + } + }, + { + "accepted": false, + "cache_miss": false, + "case": "scatter", + "outcome": { + "accepted": false, + "exception": "targets not y + x: [0]" + } + }, + { + "accepted": false, + "cache_miss": true, + "case": "changed h", + "outcome": { + "accepted": false, + "exception": "not an E8 bit word header" + } + }, + { + "accepted": false, + "cache_miss": true, + "case": "changed v", + "outcome": { + "accepted": false, + "exception": "not an E8 bit word header" + } + }, + { + "accepted": false, + "cache_miss": true, + "case": "changed R", + "outcome": { + "accepted": false, + "exception": "D gate 0: bad operands" + } + }, + { + "accepted": false, + "cache_miss": true, + "case": "changed form", + "outcome": { + "accepted": false, + "exception": "not an E8 bit word header" + } + }, + { + "accepted": false, + "cache_miss": true, + "case": "changed label", + "outcome": { + "accepted": false, + "exception": "form not integral" + } + }, + { + "accepted": false, + "cache_miss": true, + "case": "nonclosed full frame", + "outcome": { + "accepted": false, + "exception": "frame 1 is not closed" + } + }, + { + "accepted": false, + "case": "failed geometry is not cached" + }, + { + "accepted": true, + "cache_miss": true, + "case": "valid reflected E8 labels", + "outcome": { + "accepted": true, + "signature_sha256": "e60de9aa9f4a1e9d8def7dee4f7f8b881455653fc28ca4a53ac9cca99696a9f9" + } + }, + { + "accepted": true, + "case": "returned geometry and receipt mutation" + }, + { + "accepted": false, + "case": "in-place source input mutation" + }, + { + "accepted": true, + "case": "capacity-one eviction and revalidation" + }, + { + "accepted": false, + "case": "changed predecessor source pin" + } + ] +} diff --git a/research/r420-geometry-cache/evidence/cached.json b/research/r420-geometry-cache/evidence/cached.json new file mode 100644 index 0000000000..b25c426e6b --- /dev/null +++ b/research/r420-geometry-cache/evidence/cached.json @@ -0,0 +1,65 @@ +{ + "status": "PASS_INTERLEAVED_INTERFACE_MUTATION_CONTROLS", + "controls": [ + { + "control": "m1", + "mutation": "target feeds a source (cancelled pair, F2-neutral)", + "rejected": true, + "by": "interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full" + }, + { + "control": "m2", + "mutation": "target feeds a helper (cancelled pair, F2-neutral)", + "rejected": true, + "by": "interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full" + }, + { + "control": "m3", + "mutation": "drop a cleanup gate (inverse of the last phase-B source write)", + "rejected": true, + "by": "replay: sources not restored: [11, 41, 44, 83, 86]" + }, + { + "control": "m4", + "mutation": "corrupt a phase-B source write (operand 10 -> 6, cleanup changed alike)", + "rejected": true, + "by": "replay: targets not y + x: [0, 66, 67, 68, 69]" + }, + { + "control": "m5", + "mutation": "phase-B source write moved down to the destination's own line frame", + "rejected": true, + "by": "replay: climb not nested: register 5 from frame 123 (dim 2) to frame 7 (dim 1)" + }, + { + "control": "m6", + "mutation": "a target reads another target (single read, V != I)", + "rejected": true, + "by": "replay: targets not y + x: [0]" + }, + { + "control": "m7", + "mutation": "frame-0 preconditioner corrupted (one helper read dropped)", + "rejected": true, + "by": "replay: targets not y + x: [0]" + }, + { + "control": "m8", + "mutation": "phase-B source write moved before the target read of that register", + "rejected": true, + "by": "replay: climb not nested: register 5 from frame 542 (dim 4) to frame 123 (dim 2)" + }, + { + "control": "m9", + "mutation": "cleanup gate moved off the full frame (to the frame of the gate it inverts)", + "rejected": true, + "by": "replay: climb not nested: register 240 from frame 1 (dim 8) to frame 2 (dim 1)" + }, + { + "control": "positive", + "mutation": "cancelled pair of target-to-target reads at frame 0 (V = I)", + "rejected": false, + "by": "accepted" + } + ] +} \ No newline at end of file diff --git a/research/r420-geometry-cache/evidence/cached.log b/research/r420-geometry-cache/evidence/cached.log new file mode 100644 index 0000000000..c97628e75e --- /dev/null +++ b/research/r420-geometry-cache/evidence/cached.log @@ -0,0 +1,11 @@ + REJECTED target feeds a source (cancelled pair, F2-neutral) :: interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full + REJECTED target feeds a helper (cancelled pair, F2-neutral) :: interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full + REJECTED drop a cleanup gate (inverse of the last phase-B source write) :: replay: sources not restored: [11, 41, 44, 83, 86] + REJECTED corrupt a phase-B source write (operand 10 -> 6, cleanup changed alike) :: replay: targets not y + x: [0, 66, 67, 68, 69] + REJECTED phase-B source write moved down to the destination's own line frame :: replay: climb not nested: register 5 from frame 123 (dim 2) to frame 7 (dim 1) + REJECTED a target reads another target (single read, V != I) :: replay: targets not y + x: [0] + REJECTED frame-0 preconditioner corrupted (one helper read dropped) :: replay: targets not y + x: [0] + REJECTED phase-B source write moved before the target read of that register :: replay: climb not nested: register 5 from frame 542 (dim 4) to frame 123 (dim 2) + REJECTED cleanup gate moved off the full frame (to the frame of the gate it inverts) :: replay: climb not nested: register 240 from frame 1 (dim 8) to frame 2 (dim 1) + accepted cancelled pair of target-to-target reads at frame 0 (V = I) :: accepted +PASS mutation controls: 9/9 negative controls rejected, 1/1 positive control accepted diff --git a/research/r420-geometry-cache/evidence/original.json b/research/r420-geometry-cache/evidence/original.json new file mode 100644 index 0000000000..b25c426e6b --- /dev/null +++ b/research/r420-geometry-cache/evidence/original.json @@ -0,0 +1,65 @@ +{ + "status": "PASS_INTERLEAVED_INTERFACE_MUTATION_CONTROLS", + "controls": [ + { + "control": "m1", + "mutation": "target feeds a source (cancelled pair, F2-neutral)", + "rejected": true, + "by": "interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full" + }, + { + "control": "m2", + "mutation": "target feeds a helper (cancelled pair, F2-neutral)", + "rejected": true, + "by": "interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full" + }, + { + "control": "m3", + "mutation": "drop a cleanup gate (inverse of the last phase-B source write)", + "rejected": true, + "by": "replay: sources not restored: [11, 41, 44, 83, 86]" + }, + { + "control": "m4", + "mutation": "corrupt a phase-B source write (operand 10 -> 6, cleanup changed alike)", + "rejected": true, + "by": "replay: targets not y + x: [0, 66, 67, 68, 69]" + }, + { + "control": "m5", + "mutation": "phase-B source write moved down to the destination's own line frame", + "rejected": true, + "by": "replay: climb not nested: register 5 from frame 123 (dim 2) to frame 7 (dim 1)" + }, + { + "control": "m6", + "mutation": "a target reads another target (single read, V != I)", + "rejected": true, + "by": "replay: targets not y + x: [0]" + }, + { + "control": "m7", + "mutation": "frame-0 preconditioner corrupted (one helper read dropped)", + "rejected": true, + "by": "replay: targets not y + x: [0]" + }, + { + "control": "m8", + "mutation": "phase-B source write moved before the target read of that register", + "rejected": true, + "by": "replay: climb not nested: register 5 from frame 542 (dim 4) to frame 123 (dim 2)" + }, + { + "control": "m9", + "mutation": "cleanup gate moved off the full frame (to the frame of the gate it inverts)", + "rejected": true, + "by": "replay: climb not nested: register 240 from frame 1 (dim 8) to frame 2 (dim 1)" + }, + { + "control": "positive", + "mutation": "cancelled pair of target-to-target reads at frame 0 (V = I)", + "rejected": false, + "by": "accepted" + } + ] +} \ No newline at end of file diff --git a/research/r420-geometry-cache/evidence/original.log b/research/r420-geometry-cache/evidence/original.log new file mode 100644 index 0000000000..c97628e75e --- /dev/null +++ b/research/r420-geometry-cache/evidence/original.log @@ -0,0 +1,11 @@ + REJECTED target feeds a source (cancelled pair, F2-neutral) :: interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full + REJECTED target feeds a helper (cancelled pair, F2-neutral) :: interface: fails H1_no_target_feeds_z,H3_A_z_only_scatter_targets_B_split,H4_C_literal_reverse_at_full + REJECTED drop a cleanup gate (inverse of the last phase-B source write) :: replay: sources not restored: [11, 41, 44, 83, 86] + REJECTED corrupt a phase-B source write (operand 10 -> 6, cleanup changed alike) :: replay: targets not y + x: [0, 66, 67, 68, 69] + REJECTED phase-B source write moved down to the destination's own line frame :: replay: climb not nested: register 5 from frame 123 (dim 2) to frame 7 (dim 1) + REJECTED a target reads another target (single read, V != I) :: replay: targets not y + x: [0] + REJECTED frame-0 preconditioner corrupted (one helper read dropped) :: replay: targets not y + x: [0] + REJECTED phase-B source write moved before the target read of that register :: replay: climb not nested: register 5 from frame 542 (dim 4) to frame 123 (dim 2) + REJECTED cleanup gate moved off the full frame (to the frame of the gate it inverts) :: replay: climb not nested: register 240 from frame 1 (dim 8) to frame 2 (dim 1) + accepted cancelled pair of target-to-target reads at frame 0 (V = I) :: accepted +PASS mutation controls: 9/9 negative controls rejected, 1/1 positive control accepted diff --git a/research/r420-geometry-cache/verify.py b/research/r420-geometry-cache/verify.py new file mode 100644 index 0000000000..ffe222ceca --- /dev/null +++ b/research/r420-geometry-cache/verify.py @@ -0,0 +1,200 @@ +"""One bounded A/B of the original mutation suite plus cache failure controls. + +Prepared for mtpsl with substantial OpenAI Codex assistance; Apache-2.0. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import platform +import subprocess +import sys +import tempfile +import time + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = Path("research/r420-geometry-cache") +SOURCE = Path("research/e8-bit-r420/code/xcheck.py") +HARNESS = Path("research/e8-bit-r420/code/mutants.py") +WORD = Path("research/e8-bit-r420/data/bitE8mut-r420.json.gz") + + +def need(condition, message): + if not condition: + raise RuntimeError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def sha(value): + return hashlib.sha256(value).hexdigest() + + +def signature(result): + obj, *receipts = result + fields = ("v", "R", "n", "lines", "fdim", "fperp", "FULL", "ZERO") + return {"geometry": {key: getattr(obj, key) for key in fields}, "receipts": receipts} + + +def outcome(check, word, reject): + try: + result = check(word) + except reject as error: + return {"accepted": False, "exception": str(error)} + return {"accepted": all(result[3].values()) and all(result[4].values()), + "signature_sha256": sha(canonical(signature(result)))} + + +def run(output): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for path, pin in pins["execution_inputs"].items(): + need(sha((ROOT / path).read_bytes()) == pin["sha256"], "input pin changed: " + path) + + benchmark = {} + receipts = {} + for name, checker in (("original", SOURCE), ("cached", PACKAGE / "cached_xcheck.py")): + command = [sys.executable, "-I", "-B", str(ROOT / HARNESS), str(ROOT / checker), + str(ROOT / WORD), "--json", str(output / (name + ".json"))] + start = time.perf_counter() + proc = subprocess.run(command, capture_output=True, text=True) + elapsed = time.perf_counter() - start + (output / (name + ".log")).write_text(proc.stdout + proc.stderr) + need(proc.returncode == 0, name + " mutation suite failed: " + proc.stderr[-500:]) + receipts[name] = json.loads((output / (name + ".json")).read_text()) + need(receipts[name]["status"] == "PASS_INTERLEAVED_INTERFACE_MUTATION_CONTROLS", + name + " incorrect status") + rows = receipts[name]["controls"] + need(len(rows) == 10 and all(r["rejected"] for r in rows[:9]) + and not rows[9]["rejected"], name + " changed mutation coverage") + benchmark[name + "_seconds"] = elapsed + need(receipts["original"] == receipts["cached"], "original/cached mutation receipts differ") + need((output / "original.log").read_bytes() == (output / "cached.log").read_bytes(), + "original/cached diagnostics differ") + benchmark["speedup"] = benchmark["original_seconds"] / benchmark["cached_seconds"] + benchmark["method"] = "one original-then-cached pair, separate cold processes, identical harness/input; OS caches not flushed" + + spec = importlib.util.spec_from_file_location("cached_xcheck_test", HERE / "cached_xcheck.py") + adapter = importlib.util.module_from_spec(spec) + spec.loader.exec_module(adapter) + original = adapter.original + base = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + cache = adapter.GeometryCache() + baseline = outcome(original.check, base, original.Reject) + need(baseline["accepted"], "baseline rejected") + need(outcome(cache.check, base, original.Reject) == baseline, "initial cached result differs") + checks = [] + + def compare(name, changed, geometry, accept=False): + expected = outcome(original.check, changed, original.Reject) + before = (cache.hits, cache.misses) + actual = outcome(cache.check, changed, original.Reject) + need(actual == expected, name + " differs from uncached checker") + need(actual["accepted"] == accept, name + " unexpected acceptance") + delta = (cache.hits - before[0], cache.misses - before[1]) + need(delta == ((0, 1) if geometry else (1, 0)), name + " wrong cache invalidation") + checks.append({"case": name, "accepted": accept, "cache_miss": geometry, + "outcome": actual}) + + # Every omitted-from-key field still receives its full per-word checks. + mutations = [] + w = copy.deepcopy(base); w["start"][240] = 1; mutations.append(("start frame", w)) + w = copy.deepcopy(base); w["final"][240] = 0; mutations.append(("final frame", w)) + w = copy.deepcopy(base); w["A"].pop(0); mutations.append(("A gate", w)) + w = copy.deepcopy(base); w["B"].pop(0); mutations.append(("B gate", w)) + w = copy.deepcopy(base); w["C"].pop(0); mutations.append(("C cleanup", w)) + w = copy.deepcopy(base); w["D"][0][2].pop(); mutations.append(("D compensation", w)) + w = copy.deepcopy(base); w["ret"][0], w["ret"][1] = w["ret"][1], w["ret"][0] + mutations.append(("retained totals", w)) + w = copy.deepcopy(base); w["scatter"][0] = []; mutations.append(("scatter", w)) + for name, w in mutations: + compare(name, w, geometry=False) + + # Each geometry dependency independently forces validation, even when the + # invalid word has the same gate stream as the previously accepted word. + for field, value in (("h", 9), ("v", 119), ("R", 419), ("form", "wrong")): + w = copy.deepcopy(base); w[field] = value + compare("changed " + field, w, geometry=True) + w = copy.deepcopy(base); w["lines"][0][0] = 3 + compare("changed label", w, geometry=True) + w = copy.deepcopy(base); w["frames"][1].pop() + compare("nonclosed full frame", w, geometry=True) + miss = cache.misses + need(not outcome(cache.check, w, original.Reject)["accepted"], "failed geometry accepted on repeat") + need(cache.misses == miss + 1, "failed geometry was cached") + checks.append({"case": "failed geometry is not cached", "accepted": False}) + + # A new valid geometry must also be verified, not simply refused or aliased. + reflected = copy.deepcopy(base) + for row in reflected["lines"]: + row[0] = -row[0] + compare("valid reflected E8 labels", reflected, geometry=True, accept=True) + need(outcome(cache.check, reflected, original.Reject)["accepted"], "valid reflected hit failed") + + # Results returned by check are mutable in the predecessor API. Corrupting + # them must not corrupt private derived data used by another call. + cache = adapter.GeometryCache() + word = copy.deepcopy(base) + obj, lab, *_ = cache.check(word) + obj.lines[0] = (0,) * 8 + obj.fdim[1] = 0 + obj.fperp[2].append([1] * 8) + obj._nest[(1, 0)] = True + obj.v = 1 + lab["gram_det"] = 999 + need(outcome(cache.check, base, original.Reject) == baseline, "returned objects poisoned cache") + checks.append({"case": "returned geometry and receipt mutation", "accepted": True}) + word["lines"][0][0] = 3 + need(not outcome(cache.check, word, original.Reject)["accepted"], "in-place input mutation bypassed key") + need(outcome(cache.check, base, original.Reject) == baseline, "input mutation poisoned cache") + checks.append({"case": "in-place source input mutation", "accepted": False}) + + single = adapter.GeometryCache(capacity=1) + for w in (base, reflected, base): + need(outcome(single.check, w, original.Reject)["accepted"], "eviction replay failed") + need(single.misses == 3 and single.hits == 0 and len(single._entries) == 1, + "bounded eviction failed") + checks.append({"case": "capacity-one eviction and revalidation", "accepted": True}) + + # Exercise the unmodified adapter in a relocated minimal tree with a changed + # predecessor. It must refuse to import before using any stale cached proof. + relocated = output / "pin-control" + dest = relocated / PACKAGE / "cached_xcheck.py" + dest.parent.mkdir(parents=True) + dest.write_bytes((HERE / "cached_xcheck.py").read_bytes()) + source = relocated / SOURCE + source.parent.mkdir(parents=True) + source.write_bytes((ROOT / SOURCE).read_bytes() + b"\n# changed source\n") + proc = subprocess.run([sys.executable, "-I", "-B", str(dest)], capture_output=True, text=True) + need(proc.returncode != 0 and "pinned xcheck source changed" in proc.stderr, "changed source pin accepted") + checks.append({"case": "changed predecessor source pin", "accepted": False}) + + result = {"status": "PASS_R420_GEOMETRY_CACHE", "benchmark": benchmark, + "environment": {"python": sys.version.split()[0], "platform": platform.system(), + "machine": platform.machine()}, + "mutation_receipt_sha256": sha(canonical(receipts["original"])), + "mutation_diagnostics_sha256": sha((output / "original.log").read_bytes()), + "baseline_signature_sha256": baseline["signature_sha256"], + "supplemental_checks": checks, "source_pins": pins["execution_inputs"]} + (output / "RESULT.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + print("PASS_R420_GEOMETRY_CACHE original_controls=10 supplemental_checks=" + str(len(checks))) + print("same-input mutation suite: %.3fs -> %.3fs (%.2fx); timing is diagnostic, not an acceptance threshold" + % (benchmark["original_seconds"], benchmark["cached_seconds"], benchmark["speedup"])) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="new output directory for logs, comparison and timings") + args = parser.parse_args() + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + run(args.output.resolve()) + else: + with tempfile.TemporaryDirectory(prefix="r420-geometry-cache-") as work: + run(Path(work))