diff --git a/research/leaver-cell-audit-seed65/README.md b/research/leaver-cell-audit-seed65/README.md new file mode 100644 index 0000000000..13a3615c5a --- /dev/null +++ b/research/leaver-cell-audit-seed65/README.md @@ -0,0 +1,128 @@ +# Independent audit of the mutable-leaver all-K cells (PR1005) and the seven-slot word (PR1018) + +**Status: adversarial audit / independent verification. No new kappa. No counterexample found; one +documentation discrepancy.** The selected result and `upstream/` are unchanged. + +Track 60–74 (adversarial audit), OS-random assignment seed **65** (`secrets.randbelow(100)`). +Base `2921874911956718fcaaaf9396fe8267b3cfa9f0`. Audited heads: PR1005 +`779e80aef469bc3a28b19f1adde199871a9a22e3` and PR1018 `eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef`. +PR1022, PR1028, PR1031 and PR1042 pin the same seven-slot local word (`c2b29430…`), so the +local-word results below also apply to them. Their owner maps and global replays are not covered. + +## Why this object + +PR1004/1005 introduce "mutable-leaver" cells. A coded 21-gate circuit uses face-event operands that +have no later reads as mutable scratch, and the "inherited cleanup" restores them at FULL. The k8 +cells are the local word for six open κ claims (PR1005, PR1018, PR1022, PR1028, PR1031, PR1042). Their +recorded reviews come from the authors' own reviewer agents. Checking the premise independently is +the cheapest way to support or block that whole lineage. + +## Statements checked + +The verifier is standard-library only and imports nothing from the audited packages. Their words are +read as data (inputs pinned in `SOURCES.json`). + +1. **Exact local map (all three words).** Every one of the 224 data columns, replayed forward through + precondition, A, cut, B, tail and cleanup, gives `x -> x` and `y_t -> y_t + x_t`. For each of the 480 + helper columns, the inverse of the post-precondition program returns the unit vector plus a residue + supported on targets only. This is exactly the condition for the pre-main compensation `y -= a·h` + to exist, and it is a different formulation from the authors' constructive one. The residue + vanishes for every entering helper. +2. **Frames.** An independent replay of monotone climbs over A, the centre paths, B, the early-cleanup + tail and the terminal ends reproduces each word's recorded paid profile. The FULL cleanup touches + only registers that end at FULL. +3. **Leaver premise.** All 8 coded cells are found literally, each exactly once, contiguous and in the + published gate order, by unifying the `scaled` gate lists of `CODED-CELLS-k8.json`. The target sets + come from `TRI-LEAVER-k8.json`; the coded target index is the TRI read index + 8, checked for all + cells. The 24 mutated leavers (12 data registers, 12 helpers) satisfy all of the following: + * none is a centre, entering helper or low-ended helper; + * none is touched again in A, cut, B or the early-cleanup tail after its cell; + * each is written in the FULL cleanup; + * each holds a value different from its input at the end of B, so the restoration is real FULL + work. +4. **No new class of source mutation.** Each of the 12 data-register leavers receives exactly one + B-section write in both the no-triangle base word (`3e99ba77…`) and the cell word, and their + A-section writes are identical. The cells re-pair or re-scale these pre-existing face-event writes + (8 of 12 differ) and remove the packet-copy helpers. They add no mutation event to any data + register. The dependence on mutable sources is therefore the one the gauge44 lineage already + inherits. +5. **Profile deltas.** The raw-stage paid profiles, recounted with the replay of item 2, are additive + per cell: + + | word | R | raw paid profile | + |---|---:|---| + | no-triangle | 504 | `{1:1880, 2:832, 3:312, 4:168, 5:168, 6:56, 8:8}` | + | k5 cells | 489 | `{1:1910, 2:772, 3:327, 4:168, 5:168, 6:41, 8:8}` | + | k8 cells | 480 | `{1:1928, 2:736, 3:336, 4:168, 5:168, 6:32, 8:8}` | + + `k5 − notri = 5u` and `k8 − k5 = 3u`, where **u = +6H1 −12H2 +3H3 −3H6** (rank mass −27, three + helpers removed per cell). The seven-slot word differs from the final k8 word by exactly + `7×{3:+2, 4:−4, 5:+2}`, which matches PR987's per-slot claim. + +## Finding: per-cell profile claim not reproduced + +The PR1004/PR1005 descriptions state: "Each cell changes the raw paid profile by exactly +−30H1+6H2+6H3." That claim is rank-mass-neutral. Against the no-triangle comparator, the measured +per-cell change is `+6H1 −12H2 +3H3 −3H6`. No rebuilt stage (raw, regroup, hpe, cold44) shows the +stated vector. The packages do not state the claim's comparator, and no code asserts it. + +**This does not affect κ.** κ is priced from the final word's full profile through the reviewed +global replay. It is a description that reviewers should not rely on. The authors should state the +comparator or correct the sentence. + +## Negative controls + +Each mutant must be rejected by the check it targets. All 14 are rejected (7 on the final k8 word, 7 +on the seven-slot word): + +| control | rejected by | +|---|---| +| N1 drop a leaver write | endpoint | +| N2 drop the FULL-cleanup restoration of a leaver | endpoint | +| N3 neutral `h += ½x; h −= ½x` on a leaver at FULL after its cell | **premise only** | +| N4 wrong cell coefficient | endpoint | +| N5 leaver write moved after its first dependent read | endpoint | +| N6 entering-helper dirt into a cell target | endpoint (entering response) | +| N7 leaver gate below its current frame | frames | + +N3 passes both the exact endpoint and the frame replay with an unchanged paid profile. The stated +premise is therefore a design property that the exact map and frame checks do not enforce on their +own. This audit checks it separately. + +## Reproduce + +```sh +python3 -I -B research/leaver-cell-audit-seed65/verify.py +``` + +Expected (about 5 s), with the result byte-compared to `RESULT.json`: + +```text +PASS_INDEPENDENT_MUTABLE_LEAVER_AUDIT cells=8 leavers=24 columns=704 controls=14 per_cell_raw={1: 6, 2: -12, 3: 3, 6: -3} claimed_match=False +``` + +To rebuild the inputs, follow the README clean-clone commands of PR1005 (`reproduce.py --until word`, +`reproduce_notri.py --word-only`, `reproduce_leaver.py --id k8|k5 --word-only`, +`reproduce_leaver_chain.py --id k8`) and PR1018's `verify_slots.py --baseline `. The PR635 +supplier is pinned at `a6895a69…`. `SOURCES.json` names each output file and its content hash. Every +hash equals the pin the PRs publish. In this run all 21 PR1005 chain steps (`STEPS.json`) exited 0, and PR1018 printed +`PASS_SLOTS_ON_CHECKED_K8_BASELINE 0.00167166528321877`. + +## Scope and open obligations + +This audit checks the local scalar/frame words only. It does not check the owner maps (K8c8, the T16 +packings), hosting, the finite invoice, the moment and outer pricing, or any κ value. Nor does it check +the inherited mutable-source/common-label realization, Lemma A/G content, all-size compilation, +precision/tape or the analytic interfaces. Item 4 shows that the cells require nothing beyond the +inherited interface; it does not prove that interface. Finite replays are not a formal proof. + +## Credit and disclosure + +The construction and the audited packages are Jeremy Kothe's PR1004/PR1005/PR1018 (LeaverSAT, the +reviewer agents and G44Pack3 as named there). They build on rohanarun's PR987 slot search, NewBArch's +PR869 triangle-hybrid delivery, icekylinx's PR645 gauge44 construction and its `audit_local.py`, and +chafreaky's PR685/741 lineage. Two input files (`CODED-CELLS-k8.json`, `TRI-LEAVER-k8.json`) are +copied unchanged from PR1005 under the repository's Apache-2.0 license. The other inputs are outputs +of the authors' drivers. + +Prepared by Sagar Thakrar with substantial assistance from Anthropic Claude (Claude Code). diff --git a/research/leaver-cell-audit-seed65/RESULT.json b/research/leaver-cell-audit-seed65/RESULT.json new file mode 100644 index 0000000000..2ca2e52a29 --- /dev/null +++ b/research/leaver-cell-audit-seed65/RESULT.json @@ -0,0 +1,1047 @@ +{ + "audited": { + "cell": { + "R": 480, + "cells": [ + { + "cell": "01+", + "leavers": [ + 17, + 25, + 57 + ], + "main_index": 4085 + }, + { + "cell": "23+", + "leavers": [ + 81, + 89, + 239 + ], + "main_index": 4106 + }, + { + "cell": "45+", + "leavers": [ + 49, + 255, + 415 + ], + "main_index": 4127 + }, + { + "cell": "67+", + "leavers": [ + 271, + 431, + 447 + ], + "main_index": 4148 + }, + { + "cell": "67-", + "leavers": [ + 18, + 50, + 82 + ], + "main_index": 4169 + }, + { + "cell": "01-", + "leavers": [ + 233, + 249, + 265 + ], + "main_index": 4190 + }, + { + "cell": "23-", + "leavers": [ + 58, + 409, + 425 + ], + "main_index": 4211 + }, + { + "cell": "45-", + "leavers": [ + 26, + 90, + 441 + ], + "main_index": 4232 + } + ], + "content_sha256": "58e14a02f2c1d4dcfeb363ebd5fa2e713064b5c724d90f6721419a8cfa67729b", + "endpoint": { + "columns": 704, + "data_columns": 224, + "helper_columns": 480, + "target_residue_entries": 7336 + }, + "leavers": [ + { + "cell": "01+", + "first_full_cleanup_write": 1124, + "full_cleanup_writes": 9, + "kind": "data", + "register": 17 + }, + { + "cell": "01+", + "first_full_cleanup_write": 858, + "full_cleanup_writes": 14, + "kind": "data", + "register": 25 + }, + { + "cell": "01+", + "first_full_cleanup_write": 3939, + "full_cleanup_writes": 14, + "kind": "data", + "register": 57 + }, + { + "cell": "23+", + "first_full_cleanup_write": 5951, + "full_cleanup_writes": 84, + "kind": "data", + "register": 81 + }, + { + "cell": "23+", + "first_full_cleanup_write": 5812, + "full_cleanup_writes": 76, + "kind": "data", + "register": 89 + }, + { + "cell": "23+", + "first_full_cleanup_write": 3951, + "full_cleanup_writes": 62, + "kind": "helper", + "register": 239 + }, + { + "cell": "45+", + "first_full_cleanup_write": 3841, + "full_cleanup_writes": 13, + "kind": "data", + "register": 49 + }, + { + "cell": "45+", + "first_full_cleanup_write": 1766, + "full_cleanup_writes": 101, + "kind": "helper", + "register": 255 + }, + { + "cell": "45+", + "first_full_cleanup_write": 3819, + "full_cleanup_writes": 84, + "kind": "helper", + "register": 415 + }, + { + "cell": "67+", + "first_full_cleanup_write": 880, + "full_cleanup_writes": 88, + "kind": "helper", + "register": 271 + }, + { + "cell": "67+", + "first_full_cleanup_write": 3820, + "full_cleanup_writes": 78, + "kind": "helper", + "register": 431 + }, + { + "cell": "67+", + "first_full_cleanup_write": 3886, + "full_cleanup_writes": 87, + "kind": "helper", + "register": 447 + }, + { + "cell": "67-", + "first_full_cleanup_write": 1014, + "full_cleanup_writes": 9, + "kind": "data", + "register": 18 + }, + { + "cell": "67-", + "first_full_cleanup_write": 3827, + "full_cleanup_writes": 13, + "kind": "data", + "register": 50 + }, + { + "cell": "67-", + "first_full_cleanup_write": 3889, + "full_cleanup_writes": 88, + "kind": "data", + "register": 82 + }, + { + "cell": "01-", + "first_full_cleanup_write": 3992, + "full_cleanup_writes": 47, + "kind": "helper", + "register": 233 + }, + { + "cell": "01-", + "first_full_cleanup_write": 1564, + "full_cleanup_writes": 112, + "kind": "helper", + "register": 249 + }, + { + "cell": "01-", + "first_full_cleanup_write": 1448, + "full_cleanup_writes": 48, + "kind": "helper", + "register": 265 + }, + { + "cell": "23-", + "first_full_cleanup_write": 3952, + "full_cleanup_writes": 13, + "kind": "data", + "register": 58 + }, + { + "cell": "23-", + "first_full_cleanup_write": 6198, + "full_cleanup_writes": 15, + "kind": "helper", + "register": 409 + }, + { + "cell": "23-", + "first_full_cleanup_write": 6129, + "full_cleanup_writes": 18, + "kind": "helper", + "register": 425 + }, + { + "cell": "45-", + "first_full_cleanup_write": 1897, + "full_cleanup_writes": 13, + "kind": "data", + "register": 26 + }, + { + "cell": "45-", + "first_full_cleanup_write": 3894, + "full_cleanup_writes": 82, + "kind": "data", + "register": 90 + }, + { + "cell": "45-", + "first_full_cleanup_write": 3884, + "full_cleanup_writes": 85, + "kind": "helper", + "register": 441 + } + ], + "paid_profile": { + "1": 2394, + "2": 398, + "3": 508, + "4": 142, + "5": 56, + "8": 8 + } + }, + "final": { + "R": 480, + "cells": [ + { + "cell": "01+", + "leavers": [ + 17, + 25, + 57 + ], + "main_index": 4154 + }, + { + "cell": "23+", + "leavers": [ + 81, + 89, + 239 + ], + "main_index": 4175 + }, + { + "cell": "45+", + "leavers": [ + 49, + 255, + 415 + ], + "main_index": 4196 + }, + { + "cell": "67+", + "leavers": [ + 271, + 431, + 447 + ], + "main_index": 4217 + }, + { + "cell": "67-", + "leavers": [ + 18, + 50, + 82 + ], + "main_index": 4238 + }, + { + "cell": "01-", + "leavers": [ + 233, + 249, + 265 + ], + "main_index": 4259 + }, + { + "cell": "23-", + "leavers": [ + 58, + 409, + 425 + ], + "main_index": 4280 + }, + { + "cell": "45-", + "leavers": [ + 26, + 90, + 441 + ], + "main_index": 4301 + } + ], + "content_sha256": "db2c7cfb3f8eee2b76c2e0154fc530520fb4d90cd9511a002cab527b16033b83", + "endpoint": { + "columns": 704, + "data_columns": 224, + "helper_columns": 480, + "target_residue_entries": 7208 + }, + "leavers": [ + { + "cell": "01+", + "first_full_cleanup_write": 2145, + "full_cleanup_writes": 6, + "kind": "data", + "register": 17 + }, + { + "cell": "01+", + "first_full_cleanup_write": 1322, + "full_cleanup_writes": 10, + "kind": "data", + "register": 25 + }, + { + "cell": "01+", + "first_full_cleanup_write": 514, + "full_cleanup_writes": 3, + "kind": "data", + "register": 57 + }, + { + "cell": "23+", + "first_full_cleanup_write": 3072, + "full_cleanup_writes": 5, + "kind": "data", + "register": 81 + }, + { + "cell": "23+", + "first_full_cleanup_write": 4424, + "full_cleanup_writes": 4, + "kind": "data", + "register": 89 + }, + { + "cell": "23+", + "first_full_cleanup_write": 473, + "full_cleanup_writes": 76, + "kind": "helper", + "register": 239 + }, + { + "cell": "45+", + "first_full_cleanup_write": 869, + "full_cleanup_writes": 4, + "kind": "data", + "register": 49 + }, + { + "cell": "45+", + "first_full_cleanup_write": 1261, + "full_cleanup_writes": 57, + "kind": "helper", + "register": 255 + }, + { + "cell": "45+", + "first_full_cleanup_write": 1195, + "full_cleanup_writes": 8, + "kind": "helper", + "register": 415 + }, + { + "cell": "67+", + "first_full_cleanup_write": 2236, + "full_cleanup_writes": 15, + "kind": "helper", + "register": 271 + }, + { + "cell": "67+", + "first_full_cleanup_write": 1196, + "full_cleanup_writes": 10, + "kind": "helper", + "register": 431 + }, + { + "cell": "67+", + "first_full_cleanup_write": 774, + "full_cleanup_writes": 16, + "kind": "helper", + "register": 447 + }, + { + "cell": "67-", + "first_full_cleanup_write": 2144, + "full_cleanup_writes": 6, + "kind": "data", + "register": 18 + }, + { + "cell": "67-", + "first_full_cleanup_write": 794, + "full_cleanup_writes": 4, + "kind": "data", + "register": 50 + }, + { + "cell": "67-", + "first_full_cleanup_write": 3711, + "full_cleanup_writes": 4, + "kind": "data", + "register": 82 + }, + { + "cell": "01-", + "first_full_cleanup_write": 515, + "full_cleanup_writes": 63, + "kind": "helper", + "register": 233 + }, + { + "cell": "01-", + "first_full_cleanup_write": 1295, + "full_cleanup_writes": 32, + "kind": "helper", + "register": 249 + }, + { + "cell": "01-", + "first_full_cleanup_write": 1371, + "full_cleanup_writes": 22, + "kind": "helper", + "register": 265 + }, + { + "cell": "23-", + "first_full_cleanup_write": 501, + "full_cleanup_writes": 3, + "kind": "data", + "register": 58 + }, + { + "cell": "23-", + "first_full_cleanup_write": 3816, + "full_cleanup_writes": 12, + "kind": "helper", + "register": 409 + }, + { + "cell": "23-", + "first_full_cleanup_write": 3732, + "full_cleanup_writes": 10, + "kind": "helper", + "register": 425 + }, + { + "cell": "45-", + "first_full_cleanup_write": 1294, + "full_cleanup_writes": 10, + "kind": "data", + "register": 26 + }, + { + "cell": "45-", + "first_full_cleanup_write": 4421, + "full_cleanup_writes": 4, + "kind": "data", + "register": 90 + }, + { + "cell": "45-", + "first_full_cleanup_write": 795, + "full_cleanup_writes": 10, + "kind": "helper", + "register": 441 + } + ], + "paid_profile": { + "1": 2412, + "2": 418, + "3": 418, + "4": 170, + "5": 68, + "8": 8 + } + }, + "seven_slot": { + "R": 480, + "cells": [ + { + "cell": "01+", + "leavers": [ + 17, + 25, + 57 + ], + "main_index": 4154 + }, + { + "cell": "23+", + "leavers": [ + 81, + 89, + 239 + ], + "main_index": 4175 + }, + { + "cell": "45+", + "leavers": [ + 49, + 255, + 415 + ], + "main_index": 4196 + }, + { + "cell": "67+", + "leavers": [ + 271, + 431, + 447 + ], + "main_index": 4217 + }, + { + "cell": "67-", + "leavers": [ + 18, + 50, + 82 + ], + "main_index": 4238 + }, + { + "cell": "01-", + "leavers": [ + 233, + 249, + 265 + ], + "main_index": 4259 + }, + { + "cell": "23-", + "leavers": [ + 58, + 409, + 425 + ], + "main_index": 4280 + }, + { + "cell": "45-", + "leavers": [ + 26, + 90, + 441 + ], + "main_index": 4301 + } + ], + "content_sha256": "c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8", + "endpoint": { + "columns": 704, + "data_columns": 224, + "helper_columns": 480, + "target_residue_entries": 7208 + }, + "leavers": [ + { + "cell": "01+", + "first_full_cleanup_write": 2152, + "full_cleanup_writes": 6, + "kind": "data", + "register": 17 + }, + { + "cell": "01+", + "first_full_cleanup_write": 1329, + "full_cleanup_writes": 10, + "kind": "data", + "register": 25 + }, + { + "cell": "01+", + "first_full_cleanup_write": 521, + "full_cleanup_writes": 3, + "kind": "data", + "register": 57 + }, + { + "cell": "23+", + "first_full_cleanup_write": 3079, + "full_cleanup_writes": 5, + "kind": "data", + "register": 81 + }, + { + "cell": "23+", + "first_full_cleanup_write": 4431, + "full_cleanup_writes": 4, + "kind": "data", + "register": 89 + }, + { + "cell": "23+", + "first_full_cleanup_write": 480, + "full_cleanup_writes": 76, + "kind": "helper", + "register": 239 + }, + { + "cell": "45+", + "first_full_cleanup_write": 876, + "full_cleanup_writes": 4, + "kind": "data", + "register": 49 + }, + { + "cell": "45+", + "first_full_cleanup_write": 1268, + "full_cleanup_writes": 57, + "kind": "helper", + "register": 255 + }, + { + "cell": "45+", + "first_full_cleanup_write": 1202, + "full_cleanup_writes": 8, + "kind": "helper", + "register": 415 + }, + { + "cell": "67+", + "first_full_cleanup_write": 2243, + "full_cleanup_writes": 15, + "kind": "helper", + "register": 271 + }, + { + "cell": "67+", + "first_full_cleanup_write": 1203, + "full_cleanup_writes": 10, + "kind": "helper", + "register": 431 + }, + { + "cell": "67+", + "first_full_cleanup_write": 781, + "full_cleanup_writes": 16, + "kind": "helper", + "register": 447 + }, + { + "cell": "67-", + "first_full_cleanup_write": 2151, + "full_cleanup_writes": 6, + "kind": "data", + "register": 18 + }, + { + "cell": "67-", + "first_full_cleanup_write": 801, + "full_cleanup_writes": 4, + "kind": "data", + "register": 50 + }, + { + "cell": "67-", + "first_full_cleanup_write": 3718, + "full_cleanup_writes": 4, + "kind": "data", + "register": 82 + }, + { + "cell": "01-", + "first_full_cleanup_write": 522, + "full_cleanup_writes": 63, + "kind": "helper", + "register": 233 + }, + { + "cell": "01-", + "first_full_cleanup_write": 1302, + "full_cleanup_writes": 32, + "kind": "helper", + "register": 249 + }, + { + "cell": "01-", + "first_full_cleanup_write": 1378, + "full_cleanup_writes": 22, + "kind": "helper", + "register": 265 + }, + { + "cell": "23-", + "first_full_cleanup_write": 508, + "full_cleanup_writes": 3, + "kind": "data", + "register": 58 + }, + { + "cell": "23-", + "first_full_cleanup_write": 3823, + "full_cleanup_writes": 12, + "kind": "helper", + "register": 409 + }, + { + "cell": "23-", + "first_full_cleanup_write": 3739, + "full_cleanup_writes": 10, + "kind": "helper", + "register": 425 + }, + { + "cell": "45-", + "first_full_cleanup_write": 1301, + "full_cleanup_writes": 10, + "kind": "data", + "register": 26 + }, + { + "cell": "45-", + "first_full_cleanup_write": 4428, + "full_cleanup_writes": 4, + "kind": "data", + "register": 90 + }, + { + "cell": "45-", + "first_full_cleanup_write": 802, + "full_cleanup_writes": 10, + "kind": "helper", + "register": 441 + } + ], + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + } + }, + "controls": { + "final": { + "N1_drop_leaver_write": "endpoint: endpoint failures [('data', 56), ('data', 59)]", + "N2_drop_full_cleanup_restore": "endpoint: endpoint failures [('data', 17), ('data', 18), ('data', 21), ('data', ", + "N3_neutral_touch_of_leaver_after_cell": "premise: leaver 17 touched in main after its cell (index 5473)", + "N4_wrong_cell_coefficient": "endpoint: endpoint failures [('data', 57), ('data', 58)]", + "N5_leaver_write_after_its_read": "endpoint: endpoint failures [('data', 56), ('data', 59)]", + "N6_entering_dirt_into_cell_target": "endpoint: endpoint failures [('entering-response', 448)]", + "N7_leaver_gate_below_current_frame": "frames: non-monotone climb in B, register 57" + }, + "seven_slot": { + "N1_drop_leaver_write": "endpoint: endpoint failures [('data', 56), ('data', 59)]", + "N2_drop_full_cleanup_restore": "endpoint: endpoint failures [('data', 17), ('data', 18), ('data', 21), ('data', ", + "N3_neutral_touch_of_leaver_after_cell": "premise: leaver 17 touched in main after its cell (index 5473)", + "N4_wrong_cell_coefficient": "endpoint: endpoint failures [('data', 57), ('data', 58)]", + "N5_leaver_write_after_its_read": "endpoint: endpoint failures [('data', 56), ('data', 59)]", + "N6_entering_dirt_into_cell_target": "endpoint: endpoint failures [('entering-response', 448)]", + "N7_leaver_gate_below_current_frame": "frames: non-monotone climb in B, register 57" + } + }, + "face_events": { + "base_B_write": { + "17": [ + [ + 16, + "1" + ] + ], + "18": [ + [ + 269, + "1" + ] + ], + "25": [ + [ + 24, + "1" + ] + ], + "26": [ + [ + 253, + "1" + ] + ], + "49": [ + [ + 48, + "1" + ] + ], + "50": [ + [ + 445, + "1" + ] + ], + "57": [ + [ + 56, + "1" + ] + ], + "58": [ + [ + 237, + "1" + ] + ], + "81": [ + [ + 80, + "1" + ] + ], + "82": [ + [ + 429, + "1" + ] + ], + "89": [ + [ + 88, + "1" + ] + ], + "90": [ + [ + 413, + "1" + ] + ] + }, + "cell_B_write": { + "17": [ + [ + 24, + "1" + ] + ], + "18": [ + [ + 269, + "1" + ] + ], + "25": [ + [ + 16, + "1" + ] + ], + "26": [ + [ + 253, + "1" + ] + ], + "49": [ + [ + 91, + "-2" + ] + ], + "50": [ + [ + 429, + "1" + ] + ], + "57": [ + [ + 56, + "1" + ] + ], + "58": [ + [ + 237, + "1" + ] + ], + "81": [ + [ + 88, + "1" + ] + ], + "82": [ + [ + 445, + "1" + ] + ], + "89": [ + [ + 80, + "1" + ] + ], + "90": [ + [ + 443, + "-1/2" + ] + ] + }, + "data_leavers": [ + 17, + 18, + 25, + 26, + 49, + 50, + 57, + 58, + 81, + 82, + 89, + 90 + ], + "repaired": [ + 17, + 25, + 49, + 50, + 81, + 82, + 89, + 90 + ] + }, + "profile_deltas": { + "helpers_removed_per_cell": 3, + "k5_minus_notri": { + "1": 30, + "2": -60, + "3": 15, + "6": -15 + }, + "k8_minus_k5": { + "1": 18, + "2": -36, + "3": 9, + "6": -9 + }, + "matches_pr_description": false, + "per_cell_raw": { + "1": 6, + "2": -12, + "3": 3, + "6": -3 + }, + "pr_description_per_cell": { + "1": -30, + "2": 6, + "3": 6 + }, + "rank_mass_per_cell_raw": -27, + "raw_profiles": { + "k5": { + "1": 1910, + "2": 772, + "3": 327, + "4": 168, + "5": 168, + "6": 41, + "8": 8 + }, + "k8": { + "1": 1928, + "2": 736, + "3": 336, + "4": 168, + "5": 168, + "6": 32, + "8": 8 + }, + "notri": { + "1": 1880, + "2": 832, + "3": 312, + "4": 168, + "5": 168, + "6": 56, + "8": 8 + } + }, + "seven_slot_minus_final": { + "3": 14, + "4": -28, + "5": 14 + } + }, + "status": "PASS_INDEPENDENT_MUTABLE_LEAVER_AUDIT" +} diff --git a/research/leaver-cell-audit-seed65/SOURCES.json b/research/leaver-cell-audit-seed65/SOURCES.json new file mode 100644 index 0000000000..60c7cfc4bb --- /dev/null +++ b/research/leaver-cell-audit-seed65/SOURCES.json @@ -0,0 +1,60 @@ +{ + "base_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "audited_heads": { + "1005": "779e80aef469bc3a28b19f1adde199871a9a22e3", + "1018": "eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef" + }, + "same_local_word_pinned_by": { + "1022": "58618bcbfe88a252467755fc283c04c3db5ca4fd", + "1028": "be4bd89cb4483dcee43257200cd27601f938f13d", + "1031": "e900534f0beda892c726723524203b97471fb9a3", + "1042": "7e8ef087c02a77038a28a337a7ee3a77039cac0d" + }, + "pr635_supplier": { + "commit": "a6895a69f8ad98ab45777b03e9e6f48888c39f6f", + "path": "research/complex-571-cold14-st2" + }, + "environment": "macOS (Darwin 25.5), CPython 3.14.8; inputs rebuilt with the audited packages' own drivers, then read here as data only", + "inputs": { + "CODED-CELLS-k8.json": { + "copied_from": "PR1005 research/gauge44-leaver8/construction/leaver/CODED-CELLS-k8.json", + "git_blob": "cd23561e0be5bd060e6e0b94643e550374ecd7d8" + }, + "TRI-LEAVER-k8.json": { + "copied_from": "PR1005 research/gauge44-leaver8/construction/leaver/TRI-LEAVER-k8.json", + "git_blob": "e3bb24cc49812a90a82e8e77ee8588f3d00d81e4" + }, + "k8-cell-word.json.gz": { + "content_sha256": "58e14a02f2c1d4dcfeb363ebd5fa2e713064b5c724d90f6721419a8cfa67729b", + "pr_pin": "PR1005 PROOF-NOTE-LEAVER.md 'cell word is cold44 58e14a02...'", + "built_by": "research/gauge44-leaver8/construction/leaver/reproduce_leaver.py --id k8 --word-only (output cold44/FULL-WORD.json.gz)" + }, + "k8-final-word.json.gz": { + "content_sha256": "db2c7cfb3f8eee2b76c2e0154fc530520fb4d90cd9511a002cab527b16033b83", + "pr_pin": "PR1005 README 'final word db2c7cfb...'; PR1018 RECIPE-SLOTS-k8.json base_sha256", + "built_by": "research/gauge44-leaver8/construction/leaver/reproduce_leaver_chain.py --id k8 (output frames/FULL-WORD.json.gz; all 21 chain steps exit 0)" + }, + "k8-seven-slot-word.json.gz": { + "content_sha256": "c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8", + "pr_pin": "PR1018 description 'output c2b29430...'", + "built_by": "PR1018 research/gauge44-slots/construction/slots/verify_slots.py on the rebuilt PR1005 chain (output slots/FULL-WORD.json.gz; PASS_SLOTS_ON_CHECKED_K8_BASELINE 0.00167166528321877)" + }, + "notri-cold44-word.json.gz": { + "content_sha256": "3e99ba778ab8a97853f50912776247802b529439937176363f6c42786163b1f9", + "pr_pin": "PR1005 README no-triangle word '3e99ba77...'", + "built_by": "research/gauge44-leaver8/construction/notri/reproduce_notri.py --word-only (output cold44/FULL-WORD.json.gz)" + }, + "raw-notri.json.gz": { + "content_sha256": "5a55ea28628e3d76ed31393505f4605d7a8d5b002716a44115fea60cdc3477e3", + "built_by": "same run as notri-cold44-word, output raw/FULL-WORD.json.gz" + }, + "raw-k5.json.gz": { + "content_sha256": "c9114254533c7e272504016764c93370e18734469587a86fb07652b85f8ae209", + "built_by": "PR1005 research/gauge44-leaver/construction/leaver/reproduce_leaver.py --id k5 --word-only, output raw/FULL-WORD.json.gz (cell word e10817e0...)" + }, + "raw-k8.json.gz": { + "content_sha256": "85c0e64718a9ceafe094e7152ea27ec9d7f804e514b5efaab085a94b7ef1841f", + "built_by": "same run as k8-cell-word, output raw/FULL-WORD.json.gz" + } + } +} diff --git a/research/leaver-cell-audit-seed65/inputs/CODED-CELLS-k8.json b/research/leaver-cell-audit-seed65/inputs/CODED-CELLS-k8.json new file mode 100644 index 0000000000..cd23561e0b --- /dev/null +++ b/research/leaver-cell-audit-seed65/inputs/CODED-CELLS-k8.json @@ -0,0 +1,2826 @@ +[ + { + "cell": "01+", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 1 + ], + "x1": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 0 + ], + "x2": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 1 + ], + "x3": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 0 + ], + "x4": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 1 + ], + "x5": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 0 + ], + "y0": [ + "target", + 65 + ], + "y1": [ + "target", + 64 + ], + "y2": [ + "target", + 33 + ], + "y3": [ + "target", + 32 + ], + "y4": [ + "target", + 25 + ], + "y5": [ + "target", + 24 + ] + }, + "scaled": [ + [ + "y1", + "x0", + "-1/2" + ], + [ + "y0", + "x1", + "-1/2" + ], + [ + "y2", + "x5", + "-1/2" + ], + [ + "y3", + "x4", + "-1/2" + ], + [ + "y4", + "x3", + "-1/2" + ], + [ + "y5", + "x2", + "-1/2" + ], + [ + "x0", + "x1", + "1" + ], + [ + "x2", + "x5", + "1" + ], + [ + "x4", + "x3", + "1" + ], + [ + "y1", + "x2", + "-1/2" + ], + [ + "y3", + "x0", + "-1/2" + ], + [ + "y5", + "x4", + "-1/2" + ], + [ + "y0", + "y5", + "1" + ], + [ + "y2", + "y3", + "1" + ], + [ + "y4", + "y1", + "1" + ], + [ + "y1", + "x4", + "-1/2" + ], + [ + "y0", + "x5", + "-1/2" + ], + [ + "y2", + "x3", + "-1/2" + ], + [ + "y3", + "x2", + "-1/2" + ], + [ + "y4", + "x1", + "-1/2" + ], + [ + "y5", + "x0", + "-1/2" + ] + ], + "unit": [ + [ + "y1", + "x0", + 1 + ], + [ + "y0", + "x1", + 1 + ], + [ + "y2", + "x5", + 1 + ], + [ + "y3", + "x4", + 1 + ], + [ + "y4", + "x3", + 1 + ], + [ + "y5", + "x2", + 1 + ], + [ + "x0", + "x1", + 1 + ], + [ + "x2", + "x5", + 1 + ], + [ + "x4", + "x3", + 1 + ], + [ + "y1", + "x2", + 1 + ], + [ + "y3", + "x0", + 1 + ], + [ + "y5", + "x4", + 1 + ], + [ + "y0", + "y5", + 1 + ], + [ + "y2", + "y3", + 1 + ], + [ + "y4", + "y1", + 1 + ], + [ + "y1", + "x4", + 1 + ], + [ + "y0", + "x5", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y4", + "x1", + 1 + ], + [ + "y5", + "x0", + 1 + ] + ], + "coefficients": [ + [ + "0", + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "0", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "0", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "-1/2", + "0", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "0", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "0" + ] + ] + }, + { + "cell": "23+", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 23 + ], + "x1": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 3 + ], + "x2": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 1 + ], + "x3": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 0 + ], + "x4": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 1 + ], + "x5": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 0 + ], + "y0": [ + "target", + 71 + ], + "y1": [ + "target", + 67 + ], + "y2": [ + "target", + 97 + ], + "y3": [ + "target", + 96 + ], + "y4": [ + "target", + 89 + ], + "y5": [ + "target", + 88 + ] + }, + "scaled": [ + [ + "y1", + "x0", + "1" + ], + [ + "y0", + "x1", + "1" + ], + [ + "y2", + "x5", + "-1/2" + ], + [ + "y3", + "x4", + "-1/2" + ], + [ + "y4", + "x3", + "-1/2" + ], + [ + "y5", + "x2", + "-1/2" + ], + [ + "x0", + "x1", + "1" + ], + [ + "x2", + "x5", + "1" + ], + [ + "x4", + "x3", + "1" + ], + [ + "y1", + "x2", + "-1/2" + ], + [ + "y3", + "x0", + "1" + ], + [ + "y5", + "x4", + "-1/2" + ], + [ + "y0", + "y5", + "1" + ], + [ + "y2", + "y3", + "1" + ], + [ + "y4", + "y1", + "1" + ], + [ + "y1", + "x4", + "-1/2" + ], + [ + "y0", + "x5", + "-1/2" + ], + [ + "y2", + "x3", + "-1/2" + ], + [ + "y3", + "x2", + "-1/2" + ], + [ + "y4", + "x1", + "1" + ], + [ + "y5", + "x0", + "1" + ] + ], + "unit": [ + [ + "y1", + "x0", + 1 + ], + [ + "y0", + "x1", + 1 + ], + [ + "y2", + "x5", + 1 + ], + [ + "y3", + "x4", + 1 + ], + [ + "y4", + "x3", + 1 + ], + [ + "y5", + "x2", + 1 + ], + [ + "x0", + "x1", + 1 + ], + [ + "x2", + "x5", + 1 + ], + [ + "x4", + "x3", + 1 + ], + [ + "y1", + "x2", + 1 + ], + [ + "y3", + "x0", + 1 + ], + [ + "y5", + "x4", + 1 + ], + [ + "y0", + "y5", + 1 + ], + [ + "y2", + "y3", + 1 + ], + [ + "y4", + "y1", + 1 + ], + [ + "y1", + "x4", + 1 + ], + [ + "y0", + "x5", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y4", + "x1", + 1 + ], + [ + "y5", + "x0", + 1 + ] + ], + "coefficients": [ + [ + "0", + "1", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "1", + "0", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "0", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "-1/2", + "0", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "-1/2", + "-1/2", + "0", + "-1/2" + ], + [ + "1", + "1", + "-1/2", + "-1/2", + "-1/2", + "0" + ] + ] + }, + { + "cell": "45+", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 23 + ], + "x1": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 3 + ], + "x2": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 23 + ], + "x3": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 3 + ], + "x4": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 1 + ], + "x5": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 0 + ], + "y0": [ + "target", + 39 + ], + "y1": [ + "target", + 35 + ], + "y2": [ + "target", + 103 + ], + "y3": [ + "target", + 99 + ], + "y4": [ + "target", + 57 + ], + "y5": [ + "target", + 56 + ] + }, + "scaled": [ + [ + "y1", + "x0", + "1" + ], + [ + "y0", + "x1", + "1" + ], + [ + "y2", + "x5", + "-1/2" + ], + [ + "y3", + "x4", + "-1/2" + ], + [ + "y4", + "x3", + "1" + ], + [ + "y5", + "x2", + "1" + ], + [ + "x0", + "x1", + "1" + ], + [ + "x2", + "x5", + "-1/2" + ], + [ + "x4", + "x3", + "-2" + ], + [ + "y1", + "x2", + "1" + ], + [ + "y3", + "x0", + "1" + ], + [ + "y5", + "x4", + "-1/2" + ], + [ + "y0", + "y5", + "1" + ], + [ + "y2", + "y3", + "1" + ], + [ + "y4", + "y1", + "1" + ], + [ + "y1", + "x4", + "-1/2" + ], + [ + "y0", + "x5", + "-1/2" + ], + [ + "y2", + "x3", + "1" + ], + [ + "y3", + "x2", + "1" + ], + [ + "y4", + "x1", + "1" + ], + [ + "y5", + "x0", + "1" + ] + ], + "unit": [ + [ + "y1", + "x0", + 1 + ], + [ + "y0", + "x1", + 1 + ], + [ + "y2", + "x5", + 1 + ], + [ + "y3", + "x4", + 1 + ], + [ + "y4", + "x3", + 1 + ], + [ + "y5", + "x2", + 1 + ], + [ + "x0", + "x1", + 1 + ], + [ + "x2", + "x5", + 1 + ], + [ + "x4", + "x3", + 1 + ], + [ + "y1", + "x2", + 1 + ], + [ + "y3", + "x0", + 1 + ], + [ + "y5", + "x4", + 1 + ], + [ + "y0", + "y5", + 1 + ], + [ + "y2", + "y3", + 1 + ], + [ + "y4", + "y1", + 1 + ], + [ + "y1", + "x4", + 1 + ], + [ + "y0", + "x5", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y4", + "x1", + 1 + ], + [ + "y5", + "x0", + 1 + ] + ], + "coefficients": [ + [ + "0", + "1", + "1", + "1", + "-1/2", + "-1/2" + ], + [ + "1", + "0", + "1", + "1", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "0", + "1", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "1", + "0", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "1", + "1", + "0", + "-1/2" + ], + [ + "1", + "1", + "1", + "1", + "-1/2", + "0" + ] + ] + }, + { + "cell": "67+", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 23 + ], + "x1": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 3 + ], + "x2": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 23 + ], + "x3": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 3 + ], + "x4": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 23 + ], + "x5": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 3 + ], + "y0": [ + "target", + 31 + ], + "y1": [ + "target", + 27 + ], + "y2": [ + "target", + 95 + ], + "y3": [ + "target", + 91 + ], + "y4": [ + "target", + 63 + ], + "y5": [ + "target", + 59 + ] + }, + "scaled": [ + [ + "y1", + "x0", + "1" + ], + [ + "y0", + "x1", + "1" + ], + [ + "y2", + "x5", + "1" + ], + [ + "y3", + "x4", + "1" + ], + [ + "y4", + "x3", + "1" + ], + [ + "y5", + "x2", + "1" + ], + [ + "x0", + "x1", + "1" + ], + [ + "x2", + "x5", + "1" + ], + [ + "x4", + "x3", + "1" + ], + [ + "y1", + "x2", + "1" + ], + [ + "y3", + "x0", + "1" + ], + [ + "y5", + "x4", + "1" + ], + [ + "y0", + "y5", + "1" + ], + [ + "y2", + "y3", + "1" + ], + [ + "y4", + "y1", + "1" + ], + [ + "y1", + "x4", + "1" + ], + [ + "y0", + "x5", + "1" + ], + [ + "y2", + "x3", + "1" + ], + [ + "y3", + "x2", + "1" + ], + [ + "y4", + "x1", + "1" + ], + [ + "y5", + "x0", + "1" + ] + ], + "unit": [ + [ + "y1", + "x0", + 1 + ], + [ + "y0", + "x1", + 1 + ], + [ + "y2", + "x5", + 1 + ], + [ + "y3", + "x4", + 1 + ], + [ + "y4", + "x3", + 1 + ], + [ + "y5", + "x2", + 1 + ], + [ + "x0", + "x1", + 1 + ], + [ + "x2", + "x5", + 1 + ], + [ + "x4", + "x3", + 1 + ], + [ + "y1", + "x2", + 1 + ], + [ + "y3", + "x0", + 1 + ], + [ + "y5", + "x4", + 1 + ], + [ + "y0", + "y5", + 1 + ], + [ + "y2", + "y3", + 1 + ], + [ + "y4", + "y1", + 1 + ], + [ + "y1", + "x4", + 1 + ], + [ + "y0", + "x5", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y4", + "x1", + 1 + ], + [ + "y5", + "x0", + 1 + ] + ], + "coefficients": [ + [ + "0", + "1", + "1", + "1", + "1", + "1" + ], + [ + "1", + "0", + "1", + "1", + "1", + "1" + ], + [ + "1", + "1", + "0", + "1", + "1", + "1" + ], + [ + "1", + "1", + "1", + "0", + "1", + "1" + ], + [ + "1", + "1", + "1", + "1", + "0", + "1" + ], + [ + "1", + "1", + "1", + "1", + "1", + "0" + ] + ] + }, + { + "cell": "67-", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 2 + ], + "x1": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 21 + ], + "x2": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 2 + ], + "x3": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 21 + ], + "x4": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 2 + ], + "x5": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 21 + ], + "y0": [ + "target", + 26 + ], + "y1": [ + "target", + 30 + ], + "y2": [ + "target", + 90 + ], + "y3": [ + "target", + 94 + ], + "y4": [ + "target", + 58 + ], + "y5": [ + "target", + 62 + ] + }, + "scaled": [ + [ + "y1", + "x0", + "1" + ], + [ + "y0", + "x1", + "1" + ], + [ + "y2", + "x5", + "1" + ], + [ + "y3", + "x4", + "1" + ], + [ + "y4", + "x3", + "1" + ], + [ + "y5", + "x2", + "1" + ], + [ + "x0", + "x1", + "1" + ], + [ + "x2", + "x5", + "1" + ], + [ + "x4", + "x3", + "1" + ], + [ + "y1", + "x2", + "1" + ], + [ + "y3", + "x0", + "1" + ], + [ + "y5", + "x4", + "1" + ], + [ + "y0", + "y5", + "1" + ], + [ + "y2", + "y3", + "1" + ], + [ + "y4", + "y1", + "1" + ], + [ + "y1", + "x4", + "1" + ], + [ + "y0", + "x5", + "1" + ], + [ + "y2", + "x3", + "1" + ], + [ + "y3", + "x2", + "1" + ], + [ + "y4", + "x1", + "1" + ], + [ + "y5", + "x0", + "1" + ] + ], + "unit": [ + [ + "y1", + "x0", + 1 + ], + [ + "y0", + "x1", + 1 + ], + [ + "y2", + "x5", + 1 + ], + [ + "y3", + "x4", + 1 + ], + [ + "y4", + "x3", + 1 + ], + [ + "y5", + "x2", + 1 + ], + [ + "x0", + "x1", + 1 + ], + [ + "x2", + "x5", + 1 + ], + [ + "x4", + "x3", + 1 + ], + [ + "y1", + "x2", + 1 + ], + [ + "y3", + "x0", + 1 + ], + [ + "y5", + "x4", + 1 + ], + [ + "y0", + "y5", + 1 + ], + [ + "y2", + "y3", + 1 + ], + [ + "y4", + "y1", + 1 + ], + [ + "y1", + "x4", + 1 + ], + [ + "y0", + "x5", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y4", + "x1", + 1 + ], + [ + "y5", + "x0", + 1 + ] + ], + "coefficients": [ + [ + "0", + "1", + "1", + "1", + "1", + "1" + ], + [ + "1", + "0", + "1", + "1", + "1", + "1" + ], + [ + "1", + "1", + "0", + "1", + "1", + "1" + ], + [ + "1", + "1", + "1", + "0", + "1", + "1" + ], + [ + "1", + "1", + "1", + "1", + "0", + "1" + ], + [ + "1", + "1", + "1", + "1", + "1", + "0" + ] + ] + }, + { + "cell": "01-", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 19 + ], + "x1": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 17 + ], + "x2": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 19 + ], + "x3": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 17 + ], + "x4": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 19 + ], + "x5": [ + "source", + [ + 0, + 1, + 6, + 7 + ], + 17 + ], + "y0": [ + "target", + 69 + ], + "y1": [ + "target", + 68 + ], + "y2": [ + "target", + 37 + ], + "y3": [ + "target", + 36 + ], + "y4": [ + "target", + 29 + ], + "y5": [ + "target", + 28 + ] + }, + "scaled": [ + [ + "y0", + "x1", + "-1/2" + ], + [ + "y1", + "x0", + "-1/2" + ], + [ + "y3", + "x4", + "-1/2" + ], + [ + "y2", + "x5", + "-1/2" + ], + [ + "y5", + "x2", + "-1/2" + ], + [ + "y4", + "x3", + "-1/2" + ], + [ + "x1", + "x0", + "1" + ], + [ + "x3", + "x4", + "1" + ], + [ + "x5", + "x2", + "1" + ], + [ + "y0", + "x3", + "-1/2" + ], + [ + "y2", + "x1", + "-1/2" + ], + [ + "y4", + "x5", + "-1/2" + ], + [ + "y1", + "y4", + "1" + ], + [ + "y3", + "y2", + "1" + ], + [ + "y5", + "y0", + "1" + ], + [ + "y0", + "x5", + "-1/2" + ], + [ + "y1", + "x4", + "-1/2" + ], + [ + "y3", + "x2", + "-1/2" + ], + [ + "y2", + "x3", + "-1/2" + ], + [ + "y5", + "x0", + "-1/2" + ], + [ + "y4", + "x1", + "-1/2" + ] + ], + "unit": [ + [ + "y0", + "x1", + 1 + ], + [ + "y1", + "x0", + 1 + ], + [ + "y3", + "x4", + 1 + ], + [ + "y2", + "x5", + 1 + ], + [ + "y5", + "x2", + 1 + ], + [ + "y4", + "x3", + 1 + ], + [ + "x1", + "x0", + 1 + ], + [ + "x3", + "x4", + 1 + ], + [ + "x5", + "x2", + 1 + ], + [ + "y0", + "x3", + 1 + ], + [ + "y2", + "x1", + 1 + ], + [ + "y4", + "x5", + 1 + ], + [ + "y1", + "y4", + 1 + ], + [ + "y3", + "y2", + 1 + ], + [ + "y5", + "y0", + 1 + ], + [ + "y0", + "x5", + 1 + ], + [ + "y1", + "x4", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y5", + "x0", + 1 + ], + [ + "y4", + "x1", + 1 + ] + ], + "coefficients": [ + [ + "0", + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "0", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "0", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "-1/2", + "0", + "-1/2", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "0", + "-1/2" + ], + [ + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "-1/2", + "0" + ] + ] + }, + { + "cell": "23-", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 2 + ], + "x1": [ + "source", + [ + 0, + 1, + 2, + 3 + ], + 21 + ], + "x2": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 19 + ], + "x3": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 17 + ], + "x4": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 19 + ], + "x5": [ + "source", + [ + 2, + 3, + 6, + 7 + ], + 17 + ], + "y0": [ + "target", + 66 + ], + "y1": [ + "target", + 70 + ], + "y2": [ + "target", + 101 + ], + "y3": [ + "target", + 100 + ], + "y4": [ + "target", + 93 + ], + "y5": [ + "target", + 92 + ] + }, + "scaled": [ + [ + "y1", + "x0", + "1" + ], + [ + "y0", + "x1", + "1" + ], + [ + "y3", + "x4", + "-1/2" + ], + [ + "y2", + "x5", + "-1/2" + ], + [ + "y5", + "x2", + "-1/2" + ], + [ + "y4", + "x3", + "-1/2" + ], + [ + "x0", + "x1", + "1" + ], + [ + "x3", + "x4", + "1" + ], + [ + "x5", + "x2", + "1" + ], + [ + "y1", + "x3", + "-1/2" + ], + [ + "y2", + "x0", + "1" + ], + [ + "y4", + "x5", + "-1/2" + ], + [ + "y0", + "y4", + "1" + ], + [ + "y3", + "y2", + "1" + ], + [ + "y5", + "y1", + "1" + ], + [ + "y1", + "x5", + "-1/2" + ], + [ + "y0", + "x4", + "-1/2" + ], + [ + "y3", + "x2", + "-1/2" + ], + [ + "y2", + "x3", + "-1/2" + ], + [ + "y5", + "x1", + "1" + ], + [ + "y4", + "x0", + "1" + ] + ], + "unit": [ + [ + "y1", + "x0", + 1 + ], + [ + "y0", + "x1", + 1 + ], + [ + "y3", + "x4", + 1 + ], + [ + "y2", + "x5", + 1 + ], + [ + "y5", + "x2", + 1 + ], + [ + "y4", + "x3", + 1 + ], + [ + "x0", + "x1", + 1 + ], + [ + "x3", + "x4", + 1 + ], + [ + "x5", + "x2", + 1 + ], + [ + "y1", + "x3", + 1 + ], + [ + "y2", + "x0", + 1 + ], + [ + "y4", + "x5", + 1 + ], + [ + "y0", + "y4", + 1 + ], + [ + "y3", + "y2", + 1 + ], + [ + "y5", + "y1", + 1 + ], + [ + "y1", + "x5", + 1 + ], + [ + "y0", + "x4", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y5", + "x1", + 1 + ], + [ + "y4", + "x0", + 1 + ] + ], + "coefficients": [ + [ + "0", + "1", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "1", + "0", + "-1/2", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "0", + "-1/2", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "-1/2", + "0", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "-1/2", + "-1/2", + "0", + "-1/2" + ], + [ + "1", + "1", + "-1/2", + "-1/2", + "-1/2", + "0" + ] + ] + }, + { + "cell": "45-", + "bindings": { + "x0": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 2 + ], + "x1": [ + "source", + [ + 0, + 1, + 4, + 5 + ], + 21 + ], + "x2": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 2 + ], + "x3": [ + "source", + [ + 2, + 3, + 4, + 5 + ], + 21 + ], + "x4": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 19 + ], + "x5": [ + "source", + [ + 4, + 5, + 6, + 7 + ], + 17 + ], + "y0": [ + "target", + 34 + ], + "y1": [ + "target", + 38 + ], + "y2": [ + "target", + 98 + ], + "y3": [ + "target", + 102 + ], + "y4": [ + "target", + 61 + ], + "y5": [ + "target", + 60 + ] + }, + "scaled": [ + [ + "y1", + "x0", + "1" + ], + [ + "y0", + "x1", + "1" + ], + [ + "y2", + "x4", + "-1/2" + ], + [ + "y3", + "x5", + "-1/2" + ], + [ + "y5", + "x3", + "1" + ], + [ + "y4", + "x2", + "1" + ], + [ + "x0", + "x1", + "1" + ], + [ + "x2", + "x4", + "-1/2" + ], + [ + "x5", + "x3", + "-2" + ], + [ + "y1", + "x2", + "1" + ], + [ + "y3", + "x0", + "1" + ], + [ + "y4", + "x5", + "-1/2" + ], + [ + "y0", + "y4", + "1" + ], + [ + "y2", + "y3", + "1" + ], + [ + "y5", + "y1", + "1" + ], + [ + "y1", + "x5", + "-1/2" + ], + [ + "y0", + "x4", + "-1/2" + ], + [ + "y2", + "x3", + "1" + ], + [ + "y3", + "x2", + "1" + ], + [ + "y5", + "x1", + "1" + ], + [ + "y4", + "x0", + "1" + ] + ], + "unit": [ + [ + "y1", + "x0", + 1 + ], + [ + "y0", + "x1", + 1 + ], + [ + "y2", + "x4", + 1 + ], + [ + "y3", + "x5", + 1 + ], + [ + "y5", + "x3", + 1 + ], + [ + "y4", + "x2", + 1 + ], + [ + "x0", + "x1", + 1 + ], + [ + "x2", + "x4", + 1 + ], + [ + "x5", + "x3", + 1 + ], + [ + "y1", + "x2", + 1 + ], + [ + "y3", + "x0", + 1 + ], + [ + "y4", + "x5", + 1 + ], + [ + "y0", + "y4", + 1 + ], + [ + "y2", + "y3", + 1 + ], + [ + "y5", + "y1", + 1 + ], + [ + "y1", + "x5", + 1 + ], + [ + "y0", + "x4", + 1 + ], + [ + "y2", + "x3", + 1 + ], + [ + "y3", + "x2", + 1 + ], + [ + "y5", + "x1", + 1 + ], + [ + "y4", + "x0", + 1 + ] + ], + "coefficients": [ + [ + "0", + "1", + "1", + "1", + "-1/2", + "-1/2" + ], + [ + "1", + "0", + "1", + "1", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "0", + "1", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "1", + "0", + "-1/2", + "-1/2" + ], + [ + "1", + "1", + "1", + "1", + "0", + "-1/2" + ], + [ + "1", + "1", + "1", + "1", + "-1/2", + "0" + ] + ] + } +] diff --git a/research/leaver-cell-audit-seed65/inputs/TRI-LEAVER-k8.json b/research/leaver-cell-audit-seed65/inputs/TRI-LEAVER-k8.json new file mode 100644 index 0000000000..e3bb24cc49 --- /dev/null +++ b/research/leaver-cell-audit-seed65/inputs/TRI-LEAVER-k8.json @@ -0,0 +1,590 @@ +{ + "full_pairs": [ + [ + 0, + 1 + ], + [ + 2, + 3 + ], + [ + 4, + 5 + ], + [ + 6, + 7 + ] + ], + "triangles": [ + { + "p": [ + 0, + 1 + ], + "e": 1, + "reads": [ + [ + 57, + [ + 0, + 1, + 2, + 3 + ], + 0 + ], + [ + 56, + [ + 0, + 1, + 2, + 3 + ], + 1 + ], + [ + 25, + [ + 0, + 1, + 4, + 5 + ], + 0 + ], + [ + 24, + [ + 0, + 1, + 4, + 5 + ], + 1 + ], + [ + 17, + [ + 0, + 1, + 6, + 7 + ], + 0 + ], + [ + 16, + [ + 0, + 1, + 6, + 7 + ], + 1 + ] + ], + "coded": true, + "cell": 0 + }, + { + "p": [ + 2, + 3 + ], + "e": 1, + "reads": [ + [ + 63, + [ + 0, + 1, + 2, + 3 + ], + 3 + ], + [ + 59, + [ + 0, + 1, + 2, + 3 + ], + 23 + ], + [ + 89, + [ + 2, + 3, + 4, + 5 + ], + 0 + ], + [ + 88, + [ + 2, + 3, + 4, + 5 + ], + 1 + ], + [ + 81, + [ + 2, + 3, + 6, + 7 + ], + 0 + ], + [ + 80, + [ + 2, + 3, + 6, + 7 + ], + 1 + ] + ], + "coded": true, + "cell": 1 + }, + { + "p": [ + 4, + 5 + ], + "e": 1, + "reads": [ + [ + 31, + [ + 0, + 1, + 4, + 5 + ], + 3 + ], + [ + 27, + [ + 0, + 1, + 4, + 5 + ], + 23 + ], + [ + 95, + [ + 2, + 3, + 4, + 5 + ], + 3 + ], + [ + 91, + [ + 2, + 3, + 4, + 5 + ], + 23 + ], + [ + 49, + [ + 4, + 5, + 6, + 7 + ], + 0 + ], + [ + 48, + [ + 4, + 5, + 6, + 7 + ], + 1 + ] + ], + "coded": true, + "cell": 2 + }, + { + "p": [ + 6, + 7 + ], + "e": 1, + "reads": [ + [ + 23, + [ + 0, + 1, + 6, + 7 + ], + 3 + ], + [ + 19, + [ + 0, + 1, + 6, + 7 + ], + 23 + ], + [ + 87, + [ + 2, + 3, + 6, + 7 + ], + 3 + ], + [ + 83, + [ + 2, + 3, + 6, + 7 + ], + 23 + ], + [ + 55, + [ + 4, + 5, + 6, + 7 + ], + 3 + ], + [ + 51, + [ + 4, + 5, + 6, + 7 + ], + 23 + ] + ], + "coded": true, + "cell": 3 + }, + { + "p": [ + 6, + 7 + ], + "e": -1, + "reads": [ + [ + 18, + [ + 0, + 1, + 6, + 7 + ], + 21 + ], + [ + 22, + [ + 0, + 1, + 6, + 7 + ], + 2 + ], + [ + 82, + [ + 2, + 3, + 6, + 7 + ], + 21 + ], + [ + 86, + [ + 2, + 3, + 6, + 7 + ], + 2 + ], + [ + 50, + [ + 4, + 5, + 6, + 7 + ], + 21 + ], + [ + 54, + [ + 4, + 5, + 6, + 7 + ], + 2 + ] + ], + "coded": true, + "cell": 4 + }, + { + "p": [ + 0, + 1 + ], + "e": -1, + "reads": [ + [ + 61, + [ + 0, + 1, + 2, + 3 + ], + 17 + ], + [ + 60, + [ + 0, + 1, + 2, + 3 + ], + 19 + ], + [ + 29, + [ + 0, + 1, + 4, + 5 + ], + 17 + ], + [ + 28, + [ + 0, + 1, + 4, + 5 + ], + 19 + ], + [ + 21, + [ + 0, + 1, + 6, + 7 + ], + 17 + ], + [ + 20, + [ + 0, + 1, + 6, + 7 + ], + 19 + ] + ], + "coded": true, + "cell": 5 + }, + { + "p": [ + 2, + 3 + ], + "e": -1, + "reads": [ + [ + 58, + [ + 0, + 1, + 2, + 3 + ], + 21 + ], + [ + 62, + [ + 0, + 1, + 2, + 3 + ], + 2 + ], + [ + 93, + [ + 2, + 3, + 4, + 5 + ], + 17 + ], + [ + 92, + [ + 2, + 3, + 4, + 5 + ], + 19 + ], + [ + 85, + [ + 2, + 3, + 6, + 7 + ], + 17 + ], + [ + 84, + [ + 2, + 3, + 6, + 7 + ], + 19 + ] + ], + "coded": true, + "cell": 6 + }, + { + "p": [ + 4, + 5 + ], + "e": -1, + "reads": [ + [ + 26, + [ + 0, + 1, + 4, + 5 + ], + 21 + ], + [ + 30, + [ + 0, + 1, + 4, + 5 + ], + 2 + ], + [ + 90, + [ + 2, + 3, + 4, + 5 + ], + 21 + ], + [ + 94, + [ + 2, + 3, + 4, + 5 + ], + 2 + ], + [ + 53, + [ + 4, + 5, + 6, + 7 + ], + 17 + ], + [ + 52, + [ + 4, + 5, + 6, + 7 + ], + 19 + ] + ], + "coded": true, + "cell": 7 + } + ] +} diff --git a/research/leaver-cell-audit-seed65/inputs/k8-cell-word.json.gz b/research/leaver-cell-audit-seed65/inputs/k8-cell-word.json.gz new file mode 100644 index 0000000000..fc4f0faefa Binary files /dev/null and b/research/leaver-cell-audit-seed65/inputs/k8-cell-word.json.gz differ diff --git a/research/leaver-cell-audit-seed65/inputs/k8-final-word.json.gz b/research/leaver-cell-audit-seed65/inputs/k8-final-word.json.gz new file mode 100644 index 0000000000..e9d9317fb2 Binary files /dev/null and b/research/leaver-cell-audit-seed65/inputs/k8-final-word.json.gz differ diff --git a/research/leaver-cell-audit-seed65/inputs/k8-seven-slot-word.json.gz b/research/leaver-cell-audit-seed65/inputs/k8-seven-slot-word.json.gz new file mode 100644 index 0000000000..723decbca8 Binary files /dev/null and b/research/leaver-cell-audit-seed65/inputs/k8-seven-slot-word.json.gz differ diff --git a/research/leaver-cell-audit-seed65/inputs/notri-cold44-word.json.gz b/research/leaver-cell-audit-seed65/inputs/notri-cold44-word.json.gz new file mode 100644 index 0000000000..e3a777d2e8 Binary files /dev/null and b/research/leaver-cell-audit-seed65/inputs/notri-cold44-word.json.gz differ diff --git a/research/leaver-cell-audit-seed65/inputs/raw-k5.json.gz b/research/leaver-cell-audit-seed65/inputs/raw-k5.json.gz new file mode 100644 index 0000000000..a46e1c44d2 Binary files /dev/null and b/research/leaver-cell-audit-seed65/inputs/raw-k5.json.gz differ diff --git a/research/leaver-cell-audit-seed65/inputs/raw-k8.json.gz b/research/leaver-cell-audit-seed65/inputs/raw-k8.json.gz new file mode 100644 index 0000000000..46f120fecf Binary files /dev/null and b/research/leaver-cell-audit-seed65/inputs/raw-k8.json.gz differ diff --git a/research/leaver-cell-audit-seed65/inputs/raw-notri.json.gz b/research/leaver-cell-audit-seed65/inputs/raw-notri.json.gz new file mode 100644 index 0000000000..87208e1044 Binary files /dev/null and b/research/leaver-cell-audit-seed65/inputs/raw-notri.json.gz differ diff --git a/research/leaver-cell-audit-seed65/verify.py b/research/leaver-cell-audit-seed65/verify.py new file mode 100644 index 0000000000..3e34e2c5a6 --- /dev/null +++ b/research/leaver-cell-audit-seed65/verify.py @@ -0,0 +1,430 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +# Prepared by Sagar Thakrar with substantial Anthropic Claude assistance. +"""Independent audit of the mutable-leaver all-K cells of PR1005, and of the same cells in PR1018's word. + +Standard library only. No code from the audited packages is imported; their words are read as data +(see SOURCES.json for how each pinned input was produced). The checks follow the documented +scalar/frame semantics of the gauge44 local words: + +E Endpoint. Each data column is replayed forward through precondition + A + cut + B + tail + + cleanup and must give x_t -> x_t + y_t-coordinate, i.e. x -> x, y_t -> y_t + x_t. Each helper + column is replayed through the inverse of the post-precondition program; the result must be + the unit vector plus a target-only residue. That is exactly the condition under which a + pre-main compensation y -= a*h exists. The residue must vanish for entering helpers. +F Frames. Monotone climbs over A, the centre paths, B, the early-cleanup tail and the terminal + ends. The FULL cleanup may touch only registers that end at FULL. The paid histogram must equal + the word's recorded local profile. +L Leaver cells. Each coded cell's 21 scaled gates are located literally (contiguous, in order) + in A + cut + B by unification. Each name binds to one register, the y-names bind to the cell's + six targets (TRI read indices; the coded index is t8 + 8), and the x-names bind to non-targets. + For every mutated leaver: it is not a centre, entering helper or low-ended helper. It is never + touched again in A/cut/B or the tail after its cell, and it is written later in the FULL + cleanup. Its value at the end of B differs from its input, so the restoration is real work. +D Profile deltas. The raw-stage paid profiles of the no-triangle, k5 and k8 words are recomputed + with F and differenced. +Every check raises AuditError directly (no assert), so it also runs under python -O. +""" +import argparse, copy, gzip, hashlib, json, sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +IN = HERE / 'inputs' +PINS = { # sha256 of the decompressed JSON (of the file itself for .json) + 'k8-cell-word.json.gz': '58e14a02f2c1d4dcfeb363ebd5fa2e713064b5c724d90f6721419a8cfa67729b', + 'k8-final-word.json.gz': 'db2c7cfb3f8eee2b76c2e0154fc530520fb4d90cd9511a002cab527b16033b83', + 'k8-seven-slot-word.json.gz': 'c2b294300760e1fd6eeab8c22c4d13e4633dca40e52cac8da0d68163a76e3ca8', + 'notri-cold44-word.json.gz': '3e99ba778ab8a97853f50912776247802b529439937176363f6c42786163b1f9', + 'raw-notri.json.gz': '5a55ea28628e3d76ed31393505f4605d7a8d5b002716a44115fea60cdc3477e3', + 'raw-k5.json.gz': 'c9114254533c7e272504016764c93370e18734469587a86fb07652b85f8ae209', + 'raw-k8.json.gz': '85c0e64718a9ceafe094e7152ea27ec9d7f804e514b5efaab085a94b7ef1841f', + 'CODED-CELLS-k8.json': '7347f814850a838bd617bc7a55c307cec2b72becde2f12ea3e2e1af344b43563', + 'TRI-LEAVER-k8.json': 'b22e6ecf76104de66844bd617c4ca80f5546ba0966a50e5e9aa0ffea4976cb30', +} + + +class AuditError(Exception): + pass + + +def need(ok, msg): + if not ok: + raise AuditError(msg) + + +def read_pinned(name): + data = (IN / name).read_bytes() + raw = gzip.decompress(data) if name.endswith('.gz') else data + need(hashlib.sha256(raw).hexdigest() == PINS[name], 'input pin mismatch: ' + name) + return json.loads(raw) + + +# ------------------------------------------------------------------ scalar semantics + +def regs(g): + return (g[1], g[2]) if g[0] == 'add' else (g[1],) + + +def coef(g): + return Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + + +def forward(gates, col): + for g in gates: + if g[0] == 'add': + x = col.get(g[2]) + if x: + y = col.get(g[1], 0) + coef(g) * x + if y: + col[g[1]] = y + else: + col.pop(g[1], None) + elif g[0] == 'scale': + if g[1] in col: + col[g[1]] *= coef(g) + else: + raise AuditError('unknown gate ' + str(g[0])) + return col + + +def inverse(gates, col): + for g in reversed(gates): + if g[0] == 'add': + x = col.get(g[2]) + if x: + y = col.get(g[1], 0) - coef(g) * x + if y: + col[g[1]] = y + else: + col.pop(g[1], None) + elif g[1] in col: + col[g[1]] /= coef(g) + return col + + +def parts(w): + early = w.get('early_cleanup', []) + ids = [i for i, _ in early] + need(len(ids) == len(set(ids)), 'duplicate early-cleanup index') + tail = [list(w['cleanup'][i][:-1]) + [U] for i, U in early] + cleanup = [g for i, g in enumerate(w['cleanup']) if i not in set(ids)] + return w['precondition'], w['A'] + w['cut'] + w['B'], tail, cleanup + + +def endpoint(w): + v, R = w['report']['v'], w['report']['R'] + n = 2 * v + R + pre, main, tail, cleanup = parts(w) + for g in pre + main + tail + cleanup: + need(all(0 <= r < n for r in regs(g)), 'register out of range') + need(g[0] != 'add' or g[1] != g[2], 'self add') + q = coef(g) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic or zero scalar') + need(all(v <= r < 2 * v for g in pre for r in regs(g)), 'precondition touches a non-target') + full, post = pre + main + tail + cleanup, main + tail + cleanup + entering = {int(k) for k in w.get('start_extra', {})} + bad, residue = [], 0 + for c in range(2 * v): + want = {c: Q(1)} + if c < v: + want[v + c] = Q(1) + if forward(full, {c: Q(1)}) != want: + bad.append(('data', c)) + for k in range(2 * v, n): + out = inverse(post, {k: Q(1)}) + rest = {r: x for r, x in out.items() if r != k} + if out.get(k) != 1 or any(not v <= r < 2 * v for r in rest): + bad.append(('helper', k)) + elif rest and k in entering: + bad.append(('entering-response', k)) + residue += len(rest) + need(not bad, 'endpoint failures %s' % bad[:6]) + return dict(columns=n, data_columns=2 * v, helper_columns=R, target_residue_entries=residue) + + +# ------------------------------------------------------------------ frames + +def span(vectors): + piv = {} + for x in vectors: + need(type(x) is int and x >= 0, 'bad frame vector') + while x: + b = x.bit_length() - 1 + if b in piv: + x ^= piv[b] + else: + piv[b] = x + break + for b in sorted(piv): + for u in piv: + if u > b and piv[u] >> b & 1: + piv[u] ^= piv[b] + return frozenset(piv.values()) + + +def frames(w): + v, h, R = w['report']['v'], w['report']['h'], w['report']['R'] + n = 2 * v + R + FULL = span([1 << i for i in range(h)]) + hyper = lambda p: span([x for x in range(1, 1 << h) if bin(x & p).count('1') % 2 == 0]) + cur = [span([p]) for p in w['ports']] + [span([])] * (v + R) + for q, U in w.get('start_extra', {}).items(): + need(2 * v <= int(q) < n, 'entrance on a non-helper') + cur[int(q)] = span(U) + start = list(cur) + end = [FULL] * v + [hyper(p) for p in w['ports']] + [FULL] * R + for q, U in w.get('helper_final', {}).items(): + end[int(q)] = span(U) + paid = Counter() + + def climb(r, U, where): + U = U if isinstance(U, frozenset) else span(U) + need(span(list(cur[r]) + list(U)) == U, 'non-monotone climb in %s, register %d' % (where, r)) + if len(U) > len(cur[r]): + paid[len(U) - len(cur[r])] += 1 + cur[r] = U + + pre, main, tail, cleanup = parts(w) + for g in w['A']: + for r in regs(g): + climb(r, g[-1], 'A') + need(not w.get('target_levels'), 'nonzero target levels are outside this audit') + need(all(cur[v + t] == span([]) for t in range(v)), 'targets not at level zero before B') + for q, U in zip(w['centers'], w['center_frames']): + need(cur[q] == span(U), 'centre carrier frame') + paid[len(span(U))] += 1 + for g in w['B']: + for r in regs(g): + climb(r, g[-1], 'B') + for g in tail: + for r in regs(g): + climb(r, g[-1], 'tail') + for r in range(n): + climb(r, end[r], 'end') + need(all(end[r] == FULL for g in cleanup for r in regs(g)), 'FULL cleanup touches a low end') + paid = {k: paid[k] for k in sorted(paid)} + need(paid == {int(k): x for k, x in w['report']['local_profile'].items()}, 'paid profile differs from the recorded profile') + return paid + + +# ------------------------------------------------------------------ leaver cells + +def cell_targets(cells, tri): + out = {} + for tr in tri['triangles']: + if tr.get('coded'): + c = cells[tr['cell']] + t8 = {r[0] for r in tr['reads']} + need({b[1] - 8 for b in c['bindings'].values() if b[0] == 'target'} == t8, 'TRI/coded index mismatch ' + c['cell']) + out[c['cell']] = t8 + need(len(out) == len(cells), 'a coded cell lacks a TRI entry') + return out + + +def locate(w, cells, targets): + v = w['report']['v'] + main = w['A'] + w['cut'] + w['B'] + found = [] + for cell in cells: + pat = [(t, s, Q(q)) for t, s, q in cell['scaled']] + T = {v + t for t in targets[cell['cell']]} + hits = [] + for i in range(len(main) - len(pat) + 1): + bind, ok = {}, True + for k, (tn, sn, q) in enumerate(pat): + g = main[i + k] + if g[0] != 'add' or Q(g[3], g[4]) != q: + ok = False + break + for name, reg in ((tn, g[1]), (sn, g[2])): + if bind.setdefault(name, reg) != reg or (name[0] == 'y') != (reg in T): + ok = False + if not ok: + break + if ok and len(set(bind.values())) == len(bind): + hits.append((i, bind)) + need(len(hits) == 1, 'cell %s located %d times' % (cell['cell'], len(hits))) + i, bind = hits[0] + need({bind[x] for x in bind if x[0] == 'y'} == T, 'cell %s target set' % cell['cell']) + found.append(dict(cell=cell['cell'], start=i, stop=i + len(pat), bind=bind, + leavers=sorted({bind[t] for t, s, q in pat if t[0] == 'x'}))) + ivals = sorted((c['start'], c['stop']) for c in found) + need(all(a[1] <= b[0] for a, b in zip(ivals, ivals[1:])), 'overlapping cells') + return found + + +def premise(w, found): + v, R = w['report']['v'], w['report']['R'] + pre, main, tail, cleanup = parts(w) + special = set(w['centers']) | {int(k) for k in w.get('start_extra', {})} | {int(k) for k in w.get('helper_final', {})} + tail_regs = {r for g in tail for r in regs(g)} + rows = [] + for c in found: + for r in c['leavers']: + need(r not in special, 'leaver %d is a centre, entering or low-ended register' % r) + later = [j for j in range(c['stop'], len(main)) if r in regs(main[j])] + need(not later, 'leaver %d touched in main after its cell (index %d)' % (r, later[0] if later else -1)) + need(r not in tail_regs, 'leaver %d touched in the early-cleanup tail' % r) + writes = [j for j, g in enumerate(cleanup) if g[1] == r] + need(writes, 'leaver %d is never written in the FULL cleanup' % r) + rows.append(dict(cell=c['cell'], register=r, kind='data' if r < v else 'helper', + first_full_cleanup_write=writes[0], full_cleanup_writes=len(writes))) + # value after precondition + main, as a linear form in the inputs + want = {row['register'] for row in rows} + form = {r: {r: Q(1)} for r in range(2 * v + R)} + for g in pre + main: + if g[0] == 'add': + dst, q = form[g[1]], coef(g) + for k, x in form[g[2]].items(): + y = dst.get(k, 0) + q * x + if y: + dst[k] = y + else: + dst.pop(k, None) + else: + form[g[1]] = {k: x * coef(g) for k, x in form[g[1]].items()} + need(all(form[r] != {r: Q(1)} for r in want), 'a leaver holds its input value at the end of B') + return rows + + +def audit_word(w, cells, targets): + found = locate(w, cells, targets) + rows = premise(w, found) + return found, dict(R=w['report']['R'], paid_profile=frames(w), endpoint=endpoint(w), + cells=[dict(cell=c['cell'], main_index=c['start'], leavers=c['leavers']) for c in found], + leavers=rows) + + +# ------------------------------------------------------------------ negative controls + +def controls(w, found, cells, targets): + by = {c['cell']: c for c in cells} + nA, nC = len(w['A']), len(w['cut']) + c0 = found[0] + pat = by[c0['cell']]['scaled'] + r0 = c0['leavers'][0] + + def at(i): + return ('A', i) if i < nA else (('cut', i - nA) if i < nA + nC else ('B', i - nA - nC)) + + def outcome(name, m, expect): + for check, fn in (('endpoint', lambda: endpoint(m)), ('frames', lambda: frames(m)), + ('premise', lambda: premise(m, found))): + try: + fn() + except AuditError as e: + need(check == expect, 'control %s rejected by %s, expected %s: %s' % (name, check, expect, e)) + return name, '%s: %s' % (check, str(e)[:70]) + raise SystemExit('CONTROL ACCEPTED: ' + name) + + out = [] + h = w['report']['h'] + FULLF = [1 << j for j in range(h)] + kx = next(k for k, (t, s, q) in enumerate(pat) if t[0] == 'x') + m = copy.deepcopy(w); sec, i = at(c0['start'] + kx); del m[sec][i] + out.append(outcome('N1_drop_leaver_write', m, 'endpoint')) + early = {i for i, _ in w.get('early_cleanup', [])} + k = next(i for i, g in enumerate(w['cleanup']) if i not in early and g[1] == r0) + m = copy.deepcopy(w); del m['cleanup'][k] + m['early_cleanup'] = [[i - (i > k), U] for i, U in w.get('early_cleanup', [])] + out.append(outcome('N2_drop_full_cleanup_restore', m, 'endpoint')) + # A semantically neutral pair at FULL: only the premise check can see it. + pre, main, tail, cleanup = parts(w) + busy = {r for g in tail for r in regs(g)} | set(w['centers']) | {int(q) for q in w.get('helper_final', {})} + v, R = w['report']['v'], w['report']['R'] + hh = max(r for r in range(2 * v, 2 * v + R) if r not in busy) + m = copy.deepcopy(w); m['B'] += [['add', hh, r0, 1, 2, FULLF], ['add', hh, r0, -1, 2, FULLF]] + out.append(outcome('N3_neutral_touch_of_leaver_after_cell', m, 'premise')) + m = copy.deepcopy(w); sec, i = at(c0['start']); m[sec][i][3] *= 3 + out.append(outcome('N4_wrong_cell_coefficient', m, 'endpoint')) + xn = pat[kx][0] + kr = next(k for k, (t, s, q) in enumerate(pat) if k > kx and s == xn) + m = copy.deepcopy(w); a, b = at(c0['start'] + kx), at(c0['start'] + kr) + need(a[0] == b[0], 'control N5 spans sections') + m[a[0]][a[1]], m[b[0]][b[1]] = m[b[0]][b[1]], m[a[0]][a[1]] + out.append(outcome('N5_leaver_write_after_its_read', m, 'endpoint')) + y = next(b for nm, b in c0['bind'].items() if nm[0] == 'y') + e = min(int(q) for q in w['start_extra']) + m = copy.deepcopy(w); m['B'].insert(0, ['add', y, e, 1, 1, FULLF]) + out.append(outcome('N6_entering_dirt_into_cell_target', m, 'endpoint')) + m = copy.deepcopy(w); sec, i = at(c0['start'] + kx); m[sec][i][-1] = [] + out.append(outcome('N7_leaver_gate_below_current_frame', m, 'frames')) + return dict(out) + + +# ------------------------------------------------------------------ driver + +def delta(a, b): + return {r: a.get(r, 0) - b.get(r, 0) for r in sorted(set(a) | set(b)) if a.get(r, 0) != b.get(r, 0)} + + +def scale(u, s): + return {r: s * x for r, x in u.items()} + + +def run(): + cells = read_pinned('CODED-CELLS-k8.json') + targets = cell_targets(cells, read_pinned('TRI-LEAVER-k8.json')) + words = {name: read_pinned(f) for name, f in [('cell', 'k8-cell-word.json.gz'), ('final', 'k8-final-word.json.gz'), + ('seven_slot', 'k8-seven-slot-word.json.gz')]} + res = dict(status=None, audited={}, controls={}) + keep = {} + for name, w in words.items(): + found, res['audited'][name] = audit_word(w, cells, targets) + res['audited'][name]['content_sha256'] = PINS[{'cell': 'k8-cell-word.json.gz', 'final': 'k8-final-word.json.gz', 'seven_slot': 'k8-seven-slot-word.json.gz'}[name]] + keep[name] = found + print('PASS', name, res['audited'][name]['paid_profile'], flush=True) + for name in ('final', 'seven_slot'): + res['controls'][name] = controls(words[name], keep[name], cells, targets) + print('PASS controls', name, len(res['controls'][name]), flush=True) + # Face events: data-register leavers receive one B-section write in both the base and the cell word. + base = read_pinned('notri-cold44-word.json.gz') + v = base['report']['v'] + data_leavers = sorted(r for c in keep['cell'] for r in c['leavers'] if r < v) + def bwrites(w): + return {x: [[g[2], str(coef(g))] for g in w['B'] if g[0] == 'add' and g[1] == x] for x in data_leavers} + wb, wc = bwrites(base), bwrites(words['cell']) + need(all(len(wb[x]) == 1 and len(wc[x]) == 1 for x in data_leavers), 'a data leaver lacks exactly one B write') + awrites = lambda w: [[g[1], g[2], str(coef(g))] for g in w['A'] if g[0] == 'add' and g[1] in data_leavers] + need(awrites(base) == awrites(words['cell']), 'A-section writes to data leavers changed') + res['face_events'] = dict(data_leavers=data_leavers, base_B_write=wb, cell_B_write=wc, + repaired=[x for x in data_leavers if wb[x] != wc[x]]) + # Profile deltas. + raw = {k: read_pinned(f) for k, f in [('notri', 'raw-notri.json.gz'), ('k5', 'raw-k5.json.gz'), ('k8', 'raw-k8.json.gz')]} + P = {k: frames(w) for k, w in raw.items()} + d5, d3 = delta(P['k5'], P['notri']), delta(P['k8'], P['k5']) + unit = {r: x // 5 for r, x in d5.items()} + need(scale(unit, 5) == d5 and scale(unit, 3) == d3, 'raw per-cell deltas are not additive') + need(raw['notri']['report']['R'] - raw['k5']['report']['R'] == 15 and raw['k5']['report']['R'] - raw['k8']['report']['R'] == 9, 'helper counts') + claimed = {1: -30, 2: 6, 3: 6} + slot = delta(res['audited']['seven_slot']['paid_profile'], res['audited']['final']['paid_profile']) + need(slot == scale({3: 2, 4: -4, 5: 2}, 7), 'seven-slot delta is not 7 x {3:+2,4:-4,5:+2}') + res['profile_deltas'] = dict(raw_profiles={k: P[k] for k in P}, k5_minus_notri=d5, k8_minus_k5=d3, + per_cell_raw=unit, helpers_removed_per_cell=3, + pr_description_per_cell=claimed, matches_pr_description=unit == claimed, + rank_mass_per_cell_raw=sum(r * x for r, x in unit.items()), + seven_slot_minus_final=slot) + res['status'] = 'PASS_INDEPENDENT_MUTABLE_LEAVER_AUDIT' + return res + + +if __name__ == '__main__': + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write', action='store_true', help='write RESULT.json instead of comparing with it') + a = ap.parse_args() + try: + res = run() + except AuditError as e: + print('FAIL', e) + sys.exit(1) + text = json.dumps(res, indent=1, sort_keys=True) + '\n' + if a.write: + (HERE / 'RESULT.json').write_text(text) + else: + need((HERE / 'RESULT.json').read_text() == text, 'result differs from committed RESULT.json') + d = res['profile_deltas'] + print('%s cells=8 leavers=%d columns=%d controls=%d per_cell_raw=%s claimed_match=%s' % ( + res['status'], len(res['audited']['final']['leavers']), res['audited']['final']['endpoint']['columns'], + sum(map(len, res['controls'].values())), d['per_cell_raw'], d['matches_pr_description']))