diff --git a/.github/workflows/r420-two-sided-basis.yml b/.github/workflows/r420-two-sided-basis.yml new file mode 100644 index 0000000000..9fe99e36b0 --- /dev/null +++ b/.github/workflows/r420-two-sided-basis.yml @@ -0,0 +1,42 @@ +name: r420-two-sided-basis + +on: + push: + paths: + - 'research/r420-two-sided-basis/**' + - '.github/workflows/r420-two-sided-basis.yml' + pull_request: + paths: + - 'research/r420-two-sided-basis/**' + - '.github/workflows/r420-two-sided-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-two-sided-basis/verify.py + - run: python -B -m unittest discover -s research/r420-two-sided-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-two-sided-basis/native.py + - run: git diff --exit-code diff --git a/research/r420-two-sided-basis/.gitattributes b/research/r420-two-sided-basis/.gitattributes new file mode 100644 index 0000000000..4c0124a118 --- /dev/null +++ b/research/r420-two-sided-basis/.gitattributes @@ -0,0 +1,2 @@ +# Preserve immutable predecessor source bytes. +vendor/* -text diff --git a/research/r420-two-sided-basis/CERTIFICATE.json b/research/r420-two-sided-basis/CERTIFICATE.json new file mode 100644 index 0000000000..fc702567f3 --- /dev/null +++ b/research/r420-two-sided-basis/CERTIFICATE.json @@ -0,0 +1,92 @@ +{ + "D_ADDs": [ + 19922, + 12988, + 11554 + ], + "after": { + "ADDs": 18548, + "forward_prefix": 202699, + "histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload_bits": 103, + "payload_prefix_upper": "9190258315617780048732559342336", + "rank_mass": 5112, + "record_sha256": "5fb3e9f78a4a9e855664e6367335d5fb0da9b5bb7ae043cef764499d45a99754", + "records": 21506, + "reverse_prefix": 4152374 + }, + "assignment_seed": 2, + "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 + }, + "changed_word_canonical_sha256": "6043bf9ac3dd840604c60d24a8d21c1d1aa9c36ba69fc4600e656366a0aa5fe7", + "columns_in_each_direction": 660, + "controls": [ + "missing helper preparation", + "missing target preparation", + "missing target restoration", + "missing helper restoration", + "wrong PKQ helper coefficient", + "basis operation above frame zero", + "cleanup omitted", + "target price incorrectly inherited from K", + "middle PK used instead of PKQ", + "missing (P-I)K(Q-I) cross term" + ], + "helper_only": { + "ADDs": 19982, + "forward_prefix": 202699, + "histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload_bits": 102, + "payload_prefix_upper": "3191004937361206117331766365184", + "rank_mass": 5112, + "record_sha256": "17cf0f3edef8899ed34c180c89f9eb9d49d03dcb6d0e1a4a9ae5ea7973df9e46", + "records": 22940, + "reverse_prefix": 2446788 + }, + "helper_pairs": 201, + "labels": { + "frames": 672, + "gram_det": 1, + "labels": 120, + "lattice_rank": 8 + }, + "literal_H2_and_K_accept": false, + "naive_sum_of_predecessor_savings_is_not_the_result": { + "actual": 8368, + "naive": 10084 + }, + "saved_over_PR694": 1434, + "saved_over_original": 8368, + "scope": "finite two-sided D construction; no new kappa", + "status": "PASS_R420_TWO_SIDED_BASIS", + "target_orientations_scored": 14280, + "target_pairs": 57 +} diff --git a/research/r420-two-sided-basis/CLAIM.json b/research/r420-two-sided-basis/CLAIM.json new file mode 100644 index 0000000000..b81cd3d3a7 --- /dev/null +++ b/research/r420-two-sided-basis/CLAIM.json @@ -0,0 +1,50 @@ +{ + "track": "Bit supplier", + "assignment_seed": 2, + "randomness": "secrets.randbelow(100), operating-system randomness, 2026-10-13 04:47:58 UTC", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "candidates": [ + { + "task": "another phase-B block synthesis", + "decision": "deferred: heavily explored by PR670/674/688" + }, + { + "task": "split final target reads into smaller frames", + "decision": "closed by PR718 for the fixed segment" + }, + { + "task": "two-sided D factorization with fixed PR694 helper pairs and fresh target pairing on KQ", + "decision": "chosen: neither PR694 nor PR713/716 composes both basis changes" + } + ], + "object": "PR543 D: fixed helper involution Q from PR694; seed-2 target involution P scored on KQ; fully paid P K Q implementation", + "method": "score all 14280 target orientations on KQ, one seeded greedy disjoint pass, exact all-input/frame/positive-prefix and C++ 5/9/11-stage replay", + "expected_deliverable": "finite two-sided construction and compatibility evidence; no kappa", + "expected_finish_utc": "2026-10-13 05:09:00 UTC", + "coordination": "No pinned coordination issue; local claim", + "overlap_checked_through_pr": 730, + "optimistic_complete_cost": { + "helpers_unchanged": 420, + "Q_preparation_and_restoration": 402, + "P_preparation_and_restoration": 114, + "middle_helper_reads": 11038, + "D_total": 11554, + "full_native_ADDs": 18548, + "new_helpers": 0, + "new_COPYs": 0, + "new_frame_moves": 0, + "payload_bits": 103, + "no_kappa": "Recursive profile unchanged; global invoice and assembly still separate" + }, + "status": "completed", + "result": { + "original_native_ADDs": 26916, + "helper_only_native_ADDs": 19982, + "new_native_ADDs": 18548, + "saved": 8368, + "incremental_saving": 1434, + "payload_bits": 103, + "kappa": "unchanged", + "url": "https://github.com/swbiggart/integer-mult-bounds/tree/research/seed2-two-sided-d/research/r420-two-sided-basis" + } +} diff --git a/research/r420-two-sided-basis/NATIVE-CERTIFICATE.json b/research/r420-two-sided-basis/NATIVE-CERTIFICATE.json new file mode 100644 index 0000000000..8a2f7a5a48 --- /dev/null +++ b/research/r420-two-sided-basis/NATIVE-CERTIFICATE.json @@ -0,0 +1,52 @@ +{ + "source_pins": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1", + "status": "PASS_R420_TWO_SIDED_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-two-sided-basis/README.md b/research/r420-two-sided-basis/README.md new file mode 100644 index 0000000000..e808135b92 --- /dev/null +++ b/research/r420-two-sided-basis/README.md @@ -0,0 +1,191 @@ +# Two-sided basis factoring of the R420 dirt correction + +**Finite bit-circuit construction and composition evidence; no new κ.** +This combines Greer Guthrie's PR694 helper-basis construction with a fresh +target matching on its transformed coefficient matrix. The result saves +**8,368 binary XORs** in PR543's complete native word: +**26,916 → 18,548**, including all preparation and restoration. It saves +**1,434 more ADDs than PR694**. The predecessor mechanisms are credited to +their authors; the contribution here is the checked two-sided construction. + +| Quantity | Original PR543 | Helper basis PR694 | Two-sided | +|---|---:|---:|---:| +| D additions | 19,922 | 12,988 | 11,554 | +| Complete native ADDs | 26,916 | 19,982 | 18,548 | +| Exported records | 29,874 | 22,940 | 21,506 | +| Forward positive prefix | 144,651 | 202,699 | 202,699 | +| Reverse positive prefix | 2,270,064 | 2,446,788 | 4,152,374 | +| Local payload allowance, bits | 100 | 102 | 103 | +| Helpers / copies / rank mass | 420 / 9 / 5,112 | same | same | + +All 201 helper pairs from PR694 are fixed. All 57 target pairs are nominated +on the resulting matrix `KQ`, using seed 2. The complete D cost is +**201 + 57 + 11,038 + 57 + 201 = 11,554 ADDs**. It uses the same registers, +no new source access, no additional scratch, no new frame movements, and +no additional copies or recursive children. All transformed helpers are +restored before A. + +The larger reverse prefix is fully charged: +`64 * 202699^3 * 4152374^2 = 9190258315617780048732559342336 < 2^104`. +This is a local cohort bound, not a rebuilt hosted-parent invoice. No old +global precision charge or bit exponent is inherited for the changed word. + +## Reproduce + +Python 3.9 or later, standard library only: + +```sh +python3 -B research/r420-two-sided-basis/verify.py +python3 -B -m unittest discover -s research/r420-two-sided-basis -p 'test_*.py' +``` + +Expected verifier output: + +```text +PASS_R420_TWO_SIDED_BASIS native_ADDs=26916->18548 saved=8368 beyond_PR694=1434 payload_bits=103 kappa=unchanged +``` + +For fresh, unchanged C++17 legality and five-/nine-/eleven-stage checks: + +```sh +python3 -B research/r420-two-sided-basis/native.py +``` + +Boost headers are required; set `BOOST_INCLUDE` to their containing directory +and `CXX` to the compiler if needed. Expected final line: + +```text +PASS_R420_TWO_SIDED_BASIS_NATIVE words=2 stages=5,9,11 columns=900,1380,1620 bridge_controls=96 missing_D_controls=6 +``` + +Both entry points compare the complete committed certificates. Explicit +`--write-certificate NEW_PATH` requires a new path and never overwrites a +file. Optimized Python is refused because the inherited exporter uses +assertions. The checker compares decompressed source bytes, so changing gzip +headers does not invalidate the mathematical input. + +## Exact construction and sufficient interface + +All matrices in this construction act over F2. Let the old D be +`(x,s,y) -> (x,s,y+Ks)`, for 420 arbitrary dirty helpers `s` and 120 arbitrary +targets `y`. Let `Q` be PR694's product of disjoint helper transvections, +and `P` the product of the new disjoint target transvections. Both satisfy +`P^2=I` and `Q^2=I`. The literal new D is: + +1. Execute Q on the helpers, obtaining `Qs` (201 ADDs). +2. Execute P on the targets, obtaining `Py` (57 ADDs). +3. Add `(PKQ)(Qs)` to `Py`, using exactly 11,038 helper reads. +4. Undo P (57 ADDs), then undo Q (201 ADDs). + +Thus the target output is `P(Py+PKQ Qs)=y+Ks`, and the helpers return to `s`. +Every gate touches only target/helper registers at frame zero. No source is +accessed in D. Every field outside D is required to equal the original word. +Substitution of this equal complete prefix preserves the original endpoint. + +The target matching must be scored on `KQ`, not K. For a proposed pair +`(a,b)`, its fully charged saving is +`weight((KQ)_b) - weight((KQ)_a XOR (KQ)_b) - 2`. +Adding the standalone predecessor savings (6,934 + 3,150 = 10,084) is not +the saving of this circuit. The exact result is 8,368. + +Writing `P=I+A` and `Q=I+B` gives +`PKQ = K + AK + KB + AKB`. The last term is necessary: a control that omits +only `AKB` fails the full D operator. The tests separately check all 50,400 +middle-matrix coefficients using this direct four-term formula rather than +the producer's sequential row changes. + +The original literal H2 and literal extraction of K reject the changed D +syntax. They remain unchanged. The sufficient semantic replacement is that +D is a legal zero-frame prefix implementing exactly `(x,s,y+Ks)` and +restoring every helper. The proof above and the complete 660-input operator +check establish that finite claim; all other original H1/H3/H4/H5 and +decomposed conclusions are checked. Acceptance of this semantic replacement +under the inherited common-label/mutable-basis interface remains a review +obligation. + +Every register has exactly its original ordered frame path. The entire +MOVE/COPY/ERASE subsequence is identical, so the paid histogram remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}` with rank mass 5,112. All retained +copies, their closing operations, helper restoration and recursive children +are counted. F2 endpoint equality is not asserted to be equality of the +two forward integer operators. Signed inverse shears and cancellation-free +integer prefix bounds are checked separately by the retained C++ tools. + +## Evidence, search coverage and independence + +The verifier reconstructs PR694 from its recipe using direct row updates, +checks its complete native record hash and both prefix bounds against that +author's certificate, then constructs and exports the new word. It checks +original, helper-only and two-sided words on all 660 arbitrary inputs in +both directions. E8 geometry and full scalar legality use eumemic's retained +checker. Record synthesis and set-valued replay reuse pinned PR713 utilities; +this is **not a wholly independent implementation** of those checks. + +The official exporter independently matches every literal instruction. +Fresh unchanged C++ checks cover original and combined words on +900/1,380/1,620 formal columns at five/nine/eleven stages. All 96 omitted +bridges and six omitted-D-end controls are rejected across the two words. +Ten local controls include both helper/target preparation and restoration, +a wrong coefficient, illegal frame, omitted cleanup, stale target pricing, +using PK instead of PKQ, and omitting only the cross term. Four additional +tests check the direct matrix formula, all pair scores, overlap and cost. + +The OS assignment seed is **2**. Candidate tasks were another phase-B block +synthesis (crowded by PR670/674/688), split target frames (closed in the +specified domain by PR718), and this two-sided composition (chosen). +Exactly 14,280 ordered target pairs on the fixed KQ matrix are scored. +Lexicographic pair enumeration with `random.Random(2)` tie keys and one +decreasing `(gain,tie,a,b)` greedy disjoint pass selects 57 pairs. Search +stops after that pass. There is no matching optimality or general circuit +optimality claim. `CLAIM.json` records the local claim because no pinned +coordination issue existed. The presubmission refresh covered open PRs through +#730 and found no two-sided composition. + +## Provenance, attribution and scope + +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +Selected source: PR626 `660de893d27bb7abd1d5b01b1640207528a5c851`, +conditional κ `51110230636731/31250000000000000`, using eumemic's PR543 +`2065fe4f72a914d907f1046603f5a36f17018535` bit supplier. + +Direct predecessors: + +- **Greer Guthrie's [PR694](https://github.com/CrocSwap/integer-mult-bounds/pull/694)**, + `9732ac127dd4bef98a846aaa904c20b5a84e72c1`: all 201 helper pairs and the + helper-only construction. Its recipe, certificate, README and notice are + retained byte for byte. PR686 (Mikhail R. Gadelha) supplies the preceding + single-helper-pair mechanism and semantic prefix contract. +- **Scott Woolsey Biggart's [PR713](https://github.com/CrocSwap/integer-mult-bounds/pull/713)**, + `1a19af5c5ddb6de9797a6d085e5df0b90ed6d58b`: target-basis construction and + record/set verification utilities. Those utilities and its recipe/README + are retained byte for byte; the native harness is adapted with attribution. +- Sagar Thakrar's concurrent [PR716](https://github.com/CrocSwap/integer-mult-bounds/pull/716), + `c804e7d79ac524723aa8c2d0d6a59d5e662763b3`, independently corroborates the + target-pair construction. It is credited, not imported. Its attribution + points to Dugongue's earlier [PR476](https://github.com/CrocSwap/integer-mult-bounds/pull/476), + `e850569c33ad1d5771e2f8b1c6dfe7a445396167`, for reversible target factoring + in phase B, following PR450. No new elementary identity is claimed here. + +PR708's decoder sharing, PR710's cleanup conjugation and the phase-A/B block +improvements are not composed here. PR661/711/718 concern restricted frame +searches, which this changed circuit does not reopen. `SOURCES.json` pins +every consumed source and the exact commits/Git blobs of vendored inputs. +Original attribution and licenses are retained in the linked notices. + +The selected construction and `upstream/` are unchanged. The selected assembly +is complex-limited, and this identical recursive profile does not produce a +new exponent. Full hosted-parent emission, whole-owner allocation, revised +global precision/finite invoices and outer assembly are separate integration +work. All inherited compiler/common-label/mutable-basis/physical/hosting/ +residual/precision/tape/analytic assumptions remain. This is finite evidence, +not a formal proof of the full multiplication theorem or a measured runtime +improvement. + +Prepared by **Scott Woolsey Biggart (@swbiggart)** with substantial +**OpenAI Codex assistance** in research, implementation, proof, verification +and packaging. Apache-2.0; no independent human review claimed. Credit also +remains with eumemic, Dylan Crow, DaysSky, Zhihao Chen, DreamingOfClouds, +Chafik Boukhalfa, icekylinx, Rohan Arun and the cumulative lineage in the +unchanged [R420 notice](../e8-bit-r420/NOTICE.md), +[carrier notice](../e8-bit-carrier-skeleton/NOTICE.md) and +[PR694 notice](vendor/pr694-NOTICE.md). diff --git a/research/r420-two-sided-basis/RECIPE.json b/research/r420-two-sided-basis/RECIPE.json new file mode 100644 index 0000000000..7c6acd2a10 --- /dev/null +++ b/research/r420-two-sided-basis/RECIPE.json @@ -0,0 +1,293 @@ +{ + "assignment_seed": 2, + "fixed_helper_recipe_sha256": "df48dd3b1c8d1d0f8894bb901043a9a8ba21777ecdacb21800c22fd71290d01e", + "matrix_scored": "KQ", + "ordered_target_pairs_scored": 14280, + "target_pairs": [ + [ + 222, + 219, + 46 + ], + [ + 145, + 148, + 44 + ], + [ + 239, + 233, + 42 + ], + [ + 236, + 234, + 42 + ], + [ + 143, + 137, + 41 + ], + [ + 230, + 224, + 40 + ], + [ + 139, + 141, + 39 + ], + [ + 225, + 231, + 36 + ], + [ + 174, + 173, + 35 + ], + [ + 120, + 125, + 35 + ], + [ + 133, + 131, + 35 + ], + [ + 144, + 149, + 35 + ], + [ + 193, + 194, + 34 + ], + [ + 156, + 200, + 34 + ], + [ + 182, + 176, + 33 + ], + [ + 181, + 196, + 32 + ], + [ + 185, + 191, + 32 + ], + [ + 134, + 128, + 31 + ], + [ + 170, + 189, + 31 + ], + [ + 138, + 140, + 28 + ], + [ + 217, + 220, + 28 + ], + [ + 229, + 227, + 27 + ], + [ + 208, + 214, + 27 + ], + [ + 198, + 178, + 26 + ], + [ + 199, + 179, + 26 + ], + [ + 136, + 142, + 25 + ], + [ + 154, + 205, + 25 + ], + [ + 235, + 237, + 25 + ], + [ + 238, + 232, + 24 + ], + [ + 151, + 146, + 24 + ], + [ + 207, + 202, + 24 + ], + [ + 162, + 135, + 24 + ], + [ + 124, + 122, + 24 + ], + [ + 152, + 158, + 24 + ], + [ + 212, + 210, + 23 + ], + [ + 211, + 209, + 23 + ], + [ + 216, + 221, + 22 + ], + [ + 171, + 186, + 22 + ], + [ + 183, + 195, + 20 + ], + [ + 213, + 215, + 20 + ], + [ + 163, + 166, + 20 + ], + [ + 123, + 126, + 19 + ], + [ + 169, + 187, + 19 + ], + [ + 218, + 223, + 18 + ], + [ + 197, + 180, + 17 + ], + [ + 157, + 155, + 16 + ], + [ + 165, + 160, + 16 + ], + [ + 184, + 175, + 15 + ], + [ + 168, + 177, + 14 + ], + [ + 172, + 190, + 11 + ], + [ + 203, + 206, + 11 + ], + [ + 127, + 121, + 11 + ], + [ + 188, + 150, + 11 + ], + [ + 228, + 226, + 10 + ], + [ + 159, + 167, + 8 + ], + [ + 132, + 129, + 7 + ], + [ + 161, + 164, + 3 + ] + ] +} diff --git a/research/r420-two-sided-basis/SOURCES.json b/research/r420-two-sided-basis/SOURCES.json new file mode 100644 index 0000000000..5d718e11e6 --- /dev/null +++ b/research/r420-two-sided-basis/SOURCES.json @@ -0,0 +1,123 @@ +{ + "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" + }, + "research/r420-two-sided-basis/vendor/pr694-RECIPE.json": { + "representation": "bytes", + "sha256": "df48dd3b1c8d1d0f8894bb901043a9a8ba21777ecdacb21800c22fd71290d01e" + }, + "research/r420-two-sided-basis/vendor/pr694-CERTIFICATE.json": { + "representation": "bytes", + "sha256": "f31f84984274591641b515758eb5dbfa202963f9d805e4326f0d45e625a9a62d" + }, + "research/r420-two-sided-basis/vendor/pr694-README.md": { + "representation": "bytes", + "sha256": "49ac485beb609b3871ee7aee8f477e5d3ffd54109f2008cb040725fd4da9b8cb" + }, + "research/r420-two-sided-basis/vendor/pr694-NOTICE.md": { + "representation": "bytes", + "sha256": "0e0e3adfd8322d5de4d197ceb46a37169a22904342ab079076ae6ac4afe806fa" + }, + "research/r420-two-sided-basis/vendor/pr713-verify.py": { + "representation": "bytes", + "sha256": "48f7ad712a9a137166b4db8b7b625d37fb958573e445a7f136d6c5279895fc7d" + }, + "research/r420-two-sided-basis/vendor/pr713-RECIPE.json": { + "representation": "bytes", + "sha256": "cc899dec908e8d4a199944c3d6ed2643e50ac363ca9d94691425e71dec7694a5" + }, + "research/r420-two-sided-basis/vendor/pr713-README.md": { + "representation": "bytes", + "sha256": "3c716471d30ba70bdfda3f1e250f91dffe8951c036a844ea2b9e873d02737ef4" + } + }, + "predecessors": { + "research/r420-two-sided-basis/vendor/pr694-RECIPE.json": { + "commit": "9732ac127dd4bef98a846aaa904c20b5a84e72c1", + "source_path": "research/r420-compensation-basis/RECIPE.json", + "git_blob": "d81608927fd166b166b873eaa4125d2cc63c38a1" + }, + "research/r420-two-sided-basis/vendor/pr694-CERTIFICATE.json": { + "commit": "9732ac127dd4bef98a846aaa904c20b5a84e72c1", + "source_path": "research/r420-compensation-basis/CERTIFICATE.json", + "git_blob": "df40ea3be48a5f21b6199a96b854d407538005ee" + }, + "research/r420-two-sided-basis/vendor/pr694-README.md": { + "commit": "9732ac127dd4bef98a846aaa904c20b5a84e72c1", + "source_path": "research/r420-compensation-basis/README.md", + "git_blob": "f7666c749e23c75ae18beb921befe4801337cb59" + }, + "research/r420-two-sided-basis/vendor/pr694-NOTICE.md": { + "commit": "9732ac127dd4bef98a846aaa904c20b5a84e72c1", + "source_path": "research/r420-compensation-basis/NOTICE.md", + "git_blob": "f6aa24934dcd7c6b400be8e0f07183517c8128a3" + }, + "research/r420-two-sided-basis/vendor/pr713-verify.py": { + "commit": "1a19af5c5ddb6de9797a6d085e5df0b90ed6d58b", + "source_path": "research/r420-target-basis/verify.py", + "git_blob": "f31d59473990bb9b395c3314da721318a03e20a7" + }, + "research/r420-two-sided-basis/vendor/pr713-RECIPE.json": { + "commit": "1a19af5c5ddb6de9797a6d085e5df0b90ed6d58b", + "source_path": "research/r420-target-basis/RECIPE.json", + "git_blob": "31adc3b8bc4958d1e81d3ad028ae396ee6479bd7" + }, + "research/r420-two-sided-basis/vendor/pr713-README.md": { + "commit": "1a19af5c5ddb6de9797a6d085e5df0b90ed6d58b", + "source_path": "research/r420-target-basis/README.md", + "git_blob": "3fb52afa32f35094c50a0c6aca42ea7ed5cab1d5" + } + } +} diff --git a/research/r420-two-sided-basis/VALIDATION.json b/research/r420-two-sided-basis/VALIDATION.json new file mode 100644 index 0000000000..289387a26a --- /dev/null +++ b/research/r420-two-sided-basis/VALIDATION.json @@ -0,0 +1,52 @@ +{ + "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" + ], + "exact_certificates": "PASS all versions", + "unit_tests": "four passed on all versions; direct 50400-entry matrix formula and complete 14280 pair-score census", + "native": { + "status": "PASS", + "compiler": "Apple Clang 21.0.0", + "boost": "1.85.0", + "boost_archive_sha256": "7009fe1faa1697476bdc7027703a2badb84e849b7b0baad5086b087b971f8617", + "words": [ + "original", + "two-sided" + ], + "stage_counts": [ + 5, + 9, + 11 + ], + "formal_columns": [ + 900, + 1380, + 1620 + ], + "omitted_bridge_controls_total": 96, + "omitted_D_controls_total": 6, + "receipt": "NATIVE-CERTIFICATE.json" + }, + "selected_result_check": "PASS", + "overlap_checked_through": 730, + "not_claimed": [ + "full hosted-parent/owner replay", + "new global finite invoice", + "changed-word outer assembly", + "repository-wide make verify pass", + "full Lean theorem", + "remote CI at local commit time" + ], + "repository_suite_context": "The earlier session-wide make verify attempt stopped at missing Boost after earlier groups passed. It was not repeated for this isolated research addition. Both affected native words now pass fresh unchanged C++ checks with pinned Boost.", + "minimal_checkout": "PASS: package and declared sources only, launched outside checkout with recompressed word", + "external_rejection_controls": [ + "underpriced certificate", + "altered pinned PR694 recipe", + "optimized Python" + ] +} diff --git a/research/r420-two-sided-basis/native.py b/research/r420-two-sided-basis/native.py new file mode 100644 index 0000000000..298d844491 --- /dev/null +++ b/research/r420-two-sided-basis/native.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Fresh unchanged PR543 C++ checks for the two-sided D circuit. + +Harness adapted from Scott Woolsey Biggart / OpenAI Codex PR713. + +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_TWO_SIDED_BASIS_NATIVE', 'source_pins': v.sha((v.HERE / 'SOURCES.json').read_bytes()), + 'words': {}} + with tempfile.TemporaryDirectory(prefix='r420-two-sided-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 helper 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_TWO_SIDED_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-two-sided-basis/test_verify.py b/research/r420-two-sided-basis/test_verify.py new file mode 100644 index 0000000000..268bebf1d8 --- /dev/null +++ b/research/r420-two-sided-basis/test_verify.py @@ -0,0 +1,55 @@ +"""Exact obligations specific to two-sided composition; Apache-2.0.""" +import copy +import unittest + +import verify as v + + +class TwoSidedTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.word = v.read_sources() + cls.recipe = v.nominate(cls.word) + + def test_four_term_matrix_formula(self): + original = v.original_rows(self.word) + _, helper_gates = v.helper_transform(self.word) + target_parent = {b: a for a, b, _ in self.recipe['target_pairs']} + helper_parent = {g[2][0]: g[1] for g in helper_gates} + # Direct four-entry formula, without sequential basis transformation. + expected = {} + for t in range(120, 240): + expected[t] = set() + for h in range(240, 660): + ts = [t] + ([target_parent[t]] if t in target_parent else []) + hs = [h] + ([helper_parent[h]] if h in helper_parent else []) + if sum(s in original[r] for r in ts for s in hs) % 2: + expected[t].add(h) + word = v.build(self.word, self.recipe) + boundary = len(helper_gates) + len(self.recipe['target_pairs']) + middle = {dst: set(srcs) for _, dst, srcs in word['D'][boundary:-boundary]} + self.assertEqual(expected, middle) + + def test_all_target_scores_by_column_incidence(self): + matrix, _ = v.helper_transform(self.word) + for a in range(120, 240): + for b in range(120, 240): + if a != b: + cost = sum(1 if s in matrix[b] else -1 for s in range(240, 660) if s in matrix[a]) - 2 + self.assertEqual(cost, len(matrix[b]) - len(matrix[a] ^ matrix[b]) - 2) + + def test_overlapping_target_pairs_rejected(self): + recipe = copy.deepcopy(self.recipe) + recipe['target_pairs'].append(recipe['target_pairs'][0]) + with self.assertRaisesRegex(v.Reject, 'overlap'): + v.build(self.word, recipe) + + def test_no_uncharged_basis_operations(self): + recipe = copy.deepcopy(self.recipe) + recipe['target_pairs'][0][2] += 2 + with self.assertRaisesRegex(v.Reject, 'priced on KQ'): + v.build(self.word, recipe) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/r420-two-sided-basis/vendor/pr694-CERTIFICATE.json b/research/r420-two-sided-basis/vendor/pr694-CERTIFICATE.json new file mode 100644 index 0000000000..df40ea3be4 --- /dev/null +++ b/research/r420-two-sided-basis/vendor/pr694-CERTIFICATE.json @@ -0,0 +1,126 @@ +{ + "after": { + "D_binary_additions": 12988, + "D_grouped_gates": 522, + "binary_additions": 19982, + "exported_records": 22940, + "forward_and_reverse": [ + { + "columns": 660, + "copies": 9 + }, + { + "columns": 660, + "copies": 9 + } + ], + "forward_prefix": 202699, + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca", + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload_prefix_bits": 102, + "payload_prefix_upper": "3191004937361206117331766365184", + "rank_mass": 5112, + "record_sha256": "17cf0f3edef8899ed34c180c89f9eb9d49d03dcb6d0e1a4a9ae5ea7973df9e46", + "reverse_prefix": 2446788, + "scalar_stream_sha256": "06007a8cad184bf9bea1941a5b0a19ce6273992836f8e0250d1173eff7e05c91", + "semantic_word_sha256": "02a652417125bef15a2c01946a642d45dae8bba11a09a1ac13f3b7d2057be3dc" + }, + "all_other_legacy_interface_checks_pass": true, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "before": { + "D_binary_additions": 19922, + "D_grouped_gates": 120, + "binary_additions": 26916, + "exported_records": 29874, + "forward_and_reverse": [ + { + "columns": 660, + "copies": 9 + }, + { + "columns": 660, + "copies": 9 + } + ], + "forward_prefix": 144651, + "frame_paths_sha256": "ef52add0118de86406ed3c58d6ff53b06b127c05238895b475181e55b98021ca", + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "payload_prefix_bits": 100, + "payload_prefix_upper": "998206739997057013039187410944", + "rank_mass": 5112, + "record_sha256": "f7e6cceaceb04d7bd70918981405dcead988a890cfca03b51e80d935f00a960f", + "reverse_prefix": 2270064, + "scalar_stream_sha256": "95be862aadd3cd5dc9a8ba76e1ede1cc367d51f26fc24af3f56795b4807ba6f0", + "semantic_word_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2" + }, + "binary_additions_saved": 6934, + "controls": [ + { + "name": "missing compute", + "rejected_by": "D endpoint differs on an independent input column" + }, + { + "name": "missing helper restoration", + "rejected_by": "D endpoint differs on an independent input column" + }, + { + "name": "missing recoded target read", + "rejected_by": "D endpoint differs on an independent input column" + }, + { + "name": "cancelled compute", + "rejected_by": "D endpoint differs on an independent input column" + }, + { + "name": "nonzero prefix frame", + "rejected_by": "D is not at the zero frame" + }, + { + "name": "F2-neutral target-fed helper outside the contract", + "rejected_by": "D reads a source or target" + }, + { + "name": "unrelated A change", + "rejected_by": "change outside D" + }, + { + "accepted_endpoint": true, + "extra_binary_additions": 2, + "name": "neutral pair still charged" + } + ], + "labels": { + "frames": 672, + "gram_det": 1, + "labels": 120, + "lattice_rank": 8 + }, + "legacy_H2_accepts_changed_syntax": false, + "legacy_raw_D_column_extraction_accepts_changed_syntax": false, + "matching_pairs": 201, + "schema": "r420-compensation-basis/1", + "scope": "Finite circuit improvement; semantic D-prefix substitution is proved separately. No new kappa or hosted-supplier invoice.", + "seed": 12, + "semantic_prefix_contract": { + "all_columns": 660, + "all_helpers_restored_before_A": true, + "dirty_helper_columns": 420, + "target_response_sha256": "98e46ceb6f4dc645e07c02417ac8782cc2de48406f793d5441ca7ce2f3acb7b2" + }, + "source_pr": 543, + "source_pr_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "status": "PASS_R420_COMPENSATION_BASIS", + "touched_helpers": 402 +} diff --git a/research/r420-two-sided-basis/vendor/pr694-NOTICE.md b/research/r420-two-sided-basis/vendor/pr694-NOTICE.md new file mode 100644 index 0000000000..f6aa24934d --- /dev/null +++ b/research/r420-two-sided-basis/vendor/pr694-NOTICE.md @@ -0,0 +1,27 @@ +# Attribution and license + +Prepared by **Greer Guthrie (g-guthrie)** with substantial **OpenAI Codex** +assistance in research, implementation, verification and writing. New +material is under the repository's Apache-2.0 license. + +- **eumemic**: #543 R420 bit circuit, source data, interleaved-interface + proof, exact labels/frames and arbitrary-dirty-input checker; #493 lineage. +- **Dylan Crow / DreamingOfClouds**: the literal record exporter, E8 + adaptations and preceding bit-circuit work. +- **DaysSky**: the generalized bridged-stage column checker and its controls. +- **Zhihao Chen, Chafik Boukhalfa, icekylinx, Rohan Arun** and all authors + credited in the retained #543/#493 notices: mutable-source realization, + compilation, hosting, exact arithmetic and finite accounting. +- **Mikhail R. Gadelha (@mikhailramalho), concurrent #686**: the same + restored frame-zero helper-pair mechanism and semantic prefix contract, + published for helpers 552/521 while this experiment was underway. That + pair is included here. This contribution adds the 201-pair simultaneous + matching and its full cost/prefix evidence, without a priority claim for + the one-pair idea. No #686 source code is imported. +- **yongjae321, x0hu and Ali Romman**, #670/#674/#688: distinct concurrent + phase-B block simplifications and their integration; not imported here. + +The elementary binary basis-change identity is standard linear algebra. +The response-kernel/entrance lineage, including #259, is related prior +work; this construction restores its helper basis before the unchanged A. +All original files and their assistance disclosures remain unchanged. diff --git a/research/r420-two-sided-basis/vendor/pr694-README.md b/research/r420-two-sided-basis/vendor/pr694-README.md new file mode 100644 index 0000000000..f7666c749e --- /dev/null +++ b/research/r420-two-sided-basis/vendor/pr694-README.md @@ -0,0 +1,223 @@ +# R420 compensation through 201 restored helper-basis pairs + +**Finite bit-circuit improvement; no new κ.** The frame-zero dirt +compensation in eumemic's accepted #543 R420 word uses 19,922 binary XOR +additions. A simultaneous disjoint helper-basis change reduces this to +**12,988**, including all 201 preparation and 201 restoration additions. +The complete native word falls from **26,916 to 19,982 ADDs**: 6,934 fewer, +about 25.8%. No helper, COPY, frame transition or recursive rank is removed. + +The signed-prefix allowance rises from 100 to **102 bits**, within the +original strict 104-bit cap. This tradeoff is part of the result; a lower +ADD count alone would not establish admissibility. A hosted-parent invoice +and integration of the semantic prefix contract remain separate work. + +## Reproduce + +Python 3.11 or later, standard library only: + +```sh +python3 -B research/r420-compensation-basis/verify.py +``` + +Expected: + +```text +PASS_R420_COMPENSATION_BASIS D=19922->12988 native_ADDs=26916->19982 saved=6934 rank_mass=5112 payload_bits=102<104 +``` + +This regenerates the seeded matching, rebuilds the word, checks all pinned +sources, compares the complete certificate, runs the original E8/frame and +all-column audits, checks the semantic prefix contract independently, and +replays both exported scalar orientations and their positive-prefix bills. +It takes about two seconds on the contributor's macOS machine. Checks stay +active under `-I -O`; no admission predicate relies on Python assertions. +The unchanged exporter is launched in a separate isolated interpreter with +assertions enabled. + +For the unchanged C++ legality and five/nine/eleven-stage column checkers: + +```sh +python3 -B research/r420-compensation-basis/verify.py --native +``` + +This additionally requires a C++17 compiler and Boost headers. Use +`--cxx /path/to/compiler --boost-include /path/to/include` when needed. +`--output /path/to/new-directory` writes the reconstructed `word.json.gz`, +the matched `certificate.json`, and, with `--native`, `native.json`. +An existing output directory is rejected. Linux CI runs the native command +on Python 3.11 and 3.14; its result is reported separately from local tests. + +## Sources and concurrent work + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The reviewed #543 source head is `2065fe4f72a914d907f1046603f5a36f17018535`. +[SOURCES.json](SOURCES.json) pins the exact word, checker, emitter, C++ +sources and supporting files. The word's full decompressed payload is +pinned, so changing only gzip headers does not invalidate its mathematics. + +The first reference word has semantic SHA-256 +`e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2`; +the reconstructed candidate has +`02a652417125bef15a2c01946a642d45dae8bba11a09a1ac13f3b7d2057be3dc`. +All fields except `D` are identical, including literal `A`, `B`, `C`, +the scatter, labels, source/target boundaries and retained totals. + +**Concurrent #686 is directly related and credited.** Mikhail R. Gadelha's +[single-pair contribution](https://github.com/CrocSwap/integer-mult-bounds/pull/686), +at `23dcb610c2b156b76b9d599ea296c3cbde224b2d`, appeared while this experiment +was underway. It publishes the same restored frame-zero mechanism for +helpers 552 and 521, saving 108 ADDs, and states the same semantic H2 +replacement. This matching contains that pair. No priority for that +mechanism or contract is claimed here. The additional result is a literal +**201-pair simultaneous construction**, its complete 6,934-ADD reduction, +and the measured increase in prefix bounds. No #686 code is imported. + +The earlier #670/#674 proposals change separate phase-B blocks; #688 +composes and hosts those block changes. This word does not import those +changes. #661 fixes D and the scalar gate stream. The historical +response-kernel/entrance lineage, including #259, changes recursive +interfaces; this prefix restores its entire helper basis before A. + +## Circuit and sufficient prefix contract + +Let `s` be the 420 arbitrary helper inputs, `y` the 120 arbitrary targets, +and `K` the binary 120-by-420 compensation matrix read from the original D. +The source inputs `x` are untouched by D. The required prefix is + +```text +(x, s, y) -> (x, s, y + K s), over F2. +``` + +Choose disjoint ordered helper pairs `(a,b)`. Each preparation operation is +`s_a <- s_a XOR s_b`. Let their product be `P`. Every elementary operation +is an involution; disjointness makes them commute, and the implementation +also records a literal reverse-order undo. Replace the original reads by +the matrix `K' = K P^-1`: + +```text +s' = P s +y' = y + K' s' = y + K s +s = P^-1 s'. +``` + +For one pair this keeps column `K_a` and changes column `K_b` to +`K_b XOR K_a`. The operations are ordinary binary XORs, at frame zero, +on existing helpers. Every helper is restored before the first A gate. +There are no initialized scratch, fresh-zero helper, source-access or +free-restoration assumptions. Arbitrarily correlated helper inputs are +covered by the full linear operator identity. + +All starts of the touched helper and target registers are frame zero. +Consequently preparation, recoded reads and restoration introduce no +MOVE or recursive child. Their scalar work is charged explicitly. The +unchanged remainder sees exactly the original `(x,s,y+Ks)` state and the +original frames. Under the inherited common-label realization, this +pointwise frame-zero identity supplies the same prefix on every address. +It does not prove that inherited all-size realization interface anew. + +### Why the old syntactic H2 still rejects this representation + +The original `xcheck.py` requires every D destination to be a target. +It also extracts K by reading each D gate as a direct helper-to-target +addition. Those two predicates cannot represent a temporary helper basis. +They continue to reject this candidate; no predecessor checker is patched +or its rejection hidden. + +The sufficient replacement is stronger than a comparison on clean inputs: +every D gate is legal at frame zero, uses only existing helpers as donors, +does not write a source, and its **complete operator on all 660 input +columns equals the original D**. All 420 helper columns are restored. +Every field outside D must equal the pinned word. The verifier checks this +with independent set-valued symbolic rows before relying on the original +interleaved-prefix proof. It separately runs the original checker on the +actual changed word: labels, frames, full arbitrary-dirt endpoint and all +other interface predicates pass. The canonical source word still passes +every original H1–H5 and conclusion predicate. + +This is a finite semantic-prefix substitution with a written composition +argument, not a claim that the changed syntax is accepted by every existing +supplier pipeline. In particular, no signed integer endpoint equality is +asserted: the circuit identity is over F2, and the signed lift's actual +nonnegative coefficient bounds are recomputed below. + +## Search and complete bill + +The operating-system assignment seed was **12**, selecting the bit track. +It seeds only the tie order in a deterministic greedy matching. Three +candidate tasks and the local scope claim are recorded in +[CLAIM.json](CLAIM.json); no pinned coordination issue existed. + +For columns `K_a,K_b`, the net saving from `s_a ^= s_b` is + +```text +weight(K_b) - weight(K_b XOR K_a) - 2. +``` + +The final `2` pays preparation and restoration. Both orientations of all +87,990 unordered helper pairs are scored. For each pair retain its better +positive orientation (lower-index destination breaks orientation ties), +then sort by descending gain and seed-12 64-bit tie keys. Take a pair only +when neither helper has already been used. The selected gains are additive +because the supports are disjoint. There are 27,653 positive candidates +and 201 selected pairs, touching 402 existing helpers. + +The stopping rule is exactly one complete pair-score enumeration and one +greedy matching. No maximum-weight matching, optimal circuit, or exhaustive +multi-operation search is claimed. [RECIPE.json](RECIPE.json) freezes the +literal pairs and gains; the verifier re-nominates them and also recounts +the complete emitted program, so a search score is not an admission receipt. + +| Item | Original | Changed | +|---|---:|---:| +| Basis preparation ADDs | 0 | 201 | +| Compensation target ADDs | 19,922 | 12,586 | +| Basis restoration ADDs | 0 | 201 | +| Complete D ADDs | 19,922 | 12,988 | +| Complete native ADDs | 26,916 | 19,982 | +| Exported records | 29,874 | 22,940 | +| Helpers / COPYs | 420 / 9 | 420 / 9 | +| Rank mass | 5,112 | 5,112 | +| Forward positive-prefix bound | 144,651 | 202,699 | +| Reverse positive-prefix bound | 2,270,064 | 2,446,788 | +| `64 * forward^3 * reverse^2`, in bits | 100 | 102 | + +Binary ADDs are the primitive count. The higher-level grouped D gate count +actually rises from 120 to 522, because each of the 120 target rows was +already represented as one multi-source gate. The unchanged recursive +profile is `{1:1320, 2:1440, 4:60, 5:120, 8:9}`. Every register's complete +frame path, not just that histogram, is compared exactly. The normalizer +counts all ADDs, source accesses, COPY and ERASE operations in the literal +record stream; no work is inferred from a reduced matrix rank. + +## Evidence and limitations + +[CERTIFICATE.json](CERTIFICATE.json) retains exact input/output hashes, +all-column results, chronological frame-path hash, emitted-record hashes, +primitive counts and integer prefix bounds. Its seven rejection controls +cover missing preparation, missing restoration, a missing recoded read, +cancelled preparation, nonzero prefix frames, a neutral target-fed-helper +pair outside the stated contract, and an unrelated A change. A positive +control inserts a cancelling helper pair: it has the correct endpoint and +must still be charged two ADDs. + +[VALIDATION.json](VALIDATION.json) records local normal/optimized execution, +a relocated minimal checkout with a recompressed input, and rejection of +corrupt source data, a changed recipe and an underpriced prefix certificate. +The separate selected-record inventory/proof binding check passed as well. + +The `--native` path compiles the original C++ sources and checks 900, +1,380 and 1,620 formal columns at five, nine and eleven stages. It retains +all 6/18/24 omitted-bridge controls and requires the independently computed +prefix bounds and profiles to agree. Removing a helper restoration must +also fail the actual C++ endpoint check at each stage count. The original +legality check prices the emitted ADDs, frame moves and COPY lifecycles. + +This is a useful finite circuit reduction, not an exponent improvement. +Full hosted-parent reconstruction, whole-owner/finite invoices, integration +of the semantic D-prefix contract and a changed-word outer assembly remain +necessary before treating it as an admitted supplier replacement. The +all-size compiler, common-label/mutable-basis realization, whole-call +hosting, precision/tape and analytic-transfer assumptions remain inherited. +No practical multiplication speedup, full Lean proof or selected-frontier +change is claimed. See [NOTICE.md](NOTICE.md) for attribution. diff --git a/research/r420-two-sided-basis/vendor/pr694-RECIPE.json b/research/r420-two-sided-basis/vendor/pr694-RECIPE.json new file mode 100644 index 0000000000..d81608927f --- /dev/null +++ b/research/r420-two-sided-basis/vendor/pr694-RECIPE.json @@ -0,0 +1,1015 @@ +{ + "optimality_claim": false, + "orientations_per_pair": 2, + "pairs": [ + { + "dst": 552, + "net_saved_additions": 108, + "src": 521 + }, + { + "dst": 286, + "net_saved_additions": 97, + "src": 296 + }, + { + "dst": 275, + "net_saved_additions": 65, + "src": 448 + }, + { + "dst": 477, + "net_saved_additions": 65, + "src": 249 + }, + { + "dst": 425, + "net_saved_additions": 63, + "src": 415 + }, + { + "dst": 433, + "net_saved_additions": 63, + "src": 280 + }, + { + "dst": 360, + "net_saved_additions": 62, + "src": 350 + }, + { + "dst": 435, + "net_saved_additions": 62, + "src": 451 + }, + { + "dst": 395, + "net_saved_additions": 62, + "src": 369 + }, + { + "dst": 613, + "net_saved_additions": 62, + "src": 637 + }, + { + "dst": 549, + "net_saved_additions": 62, + "src": 584 + }, + { + "dst": 380, + "net_saved_additions": 62, + "src": 351 + }, + { + "dst": 404, + "net_saved_additions": 62, + "src": 304 + }, + { + "dst": 371, + "net_saved_additions": 62, + "src": 389 + }, + { + "dst": 386, + "net_saved_additions": 62, + "src": 365 + }, + { + "dst": 354, + "net_saved_additions": 62, + "src": 340 + }, + { + "dst": 370, + "net_saved_additions": 61, + "src": 348 + }, + { + "dst": 263, + "net_saved_additions": 61, + "src": 472 + }, + { + "dst": 463, + "net_saved_additions": 61, + "src": 289 + }, + { + "dst": 419, + "net_saved_additions": 61, + "src": 403 + }, + { + "dst": 313, + "net_saved_additions": 61, + "src": 422 + }, + { + "dst": 429, + "net_saved_additions": 61, + "src": 319 + }, + { + "dst": 550, + "net_saved_additions": 60, + "src": 650 + }, + { + "dst": 532, + "net_saved_additions": 60, + "src": 565 + }, + { + "dst": 639, + "net_saved_additions": 60, + "src": 597 + }, + { + "dst": 493, + "net_saved_additions": 60, + "src": 511 + }, + { + "dst": 531, + "net_saved_additions": 60, + "src": 566 + }, + { + "dst": 527, + "net_saved_additions": 60, + "src": 558 + }, + { + "dst": 547, + "net_saved_additions": 60, + "src": 586 + }, + { + "dst": 413, + "net_saved_additions": 60, + "src": 329 + }, + { + "dst": 551, + "net_saved_additions": 60, + "src": 582 + }, + { + "dst": 621, + "net_saved_additions": 60, + "src": 633 + }, + { + "dst": 376, + "net_saved_additions": 60, + "src": 372 + }, + { + "dst": 453, + "net_saved_additions": 60, + "src": 300 + }, + { + "dst": 442, + "net_saved_additions": 59, + "src": 277 + }, + { + "dst": 504, + "net_saved_additions": 58, + "src": 423 + }, + { + "dst": 602, + "net_saved_additions": 58, + "src": 583 + }, + { + "dst": 540, + "net_saved_additions": 58, + "src": 604 + }, + { + "dst": 400, + "net_saved_additions": 57, + "src": 324 + }, + { + "dst": 290, + "net_saved_additions": 56, + "src": 516 + }, + { + "dst": 467, + "net_saved_additions": 56, + "src": 268 + }, + { + "dst": 367, + "net_saved_additions": 55, + "src": 341 + }, + { + "dst": 303, + "net_saved_additions": 55, + "src": 454 + }, + { + "dst": 392, + "net_saved_additions": 54, + "src": 505 + }, + { + "dst": 627, + "net_saved_additions": 54, + "src": 248 + }, + { + "dst": 305, + "net_saved_additions": 54, + "src": 420 + }, + { + "dst": 595, + "net_saved_additions": 54, + "src": 655 + }, + { + "dst": 337, + "net_saved_additions": 54, + "src": 362 + }, + { + "dst": 272, + "net_saved_additions": 54, + "src": 436 + }, + { + "dst": 358, + "net_saved_additions": 54, + "src": 336 + }, + { + "dst": 622, + "net_saved_additions": 54, + "src": 634 + }, + { + "dst": 295, + "net_saved_additions": 54, + "src": 452 + }, + { + "dst": 414, + "net_saved_additions": 54, + "src": 317 + }, + { + "dst": 616, + "net_saved_additions": 54, + "src": 640 + }, + { + "dst": 375, + "net_saved_additions": 54, + "src": 390 + }, + { + "dst": 325, + "net_saved_additions": 54, + "src": 410 + }, + { + "dst": 449, + "net_saved_additions": 53, + "src": 291 + }, + { + "dst": 416, + "net_saved_additions": 53, + "src": 307 + }, + { + "dst": 345, + "net_saved_additions": 53, + "src": 394 + }, + { + "dst": 308, + "net_saved_additions": 53, + "src": 312 + }, + { + "dst": 461, + "net_saved_additions": 53, + "src": 445 + }, + { + "dst": 430, + "net_saved_additions": 53, + "src": 311 + }, + { + "dst": 409, + "net_saved_additions": 53, + "src": 431 + }, + { + "dst": 378, + "net_saved_additions": 53, + "src": 385 + }, + { + "dst": 399, + "net_saved_additions": 53, + "src": 393 + }, + { + "dst": 282, + "net_saved_additions": 53, + "src": 434 + }, + { + "dst": 383, + "net_saved_additions": 52, + "src": 387 + }, + { + "dst": 596, + "net_saved_additions": 52, + "src": 656 + }, + { + "dst": 614, + "net_saved_additions": 52, + "src": 638 + }, + { + "dst": 533, + "net_saved_additions": 52, + "src": 619 + }, + { + "dst": 601, + "net_saved_additions": 52, + "src": 649 + }, + { + "dst": 620, + "net_saved_additions": 52, + "src": 632 + }, + { + "dst": 580, + "net_saved_additions": 52, + "src": 544 + }, + { + "dst": 427, + "net_saved_additions": 52, + "src": 598 + }, + { + "dst": 278, + "net_saved_additions": 52, + "src": 570 + }, + { + "dst": 523, + "net_saved_additions": 52, + "src": 559 + }, + { + "dst": 469, + "net_saved_additions": 51, + "src": 479 + }, + { + "dst": 446, + "net_saved_additions": 51, + "src": 273 + }, + { + "dst": 548, + "net_saved_additions": 50, + "src": 585 + }, + { + "dst": 412, + "net_saved_additions": 50, + "src": 323 + }, + { + "dst": 529, + "net_saved_additions": 50, + "src": 539 + }, + { + "dst": 279, + "net_saved_additions": 49, + "src": 462 + }, + { + "dst": 608, + "net_saved_additions": 48, + "src": 659 + }, + { + "dst": 600, + "net_saved_additions": 48, + "src": 625 + }, + { + "dst": 610, + "net_saved_additions": 48, + "src": 528 + }, + { + "dst": 498, + "net_saved_additions": 48, + "src": 502 + }, + { + "dst": 603, + "net_saved_additions": 48, + "src": 346 + }, + { + "dst": 253, + "net_saved_additions": 46, + "src": 484 + }, + { + "dst": 355, + "net_saved_additions": 46, + "src": 497 + }, + { + "dst": 252, + "net_saved_additions": 45, + "src": 259 + }, + { + "dst": 492, + "net_saved_additions": 44, + "src": 338 + }, + { + "dst": 534, + "net_saved_additions": 44, + "src": 509 + }, + { + "dst": 495, + "net_saved_additions": 44, + "src": 568 + }, + { + "dst": 391, + "net_saved_additions": 44, + "src": 515 + }, + { + "dst": 246, + "net_saved_additions": 44, + "src": 240 + }, + { + "dst": 475, + "net_saved_additions": 44, + "src": 465 + }, + { + "dst": 243, + "net_saved_additions": 44, + "src": 456 + }, + { + "dst": 407, + "net_saved_additions": 44, + "src": 417 + }, + { + "dst": 255, + "net_saved_additions": 43, + "src": 474 + }, + { + "dst": 247, + "net_saved_additions": 43, + "src": 271 + }, + { + "dst": 251, + "net_saved_additions": 41, + "src": 260 + }, + { + "dst": 287, + "net_saved_additions": 40, + "src": 438 + }, + { + "dst": 569, + "net_saved_additions": 38, + "src": 575 + }, + { + "dst": 631, + "net_saved_additions": 38, + "src": 508 + }, + { + "dst": 457, + "net_saved_additions": 36, + "src": 437 + }, + { + "dst": 314, + "net_saved_additions": 34, + "src": 402 + }, + { + "dst": 443, + "net_saved_additions": 34, + "src": 455 + }, + { + "dst": 257, + "net_saved_additions": 32, + "src": 468 + }, + { + "dst": 283, + "net_saved_additions": 32, + "src": 288 + }, + { + "dst": 320, + "net_saved_additions": 30, + "src": 334 + }, + { + "dst": 306, + "net_saved_additions": 28, + "src": 326 + }, + { + "dst": 293, + "net_saved_additions": 28, + "src": 458 + }, + { + "dst": 459, + "net_saved_additions": 26, + "src": 364 + }, + { + "dst": 267, + "net_saved_additions": 26, + "src": 478 + }, + { + "dst": 285, + "net_saved_additions": 26, + "src": 447 + }, + { + "dst": 327, + "net_saved_additions": 24, + "src": 347 + }, + { + "dst": 342, + "net_saved_additions": 24, + "src": 359 + }, + { + "dst": 332, + "net_saved_additions": 22, + "src": 444 + }, + { + "dst": 441, + "net_saved_additions": 22, + "src": 269 + }, + { + "dst": 379, + "net_saved_additions": 22, + "src": 373 + }, + { + "dst": 330, + "net_saved_additions": 20, + "src": 440 + }, + { + "dst": 382, + "net_saved_additions": 20, + "src": 343 + }, + { + "dst": 242, + "net_saved_additions": 18, + "src": 470 + }, + { + "dst": 264, + "net_saved_additions": 18, + "src": 357 + }, + { + "dst": 381, + "net_saved_additions": 18, + "src": 615 + }, + { + "dst": 476, + "net_saved_additions": 18, + "src": 245 + }, + { + "dst": 418, + "net_saved_additions": 18, + "src": 315 + }, + { + "dst": 352, + "net_saved_additions": 18, + "src": 439 + }, + { + "dst": 261, + "net_saved_additions": 18, + "src": 483 + }, + { + "dst": 651, + "net_saved_additions": 18, + "src": 406 + }, + { + "dst": 401, + "net_saved_additions": 16, + "src": 361 + }, + { + "dst": 302, + "net_saved_additions": 16, + "src": 292 + }, + { + "dst": 310, + "net_saved_additions": 16, + "src": 363 + }, + { + "dst": 530, + "net_saved_additions": 16, + "src": 514 + }, + { + "dst": 256, + "net_saved_additions": 16, + "src": 266 + }, + { + "dst": 464, + "net_saved_additions": 14, + "src": 377 + }, + { + "dst": 328, + "net_saved_additions": 14, + "src": 421 + }, + { + "dst": 396, + "net_saved_additions": 14, + "src": 428 + }, + { + "dst": 368, + "net_saved_additions": 14, + "src": 384 + }, + { + "dst": 250, + "net_saved_additions": 14, + "src": 487 + }, + { + "dst": 318, + "net_saved_additions": 14, + "src": 450 + }, + { + "dst": 466, + "net_saved_additions": 12, + "src": 398 + }, + { + "dst": 557, + "net_saved_additions": 12, + "src": 658 + }, + { + "dst": 274, + "net_saved_additions": 12, + "src": 339 + }, + { + "dst": 374, + "net_saved_additions": 12, + "src": 460 + }, + { + "dst": 297, + "net_saved_additions": 12, + "src": 432 + }, + { + "dst": 471, + "net_saved_additions": 12, + "src": 301 + }, + { + "dst": 294, + "net_saved_additions": 10, + "src": 366 + }, + { + "dst": 349, + "net_saved_additions": 10, + "src": 581 + }, + { + "dst": 333, + "net_saved_additions": 10, + "src": 335 + }, + { + "dst": 344, + "net_saved_additions": 10, + "src": 331 + }, + { + "dst": 284, + "net_saved_additions": 10, + "src": 397 + }, + { + "dst": 244, + "net_saved_additions": 10, + "src": 411 + }, + { + "dst": 316, + "net_saved_additions": 10, + "src": 353 + }, + { + "dst": 496, + "net_saved_additions": 10, + "src": 567 + }, + { + "dst": 426, + "net_saved_additions": 10, + "src": 281 + }, + { + "dst": 322, + "net_saved_additions": 10, + "src": 507 + }, + { + "dst": 270, + "net_saved_additions": 8, + "src": 299 + }, + { + "dst": 405, + "net_saved_additions": 8, + "src": 298 + }, + { + "dst": 657, + "net_saved_additions": 8, + "src": 388 + }, + { + "dst": 574, + "net_saved_additions": 8, + "src": 545 + }, + { + "dst": 588, + "net_saved_additions": 8, + "src": 262 + }, + { + "dst": 606, + "net_saved_additions": 8, + "src": 254 + }, + { + "dst": 636, + "net_saved_additions": 8, + "src": 276 + }, + { + "dst": 624, + "net_saved_additions": 8, + "src": 473 + }, + { + "dst": 579, + "net_saved_additions": 8, + "src": 408 + }, + { + "dst": 503, + "net_saved_additions": 8, + "src": 265 + }, + { + "dst": 591, + "net_saved_additions": 6, + "src": 644 + }, + { + "dst": 642, + "net_saved_additions": 6, + "src": 593 + }, + { + "dst": 609, + "net_saved_additions": 6, + "src": 626 + }, + { + "dst": 499, + "net_saved_additions": 6, + "src": 241 + }, + { + "dst": 556, + "net_saved_additions": 6, + "src": 520 + }, + { + "dst": 618, + "net_saved_additions": 6, + "src": 635 + }, + { + "dst": 554, + "net_saved_additions": 6, + "src": 482 + }, + { + "dst": 589, + "net_saved_additions": 6, + "src": 646 + }, + { + "dst": 630, + "net_saved_additions": 6, + "src": 489 + }, + { + "dst": 560, + "net_saved_additions": 6, + "src": 424 + }, + { + "dst": 612, + "net_saved_additions": 6, + "src": 641 + }, + { + "dst": 525, + "net_saved_additions": 6, + "src": 561 + }, + { + "dst": 564, + "net_saved_additions": 6, + "src": 506 + }, + { + "dst": 645, + "net_saved_additions": 6, + "src": 590 + }, + { + "dst": 512, + "net_saved_additions": 6, + "src": 494 + }, + { + "dst": 587, + "net_saved_additions": 6, + "src": 546 + }, + { + "dst": 605, + "net_saved_additions": 6, + "src": 648 + }, + { + "dst": 643, + "net_saved_additions": 6, + "src": 592 + }, + { + "dst": 577, + "net_saved_additions": 6, + "src": 541 + }, + { + "dst": 538, + "net_saved_additions": 6, + "src": 309 + }, + { + "dst": 526, + "net_saved_additions": 6, + "src": 562 + }, + { + "dst": 563, + "net_saved_additions": 6, + "src": 522 + }, + { + "dst": 481, + "net_saved_additions": 6, + "src": 258 + }, + { + "dst": 491, + "net_saved_additions": 6, + "src": 321 + }, + { + "dst": 571, + "net_saved_additions": 6, + "src": 535 + }, + { + "dst": 517, + "net_saved_additions": 4, + "src": 553 + }, + { + "dst": 542, + "net_saved_additions": 4, + "src": 578 + }, + { + "dst": 607, + "net_saved_additions": 4, + "src": 628 + }, + { + "dst": 537, + "net_saved_additions": 4, + "src": 573 + }, + { + "dst": 519, + "net_saved_additions": 4, + "src": 555 + }, + { + "dst": 599, + "net_saved_additions": 4, + "src": 654 + }, + { + "dst": 524, + "net_saved_additions": 4, + "src": 543 + }, + { + "dst": 536, + "net_saved_additions": 4, + "src": 572 + }, + { + "dst": 576, + "net_saved_additions": 2, + "src": 652 + } + ], + "positive_pair_candidates": 27653, + "seed": 12, + "stopping_rule": "one score enumeration and one greedy matching", + "unordered_pairs_scored": 87990 +} diff --git a/research/r420-two-sided-basis/vendor/pr713-README.md b/research/r420-two-sided-basis/vendor/pr713-README.md new file mode 100644 index 0000000000..3fb52afa32 --- /dev/null +++ b/research/r420-two-sided-basis/vendor/pr713-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-two-sided-basis/vendor/pr713-RECIPE.json b/research/r420-two-sided-basis/vendor/pr713-RECIPE.json new file mode 100644 index 0000000000..31adc3b8bc --- /dev/null +++ b/research/r420-two-sided-basis/vendor/pr713-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-two-sided-basis/vendor/pr713-verify.py b/research/r420-two-sided-basis/vendor/pr713-verify.py new file mode 100644 index 0000000000..f31d594739 --- /dev/null +++ b/research/r420-two-sided-basis/vendor/pr713-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) diff --git a/research/r420-two-sided-basis/verify.py b/research/r420-two-sided-basis/verify.py new file mode 100644 index 0000000000..8be8816df6 --- /dev/null +++ b/research/r420-two-sided-basis/verify.py @@ -0,0 +1,267 @@ +#!/usr/bin/env python3 +"""Two-sided R420 D factorization, exact finite evidence; Apache-2.0. + +Scott Woolsey Biggart, with substantial OpenAI Codex assistance. +Builds on Greer Guthrie's PR694 and the author's PR713; see README. +""" +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 + +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' + + +def load_module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +class Reject(Exception): + pass + + +def need(condition, reason): + if not condition: + raise Reject(reason) + + +def read_sources(): + for path, pin in json.loads((HERE / 'SOURCES.json').read_text())['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 original_rows(word): + matrix = {} + for frame, dst, sources in word['D']: + need(frame == 0 and 120 <= dst < 240 and dst not in matrix and + len(sources) == len(set(sources)) and all(240 <= s < 660 for s in sources), 'original D shape') + matrix[dst] = set(sources) + need(set(matrix) == set(range(120, 240)), 'complete original rows') + return matrix + + +def helper_transform(word): + """Recover KQ by changing rows directly, independently of PR694's columns.""" + recipe = json.loads((HERE / 'vendor/pr694-RECIPE.json').read_text()) + matrix = original_rows(word) + used, gates, savings = set(), [], 0 + for pair in recipe['pairs']: + a, b = pair['dst'], pair['src'] + need(240 <= a < 660 and 240 <= b < 660 and a != b and not ({a, b} & used), + 'helper pairs must be disjoint') + before = sum(len(row) for row in matrix.values()) + for row in matrix.values(): + if a in row: + row.symmetric_difference_update({b}) + gain = before - sum(len(row) for row in matrix.values()) - 2 + need(gain == pair['net_saved_additions'] and gain > 0, 'PR694 helper gain') + savings += gain + used.update((a, b)) + gates.append([0, a, [b]]) + need(len(gates) == 201 and savings == 6934, 'PR694 recipe totals') + return matrix, gates + + +def nominate(word): + matrix, _ = helper_transform(word) + rng = random.Random(2) + 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, pairs = set(), [] + for gain, _, a, b in sorted(candidates, reverse=True): + if gain > 0 and not ({a, b} & used): + pairs.append([a, b, gain]) + used.update((a, b)) + return {'assignment_seed': 2, 'fixed_helper_recipe_sha256': sha((HERE / 'vendor/pr694-RECIPE.json').read_bytes()), + 'matrix_scored': 'KQ', 'ordered_target_pairs_scored': len(candidates), 'target_pairs': pairs} + + +def build(word, recipe, helper_only=False): + matrix, q_gates = helper_transform(word) + used, p_gates = set(), [] + for a, b, gain in ([] if helper_only else recipe['target_pairs']): + need(a in matrix and b in matrix and a != b and not ({a, b} & used), 'target matching overlap') + need(gain == len(matrix[b]) - len(matrix[a] ^ matrix[b]) - 2 and gain > 0, + 'target gain must be priced on KQ') + matrix[b] ^= matrix[a] + used.update((a, b)) + p_gates.append([0, b, [a]]) + changed = copy.deepcopy(word) + changed['D'] = q_gates + p_gates + [[0, t, sorted(row)] for t, row in sorted(matrix.items()) if row] + changed['D'] += copy.deepcopy(list(reversed(p_gates)) + list(reversed(q_gates))) + return changed + + +def prefix(word): + values = [{r} for r in range(660)] + for frame, dst, srcs in word['D']: + need(frame == 0 and 120 <= dst < 660 and srcs and + len(set(srcs + [dst])) == len(srcs) + 1 and all(120 <= s < 660 for s in srcs), 'D frame/operands') + need(dst < 240 or all(s >= 240 for s in srcs), 'target feeds a helper') + for src in srcs: + values[dst].symmetric_difference_update(values[src]) + return values + + +def contract(word, changed): + need({k: v for k, v in word.items() if k != 'D'} == {k: v for k, v in changed.items() if k != 'D'}, + 'outside D changed') + need(prefix(word) == prefix(changed), 'arbitrary-input D operator changed') + + +def controls(word, changed, recipe): + names = [] + def reject(name, action): + try: + action() + except Reject: + names.append(name) + else: + raise Reject('negative control accepted: ' + name) + for name, index in [('missing helper preparation', 0), ('missing target preparation', 201), + ('missing target restoration', -202), ('missing helper restoration', -1)]: + mutant = copy.deepcopy(changed); mutant['D'].pop(index) + reject(name, lambda: contract(word, mutant)) + mutant = copy.deepcopy(changed); mutant['D'][258][2].pop() + reject('wrong PKQ helper coefficient', lambda: contract(word, mutant)) + mutant = copy.deepcopy(changed); mutant['D'][0][0] = 1 + reject('basis operation above frame zero', lambda: contract(word, mutant)) + mutant = copy.deepcopy(changed); mutant['C'].pop() + reject('cleanup omitted', lambda: contract(word, mutant)) + wrong = copy.deepcopy(recipe) + a, b, _ = wrong['target_pairs'][0] + original = original_rows(word) + wrong['target_pairs'][0][2] = len(original[b]) - len(original[a] ^ original[b]) - 2 + need(wrong != recipe, 'stale-price control must differ') + reject('target price incorrectly inherited from K', lambda: build(word, wrong)) + # The middle must be PKQ, not PK. Omitting Q from its coefficients is invalid. + q = changed['D'][:201] + p = changed['D'][201:258] + matrix = original_rows(word) + for a, b, _ in recipe['target_pairs']: + matrix[b] ^= matrix[a] + mutant = copy.deepcopy(word) + mutant['D'] = q + p + [[0, t, sorted(row)] for t, row in sorted(matrix.items()) if row] + mutant['D'] += copy.deepcopy(list(reversed(p)) + list(reversed(q))) + reject('middle PK used instead of PKQ', lambda: contract(word, mutant)) + # Combining the separate changes also requires their bilinear cross term. + original = original_rows(word) + target_parent = {b: a for a, b, _ in recipe['target_pairs']} + helper_parent = {gate[2][0]: gate[1] for gate in q} + incomplete = {} + for t in range(120, 240): + incomplete[t] = {s for s in range(240, 660) if + ((s in original[t]) ^ + (t in target_parent and s in original[target_parent[t]]) ^ + (s in helper_parent and helper_parent[s] in original[t]))} + mutant['D'] = q + p + [[0, t, sorted(row)] for t, row in sorted(incomplete.items()) if row] + mutant['D'] += copy.deepcopy(list(reversed(p)) + list(reversed(q))) + reject('missing (P-I)K(Q-I) cross term', lambda: contract(word, mutant)) + return names + + +def certificate(): + word = read_sources() + # Import pinned predecessor tools only after verifying their bytes. + old = load_module('pr713_utilities', HERE / 'vendor/pr713-verify.py') + geometry = load_module('r420_geometry', ROOT / CHECK) + recipe = nominate(word) + need(recipe == json.loads((HERE / 'RECIPE.json').read_text()), 'matching differs') + helper = build(word, recipe, helper_only=True) + changed = build(word, recipe) + contract(word, helper); contract(word, changed) + baseline = geometry.Word(word) + labels = baseline.labels(); baseline.full() + h, c, _ = baseline.interface() + need(all(h.values()) and all(c.values()), 'original interface') + for candidate in (helper, changed): + check = geometry.Word(candidate); check.full() + h, c, _ = check.interface() + need([k for k, ok in h.items() if not ok] == ['H2_D_frame0_targets_from_helpers'] and + [k for k, ok in c.items() if not ok] == ['K_equals_D'], 'only literal H2/K may fail') + streams = [old.records(w, baseline.fdim) for w in (word, helper, changed)] + common = [r for r in streams[0] if r[0] != 1] + need(all([r for r in stream if r[0] != 1] == common for stream in streams), 'frame/copy paths differ') + bills = [] + with tempfile.TemporaryDirectory(prefix='r420-two-sided-') as tmp: + for i, (w, stream) in enumerate(zip((word, helper, changed), streams)): + folder = Path(tmp) / str(i); folder.mkdir() + # Same retained exporter as PR713, supplied via this checkout. + path = folder / 'word.json'; path.write_bytes(canonical(w)) + subprocess.run([sys.executable, '-I', '-B', str(ROOT / EXPORT), str(path), str(folder / 'out')], + check=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE) + actual = list(struct.iter_unpack('<6i', (folder / 'out/249-records.bin').read_bytes())) + need(actual == stream, 'official exporter stream mismatch') + bills.append(old.bill(stream)) + predecessor = json.loads((HERE / 'vendor/pr694-CERTIFICATE.json').read_text())['after'] + for key, original_key in [('ADDs', 'binary_additions'), ('record_sha256', 'record_sha256'), + ('forward_prefix', 'forward_prefix'), ('reverse_prefix', 'reverse_prefix'), + ('payload_prefix_upper', 'payload_prefix_upper')]: + need(bills[1][key] == predecessor[original_key], 'PR694 reconstruction: ' + key) + need(bills[0]['histogram'] == bills[1]['histogram'] == bills[2]['histogram'] == + {'1': 1320, '2': 1440, '4': 60, '5': 120, '8': 9}, 'paid profile') + extra = sum(p[2] for p in recipe['target_pairs']) + need(bills[1]['ADDs'] - bills[2]['ADDs'] == extra == 1434, 'fully charged incremental gain') + return {'status': 'PASS_R420_TWO_SIDED_BASIS', 'base_commit': '66849e1475c930fd7732b1a0067ffee7e1e95f60', + 'assignment_seed': 2, 'scope': 'finite two-sided D construction; no new kappa', + 'labels': labels, 'helper_pairs': 201, 'target_pairs': len(recipe['target_pairs']), + 'target_orientations_scored': recipe['ordered_target_pairs_scored'], + 'before': bills[0], 'helper_only': bills[1], 'after': bills[2], + 'D_ADDs': [sum(len(g[2]) for g in w['D']) for w in (word, helper, changed)], + 'saved_over_original': bills[0]['ADDs'] - bills[2]['ADDs'], 'saved_over_PR694': extra, + 'naive_sum_of_predecessor_savings_is_not_the_result': {'naive': 6934 + 3150, 'actual': 8368}, + 'columns_in_each_direction': 660, 'changed_word_canonical_sha256': sha(canonical(changed)), + 'controls': controls(word, changed, recipe), 'literal_H2_and_K_accept': False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', type=Path) + args = parser.parse_args() + need(not sys.flags.optimize, 'run without -O: inherited exporter uses 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_TWO_SIDED_BASIS native_ADDs=26916->18548 saved=8368 beyond_PR694=1434 payload_bits=103 kappa=unchanged') + + +if __name__ == '__main__': + try: + main() + except (Reject, OSError, ValueError, KeyError) as error: + print('REJECT:', error, file=sys.stderr) + sys.exit(1)