From 0669abfe0d82b7150f3f215dad6b4eaf324e2ce7 Mon Sep 17 00:00:00 2001 From: ross Date: Wed, 14 Oct 2026 16:53:02 +1100 Subject: [PATCH] Speed exact PR886 frame closure with one modular basis --- .../bit-frame-closure-basis/BENCHMARK.json | 251 ++++++++++++++++++ .../bit-frame-closure-basis/EXPECTED.json | 137 ++++++++++ research/bit-frame-closure-basis/PROOF.md | 82 ++++++ research/bit-frame-closure-basis/README.md | 133 ++++++++++ research/bit-frame-closure-basis/SOURCES.json | 48 ++++ research/bit-frame-closure-basis/TASK.json | 135 ++++++++++ .../bit-frame-closure-basis/VALIDATION.md | 75 ++++++ research/bit-frame-closure-basis/VERIFY.json | 25 ++ research/bit-frame-closure-basis/benchmark.py | 66 +++++ research/bit-frame-closure-basis/closure.py | 87 ++++++ research/bit-frame-closure-basis/run.py | 116 ++++++++ .../bit-frame-closure-basis/test_closure.py | 182 +++++++++++++ research/bit-frame-closure-basis/verify.py | 70 +++++ 13 files changed, 1407 insertions(+) create mode 100644 research/bit-frame-closure-basis/BENCHMARK.json create mode 100644 research/bit-frame-closure-basis/EXPECTED.json create mode 100644 research/bit-frame-closure-basis/PROOF.md create mode 100644 research/bit-frame-closure-basis/README.md create mode 100644 research/bit-frame-closure-basis/SOURCES.json create mode 100644 research/bit-frame-closure-basis/TASK.json create mode 100644 research/bit-frame-closure-basis/VALIDATION.md create mode 100644 research/bit-frame-closure-basis/VERIFY.json create mode 100644 research/bit-frame-closure-basis/benchmark.py create mode 100644 research/bit-frame-closure-basis/closure.py create mode 100644 research/bit-frame-closure-basis/run.py create mode 100644 research/bit-frame-closure-basis/test_closure.py create mode 100644 research/bit-frame-closure-basis/verify.py diff --git a/research/bit-frame-closure-basis/BENCHMARK.json b/research/bit-frame-closure-basis/BENCHMARK.json new file mode 100644 index 0000000000..b81c66186f --- /dev/null +++ b/research/bit-frame-closure-basis/BENCHMARK.json @@ -0,0 +1,251 @@ +{ + "status": "PASS_BIT_FRAME_CLOSURE_BENCHMARK", + "samples": [ + { + "pair": 0, + "order": [ + "reference", + "basis" + ], + "engines": { + "reference": { + "seconds": 30.93506745796185, + "cases": { + "pr589": { + "seconds": 10.3824437080184, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 10.024701665970497, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 10.527642667060718, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + }, + "basis": { + "seconds": 5.71508595906198, + "cases": { + "pr589": { + "seconds": 1.9619243339402601, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 1.7693556669401005, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 1.983572750003077, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + } + } + }, + { + "pair": 1, + "order": [ + "basis", + "reference" + ], + "engines": { + "basis": { + "seconds": 5.703479459043592, + "cases": { + "pr589": { + "seconds": 1.9423902080161497, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 1.7954174579354003, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 1.9654521669726819, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + }, + "reference": { + "seconds": 30.964114416972734, + "cases": { + "pr589": { + "seconds": 10.366719332989305, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 10.102655207971111, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 10.494463707902469, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + } + } + }, + { + "pair": 2, + "order": [ + "reference", + "basis" + ], + "engines": { + "reference": { + "seconds": 32.6134802919114, + "cases": { + "pr589": { + "seconds": 10.703001499990933, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 10.765563208027743, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 11.144659584038891, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + }, + "basis": { + "seconds": 5.907537999912165, + "cases": { + "pr589": { + "seconds": 2.030974750057794, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 1.8459598339395598, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 2.0303760420065373, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + } + } + }, + { + "pair": 3, + "order": [ + "basis", + "reference" + ], + "engines": { + "basis": { + "seconds": 6.311234583030455, + "cases": { + "pr589": { + "seconds": 2.0816027499968186, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 2.063415333046578, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 2.1659246659837663, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + }, + "reference": { + "seconds": 43.282476166961715, + "cases": { + "pr589": { + "seconds": 12.81674420798663, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 15.084301250055432, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 15.380409959005192, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + } + } + }, + { + "pair": 4, + "order": [ + "reference", + "basis" + ], + "engines": { + "reference": { + "seconds": 50.12656000000425, + "cases": { + "pr589": { + "seconds": 15.884748458047397, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 14.376700167078525, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 19.864370208000764, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + }, + "basis": { + "seconds": 9.401485707960092, + "cases": { + "pr589": { + "seconds": 3.2756130000343546, + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + }, + "pr555": { + "seconds": 2.9492821249878034, + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + }, + "degraded": { + "seconds": 3.175984041998163, + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + } + } + } + } + } + ], + "median_suite_seconds": { + "reference": 32.6134802919114, + "basis": 5.907537999912165 + }, + "suite_ratio": 5.520655185357471, + "median_case_seconds": { + "pr589": { + "reference": 10.703001499990933, + "basis": 2.030974750057794 + }, + "pr555": { + "reference": 10.765563208027743, + "basis": 1.8459598339395598 + }, + "degraded": { + "reference": 11.144659584038891, + "basis": 2.0303760420065373 + } + }, + "finished_at": "2026-10-14T05:45:21.412584+00:00", + "python": "3.12.12 (main, Oct 9 2025, 11:07:00) [Clang 17.0.0 (clang-1700.6.3.2)]", + "executable": "/opt/homebrew/opt/python@3.12/bin/python3.12", + "platform": "macOS-26.5.2-arm64-arm-64bit", + "implementation_sha256": { + "closure.py": "febc46cb43be709684bb51e48bc2c849b63f02809e2bf5bb461c62d55953c4fd", + "run.py": "4e40c4497143ee2525028c78fcf527e6690761a984eb132e74d30c50081b8698", + "benchmark.py": "d579af460de5d8b076403714c17ba8595d900ad6a5c51d84f5e63ab28723ade4", + "EXPECTED.json": "dac0e71d005bf700444f866209f588fef2a276ea6ce2cf17b6279e7881a5647e", + "SOURCES.json": "b94b723b5585ec673b82da156b50afa28b9122d441616f4a282754fed8b7dea8" + }, + "scope": "Three complete pinned checker cases in fresh interpreters per engine; same sources, closure inventories and receipts; warm OS caches; no timing acceptance threshold or selected-replay claim." +} diff --git a/research/bit-frame-closure-basis/EXPECTED.json b/research/bit-frame-closure-basis/EXPECTED.json new file mode 100644 index 0000000000..c8703852e7 --- /dev/null +++ b/research/bit-frame-closure-basis/EXPECTED.json @@ -0,0 +1,137 @@ +{ + "pr589": { + "case": "pr589", + "closure_count": 2202, + "closure_sha256": "a087c5752bcc03a7a2e9107588cd0c564079aa94ca1e9f5ab794039b891c2bcd", + "receipt": { + "assignments_enumerated": 398, + "component_sizes": { + "1": 119, + "2": 4, + "3": 9, + "5": 1 + }, + "components": 133, + "degraded_start": false, + "exact_interval_comparisons": true, + "free_gates": 159, + "gates": 5472, + "improving_components": 0, + "non_nesting_rejected": 55, + "optimum_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rational_rank_justified_by_hadamard": true, + "same_profile_alternatives": 10, + "smallest_alternative_delta": 0.0009110061088407877, + "start_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "weighted_cost_delta": 0.0, + "word": "bitE8mut-p111-tuned.json.gz" + }, + "stdout_sha256": "c2b934b04670760a1d3001e1dbe56935a217344e84550b120dce7e294ca2ab3f" + }, + "pr555": { + "case": "pr555", + "closure_count": 2073, + "closure_sha256": "aefeca30d9bb745c04216b55332f4567f44e700f38b22a072d53be8c72aece9a", + "receipt": { + "assignments_enumerated": 360, + "component_sizes": { + "1": 121, + "2": 3, + "3": 8, + "5": 1 + }, + "components": 133, + "degraded_start": false, + "exact_interval_comparisons": true, + "free_gates": 156, + "gates": 5468, + "improving_components": 0, + "non_nesting_rejected": 42, + "optimum_profile": { + "1": 1321, + "2": 1342, + "3": 80, + "4": 47, + "5": 102, + "6": 10, + "7": 18 + }, + "rational_rank_justified_by_hadamard": true, + "same_profile_alternatives": 9, + "smallest_alternative_delta": 0.0009108085751431813, + "start_profile": { + "1": 1321, + "2": 1342, + "3": 80, + "4": 47, + "5": 102, + "6": 10, + "7": 18 + }, + "weighted_cost_delta": 0.0, + "word": "bitE8mut-p111.json.gz" + }, + "stdout_sha256": "a96847c1e6b43991aab44001622b6ab3bec51f766df8da6572af2f4bc51b95a6" + }, + "degraded": { + "case": "degraded", + "closure_count": 2202, + "closure_sha256": "a087c5752bcc03a7a2e9107588cd0c564079aa94ca1e9f5ab794039b891c2bcd", + "receipt": { + "assignments_enumerated": 398, + "component_sizes": { + "1": 119, + "2": 4, + "3": 9, + "5": 1 + }, + "components": 133, + "degraded_start": true, + "exact_interval_comparisons": true, + "free_gates": 159, + "gates": 5472, + "improving_components": 37, + "non_nesting_rejected": 55, + "optimum_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rational_rank_justified_by_hadamard": true, + "same_profile_alternatives": 8, + "smallest_alternative_delta": -0.009078931270804107, + "start_profile": { + "1": 1446, + "2": 1326, + "3": 49, + "4": 44, + "5": 103, + "6": 10, + "7": 19 + }, + "weighted_cost_delta": -0.21588258900786786, + "word": "bitE8mut-p111-tuned.json.gz" + }, + "stdout_sha256": "c1aa53b899416466584efa27bf591b7d5818339f8d15d17dc05c2eb2b5c4ccf7" + } +} diff --git a/research/bit-frame-closure-basis/PROOF.md b/research/bit-frame-closure-basis/PROOF.md new file mode 100644 index 0000000000..a086311e8a --- /dev/null +++ b/research/bit-frame-closure-basis/PROOF.md @@ -0,0 +1,82 @@ +# Why the one-basis closure is equivalent + +Let the immutable live-line table be integer vectors `L_i` of dimension `d`, +and let `p = 2147483647`. For a nonempty mask `M`, the frozen PR886 checker +forms `S = {L_i : i in M}` and returns + +``` +({i : rank_p(S union {L_i}) = rank_p(S)}, rank_p(S)). +``` + +It includes selected lines without a second rank call. The new implementation +returns the same pair by constructing one echelon basis of `span_p(S)` and +testing each remaining line for membership in that basis. This is an exact +linear-algebra identity over the fixed prime field, not a probabilistic test. + +## Basis construction and membership + +Process selected rows in their original order. Reduce a row against the +existing unit-pivot rows, in increasing pivot order. Each subtraction is a row +operation, so the residual differs from the original row by an element of the +existing span. A zero residual adds no dimension. Otherwise normalize its +first nonzero coordinate using its inverse in the field and insert the row at +that pivot. The new pivot is absent from the existing basis, so the new row is +independent. Earlier coordinates of a row with a later pivot are zero; sorting +the pivots therefore preserves echelon form even when a new pivot precedes a +previously inserted one. Induction gives exactly `span_p(S)` and its dimension. + +For any candidate line, subtract the basis rows in increasing pivot order. +Later rows cannot reintroduce an earlier pivot. A zero residual means the line +was a combination of the basis rows. Conversely, a combination reduces to zero +by that elimination. The membership predicate is therefore equivalent to the +frozen `rank_p(S union {L_i}) == rank_p(S)` predicate. If the basis has `d` +pivots, it spans the entire coordinate space and every live line is admitted. + +The empty-mask result remains `(0, 0)`, exactly the reference's explicit +convention. Actual E8 live lines are nonzero. Synthetic zero-line tests retain +that empty convention and check ordinary span membership for nonempty masks. + +## Why the modular rank is the rational rank here + +Both the integrated reference and the new factory enforce the sufficient +Hadamard guard + +``` +B^d < p^2, where B = max_i sum_j L_ij^2. +``` + +For any nonzero `k` by `k` minor of original live rows, `k <= d`, Hadamard gives +`det^2 <= B^k <= B^d < p^2` when `B >= 1`. Thus its nonzero integer determinant +has absolute value below `p` and remains nonzero modulo `p`. Vanishing integer +minors also vanish modulo `p`, so every subset of live rows has the same rank +over the rationals and the prime field. The `B = 0` case has rank zero over +both. This covers augmented sets used in membership tests as well. No guard +about large coefficients in an intermediate modular basis is necessary: the +minor argument applies to the original integer rows. + +The test table containing `p*e_1` shows why the guard matters: rational rank is +one while its modular rank is zero. The factory rejects that table. This is +a concrete failure control, not a claim that this sufficient guard is necessary. + +## Coverage preserved by the adapter + +Five consumed files are admitted by their pinned SHA256 bytes before execution. +The adapter replaces only the top-level `close` function in the parsed frozen +checker. The resulting code is compiled with `optimize=0`; optimized CLI +invocations are additionally refused. All original frame catalogue checks, +least/greatest bounds, options, component enumeration, nesting rejection, +paid profiles, rational moment intervals and selected-minimum comparisons run. +All other AST statements, including the original `rank` function and assertion +sites, remain present. Existing sources and defaults are not edited. + +The cache uses precisely the old input-mask boundary. It starts empty for each +word execution, and the factory copies its line coordinates into immutable +tuples. There is no persistent cache, cross-word reuse, changed pricing, or +enumeration pruning. Complete differential replay compares every mask, closed +mask and rank, not just the final optimum. Receipt equality includes the +reference's full printed JSON through an exact stdout digest. + +This argument establishes the closure algorithm's equivalence under the stated +domain. The accompanying finite replay corroborates its implementation. Neither +is a formal proof of the full multiplication theorem, a new frame optimum, or +an extension of the predecessor's fixed-word search domain. diff --git a/research/bit-frame-closure-basis/README.md b/research/bit-frame-closure-basis/README.md new file mode 100644 index 0000000000..e01fa237b7 --- /dev/null +++ b/research/bit-frame-closure-basis/README.md @@ -0,0 +1,133 @@ +# One-basis closure for the historical PR886 bit-frame audit + +**Verification tooling; no new kappa.** This opt-in adapter accelerates Seth +Burkart's incorporated PR886 checker on its exact PR589 and PR555 words and +degraded PR589 positive control. It preserves every complete receipt, every +closure result, every enumerated assignment and the exact moment comparisons. +No source, default verifier, selected record or `upstream/` file is changed. + +The old closure routine computes a fresh modular rank for each candidate line. +The replacement builds one echelon basis per input mask and reduces remaining +lines against it. The original sufficient Hadamard guard still justifies +rational rank; the implementation also enforces that guard without assertions. +See [PROOF.md](PROOF.md) for the equivalence argument and its precise domain. + +## Reproduce + +From a full repository checkout, using standard-library Python 3.12: + +```sh +python3.12 scripts/research_package.py --package research/bit-frame-closure-basis +``` + +Expected: nine test groups pass, `PASS_BIT_FRAME_CLOSURE_BASIS` reports the +three rows below with `no_new_kappa: true`, and the registered runner prints +`PASS_REGISTERED_RESEARCH_PACKAGE research/bit-frame-closure-basis outcome=completed`. + +| Complete case | Closure entries compared | Assignments | Non-nesting rejected | Improving components | +| --- | ---: | ---: | ---: | ---: | +| PR589 tuned word | 2,202 | 398 | 55 | 0 | +| PR555 base word | 2,073 | 360 | 42 | 0 | +| Degraded PR589 control | 2,202 | 398 | 55 | 37 | + +The 6,477 closure entries are compared directly between the reference and +candidate, including their input masks, closed masks and ranks. They are a +sum across three cases, not a claim of 6,477 distinct mathematical masks. +`EXPECTED.json` was generated using only the unchanged reference. Both engines +must match its complete reports and original stdout digests. The degraded +control must recover the exact tuned profile. + +A single opt-in execution is: + +```sh +python3 -I -B research/bit-frame-closure-basis/run.py --case pr589 --engine basis +``` + +Use `--engine reference` for the frozen checker. The wrapper prints its entire +original receipt plus closure inventory hashes. `--closure-output /tmp/fresh.json` +also exports every closure; the destination must be fresh and outside the repo. +The wrapper rejects `-O`; the verifier launches assertion-enabled isolated +children even if its parent inherited `PYTHONOPTIMIZE`. + +## Performance experiment + +The orientation profile found 179,707 rank calls consuming 9.55 of 11.99 +instrumented seconds on the tuned word. Those profiler numbers motivated the +change; they are not the benchmark speedup. The first uninstrumented complete +comparison measured 10.05 s to 1.85 s and matched all 2,202 closures. Repeated +measurements give median complete-suite time **32.61348 s to 5.90754 s +(5.52066x)** on macOS arm64 / CPython 3.12.12, over five alternating pairs. +Every raw sample and the implementation hashes are retained in `BENCHMARK.json`. +The verifier checks those bindings and the timing summary arithmetic without +requiring a speed threshold. See `VALIDATION.md` for the executed checks. + +Repeat the alternating benchmark with a fresh external output path: + +```sh +python3.12 -I -B research/bit-frame-closure-basis/benchmark.py --pairs 5 \ + --output /tmp/bit-frame-closure-benchmark.json +``` + +Each engine runs all three complete cases in fresh interpreters, with source +admission, the full enumeration, exact arithmetic, output serialization and +receipt comparison. Pair order alternates. OS caches are not flushed; timings +are local descriptive measurements on a shared host, not a performance gate. +No selected-frontier replay or multiplication-runtime speedup follows. + +## Independent checks and failure controls + +The separate Fraction Gauss-Jordan oracle checks 1,100 cases: all 512 masks of +a nine-row synthetic table, all 16 masks under all 24 permutations of a +four-row nonunit-pivot table, and 111 E8 singletons plus 93 seeded E8 masks of +sizes zero through ten. These are bounded implementation checks, not an +exhaustive enumeration of all subsets of 111 lines. Seed 93 fixes the extra +masks; the actual reference closure inventory is checked in full separately. + +Failure controls catch false membership, lost pivots, a rational/modular alias +outside the Hadamard domain, malformed coordinates and masks, stale cross-word +state, corruption of each of the five consumed inputs, missing or duplicate +pins, missing or duplicate adaptation anchors, and disabled inherited +assertions. The mathematical negative controls exercise the kernel beyond +source-hash rejection. Normal and optimized-parent execution are distinguished +in `VALIDATION.md`. + +## Scope, provenance and credit + +Base: `2de86c77b4127d2f01f504e0c7c5e4db737caa3c`. The selected record at that +base is PR1094's conditional `836330098538459/500000000000000000`; this package +does not change or re-prove it. `SOURCES.json` pins exact input Git blobs and +SHA256 bytes, with historical selected-record/catalogue provenance. `TASK.json` +records the assignment, three considered tasks, local claim, stopping rule and +overlap coverage. No pinned sprint coordination issue existed. + +Seth Burkart (`SethBurkart123`) supplied PR886, source head +`881f72ec596a5c6d7aba801153792292ecc39737`, with disclosed Claude Code assistance. +This package uses the **integrated refinement**, whose exact interval comparisons +and Hadamard guard were added in maintainer commit +`3b83e4f14825ce1ae038a8c8159f130646991086`, rather than the submitted floating-point +decision logic. Credit Douglas Colkitt for that review and arithmetic integration. +DreamingOfClouds supplied PR589's word and tuner on eumemic's PR555 and the +PR543/545/510 lineage. All predecessor files and notices remain in place. + +CubeJerry's pending PR1459/1461 use related basis/annihilator ideas for rational +frame containment in different historical checkers. Sagar Thakrar's PR1433 +batches a different Boolean omission replay. Those are related verification +work, not dependencies or priority claims for basic elimination reuse. +PR933/1345 investigate distinct gate-reordering classes; this work neither +reopens those searches nor changes PR886's fixed-word conclusion. + +Only the historical frame audit is accelerated. Native supplier admission, +physical hosting, a selected cold replay, all-size compiler/realization, +precision/tape, analytic transfer and a full Lean multiplication theorem are +outside this package. Hosted CI is reported separately from local checks. + +New material: Ross Richardson with substantial OpenAI Codex assistance in +implementation, proof explanation, tests and validation. Apache-2.0; no +subagents were used. + +## Open next questions + +Profile one pinned PR933 or PR1345 transport checker to see whether closure is +also a material cost there. Its mutable-state and rank contracts must be +checked before reuse. This package supplies no speed or correctness claim for +those checkers; `TASK.json` records that first step and its blockers. diff --git a/research/bit-frame-closure-basis/SOURCES.json b/research/bit-frame-closure-basis/SOURCES.json new file mode 100644 index 0000000000..c2b1c694d9 --- /dev/null +++ b/research/bit-frame-closure-basis/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "2de86c77b4127d2f01f504e0c7c5e4db737caa3c", + "files": [ + { + "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/bit589-frame-optimum/frameopt.py", + "usage": "input", + "git_blob": "1622844ff90529c47e539f502c92b4f2371524e9", + "sha256": "d18d5ed96a6d3146b2141b9bdd29900dd612defdcd5ebc7040542064ec89f237" + }, + { + "path": "research/bit589-frame-optimum/verify.sh", + "usage": "input", + "git_blob": "4352170bc26141d630140647c2181f142289dd55", + "sha256": "eb69e2482686dd61f7727d58dc0ecd0aec5d34739b5d9b887f3c0b54c16f1c52" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", + "usage": "input", + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + { + "path": "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz", + "usage": "input", + "git_blob": "bdbb95aa970647bd52895c120b494f0f591f3f87", + "sha256": "1bc3c53d4baf4927c6a00c339ea3975516471a48074d4d97c6addaded2a4d858" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + } + ] +} diff --git a/research/bit-frame-closure-basis/TASK.json b/research/bit-frame-closure-basis/TASK.json new file mode 100644 index 0000000000..671dd702a8 --- /dev/null +++ b/research/bit-frame-closure-basis/TASK.json @@ -0,0 +1,135 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 3, + "base_commit": "2de86c77b4127d2f01f504e0c7c5e4db737caa3c", + "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": "Accelerate only PR886 frameopt.close on pinned PR589, PR555, and the degraded PR589 positive control by retaining one modular basis per closure; preserve the complete enumeration and receipt.", + "scope_change_reason": "The seed-93 engineering assignment chooses a historical exact checker with a measured elimination bottleneck, rather than the newest selected supplier.", + "bottleneck_link": "Reduces repeat review cost for a finite frame-only obstruction; this is verifier throughput, not a supplier or multiplication-runtime gain.", + "budget_minutes": 60, + "stop_rule": "60 minute session from 2026-10-14 05:27 UTC; select by 05:39, freeze implementation by 06:12 and finish by 06:27. Stop if identical full receipts and actual before/after gain cannot be established.", + "outcome": "completed", + "evidence": "EXPECTED.json contains unchanged reference receipts and all closure inventory hashes; verify.py compares all returned closures between both engines and runs nine independent rational-oracle/failure-control groups. BENCHMARK.json records alternating complete-case timings.", + "author": "Ross Richardson with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in implementation, mathematical explanation, controls and validation; no subagents.", + "open_questions": [ + { + "question": "Does the same one-basis closure implementation accelerate the nearby PR933 or PR1345 transport searches?", + "why_it_matters": "Their larger repeated frame computations may benefit from the same exact rank membership mechanism.", + "first_step": "Pin one of those checkers, profile its actual closure workload and check its complete coverage and source contract before attempting an adapter.", + "blocked_by": "Not tested here; mutable line sets or different rank guards would need separate source admission and correctness checks." + } + ], + "assignment_seed": 93, + "assignment_draw_note": "initial stdout-only draw lost in truncated batched output; this retained draw is the assignment", + "claim": { + "location": "local; pinnedIssues inventory empty at 05:27 UTC", + "claimed_at": "2026-10-14T05:33:00Z", + "expected_finish": "2026-10-14T06:27:00Z", + "expected_deliverable": "Opt-in source-pinned closure adapter, exact differential controls and alternating whole-check benchmarks; no new kappa", + "result": { + "status": "completed", + "summary": "Complete PR886 suite median 32.61348s to 5.90754s (5.52066x); all 6477 closures and 1156 assignments preserved; no new kappa.", + "artifact": "research/bit-frame-closure-basis/README.md", + "reproduce": "python3.12 scripts/research_package.py --package research/bit-frame-closure-basis", + "updated_at": "2026-10-14T05:52:00Z" + } + }, + "candidate_tasks": [ + { + "task": "PR1096 positive prefix triple-evaluation reuse", + "decision": "Not selected: profile shows under one second in the two replays; smaller full-check opportunity." + }, + { + "task": "PR886 one-basis modular frame closure", + "decision": "Selected: one profiled tuned-word run spends 9.55 of 11.99 instrumented seconds in 179707 rank eliminations." + }, + { + "task": "Selected PR1042 phase recipe sparse compilation", + "decision": "Not selected: directly overlaps open PR1646 and its credited PR1029/1041 lineage." + } + ], + "overlap": { + "checked_at": "2026-10-14T05:30:37Z", + "open_prs": 532, + "discussions": 302, + "complete_pagination": true, + "warnings": [], + "nearby": { + "886": "Frozen frame-only result being accelerated, not a reopened search.", + "933": "Gate relocation and Steinberg class; distinct mathematical domain.", + "1345": "Transport-local optimum; no closure accelerator claimed in inspected body.", + "1459": "Exact rational-frame containment adapter; related elimination reuse, different checker and arithmetic.", + "1461": "Exact rational annihilator adapter; related containment algebra, different checker and arithmetic.", + "1646": "Selected sparse phase recipe accelerator; excluded candidate." + }, + "limitations": "Titles/bodies/comments/replies and local README/TASK/ledger; no exhaustive code-diff novelty claim.", + "final_refresh": { + "searched_at": "2026-10-14T05:45:24.773378+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T05:44:11.140613+00:00", + "complete_pagination": true, + "records": 536 + }, + "discussions": { + "fetched_at": "2026-10-14T05:45:24.710901+00:00", + "complete_pagination": true, + "records": 310 + } + }, + "warnings": [], + "matched_records": 11, + "conclusion": "Inspected returned leads; no duplicate adapter for PR886 close found. The remote search is not an exhaustive code-diff novelty check." + } + }, + "current_main_compatibility": { + "head": "a18b4b0136d647529971e9fcb99fa83f5b9a0b81", + "checks": { + "certificates/selected-result.json": true, + "research/bit589-frame-optimum/frameopt.py": true, + "research/bit589-frame-optimum/verify.sh": true, + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py": true, + "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz": true, + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": true + } + } +} diff --git a/research/bit-frame-closure-basis/VALIDATION.md b/research/bit-frame-closure-basis/VALIDATION.md new file mode 100644 index 0000000000..0d4b1da781 --- /dev/null +++ b/research/bit-frame-closure-basis/VALIDATION.md @@ -0,0 +1,75 @@ +# Local validation receipt — 2026-10-14 + +Base: `2de86c77b4127d2f01f504e0c7c5e4db737caa3c`. Assignment seed: 93. +All changes are confined to `research/bit-frame-closure-basis/`. +`upstream/`, the selected record, frozen words and predecessor code are unchanged. + +## Exact execution and controls + +- Python 3.12.12: complete paired reference/basis replay passes for PR589, + PR555 and degraded PR589. Every one of the 6,477 returned closure entries and + all three complete reports agree. The unchanged enumeration visits 1,156 + assignments; the degraded fixture recovers the tuned word's paid profile. +- The registered package runner and exact Git/SHA source metadata check pass. + The ninth control group binds the benchmark to its code, case coverage, + receipts and summary arithmetic. No mathematical kernel changed after timing. +- All nine current control groups pass under an optimized Python 3.12 parent. + The adapter rejects optimized direct execution and compiles the inherited + checker with assertions enabled; its ordinary child runs use `-I -B`. +- A minimal source export containing only this package and the five consumed + inputs passes the complete paired replay and all nine groups under Python + 3.14.6. Every exported file was mode 0444 and every directory mode 0555. The + command ran from `/private/tmp`, outside the export, with `-I -O -B` on the + parent verifier and inherited `PYTHONOPTIMIZE=2`. Its children still had + assertions enabled. No Git metadata or precomputed cache was required for + this direct `verify.py` replay; the registered metadata command separately + needs the pinned Git history. +- `make selected-record-check` passes for the unchanged conditional + `836330098538459/500000000000000000` record. This is a source-binding check, + not the selected construction's cold replay. + +The exact rational oracle checks 1,100 bounded cases. Controls detect wrong +membership and rank, unsafe modular aliasing, malformed inputs, cross-word +cache misuse, five changed input files, missing/duplicate inventory entries, +missing/duplicate adapter anchors, optimized inherited execution, and stale or +incomplete benchmark evidence. The new code uses explicit failure checks. + +## Same-input benchmark + +Five alternating pairs, each engine running the identical three-case suite in +fresh interpreters. macOS 26.5.2 arm64, CPython 3.12.12; normal OS caching. + +| Workload | Reference median seconds | Basis median seconds | +| --- | ---: | ---: | +| PR589 | 10.70300 | 2.03097 | +| PR555 | 10.76556 | 1.84596 | +| Degraded PR589 | 11.14466 | 2.03038 | +| Complete three-case suite | **32.61348** | **5.90754** | + +Ratio of suite medians: **5.52066x**. The suite median is computed from complete +pair totals, not by summing per-case medians. Reference totals range from +30.93507 to 50.12656 seconds; basis totals range from 5.70348 to 9.40149 seconds. +All samples, including the slower fourth and fifth pairs on the shared host, +are retained in `BENCHMARK.json`. No samples were discarded. Each timed result +matches the same full receipt and closure inventory hash. Its code, source +manifest and expected-result hashes are checked by the package verifier. +There is no timing-based acceptance test. + +## Coordination and handoff boundary + +The final overlap snapshot at 05:45 UTC paginated 536 open PRs and 310 +Discussion records, with no warnings. Exact checker-path and closure-related +searches found no duplicate PR886 adapter in the inspected records. PR933 and +PR1345 remain distinct transport-search work; PR1459/1461 concern different +rational-frame containment checkers. These searches do not inspect every code +diff and are not a novelty proof. + +Current-main compatibility was checked at +`a18b4b0136d647529971e9fcb99fa83f5b9a0b81`: all five consumed Git blobs and the +selected-record blob are identical to the pinned base. The package retains its +original base and historical provenance instead of moving those pins. + +The contribution is ready for independent review as verification tooling. +No selected-frontier cold replay, native/physical supplier admission, Lean +build, full historical suite or multiplication theorem is claimed. Hosted CI +and publication are external handoff state, not established by this receipt. diff --git a/research/bit-frame-closure-basis/VERIFY.json b/research/bit-frame-closure-basis/VERIFY.json new file mode 100644 index 0000000000..c73f3068f7 --- /dev/null +++ b/research/bit-frame-closure-basis/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit589-frame-optimum/frameopt.py", + "research/bit589-frame-optimum/verify.sh", + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", + "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Three full reference/basis pairs; all 6477 closure mask/rank entries, 1156 assignments, complete receipts, rational oracles and meaningful failure controls." + } + ] +} diff --git a/research/bit-frame-closure-basis/benchmark.py b/research/bit-frame-closure-basis/benchmark.py new file mode 100644 index 0000000000..2de10277f5 --- /dev/null +++ b/research/bit-frame-closure-basis/benchmark.py @@ -0,0 +1,66 @@ +"""Alternating fresh-process comparisons of the identical complete PR886 suite.""" +import argparse +import datetime +import json +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import run + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--pairs", type=int, default=5) + parser.add_argument("--output", type=Path, required=True) + args = parser.parse_args() + run.require(1 <= args.pairs <= 20, "pairs must be 1..20") + destination = args.output.resolve() + run.require(not destination.exists() and not destination.is_relative_to(run.ROOT), + "use a fresh external benchmark path") + run.check_sources() + expected = json.loads((HERE / "EXPECTED.json").read_text()) + samples = [] + for pair in range(args.pairs): + order = ("reference", "basis") if pair % 2 == 0 else ("basis", "reference") + sample = {"pair": pair, "order": list(order), "engines": {}} + for engine in order: + cases = {} + start_suite = time.perf_counter() + for case in run.CASES: + start = time.perf_counter() + process = subprocess.run([sys.executable, "-I", "-B", str(HERE / "run.py"), + "--case", case, "--engine", engine], capture_output=True, text=True, timeout=150) + seconds = time.perf_counter() - start + run.require(process.returncode == 0, engine + " " + case + ": " + process.stderr) + report = json.loads(process.stdout) + run.require(report == expected[case], "timed full receipt: " + case) + cases[case] = {"seconds": seconds, "report_sha256": run.sha(run.canonical(report).encode())} + sample["engines"][engine] = {"seconds": time.perf_counter() - start_suite, "cases": cases} + samples.append(sample) + print("PAIR", pair, {k: round(v["seconds"], 4) for k, v in sample["engines"].items()}, flush=True) + medians = {engine: statistics.median(s["engines"][engine]["seconds"] for s in samples) + for engine in ("reference", "basis")} + case_medians = {case: {engine: statistics.median(s["engines"][engine]["cases"][case]["seconds"] + for s in samples) for engine in medians} for case in run.CASES} + result = {"status": "PASS_BIT_FRAME_CLOSURE_BENCHMARK", "samples": samples, + "median_suite_seconds": medians, "suite_ratio": medians["reference"] / medians["basis"], + "median_case_seconds": case_medians, + "finished_at": datetime.datetime.now(datetime.timezone.utc).isoformat(), + "python": sys.version, "executable": sys.executable, "platform": platform.platform(), + "implementation_sha256": {name: run.sha((HERE / name).read_bytes()) + for name in ("closure.py", "run.py", "benchmark.py", "EXPECTED.json", "SOURCES.json")}, + "scope": "Three complete pinned checker cases in fresh interpreters per engine; same sources, closure inventories and receipts; warm OS caches; no timing acceptance threshold or selected-replay claim."} + with destination.open("x") as stream: + json.dump(result, stream, indent=2) + stream.write("\n") + print(result["status"], "ratio=" + str(result["suite_ratio"])) + + +if __name__ == "__main__": + main() diff --git a/research/bit-frame-closure-basis/closure.py b/research/bit-frame-closure-basis/closure.py new file mode 100644 index 0000000000..df194142ca --- /dev/null +++ b/research/bit-frame-closure-basis/closure.py @@ -0,0 +1,87 @@ +"""Exact modular closure with one echelon basis per input mask. + +Ross Richardson with substantial OpenAI Codex assistance. Apache-2.0. +The closure contract and Hadamard guard follow Seth Burkart's PR886 as +refined during maintainer integration. See README.md for scope and credit. +""" + +PRIME = 2147483647 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def echelon(rows, width): + """An increasing-pivot, unit-pivot basis over the fixed prime field.""" + basis = [] + for source in rows: + row = [x % PRIME for x in source] + for pivot, vector in basis: + factor = row[pivot] + if factor: + for j in range(pivot, width): + row[j] = (row[j] - factor * vector[j]) % PRIME + pivot = next((j for j, x in enumerate(row) if x), None) + if pivot is not None: + inverse = pow(row[pivot], -1, PRIME) + row = tuple(x * inverse % PRIME for x in row) + basis.append((pivot, row)) + basis.sort(key=lambda item: item[0]) + return basis + + +def contains(source, basis, width): + row = [x % PRIME for x in source] + for pivot, vector in basis: + factor = row[pivot] + if factor: + for j in range(pivot, width): + row[j] = (row[j] - factor * vector[j]) % PRIME + return not any(row) + + +def make_close(lines, count, cache): + """Return the PR886 close(mask) contract on this immutable line table. + + The table and cache are private to one checker execution. No result is + reused between words or processes. Check the guard even if the caller + disabled assertions; rational equivalence needs this domain restriction. + """ + require(type(count) is int and count > 0 and count == len(lines), + "line count") + vectors = tuple(tuple(row) for row in lines) + width = len(vectors[0]) + require(width > 0 and all(len(row) == width for row in vectors), + "rectangular nonempty coordinates") + require(all(type(x) is int for row in vectors for x in row), + "integer coordinates") + norm = max(sum(x*x for x in row) for row in vectors) + require(norm ** width < PRIME ** 2, "Hadamard guard") + require(not cache, "fresh per-word cache") + full = (1 << count) - 1 + + def close(mask): + # This is the same input-mask cache boundary as the frozen checker. + if mask not in cache: + require(type(mask) is int and 0 <= mask <= full, "line mask") + if mask == 0: + # Preserve the reference's explicit empty-selection convention. + answer = (0, 0) + else: + basis = echelon((row for i, row in enumerate(vectors) + if mask >> i & 1), width) + rank = len(basis) + if rank == width: + closed = full + else: + closed = mask + for i, row in enumerate(vectors): + if not (mask >> i & 1) and contains(row, basis, width): + closed |= 1 << i + answer = (closed, rank) + cache[mask] = answer + return cache[mask] + + return close diff --git a/research/bit-frame-closure-basis/run.py b/research/bit-frame-closure-basis/run.py new file mode 100644 index 0000000000..dd69ab9dcf --- /dev/null +++ b/research/bit-frame-closure-basis/run.py @@ -0,0 +1,116 @@ +"""Opt-in execution of the frozen PR886 checker; no source files are edited.""" +import argparse +import ast +from contextlib import redirect_stdout +import hashlib +import io +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from closure import make_close, require + +CHECKER = "research/bit589-frame-optimum/frameopt.py" +TUNED = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +BASE_WORD = "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz" +INPUTS = { + CHECKER, TUNED, BASE_WORD, + "research/bit589-frame-optimum/verify.sh", + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", +} +CASES = { + "pr589": (TUNED, "1733427039589844234749/1000000000000000000000000", False), + "pr555": (BASE_WORD, "1733052823330162099157/1000000000000000000000000", False), + "degraded": (TUNED, "1733427039589844234749/1000000000000000000000000", True), +} + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def sha(raw): + return hashlib.sha256(raw).hexdigest() + + +def check_sources(root=ROOT, pins=None): + if pins is None: + pins = json.loads((HERE / "SOURCES.json").read_text()) + records = [row for row in pins["files"] if row["usage"] == "input"] + require(len(records) == len(INPUTS) and + {row["path"] for row in records} == INPUTS, "exact input inventory") + for row in records: + path = root / row["path"] + require(path.is_file(), "missing input: " + row["path"]) + require(sha(path.read_bytes()) == row["sha256"], + "source digest: " + row["path"]) + + +def program(source, filename, engine): + tree = ast.parse(source, filename=filename) + if engine == "basis": + matches = [i for i, node in enumerate(tree.body) + if isinstance(node, ast.FunctionDef) and node.name == "close"] + require(len(matches) == 1, "unique close function") + i = matches[0] + replacement = ast.parse("close = _make_close(L, V, _close)").body[0] + tree.body[i] = ast.copy_location(replacement, tree.body[i]) + else: + require(engine == "reference", "engine") + # Explicit optimize=0 retains every inherited assertion, regardless of + # parent process state. The CLI additionally rejects optimized invocation. + return compile(ast.fix_missing_locations(tree), filename, "exec", optimize=0) + + +def execute(case, engine): + require(not sys.flags.optimize, "inherited checker requires assertions") + check_sources() + path, endpoint, degraded = CASES[case] + filename = ROOT / CHECKER + code = program(filename.read_text(), str(filename), engine) + namespace = {"__file__": str(filename), "__name__": "__main__", + "_make_close": make_close} + output = io.StringIO() + previous = sys.argv + try: + sys.argv = [str(filename), str(ROOT / path), endpoint] + if degraded: + sys.argv.append("--degrade") + with redirect_stdout(output): + exec(code, namespace) + finally: + sys.argv = previous + text = output.getvalue() + receipt = json.loads(text) + closures = [[str(mask), str(closed), rank] + for mask, (closed, rank) in sorted(namespace["_close"].items())] + report = { + "case": case, "receipt": receipt, "stdout_sha256": sha(text.encode()), + "closure_count": len(closures), + "closure_sha256": sha(canonical(closures).encode()), + } + return report, closures + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--engine", choices=("reference", "basis"), default="basis") + parser.add_argument("--case", choices=tuple(CASES), default="pr589") + parser.add_argument("--closure-output", type=Path) + args = parser.parse_args() + if args.closure_output: + destination = args.closure_output.resolve() + require(not destination.exists() and not destination.is_relative_to(ROOT), + "use a fresh external closure output") + report, closures = execute(args.case, args.engine) + if args.closure_output: + with destination.open("x") as stream: + stream.write(canonical(closures) + "\n") + print(canonical(report)) + + +if __name__ == "__main__": + main() diff --git a/research/bit-frame-closure-basis/test_closure.py b/research/bit-frame-closure-basis/test_closure.py new file mode 100644 index 0000000000..8231bb2eba --- /dev/null +++ b/research/bit-frame-closure-basis/test_closure.py @@ -0,0 +1,182 @@ +"""Independent rational oracles and failure controls for the opt-in kernel.""" +import copy +from fractions import Fraction +import gzip +import itertools +import json +from pathlib import Path +import random +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import closure +import run + + +def rational_rank(rows): + """Fraction Gauss-Jordan rank; no modular arithmetic or kernel imports.""" + if not rows: + return 0 + matrix = [list(map(Fraction, row)) for row in rows] + rank = 0 + for j in range(len(matrix[0])): + candidates = [i for i in range(rank, len(matrix)) if matrix[i][j]] + if not candidates: + continue + i = candidates[0] + matrix[rank], matrix[i] = matrix[i], matrix[rank] + divisor = matrix[rank][j] + matrix[rank] = [x / divisor for x in matrix[rank]] + for i in range(len(matrix)): + if i != rank: + factor = matrix[i][j] + matrix[i] = [x - factor*y for x, y in zip(matrix[i], matrix[rank])] + rank += 1 + return rank + + +def oracle(lines, mask): + if mask == 0: + return (0, 0) + selected = [row for i, row in enumerate(lines) if mask >> i & 1] + rank = rational_rank(selected) + closed = sum(1 << i for i, row in enumerate(lines) + if rational_rank(selected + [row]) == rank) + return closed, rank + + +class ClosureTests(unittest.TestCase): + def test_all_512_small_masks_against_rational_rank(self): + lines = [(0, 0, 0), (2, 0, 0), (-1, 0, 0), (0, -3, 0), + (1, 1, 0), (0, 0, 2), (1, 0, 1), (0, 1, -1), (2, -2, 2)] + cache = {} + close = closure.make_close(lines, len(lines), cache) + for mask in range(1 << len(lines)): + self.assertEqual(close(mask), oracle(lines, mask), mask) + self.assertEqual(len(cache), 512) + + def test_pivot_order_and_nonunit_coefficients(self): + lines = [(0, 0, -2), (0, 3, 1), (-2, 1, 1), (2, -1, -1)] + for ordering in itertools.permutations(lines): + close = closure.make_close(ordering, len(ordering), {}) + for mask in range(16): + self.assertEqual(close(mask), oracle(ordering, mask)) + + def test_seed93_live_root_masks_against_rational_rank(self): + word = json.loads(gzip.decompress((run.ROOT / run.TUNED).read_bytes())) + lines = word["lines"] + rng = random.Random(93) + close = closure.make_close(lines, len(lines), {}) + masks = [1 << i for i in range(len(lines))] + masks += [sum(1 << i for i in rng.sample(range(len(lines)), j % 11)) + for j in range(93)] + for mask in masks: + self.assertEqual(close(mask), oracle(lines, mask), mask) + + def test_bad_domains_and_modular_alias_guard(self): + bad = [([], 0, {}, "line count"), ([[1], [1, 2]], 2, {}, "rectangular"), + ([[1.0]], 1, {}, "integer"), ([[1]], 2, {}, "line count"), + ([[1]], 1, {0: (0, 0)}, "fresh"), + ([[closure.PRIME, 0], [0, 1]], 2, {}, "Hadamard")] + for lines, count, cache, error in bad: + with self.assertRaisesRegex(ValueError, error): + closure.make_close(lines, count, cache) + close = closure.make_close([[1, 0], [0, 1]], 2, {}) + for mask in (-1, 4, 1.5): + with self.assertRaisesRegex(ValueError, "line mask"): + close(mask) + self.assertEqual(rational_rank([[closure.PRIME, 0]]), 1) + self.assertEqual(len(closure.echelon([[closure.PRIME, 0]], 2)), 0) + + def test_wrong_membership_and_lost_pivot_are_detected(self): + lines = [(2, 0), (1, 0), (0, 1)] + def compare(mask): + actual = closure.make_close(lines, 3, {})(mask) + closure.require(actual == oracle(lines, mask), "mathematical mismatch") + for answer in (True, False): + with patch.object(closure, "contains", return_value=answer): + with self.assertRaisesRegex(ValueError, "mathematical mismatch"): + compare(1) + original = closure.echelon + with patch.object(closure, "echelon", side_effect=lambda rows, width: original(rows, width)[:-1]): + with self.assertRaisesRegex(ValueError, "mathematical mismatch"): + compare(5) + + def test_cache_is_word_local_and_coordinates_are_copied(self): + lines = [[1, 0], [0, 1], [1, 0]] + first = closure.make_close(lines, 3, {}) + lines[2][:] = [0, 1] + second = closure.make_close(lines, 3, {}) + self.assertEqual(first(1), (5, 1)) + self.assertEqual(second(1), (1, 1)) + + def test_all_input_pins_and_inventory_fail_closed(self): + pins = json.loads((HERE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory(prefix="closure-pins-") as temp: + root = Path(temp) + for path in run.INPUTS: + destination = root / path + destination.parent.mkdir(parents=True, exist_ok=True) + destination.write_bytes((run.ROOT / path).read_bytes()) + run.check_sources(root, pins) + for path in sorted(run.INPUTS): + destination = root / path + saved = destination.read_bytes() + destination.write_bytes(saved + b"corruption") + with self.assertRaisesRegex(ValueError, "source digest"): + run.check_sources(root, pins) + destination.write_bytes(saved) + destination.unlink() + with self.assertRaisesRegex(ValueError, "missing input"): + run.check_sources(root, pins) + for mutation in ("missing", "duplicate"): + bad = copy.deepcopy(pins) + row = next(r for r in bad["files"] if r["usage"] == "input") + if mutation == "missing": + bad["files"].remove(row) + else: + bad["files"].append(row) + with self.assertRaisesRegex(ValueError, "exact input inventory"): + run.check_sources(pins=bad) + + def test_adapter_anchor_and_inherited_assertions(self): + source = (run.ROOT / run.CHECKER).read_text() + for changed in (source.replace("def close(m):", "def renamed(m):"), + source + "\ndef close(m): return (m, 0)\n"): + with self.assertRaisesRegex(ValueError, "unique close function"): + run.program(changed, "test.py", "basis") + small = "L=[[1]]\nV=1\n_close={}\ndef close(m): return (m, m)\nassert False, 'retained assertion'\n" + for engine in ("reference", "basis"): + with self.assertRaisesRegex(AssertionError, "retained assertion"): + exec(run.program(small, "test.py", engine), {"_make_close": closure.make_close}) + p = subprocess.run([sys.executable, "-I", "-O", "-B", str(HERE / "run.py")], + capture_output=True, text=True) + self.assertNotEqual(p.returncode, 0) + self.assertIn("inherited checker requires assertions", p.stderr) + + def test_benchmark_code_and_coverage_bindings(self): + import verify + expected = json.loads((HERE / "EXPECTED.json").read_text()) + evidence = json.loads((HERE / "BENCHMARK.json").read_text()) + verify.check_benchmark(expected, evidence) + for label in ("source", "receipt", "coverage", "median"): + bad = copy.deepcopy(evidence) + if label == "source": + bad["implementation_sha256"]["closure.py"] = "0" * 64 + elif label == "receipt": + bad["samples"][0]["engines"]["basis"]["cases"]["pr589"]["report_sha256"] = "0" * 64 + elif label == "coverage": + del bad["samples"][0]["engines"]["basis"]["cases"]["degraded"] + else: + bad["median_suite_seconds"]["basis"] *= 2 + with self.assertRaisesRegex(ValueError, "benchmark"): + verify.check_benchmark(expected, bad) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/bit-frame-closure-basis/verify.py b/research/bit-frame-closure-basis/verify.py new file mode 100644 index 0000000000..43ab150968 --- /dev/null +++ b/research/bit-frame-closure-basis/verify.py @@ -0,0 +1,70 @@ +"""Replay both engines, compare every closure, and run independent controls.""" +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import statistics + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import run + + +def check_benchmark(expected, evidence=None): + if evidence is None: + evidence = json.loads((HERE / "BENCHMARK.json").read_text()) + names = {"closure.py", "run.py", "benchmark.py", "EXPECTED.json", "SOURCES.json"} + run.require(set(evidence["implementation_sha256"]) == names, "benchmark input inventory") + for name, digest in evidence["implementation_sha256"].items(): + run.require(run.sha((HERE / name).read_bytes()) == digest, "benchmark source binding: " + name) + samples = evidence["samples"] + run.require(bool(samples), "benchmark samples") + for index, sample in enumerate(samples): + order = ["reference", "basis"] if index % 2 == 0 else ["basis", "reference"] + run.require(sample["pair"] == index and sample["order"] == order, "alternating benchmark pairs") + for engine in order: + cases = sample["engines"][engine]["cases"] + run.require(set(cases) == set(expected), "benchmark case coverage") + for case in cases: + digest = run.sha(run.canonical(expected[case]).encode()) + run.require(cases[case]["report_sha256"] == digest, "benchmark complete receipt: " + case) + medians = {engine: statistics.median(s["engines"][engine]["seconds"] for s in samples) + for engine in ("reference", "basis")} + run.require(medians == evidence["median_suite_seconds"], "benchmark median arithmetic") + run.require(evidence["suite_ratio"] == medians["reference"] / medians["basis"], + "benchmark ratio arithmetic") + # There is deliberately no speed threshold: timings are descriptive. + + +def main(): + run.check_sources() + expected = json.loads((HERE / "EXPECTED.json").read_text()) + check_benchmark(expected) + comparisons = [] + with tempfile.TemporaryDirectory(prefix="bit-frame-closure-") as temp: + for case in run.CASES: + reports, inventories = {}, {} + for engine in ("reference", "basis"): + destination = Path(temp) / (case + "-" + engine + ".json") + command = [sys.executable, "-I", "-B", str(HERE / "run.py"), + "--case", case, "--engine", engine, + "--closure-output", str(destination)] + process = subprocess.run(command, capture_output=True, text=True, timeout=150) + run.require(process.returncode == 0, engine + " " + case + ": " + process.stderr) + reports[engine] = json.loads(process.stdout) + inventories[engine] = json.loads(destination.read_text()) + run.require(reports[engine] == expected[case], "complete receipt: " + engine + " " + case) + run.require(inventories["reference"] == inventories["basis"], + "every closure mask and rank: " + case) + comparisons.append({"case": case, "closures": len(inventories["basis"]), + "assignments": reports["basis"]["receipt"]["assignments_enumerated"]}) + process = subprocess.run([sys.executable, "-I", "-B", str(HERE / "test_closure.py")], + timeout=150) + run.require(process.returncode == 0, "rational oracle and negative controls") + print(run.canonical({"status": "PASS_BIT_FRAME_CLOSURE_BASIS", "cases": comparisons, + "no_new_kappa": True})) + + +if __name__ == "__main__": + main()