diff --git a/research/r420-block5-resynthesis/CLAIM.json b/research/r420-block5-resynthesis/CLAIM.json new file mode 100644 index 0000000000..e283655f73 --- /dev/null +++ b/research/r420-block5-resynthesis/CLAIM.json @@ -0,0 +1,23 @@ +{ + "track": "bit supplier", + "assignment_seed": 5, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "claimed_at_utc": "2026-10-13T03:28:00Z", + "expected_finish_utc": "2026-10-13T04:05:00Z", + "coordination": "GitHub pinnedIssues returned no nodes; claim recorded locally", + "object": "PR543 R420 bit word, zero-based D4 block 5, twelve-register phase-B XOR transform and its literal cleanup", + "method": "Exact local XOR circuit identities and bounded bidirectional synthesis, beyond the predecessor randomized LU class; compare complete word scalar semantics, restoration, frames and cancellation-free cost", + "deliverable": "One pinned reversible-circuit improvement with exact checks, or a reproducible scoped negative result; no kappa claim from gate count alone", + "candidates_considered": [ + "Simultaneous phase-B frame reassignment: overlapped by PR661", + "E8 decoder changes: heavily covered by PR620 and PR631", + "Block-5 circuit resynthesis: selected; changes gate stream excluded by PR661" + ], + "overlap_snapshot": "Open PRs through #668; review ledger and existing negative results inspected", + "status": "completed", + "result": "Block 5: 46 -> 34 XORs; literal cleanup saves another 12; full native ADDs 26916 -> 26892; complete 660-column replay, identical frame paths and rank profile; no new kappa", + "final_overlap_snapshot": "Open PRs refreshed through #671; concurrent #670 rewrites distinct block3, credited in README", + "stopping_rule": "Stopped after five exact common-sum rewrites yielded a verified improvement; no exhaustive search or optimum claimed", + "result_url": "https://github.com/x0hu/integer-mult-bounds/tree/codex/r420-block5-resynthesis/research/r420-block5-resynthesis" +} diff --git a/research/r420-block5-resynthesis/README.md b/research/r420-block5-resynthesis/README.md new file mode 100644 index 0000000000..1366b768f1 --- /dev/null +++ b/research/r420-block5-resynthesis/README.md @@ -0,0 +1,164 @@ +# A 34-gate replacement for R420 block 5 + +This finite bit-circuit improvement replaces one 46-gate phase-B block of +eumemic's PR #543 R420 word with 34 gates on the same twelve registers. +Regenerating its literal cleanup saves another twelve gates. The full native +word uses 26,892 scalar ADDs instead of 26,916. All 660 symbolic input columns, +including arbitrary helper dirt, pass the predecessor's exact replay. + +The paid rank profile and every register's frame path are unchanged. This +contribution claims no new bit exponent or kappa. It does not change the +selected construction or any predecessor package. + +| Quantity | Original | Replacement | +|---|---:|---:| +| Block-5 XOR gates | 46 | 34 | +| Block plus literal cleanup, unit-input norm bound | 1,075 | 485 | +| Native word scalar ADDs | 26,916 | 26,892 | +| Native forward cancellation-free bound | 144,651 | 144,651 | +| Native reverse cancellation-free bound | 2,270,064 | 2,229,592 | +| Paid rank mass | 5,112 | 5,112 | +| Nine-stage prefix bound, bit length | 189 | 189 | +| Nine-stage charged prefix bits | 192 | 192 | + +## Reproduce + +From the repository root, with Python 3.11 or newer and no external packages: + +```sh +python3 -B research/r420-block5-resynthesis/verify.py +``` + +Expected final line: + +```text +PASS_R420_BLOCK5_RESYNTHESIS block=46->34 native_adds=26916->26892 rank_mass=5112 kappa=unchanged +``` + +To retain the rebuilt word and exported records, add +`--output /tmp/r420-block5-replay`. The default uses a temporary directory. +Verification reconstructs the candidate from the pinned original, checks the +exact matrices, replays both native words and compares the complete result with +`certificate.json`. Gzip containers are not compared: the certificate pins the +canonical decompressed JSON. Runs with Python's `-O` option are refused. + +## Exact change and proof + +The object is zero-based D4 block 5, at the half-open slice `B[371:417]` in +`research/e8-bit-r420/data/bitE8mut-r420.json.gz`. Its frame ID is 547 and its +registers, in matrix order, are + +```text +19, 24, 35, 40, 54, 56, 65, 74, 84, 95, 100, 111 +``` + +Each operation below means `destination += source`; reduce modulo two for the +bit circuit. Five explicit rewrites advance an existing addition before readers +that need the resulting sum, then remove their redundant direct reads: + +1. Advance `111 += 100` before the first read by register 54. Remove + `54 += 100`, `65 += 100` and `56 += 100`. +2. Advance `74 += 100` to immediately before the late reads by register 40. + Remove the additions from 100 to 40, 84, 19 and 95. +3. Advance `65 += 54` before `74 += 56`. Remove the additions from 54 to 74 + and 56. +4. Advance `56 += 65` before `74 += 56`. Remove `74 += 65`. +5. Advance `40 += 35` to the beginning of the block. Remove the additions + from 35 to 100 and 95. + +The gate counts after these steps are 43, 39, 37, 36 and 34. The certificate +includes the resulting operation list, original gate offsets, forward integer +matrix and both reverse majorant matrices. Each step preserves the full integer +forward matrix, with outputs on their original wires. Equality over the integers +implies equality over F2 and on arbitrary dirty register contents. No temporary +register, copy, source-access operation or extra frame change is introduced. + +For a list of additions, replace each evolving value by a nonnegative bound on +its norm and perform the same additions. The resulting nonnegative integer matrix +maps input norm bounds to output norm bounds. Norms never decrease within this +calculation, so terminal row bounds also bound every prefix. The replacement's +forward matrix equals the original's. Its literal-reverse majorant is entrywise +no larger, with 28 strict entries. Its forward-plus-reverse majorant has 97 strict +improvements. This comparison holds for every nonnegative starting-bound vector, +not only for the unit-input numbers in the table. The verifier also compares the +signed inverse matrices, obtained by reversing and negating the additions. + +All rewrites occur at one D4 frame between the same outside gates. Every affected +register still visits that frame. Exact replay checks legal nesting and equality +of the full per-register frame paths, including final climbs. Phase C is rebuilt +as the literal reverse of every source/helper write in A and B at the full frame. +The old D remains valid because the new block has the same map on all its inputs. +The predecessor's H1-H5 interface checks and U/J/K/U-inverse conclusions all pass. + +## Complete cost and limits + +`record_audit.py` independently interprets the predecessor exporter's MOVE, ADD, +COPY and ERASE stream in both directions. It checks all 660 columns, copied-center +lifecycle, complete frame paths, the rank histogram and cancellation-free prefix +bounds. The local histogram remains +`{1:1320, 2:1440, 4:60, 5:120, 8:9}`, including all nine rank-8 copies. +There are still 420 helpers, nine retained totals and 2,940 MOVE records. + +The five-stage prefix expression is `64 * cf^3 * cb^2`. The nine-stage expression +is `2^18 * cf^5 * cb^4`, with `cf` and `cb` the native forward and reverse bounds. +Both formulas and the nine-stage invoice code are pinned in `SOURCES.json`. +The exact unrounded bounds are in the certificate. The five-stage bound still +uses 100 bits and the nine-stage bound still uses 189 bits, charged at 192. + +In the inherited nine-stage, 32-replica invoice, the local-ADD term would decrease +by `9 * 32 * 24 = 6912`. The paid recursive profile is unchanged. This is a +reduction in finite circuit work and a prefix bound, not an asymptotic saving or +a measured multiplication speedup. No new owner assignment, hosted global program, +outer assembly or full frontier replay is supplied. Reusing the construction in +a selected supplier still calls for that supplier's normal complete replay. + +All-size compilation, common-label and mutable-basis realization, pooled hosting, +normalized residuals, precision/tape recovery and analytic transfer remain +inherited assumptions. Exact finite replay is not a formal proof of the full +integer multiplication theorem. + +## Coverage, controls and prior work + +Assignment seed 5 selected the bit-supplier track and block index `5 mod 10`. +The bounded experiment applied the five recorded sum-sharing rewrites to this +one block and stopped once they produced a verified improvement. A separate +worker briefly explored bidirectional elimination and did not supply the chosen +circuit. There is no exhaustive circuit search or optimality claim. In particular, +34 is an attained gate count, not a lower bound. + +Negative controls omit a block gate, alter its source, insert a doubled pair +that preserves F2 semantics but worsens the positive matrix, omit a cleanup gate, +use an illegal zero frame and reuse stale cleanup. The stale cleanup still has +the right scalar map but fails the required literal-reverse interface. Record +controls independently alter an ADD, a MOVE rank and COPY/ERASE lifecycle data. + +The exact base commit is +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. The source is eumemic's +[PR #543](https://github.com/CrocSwap/integer-mult-bounds/pull/543), pinned at +`2065fe4f72a914d907f1046603f5a36f17018535`. That contribution supplies the R420 +construction, interleaved interface argument and bill-aware LU circuit. +Eumemic's #493 supplies its skeleton; Dylan Crow's #370 lineage supplies the word +format and exporter; DreamingOfClouds' #510 and the #463/#442 lineage supply the +retained nine-stage accounting. Original source files and notices remain intact. + +[PR #661](https://github.com/CrocSwap/integer-mult-bounds/pull/661), inspected at +`9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89`, proves a fixed-order phase-B frame +bound and explicitly excludes circuit resynthesis. This contribution changes +the circuit while retaining its frame paths, consistent with that result. +DreamingOfClouds' incorporated #589 instead changes frames of the punctured bit +word and improves its paid profile. Decoder research in #620/#631 concerns a +different mechanism. Open-PR metadata and the review ledger informed the scope; +pending PR claims are not treated as accepted frontier results. + +The final refresh found yongjae321's concurrent +[PR #670](https://github.com/CrocSwap/integer-mult-bounds/pull/670), at +`2e31fcad7f9ecc8b97039ecb2333e581fd725fa1`. It reports a 50-to-33-gate replacement +for block 3. The contribution here replaces the separate 46-gate block 5 and +adds exact forward equality over the integers for its five explicit rewrites. +It does not depend on #670, and this package does not certify their composition. +Both contributions improve finite work while retaining the paid frame profile. + +Prepared for GitHub contributor **x0hu** with substantial OpenAI Codex assistance, +including separate Codex workers for circuit and record-level verification. No +independent human review is claimed. New files are under the repository's +Apache-2.0 license. diff --git a/research/r420-block5-resynthesis/SOURCES.json b/research/r420-block5-resynthesis/SOURCES.json new file mode 100644 index 0000000000..780d84a8e6 --- /dev/null +++ b/research/r420-block5-resynthesis/SOURCES.json @@ -0,0 +1,22 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "context_pr_heads": { + "661": "9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89", + "670": "2e31fcad7f9ecc8b97039ecb2333e581fd725fa1" + }, + "dependency_pr_heads": { + "543": "2065fe4f72a914d907f1046603f5a36f17018535" + }, + "sha256": { + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-r420/EXPECTED.json": "06eccee9f6b77e140833df83407e7996dc948c17d49b0779ab171fbe463fd28d", + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/e8-bit-r420/code/gen_l3.py": "d5c802447c99255db1bdfcae62b2116bfc9612c9dc9000d41aa4f5f2fec9f2f2", + "research/e8-bit-r420/code/nodeopt.py": "6a5896f60b1fe05c41ab28ce822dff782c635e12d0c74fad20b5ce2a4010fa3f", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/code/assemble9.py": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + } +} diff --git a/research/r420-block5-resynthesis/VALIDATION.json b/research/r420-block5-resynthesis/VALIDATION.json new file mode 100644 index 0000000000..cb1ed08e79 --- /dev/null +++ b/research/r420-block5-resynthesis/VALIDATION.json @@ -0,0 +1,31 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "platform": "macOS arm64", + "python_versions_passed": ["3.12.13", "3.13.12", "3.14.3"], + "reproduce": "python3 -B research/r420-block5-resynthesis/verify.py", + "expected": "PASS_R420_BLOCK5_RESYNTHESIS block=46->34 native_adds=26916->26892 rank_mass=5112 kappa=unchanged", + "checks": [ + "Exact matrix equality and reverse-majorant domination at each of five rewrites", + "Pinned predecessor E8 labels, 672 closed frames, 660 symbolic columns, H1-H5 and interface conclusions", + "Independent record interpreter: all columns in both directions, complete frame paths, paid histogram and prefix bounds", + "Six circuit/interface controls and four record controls on each of the two words", + "Optimized Python rejected with exit 1 before creating the requested output directory", + "Selected-record source binding and exact kappa check passed", + "Whitespace check passed" + ], + "review": { + "reviewer": "Separate OpenAI Codex worker, not involved in construction", + "result": "No mathematical or accounting blocker found", + "supplementary_checks": "Separately enumerated all 4096 block inputs and reversed both circuits; independently confirmed 97 strict roundtrip-majorant entries", + "fix_applied": "Use POSIX paths in source-digest receipt keys for portable JSON equality", + "human_review_claimed": false + }, + "not_run": [ + "Full C++ multistage replay", + "Complete hosted supplier invoice and frontier626 replay", + "Repository-wide make verify", + "Lean proof", + "Remote Linux or Windows execution" + ], + "scope_reason": "Standalone finite block/native-word addition; upstream, selected construction and existing generators are unchanged. Full integration still requires the normal supplier replay." +} diff --git a/research/r420-block5-resynthesis/certificate.json b/research/r420-block5-resynthesis/certificate.json new file mode 100644 index 0000000000..cc16574133 --- /dev/null +++ b/research/r420-block5-resynthesis/certificate.json @@ -0,0 +1,865 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "baseline_local_roundtrip_peak": 1075, + "baseline_reverse_majorant": [ + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 4, + 0, + 1, + 7, + 1 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 1, + 3, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3, + 1, + 1, + 5, + 0 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 5, + 2, + 1, + 9, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 3, + 0, + 0, + 7, + 2 + ], + [ + 0, + 0, + 0, + 0, + 2, + 4, + 1, + 9, + 0, + 0, + 23, + 7 + ], + [ + 0, + 0, + 0, + 0, + 1, + 2, + 1, + 5, + 0, + 0, + 13, + 4 + ], + [ + 0, + 0, + 0, + 0, + 4, + 7, + 2, + 18, + 0, + 0, + 44, + 13 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 5, + 2, + 1, + 9, + 1 + ], + [ + 0, + 0, + 2, + 1, + 0, + 0, + 0, + 10, + 3, + 3, + 18, + 1 + ], + [ + 1, + 2, + 5, + 2, + 0, + 0, + 0, + 29, + 8, + 8, + 52, + 3 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 2, + 1 + ] + ], + "candidate_canonical_sha256": "aef2fc8c510b87b4da62d5756c2be3d16da1c2557bfd8358e01ee25d02ffbc99", + "candidate_local_roundtrip_peak": 485, + "candidate_reverse_majorant": [ + [ + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 4, + 0, + 1, + 3, + 1 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 1, + 1, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3, + 1, + 1, + 1, + 0 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 5, + 2, + 1, + 1, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 1, + 0, + 3, + 0, + 0, + 3, + 2 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 1, + 3, + 0, + 0, + 3, + 3 + ], + [ + 0, + 0, + 0, + 0, + 1, + 2, + 1, + 5, + 0, + 0, + 5, + 4 + ], + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 2, + 0, + 0, + 2, + 1 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 5, + 2, + 1, + 3, + 1 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 4, + 1, + 1, + 2, + 1 + ], + [ + 1, + 2, + 1, + 2, + 0, + 0, + 0, + 17, + 4, + 4, + 10, + 3 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 2, + 1 + ] + ], + "cost": { + "baseline": { + "adds_by_phase": { + "1": 19922, + "2": 2376, + "3": 568, + "4": 1077, + "5": 2973 + }, + "five_stage_payload_bits": 100, + "five_stage_payload_bound": "998206739997057013039187410944", + "forward": { + "all_columns": 660, + "bits": 18, + "cancellation_free_row_l1": 144651, + "maximum_at": { + "destination": 528, + "phase": 5, + "record_in_direction": 29536 + } + }, + "negative_controls": { + "broken_COPY_source": "ERASE source frame or workspace mismatch", + "missing_ERASE": "copy workspace already open", + "modified_MOVE_rank": "MOVE rank mismatch", + "omitted_B_source_ADD": "scalar endpoint mismatch" + }, + "nine_stage_charged_prefix_bits": 192, + "nine_stage_prefix_bits": 189, + "nine_stage_prefix_bound": "440858815560454746902811617646181283465263876766227759104", + "operations": { + "0": 2940, + "1": 26916, + "2": 9, + "3": 9 + }, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "paid_rank_mass": 5112, + "records": 29874, + "reverse": { + "all_columns": 660, + "bits": 22, + "cancellation_free_row_l1": 2270064, + "maximum_at": { + "destination": 141, + "phase": 1, + "record_in_direction": 26356 + } + } + }, + "candidate": { + "adds_by_phase": { + "1": 19922, + "2": 2376, + "3": 568, + "4": 1065, + "5": 2961 + }, + "five_stage_payload_bits": 100, + "five_stage_payload_bound": "962930826045767086638403792896", + "forward": { + "all_columns": 660, + "bits": 18, + "cancellation_free_row_l1": 144651, + "maximum_at": { + "destination": 528, + "phase": 5, + "record_in_direction": 29512 + } + }, + "negative_controls": { + "broken_COPY_source": "ERASE source frame or workspace mismatch", + "missing_ERASE": "copy workspace already open", + "modified_MOVE_rank": "MOVE rank mismatch", + "omitted_B_source_ADD": "scalar endpoint mismatch" + }, + "nine_stage_charged_prefix_bits": 192, + "nine_stage_prefix_bits": 189, + "nine_stage_prefix_bound": "410250116818741208821899034315310017378193525612293914624", + "operations": { + "0": 2940, + "1": 26892, + "2": 9, + "3": 9 + }, + "paid_histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "paid_rank_mass": 5112, + "records": 29850, + "reverse": { + "all_columns": 660, + "bits": 22, + "cancellation_free_row_l1": 2229592, + "maximum_at": { + "destination": 141, + "phase": 1, + "record_in_direction": 26332 + } + } + }, + "formula_and_exporter_sources": { + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + "same_frame_paths": true, + "status": "PASS_LOCAL_SCALAR_PROFILE_AND_PREFIX_AUDIT" + }, + "full_word_checks": { + "H1_H5_and_conclusion": true, + "closed_frames": 672, + "columns": 660 + }, + "integer_forward_matrix": [ + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 1 + ], + [ + 0, + 0, + 3, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 2 + ], + [ + 1, + 1, + 3, + 2, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 3, + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 2, + 1, + 2, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1, + 1, + 1, + 2, + 1, + 1, + 1 + ], + [ + 1, + 1, + 2, + 2, + 1, + 1, + 1, + 1, + 1, + 2, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + "negative_controls": [ + "omit block gate", + "change block source", + "parity-preserving duplicated pair", + "omit cleanup gate", + "block gate at zero frame", + "stale cleanup violates literal-reverse interface" + ], + "registers": [ + 19, + 24, + 35, + 40, + 54, + 56, + 65, + 74, + 84, + 95, + 100, + 111 + ], + "replacement_ops": [ + [ + 40, + 35 + ], + [ + 100, + 95 + ], + [ + 100, + 19 + ], + [ + 100, + 84 + ], + [ + 100, + 40 + ], + [ + 100, + 24 + ], + [ + 65, + 54 + ], + [ + 56, + 65 + ], + [ + 74, + 56 + ], + [ + 95, + 40 + ], + [ + 95, + 111 + ], + [ + 19, + 111 + ], + [ + 19, + 24 + ], + [ + 84, + 111 + ], + [ + 84, + 35 + ], + [ + 35, + 74 + ], + [ + 35, + 95 + ], + [ + 35, + 84 + ], + [ + 111, + 100 + ], + [ + 54, + 74 + ], + [ + 54, + 111 + ], + [ + 54, + 56 + ], + [ + 65, + 111 + ], + [ + 65, + 56 + ], + [ + 24, + 74 + ], + [ + 24, + 95 + ], + [ + 56, + 111 + ], + [ + 111, + 74 + ], + [ + 74, + 100 + ], + [ + 40, + 74 + ], + [ + 40, + 84 + ], + [ + 84, + 74 + ], + [ + 19, + 74 + ], + [ + 95, + 74 + ] + ], + "scope": "Finite block and native-word improvement; no new kappa, full hosting replay or full theorem proof", + "source_B_slice": [ + 371, + 417 + ], + "source_offsets": [ + 16, + 0, + 1, + 2, + 3, + 4, + 19, + 17, + 6, + 9, + 10, + 12, + 13, + 14, + 15, + 20, + 21, + 22, + 34, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 33, + 35, + 45, + 37, + 38, + 40, + 42, + 44 + ], + "status": "PASS_R420_BLOCK5_RESYNTHESIS", + "steps": [ + { + "gates": 43, + "roundtrip_unit_peak": 1075 + }, + { + "gates": 39, + "roundtrip_unit_peak": 809 + }, + { + "gates": 37, + "roundtrip_unit_peak": 809 + }, + { + "gates": 36, + "roundtrip_unit_peak": 809 + }, + { + "gates": 34, + "roundtrip_unit_peak": 485 + } + ], + "strict_reverse_entries": 28 +} diff --git a/research/r420-block5-resynthesis/record_audit.py b/research/r420-block5-resynthesis/record_audit.py new file mode 100644 index 0000000000..f49306fdf5 --- /dev/null +++ b/research/r420-block5-resynthesis/record_audit.py @@ -0,0 +1,178 @@ +"""Replay stock records on every scalar column and count paid moves and prefix bounds. + +This audit checks one local R420 word in both directions. It does not run a +global hosting or price pipeline. Output receipts omit paths and timing. + +Prepared for x0hu with substantial OpenAI Codex assistance; Apache-2.0. +""" +import argparse +import hashlib +import json +from pathlib import Path +import struct +import subprocess +import sys +from collections import Counter + +ROOT = Path(__file__).resolve().parents[2] +EXPORTER = ROOT / "research/e8-bit-carrier-skeleton/code/bit/export_records.py" +FIVE_FORMULA = ROOT / "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp" +NINE_FORMULA = ROOT / ("research/e8-bit-r420/vendor/pr510/e8-r480-nine-stage/" + "vendor/e8-r715-eleven-stage-whole/code/global_k.py") + + +class Reject(ValueError): + """A record violates the checked local contract.""" + + +def require(condition, message): + if not condition: + raise Reject(message) + + +def replay(records, states, frames, reverse=False): + """Replay MOVE/ADD/COPY/ERASE records, including arbitrary helper dirt.""" + n, v, h = states["n"], states["v"], states["h"] + require((n, v, h, states["R"]) == (660, 120, 8, 420), "wrong R420 header") + dim = {int(k): x["dim"] for k, x in frames.items()} + src, dest = ("final", "initial") if reverse else ("initial", "final") + cur = [states[src][str(i)] for i in range(n)] + [-1] + vals = [1 << i for i in range(n)] + [0] + norm = [1] * n + [0] + maximum, maximum_at, center = 1, None, None + hist, counts = Counter(), Counter() + for index, row in enumerate(reversed(records) if reverse else records): + require(len(row) == 6, "malformed record") + op, x, y, c, f, z = row + require(op in (0, 1, 2, 3) and 0 <= x < n, "invalid operation or destination") + counts[op] += 1 + if op == 0: + old, new = (c, y) if reverse else (y, c) + require(old in dim and new in dim, "unknown MOVE frame") + require(cur[x] == old, "MOVE source frame mismatch") + rank = dim[old] - dim[new] if reverse else dim[new] - dim[old] + require(rank == f and f > 0, "MOVE rank mismatch") + lo, hi = (new, old) if reverse else (old, new) + require(all(sum(a*b for a, b in zip(ann, basis)) == 0 + for ann in frames[str(hi)]["A"] for basis in frames[str(lo)]["B"]), + "MOVE frames not nested") + cur[x] = new + hist[f] += 1 + elif op == 1: + require(0 <= y <= n and x != y and f in dim, "invalid ADD operands") + require(cur[x] == cur[y] == f, "ADD frame mismatch") + require(center is None or x != center, "copied center modified") + require(y != n or center is not None, "ADD reads closed copy workspace") + if c & 1: + vals[x] ^= vals[y] + norm[x] += abs(c) * norm[y] + if norm[x] > maximum: + maximum = norm[x] + maximum_at = dict(record_in_direction=index, destination=x, phase=z) + elif op == (3 if reverse else 2): + require(center is None, "copy workspace already open") + require(y == n and c in dim and f in dim and cur[x] == c and vals[n] == 0, + "COPY source frame or workspace mismatch") + rank = abs(dim[c] - dim[f]) + require(rank == 8 and z == (0 if reverse else rank), "COPY rank mismatch") + center, cur[n], vals[n], norm[n] = x, f, vals[x], norm[x] + hist[rank] += 1 + else: + require(op == (2 if reverse else 3), "unexpected operation") + require(center == x and y == n and cur[x] == c and cur[n] == f, + "ERASE source frame or workspace mismatch") + require(z == (8 if reverse else 0), "ERASE rank field mismatch") + require(vals[n] == vals[x], "ERASE copy contents mismatch") + center, cur[n], vals[n], norm[n] = None, -1, 0, 0 + require(center is None and vals[n] == 0, "copy workspace not closed") + require(counts[2] == counts[3] == len(states["retained_totals"]) == 9, "COPY/ERASE count mismatch") + require(cur[:n] == [states[dest][str(i)] for i in range(n)], "final frames mismatch") + require(all(vals[i] == ((1 << i) ^ ((1 << (i-v)) if v <= i < 2*v else 0)) + for i in range(n)), "scalar endpoint mismatch") + return dict(cancellation_free_row_l1=maximum, bits=maximum.bit_length(), + maximum_at=maximum_at, all_columns=n, paid_histogram=dict(sorted(hist.items()))) + + +def negative_controls(records, states, frames): + """Four mutations exercise scalar, move-rank and copy lifecycle checks.""" + add = next(i for i, r in enumerate(records) if r[0] == 1 and r[5] == 4 and r[1] < 120) + move = next(i for i, r in enumerate(records) if r[0] == 0) + copy = next(i for i, r in enumerate(records) if r[0] == 2) + erase = next(i for i, r in enumerate(records) if r[0] == 3) + bad_rank = list(records[move]); bad_rank[4] += 1 + bad_copy = list(records[copy]); bad_copy[1] = (bad_copy[1] + 1) % states["n"] + mutants = { + "omitted_B_source_ADD": records[:add] + records[add+1:], + "modified_MOVE_rank": records[:move] + [bad_rank] + records[move+1:], + "broken_COPY_source": records[:copy] + [bad_copy] + records[copy+1:], + "missing_ERASE": records[:erase] + records[erase+1:], + } + rejected = {} + for name, mutant in mutants.items(): + try: + replay(mutant, states, frames) + replay(mutant, states, frames, reverse=True) + except Reject as error: + rejected[name] = str(error) + else: + raise Reject("negative control accepted: " + name) + return rejected + + +def audit(word_path, output_path): + output_path.mkdir(parents=True, exist_ok=True) + # -I ignores PYTHONOPTIMIZE and PYTHONPATH; stock exporter assertions stay on. + subprocess.run([sys.executable, "-I", "-B", str(EXPORTER), str(word_path), str(output_path)], + check=True, stdout=subprocess.DEVNULL) + records = list(struct.iter_unpack("<6i", (output_path / "249-records.bin").read_bytes())) + states = json.loads((output_path / "249-states.json").read_text()) + frames = json.loads((output_path / "frames.json").read_text())["frames"] + forward = replay(records, states, frames) + reverse = replay(records, states, frames, reverse=True) + require(forward["paid_histogram"] == reverse["paid_histogram"], "direction profiles differ") + histogram = forward.pop("paid_histogram") + reverse.pop("paid_histogram") + cf, cb = forward["cancellation_free_row_l1"], reverse["cancellation_free_row_l1"] + # columns_h.cpp: payload = 64 * F^3 * B^2. + five = 64 * cf**3 * cb**2 + require(five < 2**104, "five-stage payload exceeds inherited bound") + # global_k.py with K=4: nb=6*(K-1)=18, prefix=2^nb*F^(K+1)*B^K. + nine = 2**18 * cf**5 * cb**4 + paths = {str(i): [states["initial"][str(i)]] for i in range(states["n"])} + for op, x, y, c, f, z in records: + if op == 0: + paths[str(x)].append(c) + result = dict(records=len(records), + operations=dict(sorted(Counter(r[0] for r in records).items())), + adds_by_phase=dict(sorted(Counter(r[5] for r in records if r[0] == 1).items())), + forward=forward, reverse=reverse, paid_histogram=histogram, + paid_rank_mass=sum(r*z for r, z in histogram.items()), + five_stage_payload_bound=str(five), five_stage_payload_bits=five.bit_length(), + nine_stage_prefix_bound=str(nine), nine_stage_prefix_bits=nine.bit_length(), + nine_stage_charged_prefix_bits=max(192, 64*((nine.bit_length()+63)//64)), + negative_controls=negative_controls(records, states, frames)) + return result, paths + + +def compare(baseline_path, candidate_path, output_path): + """Write exported records and receipt.json below output_path; return receipt.""" + output_path = Path(output_path) + base, base_paths = audit(Path(baseline_path), output_path / "baseline-records") + candidate, candidate_paths = audit(Path(candidate_path), output_path / "candidate-records") + require(base_paths == candidate_paths, "register frame paths changed") + require(base["paid_histogram"] == candidate["paid_histogram"], "paid histogram changed") + sources = {path.relative_to(ROOT).as_posix(): hashlib.sha256(path.read_bytes()).hexdigest() + for path in (EXPORTER, FIVE_FORMULA, NINE_FORMULA)} + receipt = dict(status="PASS_LOCAL_SCALAR_PROFILE_AND_PREFIX_AUDIT", same_frame_paths=True, + formula_and_exporter_sources=sources, baseline=base, candidate=candidate) + (output_path / "receipt.json").write_text(json.dumps(receipt, indent=2) + "\n") + return receipt + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("baseline", type=Path) + parser.add_argument("candidate", type=Path) + parser.add_argument("output", type=Path) + args = parser.parse_args() + print(json.dumps(compare(args.baseline, args.candidate, args.output), indent=2)) diff --git a/research/r420-block5-resynthesis/verify.py b/research/r420-block5-resynthesis/verify.py new file mode 100644 index 0000000000..3723393eed --- /dev/null +++ b/research/r420-block5-resynthesis/verify.py @@ -0,0 +1,188 @@ +"""Rebuild and check one fixed-output R420 block rewrite. Standard library only. + +Prepared for x0hu with substantial OpenAI Codex assistance; Apache-2.0. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import sys +import tempfile + +import record_audit + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +CHECKER = "research/e8-bit-r420/code/xcheck.py" +START, STOP, FRAME = 371, 417, 547 +REGISTERS = [19, 24, 35, 40, 54, 56, 65, 74, 84, 95, 100, 111] +# Each move advances dst += src before a reader, removing the now-redundant +# direct additions of src to that reader. Outputs stay on the original wires. +STEPS = [ + ((111, 100), (54, 100), [(54, 100), (65, 100), (56, 100)]), + ((74, 100), (40, 100), [(40, 100), (84, 100), (19, 100), (95, 100)]), + ((65, 54), (74, 56), [(74, 54), (56, 54)]), + ((56, 65), (74, 56), [(74, 65)]), + ((40, 35), (100, 95), [(100, 35), (95, 35)]), +] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def transfer(ops, sign=1): + """Exact integer matrix, so positive bounds and signed inverses are checked.""" + n = len(REGISTERS) + index = {r: i for i, r in enumerate(REGISTERS)} + rows = [[int(i == j) for j in range(n)] for i in range(n)] + for dst, src in ops: + require(dst in index and src in index and dst != src, "invalid block operands") + d, s = index[dst], index[src] + rows[d] = [x + sign * y for x, y in zip(rows[d], rows[s])] + return rows + + +def dominates(before, after): + return all(y <= x for a, b in zip(before, after) for x, y in zip(a, b)) + + +def improvement(before, after): + require(transfer(before) == transfer(after), "integer forward transfer changed") + require(transfer(before[::-1], -1) == transfer(after[::-1], -1), + "signed inverse transfer changed") + require(dominates(transfer(before[::-1]), transfer(after[::-1])), + "reverse cancellation-free transfer increased") + + +def rebuild(word): + block = word["B"][START:STOP] + require(len(block) == 46 and all(f == FRAME and len(s) == 1 for f, d, s in block), + "unexpected block boundaries") + before = [(d, s[0]) for f, d, s in block] + require(sorted({r for op in before for r in op}) == REGISTERS, "block wires changed") + ops, stages = list(before), [] + for gate, anchor, removed in STEPS: + previous = list(ops) + ops.remove(gate) + ops.insert(ops.index(anchor), gate) + for op in removed: + ops.remove(op) + improvement(previous, ops) + stages.append({"gates": len(ops), "roundtrip_unit_peak": + max(map(sum, transfer(ops + ops[::-1])))}) + improvement(before, ops) + require(len(ops) == 34, "unexpected rewritten length") + candidate = copy.deepcopy(word) + candidate["B"][START:STOP] = [[FRAME, d, [s]] for d, s in ops] + candidate["C"] = [[1, d, srcs] for _, d, srcs in reversed(candidate["A"] + candidate["B"]) + if not 120 <= d < 240] + return candidate, before, ops, stages + + +def must_reject(name, callback, catches=(ValueError,)): + try: + callback() + except catches: + return name + raise ValueError("negative control accepted: " + name) + + +def run(output): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for path, sha in sources["sha256"].items(): + require(digest((ROOT / path).read_bytes()) == sha, "source pin mismatch: " + path) + baseline = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + candidate, before, after, stages = rebuild(baseline) + spec = importlib.util.spec_from_file_location("r420_original_xcheck", ROOT / CHECKER) + checker = importlib.util.module_from_spec(spec) + spec.loader.exec_module(checker) + for word in (baseline, candidate): + _, labels, full, hypotheses, conclusion, _ = checker.check(word) + require(all(hypotheses.values()) and all(conclusion.values()), "interface failure") + require(full["columns"] == 660 and labels["frames"] == 672, "coverage changed") + output.mkdir(parents=True, exist_ok=True) + path = output / "candidate.json.gz" + # Canonical decompressed bytes, not the platform's gzip header, identify the word. + with path.open("wb") as stream: + with gzip.GzipFile(fileobj=stream, mode="wb", filename="", mtime=0) as compressed: + compressed.write(canonical(candidate)) + cost = record_audit.compare(ROOT / WORD, path, output / "records") + controls = [] + controls.append(must_reject("omit block gate", lambda: improvement(before, after[1:]))) + wrong = list(after) + wrong[0] = (40, 19) + controls.append(must_reject("change block source", lambda: improvement(before, wrong))) + doubled = after + [after[0], after[0]] + require([[x % 2 for x in row] for row in transfer(doubled)] == + [[x % 2 for x in row] for row in transfer(after)], "invalid parity-only control") + controls.append(must_reject("parity-preserving duplicated pair", lambda: improvement(before, doubled))) + bad_cleanup = copy.deepcopy(candidate) + bad_cleanup["C"].pop() + controls.append(must_reject("omit cleanup gate", lambda: checker.check(bad_cleanup), (checker.Reject,))) + bad_frame = copy.deepcopy(candidate) + bad_frame["B"][START][0] = 0 + controls.append(must_reject("block gate at zero frame", lambda: checker.check(bad_frame), (checker.Reject,))) + # Check that the original cleanup cannot be reused after the rewrite. + stale = copy.deepcopy(candidate) + stale["C"] = baseline["C"] + stale_hypotheses = checker.Word(stale).interface()[0] + require(not stale_hypotheses["H4_C_literal_reverse_at_full"], "stale cleanup passed H4") + controls.append("stale cleanup violates literal-reverse interface") + old_reverse, new_reverse = transfer(before[::-1]), transfer(after[::-1]) + result = { + "status": "PASS_R420_BLOCK5_RESYNTHESIS", + "base_commit": sources["base_commit"], + "registers": REGISTERS, + "source_B_slice": [START, STOP], + "source_offsets": [before.index(op) for op in after], + "replacement_ops": after, + "steps": stages, + "integer_forward_matrix": transfer(after), + "baseline_reverse_majorant": old_reverse, + "candidate_reverse_majorant": new_reverse, + "strict_reverse_entries": sum(y < x for a, b in zip(old_reverse, new_reverse) for x, y in zip(a, b)), + "baseline_local_roundtrip_peak": max(map(sum, transfer(before + before[::-1]))), + "candidate_local_roundtrip_peak": max(map(sum, transfer(after + after[::-1]))), + "candidate_canonical_sha256": digest(canonical(candidate)), + "full_word_checks": {"columns": 660, "closed_frames": 672, "H1_H5_and_conclusion": True}, + "cost": cost, + "negative_controls": controls, + "scope": "Finite block and native-word improvement; no new kappa, full hosting replay or full theorem proof", + } + # Normalize JSON object keys and tuple/list representations before comparison. + return json.loads(canonical(result)) + + +def main(): + if not __debug__: + raise SystemExit("REJECT: run without -O; inherited checkers use assertions") + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="directory for candidate and replay records") + parser.add_argument("--write-certificate", action="store_true", help="regenerate the committed exact certificate") + args = parser.parse_args() + with tempfile.TemporaryDirectory(prefix="r420-block5-") as scratch: + result = run(args.output if args.output else Path(scratch)) + cert = HERE / "certificate.json" + if args.write_certificate: + cert.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + expected = json.loads(cert.read_text()) + require(result == expected, "certificate mismatch") + print("PASS_R420_BLOCK5_RESYNTHESIS block=46->34 native_adds=26916->26892 rank_mass=5112 kappa=unchanged") + + +if __name__ == "__main__": + main()