From 117c48527dd4f066dad103121761154cf1bb39cd Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Tue, 13 Oct 2026 04:47:48 -0400 Subject: [PATCH] Research construction: shorten R439 phase-B block 508 from 37 to 30 ADDs (no new kappa) --- .../r439-block508-schedule/CANDIDATE.json | 234 ++++++++++ .../r439-block508-schedule/CERTIFICATE.json | 255 +++++++++++ research/r439-block508-schedule/CLAIM.md | 43 ++ research/r439-block508-schedule/EXPECTED.json | 86 ++++ research/r439-block508-schedule/README.md | 80 ++++ research/r439-block508-schedule/SOURCES.json | 10 + research/r439-block508-schedule/VALIDATION.md | 51 +++ research/r439-block508-schedule/search.py | 145 ++++++ research/r439-block508-schedule/verify.py | 416 ++++++++++++++++++ 9 files changed, 1320 insertions(+) create mode 100644 research/r439-block508-schedule/CANDIDATE.json create mode 100644 research/r439-block508-schedule/CERTIFICATE.json create mode 100644 research/r439-block508-schedule/CLAIM.md create mode 100644 research/r439-block508-schedule/EXPECTED.json create mode 100644 research/r439-block508-schedule/README.md create mode 100644 research/r439-block508-schedule/SOURCES.json create mode 100644 research/r439-block508-schedule/VALIDATION.md create mode 100644 research/r439-block508-schedule/search.py create mode 100644 research/r439-block508-schedule/verify.py diff --git a/research/r439-block508-schedule/CANDIDATE.json b/research/r439-block508-schedule/CANDIDATE.json new file mode 100644 index 0000000000..f490db75ba --- /dev/null +++ b/research/r439-block508-schedule/CANDIDATE.json @@ -0,0 +1,234 @@ +{ + "frame": 508, + "gates": [ + [ + 508, + 66, + [ + 19 + ] + ], + [ + 508, + 66, + [ + 35 + ] + ], + [ + 508, + 66, + [ + 43 + ] + ], + [ + 508, + 66, + [ + 57 + ] + ], + [ + 508, + 66, + [ + 65 + ] + ], + [ + 508, + 66, + [ + 74 + ] + ], + [ + 508, + 66, + [ + 97 + ] + ], + [ + 508, + 89, + [ + 19 + ] + ], + [ + 508, + 89, + [ + 27 + ] + ], + [ + 508, + 89, + [ + 35 + ] + ], + [ + 508, + 89, + [ + 43 + ] + ], + [ + 508, + 89, + [ + 74 + ] + ], + [ + 508, + 89, + [ + 97 + ] + ], + [ + 508, + 466, + [ + 43 + ] + ], + [ + 508, + 466, + [ + 66 + ] + ], + [ + 508, + 466, + [ + 89 + ] + ], + [ + 508, + 466, + [ + 97 + ] + ], + [ + 508, + 43, + [ + 19 + ] + ], + [ + 508, + 43, + [ + 66 + ] + ], + [ + 508, + 43, + [ + 89 + ] + ], + [ + 508, + 43, + [ + 97 + ] + ], + [ + 508, + 74, + [ + 43 + ] + ], + [ + 508, + 35, + [ + 27 + ] + ], + [ + 508, + 35, + [ + 74 + ] + ], + [ + 508, + 35, + [ + 97 + ] + ], + [ + 508, + 27, + [ + 66 + ] + ], + [ + 508, + 57, + [ + 89 + ] + ], + [ + 508, + 65, + [ + 89 + ] + ], + [ + 508, + 97, + [ + 19 + ] + ], + [ + 508, + 97, + [ + 27 + ] + ] + ], + "minimum": 30, + "original_gates": 37, + "registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ], + "slice": [ + 205, + 242 + ] +} diff --git a/research/r439-block508-schedule/CERTIFICATE.json b/research/r439-block508-schedule/CERTIFICATE.json new file mode 100644 index 0000000000..65b4e81a6e --- /dev/null +++ b/research/r439-block508-schedule/CERTIFICATE.json @@ -0,0 +1,255 @@ +{ + "backward_optimality": { + "backward_distances_sha256": "939856f3366b7012aeb1e08a2038bb7deef926a85c0155891a186fa036a49b5e", + "feasible_edges": 4376, + "minimum": 30, + "state_destination_pairs": 11264, + "states": 2048 + }, + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "binding": { + "block": 508, + "frame": 508, + "registers": [ + 19, + 27, + 35, + 43, + 57, + 65, + 66, + 74, + 89, + 97, + 466 + ], + "section": "B", + "slice": [ + 205, + 242 + ], + "source": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + }, + "forward_minimum": 30, + "forward_total": 129, + "gates": [ + [ + 508, + 66, + [ + 19 + ] + ], + [ + 508, + 66, + [ + 35 + ] + ], + [ + 508, + 66, + [ + 43 + ] + ], + [ + 508, + 66, + [ + 57 + ] + ], + [ + 508, + 66, + [ + 65 + ] + ], + [ + 508, + 66, + [ + 74 + ] + ], + [ + 508, + 66, + [ + 97 + ] + ], + [ + 508, + 89, + [ + 19 + ] + ], + [ + 508, + 89, + [ + 27 + ] + ], + [ + 508, + 89, + [ + 35 + ] + ], + [ + 508, + 89, + [ + 43 + ] + ], + [ + 508, + 89, + [ + 74 + ] + ], + [ + 508, + 89, + [ + 97 + ] + ], + [ + 508, + 466, + [ + 43 + ] + ], + [ + 508, + 466, + [ + 66 + ] + ], + [ + 508, + 466, + [ + 89 + ] + ], + [ + 508, + 466, + [ + 97 + ] + ], + [ + 508, + 43, + [ + 19 + ] + ], + [ + 508, + 43, + [ + 66 + ] + ], + [ + 508, + 43, + [ + 89 + ] + ], + [ + 508, + 43, + [ + 97 + ] + ], + [ + 508, + 74, + [ + 43 + ] + ], + [ + 508, + 35, + [ + 27 + ] + ], + [ + 508, + 35, + [ + 74 + ] + ], + [ + 508, + 35, + [ + 97 + ] + ], + [ + 508, + 27, + [ + 66 + ] + ], + [ + 508, + 57, + [ + 89 + ] + ], + [ + 508, + 65, + [ + 89 + ] + ], + [ + 508, + 97, + [ + 19 + ] + ], + [ + 508, + 97, + [ + 27 + ] + ] + ], + "original_gates": 37, + "schema": "r439-block508-schedule/1", + "source_sha256": { + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + "supplier_head_589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46" +} diff --git a/research/r439-block508-schedule/CLAIM.md b/research/r439-block508-schedule/CLAIM.md new file mode 100644 index 0000000000..ba51149785 --- /dev/null +++ b/research/r439-block508-schedule/CLAIM.md @@ -0,0 +1,43 @@ +# Sprint claim (local; no pinned coordination issue exists) + +- Track: bit supplier (00-19). OS-random assignment seed: **5** + (RNGCryptoServiceProvider, mod 100). A non-crypto shell draw returned 76 + first and was discarded in favor of the OS-random draw per the task spec. +- Base commit: `f567884aeb8851b6e794af1184119a3bfbe1e631` +- Object: tuned R439 phase-B block at frame 508 (`B[205:242]`, 37 gates, + registers `[19, 27, 35, 43, 57, 65, 66, 74, 89, 97, 466]`). +- Method: exact whole-block single-write rescheduling; forward discovery DP + plus independent backward-DP minimum certificate; full local exact + verification (integer maps, Boolean tables, splice + literal cleanup, + frame paths, paid profile, 661-column endpoint, H1-H5, exported bills). +- Deliverable: `research/r439-block508-schedule/` with `verify.py` (one + reproducible command, stdlib only). +- Expected finish: within the session; status: **complete**. + +## Selection trail (three candidates, seed-diversified) + +1. Block 522 (43 gates): single-write class infeasible (outputs 29/106 + exclude the hub total while every shareable compound includes it), so no + layered rescheduling can realize it; beating 43 requires multi-write + interleaving. Not pursued as a construction. +2. Block 521 (47 gates, largest): same infeasibility result. Not pursued. +3. Block 508 (37 gates): whole-block single-write minimum is 30 with an + achieving witness. **Selected.** + +The choice pivots once, on this evidence, from the seed-shortlisted block 522 +to block 508. Related open work inspected before claiming: #843 (frame 509 +sum reuse), #844 (block 4 fixed-factor schedule), #857 (block 8 integer +factorization), #728/#792 (phase-A mini-nodes, different section; their +frame-507/508 no-improvement statement covers mini-nodes only), #867 +(selected-source coverage audit, different track). None covers the B-section +block at frame 508. + +## Result + +Construction complete, no new kappa: 37 -> 30 block additions, 24,305 -> +24,291 complete ADDs, forward positive bound equal (49,347), reverse bound +reduced (1,113,070 -> 1,086,054), payload 93 bits, paid profile and rank mass +unchanged, minimum 30 certified by two independent DP implementations. +`verify.py` passes in normal, optimized (`-O`) and isolated (`-I`) modes. +Native C++ replay, hosted invoice, global assembly, Lean and remote CI remain +open obligations, recorded in README.md. diff --git a/research/r439-block508-schedule/EXPECTED.json b/research/r439-block508-schedule/EXPECTED.json new file mode 100644 index 0000000000..8d9925d8d0 --- /dev/null +++ b/research/r439-block508-schedule/EXPECTED.json @@ -0,0 +1,86 @@ +{ + "adds_saved": 14, + "after": { + "adds": 24291, + "copies": 9, + "erasures": 9, + "forward_positive_bound": 49347, + "payload_bits": 93, + "record_sha256": "b75649641476366d4f8766cf6168121ab7f00cfa7f4df499a95212eb18e54129", + "records": 27220, + "reverse_positive_bound": 1086054 + }, + "backward_optimality": { + "backward_distances_sha256": "939856f3366b7012aeb1e08a2038bb7deef926a85c0155891a186fa036a49b5e", + "feasible_edges": 4376, + "minimum": 30, + "state_destination_pairs": 11264, + "states": 2048 + }, + "before": { + "adds": 24305, + "copies": 9, + "erasures": 9, + "forward_positive_bound": 49347, + "payload_bits": 93, + "record_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a", + "records": 27234, + "reverse_positive_bound": 1113070 + }, + "block": { + "boolean_inputs_checked": 2048, + "reverse_new_total": 87, + "reverse_old_total": 169, + "reverse_strictly_smaller_entries": 20 + }, + "closed_frames": 636, + "columns": 661, + "conclusion": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": true, + "U_block_form": true + }, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "identical_register_frame_paths": 661, + "negative_controls": [ + "mutated_candidate_source", + "unpaid_gate", + "inverted_domination", + "omitted_cleanup", + "missing_gate_with_matching_cleanup", + "illegal_frame_descent", + "stale_cleanup_literal_H4", + "wrong_slice_binding" + ], + "new_kappa_claim": false, + "paid_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "status": "PASS_R439_BLOCK508_SCHEDULE", + "word_sha256": "5a8d0e42ca5ac00269e1589a16fe992ced14a671baddca29244a11410c0ecc90" +} diff --git a/research/r439-block508-schedule/README.md b/research/r439-block508-schedule/README.md new file mode 100644 index 0000000000..56106bfae1 --- /dev/null +++ b/research/r439-block508-schedule/README.md @@ -0,0 +1,80 @@ +# R439 phase-B block 508: 37 to 30 additions (no new kappa) + +Finite bit-supplier construction. The tuned R439 phase-B block at frame 508 +(`B[205:242]` of `research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`, +registers `[19, 27, 35, 43, 57, 65, 66, 74, 89, 97, 466]`) is replaced with a +30-addition program computing the identical forward integer map. Rebuilding its +literal reverse cleanup reduces the complete native word from **24,305 to +24,291 ADDs** (7 forward + 7 reverse). + +| Quantity | Before | After | +|---|---:|---:| +| Block additions (frame 508) | 37 | **30** | +| Complete exported ADDs | 24,305 | **24,291** | +| Forward positive bound | 49,347 | 49,347 (equal) | +| Reverse positive bound | 1,113,070 | **1,086,054** | +| Payload | 93 bits | 93 bits (cap 104) | +| Local paid profile / rank mass | `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}` / 5,129 | unchanged | +| Bit saving / kappa | conditional, complex-bound | unchanged, no new kappa | + +## Method + +The block is treated as an integer-linear straight-line program over its 11 +registers. Discovery (`search.py`, deterministic, no randomness) runs a +forward dynamic program over realized-register subsets: each register is +realized once, in some order, from already-realized rows or entry singletons, +each donor used at most once (doubling-free positive-addition class). The +minimum is 30 and the recovered witness achieves it. + +Verification (`verify.py`, imports no search code) rechecks the minimum with an +independently written backward Bellman recursion: 2,048 states, 11,264 +state/destination pairs, 4,376 feasible edges, minimum 30. It further checks +forward integer-map equality, reverse-map entrywise domination (strict in 20 +entries), all 2,048 Boolean input tables, the splice with literally rebuilt +cleanup, identical register frame paths, the unchanged paid profile and rank +mass, the exact F2 endpoint on all 661 columns, the inherited H1-H5 interface +and conclusions via the pinned `xcheck_p.py`, and the exported scalar bills +and positive/payload bounds via the pinned `export_records.py` (forward bound +equal, reverse bound reduced, payload 93 bits). Eight negative controls are +rejected. + +This differs from the neighboring block results: PR #844 (block 4) optimizes +within a fixed two-factor split, PR #857 (block 8) searches whole-block +integer factorizations with randomized trials, and PR #843 (frame 509) reuses +one existing sum. The mechanism here is exact whole-block single-write +rescheduling with a certified class minimum. PRs #728/#792 change phase-A +mini-nodes (a different section); they report no improvement at frames 507/508 +in their mini-node class, which does not cover this B-section block. + +## Scope and obligations + +Base `f567884aeb8851b6e794af1184119a3bfbe1e631` (selected PR799/PR589, +conditional kappa 0.001661634653669567). Only this directory is added; +`upstream/` and the selected certificate are unchanged. The minimum is +certified inside the doubling-free single-write class; multi-write +interleavings outside that class are not excluded. The C++ legality and +5/9/11-stage replays, hosted invoice, global assembly, Lean formalization and +remote CI are not run here; forward-map equality plus reverse domination imply +the payload bounds carry over, and an independent native replay remains to +confirm. All inherited all-size/compiler, common-label/mutable-source, +hosting, precision/tape and analytic assumptions remain. + +## Reproduce + +Standard-library Python 3.11+ from the repository root: + +```sh +python3 -I -B research/r439-block508-schedule/verify.py +``` + +Expected: `PASS_R439_BLOCK508_SCHEDULE gates=37->30 ADDs=24305->24291 +saved=14 columns=661 controls=8 minimum=30 rank_mass=5129 no_new_kappa`. + +## Credit + +Base word and checkers: eumemic (PR543/PR555), DreamingOfClouds (PR545/PR589), +Dylan Crow (record exporter), Zhihao Chen and the retained supplier lineage. +Method patterns adapt the open PR #844 (Gautam Gupta) and PR #792 (Ryan +Haines) verification structures with attribution; their objects and savings +are not imported. Prepared with help from opencode. Apache-2.0. No +independent human review is claimed. diff --git a/research/r439-block508-schedule/SOURCES.json b/research/r439-block508-schedule/SOURCES.json new file mode 100644 index 0000000000..45693720b8 --- /dev/null +++ b/research/r439-block508-schedule/SOURCES.json @@ -0,0 +1,10 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "supplier_head_589": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "selected_kappa": "0.001661634653669567", + "files": { + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + } +} diff --git a/research/r439-block508-schedule/VALIDATION.md b/research/r439-block508-schedule/VALIDATION.md new file mode 100644 index 0000000000..9fec8bcdfc --- /dev/null +++ b/research/r439-block508-schedule/VALIDATION.md @@ -0,0 +1,51 @@ +# Validation record + +## Commands (repository root, standard-library Python 3.13.15, Windows x64) + +```sh +python -I -B research/r439-block508-schedule/search.py +python -I -B research/r439-block508-schedule/verify.py --record-expected research/r439-block508-schedule/EXPECTED.json +python -I -B research/r439-block508-schedule/verify.py +python -B research/r439-block508-schedule/verify.py +python -O -B research/r439-block508-schedule/verify.py +``` + +Discovery output: 37 original gates, forward single-write minimum 30, +30-gate witness, candidate sha256 +`2947e9d017aabae36f0f196f65417aee18cc45f2485b4dc5e34e9ac20ab0cf82`. + +All verify runs print: + +```text +PASS_R439_BLOCK508_SCHEDULE gates=37->30 ADDs=24305->24291 saved=14 columns=661 controls=8 minimum=30 rank_mass=5129 no_new_kappa +``` + +The `--record-expected` run wrote `EXPECTED.json`; subsequent runs compare +the full receipt byte-for-byte (JSON-canonical) and pass, so the receipt is +deterministic across normal, optimized and isolated modes. `search.py` reruns +deterministically to the same candidate hash. + +## Coverage in verify.py + +- Source pins (word, owning interface checker, record exporter) and base + commit constant; wrong slice/binding rejected. +- Block certificate: exact forward integer-map equality, reverse-map + entrywise domination (strict in 20 entries), all 2,048 Boolean tables. +- Optimality: backward Bellman minimum 30 (2,048 states, 11,264 + state/destination pairs, 4,376 feasible edges) agreeing with the forward + discovery minimum and the 30-gate witness. +- Splice: only `B[205:242]` and `C` change; `C` is the literal reverse; + identical register frame paths; unchanged paid profile and rank mass 5,129; + exact F2 endpoint on all 661 columns; inherited H1-H5 and conclusions pass. +- Bills: 24,305 -> 24,291 ADDs; forward bound 49,347 equal; reverse bound + 1,113,070 -> 1,086,054; payload 93 bits (< 104); non-ADD inventory equal; + 9 copies / 9 erasures. +- Eight negative controls rejected, including a stale-cleanup control that + passes the endpoint but fails literal H4. + +## Not run (open obligations) + +C++ legality and 5/9/11-stage replays (no C++17/Boost toolchain on this +machine), the hosted invoice, the global assembly, `make verify`, Lean and +remote CI. Forward-map equality plus reverse domination imply the payload +bounds carry over; independent native replay remains to confirm. diff --git a/research/r439-block508-schedule/search.py b/research/r439-block508-schedule/search.py new file mode 100644 index 0000000000..9af8efbaba --- /dev/null +++ b/research/r439-block508-schedule/search.py @@ -0,0 +1,145 @@ +"""Deterministic discovery: whole-block single-write minimum for the R439 +phase-B block at frame 508 (B[205:242]) of the tuned word, and one achieving +witness program. + +Method: forward dynamic programming over realized-register subsets. Each of +the block's registers is realized once, in some order, from donors that are +either already-realized rows (their final integer values) or not-yet-realized +registers (their entry singletons), each donor used at most once per +realization (doubling-free positive-addition class). Integer sums must match +the block's forward integer map exactly. No randomness is used. + +This discovery program is NOT imported by verify.py, which rechecks the +minimum with an independently written backward Bellman recursion. + +Prepared with help from opencode. Apache-2.0. +""" +import gzip +import hashlib +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +FRAME = 508 +BEGIN, END = 205, 242 + + +def load_word(): + return json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + + +def block_map(word): + gates = word["B"][BEGIN:END] + assert len(gates) == END - BEGIN + assert all(f == FRAME and len(ss) == 1 for f, _, ss in gates) + regs = sorted({t for _, t, _ in gates} | {s for _, _, ss in gates for s in ss}) + index = {r: i for i, r in enumerate(regs)} + pairs = [(index[t], index[s]) for _, t, (s,) in gates] + n = len(regs) + cols = [] + for c in range(n): + values = [1 if i == c else 0 for i in range(n)] + for dst, src in pairs: + values[dst] += values[src] + cols.append(values) + forward = [list(row) for row in zip(*cols)] + return regs, pairs, forward + + +def packed(row): + assert all(0 <= x < 16 for x in row), "row entry outside base-16 digit range" + return sum(x << (4 * j) for j, x in enumerate(row)) + + +def forward_minimum(forward): + """Returns (minimum, predecessor table). Deterministic; no randomness.""" + n = len(forward) + assert all(forward[i][i] >= 1 for i in range(n)) + wanted = [] + for i in range(n): + row = list(forward[i]) + row[i] -= 1 + wanted.append(packed(row)) + rows = [packed(row) for row in forward] + size = 1 << n + infinity = 10 ** 9 + best = [infinity] * size + parent = [None] * size + best[0] = 0 + for mask in range(size): + if best[mask] == infinity: + continue + for i in range(n): + if mask >> i & 1: + continue + goal = wanted[i] + donors = [] + for d in range(n): + if d == i: + continue + value = rows[d] if mask >> d & 1 else (1 << (4 * d)) + fits = True + for j in range(n): + if ((value >> (4 * j)) & 15) > ((goal >> (4 * j)) & 15): + fits = False + break + if fits: + donors.append((d, value)) + sums = {0: (0, ())} + for d, value in donors: + for total, (cost, used) in list(sums.items()): + merged = total + value + overflows = False + for j in range(n): + if ((merged >> (4 * j)) & 15) > ((goal >> (4 * j)) & 15): + overflows = True + break + if overflows: + continue + if merged not in sums: + sums[merged] = (cost + 1, used + (d,)) + if goal in sums: + cost, used = sums[goal] + nxt = mask | (1 << i) + if best[mask] + cost < best[nxt]: + best[nxt] = best[mask] + cost + parent[nxt] = (mask, i, used) + return best[size - 1], parent + + +def recover(parent, regs): + n = len(regs) + mask = (1 << n) - 1 + steps = [] + while mask: + prev, i, donors = parent[mask] + steps.append((i, donors)) + mask = prev + steps.reverse() + return [[FRAME, regs[i], [regs[d]]] for i, donors in steps for d in donors] + + +def main(): + word = load_word() + regs, pairs, forward = block_map(word) + print("block registers: %s" % (regs,)) + print("original gates: %d" % len(pairs)) + minimum, parent = forward_minimum(forward) + print("forward single-write minimum: %d" % minimum) + gates = recover(parent, regs) + print("witness gates: %d" % len(gates)) + out = {"frame": FRAME, "slice": [BEGIN, END], "registers": regs, + "original_gates": len(pairs), "minimum": minimum, "gates": gates} + digest = hashlib.sha256(json.dumps(out, sort_keys=True, separators=(",", ":")).encode()) + print("candidate sha256: %s" % digest.hexdigest()) + if "--write" in sys.argv: + path = HERE / "CANDIDATE.json" + path.write_text(json.dumps(out, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print("wrote %s" % path) + + +if __name__ == "__main__": + main() diff --git a/research/r439-block508-schedule/verify.py b/research/r439-block508-schedule/verify.py new file mode 100644 index 0000000000..d410b930f9 --- /dev/null +++ b/research/r439-block508-schedule/verify.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +"""Exact finite verification for the shorter R439 phase-B block-508 circuit. + +No search code is imported: the whole-block single-write minimum is rechecked +here with an independently written backward Bellman recursion, and the +candidate's forward integer map, reverse positive map, Boolean tables, splice, +frame paths, paid profile, exact F2 endpoint, inherited H1-H5 interface, +exported scalar bills and positive/payload bounds are all recomputed. + +The owning geometry/interface checker is eumemic's PR555/PR589 xcheck_p.py and +the record exporter is Dylan Crow's export_records.py; both are pinned by +SHA-256 and used unmodified. + +Prepared with help from opencode. Apache-2.0. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import itertools +import json +import struct +import subprocess +import sys +import tempfile +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +CHECKER = "research/e8-bit-p111-tuned/code/xcheck_p.py" +EXPORTER = "research/e8-bit-carrier-skeleton/code/bit/export_records.py" + + +class Reject(Exception): + pass + + +def need(ok, message): + if not ok: + raise Reject(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def pins(certificate): + need(certificate["schema"] == "r439-block508-schedule/1", "unknown schema") + need(certificate["base_commit"] == "f567884aeb8851b6e794af1184119a3bfbe1e631", + "certificate built against a different base") + for path, expected in certificate["source_sha256"].items(): + actual = hashlib.sha256((ROOT / path).read_bytes()).hexdigest() + need(actual == expected, "source pin mismatch: " + path) + + +def integer_map(ops, n): + """Propagate each integer basis column independently (fresh implementation).""" + columns = [] + for column in range(n): + values = [1 if i == column else 0 for i in range(n)] + for dst, src in ops: + need(type(dst) is int and type(src) is int and 0 <= dst < n and 0 <= src < n + and dst != src, "invalid block operation") + values[dst] += values[src] + columns.append(values) + return [list(row) for row in zip(*columns)] + + +def dominated(new, old): + return all(x <= y for a, b in zip(new, old) for x, y in zip(a, b)) + + +def bind_and_check_maps(word, certificate): + binding = certificate["binding"] + need(binding["source"] == WORD and binding["section"] == "B" + and binding["frame"] == 508 and binding["slice"] == [205, 242], "wrong binding") + regs = binding["registers"] + need(regs == [19, 27, 35, 43, 57, 65, 66, 74, 89, 97, 466], "wrong block registers") + need(certificate["original_gates"] == 37, "wrong original bill") + old = word["B"][205:242] + need(len(old) == 37 and all(f == 508 and len(ss) == 1 for f, t, ss in old), + "source block changed") + need(sorted({t for _, t, _ in old} | {s for _, _, ss in old for s in ss}) == regs, + "block touches undeclared wires") + index = {r: i for i, r in enumerate(regs)} + original = [(index[t], index[s]) for _, t, (s,) in old] + gates = certificate["gates"] + need(len(gates) == 30, "candidate gate count differs") + need(all(f == 508 and len(ss) == 1 and t in index and ss[0] in index and ss[0] != t + for f, t, ss in gates), "candidate leaves the single-wire block class") + new = [(index[t], index[s]) for _, t, (s,) in gates] + forward_old = integer_map(original, len(regs)) + forward_new = integer_map(new, len(regs)) + need(forward_new == forward_old, "forward integer map differs") + reverse_old = integer_map(original[::-1], len(regs)) + reverse_new = integer_map(new[::-1], len(regs)) + need(dominated(reverse_new, reverse_old), "reverse positive map not dominated") + strict = sum(1 for a, b in zip(reverse_new, reverse_old) for x, y in zip(a, b) if x < y) + need(strict > 0, "reverse map shows no strict improvement") + need(certificate["forward_total"] == sum(map(sum, forward_old)) == sum(map(sum, forward_new)), + "forward total receipt differs") + # Exhaustive Boolean truth tables over the block registers. + table_hits = 0 + for value in range(1 << len(regs)): + state_old = [(value >> i) & 1 for i in range(len(regs))] + state_new = list(state_old) + for ops, state in ((original, state_old), (new, state_new)): + for dst, src in ops: + state[dst] ^= state[src] + need(state_old == state_new, "Boolean input counterexample: %d" % value) + table_hits += 1 + return original, new, {"boolean_inputs_checked": table_hits, + "reverse_strictly_smaller_entries": strict, + "reverse_old_total": sum(map(sum, reverse_old)), + "reverse_new_total": sum(map(sum, reverse_new))} + + +def pack_row(row): + need(all(type(x) is int and 0 <= x < 16 for x in row), "row entry outside digit range") + return sum(x << (4 * j) for j, x in enumerate(row)) + + +def backward_minimum(forward): + """Backward Bellman recursion over realized-row subsets. + + State `done` holds the rows already realized (from the full set downward). + Realizing row i appends donor additions whose values are final rows for + donors already done and entry singletons otherwise; each donor is used at + most once and integer sums must match exactly. Written independently of + the forward discovery DP in search.py. + """ + n = len(forward) + need(all(forward[i][i] >= 1 for i in range(n)), "missing diagonal") + rows = [pack_row(row) for row in forward] + goal = [] + for i in range(n): + row = list(forward[i]) + row[i] -= 1 + goal.append(pack_row(row)) + size = 1 << n + infinity = 10 ** 9 + dist = [infinity] * size + dist[size - 1] = 0 + feasible = 0 + for done in range(size - 2, -1, -1): + for dst in range(n): + if done >> dst & 1: + continue + want = goal[dst] + donors = [] + for src in range(n): + if src == dst: + continue + value = rows[src] if done >> src & 1 else (1 << (4 * src)) + fits = True + for j in range(n): + if ((value >> (4 * j)) & 15) > ((want >> (4 * j)) & 15): + fits = False + break + if fits: + donors.append(value) + sums = {0: 0} + for value in donors: + for total, cost in list(sums.items()): + merged = total + value + overflows = False + for j in range(n): + if ((merged >> (4 * j)) & 15) > ((want >> (4 * j)) & 15): + overflows = True + break + if overflows: + continue + if merged not in sums: + sums[merged] = cost + 1 + if want in sums: + feasible += 1 + nxt = done | (1 << dst) + dist[done] = min(dist[done], sums[want] + dist[nxt]) + return {"minimum": dist[0], "states": size, + "state_destination_pairs": n * (1 << (n - 1)), + "feasible_edges": feasible, + "backward_distances_sha256": digest(dist)} + + +def rebuild_cleanup(word): + full = next(i for i, frame in enumerate(word["frames"]) if len(frame) == word["v"]) + return [[full, d, list(ss)] for _, d, ss in reversed(word["A"] + word["B"]) + if d < word["v"] or d >= 2 * word["v"]] + + +def build_word(word, certificate): + need(certificate["binding"]["slice"] == [205, 242], "splice slice mismatch") + result = copy.deepcopy(word) + result["B"][205:242] = copy.deepcopy(certificate["gates"]) + result["C"] = rebuild_cleanup(result) + return result + + +def frame_paths(word): + frames = [set(f) for f in word["frames"]] + paths = [[f] for f in word["start"]] + + def move(r, f): + if paths[r][-1] != f: + need(frames[paths[r][-1]] < frames[f], "illegal frame descent or lateral move") + paths[r].append(f) + for section in "DABC": + for f, d, ss in word[section]: + for r in [d, *ss]: + move(r, f) + for r, f in enumerate(word["final"]): + move(r, f) + return paths + + +def whole_endpoint(word): + n, v = 2 * word["v"] + word["R"], word["v"] + state = [{i} for i in range(n)] + + def run(section): + for _, d, sources in word[section]: + for s in sources: + state[d].symmetric_difference_update(state[s]) + run("D") + run("A") + snapshots = [state[r].copy() for r in word["ret"]] + for t, reads in enumerate(word["scatter"]): + for k in reads: + state[v + t].symmetric_difference_update(snapshots[k]) + run("B") + run("C") + for r, actual in enumerate(state): + expected = {r, r - v} if v <= r < 2 * v else {r} + need(actual == expected, "dirty-input endpoint mismatch at register %d" % r) + return n + + +def load_checker(): + spec = importlib.util.spec_from_file_location("block508_original_xcheck", ROOT / CHECKER) + checker = importlib.util.module_from_spec(spec) + spec.loader.exec_module(checker) + return checker + + +def export_and_bound(word, out): + out.mkdir(parents=True, exist_ok=True) + path = out / "word.json.gz" + path.write_bytes(gzip.compress(canonical(word), mtime=0)) + subprocess.run([sys.executable, "-I", "-B", str(ROOT / EXPORTER), + str(path), str(out / "records")], + check=True, capture_output=True, text=True) + raw = (out / "records/249-records.bin").read_bytes() + need(len(raw) % 24 == 0, "misaligned exporter records") + records = list(struct.iter_unpack("<6i", raw)) + n = 2 * word["v"] + word["R"] + bounds = [] + for reverse in (False, True): + norms, maximum, opened = [1] * (n + 1), 1, False + for op, a, b, coefficient, _, _ in (reversed(records) if reverse else records): + if op == 0: + continue + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + norms[a] += abs(coefficient) * norms[b] + maximum = max(maximum, norms[a]) + elif op == 2: + need(not opened, "nested retained copy") + norms[b], opened = norms[a], True + elif op == 3: + need(opened, "unmatched retained erase") + norms[b], opened = 0, False + else: + raise Reject("unknown record opcode") + need(not opened, "unclosed retained copy") + bounds.append(maximum) + payload = 64 * bounds[0] ** 3 * bounds[1] ** 2 + need(payload < 1 << 104, "positive-prefix cap exceeded") + return {"records": len(records), "adds": sum(r[0] == 1 for r in records), + "copies": sum(r[0] == 2 for r in records), + "erasures": sum(r[0] == 3 for r in records), + "forward_positive_bound": bounds[0], "reverse_positive_bound": bounds[1], + "payload_bits": payload.bit_length(), + "record_sha256": hashlib.sha256(raw).hexdigest()}, records + + +def must_reject(name, action): + try: + action() + except Reject: + return name + raise Reject("negative control accepted: " + name) + + +def verify(out): + certificate = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) + pins(certificate) + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + original, new, block = bind_and_check_maps(word, certificate) + optimality = backward_minimum(integer_map(original, len(certificate["binding"]["registers"]))) + need(optimality["minimum"] == 30 == len(certificate["gates"]) == certificate["forward_minimum"], + "minimum/gate-count/minimum receipt disagree") + need(optimality == certificate["backward_optimality"], "backward optimality receipt differs") + candidate = build_word(word, certificate) + need(all(candidate[k] == word[k] for k in word if k not in ("B", "C")), "unrelated field changed") + need(candidate["C"] == rebuild_cleanup(candidate), "literal cleanup reversal fails") + before_paths, after_paths = frame_paths(word), frame_paths(candidate) + need(before_paths == after_paths, "register frame path changed") + whole_endpoint(word) + columns = whole_endpoint(candidate) + checker = load_checker() + dimensions, labels, flow, hypotheses, conclusion, _ = checker.check(candidate) + need(all(hypotheses.values()) and all(conclusion.values()), "inherited interface guard fails") + profile = Counter(dimensions.fdim[b] - dimensions.fdim[a] + for path in after_paths for a, b in itertools.pairwise(path)) + profile.update(t["rank"] for t in flow["totals"]) + need(dict(sorted(profile.items())) == {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}, + "paid profile changed") + need(sum(k * v for k, v in profile.items()) == 5129, "rank mass changed") + before_bill, before_records = export_and_bound(word, out / "before") + after_bill, after_records = export_and_bound(candidate, out / "after") + need(before_bill["adds"] == 24305 and after_bill["adds"] == 24291, "ADD bills differ") + need(before_bill["copies"] == after_bill["copies"] == 9, "retained copy count changed") + need(before_bill["erasures"] == after_bill["erasures"] == 9, "retained erasure count changed") + need(Counter(r for r in before_records if r[0] != 1) + == Counter(r for r in after_records if r[0] != 1), "non-ADD event inventory changed") + need(after_bill["forward_positive_bound"] == before_bill["forward_positive_bound"] == 49347, + "forward positive bound changed") + need(after_bill["reverse_positive_bound"] == 1086054 <= before_bill["reverse_positive_bound"] == 1113070, + "reverse positive bound not reduced as certified") + need(after_bill["payload_bits"] == before_bill["payload_bits"] == 93, "payload bits changed") + + controls = [] + bad = copy.deepcopy(certificate["gates"]) + bad[0][2] = [19] if bad[0][2] != [19] else [27] + controls.append(must_reject("mutated_candidate_source", + lambda: bind_and_check_maps(word, dict(certificate, gates=bad)))) + short = copy.deepcopy(certificate["gates"])[:-1] + controls.append(must_reject("unpaid_gate", + lambda: bind_and_check_maps(word, dict(certificate, gates=short)))) + controls.append(must_reject("inverted_domination", + lambda: need(dominated(integer_map(original[::-1], 11), + integer_map(new[::-1], 11)), + "inverted domination holds"))) + bad_word = copy.deepcopy(candidate) + bad_word["C"].pop() + controls.append(must_reject("omitted_cleanup", lambda: whole_endpoint(bad_word))) + bad_word = copy.deepcopy(candidate) + del bad_word["B"][205] + bad_word["C"] = rebuild_cleanup(bad_word) + controls.append(must_reject("missing_gate_with_matching_cleanup", + lambda: whole_endpoint(bad_word))) + bad_word = copy.deepcopy(candidate) + bad_word["B"][205][0] = 0 + controls.append(must_reject("illegal_frame_descent", lambda: frame_paths(bad_word))) + stale = copy.deepcopy(candidate) + stale["C"] = word["C"] + whole_endpoint(stale) # Positive semantic control; rejected only by literal H4. + controls.append(must_reject("stale_cleanup_literal_H4", + lambda: need(stale["C"] == rebuild_cleanup(stale), "H4 fails"))) + bad_cert = copy.deepcopy(certificate) + bad_cert["binding"] = dict(certificate["binding"], slice=[206, 243]) + controls.append(must_reject("wrong_slice_binding", + lambda: bind_and_check_maps(word, bad_cert))) + + return {"status": "PASS_R439_BLOCK508_SCHEDULE", "block": block, + "backward_optimality": optimality, "columns": columns, + "closed_frames": labels["frames"], + "copy_ranks": [t["rank"] for t in flow["totals"]], + "paid_profile": {str(k): v for k, v in sorted(profile.items())}, + "rank_mass": 5129, + "identical_register_frame_paths": len(after_paths), + "hypotheses": hypotheses, "conclusion": conclusion, + "before": before_bill, "after": after_bill, + "adds_saved": 14, "new_kappa_claim": False, + "word_sha256": hashlib.sha256(canonical(candidate)).hexdigest(), + "negative_controls": controls} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--out", type=Path, help="new output directory; must not exist") + parser.add_argument("--record-expected", type=Path, help="write a NEW expected receipt") + args = parser.parse_args() + if args.out: + args.out.mkdir(parents=True, exist_ok=False) + result = verify(args.out.resolve()) + else: + with tempfile.TemporaryDirectory(prefix="r439-block508-") as directory: + result = verify(Path(directory)) + if args.record_expected: + with args.record_expected.open("x", encoding="utf-8", newline="\n") as handle: + json.dump(result, handle, indent=2, sort_keys=True) + handle.write("\n") + else: + expected = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8")) + need(result == expected, "deterministic receipt differs from EXPECTED.json") + if args.out: + (args.out / "receipt.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", + encoding="utf-8") + print("PASS_R439_BLOCK508_SCHEDULE gates=37->30 ADDs=24305->24291 saved=14 " + "columns=661 controls=8 minimum=30 rank_mass=5129 no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except (Reject, ValueError, OSError) as error: + raise SystemExit("REJECT: " + str(error)) from error