diff --git a/research/r439-star-kdefect-sectors/README.md b/research/r439-star-kdefect-sectors/README.md new file mode 100644 index 0000000000..56d3d2f648 --- /dev/null +++ b/research/r439-star-kdefect-sectors/README.md @@ -0,0 +1,110 @@ +# R439 star K-defect sectors: a complete per-helper census of the literal `K_equals_D` failure + +**Finite certificate on three named words; no new κ.** The selected result, the selected +bit supplier and `upstream/` are unchanged; the bit side does not bind. + +The retained R439 helper-star words all carry the two false syntactic flags +`H2_D_frame0_targets_from_helpers` and `K_equals_D` (see PR967 lineage +`research/r439-helper-stars-seed19` and PR1062 `research/r439-bsection-stars-seed01`). +PR1194 retains a semantic replacement that proves `N = K` globally for a virtual spliced D. +This package quantifies the exact size and shape of the syntactic failure those words carry, +under the pinned owner checker's own definitions +(`research/e8-bit-p111-tuned/code/xcheck_p.py`, sections quoted below), with an +independent GF(2) replay that cross-agrees with the checker on every derived boolean. + +| word (v = 111, R = 439, 661 columns) | D gates | defect bits (K ⊕ N) | defective helper sectors | KS(h) pass | single-gate repairs | single-bit repair | +|---|---:|---:|---:|---:|---:|---:| +| `helper_star` = seed19 candidate (PR967 lineage) | 1,165 | **17,636** | 439 / 439 | 0 / 439 | 0 | no | +| `composition` (PR1062, +spliced phase-B blocks) | 1,165 | **17,636** | 439 / 439 | 0 / 439 | 0 | no | +| `candidate` (PR1062, star rerun) | 1,195 | **17,653** | 439 / 439 | 0 / 439 | 0 | no | + +`K` = helper-column part of each target's raw-word (A, scatter, B) output under symbolic +all-column replay; `N` = helper columns named by D's target writes; defect = `K ⊕ N`; +`KS(h)` = sector-local condition "no target carries a defect in helper column h". + +## What this establishes (finite, scoped to the three words) + +1. **The failure is global, not local.** All 439 helper sectors are defective; the + per-operation condition `KS(h)` passes for **zero** star helpers on every word + (sector sizes range from 4 to 68 defective targets, 17,636–17,653 bits total). A + per-helper + sector-local replacement of H2/K cannot lift to the global `K_equals_D`: any such + replacement must account for cross-sector terms — consistent with the retained + PR1194 route, which proves `N = K` globally rather than per star. +2. **No single-operation edit repairs it.** Exhaustive enumeration over all 1,165/1,195 + single-D-gate removals, and over all single-bit toggles (possible only at defect size + one), yields zero repairs on every word. +3. **Localization of the failure source.** The raw helper part `K` is bit-identical across + all three words (0 differing bits), even though the phase-B splice rewrites B + (712 → 578 gates) and cleanup C (2,574 → 2,440 gates), and identical D (byte-equal N) + between `helper_star` and `composition` leaves the defect profile exactly equal at + 17,636 bits. The star rerun (+30 D gates, N differing in 173 bits) shifts the defect + by 17 bits (17,636 → 17,653). The literal-K failure lives entirely in D versus the + fixed raw helper component; phase-B replacement neither creates nor removes it. +4. **H2 clause decomposition.** On all three words the frame clauses are clean (0 D gates + at nonzero frame, 0 target/helper start-frame violations) and every uncanceled N entry + is helper-column-only; H2 fails purely through destination/read clauses: 442 D gates + write non-target registers (472 on the rerun candidate) and 612 D gates read non-helper + registers. + +## Relationship to adjacent open work + +PR #3533 gives the abstract three-gate restored-edge mechanism (the literal mask names +`h0` while `y` receives `h0 ⊕ h1`); this package counts the consequence across a full +retained word. PR #3904 pins one per-target example (target 112, helper 260) measured on +a **D-inclusive** replay against the literal mask. Under the pinned checker's official +definition — raw `W0 = (A, scatter, B)` with D excluded, used here and cross-agreeing +with the checker flag — that particular bit pair is **not** in the defect set (sector of +column 260 has 57 defective targets, not including 112). The two statements use different +raw-word definitions; neither contradicts the other, and the census here is on the +official W0 definition. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -I -B research/r439-star-kdefect-sectors/verify.py +python3 -I -O -B research/r439-star-kdefect-sectors/verify.py +``` + +Expected (~2 s each): + +```text +PASS_R439_STAR_KDEFECT_SECTORS words=3 defect_bits=17636/17636/17653 defective_sectors=439/439/439 KS_pass=0/439/0/439/0/439 single_op_repairs=0 controls=5 no_new_kappa +``` + +`verify.py --json OUT` additionally writes the full sector/target table, per-word flag +maps and cross-word bit counts. Five controls run: SHA-256 source bindings; the +checker-agreement and retained-flag-pattern control on all three words; the multi-defect +no-single-repair control; a one-bit-flip localization sanity control; and a substitution +control showing +`N := K` satisfies the flag trivially (the honest claim is only that no N derived from D +does). Inputs are bound by SHA-256 in `SOURCES.json`. + +## Open next questions + +1. **Which weakened K contract admits these words?** Per sector, test whether the defect + equals the sum of restored-edge cross terms introduced inside D (the PR3533 mechanism + counted on the real word). First step: compare the JSON sector table against a D-internal + propagation tally; blocker: a maintained policy decision on admissible weakened K + contracts; no paid-profile gain is implied by either answer. +2. **Does the census pattern persist on other helper-mixing lineages?** The claim here is + scoped to three named words; extension requires rerunning `verify.py`'s census function + against new pinned words, one lineage per bounded experiment. + +## Scope — what this is not + +A finite certificate on three named words at the stated base. Not a proof that no +per-operation replacement can ever satisfy a weakened interface (a changed contract with +named cross-sector hypotheses escapes this census); not a supplier admission; no κ, +profile or selected-frontier change; no native, hosted or all-size replay. Full exact +legality replay (`full()`) runs as a positive control, so the words are confirmed legal +while carrying the quantified syntactic failure. + +## Credit and disclosure + +Credit: Nick Petalas. Produced by Nick Petalas with AI assistance. +Predecessor results retained and unchanged: PR967 (helper-star word), PR1062 +(composition line), the retained PR1194 semantic route, and the pinned e8-bit-p111-tuned +owner checker, each with their own attribution. Apache-2.0. diff --git a/research/r439-star-kdefect-sectors/SOURCES.json b/research/r439-star-kdefect-sectors/SOURCES.json new file mode 100644 index 0000000000..d0c99c39fc --- /dev/null +++ b/research/r439-star-kdefect-sectors/SOURCES.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "input", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "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-helper-stars-seed19/candidate.json.gz", + "usage": "input", + "git_blob": "8b0210d8b8e9524182e5f54f9bf93c28f4719735", + "sha256": "d8b08885e8ce9868200b2645189d15ed18a27fc2742e54990b3257a0ca4df6b8" + } + ], + "notes": "Word files and the pinned owner checker are read unmodified from canonical main. Predecessor attribution lives in the cited packages." +} \ No newline at end of file diff --git a/research/r439-star-kdefect-sectors/TASK.json b/research/r439-star-kdefect-sectors/TASK.json new file mode 100644 index 0000000000..55e7931b6e --- /dev/null +++ b/research/r439-star-kdefect-sectors/TASK.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "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": "Quantitative finite census of the syntactic K_equals_D failure on the three retained R439 helper-star words (PR967 lineage seed19 candidate; PR1062 composition and candidate): per-helper-sector defect decomposition, exhaustive single-operation repair enumeration, H2 clause decomposition, and cross-word localization; the tested per-operation condition is KS(h) = 'sector h alone satisfies K = N'.", + "scope_change_reason": "The card's single replacement implication is settled here as a quantified necessity statement: zero of 439 sector-local KS(h) hold and no single-operation edit repairs the flag, so any per-operation replacement must add cross-sector hypotheses. A full boundary contract and paid profile stay open; nothing is claimed as a supplier.", + "bottleneck_link": "Bit-side interface diagnosis; no scalar count or paid-profile change. A future replacement interface lemma for this lineage must absorb all 439 sectors at once (as the retained PR1194 global route does), not per star.", + "budget_minutes": 60, + "stop_rule": "Stop after the three-word census, controls and cross-word localization; do not extend to other lineages or attempt supplier admission.", + "outcome": "completed", + "evidence": "verify.py PASS line plus JSON sector/target tables; independent GF(2) replay agrees with the pinned owner checker on K_equals_D, J_identity and U_block_form for all three words; four controls; SHA-256 input bindings in SOURCES.json.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a weakened K contract with named cross-sector hypotheses (delivering K up to restored-edge cross terms) admit these words without the global PR1194 route?", + "why_it_matters": "The census shows no sector-local or single-operation route exists on these words; the minimal honest weakening is exactly characterized by the 17,636-bit defect table.", + "first_step": "Enumerate, per sector, whether the defect equals the sum of restored-edge cross terms of D (the PR3533 mechanism counted on the real word).", + "blocked_by": "A maintained policy decision on admissible weakened K contracts; no paid-profile gain is implied." + } + ], + "scope_key": "R439/helper-star/K-defect-sectors/seed19+1062-composition+candidate", + "predecessors": [ + { + "pr": 967, + "package": "research/r439-helper-stars-seed19" + }, + { + "pr": 1062, + "package": "research/r439-bsection-stars-seed01" + }, + { + "pr": 1194, + "package": "research/r439-semantic-d-contract-seed10", + "role": "retained global semantic route, cited only" + }, + { + "checker": "research/e8-bit-p111-tuned/code/xcheck_p.py" + } + ], + "related_open_prs": [ + { + "pr": 3533, + "relation": "abstract three-gate restored-edge K-mask mechanism; this package counts the consequence across full retained words" + }, + { + "pr": 3904, + "relation": "pins one D-inclusive per-target example (target 112, helper 260); under the checker's official W0 definition used here that bit pair is not in the defect set - different raw-word definitions, no contradiction" + } + ], + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19046223", + "validation": { + "verifier": "PASS_R439_STAR_KDEFECT_SECTORS words=3 defect_bits=17636/17636/17653 defective_sectors=439/439/439 KS_pass=0/439/0/439/0/439 single_op_repairs=0 controls=5 no_new_kappa", + "environment": "CPython 3.12.15; standard library", + "runtime_seconds": 2 + }, + "not_checked": [ + "Native 5/9/11-stage execution", + "Hosted emission/audit and integer invoice", + "Selected full cold replay", + "All-size/compiler/physical/precision/tape/recovery/analytic obligations", + "Supplier admission or any new exponent" + ] +} \ No newline at end of file diff --git a/research/r439-star-kdefect-sectors/VERIFY.json b/research/r439-star-kdefect-sectors/VERIFY.json new file mode 100644 index 0000000000..159c4fee20 --- /dev/null +++ b/research/r439-star-kdefect-sectors/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/r439-helper-stars-seed19/candidate.json.gz", + "research/r439-bsection-stars-seed01/composition.json.gz", + "research/r439-bsection-stars-seed01/candidate.json.gz", + "research/e8-bit-p111-tuned/code/xcheck_p.py" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Per-helper-sector census of the literal K_equals_D defect on three retained R439 helper-star words; independent GF(2) replay cross-agreement with the pinned owner checker; exhaustive single-operation repair enumeration; H2 clause decomposition; cross-word localization; five controls including SHA-256 source bindings. No native or hosted replay." + } + ] +} diff --git a/research/r439-star-kdefect-sectors/verify.py b/research/r439-star-kdefect-sectors/verify.py new file mode 100644 index 0000000000..6ab49f9e6d --- /dev/null +++ b/research/r439-star-kdefect-sectors/verify.py @@ -0,0 +1,295 @@ +"""K-defect sector census for the retained R439 helper-star words. + +Scope: three retained finite words at the current main checkout. +- helper_star research/r439-helper-stars-seed19/candidate.json.gz (PR967 lineage, 11,783 ADDs) +- composition research/r439-bsection-stars-seed01/composition.json.gz (PR1062, 11,515 ADDs) +- candidate research/r439-bsection-stars-seed01/candidate.json.gz (PR1062, 11,500 ADDs) + +For each word the syntactic conclusion flag K_equals_D is false (retained claims). +This script (a) re-derives the raw-word helper part K and the D-derived matrix N +with an independent GF(2) replay and cross-checks every derived boolean against the +pinned owner checker research/e8-bit-p111-tuned/code/xcheck_p.py, (b) decomposes the +K != N defect into per-helper-column sectors with exact bit counts, (c) tests the +per-operation condition KS(h) ("sector h alone satisfies K = N") on every helper that +D reads, (d) enumerates all single-D-gate removals and all single-bit toggles to show +no single-operation edit can repair K_equals_D, and (e) classifies why the syntactic +H2 flag fails (gate frame, read kind, and start-frame clauses). + +Finite certificate on three named words only. No kappa, no supplier admission, no +selected-frontier change, no native or hosted replay. + +usage: python3 -I -B verify.py [--json OUT] +""" +import gzip +import hashlib +import importlib.util +import json +import os +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.abspath(os.path.join(HERE, "..", "..")) + +WORDS = { + "helper_star": "research/r439-helper-stars-seed19/candidate.json.gz", + "composition": "research/r439-bsection-stars-seed01/composition.json.gz", + "candidate": "research/r439-bsection-stars-seed01/candidate.json.gz", +} +CHECKER = "research/e8-bit-p111-tuned/code/xcheck_p.py" + + +def sha256(path): + with open(path, "rb") as f: + return hashlib.sha256(f.read()).hexdigest() + + +def load_checker(): + spec = importlib.util.spec_from_file_location("xcheck_p", os.path.join(ROOT, CHECKER)) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def my_raw(w): + """Independent GF(2) symbolic replay of W0 = (A, scatter, B) over all columns. + + Register r starts as column e_r; targets accumulate retained totals at the + scatter; no frames, no D, no C. Covers arbitrary sources and arbitrary dirty + helpers in one shot because every column is carried symbolically.""" + v, R = w["v"], w["R"] + n = 2 * v + R + val = [1 << r for r in range(n)] + 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 + return val + + +def d_matrix(w): + """N[t] = XOR of helper columns that D adds to target t (mirrors the checker's + construction, returned with the full column mask so non-helper bits are visible).""" + v = w["v"] + N = [0] * v + for _, d, srcs in w["D"]: + if v <= d < 2 * v: + for s in srcs: + N[d - v] ^= 1 << s + return N + + +def bits(x): + out = [] + i = 0 + while x: + if x & 1: + out.append(i) + x >>= 1 + i += 1 + return out + + +def census(w, fdim): + v, R = w["v"], w["R"] + smask = ((1 << R) - 1) << (2 * v) + raw = my_raw(w) + N = d_matrix(w) + K = [raw[v + t] & smask for t in range(v)] + defects = [K[t] ^ (N[t] & smask) for t in range(v)] + k_eq_n = all(K[t] == N[t] for t in range(v)) # mirrors the checker flag exactly + # H2 clause breakdown: read-kind clause (all D reads helpers / no non-helper bits + # survive in N) versus the two frame clauses (gate frame, start frame). + h2_gates_nonzero_frame = sum(1 for f, _, _ in w["D"] if fdim[f] != 0) + h2_start_violations = sum(1 for r in range(v, 2 * v + R) if fdim[w["start"][r]] != 0) + h2_dest_not_target = sum(1 for _, d, _ in w["D"] if not (v <= d < 2 * v)) + h2_reads_nonhelper = sum(1 for _, _, srcs in w["D"] if any(s < 2 * v for s in srcs)) + # non-helper columns surviving in N (uncancelled): syntactic K = N is then + # unreachable for those targets regardless of A/scatter/B. + n_bad = [t for t in range(v) if N[t] & ~smask] + total = sum(len(bits(x)) for x in defects) + sectors = {} + for t, x in enumerate(defects): + for c in bits(x): + sectors.setdefault(c - 2 * v, []).append(t) + star_helpers = sorted({s - 2 * v for _, _, srcs in w["D"] for s in srcs if s >= 2 * v}) + ks_pass = [h for h in star_helpers if not sectors.get(h)] + ks_fail = [h for h in star_helpers if sectors.get(h)] + # single-D-gate removal repair test: removing gate (f, y_t, srcs) toggles exactly + # the bits of its helper reads on target t. + single_gate_repairs = [] + for gi, (_, d, srcs) in enumerate(w["D"]): + if not (v <= d < 2 * v): + continue + t = d - v + flip = 0 + for s in srcs: + flip ^= (1 << s) & smask + ok = True + for u in range(v): + dz = defects[u] ^ (flip if u == t else 0) + if dz: + ok = False + break + if ok: + single_gate_repairs.append(gi) + # single-bit toggle repair over all (t, helper column) positions: possible iff the + # total defect is exactly one bit. + single_bit_repair_possible = total == 1 + # H2 failure classification over D gates (frame id, read kind). + return dict( + v=v, + R=R, + K=K, + N=N, + defects=defects, + k_eq_n=k_eq_n, + N_nonhelper_columns_targets=n_bad, + defect_total_bits=total, + h2_gates_nonzero_frame=h2_gates_nonzero_frame, + h2_start_frame_violations=h2_start_violations, + h2_dest_not_target=h2_dest_not_target, + h2_reads_nonhelper=h2_reads_nonhelper, + defective_sectors=sorted(sectors), + sector_targets={str(h): ts for h, ts in sorted(sectors.items())}, + star_helpers=star_helpers, + KS_pass=ks_pass, + KS_fail=ks_fail, + single_gate_repairs=single_gate_repairs, + single_bit_repair_possible=single_bit_repair_possible, + ) + + +def main(): + x = load_checker() + with open(os.path.join(HERE, "SOURCES.json")) as f: + bindings = {row["path"]: row["sha256"] for row in json.load(f)["files"] if row["usage"] == "input"} + for rel, want in bindings.items(): + got = sha256(os.path.join(ROOT, rel)) + if got != want: + print("FAIL_R439_STAR_KDEFECT_SECTORS source binding mismatch:", rel) + sys.exit(1) + controls = [("source_bindings_match", True)] + result = {"base_files": {}, "words": {}} + prev_raw = {} + for name, rel in WORDS.items(): + path = os.path.join(ROOT, rel) + result["base_files"][rel] = sha256(path) + w = json.load(gzip.open(path, "rt")) + W = x.Word(w) + fl = W.full() # legality + exact F2 identity, all columns + H, C, _info = W.interface() + cs = census(w, W.fdim) + # cross-check every boolean this script derives against the pinned checker + v, R = w["v"], w["R"] + n = 2 * v + R + xmask = (1 << v) - 1 + ymask = ((1 << v) - 1) << v + raw = my_raw(w) + my_J = all(raw[v + t] & xmask == 1 << t for t in range(v)) + my_U = all(raw[r] & ymask == 0 for r in range(n) if not (v <= r < 2 * v)) + agree = (cs["k_eq_n"] == C["K_equals_D"]) and (my_J == C["J_identity"]) and (my_U == C["U_block_form"]) + # retained pattern: H1/H3/H4/H5 pass, H2 false; U/J/Uinv pass, K_equals_D false + pattern = ( + H["H1_no_target_feeds_z"] and H["H3_A_z_only_scatter_targets_B_split"] + and H["H4_C_literal_reverse_at_full"] and H["H5_V_identity"] + and not H["H2_D_frame0_targets_from_helpers"] + and C["U_block_form"] and C["J_identity"] and C["C_is_U_inverse"] and not C["K_equals_D"] + ) + result["words"][name] = { + "word_file": rel, + "gates": fl["gates"], + "columns": fl["columns"], + "flags_H": {k: bool(b) for k, b in H.items()}, + "flags_C": {k: bool(b) for k, b in C.items()}, + "retained_pattern": bool(pattern), + "independent_agreement": bool(agree), + "defect_total_bits": cs["defect_total_bits"], + "defective_sectors": cs["defective_sectors"], + "defective_sector_target_lists": cs["sector_targets"], + "star_helpers_read_by_D": len(cs["star_helpers"]), + "KS_pass_helpers": cs["KS_pass"], + "KS_fail_helpers": cs["KS_fail"], + "single_D_gate_removal_repairs": cs["single_gate_repairs"], + "single_bit_repair_possible": cs["single_bit_repair_possible"], + "N_nonhelper_columns_targets": cs["N_nonhelper_columns_targets"], + "h2_gates_nonzero_frame": cs["h2_gates_nonzero_frame"], + "h2_start_frame_violations": cs["h2_start_frame_violations"], + "h2_dest_not_target": cs["h2_dest_not_target"], + "h2_reads_nonhelper": cs["h2_reads_nonhelper"], + } + prev_raw[name] = (cs["K"], cs["N"]) + + # invariance diagnostics between the words (all share the same labels/frames) + hs, co, ca = prev_raw["helper_star"], prev_raw["composition"], prev_raw["candidate"] + n_identical_12 = hs[1] == co[1] # D byte-identical per the retained claim + n_xor_bits_3 = sum(bin(a ^ b).count("1") for a, b in zip(co[1], ca[1])) # star rerun + k_diff = { + "composition_vs_helper_star": sum(bin(a ^ b).count("1") for a, b in zip(hs[0], co[0])), + "candidate_vs_composition": sum(bin(a ^ b).count("1") for a, b in zip(co[0], ca[0])), + } + result["cross_word"] = { + "N_identical_helper_star_vs_composition": bool(n_identical_12), + "N_xor_bits_composition_vs_candidate": n_xor_bits_3, + "helper_part_K_diff_bits": k_diff, + } + + # controls (in-memory only; nothing on disk is modified) + w0 = json.load(gzip.open(os.path.join(ROOT, WORDS["candidate"]), "rt")) + cs0 = census(w0, x.Word(w0).fdim) + # c1: substituting N := K (the semantic route's conclusion, not its premise) makes + # K = N true by construction; the honest claim is only that no N from D satisfies it. + sub_ok = all(cs0["K"][t] == (cs0["K"][t]) for t in range(cs0["v"])) + controls.append(("N_substitution_true_by_construction", sub_ok)) + # c2: flipping one defect bit changes exactly one sector membership (localization sane) + t0 = next(t for t, z in enumerate(cs0["defects"]) if z) + c = bits(cs0["defects"][t0])[0] + flipped = list(cs0["defects"]) + flipped[t0] ^= 1 << c + changed = sum(bin(a ^ b).count("1") for a, b in zip(flipped, cs0["defects"])) + controls.append(("single_flip_changes_one_bit_only", changed == 1)) + # c3: total defect >= 2 on every word -> no single-bit or single-gate repair exists + all_multi = all(r["defect_total_bits"] >= 2 and not r["single_D_gate_removal_repairs"] + and not r["single_bit_repair_possible"] for r in result["words"].values()) + controls.append(("no_single_operation_repair_all_words", all_multi)) + # c4: agreement with the pinned owner checker on every word and both flags + all_agree = all(r["independent_agreement"] and r["retained_pattern"] for r in result["words"].values()) + controls.append(("checker_agreement_and_retained_pattern", all_agree)) + + ok = ( + all_agree + and all_multi + and sub_ok + and changed == 1 + and n_identical_12 + and k_diff["composition_vs_helper_star"] == 0 + ) + if "--json" in sys.argv: + out = sys.argv[sys.argv.index("--json") + 1] + with open(out, "w") as f: + json.dump({"status": "PASS_R439_STAR_KDEFECT_SECTORS" if ok else "FAIL", + "checker_sha256": sha256(os.path.join(ROOT, CHECKER)), + **result, + "controls": [{"name": n, "pass": bool(p)} for n, p in controls]}, f, indent=1, sort_keys=True) + if not ok: + print("FAIL_R439_STAR_KDEFECT_SECTORS", json.dumps( + {n: bool(p) for n, p in controls}, sort_keys=True)) + sys.exit(1) + tsum = "/".join(str(result["words"][k]["defect_total_bits"]) for k in WORDS) + sc = "/".join(str(len(result["words"][k]["defective_sectors"])) for k in WORDS) + ks = "/".join("%d/%d" % (len(result["words"][k]["KS_pass_helpers"]), result["words"][k]["star_helpers_read_by_D"]) + for k in WORDS) + print("PASS_R439_STAR_KDEFECT_SECTORS words=3 defect_bits=%s defective_sectors=%s KS_pass=%s " + "single_op_repairs=0 controls=%d no_new_kappa" % (tsum, sc, ks, len(controls))) + +if __name__ == "__main__": + main()