diff --git a/.github/workflows/r420-target-basis.yml b/.github/workflows/r420-target-basis.yml new file mode 100644 index 0000000000..fa105efb5c --- /dev/null +++ b/.github/workflows/r420-target-basis.yml @@ -0,0 +1,42 @@ +name: r420-target-basis + +on: + push: + paths: + - 'research/r420-target-basis/**' + - '.github/workflows/r420-target-basis.yml' + pull_request: + paths: + - 'research/r420-target-basis/**' + - '.github/workflows/r420-target-basis.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-24.04 + timeout-minutes: 8 + strategy: + fail-fast: false + matrix: + python-version: ['3.11', '3.13'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: ${{ matrix.python-version }} + - run: python -B research/r420-target-basis/verify.py + - run: python -B -m unittest discover -s research/r420-target-basis -p 'test_*.py' + - name: Install Boost for unchanged C++ checkers + if: matrix.python-version == '3.13' + run: | + sudo apt-get update -qq + sudo apt-get install -y --no-install-recommends libboost-dev + - name: Fresh C++ legality and multistage columns + if: matrix.python-version == '3.13' + run: CXX=g++ python -B research/r420-target-basis/native.py + - run: git diff --exit-code diff --git a/research/r420-target-basis/CERTIFICATE.json b/research/r420-target-basis/CERTIFICATE.json new file mode 100644 index 0000000000..4d3d708e5d --- /dev/null +++ b/research/r420-target-basis/CERTIFICATE.json @@ -0,0 +1,68 @@ +{ + "D_ADDs": [ + 19922, + 16772 + ], + "after": { + "ADDs": 23766, + "forward_prefix": 144651, + "histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload_bits": 102, + "payload_prefix_upper": "2657306775507971405724759110400", + "rank_mass": 5112, + "record_sha256": "6ca2f063e4e160d613bb638edf6b0306de0f98a21c9d34d4c491f1e4af5b3dc7", + "records": 26724, + "reverse_prefix": 3703810 + }, + "assignment_seed": 5, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "before": { + "ADDs": 26916, + "forward_prefix": 144651, + "histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload_bits": 100, + "payload_prefix_upper": "998206739997057013039187410944", + "rank_mass": 5112, + "record_sha256": "f7e6cceaceb04d7bd70918981405dcead988a890cfca03b51e80d935f00a960f", + "records": 29874, + "reverse_prefix": 2270064 + }, + "candidate_word_canonical_sha256": "091a62fa54f0aeb3a46c7e3ebefbbbc2e0b00b85be9d90521b9077456e650e09", + "columns_in_each_direction": 660, + "labels": { + "frames": 672, + "gram_det": 1, + "labels": 120, + "lattice_rank": 8 + }, + "legacy_H2_and_literal_K_accept": false, + "oriented_pairs_scored": 14280, + "pair_count": 57, + "positive_control": "F2-neutral target pair preserves operator and costs two ADDs", + "rejection_controls": [ + "missing final target restoration", + "missing initial target shear", + "wrong transformed helper row", + "nonzero D frame", + "source accessed at frame zero", + "unrelated cleanup modification", + "omitted exported ERASE", + "omitted exported target shear" + ], + "saved_ADDs": 3150, + "scope": "finite native bit circuit; no new kappa", + "source_pr543": "2065fe4f72a914d907f1046603f5a36f17018535", + "status": "PASS_R420_TARGET_BASIS" +} diff --git a/research/r420-target-basis/CLAIM.json b/research/r420-target-basis/CLAIM.json new file mode 100644 index 0000000000..8b340aeaa6 --- /dev/null +++ b/research/r420-target-basis/CLAIM.json @@ -0,0 +1,51 @@ +{ + "track": "Bit supplier", + "assignment_seed": 5, + "randomness": "secrets.randbelow(100), OS randomness, 2026-10-13 04:23:56 UTC", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "object": "PR543 R420 frame-zero D correction: conjugation by disjoint target transvections, with arbitrary target inputs restored", + "method": "score all 14280 oriented pairs of 120 targets; greedy disjoint positive-gain matching with Random(5) tie breaking; no helper basis changes", + "candidates": [ + { + "task": "phase-B block 5 resynthesis", + "disposition": "already completed by PR674 and composed by PR688" + }, + { + "task": "phase-A quad 5 resynthesis", + "disposition": "possible but near concurrent PR691 quad13 mechanism" + }, + { + "task": "frame-zero target-basis conjugation", + "disposition": "chosen: changes target rows, unlike helper-column factoring in PR686/694" + } + ], + "overlap_checked_through_pr": 709, + "coordination": "No pinned issue exists; local claim", + "expected_deliverable": "finite exact circuit, complete native dirty-input/frame replay, charged restoration/prefix costs, rejection controls; no kappa claim", + "expected_finish_utc": "2026-10-13 04:49:00 UTC", + "status": "completed", + "optimistic_complete_cost": { + "baseline_D_ADDs": 19922, + "transformed_row_reads": 16658, + "preparation_ADDs": 57, + "restoration_ADDs": 57, + "total_D_ADDs": 16772, + "new_helpers": 0, + "new_COPYs": 0, + "new_frame_moves": 0, + "recursive_profile": "unchanged", + "no_kappa_reason": "selected composition is complex-limited; local scalar count changes finite overhead only" + }, + "result": { + "saved_native_ADDs": 3150, + "target_pairs": 57, + "new_local_payload_bits": 102, + "native_stage_counts": [ + 5, + 9, + 11 + ], + "kappa": "unchanged", + "url": "https://github.com/swbiggart/integer-mult-bounds/tree/research/seed5-target-basis/research/r420-target-basis" + } +} diff --git a/research/r420-target-basis/NATIVE-CERTIFICATE.json b/research/r420-target-basis/NATIVE-CERTIFICATE.json new file mode 100644 index 0000000000..e095460239 --- /dev/null +++ b/research/r420-target-basis/NATIVE-CERTIFICATE.json @@ -0,0 +1,52 @@ +{ + "source_pins": "cecb7cb56f36434b5ddca4be7aa2eef4b39841337b874effb90f1355348d5b09", + "status": "PASS_R420_TARGET_BASIS_NATIVE", + "words": { + "after": { + "legality": "PASS", + "stages": [ + { + "bridge_controls": 6, + "formal_columns": 900, + "missing_D_end_rejected": true, + "stages": 5 + }, + { + "bridge_controls": 18, + "formal_columns": 1380, + "missing_D_end_rejected": true, + "stages": 9 + }, + { + "bridge_controls": 24, + "formal_columns": 1620, + "missing_D_end_rejected": true, + "stages": 11 + } + ] + }, + "before": { + "legality": "PASS", + "stages": [ + { + "bridge_controls": 6, + "formal_columns": 900, + "missing_D_end_rejected": true, + "stages": 5 + }, + { + "bridge_controls": 18, + "formal_columns": 1380, + "missing_D_end_rejected": true, + "stages": 9 + }, + { + "bridge_controls": 24, + "formal_columns": 1620, + "missing_D_end_rejected": true, + "stages": 11 + } + ] + } + } +} diff --git a/research/r420-target-basis/README.md b/research/r420-target-basis/README.md new file mode 100644 index 0000000000..3fb52afa32 --- /dev/null +++ b/research/r420-target-basis/README.md @@ -0,0 +1,183 @@ +# R420 dirt correction through a restored target basis + +**Finite bit-circuit construction; no new κ.** On eumemic's accepted PR543 +R420 word, 57 disjoint target transvections reduce the frame-zero dirt +correction from **19,922 to 16,772 binary XORs**. Including preparation and +restoration, the complete native word falls from **26,916 to 23,766 ADDs** +(3,150 saved). No extra helper, copy, source access or frame movement is used. + +| Quantity | Original | Target basis | +|---|---:|---:| +| D helper reads | 19,922 | 16,658 | +| D target preparation / restoration | 0 / 0 | 57 / 57 | +| Complete native ADDs | 26,916 | 23,766 | +| Exported records | 29,874 | 26,724 | +| Forward positive prefix | 144,651 | 144,651 | +| Reverse positive prefix | 2,270,064 | 3,703,810 | +| Local payload allowance, bits | 100 | 102 | +| Helpers / retained copies / rank mass | 420 / 9 / 5,112 | 420 / 9 / 5,112 | + +The larger reverse prefix is charged, not inherited from the old circuit. +The new exact payload bound is +`64 * 144651^3 * 3703810^2 = 2657306775507971405724759110400 < 2^104`. +This is the local cohort allowance. A new hosted-parent finite invoice is +**not** supplied, and the old global precision charges are not asserted for +the changed word. + +## Reproduce + +From the repository root, with Python 3.9 or later and its standard library: + +```sh +python3 -B research/r420-target-basis/verify.py +python3 -B -m unittest discover -s research/r420-target-basis -p 'test_*.py' +``` + +The verifier's final line is: + +```text +PASS_R420_TARGET_BASIS D=19922->16772 native_ADDs=26916->23766 saved=3150 columns=660 rank_mass=5112 kappa=unchanged +``` + +It reproduces the matching, reconstructs the actual changed word, compares +every certificate field, runs the retained E8/frame checker, interprets all +660 symbolic inputs in both directions using a separate set representation, +and compares every record with the unmodified official exporter. Eight +negative controls and an F2-neutral but paid positive control are included. +Optimized Python is refused because the inherited exporter uses assertions. +No output files are overwritten; explicit certificate generation uses +`--write-certificate NEW_PATH` and exclusive file creation. + +For the fresh C++17 legality and five-, nine- and eleven-stage replays: + +```sh +python3 -B research/r420-target-basis/native.py +``` + +Install Boost headers or set `BOOST_INCLUDE` to their containing directory; +set `CXX` if the compiler is not `c++`. Expected final line: + +```text +PASS_R420_TARGET_BASIS_NATIVE words=2 stages=5,9,11 columns=900,1380,1620 bridge_controls=96 missing_D_controls=6 +``` + +Both original and changed words pass the unchanged C++ checkers. Each word +checks 900/1,380/1,620 physical formal columns and 6/18/24 omitted bridges. +A missing final D ADD is also rejected at every stage count; for the new +word that ADD is a mandatory target restoration. These are finite replays, +not a formal proof of the full multiplication theorem. + +## Construction and sufficient interface + +Work over F2. Let `K` be the original 120-by-420 helper-incidence matrix of +D, so D maps `(x,s,y)` to `(x,s,y+Ks)`. For distinct targets `a,b`, let +`P_ab` add coordinate `a` to coordinate `b`. It is an involution. For a +matching of disjoint ordered pairs, the transvections commute and their +product `P` is also an involution. + +The new D performs three operations: + +1. Add `y_a` into `y_b` once for each selected pair, producing `Py`. +2. Read the helper rows of `PK`. Row `a` stays `K_a`; row `b` becomes + `K_a XOR K_b`; every other row stays unchanged. +3. Undo the target transvections in reverse order. + +The result is `P(Py+PKs)=y+Ks`. This equality holds for **arbitrary target +inputs** as well as arbitrary helper dirt. Helpers and sources are never +written by D. Every touched register is a target or helper at frame zero, +so the extra ADDs are common-frame operations. Targets remain at frame zero +until the original scatter; all later instructions are unchanged. + +The original literal H2 permits only helper-to-target reads in D. It rejects +this syntax, and its literal extraction of K also fails. We do not change +or disable either predicate. The sufficient replacement is: + +> D is a legal frame-zero prefix whose complete operator is +> `(x,s,y) -> (x,s,y+Ks)`, with every helper unchanged before A. + +The proof above establishes this replacement. The verifier separately checks +that operator on all 660 inputs, compares every field outside D with the +pinned source, and checks that the original H1/H3/H4/H5 and remaining +decomposed conclusions still hold. Substituting an equal prefix into the +unchanged `(A, scatter, B, C)` program preserves its F2 endpoint. The +original mutable-basis/common-label realization remains a conditional +interface requiring maintainer review for this changed D syntax. + +This is an F2 endpoint statement. It does not assert equality of the two +forward integer matrices. Signed reverse execution uses inverse shears; +the cancellation-free integer bounds are recomputed in both directions. + +The complete MOVE/COPY/ERASE subsequence is identical to the original, giving +the unchanged paid histogram `{1:1320, 2:1440, 4:60, 5:120, 8:9}`. All copies, +their closing operations and the original recursive children are retained. +The selected assembly is complex-limited, and a reduced scalar count alone +does not change a recursive exponent. No new bit exponent or κ is claimed. + +## Search domain and controls + +OS randomness assigned seed **5** and the bit-supplier track. We compared +three narrow candidates: phase-B block 5 (already PR674/688), phase-A quad 5 +(close to PR691's quad-13 mechanism), and target-row conjugation (chosen). +No pinned sprint issue existed, so the scope is in `CLAIM.json`. + +The search scores **all 14,280 ordered pairs** of 120 target rows. The exact +fully charged gain for `(a,b)` is +`weight(K_b) - weight(K_a XOR K_b) - 2`. A separate column-incidence census +checks every score. `random.Random(5)` supplies tie keys in lexicographic +pair order; decreasing `(gain,tie,a,b)` order and one greedy disjoint pass +select 57 positive pairs. Search stops after that pass. `RECIPE.json` records +every chosen pair and gain. No maximum-weight matching, optimal circuit, +or broader impossibility result is claimed. + +Controls reject missing initial/final shears, a wrong helper row, nonzero +prefix frames, source access at frame zero, unrelated cleanup changes, +an omitted exported ERASE and an omitted exported target shear. In +particular, omitting the initial shear **passes every zero-target input** +but leaks arbitrary target dirt; an explicit test demonstrates why the +full input basis is needed. A cancelled target pair is accepted semantically +and charged two ADDs. Tests also reject overlapping pairs and a recipe +that omits restoration cost. + +## Pins, related work and remaining obligations + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +PR543 source: `2065fe4f72a914d907f1046603f5a36f17018535`. +Selected PR626 source: `660de893d27bb7abd1d5b01b1640207528a5c851`, +conditional κ `51110230636731/31250000000000000`. +`SOURCES.json` pins every consumed predecessor implementation, original +notice and selected-record input. The compressed word is pinned by its +decompressed bytes. `CERTIFICATE.json` pins the canonical new word and both +native instruction streams; `NATIVE-CERTIFICATE.json` records C++ coverage. + +Concurrent [PR686](https://github.com/CrocSwap/integer-mult-bounds/pull/686) +by Mikhail R. Gadelha and +[PR694](https://github.com/CrocSwap/integer-mult-bounds/pull/694) by Greer +Guthrie factor **helper columns** and establish the semantic D-prefix +approach. They are credited predecessors to this investigation, not new +priority claims. PR694 head `9732ac127dd4bef98a846aaa904c20b5a84e72c1` +was inspected. This package factors **target rows**, restores arbitrary +target dirt, and imports neither their circuits nor their code. Its native +harness follows the validation pattern demonstrated in PR694. No composition +with those changes is certified here. PR670/674/688 concern phase-B blocks; +PR691 concerns a phase-A quad. Concurrent PR708 (Sagar Thakrar, head +`2ec522a466ec448f148d4355dc43b51c0ef1e0b5`) shares operands of the +separate FULL-frame decoder totals; it is not composed here. The final +overlap refresh covered open PRs through #709. PR661's fixed-order frame bound explicitly +excludes circuit changes, so this does not reopen its closed search. + +Full hosted-parent reconstruction, whole-owner allocation, revised global +precision/finite invoices and a changed-word outer assembly remain separate +integration work. All-size compilation, common labels, mutable bases, +physical routing, residual hosting, precision/tape and analytic assumptions +remain. Neither `upstream/` nor the selected construction is changed. + +Prepared by **Scott Woolsey Biggart (@swbiggart)** with substantial +**OpenAI Codex assistance** in the construction, proof, checking and +packaging. No independent human review is claimed. Apache-2.0. Credit remains +with eumemic (PR543/493 and xcheck), Dylan Crow (format/exporter/cohort +checkers), DaysSky (bridged stages and hosting), Zhihao Chen (scalar +interface), DreamingOfClouds (totals, pricing and engines), Chafik Boukhalfa, +icekylinx, Rohan Arun and the cumulative supplier/realization lineage. See +the unchanged [R420 notice](../e8-bit-r420/NOTICE.md) and +[carrier-skeleton notice](../e8-bit-carrier-skeleton/NOTICE.md) for the +complete inherited attribution and AI disclosures. diff --git a/research/r420-target-basis/RECIPE.json b/research/r420-target-basis/RECIPE.json new file mode 100644 index 0000000000..31adc3b8bc --- /dev/null +++ b/research/r420-target-basis/RECIPE.json @@ -0,0 +1,291 @@ +{ + "seed": 5, + "oriented_pairs_scored": 14280, + "pairs": [ + [ + 219, + 222, + 95 + ], + [ + 233, + 239, + 94 + ], + [ + 236, + 234, + 94 + ], + [ + 143, + 137, + 91 + ], + [ + 145, + 148, + 85 + ], + [ + 134, + 128, + 84 + ], + [ + 156, + 200, + 79 + ], + [ + 230, + 224, + 79 + ], + [ + 173, + 174, + 76 + ], + [ + 194, + 193, + 75 + ], + [ + 133, + 131, + 74 + ], + [ + 139, + 141, + 71 + ], + [ + 208, + 214, + 69 + ], + [ + 198, + 181, + 68 + ], + [ + 154, + 205, + 67 + ], + [ + 199, + 197, + 66 + ], + [ + 182, + 176, + 65 + ], + [ + 185, + 191, + 64 + ], + [ + 187, + 189, + 63 + ], + [ + 216, + 221, + 61 + ], + [ + 170, + 178, + 61 + ], + [ + 138, + 140, + 60 + ], + [ + 211, + 209, + 60 + ], + [ + 144, + 149, + 57 + ], + [ + 238, + 232, + 57 + ], + [ + 235, + 237, + 56 + ], + [ + 151, + 146, + 56 + ], + [ + 175, + 155, + 54 + ], + [ + 123, + 125, + 54 + ], + [ + 223, + 218, + 54 + ], + [ + 171, + 184, + 53 + ], + [ + 225, + 231, + 52 + ], + [ + 136, + 142, + 52 + ], + [ + 126, + 202, + 50 + ], + [ + 177, + 183, + 50 + ], + [ + 227, + 229, + 50 + ], + [ + 160, + 196, + 49 + ], + [ + 129, + 135, + 48 + ], + [ + 212, + 210, + 47 + ], + [ + 192, + 195, + 46 + ], + [ + 124, + 122, + 45 + ], + [ + 213, + 179, + 44 + ], + [ + 217, + 220, + 44 + ], + [ + 152, + 158, + 44 + ], + [ + 161, + 165, + 43 + ], + [ + 163, + 166, + 42 + ], + [ + 127, + 121, + 37 + ], + [ + 157, + 168, + 35 + ], + [ + 228, + 226, + 34 + ], + [ + 159, + 167, + 30 + ], + [ + 188, + 169, + 29 + ], + [ + 203, + 206, + 29 + ], + [ + 162, + 215, + 26 + ], + [ + 153, + 186, + 25 + ], + [ + 190, + 150, + 25 + ], + [ + 172, + 132, + 16 + ], + [ + 147, + 180, + 16 + ] + ] +} diff --git a/research/r420-target-basis/SOURCES.json b/research/r420-target-basis/SOURCES.json new file mode 100644 index 0000000000..afbc0632fa --- /dev/null +++ b/research/r420-target-basis/SOURCES.json @@ -0,0 +1,58 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "source_pr543": "2065fe4f72a914d907f1046603f5a36f17018535", + "files": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": { + "representation": "gzip-payload", + "sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2" + }, + "research/e8-bit-r420/code/xcheck.py": { + "representation": "bytes", + "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" + }, + "research/e8-bit-r420/README.md": { + "representation": "bytes", + "sha256": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f" + }, + "research/e8-bit-r420/NOTICE.md": { + "representation": "bytes", + "sha256": "12ba6e0845f222e9940b00f6c60d261db104246a8d3143da267682973479f811" + }, + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": { + "representation": "bytes", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp": { + "representation": "bytes", + "sha256": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce" + }, + "research/e8-bit-carrier-skeleton/NOTICE.md": { + "representation": "bytes", + "sha256": "5f4b7fcbf99f572be28b6da612ce775363908cdfc7810f7aca167be01c86e49a" + }, + "certificates/selected-result.json": { + "representation": "bytes", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": { + "representation": "bytes", + "sha256": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": { + "representation": "bytes", + "sha256": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": { + "representation": "bytes", + "sha256": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63" + }, + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": { + "representation": "bytes", + "sha256": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a" + }, + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": { + "representation": "bytes", + "sha256": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99" + } + } +} diff --git a/research/r420-target-basis/VALIDATION.json b/research/r420-target-basis/VALIDATION.json new file mode 100644 index 0000000000..c052cd9cae --- /dev/null +++ b/research/r420-target-basis/VALIDATION.json @@ -0,0 +1,38 @@ +{ + "status": "PASS_SCOPED_LOCAL_VALIDATION", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "platform": "macOS-27.2-arm64-arm-64bit", + "python_versions": [ + "3.9.6", + "3.11.16", + "3.13.16" + ], + "standard_library_verifier": "all three versions passed with exact CERTIFICATE equality", + "obligation_tests": "4 tests passed on all three versions; all 14280 pair scores cross-checked", + "native": { + "status": "PASS", + "compiler": "Apple clang 21.0.0, arm64-apple-darwin27.2.0", + "python": "3.9.6", + "boost": "1.85.0", + "boost_archive_url": "https://archives.boost.io/release/1.85.0/source/boost_1_85_0.tar.bz2", + "boost_archive_sha256": "7009fe1faa1697476bdc7027703a2badb84e849b7b0baad5086b087b971f8617", + "certificate": "NATIVE-CERTIFICATE.json" + }, + "selected_record_check": "PASS", + "not_claimed": [ + "hosted-parent reconstruction and global invoice", + "changed-word outer assembly", + "repository-wide make verify pass", + "full Lean proof", + "remote CI result at time of local commit" + ], + "repository_suite_context": "Earlier in this session, make verify was attempted on the preceding base and stopped at missing Boost headers after earlier groups passed. It was not repeated for this isolated research addition. Fresh unchanged native checks for both affected local words now pass with pinned Boost headers.", + "overlap_refresh_through": 709, + "relocated_minimal_checkout": "PASS using only package and declared source pins, launched outside repo", + "gzip_recompression": "PASS after changing gzip timestamp", + "extra_rejections": [ + "underpriced certificate", + "modified pinned source", + "optimized Python" + ] +} diff --git a/research/r420-target-basis/native.py b/research/r420-target-basis/native.py new file mode 100644 index 0000000000..456852f72b --- /dev/null +++ b/research/r420-target-basis/native.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +"""Fresh unchanged PR543 C++ legality and 5/9/11-stage replays. + +Requires C++17 and Boost; set CXX and BOOST_INCLUDE if needed. +Scott Woolsey Biggart with substantial OpenAI Codex assistance; Apache-2.0. +""" +import argparse +import json +import os +from pathlib import Path +import struct +import subprocess +import tempfile + +import verify as v + + +def run(command): + result = subprocess.run([str(x) for x in command], capture_output=True, text=True) + v.need(result.returncode == 0, 'command failed: ' + ' '.join(map(str, command)) + '\n' + result.stderr) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', type=Path) + args = parser.parse_args() + v.need(not v.sys.flags.optimize, 'run without -O') + local = v.certificate() + v.need(local == json.loads((v.HERE / 'CERTIFICATE.json').read_text()), 'local certificate differs') + original = v.read_sources() + changed = v.build(original, v.nominate(original)) + bit = v.ROOT / 'research/e8-bit-carrier-skeleton/code/bit' + cpp = bit / 'checkers' + include = ['-I' + str(cpp), '-I' + str(v.ROOT / 'research/e8-bit-carrier-skeleton/portable-include')] + if os.environ.get('BOOST_INCLUDE'): + include.append('-I' + os.environ['BOOST_INCLUDE']) + compiler = [os.environ.get('CXX', 'c++'), '-O2', '-std=c++17', '-DHDIM=8', '-DNCOPY=9'] + include + result = {'status': 'PASS_R420_TARGET_BASIS_NATIVE', 'source_pins': v.sha((v.HERE / 'SOURCES.json').read_bytes()), + 'words': {}} + with tempfile.TemporaryDirectory(prefix='r420-target-native-') as tmp: + work = Path(tmp) + legality = work / 'legality' + run(compiler + [cpp / 'legality_h.cpp', '-o', legality]) + binaries = {} + for pairs in (2, 4, 5): + binaries[pairs] = work / ('columns-' + str(pairs)) + run(compiler + ['-DVPORTS=120', '-DRHELP=420', '-DKPAIRS=' + str(pairs), + cpp / 'columns_k.cpp', '-o', binaries[pairs]]) + for name, word in [('before', original), ('after', changed)]: + folder = work / name; folder.mkdir() + word_path = folder / 'word.json'; word_path.write_bytes(v.canonical(word)) + export = folder / 'export' + run([v.sys.executable, '-I', '-B', v.ROOT / v.EXPORT, word_path, export]) + cin, cout = folder / 'cin', folder / 'cout' + run([v.sys.executable, '-I', '-B', bit / 'regression/stage_cohort.py', export, export, cin, cout]) + output = folder / 'legality.json' + run([legality, cin, cout, output]) + admitted = json.loads(output.read_text()) + v.need(admitted['common_frame_ADDs'] == local[name]['ADDs'] and admitted['rank_mass'] == 5112 and + admitted['copies'] == admitted['erasures'] == 9 and admitted['all_final_frames_pass'], + 'C++ legality invoice') + raw = cout / 'COHORT249-RECORDS.bin' + v.need(v.sha(raw.read_bytes()) == local[name]['record_sha256'], 'staged stream changed') + evidence = {'legality': 'PASS', 'stages': []} + stream = list(struct.iter_unpack('<6i', raw.read_bytes())) + # Delete a final D ADD. On the changed word this is target restoration. + index = max(i for i, r in enumerate(stream) if r[0] == 1 and r[5] == 1) + mutant = folder / 'missing-D-end.bin' + mutant.write_bytes(b''.join(struct.pack('<6i', *r) for i, r in enumerate(stream) if i != index)) + for pairs, binary in binaries.items(): + output = folder / ('columns-' + str(pairs) + '.json') + run([binary, raw, output]) + checked = json.loads(output.read_text()) + v.need(checked['formal_columns_checked'] == 240 * pairs + 420 and + checked['local_scalar_additions'] == local[name]['ADDs'] and + checked['payload_prefix_upper'] == local[name]['payload_prefix_upper'] and + checked['payload_prefix_bits'] == local[name]['payload_bits'] and + dict(checked['local_raw_H']) == {int(k): n for k, n in local[name]['histogram'].items()}, + 'C++ columns/prefix/profile mismatch') + controls = checked['negative_controls'] + v.need(len(controls) == 6 * (pairs - 1) and all(c['rejected'] for c in controls), 'bridge controls') + rejected = subprocess.run([str(binary), str(mutant), str(folder / 'invalid.json')], + capture_output=True, text=True) + v.need(rejected.returncode != 0 and 'local defining-decoder full formal column' in rejected.stderr, + 'C++ missing D end must fail on its endpoint') + evidence['stages'].append({'stages': 2 * pairs + 1, + 'formal_columns': checked['formal_columns_checked'], + 'bridge_controls': len(controls), 'missing_D_end_rejected': True}) + result['words'][name] = evidence + if args.write_certificate: + with args.write_certificate.open('x') as out: + out.write(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + v.need(result == json.loads((v.HERE / 'NATIVE-CERTIFICATE.json').read_text()), 'native certificate differs') + print('PASS_R420_TARGET_BASIS_NATIVE words=2 stages=5,9,11 columns=900,1380,1620 bridge_controls=96 missing_D_controls=6') + + +if __name__ == '__main__': + main() diff --git a/research/r420-target-basis/test_verify.py b/research/r420-target-basis/test_verify.py new file mode 100644 index 0000000000..fb7db5901e --- /dev/null +++ b/research/r420-target-basis/test_verify.py @@ -0,0 +1,48 @@ +"""Obligation tests beyond the frozen successful construction; Apache-2.0.""" +import copy +import unittest + +import verify as v + + +class TargetBasisTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.word = v.read_sources() + cls.recipe = v.nominate(cls.word) + + def test_all_pair_scores_by_column_census(self): + # Independently count removed and introduced helper incidences. + matrix = v.rows(self.word) + for a in range(120, 240): + for b in range(120, 240): + if a != b: + gain = sum((1 if h in matrix[b] else -1) + for h in range(240, 660) if h in matrix[a]) - 2 + self.assertEqual(gain, len(matrix[b]) - len(matrix[a] ^ matrix[b]) - 2) + + def test_overlapping_pairs_rejected(self): + recipe = copy.deepcopy(self.recipe) + recipe['pairs'].append(recipe['pairs'][0]) + with self.assertRaisesRegex(v.Reject, 'disjoint'): + v.build(self.word, recipe) + + def test_underpriced_restoration_rejected(self): + recipe = copy.deepcopy(self.recipe) + recipe['pairs'][0][2] += 2 + with self.assertRaisesRegex(v.Reject, 'charged gain'): + v.build(self.word, recipe) + + def test_target_dirt_is_essential(self): + changed = v.build(self.word, self.recipe) + changed['D'].pop(0) + correct, wrong = v.set_prefix(self.word), v.set_prefix(changed) + targets = set(range(120, 240)) + self.assertEqual([s - targets for s in correct], [s - targets for s in wrong]) + self.assertNotEqual(correct, wrong) + with self.assertRaisesRegex(v.Reject, 'arbitrary inputs'): + v.prefix_contract(self.word, changed) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/r420-target-basis/verify.py b/research/r420-target-basis/verify.py new file mode 100644 index 0000000000..f31d594739 --- /dev/null +++ b/research/r420-target-basis/verify.py @@ -0,0 +1,315 @@ +#!/usr/bin/env python3 +"""Exact finite target-row conjugation of PR543's D prefix; Apache-2.0. + +Scott Woolsey Biggart, with substantial OpenAI Codex assistance. +Uses eumemic's pinned xcheck for E8 geometry and original interface checks. +The target matching, synthesis and record/set interpreters below are new. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import random +import struct +import subprocess +import sys +import tempfile +from collections import Counter + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = 'research/e8-bit-r420/data/bitE8mut-r420.json.gz' +CHECK = 'research/e8-bit-r420/code/xcheck.py' +EXPORT = 'research/e8-bit-carrier-skeleton/code/bit/export_records.py' + + +class Reject(Exception): + pass + + +def need(condition, message): + if not condition: + raise Reject(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def read_sources(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for path, pin in pins['files'].items(): + data = (ROOT / path).read_bytes() + if pin['representation'] == 'gzip-payload': + data = gzip.decompress(data) + need(sha(data) == pin['sha256'], 'source pin: ' + path) + return json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + + +def rows(word): + result = {} + for frame, target, sources in word['D']: + need(frame == 0 and 120 <= target < 240 and target not in result, + 'original D must have one zero-frame row per target') + need(len(set(sources)) == len(sources) and all(240 <= s < 660 for s in sources), + 'original D helper operands') + result[target] = set(sources) + need(set(result) == set(range(120, 240)), 'complete original D rows') + return result + + +def nominate(word): + """Exactly 14,280 directed pairs, one seeded greedy matching, then stop.""" + matrix = rows(word) + rng = random.Random(5) + candidates = [] + for a in sorted(matrix): + for b in sorted(matrix): + if a != b: + gain = len(matrix[b]) - len(matrix[a] ^ matrix[b]) - 2 + candidates.append((gain, rng.random(), a, b)) + used, selected = set(), [] + for gain, _, a, b in sorted(candidates, reverse=True): + if gain > 0 and a not in used and b not in used: + selected.append([a, b, gain]) + used.update((a, b)) + return {'seed': 5, 'oriented_pairs_scored': len(candidates), 'pairs': selected} + + +def build(word, recipe): + matrix = rows(word) + used, shears = set(), [] + for a, b, gain in recipe['pairs']: + need(a in matrix and b in matrix and a != b and not ({a, b} & used), + 'target matching must be disjoint') + need(gain == len(matrix[b]) - len(matrix[a] ^ matrix[b]) - 2 and gain > 0, + 'incorrect fully charged gain') + matrix[b] ^= matrix[a] + used.update((a, b)) + shears.append([0, b, [a]]) + changed = copy.deepcopy(word) + changed['D'] = shears + [[0, t, sorted(matrix[t])] for t in sorted(matrix) if matrix[t]] + changed['D'] += copy.deepcopy(list(reversed(shears))) + return changed + + +def set_prefix(word): + """Set-valued symbolic interpreter, independent of bit-packed xcheck.""" + values = [{r} for r in range(660)] + for frame, target, sources in word['D']: + need(frame == 0 and 120 <= target < 240 and sources and + len(set(sources + [target])) == len(sources) + 1 and + all(120 <= s < 660 for s in sources), 'illegal D gate') + for source in sources: + values[target].symmetric_difference_update(values[source]) + return values + + +def prefix_contract(original, changed): + need({k: v for k, v in original.items() if k != 'D'} == + {k: v for k, v in changed.items() if k != 'D'}, 'field outside D changed') + need(set_prefix(original) == set_prefix(changed), 'D operator changed on arbitrary inputs') + + +def records(word, dimensions): + """Compile literal records separately from the retained official exporter.""" + state = list(word['start']) + out = [] + def move(reg, frame): + if state[reg] != frame: + out.append((0, reg, state[reg], frame, dimensions[frame] - dimensions[state[reg]], 0)) + state[reg] = frame + def gates(section, phase): + for frame, dst, srcs in word[section]: + for reg in [dst] + srcs: + move(reg, frame) + out.extend((1, dst, src, 1, frame, phase) for src in srcs) + gates('D', 1) + gates('A', 2) + for k, center in enumerate(word['ret']): + frame = state[center] + out.append((2, center, 660, frame, 0, dimensions[frame])) + out.extend((1, 120 + t, 660, 1, 0, 3) for t, row in enumerate(word['scatter']) if k in row) + out.append((3, center, 660, frame, 0, 0)) + gates('B', 4) + gates('C', 5) + for reg, frame in enumerate(word['final']): + move(reg, frame) + return out + + +def replay(stream, reverse=False): + """All 660 dirty-input columns using sets; integer positive prefix in parallel.""" + values = [{r} for r in range(660)] + [set()] + norms = [1] * 660 + [0] + largest = 1 + center = None + copies = 0 + for op, a, b, c, f, z in (reversed(stream) if reverse else stream): + if op == 0: + continue + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + need(c == 1 and 0 <= a < 660 and 0 <= b <= 660 and a != b and + a != center and (b != 660 or center is not None), 'invalid ADD/copy lifetime') + values[a].symmetric_difference_update(values[b]) + norms[a] += norms[b] + largest = max(largest, norms[a]) + elif op == 2: + need(center is None and b == 660 and 0 <= a < 660, 'COPY lifetime') + center = a + copies += 1 + values[660] = values[a].copy() + norms[660] = norms[a] + elif op == 3: + need(center == a and b == 660, 'ERASE lifetime') + center = None + values[660] = set() + norms[660] = 0 + else: + raise Reject('unknown record opcode') + need(center is None and copies == 9 and not values[660], 'copy closure') + expected = [{r, r - 120} if 120 <= r < 240 else {r} for r in range(660)] + need(values[:660] == expected, 'full dirty-input endpoint') + return largest + + +def bill(stream): + forward, backward = replay(stream), replay(stream, True) + payload = 64 * forward ** 3 * backward ** 2 + need(payload < 2 ** 104, '104-bit local prefix cap') + paid = Counter() + for op, a, b, c, f, z in stream: + if op == 0: + need(f > 0, 'nonpositive frame move') + paid[f] += 1 + elif op == 2: + paid[z] += 1 + return {'ADDs': sum(r[0] == 1 for r in stream), 'records': len(stream), + 'forward_prefix': forward, 'reverse_prefix': backward, + 'payload_prefix_upper': str(payload), 'payload_bits': payload.bit_length(), + 'histogram': {str(k): v for k, v in sorted(paid.items())}, + 'rank_mass': sum(k * v for k, v in paid.items()), + 'record_sha256': sha(b''.join(struct.pack('<6i', *r) for r in stream))} + + +def export_compare(word, expected, directory): + path = directory / 'word.json' + path.write_bytes(canonical(word)) + subprocess.run([sys.executable, '-I', '-B', str(ROOT / EXPORT), str(path), str(directory / 'export')], + check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + got = list(struct.iter_unpack('<6i', (directory / 'export/249-records.bin').read_bytes())) + need(got == expected, 'official exported records differ') + + +def controls(original, changed, stream): + names = [] + def rejects(name, action): + try: + action() + except Reject: + names.append(name) + else: + raise Reject('negative control accepted: ' + name) + x = copy.deepcopy(changed); x['D'].pop() + rejects('missing final target restoration', lambda: prefix_contract(original, x)) + x = copy.deepcopy(changed); x['D'].pop(0) + # This bug is invisible if tests initialize every target to zero. + projected = lambda w: [s - set(range(120, 240)) for s in set_prefix(w)] + need(projected(original) == projected(x), 'missing initial shear should evade zero-target tests') + rejects('missing initial target shear', lambda: prefix_contract(original, x)) + x = copy.deepcopy(changed); x['D'][57][2].pop() + rejects('wrong transformed helper row', lambda: prefix_contract(original, x)) + x = copy.deepcopy(changed); x['D'][0][0] = 1 + rejects('nonzero D frame', lambda: prefix_contract(original, x)) + x = copy.deepcopy(changed); x['D'][0][2] = [0] + rejects('source accessed at frame zero', lambda: prefix_contract(original, x)) + x = copy.deepcopy(changed); x['C'].pop() + rejects('unrelated cleanup modification', lambda: prefix_contract(original, x)) + damaged = list(stream); damaged.pop(next(i for i, r in enumerate(damaged) if r[0] == 3)) + rejects('omitted exported ERASE', lambda: replay(damaged)) + damaged = list(stream); damaged.pop(next(i for i, r in enumerate(damaged) if r[0] == 1)) + rejects('omitted exported target shear', lambda: replay(damaged)) + # F2-neutral overhead is accepted semantically and still pays two ADDs. + neutral = copy.deepcopy(changed) + neutral['D'] = [[0, 120, [121]], [0, 120, [121]]] + neutral['D'] + prefix_contract(original, neutral) + need(sum(len(g[2]) for g in neutral['D']) == sum(len(g[2]) for g in changed['D']) + 2, + 'neutral pair must pay both gates') + return names + + +def certificate(): + word = read_sources() + recipe = nominate(word) + need(recipe == json.loads((HERE / 'RECIPE.json').read_text()), 'frozen matching mismatch') + changed = build(word, recipe) + prefix_contract(word, changed) + spec = importlib.util.spec_from_file_location('r420_pinned_xcheck', ROOT / CHECK) + module = importlib.util.module_from_spec(spec); spec.loader.exec_module(module) + original = module.Word(word) + labels = original.labels() + original.full() + hypotheses, conclusions, _ = original.interface() + need(all(hypotheses.values()) and all(conclusions.values()), 'original interface') + candidate = module.Word(changed) + candidate.full() + h, c, _ = candidate.interface() + need([k for k, v in h.items() if not v] == ['H2_D_frame0_targets_from_helpers'], + 'only literal H2 should fail') + need([k for k, v in c.items() if not v] == ['K_equals_D'], 'literal K extractor should fail') + before, after = records(word, original.fdim), records(changed, original.fdim) + need([r for r in before if r[0] != 1] == [r for r in after if r[0] != 1], + 'MOVE/COPY/ERASE subsequence changed') + receipts = [] + with tempfile.TemporaryDirectory(prefix='r420-target-') as tmp: + for i, (w, stream) in enumerate(((word, before), (changed, after))): + directory = Path(tmp) / str(i); directory.mkdir() + export_compare(w, stream, directory) + receipts.append(bill(stream)) + need(receipts[0]['histogram'] == receipts[1]['histogram'] == + {'1': 1320, '2': 1440, '4': 60, '5': 120, '8': 9}, 'paid profile changed') + saved = sum(p[2] for p in recipe['pairs']) + need(receipts[0]['ADDs'] - receipts[1]['ADDs'] == saved, 'full charged saving') + d_counts = [sum(len(g[2]) for g in w['D']) for w in (word, changed)] + return {'status': 'PASS_R420_TARGET_BASIS', 'scope': 'finite native bit circuit; no new kappa', + 'base_commit': '66849e1475c930fd7732b1a0067ffee7e1e95f60', + 'source_pr543': '2065fe4f72a914d907f1046603f5a36f17018535', + 'assignment_seed': 5, 'pair_count': len(recipe['pairs']), + 'oriented_pairs_scored': recipe['oriented_pairs_scored'], + 'D_ADDs': d_counts, 'saved_ADDs': saved, 'columns_in_each_direction': 660, + 'labels': labels, 'before': receipts[0], 'after': receipts[1], + 'candidate_word_canonical_sha256': sha(canonical(changed)), + 'rejection_controls': controls(word, changed, after), + 'positive_control': 'F2-neutral target pair preserves operator and costs two ADDs', + 'legacy_H2_and_literal_K_accept': False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', type=Path) + args = parser.parse_args() + need(sys.flags.optimize == 0, 'run without -O: inherited exporter has assertions') + result = certificate() + if args.write_certificate: + with args.write_certificate.open('x') as out: + out.write(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + need(result == json.loads((HERE / 'CERTIFICATE.json').read_text()), 'certificate differs') + print('PASS_R420_TARGET_BASIS D=19922->16772 native_ADDs=26916->23766 saved=3150 columns=660 rank_mass=5112 kappa=unchanged') + + +if __name__ == '__main__': + try: + main() + except (Reject, ValueError, KeyError, OSError) as error: + print('REJECT:', error, file=sys.stderr) + sys.exit(1)