diff --git a/research/t74-retired7-increment-audit/README.md b/research/t74-retired7-increment-audit/README.md new file mode 100644 index 0000000000..94c6111df8 --- /dev/null +++ b/research/t74-retired7-increment-audit/README.md @@ -0,0 +1,451 @@ +# Independent verification (no κ): #2802's seven-stage increment over #2751 (retired5 + retired7 stages); covers #2818's identical construction + +**Status: independent verification (no κ). No defect found: all 28 named rules pass, and all 20 negative controls are +rejected by their named rules (7 of them must also be accepted by named rules, and are). A pass is necessary but not +sufficient for any T74 claim built on this construction. The T74/#1319 supplier admission, native lowering and PR1673 +outer proof are still required. No selected frontier is changed.** + +## What this decides + +Refreshed 2026-10-16 02:10 UTC. PR heads are unchanged at the pins below. + +1. **The word construction.** #2802's seven declared stages turn PR #2751's two BORROW-WORDs into the words with git + blobs `91bd9c68f209…` (base) and `6c4a9a4395cf…` (extra). Fresh code checks this construction independently, and + separates it from #2751 and PR #2766. Seven pending claims build on it: + - #2802 and #2818 ship these words unchanged. + - #2824 (head `f1826afe`), #2827 (head `4dc1286a`) and #2839 (head `2fdd289f`), all by Dugongue, vendor these words + and #2802's fill (`6441c0be…`), then re-allocate or re-price. + - #2833 (jeremykothe2, head `e9307b48`) uses #2818's `retired7_43{base,extra}.json` patch blobs (`f5497db5…`, + `2e02c6a6…`) unchanged, then adds a `dirtentry` stage. + - #2843 (mdumitrean, head `47a7227c`) merges #2833, #2824 and #2827, and adds a T124 allocation on #2833's words. + + These blob identities were read from the GitHub pull-request file lists at 02:10 UTC. They are not part of the + verifier. Further downstream candidates on this base are being discussed in #2612; this list is dated. +2. **#2802's two changed acceptance checks.** Neither is an acceptance gap for κ. + - R is bound to the words. + - Alias occupancy holds for the shipped words. No check on the model's pricing path reads it, so in the finite + model it is a conformance property, not a soundness condition for κ. +3. **Not covered.** + - #2824/#2827's allocations, fills and reserves; #2839's block-norm accounting. + - #2833's `dirtentry` stage and its re-derived fill; #2843's T124 allocation. + - #2818's 10⁻³⁰⁰⁰ endpoint. + - Native lowering, supplier admission and the outer proof. + +## Reproduce + +From the repository root, with `git` and Python (standard library only), in about 2 minutes and under 0.6 GB RSS: + +```sh +python3 -I -B research/t74-retired7-increment-audit/verify.py --fetch +``` + +`--fetch` downloads `refs/pull/{2802,2751,2818,2766}/head` only when a pinned commit is absent, and writes only +`FETCH_HEAD`. Every input is checked against its sha256 pin in `increment_audit.py` (`PINS`). A missing or mismatching +input prints a `FAIL_T74_RETIRED7_INCREMENT_AUDIT inputs: …` line (exit 1). Expected last line: + +```text +PASS_T74_RETIRED7_INCREMENT_AUDIT rules=28/28 controls=20/20 commit2802=17b2ee6ef3cf commit2818=175822aee7a1 +``` + +`--out RECEIPT.json` rewrites the deterministic receipt shipped here. It records every rule's details, and for every +control its failing rules and the expectations it met. If the local zlib does not reproduce #2802's `FILL.json.gz` +bytes, a `NOTE:` line reports the fallback described under "Separating the new construction from its ancestors". + +**Python versions.** Only Python 3.14 has been run. `VERIFY.json` registers the same argv for the repository hook +(`scripts/research_package.py`), which pins Python 3.12. That hook was **not** replayed locally, because only 3.14 is +installed; `--check-only` metadata validation passes. The sources parse under Python 3.10 syntax but were not executed +there. + +## Terms + +- **W2751, W2802.** The parent words (#2751) and final words (#2802). There are two of each: `base` and `extra`. The + providers, the fill dispatch and #2802's code call the base word's provider `gauge44`. +- **Stages.** The *retired5 stages* are `refit5 → alias5 → refit5c`. The *retired7 stages* are + `refit7 → hostmove2 → alias7 → refit7c`. "retired7" in file and rule names follows #2802's package name + (`t74-joint-twelve-retired7`). In this text it means only the last four stages. +- **Alias, lender, follower.** In an alias h←L, a removed *follower* helper h reuses the register of a *lender* L + after L's own life. A B-warp K_G on L marks the hand-over. A *hostee move* re-hosts an existing warp's hostee on a + different lender. +- **Occupancy.** No lender event occurs at or after its alias warp, and no follower event occurs before it. +- **Dead write.** A write to a lender after the lender's last read in its own life. For 401 the last read is A3159 + (`add 400 += −1·401`), and A3160, A3163, A3167 and A3175 are dead writes. +- **Numbering.** "Warp N" is #2802's 1-based op id: the record `warps[N−1]` of the word. Gate positions such as A3175, + B259 or restore60 are 0-based indices into their section. + +## Statement + +PR #2802 (Marius-Paul Dumitrean, head `17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd`, `research/t74-joint-twelve-retired7/`) +turns PR #2751's two T74 BORROW-WORDs (Tekalign, head `4cfbb0cc8314d7fb4e8e754545a49a42eb590a69`) into new words in +seven declared stages. Together these contain: +- seven retired-lender aliases: 606←550, 635←551, 637←552, 638←553, 639←562, 667←401 and 669←403; +- two hostee moves: warp 30 from 401 to 564, and warp 31 from 403 to 565; +- the refit frames. + +#2802 then drops the seven followers' roles from PR #2751's owner fill. It claims κ = C − 10⁻⁴⁶ − 10⁻⁷⁰ with +C = 0.001717794984118634663827, which is +5.38×10⁻⁷ over #2766/#2767. + +We wrote fresh standard-library code and ran it on both words. PR code was read only as pinned data, never imported +or executed. All arithmetic is exact, except the moment-root bracket in item 7, which is rigorous through a written +error budget. The matrix realisation in item 3 is a randomized second method; the free-algebra replay is the exact one. + +1. **S1 event diff.** Every difference between W2751 and W2802 is a declared stage edit. + - **Relabels.** Exactly 63 B gates are relabelled: 35 by `alias5`, 14 by `hostmove2` and 14 by `alias7`. They sit at + exactly the positions of the declared delete/insert pairs. + - **Frames.** Exactly 62 frames change: 26 by `refit5`, 32 by `refit5c`, 2 by `refit7` and 2 by `refit7c`. Each is + present at its declared final value. + - **Warps and helper lists.** Warps 30/31 are replaced in place and warps 66–72 are appended. `removed` gains the + seven followers, and `start_extra` loses only them. + - **Everything else is unchanged** (equal as parsed JSON): `ports`, `centers`, `center_frames`, `target_levels`, + `precondition`, `compensation`, `initial_corrections`, `prelude_events`, `helper_final` and `cut`. A, restore and B + keep their lengths, and their gates are unchanged apart from these relabels. + - **Stage rebuild.** Substituting each stage file's fields, as #2802 does, and re-deriving the cleanup reproduces + W2802 exactly. This checks that the stage files are consistent; it is not an independent derivation. The + independent evidence is the S1 diff plus `S1-STAGE-RECORDS`. Every intermediate state passes the frame chain, its + declared profile and inventory, and both replays. Profiles (helpers, mass) per state: + - `refit5`: 415, 5223; + - `alias5`, `refit5c`, `refit7` and `hostmove2`: 410, 5198; + - `alias7` and `refit7c`: 408, 5188. +2. **S2 occupancy timeline.** Each register's forward event list (corrections, wrapper, A, cut, B, restore) is split at + that register's warps. That gives 704 segments: 632 live registers + 72 B warps in the final word, and 639 + 65 in + the parent. The count equals the size of the register namespace because, in both words, there are as many removed + registers as warps. Every final segment is exactly one parent role, with the same events and the same gates up to + the declared relabel, in time order. The new warps: + + | follower ← lender (warp) | lender's last own event | warp before | follower's first event | + |---|---|---|---| + | 606 ← 550 (66) | B901 | B947 | B947 | + | 635 ← 551 (67) | B902 | B1024 | B1024 | + | 637 ← 552 (68) | B909 | B1027 | B1027 | + | 638 ← 553 (69) | B910 | B1030 | B1030 | + | 639 ← 562 (70) | B903 | B1033 | B1033 | + | 667 ← 401 (71) | **A3175** (27 A + 54 compensation events) | B259 | B259 | + | 669 ← 403 (72) | **A3174** (26 A + 60 compensation events) | B262 | B262 | + | hostee of warp 30 → 564 | B911 | B941 (was B941 on 401) | B941 | + | hostee of warp 31 → 565 | B912 | B944 (was B941 on 403) | B944 | + + Further checks on the timeline: + - No lender has a restore event, and no follower has an event before its warp. + - The old lenders 401/403 keep no hostee event. + - The cleanup is the exact inverse-reverse of the recorded program. It is re-derived and equals the shipped + 4,547 items. Within each register's cleanup, the order is therefore mirrored: follower, inverse warp, lender. + - The dual orientation applies g⁻ᵀ item by item in the same order, and each g⁻ᵀ touches the same registers as g. So + the timeline, and this check, are the same in both orientations. +3. **S2 replay.** An exact replay over ℚ⟨free group⟩ treats all 632 live registers as independent dirty symbols and + the 72 private zero buffers as zero. + - It passes forward (Yᵢ ← Yᵢ + Xᵢ) and dual (Xᵢ ← Xᵢ − Yᵢ). The dual treats K⁻ᵀ as new free letters. + - Before cleanup, each restored helper is its own input and is read by no other register. + - A second, independent method realises every K_op as a random invertible 4×4 matrix over GF(2⁶¹−1), with K⁻ᵀ the + actual inverse transpose. It also passes forward and dual, for 2 seeds. +4. **S3 frames.** The check covers 72 B warps and 24 prelude warp items. For each: + - G is invertible over GF(2), dim U = dim E, G(U) = E and G⁻ᵀ(U^⊥) = E^⊥; + - the binary-symplectic image of K_G is symplectic and maps L_U onto L_E. + + Each B warp's U equals the lender's **actual propagated frame**, taken from our own literal frame chain. The new + and moved warps are 30, 31 and 66–70 (dim 5) and 71–72 (dim 4). Every gate climbs monotonically. + + Refit exactness, against the propagated floor (the join of the incident registers' pre-gate frames): + + | stage | frames at the floor | + |---|---| + | `refit5` | 26/26 | + | `refit7` | 2/2: B911/B912, dim 6→5 | + | `refit7c` | 2/2: B1170/B1171, dim 6→5 | + | `refit5c` | 25/32 | + + Seven `refit5c` frames sit above the floor: B771, B773, B776, B778, B783 and B788 (dim 5, floor 4), and restore60 + (dim 8, floor 6). **They cost nothing.** Lowering any one of them, or all seven, to the floor keeps the chain legal + and leaves the local profile unchanged (`S3-ABOVE-FLOOR-NEUTRAL`). They are #2802's own `refit5c` choices; PR2766's + word does not contain them (see the attribution section below). +5. **S4 profile.** Our recount gives the local profile `{1:2382,2:648,3:268,4:128,5:26,8:8}` (mass 5188) on both words. + - This equals the word reports and both providers' `actual_paid_profile`. + - A second frame chain represents subspaces by canonical reduced bases instead of element sets. It gives the same + profile and inventory, confirms every warp's U and G(U) = E, and reproduces the parent's profile. + - The width inventory is `{4:26,5:2,7:62,8:78,9:240}` = 408 helpers. The ordered widths dim(end) − dim(entrance) + equal the providers' `widths`. +6. **S5 fill with word-derived R.** R = 408 and the per-helper widths are derived **from the words**, not from the + providers. + - The fill's 271,728 = 666 × 408 roles cover each call's helper set exactly once. + - Each role lies strictly inside its window. We rebuilt the 1,332 windows from GLOBAL-TEMPLATE and ORDER. + - No family hosts two helpers in one call. + - Bins are disjoint, within capacity and prefix-compact. The idle remainders are + `{1:17316,3:6594,5:9878,32:1,48:26558}`. + - Independently, FILL equals FILL2751 minus exactly the 4,662 = 666 × 7 roles of the seven followers, with every bin + and in-bin order preserved over 122,625 bins. +7. **S6 price (repeat check).** + - The complete profile is `{1:1603728,2:431568,3:185082,4:85248,5:27194,8:5328,32:1,48:26558}`. Its mass is + 4,816,512 = 2·73·33,152 − 2·11,840. + - Let f(z) = Σ nᵣ (r/73)^(1−z). Then f(C) < 66,304 < f(C + 10⁻²⁴). + - f is evaluated at 80 digits. Python's Decimal `ln`/`exp` are correctly rounded, half-even, whatever the context + rounding mode; the other operations use directed rounding. A written error budget, in `root_bracket`, bounds the + relative error below 3×10⁻⁷⁸. The bracket is widened by a 10⁻⁷⁰ relative slack in a 100-digit directed context. + - After widening, f(C) is 4.36×10⁻²⁰ below 66,304 and f(C + 10⁻²⁴) is 1.46×10⁻¹⁹ above it. + - κ = C − 10⁻⁴⁶ − 10⁻⁷⁰ exactly. The margins are: + - over #2751: `326698885104162859/500000000000000000000000`; + - over #2766: `538010651632355557/1000000000000000000000000`; + - over #2767: 5.380106516323555560552…×10⁻⁷. +8. **#2818 (Jeremy Kothe, head `175822aee7a1858ec653f7f92d7a750aec2c2795`).** + - These files are byte-identical to #2802's: its words (`new/borrow/words/BORROW-WORD-43{base,extra}.json.gz`), + `new/borrow-fill/FILL.json.gz`, `ORDER.json` and `new/BORROW-PROVIDERS.json`. + - Its DISPATCH is the same map, and every field of its `retired7_43{base,extra}.json` patch equals #2802's final word. + - The verdict above therefore covers #2818's construction. Its 10⁻³⁰⁰⁰ endpoint certificate is not checked here. + +**Positive control.** The same code runs on the #2751 parent. It reproduces that profile +`{1:2366,2:646,3:297,4:120,5:26,8:8}` (415 helpers), both replays, and the parent fill of 276,390 roles with R = 415. +The fill's complete profile equals #2751's claim. + +## Separating the new construction from its ancestors + +#2802's κ composes three steps over #2751. Each is priced here with the same code and bracketed with the same root +evaluator. #2802's README already states this split, and #2802 records retired5's endpoint, fill hash and local +profile in `evidence/retired5/`. This audit **independently reproduces** those recorded values; it does not originate +them. + +| step | what is checked | endpoint C (root in [C, C + 10⁻²⁴]) | gain | +|---|---|---|---| +| PR2766 (DavidAriasC) | PR2766's own pinned word differs from W2751 only at B1151 (dim 6→5), the same frame as #2802's `refit5c`. Recounted, it gives PR2766's reported local profile (H1 −2, H2 +1 per call). With FILL2751 that yields PR2766's claimed complete profile. | 0.001717256973467002308270 | (PR2766's claim) | +| retired5 stages: `refit5`, `alias5`, `refit5c` | Rebuilt as the `refit5c` state. Its fill is FILL2751 minus the five followers, re-tiled. Local profile `{1:2386,2:642,3:274,4:128,5:26,8:8}` and endpoint equal #2802's records. The reconstructed fill's gzip sha256 equals #2802's recorded `3501f6bd…` (see the note on the fill hash below). | 0.001717409316335491643448 | +1.52342868489335178×10⁻⁷ over PR2766 | +| retired7 stages: `refit7`, `hostmove2`, `alias7`, `refit7c` | All rules above | 0.001717794984118634663827 | **+385667783143020379/10²⁴ ≈ 3.857×10⁻⁷ over retired5** | + +**Provenance of the 20 frames.** #2802's README lists "PR2766's frame refit … B1151 … plus A0–A11, B771–788 and +restore 60". PR2766's own word changes **only B1151**. The other 19 `refit5c` frames are not in PR2766's word: +A0–A11 (dim 1→0), B771/773/776/778/783/788 (4→5) and restore60 (6→8). They are cost-neutral. Applied alone to W2751, +they leave its profile unchanged. Reverted to W2751's values in the final word, they leave the final profile unchanged +and the chain legal. Together with B1151 they give exactly PR2766's profile. All seven above-floor frames are among +these 19. + +**Who did what.** Both steps are first published in #2802 by the same author. Retired5 was the author's local branch. +Its words are not shipped as files, but they are rebuilt here from #2802's published stage files (`S1-STAGE-CHAIN`). +Only its fill is unpublished; #2802 records its endpoint, local profile and fill hash. The part #2802 labels new is the +retired7 stages. + +**Note on the fill hash.** #2802 hashes the gzip bytes of its fills, and gzip output depends on the zlib build. +`ATTRIBUTION-RETIRED5` first checks that our serializer reproduces #2802's pinned `FILL.json.gz` bytes exactly. Only +then does it compare the reconstructed retired5 fill with #2802's recorded `fill_sha256`. This was the case on the +machine that produced the shipped receipt (zlib 1.3.1; `fill_gzip_sha256_equals_recorded: true`). Otherwise the rule +reports that comparison as not applicable and still requires the reconstruction's canonical-JSON sha256 to equal a pin +recorded here (`ef4bd5d4…`, the same fill content), and `verify.py` prints a `NOTE:` line. The same serializer does +not reproduce #2751's `FILL2751.json.gz` bytes; that file is never compared by gzip hash. + +## The two acceptance checks #2802 changed + +**R read from the providers.** `independent_owners.check` sets R to the length of the providers' widths, and those +widths are themselves under test. This is **not an open gap**: +- #2802's `verify.py` `compact()` requires the new provider widths to equal the parent widths re-indexed by the + word-derived live set. +- The inherited ENTRANCE-WIDTH-BINDING stage of `new/rebuild_borrow.py` binds the word-derived widths to the providers. + Its code is present both in #2802's overlay and in #2818. #2802's recorded release logs show + `ENTRANCE-WIDTH-BINDING ... bound True` for both words (author-recorded; not re-run here). +- Our S5 makes the binding explicit and independent. Control C8 keeps follower 667 live: providers and fill still say + 408, but the words say 409. Control C11 adds helper index 408. `S5-FILL-WORD-DERIVED-R` rejects both. + +**Alias occupancy and the replaced control.** For `alias7`, #2802 replaced the control "warp before lender retirement" +with "warp after the follower's first gate", because 401/403 retire in A. Only 401/403 do. Lenders 550–553/562 retire +in B (B901–B910) and keep the original control. No shipped control moves 401's or 403's own event past its alias warp, +so we built such mutants from their A events. 401's last read is A3159 and its last write is the dead write A3175 +(`add 401 += 41`). 403's last read is A3145 and its last write is the dead write A3174. The table summarises the +mutants: + +| mutant | both scalar replays | frame chain (S3S4, second recount, refits) | fill (S5) and price (S6) | rejected by | +|---|---|---|---|---| +| C4a 401 / C4c 403: last (dead) write moved into B right after the alias warp, own frame | accept | reject: `frame not monotone` at B259 / B262 | S5 accepts; S6 fails only because S3S4 failed | the frame chain. OCC, S1-DIFF and S1-STAGE-RECORDS report errors caused by the inserted B gate shifting later B indices and warp positions; these fire first, and OCC's segment-equality check would also reject the moved event, which lies inside the lender's final segment. X-2818 fails on any edit | +| C4b 401: last (dead) write moved to the end of restore, own frame | accept | reject (not monotone) | S5 accepts; S6 fails as above | OCC (`final segment of 401 … not exactly follower 667`) and the frame chain; S1-DIFF/X-2818 as an undeclared edit | +| C4d 401 / C4e 403: last (dead) write moved to the end of restore **at frame FULL** | accept | **accept** | **accept**: profile, fill and price unchanged | **only** OCC-TIMELINE, plus S1-DIFF and X-2818 as an undeclared edit | +| C4f 401: last read (A3159, `add 400 += −1·401`) moved to the end of restore at FULL | **reject**: `forward target 0 wrong before cleanup` | accept | accept | the replays; OCC, S1-DIFF and X-2818 | +| C4g 401: last write *before* its last read (A3158, `add 401 += 400`) moved to the end of restore at FULL | **reject**: matrix `wrong on register 112`, free `forward target 0 wrong before cleanup` | accept | accept | the replays; OCC, S1-DIFF and X-2818 | + +The verifier checks the C4a–C4c replay cells and every cell of the C4d–C4g rows as `must_accept` and `exact_failing` +expectations. The other cells are read from each control's recorded failing set in `RECEIPT.json`. + +This has three consequences. + +1. **Occupancy is a conformance property, not a soundness condition for κ, in the finite model.** No rule on the + model's pricing path reads occupancy. Our replays, frame chain, recount, fill and price do not, and neither does the + pinned PR2679 auditor (read, not run). A word that violates occupancy but passes those rules is therefore correct in + the model's sense and is priced by its own profile. C4d/C4e show that such words exist; here their price is + identical. + - *Why C4d passes.* The moved write is dead. Follower 667 borrows the register dirty, and the targets come out the + same with the changed content it finds there (both replays confirm this for these words). The cleanup is + re-derived as the inverse-reverse of the whole recorded program, so it undoes the moved write first. + - *What the replay catches.* A moved read (C4f) or a moved write that the lender still reads (C4g) changes what is + computed, and both replays reject it. + + These are examples, not a classification of every possible occupancy violation. The structural statement above is + what carries the conclusion. +2. **Which checks enforce occupancy** (all read, not run): + - **#2802.** The registered `verify_retired7.py` enforces it structurally, not semantically. + - Every stage must leave A and restore unchanged apart from declared refit frames ("alias5 records", + "hostmove2 changes nothing else", "alias7 records"). The final word must equal the rebuilt chain ("declared + stages rebuild the candidate word"). No event of 401/403, which lie in A, can therefore move. + - On the pre-alias states it checks "lenders retired before their followers enter" (retired5, on W2751) and + "alias7 lenders retired before their followers enter". After `hostmove2` it checks "old lenders untouched after + their A lives". + - The `alias5`/`alias7` B edits are checked only against their own declarations (`kernel_gate_edit` equals + `declared_gate_edit`). #2802 checks that an edit is exactly a relabel from the warp position only for + `hostmove2`. That the declared alias edits are exactly the follower relabels is established here by S1-DIFF and + S1-STAGE-RECORDS. + + The pinned PR2679 auditor and the retired7 tamper suite contain no occupancy predicate. Their monotone climb + should reject C4a/C4b/C4c-type mutants. We expect them to accept C4d-type mutants, since our implementations of + the same replay, frame chain and profile do. + - **#2818.** `rebuild_borrow.py` applies retired7 as one patch whose A, B, removed, start_extra and warps fields + replace the parent's. Its checks are: the B edit equals the patch's own declaration, some fields are unchanged, + the final word equals the rebuilt state, plus the auditor and five stage controls. We found no occupancy predicate. + #2818's words are byte-identical to #2802's, so OCC-TIMELINE establishes occupancy for them directly. +3. **What is missing is at most a regression control**, not an acceptance check. A control that expects + `frame not monotone` would not cover C4d-type moves. An optional regression control could add a C4d-type mutant + against #2802's stage-structure check, or an occupancy predicate to #2818's patch check. Neither is needed for κ in + the finite model. + +Unchecked here: whether any layer outside the finite model relies on occupancy, for example a native lowering or +physical hosting that assigns one role per register segment. PR2226 `PROOF.md` §1 speaks of a "retiring field". Its +identity, that R_in = T_E K_G T_U⁻¹ has Fourier rank zero, is an exact operator-level (Clifford) statement, phases +included, and does not refer to the field's later use. This audit checks only its model-level conditions: G(U) = E, +G⁻ᵀ(U^⊥) = E^⊥ and K_G(L_U) = L_E, with U the propagated frame. C4d satisfies them. The exact native form is Open Q3. + +## Negative controls + +A control counts only if the named rule rejects the mutant, every `must_accept` rule accepts it, the failing set +matches `exact_failing` where one is given, and no rule crashes. The cleanup of every word mutant is re-derived from +its own forward program, so a stale cleanup is never the reason for a rejection. Each mutant is re-checked by every +rule except four kinds: the parent positive control, the stage-chain rules, the attribution rules and the above-floor +neutrality rule. Those rebuild, reprice or vary unmutated inputs, and run once on the pinned inputs. Word controls +mutate the base word unless marked *extra*; C8 mutates both words, C11 the fill and C14 #2818's copy of the base word. + +| control | rule | reason recorded | +|---|---|---| +| C1 `refit7` B911 undone (dim 6) | S3S4-FRAMES-PROFILE | warp frame mismatch: op 30 lender 564 | +| C2 hostee move 401→564 reverted | OCC-TIMELINE | follower 667 outlives the segment (401 would host 667 and hostee 30 at once) | +| C3 warp 66 placed before lender 550's last gate B901 | OCC-TIMELINE | lender 550 has an own event at/after its alias warp | +| C4a 401's last (dead) A write moved into B after warp 71 | S3S4-FRAMES-PROFILE | frame not monotone: register 401 at B259 (both replays must accept) | +| C4b 401's last (dead) A write moved to the end of restore | OCC-TIMELINE | final segment of 401 after warp 71 is not exactly follower 667 (both replays must accept) | +| C4c *extra*: 403's last (dead) A write moved into B after warp 72 | S3S4-FRAMES-PROFILE-extra | frame not monotone: register 403 at B262 (both replays must accept) | +| C4d 401's last (dead) A write moved to the end of restore at FULL | OCC-TIMELINE | final segment of 401 after warp 71 is not exactly follower 667. Must be accepted by the replays, frames, recount, refits, stage records, fill and price; fails exactly {OCC-TIMELINE, S1-DIFF, X-2818} | +| C4e *extra*: 403's last (dead) A write moved to the end of restore at FULL | OCC-TIMELINE-extra | final segment of 403 after warp 72 is not exactly follower 669. Same acceptance and exact-failure expectations as C4d | +| C4f 401's last A read (A3159, `add 400 += −1·401`) moved to the end of restore at FULL | S2-REPLAY-FREE | forward target 0 wrong before cleanup. Must be accepted by the frames, recount, refits, stage records, fill and price; fails exactly {both replays, OCC-TIMELINE, S1-DIFF, X-2818} | +| C4g 401's last A write before its last read (A3158, `add 401 += 400`) moved to the end of restore at FULL | S2-REPLAY-MATRIX | matrix realisation (forward, seed 1) wrong on register 112. Same acceptance and exact-failure expectations as C4f | +| C5 warp 71 after follower 667's first gate | OCC-TIMELINE | follower 667 has an event before alias warp 71 | +| C6 wrong G on warp 71 | S3S4-FRAMES-PROFILE | G(U) != E | +| C7 consistent (U′, G(U′)) on warp 71, U′ ≠ propagated frame | S3S4-FRAMES-PROFILE | warp frame mismatch: op 71 lender 401 | +| C8 removed follower 667 kept live | S5-FILL-WORD-DERIVED-R | role count 271728 != 666 × word-derived 409 | +| C9 lenders of warps 71/72 swapped (declaration conformance) | OCC-TIMELINE | alias warp 71 is not on lender 401 | +| C10 first restore gate dropped | S2-REPLAY-FREE | restored helper 572 not its own input | +| C11 fill inflated to R + 1 helper indices | S5-FILL-WORD-DERIVED-R | role count 272394 != 666 × 408 | +| C12 one hostee-30 gate left on 401 | S1-DIFF | B941 is not the declared relabel | +| C13 undeclared frame raise (B1500 → FULL) | S1-DIFF | undeclared frame changes | +| C14 #2818 base word altered by one sign | X-2818-SAME-CONSTRUCTION | words differ | + +## Scope, inherited assumptions and unresolved obligations + +- **Model.** We check the finite BORROW-WORD model as written in PR2226 `PROOF.md` and the PR2679/PR2751 lineage: + frames, rank-zero K_G warps, COPY charges, derived cleanup and windows. The model itself is not validated. Its + conventions are taken as the specification: free warps, free cleanup at FULL, idle children priced by remainder, and + the window rule rebuilt from the template. +- **Not re-derived here.** PR #2751's twelve-source recovery, its 4(H8−H7−H1) delta and the PR2720 reconciliation. A + sibling session claimed these in #2612. We use W2751 as a pinned parent and check that #2802's copies are + byte-identical to #2751's own files. +- **Author-recorded in #2802's release; not independently re-checked here.** + - The native lowering of both final words, including Clifford recipes and warp-recipe checks for the new warps 30, + 31 and 66–72 (`evidence/retired7/NATIVE-RECEIPT.json`, `NATIVE-STANDALONE.json`). + - The strict T74 assembly (`RELEASE-VERIFY-RESULT.json`, stage `strict-t74`). That record carries κ + 0.001714849224721887, not the claimed κ. This is the supplier-only κ of the strict supplier assembly under its + older outer witness, the same value that #2818's `CLAIM.json` reports as `kappa` and explains in `kappa_layers`. + - The modern outer arithmetic that yields the claimed κ (`ADMISSION-RESULT.json`, `complex_lower` = C). + - This audit checks the new warps only through their binary-symplectic image. +- **Inherited and open.** + - By #2802's own scope statement: the all-size compiler, common-label/mutable-source realization, whole-call hosting, + precision/tape, exact recovery, analytic transfer, the PR559 recurrence correction and the PR589 bit H1–H5 + assumptions. + - The T74/#1319 supplier admission and the PR1673 capped phase-cell fusion outer. + - The physical stock identity 66,794 = 66,304 + 408 + 8 + 72 + 2. Of its components, R = 408 and the 72 buffers + (= |helper_final|) agree with the words. + - The "at most two aliases" census and philippeVV's 670/671 pigeonhole in #2802. + - #2818's 10⁻³⁰⁰⁰ endpoint. +- **Claim strength.** This is a finite exact check of one construction, not a proof of the multiplication theorem. + A pass removes no inherited obligation. + +## Changes after review (round 1) + +AI review passes in the same loop raised these points; all are addressed here. +- **Overstated claim about occupancy.** The previous text said only frame monotonicity and occupancy reject C4a/C4b, + and proposed controls "expecting frame not monotone". Per the receipt, S1-DIFF and X-2818 also reject them. Variant + C4d shows that frame monotonicity does not protect occupancy. The section above, and controls C4c–C4f, replace that + text. +- **Wrong frame provenance.** The 20 frames had been attributed to PR2766 as #2802 lists them. PR2766's word changes + only B1151; rule `ATTRIBUTION-PR2766-WORD` now checks against PR2766's pinned word. +- **Split not credited to #2802.** The retired5/retired7 split had been presented as derived here. It is #2802's own + split; the rule now also matches #2802's recorded retired5 endpoint, profile and fill hash. +- **Root-bracket slack applied at too low a precision.** Our own re-reading found that the 10⁻⁷⁰ slack was applied in + Python's default 28-digit context, where it rounds away. The earlier PASS stood only because the actual margins + (three root brackets, six margins, minimum 1.046×10⁻²⁰) exceed 28-digit rounding (≤ 5×10⁻²⁴). The widening is now + done at 100 digits with directed rounding, and the error budget is written down. +- **Verifier output.** The verifier now emits the 24 prelude warp items, the 35/14/14 relabel split and refit7c's + dims. A pin mismatch now prints a FAIL line instead of a traceback. + +## Changes after review (round 2) + +AI review passes in the same loop raised these points; all are addressed here. No number, rule verdict or conclusion +changed; one control was added. +- **Occupancy wording too general.** "A lender write moved past its alias warp at FULL is correct" holds for dead + writes, not for every write; a referee mutant moving 401's write A3158 was rejected by both replays. "So … cannot + change κ" inferred a universal from two examples. The conclusion now rests on the structural fact that no pricing + check reads occupancy, explains why C4d passes, and new control C4g (with `must_accept`/`exact_failing` for C4f and + C4g) machine-checks that a moved write the lender still reads is rejected by the replays. +- **PR2226 §1 overstated.** The model checks only the binary-symplectic conditions of the Clifford identity, not the + identity itself; the paragraph now says so. +- **Fill-hash fallback undisclosed.** The zlib-dependent comparison and its canonical-JSON fallback are now described, + and `verify.py` prints a `NOTE:` line if the fallback runs. +- **strict-t74 κ.** The release record carries the supplier-only κ, not the claimed κ; the scope list now says so. +- **Precision.** Scoped "no shipped control" to 401/403; marked the optional regression control as optional; described + #2802's structural checks exactly (pure-relabel check only for `hostmove2`); retired5's words are rebuilt from + published stage files; the native inputs of Open Q1/Q3 are obtainable through #2802's `full_replay.py`; stated that + C8, C11 and C14 do not mutate only the base word; stated the 1-based warp and 0-based gate numbering; corrected the + bracket count; moved Reproduce up; and refreshed "What this decides" (#2839 and #2843 added). + +## Open next questions + +1. **Does any layer outside the finite model rely on alias occupancy?** *Why:* in the model, a C4d-type violation is + correct and identically priced. Occupancy therefore matters only if the native lowering, physical hosting or + routing reads a warp as the hand-over point of a register. *First step:* inspect whether #2802's native lowering + (full release) assigns roles per register segment. If it does, add a C4d-type mutant against #2802's stage-structure + check and an occupancy predicate to #2818's patch check. *Access:* not blocked. #2802's `full_replay.py` downloads + and authenticates the 491 pinned PR2679 files and rebuilds the native providers; it needs the packages in #2802's + `requirements.txt` (author-recorded cold run: 411 s). An independent check should read its outputs as data. +2. **Is the whole refit frame assignment optimal under the moment cost?** `refit5c` claims "certified optimal". *Why:* + a better assignment could only raise κ. It cannot invalidate the checked value, and the seven above-floor frames + carry no cost. *First step:* an independent exact optimiser over all gates' frames with the same COPY pricing. + *Blocked by:* a written objective for the #1186 `optimal_frames` certificate. +3. **Do the new warps 30, 31 and 66–72 have exact native Clifford/Gaussian lifts in both orientations?** *Why:* #2802 + records them, but this audit checks K_G only through its binary-symplectic image. *First step:* instantiate the + exact Gaussian products of each new K_G and check every column, as PR2226 did for its 80 pairs. *Access:* the native + inputs are rebuilt by #2802's `full_replay.py` from the pinned PR2679 sources, as in Q1. + +## Credits and provenance + +- **Checked work.** + - Marius-Paul Dumitrean (mdumitrean), PR #2802: the retired5 and retired7 stages, the census and the recorded + retired5 evidence. + - Jeremy Kothe (jeremykothe2), PR #2818: repackages #2802 with a finer endpoint (concurrent work). Also the + PR2673/#2745 lineage, the gmx-t74-borrow43 machinery, and PR #2767, whose κ is one of the margins checked here. + - Tekalign (tekuuu), PR #2751: the parent words, fill transform and independent checkers. + - Philippe Van Velzen (philippeVV), PR #2679/#2559: the retired-lender alias and the pre-life hostings. + - Cinna Davis, PR #2226: anticipatory dirty borrowing and the free-operator replay idea. + - Mason Hale, PR #2696: the eight-lender assignment. + - DavidAriasC, PR #2766: the B1151 refit of #2751's words, composed from mdumitrean's PR2733 refit. + - Vlado Vojdanovski (Vlado-V), PR #2322: the coherent handoff in the word lineage. + - zxv, PR #2530. +- **Downstream claims named in "What this decides".** Dugongue (#2824, #2827, #2839), jeremykothe2 (#2833) and + mdumitrean (#2843). Their own stages are not checked here. +- **Related prior audit.** commdata2338's PR #2656 independently audited PR #2588's swapped-alias frame bill and lender + handoffs. That is the same kind of check applied here to #2802's aliases. No code or data from it is used. +- **Related work by the same account (disclosed).** + - The merged `research/t74-borrow43-independent-check` (PR #2315) was a semantic reference for the BORROW-WORD model; + no code was copied. + - Sibling PR #2804 audits #2530's words and the #2679 order/windows. + - The concurrent sibling #2612 claim covers #2751's twelve-source recovery. + - The pinned PR2679 auditor and the #2802/#2818 scripts were read as data only. +- **Base and assignment.** Base `544a7e82810e30cab61c297cb2e2ea86127fe944` (priority revision 5). Sprint track 60–74 + (adversarial audit), OS seed 71. Claim: Discussion #1163 comment 18961174. Canonical thread: Discussion #2612. +- **AI assistance.** Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). + One session wrote and ran the code and these notes. AI review passes in the same loop (reproducibility, + mathematics, provenance, referee) reviewed them in two rounds, and two revisions addressed their findings. No human + has checked the findings by hand. Apache-2.0. diff --git a/research/t74-retired7-increment-audit/RECEIPT.json b/research/t74-retired7-increment-audit/RECEIPT.json new file mode 100644 index 0000000000..f395e7b47f --- /dev/null +++ b/research/t74-retired7-increment-audit/RECEIPT.json @@ -0,0 +1,2774 @@ +{ + "claims_under_test": { + "C": "0.001717794984118634663827", + "aliases": [ + [ + 606, + 550 + ], + [ + 635, + 551 + ], + [ + 637, + 552 + ], + [ + 638, + 553 + ], + [ + 639, + 562 + ], + [ + 667, + 401 + ], + [ + 669, + 403 + ] + ], + "complete_profile": { + "1": 1603728, + "2": 431568, + "3": 185082, + "4": 85248, + "5": 27194, + "8": 5328, + "32": 1, + "48": 26558 + }, + "helpers": 408, + "inventory": { + "4": 26, + "5": 2, + "7": 62, + "8": 78, + "9": 240 + }, + "local_profile": { + "1": 2382, + "2": 648, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + }, + "margin_2751": "326698885104162859/500000000000000000000000", + "margin_2766": "538010651632355557/1000000000000000000000000", + "mass": 4816512, + "moves": [ + [ + 30, + 401, + 564 + ], + [ + 31, + 403, + 565 + ] + ], + "roles": 271728 + }, + "commits": { + "c2751": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "c2766": "e6df920cd0110e4b629e2ad84eddcb539001e174", + "c2802": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "c2818": "175822aee7a1858ec653f7f92d7a750aec2c2795" + }, + "controls": { + "C1 refit7 B911 undone": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S3S4-FRAMES-PROFILE-base", + "expected_rule_message": "warp frame mismatch: op 30 lender 564 (U is not the propagated frame)", + "failing_rules": [ + "S1-DIFF-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C10 first restore gate dropped": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S2-REPLAY-FREE-base", + "expected_rule_message": "restored helper 572 not its own input", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C11 fill inflated to R+1 helper indices": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S5-FILL-WORD-DERIVED-R", + "expected_rule_message": "role count 272394 != calls x word-derived R (666 x 408)", + "failing_rules": [ + "S5-FILL-TRANSFORM", + "S5-FILL-WORD-DERIVED-R", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C12 first hostee gate of warp 30 left on old lender 401": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S1-DIFF-base", + "expected_rule_message": "B941: final gate ['add', 600, 401, -1, 1] is not the declared relabel ['add', 600, 564, -1, 1] of parent ['add', 600, 401, -1, 1]", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S1-STAGE-RECORDS-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C13 undeclared frame raise on a B gate": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S1-DIFF-base", + "expected_rule_message": "undeclared frame changes: [('B', 1500)]", + "failing_rules": [ + "S1-DIFF-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C14 #2818 base word differs by one sign": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "X-2818-SAME-CONSTRUCTION", + "expected_rule_message": "words differ", + "failing_rules": [ + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C2 hostee move 401->564 reverted (401 then hosts follower 667 and hostee 30 at once)": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "OCC-TIMELINE-base", + "expected_rule_message": "OCC: follower 667 outlives the segment", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S1-STAGE-RECORDS-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C3 alias warp 66 moved before lender 550 last gate (B901)": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "OCC-TIMELINE-base", + "expected_rule_message": "OCC: lender 550 has an own event at/after its alias warp 66", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-STAGE-RECORDS-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C4a lender 401: last A write (A3175) moved into B right after alias warp 71, own frame": { + "accepted_as_expected": true, + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S3S4-FRAMES-PROFILE-base", + "expected_rule_message": "frame not monotone: register 401 at B259", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S1-STAGE-RECORDS-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "must_accept": [ + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base" + ], + "rejected_by_expected_rule": true + }, + "C4b lender 401: last A write moved to the end of restore, own frame": { + "accepted_as_expected": true, + "control_ok": true, + "crashed_rules": [], + "expected_rule": "OCC-TIMELINE-base", + "expected_rule_message": "OCC: final segment of 401 after warp 71 is not exactly follower 667", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "must_accept": [ + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base" + ], + "rejected_by_expected_rule": true + }, + "C4c lender 403 (extra word): last A write (A3174) moved into B right after alias warp 72, own frame": { + "accepted_as_expected": true, + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S3S4-FRAMES-PROFILE-extra", + "expected_rule_message": "frame not monotone: register 403 at B262", + "failing_rules": [ + "OCC-TIMELINE-extra", + "S1-DIFF-extra", + "S1-STAGE-RECORDS-extra", + "S3-REFIT-EXACT-extra", + "S3S4-FRAMES-PROFILE-extra", + "S4-FRAMES-RREF-extra", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "must_accept": [ + "S2-REPLAY-FREE-extra", + "S2-REPLAY-MATRIX-extra" + ], + "rejected_by_expected_rule": true + }, + "C4d lender 401: last A write moved to the end of restore at frame FULL": { + "accepted_as_expected": true, + "control_ok": true, + "crashed_rules": [], + "exact_failing": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "X-2818-SAME-CONSTRUCTION" + ], + "exact_failing_ok": true, + "expected_rule": "OCC-TIMELINE-base", + "expected_rule_message": "OCC: final segment of 401 after warp 71 is not exactly follower 667", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "X-2818-SAME-CONSTRUCTION" + ], + "must_accept": [ + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S3-REFIT-EXACT-base", + "S1-STAGE-RECORDS-base", + "S5-FILL-WORD-DERIVED-R", + "S5-FILL-TRANSFORM", + "S6-PROFILE-MASS-ROOT" + ], + "rejected_by_expected_rule": true + }, + "C4e lender 403 (extra word): last A write moved to the end of restore at frame FULL": { + "accepted_as_expected": true, + "control_ok": true, + "crashed_rules": [], + "exact_failing": [ + "OCC-TIMELINE-extra", + "S1-DIFF-extra", + "X-2818-SAME-CONSTRUCTION" + ], + "exact_failing_ok": true, + "expected_rule": "OCC-TIMELINE-extra", + "expected_rule_message": "OCC: final segment of 403 after warp 72 is not exactly follower 669", + "failing_rules": [ + "OCC-TIMELINE-extra", + "S1-DIFF-extra", + "X-2818-SAME-CONSTRUCTION" + ], + "must_accept": [ + "S2-REPLAY-FREE-extra", + "S2-REPLAY-MATRIX-extra", + "S3S4-FRAMES-PROFILE-extra", + "S4-FRAMES-RREF-extra", + "S3-REFIT-EXACT-extra", + "S1-STAGE-RECORDS-extra", + "S5-FILL-WORD-DERIVED-R", + "S5-FILL-TRANSFORM", + "S6-PROFILE-MASS-ROOT" + ], + "rejected_by_expected_rule": true + }, + "C4f lender 401: last A read (an add with source 401) moved to the end of restore at frame FULL": { + "accepted_as_expected": true, + "control_ok": true, + "crashed_rules": [], + "exact_failing": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "X-2818-SAME-CONSTRUCTION" + ], + "exact_failing_ok": true, + "expected_rule": "S2-REPLAY-FREE-base", + "expected_rule_message": "forward target 0 wrong before cleanup", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "X-2818-SAME-CONSTRUCTION" + ], + "must_accept": [ + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S3-REFIT-EXACT-base", + "S1-STAGE-RECORDS-base", + "S5-FILL-WORD-DERIVED-R", + "S5-FILL-TRANSFORM", + "S6-PROFILE-MASS-ROOT" + ], + "rejected_by_expected_rule": true + }, + "C4g lender 401: last A write before its last read (A3158) moved to the end of restore at frame FULL": { + "accepted_as_expected": true, + "control_ok": true, + "crashed_rules": [], + "exact_failing": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "X-2818-SAME-CONSTRUCTION" + ], + "exact_failing_ok": true, + "expected_rule": "S2-REPLAY-MATRIX-base", + "expected_rule_message": "matrix realisation (forward, seed 1) wrong on register 112", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "X-2818-SAME-CONSTRUCTION" + ], + "must_accept": [ + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S3-REFIT-EXACT-base", + "S1-STAGE-RECORDS-base", + "S5-FILL-WORD-DERIVED-R", + "S5-FILL-TRANSFORM", + "S6-PROFILE-MASS-ROOT" + ], + "rejected_by_expected_rule": true + }, + "C5 alias warp 71 after follower 667 first gate (B260)": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "OCC-TIMELINE-base", + "expected_rule_message": "OCC: follower 667 has an event before alias warp 71", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-STAGE-RECORDS-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C6 wrong G on warp 71": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S3S4-FRAMES-PROFILE-base", + "expected_rule_message": "G(U) != E", + "failing_rules": [ + "S1-STAGE-RECORDS-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C7 warp 71 with G(U')=E' for a U' that is not 401's propagated frame": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S3S4-FRAMES-PROFILE-base", + "expected_rule_message": "warp frame mismatch: op 71 lender 401 (U is not the propagated frame)", + "failing_rules": [ + "S1-STAGE-RECORDS-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C8 removed follower 667 kept as a live helper (R self-reference)": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "S5-FILL-WORD-DERIVED-R", + "expected_rule_message": "role count 271728 != calls x word-derived R (666 x 409)", + "failing_rules": [ + "S1-DIFF-base", + "S1-DIFF-extra", + "S3S4-FRAMES-PROFILE-base", + "S3S4-FRAMES-PROFILE-extra", + "S4-FRAMES-RREF-base", + "S4-FRAMES-RREF-extra", + "S5-FILL-TRANSFORM", + "S5-FILL-WORD-DERIVED-R", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + }, + "C9 alias lenders of warps 71/72 swapped (declaration conformance)": { + "control_ok": true, + "crashed_rules": [], + "expected_rule": "OCC-TIMELINE-base", + "expected_rule_message": "OCC: alias warp 71 is not on lender 401", + "failing_rules": [ + "OCC-TIMELINE-base", + "S1-DIFF-base", + "S1-STAGE-RECORDS-base", + "S2-REPLAY-FREE-base", + "S2-REPLAY-MATRIX-base", + "S3-REFIT-EXACT-base", + "S3S4-FRAMES-PROFILE-base", + "S4-FRAMES-RREF-base", + "S6-PROFILE-MASS-ROOT", + "X-2818-SAME-CONSTRUCTION" + ], + "rejected_by_expected_rule": true + } + }, + "pins": { + "CLAIM": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/CLAIM.json", + "sha256": "a2fcbc8a3ad3095ecbd310a26c02e9d11c28e4d105669a08bbdfb39d7704db51" + }, + "DISPATCH": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/DISPATCH.json.gz", + "sha256": "14fe756dcac93a0f3b2b7f38ba7b998dec89d56d5171b691af4fae45e5d83d11" + }, + "FILL": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/FILL.json.gz", + "sha256": "2f2a25a8d82b424b1e643a8a5167361fcc5ab33cfbc6f186f4cb7ddcaf9df7d9" + }, + "FILL51": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/FILL2751.json.gz", + "sha256": "9ce94578640b4927cb9c73244692b1f79ac2999179d309f6bf0c015c06f7a2f1" + }, + "FILL51_own": { + "commit": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "path": "research/t74-joint-twelve/inputs/FILL.json.gz", + "sha256": "9ce94578640b4927cb9c73244692b1f79ac2999179d309f6bf0c015c06f7a2f1" + }, + "K2751": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/evidence/PR2751-CLAIM.json", + "sha256": "78e99222196fca8b74a895b9e2db40a0e4afd1d69cd4fb52f38bfb157bac2438" + }, + "K2751_own": { + "commit": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "path": "research/t74-joint-twelve/CLAIM.json", + "sha256": "78e99222196fca8b74a895b9e2db40a0e4afd1d69cd4fb52f38bfb157bac2438" + }, + "K2766": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/evidence/PR2766-CLAIM.json", + "sha256": "399e20ffb8bac62363f7d48c59021d5afef5f62bb6c51986ca847b02ec1e73a8" + }, + "K2766_own": { + "commit": "e6df920cd0110e4b629e2ad84eddcb539001e174", + "path": "research/complex-routing-leaf-fusion/CLAIM.json", + "sha256": "399e20ffb8bac62363f7d48c59021d5afef5f62bb6c51986ca847b02ec1e73a8" + }, + "K2767": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/evidence/PR2767-OUTER-CLAIM.json", + "sha256": "252b7bbdbef293f643633ff95ba7d1eabbe83e1eebcd1cb06f51834256bde1f3" + }, + "ORDER": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/ORDER.json", + "sha256": "129e791d5b45c279443ff9e1edef5ac33d5abc51717ecbae8265abea5c247ae7" + }, + "P51_base": { + "commit": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "path": "research/t74-joint-twelve/inputs/WORD-base.json.gz", + "sha256": "ae8b6b4d62a9da29331062fae1bd68b0341edf83152f5a5ef50c5109ba578f9a" + }, + "P51_extra": { + "commit": "4cfbb0cc8314d7fb4e8e754545a49a42eb590a69", + "path": "research/t74-joint-twelve/inputs/WORD-extra.json.gz", + "sha256": "1bb44a73d5841afb954b49ae94dba2e0c536b1eea9436ae5d89de87d8a04e127" + }, + "PLAN": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/PLAN.json.gz", + "sha256": "afb3c5c8134fc2cfce0b50a21758490c225574994b2c3c5161e53e2355acc6fa" + }, + "PROFILE": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/PROFILE.json", + "sha256": "9d71407ded0b17496b0f94ca896355933a850dc6fc8456e39b0a1f72995b1406" + }, + "PROV": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/PROVIDERS.json", + "sha256": "391075b1411a3976850c633f92f58c35ed3f046f09d55bd435d7545124543fd4" + }, + "PROV51": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/PROVIDERS2751.json", + "sha256": "ec4802a33c0e1d41369da77b19b9b783dc812b2d3246e096fee13d29f226dd66" + }, + "P_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/WORD2751-base.json.gz", + "sha256": "ae8b6b4d62a9da29331062fae1bd68b0341edf83152f5a5ef50c5109ba578f9a" + }, + "P_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/WORD2751-extra.json.gz", + "sha256": "1bb44a73d5841afb954b49ae94dba2e0c536b1eea9436ae5d89de87d8a04e127" + }, + "R5_ADMISSION": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/evidence/retired5/ADMISSION-RESULT.json", + "sha256": "e441d6bfef1554491087a5b4701a8b23b331af3b57f77a38f3de4a47d940a6bf" + }, + "R5_HOOK": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/evidence/retired5/HOOK-RESULT.json", + "sha256": "76b67d54df3a6da3bb7f6fe3402f11d2926cb48353bf068dc34eeb560784771a" + }, + "ST_alias5_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/alias5_43base.json", + "sha256": "a9ef916e6afcba33345bce3fd0e33606f09f340e0378cf017e2994a9206b969d" + }, + "ST_alias5_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/alias5_43extra.json", + "sha256": "aeff3d1ffa74e4bffa892293f88a968e2c2b0330ad61128696a6bce7bc383b46" + }, + "ST_alias7_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/alias7_43base.json", + "sha256": "100558d0f0ffbb2df38668b3d2bc4e4e11d5f328f629f5b4d931b0f619d49700" + }, + "ST_alias7_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/alias7_43extra.json", + "sha256": "783ed700791b1dcd4bb35422f5fb8114a0c5d82773394b87a613e5f32da51250" + }, + "ST_hostmove2_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/hostmove2_43base.json", + "sha256": "ee0f0de1ebe2f84e37e439f783a76f5d210fa1c34b3497a8d3c490296ee88e3b" + }, + "ST_hostmove2_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/hostmove2_43extra.json", + "sha256": "d06b7a56b457c16ea138e8265fc6f2d1b32711f0515a76137e86325a6f77a024" + }, + "ST_refit5_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit5_43base.json", + "sha256": "ff434b1820339f0f7c2c8ba7982edc4c236e522ea30aaa56890206c0fa96f642" + }, + "ST_refit5_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit5_43extra.json", + "sha256": "ff434b1820339f0f7c2c8ba7982edc4c236e522ea30aaa56890206c0fa96f642" + }, + "ST_refit5c_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit5c_43base.json", + "sha256": "cd8e6b7f8b8dacf21875f465e3df05bf827f12dd063fe1be7557c7281bff16f1" + }, + "ST_refit5c_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit5c_43extra.json", + "sha256": "cd8e6b7f8b8dacf21875f465e3df05bf827f12dd063fe1be7557c7281bff16f1" + }, + "ST_refit7_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit7_43base.json", + "sha256": "c1ca4637c3b88828d2628c87a20f93088769dbceb9f487cb75ce90ec1a0ff5f7" + }, + "ST_refit7_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit7_43extra.json", + "sha256": "c1ca4637c3b88828d2628c87a20f93088769dbceb9f487cb75ce90ec1a0ff5f7" + }, + "ST_refit7c_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit7c_43base.json", + "sha256": "086dc27f17448ab9bddb2e890752cf13d5965a63cd79fcf25aa7f1c9402503df" + }, + "ST_refit7c_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/refit7c_43extra.json", + "sha256": "086dc27f17448ab9bddb2e890752cf13d5965a63cd79fcf25aa7f1c9402503df" + }, + "TEMPLATE": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/GLOBAL-TEMPLATE.json.gz", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + }, + "W66_base": { + "commit": "e6df920cd0110e4b629e2ad84eddcb539001e174", + "path": "research/complex-routing-leaf-fusion/inputs/WORD-base.json.gz", + "sha256": "80e309cc16d0a86a0854d32f4f43e0d856768ea3cf5b6437061b427997ae4790" + }, + "W66_extra": { + "commit": "e6df920cd0110e4b629e2ad84eddcb539001e174", + "path": "research/complex-routing-leaf-fusion/inputs/WORD-extra.json.gz", + "sha256": "88e55acb7e274c62fbb0deab7f420d85fde3c2a471735222f0b5d039bc34e2e6" + }, + "W_base": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/WORD-base.json.gz", + "sha256": "dca8becca633ffc5e998985631bcbcab1123b27ca7f10ac6a96b1ec21ce69a66" + }, + "W_extra": { + "commit": "17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd", + "path": "research/t74-joint-twelve-retired7/inputs/WORD-extra.json.gz", + "sha256": "6bcb3c2c73eaf7558ddc6ef6b484334f8d96b9d2b227e265483b657de00f4bb7" + }, + "X_DISPATCH": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/borrow-fill/DISPATCH.json", + "sha256": "fd8132ec8957b908ee6d871216848f18bafc6bd9304acd6185519ee26d97b1ca" + }, + "X_FILL": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/borrow-fill/FILL.json.gz", + "sha256": "2f2a25a8d82b424b1e643a8a5167361fcc5ab33cfbc6f186f4cb7ddcaf9df7d9" + }, + "X_ORDER": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/borrow-fill/ORDER.json", + "sha256": "129e791d5b45c279443ff9e1edef5ac33d5abc51717ecbae8265abea5c247ae7" + }, + "X_PROV": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/BORROW-PROVIDERS.json", + "sha256": "391075b1411a3976850c633f92f58c35ed3f046f09d55bd435d7545124543fd4" + }, + "X_R7_base": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/borrow/inputs/retired7_43base.json", + "sha256": "74daf5826d9191be4613a61447f4dc12789190fb49a3219f6a9df63075cac1e1" + }, + "X_R7_extra": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/borrow/inputs/retired7_43extra.json", + "sha256": "25d9774b512da78f042287ce1de91c79c8658d06488b8fe94e548cbdd036f034" + }, + "X_W_base": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/borrow/words/BORROW-WORD-43base.json.gz", + "sha256": "dca8becca633ffc5e998985631bcbcab1123b27ca7f10ac6a96b1ec21ce69a66" + }, + "X_W_extra": { + "commit": "175822aee7a1858ec653f7f92d7a750aec2c2795", + "path": "research/gmx-t74-borrow43-handoff/new/borrow/words/BORROW-WORD-43extra.json.gz", + "sha256": "6bcb3c2c73eaf7558ddc6ef6b484334f8d96b9d2b227e265483b657de00f4bb7" + } + }, + "rules": { + "ATTRIBUTION-PR2766-WORD": { + "info": { + "PR2766_root_in": [ + "171725697346700230827/100000000000000000000000", + "1717256973467002308271/1000000000000000000000000" + ], + "base": { + "delta": { + "1": -2, + "2": 1 + }, + "other_19_frames": "cost-neutral on W2751 and on the final word", + "pr2766_local_profile": { + "1": 2364, + "2": 647, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + }, + "pr2766_word_change": "B1151 dim 6 -> 5" + }, + "complete_profile_equals_PR2766_claim": true, + "extra": { + "delta": { + "1": -2, + "2": 1 + }, + "other_19_frames": "cost-neutral on W2751 and on the final word", + "pr2766_local_profile": { + "1": 2364, + "2": 647, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + }, + "pr2766_word_change": "B1151 dim 6 -> 5" + }, + "root_margins": [ + "1.7903e-19", + "1.0461e-20" + ] + }, + "ok": true + }, + "ATTRIBUTION-RETIRED5": { + "info": { + "fill_gzip_sha256_equals_recorded": true, + "fill_json_sha256": "ef4bd5d44e707b4a26391328e784aec6763a7684c7c15720c6a5e9f743fb498b", + "gain_retired5_over_2766": "1.52342868489335178E-7", + "gain_retired7_stages_over_retired5": "385667783143020379/1000000000000000000000000", + "recorded_endpoint_profile_equal": true, + "retired5_complete": { + "1": 1606392, + "2": 427572, + "3": 189078, + "4": 85248, + "5": 25862, + "8": 5328, + "32": 1, + "48": 26558 + }, + "retired5_idle": { + "1": 17316, + "3": 6594, + "5": 8546, + "32": 1, + "48": 26558 + }, + "retired5_profile": { + "1": 2386, + "2": 642, + "3": 274, + "4": 128, + "5": 26, + "8": 8 + }, + "retired5_root_in": [ + "214676164541936455431/125000000000000000000000", + "1717409316335491643449/1000000000000000000000000" + ], + "root_margins": [ + "8.6871e-20", + "1.0261e-19" + ] + }, + "ok": true + }, + "OCC-TIMELINE-base": { + "info": { + "occupancy": [ + { + "follower": 606, + "follower_events": 7, + "follower_first": [ + "B", + 947 + ], + "lender": 550, + "lender_events": 3, + "lender_last": [ + "B", + 901 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 66, + "warp_B_pos": 947 + }, + { + "follower": 635, + "follower_events": 7, + "follower_first": [ + "B", + 1024 + ], + "lender": 551, + "lender_events": 3, + "lender_last": [ + "B", + 902 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 67, + "warp_B_pos": 1024 + }, + { + "follower": 637, + "follower_events": 7, + "follower_first": [ + "B", + 1027 + ], + "lender": 552, + "lender_events": 3, + "lender_last": [ + "B", + 909 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 68, + "warp_B_pos": 1027 + }, + { + "follower": 638, + "follower_events": 7, + "follower_first": [ + "B", + 1030 + ], + "lender": 553, + "lender_events": 3, + "lender_last": [ + "B", + 910 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 69, + "warp_B_pos": 1030 + }, + { + "follower": 639, + "follower_events": 7, + "follower_first": [ + "B", + 1033 + ], + "lender": 562, + "lender_events": 3, + "lender_last": [ + "B", + 903 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 70, + "warp_B_pos": 1033 + }, + { + "follower": 667, + "follower_events": 7, + "follower_first": [ + "B", + 259 + ], + "lender": 401, + "lender_events": 81, + "lender_last": [ + "A", + 3175 + ], + "lender_sections": { + "A": 27, + "compensation": 54 + }, + "op": 71, + "warp_B_pos": 259 + }, + { + "follower": 669, + "follower_events": 7, + "follower_first": [ + "B", + 262 + ], + "lender": 403, + "lender_events": 86, + "lender_last": [ + "A", + 3174 + ], + "lender_sections": { + "A": 26, + "compensation": 60 + }, + "op": 72, + "warp_B_pos": 262 + }, + { + "hostee_events": 7, + "hostee_first": [ + "B", + 941 + ], + "hostee_warp": 30, + "new_lender": 564, + "new_lender_last": [ + "B", + 911 + ], + "old_lender": 401, + "old_warp_B_pos": 941, + "warp_B_pos": 941 + }, + { + "hostee_events": 7, + "hostee_first": [ + "B", + 944 + ], + "hostee_warp": 31, + "new_lender": 565, + "new_lender_last": [ + "B", + 912 + ], + "old_lender": 403, + "old_warp_B_pos": 941, + "warp_B_pos": 944 + } + ], + "segments_checked": 704 + }, + "ok": true + }, + "OCC-TIMELINE-extra": { + "info": { + "occupancy": [ + { + "follower": 606, + "follower_events": 7, + "follower_first": [ + "B", + 947 + ], + "lender": 550, + "lender_events": 3, + "lender_last": [ + "B", + 901 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 66, + "warp_B_pos": 947 + }, + { + "follower": 635, + "follower_events": 7, + "follower_first": [ + "B", + 1024 + ], + "lender": 551, + "lender_events": 3, + "lender_last": [ + "B", + 902 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 67, + "warp_B_pos": 1024 + }, + { + "follower": 637, + "follower_events": 7, + "follower_first": [ + "B", + 1027 + ], + "lender": 552, + "lender_events": 3, + "lender_last": [ + "B", + 909 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 68, + "warp_B_pos": 1027 + }, + { + "follower": 638, + "follower_events": 7, + "follower_first": [ + "B", + 1030 + ], + "lender": 553, + "lender_events": 3, + "lender_last": [ + "B", + 910 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 69, + "warp_B_pos": 1030 + }, + { + "follower": 639, + "follower_events": 7, + "follower_first": [ + "B", + 1033 + ], + "lender": 562, + "lender_events": 3, + "lender_last": [ + "B", + 903 + ], + "lender_sections": { + "A": 1, + "B": 2 + }, + "op": 70, + "warp_B_pos": 1033 + }, + { + "follower": 667, + "follower_events": 7, + "follower_first": [ + "B", + 259 + ], + "lender": 401, + "lender_events": 81, + "lender_last": [ + "A", + 3175 + ], + "lender_sections": { + "A": 27, + "compensation": 54 + }, + "op": 71, + "warp_B_pos": 259 + }, + { + "follower": 669, + "follower_events": 7, + "follower_first": [ + "B", + 262 + ], + "lender": 403, + "lender_events": 86, + "lender_last": [ + "A", + 3174 + ], + "lender_sections": { + "A": 26, + "compensation": 60 + }, + "op": 72, + "warp_B_pos": 262 + }, + { + "hostee_events": 7, + "hostee_first": [ + "B", + 941 + ], + "hostee_warp": 30, + "new_lender": 564, + "new_lender_last": [ + "B", + 911 + ], + "old_lender": 401, + "old_warp_B_pos": 941, + "warp_B_pos": 941 + }, + { + "hostee_events": 7, + "hostee_first": [ + "B", + 944 + ], + "hostee_warp": 31, + "new_lender": 565, + "new_lender_last": [ + "B", + 912 + ], + "old_lender": 403, + "old_warp_B_pos": 941, + "warp_B_pos": 944 + } + ], + "segments_checked": 704 + }, + "ok": true + }, + "PIN-2751-COPIES": { + "info": "byte-identical", + "ok": true + }, + "POSITIVE-PARENT-2751": { + "info": { + "base": { + "helpers": 415, + "profile": { + "1": 2366, + "2": 646, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + } + }, + "extra": { + "helpers": 415, + "profile": { + "1": 2366, + "2": 646, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + } + }, + "fill": { + "R": 415, + "idle": { + "1": 17316, + "3": 6594, + "5": 5216, + "32": 1, + "48": 26558 + }, + "roles": 276390 + } + }, + "ok": true + }, + "S1-DIFF-base": { + "info": { + "B_relabelled_gates": 63, + "declared_frames": 62, + "declared_frames_effective": 62, + "frame_changes": 62 + }, + "ok": true + }, + "S1-DIFF-extra": { + "info": { + "B_relabelled_gates": 63, + "declared_frames": 62, + "declared_frames_effective": 62, + "frame_changes": 62 + }, + "ok": true + }, + "S1-STAGE-CHAIN-base": { + "info": [ + { + "helpers": 415, + "mass": 5223, + "profile": { + "1": 2401, + "2": 639, + "3": 278, + "4": 129, + "5": 26, + "8": 8 + }, + "stage": "refit5" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2396, + "2": 639, + "3": 278, + "4": 124, + "5": 26, + "8": 8 + }, + "stage": "alias5" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2386, + "2": 642, + "3": 274, + "4": 128, + "5": 26, + "8": 8 + }, + "stage": "refit5c" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2388, + "2": 646, + "3": 268, + "4": 130, + "5": 26, + "8": 8 + }, + "stage": "refit7" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2386, + "2": 646, + "3": 268, + "4": 128, + "5": 28, + "8": 8 + }, + "stage": "hostmove2" + }, + { + "helpers": 408, + "mass": 5188, + "profile": { + "1": 2386, + "2": 646, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + }, + "stage": "alias7" + }, + { + "helpers": 408, + "mass": 5188, + "profile": { + "1": 2382, + "2": 648, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + }, + "stage": "refit7c" + } + ], + "ok": true + }, + "S1-STAGE-CHAIN-extra": { + "info": [ + { + "helpers": 415, + "mass": 5223, + "profile": { + "1": 2401, + "2": 639, + "3": 278, + "4": 129, + "5": 26, + "8": 8 + }, + "stage": "refit5" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2396, + "2": 639, + "3": 278, + "4": 124, + "5": 26, + "8": 8 + }, + "stage": "alias5" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2386, + "2": 642, + "3": 274, + "4": 128, + "5": 26, + "8": 8 + }, + "stage": "refit5c" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2388, + "2": 646, + "3": 268, + "4": 130, + "5": 26, + "8": 8 + }, + "stage": "refit7" + }, + { + "helpers": 410, + "mass": 5198, + "profile": { + "1": 2386, + "2": 646, + "3": 268, + "4": 128, + "5": 28, + "8": 8 + }, + "stage": "hostmove2" + }, + { + "helpers": 408, + "mass": 5188, + "profile": { + "1": 2386, + "2": 646, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + }, + "stage": "alias7" + }, + { + "helpers": 408, + "mass": 5188, + "profile": { + "1": 2382, + "2": 648, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + }, + "stage": "refit7c" + } + ], + "ok": true + }, + "S1-STAGE-RECORDS-base": { + "info": { + "declared_edit_pairs_per_stage": { + "alias5": 35, + "alias7": 14, + "hostmove2": 14 + }, + "declared_gate_edits": { + "delete": 63, + "insert": 63 + }, + "refit7_dims": [ + [ + "B", + 911, + 6, + 5 + ], + [ + "B", + 912, + 6, + 5 + ] + ], + "refit7_prev": [ + [ + "B", + 911, + [ + 258, + 130, + 76, + 44, + 24, + 1 + ] + ], + [ + "B", + 912, + [ + 258, + 130, + 74, + 43, + 25, + 6 + ] + ] + ], + "refit7c_dims": [ + [ + "B", + 1170, + 6, + 5 + ], + [ + "B", + 1171, + 6, + 5 + ] + ], + "refit_frames": { + "refit5": 26, + "refit5c": 32, + "refit7": 2, + "refit7c": 2 + }, + "relabelled_positions": 63 + }, + "ok": true + }, + "S1-STAGE-RECORDS-extra": { + "info": { + "declared_edit_pairs_per_stage": { + "alias5": 35, + "alias7": 14, + "hostmove2": 14 + }, + "declared_gate_edits": { + "delete": 63, + "insert": 63 + }, + "refit7_dims": [ + [ + "B", + 911, + 6, + 5 + ], + [ + "B", + 912, + 6, + 5 + ] + ], + "refit7_prev": [ + [ + "B", + 911, + [ + 258, + 130, + 76, + 44, + 24, + 1 + ] + ], + [ + "B", + 912, + [ + 258, + 130, + 74, + 43, + 25, + 6 + ] + ] + ], + "refit7c_dims": [ + [ + "B", + 1170, + 6, + 5 + ], + [ + "B", + 1171, + 6, + 5 + ] + ], + "refit_frames": { + "refit5": 26, + "refit5c": 32, + "refit7": 2, + "refit7c": 2 + }, + "relabelled_positions": 63 + }, + "ok": true + }, + "S2-REPLAY-FREE-base": { + "info": { + "cleanup": 4547, + "live_inputs": 632, + "restored": 72, + "words_dual": 91, + "words_fwd": 73 + }, + "ok": true + }, + "S2-REPLAY-FREE-extra": { + "info": { + "cleanup": 4547, + "live_inputs": 632, + "restored": 72, + "words_dual": 91, + "words_fwd": 73 + }, + "ok": true + }, + "S2-REPLAY-MATRIX-base": { + "info": "forward+dual, 2 seeds, 4x4 over GF(2^61-1)", + "ok": true + }, + "S2-REPLAY-MATRIX-extra": { + "info": "forward+dual, 2 seeds, 4x4 over GF(2^61-1)", + "ok": true + }, + "S3-ABOVE-FLOOR-NEUTRAL-base": { + "info": { + "above_floor": [ + "B771 dim 5 floor 4", + "B773 dim 5 floor 4", + "B776 dim 5 floor 4", + "B778 dim 5 floor 4", + "B783 dim 5 floor 4", + "B788 dim 5 floor 4", + "restore60 dim 8 floor 6" + ], + "profile_unchanged": true, + "variants_checked": 8 + }, + "ok": true + }, + "S3-ABOVE-FLOOR-NEUTRAL-extra": { + "info": { + "above_floor": [ + "B771 dim 5 floor 4", + "B773 dim 5 floor 4", + "B776 dim 5 floor 4", + "B778 dim 5 floor 4", + "B783 dim 5 floor 4", + "B788 dim 5 floor 4", + "restore60 dim 8 floor 6" + ], + "profile_unchanged": true, + "variants_checked": 8 + }, + "ok": true + }, + "S3-REFIT-EXACT-base": { + "info": [ + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B901", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B902", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B903", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B909", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B910", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B947", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B948", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B949", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B951", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B952", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1024", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1025", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1026", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1027", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1028", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1029", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1030", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1031", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1032", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1033", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1034", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1035", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1040", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1041", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1042", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1043", + "stage": "refit5" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A0", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A1", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A2", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A3", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A4", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A5", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A6", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A7", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A8", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A9", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A10", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A11", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B771", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B773", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B776", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B778", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B783", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B788", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B941", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B942", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B943", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B944", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B945", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B946", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B950", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1148", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1149", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1150", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1151", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1168", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1169", + "stage": "refit5c" + }, + { + "dim": 8, + "exact_floor": false, + "floor_dim": 6, + "gate": "restore60", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B911", + "stage": "refit7" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B912", + "stage": "refit7" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1170", + "stage": "refit7c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1171", + "stage": "refit7c" + } + ], + "ok": true + }, + "S3-REFIT-EXACT-extra": { + "info": [ + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B901", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B902", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B903", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B909", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B910", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B947", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B948", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B949", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B951", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B952", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1024", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1025", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1026", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1027", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1028", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1029", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1030", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1031", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1032", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1033", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1034", + "stage": "refit5" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1035", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1040", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1041", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1042", + "stage": "refit5" + }, + { + "dim": 6, + "exact_floor": true, + "floor_dim": 6, + "gate": "B1043", + "stage": "refit5" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A0", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A1", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A2", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A3", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A4", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A5", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A6", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A7", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A8", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A9", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A10", + "stage": "refit5c" + }, + { + "dim": 0, + "exact_floor": true, + "floor_dim": 0, + "gate": "A11", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B771", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B773", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B776", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B778", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B783", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": false, + "floor_dim": 4, + "gate": "B788", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B941", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B942", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B943", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B944", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B945", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B946", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B950", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1148", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1149", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1150", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1151", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1168", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1169", + "stage": "refit5c" + }, + { + "dim": 8, + "exact_floor": false, + "floor_dim": 6, + "gate": "restore60", + "stage": "refit5c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B911", + "stage": "refit7" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B912", + "stage": "refit7" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1170", + "stage": "refit7c" + }, + { + "dim": 5, + "exact_floor": true, + "floor_dim": 5, + "gate": "B1171", + "stage": "refit7c" + } + ], + "ok": true + }, + "S3S4-FRAMES-PROFILE-base": { + "info": { + "helpers": 408, + "inventory": { + "4": 26, + "5": 2, + "7": 62, + "8": 78, + "9": 240 + }, + "mass": 5188, + "new_or_moved": { + "30": { + "U_dim": 5, + "U_is_propagated": true + }, + "31": { + "U_dim": 5, + "U_is_propagated": true + }, + "66": { + "U_dim": 5, + "U_is_propagated": true + }, + "67": { + "U_dim": 5, + "U_is_propagated": true + }, + "68": { + "U_dim": 5, + "U_is_propagated": true + }, + "69": { + "U_dim": 5, + "U_is_propagated": true + }, + "70": { + "U_dim": 5, + "U_is_propagated": true + }, + "71": { + "U_dim": 4, + "U_is_propagated": true + }, + "72": { + "U_dim": 4, + "U_is_propagated": true + } + }, + "prelude_warp_items_checked": 24, + "profile": { + "1": 2382, + "2": 648, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + }, + "warps_checked": 72 + }, + "ok": true + }, + "S3S4-FRAMES-PROFILE-extra": { + "info": { + "helpers": 408, + "inventory": { + "4": 26, + "5": 2, + "7": 62, + "8": 78, + "9": 240 + }, + "mass": 5188, + "new_or_moved": { + "30": { + "U_dim": 5, + "U_is_propagated": true + }, + "31": { + "U_dim": 5, + "U_is_propagated": true + }, + "66": { + "U_dim": 5, + "U_is_propagated": true + }, + "67": { + "U_dim": 5, + "U_is_propagated": true + }, + "68": { + "U_dim": 5, + "U_is_propagated": true + }, + "69": { + "U_dim": 5, + "U_is_propagated": true + }, + "70": { + "U_dim": 5, + "U_is_propagated": true + }, + "71": { + "U_dim": 4, + "U_is_propagated": true + }, + "72": { + "U_dim": 4, + "U_is_propagated": true + } + }, + "prelude_warp_items_checked": 24, + "profile": { + "1": 2382, + "2": 648, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + }, + "warps_checked": 72 + }, + "ok": true + }, + "S4-FRAMES-RREF-base": { + "info": { + "inventory": { + "4": 26, + "5": 2, + "7": 62, + "8": 78, + "9": 240 + }, + "parent_profile": { + "1": 2366, + "2": 646, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + }, + "profile": { + "1": 2382, + "2": 648, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + } + }, + "ok": true + }, + "S4-FRAMES-RREF-extra": { + "info": { + "inventory": { + "4": 26, + "5": 2, + "7": 62, + "8": 78, + "9": 240 + }, + "parent_profile": { + "1": 2366, + "2": 646, + "3": 297, + "4": 120, + "5": 26, + "8": 8 + }, + "profile": { + "1": 2382, + "2": 648, + "3": 268, + "4": 128, + "5": 26, + "8": 8 + } + }, + "ok": true + }, + "S5-FILL-TRANSFORM": { + "info": { + "bins": 122625, + "dropped_roles": 4662 + }, + "ok": true + }, + "S5-FILL-WORD-DERIVED-R": { + "info": { + "R": 408, + "dispatch": { + "extra": 417, + "gauge44": 249 + }, + "idle": { + "1": 17316, + "3": 6594, + "5": 9878, + "32": 1, + "48": 26558 + }, + "roles": 271728, + "windows": 1332 + }, + "ok": true + }, + "S6-PROFILE-MASS-ROOT": { + "info": { + "f_values": [ + "66303.9999999999999999999564452703792106", + "66304.0000000000000000001458808452731837", + [ + "4.3555e-20", + "1.4588e-19" + ] + ], + "margin_2751": "326698885104162859/500000000000000000000000", + "margin_2766": "538010651632355557/1000000000000000000000000", + "margin_2767": "5.380106516323555560552030930847873881229E-7", + "mass": 4816512, + "root_in": [ + "1717794984118634663827/1000000000000000000000000", + "429448746029658665957/250000000000000000000000" + ] + }, + "ok": true + }, + "X-2818-SAME-CONSTRUCTION": { + "info": { + "dispatch": "same map", + "fill": "identical", + "order": "identical", + "patch_fields": { + "base": [ + "A", + "B", + "removed", + "start_extra", + "warps" + ], + "extra": [ + "A", + "B", + "removed", + "start_extra", + "warps" + ] + }, + "providers": "identical", + "words": "identical" + }, + "ok": true + } + }, + "scope": "Finite exact checks of the PR #2802 seven-stage increment (retired5 stages refit5/alias5/refit5c, retired7 stages refit7/hostmove2/alias7/refit7c) over the pinned PR #2751 words: event diff, per-register occupancy, warps/frames/profile, free-algebra and matrix replays, the 271728-role fill with word-derived R, complete profile/mass/root, PR #2818 identity, and attribution against PR #2766 and the recorded retired5 step. Inherited T74/#1319 admission, native lowering, outer proof and PR #2751 recovery are not checked.", + "status": "PASS" +} diff --git a/research/t74-retired7-increment-audit/SOURCES.json b/research/t74-retired7-increment-audit/SOURCES.json new file mode 100644 index 0000000000..5b1dfb144b --- /dev/null +++ b/research/t74-retired7-increment-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "544a7e82810e30cab61c297cb2e2ea86127fe944", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + } + ] +} diff --git a/research/t74-retired7-increment-audit/TASK.json b/research/t74-retired7-increment-audit/TASK.json new file mode 100644 index 0000000000..dd89030376 --- /dev/null +++ b/research/t74-retired7-increment-audit/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 5, + "base_commit": "544a7e82810e30cab61c297cb2e2ea86127fe944", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "changed", + "actual_scope": "Adversarial audit of PR #2802's seven-stage increment (head 17b2ee6e) over its parent PR #2751 (head 4cfbb0cc): the retired5 stages refit5/alias5/refit5c and the retired7 stages refit7/hostmove2/alias7/refit7c (seven retired-lender aliases, two hostee moves, refits) and the FILL2751->FILL transform, checked with fresh exact code on both words: event diff, per-register occupancy timeline, forward/dual free-algebra replay plus a matrix realisation, GF(2) warp frames, refit exactness and above-floor neutrality, profile/inventory recount by two subspace representations, the 271,728-role fill with word-derived R, complete profile/mass/root, and attribution against PR #2766's pinned word and #2802's recorded retired5 evidence. The verdict extends to PR #2818 (head 175822ae), whose words/fill/order/providers are byte-identical, and covers the shared word-level base of #2824, #2827, #2833, #2839 and #2843 (their own later stages are not checked).", + "scope_change_reason": "The card asks whether one selected-supplier obligation follows from its source-bound checks. The selected supplier is unchanged. The audited object is instead the pending T74 construction of #2802 (repackaged by #2818, and the base of #2824/#2827/#2833/#2839/#2843 as of 2026-10-16 02:10 UTC): it changed two acceptance checks (R read from the providers; the A-retired-lender alias control), and its new construction had no independent check. The maintainer's T74 reviews (community-efficient1000, #1992 row) ask to separate the actual new construction from inherited ancestors.", + "bottleneck_link": "A defect would remove the +5.38e-7 kappa margin of #2802/#2818 over #2766/#2767 and the shared base of #2824/#2827/#2833/#2839/#2843; a pass is necessary but not sufficient (T74/#1319 admission, native lowering and the PR1673 outer proof remain). It also settles the two changed acceptance checks: R is bound to the words, and alias occupancy holds for the shipped words but is a conformance property, not a kappa-soundness condition, in the finite model: no check on the pricing path reads it, and a lender's dead last write (after its last read) moved past its alias warp to the end of restore at frame FULL (C4d/C4e) still replays correctly and is identically priced, while a moved read (C4f) or a moved write the lender still reads (C4g) is rejected by both replays.", + "budget_minutes": 180, + "stop_rule": "Publish an independent verification if S1, S2 and S5 pass, S3/S4/S6 agree and every negative control is rejected by its named rule; on any mismatch minimise a witness, post a FINDING in #2612 and ship a negative result without repair. No search; #2751's twelve-source recovery treated as a pinned parent.", + "outcome": "completed", + "evidence": "verify.py --fetch: PASS_T74_RETIRED7_INCREMENT_AUDIT rules=28/28 controls=20/20 (about 2 minutes). Both words: 63 relabelled B gates = 63 declared edit pairs (alias5 35, hostmove2 14, alias7 14); 62 frame changes = 62 declared refit frames; nothing else changed; 704 register segments (632 + 72 = 639 + 65) each exactly one parent role (lenders 401/403 last act at A3175/A3174 before warps at B259/B262; 550-553/562 at B901-B910; 564/565 at B911/B912 before B941/B944); forward+dual replay over Q on 632 live inputs with 72 zero buffers and the re-derived 4547-item cleanup; 4x4 matrix realisation mod 2^61-1; 72 B warps + 24 prelude warp items with G(U)=E and U the propagated frame; refit floors 26/26, 25/32, 2/2, 2/2, the 7 above-floor refit5c frames cost-neutral; profile {1:2382,2:648,3:268,4:128,5:26,8:8}, inventory {4:26,5:2,7:62,8:78,9:240}; fill R=408 from the words, 271728 roles, idle {1:17316,3:6594,5:9878,32:1,48:26558}, FILL = FILL2751 minus 4662 roles; complete profile and mass 4816512; f(C) < 66304 < f(C+1e-24) with a written error budget. Attribution: PR #2766's own word differs from W2751 only at B1151; the other 19 frames #2802 lists with it are cost-neutral; the reconstructed retired5 state reproduces #2802's recorded retired5 endpoint 0.001717409316335491643448, local profile and fill sha256 3501f6bd...; the retired7 stages add 385667783143020379/10^24 over retired5 (the split #2802 states). Occupancy controls: a lender's last (dead) write moved past its alias warp is accepted by both scalar replays (C4a-C4e); at frame FULL (C4d/C4e) also by the frame chain, recount, refits, stage records, fill and price, and rejected only by OCC-TIMELINE plus the undeclared-edit checks; a moved lender read (C4f) and a moved write that precedes the lender's last read (C4g, A3158) are rejected by both replays and accepted by the frame chain, fill and price. #2818 identical.", + "author": "thakrarsagar", + "ai_assistance": "Substantial AI assistance: Claude (Anthropic, Claude Opus 5.5) wrote and ran increment_audit.py, increment_controls.py and verify.py from the written model (PR2226 PROOF.md, PR README text and the JSON layouts); PR code was read as pinned data only and never imported or executed. AI review passes in the same loop (reproducibility, mathematics, provenance, referee) reviewed the package in two rounds and two revisions addressed their findings. No human has hand-checked the findings.", + "open_questions": [ + { + "question": "Does any layer outside the finite BORROW-WORD model rely on alias occupancy (no lender event at or after its alias warp)?", + "why_it_matters": "In the finite model no pricing check reads occupancy, and a lender's dead last write moved past its alias warp to the end of restore at frame FULL (C4d/C4e) is a correct, identically priced word, so occupancy matters only if the native lowering, physical hosting or routing treats a warp as a register hand-over point.", + "first_step": "Inspect whether #2802's native lowering assigns roles per register segment; if so, add a C4d-type mutant against #2802's stage-structure check and an occupancy predicate to #2818's retired7 patch check (optional regression controls otherwise).", + "blocked_by": "Not blocked by access: #2802's full_replay.py downloads and authenticates the 491 pinned PR2679 files and rebuilds the native providers (needs #2802's requirements.txt; author-recorded cold run 411 s); an independent check should read its outputs as data." + }, + { + "question": "Is the whole refit frame assignment (refit5c/refit7c, 'certified optimal') optimal under the moment cost?", + "why_it_matters": "A better assignment could only raise kappa; it cannot invalidate the checked value, and the seven above-floor refit5c frames are cost-neutral.", + "first_step": "Run an independent exact optimiser over all gates' frames with the same COPY pricing.", + "blocked_by": "A written objective for the #1186 optimal_frames certificate." + }, + { + "question": "Do the new warps 30, 31 and 66-72 have exact native Clifford/Gaussian lifts in both orientations?", + "why_it_matters": "#2802's release records native warp-recipe checks, but this audit checks K_G only through its binary-symplectic image.", + "first_step": "Instantiate the exact Gaussian products of each new K_G and check every column, as PR2226 did for its 80 pairs.", + "blocked_by": "Not blocked by access: the native inputs are rebuilt by #2802's full_replay.py from the pinned PR2679 sources (as for question 1)." + } + ] +} diff --git a/research/t74-retired7-increment-audit/VERIFY.json b/research/t74-retired7-increment-audit/VERIFY.json new file mode 100644 index 0000000000..4cd8b575ac --- /dev/null +++ b/research/t74-retired7-increment-audit/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--fetch" + ], + "timeout_seconds": 600, + "checks": "fetches PR #2802/#2751/#2818/#2766 heads only if absent (inputs pinned by sha256); 28 named rules on both words: event diff, occupancy timeline, free-algebra and matrix replays, GF(2) warps/refits and above-floor neutrality, profile, fill with word-derived R, complete profile/mass/root, #2818 identity, #2751 positive control, stage-chain rebuild, attribution against PR #2766's word and #2802's recorded retired5 evidence; 20 negative controls, each rejected by its named rule, seven also accepted by named rules" + } + ] +} diff --git a/research/t74-retired7-increment-audit/increment_audit.py b/research/t74-retired7-increment-audit/increment_audit.py new file mode 100644 index 0000000000..e07d646920 --- /dev/null +++ b/research/t74-retired7-increment-audit/increment_audit.py @@ -0,0 +1,1608 @@ +#!/usr/bin/env python3 +"""Independent adversarial audit of PR #2802's seven-stage increment over PR #2751 (retired5 stages refit5/alias5/refit5c +plus retired7 stages refit7/hostmove2/alias7/refit7c), verdict extended to PR #2818. "retired7" in identifiers follows +#2802's package name (t74-joint-twelve-retired7); in prose it means only the last four stages. + +Objects (read as pinned git blobs, never imported or executed): + PR #2802 (mdumitrean) head 17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd, research/t74-joint-twelve-retired7/ + PR #2751 (tekuuu) head 4cfbb0cc8314d7fb4e8e754545a49a42eb590a69, research/t74-joint-twelve/ + PR #2818 (jeremykothe2) head 175822aee7a1858ec653f7f92d7a750aec2c2795, research/gmx-t74-borrow43-handoff/ + PR #2766 (DavidAriasC) head e6df920cd0110e4b629e2ad84eddcb539001e174, research/complex-routing-leaf-fusion/ (attribution only) + +Fresh standard-library code. Every check is a named rule; the run prints one line per rule and a final +PASS/FAIL line. Negative controls mutate the pinned inputs and must each be rejected by a named rule. + +Model (the BORROW-WORD model as written in PR2226 PROOF.md and the PR2679/PR2751 lineage; restated here): + registers 0..111 X, 112..223 Y, 224..703 helper namespace (report.R = 480); removed helpers do not exist; + frames are GF(2)-subspaces of F_2^9 (represented here as the frozenset of all their elements); + every framed gate climbs each incident register to the gate frame (monotone; a strict climb pays one child + of rank = dimension increase); a B warp [pos, L, G, U, E] is applied before B[pos], needs cur(L) == U, sets + cur(L) = E and is free (rank-zero reference change K_G); cut charges nested COPY chains; every live register + finally climbs to its end frame; cleanup = inverse-reverse of the recorded (non-target and warp) program at + FULL with private zero buffers for helper_final registers. Logic: exact replay over Q with every + live register an independent dirty symbol, forward and dual (g -> g^-T with K^-T as new free letters). +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import argparse +import gzip +import hashlib +import json +import os +import random +import subprocess +import sys +from collections import Counter, defaultdict +from fractions import Fraction +from decimal import Decimal, ROUND_FLOOR, ROUND_CEILING, localcontext + +COMMIT = dict(c2802='17b2ee6ef3cf1468e78a6267f0ecbc9a0e6f60dd', c2751='4cfbb0cc8314d7fb4e8e754545a49a42eb590a69', + c2818='175822aee7a1858ec653f7f92d7a750aec2c2795', c2766='e6df920cd0110e4b629e2ad84eddcb539001e174') +D02 = 'research/t74-joint-twelve-retired7/' +D51 = 'research/t74-joint-twelve/' +D18 = 'research/gmx-t74-borrow43-handoff/' +D66 = 'research/complex-routing-leaf-fusion/' +# key -> (commit key, path, sha256 of the blob bytes) +PINS = { + 'W_base': ('c2802', D02 + 'inputs/WORD-base.json.gz', 'dca8becca633ffc5e998985631bcbcab1123b27ca7f10ac6a96b1ec21ce69a66'), + 'W_extra': ('c2802', D02 + 'inputs/WORD-extra.json.gz', '6bcb3c2c73eaf7558ddc6ef6b484334f8d96b9d2b227e265483b657de00f4bb7'), + 'P_base': ('c2802', D02 + 'inputs/WORD2751-base.json.gz', 'ae8b6b4d62a9da29331062fae1bd68b0341edf83152f5a5ef50c5109ba578f9a'), + 'P_extra': ('c2802', D02 + 'inputs/WORD2751-extra.json.gz', '1bb44a73d5841afb954b49ae94dba2e0c536b1eea9436ae5d89de87d8a04e127'), + 'P51_base': ('c2751', D51 + 'inputs/WORD-base.json.gz', 'ae8b6b4d62a9da29331062fae1bd68b0341edf83152f5a5ef50c5109ba578f9a'), + 'P51_extra': ('c2751', D51 + 'inputs/WORD-extra.json.gz', '1bb44a73d5841afb954b49ae94dba2e0c536b1eea9436ae5d89de87d8a04e127'), + 'FILL': ('c2802', D02 + 'inputs/FILL.json.gz', '2f2a25a8d82b424b1e643a8a5167361fcc5ab33cfbc6f186f4cb7ddcaf9df7d9'), + 'FILL51': ('c2802', D02 + 'inputs/FILL2751.json.gz', '9ce94578640b4927cb9c73244692b1f79ac2999179d309f6bf0c015c06f7a2f1'), + 'FILL51_own': ('c2751', D51 + 'inputs/FILL.json.gz', '9ce94578640b4927cb9c73244692b1f79ac2999179d309f6bf0c015c06f7a2f1'), + 'PROV': ('c2802', D02 + 'inputs/PROVIDERS.json', '391075b1411a3976850c633f92f58c35ed3f046f09d55bd435d7545124543fd4'), + 'PROV51': ('c2802', D02 + 'inputs/PROVIDERS2751.json', 'ec4802a33c0e1d41369da77b19b9b783dc812b2d3246e096fee13d29f226dd66'), + 'ORDER': ('c2802', D02 + 'inputs/ORDER.json', '129e791d5b45c279443ff9e1edef5ac33d5abc51717ecbae8265abea5c247ae7'), + 'DISPATCH': ('c2802', D02 + 'inputs/DISPATCH.json.gz', '14fe756dcac93a0f3b2b7f38ba7b998dec89d56d5171b691af4fae45e5d83d11'), + 'PLAN': ('c2802', D02 + 'inputs/PLAN.json.gz', 'afb3c5c8134fc2cfce0b50a21758490c225574994b2c3c5161e53e2355acc6fa'), + 'TEMPLATE': ('c2802', D02 + 'inputs/GLOBAL-TEMPLATE.json.gz', '21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e'), + 'CLAIM': ('c2802', D02 + 'CLAIM.json', 'a2fcbc8a3ad3095ecbd310a26c02e9d11c28e4d105669a08bbdfb39d7704db51'), + 'PROFILE': ('c2802', D02 + 'PROFILE.json', '9d71407ded0b17496b0f94ca896355933a850dc6fc8456e39b0a1f72995b1406'), + 'K2751': ('c2802', D02 + 'evidence/PR2751-CLAIM.json', '78e99222196fca8b74a895b9e2db40a0e4afd1d69cd4fb52f38bfb157bac2438'), + 'K2751_own': ('c2751', D51 + 'CLAIM.json', '78e99222196fca8b74a895b9e2db40a0e4afd1d69cd4fb52f38bfb157bac2438'), + 'K2766': ('c2802', D02 + 'evidence/PR2766-CLAIM.json', '399e20ffb8bac62363f7d48c59021d5afef5f62bb6c51986ca847b02ec1e73a8'), + 'K2767': ('c2802', D02 + 'evidence/PR2767-OUTER-CLAIM.json', '252b7bbdbef293f643633ff95ba7d1eabbe83e1eebcd1cb06f51834256bde1f3'), + 'X_W_base': ('c2818', D18 + 'new/borrow/words/BORROW-WORD-43base.json.gz', 'dca8becca633ffc5e998985631bcbcab1123b27ca7f10ac6a96b1ec21ce69a66'), + 'X_W_extra': ('c2818', D18 + 'new/borrow/words/BORROW-WORD-43extra.json.gz', '6bcb3c2c73eaf7558ddc6ef6b484334f8d96b9d2b227e265483b657de00f4bb7'), + 'X_FILL': ('c2818', D18 + 'new/borrow-fill/FILL.json.gz', '2f2a25a8d82b424b1e643a8a5167361fcc5ab33cfbc6f186f4cb7ddcaf9df7d9'), + 'X_ORDER': ('c2818', D18 + 'new/borrow-fill/ORDER.json', '129e791d5b45c279443ff9e1edef5ac33d5abc51717ecbae8265abea5c247ae7'), + 'X_DISPATCH': ('c2818', D18 + 'new/borrow-fill/DISPATCH.json', 'fd8132ec8957b908ee6d871216848f18bafc6bd9304acd6185519ee26d97b1ca'), + 'X_PROV': ('c2818', D18 + 'new/BORROW-PROVIDERS.json', '391075b1411a3976850c633f92f58c35ed3f046f09d55bd435d7545124543fd4'), + 'X_R7_base': ('c2818', D18 + 'new/borrow/inputs/retired7_43base.json', '74daf5826d9191be4613a61447f4dc12789190fb49a3219f6a9df63075cac1e1'), + 'X_R7_extra': ('c2818', D18 + 'new/borrow/inputs/retired7_43extra.json', '25d9774b512da78f042287ce1de91c79c8658d06488b8fe94e548cbdd036f034'), + # attribution inputs: PR #2766's own words and claim; #2802's recorded retired5 endpoint, fill hash and local profile + 'W66_base': ('c2766', D66 + 'inputs/WORD-base.json.gz', '80e309cc16d0a86a0854d32f4f43e0d856768ea3cf5b6437061b427997ae4790'), + 'W66_extra': ('c2766', D66 + 'inputs/WORD-extra.json.gz', '88e55acb7e274c62fbb0deab7f420d85fde3c2a471735222f0b5d039bc34e2e6'), + 'K2766_own': ('c2766', D66 + 'CLAIM.json', '399e20ffb8bac62363f7d48c59021d5afef5f62bb6c51986ca847b02ec1e73a8'), + 'R5_ADMISSION': ('c2802', D02 + 'evidence/retired5/ADMISSION-RESULT.json', 'e441d6bfef1554491087a5b4701a8b23b331af3b57f77a38f3de4a47d940a6bf'), + 'R5_HOOK': ('c2802', D02 + 'evidence/retired5/HOOK-RESULT.json', '76b67d54df3a6da3bb7f6fe3402f11d2926cb48353bf068dc34eeb560784771a'), +} +STAGES = ('refit5', 'alias5', 'refit5c', 'refit7', 'hostmove2', 'alias7', 'refit7c') +STAGE_SHA = { + ('refit5', 'base'): 'ff434b1820339f0f7c2c8ba7982edc4c236e522ea30aaa56890206c0fa96f642', + ('refit5', 'extra'): 'ff434b1820339f0f7c2c8ba7982edc4c236e522ea30aaa56890206c0fa96f642', + ('alias5', 'base'): 'a9ef916e6afcba33345bce3fd0e33606f09f340e0378cf017e2994a9206b969d', + ('alias5', 'extra'): 'aeff3d1ffa74e4bffa892293f88a968e2c2b0330ad61128696a6bce7bc383b46', + ('refit5c', 'base'): 'cd8e6b7f8b8dacf21875f465e3df05bf827f12dd063fe1be7557c7281bff16f1', + ('refit5c', 'extra'): 'cd8e6b7f8b8dacf21875f465e3df05bf827f12dd063fe1be7557c7281bff16f1', + ('refit7', 'base'): 'c1ca4637c3b88828d2628c87a20f93088769dbceb9f487cb75ce90ec1a0ff5f7', + ('refit7', 'extra'): 'c1ca4637c3b88828d2628c87a20f93088769dbceb9f487cb75ce90ec1a0ff5f7', + ('hostmove2', 'base'): 'ee0f0de1ebe2f84e37e439f783a76f5d210fa1c34b3497a8d3c490296ee88e3b', + ('hostmove2', 'extra'): 'd06b7a56b457c16ea138e8265fc6f2d1b32711f0515a76137e86325a6f77a024', + ('alias7', 'base'): '100558d0f0ffbb2df38668b3d2bc4e4e11d5f328f629f5b4d931b0f619d49700', + ('alias7', 'extra'): '783ed700791b1dcd4bb35422f5fb8114a0c5d82773394b87a613e5f32da51250', + ('refit7c', 'base'): '086dc27f17448ab9bddb2e890752cf13d5965a63cd79fcf25aa7f1c9402503df', + ('refit7c', 'extra'): '086dc27f17448ab9bddb2e890752cf13d5965a63cd79fcf25aa7f1c9402503df', +} +for (_s, _t), _h in STAGE_SHA.items(): + PINS['ST_%s_%s' % (_s, _t)] = ('c2802', D02 + 'inputs/%s_43%s.json' % (_s, _t), _h) + +# Claims under test, transcribed from the PR #2802 README / CLAIM.json text (not computed from its code). +CLAIMED = dict( + aliases=[(606, 550), (635, 551), (637, 552), (638, 553), (639, 562), (667, 401), (669, 403)], + moves=[(30, 401, 564), (31, 403, 565)], + local_profile={1: 2382, 2: 648, 3: 268, 4: 128, 5: 26, 8: 8}, + inventory={4: 26, 5: 2, 7: 62, 8: 78, 9: 240}, helpers=408, roles=271728, + complete_profile={1: 1603728, 2: 431568, 3: 185082, 4: 85248, 5: 27194, 8: 5328, 32: 1, 48: 26558}, + mass=4816512, C='0.001717794984118634663827', + margin_2766='538010651632355557/1000000000000000000000000', + margin_2751='326698885104162859/500000000000000000000000', +) +# canonical-JSON sha256 of the reconstructed retired5 fill (recorded when its gzip bytes matched #2802's fill_sha256) +RETIRED5_FILL_JSON_SHA = 'ef4bd5d44e707b4a26391328e784aec6763a7684c7c15720c6a5e9f743fb498b' +V, H = 112, 9 +NSPACE = 2 * V + 480 +FULL_GENS = tuple(1 << i for i in range(H)) + + +class Fail(Exception): + pass + + +def need(cond, msg): + if not cond: + raise Fail(msg) + + +# ----------------------------------------------------------------------------------------------- inputs +def clean_env(): + env = dict(os.environ) + for k in list(env): + if k.startswith('GIT_'): + env.pop(k) + return env + + +def read_blob(repo, commit, path): + r = subprocess.run(['git', '-C', repo, 'cat-file', 'blob', '%s:%s' % (commit, path)], capture_output=True, env=clean_env()) + if r.returncode != 0: + raise Fail('cannot read %s at %s (fetch refs/pull//head first): %s' % (path, commit[:12], r.stderr.decode()[:200])) + return r.stdout + + +CANON = 'https://github.com/CrocSwap/integer-mult-bounds.git' +PULLS = dict(c2802=2802, c2751=2751, c2818=2818, c2766=2766) + + +def fetch_missing(repo): + """fetch refs/pull//head (then the bare commit) only for absent pinned commits; writes only FETCH_HEAD""" + for ck, sha in sorted(COMMIT.items()): + have = subprocess.run(['git', '-C', repo, 'cat-file', '-e', sha + '^{commit}'], capture_output=True, env=clean_env()) + if have.returncode == 0: + continue + for ref in ('refs/pull/%d/head' % PULLS[ck], sha): + subprocess.run(['git', '-C', repo, 'fetch', '--no-tags', '--quiet', CANON, ref], capture_output=True, env=clean_env()) + if subprocess.run(['git', '-C', repo, 'cat-file', '-e', sha + '^{commit}'], capture_output=True, env=clean_env()).returncode == 0: + break + + +def load_all(repo, blob_dir): + raw = {} + for key, (ck, path, sha) in sorted(PINS.items()): + if blob_dir: + fp = os.path.join(blob_dir, COMMIT[ck][:12], path) + with open(fp, 'rb') as fh: + data = fh.read() + else: + data = read_blob(repo, COMMIT[ck], path) + need(hashlib.sha256(data).hexdigest() == sha, 'pin mismatch ' + key) + raw[key] = data + js = {} + for key, data in raw.items(): + if PINS[key][1].endswith('.gz'): + data = gzip.decompress(data) + js[key] = json.loads(data.decode()) + return js + + +# ----------------------------------------------------------------------------------------------- GF(2) frames as element sets +_SUB = {} + + +def sub(gens): + """the subspace spanned by gens, as the frozenset of all its elements""" + key = tuple(sorted(int(g) for g in gens)) + s = _SUB.get(key) + if s is None: + el = {0} + for g in key: + if g not in el: + el |= {x ^ g for x in el} + s = frozenset(el) + _SUB[key] = s + return s + + +def dim(s): + return len(s).bit_length() - 1 + + +ZERO = sub(()) +FULL = sub(FULL_GENS) + + +_PERP = {} + + +def basis_of(s): + span, out = {0}, [] + for x in sorted(s): + if x not in span: + out.append(x) + span |= {y ^ x for y in span} + return out + + +def perp(s): + p = _PERP.get(s) + if p is None: + b = basis_of(s) + p = frozenset(x for x in range(1 << H) if all(bin(x & u).count('1') % 2 == 0 for u in b)) + _PERP[s] = p + return p + + +def gapply(cols, x): + y = 0 + for i in range(H): + if (x >> i) & 1: + y ^= cols[i] + return y + + +def warp_algebra(cols, U, E): + """G invertible, G(U)=E, dim U = dim E, G^-T(U^perp)=E^perp and the K_G symplectic image sends L_U to L_E""" + need(len(cols) == H and all(0 <= c < (1 << H) for c in cols), 'G shape') + table = [gapply(cols, x) for x in range(1 << H)] + need(len(set(table)) == 1 << H, 'G singular') + inv = [0] * (1 << H) + for x, y in enumerate(table): + inv[y] = x + need(len(U) == len(E), 'dim U != dim E') + need(frozenset(table[u] for u in U) == E, 'G(U) != E') + # G^-T as columns: bit j of G^-T(e_i) = bit i of G^-1(e_j) + ginv_cols = [inv[1 << j] for j in range(H)] + git_cols = [sum(((ginv_cols[j] >> i) & 1) << j for j in range(H)) for i in range(H)] + need(frozenset(gapply(git_cols, p) for p in perp(U)) == perp(E), 'G^-T(U^perp) != E^perp') + + def M(x, z): + gx = gapply(cols, x) + return gx, gx ^ gapply(git_cols, x) ^ gapply(git_cols, z) + LU = {(u, u ^ p) for u in U for p in perp(U)} + LE = {(e, e ^ p) for e in E for p in perp(E)} + need({M(x, z) for x, z in LU} == LE, 'K_G(L_U) != L_E') + # symplectic: omega((x,z),(x',z')) = x.z' + z.x' preserved on a basis of F_2^18 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + + def om(a, b): + return (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) % 2 + img = [M(*b) for b in basis] + need(all(om(img[i], img[j]) == om(basis[i], basis[j]) for i in range(2 * H) for j in range(2 * H)), 'K_G not symplectic') + return git_cols + + +# ----------------------------------------------------------------------------------------------- word program +def regs(e): + if e[0] == 'add': + return (e[1], e[2]) + return (e[1],) + + +def is_t(r): + return V <= r < 2 * V + + +def program(w): + """forward chronological event list: (time, sec, idx, item); warps get sec 'W' with idx = op""" + ev = [] + t = 0 + for i, c in enumerate(w['initial_corrections']): + ev.append((t, 'corr', i, ('corr', c['target'], c['source'], tuple(c['operator_word']), Fraction(c['coefficient'])))) + t += 1 + for sec in ('precondition', 'compensation', 'A', 'cut'): + for i, e in enumerate(w[sec]): + ev.append((t, sec, i, e)) + t += 1 + at = defaultdict(list) + for op, rec in enumerate(w['warps'], 1): + at[rec[0]].append(op) + for p in range(len(w['B']) + 1): + for op in at.get(p, []): + ev.append((t, 'W', op, ('warp', w['warps'][op - 1][1], op))) + t += 1 + if p < len(w['B']): + ev.append((t, 'B', p, w['B'][p])) + t += 1 + for i, e in enumerate(w['restore']): + ev.append((t, 'restore', i, e)) + t += 1 + return ev + + +def item_regs(it): + if it[0] == 'corr': + return (it[1], it[2]) + if it[0] == 'warp': + return (it[1],) + return regs(it) + + +def derive_cleanup(w, ev): + npre = w['prelude_events'] + restored = {int(k) for k in w['helper_final']} + + def b(r): + return r + NSPACE if r in restored else r + rec = [] + for (t, sec, i, it) in ev: + if sec in ('corr', 'precondition', 'compensation', 'cut'): + continue + if sec == 'A' and i < npre: + continue + if it[0] == 'warp' or not is_t(it[1]): + rec.append(it) + out = [] + for it in reversed(rec): + if it[0] == 'warp': + out.append(('warp', b(it[1]), -it[2])) + elif it[0] == 'add': + out.append(('add', b(it[1]), b(it[2]), -it[3], it[4])) + else: + out.append(('scale', b(it[1]), it[3], it[2])) + return out, restored + + +def check_cleanup(w, ev): + der, restored = derive_cleanup(w, ev) + given = w['cleanup'] + need(len(given) == len(der), 'cleanup length %d != derived %d' % (len(given), len(der))) + for k, (g, d) in enumerate(zip(given, der)): + need(tuple(g[:-1]) == d, 'cleanup item %d differs from derived inverse-reverse' % k) + need(sub(g[-1]) == FULL, 'cleanup item %d not at FULL' % k) + bufs = {r - NSPACE for g in given for r in (regs(g) if g[0] != 'warp' else (g[1],)) if r >= NSPACE} + need(bufs <= restored, 'buffer for a non-restored register') + return der, restored + + +# ----------------------------------------------------------------------------------------------- frames / profile (S3, S4) +def frames(w, live, ev, record=None): + """literal frame chain; returns (profile, inventory, starts, ends, at_warp) ; record: dict to fill with per-gate pre-frames""" + ports = w['ports'] + start = {} + end = {} + for r in live: + if r < V: + start[r], end[r] = sub((ports[r],)), FULL + elif r < 2 * V: + p = ports[r - V] + start[r], end[r] = ZERO, frozenset(x for x in range(1 << H) if bin(x & p).count('1') % 2 == 0) + else: + start[r] = sub(w['start_extra'][str(r)]) if str(r) in w['start_extra'] else ZERO + end[r] = sub(w['helper_final'][str(r)]) if str(r) in w['helper_final'] else FULL + cur = dict(start) + paid = Counter() + npre = w['prelude_events'] + warps_seen = {} + + def climb(q, F, where): + need(q in cur, 'register %d not live at %s' % (q, where)) + need(cur[q] <= F, 'frame not monotone: register %d at %s' % (q, where)) + d = dim(F) - dim(cur[q]) + if d: + paid[d] += 1 + cur[q] = F + after_A = False + for (t, sec, i, it) in ev: + if sec == 'corr': + need(is_t(it[1]) and it[2] in live and it[2] >= 2 * V, 'correction target/source') + need(start[it[2]] == ZERO, 'correction source with nonzero entrance frame') + need(all(w['warps'][abs(o) - 1][1] == it[2] for o in it[3]), 'correction source is not the lender of its operator') + continue + if sec in ('precondition', 'compensation'): + need(it[-1] == [] and is_t(it[1]), 'wrapper gate not a zero-frame target write') + for q in item_regs(it): + need(q in cur, 'wrapper touches non-live %d' % q) + need(not (q >= 2 * V and (str(q) in w['start_extra'] or str(q) in w['helper_final'])), + 'wrapper touches an entering or restored helper %d' % q) + continue + if sec == 'A' and i < npre: + if it[0] == 'warp': + _, r, op, fr, to = it + rec = w['warps'][abs(op) - 1] + need(rec[1] == r, 'prelude warp lender') + U, E = (sub(fr), sub(to)) + if op > 0: + warp_algebra(rec[2], U, E) + else: + warp_algebra(rec[2], E, U) + need(cur[r] == U, 'prelude warp frame mismatch on %d' % r) + cur[r] = E + else: + need(is_t(it[1]), 'prelude non-target write') + if record is not None: + record[(sec, i)] = {q: cur[q] for q in regs(it)} + for q in regs(it): + climb(q, sub(it[-1]), 'A%d' % i) + continue + if sec in ('cut', 'W', 'B', 'restore') and not after_A: + after_A = True + lev = {int(k): sub(v) for k, v in w['target_levels'].items()} + for tt in range(V): + need(cur[V + tt] == lev.get(tt, ZERO), 'target %d off its level after A' % tt) + for q, U in zip(w['centers'], w['center_frames']): + U = sub(U) + need(cur[q] == U, 'centre %d frame' % q) + served = {lev.get(e[1] - V, ZERO) for e in w['cut'] if e[2] == q} + for T in sorted(served, key=lambda s: -len(s)): + need(T <= U, 'centre chain not nested') + if T != U: + paid[dim(U) - dim(T)] += 1 + U = T + if sec == 'cut': + need(it[-1] is None and is_t(it[1]), 'cut gate shape') + continue + if sec == 'W': + op = i + pos, L, cols, U, E = w['warps'][op - 1] + U, E = sub(U), sub(E) + need(L in cur and not is_t(L), 'warp %d lender not live' % op) + warp_algebra(cols, U, E) + need(cur[L] == U, 'warp frame mismatch: op %d lender %d (U is not the propagated frame)' % (op, L)) + warps_seen[op] = (dict(U=U, E=E, cur_before=cur[L])) + cur[L] = E + continue + if sec in ('A', 'B', 'restore'): + F = sub(it[-1]) + if record is not None: + record[(sec, i)] = {q: cur[q] for q in regs(it)} + for q in regs(it): + climb(q, F, '%s%d' % (sec, i)) + for q in live: + climb(q, end[q], 'end') + inv = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return paid, inv, start, end, warps_seen + + +# ----------------------------------------------------------------------------------------------- second frame method (S3/S4) +def rref(vecs): + """canonical reduced row-echelon basis of span(vecs) over GF(2), as a sorted tuple (second representation)""" + rows = [] + for v in vecs: + v = int(v) + for b in rows: + if v ^ b < v: + v ^= b + if v: + rows = [b ^ v if b ^ v < b else b for b in rows] + rows.append(v) + rows.sort(reverse=True) + # re-reduce so that every pivot (top bit) is cleared from the other rows + out = [] + for b in rows: + for c in out: + if b ^ c < b: + b ^= c + out.append(b) + rows = out + for i in range(len(rows)): + for j in range(len(rows)): + if i != j and (rows[j] >> (rows[i].bit_length() - 1)) & 1: + rows[j] ^= rows[i] + rows.sort(reverse=True) + return tuple(rows) + + +def r_le(a, b): + """span(a) <= span(b) for canonical bases""" + return rref(a + b) == b + + +def frames_rref(w, live): + """independent recount: profile, inventory and every warp's U against the propagated frame, with RREF bases""" + full = rref(FULL_GENS) + ports = w['ports'] + cur, end, start = {}, {}, {} + for r in live: + if r < V: + start[r], end[r] = rref([ports[r]]), full + elif r < 2 * V: + p = ports[r - V] + start[r] = () + end[r] = rref([x for x in range(1, 1 << H) if bin(x & p).count('1') % 2 == 0]) + else: + start[r] = rref(w['start_extra'].get(str(r), [])) + end[r] = rref(w['helper_final'][str(r)]) if str(r) in w['helper_final'] else full + cur = dict(start) + paid = Counter() + + def up(q, F): + need(r_le(cur[q], F), 'rref: non-monotone climb on %d' % q) + if len(F) > len(cur[q]): + paid[len(F) - len(cur[q])] += 1 + cur[q] = F + for e in w['A'][:w['prelude_events']]: + if e[0] == 'warp': + need(cur[e[1]] == rref(e[3]), 'rref: prelude warp frame') + cur[e[1]] = rref(e[4]) + else: + for q in regs(e): + up(q, rref(e[-1])) + for e in w['A'][w['prelude_events']:]: + for q in regs(e): + up(q, rref(e[-1])) + lev = {int(k): rref(v) for k, v in w['target_levels'].items()} + for q, U in zip(w['centers'], w['center_frames']): + U = rref(U) + need(cur[q] == U, 'rref: centre frame') + for T in sorted({lev.get(e[1] - V, ()) for e in w['cut'] if e[2] == q}, key=len, reverse=True): + need(r_le(T, U), 'rref: centre chain') + if T != U: + paid[len(U) - len(T)] += 1 + U = T + at = defaultdict(list) + for op, rec in enumerate(w['warps'], 1): + at[rec[0]].append(op) + for p in range(len(w['B']) + 1): + for op in at.get(p, []): + pos, L, cols, U, E = w['warps'][op - 1] + need(cur[L] == rref(U), 'rref: warp %d U is not the propagated frame of %d' % (op, L)) + need(rref([gapply(cols, u) for u in U]) == rref(E), 'rref: G(U) != E for warp %d' % op) + cur[L] = rref(E) + if p < len(w['B']): + for q in regs(w['B'][p]): + up(q, rref(w['B'][p][-1])) + for e in w['restore']: + for q in regs(e): + up(q, rref(e[-1])) + for q in live: + up(q, end[q]) + inv = Counter(len(end[r]) - len(start[r]) for r in live if r >= 2 * V) + return dict(sorted(paid.items())), dict(sorted(inv.items())) + + +# ----------------------------------------------------------------------------------------------- free-algebra replay (S2) +class Words: + """interned reduced words of the free group; id 0 is the empty word""" + + def __init__(self): + self.first = [0] + self.rest = [0] + self.kids = {} + + def lmul(self, op, wid): + if self.first[wid] == -op: + return self.rest[wid] + k = (op, wid) + n = self.kids.get(k) + if n is None: + n = len(self.first) + self.first.append(op) + self.rest.append(wid) + self.kids[k] = n + return n + + +DUAL = 100000 + + +def replay(w, live, ev, cleanup, restored, dual): + W = Words() + rows = {r: {(r, 0): Fraction(1)} for r in live} + for c in restored: + rows[c + NSPACE] = {} + + def addrow(dst, src, q): + for k, x in src.items(): + y = dst.get(k, 0) + q * x + if y: + dst[k] = y + else: + dst.pop(k, None) + + def lm(row, op): + return {(v, W.lmul(op, wid)): x for (v, wid), x in row.items()} + + def step(it): + k = it[0] + if k == 'corr': + _, t, s, word, c = it + if not dual: + row = rows[s] + for op in reversed(word): + row = lm(row, op) + addrow(rows[t], row, c) + else: + row = rows[t] + for op in word: # (K_o1..K_ok)^T = K_ok^T..K_o1^T and K_o^T = (D_o)^-1 + sg = 1 if op > 0 else -1 + row = lm(row, -sg * (abs(op) + DUAL)) + addrow(rows[s], row, -c) + elif k == 'warp': + op = it[2] + if dual: + op = (1 if op > 0 else -1) * (abs(op) + DUAL) + rows[it[1]] = lm(rows[it[1]], op) + elif k == 'add': + q = Fraction(it[3], it[4]) + need(it[1] != it[2], 'self add') + if not dual: + addrow(rows[it[1]], rows[it[2]], q) + else: + addrow(rows[it[2]], rows[it[1]], -q) + elif k == 'scale': + q = Fraction(it[2], it[3]) + need(q != 0, 'zero scale') + if dual: + q = 1 / q + rows[it[1]] = {kk: q * x for kk, x in rows[it[1]].items()} + else: + raise Fail('unknown item ' + str(k)) + for (t, sec, i, it) in ev: + if it[0] == 'warp' and sec == 'A': + step(('warp', it[1], it[2])) + else: + step(it) + if not dual: + for tt in range(V): + need(rows[V + tt] == {(V + tt, 0): 1, (tt, 0): 1}, 'forward target %d wrong before cleanup' % tt) + for c in restored: + need(rows[c] == {(c, 0): 1}, 'restored helper %d not its own input' % c) + need(not any(v == c for r in live if r != c for (v, _) in rows[r]), 'restored input %d still read' % c) + need(rows[c + NSPACE] == {}, 'buffer dirty before cleanup') + for it in cleanup: + step(it) + for r in live: + if dual and r < V: + exp = {(r, 0): 1, (r + V, 0): -1} + elif (not dual) and is_t(r): + exp = {(r, 0): 1, (r - V, 0): 1} + else: + exp = {(r, 0): 1} + need(rows[r] == exp, '%s endpoint wrong on register %d' % ('dual' if dual else 'forward', r)) + for c in restored: + need(rows[c + NSPACE] == {}, 'zero buffer %d not returned to zero' % c) + return len(W.first) + + +# ----------------------------------------------------------------------------------------------- second method: random matrix realisation mod p +PRIME = (1 << 61) - 1 + + +def matmul(A, B): + n = len(A) + return [[sum(A[i][k] * B[k][j] for k in range(n)) % PRIME for j in range(n)] for i in range(n)] + + +def matinv(A): + n = len(A) + M = [list(A[i]) + [1 if i == j else 0 for j in range(n)] for i in range(n)] + for c in range(n): + p = next((r for r in range(c, n) if M[r][c]), None) + if p is None: + return None + M[c], M[p] = M[p], M[c] + iv = pow(M[c][c], PRIME - 2, PRIME) + M[c] = [x * iv % PRIME for x in M[c]] + for r in range(n): + if r != c and M[r][c]: + f = M[r][c] + M[r] = [(x - f * y) % PRIME for x, y in zip(M[r], M[c])] + return [row[n:] for row in M] + + +def realise(w, live, ev, cleanup, restored, dual, seed, d=4): + rnd = random.Random(seed) + K = {} + for op in range(1, len(w['warps']) + 1): + while True: + A = [[rnd.randrange(PRIME) for _ in range(d)] for _ in range(d)] + Ai = matinv(A) + if Ai is not None: + break + At = [list(x) for x in zip(*A)] + AiT = [list(x) for x in zip(*Ai)] + # forward letters K, K^-1; dual letters D = K^-T, D^-1 = K^T + K[op], K[-op], K[op + DUAL], K[-(op + DUAL)] = A, Ai, AiT, At + vec = {r: [rnd.randrange(PRIME) for _ in range(d)] for r in live} + init = {r: list(x) for r, x in vec.items()} + for c in restored: + vec[c + NSPACE] = [0] * d + + def mv(M, x): + return [sum(M[i][k] * x[k] for k in range(d)) % PRIME for i in range(d)] + + def q_of(n, m): + return n * pow(m % PRIME, PRIME - 2, PRIME) % PRIME + + def step(it): + k = it[0] + if k == 'corr': + _, t, s, word, c = it + c = q_of(c.numerator, c.denominator) + if not dual: + x = vec[s] + for op in reversed(word): + x = mv(K[op], x) + vec[t] = [(a + c * b) % PRIME for a, b in zip(vec[t], x)] + else: + x = vec[t] + for op in word: + sg = 1 if op > 0 else -1 + x = mv(K[-sg * (abs(op) + DUAL)], x) + vec[s] = [(a - c * b) % PRIME for a, b in zip(vec[s], x)] + elif k == 'warp': + op = it[2] + if dual: + op = (1 if op > 0 else -1) * (abs(op) + DUAL) + vec[it[1]] = mv(K[op], vec[it[1]]) + elif k == 'add': + q = q_of(it[3], it[4]) + if not dual: + vec[it[1]] = [(a + q * b) % PRIME for a, b in zip(vec[it[1]], vec[it[2]])] + else: + vec[it[2]] = [(a - q * b) % PRIME for a, b in zip(vec[it[2]], vec[it[1]])] + else: + q = q_of(it[2], it[3]) + if dual: + q = pow(q, PRIME - 2, PRIME) + vec[it[1]] = [a * q % PRIME for a in vec[it[1]]] + for (t, sec, i, it) in ev: + step(('warp', it[1], it[2]) if (it[0] == 'warp' and sec == 'A') else it) + for it in cleanup: + step(it) + for r in live: + if dual and r < V: + exp = [(a - b) % PRIME for a, b in zip(init[r], init[r + V])] + elif (not dual) and is_t(r): + exp = [(a + b) % PRIME for a, b in zip(init[r], init[r - V])] + else: + exp = init[r] + need(vec[r] == exp, 'matrix realisation (%s, seed %d) wrong on register %d' % ('dual' if dual else 'forward', seed, r)) + for c in restored: + need(vec[c + NSPACE] == [0] * d, 'matrix realisation buffer %d nonzero' % c) + + +# ----------------------------------------------------------------------------------------------- S1 + occupancy timeline (S2) +def segments(w, ev): + """per register: list of segments; segment k = (opening warp op or None, [(time, sec, idx, item)])""" + seg = defaultdict(lambda: [[None, []]]) + for e in ev: + t, sec, i, it = e + if sec == 'W': + seg[it[1]].append([it[2], [], (5, w['warps'][it[2] - 1][0] - 0.5)]) + continue + for r in set(item_regs(it)): + seg[r][-1][1].append(e) + return seg + + +def role_map(P, W, aliases, moves): + """declared map of parent roles (register, segment) to final registers; returns function (r, k) -> r'""" + mp = {} + for (h, L, op) in aliases: + mp[(h, 0)] = (L, op) + for (op, L0, L1, k0) in moves: + mp[(L0, k0)] = (L1, op) + return mp + + +SR = dict(corr=0, precondition=1, compensation=2, A=3, cut=4, B=5, restore=6) + + +def pk(e): + return (SR[e[1]], e[2]) + + +def s1_and_occupancy(P, W, live_W, decl, part='both'): + """event-level diff P -> W and the per-register occupancy timeline; returns a report dict""" + rep = {} + if part == 'occ': + return occupancy_only(P, W, rep) + keys_same = ('ports', 'centers', 'center_frames', 'target_levels', 'precondition', 'compensation', + 'initial_corrections', 'prelude_events', 'helper_final', 'cut', 'kind', 'base') + need(set(P) == set(W), 'top-level keys differ') + for k in keys_same: + need(P[k] == W[k], 'field %s changed (undeclared)' % k) + new_removed = [h for h, _ in CLAIMED['aliases']] + need(W['removed'] == P['removed'] + new_removed, 'removed list is not parent + the seven followers') + need({k: v for k, v in P['start_extra'].items() if int(k) not in new_removed} == W['start_extra'], 'start_extra change beyond the removed followers') + need(all(W['report'][k] == P['report'][k] for k in ('R', 'h', 'v')), 'report R/h/v changed') + # warps: 1..65 unchanged except 30, 31 replaced in place; 66..72 appended + need(len(P['warps']) == 65 and len(W['warps']) == 72, 'warp counts') + changed = [op for op in range(1, 66) if P['warps'][op - 1] != W['warps'][op - 1]] + need(changed == [30, 31], 'warps changed in place: %s' % changed) + need([W['warps'][op - 1][1] for op in range(66, 73)] == [L for _, L in CLAIMED['aliases']], 'appended warp lenders') + need([(op, P['warps'][op - 1][1], W['warps'][op - 1][1]) for op in (30, 31)] == [(o, a, b) for o, a, b in CLAIMED['moves']], 'moved warp lenders') + # A and restore: identical gates; frame changes only + fr_changes = {} + for sec in ('A', 'restore'): + need(len(P[sec]) == len(W[sec]), 'section %s length' % sec) + for i, (a, b) in enumerate(zip(P[sec], W[sec])): + need(a[:-1] == b[:-1], 'gate %s%d changed' % (sec, i)) + if a[-1] != b[-1]: + need(a[0] != 'warp', 'prelude warp frames changed') + fr_changes[(sec, i)] = (a[-1], b[-1]) + # B: role-aligned comparison + evP, evW = program(P), program(W) + segP, segW = segments(P, evP), segments(W, evW) + # parent segment index of each move's hostee = the segment opened by the old warp op + moves = [] + for (op, L0, L1) in CLAIMED['moves']: + k0 = next(k for k, s in enumerate(segP[L0]) if s[0] == op) + moves.append((op, L0, L1, k0)) + aliases = [(h, L, 65 + j + 1) for j, (h, L) in enumerate(CLAIMED['aliases'])] + mp = role_map(P, W, aliases, moves) + # final register of every parent (register, time): walk the parent's segments + target_of = {} + for r, sl in segP.items(): + for k, s in enumerate(sl): + dest = mp.get((r, k)) + for e in s[1]: + target_of[(r, e[0])] = dest[0] if dest else r + timeP = {e[0]: e for e in evP if e[1] != 'W'} + # map parent non-warp events onto final events by (section, index) + keyW = {(e[1], e[2]): e for e in evW if e[1] != 'W'} + relabelled = Counter() + for e in evP: + t, sec, i, it = e + if sec == 'W': + continue + f = keyW.get((sec, i)) + need(f is not None, 'parent event %s%d missing in final' % (sec, i)) + fit = f[3] + if it[0] == 'corr': + need(it == fit, 'correction changed') + continue + if sec in ('B',): + exp = list(it[:-1]) + for j in ((1, 2) if it[0] == 'add' else (1,)): + exp[j] = target_of.get((it[j], t), it[j]) + if exp != list(fit[:-1]): + raise Fail('B%d: final gate %s is not the declared relabel %s of parent %s' % (i, fit[:-1], exp, it[:-1])) + if exp != list(it[:-1]): + relabelled[sec] += 1 + if it[-1] != fit[-1]: + fr_changes[(sec, i)] = (it[-1], fit[-1]) + else: + need(list(it) == list(fit) or (sec in ('A', 'restore')), 'event %s%d changed' % (sec, i)) + need(len([e for e in evP if e[1] == 'B']) == len([e for e in evW if e[1] == 'B']), 'B length changed') + rep['B_relabelled_gates'] = relabelled['B'] + rep['frame_changes'] = len(fr_changes) + # declared frames: last writer over the refit stages + declared = {} + for st in ('refit5', 'refit5c', 'refit7', 'refit7c'): + for sec, i, F in decl[st]['frames']: + declared[(sec, i)] = F + undeclared = sorted(k for k in fr_changes if k not in declared or sub(declared[k]) != sub(fr_changes[k][1])) + # frames of gates that the alias/hostmove stages re-emit are allowed only if unchanged or declared + need(not undeclared, 'undeclared frame changes: %s' % undeclared[:6]) + notapplied = sorted(k for k in declared if sub(W[k[0]][k[1]][-1]) != sub(declared[k])) + need(not notapplied, 'declared refit frames not present in the final word: %s' % notapplied[:6]) + rep['declared_frames'] = len(declared) + rep['declared_frames_effective'] = len([k for k in declared if k in fr_changes]) + return rep, fr_changes, evW + + +def occupancy_only(P, W, rep): + evP, evW = program(P), program(W) + segP, segW = segments(P, evP), segments(W, evW) + moves = [] + for (op, L0, L1) in CLAIMED['moves']: + k0 = next(k for k, s in enumerate(segP[L0]) if s[0] == op) + moves.append((op, L0, L1, k0)) + aliases = [(h, L, 65 + j + 1) for j, (h, L) in enumerate(CLAIMED['aliases'])] + mp = role_map(P, W, aliases, moves) + # occupancy timeline on the final word: every final segment = exactly one parent role, time-ordered + occ = [] + for (h, L, op) in aliases: + sP_L = segP[L] + sW_L = segW[L] + kWs = [k for k, s in enumerate(sW_L) if s[0] == op] + need(len(kWs) == 1, 'OCC: alias warp %d is not on lender %d' % (op, L)) + kW = kWs[0] + wtime = sW_L[kW][2] + # the lender role(s) that precede the warp: all parent segments of L that stay on L + stay = [e for k, s in enumerate(sP_L) if (L, k) not in mp for e in s[1]] + lend_last = max(pk(e) for e in stay) + fol = segP[h] + need(len(fol) == 1, 'follower %d had warps in the parent' % h) + fol_ev = fol[0][1] + fol_first = min(pk(e) for e in fol_ev) + need(lend_last < wtime, 'OCC: lender %d has an own event at/after its alias warp %d' % (L, op)) + need(fol_first > wtime, 'OCC: follower %d has an event before alias warp %d' % (h, op)) + need(all(e[1] in ('B', 'restore') for e in fol_ev), 'OCC: follower %d has events outside B/restore' % h) + need(kW == len(sW_L) - 1 or all(pk(e) < sW_L[kW + 1][2] for e in fol_ev), 'OCC: follower %d outlives the segment' % h) + # the final segment after the warp is exactly the follower's events (same times, same items up to relabel) + segev = [(e[1], e[2]) for e in sW_L[kW][1]] + need(segev == [(e[1], e[2]) for e in fol_ev], 'OCC: final segment of %d after warp %d is not exactly follower %d' % (L, op, h)) + need(all(e[1] == 'A' or e[1] in ('corr', 'precondition', 'compensation', 'cut') or e[1] == 'B' for e in stay), 'lender restore event') + last_sec = next(e for e in stay if pk(e) == lend_last) + occ.append(dict(follower=h, lender=L, op=op, warp_B_pos=W['warps'][op - 1][0], + lender_last=[last_sec[1], last_sec[2]], follower_first=['B', min(e[2] for e in fol_ev if e[1] == 'B')], + lender_events=len(stay), follower_events=len(fol_ev), + lender_sections=dict(Counter(e[1] for e in stay)))) + for (op, L0, L1, k0) in moves: + host = segP[L0][k0][1] + sW = segW[L1] + kWs = [k for k, s in enumerate(sW) if s[0] == op] + need(len(kWs) == 1, 'OCC: moved warp %d is not on new lender %d' % (op, L1)) + kW = kWs[0] + wtime = sW[kW][2] + own = [e for k, s in enumerate(segP[L1]) for e in s[1]] + need(len(segP[L1]) == 1, 'new lender %d already a lender in the parent' % L1) + need(max(pk(e) for e in own) < wtime, 'OCC: new lender %d acts at/after moved warp %d' % (L1, op)) + need(min(pk(e) for e in host) > wtime, 'OCC: hostee of %d enters before its moved warp' % op) + need([(e[1], e[2]) for e in sW[kW][1]] == [(e[1], e[2]) for e in host], 'OCC: final segment of %d after warp %d is not exactly the hostee' % (L1, op)) + need(kW == len(sW) - 1, 'OCC: later warp on %d' % L1) + # the old lender keeps no hostee event + rest_old = [e for k, s in enumerate(segW[L0]) for e in s[1] if s[0] == op] + need(not rest_old, 'old lender keeps the moved warp') + last = max(own, key=pk) + occ.append(dict(hostee_warp=op, old_lender=L0, new_lender=L1, warp_B_pos=W['warps'][op - 1][0], + old_warp_B_pos=P['warps'][op - 1][0], new_lender_last=[last[1], last[2]], + hostee_first=['B', min(e[2] for e in host if e[1] == 'B')], hostee_events=len(host))) + # every final register: segments are exactly the mapped parent roles (complete partition) + roles_to = defaultdict(list) + for r, sl in segP.items(): + for k, s in enumerate(sl): + dest = mp.get((r, k)) + if dest: + roles_to[dest].append((r, k)) + else: + roles_to[(r, s[0])].append((r, k)) + target_of = {} + for r, sl in segP.items(): + for k, s in enumerate(sl): + dest = mp.get((r, k)) + for e in s[1]: + target_of[(r, e[0])] = dest[0] if dest else r + + def relabel(e): + t, sec, i, it = e + if it[0] == 'corr': + return it + x = list(it[:-1]) if sec in ('A', 'B', 'restore') and it[0] != 'warp' else list(it) + if it[0] != 'warp': + for j in ((1, 2) if it[0] == 'add' else (1,)): + x[j] = target_of.get((it[j], t), it[j]) + return x + + def body(e): + t, sec, i, it = e + if it[0] == 'corr': + return it + return list(it[:-1]) if sec in ('A', 'B', 'restore') and it[0] != 'warp' else list(it) + for r, sl in segW.items(): + for k, s in enumerate(sl): + src = roles_to.get((r, s[0]), []) + need(len(src) == 1, 'OCC: final segment (%d, opened by %s) maps to %d parent roles' % (r, s[0], len(src))) + pr, pkk = src[0] + pe = segP[pr][pkk][1] + need([(e[1], e[2]) for e in s[1]] == [(e[1], e[2]) for e in pe], + 'OCC: final segment (%d, %s) events differ from parent role (%d, %d)' % (r, s[0], pr, pkk)) + need([body(e) for e in s[1]] == [relabel(e) for e in pe], + 'OCC: final segment (%d, %s) gate content differs from relabelled parent role (%d, %d)' % (r, s[0], pr, pkk)) + for h, _ in CLAIMED['aliases']: + need(h not in segW or all(not s[1] for s in segW[h]), 'removed follower %d still has events' % h) + rep['occupancy'] = occ + rep['segments_checked'] = sum(len(sl) for sl in segW.values()) + return rep + + +# ----------------------------------------------------------------------------------------------- stage records vs diff +def stage_records(P, W, decl, fr_changes): + rep = {} + a5 = decl['alias5']['aliases'] + a7 = decl['alias7']['aliases'] + mv = decl['hostmove2']['moves'] + need([(a['h'], a['L']) for a in a5 + a7] == CLAIMED['aliases'], 'alias stage records') + need([[a['pos'], a['L'], a['G'], a['U'], a['E']] for a in a5 + a7] == W['warps'][65:72], 'alias warp records') + need([[m['pos'], m['L_new'], m['G'], m['U'], m['E']] for m in mv] == [W['warps'][29], W['warps'][30]], 'move warp records') + need([m['old_record'] for m in mv] == [P['warps'][29], P['warps'][30]], 'move old records') + need(len(decl['alias5']['declared_gate_edit']) == 70 and len(decl['hostmove2']['declared_gate_edit']) == 28 and + len(decl['alias7']['declared_gate_edit']) == 28, 'declared gate edit counts') + ins = Counter() + per_stage = {} + dels, adds = {}, {} + for st in ('alias5', 'hostmove2', 'alias7'): + k_st = Counter() + for kind, i, g in decl[st]['declared_gate_edit']: + ins[kind] += 1 + k_st[kind] += 1 + d = dels if kind == 'delete' else adds + need(i not in d, 'B%d edited by two stages' % i) + d[i] = g + need(k_st['delete'] == k_st['insert'], 'stage %s: deletes and inserts do not pair up' % st) + per_stage[st] = k_st['delete'] + rep['declared_gate_edits'] = dict(ins) + rep['declared_edit_pairs_per_stage'] = per_stage + # the declared edits are exactly the relabelled positions: deletes = parent gates, inserts = final gates + moved = sorted(i for i in range(len(P['B'])) if P['B'][i][:-1] != W['B'][i][:-1]) + need(sorted(dels) == sorted(adds) == moved, 'declared gate-edit positions differ from the relabelled positions') + need(all(dels[i] == P['B'][i][:-1] and adds[i] == W['B'][i][:-1] for i in moved), 'declared gate edits differ from parent/final gates') + rep['relabelled_positions'] = len(moved) + rep['refit_frames'] = {st: len(decl[st]['frames']) for st in ('refit5', 'refit5c', 'refit7', 'refit7c')} + rep['refit7_prev'] = decl['refit7']['previous_frames'] + rep['refit7_dims'] = [[sec, i, dim(sub(F0)), dim(sub(W[sec][i][-1]))] for sec, i, F0 in decl['refit7']['previous_frames']] + # refit7c records no previous frames; no earlier stage touches its gates, so the previous frame is the parent's + earlier = {(sec, i) for st in ('refit5', 'refit5c', 'refit7') for sec, i, _ in decl[st]['frames']} + need(not any((sec, i) in earlier for sec, i, _ in decl['refit7c']['frames']), 'refit7c gate also refitted earlier') + rep['refit7c_dims'] = [[sec, i, dim(sub(P[sec][i][-1])), dim(sub(W[sec][i][-1]))] for sec, i, _ in decl['refit7c']['frames']] + return rep + + +def refit_exactness(W, live, decl): + """S3 refits: each declared frame contains the propagated floor (join of incident pre-frames); report exactness""" + ev = program(W) + rec = {} + frames(W, live, ev, record=rec) + out = [] + declared = [] + for st in ('refit5', 'refit5c', 'refit7', 'refit7c'): + for sec, i, F in decl[st]['frames']: + declared.append((st, sec, i, F)) + final_of = {} + for st, sec, i, F in declared: + final_of[(sec, i)] = st + for st, sec, i, F in declared: + if final_of[(sec, i)] != st: + continue + pre = rec[(sec, i)] + floor = sub([x for s in pre.values() for x in s]) + Fs = sub(W[sec][i][-1]) + need(floor <= Fs, 'refit %s %s%d below the propagated floor' % (st, sec, i)) + out.append(dict(stage=st, gate='%s%d' % (sec, i), dim=dim(Fs), floor_dim=dim(floor), exact_floor=(Fs == floor))) + return out + + +def above_floor_neutral(W, live, decl): + """the declared refit frames above their propagated floor: lowering each one alone, and all of them together, to the + floor keeps the frame chain legal (monotone climbs; every warp's U equals the propagated frame) and leaves the local + profile unchanged, so these frames carry no cost""" + ev = program(W) + rec = {} + base = dict(frames(W, live, ev, record=rec)[0]) + need(base == CLAIMED['local_profile'], 'final profile') + above = {} + for st in ('refit5', 'refit5c', 'refit7', 'refit7c'): + for sec, i, F in decl[st]['frames']: + floor = sub([x for s_ in rec[(sec, i)].values() for x in s_]) + if sub(W[sec][i][-1]) != floor: + above[(sec, i)] = floor + keys = sorted(above, key=lambda k: (SR[k[0]], k[1])) + variants = [[k] for k in keys] + [keys] + for sel in variants: + w = dict(W) + for sec in {k[0] for k in sel}: + w[sec] = list(W[sec]) + for sec, i in sel: + w[sec][i] = list(W[sec][i][:-1]) + [basis_of(above[(sec, i)])] + paid = dict(frames(w, live, program(w))[0]) + need(paid == base, 'lowering %s to the floor changes the profile to %s' % (sel, dict(sorted(paid.items())))) + return dict(above_floor=['%s%d dim %d floor %d' % (sec, i, dim(sub(W[sec][i][-1])), dim(above[(sec, i)])) for sec, i in keys], + variants_checked=len(variants), profile_unchanged=True) + + +# ----------------------------------------------------------------------------------------------- stage chain (S1, attribution) +def apply_stage(state, name, patch): + """own application of one declared stage: refits replace frames only; alias/move stages replace the listed + fields and the report; the inverse-reverse cleanup is re-derived (our derive_cleanup)""" + import copy + w = copy.deepcopy(state) + if name.startswith('refit'): + for sec, i, F in patch['frames']: + need(sec in ('A', 'B', 'restore') and w[sec][i][0] != 'warp', 'refit target %s%d' % (sec, i)) + w[sec][i] = list(w[sec][i][:-1]) + [F] + w['report'] = dict(w['report'], local_profile=patch['local_profile']) + else: + need(set(patch['fields']) <= {'start_extra', 'removed', 'B', 'restore', 'warps'}, 'stage %s replaces unexpected fields' % name) + need(patch['prelude_events'] == w['prelude_events'], 'prelude count') + for k, v in patch['fields'].items(): + w[k] = copy.deepcopy(v) + w['report'] = copy.deepcopy(patch['report']) + der, _ = derive_cleanup(w, program(w)) + w['cleanup'] = [list(x) + [list(FULL_GENS[::-1])] for x in der] + return w + + +def stage_chain(P, W, decl): + """rebuild W from P through the seven declared stages; every intermediate state passes frames, profile and both replays""" + st = P + out = [] + states = {} + for name in STAGES: + st = apply_stage(st, name, decl[name]) + live = set(r for r in range(NSPACE) if r not in set(st['removed'])) + ev = program(st) + paid, inv, _, _, _ = frames(st, live, ev) + need(dict(paid) == {int(k): v for k, v in st['report']['local_profile'].items()}, 'stage %s profile %s' % (name, dict(paid))) + need(dict(inv) == {int(k): v for k, v in st['report']['width_inventory'].items()}, 'stage %s inventory' % name) + cl, restored = check_cleanup(st, ev) + replay(st, live, ev, cl, restored, False) + replay(st, live, ev, cl, restored, True) + states[name] = st + out.append(dict(stage=name, profile=dict(sorted(paid.items())), mass=sum(k * v for k, v in paid.items()), + helpers=len([r for r in live if r >= 2 * V]))) + norm = lambda w: json.loads(json.dumps(w)) + need(norm(st) == norm(W), 'the declared stages do not rebuild the final word') + return out, states + + +# ----------------------------------------------------------------------------------------------- S5 fill +def windows_from_template(template, order): + rank = {} + for c in template['idle_children']: + need(rank.get(c['child'], c['rank']) == c['rank'], 'idle child rank varies') + rank[c['child']] = c['rank'] + pair_of_stage = {e['stage']: e['pair'] for e in template['recipe'] if e['kind'] == 'local'} + blocks = [] + for e in template['execution_schedule']: + if e['kind'] == 'local_cover_sweep': + blocks.append([e]) + elif e['kind'] in ('idle_cover_sweep', 'bridge'): + need(blocks, 'event before the first local sweep') + blocks[-1].append(e) + by_stage = {b[0]['stage']: b for b in blocks} + seen = Counter() + last = {} + win = {} + for t, (stage, rep) in enumerate(order): + need(seen[rep] == stage, 'order is not stage-chronological per replica') + seen[rep] += 1 + for e in by_stage[stage]: + if e['kind'] == 'local_cover_sweep': + last[(rep, pair_of_stage[stage])] = t + elif e['kind'] == 'bridge': + last[(rep, e['src'])] = t + last[(rep, e['dst'])] = t + else: + lo = last.get((rep, e['pair']), -1) + for c in e['child_indices']: + if c in rank: + win[(rep, c)] = (rank[c], lo, t) + need(set(seen.values()) == {9} and len(seen) == 74, 'replica progression') + return win + + +def static_widths(w, helpers): + """hosting width of each live helper = dim(end frame) - dim(entrance frame), read from the word itself""" + out = {} + for r in helpers: + s = sub(w['start_extra'][str(r)]) if str(r) in w['start_extra'] else ZERO + e = sub(w['helper_final'][str(r)]) if str(r) in w['helper_final'] else FULL + need(s <= e, 'entrance frame not inside end frame for %d' % r) + out[r] = dim(e) - dim(s) + return out + + +def s5_fill(js, words, live_by_tag, widths_by_tag, fill_key='FILL'): + fill = js[fill_key] + order = js['ORDER'] + dispatch = {(s, r): p for s, r, p in js['DISPATCH']} + for s, r, p in fill['dispatch_overrides']: + dispatch[(s, r)] = p + need(fill['columns'] == ['time', 'helper', 'owner_replica', 'child', 'port', 'offset'], 'fill columns') + tag_of = {'gauge44': 'base', 'extra': 'extra'} + need(live_by_tag['base'] == live_by_tag['extra'], 'live helper sets differ between words') + live = live_by_tag['base'] + R = len(live) + win = windows_from_template(js['TEMPLATE'], order) + plan = js['PLAN'] + fam = {} + used = defaultdict(int) + per_call = [0] * len(order) + rows = fill['rows'] + need(len(rows) == len(order) * R, 'role count %d != calls x word-derived R (%d x %d)' % (len(rows), len(order), R)) + for row in rows: + need(len(row) == 6 and all(type(x) is int for x in row), 'role shape') + t, h, o, c, port, off = row + need(0 <= t < len(order) and 0 <= port < V, 'role bounds') + need(0 <= h < R, 'FILL-HELPER-SET: helper index %d outside the word-derived inventory (R=%d)' % (h, R)) + need((o, c) in win, 'no window for owner %d child %d' % (o, c)) + cap, lo, hi = win[(o, c)] + need(lo < t <= hi, 'role outside its window') + need(not (per_call[t] >> h) & 1, 'helper hosted twice in one call') + per_call[t] |= 1 << h + fk = (t, o, 2 * plan['pairs'][str(c)] + plan['sides'][str(c)], port) + need(fk not in fam, 'family hosts two helpers in one call') + fam[fk] = 1 + width = widths_by_tag[tag_of[dispatch[tuple(order[t])]]][live[h]] + need(off >= 0 and off + width <= cap, 'bin capacity') + m = ((1 << width) - 1) << off + b = (o, c, port) + need(not used[b] & m, 'overlapping bin cells') + used[b] |= m + need(all(x == (1 << R) - 1 for x in per_call), 'FILL-HELPER-SET: some call does not host exactly the word-derived helper set') + idle = Counter() + for (o, c), (cap, lo, hi) in win.items(): + for port in range(V): + m = used.get((o, c, port), 0) + u = m.bit_length() + need(m == (1 << u) - 1, 'bin not prefix-compact') + if cap > u: + idle[cap - u] += 1 + return dict(R=R, roles=len(rows), windows=len(win), idle=dict(sorted(idle.items())), dispatch=dict(Counter(dispatch[tuple(x)] for x in order))) + + +def fill_transform(js, liveP, liveW): + """FILL = FILL2751 minus the seven removed followers' roles, renumbered, offsets re-tiled in old offset order""" + gone = set(liveP) - set(liveW) + need(sorted(gone) == sorted(h for h, _ in CLAIMED['aliases']), 'removed helper set between fills') + newidx = {r: i for i, r in enumerate(liveW)} + old = defaultdict(list) + for t, h, o, c, p, off in js['FILL51']['rows']: + r = liveP[h] + if r in gone: + continue + old[(o, c, p)].append((off, t, newidx[r])) + new = defaultdict(list) + for t, h, o, c, p, off in js['FILL']['rows']: + new[(o, c, p)].append((off, t, h)) + need(set(old) == set(new), 'bins differ') + for b in old: + a = [(t, h) for off, t, h in sorted(old[b])] + n = [(t, h) for off, t, h in sorted(new[b])] + need(a == n, 'bin %s: roles or their order differ from the parent fill' % (b,)) + return dict(dropped_roles=len(js['FILL51']['rows']) - len(js['FILL']['rows']), bins=len(old)) + + +# ----------------------------------------------------------------------------------------------- S6 moment root +SLACK = Decimal('1e-70') + + +def moment(profile, z, prec, rounding): + """f(z) = sum n_r (r/73)^(1-z) at `prec` significant digits (z rational, all r < 73, so f increases in z). + Python's Decimal ln() and exp() are correctly rounded with ROUND_HALF_EVEN whatever the context rounding mode; + `rounding` applies only to the divisions, the subtraction, the products and the sums. The value is therefore an + approximation, not a directed bound; root_bracket() turns it into a bound with an explicit error budget.""" + with localcontext() as ctx: + ctx.prec = prec + ctx.rounding = rounding + zd = Decimal(z.numerator) / Decimal(z.denominator) + s = Decimal(0) + for r, n in sorted(profile.items()): + # (r/73)^(1-z) = exp((1-z) ln(r/73)); ln(r/73) < 0, 1-z > 0 + lr = (Decimal(r) / Decimal(73)).ln() + s += Decimal(n) * ((Decimal(1) - zd) * lr).exp() + return s + + +def root_bracket(profile, total, lo, hi): + """certify f(lo) < total < f(hi), hence a root in (lo, hi). + + Error budget at 80 digits, with u = 1e-79 bounding the relative error of one rounded operation in any mode: + z: rel. <= u; a = 1 - z: abs. <= 2u (0 < z < 1); q = r/73: rel. <= u; ln q: abs. <= u + |ln q| u <= 5.3u + (|ln q| <= ln 73 < 4.3); y = a ln q: abs. <= 5.3u + 4.3 * 2u + 4.3u < 19u; exp(y): rel. <= e^(19u) - 1 + u < 21u; + the product with n and at most 8 positive summands add <= 9u. Hence |computed - f| < 30u f = 3e-78 f, far inside + the relative slack 1e-70. The widening itself is done at 100 digits with directed rounding (1 +- 1e-70 is exact + there), so f_lo_upper >= f(lo) and f_hi_lower <= f(hi) rigorously; Decimal comparisons are exact.""" + up = moment(profile, lo, 80, ROUND_CEILING) + dn = moment(profile, hi, 80, ROUND_FLOOR) + with localcontext() as ctx: + ctx.prec = 100 + ctx.rounding = ROUND_CEILING + f_lo_upper = up * (Decimal(1) + SLACK) + ctx.rounding = ROUND_FLOOR + f_hi_lower = dn * (Decimal(1) - SLACK) + ok = f_lo_upper < total < f_hi_lower + margins = ('%.4e' % (total - f_lo_upper), '%.4e' % (f_hi_lower - total)) + return ok, (str(up)[:40], str(dn)[:40], margins) + + +def dec(q, digits): + with localcontext() as ctx: + ctx.prec = digits + return str(Decimal(q.numerator) / Decimal(q.denominator)) + + +# ----------------------------------------------------------------------------------------------- driver +def run_all(js, quick=False, log=print, skip=()): + res = dict(rules={}) + + def rule(name, fn): + if any(name.startswith(p) for p in skip): + return None + try: + v = fn() + res['rules'][name] = dict(ok=True, info=v) + log('PASS %-34s %s' % (name, '' if v is None else json.dumps(v, default=str)[:160])) + return v + except Fail as e: + res['rules'][name] = dict(ok=False, info=str(e)) + log('FAIL %-34s %s' % (name, e)) + return None + except Exception as e: # a crash is a failure too, but is labelled so that controls cannot count it + res['rules'][name] = dict(ok=False, info='ERROR %s: %s' % (type(e).__name__, e)) + log('FAIL %-34s ERROR %s: %s' % (name, type(e).__name__, e)) + return None + # pins and identities + rule('PIN-2751-COPIES', lambda: need(js['P_base'] == js['P51_base'] and js['P_extra'] == js['P51_extra'] and js['FILL51'] == js['FILL51_own'] and js['K2751'] == js['K2751_own'], 'copies differ') or 'byte-identical') + words = {} + live = {} + widths = {} + profiles = {} + r5 = {} + for tag in ('base', 'extra'): + P, W = js['P_' + tag], js['W_' + tag] + decl = {st: js['ST_%s_%s' % (st, tag)] for st in STAGES} + liveW = [r for r in range(NSPACE) if r not in set(W['removed'])] + liveP = [r for r in range(NSPACE) if r not in set(P['removed'])] + live[tag] = [r for r in liveW if r >= 2 * V] + live['P_' + tag] = [r for r in liveP if r >= 2 * V] + widths[tag] = static_widths(W, live[tag]) + widths['P_' + tag] = static_widths(P, live['P_' + tag]) + out = {} + + def s1(): + rep, fr, evW = s1_and_occupancy(P, W, liveW, decl) + out['ev'] = evW + out['fr'] = fr + return rep + rule('S1-DIFF-%s' % tag, s1) + rule('OCC-TIMELINE-%s' % tag, lambda: s1_and_occupancy(P, W, liveW, decl, part='occ')) + rule('S1-STAGE-RECORDS-%s' % tag, lambda: stage_records(P, W, decl, out.get('fr', {}))) + ev = program(W) + + def s3s4(): + paid, inv, start, end, ws = frames(W, set(liveW), ev) + need(dict(paid) == CLAIMED['local_profile'], 'local profile %s' % dict(sorted(paid.items()))) + need(dict(paid) == {int(k): v for k, v in W['report']['local_profile'].items()}, 'report profile') + prov = js['PROV']['gauge44' if tag == 'base' else 'extra'] + need(dict(paid) == {int(k): v for k, v in prov['actual_paid_profile'].items()}, 'provider profile') + need(dict(inv) == CLAIMED['inventory'] and dict(inv) == {int(k): v for k, v in W['report']['width_inventory'].items()}, 'inventory %s' % dict(inv)) + need(len(live[tag]) == CLAIMED['helpers'], 'helper count') + need(widths[tag] == {r: dim(end[r]) - dim(start[r]) for r in live[tag]}, 'widths') + profiles[tag] = dict(paid) + need([widths[tag][r] for r in live[tag]] == prov['widths'], 'provider widths differ from word-derived widths') + news = {op: dict(U_dim=dim(ws[op]['U']), U_is_propagated=ws[op]['cur_before'] == ws[op]['U']) for op in (30, 31) + tuple(range(66, 73))} + # frames() runs warp_algebra and the propagated-frame equality on every prelude warp item as well + npw = sum(1 for e in W['A'][:W['prelude_events']] if e[0] == 'warp') + return dict(profile=dict(sorted(paid.items())), mass=sum(k * v for k, v in paid.items()), inventory=dict(sorted(inv.items())), + helpers=len(live[tag]), warps_checked=len(ws), prelude_warp_items_checked=npw, new_or_moved=news) + rule('S3S4-FRAMES-PROFILE-%s' % tag, s3s4) + rule('S3-REFIT-EXACT-%s' % tag, lambda: refit_exactness(W, set(liveW), decl)) + rule('S3-ABOVE-FLOOR-NEUTRAL-%s' % tag, lambda: above_floor_neutral(W, set(liveW), decl)) + + def s4b(): + prof, inv = frames_rref(W, sorted(liveW)) + need(prof == CLAIMED['local_profile'], 'rref profile %s' % prof) + need(inv == CLAIMED['inventory'], 'rref inventory %s' % inv) + profP, invP = frames_rref(P, sorted(liveP)) + need(profP == {int(k): v for k, v in P['report']['local_profile'].items()}, 'rref parent profile %s' % profP) + return dict(profile=prof, inventory=inv, parent_profile=profP) + rule('S4-FRAMES-RREF-%s' % tag, s4b) + + def chain(): + rep, states = stage_chain(P, W, decl) + r5[tag] = states['refit5c'] + return rep + rule('S1-STAGE-CHAIN-%s' % tag, chain) + + def s2(): + cl, restored = check_cleanup(W, ev) + n1 = replay(W, set(liveW), ev, cl, restored, False) + n2 = replay(W, set(liveW), ev, cl, restored, True) + return dict(live_inputs=len(liveW), restored=len(restored), cleanup=len(cl), words_fwd=n1, words_dual=n2) + rule('S2-REPLAY-FREE-%s' % tag, s2) + + def s2b(): + cl, restored = derive_cleanup(W, ev) + for seed in (1, 2): + realise(W, set(liveW), ev, cl, restored, False, seed) + realise(W, set(liveW), ev, cl, restored, True, seed) + return 'forward+dual, 2 seeds, 4x4 over GF(2^61-1)' + rule('S2-REPLAY-MATRIX-%s' % tag, s2b) + words[tag] = W + + def parent_positive(): + out = {} + pprof = {} + for tag in ('base', 'extra'): + P = js['P_' + tag] + liveP = [r for r in range(NSPACE) if r not in set(P['removed'])] + evP = program(P) + paid, inv, start, end, ws = frames(P, set(liveP), evP) + prov = js['PROV51']['gauge44' if tag == 'base' else 'extra'] + need(dict(paid) == {int(k): v for k, v in P['report']['local_profile'].items()} == + {int(k): v for k, v in prov['actual_paid_profile'].items()}, 'parent profile') + need(dict(inv) == {int(k): v for k, v in P['report']['width_inventory'].items()}, 'parent inventory') + need([widths['P_' + tag][r] for r in live['P_' + tag]] == prov['widths'], 'parent widths') + cl, restored = check_cleanup(P, evP) + replay(P, set(liveP), evP, cl, restored, False) + replay(P, set(liveP), evP, cl, restored, True) + pprof[tag] = dict(paid) + out[tag] = dict(profile=dict(sorted(paid.items())), helpers=len(live['P_' + tag])) + fill = s5_fill(js, None, {'base': live['P_base'], 'extra': live['P_extra']}, + {'base': widths['P_base'], 'extra': widths['P_extra']}, fill_key='FILL51') + prof = Counter({int(k): v for k, v in fill['idle'].items()}) + for pid, n in fill['dispatch'].items(): + for k, v in pprof['base' if pid == 'gauge44' else 'extra'].items(): + prof[k] += n * v + need(dict(prof) == {int(k): v for k, v in js['K2751']['profile'].items()}, 'parent complete profile') + out['fill'] = dict(R=fill['R'], roles=fill['roles'], idle=fill['idle']) + return out + rule('POSITIVE-PARENT-2751', parent_positive) + rule('S5-FILL-WORD-DERIVED-R', lambda: s5_fill(js, words, {t: live[t] for t in ('base', 'extra')}, widths)) + rule('S5-FILL-TRANSFORM', lambda: fill_transform(js, live['P_base'], live['base'])) + + def s6(): + need('base' in profiles and 'extra' in profiles, 'word profiles unavailable (S3S4 failed)') + fill = s5_fill(js, words, {t: live[t] for t in ('base', 'extra')}, widths) + prof = Counter({int(k): v for k, v in fill['idle'].items()}) + disp = fill['dispatch'] + for pid, n in disp.items(): + tag = 'base' if pid == 'gauge44' else 'extra' + for k, v in profiles[tag].items(): + prof[k] += n * v + need(dict(prof) == CLAIMED['complete_profile'], 'complete profile %s' % dict(sorted(prof.items()))) + need(dict(prof) == {int(k): v for k, v in js['CLAIM']['profile'].items()}, 'CLAIM profile') + mass = sum(k * v for k, v in prof.items()) + need(mass == CLAIMED['mass'] == 73 * js['PLAN']['live'] * 2 - js['PLAN']['deficit'] * 2, 'mass') + C = Fraction(CLAIMED['C']) + need(Fraction(js['CLAIM']['complex_lower']) == C, 'claimed C') + ok, vals = root_bracket(dict(prof), Decimal(66304), C, C + Fraction(1, 10 ** 24)) + need(ok, 'root not in [C, C+1e-24]: %s' % (vals,)) + ok2, _ = root_bracket(dict(prof), Decimal(66304), C + Fraction(1, 10 ** 24), C + Fraction(2, 10 ** 24)) + need(not ok2, 'bracket test vacuous') + K = C - Fraction(1, 10 ** 46) - Fraction(1, 10 ** 70) + need(Fraction(js['CLAIM']['kappa']) == K, 'kappa = C - 1e-46 - 1e-70') + m51 = K - Fraction(js['K2751']['kappa']) + m66 = K - Fraction(js['K2766']['kappa']) + m67 = K - Fraction(js['K2767']['kappa']) + need(m51 == Fraction(CLAIMED['margin_2751']) and m66 == Fraction(CLAIMED['margin_2766']) and m67 > 0, 'margins') + return dict(mass=mass, root_in=[str(C), str(C + Fraction(1, 10 ** 24))], f_values=vals, + margin_2751=str(m51), margin_2766=str(m66), margin_2767=dec(m67, 40)) + rule('S6-PROFILE-MASS-ROOT', s6) + + def attribution(): + """retired5 (its words and fill are not published; #2802 records its endpoint, fill hash and local profile in + evidence/retired5/) reconstructed independently: the refit5c state of both words, and PR2751's fill minus the five + retired5 followers, re-tiled in old in-bin order. Its complete profile must bracket the recorded retired5 root, + and the reconstruction must equal #2802's recorded retired5 fill (hash) and local profile.""" + need('base' in r5 and 'extra' in r5, 'retired5 states unavailable (stage chain failed)') + C5 = Fraction('0.001717409316335491643448') + need(Fraction(js['CLAIM']['local_predecessor']['exact_kappa']) == C5 - Fraction(1, 10 ** 46) - Fraction(1, 10 ** 70), 'retired5 claim') + need(Fraction(js['R5_ADMISSION']['complex_lower']) == C5, 'recorded retired5 endpoint') + prof5, live5, wid5 = {}, {}, {} + for tag in ('base', 'extra'): + w5 = r5[tag] + l5 = [r for r in range(NSPACE) if r not in set(w5['removed'])] + prof5[tag] = dict(frames(w5, set(l5), program(w5))[0]) + need(prof5[tag] == {int(k): v for k, v in js['R5_HOOK']['words'][tag]['local_profile'].items()}, 'recorded retired5 local profile (%s)' % tag) + live5[tag] = [r for r in l5 if r >= 2 * V] + wid5[tag] = static_widths(w5, live5[tag]) + gone = set(live['P_base']) - set(live5['base']) + need(sorted(gone) == [606, 635, 637, 638, 639], 'retired5 removed set') + newidx = {r: i for i, r in enumerate(live5['base'])} + order = js['ORDER'] + disp = {(a, b): p for a, b, p in js['DISPATCH']} + bins = defaultdict(list) + for t, h, o, c, p, off in js['FILL51']['rows']: + r = live['P_base'][h] + if r not in gone: + bins[(o, c, p)].append((off, t, newidx[r])) + rows = [] + for (o, c, p), lst in bins.items(): + pos = 0 + for off, t, h in sorted(lst): + rows.append([t, h, o, c, p, pos]) + pos += wid5['base' if disp[tuple(order[t])] == 'gauge44' else 'extra'][live5['base'][h]] + rows.sort(key=lambda x: (x[0], x[1])) + js5 = dict(js) + js5['FILL5'] = dict(js['FILL51'], rows=rows) + fill = s5_fill(js5, None, live5, wid5, fill_key='FILL5') + # #2802 hashes the gzip bytes of its fills; the serializer below reproduces its pinned FILL.json.gz bytes exactly + # (checked first). The canonical-JSON hash of the reconstruction is pinned too, for zlib builds whose deflate + # output differs (then the gzip comparison is reported as not applicable). + ser = lambda d: json.dumps(d, sort_keys=True, separators=(',', ':')).encode() + gz = lambda d: gzip.compress(ser(d), compresslevel=9, mtime=0) + serializer_ok = hashlib.sha256(gz(js['FILL'])).hexdigest() == PINS['FILL'][2] + json_sha = hashlib.sha256(ser(js5['FILL5'])).hexdigest() + need(json_sha == RETIRED5_FILL_JSON_SHA, 'reconstructed retired5 fill JSON %s' % json_sha) + if serializer_ok: + need(hashlib.sha256(gz(js5['FILL5'])).hexdigest() == js['R5_ADMISSION']['fill_sha256'], "reconstructed retired5 fill differs from #2802's recorded fill_sha256") + prof = Counter({int(k): v for k, v in fill['idle'].items()}) + for pid, n in fill['dispatch'].items(): + for k, v in prof5['base' if pid == 'gauge44' else 'extra'].items(): + prof[k] += n * v + ok, vals = root_bracket(dict(prof), Decimal(66304), C5, C5 + Fraction(1, 10 ** 24)) + need(ok, 'retired5 root not in [C5, C5+1e-24]') + ok2, _ = root_bracket(dict(prof), Decimal(66304), C5 + Fraction(1, 10 ** 24), C5 + Fraction(2, 10 ** 24)) + need(not ok2, 'retired5 bracket test vacuous') + C = Fraction(CLAIMED['C']) + C66 = Fraction(js['K2766']['complex_lower']) + return dict(retired5_profile=prof5['base'], retired5_idle=fill['idle'], retired5_complete=dict(sorted(prof.items())), + retired5_root_in=[str(C5), str(C5 + Fraction(1, 10 ** 24))], root_margins=vals[2], + recorded_endpoint_profile_equal=True, + fill_gzip_sha256_equals_recorded=(True if serializer_ok else 'not applicable: this zlib does not reproduce the pinned FILL bytes'), + fill_json_sha256=json_sha, + gain_retired5_over_2766=dec(C5 - C66, 30), gain_retired7_stages_over_retired5=str(C - C5)) + rule('ATTRIBUTION-RETIRED5', attribution) + + def attribution_2766(): + """PR #2766's own pinned words differ from W2751 only in the frame of B1151, which equals #2802's refit5c frame there; + their recount equals PR #2766's reported local profile, and with PR #2751's fill they give PR #2766's claimed complete + profile and root. The other 19 refit5c frames that #2802's README lists with PR #2766's refit (A0-A11, + B771/773/776/778/783/788, restore60) are not in PR #2766's word. They are cost-neutral: applied alone to W2751, or + reverted to W2751's frames in the final word, the frame chain stays legal and the local profile is unchanged.""" + need(js['K2766_own'] == js['K2766'], "#2802's copy of PR2766's claim differs from PR2766's own") + b1151 = ('B', 1151) + others = [('A', i) for i in range(12)] + [('B', i) for i in (771, 773, 776, 778, 783, 788)] + [('restore', 60)] + out = {} + profs = {} + for tag in ('base', 'extra'): + P, W, W66 = js['P_' + tag], js['W_' + tag], js['W66_' + tag] + need(set(W66) == set(P), 'PR2766 word keys') + diff_fields = sorted(k for k in P if P[k] != W66[k]) + need(diff_fields == ['B', 'report'], 'PR2766 word differs from W2751 in %s' % diff_fields) + need(len(P['B']) == len(W66['B']), 'PR2766 B length') + fdiff = [i for i, (a, b) in enumerate(zip(P['B'], W66['B'])) if a != b] + need(fdiff == [1151] and P['B'][1151][:-1] == W66['B'][1151][:-1], 'PR2766 word changes B gates %s' % fdiff[:5]) + need({k: v for k, v in P['report'].items() if k != 'local_profile'} == {k: v for k, v in W66['report'].items() if k != 'local_profile'}, + 'PR2766 report differs beyond local_profile') + frm = {(sec, i): F for sec, i, F in js['ST_refit5c_' + tag]['frames']} + need(all(k in frm for k in others + [b1151]), 'credited frames not all in refit5c') + need(sub(frm[b1151]) == sub(W66['B'][1151][-1]), "#2802's B1151 frame differs from PR2766's") + l66 = [r for r in range(NSPACE) if r not in set(W66['removed'])] + paid66 = dict(frames(W66, set(l66), program(W66))[0]) + need(paid66 == {int(k): v for k, v in W66['report']['local_profile'].items()}, 'PR2766 word profile differs from its report') + base = {int(k): v for k, v in P['report']['local_profile'].items()} + delta = {k: paid66.get(k, 0) - base.get(k, 0) for k in set(paid66) | set(base) if paid66.get(k, 0) != base.get(k, 0)} + need(delta == {1: -2, 2: 1}, 'PR2766 delta %s' % delta) + + def prof_of(w): + lw = [r for r in range(NSPACE) if r not in set(w['removed'])] + return dict(frames(w, set(lw), program(w))[0]) + on_parent = apply_stage(P, 'refit-others', dict(frames=[[k[0], k[1], frm[k]] for k in others], local_profile=P['report']['local_profile'])) + need(prof_of(on_parent) == base, 'the 19 frames change the W2751 profile') + all20 = apply_stage(P, 'refit-all20', dict(frames=[[k[0], k[1], frm[k]] for k in others + [b1151]], local_profile=P['report']['local_profile'])) + need(prof_of(all20) == paid66, 'the 20 frames together differ from PR2766 alone') + reverted = apply_stage(W, 'refit-revert', dict(frames=[[k[0], k[1], P[k[0]][k[1]][-1]] for k in others], local_profile=W['report']['local_profile'])) + need(prof_of(reverted) == CLAIMED['local_profile'], 'reverting the 19 frames changes the final profile') + profs[tag] = paid66 + out[tag] = dict(pr2766_word_change='B1151 dim %d -> %d' % (dim(sub(P['B'][1151][-1])), dim(sub(W66['B'][1151][-1]))), + pr2766_local_profile=dict(sorted(paid66.items())), delta=dict(sorted(delta.items())), + other_19_frames='cost-neutral on W2751 and on the final word') + fill = s5_fill(js, None, {'base': live['P_base'], 'extra': live['P_extra']}, + {'base': widths['P_base'], 'extra': widths['P_extra']}, fill_key='FILL51') + prof = Counter({int(k): v for k, v in fill['idle'].items()}) + for pid, n in fill['dispatch'].items(): + for k, v in profs['base' if pid == 'gauge44' else 'extra'].items(): + prof[k] += n * v + claimed = {int(k): v for k, v in js['K2766']['profile'].items()} + need(dict(prof) == claimed, 'PR2766 complete profile %s' % dict(sorted(prof.items()))) + out['complete_profile_equals_PR2766_claim'] = True + C66 = Fraction(js['K2766']['complex_lower']) + ok, vals = root_bracket(dict(prof), Decimal(66304), C66, C66 + Fraction(1, 10 ** 24)) + need(ok, 'PR2766 root not in [C, C+1e-24]') + out['PR2766_root_in'] = [str(C66), str(C66 + Fraction(1, 10 ** 24))] + out['root_margins'] = vals[2] + return out + rule('ATTRIBUTION-PR2766-WORD', attribution_2766) + + def x2818(): + need(js['X_W_base'] == js['W_base'] and js['X_W_extra'] == js['W_extra'], 'words differ') + need(js['X_FILL'] == js['FILL'] and js['X_ORDER'] == js['ORDER'] and js['X_PROV'] == js['PROV'], 'fill/order/providers differ') + d1 = {(s, r): p for s, r, p in js['DISPATCH']} + dx = js['X_DISPATCH'] + if isinstance(dx, dict): + d2 = {tuple(map(int, k.split(','))): v for k, v in dx.items()} + else: + d2 = {(s, r): p for s, r, p in dx} + need(d1 == d2, 'dispatch differs') + out = {} + for tag in ('base', 'extra'): + pt = js['X_R7_' + tag] + W = js['W_' + tag] + for k, v in pt['fields'].items(): + need(W[k] == v, '#2818 retired7 field %s differs from #2802 final word' % k) + need(pt['report'] == W['report'], 'report differs') + out[tag] = sorted(pt['fields']) + return dict(words='identical', fill='identical', order='identical', providers='identical', dispatch='same map', patch_fields=out) + rule('X-2818-SAME-CONSTRUCTION', x2818) + res['ok'] = all(v['ok'] for v in res['rules'].values()) + return res + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--repo', default=os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))) + ap.add_argument('--blob-dir') + ap.add_argument('--out') + ap.add_argument('--fetch', action='store_true') + a = ap.parse_args() + if a.fetch and not a.blob_dir: + fetch_missing(a.repo) + js = load_all(a.repo, a.blob_dir) + res = run_all(js) + if a.out: + with open(a.out, 'w') as fh: + json.dump(res, fh, indent=1, sort_keys=True, default=str) + print("PASS_T74_RETIRED7_INCREMENT_RULES" if res["ok"] else "FAIL_T74_RETIRED7_INCREMENT_RULES") + return 0 if res['ok'] else 1 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/research/t74-retired7-increment-audit/increment_controls.py b/research/t74-retired7-increment-audit/increment_controls.py new file mode 100644 index 0000000000..8015045e73 --- /dev/null +++ b/research/t74-retired7-increment-audit/increment_controls.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Negative controls for increment_audit.py: each mutant of the pinned inputs must be rejected by its named rule. + +Word mutants carry an inverse-reverse cleanup re-derived from their own forward program, so a stale cleanup is never +the reason for a rejection. Some controls also state which rules must ACCEPT the mutant ('must_accept') or the exact +set of rules that reject it ('exact_failing'). These expectations make the occupancy observations machine-checked: a +lender's dead write (after the lender's last read) moved past its alias warp is invisible to both scalar replays, and at +frame FULL also to the frame chain, the recount, the refits, the stage records, the fill and the price (C4d/C4e); a moved +lender read (C4f) or a moved write that precedes the lender's last read (C4g) is rejected by both replays and accepted by +the frame chain, fill and price. A control counts only if every expectation holds and no rule crashed. + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import copy +import json +import os +import sys + +sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) +import increment_audit as A # noqa: E402 + +FULLL = [256, 128, 64, 32, 16, 8, 4, 2, 1] +# rules re-run on every mutant: all except the parent positive control, the stage-chain and attribution rules and the +# above-floor neutrality rule, which rebuild, reprice or vary unmutated inputs (they run once on the pinned inputs) +SKIP = ('POSITIVE-PARENT', 'S1-STAGE-CHAIN', 'ATTRIBUTION', 'S3-ABOVE-FLOOR') +REPLAYS = ('S2-REPLAY-FREE-%s', 'S2-REPLAY-MATRIX-%s') +# every per-word rule on the pricing path: replays, frame chain, second recount, refits, stage records +PRICED = REPLAYS + ('S3S4-FRAMES-PROFILE-%s', 'S4-FRAMES-RREF-%s', 'S3-REFIT-EXACT-%s', 'S1-STAGE-RECORDS-%s') +# and the global ones: fill with word-derived R, fill transform, complete profile, mass and root +PRICED_GLOBAL = ('S5-FILL-WORD-DERIVED-R', 'S5-FILL-TRANSFORM', 'S6-PROFILE-MASS-ROOT') + + +def rederive(w): + ev = A.program(w) + der, _ = A.derive_cleanup(w, ev) + w['cleanup'] = [list(x) + [FULLL] for x in der] + return w + + +def relabel_B(w, start, a, b, stop=None): + for i in range(start, len(w['B']) if stop is None else stop): + e = w['B'][i] + if e[0] == 'add': + if e[1] == a: + e[1] = b + if e[2] == a: + e[2] = b + elif e[1] == a: + e[1] = b + + +def last_A(w, r, role): + """index of register r's last A event in role 'write' (r is the written register), 'read' (r is an add's source) or + 'prewrite' (the last write to r that precedes r's last read, i.e. a write whose value is still read in A)""" + def ok(e, rl): + if e[0] == 'warp': + return False + if rl == 'write': + return e[1] == r + return e[0] == 'add' and e[2] == r + if role == 'prewrite': + lr = last_A(w, r, 'read') + return max(i for i, e in enumerate(w['A']) if i < lr and ok(e, 'write')) + return max(i for i, e in enumerate(w['A']) if ok(e, role)) + + +def mutants(js): + st = {s: js['ST_%s_base' % s] for s in A.STAGES} + out = [] + + def word(name, expect, f, tag='base', must_accept=(), exact_failing=None): + w = copy.deepcopy(js['W_' + tag]) + f(w) + rederive(w) + m = dict(js) + m['W_' + tag] = w + out.append((name, expect, m, dict(must_accept=list(must_accept), exact_failing=exact_failing))) + + # C1 refit7 undone (B911 back to its previous dim-6 frame) + prev = {(s, i): F for s, i, F in st['refit7']['previous_frames']} + word('C1 refit7 B911 undone', 'S3S4-FRAMES-PROFILE-base', lambda w: w['B'][911].__setitem__(-1, prev[('B', 911)])) + + # C2 hostee move of warp 30 reverted: record back to 401 at 941 and the hostee's gates back on 401 + def c2(w): + mv = st['hostmove2']['moves'][0] + w['warps'][29] = copy.deepcopy(mv['old_record']) + relabel_B(w, mv['old_pos'], 564, 401) + word('C2 hostee move 401->564 reverted (401 then hosts follower 667 and hostee 30 at once)', 'OCC-TIMELINE-base', c2) + + # C3 early alias warp for a B-retired lender: warp 66 (606<-550) placed before 550's last gate B901 + word('C3 alias warp 66 moved before lender 550 last gate (B901)', 'OCC-TIMELINE-base', lambda w: w['warps'][65].__setitem__(0, 901)) + + # C4a-C4g: an A-retired lender's A event moved past its alias warp. Lender 401 (alias warp 71 at B259) on the + # base word; lender 403 (alias warp 72 at B262) on the extra word. + def into_B(r, pos): + def f(w): + g = w['A'].pop(last_A(w, r, 'write')) + w['B'].insert(pos, g) + for rec in w['warps']: + if rec[0] > pos: + rec[0] += 1 + return f + + def to_restore(r, role, full): + def f(w): + g = w['A'].pop(last_A(w, r, role)) + if full: + g = list(g[:-1]) + [FULLL] + w['restore'].append(g) + return f + word('C4a lender 401: last A write (A3175) moved into B right after alias warp 71, own frame', 'S3S4-FRAMES-PROFILE-base', + into_B(401, 259), must_accept=[x % 'base' for x in REPLAYS]) + word('C4b lender 401: last A write moved to the end of restore, own frame', 'OCC-TIMELINE-base', + to_restore(401, 'write', False), must_accept=[x % 'base' for x in REPLAYS]) + word('C4c lender 403 (extra word): last A write (A3174) moved into B right after alias warp 72, own frame', + 'S3S4-FRAMES-PROFILE-extra', into_B(403, 262), tag='extra', must_accept=[x % 'extra' for x in REPLAYS]) + word('C4d lender 401: last A write moved to the end of restore at frame FULL', 'OCC-TIMELINE-base', + to_restore(401, 'write', True), must_accept=[x % 'base' for x in PRICED] + list(PRICED_GLOBAL), + exact_failing=['OCC-TIMELINE-base', 'S1-DIFF-base', 'X-2818-SAME-CONSTRUCTION']) + word('C4e lender 403 (extra word): last A write moved to the end of restore at frame FULL', 'OCC-TIMELINE-extra', + to_restore(403, 'write', True), tag='extra', must_accept=[x % 'extra' for x in PRICED] + list(PRICED_GLOBAL), + exact_failing=['OCC-TIMELINE-extra', 'S1-DIFF-extra', 'X-2818-SAME-CONSTRUCTION']) + # C4f/C4g change what is computed: both replays reject them, while the frame chain, recount, refits, stage records, + # fill and price accept them (they price the moved gate at FULL exactly as C4d does) + computed = [x % 'base' for x in PRICED if x not in REPLAYS] + list(PRICED_GLOBAL) + changed = ['S2-REPLAY-FREE-base', 'S2-REPLAY-MATRIX-base', 'OCC-TIMELINE-base', 'S1-DIFF-base', 'X-2818-SAME-CONSTRUCTION'] + word('C4f lender 401: last A read (an add with source 401) moved to the end of restore at frame FULL', 'S2-REPLAY-FREE-base', + to_restore(401, 'read', True), must_accept=computed, exact_failing=changed) + word('C4g lender 401: last A write before its last read (A3158) moved to the end of restore at frame FULL', + 'S2-REPLAY-MATRIX-base', to_restore(401, 'prewrite', True), must_accept=computed, exact_failing=changed) + + # C5 alias warp after the follower's first gate (the replacement control of #2802), A-retired lender 401 + word('C5 alias warp 71 after follower 667 first gate (B260)', 'OCC-TIMELINE-base', lambda w: w['warps'][70].__setitem__(0, 260)) + + # C6 wrong G on alias warp 71 + def c6(w): + g = w['warps'][70][2] + g[0] ^= g[1] + word('C6 wrong G on warp 71', 'S3S4-FRAMES-PROFILE-base', c6) + + # C7 U is not the lender's propagated frame: consistent pair (U', G(U')) with a different U' + def c7(w): + rec = w['warps'][70] + U2 = [1, 2, 4, 8] + rec[3] = U2 + rec[4] = [A.gapply(rec[2], u) for u in U2] + word("C7 warp 71 with G(U')=E' for a U' that is not 401's propagated frame", 'S3S4-FRAMES-PROFILE-base', c7) + + # C8 keep removed follower 667 (both words): the word-derived R becomes 409 while the providers still say 408 + m = dict(js) + for tag in ('base', 'extra'): + w = copy.deepcopy(js['W_' + tag]) + w['removed'] = [h for h in w['removed'] if h != 667] + m['W_' + tag] = rederive(w) + out.append(('C8 removed follower 667 kept as a live helper (R self-reference)', 'S5-FILL-WORD-DERIVED-R', m, {})) + + # C9 swap the two alias lenders of warps 71/72 (declaration conformance: each alias warp sits on its declared lender) + def c9(w): + w['warps'][70][1], w['warps'][71][1] = w['warps'][71][1], w['warps'][70][1] + word('C9 alias lenders of warps 71/72 swapped (declaration conformance)', 'OCC-TIMELINE-base', c9) + + # C10 drop one restore read + word('C10 first restore gate dropped', 'S2-REPLAY-FREE-base', lambda w: w['restore'].pop(0)) + + # C11 R + 1 in the fill: one extra helper index per call + m = dict(js) + f = copy.deepcopy(js['FILL']) + extra = [[t, 408, o, c, p, off] for (t, h, o, c, p, off) in f['rows'] if h == 407] + f['rows'] = f['rows'] + extra + m['FILL'] = f + out.append(('C11 fill inflated to R+1 helper indices', 'S5-FILL-WORD-DERIVED-R', m, {})) + + # C12 one hostee gate left on the old lender 401 + def c12(w): + i = next(i for i in range(941, len(w['B'])) if 564 in A.regs(w['B'][i])) + relabel_B(w, i, 564, 401, stop=i + 1) + word('C12 first hostee gate of warp 30 left on old lender 401', 'S1-DIFF-base', c12) + + # C13 undeclared frame change on a gate outside every refit list + def c13(w): + declared = {(s, i) for x in ('refit5', 'refit5c', 'refit7', 'refit7c') for s, i, _ in st[x]['frames']} + i = next(i for i in range(1500, len(w['B'])) if ('B', i) not in declared and w['B'][i][0] == 'add' and len(w['B'][i][-1]) < 9) + w['B'][i][-1] = FULLL + word('C13 undeclared frame raise on a B gate', 'S1-DIFF-base', c13) + + # C14 #2818 copy of the base word altered by one coefficient + m = dict(js) + x = copy.deepcopy(js['X_W_base']) + x['B'][0][3] = -x['B'][0][3] + m['X_W_base'] = x + out.append(('C14 #2818 base word differs by one sign', 'X-2818-SAME-CONSTRUCTION', m, {})) + return out + + +def run(js, log=print): + res = {} + ok = True + for name, expect, m, exp in mutants(js): + r = A.run_all(m, log=lambda s: None, skip=SKIP) + failing = sorted(k for k, v in r['rules'].items() if not v['ok']) + crashed = sorted(k for k, v in r['rules'].items() if not v['ok'] and str(v['info']).startswith('ERROR')) + good = expect in failing and not str(r['rules'][expect]['info']).startswith('ERROR') + acc = list(exp.get('must_accept', ())) + acc_ok = all(k in r['rules'] and r['rules'][k]['ok'] for k in acc) + exact = exp.get('exact_failing') + exact_ok = exact is None or failing == sorted(exact) + this = good and acc_ok and exact_ok and not crashed + ok &= this + entry = dict(expected_rule=expect, rejected_by_expected_rule=good, failing_rules=failing, + expected_rule_message=r['rules'][expect]['info'] if expect in r['rules'] else None, + crashed_rules=crashed, control_ok=this) + if acc: + entry.update(must_accept=acc, accepted_as_expected=acc_ok) + if exact is not None: + entry.update(exact_failing=sorted(exact), exact_failing_ok=exact_ok) + res[name] = entry + log('%s %-80s expected %-28s failing=%s' % ('REJECTED' if this else 'CONTROL-FAILURE', name[:80], expect, ','.join(failing))) + return ok, res + + +if __name__ == '__main__': + repo = sys.argv[1] + js = A.load_all(repo, None) + ok, res = run(js) + if len(sys.argv) > 2: + with open(sys.argv[2], 'w') as fh: + json.dump(res, fh, indent=1, sort_keys=True, default=str) + print('ALL_CONTROLS_REJECTED' if ok else 'CONTROL_FAILURE') + sys.exit(0 if ok else 1) diff --git a/research/t74-retired7-increment-audit/verify.py b/research/t74-retired7-increment-audit/verify.py new file mode 100644 index 0000000000..4f20454da7 --- /dev/null +++ b/research/t74-retired7-increment-audit/verify.py @@ -0,0 +1,76 @@ +#!/usr/bin/env python3 +"""Entry point: independent audit of PR #2802's seven-stage increment over PR #2751 (retired5 + retired7 stages), +verdict extended to PR #2818. + +Runs the 28 named rules of increment_audit.py on the pinned inputs, then the 20 negative controls of +increment_controls.py (each must be rejected by its named rule, and some must also be accepted by named rules). +Inputs are git blobs at the pinned PR heads, checked against sha256 pins; --fetch downloads refs/pull//head only +for absent commits (FETCH_HEAD only). An unreadable or mismatching input prints a FAIL line (exit 1). + +Usage (repository root): python3 -I -B research/t74-retired7-increment-audit/verify.py --fetch [--out RECEIPT.json] +Final line: PASS_T74_RETIRED7_INCREMENT_AUDIT rules=28/28 controls=20/20 ... or FAIL_T74_RETIRED7_INCREMENT_AUDIT ... +If this zlib does not reproduce #2802's pinned FILL.json.gz bytes, ATTRIBUTION-RETIRED5 compares the reconstructed +retired5 fill only through its pinned canonical-JSON sha256 (not with #2802's recorded gzip hash) and a NOTE line says so. + +Prepared by thakrarsagar with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import argparse +import json +import os +import sys +import time + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +sys.dont_write_bytecode = True +import increment_audit as A # noqa: E402 +import increment_controls as K # noqa: E402 + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--repo', default=os.path.dirname(os.path.dirname(HERE))) + ap.add_argument('--blob-dir', help='exported blobs laid out as DIR//') + ap.add_argument('--fetch', action='store_true', help='fetch the pinned PR heads if absent (writes FETCH_HEAD only)') + ap.add_argument('--out', help='write the deterministic receipt here') + a = ap.parse_args() + t0 = time.monotonic() + if a.fetch and not a.blob_dir: + A.fetch_missing(a.repo) + try: + js = A.load_all(a.repo, a.blob_dir) + except (A.Fail, OSError, ValueError) as e: + print('FAIL_T74_RETIRED7_INCREMENT_AUDIT inputs: %s' % e) + return 1 + res = A.run_all(js) + r5 = res['rules'].get('ATTRIBUTION-RETIRED5', {}) + if r5.get('ok') and r5['info'].get('fill_gzip_sha256_equals_recorded') is not True: + print("NOTE: this zlib does not reproduce #2802's FILL.json.gz bytes; the retired5 fill was compared through its " + "pinned canonical-JSON sha256 only, not with #2802's recorded gzip fill_sha256") + ok_c, ctl = K.run(js) + n_rules = len(res['rules']) + n_pass = sum(1 for v in res['rules'].values() if v['ok']) + n_ctl = sum(1 for v in ctl.values() if v['control_ok']) + receipt = dict( + status='PASS' if (res['ok'] and ok_c) else 'FAIL', + commits=A.COMMIT, pins={k: dict(commit=A.COMMIT[v[0]], path=v[1], sha256=v[2]) for k, v in sorted(A.PINS.items())}, + claims_under_test=A.CLAIMED, rules=res['rules'], controls=ctl, + scope=('Finite exact checks of the PR #2802 seven-stage increment (retired5 stages refit5/alias5/refit5c, retired7 ' + 'stages refit7/hostmove2/alias7/refit7c) over the pinned PR #2751 words: event diff, per-register occupancy, ' + 'warps/frames/profile, free-algebra and matrix replays, the 271728-role fill with word-derived R, complete ' + 'profile/mass/root, PR #2818 identity, and attribution against PR #2766 and the recorded retired5 step. ' + 'Inherited T74/#1319 admission, native lowering, outer proof and PR #2751 recovery are not checked.')) + if a.out: + with open(a.out, 'w') as fh: + json.dump(receipt, fh, indent=1, sort_keys=True, default=str) + fh.write('\n') + line = '%s rules=%d/%d controls=%d/%d commit2802=%s commit2818=%s' % ( + 'PASS_T74_RETIRED7_INCREMENT_AUDIT' if receipt['status'] == 'PASS' else 'FAIL_T74_RETIRED7_INCREMENT_AUDIT', + n_pass, n_rules, n_ctl, len(ctl), A.COMMIT['c2802'][:12], A.COMMIT['c2818'][:12]) + print('elapsed %.0fs' % (time.monotonic() - t0)) + print(line) + return 0 if receipt['status'] == 'PASS' else 1 + + +if __name__ == '__main__': + sys.exit(main())