diff --git a/research/r420-adjoint-compensation/CLAIM.md b/research/r420-adjoint-compensation/CLAIM.md new file mode 100644 index 0000000000..7f078f1ee3 --- /dev/null +++ b/research/r420-adjoint-compensation/CLAIM.md @@ -0,0 +1,57 @@ +# R420 adjoint compensation claim + +- Track: independent verification, OS-random assignment seed 81. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Selected context: PR626 with PR543, conditional kappa + `51110230636731/31250000000000000`. No new bound is proposed. +- Object: the 120 by 420 dirty-helper compensation matrix in the selected + PR543 R420 native word. Check the raw A/scatter/B target map and equality + with D by reverse covector propagation, independently of the supplier's + forward all-column checker. +- Deliverable: a standalone standard-library verifier, exact matrix/cut + certificate, rank and kernel information, rejecting controls, and proof note. +- Time budget: approximately 30 minutes from 2026-10-13 04:50 UTC. Finish by + 05:20 UTC, with the final 7.5 minutes reserved for verification and handoff. +- Coordination: GitHub returned no pinned issues. This is the local claim. + Open PR titles and relevant bodies were inspected before claiming. + +Three candidates considered were the R420 compensation identity, selected +complex cold-wrapper phases, and selected supplier moment bounds. PR702/712 +cover the phase route and PR678/706 cover the moments. Seed 81 selects the bit +object and backward scalar method. PR612 checks typed R420 boundaries and +B-XOR target translation, but explicitly leaves D parity/compensation equality +open. The supplier's existing `xcheck.py` already checks that equality by a +forward symbolic replay. This work independently corroborates it with backward +covectors and an explicit matrix certificate; it does not claim that the +identity itself is new or that a Python check completes the Lean obligation. + +Scope excludes frame legality, COPY/ERASE realization, hosting, costs, moments, +all-size compilation and the multiplication theorem. No existing supplier, +selected certificate, or `upstream/` file will change. Acceptance requires +exact equality for every target and every original input coordinate, source +binding, deterministic evidence, and controls that reject altered compensation +and incorrect transpose semantics. + +Prepared for Sagar Thakrar (@thakrarsagar) with substantial OpenAI Codex +assistance. Apache-2.0; independent implementation is not independent human +peer review. + +## Completed result and one scope pivot + +Submitted [PR762](https://github.com/CrocSwap/integer-mult-bounds/pull/762). +The result is ten optimal nonadaptive dirty-input tests for compensation-row +errors of weight at most three, with an executable four-error blind witness. +The primary command passes 129 rejection controls. The separate support-set +and Boolean checker confirms the fixed baseline, all ten probes and malformed +suite rejection. See README.md and VALIDATION.md for exact scope and checks. + +The initial queue scan ended at PR725. A later refresh discovered Joshua +Snider's PR731 at `cf5ff54a358b400a7e69abe941d1d0ad0944b25e`, which had +submitted the same adjoint/rank work with additional kernel evidence. The +planned rank certificate was removed and the scope pivoted once to the +optimal ten-test suite. This credits PR731 and adds a distinct result on the +test matrix, not another claim about its compensation kernel. + +The pre-submission refresh covered 578 open PRs through PR759. No pinned +coordination issue existed, so this is the single local completion update. +No pending code was imported. Only this seven-file package was added. diff --git a/research/r420-adjoint-compensation/EXPECTED.json b/research/r420-adjoint-compensation/EXPECTED.json new file mode 100644 index 0000000000..f65632dd6b --- /dev/null +++ b/research/r420-adjoint-compensation/EXPECTED.json @@ -0,0 +1,192 @@ +{ + "assignment_seed": 81, + "domain": { + "helpers": 420, + "original_inputs": 660, + "targets": 120 + }, + "format": "r420-compensation-optimal-test-suite-v1", + "gate_counts": { + "A": 2064, + "B": 837, + "C": 2661, + "D": 120 + }, + "matrix_binary_sha256": "c833a715013f78e383ca95a684d26c000db5cba0dc848221bb05e5db6e63d4ed", + "negative_controls": [ + "omit_D_operand_0", + "omit_D_operand_1", + "omit_D_operand_2", + "omit_D_operand_3", + "omit_D_operand_4", + "omit_D_operand_5", + "omit_D_operand_6", + "omit_D_operand_7", + "omit_D_operand_8", + "omit_D_operand_9", + "omit_D_operand_10", + "omit_D_operand_11", + "omit_D_operand_12", + "omit_D_operand_13", + "omit_D_operand_14", + "omit_D_operand_15", + "omit_D_operand_16", + "omit_D_operand_17", + "omit_D_operand_18", + "omit_D_operand_19", + "omit_D_operand_20", + "omit_D_operand_21", + "omit_D_operand_22", + "omit_D_operand_23", + "omit_D_operand_24", + "omit_D_operand_25", + "omit_D_operand_26", + "omit_D_operand_27", + "omit_D_operand_28", + "omit_D_operand_29", + "omit_D_operand_30", + "omit_D_operand_31", + "omit_D_operand_32", + "omit_D_operand_33", + "omit_D_operand_34", + "omit_D_operand_35", + "omit_D_operand_36", + "omit_D_operand_37", + "omit_D_operand_38", + "omit_D_operand_39", + "omit_D_operand_40", + "omit_D_operand_41", + "omit_D_operand_42", + "omit_D_operand_43", + "omit_D_operand_44", + "omit_D_operand_45", + "omit_D_operand_46", + "omit_D_operand_47", + "omit_D_operand_48", + "omit_D_operand_49", + "omit_D_operand_50", + "omit_D_operand_51", + "omit_D_operand_52", + "omit_D_operand_53", + "omit_D_operand_54", + "omit_D_operand_55", + "omit_D_operand_56", + "omit_D_operand_57", + "omit_D_operand_58", + "omit_D_operand_59", + "omit_D_operand_60", + "omit_D_operand_61", + "omit_D_operand_62", + "omit_D_operand_63", + "omit_D_operand_64", + "omit_D_operand_65", + "omit_D_operand_66", + "omit_D_operand_67", + "omit_D_operand_68", + "omit_D_operand_69", + "omit_D_operand_70", + "omit_D_operand_71", + "omit_D_operand_72", + "omit_D_operand_73", + "omit_D_operand_74", + "omit_D_operand_75", + "omit_D_operand_76", + "omit_D_operand_77", + "omit_D_operand_78", + "omit_D_operand_79", + "omit_D_operand_80", + "omit_D_operand_81", + "omit_D_operand_82", + "omit_D_operand_83", + "omit_D_operand_84", + "omit_D_operand_85", + "omit_D_operand_86", + "omit_D_operand_87", + "omit_D_operand_88", + "omit_D_operand_89", + "omit_D_operand_90", + "omit_D_operand_91", + "omit_D_operand_92", + "omit_D_operand_93", + "omit_D_operand_94", + "omit_D_operand_95", + "omit_D_operand_96", + "omit_D_operand_97", + "omit_D_operand_98", + "omit_D_operand_99", + "omit_D_operand_100", + "omit_D_operand_101", + "omit_D_operand_102", + "omit_D_operand_103", + "omit_D_operand_104", + "omit_D_operand_105", + "omit_D_operand_106", + "omit_D_operand_107", + "omit_D_operand_108", + "omit_D_operand_109", + "omit_D_operand_110", + "omit_D_operand_111", + "omit_D_operand_112", + "omit_D_operand_113", + "omit_D_operand_114", + "omit_D_operand_115", + "omit_D_operand_116", + "omit_D_operand_117", + "omit_D_operand_118", + "omit_D_operand_119", + "omit_D", + "duplicate_D_operand", + "swap_D_targets", + "wrong_A_order", + "wrong_B_order", + "wrong_scatter_helpers", + "omit_scatter_operand", + "D_reads_source", + "self_alias" + ], + "nonzero_entries": 19922, + "positive_controls": [ + "duplicate_D_pair", + "two_gate_transpose", + "two_gate_wrong_order" + ], + "raw_sections": [ + "A", + "scatter", + "B" + ], + "row_weight_range": [ + 121, + 204 + ], + "suite": { + "blind_four_support": [ + 240, + 241, + 242, + 243 + ], + "blind_target": 201, + "blind_witness_dirty_helper": 240, + "column_rule": "1 | (helper_relative_index << 1)", + "fault_radius_per_target": 3, + "optimality_bound": "420 <= 2^(q-1), hence q >= 10", + "pair_supports": 87990, + "pattern_hex": [ + "fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff", + "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa", + "ccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccccc", + "0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0f0", + "0ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00ff00", + "0ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000ffff0000", + "f00000000ffffffff00000000ffffffff00000000ffffffff00000000ffffffff00000000ffffffff00000000ffffffff00000000", + "000000000ffffffffffffffff0000000000000000ffffffffffffffff0000000000000000ffffffffffffffff0000000000000000", + "fffffffff00000000000000000000000000000000ffffffffffffffffffffffffffffffff00000000000000000000000000000000", + "fffffffffffffffffffffffffffffffffffffffff0000000000000000000000000000000000000000000000000000000000000000" + ], + "single_supports": 420, + "test_count": 10, + "triple_supports": 12259940 + }, + "zero_columns": [] +} diff --git a/research/r420-adjoint-compensation/README.md b/research/r420-adjoint-compensation/README.md new file mode 100644 index 0000000000..6bb7e77fa1 --- /dev/null +++ b/research/r420-adjoint-compensation/README.md @@ -0,0 +1,186 @@ +# Ten optimal dirty-input tests for R420 compensation faults + +Ten fixed dirty-helper assignments detect every nonzero change of at most +three coefficients in each target row of the selected R420 word's D +compensation. No set of nine nonadaptive binary assignments can give that +guarantee. This package supplies the assignments, an elementary optimality +proof, two independent execution methods, and a four-coefficient error that +all ten assignments miss. + +This is an independent-verification research note, with no new circuit or +kappa. The ten tests do not replace the full symbolic checker. + +## Reproduce + +From the repository root, with Python 3.9 or later and its standard library: + +```sh +python3 -I -B research/r420-adjoint-compensation/verify.py +python3 -I -B research/r420-adjoint-compensation/independent_check.py +``` + +The first command must print: + +```text +PASS_R420_COMPENSATION_SUITE tests=10 optimal=10 radius=3 targets=120 blind_weight=4 controls=129 +``` + +The second independently replays all ten Boolean inputs and reports success. +Both commands are offline and read-only. `verify.py --emit` prints the complete +deterministic certificate. The default compares every field with `EXPECTED.json`. + +## Fixed map and fault model + +The word is `research/e8-bit-r420/data/bitE8mut-r420.json.gz`. Registers +0 through 119 hold x, 120 through 239 hold y, and 240 through 659 hold arbitrary +helper dirt s. The ordered raw A/scatter/B target map over F2 is + +```text +W0(x,y,s)_targets = x + y + K s, K: 120 by 420. +``` + +Initial D adds Ks to y. Suppose only that correction changes to K+E; A, +scatter, B and C remain fixed. The raw target-to-target block is the identity, +so the final target error is exactly Es. C does not write targets. Repeated +source operands count modulo two. Fault weight therefore means changed matrix +coefficients, not the number of edited source-list entries. + +The guarantee covers any nonzero E whose nonzero rows each have weight at +most three. Multiple rows may be faulty simultaneously. Outputs are observed +exactly, with each target separately visible, and inputs are fixed in advance. +Changes to the raw word, state-dependent faults, physical frame errors and +arbitrary higher-weight errors are outside this model. + +The primary checker independently confirms the baseline map using backward +covectors. For a gate `z[d] ^= sum(z[s])`, its transpose adds the old +destination coefficient to each listed source coefficient. Transposes execute +in reverse gate order. Scatter indices resolve through `ret`, and operand +multiplicities are retained. All 120 target rows are checked on all 660 input +coordinates. The helper block must equal D; pulling the raw rows back through +D must leave exactly x_t+y_t. + +This confirms J=I, V=I and K=D for the pinned scalar word and all 2^660 scalar +assignments, by linearity. K has 19,922 nonzero entries. Its 50,400 row-major +binary entries, encoded as one byte 0 or 1 each, have SHA-256 +`c833a715013f78e383ca95a684d26c000db5cba0dc848221bb05e5db6e63d4ed`. +This baseline corroborates existing work. The new result is the optimal +test suite and its exact fault boundary. + +## Construction and proof + +Assign helper-relative coordinate j, from 0 through 419, the ten-bit column + +```text +h[j] = 1 | (j << 1). +``` + +Test k sets helper j to bit k of h[j], for k from 0 through 9. Source and +target inputs are zero. The first test sets all helpers to one; the other +nine use the binary digits of j. For a changed coefficient support S in +one target row, the vector of ten errors is the XOR of h[j] over j in S. + +- One or three coefficients give low bit one, hence a nonzero syndrome. +- Two distinct coefficients give distinct columns, hence a nonzero XOR. + +This applies independently to every target row. The primary checker checks +420 distinct odd columns and all 87,990 pairs, then executes the actual word +under all ten assignments. Three additional packed executions put respectively +one, two and three coefficient changes into every target row and check all +120 exact syndromes. The odd-column invariant proves coverage of all +12,259,940 triples without enumerating them. This covers 12,348,350 nonempty +supports of size at most three per target. + +For optimality, consider any q nonadaptive binary assignments and their +420 q-bit helper response columns. Detecting singles requires nonzero columns; +detecting pairs requires distinct columns; detecting triples forbids three +distinct columns a,b,c with a+b=c. If A is their set and a is in A, the sets +A and a+A are disjoint. An intersection would give a forbidden triple; cases +with repeated members require a zero column. Therefore + +```text +2 |A| <= 2^q, so 420 <= 2^(q-1), hence q >= 10. +``` + +Our construction attains ten. Varying source or target inputs cannot improve +this bound in the stated model, because Es depends only on helper inputs. +The bound does not cover adaptive experiments or other observation channels. + +## Exact limit, certificate and controls + +Toggle D's four coefficients for absolute helpers `[240,241,242,243]` at +absolute target 201. Their labels XOR to zero, so all ten tests pass. +Yet helper input s_0=1 with every other input zero gives error one at target +201. Both facts are checked by literal scalar execution, and the full +covector check rejects this mutant's D parity. This is a deliberately changed +D, not a defect in the accepted word. These coordinates form a kernel vector +of the test matrix; no claim is made that they form a kernel vector of K. + +`EXPECTED.json` contains `suite.pattern_hex`: ten 420-bit assignments, +each a 105-digit hexadecimal integer. Bit j selects helper 240+j. The +certificate also records the fault radius, counts, column rule and blind +witness. It contains no regenerated compressed artifact. + +The 129 primary rejecting controls include one omitted D operand per target, +plus omitted D, a duplicate operand, exchanged D destinations, reversed A, +reversed B, wrong scatter helpers, a missing scatter operand, a source read +in D, and self-aliasing. Row t's omitted operand has index +`(81+t) % len(D[t].sources)`. Positive controls preserve duplicate-pair +parity and distinguish transpose propagation on a two-gate example. + +The independent checker uses forward support sets for the baseline and ten +separate Boolean executions. It imports neither the primary checker nor +supplier code. It also checks the four-error blind witness and malformed +test suites. The fixed coverage and proof above are the stopping rule. +This is not an exhaustive arbitrary-mutation search. The elementary +optimality proof is not machine-formalized. + +## Concurrent work and provenance + +The initial queue refresh ended at PR725. During implementation Joshua +Snider's [PR731](https://github.com/CrocSwap/integer-mult-bounds/pull/731), +at `cf5ff54a358b400a7e69abe941d1d0ad0944b25e`, submitted the same backward +compensation reconstruction, rank/right-inverse evidence and further kernel +results. Those baseline findings are credited to that concurrent submission. +This package then pivoted to the ten-test optimum and four-error blind +witness. PR731's kernel concerns K; our blind witness concerns the separate +ten-by-420 test matrix. No PR731 code or certificate is consumed, and its +additional kernel claims are not audited here. + +PR612 at `ce37f3ce35ba8891771e01492b3a21978763bebb` supplies typed R420 +boundaries and B-XOR semantics. This Python check does not close its open D +parity formalization. PR737 concerns R420 frame geometry; PR745 concerns +complex JP8 private-input restoration. Neither is a dependency. + +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- PR543: `2065fe4f72a914d907f1046603f5a36f17018535`. +- Selected PR626: `660de893d27bb7abd1d5b01b1640207528a5c851`. +- Selected conditional kappa: `51110230636731/31250000000000000`. +- Native word Git blob: `0c63ca62759dc63d302be6552aeeee1ede70350f`, + identical at the base and PR543 commits. + +`SOURCES.json` pins all consumed source/context files, including compressed +and decompressed word hashes. The verifier also binds the word to the selected +source manifest and PR543 dependency. Scope references are not imported. + +The selected frontier and `upstream/` are unchanged. Frame legality, +COPY/ERASE realization, source/helper restoration, common-label and +mutable-basis interfaces, hosting, paid profiles, moments, precision, tapes, +exact recovery, all-size compilation and analytic transfer remain outside +the result. The independent checker's ten scalar endpoint examples do not +prove general restoration. + +## Attribution + +Credit eumemic's PR543 word and checker, including its disclosed Anthropic +Claude assistance; eumemic's PR493 skeleton; Dylan Crow's PR370 format and +decoder; Jacob Sussman's E8 unit; DreamingOfClouds' PR503/510 lineage; +Zhihao Chen's PR425 scalar-interface lemma; and icekylinx's mutable-source +carryover. The full predecessor notice remains in the pinned R420 package. +The selected context also credits Jeremy Kothe's PR622 construction and +Chafik Boukhalfa's PR626 allocation. Credit Joshua Snider's concurrent PR731 +and the PR612 authors' typed boundary work. + +Prepared for Sagar Thakrar (@thakrarsagar) with substantial OpenAI Codex +assistance, including a separate Codex worker's forward implementation and +proof review. Independent implementation is not independent human peer +review. New files use Apache-2.0. No predecessor code is copied here. diff --git a/research/r420-adjoint-compensation/SOURCES.json b/research/r420-adjoint-compensation/SOURCES.json new file mode 100644 index 0000000000..2151f6a555 --- /dev/null +++ b/research/r420-adjoint-compensation/SOURCES.json @@ -0,0 +1,35 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "pr543_head": "2065fe4f72a914d907f1046603f5a36f17018535", + "selected_pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "word_payload_sha256": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "files": { + "certificates/selected-result.json": { + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "research/community-k492-audit/SELECTED-SOURCE.json": { + "sha256": "36e9e421230c4cb7b6a537d76a4bdfb6f667730d383e56062d4e45957484ab9e" + }, + "research/e8-bit-r420/data/bitE8mut-r420.json.gz": { + "sha256": "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784", + "git_blob": "0c63ca62759dc63d302be6552aeeee1ede70350f" + }, + "research/e8-bit-r420/code/xcheck.py": { + "sha256": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" + }, + "research/e8-bit-r420/README.md": { + "sha256": "9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f" + }, + "research/e8-bit-r420/NOTICE.md": { + "sha256": "12ba6e0845f222e9940b00f6c60d261db104246a8d3143da267682973479f811" + }, + "docs/research/community-k492-review.md": { + "sha256": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47" + } + }, + "scope_reference": { + "pr731_head": "cf5ff54a358b400a7e69abe941d1d0ad0944b25e", + "pr612_head": "ce37f3ce35ba8891771e01492b3a21978763bebb", + "description": "R420 Lean boundary and B-XOR work; no code imported or theorem object consumed" + } +} diff --git a/research/r420-adjoint-compensation/VALIDATION.md b/research/r420-adjoint-compensation/VALIDATION.md new file mode 100644 index 0000000000..f63f8636b3 --- /dev/null +++ b/research/r420-adjoint-compensation/VALIDATION.md @@ -0,0 +1,38 @@ +# Validation record + +Executed on 2026-10-13, macOS arm64. The checks below passed with the pinned +base and sources listed in `SOURCES.json`. + +| Check | Result | +| --- | --- | +| Primary backward verifier, isolated Python 3.9.6 | PASS, 129 rejecting controls | +| Primary backward verifier, isolated optimized Python 3.9.6 | PASS, same certificate | +| Primary backward verifier, Python 3.14.8 | PASS | +| Separate support-set and Boolean verifier, Python 3.9.6 and 3.14.8 | PASS, ten full scalar probes, bounded fault controls, three malformed suites | +| Certificate emission, Python 3.9.6 versus optimized Python 3.14.8 | Byte-identical | +| Both final checkers from a minimal copied tree with spaces, unrelated working directory, Python 3.9.6 | PASS | +| Corrupted compressed source bytes | Rejected by source pin before decompression | +| Zeroed parity probe | Rejected by both checkers | +| Changed test count in committed receipt | Rejected by primary checker | +| Missing certificate and missing pinned source | Both rejected | +| `make selected-record-check` | PASS, exact selected kappa and source inventory | +| Native word Git blob at base versus PR543 source | Identical | + +The complete canonical `--emit` output has SHA-256 +`e340ed4188ae666b408143195b394686eba26cb266e2ded2fe0a53f6c519b607`. +This hash describes the JSON output, not a regenerated gzip container. + +The minimal-tree and external mutation tests used temporary copies of this +package and exactly the seven pinned source/context files. They did not +modify repository inputs. The certificate, source and missing-file tests are +fail-closed execution checks; they are separate from the 129 in-process +mathematical/schema controls in the reproducible primary command. + +A separate Codex worker wrote and ran the forward support-set/Boolean checker +and reviewed the adjoint implementation and ten-test optimality proof. No blocking +finding remained. This is disclosed AI review, not independent human review. + +The full repository suite, full selected cold replay, remote Linux CI and +Lean were not run. No existing generator, supplier, selected certificate or +`upstream/` file changed. The result has the scalar scope stated in README.md; +it does not verify physical interfaces, restoration, cost or the full theorem. diff --git a/research/r420-adjoint-compensation/independent_check.py b/research/r420-adjoint-compensation/independent_check.py new file mode 100644 index 0000000000..6275bacfd5 --- /dev/null +++ b/research/r420-adjoint-compensation/independent_check.py @@ -0,0 +1,138 @@ +#!/usr/bin/env python3 +"""Independent support-set and Boolean checks for the ten dirty probes. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +SPDX-License-Identifier: Apache-2.0 +""" +import copy +import gzip +import hashlib +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +WORD = HERE.parent / "e8-bit-r420/data/bitE8mut-r420.json.gz" +SOURCE_SHA256 = "9721a3819efd68307f66f00d84a952eb28eb7c3ad2ce79653ce295c98a764784" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def gates(word, section): + if section == "scatter": + return [(0, 120 + t, [word["ret"][i] for i in row]) + for t, row in enumerate(word["scatter"])] + return word[section] + + +def raw_supports(word): + values = [{i} for i in range(660)] + for section in ("A", "scatter", "B"): + for _, destination, sources in gates(word, section): + require(destination not in sources, "self-reading gate outside scope") + delta = set() + for source in sources: + delta.symmetric_difference_update(values[source]) + values[destination].symmetric_difference_update(delta) + return values[120:240] + + +def execute_boolean(word, dirt): + values = [False] * 240 + [j in dirt for j in range(420)] + for section in ("D", "A", "scatter", "B", "C"): + for _, destination, sources in gates(word, section): + delta = False + for source in sources: + delta ^= values[source] + values[destination] ^= delta + return values + + +def decode_hex(value): + bits = format(int(value, 16), "b") + require(len(bits) <= 420, "probe exceeds helper width") + return {i for i, bit in enumerate(reversed(bits)) if bit == "1"} + + +def validate_labels(labels): + require(len(labels) == 420 and all(0 < x < 1024 for x in labels), "zero or invalid column") + pool = set(labels) + require(len(pool) == len(labels), "duplicate columns conceal a pair") + for i, first in enumerate(labels): + for second in labels[i + 1:]: + require(first ^ second not in pool, "three columns sum to zero") + + +def main(): + compressed = WORD.read_bytes() + require(hashlib.sha256(compressed).hexdigest() == SOURCE_SHA256, "source pin mismatch") + word = json.loads(gzip.decompress(compressed)) + require((word["v"], word["R"]) == (120, 420), "unexpected dimensions") + raw = raw_supports(word) + compensation = [set() for _ in range(120)] + for frame, destination, sources in word["D"]: + require(frame == 0 and 120 <= destination < 240 and + all(240 <= source < 660 for source in sources), "invalid D interface") + for source in sources: + compensation[destination - 120].symmetric_difference_update({source}) + require(raw == [{t, 120 + t} | compensation[t] for t in range(120)], "baseline K=D fails") + + certificate = json.loads((HERE / "EXPECTED.json").read_text()) + probes = [decode_hex(row) for row in certificate["suite"]["pattern_hex"]] + require(len(probes) == 10, "expected ten probes") + labels = [sum(2 ** k for k, probe in enumerate(probes) if j in probe) for j in range(420)] + require(labels == [1 + 2 * j for j in range(420)], "probe columns differ from construction") + validate_labels(labels) + require(2 * 420 > 2 ** 9 and 2 * 420 <= 2 ** 10, "minimality arithmetic") + for probe in probes: + expected = [False] * 240 + [j in probe for j in range(420)] + require(execute_boolean(word, probe) == expected, "full-word Boolean probe failed") + + # Distinct mutated D parities of each promised weight exercise the real word. + mutation_controls = [] + for support in ([81], [81, 82], [81, 82, 83]): + mutant = copy.deepcopy(word) + mutant["D"][81][2] = sorted(set(mutant["D"][81][2]) ^ {240 + j for j in support}) + syndrome = 0 + for j in support: + syndrome ^= labels[j] + detected = 0 + for k, probe in enumerate(probes): + expected = [False] * 240 + [j in probe for j in range(420)] + expected[120 + 81] = bool(syndrome & (2 ** k)) + require(execute_boolean(mutant, probe) == expected, "D fault syndrome differs from prediction") + detected += bool(expected[120 + 81]) + require(detected > 0, "promised fault went undetected") + mutation_controls.append({"weight": len(support), "detecting_probes": detected}) + + rejected = [] + for name, index, replacement in (("zero_column", 0, 0), ("duplicate_columns", 1, labels[0]), + ("triple_sum_zero", 2, labels[0] ^ labels[1])): + malformed = labels.copy() + malformed[index] = replacement + try: + validate_labels(malformed) + except ValueError: + rejected.append(name) + else: + raise ValueError("malformed suite accepted: " + name) + + blind = copy.deepcopy(word) + blind["D"][81][2] = sorted(set(blind["D"][81][2]) ^ {240, 241, 242, 243}) + require(all(len(probe & {0, 1, 2, 3}) % 2 == 0 for probe in probes), "four-term blind spot absent") + require(all(execute_boolean(blind, probe) == execute_boolean(word, probe) for probe in probes), + "four-term blind spot did not survive actual replay") + require(execute_boolean(blind, {0})[201] and not execute_boolean(word, {0})[201], + "singleton dirty input must expose the blind fault") + print(json.dumps({"method": "support sets, then full-word Boolean execution", "test_count": 10, + "baseline_K_equals_D": True, "all_columns_nonzero_distinct_sum_free": True, + "minimum_test_count": 10, "mutated_word_controls": mutation_controls, + "malformed_suites_rejected": rejected, + "weight_four_fault_passes_all_ten": [0, 1, 2, 3]}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/r420-adjoint-compensation/verify.py b/research/r420-adjoint-compensation/verify.py new file mode 100644 index 0000000000..bc87b83918 --- /dev/null +++ b/research/r420-adjoint-compensation/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Exact backward-covector certificate for the selected R420 compensation. + +Prepared for Sagar Thakrar with substantial OpenAI Codex assistance. +Apache-2.0. No supplier implementation is imported or executed. +""" +import copy +import gzip +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SEED = 81 +WORD = "research/e8-bit-r420/data/bitE8mut-r420.json.gz" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_word(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + for path, pin in pins["files"].items(): + raw = (ROOT / path).read_bytes() + need(hashlib.sha256(raw).hexdigest() == pin["sha256"], "source pin: " + path) + selected = json.loads((ROOT / "certificates/selected-result.json").read_text()) + need(selected["reviewed_dependency_heads"]["543"] == pins["pr543_head"], "PR543 binding") + manifest = json.loads((ROOT / selected["source_manifest"]).read_text()) + need(manifest["files"][WORD] == pins["files"][WORD]["sha256"], "selected word binding") + payload = gzip.decompress((ROOT / WORD).read_bytes()) + need(hashlib.sha256(payload).hexdigest() == pins["word_payload_sha256"], "payload pin") + return json.loads(payload) + + +def validate(w): + need((w["v"], w["R"]) == (120, 420), "dimensions") + n = 660 + for section in ("D", "A", "B", "C"): + for f, d, sources in w[section]: + need(type(f) is int and 0 <= f < len(w["frames"]), "frame index") + need(type(d) is int and 0 <= d < n, "destination index") + need(all(type(s) is int and 0 <= s < n and s != d for s in sources), "operand index or alias") + need(len(w["scatter"]) == 120 and all(240 <= h < n for h in w["ret"]), "scatter shape") + need(all(type(k) is int and 0 <= k < len(w["ret"]) for row in w["scatter"] for k in row), "scatter index") + need(all(120 <= d < 240 and all(s >= 240 for s in src) for _, d, src in w["D"]), "D must correct targets from helpers") + need(all(not 120 <= d < 240 for _, d, _ in w["C"]), "C changes a target") + + +def pullback(q, gates): + """For x[d] ^= sum(x[s]), transpose sends q[s] ^= old q[d].""" + for _, d, sources in reversed(gates): + if q & (1 << d): + for s in sources: + q ^= 1 << s + return q + + +def raw_covectors(w): + rows = [] + for target in range(120): + q = pullback(1 << (120 + target), w["B"]) + for t, indices in enumerate(w["scatter"]): + if q & (1 << (120 + t)): + for k in indices: + q ^= 1 << w["ret"][k] + rows.append(pullback(q, w["A"])) + return rows + + +def compensation_rows(w): + rows = [0] * 120 + for _, d, sources in w["D"]: + for s in sources: + rows[d - 120] ^= 1 << (s - 240) + return rows + + +def check_identity(w): + validate(w) + raw = raw_covectors(w) + correction = compensation_rows(w) + for t, q in enumerate(raw): + wanted = (1 << t) | (1 << (120 + t)) + need(q & ((1 << 240) - 1) == wanted, "J/V identity: target " + str(t)) + need(q >> 240 == correction[t], "D parity: target " + str(t)) + need(pullback(q, w["D"]) == wanted, "complete target map: " + str(t)) + return [q >> 240 for q in raw] + + +def scalar_tests(w, labels): + """Bit k of each value is the execution under dirty assignment k.""" + values = [0] * 240 + list(labels) + for section in ("D", "A", "scatter", "B", "C"): + if section == "scatter": + gates = [(0, 120 + t, [w["ret"][i] for i in row]) + for t, row in enumerate(w["scatter"])] + else: + gates = w[section] + for _, d, sources in gates: + delta = 0 + for s in sources: + delta ^= values[s] + values[d] ^= delta + return values[120:240] + + +def suite_certificate(w): + labels = [1 | (j << 1) for j in range(420)] + patterns = [sum(1 << j for j, label in enumerate(labels) if label & (1 << k)) for k in range(10)] + need(all(labels) and len(set(labels)) == 420, "zero or duplicate syndrome column") + need(all(label & 1 for label in labels), "odd-error parity row") + pairs = [(i, j) for i in range(420) for j in range(i + 1, 420)] + need(all(labels[i] ^ labels[j] for i, j in pairs), "undetected two-coefficient fault") + need(scalar_tests(w, labels) == [0] * 120, "baseline ten-test replay") + for weight in (1, 2, 3): + bad = copy.deepcopy(w) + expected = [] + for t in range(120): + support = [(SEED + t + k) % 420 for k in range(weight)] + bad["D"][t][2] = sorted(set(bad["D"][t][2]) ^ {240 + j for j in support}) + syndrome = 0 + for j in support: + syndrome ^= labels[j] + expected.append(syndrome) + need(all(expected) and scalar_tests(bad, labels) == expected, "bounded D fault replay") + # Outside the promised radius, all ten tests can miss an actual scalar fault. + blind = copy.deepcopy(w) + blind["D"][SEED][2] = sorted(set(blind["D"][SEED][2]) ^ {240, 241, 242, 243}) + need(scalar_tests(blind, labels) == [0] * 120, "four-coefficient blind control") + try: + check_identity(blind) + except ValueError as error: + need(str(error).startswith("D parity:"), "blind control failed for another reason") + else: + raise ValueError("full check missed four-coefficient fault") + need(scalar_tests(blind, [1] + [0] * 419)[SEED] == 1, "blind control basis witness") + return { + "test_count": 10, + "pattern_hex": [format(pattern, "0105x") for pattern in patterns], + "column_rule": "1 | (helper_relative_index << 1)", + "fault_radius_per_target": 3, + "single_supports": 420, + "pair_supports": len(pairs), + "triple_supports": 420 * 419 * 418 // 6, + "optimality_bound": "420 <= 2^(q-1), hence q >= 10", + "blind_four_support": [240, 241, 242, 243], + "blind_target": 120 + SEED, + "blind_witness_dirty_helper": 240, + } + + +def negative_controls(w): + rejected = [] + + def reject(name, mutant): + try: + check_identity(mutant) + except ValueError: + rejected.append(name) + else: + raise ValueError("control accepted: " + name) + + # One selected omission in every D row, with all covectors recomputed. + for t in range(120): + bad = copy.deepcopy(w) + del bad["D"][t][2][(SEED + t) % len(bad["D"][t][2])] + reject("omit_D_operand_" + str(t), bad) + bad = copy.deepcopy(w) + bad["D"] = [] + reject("omit_D", bad) + bad = copy.deepcopy(w) + bad["D"][SEED][2].append(bad["D"][SEED][2][0]) + reject("duplicate_D_operand", bad) + bad = copy.deepcopy(w) + bad["D"][SEED][1], bad["D"][SEED + 1][1] = bad["D"][SEED + 1][1], bad["D"][SEED][1] + reject("swap_D_targets", bad) + bad = copy.deepcopy(w) + bad["A"].reverse() + reject("wrong_A_order", bad) + bad = copy.deepcopy(w) + bad["B"].reverse() + reject("wrong_B_order", bad) + bad = copy.deepcopy(w) + bad["ret"] = [240 + k for k in range(len(w["ret"]))] + reject("wrong_scatter_helpers", bad) + bad = copy.deepcopy(w) + bad["scatter"][SEED].pop() + reject("omit_scatter_operand", bad) + bad = copy.deepcopy(w) + bad["D"][SEED][2][0] = SEED + reject("D_reads_source", bad) + bad = copy.deepcopy(w) + bad["A"][SEED][2].append(bad["A"][SEED][1]) + reject("self_alias", bad) + # Even duplicate occurrences cancel; lists must retain XOR multiplicity. + same = copy.deepcopy(w) + operand = same["D"][SEED][2][0] + same["D"][SEED][2].extend([operand, operand]) + need(check_identity(same) == check_identity(w), "duplicate-pair positive control") + # Distinguish reverse transpose from simply running the gates backward. + toy = [[0, 1, [0]], [0, 2, [1]]] + need(pullback(1 << 2, toy) == 7, "two-gate transpose control") + need(pullback(1 << 2, list(reversed(toy))) == 6, "order-sensitive toy control") + return rejected + + +def evidence(w): + rows = check_identity(w) + binary = bytes((row >> col) & 1 for row in rows for col in range(420)) + controls = negative_controls(w) + return { + "format": "r420-compensation-optimal-test-suite-v1", + "assignment_seed": SEED, + "domain": {"targets": 120, "helpers": 420, "original_inputs": 660}, + "raw_sections": ["A", "scatter", "B"], + "gate_counts": {s: len(w[s]) for s in ("D", "A", "B", "C")}, + "nonzero_entries": sum(bin(row).count("1") for row in rows), + "zero_columns": [c for c in range(420) if all(not row & (1 << c) for row in rows)], + "row_weight_range": [min(bin(r).count("1") for r in rows), max(bin(r).count("1") for r in rows)], + "matrix_binary_sha256": hashlib.sha256(binary).hexdigest(), + "suite": suite_certificate(w), + "negative_controls": controls, + "positive_controls": ["duplicate_D_pair", "two_gate_transpose", "two_gate_wrong_order"], + } + + +def main(): + need(sys.argv[1:] in ([], ["--emit"]), "usage: verify.py [--emit]") + result = evidence(load_word()) + if sys.argv[1:] == ["--emit"]: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = json.loads((HERE / "EXPECTED.json").read_text()) + need(result == expected, "committed certificate mismatch") + print("PASS_R420_COMPENSATION_SUITE tests=10 optimal=10 radius=3 targets=120 blind_weight=4 controls=" + str(len(result["negative_controls"]))) + + +if __name__ == "__main__": + try: + main() + except (ValueError, KeyError, TypeError, OSError) as error: + raise SystemExit("FAIL_R420_ADJOINT: " + str(error))