diff --git a/research/r420-frame-zero-pair/CLAIM.json b/research/r420-frame-zero-pair/CLAIM.json new file mode 100644 index 0000000000..ecf112d21d --- /dev/null +++ b/research/r420-frame-zero-pair/CLAIM.json @@ -0,0 +1,35 @@ +{ + "track": "Bit supplier", + "assignment_seed": 1, + "seed_source": "Python secrets.randbelow(100), backed by operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "claimed_at_utc": "2026-10-13T03:48:00Z", + "expected_finish_utc": "2026-10-13T04:23:00Z", + "planned_verification_no_later_than_utc": "2026-10-13T04:13:00Z", + "actual_verification_started_at_utc": "2026-10-13T03:56:30Z", + "coordination": "GitHub pinnedIssues was empty; the only open issue was #650 (Discussions). Local claim used as requested.", + "candidates": [ + "Resynthesize the seed-selected R420 phase-B block 1; rejected as too close to concurrent #670 and #674 block resynthesis.", + "Optimize a fixed-order R420 phase-B frame schedule; rejected because #661 already closes this search class.", + "Factor one pair of dirty helper columns in R420's frame-zero compensation, including preparation, restoration and both positive prefix bills. Selected." + ], + "object": "PR543 R420 D compensation; single restored helper-pair factorization at frame zero", + "method": "Count all 87990 unordered pairs of 420 helper columns. Select maximum shared support, lexicographic tie break. Assignment seed parity chooses the initial orientation. Test both orientations' exact positive prefix bills. No wider search.", + "optimistic_budget": "For q shared target rows: 2q direct XORs become q+2 XORs, including two helper preparation/restoration gates. No new helpers, moves, copies, or recursive children. At q=110 the saving is 108 XORs. The paid movement profile and complex bottleneck cannot improve from this alone.", + "expected_deliverable": "Standalone finite circuit recipe, exact dirty-input and record replay, meaningful mutation controls, prefix accounting, and a scoped proof of the generalized D interface. No new kappa claim.", + "overlap_snapshot": { + "670": "2e31fcad7f9ecc8b97039ecb2333e581fd725fa1", + "674": "1b01fd8b135fb2c458554fbbbab4338336bf366d", + "661": "9ca7aa3ab0a3260a2f36ac86b9911a31fd88bd89", + "612": "ce37f3ce35ba8891771e01492b3a21978763bebb" + }, + "status": "completed: finite circuit improvement, no new kappa", + "result_update_at_utc": "2026-10-13T04:05:35Z", + "result": { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/686", + "summary": "Single restored helper pair saves 108 binary XORs: D 19922->19814, complete native word 26916->26808. No additional frame changes, copies, helpers or local recursive children; both native prefix maxima unchanged.", + "completed_coverage": "87990/87990 unordered pairs by two methods; both orientations; all 660 native columns and 1380 nine-stage columns; six D controls, 18 bridge controls per word and an F2-neutral prefix-inflation rejection.", + "handoff": "README.md, SOURCES.json, certificate.json, VALIDATION.json and one-command verify.py; generalized D interface and remaining hosting/all-size obligations explicitly documented.", + "final_overlap_refresh": "Open PR metadata refreshed through #685; no frame-zero R420 pair construction found. #670/#674 modify B; #661 holds D fixed; #673/#677 use different dirty primitives. Main remained at the exact base and no pinned issue existed." + } +} diff --git a/research/r420-frame-zero-pair/README.md b/research/r420-frame-zero-pair/README.md new file mode 100644 index 0000000000..856596568a --- /dev/null +++ b/research/r420-frame-zero-pair/README.md @@ -0,0 +1,195 @@ +# R420: share one dirty-helper pair at frame zero + +This finite bit-circuit contribution saves **108 binary XOR operations** in +eumemic's PR543 R420 word. Its frame-zero dirt compensation goes from 19,922 +to 19,814 scalar ADDs; the complete native word goes from **26,916 to 26,808**. +Both dirty helpers are restored before phase A. The nine-stage formal-column +replay, frame paths, copied information and measured native prefix bill pass. +**No new kappa or completed hosted supplier is claimed.** + +The base is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. At that base the +selected composition is PR626 with PR543, conditional +`kappa = 51110230636731/31250000000000000 = 0.001635527380375392`, and its complex +supplier binds. These facts come from the selected certificate, its actual +`research/community-k492-audit/pr626/replay/ASSEMBLY.json`, and the +[maintainer review](../../docs/research/community-k492-review.md). +The R420 README's older frontier discussion is historical. + +## Reproduce + +From the repository root, with Python 3.11+, a C++17 compiler and Boost headers: + +```sh +python3 -B research/r420-frame-zero-pair/verify.py +``` + +Expected last line: + +```text +PASS_R420_FRAME_ZERO_PAIR D=19922->19814 native_adds=26916->26808 columns=660 kappa=unchanged +``` + +Python uses only the standard library. `CXX` selects a compiler; `BOOST_INCLUDE` +can name a nonstandard Boost include directory. The command checks all source +pins, regenerates the circuit and records, compiles the unchanged predecessor +checkers, runs the controls and compares every certificate field. It uses a +temporary directory. To retain the generated word, raw records, C++ receipts, +compile logs and certificate, append `--output /absolute/new/directory`. +An existing output directory is rejected. + +Only this research directory is added. The selected frontier, predecessor +packages and `upstream/` are unchanged. The recipe is implemented in `factor` +in [verify.py](verify.py); its exact output has canonical JSON SHA-256 +`358eca016e0e1ef48267dcd7ff33d4d36c27ecc3f38fffbdceb4c924e2254349`. +[SOURCES.json](SOURCES.json) pins every imported or executed predecessor file. +[certificate.json](certificate.json) records the complete census, target list, +both orientations, accounting and controls. + +## The circuit and complete local cost + +Write `a = helper 552`, `b = helper 521`. Let T be the 110 targets whose original +D row contains both a and b. Target register IDs are 120 through 239, except +153, 161, 174, 182, 185, 193, 206, 214, 222 and 230. All operations below occur +at frame zero: + +1. Execute each original D row, omitting a and b only for rows in T. +2. Execute `a ^= b`. +3. Execute `y_t ^= a` once for each target in T. +4. Execute `a ^= b` to restore the original dirty value of a. + +No source register is accessed. For arbitrary initial values alpha and beta, +the middle register contains `alpha XOR beta`, each selected target receives +exactly its omitted two terms, and a ends as alpha. Register b is read only. +All other helper and target terms are unchanged. Thus the D map is exactly +the original map on **all input columns**, including arbitrary helper dirt and +arbitrary target inputs. Reordering the residual target-only gates is valid: +they commute, read unchanged helpers, and cannot change a or b. + +For a pair shared by q target rows, `2q` target XORs are replaced by `q+2` +XORs, including preparation and restoration. Here q=110, so the saving is 108. +The JSON D list grows from 120 grouped gates to 232 grouped gates; every source +term is still counted as a separate binary ADD. The result is not obtained by +pricing a many-source gate as a single operation. + +| Complete native quantity | Original | Candidate | +| --- | ---: | ---: | +| D scalar ADDs | 19,922 | 19,814 | +| All scalar ADDs | 26,916 | 26,808 | +| All emitted records | 29,874 | 29,766 | +| Helpers | 420 | 420 | +| Retained copies | 9 | 9 | +| Paid rank mass | 5,112 | 5,112 | +| Forward positive prefix | 144,651 | 144,651 | +| Reverse positive prefix | 2,270,064 | 2,270,064 | +| Five-stage payload bits | 100 | 100 | + +The entire MOVE/COPY/ERASE subsequence is identical, as are A, scatter, B, C, +boundary frames, labels and retained registers. There are no additional +frame changes, copies, helper allocations or local recursive children. +The paid histogram remains `{1:1320, 2:1440, 4:60, 5:120, 8:9}`. In the +nine-stage scalar replay the local saving is repeated nine times: 972 fewer +ADDs; the 2,160 bridge ADDs and 81 fresh center copies are unchanged. + +F2 equality alone does **not** imply equality of positive prefix bounds. The +restoration gate increases the unsigned helper bound even though it cancels +over F2. We explicitly replay both signed orientations with nonnegative +integer bounds, independently in Python and in the pinned C++ checker. The +unchanged payload is exactly +`64 * 144651^3 * 2270064^2 = 998206739997057013039187410944 < 2^104`. +Neither entrywise domination of every intermediate positive map nor an +integer-ring endpoint identity for the all-positive XOR stream is asserted. + +## The changed interface obligation + +PR543's literal H2 requires every D gate to write a target and read helpers. +This candidate deliberately fails that syntactic condition, since two D gates +write helper a. The original checker's `K_equals_D` calculation also assumes +literal helper reads, so it is inapplicable to the compressed circuit. +Neither check is silently weakened in the predecessor package. + +Replace H2 by the following sufficient condition, keeping H1 and H3--H5: + +> D uses only target/helper registers at frame zero, reads only helpers, and +> has aggregate map `(x,s,y) -> (x,s,y+Ns)`; in particular every helper is +> restored before A starts. + +The original block-triangular proof then applies verbatim at the boundary: +the raw A/scatter/B map is `(z,y) -> (Uz,y+Jx+Ks)` with z=(x,s), and C applies +`U^-1` to z. Composing after D gives +`(x,s,y) -> (x,s,y+Jx+(K+N)s)`. Here the unchanged raw word has J=I and the +new D has exactly the old N=K, so the final map is `(x,s,y+x)` over F2. +The two new helper gates are legal at frame zero, where helpers initially +stand. They restore before any climb, so no extra gate belongs in C and no +descent is hidden. This is a written finite-interface argument, not Lean. + +The verifier first evaluates the new D with a separate set-valued symbolic +interpreter and requires its complete map to equal the pinned original D. +It then runs PR543's exact labels, closed frames and 660-column native replay +on the actual candidate. For the inherited interface it checks that exactly +the documented H2 and syntactic K checks fail. Replacing only D by its proven +equivalent original normal form restores all H1--H5 and conclusion checks. +The unmodified C++ record checkers additionally accept actual candidate +geometry and all 1,380 columns across nine stages, including arbitrary dirt. + +## Search scope, controls and remaining work + +OS randomness supplied assignment seed **1**, selecting the bit-supplier +track. Its parity selects the orientation `552 ^= 521`; the opposite +orientation was also checked and has the same costs and prefix maxima. +The search stops after all `binomial(420,2) = 87,990` unordered helper pairs. +Two methods agree for every pair: count pair occurrences in rows, and +intersect column-incidence bitsets. Their complete histogram has a unique +maximum q=110 at `{521,552}`. Consequently 108 is the largest saving within +this **single-pair recipe with two helper updates on this fixed D matrix**. +This does not establish optimality among general XOR circuits, multiple-pair +factorizations, changed frames, changed words or supplier assemblies. + +Six D controls reject an omitted restoration, an omitted shared read, a wrong +restoration source, an F2-correct read at a nonzero frame, an F2-neutral pair +of target-to-helper reads, and an F2-neutral pair of source reads at frame +zero. A harmless adjacent pair of helper updates is a positive control. An +additional F2-neutral record preamble preserves every endpoint column but +exceeds the positive-prefix limit, and the actual C++ bill check rejects it. +Both baseline and candidate also reject all 18 omitted-bridge controls. + +This package completes the finite native circuit and nine-stage cohort +checks. Integration would still need review of the generalized D interface +in the all-size/common-label realization and a fresh hosted-parent replay, +invoice and outer assembly. Equal local frame paths and prefix maxima alone +do not certify those obligations. The selected assembly is already complex +limited; this scalar-work saving does not alter its paid local moment or +establish a better kappa. Whole-call pooled-cell hosting, normalized residuals, +mutable-basis realization, precision, fixed-tape and analytic assumptions are +inherited. No practical runtime speedup or full multiplication theorem is +asserted. + +## Relation to concurrent work and attribution + +The local [claim](CLAIM.json) records three candidates and the overlap check. +No pinned sprint issue existed. PR670 (yongjae321) resynthesizes phase-B block +3; PR674 (x0hu) resynthesizes block 5. This contribution changes D and uses +temporary helper sharing followed by restoration, adding distinct coverage. +Their changes are not imported and composition with them is not tested. +PR661's exact frame bound fixes D and the scalar gate order and explicitly +excludes resynthesis. This task changes that excluded circuit structure. +PR612's original R420 Lean boundaries do not prove this changed D interface. +PR589's punctured-word transport search is separate. +The final refresh through PR685 also checked PR673's multiway cyclic-inverse +dirty echo and PR677's native ADDRESS/DATA interface: both change different +primitives. Neither is a dependency, and no novelty of the general reversible +prepare/share/restore trick is claimed. The new evidence here is its concrete, +fully costed R420 compensation instance and changed D interface. + +Credit remains with **eumemic** for PR543's R420 construction, interleaved +interface, independent checker and PR493 carrier skeleton; **Dylan Crow** for +the bit word format and exporter; **DaysSky** for the bridged-stage checker +and hosting lineage; **Chafik Boukhalfa** for the inherited geometric checker +and invoice lineage; **Zhihao Chen** for the mutable-basis/interface lineage; +**DreamingOfClouds** for the retained-total and nine-stage bit work; and the +cumulative authors named in those packages and the repository contributor +record. Their original notices and bytes are unchanged. + +Prepared by **Mikhail R. Gadelha (@mikhailramalho)** with substantial **OpenAI +Codex assistance**, including investigation, implementation, proof drafting +and verification. No independent human review is claimed. New files follow +the repository's **Apache-2.0** license. diff --git a/research/r420-frame-zero-pair/SOURCES.json b/research/r420-frame-zero-pair/SOURCES.json new file mode 100644 index 0000000000..c4c7773445 --- /dev/null +++ b/research/r420-frame-zero-pair/SOURCES.json @@ -0,0 +1,33 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "PR543_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "selected_at_base": { + "kappa": "51110230636731/31250000000000000", + "decimal": "0.001635527380375392", + "composition": "PR626 with PR543", + "binding": "complex", + "record": "certificates/selected-result.json", + "review": "docs/research/community-k492-review.md", + "actual_certificate": "research/community-k492-audit/pr626/replay/ASSEMBLY.json" + }, + "sha256": { + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "research/e8-bit-r420/code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", + "research/e8-bit-r420/code/gen_l3.py": "d5c802447c99255db1bdfcae62b2116bfc9612c9dc9000d41aa4f5f2fec9f2f2", + "research/e8-bit-r420/README.md": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a" + }, + "attribution": { + "PR543_PR493": "eumemic: R420 construction, generator, interleaved interface, exact word checker and mutable-source carrier skeleton", + "PR370": "Dylan Crow: bit word format and record exporter", + "PR266_PR346_PR352": "Inherited common-frame legality and formal-column checking lineage, as retained in PR493", + "PR363_PR381": "DaysSky: general bridged-stage replay in columns_k.cpp", + "PR425_PR472_PR535": "Zhihao Chen and cumulative contributors: scalar interface and common-label realization carried by the PR543 proof", + "PR510_PR589": "DreamingOfClouds: nine-stage bit pricing and later punctured-bit headroom; context only, not replayed here", + "contribution": "Mikhail R. Gadelha (@mikhailramalho), with substantial OpenAI Codex assistance; Apache-2.0" + } +} diff --git a/research/r420-frame-zero-pair/VALIDATION.json b/research/r420-frame-zero-pair/VALIDATION.json new file mode 100644 index 0000000000..30a8f3bbe7 --- /dev/null +++ b/research/r420-frame-zero-pair/VALIDATION.json @@ -0,0 +1,56 @@ +{ + "status": "passed local finite verification", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "environment": { + "os": "Linux 6.17.0-41-generic x86_64 GNU/Linux", + "python": "3.13.7", + "cxx": "Ubuntu GCC 15.2.0-4ubuntu4", + "boost": "1.88" + }, + "commands": [ + { + "command": "python3 -B research/r420-frame-zero-pair/verify.py", + "result": "PASS_R420_FRAME_ZERO_PAIR D=19922->19814 native_adds=26916->26808 columns=660 kappa=unchanged" + }, + { + "command": "python3 -O -B research/r420-frame-zero-pair/verify.py --output /tmp/r420-frame-zero-pair-optimized", + "result": "Same complete certificate; optimized execution preserves all checks" + }, + { + "command": "python3 -B research/r420-frame-zero-pair/verify.py --output /tmp/r420-frame-zero-pair-optimized", + "result": "Expected FileExistsError before any output overwrite" + }, + { + "command": "make selected-record-check", + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000" + }, + { + "command": "python3 -I -B research/r420-frame-zero-pair/verify.py (from a fresh Git archive containing only this package and its nine pinned source files)", + "result": "Same PASS and complete certificate; no unlisted local dependency required" + }, + { + "command": "git diff --cached --check", + "result": "Passed; only new files in research/r420-frame-zero-pair are included" + } + ], + "coverage": [ + "All 87990 unordered helper pairs by row-pair counts and independent column-incidence intersections", + "Exact set-valued compensation map on arbitrary input dirt and targets", + "Pinned E8 labels, all closed frames and 660-column native candidate replay", + "Documented legacy H2 and K rejection; exact D normalization restores the original interface", + "Independent Python forward/reverse raw-record interpretation and positive prefix bill for both pair orientations", + "Unmodified C++ chronological geometry checker and 1380-column nine-stage checker on baseline and candidate", + "Six D rejection controls, a positive D control, 18 omitted-bridge controls per word and a bill-inflation control with exact F2 endpoint preservation", + "Complete regenerated certificate comparison, with the large integer payload stored as an exact decimal string" + ], + "not_run": [ + "Full hosted-parent reconstruction and invoice", + "Outer assembly for the changed word", + "Repository-wide regenerating make verify", + "Lean formalization", + "Remote CI" + ], + "remaining_obligations": "Review generalized D interface under all-size/common-label realization; rebuild hosted parent and invoice before supplier integration. All inherited physical, precision, tape and analytic obligations remain.", + "assistance": "Substantial OpenAI Codex assistance; no independent human review claimed", + "result_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/686" +} diff --git a/research/r420-frame-zero-pair/certificate.json b/research/r420-frame-zero-pair/certificate.json new file mode 100644 index 0000000000..d7101253e7 --- /dev/null +++ b/research/r420-frame-zero-pair/certificate.json @@ -0,0 +1,306 @@ +{ + "status": "PASS_R420_FRAME_ZERO_PAIR", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 1, + "pair": [ + 552, + 521 + ], + "shared_targets": [ + 120, + 121, + 122, + 123, + 124, + 125, + 126, + 127, + 128, + 129, + 130, + 131, + 132, + 133, + 134, + 135, + 136, + 137, + 138, + 139, + 140, + 141, + 142, + 143, + 144, + 145, + 146, + 147, + 148, + 149, + 150, + 151, + 152, + 154, + 155, + 156, + 157, + 158, + 159, + 160, + 162, + 163, + 164, + 165, + 166, + 167, + 168, + 169, + 170, + 171, + 172, + 173, + 175, + 176, + 177, + 178, + 179, + 180, + 181, + 183, + 184, + 186, + 187, + 188, + 189, + 190, + 191, + 192, + 194, + 195, + 196, + 197, + 198, + 199, + 200, + 201, + 202, + 203, + 204, + 205, + 207, + 208, + 209, + 210, + 211, + 212, + 213, + 215, + 216, + 217, + 218, + 219, + 220, + 221, + 223, + 224, + 225, + 226, + 227, + 228, + 229, + 231, + 232, + 233, + 234, + 235, + 236, + 237, + 238, + 239 + ], + "domain_pairs": 87990, + "pair_support_histogram": { + "0": 3324, + "1": 863, + "2": 3770, + "3": 1291, + "4": 9746, + "5": 5958, + "6": 3981, + "7": 930, + "8": 2979, + "9": 1579, + "10": 2520, + "11": 653, + "12": 677, + "13": 184, + "14": 280, + "15": 90, + "16": 178, + "17": 171, + "18": 440, + "19": 423, + "20": 660, + "21": 642, + "22": 1481, + "23": 1914, + "24": 2628, + "25": 2018, + "26": 3032, + "27": 3659, + "28": 5287, + "29": 3479, + "30": 3769, + "31": 3335, + "32": 4270, + "33": 2493, + "34": 2138, + "35": 1282, + "36": 1692, + "37": 834, + "38": 716, + "39": 250, + "40": 305, + "41": 108, + "42": 133, + "43": 57, + "44": 135, + "45": 89, + "46": 201, + "47": 62, + "48": 88, + "49": 54, + "50": 114, + "51": 118, + "52": 197, + "53": 94, + "54": 151, + "55": 56, + "56": 64, + "57": 20, + "58": 53, + "59": 70, + "60": 86, + "61": 31, + "62": 35, + "63": 16, + "64": 16, + "65": 2, + "66": 2, + "67": 2, + "68": 1, + "69": 1, + "70": 2, + "71": 1, + "73": 2, + "78": 1, + "80": 1, + "99": 3, + "100": 2, + "110": 1 + }, + "D_adds_before": 19922, + "D_adds_after": 19814, + "candidate_content_sha256": "358eca016e0e1ef48267dcd7ff33d4d36c27ecc3f38fffbdceb4c924e2254349", + "input_content_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "native": { + "baseline": { + "records": 29874, + "scalar_adds": 26916, + "copies": 9, + "histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "forward_prefix": 144651, + "reverse_prefix": 2270064, + "payload": "998206739997057013039187410944", + "payload_bits": 100 + }, + "candidate": { + "records": 29766, + "scalar_adds": 26808, + "copies": 9, + "histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "forward_prefix": 144651, + "reverse_prefix": 2270064, + "payload": "998206739997057013039187410944", + "payload_bits": 100 + }, + "other_orientation": { + "records": 29766, + "scalar_adds": 26808, + "copies": 9, + "histogram": { + "1": 1320, + "2": 1440, + "4": 60, + "5": 120, + "8": 9 + }, + "rank_mass": 5112, + "forward_prefix": 144651, + "reverse_prefix": 2270064, + "payload": "998206739997057013039187410944", + "payload_bits": 100 + } + }, + "cohort": { + "baseline": { + "formal_columns": 1380, + "stages": 9, + "bridge_controls": 18, + "legality_status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "column_status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "candidate": { + "formal_columns": 1380, + "stages": 9, + "bridge_controls": 18, + "legality_status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "column_status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + }, + "mutation_controls": [ + { + "name": "omitted helper restoration", + "reason": "D map differs, including dirty-helper restoration" + }, + { + "name": "omitted shared target read", + "reason": "D map differs, including dirty-helper restoration" + }, + { + "name": "wrong restoration source", + "reason": "D map differs, including dirty-helper restoration" + }, + { + "name": "F2-correct read at nonzero frame", + "reason": "D gate off frame zero" + }, + { + "name": "F2-neutral target-to-helper contamination", + "reason": "D may read only helpers" + }, + { + "name": "F2-neutral source access at frame zero", + "reason": "D may read only helpers" + } + ], + "columns": 660, + "F2_neutral_prefix_inflation_rejected": true, + "legacy_H2_rejected_as_expected": true, + "normalized_H1_H5_pass": true, + "scope": "Finite F2 circuit, D interface, unchanged geometry, nine-stage columns and native positive prefixes; no hosted invoice or new kappa" +} diff --git a/research/r420-frame-zero-pair/verify.py b/research/r420-frame-zero-pair/verify.py new file mode 100644 index 0000000000..1073e75afc --- /dev/null +++ b/research/r420-frame-zero-pair/verify.py @@ -0,0 +1,338 @@ +#!/usr/bin/env python3 +# Mikhail R. Gadelha, with substantial OpenAI Codex assistance; Apache-2.0. +"""A paid, restored helper-pair factorization of PR543's frame-zero D circuit.""" +import argparse +from collections import Counter +from copy import deepcopy +import gzip +import hashlib +import importlib.util +from itertools import combinations +import json +import os +from pathlib import Path +import shlex +import struct +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/e8-bit-r420/data/bitE8mut-r420.json.gz" +XCHECK = ROOT / "research/e8-bit-r420/code/xcheck.py" +BIT = ROOT / "research/e8-bit-carrier-skeleton/code/bit" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def pair_census(word): + v, n = word["v"], 2 * word["v"] + word["R"] + counts = Counter() + need(len({g[1] for g in word["D"]}) == len(word["D"]), "baseline D repeats a target") + for frame, dst, sources in word["D"]: + need(word["frames"][frame] == [] and v <= dst < 2 * v, + "baseline D must write targets at frame zero") + need(len(set(sources)) == len(sources) and all(2 * v <= s < n for s in sources), + "baseline D must have distinct helper sources") + counts.update(combinations(sorted(sources), 2)) + domain = list(combinations(range(2 * v, n), 2)) + # Independent column-incidence census, including all zero-support pairs. + columns = {s: sum(1 << i for i, g in enumerate(word["D"]) if s in g[2]) + for s in range(2 * v, n)} + need(all(counts[(a, b)] == (columns[a] & columns[b]).bit_count() for a, b in domain), + "pair and incidence-column censuses differ") + best = min(domain, key=lambda p: (-counts[p], p)) + return best, counts[best], Counter(counts[p] for p in domain) + + +def factor(word, pair): + """Run unaffected terms first; prepare a+b, share it, then restore a.""" + a, b = pair + need(a != b and all(2 * word["v"] <= r < 2 * word["v"] + word["R"] for r in pair), + "pair must contain distinct helpers") + zero = word["frames"].index([]) + residual, targets = [], [] + for frame, dst, sources in word["D"]: + shared = a in sources and b in sources + rest = [s for s in sources if not shared or s not in pair] + if rest: + residual.append([frame, dst, rest]) + if shared: + targets.append(dst) + result = deepcopy(word) + result["D"] = residual + [[zero, a, [b]]] + [ + [zero, dst, [a]] for dst in targets + ] + [[zero, a, [b]]] + return result, targets + + +def d_map(word): + """Separate set-valued interpreter: each set lists symbolic input columns.""" + v, n = word["v"], 2 * word["v"] + word["R"] + values = [{r} for r in range(n)] + for frame, dst, sources in word["D"]: + need(word["frames"][frame] == [], "D gate off frame zero") + need(v <= dst < n and sources and len(set([dst] + sources)) == len(sources) + 1, + "invalid D destination or operands") + need(all(2 * v <= s < n for s in sources), "D may read only helpers") + for source in sources: + values[dst].symmetric_difference_update(values[source]) + return values + + +def check_d(original, candidate): + need(d_map(candidate) == d_map(original), "D map differs, including dirty-helper restoration") + + +def record_metrics(records, n, reverse=False): + """Independent exact F2 and nonnegative prefix interpreter, with COPY/ERASE.""" + values = [1 << r for r in range(n)] + [0] + norms = [1] * (n + 1) + largest = 1 + open_center = None + adds = copies = 0 + histogram = Counter() + stream = reversed(records) if reverse else records + for opcode, a, b, coefficient, frame, rank in stream: + if opcode == 0: + if frame: + histogram[frame] += 1 + continue + if reverse and opcode in (2, 3): + opcode = 5 - opcode + if opcode == 1: + need(0 <= a < n and 0 <= b <= n and a != b, "bad scalar record") + need(b != n or open_center is not None, "read of closed copy") + need(a != open_center, "write to copied center") + if coefficient & 1: + values[a] ^= values[b] + norms[a] += abs(coefficient) * norms[b] + largest = max(largest, norms[a]) + adds += 1 + elif opcode == 2: + need(open_center is None and b == n, "bad copy opening") + open_center = a + values[n], norms[n] = values[a], norms[a] + copies += 1 + if not reverse: + histogram[rank] += 1 + elif opcode == 3: + need(open_center == a and b == n, "bad copy closing") + values[n] = norms[n] = 0 + open_center = None + else: + raise ValueError("unknown record opcode") + need(open_center is None and values[n] == 0, "unclosed copy") + return values[:n], largest, adds, copies, dict(sorted(histogram.items())) + + +def export(word, directory): + directory.mkdir() + path = directory / "word.json" + path.write_bytes(canonical(word)) + subprocess.run([sys.executable, "-I", "-B", str(BIT / "export_records.py"), + str(path), str(directory)], check=True, capture_output=True, text=True) + return list(struct.iter_unpack("<6i", (directory / "249-records.bin").read_bytes())) + + +def inspect_records(word, records): + v, n = word["v"], 2 * word["v"] + word["R"] + expected = [(1 << r) ^ (1 << (r - v) if v <= r < 2 * v else 0) for r in range(n)] + forward = record_metrics(records, n) + reverse = record_metrics(records, n, reverse=True) + need(forward[0] == reverse[0] == expected, "record endpoint is not the restored shear") + need(forward[2:4] == reverse[2:4] and forward[3] == 9, "record counts differ") + payload = 64 * forward[1] ** 3 * reverse[1] ** 2 + need(payload < 1 << 104, "native five-stage payload exceeds inherited 104-bit allowance") + return dict(records=len(records), scalar_adds=forward[2], copies=forward[3], + histogram=forward[4], rank_mass=sum(k * c for k, c in forward[4].items()), + forward_prefix=forward[1], reverse_prefix=reverse[1], + payload=str(payload), payload_bits=payload.bit_length()) + + +def rejected(name, original, candidate): + try: + check_d(original, candidate) + except ValueError as error: + return {"name": name, "reason": str(error)} + raise ValueError("control was accepted: " + name) + + +def run(command, log): + result = subprocess.run([str(x) for x in command], capture_output=True, text=True) + log.write_text(result.stdout + result.stderr) + need(result.returncode == 0, "command failed: " + " ".join(map(str, command)) + "\n" + result.stderr) + + +def cohort_check(output, metrics): + """Unmodified predecessor C++ legality, nine-stage columns and prefix bill.""" + compiler = shlex.split(os.environ.get("CXX", "c++")) + checkers = BIT / "checkers" + flags = ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9", "-DVPORTS=120", "-DRHELP=420", + "-DKPAIRS=4", "-I" + str(checkers)] + if os.environ.get("BOOST_INCLUDE"): + flags.append("-I" + os.environ["BOOST_INCLUDE"]) + for name, source in (("columns", "columns_k.cpp"), ("legality", "legality_h.cpp")): + run(compiler + flags + ["-o", str(output / name), str(checkers / source)], + output / (name + "-compile.log")) + receipts = {} + for name in ("baseline", "candidate"): + directory = output / name + cin, cout = directory / "cin", directory / "cout" + run([sys.executable, "-I", "-B", BIT / "regression/stage_cohort.py", + directory, directory, cin, cout], directory / "stage.log") + run([output / "legality", cin, cout, directory / "legality.json"], directory / "legality.log") + run([output / "columns", directory / "249-records.bin", directory / "columns.json"], + directory / "columns.log") + legality = json.loads((directory / "legality.json").read_text()) + columns = json.loads((directory / "columns.json").read_text()) + need(legality["common_frame_ADDs"] == columns["local_scalar_additions"] == metrics[name]["scalar_adds"], + "C++ scalar counts differ") + need(legality["rank_mass"] == metrics[name]["rank_mass"] == 5112, "C++ rank mass differs") + need(legality["records"] == metrics[name]["records"] and legality["copies"] == legality["erasures"] == 9, + "C++ record or copy counts differ") + need(dict(legality["paid_histogram"]) == metrics[name]["histogram"], + "C++ paid histogram differs") + need([int(r["cancellation_free_signed_row_l1_upper"]) for r in columns["signed_lift_prefix"]] + == [metrics[name]["forward_prefix"], metrics[name]["reverse_prefix"]], "C++ prefix differs") + need(columns["payload_prefix_upper"] == metrics[name]["payload"], "C++ payload differs") + need(columns["formal_columns_checked"] == 1380 and len(columns["stages"]) == 9, + "nine-stage coverage changed") + need(len(columns["negative_controls"]) == 18 and all(c["rejected"] for c in columns["negative_controls"]), + "omitted-bridge controls changed") + receipts[name] = dict(formal_columns=1380, stages=9, bridge_controls=18, + legality_status=legality["status"], column_status=columns["status"]) + # Scalar-neutral but bill-inflating control: alternating repeated dirty-helper echoes. + # It must fail at the positive-prefix guard, not at the F2 endpoint check. + directory = output / "candidate" + records = (directory / "249-records.bin").read_bytes() + echo = b"".join(struct.pack("<6i", 1, a, b, 1, 0, 1) + for _ in range(48) for a, b in ((552, 521), (521, 552))) + echo_inverse = b"".join(echo[i:i + 24] for i in range(len(echo) - 24, -1, -24)) + inflated = output / "inflated.bin" + inflated.write_bytes(echo + echo_inverse + records) + inflated_records = list(struct.iter_unpack("<6i", inflated.read_bytes())) + original_records = list(struct.iter_unpack("<6i", records)) + need(record_metrics(inflated_records, 660)[0] == record_metrics(original_records, 660)[0], + "prefix-inflation control must preserve every F2 column") + result = subprocess.run([str(output / "columns"), str(inflated), str(output / "inflated.json")], + capture_output=True, text=True) + need(result.returncode != 0 and "payloadfiniteprefix2^104" in result.stderr, + "F2-neutral positive-prefix inflation control did not fail at its bill") + return receipts + + +def verify(output): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for relative, digest in pins["sha256"].items(): + need(hashlib.sha256((ROOT / relative).read_bytes()).hexdigest() == digest, "source pin mismatch: " + relative) + with gzip.open(SOURCE, "rt") as source: + original = json.load(source) + pair, support, census = pair_census(original) + need(pair == (521, 552) and support == 110, "unexpected best pair") + # The assignment seed is 1: reverse the canonical pair, selecting destination 552. + candidate, targets = factor(original, pair[::-1]) + check_d(original, candidate) + need(all(original[k] == candidate[k] for k in original if k != "D"), "changed exterior") + spec = importlib.util.spec_from_file_location("r420_original_xcheck", XCHECK) + xc = importlib.util.module_from_spec(spec) + spec.loader.exec_module(xc) + baseline = xc.Word(original) + baseline.labels() + baseline.full() + hypotheses, conclusion, _ = baseline.interface() + need(all(hypotheses.values()) and all(conclusion.values()), "baseline interface failed") + # All geometric data are byte-for-byte equal; reuse the exact frame tables. + baseline.w = candidate + baseline.full() + raw_hypotheses, raw_conclusion, _ = baseline.interface() + need([k for k, ok in raw_hypotheses.items() if not ok] == ["H2_D_frame0_targets_from_helpers"], + "candidate violates an interface hypothesis beyond the documented H2 extension") + need([k for k, ok in raw_conclusion.items() if not ok] == ["K_equals_D"], + "unexpected legacy conclusion mismatch") + normalized = deepcopy(candidate) + normalized["D"] = deepcopy(original["D"]) + need(normalized == original, "normalization changed the retained word") + + controls = [] + bad = deepcopy(candidate) + bad["D"].pop() + controls.append(rejected("omitted helper restoration", original, bad)) + bad = deepcopy(candidate) + bad["D"].pop(-2) + controls.append(rejected("omitted shared target read", original, bad)) + bad = deepcopy(candidate) + bad["D"][-1][2] = [520] + controls.append(rejected("wrong restoration source", original, bad)) + bad = deepcopy(candidate) + bad["D"][-2][0] = 1 + controls.append(rejected("F2-correct read at nonzero frame", original, bad)) + bad = deepcopy(candidate) + bad["D"] += [[0, 552, [120]], [0, 552, [120]]] + controls.append(rejected("F2-neutral target-to-helper contamination", original, bad)) + bad = deepcopy(candidate) + bad["D"] += [[0, 552, [0]], [0, 552, [0]]] + controls.append(rejected("F2-neutral source access at frame zero", original, bad)) + # Positive control: a restored helper update independent of all target reads. + good = deepcopy(candidate) + good["D"] += [[0, 240, [241]], [0, 240, [241]]] + check_d(original, good) + + words = {"baseline": original, "candidate": candidate, + "other_orientation": factor(original, pair)[0]} + metrics = {} + baseline_nonscalar = None + for name, word in words.items(): + check_d(original, word) + records = export(word, output / name) + metrics[name] = inspect_records(word, records) + if name == "baseline": + baseline_nonscalar = [r for r in records if r[0] != 1] + else: + need([r for r in records if r[0] != 1] == baseline_nonscalar, "MOVE/COPY/ERASE sequence changed") + need(metrics["baseline"]["scalar_adds"] - metrics["candidate"]["scalar_adds"] == support - 2 == 108, + "incorrect complete XOR saving") + cohort = cohort_check(output, metrics) + return dict(status="PASS_R420_FRAME_ZERO_PAIR", base_commit="66849e1475c930fd7732b1a0067ffee7e1e95f60", + assignment_seed=1, pair=list(pair[::-1]), shared_targets=targets, + domain_pairs=sum(census.values()), pair_support_histogram=dict(sorted(census.items())), + D_adds_before=sum(len(g[2]) for g in original["D"]), + D_adds_after=sum(len(g[2]) for g in candidate["D"]), + candidate_content_sha256=hashlib.sha256(canonical(candidate)).hexdigest(), + input_content_sha256=hashlib.sha256(canonical(original)).hexdigest(), + native=metrics, cohort=cohort, mutation_controls=controls, columns=660, + F2_neutral_prefix_inflation_rejected=True, + legacy_H2_rejected_as_expected=True, normalized_H1_H5_pass=True, + scope="Finite F2 circuit, D interface, unchanged geometry, nine-stage columns and native positive prefixes; no hosted invoice or new kappa") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="New directory for generated words, records and receipt") + args = parser.parse_args() + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + result = verify(args.output) + (args.output / "certificate.json").write_text(json.dumps(result, indent=2) + "\n") + else: + with tempfile.TemporaryDirectory(prefix="r420-frame-zero-pair-") as temporary: + result = verify(Path(temporary)) + expected = json.loads((HERE / "certificate.json").read_text()) + need(json.loads(canonical(result)) == expected, "certificate mismatch") + print("Pair census: 87990/87990 pairs, unique maximum support 110; six D controls rejected") + print("Nine-stage C++ replay: 1380 columns, 18 bridge controls; F2-neutral prefix inflation rejected") + if args.output: + print("Generated evidence:", args.output.resolve()) + print("PASS_R420_FRAME_ZERO_PAIR D=19922->19814 native_adds=26916->26808 columns=660 kappa=unchanged") + + +if __name__ == "__main__": + main()