diff --git a/research/joint-dual-replay-fast/BENCHMARK.json b/research/joint-dual-replay-fast/BENCHMARK.json new file mode 100644 index 0000000000..afb295907e --- /dev/null +++ b/research/joint-dual-replay-fast/BENCHMARK.json @@ -0,0 +1,155 @@ +{ + "cpu_count": 16, + "fixture_suite": "frozen tests/test_joint_reclaim.py, unmodified, both arms must pass every test", + "fixture_unit": "replay() on certificates/joint-dual-word-{23,25}.json.gz", + "note": "Timings are measurements, never a correctness gate; receipts and test outcomes are asserted.", + "platform": "win32", + "python": "3.12.14", + "suite_pairs": [ + { + "fast": 37.84658760000457, + "fast_tests": 16, + "historical": 41.463117799998145, + "order": [ + "historical", + "fast" + ], + "pair": 0, + "tests": 16 + }, + { + "fast": 37.58070720000251, + "fast_tests": 16, + "historical": 41.76378180000029, + "order": [ + "fast", + "historical" + ], + "pair": 1, + "tests": 16 + }, + { + "fast": 37.71700059999421, + "fast_tests": 16, + "historical": 41.46604800000205, + "order": [ + "historical", + "fast" + ], + "pair": 2, + "tests": 16 + } + ], + "suite_summary": { + "fast_median": 37.71700059999421, + "historical_median": 41.46604800000205, + "speedup": 1.0993994045223314 + }, + "unit_pairs": [ + { + "fast": 1.056016599999566, + "historical": 1.7439154999956372, + "order": [ + "historical", + "fast" + ], + "pair": 0, + "word": "joint-dual-word-23.json.gz" + }, + { + "fast": 1.643908799997007, + "historical": 2.757246799999848, + "order": [ + "historical", + "fast" + ], + "pair": 0, + "word": "joint-dual-word-25.json.gz" + }, + { + "fast": 1.0395209000053, + "historical": 1.834040499998082, + "order": [ + "fast", + "historical" + ], + "pair": 1, + "word": "joint-dual-word-23.json.gz" + }, + { + "fast": 1.7002662000013515, + "historical": 2.835705000004964, + "order": [ + "fast", + "historical" + ], + "pair": 1, + "word": "joint-dual-word-25.json.gz" + }, + { + "fast": 1.036014700002852, + "historical": 1.7237578999993275, + "order": [ + "historical", + "fast" + ], + "pair": 2, + "word": "joint-dual-word-23.json.gz" + }, + { + "fast": 1.5987498999966192, + "historical": 2.7562392999971053, + "order": [ + "historical", + "fast" + ], + "pair": 2, + "word": "joint-dual-word-25.json.gz" + }, + { + "fast": 1.0163383999970392, + "historical": 1.7094021000011708, + "order": [ + "fast", + "historical" + ], + "pair": 3, + "word": "joint-dual-word-23.json.gz" + }, + { + "fast": 1.5866884999995818, + "historical": 2.6969902999990154, + "order": [ + "fast", + "historical" + ], + "pair": 3, + "word": "joint-dual-word-25.json.gz" + }, + { + "fast": 0.9554359999965527, + "historical": 1.6309984999970766, + "order": [ + "historical", + "fast" + ], + "pair": 4, + "word": "joint-dual-word-23.json.gz" + }, + { + "fast": 1.5136136000000988, + "historical": 2.6318327999979374, + "order": [ + "historical", + "fast" + ], + "pair": 4, + "word": "joint-dual-word-25.json.gz" + } + ], + "unit_summary": { + "fast_median": 1.2848150999998325, + "historical_median": 2.2329366499980097, + "speedup": 1.7379439656323317 + } +} diff --git a/research/joint-dual-replay-fast/README.md b/research/joint-dual-replay-fast/README.md new file mode 100644 index 0000000000..e320d42518 --- /dev/null +++ b/research/joint-dual-replay-fast/README.md @@ -0,0 +1,154 @@ +# joint-dual-replay-fast + +**Verifier engineering; no kappa, no certificate, supplier or frontier change.** +An opt-in adapter that speeds up the joint-dual serialized-word replay with +identical checks and identical receipts. + +Prepared by Aaron Wang, with help from opencode. Apache-2.0. + +## Scope and question + +Card `replay-runtime` (scope key `b1dd41940c60d240b47a`): can one measured +replay bottleneck be sped up without dropping coverage? The object is the +replay stage of the frozen frame-compiler chain `research/joint-dual`: +`scripts/experiments/binary_frame_replay.py:replay()` on the pinned words +`certificates/joint-dual-word-{23,25}.json.gz` (the words of the PR25-PR58 +lineage; source freeze `research/joint-dual/SOURCE.json`, enforced by +`joint_dual_compose.check_sources()`). + +Card selection note: the first-choice drawn card `portable-replay` (scope key +`831cc1a3c8f9ff01b197`) matched the fresh claim posted 2026-10-14T11:24Z in +https://github.com/CrocSwap/integer-mult-bounds/discussions/1166 (completed as +https://github.com/CrocSwap/integer-mult-bounds/pull/1834), so per the +pair-collision rule this session took the second-choice card. See TASK.json. + +## The measured bottleneck + +cProfile of `replay()` on the h=23 word (CPython 3.12, Windows) shows 2.045 s +total, of which **0.84 s** is the per-output full-triple scan + +```python +expected = sum(1 << i for i, t in enumerate(triples) + if common in t and not (set(t) & (set(triple) - {common}))) +tt = [i for i, t in enumerate(triples) if common in t] +``` + +(1,020,119 generator iterations at that line: 5,336 outputs x 1,771 triples). +The rest is the full-basis word simulation and the event loops. + +## What this package changes + +`fast_replay.py` re-executes the historical replay body with **every assertion, +both full-basis orientations and the receipt kept identical**, replacing only +the scans with containment masks over the same `combinations(range(h), 3)` +enumeration: bit i of `center_mask[c]` is `c in triples[i]`, bit i of +`pair_mask[c][x]` is `{c, x} <= triples[i]`, and + +``` +expected(common, triple) = center_mask[common] + & ~pair_mask[common][x] for each x in set(triple) - {common} +``` + +is exactly the literal condition. `check_word` (including PR64/rfu08's +cancelling-scatter control) and the whole transitions stage +(`binary_frame_profile_prepare.prepare`) are the frozen historical +implementations, loaded unchanged. The historical scripts, certificates and +`tests/test_joint_reclaim.py` are **not modified**; this is the opt-in adapter +pattern of `research/ck-dyadic-replay-fast`. + +`shim/binary_frame_replay.py` and `suite_arm.py` exist only for adoption +simulation: preloading the shim routes the *unmodified* frozen test module's +`from binary_frame_replay import replay` to the adapter. + +## Evidence + +- **Identical receipts.** Historical and adapter replay receipts are equal on + both pinned words and equal to the recorded receipts in + `certificates/joint-dual-compiler.json`; the delegated transitions stage + equals `certificates/joint-dual-transitions-{23,25}.json`. +- **Full cross-check.** On all 12,261 outputs of both words the mask algebra + equals an independently written literal scan. +- **Oracle matrix.** The exact twelve mutations of the frozen + `tests/test_joint_reclaim.py` (eleven rejections plus the scatter-reversal + acceptance) on both words: every accept/reject outcome agrees with the + historical module in both checkers (24 cases), and the documented rejections + reject. +- **Failure controls.** A corrupted containment table is detected by the + cross-check (40/44 mismatching outputs at h=23/25); an unchecked word + rejects; `-O` entry refuses to run ("Assertions must remain enabled"); the + source freeze and word pins are re-checked every run. +- **Adoption simulation.** The frozen test module runs unmodified against the + adapter through the shim and passes all 16 tests. + +## Before/after wall time (same fixture, measurements never gates) + +Paired alternating runs, CPython 3.12, Windows; see `BENCHMARK.json`: + +| Fixture | Historical median | Adapter median | Speedup | +|---|---:|---:|---:| +| `replay()` on both pinned words (5 pairs) | 2.233 s | 1.285 s | **1.74x** | +| frozen `tests/test_joint_reclaim.py`, unmodified (3 pairs) | 41.47 s | 37.72 s | 1.10x | + +The unit fixture clears the stated target of at least 25 percent. The suite +fixture improves only 10 percent because most of that module is JSON +deep-copies, mutation rejection paths that never reach the scan, and the +unchanged transitions stage; no coverage was dropped to improve it. + +Retained checks: `check_word`, every replay assertion, both full-basis +orientations, the unchanged transitions stage, and the frozen test module as +oracle. Invalidation: the containment tables are rebuilt from the word on +**every call** — there is no persistent cache and no staleness; the source +freeze and word pins are re-verified on every replay. + +## Reproduce + +```sh +python3.12 -B scripts/research_package.py --package research/joint-dual-replay-fast --check-only +python3.12 scripts/research_package.py --package research/joint-dual-replay-fast +python3.12 -I -B research/joint-dual-replay-fast/benchmark.py # paired timings +``` + +Expected: `PASS_JOINT_DUAL_REPLAY_FAST_EQUIVALENCE` (see RESULT.json), +`PASS_REGISTERED_RESEARCH_PACKAGE research/joint-dual-replay-fast outcome=completed`, +and a BENCHMARK.json with the paired timings above (values vary by machine). + +## Limitations + +- Opt-in only: the historical chain, its frozen pins and the suite default are + unchanged, so the repository-wide suite wall time benefits only after a + maintainer adopts the adapter (adoption would require superseding the + `research/joint-dual/SOURCE.json` freeze, which this PR does not do). +- Domain is exactly the two frozen words at h in {23, 25} (the + `binary_frame_math.exactness` certified dimensions). The mask identity is + tested on synthetic shapes up to h=12 but no other word is claimed. +- The adapter mirrors the historical first-match `list.index` semantics with + explicit `ValueError`s; duplicated frames in a word keep the same behavior. +- No mathematical claim of any kind: no kappa, no bound, no supplier admission, + no selected-frontier change. + +## Open next questions + +1. **Sibling skip-frame line.** Can the same identity speed up + `verify_skip_frame.py`'s replay, which shares the triple-scan shape? First + step: profile it on its pinned words and measure the scan share. Blocked by: + that chain's own pin freeze and oracle controls; do not retrofit frozen + packages. +2. **The remaining simulation.** Is the full-basis word loop (now about 55% of + the optimized replay) reducible without weakening the two-orientation + replay? First step: measure limb traffic in the two orientation passes. + Blocked by: the requirement that every basis row of both orientations is + executed literally. + +## Credit + +- The frozen replay, transitions stage and words are the frame-compiler line of + Chafik Boukhalfa (PR25-PR58 lineage; `scripts/experiments/pin_joint_dual_sources.py`, + `research/joint-dual`), with the original word/frames checks; PR64 (rfu08) is + credited in `check_word` for the cancelling-scatter counterexample, which is + retained verbatim. +- Workflow precedent: `research/ck-dyadic-replay-fast` (opt-in adapter pattern, + paired benchmark receipts) and `research/git-provenance-stream` (timings as + measurements, never gates). Both are credited, not modified. +- Task selection, profiling, the adapter, controls and this write-up were + prepared by Aaron Wang with help from opencode; substantial AI assistance is + disclosed in TASK.json. No independent human review is claimed. diff --git a/research/joint-dual-replay-fast/RESULT.json b/research/joint-dual-replay-fast/RESULT.json new file mode 100644 index 0000000000..6acc87da08 --- /dev/null +++ b/research/joint-dual-replay-fast/RESULT.json @@ -0,0 +1,340 @@ +{ + "controls": { + "corrupted_table_mismatches": { + "23": 40, + "25": 44 + }, + "frozen_suite_seconds": 50.32977540000138, + "frozen_suite_tests": 16, + "optimize_guard": true, + "unchecked_word": true + }, + "freeze": { + "frozen_sources": 3, + "pinned_words": 2 + }, + "invalidation": "containment tables are rebuilt from the word on every call; no persistent cache; source-freeze and word pins checked each run", + "mutation_cases": 24, + "mutation_rows": [ + { + "h": 23, + "mutation": "omitted_literal_xor", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "self_xor", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "replay", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "non_nested_operation_frame", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "aliased_terminal_role", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "replay", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "missing_copied_center", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "omitted_transition", + "replay": [ + "accept", + "64302c0c6976dab2" + ], + "scope": "transitions", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "understated_physical_width", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "self_cancelling_uncharged_scatter", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "negative_operation_frame_index", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "replay", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "cancelled_repetitions_of_paid_scatter", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "missing_scatter", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 23, + "mutation": "scatter_order_acceptance", + "replay": [ + "accept", + "64302c0c6976dab2" + ], + "scope": "both", + "transitions": [ + "accept", + "d7c972f6d52f23a0" + ] + }, + { + "h": 25, + "mutation": "omitted_literal_xor", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "self_xor", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "replay", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "non_nested_operation_frame", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "aliased_terminal_role", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "replay", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "missing_copied_center", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "omitted_transition", + "replay": [ + "accept", + "40f0b98b1af18435" + ], + "scope": "transitions", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "understated_physical_width", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "self_cancelling_uncharged_scatter", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "negative_operation_frame_index", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "replay", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "cancelled_repetitions_of_paid_scatter", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "missing_scatter", + "replay": [ + "reject", + "AssertionError" + ], + "scope": "both", + "transitions": [ + "reject", + "AssertionError" + ] + }, + { + "h": 25, + "mutation": "scatter_order_acceptance", + "replay": [ + "accept", + "40f0b98b1af18435" + ], + "scope": "both", + "transitions": [ + "accept", + "28c26130b022b304" + ] + } + ], + "outputs_cross_checked": 12261, + "retained_checks": "historical check_word, every replay assertion and both full-basis orientations, the unchanged transitions stage, and the frozen tests/test_joint_reclaim.py matrix as oracle", + "scope": "Opt-in adapter equivalence on the two frozen joint-dual words; no kappa, certificate, supplier or frontier change.", + "status": "PASS_JOINT_DUAL_REPLAY_FAST_EQUIVALENCE", + "words": [ + 23, + 25 + ] +} diff --git a/research/joint-dual-replay-fast/SOURCES.json b/research/joint-dual-replay-fast/SOURCES.json new file mode 100644 index 0000000000..7884c2a9c1 --- /dev/null +++ b/research/joint-dual-replay-fast/SOURCES.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "predecessor_heads": { + "frame-compiler-joint-dual-freeze": "bc2f7ed4c20dc18898305ab17165c0c995cbb804" + }, + "files": [ + { + "path": "certificates/joint-dual-compiler.json", + "usage": "input", + "git_blob": "919fff2e6dac36adecf8ab4503a0d6fd65605e61", + "sha256": "516c4d85158553dabd0a98216a064b2a7397957a9d5dd0df1d6e5aec53a4e805" + }, + { + "path": "certificates/joint-dual-transitions-23.json", + "usage": "input", + "git_blob": "0b8e78bed7936d0eefed721470dd270bd93953c0", + "sha256": "9ee68e542768b7a8802f8e1fc8a61b17c72c319f6c1d70c69a086c811cfec7fc" + }, + { + "path": "certificates/joint-dual-transitions-25.json", + "usage": "input", + "git_blob": "e3ca531a858798204e7bd1b445c39a8e89c3691e", + "sha256": "f858c3f71d563c14013c9ae4cc10fce2b9f227da38e468a392c6890613444c8d" + }, + { + "path": "certificates/joint-dual-word-23.json.gz", + "usage": "input", + "git_blob": "143f2684b069c9c6bc034b91fa5deb3ddab3abf7", + "sha256": "634da1cb39634be15c6d4070132c6bdf4f5a927331cac3b4f13dc995dd799b6b" + }, + { + "path": "certificates/joint-dual-word-25.json.gz", + "usage": "input", + "git_blob": "fc67bf3a5789da29392ca8f82ff0fbed906af2e3", + "sha256": "dd2223d7ee0b91c4445f5acd0b7cad945f56f4e16456b6818f53ddef64a0cb16" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/joint-dual/SOURCE.json", + "usage": "input", + "git_blob": "e055d5d63d12bfc4c5e1c1d5dd4341b87907f816", + "sha256": "e60f1f78c9729700ef9606a6576163de0b553792e5e8f24591dce5f51597158c" + }, + { + "path": "scripts/experiments/binary_frame_math.py", + "usage": "input", + "git_blob": "b87855e808802c6b5dbdfb845f2328370ff8a4f0", + "sha256": "1f96e8aafc8ae89f8eeec5d03800131d93d58e01bf8a7fca8feb03702d1740d0" + }, + { + "path": "scripts/experiments/binary_frame_profile_prepare.py", + "usage": "input", + "git_blob": "21295ac2c8fb33f92649c5572ce67a7cf20e8a28", + "sha256": "16dea3d3ef3dc90db928ed3e35d002f6926d2e7388da4766fc2fd725550f739e" + }, + { + "path": "scripts/experiments/binary_frame_replay.py", + "usage": "input", + "git_blob": "a4897e5ecb5c92404257e85c8558e7264f0ef0bb", + "sha256": "1a572dbb33faba6695b3293768a7e61392d11cb4c2d5f708eedcd2cb95d0aff9" + }, + { + "path": "tests/test_joint_reclaim.py", + "usage": "input", + "git_blob": "c94302af4c27e6797baec4fa8fe3147dc088f61d", + "sha256": "c4e2817bf6e699f462aa3c589ee45e24ab0dcad6bcdb6152ca2a1e16ac7bffeb" + } + ] +} diff --git a/research/joint-dual-replay-fast/TASK.json b/research/joint-dual-replay-fast/TASK.json new file mode 100644 index 0000000000..c66b5e903f --- /dev/null +++ b/research/joint-dual-replay-fast/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "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": "One measured replay bottleneck: the per-output full-triple scans in the joint-dual serialized-word replay (scripts/experiments/binary_frame_replay.replay on certificates/joint-dual-word-{23,25}.json.gz). Replace the O(outputs x v) scans with per-call containment masks in an opt-in adapter, with the frozen historical verifier, its scripts and tests/test_joint_reclaim.py untouched and used as the oracle.", + "scope_change_reason": "Card selection: my first-choice drawn card portable-replay (scope key 831cc1a3c8f9ff01b197) matched the fresh claim of 2026-10-14T11:24Z in discussion 1166 (completed as https://github.com/CrocSwap/integer-mult-bounds/pull/1834), so per the pair-collision rule I took the second-choice card replay-runtime (scope key b1dd41940c60d240b47a, chooser OS nonce 24ae43237c3eaed2410bcdf516d854cd). Refinement inside the card: of the replay stages measurable at base (the isolated test suite, the research-workflow gate, research_package metadata validation, the joint-dual word replay), only the joint-dual word replay had a single dominant, cleanly replaceable measured bottleneck; research_package.py source validation was already batched by research/git-provenance-stream and the research-workflow gate has a flat distribution of subprocess-bound fixtures with no single hotspot.", + "bottleneck_link": "The joint-dual replay is the independent word check for the PR25-PR58 frame-compiler line (research/joint-dual) and the dominant cost of its longest isolated test module (tests/test_joint_reclaim.py). Faster identical-coverage replays shorten the review loop for that line's candidates; this is verification throughput only, not a multiplication mechanism result.", + "budget_minutes": 60, + "stop_rule": "One scan replacement in one adapter; abandon if any receipt differs from the historical implementation or the frozen words, if any mutation outcome differs from the historical oracle, or if paired same-fixture timings show less than a 25 percent reduction on the replay stage. No coverage is removed to reach the target; timings are measurements, never a correctness gate.", + "outcome": "completed", + "evidence": "RESULT.json records equal legacy/adapter receipts on both pinned words and their recorded compiler receipts, a full literal-scan cross-check over 12,261 outputs, the frozen 24-case tests/test_joint_reclaim.py mutation matrix against the historical oracle, corrupted-table/unchecked-word/-O controls, and an unmodified frozen-suite adoption run (16 tests) through the shim. BENCHMARK.json records paired timings on two identical fixtures: replay() unit median 2.233s -> 1.285s (1.74x) and the frozen test module 41.47s -> 37.72s (1.10x). Registered replay and --check-only pass; research-workflow tests pass.", + "author": "Aaron Wang", + "ai_assistance": "with help from opencode; substantial AI assistance for profiling, implementation, testing and writing. No independent human review claimed.", + "open_questions": [ + { + "question": "Can the same containment-mask identity speed up the sibling skip-frame replay line (scripts/experiments/skip_frame_compose.py / verify_skip_frame.py), whose output checks share the triple-scan shape?", + "why_it_matters": "The measured 1.74x applies only to the joint-dual replay stage; the skip-frame words (certificates/skip-frame-kappa.json lineage) are a separate frozen chain with their own replay cost.", + "first_step": "Profile verify_skip_frame.py on its pinned words, measure the triple-scan share, and if material apply the mask identity behind an adapter cross-checked against that chain's own literal scans and mutation controls.", + "blocked_by": "A separate pin freeze and its own oracle controls; this package does not retro-fit or modify any frozen chain." + }, + { + "question": "Is the remaining full-basis word simulation (M+J+M^-1+V applied twice to all 2v+R basis rows, about 55 percent of the optimized replay) reducible without weakening the independent two-orientation replay?", + "why_it_matters": "That loop, not the scans, is now the replay bottleneck; algebraic shortcuts would change the independent-replay character that makes the check trustworthy.", + "first_step": "Measure limb traffic and allocation in the two orientation passes on the pinned words and look for a representation change that still executes every XOR of every basis row.", + "blocked_by": "The requirement that every basis row of both orientations be executed literally; any shortcut must be justified as an identical check, not a sampled one." + } + ] +} diff --git a/research/joint-dual-replay-fast/VERIFY.json b/research/joint-dual-replay-fast/VERIFY.json new file mode 100644 index 0000000000..90a198c44f --- /dev/null +++ b/research/joint-dual-replay-fast/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/joint-dual-compiler.json", + "certificates/joint-dual-transitions-23.json", + "certificates/joint-dual-transitions-25.json", + "certificates/joint-dual-word-23.json.gz", + "certificates/joint-dual-word-25.json.gz", + "research/joint-dual/SOURCE.json", + "scripts/experiments/binary_frame_math.py", + "scripts/experiments/binary_frame_profile_prepare.py", + "scripts/experiments/binary_frame_replay.py", + "tests/test_joint_reclaim.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Source-freeze binding for the three frozen scripts/tests and both pinned words; identical historical/adapter replay receipts on both words and equality with the recorded compiler receipts; unchanged transitions stage equals the recorded transitions receipts; full literal-scan cross-check of the mask identity on all 12,261 outputs; the frozen tests/test_joint_reclaim.py mutation matrix (11 rejections plus the scatter-reversal acceptance) on both words with the historical module as accept/reject oracle; corrupted-table, unchecked-word and -O failure controls; unmodified frozen-suite adoption run through the shim (all tests must pass and must use the adapter)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_fast_replay.py" + ], + "timeout_seconds": 120, + "checks": "Mask-algebra identity against the literal scan on exhaustive small shapes and seeded random shapes (h in 3..12), corrupted-table disagreement control, shim re-export identity, and the -O entry guard." + } + ] +} diff --git a/research/joint-dual-replay-fast/benchmark.py b/research/joint-dual-replay-fast/benchmark.py new file mode 100644 index 0000000000..433cee48b1 --- /dev/null +++ b/research/joint-dual-replay-fast/benchmark.py @@ -0,0 +1,112 @@ +#!/usr/bin/env python3 +"""Paired before/after timings on the same fixture; measurements, never gates. + +Two fixtures: + unit -- `replay()` on the two pinned words, five alternating pairs + (historical scripts/experiments/binary_frame_replay.py vs this + package's adapter); identical receipts asserted every run. + suite -- the frozen historical test module tests/test_joint_reclaim.py run + unmodified in a clean subprocess through suite_arm.py, three + alternating pairs: the `historical` arm imports the frozen + modules, the `fast` arm preloads shim/binary_frame_replay.py so + the module's own `from binary_frame_replay import replay` + resolves to the adapter. Every test must pass in both arms. + +Only the replay implementation differs between arms; the test module bytes, +the words, the checks and the transitions stage are identical. A suite run is +accepted only when it passes every test, so no speedup can come from dropped +coverage. + +Usage: python3 benchmark.py [--pairs 3] [--unit-pairs 5] [--out BENCHMARK.json] +""" +import sys +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') + +import argparse +import hashlib +import json +import os +from pathlib import Path +import statistics +import subprocess +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORDS = [ROOT / 'certificates/joint-dual-word-23.json.gz', + ROOT / 'certificates/joint-dual-word-25.json.gz'] + + +def suite_run(arm): + process = subprocess.run([sys.executable, '-I', '-B', str(HERE / 'suite_arm.py'), str(ROOT), arm], + capture_output=True, text=True, cwd=str(ROOT)) + if process.returncode != 0: + raise SystemExit(f'{arm} arm failed to run:\n{process.stdout}\n{process.stderr}') + record = json.loads(process.stdout.strip().splitlines()[-1]) + if record['failures'] or record['errors'] or record['tests'] == 0: + raise SystemExit(f'{arm} arm did not pass cleanly: {record}') + return record + + +def unit_pairs(count): + sys.path.insert(0, str(HERE)) + import fast_replay + legacy = fast_replay.historical_replay + rows = [] + for pair in range(count): + for word in WORDS: + order = ('historical', 'fast') if pair % 2 == 0 else ('fast', 'historical') + run = {} + for arm in order: + replay = legacy.replay if arm == 'historical' else fast_replay.replay + start = time.perf_counter() + receipt = replay(word) + run[arm] = dict(seconds=time.perf_counter() - start, + receipt=hashlib.sha256( + json.dumps(receipt, sort_keys=True).encode()).hexdigest()) + if run['historical']['receipt'] != run['fast']['receipt']: + raise SystemExit('receipts differ between arms on ' + word.name) + rows.append(dict(pair=pair, word=word.name, order=list(order), + historical=run['historical']['seconds'], + fast=run['fast']['seconds'])) + return rows + + +def summary(rows): + old = statistics.median(r['historical'] for r in rows) + new = statistics.median(r['fast'] for r in rows) + return dict(historical_median=old, fast_median=new, speedup=old / new) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--pairs', type=int, default=3) + parser.add_argument('--unit-pairs', type=int, default=5) + parser.add_argument('--out', default=str(HERE / 'BENCHMARK.json')) + args = parser.parse_args() + unit = unit_pairs(args.unit_pairs) + suite_rows = [] + for pair in range(args.pairs): + order = ('historical', 'fast') if pair % 2 == 0 else ('fast', 'historical') + run = {} + for arm in order: + run[arm] = suite_run(arm) + suite_rows.append(dict(pair=pair, order=list(order), + historical=run['historical']['seconds'], + fast=run['fast']['seconds'], + tests=run['historical']['tests'], + fast_tests=run['fast']['tests'])) + document = dict( + fixture_unit='replay() on certificates/joint-dual-word-{23,25}.json.gz', + fixture_suite='frozen tests/test_joint_reclaim.py, unmodified, both arms must pass every test', + python=sys.version.split()[0], platform=sys.platform, cpu_count=os.cpu_count(), + unit_pairs=unit, unit_summary=summary(unit), + suite_pairs=suite_rows, suite_summary=summary(suite_rows), + note='Timings are measurements, never a correctness gate; receipts and test outcomes are asserted.') + Path(args.out).write_text(json.dumps(document, indent=2, sort_keys=True) + '\n', encoding='utf-8') + print(json.dumps(dict(unit=document['unit_summary'], suite=document['suite_summary']), indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/joint-dual-replay-fast/fast_replay.py b/research/joint-dual-replay-fast/fast_replay.py new file mode 100644 index 0000000000..a14c466421 --- /dev/null +++ b/research/joint-dual-replay-fast/fast_replay.py @@ -0,0 +1,204 @@ +#!/usr/bin/env python3 +"""Opt-in adapter: faster joint-dual serialized-word replay with identical checks. + +The historical verifier `scripts/experiments/binary_frame_replay.py`, its +transitions stage `binary_frame_profile_prepare.py` and the frozen pin record +`research/joint-dual/SOURCE.json` are untouched; this adapter is additive. + +Measured bottleneck (CPython 3.12, Windows): in `replay` on the pinned word +`certificates/joint-dual-word-23.json.gz`, the per-output full-triple scans + + expected = sum(1 << i for i, t in enumerate(triples) + if common in t and not (set(t) & (set(triple) - {common}))) + tt = [i for i, t in enumerate(triples) if common in t] + +cost 0.84 s of a 2.045 s call (cProfile: 1,020,119 generator iterations at +that line; 5,336 outputs x 1,771 triples). The adapter replaces the scans with +containment masks over the same triple enumeration: + + expected(common, triple) = center_mask[common] + & ~pair_mask[common][x] for each x in set(triple)-{common} + +which is exactly the literal condition `common in t and not (set(t) & ...)`: +bit i of `center_mask[c]` is `c in triples[i]`, bit i of `pair_mask[c][x]` is +`{c, x} <= triples[i]`. The tables are rebuilt on every call from the word's +own `h`, so there is no persistent cache and no invalidation state. + +Every assertion, both full-basis orientations and the complete receipt are +retained. `check_word` and the whole transitions stage are the frozen +historical implementations, imported unchanged. The package's verify.py +cross-checks the mask identity against a literal scan on every output of both +pinned words and against the complete `tests/test_joint_reclaim.py` mutation +matrix, using the historical module as oracle. + +Prepared by Aaron Wang, with help from opencode. Apache-2.0. +""" +import sys +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') + +from collections import Counter +import gzip +import importlib.util +from itertools import combinations +from pathlib import Path +import json + +ROOT = Path(__file__).resolve().parents[2] +EXPERIMENTS = ROOT / 'scripts' / 'experiments' + + +def _load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +# The frozen historical implementations, loaded by exact path under private +# names so this adapter works even when its own shim shadows the historical +# module name (see shim/binary_frame_replay.py). +historical_replay = _load('_jd_historical_frame_replay', EXPERIMENTS / 'binary_frame_replay.py') +check_word = historical_replay.check_word # retained unchanged (incl. PR64 scatter control) + +_historical_prepare = None + + +def prepare(path, destination): + """The frozen historical transitions stage, delegated unchanged.""" + global _historical_prepare + if _historical_prepare is None: + # Lazy: the historical module imports `binary_frame_replay` by name, + # which a preloaded shim may occupy; load only at call time. + if 'binary_frame_replay' not in sys.modules: + sys.path.insert(0, str(EXPERIMENTS)) + _historical_prepare = _load('_jd_historical_frame_profile_prepare', + EXPERIMENTS / 'binary_frame_profile_prepare.py') + return _historical_prepare.prepare(path, destination) + + +def tables(h): + """Containment masks, destination lists and triple lookup over combinations(range(h), 3).""" + triples = list(combinations(range(h), 3)) + center = [0] * h + pair = [[0] * h for _ in range(h)] + for i, t in enumerate(triples): + bit = 1 << i + for c in t: + center[c] |= bit + for x in t: + pair[c][x] |= bit + destinations = [[i for i, t in enumerate(triples) if c in t] for c in range(h)] + return triples, center, pair, destinations, {t: i for i, t in enumerate(triples)} + + +def expected_mask(center, pair, common, triple): + """The literal per-output scan as O(1) bitmask algebra (see module docstring).""" + mask = center[common] + for x in set(triple) - {common}: + mask &= ~pair[common][x] + return mask + + +def replay(path): + """Identical contract, checks and receipt to binary_frame_replay.replay.""" + raw = Path(path).read_bytes() + raw = gzip.decompress(raw) if str(path).endswith('.gz') else raw + d = json.loads(raw) + check_word(d) + h, v, R = d['h'], d['v'], d['R'] + F = d['frames'] + triples, center, pair, destinations, lookup = tables(h) + assert len(triples) == v + ranks = [1 if c == u else u.bit_count() - c.bit_count() for c, u in F] + for c, u in F: + assert c and not c & ~u and (c.bit_count() in (1, 2) or c == u and c.bit_count() == 3) + # First-match semantics of the historical F.index([mask, mask]) scan. + frame_index = {} + for index, frame in enumerate(F): + frame_index.setdefault(tuple(frame), index) + physical = [None] * R + symbols = [0] * R + hist = Counter() + sources = {int(i): s for i, s in d['sources'].items()} + assert len(sources) == v and len(set(sources.values())) == v + + def incidence(s, g): + old = physical[s] + if old is not None: + c, u = F[old] + cc, uu = F[g] + assert not cc & ~c and not u & ~uu + hist[ranks[g] - ranks[old]] += 1 + else: + hist[ranks[g]] += 1 + physical[s] = g + + for i, s in sources.items(): + mask = sum(1 << j for j in triples[i]) + key = (mask, mask) + if key not in frame_index: + raise ValueError(str([mask, mask]) + ' is not in list') + g = frame_index[key] + incidence(s, g) + symbols[s] = 1 << i + for a, b, g in d['ops']: + assert a != b + incidence(a, g) + incidence(b, g) + symbols[a] ^= symbols[b] + scatter = [0] * v + out = set() + for s, g, common, triple in d['outputs']: + assert s not in out + out.add(s) + incidence(s, g) + c, u = F[g] + expected = expected_mask(center, pair, common, triple) + assert symbols[s] == expected + if len(triple) == 1: + assert c == 1 << common and u == (1 << h) - 1 + r = ranks[g] + hist[r] += 1 + hist[h - r] += 1 + tt = destinations[common] + else: + assert c == 1 << common and u == ((1 << h) - 1) ^ sum(1 << j for j in triple if j != common) + hist[h - 1 - ranks[g]] += 1 + hist[1] += 1 + key = tuple(triple) + if key not in lookup: + raise ValueError(str(list(key)) + ' is not in list') + tt = [lookup[key]] + for i in tt: + scatter[i] ^= symbols[s] + for s, g in enumerate(physical): + assert g is not None + if s not in out: + hist[h - ranks[g]] += 1 + assert scatter == [1 << i for i in range(v)] + assert sum(t * n for t, n in hist.items()) == h * R + h * (h - 1) + initial = [1 << i for i in range(2 * v + R)] + M = [(2 * v + a, 2 * v + b) for a, b, g in d['ops']] + V = [(2 * v + s, i) for i, s in sources.items()] + J = [tuple(x) for x in d['scatter']] + word = M + J + M[::-1] + V + M + J + M[::-1] + V + for dual in (False, True): + x = initial.copy() + for a, b in reversed(word) if dual else word: + if dual: + a, b = b, a + x[a] ^= x[b] + assert x[2 * v:] == initial[2 * v:] + if dual: + assert x[:v] == [initial[i] ^ initial[v + i] for i in range(v)] and x[v:2 * v] == initial[v:2 * v] + else: + assert x[v:2 * v] == [initial[i] ^ initial[v + i] for i in range(v)] and x[:v] == initial[:v] + return dict(status='independent serialized word, exact frames, full input and dirty basis both orientations PASS', + h=h, roles=R, output_roles=len(out), elementary_xors=len(M), word_length=len(word), + full_basis_vectors=2 * v + R, rank_mass=sum(t * n for t, n in hist.items()), + histogram=dict(hist)) + + +if __name__ == '__main__': + print(json.dumps(replay(sys.argv[1]), indent=2)) diff --git a/research/joint-dual-replay-fast/shim/binary_frame_replay.py b/research/joint-dual-replay-fast/shim/binary_frame_replay.py new file mode 100644 index 0000000000..3ed44c0bdf --- /dev/null +++ b/research/joint-dual-replay-fast/shim/binary_frame_replay.py @@ -0,0 +1,11 @@ +"""Shim for adoption simulation and benchmarking only. + +Preloading this module as `binary_frame_replay` routes `replay` (and the +retained `check_word`) to the optimized adapter, so the frozen historical +test module `tests/test_joint_reclaim.py` can run unmodified against the +adapter via its own `from binary_frame_replay import replay`. The frozen +test file and the historical implementation are not changed by this. +""" +from fast_replay import replay, check_word # check_word is the frozen historical one + +__all__ = ['replay', 'check_word'] diff --git a/research/joint-dual-replay-fast/suite_arm.py b/research/joint-dual-replay-fast/suite_arm.py new file mode 100644 index 0000000000..4d54f9738f --- /dev/null +++ b/research/joint-dual-replay-fast/suite_arm.py @@ -0,0 +1,39 @@ +#!/usr/bin/env python3 +"""Run the frozen historical test module against one replay arm. + +argv[1] is the repository root and argv[2] is the arm: `historical` imports +the frozen scripts/experiments modules; `fast` preloads the package shim so +the test module's own `from binary_frame_replay import replay` resolves to +the optimized adapter. The test module itself is loaded unmodified either +way. Prints one JSON line with the wall time and the exact test outcome. +""" +import json +import os +import sys +import time +import unittest +from pathlib import Path + +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') + +root = Path(sys.argv[1]) +arm = sys.argv[2] +if arm not in ('historical', 'fast'): + raise SystemExit('arm must be historical or fast') +sys.path.insert(0, str(root / 'research/joint-dual-replay-fast')) +sys.path.insert(0, str(root / 'scripts/experiments')) +if arm == 'fast': + sys.path.insert(0, str(root / 'research/joint-dual-replay-fast/shim')) +import binary_frame_replay +import binary_frame_profile_prepare +sys.path.insert(0, str(root / 'tests')) +import test_joint_reclaim + +start = time.perf_counter() +suite = unittest.TestLoader().loadTestsFromModule(test_joint_reclaim) +result = unittest.TextTestRunner(stream=open(os.devnull, 'w'), verbosity=0).run(suite) +seconds = time.perf_counter() - start +print(json.dumps(dict(arm=arm, seconds=seconds, tests=result.testsRun, + failures=len(result.failures), errors=len(result.errors), + replay_module=binary_frame_replay.__file__))) diff --git a/research/joint-dual-replay-fast/test_fast_replay.py b/research/joint-dual-replay-fast/test_fast_replay.py new file mode 100644 index 0000000000..3693c5a4de --- /dev/null +++ b/research/joint-dual-replay-fast/test_fast_replay.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +"""Fast unit checks for the adapter's mask algebra and entry guards.""" +import sys +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') + +from itertools import combinations +from pathlib import Path +import random +import subprocess +import unittest + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +import fast_replay +from fast_replay import expected_mask, tables + + +def literal(triples, common, triple): + return sum(1 << i for i, t in enumerate(triples) + if common in t and not (set(t) & (set(triple) - {common}))) + + +class MaskAlgebra(unittest.TestCase): + def test_identity_on_exhaustive_small_shapes(self): + for h in range(3, 9): + triples, center, pair, _, _ = tables(h) + for i, triple in enumerate(triples): + for common in triple: + self.assertEqual(expected_mask(center, pair, common, list(triple)), + literal(triples, common, list(triple))) + self.assertEqual(expected_mask(center, pair, triple[0], [triple[0]]), + literal(triples, triple[0], [triple[0]])) + + def test_identity_on_random_shapes_and_repeats(self): + rng = random.Random(20261014) + for h in (3, 5, 8, 12): + triples, center, pair, _, _ = tables(h) + for _ in range(200): + common = rng.randrange(h) + size = rng.choice((1, 3)) + pool = [x for x in range(h) if x != common] + triple = [common] + rng.sample(pool, min(size - 1, len(pool))) + triple = sorted(triple) if size == 3 else [common] + if size == 3 and len(triple) != 3: + continue + self.assertEqual(expected_mask(center, pair, common, triple), + literal(triples, common, triple)) + + def test_corrupted_table_disagrees(self): + triples, center, pair, _, _ = tables(23) + corrupt = [row[:] for row in pair] + corrupt[0][1], corrupt[0][2] = corrupt[0][2], corrupt[0][1] + self.assertTrue(any(expected_mask(center, corrupt, 0, [0, 1, 5]) != + literal(triples, 0, [0, 1, 5]) for _ in (0,))) + + +class EntryGuards(unittest.TestCase): + def test_shim_reexports_the_adapter(self): + sys.path.insert(0, str(HERE / 'shim')) + import binary_frame_replay as shim + self.assertIs(shim.replay, fast_replay.replay) + self.assertIs(shim.check_word, fast_replay.check_word) + + def test_optimized_interpreter_refuses(self): + process = subprocess.run([sys.executable, '-O', str(HERE / 'fast_replay.py')], + capture_output=True, text=True) + self.assertNotEqual(process.returncode, 0) + self.assertIn('Assertions must remain enabled', process.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/joint-dual-replay-fast/verify.py b/research/joint-dual-replay-fast/verify.py new file mode 100644 index 0000000000..a1d2644b23 --- /dev/null +++ b/research/joint-dual-replay-fast/verify.py @@ -0,0 +1,287 @@ +#!/usr/bin/env python3 +"""Equivalence and controls for the joint-dual replay fast adapter. + +Checks, in order: + 1. Source-freeze binding: the historical replay/prepare/test files and both + pinned words still match the frozen `research/joint-dual/SOURCE.json` + record, so the adapter is compared against the frozen chain. + 2. Clean-word equivalence on both pinned words: legacy `replay` and the fast + adapter return equal receipts, equal to the recorded compiler receipt; + the transitions stage (delegated unchanged) equals the recorded receipt. + 3. Full literal cross-check: for every output of both words, the mask + algebra equals the historical literal scan expression. + 4. Mutation matrix: the exact twelve mutations of `tests/test_joint_reclaim.py` + on both words; the historical module is the oracle: every accept/reject + outcome agrees between legacy and fast implementations, the eleven + documented rejections reject, and the scatter-reversal case accepts with + equal receipts. + 5. Failure controls: a corrupted containment table is detected by the + cross-check; an unchecked word rejects; -O runs refuse to start. + +No timing is used as a gate; paired timings live in benchmark.py. +""" +import sys +if sys.flags.optimize: + raise ValueError('Assertions must remain enabled') + +from copy import deepcopy +import gzip +import hashlib +import json +from pathlib import Path +import subprocess +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +sys.path.insert(0, str(ROOT / 'scripts' / 'experiments')) + +import binary_frame_replay as legacy +import binary_frame_profile_prepare as legacy_prepare +import fast_replay + +WORDS = {h: ROOT / f'certificates/joint-dual-word-{h}.json.gz' for h in (23, 25)} +FREEZE = json.loads((ROOT / 'research/joint-dual/SOURCE.json').read_text()) +RECORDED = json.loads((ROOT / 'certificates/joint-dual-compiler.json').read_text()) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def sha(path): + return hashlib.sha256(Path(path).read_bytes()).hexdigest() + + +def js(value): + return json.loads(json.dumps(value)) + + +def literal_expected(triples, common, triple): + # The exact historical scan expression, written out independently here. + return sum(1 << i for i, t in enumerate(triples) + if common in t and not (set(t) & (set(triple) - {common}))) + + +def outcome(check, *args): + try: + receipt = check(*args) + except Exception as exc: # rejection class and message are recorded, not trusted + return ('reject', type(exc).__name__) + return ('accept', hashlib.sha256(json.dumps(js(receipt), sort_keys=True).encode()).hexdigest()[:16]) + + +def mutations(): + """The exact mutation matrix of tests/test_joint_reclaim.py (historical, frozen).""" + def omitted_literal_xor(word): + word['ops'].pop(0) + + def self_xor(word): + word['ops'][0][1] = word['ops'][0][0] + + def non_nested_operation_frame(word): + narrow = next(i for i, (core, cover) in enumerate(word['frames']) if core == cover) + operation = next(op for op in word['ops'] if word['frames'][op[2]][0] != word['frames'][op[2]][1]) + operation[2] = narrow + + def aliased_terminal_role(word): + word['outputs'][1][0] = word['outputs'][0][0] + + def missing_copied_center(word): + index = next(i for i, (_, _, _, target) in enumerate(word['outputs']) if len(target) == 1) + word['outputs'].pop(index) + + def omitted_transition(word): + word['events'].pop(0) + + def understated_physical_width(word): + word['R'] -= 1 + + def self_cancelling_uncharged_scatter(word): + # PR #64 (rfu08) counterexample: algebraic cancellation cannot + # authorize extra incidences absent from outputs. + outputs = {record[0] for record in word['outputs']} + slot = next(s for s in range(word['R']) if s not in outputs) + rogue = [word['v'], 2 * word['v'] + slot] + word['scatter'].extend([rogue, rogue]) + + def negative_operation_frame_index(word): + word['ops'][0][2] -= len(word['frames']) + + def cancelled_repetitions_of_paid_scatter(word): + word['scatter'].extend([word['scatter'][0], word['scatter'][0]]) + + def missing_scatter(word): + word['scatter'].pop(0) + + return [ + ('omitted_literal_xor', 'both', omitted_literal_xor), + ('self_xor', 'replay', self_xor), + ('non_nested_operation_frame', 'both', non_nested_operation_frame), + ('aliased_terminal_role', 'replay', aliased_terminal_role), + ('missing_copied_center', 'both', missing_copied_center), + ('omitted_transition', 'transitions', omitted_transition), + ('understated_physical_width', 'both', understated_physical_width), + ('self_cancelling_uncharged_scatter', 'both', self_cancelling_uncharged_scatter), + ('negative_operation_frame_index', 'replay', negative_operation_frame_index), + ('cancelled_repetitions_of_paid_scatter', 'both', cancelled_repetitions_of_paid_scatter), + ('missing_scatter', 'both', missing_scatter), + ] + + +def check_freeze(): + for name in ('scripts/experiments/binary_frame_replay.py', + 'scripts/experiments/binary_frame_profile_prepare.py', + 'tests/test_joint_reclaim.py'): + require(FREEZE['files'][name] == sha(ROOT / name), 'frozen source drift: ' + name) + for h, path in WORDS.items(): + require(FREEZE['files'][f'certificates/joint-dual-word-{h}.json.gz'] == sha(path), + f'pinned word drift: h={h}') + return dict(frozen_sources=3, pinned_words=2) + + +def check_clean_words(): + receipts = {} + for h, word in WORDS.items(): + old = js(legacy.replay(word)) + new = js(fast_replay.replay(word)) + require(old == new, f'legacy/fast replay receipts differ: h={h}') + require(old == RECORDED['axes'][str(h)]['replay'], f'receipt differs from recorded compiler receipt: h={h}') + with tempfile.TemporaryDirectory(prefix='jd-replay-fast-') as directory: + destination = Path(directory) / f'word{h}.bin' + old_transitions = js(legacy_prepare.prepare(word, destination)) + new_transitions = js(fast_replay.prepare(word, destination)) + require(old_transitions == new_transitions, f'transitions receipts differ: h={h}') + recorded = json.loads((ROOT / f'certificates/joint-dual-transitions-{h}.json').read_text()) + require(old_transitions == recorded, f'transitions receipt differs from recorded: h={h}') + receipts[h] = old + return receipts + + +def check_literal_cross_check(): + total = 0 + for h, word in WORDS.items(): + raw = json.loads(gzip.decompress(Path(word).read_bytes())) + triples, center, pair, destinations, lookup = fast_replay.tables(h) + for s, g, common, triple in raw['outputs']: + require(fast_replay.expected_mask(center, pair, common, triple) == + literal_expected(triples, common, triple), f'mask scan mismatch: h={h} output {s}') + if len(triple) == 1: + require(destinations[common] == [i for i, t in enumerate(triples) if common in t], + f'destination list mismatch: h={h}') + else: + require([lookup[tuple(triple)]] == [triples.index(tuple(triple))], + f'triple lookup mismatch: h={h}') + total += 1 + return total + + +def check_mutation_matrix(): + rows = [] + with tempfile.TemporaryDirectory(prefix='jd-mutations-') as directory: + work = Path(directory) + for h, source in WORDS.items(): + original = json.loads(gzip.decompress(Path(source).read_bytes())) + cases = [(name, scope, mutate) for name, scope, mutate in mutations()] + cases.append(('scatter_order_acceptance', 'both', None)) + for name, scope, mutate in cases: + changed = deepcopy(original) + if mutate is None: + changed['scatter'].reverse() + else: + mutate(changed) + path = work / f'word-{h}-{name}.json' + path.write_text(json.dumps(changed, separators=(',', ':')) + '\n', encoding='utf-8') + outcomes = { + 'replay': (outcome(legacy.replay, path), outcome(fast_replay.replay, path)), + 'transitions': (outcome(legacy_prepare.prepare, path, work / 'transitions.bin'), + outcome(fast_replay.prepare, path, work / 'transitions.bin')), + } + for checker, (old, new) in outcomes.items(): + require(old == new, + f'outcome differs for {name} h={h} checker={checker}: {old} vs {new}') + if mutate is not None: + checked = ('replay', 'transitions') if scope == 'both' else (scope,) + for checker in checked: + require(outcomes[checker][0][0] == 'reject', + f'historical checker did not reject {name} h={h} checker={checker}') + else: + require(outcomes['replay'][0][0] == 'accept' and outcomes['transitions'][0][0] == 'accept', + f'scatter reversal must accept in both checkers: h={h}') + rows.append(dict(h=h, mutation=name, scope=scope, + replay=outcomes['replay'][0], transitions=outcomes['transitions'][0])) + return rows + + +def check_failure_controls(): + detected = {} + for h, word in WORDS.items(): + raw = json.loads(gzip.decompress(Path(word).read_bytes())) + triples, center, pair, destinations, lookup = fast_replay.tables(h) + corrupt = [row[:] for row in pair] + corrupt[0][1], corrupt[0][2] = corrupt[0][2], corrupt[0][1] + mismatches = sum( + 1 for s, g, common, triple in raw['outputs'] + if fast_replay.expected_mask(center, corrupt, common, triple) != + literal_expected(triples, common, triple)) + require(mismatches > 0, f'corrupted table escaped the cross-check: h={h}') + clean = sum( + 1 for s, g, common, triple in raw['outputs'] + if fast_replay.expected_mask(center, pair, common, triple) != + literal_expected(triples, common, triple)) + require(clean == 0, f'clean table disagrees with literal scan: h={h}') + detected[h] = mismatches + unchecked = dict(h=3, v=1, R=1, frames=[[7, 7]], sources={'0': 0}, + ops=[], outputs=[], scatter=[], events=[[0, -1, 0]]) + with tempfile.TemporaryDirectory(prefix='jd-unchecked-') as directory: + path = Path(directory) / 'word.json' + path.write_text(json.dumps(unchecked) + '\n', encoding='utf-8') + require(outcome(fast_replay.replay, path)[0] == 'reject', 'unchecked word must reject') + require(outcome(fast_replay.prepare, path, Path(directory) / 'transitions.bin')[0] == 'reject', + 'unchecked word must reject in the transitions stage') + guarded = subprocess.run([sys.executable, '-O', str(HERE / 'fast_replay.py'), str(path)], + capture_output=True, text=True) + require(guarded.returncode != 0 and 'Assertions must remain enabled' in guarded.stderr, + '-O entry must refuse to run') + return dict(corrupted_table_mismatches=detected, unchecked_word=True, optimize_guard=True) + + +def check_frozen_suite(): + """Adoption simulation: the frozen historical test module passes unmodified + against the adapter through shim/binary_frame_replay.py (suite_arm.py).""" + process = subprocess.run([sys.executable, '-I', '-B', str(HERE / 'suite_arm.py'), str(ROOT), 'fast'], + capture_output=True, text=True, cwd=str(ROOT)) + require(process.returncode == 0, 'frozen suite arm failed:\n' + process.stdout + process.stderr) + record = json.loads(process.stdout.strip().splitlines()[-1]) + require(record['failures'] == 0 and record['errors'] == 0 and record['tests'] > 0, + f'frozen suite did not pass against the adapter: {record}') + require('joint-dual-replay-fast' in record['replay_module'].replace('\\', '/'), + f'frozen suite did not use the adapter: {record}') + return dict(frozen_suite_tests=record['tests'], frozen_suite_seconds=record['seconds']) + + +def verify(): + freeze = check_freeze() + receipts = check_clean_words() + outputs = check_literal_cross_check() + rows = check_mutation_matrix() + controls = check_failure_controls() + controls.update(check_frozen_suite()) + result = dict( + status='PASS_JOINT_DUAL_REPLAY_FAST_EQUIVALENCE', + words=sorted(receipts), outputs_cross_checked=outputs, + mutation_cases=len(rows), mutation_rows=rows, + retained_checks='historical check_word, every replay assertion and both full-basis orientations, the unchanged transitions stage, and the frozen tests/test_joint_reclaim.py matrix as oracle', + invalidation='containment tables are rebuilt from the word on every call; no persistent cache; source-freeze and word pins checked each run', + controls=controls, freeze=freeze, + scope='Opt-in adapter equivalence on the two frozen joint-dual words; no kappa, certificate, supplier or frontier change.') + print(json.dumps(result, indent=2, sort_keys=True)) + return result + + +if __name__ == '__main__': + result = verify() + if '--record' in sys.argv[1:]: + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n', encoding='utf-8')