diff --git a/research/r439-target-closed-k-residual/README.md b/research/r439-target-closed-k-residual/README.md new file mode 100644 index 0000000000..1ea3301668 --- /dev/null +++ b/research/r439-target-closed-k-residual/README.md @@ -0,0 +1,157 @@ +# R439 literal K defect: target reads versus helper wraps + +**Finite certificate on nine named words. No new κ.** The selected κ stays +0.001672660197076918. This adopts no replacement `K_equals_D` contract, admits +no supplier and changes no paid profile. + +## Question + +PR #4092 counted the literal `K_equals_D` defect on the three helper-star words +(17,636 / 17,636 / 17,653 bits, all 439 helper sectors defective). It asked +whether that pattern persists on other helper-mixing lineages. The merged +`r439-k-cross-term-tally` package identified the defect with +executed-versus-named columns inside `D`, but did not split it. This package +asks which part comes from the 612 target-to-target reads and which part comes +from helper-to-helper gates (helper wraps). Card `bit-helper-contract`, scope +refined to that split. + +## Definitions + +Over GF(2), register `r` starts as column `e_r`. Helper columns are registers +`2v .. 2v+R-1` (`v = 111`, `R = 439`). + +- `K_t`: helper part of target `t` after the frame-free replay of `(A, scatter, B)`. +- `N_t`: helper columns named by `D` gates that write target `t` (the literal mask). +- `N*_t`: helper columns reaching target `t` when `D` is replayed with every + helper-to-helper gate skipped (the *target-read-closed* named mask). +- `E_t`: helper columns reaching target `t` when `D` is replayed in full. +- `T_t = N*_t + N_t`: the part carried by target-to-target reads. +- `H_t = K_t + N*_t`: the residual left by helper wraps. + +The literal defect is `K_t + N_t = T_t + H_t`. On every word below `E = K`, so +`H_t = E_t + N*_t`: exactly the extra columns that wrapped helpers deliver. + +## Result + +| word | D gates | helper gates | literal \|K+N\| | target-read \|T\| | residual \|H\| | \|T∧H\| | residual sectors = donors | sectors passing after closure | +|---|---:|---:|---:|---:|---:|---:|---:|---:| +| PR915 target basis | 723 | 0 | 17,095 | 17,095 | **0** | 0 | 0 | 439 / 439 | +| PR926 disjoint pairs | 1,107 | 384 | 17,485 | 13,148 | 7,447 | 1,555 | 192 | 247 / 439 | +| PR941 matching candidate | 1,121 | 398 | 17,514 | 13,008 | 7,786 | 1,640 | 199 | 240 / 439 | +| PR941 floor word | 1,121 | 398 | 17,505 | 12,885 | 7,776 | 1,578 | 199 | 240 / 439 | +| helper triples | 1,191 | 468 | 17,541 | 12,444 | 8,685 | 1,794 | 232 | 207 / 439 | +| PR1062 pair control | 1,099 | 376 | 17,504 | 13,110 | 7,424 | 1,515 | 188 | 251 / 439 | +| PR967 helper stars | 1,165 | 442 | 17,636 | 12,275 | 8,767 | 1,703 | 221 | 218 / 439 | +| PR1062 composition | 1,165 | 442 | 17,636 | 12,275 | 8,767 | 1,703 | 221 | 218 / 439 | +| PR1062 candidate | 1,195 | 472 | 17,653 | 12,092 | 9,163 | 1,801 | 236 | 203 / 439 | + +Bit counts satisfy `|K+N| = |T| + |H| − 2|T∧H|` on every word. Each word has +612 `D` gates that write a target and read another target. The literal defect +touches all 439 helper sectors on every word. + +What this establishes on these nine words: + +1. **Target reads, not helper mixing, account for the whole literal defect of + the helper-free base.** PR915's `D` has no helper-to-helper gate, yet its + literal defect is 17,095 bits across all 439 sectors. Closing the named mask + under target reads removes all of it: `K = N*` exactly. +2. **On every helper-mixing word, the residual support is exactly the donor + set.** Call a helper a donor when some helper-to-helper gate reads it. The + helper sectors carrying residual bits are exactly the donors: 192, 199, 199, + 232, 188, 221, 221 and 236. On the star words the donors are the 221 / 236 + star leaves and the 157 / 162 written helpers are the centres. Donors and + written helpers are disjoint except for 28 helpers in the triple word. +3. **The "every sector is defective" reading of PR #4092 comes from target + reads.** After target-read closure, 203–251 helper sectors per mixing word + satisfy the sector-local condition (no residual bit in that column). The + defect left to forgive is concentrated on donor columns: 7,424–9,163 bits, + versus 17,485–17,653 literal bits. +4. `E = K` and all 439 helpers end `D` restored on all nine words. No + non-helper column survives in any `N_t`. This extends the cross-term tally's + `E = K` certificate from three words to nine. + +## Controls + +The verifier runs six controls: + +- Two-target synthetic `y0 ^= h0; y1 ^= y0` with `K = (h0, h0)`. The literal + defect is one bit; `T` is that bit and the residual is zero. +- Restored wrap `h0 ^= h1; y ^= h0; h0 ^= h1` with semantic `K = h0 + h1`. + `E = K` and the residual is the single donor column `h1`. +- The same wrap against `K = h0` (the cross-term tally's synthetic edge). + `E ≠ K`, yet the closed mask reports **zero** residual. Thus `K = N*` alone is + **not** a sound replacement check once helper gates are present. A contract + built on `N*` must still charge or check the wraps (for example `E = K` with + restored helpers). +- Deleting the first helper-to-helper gate of the PR967 star word breaks both + `E = K` and helper restoration. +- Deleting the first helper-carrying target-to-target read of PR915 leaves a + nonzero residual, so PR915's zero residual is not a property of `K` alone. +- PR #3904's pair on the PR967 star word: target register 112, helper register + 260 (helper index 38), donor of `D` gate 0 `280 ^= 260`. The bit is in `K` and + absent from `N` and `N*`, so it lies in both the literal defect and `H`. + +## Correction to PR #4092 + +PR #4092 (`r439-star-kdefect-sectors`, same author) states that the #3904 pair +is **not** in the official W0 defect set, because the "sector of column 260" +has 57 defective targets that exclude 112. That statement is wrong. It mixed +register numbers with indices. Register 260 is helper index 38. Sector 38 has +57 defective targets, and they include target index 1, which is register 112. +#4092 searched for target index 112, which does not exist (`v = 111`). Running +#4092's own `verify.py --json` confirms this: sector `"38"` lists 57 targets +including `1`. So the #3904 pair is in the official W0 defect set, and #3904 +agrees with #4092 on it. The two do not use different raw-word definitions for +this bit. #4092's census totals, sector counts and controls are unaffected. This +package does not edit #4092's files. The sixth control above pins the corrected +fact. + +## What is not established + +This is a finite certificate on nine named words. It does not adopt `K = N*`, +`E = K` or any other replacement for `K_equals_D` or H2; the third control +shows `K = N*` alone is unsound with helper gates. The 612 target-to-target +reads remain a literal H2 read-kind failure. No frame, native schedule, hosted +invoice, all-size transfer, supplier admission or selected-frontier change is +claimed. The bit side does not bind the selected exponent. + +## Reproduce + +From the repository root, CPython 3.12, standard library only (about 0.1 s): + +```sh +python3.12 -B research/r439-target-closed-k-residual/verify.py +python3.12 scripts/research_package.py --package research/r439-target-closed-k-residual +``` + +Expected: + +```text +PASS_R439_TARGET_CLOSED_K_RESIDUAL words=9 pr915_residual=0 star_residual=8767/8767/9163 sectors_equal_donors=9/9 controls=6 no_new_kappa +``` + +`verify.py --json OUT` writes the per-word record, including target-read counts, +donor and written-helper counts and sector-pass counts. All nine inputs are +bound by SHA-256 in [SOURCES.json](SOURCES.json). + +## Open next questions + +1. **Can a donor-sector contract replace `K_equals_D` on these words?** A + candidate is "`K = N*` plus, for each restored wrap, the donor columns + delivered while the wrap is open". It would be checkable from `D` alone and + would reject the third control. First step: state it for well-nested + restored wraps and test it on the nine words and the controls. Blocker: + adopting it as the H2/K interface is a maintainer policy decision. +2. **Do target reads still fail H2 after closure?** Closing the mask removes + the K mismatch from target reads but not H2's read-kind clause. First step: + check whether the PR915 semantic substitution proof already covers + target-read closure, so the 612 reads need no separate repair. + +## Credit + +Produced by Nick Petalas. Words and predecessor results are retained unchanged +with their own attribution: Gareth Davidson (PR915 target basis, PR926 helper +pairs, `r439-helper-matching` / PR941), Ross Richardson (`r439-helper-triples`), +Sricharan Vagvala (`r439-helper-stars-seed19`, PR967 lineage), Sagar Thakrar +(PR1062 `r439-bsection-stars-seed01`), the PR4092 sector census and the +`r439-k-cross-term-tally` package. Apache-2.0. diff --git a/research/r439-target-closed-k-residual/SOURCES.json b/research/r439-target-closed-k-residual/SOURCES.json new file mode 100644 index 0000000000..0fd9b448a0 --- /dev/null +++ b/research/r439-target-closed-k-residual/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/r439-bsection-stars-seed01/candidate.json.gz", + "usage": "input", + "git_blob": "9a17b4920334878d6c949191f6931bd97126fe3c", + "sha256": "b452d2c2b0b2a546d1105b1da9769aa78e5c54d6f00e97b30c77e3f54ce445ee" + }, + { + "path": "research/r439-bsection-stars-seed01/composition.json.gz", + "usage": "input", + "git_blob": "d95fc2bf795fd9ef8d8bae9d70693c5e64948cec", + "sha256": "0203fea9fa442ca206fe683aa5b6860adac680d63b9fb8be6bd42b39aa7b5cce" + }, + { + "path": "research/r439-bsection-stars-seed01/pair_control.json.gz", + "usage": "input", + "git_blob": "16972bc96de0c81321eb2feef70766c403017016", + "sha256": "628ebfebe215e153338e88e2e324040d139a111eebfb090929697c7a0b6f3f59" + }, + { + "path": "research/r439-helper-matching/candidate.json.gz", + "usage": "input", + "git_blob": "b3befb831854157e14512ac40fa48dbea289d105", + "sha256": "60531408445a1d7c793dff6821e767739012db1d2646f49aec7fdf7fe0b979f3" + }, + { + "path": "research/r439-helper-matching/floor-word.json.gz", + "usage": "input", + "git_blob": "906e935541d6a5d2ca40d2885e21e46b4675b0ee", + "sha256": "4be50c06f91bc605660d4f9fba865c330f82dc4c364041870b725c220d16244e" + }, + { + "path": "research/r439-helper-matching/vendor/pr915/candidate.json.gz", + "usage": "input", + "git_blob": "7f1f188f516ca4661f419dc72114751abf3cc920", + "sha256": "ac30266144f8772ec8cd629153993aa9eb692fe745a9f95015a1b7fa88977a2e" + }, + { + "path": "research/r439-helper-matching/vendor/pr926/candidate.json.gz", + "usage": "input", + "git_blob": "0a192829589d6cbcec0f32695a928d24e6c33549", + "sha256": "6ac771545e823c054e005429c405dbb2c01ff80fce181b714e1af5e28b6b7cb2" + }, + { + "path": "research/r439-helper-stars-seed19/candidate.json.gz", + "usage": "input", + "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735", + "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8" + }, + { + "path": "research/r439-helper-triples/candidate.json.gz", + "usage": "input", + "git_blob": "e74d3a8edecac5ca9262b774a965702c19207bea", + "sha256": "11f5c75711090892827d536b6bf82b4001e02ebd13d10e87a1aa915a4e78704b" + } + ] +} diff --git a/research/r439-target-closed-k-residual/TASK.json b/research/r439-target-closed-k-residual/TASK.json new file mode 100644 index 0000000000..d3abae5d10 --- /dev/null +++ b/research/r439-target-closed-k-residual/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "refined", + "actual_scope": "On nine pinned R439 D words from four lineages (PR915 helper-free basis, PR926/PR941 pairs, helper triples, PR1062 pair control, three helper-star words), split the literal K_equals_D defect into the part carried by target-to-target reads and the residual left by helper-to-helper gates. Answers PR #4092 open question 2; no replacement contract is adopted.", + "scope_change_reason": "The card asks for a replacement H2/K implication or a counterexample. Before stating one, the defect it must forgive needs to be located. PR #4092 counted it and r439-k-cross-term-tally identified it with executed-versus-named columns, but neither separated target reads from helper wraps. This split shows what a helper-mixing replacement actually has to cover.", + "bottleneck_link": "Side result on the non-binding bit supplier. The selected complex side and kappa are unchanged. It narrows the defect a helper-wrap replacement for K_equals_D must forgive to the donor sectors, and shows target-read closure alone is unsound once helper gates exist.", + "budget_minutes": 60, + "stop_rule": "Stop after the nine pinned words, the exact split table, the donor-support identity and six controls. Do not adopt a contract, reprice a profile or search for new words.", + "outcome": "completed", + "evidence": "Author-checked finite certificate: PR915 residual is 0 of 17,095 literal bits; on the eight helper-mixing words the residual support equals the donor set (192-236 sectors) and 203-251 sectors pass after target-read closure. E = K and helpers restore on all nine. Verifier research/r439-target-closed-k-residual/verify.py. Also corrects PR #4092's statement that the PR3904 pair lies outside the defect set (register/index mix-up).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a donor-sector contract (K = N* plus donor columns delivered while each restored wrap is open) replace K_equals_D on these words?", + "why_it_matters": "It would be checkable from D alone, would reject the mismatched-K control that K = N* accepts, and would cover exactly the residual this package locates.", + "first_step": "State it for well-nested restored wraps and test it on the nine words and the six controls.", + "blocked_by": "Adopting it as the H2/K interface is a maintainer policy decision; the finite test has no blocker." + }, + { + "question": "Does the PR915 semantic substitution proof already cover target-read closure, so the 612 target-to-target reads need no separate H2 repair?", + "why_it_matters": "Closure removes the K mismatch from target reads but not H2's literal read-kind clause.", + "first_step": "Read PR915's PROOF.md substitution argument against the N* definition used here.", + "blocked_by": "None." + } + ] +} diff --git a/research/r439-target-closed-k-residual/VERIFY.json b/research/r439-target-closed-k-residual/VERIFY.json new file mode 100644 index 0000000000..268332a68e --- /dev/null +++ b/research/r439-target-closed-k-residual/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/r439-bsection-stars-seed01/candidate.json.gz", + "research/r439-bsection-stars-seed01/composition.json.gz", + "research/r439-bsection-stars-seed01/pair_control.json.gz", + "research/r439-helper-matching/candidate.json.gz", + "research/r439-helper-matching/floor-word.json.gz", + "research/r439-helper-matching/vendor/pr915/candidate.json.gz", + "research/r439-helper-matching/vendor/pr926/candidate.json.gz", + "research/r439-helper-stars-seed19/candidate.json.gz", + "research/r439-helper-triples/candidate.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "SHA-256 pins; exact split table on nine words; residual support equals the donor set; E equals K and helpers restore; published 17636/17653 literal totals; six controls including the unsound K = N* case; PR3904 pair located in K, N, N* (corrects PR4092's comparison)" + } + ] +} diff --git a/research/r439-target-closed-k-residual/verify.py b/research/r439-target-closed-k-residual/verify.py new file mode 100644 index 0000000000..fc8a95b006 --- /dev/null +++ b/research/r439-target-closed-k-residual/verify.py @@ -0,0 +1,302 @@ +"""Split the literal K_equals_D defect of R439 D words into target-read and helper-wrap parts. + +Scope: nine repository-pinned R439 words from four lineages (helper-free PR915 target +basis, PR926/PR941 disjoint helper pairs, PR1062 pair control, helper triples, helper +stars). Every word has v = 111 targets and R = 439 helpers (661 columns). + +Definitions, all over GF(2) with register r starting as column e_r: +- K_t helper-column part of target t after the frame-free replay of (A, scatter, B). +- N_t helper columns named by D gates that write target t (the literal mask). +- N*_t helper columns reaching target t when D is replayed with every + helper-to-helper gate skipped (target-read-closed named mask). +- E_t helper columns reaching target t when D is replayed in full. +- T_t = N*_t + N_t part carried by target-to-target reads. +- H_t = K_t + N*_t residual left by helper-to-helper gates (helper wraps). +Then the literal defect K_t + N_t equals T_t + H_t. + +Finite certificate on the nine named words only. No kappa, no contract adoption, +no supplier admission, no selected-frontier change. + +usage: python3 -B verify.py [--json OUT] +""" +import gzip +import hashlib +import json +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.abspath(os.path.join(HERE, "..", "..")) + +WORDS = ( + ("pr915", "research/r439-helper-matching/vendor/pr915/candidate.json.gz"), + ("pr926", "research/r439-helper-matching/vendor/pr926/candidate.json.gz"), + ("matching", "research/r439-helper-matching/candidate.json.gz"), + ("matching_floor", "research/r439-helper-matching/floor-word.json.gz"), + ("triples", "research/r439-helper-triples/candidate.json.gz"), + ("pr1062_pair_control", "research/r439-bsection-stars-seed01/pair_control.json.gz"), + ("helper_star", "research/r439-helper-stars-seed19/candidate.json.gz"), + ("pr1062_composition", "research/r439-bsection-stars-seed01/composition.json.gz"), + ("pr1062_candidate", "research/r439-bsection-stars-seed01/candidate.json.gz"), +) + +# Exact expected table: D gates, helper-to-helper gates, literal defect bits |K+N|, +# target-read bits |T|, residual bits |H|, overlap |T and H|, residual sectors, donors. +EXPECTED = { + "pr915": (723, 0, 17095, 17095, 0, 0, 0, 0), + "pr926": (1107, 384, 17485, 13148, 7447, 1555, 192, 192), + "matching": (1121, 398, 17514, 13008, 7786, 1640, 199, 199), + "matching_floor": (1121, 398, 17505, 12885, 7776, 1578, 199, 199), + "triples": (1191, 468, 17541, 12444, 8685, 1794, 232, 232), + "pr1062_pair_control": (1099, 376, 17504, 13110, 7424, 1515, 188, 188), + "helper_star": (1165, 442, 17636, 12275, 8767, 1703, 221, 221), + "pr1062_composition": (1165, 442, 17636, 12275, 8767, 1703, 221, 221), + "pr1062_candidate": (1195, 472, 17653, 12092, 9163, 1801, 236, 236), +} +# Literal defect totals already published by PR4092 / r439-k-cross-term-tally. +PUBLISHED_LITERAL = {"helper_star": 17636, "pr1062_composition": 17636, "pr1062_candidate": 17653} + + +def fail(msg): + print("FAIL_R439_TARGET_CLOSED_K_RESIDUAL " + msg) + sys.exit(1) + + +def check_pins(): + with open(os.path.join(HERE, "SOURCES.json")) as f: + rows = {r["path"]: r["sha256"] for r in json.load(f)["files"] if r["usage"] == "input"} + for _, path in WORDS: + with open(os.path.join(ROOT, path), "rb") as f: + if hashlib.sha256(f.read()).hexdigest() != rows[path]: + fail("sha256 mismatch " + path) + + +def popcount(x): + return bin(x).count("1") + + +def column_set(x, offset): + out = set() + i = 0 + x >>= offset + while x: + if x & 1: + out.add(i) + x >>= 1 + i += 1 + return out + + +def raw_k(w): + """Helper part K_t of each target after (A, scatter, B), frames ignored.""" + v, R = w["v"], w["R"] + val = [1 << r for r in range(2 * v + R)] + for name in ("A", "scatter", "B"): + if name == "scatter": + copies = [val[q] for q in w["ret"]] + for t, row in enumerate(w["scatter"]): + acc = 0 + for k in row: + acc ^= copies[k] + val[v + t] ^= acc + else: + for _, d, srcs in w[name]: + acc = 0 + for s in srcs: + acc ^= val[s] + val[d] ^= acc + hmask = ((1 << R) - 1) << (2 * v) + return [val[v + t] & hmask for t in range(v)] + + +def replay_d(v, R, D, skip_helper_gates): + val = [1 << r for r in range(2 * v + R)] + for _, d, srcs in D: + if skip_helper_gates and d >= 2 * v: + continue + acc = 0 + for s in srcs: + acc ^= val[s] + val[d] ^= acc + return val + + +def split(v, R, D, K): + """Return the decomposition record for one D section against helper parts K.""" + hmask = ((1 << R) - 1) << (2 * v) + N = [0] * v + for _, d, srcs in D: + if v <= d < 2 * v: + for s in srcs: + N[d - v] ^= 1 << s + nonhelper_named = sum(1 for t in range(v) if N[t] & ~hmask) + full = replay_d(v, R, D, False) + closed = replay_d(v, R, D, True) + E = [full[v + t] & hmask for t in range(v)] + Ns = [closed[v + t] & hmask for t in range(v)] + Nh = [N[t] & hmask for t in range(v)] + lit = [K[t] ^ Nh[t] for t in range(v)] + T = [Ns[t] ^ Nh[t] for t in range(v)] + H = [K[t] ^ Ns[t] for t in range(v)] + for t in range(v): + if lit[t] != T[t] ^ H[t]: + fail("decomposition identity") + sectors = set() + for x in H: + sectors |= column_set(x, 2 * v) + donors, dests = set(), set() + hh = 0 + for _, d, srcs in D: + if d >= 2 * v: + hh += 1 + dests.add(d - 2 * v) + donors |= {s - 2 * v for s in srcs if s >= 2 * v} + tt_reads = sum(1 for _, d, srcs in D if v <= d < 2 * v and any(v <= s < 2 * v for s in srcs)) + return dict( + d_gates=len(D), + helper_gates=hh, + target_reads=tt_reads, + nonhelper_named_targets=nonhelper_named, + E_equals_K=all(E[t] == K[t] for t in range(v)), + helpers_restored=all(full[r] == 1 << r for r in range(2 * v, 2 * v + R)), + literal_bits=sum(map(popcount, lit)), + target_read_bits=sum(map(popcount, T)), + residual_bits=sum(map(popcount, H)), + overlap_bits=sum(popcount(a & b) for a, b in zip(T, H)), + residual_targets=sum(1 for x in H if x), + residual_sectors=len(sectors), + donors=len(donors), + destinations=len(dests), + donor_destination_overlap=len(donors & dests), + sectors_equal_donors=sectors == donors, + sector_local_pass=R - len(sectors), + literal_sector_count=len(set().union(*(column_set(x, 2 * v) for x in lit))), + ) + + +def word_records(): + out = {} + for name, path in WORDS: + with gzip.open(os.path.join(ROOT, path)) as f: + w = json.load(f) + if (w["v"], w["R"]) != (111, 439): + fail("unexpected shape " + name) + rec = split(w["v"], w["R"], w["D"], raw_k(w)) + got = (rec["d_gates"], rec["helper_gates"], rec["literal_bits"], rec["target_read_bits"], + rec["residual_bits"], rec["overlap_bits"], rec["residual_sectors"], rec["donors"]) + if got != EXPECTED[name]: + fail("table mismatch %s %r" % (name, got)) + if not (rec["E_equals_K"] and rec["helpers_restored"] and rec["sectors_equal_donors"]): + fail("structural predicate " + name) + if rec["nonhelper_named_targets"]: + fail("non-helper column named " + name) + if name in PUBLISHED_LITERAL and rec["literal_bits"] != PUBLISHED_LITERAL[name]: + fail("published literal total " + name) + if rec["literal_bits"] != rec["target_read_bits"] + rec["residual_bits"] - 2 * rec["overlap_bits"]: + fail("bit count identity " + name) + out[name] = (rec, w) + return out + + +def controls(records): + n = 0 + # 1. Target-read closure alone: y0 ^= h0; y1 ^= y0. K = (h0, h0). Literal mask names + # nothing on y1, so the literal defect is one bit; the closed mask has no residual. + v, R = 2, 2 + h0 = 1 << 4 + rec = split(v, R, [(0, 2, [4]), (0, 3, [2])], [h0, h0]) + if (rec["literal_bits"], rec["target_read_bits"], rec["residual_bits"]) != (1, 1, 0): + fail("control target-read closure") + n += 1 + # 2. Restored helper wrap: h0 ^= h1; y ^= h0; h0 ^= h1, with semantic K = h0 + h1. + # Residual is exactly the donor column h1, and E = K. + # Registers: x0=0, y0=1, h0=2, h1=3; gates are (frame, dest, srcs). + v, R = 1, 2 + rec = split(v, R, [(0, 2, [3]), (0, 1, [2]), (0, 2, [3])], [(1 << 2) | (1 << 3)]) + if not (rec["E_equals_K"] and rec["residual_bits"] == 1 and rec["sectors_equal_donors"] + and rec["target_read_bits"] == 0): + fail("control restored wrap") + n += 1 + # 3. Same wrap against K = h0 (the tally package's synthetic edge). Executed delivery + # h0 + h1 differs from K, yet the closed mask reports zero residual. So K = N* alone + # is not a sound check once helper gates are present; E = K must still be checked. + rec = split(v, R, [(0, 2, [3]), (0, 1, [2]), (0, 2, [3])], [1 << 2]) + if rec["E_equals_K"] or rec["residual_bits"] != 0: + fail("control mismatched K") + n += 1 + # 4. Mutation on a real word: delete the first helper-to-helper gate of the star word. + # The helper is no longer restored and E no longer equals K. + _, w = records["helper_star"] + first = next(i for i, g in enumerate(w["D"]) if g[1] >= 2 * w["v"]) + D = w["D"][:first] + w["D"][first + 1:] + rec = split(w["v"], w["R"], D, raw_k(w)) + if rec["E_equals_K"] or rec["helpers_restored"]: + fail("control deleted helper gate") + n += 1 + # 5. Mutation: delete the first PR915 target-to-target read that carries helper + # columns. The closed mask then leaves a nonzero residual, so the zero residual + # is not a property of K alone. + _, w = records["pr915"] + v = w["v"] + hmask = ((1 << w["R"]) - 1) << (2 * v) + val = [1 << r for r in range(2 * v + w["R"])] + first = None + for i, (_, d, srcs) in enumerate(w["D"]): + carried = 0 + for s in srcs: + if v <= s < 2 * v: + carried ^= val[s] & hmask + if first is None and v <= d < 2 * v and carried: + first = i + acc = 0 + for s in srcs: + acc ^= val[s] + val[d] ^= acc + D = w["D"][:first] + w["D"][first + 1:] + rec = split(w["v"], w["R"], D, raw_k(w)) + if rec["residual_bits"] == 0: + fail("control deleted target read") + n += 1 + # 6. PR3904's pair on the PR967 star word: target register 112, helper register 260 + # (helper index 38), donor of D gate 0 `280 ^= 260`. The bit is in K, absent from + # N and N*, so it lies in both the literal defect and the residual H. + _, w = records["helper_star"] + v = w["v"] + t, col = 112 - v, 260 + hmask = ((1 << w["R"]) - 1) << (2 * v) + K = raw_k(w) + closed = replay_d(v, w["R"], w["D"], True) + named = 0 + for _, d, srcs in w["D"]: + if d == 112: + for s in srcs: + named ^= 1 << s + bit = lambda x: (x >> col) & 1 + if w["D"][0] != [0, 280, [260]] or (bit(K[t]), bit(named), bit(closed[112] & hmask)) != (1, 0, 0): + fail("control PR3904 pair") + n += 1 + return n + + +def main(): + out_path = None + if len(sys.argv) == 3 and sys.argv[1] == "--json": + out_path = sys.argv[2] + elif len(sys.argv) != 1: + fail("usage: verify.py [--json OUT]") + check_pins() + records = word_records() + n_controls = controls(records) + table = {name: rec for name, (rec, _) in records.items()} + if out_path: + with open(out_path, "w") as f: + json.dump(table, f, indent=1, sort_keys=True) + print("PASS_R439_TARGET_CLOSED_K_RESIDUAL words=%d pr915_residual=0 " + "star_residual=%d/%d/%d sectors_equal_donors=%d/%d controls=%d no_new_kappa" % ( + len(records), table["helper_star"]["residual_bits"], + table["pr1062_composition"]["residual_bits"], table["pr1062_candidate"]["residual_bits"], + sum(1 for r in table.values() if r["sectors_equal_donors"]), len(table), n_controls)) + + +if __name__ == "__main__": + main()