diff --git a/research/r437-composed-bit-independent-audit/README.md b/research/r437-composed-bit-independent-audit/README.md new file mode 100644 index 0000000000..b9c9743a6c --- /dev/null +++ b/research/r437-composed-bit-independent-audit/README.md @@ -0,0 +1,485 @@ +# Independent audit of PR #3647's composed R437 bit word, hosting and price + +PR #3647 composes two helper deletions on the selected #589 bit word. The +helper464 deletion re-synthesizes one D4 node with a ten-gate GL block. The +helper470 deletion comes from #1043 and replaces a carrier with a late read of +SOURCE77. This package checks the resulting 659-input R437 word, its local-call +records, its hosted template and its price. The interpreter, controls and +price engine are written separately for this audit, and the word is checked +against both single-change controls. **At head `36ff4414` every check +passes**: + +- **Word.** Over F2 the word maps every input `(x, y, h)` to `(x, y + x, h)`. + Here `x` is the 111 SOURCEs, `y` the 111 targets and `h` the 437 helpers + with arbitrary dirty contents. The two edits compose with no interaction + beyond the single-change controls. The SOURCE77 read at frame 186 is in + chronological order, and the literal word gives the claimed local profile. +- **One item to confirm at intake (likely neutral).** In selected #589 all + nine captured retained totals already carry arbitrary helper dirt at the + COPY, 42 to 66 helper columns each. Two of them, h477 and h478, carried the + deleted h464's column. E464 (the helper464 GL edit) replaces it with + h340's, so they keep 46 and 43 dirt columns and their clean rows. E470 + likewise drops h470's column from h475. The edit therefore changes which + dirty helper feeds two already-dirty captures; it adds no new kind of + capture. PR #3647 does not mention the swap. The record replay checks the + COPY/ERASE discipline over every dirt column. Whether the inherited capture + contract depends on which helpers' dirt reaches a total is not checked here + ([Open question 1](#open-next-questions)). If the discard is linear in + arbitrary helper contents, as PR #3647 states, the item closes. +- **Records and hosting.** The PR's 27,132-record stream is byte-identical to + an independent lowering of the word. The hosted template's 125,856 helper + placements satisfy the selected chain's idle-hosting rule, and all 288 calls + are bound to the audited local programs. +- **Price.** The whole paid profile and the invoice's precision fields follow + from these. The price root gives + **c = 868314126713557740143/(5·10^23) = 0.001736628253427115480286**, and the + next 10^-24 grid point fails. +- **Controls.** The same price engine reproduces the selected #589 value + `0.001733427039589844234749` from main-only inputs, and #1043's + `0.001734176288479865766692`. + +This is a finite, exact, **independent check of one local bit supplier**, +under the selected chain's inherited semantics: word format, hosting rule, +invoice formula and price equation. It makes no κ claim and changes no +frontier, and it does not admit PR #3647. Physical-owner, native-transport and +all-size assumptions stay as inherited (see Scope). The selected record stays +`0.001672660197076918`. The complex side binds today, and it would still bind +if the pending complex chain PR #3653/PR #3682 were admitted (see below). + +Reproduce from the repository root (standard library only, about 15 s): + +```sh +python3 -I -B research/r437-composed-bit-independent-audit/verify.py +``` + +Expected output: `PASS_INDEPENDENT_R437_WORD_AUDIT cpu `. The command +recomputes everything and requires byte equality with the committed +[RESULT.json](RESULT.json). `--write` regenerates it. + +## Why it matters, and to whom + +**This package has no near-term κ consequence.** PR #3647's c = 0.0017366283 +is the highest priced open bit-supplier value we found. This package is an +independent finite check of it, for the intake of PR #3647 and of the PRs +that build on it (#3668, #3690). It would matter for κ only after a complex +gain of about 3.0e-6 beyond the pending chain; past that point the bit +supplier caps κ. The value may not stay the highest: PR #3645's unpriced +R429 word claims local rank mass 4,989, below R437's 5,113, so a hosted and +priced R429 may exceed this c. Neither is admitted. + +The bit side does not bind today, and it would not bind if the pending complex +chain PR #3653 (rohanarun) / PR #3682 (zxv) were admitted. That chain's complex +root is C = 0.0017304188998 (PR #3653 head `607a09ff`, +`research/retimed-t488-composition/numerics/README.md`). Under either +consistent outer convention the bit side keeps about 3.0e-6 of headroom +(exact rational arithmetic, rounded here): + +| Outer convention | Complex side | Selected #589 bit side | Headroom | With PR #3647's c | +|---|---:|---:|---:|---:| +| retained transfer, κ = a/(1+a) (the selected record) | C/(1+C) = 0.0017274297 | 0.0017304275 | 2.998e-6 | 0.0017336176 (6.188e-6) | +| modern outer used by #3653: κ = C − 10^-46 − 10^-70, and the bit enters only as bit root > effective exponent | 0.0017304189 | 0.0017334270 | 3.008e-6 | 0.0017366283 (6.209e-6) | + +The modern-outer row matches the two modern-outer ledgers archived on main +(`research/half-stage-evacuation/evidence/OUTER-LEDGER.json` and +`research/rank7-t740-carrier-skips/evidence/OUTER-LEDGER.json`). In both, +κ + `actual_bit_above_effective` equals the #589 bit root 0.0017334270 +up to 10^-46. + +> **Correction.** This loop's #1166 claim for this audit compared #589's +> retained cap a/(1+a) = 0.0017304275 with #3653's modern-outer +> κ = 0.0017304189, and concluded that the bit side would bind once the chain +> was admitted. That 8.57e-9 gap mixes two conventions; the conclusion is +> withdrawn. + +**Other checks of PR #3647.** + +- The author's own verifiers. +- **PR #3668** (jwr404) checks the histogram-to-c arithmetic on the + *published* histogram. +- **PR #3690** (zxv, head `03c141ef`, opened 2026-10-18 15:26Z while this + audit was running) serves a different purpose: the ordinary coupling at + c = 1/576. Using predecessor and author code, it reconstructs the 903,456 + paid requests from the actual R437 word, owners and residual idles. It also + passes the 7,814,016 local-call events through the retained chronology + controller and reruns the author's cold verifier. It therefore overlaps this + package's paid-profile reconstruction. + +What this package adds is a reimplementation that imports nothing: the word +identity by two methods, both single-change controls, SOURCE chronology, the +record lowering, hosting legality under the selected rule, and the c bracket +with main-only positive controls, each with mutants. + +## What was audited + +- **Object.** [PR #3647](https://github.com/CrocSwap/integer-mult-bounds/pull/3647) + (ai-nanachi), head `36ff441479ff9c7e70d83f0becccd44da50effb8`, package + `research/bit-p111-r437-gl464-470-20261018`. [inputs/](inputs/) holds + vendored copies, each pinned by Git blob and SHA256 in + [SOURCES.json](SOURCES.json): + - the R437 word (`data/r0042/R437-COMPOSED-WORD.json.gz`); + - its R438 helper464-only ancestor (`data/r0028/FINAL-R438-WORD.json.gz`); + - the R437 record stream (`data/r0042/R437-RECORDS.bin`, stored gzipped); + - the hosted template (`generated/GLOBAL-TEMPLATE.json.gz`). Its canonical + content SHA256 `2e868ff4…` equals the PR's EXPECTED value. +- **Reference word.** The selected #589 word on main: + `research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz`. The PR's + `data/SELECTED589.json.gz` is byte-identical to it. +- **helper470 control.** #1043 (Ali Romman), archive-merged on main as + `research/bit-boundary-persistence/`. The control is rebuilt here from the + edit in its PROOF.md, then compared with its `FRAME-PATHS.json` and + `CERTIFICATE.json`. +- **Semantics.** All of it is taken from the selected chain on main: + - word format: `research/e8-bit-p111-tuned/code/xcheck_p.py` and + `code/pwordl.py`; + - record and event layout, parent recipe, idle ranks and prefix bound: the + nine-stage caller + `research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py`; + - invoice coefficient formula and ROW cap: + `research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py`; + - payload-prefix cap: `research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp` + and `columns_k.cpp`, as run by the selected `verify.sh`; + - idle-hosting rule: `research/e8-bit-carrier-skeleton/code/hub/idle-axis-hosting/hosting_core.py`; + - price equation: `research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py`. + + Each of these files is pinned by Git blob and SHA256 in SOURCES.json. + + **No code from PR #3647, #1043 or main is imported or run.** Each rule is + reimplemented here from its source text. + +## The two edits, in #589 numbering + +| Edit | Removed | Added | +|---|---|---| +| E464 (PR #3647 ancestry) | `A[224] = [56, h464, [x54]]`; the three-gate D4 node `A[1986..1988]` at frame 506, two of whose gates read h464 | ten gates at frame 506 on the role registers h340, h241 and h349. They read x6, x56, h233, h319, h322, h462 and h463 (18 operands) and the role registers themselves (7), 25 operands in all | +| E470 (#1043) | `A[230] = [79, h470, [x77]]` and `A[1993] = [79, h444, [h470]]` | `[186, h444, [x77]]` in place of `A[1993]` | + +In both edits the deleted helper is removed, higher ids are renumbered, D0 is +rebuilt from the raw word, and C is rebuilt as the literal reverse of every A/B +gate whose destination is a source or helper, at the full frame. + +The ten GL gates are **taken as data** from the PR's R438 word (its +`A[1985..1994]`); they are not re-synthesized here. The composition check +therefore confirms the deletions, the renumbering and the D0/C rebuild. The +node's own correctness comes from the identity check. + +## Results (all exact; numbers from RESULT.json) + +| Word | Inputs | Gates D/A/B/C | Scalar ADDs | Local profile | Mass | +|---|---:|---|---:|---|---:| +| selected #589 | 661 | 111/2075/712/2574 | 24,305 | {1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19} | 5,129 | +| #589 + E464 (= PR R438) | 660 | 111/2081/712/2580 | 24,265 | {1:1322, 2:1342, 3:78, 4:43, 5:102, 6:11, 7:19} | 5,121 | +| #589 + E470 (#1043 R438, rebuilt) | 660 | 111/2074/712/2573 | 24,248 | {1:1321, 2:1344, 3:78, 4:44, 5:102, 6:11, 7:18} | 5,121 | +| **R437 (PR #3647)** | **659** | 111/2080/712/2579 | **24,208** | **{1:1320, 2:1344, 3:77, 4:43, 5:102, 6:11, 7:18}** | **5,113** | + +### Word level + +1. **Identity, two methods.** The primary method is a forward replay. Register + `r` starts as the column bitset `1 << r`, so one pass covers every input + column over F2. Every operand makes a strictly increasing, nested climb to + the gate's frame. Dimensions and nesting are computed from the E8 line + vectors over Q. The final frames are FULL for sources and helpers and t-perp + for targets. The second method is a reverse pull-back, the transpose action + with gates in reverse order. It yields, for each input, the set of outputs + that depend on it. For all four words both methods give `(x, y + x, h)`, and + they agree on every entry of the 659 × 659 matrix (660², 661² for the + controls). The replay is symbolic on a basis and every gate is F2-linear, so + this proves the identity for all input values. It is not a sample. The + literal reverse orientation also passes: gates are reversed, and frames + descend, which is a climb of the orthogonal complement. Over F2 it is implied + by the forward check. All 636 frames are closed in the live lines + (70,596 memberships). The finite hypotheses H1–H5 of the selected + interleaved lemma and its U/J conclusions hold. D0 and C are equal to the + rebuilt ones. + - **Second frame method: exact projectors.** For each frame, the exact + rational orthogonal projector P_F is built from its lines. Its rank and + trace equal the frame dimension for all 636 frames. All 2,384 distinct + climbs A → B of R437 satisfy P_A P_B = P_B P_A = P_A. + The address-exchange identity D_(P_B−P_A) D_(P_A) = D_(P_B) is also + evaluated on the 27 changed-register transitions. It follows from the + nesting in general, so it adds no separate coverage. +2. **Composition.** Applying E464 and E470 literally to #589 and rebuilding D0 + and C gives the PR's R437 word. All fields are equal; only the `stats` + metadata differs (`extra_carriers` 10 → 8). E464 alone gives the PR's R438 + word (with the GL node taken from it, as above). E470 alone reproduces + #1043's published results: + - every frame path in its `FRAME-PATHS.json` (660 candidate and 661 baseline + paths), machine-checked; + - its local profile `{1:1321, 2:1344, 3:78, 4:44, 5:102, 6:11, 7:18}`, its + 24,248 ADDs and its gate counts 111/2074/712/2573, machine-checked against + its `CERTIFICATE.json`; + - its D0 count of 18,030 ADDs (from #589's 18,085), computed here. Its + equality with the value stated in #1043's PROOF.md is not + machine-checked. +3. **No interaction.** Traces are aligned gate by gate across about 5,350 + common gates per comparison. The deleted helpers' columns are projected + away, and survivors are renamed. + - **E470** changes no value at all. + - **E464** changes no clean (x or y) column anywhere. With the deleted + helpers' columns projected away, the values differ only in column 340 + (helper h340's arbitrary contents), at four A gates of #589: `A[2044]` + (h340), `A[2047]` (h241), and `A[2068]` and `A[2070]`, which write the + retained totals h477 and h478. The same column also changes at the four + literal inverses of these gates in C. At the two capture writes, h340's + column takes the place of the deleted h464's column, which the + projection drops. + - **Capture census.** At the scatter, the nine retained totals of #589 + carry 42 to 66 helper-dirt columns each + (`{42, 44, 46, 63, 66, 46, 43, 62, 59}` for h472…h480). h475 carries + h470's column, and h477 and h478 carry h464's. In R437 the counts are + the same except h475 (now h473), which drops to 62 with h470's column + gone. h477 and h478 (now h475 and h476) swap h464's column for h340's + and keep 46 and 43. No other column changes. + - **Composed word.** Its trace equals the E464 control's trace with h470's + column deleted, at all 5,369 aligned gates. It equals the E470 control's + trace with h464's column deleted, except at exactly those eight gates. + - **Profile deltas** add exactly: E464 gives −e1−e3−e4, E470 gives + −2e1+2e2−e3−e7, and R437 − #589 = −3e1+2e2−2e3−e4−e7. R437 − R438(E464) + is −2e1+2e2−e3−e7 (mass −8), as the PR states. + - **Compensation.** R437's D0 is the E464 control's D0 with column h470 + deleted. For E464 alone, D0 is **not** a column deletion of #589's D0, + because the h340 dirt reaches two COPY sources. +4. **SOURCE boundaries and chronology.** + - **Source writes.** There are A0/B483/C483 source writes. All 966 + source-write gates hold, before and after, the same full rows as in #589, + with the deleted dirt columns projected away. + - **Climbs.** Every one of the 111 SOURCEs climbs through the same frames as + in #589, between the same unchanged gates. + - **Access histories** differ only at the edits. x54 loses its read at + `A[224]`. x77 loses its read at frame 79 at `A[230]` and gains the frame-186 + read. The x6 and x56 reads move inside the re-synthesized node's window. + - **The new read.** At the frame-186 read (lines {33, 77}, rational dimension + 2), x77 holds exactly its input column, with no dirt. It reached frame 186 + at `A[426]`, as in #589. Its later climbs, at B289, B525, B636 and the C + inverse of B525, are unchanged. The receiver's path is + 0 → 186 → 509 → 392 → 513 → FULL, where #589 has 0 → 79 → 509 → …. + +### Records, hosting, invoice and price + +5. **Records.** The PR's stream has 27,132 records (651,168 bytes, SHA256 + `caeb2eb0…de13cb`). It equals byte for byte a lowering written here from the + word semantics: lazy climbs, one ADD per operand, one COPY/ADD/ERASE episode + per retained total, then the final climbs. The stream is replayed in both + orientations with the selected caller's record semantics. Both pass all 659 + columns with 24,208 ADDs, 9 rank-7 COPYs and the local profile. The + cancellation-free row bounds are 49,347 forward (16 bits) and 1,113,998 + reverse (21 bits). The template's forward and reverse local programs equal + the events derived from this stream. The replay is over F2. Coefficient + signs are bound by the byte equality with the independent lowering and by + the local-program comparison, not by the replay itself. +6. **Hosting.** + - **Schedule and windows.** The template's parent schedule equals the one + derived here from main's nine-stage recipe, including idle ranks + 14, 7, 28, 7, 42, 7, 42, 28, 14 and 0. Under the selected rule, its nine + idle windows are recomputed and equal the template's. The rule: a stage's + local sweep may use a pair's idle child only if, in the schedule, it runs + strictly after the pair's last local or bridge touch and strictly before + the idle child, and it is not on that pair. + - **Slots.** Each replica has 3,933 slots. Each (stage, helper) occurrence + appears exactly once, with width 8 as the word requires. Its stage lies in + its window, and its offsets are disjoint inside the child's rank. + - **Remainders.** They equal the template's, giving the per-replica idle + children `{2:431, 4:444, 6:444, 7:666, 34:2, 42:11}`. + - **Owners.** All 288 calls (9 stages × 32 replicas) match the slots and the + selected data route. The data families form the call's pair block, with + the sides swapped in reverse sweeps. Each hosted helper sits in a + different pair's idle child at its slot. Each call's `local_hash` equals + the SHA256 of its orientation's local program (160 forward, 128 reverse). + In total 125,856 occurrences are hosted. The template's bank counters are + 0, which the owners check already implies. The 7,814,016 local events are + a count (288 × 27,132), not a separate check. +7. **Whole paid profile and invoice.** 288 × the local profile plus 32 × the + idle children gives + `{1:380160, 2:400864, 3:22176, 4:26592, 5:29376, 6:17376, 7:26496, 34:64, 42:352}`. + That is 903,456 children of rank mass 1,808,352 = 64·28,416 − 10,272, + exactly as published. The invoice precision fields are recomputed with the + selected formulas, as an envelope over every non-prefix term: + - prefix 2^18 · 49,347^5 · 1,113,998^4 has 177 bits, charged 192; + - the coefficient has 177 bits; + - the two-level coefficient has 393 bits, charged 512; + - halving depth 2, with 2·42² = 3,528 < 4,096; + - ROW = 2·(64² + 1) + 9,909 + 252 = 18,355, below the inherited cap 20,161 + asserted in `assemble9.py`; + - local payload prefix 64 · 49,347³ · 1,113,998² has 93 bits, under the + 2^104 cap of the selected chain's `columns_h.cpp`/`columns_k.cpp` + checkers. Selected #589's published value, in `tune/EXPECTED.json`, is + also 93. + + The ROW constants 9,909 and 252 and both caps are inherited. +8. **Price.** The equation is + `Σ r·n_r/(m·W) (m/r)^a + 32·m·N/(10^16·W) m^a = 1` with m = 64 and + W = 28,416 (read from the template and asserted equal to these inherited + values), including the inherited bad-class fallback. It is solved with + separate rational log/exp enclosures. At a = c the moment is < 1, and at + c + 10^-24 it is > 1, for + c = **0.001736628253427115480286**. The same engine gives two positive + controls: + - **Selected #589.** The value is built from main only: the #589 word gives + the local profile, `selection9-p111.json` the hosting patterns, and main's + recipe the windows. Its idle children are `{2:435, 4:444, 6:444, 7:666, 42:9}`. + It reproduces the selected bit value 0.001733427039589844234749 exactly at + the 10^-24 grid. + - **#1043.** Its certificate profile splits exactly over the rebuilt E470 + local profile, and the engine reproduces its c, 0.001734176288479865766692. + +### Mutants and controls (each must be rejected; one positive control must pass) + +| Mutant | Outcome | +|---|---| +| D0 dropped | identity fails on 111 columns | +| C dropped | identity fails on 545 columns | +| #589's D0 reused (deleted helpers dropped, renamed) | identity fails on 54 columns | +| #589's C reused (same projection) | identity fails on 3 columns | +| replacement read at frame 79 | illegal climb: x77 would descend from 186 to 79 | +| replacement read moved early, to the removed birth | **F2 identity and frame legality still pass**; rejected only by the SOURCE chronology check (x77 reaches 186 before `A[426]`) | +| replacement read dropped | identity fails on 55 columns | +| naive helper464 deletion (old node, h464 operands dropped) | identity fails on 54 columns | +| each of the ten GL gates dropped in turn | identity fails on 53–63 columns | +| a slot moved to a window outside its stage | window, disjointness, remainder, owner and profile checks fail | +| two slots made to overlap | disjointness and owner checks fail | +| a slot dropped | occurrence, remainder, owner and profile checks fail | +| one idle rank changed | window, remainder and profile checks fail | +| one rank-2 child of the whole profile relabelled as rank 3 | the bound at c fails | +| one rank-42 child of the whole profile relabelled as rank 34 | the bound at the next grid point fails | +| the composed word itself (positive control) | accepted | + +The early-read row shows that the identity and legality checks alone would +not detect a moved SOURCE climb. The audit adopts equality with #589's SOURCE +chronology as a **sufficient inherited condition**. It does not show that an +earlier climb would break the inherited contract. In the price bracket, each +next grid point acts as a built-in negative control. The verifier requires +each mutant's rejected flag to match its expectation, and each price mutant +to fail the expected bound. The rejection reasons are pinned through byte +equality with RESULT.json. + +## Scope, inherited assumptions and unresolved obligations + +These results are checked: + +- the local F2 identity and frame legality of the literal R437 word and both + controls; +- deletion composition at gate and trace level; +- SOURCE write boundaries and chronology against #589; +- the local profile and ADD counts; +- the byte binding of the records and the template's local programs to the + word, and of every call to its local program; +- the hosting slot assignment under the selected idle rule; +- the whole paid profile, the invoice precision fields and the price root. + +These are **not** checked: + +- **Physical semantics.** Owner routes are checked against the selected rule + and route formulas, not against a physical register machine. The private + centre reserve (physical = 28,416 + 9) and the cover classes are not + checked. +- **Native transport.** Only the projector identities above are checked. The + physical register machine, data precision and cover classes are not. Nor + is it checked that the capture contract is independent of which helpers' + dirt reaches a captured total (Open question 1). +- **Inherited formulas.** The invoice formula, the 10^-16 fallback, the ROW + constants and caps, the payload cap and the price equation are used as + stated in the selected sources, not re-derived. +- **Route factors.** The geometry's `max_route_factors` term is covered only by + the envelope; any value below 2^40 gives the same bit lengths. +- **Inherited assumptions.** These are unchanged from selected #589: the + all-size bit/Gaussian compiler, the common-label, mutable-SOURCE and + target-label realization, whole-call correlated hosting, tape and + precision, the analytic H1–H5 lemma (only its finite hypotheses are + evaluated here, not its proof) and the cited outer assembly. + +This is a finite certificate for one local supplier instance and its hosted +invoice. It is not a scoped all-size proof or a multiplication theorem, and it +does not admit PR #3647. It also makes no κ claim. Today the complex primitive +binds, and it would still bind, with about 3.0e-6 of bit headroom, if the +pending complex chain (PR #3653/PR #3682) were admitted. + +## Open next questions + +[TASK.json](TASK.json) structures these. + +1. **Does the inherited capture contract depend on which helpers' dirt + reaches a captured total?** Selected #589 already captures dirty totals: + each of its nine retained totals carries 42 to 66 helper-dirt columns at + the COPY. In two of them (h477 and h478, rank-7 captures), E464 swaps the + deleted h464's column for h340's at the same counts, with clean rows + unchanged. If the native capture lemma that #589 already needs (one paid + transform plus linear private-stream discard) is linear in arbitrary + helper contents, as PR #3647 states, the item closes. First step: state + that lemma's hypotheses as used by selected #589 and check whether any of + them names particular helpers. +2. **Does the E464 pattern recur?** In E464, a carrier's clean contribution + is recovered from the output roles of the single node that reads it, so the + carrier can be deleted. Which other carriers of #589 or R437 have that + property? First step: a read-only census of carriers with one birth whose + reads are confined to one node frame. This is an expansion question: record + the family's five-point expansion decision before any construction round. +3. **Which admission dependencies remain for PR #3647?** No complex claim we + know of would make the bit side bind, so this is not urgent. It becomes + relevant once a complex gain of more than about 3.0e-6 beyond PR #3653/#3682 + is in view. First step: in the intake review of #3647, #3668 and #3690, + map this package's checks and Open question 1 against the inherited + interface list. +4. **Is PR #3647's hosting price-optimal under the audited rule?** In window 6 + the PR places its two stage-6 leftovers (helper indices 421 and 422, + registers 643 and 644) in separate + copies 209 and 210, giving per-replica remainders `{34:2, 42:11}`. Moving + slot `[6,210,0,8,6,422]` to `[6,209,8,8,6,422]` gives `{26:1, 42:12}` at the + same rank mass. The root then rises from 0.0017366282534 to + 0.0017366460420 (+1.78e-8). One AI review pass found this. It was + re-checked locally with this package's slot checks and price engine; that + run is not shipped. Only slot legality and the price equation were + checked: the call owners were not regenerated, and the physical layer was + not checked. It is an observation for PR #3647's author, not an audit + claim. First step: regenerate the owners for the merged slot and rerun + the owners check. + +## Predecessors and credit + +- **PR #3647** (ai-nanachi; substantial OpenAI Codex assistance per its + README): the R437 composition, the helper464 GL edit, the records, the + hosted template and the claimed c, all audited here. +- **#1043** (Ali Romman): the helper470 deletion and its source-boundary proof + on main. Its other replays (PR #1302, PR #2971, PR #2653) cover helper470 + alone and are cited, not redone. +- **Selected #589 chain** (eumemic, DreamingOfClouds, DaysSky's #442 hosting, + #510/#463 nine-stage caller and invoice, and the credited chain in their + NOTICEs): every semantic rule used here. +- **PR #3668** (jwr404): histogram-to-c arithmetic on the published + histogram. This package rederives the histogram instead. +- **PR #3690** (zxv): concurrent paid-request reconstruction and ordinary + coupling for R437, built on predecessor and author code. Its overlap with + this package is described under "Why it matters". +- **Related and not audited.** PR #3645 (RossRichardson, `99b901c9`) reduces + #1043's R438 to a local R429 word, and PR #3672 (jwr404, `8f735782`) checks + the arithmetic of that R429 profile. Neither claims a c. The complex chain + is PR #3653 (rohanarun) and PR #3682 (zxv), cited only for its root. +- This loop's earlier audit, PR #3687, supplied the audit pattern only. It + covered a different, complex supplier. + +## Provenance + +The four files in [inputs/](inputs/) are byte-preserved copies of files from +PR #3647 by ai-nanachi (head `36ff4414`, package +`research/bit-p111-r437-gl464-470-20261018`), used under Apache-2.0. The +record stream is wrapped in gzip, and the verifier checks its uncompressed +SHA256. The inherited predecessor credits are listed in that package's +UPSTREAM-NOTICE.md (Git blob `90ac2537`) and its LICENSE (blob `261eeb9e`). +Those files are not on main yet, so the credit is restated here. + +These inputs are bound by the `snapshot` rows of [SOURCES.json](SOURCES.json), +not by `head:` pins. A `head:` pin requires the vendored path to equal the PR +path, and the record stream is stored gzip-wrapped. Each snapshot row records +the source PR, commit, path, Git blob and SHA256, and `verify.py` checks every +SHA256 before use. The generic runner ignores the `snapshot` key, so that +binding is enforced by this package's verifier. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Base commit +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The checks are finite exact +computations in Python 3 (standard library). The package was reviewed by +seven independent AI review passes in the same loop, in two rounds (round 1: +reproducibility, mathematics/accounting, provenance, referee; round 2: +mathematics/accounting, reproducibility, referee). Their findings are +addressed here. Two suggested texts were not adopted: a replacement sentence +that repeated the mixed-convention comparison, and keeping a 32-child price +mutant beside the two single-child ones. No human or formal-kernel review is +claimed. Apache-2.0. diff --git a/research/r437-composed-bit-independent-audit/RESULT.json b/research/r437-composed-bit-independent-audit/RESULT.json new file mode 100644 index 0000000000..100b9cd1ee --- /dev/null +++ b/research/r437-composed-bit-independent-audit/RESULT.json @@ -0,0 +1,1456 @@ +{ + "c1043_certificate_vs_rebuilt": { + "adds_equal": true, + "gates_equal": true, + "local_profile_equal": true + }, + "capture_dirt": { + "R437_pr_columns": { + "470": 42, + "471": 44, + "472": 46, + "473": 62, + "474": 66, + "475": 46, + "476": 43, + "477": 62, + "478": 59 + }, + "changes_vs_589": [ + { + "added": [ + 340 + ], + "deleted_helper_columns_dropped": [ + 464 + ], + "removed": [], + "total_589": 477, + "total_R437": 475 + }, + { + "added": [ + 340 + ], + "deleted_helper_columns_dropped": [ + 464 + ], + "removed": [], + "total_589": 478, + "total_R437": 476 + } + ], + "selected589_columns": { + "472": 42, + "473": 44, + "474": 46, + "475": 63, + "476": 66, + "477": 46, + "478": 43, + "479": 62, + "480": 59 + }, + "selected589_totals_carrying_deleted_helpers": { + "475": [ + 470 + ], + "477": [ + 464 + ], + "478": [ + 464 + ] + } + }, + "compensation_facts": { + "e464_D0_is_589_D0_with_column_deleted": false, + "e470_D0_is_589_D0_with_column_deleted": true, + "e470_D0_is_C464_D0_with_column_deleted": true + }, + "composition": { + "c464_equals_pr_R438_except_stats": true, + "canonical_sha256": { + "c470_rebuilt": "c5846159a51ae8bab3247f85200eaa4ca84d738f1c7bd6f128ef85e0d749dd48", + "pr_R437": "da77deaf11368d016622348227657b98404b6afbc7e4f3d6fe9a246baae0dcce", + "pr_R438": "7e6d45542f8f0f9879d82bac1ce701a592b7ba87cd808f6cab28eb0bce494c12", + "w589": "5642fd0e35a1acc11acff8d0c08350c1617e95f310d4d35ad63a651f9eeeba0b" + }, + "composed_equals_pr_R437_except_stats": true, + "e464_node": [ + [ + 506, + 340, + [ + 349 + ] + ], + [ + 506, + 241, + [ + 349 + ] + ], + [ + 506, + 241, + [ + 340 + ] + ], + [ + 506, + 340, + [ + 349 + ] + ], + [ + 506, + 349, + [ + 340 + ] + ], + [ + 506, + 340, + [ + 349 + ] + ], + [ + 506, + 340, + [ + 241 + ] + ], + [ + 506, + 241, + [ + 6, + 56, + 233, + 319, + 322, + 463 + ] + ], + [ + 506, + 340, + [ + 6, + 56, + 322, + 462, + 463 + ] + ], + [ + 506, + 349, + [ + 6, + 56, + 233, + 319, + 322, + 462, + 463 + ] + ] + ], + "edit_windows_589_A": { + "e464": [ + 224, + [ + 1986, + 1989 + ] + ], + "e470": [ + 230, + 1993 + ] + }, + "stats_589": { + "extra_carriers": 10, + "junk_wires": 0, + "rcv_flips": 10 + }, + "stats_pr_R437": { + "extra_carriers": 8, + "junk_wires": 0, + "rcv_flips": 10 + }, + "stats_pr_R438": { + "extra_carriers": 9, + "junk_wires": 0, + "rcv_flips": 10 + } + }, + "cpu_seconds_note": "not recorded (platform dependent)", + "frame_closure_memberships": 70596, + "frame_paths_1043": { + "c470_equals_candidate": true, + "selected589_equals_baseline": true + }, + "frames": 636, + "hosting": { + "banks": 0, + "calls": 288, + "calls_bound_to_local_programs": true, + "copy_in_range": true, + "deficit": 10272, + "emitted_local_events_count": 7814016, + "every_occurrence_once": true, + "hosted_occurrences": 125856, + "idle_children_per_replica": { + "2": 431, + "4": 444, + "6": 444, + "7": 666, + "34": 2, + "42": 11 + }, + "local_programs_equal_records": true, + "offsets_disjoint_within_rank": true, + "owners_match_slots_and_blocks": true, + "rank_mass": 1808352, + "remainders_equal_published": true, + "schedule_equals_main_recipe": true, + "slots": 3933, + "stage_inside_window": true, + "template_canonical_sha256": "2e868ff427654e47df34779299545c53aa05b8c96697ee126e80e7bc6a50990a", + "template_source_record_sha256": "caeb2eb0e417992788c32c1f5812ada60b46d1dfdba9f4ac376299b2dede13cb", + "whole_profile": { + "1": 380160, + "2": 400864, + "3": 22176, + "4": 26592, + "5": 29376, + "6": 17376, + "7": 26496, + "34": 64, + "42": 352 + }, + "width_matches_word": true, + "windows": { + "0": [ + 1, + 14, + [ + 0, + 1 + ] + ], + "1": [ + 1, + 7, + [ + 2 + ] + ], + "2": [ + 2, + 28, + [ + 0, + 1, + 2, + 3 + ] + ], + "3": [ + 2, + 7, + [ + 4 + ] + ], + "4": [ + 3, + 42, + [ + 0, + 1, + 2, + 3, + 4, + 5 + ] + ], + "5": [ + 3, + 7, + [ + 6 + ] + ], + "6": [ + 0, + 42, + [ + 3, + 4, + 5, + 6, + 7, + 8 + ] + ], + "7": [ + 1, + 28, + [ + 5, + 6, + 7, + 8 + ] + ], + "8": [ + 2, + 14, + [ + 7, + 8 + ] + ], + "9": [ + 3, + 0, + [] + ] + }, + "windows_rederived_equal": true + }, + "hosting_mutants": [ + { + "broken": [ + "stage_inside_window", + "offsets_disjoint_within_rank", + "remainders_equal_published", + "owners_match_slots_and_blocks", + "whole_profile" + ], + "mutant": "slot_moved_outside_window", + "rejected": true + }, + { + "broken": [ + "offsets_disjoint_within_rank", + "owners_match_slots_and_blocks" + ], + "mutant": "slot_offsets_overlap", + "rejected": true + }, + { + "broken": [ + "every_occurrence_once", + "remainders_equal_published", + "owners_match_slots_and_blocks", + "whole_profile" + ], + "mutant": "slot_dropped", + "rejected": true + }, + { + "broken": [ + "windows_rederived_equal", + "remainders_equal_published", + "whole_profile" + ], + "mutant": "idle_rank_changed", + "rejected": true + } + ], + "mutants": [ + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "drop_D0", + "note": "no frame-zero dirt compensation", + "reason": "identity fails on 111 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "drop_cleanup_C", + "note": "no literal reverse cleanup", + "reason": "identity fails on 545 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "stale_D0_from_589", + "note": "selected D0 reused with the deleted helpers dropped", + "reason": "identity fails on 54 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "stale_C_from_589", + "note": "selected C reused with the deleted helpers dropped", + "reason": "identity fails on 3 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": null, + "mutant": "late_read_at_frame79", + "note": "replacement read at the removed carrier frame 79 (descends SOURCE77)", + "reason": "legality: illegal climb of register 77 from frame 186 to 79 at ('A', 1998)", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": true, + "mutant": "early_read_at_birth", + "note": "replacement read moved to the removed birth position (before A[426])", + "reason": "source chronology changed for sources [77]", + "rejected": true + }, + { + "expect_rejected": false, + "legal_and_f2_identity": true, + "mutant": "positive_control_composed", + "note": "the composed word itself", + "reason": null, + "rejected": false + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "drop_replacement_read", + "note": "helper470 deleted without the replacement read", + "reason": "identity fails on 55 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "naive_464_deletion", + "note": "old node kept, helper464 operand dropped (no GL re-synthesis)", + "reason": "identity fails on 54 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_0", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 53 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_1", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 54 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_2", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 54 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_3", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 55 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_4", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 62 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_5", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 63 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_6", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 63 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_7", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 55 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_8", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 63 columns", + "rejected": true + }, + { + "expect_rejected": true, + "legal_and_f2_identity": false, + "mutant": "gl_node_drop_gate_9", + "note": "one of the ten GL node gates removed", + "reason": "identity fails on 55 columns", + "rejected": true + } + ], + "native": { + "address_exchange_identity_on_focus": true, + "climb_pairs": 2384, + "focus_transitions": [ + [ + 0, + 11 + ], + [ + 0, + 56 + ], + [ + 0, + 60 + ], + [ + 0, + 186 + ], + [ + 11, + 115 + ], + [ + 56, + 116 + ], + [ + 60, + 123 + ], + [ + 79, + 186 + ], + [ + 115, + 506 + ], + [ + 116, + 506 + ], + [ + 123, + 506 + ], + [ + 186, + 509 + ], + [ + 348, + 511 + ], + [ + 351, + 515 + ], + [ + 361, + 516 + ], + [ + 386, + 560 + ], + [ + 392, + 513 + ], + [ + 506, + 348 + ], + [ + 506, + 351 + ], + [ + 506, + 361 + ], + [ + 509, + 386 + ], + [ + 509, + 392 + ], + [ + 511, + 1 + ], + [ + 513, + 1 + ], + [ + 515, + 1 + ], + [ + 516, + 1 + ], + [ + 560, + 1 + ] + ], + "frames_projected": 636, + "nested_projector_identity": true, + "projector_rank_equals_dim": true + }, + "pins": { + "research/bit-boundary-persistence/CERTIFICATE.json": "32c6cd6103006d627909cabdaf5083238c661a6582016a8b21075bd01c892eff", + "research/bit-boundary-persistence/FRAME-PATHS.json": "0d347b9e4d8a8336a707565deceb1d505cd138c97a56831643583b83d91c3b4f", + "research/e8-bit-p111-tuned/data/selection9-p111.json": "4ab1ed4529683cd184987f8bc3031fb7408b9cd22c25ab9cf541a8aaf896eaf1", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "research/r437-composed-bit-independent-audit/inputs/FINAL-R438-WORD.json.gz": "5aa4d91fb0062265b25fb8f322a57b76d89caaf055b4110cf6fdb761f0b27463", + "research/r437-composed-bit-independent-audit/inputs/R437-COMPOSED-WORD.json.gz": "e432182d5b62c8bbefeb871fce30317234d707e5e18d4295e65ac21f7fd8365e", + "research/r437-composed-bit-independent-audit/inputs/R437-GLOBAL-TEMPLATE.json.gz": "00dee04c5372ac300b678c4ac1e6770c178923099d2d4bf01be9e4bccd2a1e72", + "research/r437-composed-bit-independent-audit/inputs/R437-RECORDS.bin.gz": "6e556dae1a2f56f3893afa9b316f6029712c6b79a3536a429f8d83cac79163e9" + }, + "precision_R437": { + "charged_prefix_bits": 192, + "charged_two_level_bits": 512, + "children": 903456, + "coefficient_bits": [ + 177, + 177 + ], + "halving_depth": 2, + "halving_inequality": [ + 3528, + 4096 + ], + "payload_below_2_104": true, + "payload_prefix_bits": 93, + "prefix_bits": 177, + "row_below_inherited_cap_20161": true, + "row_coefficient": 18355, + "two_level_bits": [ + 393, + 393 + ] + }, + "price": { + "R437": { + "c": "868314126713557740143/500000000000000000000000", + "moment_lower_at_next_grid_above_one": true, + "moment_upper_at_c_below_one": true, + "next_grid": "1736628253427115480287/1000000000000000000000000" + }, + "c1043_control": { + "bracket": { + "c": "433544072119966441673/250000000000000000000000", + "moment_lower_at_next_grid_above_one": true, + "moment_upper_at_c_below_one": true, + "next_grid": "1734176288479865766693/1000000000000000000000000" + }, + "idle_children_per_replica": { + "2": 430, + "4": 441, + "6": 443, + "7": 666, + "10": 5, + "12": 3, + "14": 1, + "42": 9 + }, + "split_exact": true + }, + "selected589_control": { + "bracket": { + "c": "1733427039589844234749/1000000000000000000000000", + "moment_lower_at_next_grid_above_one": true, + "moment_upper_at_c_below_one": true, + "next_grid": "6933708158359376939/4000000000000000000000" + }, + "every_stage_hosts_all_helpers": true, + "idle_children_per_replica": { + "2": 435, + "4": 444, + "6": 444, + "7": 666, + "42": 9 + }, + "stages_legal": true, + "whole_profile": { + "1": 381024, + "2": 400416, + "3": 22752, + "4": 26880, + "5": 29376, + "6": 17376, + "7": 26784, + "42": 288 + } + } + }, + "price_mutants": [ + { + "expected_failing_bound": "moment_upper_at_c_below_one", + "failing_bound": [ + "moment_upper_at_c_below_one" + ], + "mutant": "one_rank2_child_as_rank3", + "rejected": true + }, + { + "expected_failing_bound": "moment_lower_at_next_grid_above_one", + "failing_bound": [ + "moment_lower_at_next_grid_above_one" + ], + "mutant": "one_rank42_child_as_rank34", + "rejected": true + } + ], + "profile_delta": { + "additive": true, + "composed": { + "1": -3, + "2": 2, + "3": -2, + "4": -1, + "7": -1 + }, + "composed_vs_C464": { + "1": -2, + "2": 2, + "3": -1, + "7": -1 + }, + "e464": { + "1": -1, + "3": -1, + "4": -1 + }, + "e470": { + "1": -2, + "2": 2, + "3": -1, + "7": -1 + } + }, + "records": { + "forward": { + "adds": 24208, + "bad_columns": 0, + "bits": 16, + "cancellation_free_row_l1": 49347, + "copies": 9, + "profile": { + "1": 1320, + "2": 1344, + "3": 77, + "4": 43, + "5": 102, + "6": 11, + "7": 18 + } + }, + "independent_lowering_byte_equal": true, + "kinds": { + "0": 2906, + "1": 24208, + "2": 9, + "3": 9 + }, + "pr_stream_bytes": 651168, + "pr_stream_sha256": "caeb2eb0e417992788c32c1f5812ada60b46d1dfdba9f4ac376299b2dede13cb", + "records": 27132, + "reverse": { + "adds": 24208, + "bad_columns": 0, + "bits": 21, + "cancellation_free_row_l1": 1113998, + "copies": 9, + "profile": { + "1": 1320, + "2": 1344, + "3": 77, + "4": 43, + "5": 102, + "6": 11, + "7": 18 + } + } + }, + "source77": { + "new_read": { + "frame": 186, + "frame_dim": 2, + "frame_lines": [ + 33, + 77 + ], + "receiver": 444, + "source_value_is_clean_input": true + }, + "receiver444_climbs_589": [ + [ + "('window after', ('A', 1992))", + 0, + 79 + ], + [ + "('A', 1994)", + 79, + 509 + ], + [ + "('A', 2038)", + 509, + 392 + ], + [ + "('A', 2064)", + 392, + 513 + ], + [ + "('C', 'A', 2064)", + 513, + 1 + ] + ], + "receiver444_climbs_R437": [ + [ + "('window after', ('A', 1992))", + 0, + 186 + ], + [ + "('A', 1994)", + 186, + 509 + ], + [ + "('A', 2038)", + 509, + 392 + ], + [ + "('A', 2064)", + 392, + 513 + ], + [ + "('C', 'A', 2064)", + 513, + 1 + ] + ], + "source77_climbs_589": [ + [ + "('A', 426)", + 79, + 186 + ], + [ + "('B', 289)", + 186, + 509 + ], + [ + "('B', 525)", + 509, + 386 + ], + [ + "('B', 636)", + 386, + 560 + ], + [ + "('C', 'B', 525)", + 560, + 1 + ] + ], + "source77_climbs_R437": [ + [ + "('A', 426)", + 79, + 186 + ], + [ + "('B', 289)", + 186, + 509 + ], + [ + "('B', 525)", + 509, + 386 + ], + [ + "('B', 636)", + 386, + 560 + ], + [ + "('C', 'B', 525)", + 560, + 1 + ] + ] + }, + "source_chronology": { + "access_history_differences": { + "6": { + "added": [ + [ + "('A464', 7)", + 506, + "read" + ], + [ + "('A464', 8)", + 506, + "read" + ], + [ + "('A464', 9)", + 506, + "read" + ] + ], + "removed": [ + [ + "('A', 1986)", + 506, + "read" + ], + [ + "('A', 1988)", + 506, + "read" + ] + ] + }, + "54": { + "added": [], + "removed": [ + [ + "('A', 224)", + 56, + "read" + ] + ] + }, + "56": { + "added": [ + [ + "('A464', 7)", + 506, + "read" + ], + [ + "('A464', 8)", + 506, + "read" + ], + [ + "('A464', 9)", + 506, + "read" + ] + ], + "removed": [ + [ + "('A', 1986)", + 506, + "read" + ], + [ + "('A', 1988)", + 506, + "read" + ] + ] + }, + "77": { + "added": [ + [ + "('A470', 0)", + 186, + "read" + ] + ], + "removed": [ + [ + "('A', 230)", + 79, + "read" + ] + ] + } + }, + "all_source_climbs_identical": true + }, + "status": "PASS_INDEPENDENT_R437_WORD_AUDIT", + "traces": { + "composed_vs_589": { + "aligned_gates": 5349, + "clean_value_differences": 0, + "differing_columns": [ + 340 + ], + "full_value_differences": [ + [ + "A", + 2044 + ], + [ + "A", + 2047 + ], + [ + "A", + 2068 + ], + [ + "A", + 2070 + ], + [ + "C", + "A", + 2044 + ], + [ + "C", + "A", + 2047 + ], + [ + "C", + "A", + 2068 + ], + [ + "C", + "A", + 2070 + ] + ], + "source_write_gates_compared": 966 + }, + "composed_vs_C464": { + "aligned_gates": 5369, + "clean_value_differences": 0, + "differing_columns": [], + "full_value_differences": [], + "source_write_gates_compared": 966 + }, + "composed_vs_C470": { + "aligned_gates": 5351, + "clean_value_differences": 0, + "differing_columns": [ + 340 + ], + "full_value_differences": [ + [ + "A", + 2044 + ], + [ + "A", + 2047 + ], + [ + "A", + 2068 + ], + [ + "A", + 2070 + ], + [ + "C", + "A", + 2044 + ], + [ + "C", + "A", + 2047 + ], + [ + "C", + "A", + 2068 + ], + [ + "C", + "A", + 2070 + ] + ], + "source_write_gates_compared": 966 + }, + "e464_vs_589": { + "aligned_gates": 5353, + "clean_value_differences": 0, + "differing_columns": [ + 340 + ], + "full_value_differences": [ + [ + "A", + 2044 + ], + [ + "A", + 2047 + ], + [ + "A", + 2068 + ], + [ + "A", + 2070 + ], + [ + "C", + "A", + 2044 + ], + [ + "C", + "A", + 2047 + ], + [ + "C", + "A", + 2068 + ], + [ + "C", + "A", + 2070 + ] + ], + "source_write_gates_compared": 966 + }, + "e470_vs_589": { + "aligned_gates": 5357, + "clean_value_differences": 0, + "differing_columns": [], + "full_value_differences": [], + "source_write_gates_compared": 966 + } + }, + "whole_profile_split": { + "claimed": { + "1": 380160, + "2": 400864, + "3": 22176, + "4": 26592, + "5": 29376, + "6": 17376, + "7": 26496, + "34": 64, + "42": 352 + }, + "deficit": 10272, + "helper_occurrences": 125856, + "idle_children_per_replica": { + "2": 431, + "4": 444, + "6": 444, + "7": 666, + "34": 2, + "42": 11 + }, + "live_data": 28416, + "local_calls": 288, + "rank_mass": 1808352, + "replicas": 32 + }, + "words": { + "C464_pr_R438": { + "columns": 660, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "forward_bad_columns": 0, + "gates": { + "A": 2081, + "B": 712, + "C": 2580, + "D": 111 + }, + "helpers": 438, + "interface": { + "D0_rebuilt": true, + "H1": true, + "H2": true, + "H3": true, + "H4_C_literal_reverse": true, + "H5_V_identity": true, + "J_identity": true, + "U_block": true + }, + "mass": 5121, + "methods_agree_entrywise": true, + "profile": { + "1": 1322, + "2": 1342, + "3": 78, + "4": 43, + "5": 102, + "6": 11, + "7": 19 + }, + "pullback_bad_columns": 0, + "reverse_orientation_bad_columns": 0, + "scalar_adds": { + "A": 2134, + "B": 934, + "C": 2633, + "D": 18037, + "scatter": 527, + "total": 24265 + }, + "source_writes": { + "A": 0, + "B": 483, + "C": 483, + "D": 0 + }, + "sources": 111 + }, + "C470_rebuilt_1043": { + "columns": 660, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "forward_bad_columns": 0, + "gates": { + "A": 2074, + "B": 712, + "C": 2573, + "D": 111 + }, + "helpers": 438, + "interface": { + "D0_rebuilt": true, + "H1": true, + "H2": true, + "H3": true, + "H4_C_literal_reverse": true, + "H5_V_identity": true, + "J_identity": true, + "U_block": true + }, + "mass": 5121, + "methods_agree_entrywise": true, + "profile": { + "1": 1321, + "2": 1344, + "3": 78, + "4": 44, + "5": 102, + "6": 11, + "7": 18 + }, + "pullback_bad_columns": 0, + "reverse_orientation_bad_columns": 0, + "scalar_adds": { + "A": 2129, + "B": 934, + "C": 2628, + "D": 18030, + "scatter": 527, + "total": 24248 + }, + "source_writes": { + "A": 0, + "B": 483, + "C": 483, + "D": 0 + }, + "sources": 111 + }, + "R437_pr": { + "columns": 659, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "forward_bad_columns": 0, + "gates": { + "A": 2080, + "B": 712, + "C": 2579, + "D": 111 + }, + "helpers": 437, + "interface": { + "D0_rebuilt": true, + "H1": true, + "H2": true, + "H3": true, + "H4_C_literal_reverse": true, + "H5_V_identity": true, + "J_identity": true, + "U_block": true + }, + "mass": 5113, + "methods_agree_entrywise": true, + "profile": { + "1": 1320, + "2": 1344, + "3": 77, + "4": 43, + "5": 102, + "6": 11, + "7": 18 + }, + "pullback_bad_columns": 0, + "reverse_orientation_bad_columns": 0, + "scalar_adds": { + "A": 2133, + "B": 934, + "C": 2632, + "D": 17982, + "scatter": 527, + "total": 24208 + }, + "source_writes": { + "A": 0, + "B": 483, + "C": 483, + "D": 0 + }, + "sources": 111 + }, + "selected589": { + "columns": 661, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "forward_bad_columns": 0, + "gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 111 + }, + "helpers": 439, + "interface": { + "D0_rebuilt": true, + "H1": true, + "H2": true, + "H3": true, + "H4_C_literal_reverse": true, + "H5_V_identity": true, + "J_identity": true, + "U_block": true + }, + "mass": 5129, + "methods_agree_entrywise": true, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "pullback_bad_columns": 0, + "reverse_orientation_bad_columns": 0, + "scalar_adds": { + "A": 2130, + "B": 934, + "C": 2629, + "D": 18085, + "scatter": 527, + "total": 24305 + }, + "source_writes": { + "A": 0, + "B": 483, + "C": 483, + "D": 0 + }, + "sources": 111 + } + } +} diff --git a/research/r437-composed-bit-independent-audit/SOURCES.json b/research/r437-composed-bit-independent-audit/SOURCES.json new file mode 100644 index 0000000000..98188fe070 --- /dev/null +++ b/research/r437-composed-bit-independent-audit/SOURCES.json @@ -0,0 +1,132 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/bit-boundary-persistence/FRAME-PATHS.json", + "usage": "input", + "git_blob": "b1862b43e1fa1ee0fb02e29b303801265638dae4", + "sha256": "0d347b9e4d8a8336a707565deceb1d505cd138c97a56831643583b83d91c3b4f" + }, + { + "path": "research/bit-boundary-persistence/PROOF.md", + "usage": "provenance", + "git_blob": "560c21b5d47c2779d2b2e14b4decb1aaeba4c64f", + "sha256": "fee9059a1fb1db9ec16ce339f0dd36c29f2e6ec7103aa76c0b2296f8529bac6c" + }, + { + "path": "research/e8-bit-p111-tuned/code/xcheck_p.py", + "usage": "provenance", + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + { + "path": "research/e8-bit-p111-tuned/code/pwordl.py", + "usage": "provenance", + "git_blob": "a90bed93e227c3916aca67817794f35e24123ceb", + "sha256": "6d8fccd44508e4705b6446e0a64482a5221a3efc5663c5ca7ae90d44581ac50a" + }, + { + "path": "research/e8-bit-p111-tuned/data/selection9-p111.json", + "usage": "input", + "git_blob": "e69ea66a3add357f570fc5552ab6368b3c8f9bb2", + "sha256": "4ab1ed4529683cd184987f8bc3031fb7408b9cd22c25ab9cf541a8aaf896eaf1" + }, + { + "path": "research/bit-boundary-persistence/CERTIFICATE.json", + "usage": "input", + "git_blob": "56400920050c523e6e399f2455137b36c35cf528", + "sha256": "32c6cd6103006d627909cabdaf5083238c661a6582016a8b21075bd01c892eff" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/hub/idle-axis-hosting/hosting_core.py", + "usage": "provenance", + "git_blob": "68b536daa9e6546c0aa046934bf840aaa3c3fde3", + "sha256": "d8b90cd5d152df3c7c351230863d9e61816ad5e1f21d69bea1a86a5daad559a3" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py", + "usage": "provenance", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/vendor/e8-r715-eleven-stage-whole/code/global_k.py", + "usage": "provenance", + "git_blob": "3df12bd632f1fdba825ced57110a1fee82eb2857", + "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8" + }, + { + "path": "research/e8-bit-p111-tuned/vendor/pr510/e8-r480-nine-stage/code/assemble9.py", + "usage": "provenance", + "git_blob": "238226c568742dd5723b03eabae564a2eaa2bda9", + "sha256": "4bf6768224a3fac81ccda26df24f3763f9a4fbc35ad62bef2888595cdae519fe" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_h.cpp", + "usage": "provenance", + "git_blob": "00c5a3a5d81d083582f60f33dd2e7bea5049c37f", + "sha256": "d1297f9052be4f2496e1ff2a77e4db2c0cdbd7d460d489b4c03e50bf317238ce" + }, + { + "path": "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "usage": "provenance", + "git_blob": "42bb232fbec4de703e70cc13dc2f39a3b43a3a01", + "sha256": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2" + } + ], + "snapshot": [ + { + "local": "inputs/R437-COMPOSED-WORD.json.gz", + "source_path": "research/bit-p111-r437-gl464-470-20261018/data/r0042/R437-COMPOSED-WORD.json.gz", + "source_commit": "36ff441479ff9c7e70d83f0becccd44da50effb8", + "source_pr": 3647, + "git_blob": "c558a221dd44cbdaa732a401f9876de4c096d4a7", + "sha256": "e432182d5b62c8bbefeb871fce30317234d707e5e18d4295e65ac21f7fd8365e" + }, + { + "local": "inputs/FINAL-R438-WORD.json.gz", + "source_path": "research/bit-p111-r437-gl464-470-20261018/data/r0028/FINAL-R438-WORD.json.gz", + "source_commit": "36ff441479ff9c7e70d83f0becccd44da50effb8", + "source_pr": 3647, + "git_blob": "db621440ab3f87ece927137c21f4f7fb3ba221ef", + "sha256": "5aa4d91fb0062265b25fb8f322a57b76d89caaf055b4110cf6fdb761f0b27463" + }, + { + "local": "inputs/R437-RECORDS.bin.gz", + "source_path": "research/bit-p111-r437-gl464-470-20261018/data/r0042/R437-RECORDS.bin", + "source_commit": "36ff441479ff9c7e70d83f0becccd44da50effb8", + "source_pr": 3647, + "git_blob": "ac75dd07819be402dc28a84b09561bfe42f1cc80", + "sha256": "6e556dae1a2f56f3893afa9b316f6029712c6b79a3536a429f8d83cac79163e9", + "uncompressed_sha256": "caeb2eb0e417992788c32c1f5812ada60b46d1dfdba9f4ac376299b2dede13cb", + "note": "gzip (level 9, mtime 0) of the PR file; the verifier checks the decompressed SHA256" + }, + { + "local": "inputs/R437-GLOBAL-TEMPLATE.json.gz", + "source_path": "research/bit-p111-r437-gl464-470-20261018/generated/GLOBAL-TEMPLATE.json.gz", + "source_commit": "36ff441479ff9c7e70d83f0becccd44da50effb8", + "source_pr": 3647, + "git_blob": "df9238596dbe8cd355a65aa170caa54f543c39cd", + "sha256": "00dee04c5372ac300b678c4ac1e6770c178923099d2d4bf01be9e4bccd2a1e72" + } + ] +} diff --git a/research/r437-composed-bit-independent-audit/TASK.json b/research/r437-composed-bit-independent-audit/TASK.json new file mode 100644 index 0000000000..9cbcceed6b --- /dev/null +++ b/research/r437-composed-bit-independent-audit/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently audit PR #3647 (head 36ff4414)'s composed R437 bit supplier: the helper464 joint GL deletion composed with #1043's helper470 deletion, against single-change controls #589+E464 (the PR's R438) and #589+E470 (#1043's R438, rebuilt). Word level: the exact F2 identity on all 659 inputs with arbitrary dirty helpers, by a forward replay and a reverse pull-back, plus the literal reverse orientation; literal reconstruction of R437 from selected #589; aligned-trace non-interaction; SOURCE77 frame-186 chronology and all SOURCE write boundaries; the local profile and its deltas; exact rational projector identities as a second frame method. Stretch, completed: byte binding of the PR's records and the template's local programs; the parent schedule and idle windows from main's recipe and hosting rule; legality of the 3,933 slots per replica, and all 288 calls' owners and local-program hashes; the whole paid profile; the invoice precision envelope including the payload-prefix and ROW caps; and an independent exact price bracket for c, with positive controls reproducing selected #589's a and #1043's c. Plus 18 word mutants, 4 hosting mutants and 2 single-child price mutants, all rejected, and one positive control.", + "scope_change_reason": "The card's default object is a complex-moment/assembly claim (#2979). The loop's picker drew the bit-mechanisms track, and PR #3647 makes the highest open bit-supplier value (c = 0.001736628253427115). Apart from the author's own checks, it had only arithmetic or author-code checks: PR3668 checks the histogram-to-c arithmetic, and the concurrent PR3690 (opened during this audit) reconstructs paid requests with predecessor and author code. The card's method, reconstructing a coordinated change against its single-change controls, is applied to that supplier. Correction: this package's task selection was first justified by the claim that the bit side would bind if PR3653/PR3682 were admitted. That rested on a mixed-convention comparison (an 8.57e-9 gap between #589's retained cap a/(1+a) and #3653's modern-outer kappa) and is withdrawn. Under either consistent convention the bit side keeps about 3.0e-6 of headroom.", + "bottleneck_link": "Under the selected chain's inherited semantics, PR #3647's bit supplier c = 0.001736628253427115 (retained cap 0.0017336176; modern-outer bit value 0.0017366283) now has an independent finite check from the literal word through hosting to the price root. There is no near-term kappa consequence. The complex primitive binds today, and it would still bind if PR3653/PR3682 were admitted: the bit headroom is 2.998e-6 under the retained transfer and 3.008e-6 under the modern outer. The bit supplier caps kappa only after a further complex gain of about 3.0e-6, and this check then applies to the highest open bit value. It also records one item to confirm at intake, likely neutral: all nine captured retained totals of selected #589 already carry 42-66 helper-dirt columns at the COPY, and E464 only swaps which helper's column (the deleted h464's for h340's) reaches two of them, h477/h478, at unchanged counts 46/43.", + "budget_minutes": 180, + "stop_rule": "Stop at the first of: a confirmed discrepancy (minimize with mutants); a full PASS of identity, composition, controls, chronology, profile and mutants with both methods agreeing; word semantics not pinned within about 60 min (hand off); or a PR head change (re-pin once). Outcome: full PASS of the core within the semantics budget. The bounded hosted-invoice stretch (at most 60 min) also completed inside the experiment window: hosting, profile, precision envelope and price bracket. c is reproduced under the inherited semantics, not admitted.", + "outcome": "completed", + "evidence": "PASS_INDEPENDENT_R437_WORD_AUDIT (RESULT.json). Word: R437 (659 inputs) and controls #589 (661), #589+E464 = PR R438 (660) and #589+E470 = #1043 R438 (660, rebuilt) all map (x,y,h) to (x,y+x,h) over F2 with legal nested climbs and FULL/t-perp final frames. Forward replay and reverse pull-back agree entrywise; the reverse orientation passes; H1-H5/U/J hold; D0/C equal the rebuilt ones. #589+E464+E470 equals the PR's R437 except stats metadata. The E470 control reproduces #1043's FRAME-PATHS.json and its CERTIFICATE.json local profile, 24,248 ADDs and gates 111/2074/712/2573 (machine-checked), and D0 18,085->18,030 (computed; its equality with the value stated in PROOF.md is not machine-checked). The ten GL gates are taken as data from the PR's R438 word. E470 changes no projected value; E464 changes no clean column; with deleted columns projected away only column 340 differs, at A2044/A2047/A2068/A2070 and their C inverses. Capture census: #589's nine retained totals carry {42,44,46,63,66,46,43,62,59} helper-dirt columns at the scatter; in R437 h477/h478 swap h464's column for h340's (46/43 kept) and h475 loses h470's (63->62); nothing else changes. The composed trace equals the E464 control's with h470 deleted at all 5,369 aligned gates. Profile {1:1320,2:1344,3:77,4:43,5:102,6:11,7:18}, mass 5,113, ADDs 24,208; deltas additive. All 966 SOURCE write gates and all SOURCE climbs match #589; x77 is clean at the frame-186 read, reached at A426. Exact rational projectors: ranks equal dims for all 636 frames; P_A P_B = P_B P_A = P_A on all 2,384 climb pairs. Records: the PR stream (27,132 records, sha caeb2eb0...) is byte-identical to an independent lowering, replays over F2 in both orientations (norms 49,347/1,113,998; signs bound by the byte equality), and equals the template's local programs; all 288 calls' local_hash values equal the programs' SHA256. Hosting: the schedule equals main's recipe; the windows are rederived; 3,933 slots per replica are legal and disjoint; remainders give idle {2:431,4:444,6:444,7:666,34:2,42:11}; 288 calls' owners match the slots and data routes; 125,856 hosted. Whole profile {1:380160,2:400864,3:22176,4:26592,5:29376,6:17376,7:26496,34:64,42:352}, mass 1,808,352, deficit 10,272. Precision: prefix 177 (192), coefficient 177, two-level 393 (512), depth 2, ROW 18,355 < inherited cap 20,161, payload prefix 93 bits < 104. Price (m = 64, W = 28,416 read from the template and asserted): c = 868314126713557740143/(5e23) brackets with the next 1e-24 point failing. Controls: selected #589 a = 0.001733427039589844234749 from main-only inputs and #1043 c = 0.001734176288479865766692 are reproduced. Single-child price mutants fail the expected bound (2->3 at c; 42->34 at the next grid point). The early-read mutant passes F2 identity and legality and is rejected only by the chronology comparison, which the audit adopts as a sufficient inherited condition.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5): design, code, checks and write-up in an automated research loop. Reviewed by seven independent AI review passes in the same loop, in two rounds (four in round 1, three in round 2); findings are addressed, and two suggested texts were not adopted (a replacement sentence repeating the mixed-convention comparison, and keeping a 32-child price mutant). No human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Does the inherited capture contract depend on which helpers' dirt reaches a captured total? Selected #589's nine retained totals already carry 42-66 helper-dirt columns at the COPY; in two of them (h477/h478) E464 swaps the deleted h464's column for h340's at unchanged counts 46/43, with clean rows unchanged.", + "why_it_matters": "The rank-7 captures rely on the inherited 'one paid transform plus linear private-stream discard' contract, which #589 already needs for dirty captures. If it is linear in arbitrary helper contents, as PR #3647 states, the item closes; only if it named particular helpers would the GL edit need a separate native argument.", + "first_step": "State the native capture lemma's hypotheses as used by selected #589 and check whether any of them names particular helpers.", + "blocked_by": "Locating the native capture lemma statement in the selected sources." + }, + { + "question": "Does the E464 pattern recur: which other carriers of #589/R437 have a clean contribution recoverable from the output roles of the single node that reads them?", + "why_it_matters": "E464 is the new mechanism in PR #3647. A census would show whether it is isolated or a family, which bears on whether further bit-supplier gains of this kind exist.", + "first_step": "Run a read-only census of carriers with one birth whose reads are confined to one node frame, and record the five-point expansion decision before any construction round.", + "blocked_by": "The expansion gate; no construction is authorized by this audit." + }, + { + "question": "Which admission dependencies remain for PR #3647 as a bit supplier?", + "why_it_matters": "A checked local supplier is not an admitted one. This is not urgent: no known complex claim makes the bit side bind (about 3.0e-6 of headroom remains after PR3653/PR3682).", + "first_step": "In the intake review of #3647, #3668 and #3690, map this package's checks and open question 1 against the inherited interface list.", + "blocked_by": "Maintainer intake of PR #3647." + }, + { + "question": "Is PR #3647's hosting price-optimal under the audited rule? Merging the two stage-6 leftovers (helper indices 421 and 422, registers 643 and 644) into copy 209 of window 6 gives remainders {26:1, 42:12} instead of {34:2, 42:11} at the same mass, and raises the root by about 1.78e-8 (to 0.0017366460420).", + "why_it_matters": "It is a small, mechanism-free gain for the PR's author. It was found by one AI review pass and re-checked locally (not shipped) for slot legality and the price equation only.", + "first_step": "Regenerate the call owners for the merged slot, rerun the owners check and the physical-layer checks, then reprice.", + "blocked_by": "Owners and the physical layer for the merged slot are not checked." + } + ] +} diff --git a/research/r437-composed-bit-independent-audit/VERIFY.json b/research/r437-composed-bit-independent-audit/VERIFY.json new file mode 100644 index 0000000000..acd588497d --- /dev/null +++ b/research/r437-composed-bit-independent-audit/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/bit-boundary-persistence/FRAME-PATHS.json", + "research/e8-bit-p111-tuned/data/selection9-p111.json", + "research/bit-boundary-persistence/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Source pins; frame closure; for #589, #589+E464 (PR R438), #589+E470 (#1043 R438 rebuilt) and PR R437: F2 identity on all inputs by forward replay and reverse pull-back (entrywise agreement), reverse orientation, H1-H5/U/J, rebuilt D0/C; literal composition equals the PR's R437; #1043 FRAME-PATHS equality; exact rational projector identities on all climbs; aligned-trace non-interaction; helper-dirt census of the retained totals at the scatter (#589 vs R437); SOURCE write boundaries and chronology; profile deltas; byte equality of the PR record stream with an independent lowering, record replay in both orientations, and template local programs; schedule from main's recipe, idle windows by the selected rule, slot legality, owners and local-program hashes of 288 calls, remainders and the whole paid profile; invoice precision envelope with the payload-prefix and ROW caps; template m/W asserted equal to the inherited 64/28416; exact price bracket for c, with selected #589 and #1043 positive controls; #1043 CERTIFICATE profile, ADDs and gates vs the rebuilt control; 18 word mutants, 4 hosting mutants, 2 single-child price mutants and one positive control; receipt equality with RESULT.json." + } + ] +} diff --git a/research/r437-composed-bit-independent-audit/compose.py b/research/r437-composed-bit-independent-audit/compose.py new file mode 100644 index 0000000000..ffa70ac224 --- /dev/null +++ b/research/r437-composed-bit-independent-audit/compose.py @@ -0,0 +1,74 @@ +"""Literal construction of the single-change controls and the composed word from selected #589. + +E464 (PR #3647 ancestry R438, helper464 GL): delete A[224] = [56,464,[54]] and replace +A[1986..1988] (old D4 node at frame 506) by the ten-gate node read from the PR's R438 word. +E470 (#1043, Ali Romman): delete A[230] = [79,470,[77]] and replace A[1993] = [79,444,[470]] +by [186,444,[77]]. Indices are #589 A indices. Deleted helpers are removed and higher ids +renumbered; D0 and C are rebuilt from the raw word (wordsem.rebuild_DC).""" +import copy +from wordsem import need, rebuild_DC + +E464_DEL = 224 +E464_DEL_GATE = [56, 464, [54]] +E464_NODE_AT = (1986, 1989) +E464_OLD_NODE = [[506, 349, [6, 56, 233, 319, 322, 340, 462, 463]], + [506, 340, [233, 241, 319, 349, 464]], + [506, 241, [6, 56, 233, 319, 322, 463, 464]]] +E470_DEL = 230 +E470_DEL_GATE = [79, 470, [77]] +E470_READ = 1993 +E470_OLD_READ = [79, 444, [470]] +E470_NEW_READ = [186, 444, [77]] + + +def apply(w589, new_node=None, do464=False, do470=False, read=None, read_at=None, rebuild=True): + """Return (word, deleted helpers, renaming, origin keys of the A gates). read/read_at + override the E470 replacement gate and its position (mutants only).""" + w = copy.deepcopy(w589) + A = w['A'] + keys = [] + need(A[E464_DEL] == E464_DEL_GATE and A[E464_NODE_AT[0]:E464_NODE_AT[1]] == E464_OLD_NODE, 'E464 anchors changed') + need(A[E470_DEL] == E470_DEL_GATE and A[E470_READ] == E470_OLD_READ, 'E470 anchors changed') + out = [] + for i, g in enumerate(A): + if do464 and i == E464_DEL: + continue + if do464 and E464_NODE_AT[0] <= i < E464_NODE_AT[1]: + if i == E464_NODE_AT[0]: + out.extend(copy.deepcopy(new_node)) + keys.extend(('A464', k) for k in range(len(new_node))) + continue + if do470 and i == E470_DEL: + continue + if do470 and i == E470_READ: + if read_at is None and read != 'drop': + out.append(list(read or E470_NEW_READ)) + keys.append(('A470', 0)) + continue + out.append(g) + keys.append(('A', i)) + if do470 and read_at is not None: + out.insert(read_at, list(read or E470_NEW_READ)) + keys.insert(read_at, ('A470', 0)) + w['A'] = out + dead = sorted(([464] if do464 else []) + ([470] if do470 else [])) + v = w['v'] + for q in dead: + for sec in ('A', 'B'): + for g in w[sec]: + need(q != g[1] and q not in g[2], 'deleted helper %d still used in %s' % (q, sec)) + need(q not in w['ret'], 'deleted helper is retained') + + def ren(r): + return r - sum(1 for q in dead if r > q) + for sec in ('A', 'B'): + w[sec] = [[f, ren(d), [ren(s) for s in srcs]] for f, d, srcs in w[sec]] + w['ret'] = [ren(q) for q in w['ret']] + w['start'] = [x for r, x in enumerate(w['start']) if r not in dead] + w['final'] = [x for r, x in enumerate(w['final']) if r not in dead] + w['R'] = w['R'] - len(dead) + if rebuild: + w['D'], w['C'] = rebuild_DC(w) + else: + w['D'], w['C'] = [], [] + return w, dead, ren, keys diff --git a/research/r437-composed-bit-independent-audit/hosting.py b/research/r437-composed-bit-independent-audit/hosting.py new file mode 100644 index 0000000000..54c3947297 --- /dev/null +++ b/research/r437-composed-bit-independent-audit/hosting.py @@ -0,0 +1,214 @@ +"""Bounded check of PR #3647's R437 hosted template against the audited word and records. + +The hosting rule is taken from the selected chain's idle-axis hosting module on main +(research/e8-bit-carrier-skeleton/code/hub/idle-axis-hosting/hosting_core.py, docstrings of +windows() and expand()). This module is written separately for the audit and imports nothing +from it. + +Rule: an idle child (idx, pair p, rank r) may host a whole width-w helper residual of a local +invocation at stage s only when that invocation lies strictly between the last touch of pair p +(a local invocation on p, or a bridge naming p) and the idle child, and is not on p itself. +Each of the 2v (side, port) data families of p receives one copy of the child; a hosted residual +owns coordinates [off, off + w) of one copy, and that child keeps the remaining rank. +""" +import hashlib +import json +from collections import Counter, defaultdict + +from wordsem import need + + +def nine_stage_schedule(K=4): + """Parent recipe of the selected nine-stage caller (global_k.py on main: recipe(K) and its + idle-child insertion after each local stage), with idle children numbered in order.""" + ev = [dict(kind='local_cover_sweep', stage=0, pair=0, reverse=False)] + stage = 1 + for j in range(K): + ev.append(dict(kind='local_cover_sweep', stage=stage, pair=j, reverse=True)) + stage += 1 + if j < K - 1: + ev.append(dict(kind='bridge', dst=j, src=j + 1, coefficient=1)) + ev.append(dict(kind='local_cover_sweep', stage=stage, pair=j, reverse=False)) + stage += 1 + if j < K - 1: + ev.append(dict(kind='bridge', dst=j, src=j + 1, coefficient=-1)) + for j in reversed(range(K - 1)): + ev.append(dict(kind='bridge', dst=j + 1, src=j, coefficient=1)) + ev.append(dict(kind='exchange')) + out, levels, idx = [], [-1] * K, 0 + for e in ev: + out.append(e) + if e['kind'] != 'local_cover_sweep': + continue + s, p = e['stage'], e['pair'] + levels[p] = s + new = [] + if s % 2 == 1 and s <= 2 * K - 3: + j = (s + 1) // 2 + new.append((j, 7 * (s + 1), -1, s)) + levels[j] = s + elif s % 2 == 0 and 2 <= s <= 2 * K - 2: + new.append((s // 2, 7, s - 1, s)) + levels[s // 2] = s + elif s == 2 * K: + for j in range(K): + new.append((j, 7 * (2 * K - levels[j]), levels[j], 2 * K)) + levels[j] = 2 * K + for j, rank, lo, hi in new: + out.append(dict(kind='idle', idx=idx, pair=j, rank=rank, source_level=lo, target_level=hi)) + idx += 1 + return out + + +def windows(schedule): + last, out, local = {}, {}, [] + for pos, e in enumerate(schedule): + k = e['kind'] + if k == 'local_cover_sweep': + local.append((pos, e['stage'], e['pair'])) + last[e['pair']] = pos + elif k == 'bridge': + last[e['dst']] = pos + last[e['src']] = pos + elif k == 'idle': + p, lo = e['pair'], last.get(e['pair'], -1) + out[e['idx']] = (p, e['rank'], sorted(s for q, s, pp in local if lo < q < pos and pp != p)) + else: + need(k == 'exchange', 'unknown schedule event %r' % k) + return out + + +def events_from_records(records, reverse): + """Expected local-program events of one orientation, from the record stream, following the + event layout of the selected nine-stage caller (global_k.py on main).""" + out = [] + rank = {x: z for op, x, y, c, f, z in records if op == 2} + for op, x, y, c, f, z in (reversed(records) if reverse else records): + r = int(reverse) + if op == 0: + old, new = (c, y) if reverse else (y, c) + out.append([0, x, old, new, f, r]) + elif op == 1: + out.append([1, x, y, -c if reverse else c, f, r]) + elif op == (3 if reverse else 2): + out.append([2, x, y, c, f, rank[x], r]) + else: + out.append([3, x, y, c, f, z, r]) + return out + + +def check(template, word, geo, records, local_profile): + v, R = word['v'], word['R'] + V2, n = 2 * v, 2 * v + R + res = {} + need(template['stages'] == 9 and template['replicas'] == 32 and template['h'] == 8, 'template shape') + stages, replicas = template['stages'], template['replicas'] + pairs = 4 + fam_per_replica = pairs * V2 + sched = template['schedule'] + sweeps = {e['stage']: e for e in sched if e['kind'] == 'local_cover_sweep'} + need(sorted(sweeps) == list(range(stages)), 'one local sweep per stage') + + # 1. the template's parent schedule equals main's recipe; windows by the selected hosting rule + res['schedule_equals_main_recipe'] = sched == nine_stage_schedule() + win = windows(sched) + published = {int(k): (p, r, sorted(st)) for k, (p, r, st) in template['hosting']['windows'].items()} + res['windows_rederived_equal'] = {k: x for k, x in win.items() if x[1] > 0} == published + res['windows'] = {k: list(x) for k, x in sorted(win.items())} + + # 2. helper widths from the literal word (8 - start-frame dimension; all end at FULL) + widths = [8 - geo.dim[word['start'][2 * v + h]] for h in range(R)] + need(all(geo.dim[word['final'][2 * v + h]] == 8 for h in range(R)), 'a helper does not end at FULL') + + # 3. slot list: every (stage, helper) occurrence exactly once, legal window, disjoint offsets + slots = template['hosting']['slots'] + seen = Counter((s, h) for idx, cp, off, w, s, h in slots) + res['slots'] = len(slots) + res['every_occurrence_once'] = (set(seen) == {(s, h) for s in range(stages) for h in range(R)} + and all(c == 1 for c in seen.values())) + used = defaultdict(list) + ok_window = ok_width = ok_copy = True + for idx, cp, off, w, s, h in slots: + ok_window &= idx in win and s in win[idx][2] + ok_width &= w == widths[h] + ok_copy &= 0 <= cp < V2 + used[idx, cp].append((off, w)) + disjoint = True + for (idx, cp), segs in used.items(): + segs.sort() + end = 0 + for off, w in segs: + disjoint &= off >= end and off + w <= win[idx][1] + end = off + w + res['stage_inside_window'] = ok_window + res['width_matches_word'] = ok_width + res['copy_in_range'] = ok_copy + res['offsets_disjoint_within_rank'] = disjoint + + # 4. remainders: every copy of every positive-rank child keeps rank - used + rem = Counter() + per_idx = {} + for idx, (p, r, st) in win.items(): + if r == 0: + continue + hist = Counter(r - sum(w for _, w in used.get((idx, cp), [])) for cp in range(V2)) + per_idx[idx] = {k: x for k, x in sorted(hist.items()) if k} + rem.update({k: x for k, x in hist.items() if k}) + published_rem = {int(k): {int(a): b for a, b in x.items()} for k, x in template['hosting']['remainders'].items()} + res['remainders_equal_published'] = per_idx == published_rem + res['idle_children_per_replica'] = dict(sorted(rem.items())) + + # 5. calls: 9 stages x 32 replicas, owners agree with slots and the data blocks; no banks + slot_of = {(s, h): (idx, cp, off, w) for idx, cp, off, w, s, h in slots} + calls = template['calls'] + res['calls'] = len(calls) + good_calls = len(calls) == stages * replicas and sorted({(c['stage'], c['replica']) for c in calls}) == [ + (s, r) for s in range(stages) for r in range(replicas)] + hosted = 0 + for c in calls: + s, rep, p = c['stage'], c['replica'], c['pair'] + sw = sweeps[s] + good_calls &= p == sw['pair'] and c['orientation'] == ('reverse' if sw['reverse'] else 'forward') + own = c['owners'] + good_calls &= len(own) == n + block = rep * fam_per_replica + p * V2 + data_fams = [] + for reg, (fam, route) in enumerate(own): + if reg < V2: + # data route of the selected caller: side flips in a reverse sweep + side = (reg // v) ^ int(sw['reverse']) + good_calls &= route == ['data', s, reg % v] and fam == block + side * v + reg % v + data_fams.append(fam) + elif (s, reg - V2) not in slot_of: + good_calls = False + else: + idx, cp, off, w = slot_of[s, reg - V2] + pidx = win[idx][0] + good_calls &= (route == ['hosted', idx, off, w] and fam == rep * fam_per_replica + pidx * V2 + cp + and pidx != p) + hosted += 1 + good_calls &= sorted(data_fams) == list(range(block, block + V2)) + res['owners_match_slots_and_blocks'] = good_calls + res['hosted_occurrences'] = hosted + # template bank counters (a count read from the template; the owners check already implies none) + res['banks'] = sum(template['banks_per_stage'].values()) + sum(template['hosting']['banks_per_stage'].values()) + res['emitted_local_events_count'] = len(calls) * len(records) + + # 6. local programs bound to the audited record stream (both orientations), and every call + # bound to the program of its orientation by its local_hash + lp = template['local_programs'] + res['local_programs_equal_records'] = all(lp[k] == events_from_records(records, k == 'reverse') + for k in ('forward', 'reverse')) + digest = {k: hashlib.sha256(json.dumps(lp[k], separators=(',', ':')).encode()).hexdigest() for k in lp} + res['calls_bound_to_local_programs'] = all(c['local_hash'] == digest[c['orientation']] for c in calls) + + # 7. whole paid profile = calls x local profile + replicas x idle remainders + whole = Counter() + for k, x in local_profile.items(): + whole[int(k)] += stages * replicas * x + for k, x in rem.items(): + whole[k] += replicas * x + res['whole_profile'] = dict(sorted(whole.items())) + res['rank_mass'] = sum(k * x for k, x in whole.items()) + res['deficit'] = template['m'] * template['live'] - res['rank_mass'] + return res diff --git a/research/r437-composed-bit-independent-audit/inputs/FINAL-R438-WORD.json.gz b/research/r437-composed-bit-independent-audit/inputs/FINAL-R438-WORD.json.gz new file mode 100644 index 0000000000..db621440ab Binary files /dev/null and b/research/r437-composed-bit-independent-audit/inputs/FINAL-R438-WORD.json.gz differ diff --git a/research/r437-composed-bit-independent-audit/inputs/R437-COMPOSED-WORD.json.gz b/research/r437-composed-bit-independent-audit/inputs/R437-COMPOSED-WORD.json.gz new file mode 100644 index 0000000000..c558a221dd Binary files /dev/null and b/research/r437-composed-bit-independent-audit/inputs/R437-COMPOSED-WORD.json.gz differ diff --git a/research/r437-composed-bit-independent-audit/inputs/R437-GLOBAL-TEMPLATE.json.gz b/research/r437-composed-bit-independent-audit/inputs/R437-GLOBAL-TEMPLATE.json.gz new file mode 100644 index 0000000000..df9238596d Binary files /dev/null and b/research/r437-composed-bit-independent-audit/inputs/R437-GLOBAL-TEMPLATE.json.gz differ diff --git a/research/r437-composed-bit-independent-audit/inputs/R437-RECORDS.bin.gz b/research/r437-composed-bit-independent-audit/inputs/R437-RECORDS.bin.gz new file mode 100644 index 0000000000..73de1d8d86 Binary files /dev/null and b/research/r437-composed-bit-independent-audit/inputs/R437-RECORDS.bin.gz differ diff --git a/research/r437-composed-bit-independent-audit/native.py b/research/r437-composed-bit-independent-audit/native.py new file mode 100644 index 0000000000..40c84677d5 --- /dev/null +++ b/research/r437-composed-bit-independent-audit/native.py @@ -0,0 +1,80 @@ +"""Exact rational projectors of the frames (second method for frame dimension and nesting). + +P_F is the orthogonal projector (form = dot/2, so dot-orthogonal) onto the Q-span of +frame F's E8 lines: P = L^T (L L^T)^-1 L for a row basis L. For a climb A -> B the native +transport identities P_A P_B = P_B P_A = P_A are checked exactly; with D_U the address-half +exchange [[I-U, U], [U, I-U]], they imply D_(P_B-P_A) D_(P_A) = D_(P_B) (written argument in +README), which is also checked literally on the changed receiver and SOURCE77 paths. +""" +from fractions import Fraction as Q + + +def matmul(a, b): + return [[sum(a[i][k] * b[k][j] for k in range(len(b))) for j in range(len(b[0]))] for i in range(len(a))] + + +def basis(rows): + out = [] + for r in rows: + v = [Q(x) for x in r] + for b, p in out: + if v[p]: + f = v[p] / b[p] + v = [x - f * y for x, y in zip(v, b)] + p = next((i for i, x in enumerate(v) if x), None) + if p is not None: + out.append((v, p)) + return [v for v, _ in out] + + +def inverse(m): + n = len(m) + a = [list(r) + [Q(int(i == j)) for j in range(n)] for i, r in enumerate(m)] + for c in range(n): + p = next(i for i in range(c, n) if a[i][c]) + a[c], a[p] = a[p], a[c] + inv = 1 / a[c][c] + a[c] = [x * inv for x in a[c]] + for i in range(n): + if i != c and a[i][c]: + f = a[i][c] + a[i] = [x - f * y for x, y in zip(a[i], a[c])] + return [r[n:] for r in a] + + +def projector(lines, frame, dim=8): + L = basis([lines[i] for i in frame]) + if not L: + return [[Q(0)] * dim for _ in range(dim)], 0 + G = matmul(L, [list(c) for c in zip(*L)]) + P = matmul(matmul([list(c) for c in zip(*L)], inverse(G)), L) + return P, len(L) + + +def D(U): + n = len(U) + I = [[Q(int(i == j)) for j in range(n)] for i in range(n)] + IU = [[I[i][j] - U[i][j] for j in range(n)] for i in range(n)] + return [IU[i] + U[i] for i in range(n)] + [U[i] + IU[i] for i in range(n)] + + +def check(word, climbs, geo, focus): + lines = [list(map(int, x)) for x in word['lines']] + cache = {} + + def P(f): + if f not in cache: + cache[f] = projector(lines, word['frames'][f]) + return cache[f] + rank_ok = all(P(f)[1] == geo.dim[f] and sum(P(f)[0][i][i] for i in range(8)) == geo.dim[f] + for f in {x for _, a, b, _ in climbs for x in (a, b)}) + pairs = sorted({(a, b) for _, a, b, _ in climbs}) + nest_ok = all(matmul(P(a)[0], P(b)[0]) == P(a)[0] and matmul(P(b)[0], P(a)[0]) == P(a)[0] for a, b in pairs) + d_ok = True + for a, b in focus: + pa, pb = P(a)[0], P(b)[0] + diff = [[pb[i][j] - pa[i][j] for j in range(8)] for i in range(8)] + d_ok &= matmul(D(diff), D(pa)) == D(pb) + return dict(frames_projected=len(cache), climb_pairs=len(pairs), projector_rank_equals_dim=rank_ok, + nested_projector_identity=nest_ok, focus_transitions=[list(x) for x in focus], + address_exchange_identity_on_focus=d_ok) diff --git a/research/r437-composed-bit-independent-audit/price.py b/research/r437-composed-bit-independent-audit/price.py new file mode 100644 index 0000000000..70b1f436a0 --- /dev/null +++ b/research/r437-composed-bit-independent-audit/price.py @@ -0,0 +1,94 @@ +"""Exact root bracket of the bit price on a paid child histogram (brief cross-check; cf. PR #3668). + +Price equation, as stated by the selected chain's moment engine on main +(research/e8-bit-carrier-skeleton/code/hub/e8-r740-replica32/code/engines/moment.py), with +the inherited 10^-16 bad-class fallback: + sum_r (r n_r)/(m W) (m/r)^a + (32 m N)/(10^16 W) m^a = 1, N = sum_r n_r. +c is the largest 10^-24 grid point below the root. The bounds below are separate rational +enclosures: atanh series for log with a geometric tail, Taylor series for exp with its tail. +""" +from fractions import Fraction as Q + + +def ln_bounds(x): + """Rational lower/upper bounds of ln(x) for rational x >= 1.""" + assert x >= 1 + k = 0 + while x >= 2: + x /= 2 + k += 1 + + def atanh2(y): + z = (y - 1) / (y + 1) + s, t = Q(0), z + for j in range(80): + s += t / (2 * j + 1) + t *= z * z + return 2 * s, 2 * (s + t / (161 * (1 - z * z))) + lo, hi = atanh2(x) + l2, u2 = atanh2(Q(2)) + return lo + k * l2, hi + k * u2 + + +def exp_bounds(x): + assert 0 <= x < 1 + s = t = Q(1) + for j in range(1, 30): + t = t * x / j + s += t + return s, s + t * x / 30 / (1 - x / 31) + + +def moment(hist, m, W, a): + lo = hi = Q(0) + N = sum(hist.values()) + terms = [(Q(r * n, m * W), Q(m, r)) for r, n in hist.items()] + [(Q(32 * m * N, 10**16 * W), Q(m))] + for p, base in terms: + l, u = ln_bounds(base) + lo += p * exp_bounds(a * l)[0] + hi += p * exp_bounds(a * u)[1] + return lo, hi + + +def bracket(hist, m, W, c): + lo_at_c = moment(hist, m, W, c) + next_grid = c + Q(1, 10**24) + at_next = moment(hist, m, W, next_grid) + return dict(c=str(c), next_grid=str(next_grid), moment_upper_at_c_below_one=lo_at_c[1] < 1, + moment_lower_at_next_grid_above_one=at_next[0] > 1) + + +def precision(cf, cb, children, maxchild, R, v=111, K=4, L=9, T=32, m=64, W=28416, local_adds=0): + """Precision fields of the inherited nine-stage invoice (main: global_k.py prefix bound and + #510 assemble9.py coefficient formula), as an envelope: every non-prefix term is bounded above + generously (route factors up to 2^40, ports up to 120, doubled), so the reported bit lengths + hold for any such values. The ROW constants 9909 + 252 and the ROW cap 20161 (assemble9.py) + are inherited, not derived here. The local payload-prefix cap 64 cf^3 cb^2 < 2^104 is the + one in the selected chain's columns_h.cpp/columns_k.cpp checkers.""" + prefix = 2 ** (6 * (K - 1)) * cf ** (K + 1) * cb ** K + depth = 1 + while not 2 * maxchild ** depth < m ** depth: + depth += 1 + + def others(V, route): + unit = L * T * local_adds + 6 * (K - 1) * V * T + cee = 9 * L * T + J = 8 * T * L * (2 * V + R) + 8 * (2 * K * V * T) + 2 * L * T * R + 2 * cee + high = 16 * (m * m + 1) ** 2 + selectors = 2 * L * T * ((W - 1) + R * m * (route + 144 + 2 + (m - 1) + m)) + return (unit + J * high + J * (W + 9) + children * (8 * m * m + 8 + 128 * (2 * m) ** 3) + + 16 * m ** 3 + cee + selectors + 1) + lo = prefix + others(v, 0) + hi = prefix + 2 * others(120, 2 ** 40) + two_lo = (lo + 1) ** depth * (children + 1) ** depth + two_hi = (hi + 1) ** depth * (children + 1) ** depth + pb = prefix.bit_length() + payload = 64 * cf ** 3 * cb ** 2 + row = depth * (m * m + 1) + 9909 + 252 + return dict(payload_prefix_bits=payload.bit_length(), payload_below_2_104=payload < 2 ** 104, + prefix_bits=pb, charged_prefix_bits=192 if pb <= 192 else 64 * ((pb + 63) // 64), + coefficient_bits=[lo.bit_length(), hi.bit_length()], + two_level_bits=[two_lo.bit_length(), two_hi.bit_length()], + charged_two_level_bits=512 if two_hi.bit_length() <= 512 else None, + halving_depth=depth, halving_inequality=[2 * maxchild ** depth, m ** depth], + row_coefficient=row, row_below_inherited_cap_20161=row < 20161) diff --git a/research/r437-composed-bit-independent-audit/records.py b/research/r437-composed-bit-independent-audit/records.py new file mode 100644 index 0000000000..4af4ad097f --- /dev/null +++ b/research/r437-composed-bit-independent-audit/records.py @@ -0,0 +1,99 @@ +"""Record-level binding: lower a bitE8/1+mut word to the local-call record stream and replay +records in both orientations. + +Record layout (six little-endian int32, as in the selected nine-stage caller's global_k.py on +main): MOVE (0, reg, old frame, new frame, rank increment, 0); ADD (1, dst, src, coef, frame, +section tag D1/A2/scatter3/B4/C5); COPY (2, reg, centre, reg frame, centre frame, copy rank); +ERASE (3, reg, centre, reg frame, centre frame, 0). The centre is register id 2v+R. +The lowering below is written from the word semantics alone: lazy nested climbs before each +gate, one ADD per operand, one COPY/ADD.../ERASE episode per retained total, final climbs. +""" +import struct +from collections import Counter + +from wordsem import need + +TAG = {'D': 1, 'A': 2, 'scatter': 3, 'B': 4, 'C': 5} + + +def lower(word, geo): + v, R = word['v'], word['R'] + n = 2 * v + R + centre = n + zero = [k for k, d in enumerate(geo.dim) if d == 0] + need(len(zero) == 1, 'zero frame') + zero = zero[0] + cur = list(word['start']) + out = [] + + def move(r, f): + if cur[r] != f: + out.append((0, r, cur[r], f, geo.dim[f] - geo.dim[cur[r]], 0)) + cur[r] = f + for sec in ('D', 'A', 'scatter', 'B', 'C'): + if sec == 'scatter': + for k, q in enumerate(word['ret']): + out.append((2, q, centre, cur[q], zero, geo.dim[cur[q]] - geo.dim[zero])) + for t, row in enumerate(word['scatter']): + if k in row: + out.append((1, v + t, centre, 1, zero, TAG[sec])) + out.append((3, q, centre, cur[q], zero, 0)) + continue + for f, d, srcs in word[sec]: + for r in [d] + list(srcs): + move(r, f) + for s in srcs: + out.append((1, d, s, 1, f, TAG[sec])) + for r in range(n): + move(r, word['final'][r]) + return out + + +def pack(records): + return b''.join(struct.pack('<6i', *r) for r in records) + + +def replay(word, geo, records, reverse): + """F2 replay of a record stream. Reverse orientation: records in reverse order, every MOVE + undone (a strict climb of the orthogonal complement), coefficients negated, COPY/ERASE + exchanged around the same centre. Returns (bad columns, profile, adds, copies, max + cancellation-free row l1 norm).""" + v, R = word['v'], word['R'] + n = 2 * v + R + centre = n + H = 8 + dim = (lambda f: H - geo.dim[f]) if reverse else (lambda f: geo.dim[f]) + cur = list(word['final'] if reverse else word['start']) + [-1] + val = [1 << i for i in range(n)] + [0] + hist, adds, copies, held = Counter(), 0, 0, None + norm = [1] * n + [0] # cancellation-free row l1 bound, as in the selected caller + maxnorm = 1 + for op, x, y, c, f, z in (reversed(records) if reverse else records): + if op == 0: + old, new = (c, y) if reverse else (y, c) + need(cur[x] == old and dim(new) - dim(old) == f > 0, 'MOVE out of order') + need(geo.nested(old, new) if not reverse else geo.nested(new, old), 'MOVE not nested') + cur[x] = new + hist[f] += 1 + elif op == 1: + need(x != y and x < n and cur[x] == cur[y] == f, 'ADD operands not at the common frame') + need(y != centre or held is not None, 'ADD from an empty centre') + need(x != held, 'ADD into the held register') + need(c in (1, -1), 'coefficient') + if c & 1: + val[x] ^= val[y] + norm[x] += abs(c) * norm[y] + maxnorm = max(maxnorm, norm[x]) + adds += 1 + elif op == (3 if reverse else 2): + need(held is None and y == centre and cur[x] == c and val[centre] == 0, 'COPY discipline') + held, cur[centre], val[centre], norm[centre] = x, f, val[x], norm[x] + hist[abs(dim(c) - dim(f))] += 1 + copies += 1 + else: + need(held == x and y == centre and cur[x] == c and cur[centre] == f and val[centre] == val[x], + 'ERASE discipline') + held, cur[centre], val[centre], norm[centre] = None, -1, 0, 0 + need(held is None and cur[:n] == list(word['start'] if reverse else word['final']), 'end frames') + bad = [i for i in range(n) if val[i] != (1 << i) ^ ((1 << (i - v)) if v <= i < 2 * v else 0)] + return bad, dict(sorted(hist.items())), adds, copies, maxnorm diff --git a/research/r437-composed-bit-independent-audit/verify.py b/research/r437-composed-bit-independent-audit/verify.py new file mode 100644 index 0000000000..8f33361c7d --- /dev/null +++ b/research/r437-composed-bit-independent-audit/verify.py @@ -0,0 +1,591 @@ +"""Independent exact word-level audit of PR #3647's composed R437 bit word. + +Usage (repository root): python3 -I -B research/r437-composed-bit-independent-audit/verify.py [--write] + +Inputs: from main, the selected #589 word, its selection9-p111.json hosting patterns and #1043's +FRAME-PATHS.json and CERTIFICATE.json; from PR #3647, the R438 (helper464 GL) word, the R437 word, +the R437 record stream and the hosted template, vendored under inputs/ (all sha256-pinned in +SOURCES.json). +Semantics: wordsem.py, records.py, hosting.py and price.py, written for this audit from the +selected #589 chain's sources on main (see README); nothing from PR #3647, #1043 or main is imported. +Without --write the computed result must equal the committed RESULT.json. +Standard library only. Sagar Thakrar (thakrarsagar), with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import collections +import copy +import gzip +import hashlib +import json +import os +import struct +import sys +import time + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.abspath(os.path.join(HERE, '..', '..')) +sys.path.insert(0, HERE) +from wordsem import (Geometry, Reject, bits, canonical, check_final_frames, check_identity, # noqa: E402 + check_pullback, forward, load, need, paths, profile, pullback, rebuild_DC, + reverse_orientation) +import compose # noqa: E402 +import hosting # noqa: E402 +import native # noqa: E402 +import price # noqa: E402 +import records # noqa: E402 +from compose import apply # noqa: E402 + +W589 = 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +PATHS1043 = 'research/bit-boundary-persistence/FRAME-PATHS.json' +R438 = 'research/r437-composed-bit-independent-audit/inputs/FINAL-R438-WORD.json.gz' +R437 = 'research/r437-composed-bit-independent-audit/inputs/R437-COMPOSED-WORD.json.gz' +RECORDS = 'research/r437-composed-bit-independent-audit/inputs/R437-RECORDS.bin.gz' +TEMPLATE = 'research/r437-composed-bit-independent-audit/inputs/R437-GLOBAL-TEMPLATE.json.gz' +SEL589 = 'research/e8-bit-p111-tuned/data/selection9-p111.json' +CERT1043 = 'research/bit-boundary-persistence/CERTIFICATE.json' +C_R437 = (868314126713557740143, 500000000000000000000000) +C_589 = (1733427039589844234749, 10**24) +C_1043 = (433544072119966441673, 250000000000000000000000) + + +def sha(path): + with open(os.path.join(ROOT, path), 'rb') as fh: + return hashlib.sha256(fh.read()).hexdigest() + + +def pins(): + src = json.load(open(os.path.join(HERE, 'SOURCES.json'))) + out = {} + for f in src['files'] + src['snapshot']: + path = f.get('path') or 'research/r437-composed-bit-independent-audit/' + f['local'] + if f.get('usage', 'input') == 'input' or 'local' in f: + need(sha(path) == f['sha256'], 'pin mismatch for %s' % path) + out[path] = f['sha256'] + return out + + +def adds(w): + c = {s: sum(len(g[2]) for g in w[s]) for s in 'DABC'} + c['scatter'] = sum(len(r) for r in w['scatter']) + c['total'] = sum(c.values()) + return c + + +def interface(w, geo): + """Hypotheses of the selected interleaved scalar-interface lemma (H1-H5) and its conclusion.""" + v, n = w['v'], 2 * w['v'] + w['R'] + y = lambda r: v <= r < 2 * v + out = {} + out['H1'] = not any(not y(g[1]) and any(y(s) for s in g[2]) for sec in 'DABC' for g in w[sec]) + out['H2'] = all(len(w['frames'][g[0]]) == 0 and y(g[1]) and all(s >= 2 * v for s in g[2]) for g in w['D']) + out['H3'] = (all(not y(g[1]) for g in w['A']) and all(2 * v <= q < n for q in w['ret']) + and all(y(g[1]) or all(not y(s) for s in g[2]) for g in w['B'])) + D, C = rebuild_DC(w) + out['H4_C_literal_reverse'] = C == w['C'] + out['D0_rebuilt'] = D == w['D'] + raw, _, _, _ = forward(w, geo, sections=('A', 'scatter', 'B'), frames_on=False) + ym, xm = ((1 << v) - 1) << v, (1 << v) - 1 + out['H5_V_identity'] = all(raw[v + t] & ym == 1 << (v + t) for t in range(v)) + out['U_block'] = all(raw[r] & ym == 0 for r in range(n) if not y(r)) + out['J_identity'] = all(raw[v + t] & xm == 1 << t for t in range(v)) + return out + + +def word_checks(name, w, geo): + """Primary forward method, reverse pull-back, entrywise agreement, reverse orientation.""" + v, n = w['v'], 2 * w['v'] + w['R'] + val, cur, climbs, copies = forward(w, geo) + check_final_frames(w, geo) + bad = check_identity(w, val) + col = pullback(w) + badp = check_pullback(w, col) + agree = all(((val[r] >> j) & 1) == ((col[j] >> r) & 1) for r in range(n) for j in range(n)) + rev = check_identity(w, reverse_orientation(w, geo)) + sw = {s: sum(1 for g in w[s] if g[1] < v) for s in 'DABC'} + return dict(columns=n, sources=v, helpers=w['R'], forward_bad_columns=len(bad), pullback_bad_columns=len(badp), + methods_agree_entrywise=agree, reverse_orientation_bad_columns=len(rev), + copy_ranks=[c[2] for c in copies], profile=profile(geo, climbs, copies), + mass=sum(k * x for k, x in profile(geo, climbs, copies).items()), + scalar_adds=adds(w), gates={s: len(w[s]) for s in 'DABC'}, source_writes=sw, + interface=interface(w, geo)), (val, climbs, copies) + + +def trace(w, akeys): + """Per gate (origin key): destination, frame, value after, operand values; C gates are keyed + by the A/B gate they literally reverse.""" + geo = Geometry(w) + v = w['v'] + zkeys = [k for sec, ks in (('A', akeys), ('B', [('B', i) for i in range(len(w['B']))])) + for k, g in zip(ks, w[sec]) if not (v <= g[1] < 2 * v)] + ckeys = [('C',) + k for k in reversed(zkeys)] + need(len(ckeys) == len(w['C']), 'C length') + out, climbs = {}, [] + keymap = {'A': akeys, 'B': [('B', i) for i in range(len(w['B']))], 'C': ckeys} + + def tr(ev, val, cur): + sec = ev[0] + if sec in keymap: + k = keymap[sec][ev[1]] + out[k] = (ev[3], ev[2], val[ev[3]], tuple(val[s] for s in ev[4]), ev[4]) + _, _, cl, _ = forward(w, geo, trace=tr) + # A move inside an edited window is dated by the last unchanged gate before it, so that a + # re-synthesized node is compared window by window and any move across an unchanged gate shows. + anchor = {} + for sec in ('A', 'B', 'C'): + last = None + for k in keymap[sec]: + if unchanged(k): + last = k + anchor[k] = k + else: + anchor[k] = ('window after', last) + for r, a, b, where in cl: + if where[0] in keymap: + climbs.append((r, a, b, anchor[keymap[where[0]][where[1]]])) + else: + climbs.append((r, a, b, where)) + return out, climbs + + +EDITED_589_A = {compose.E464_DEL, compose.E470_DEL, compose.E470_READ} | set(range(*compose.E464_NODE_AT)) + + +def unchanged(k): + if k[0] == 'C': + return unchanged(k[1:]) + return k[0] == 'B' or (k[0] == 'A' and k[1] not in EDITED_589_A) + + +def project(x, dead, ren): + y = 0 + for b in bits(x): + if b not in dead: + y |= 1 << ren(b) + return y + + +def compare(T0, T1, dead, ren, v): + """Aligned trace comparison of a control/edited word (T1) against a reference (T0).""" + clean = (1 << (2 * v)) - 1 + full_diff, clean_diff, dirt_cols, sw = [], [], set(), 0 + common = [k for k in T1 if k in T0] + for k in common: + d0, f0, x0, s0, r0 = T0[k] + d1, f1, x1, s1, r1 = T1[k] + need(ren(d0) == d1 and f0 == f1 and [ren(r) for r in r0] == list(r1), 'aligned gate %s differs in shape' % (k,)) + a = [project(x0, dead, ren)] + [project(s, dead, ren) for s in s0] + b = [x1] + list(s1) + if a != b: + full_diff.append(k) + for p, q in zip(a, b): + dirt_cols |= set(bits(p ^ q)) + if [p & clean for p in a] != [q & clean for q in b]: + clean_diff.append(k) + if d1 < v: + sw += 1 + return dict(aligned_gates=len(common), full_value_differences=sorted(full_diff, key=str), + clean_value_differences=len(clean_diff), differing_columns=sorted(dirt_cols), + source_write_gates_compared=sw) + + +def source_history(T, climbs, v): + acc = {s: [] for s in range(v)} + for k, (d, f, _, _, regs) in T.items(): + if k[0] == 'C': + continue + if d < v: + acc[d].append((str(k), f, 'write')) + for s in regs: + if s < v: + acc[s].append((str(k), f, 'read')) + cl = {s: [(str(k), a, b) for r, a, b, k in climbs if r == s] for s in range(v)} + return acc, cl + + +def history_diff(h0, h1, v): + out = {} + for s in range(v): + a, b = set(h0[s]), set(h1[s]) + if a != b: + out[s] = dict(removed=sorted(a - b), added=sorted(b - a)) + return out + + +def run(): + t0 = time.process_time() + res = {'status': None, 'pins': pins()} + w589 = load(os.path.join(ROOT, W589)) + r438 = load(os.path.join(ROOT, R438)) + r437 = load(os.path.join(ROOT, R437)) + fp = json.load(open(os.path.join(ROOT, PATHS1043))) + v = w589['v'] + geo = Geometry(w589) + for w in (r438, r437): + need(all(w[k] == w589[k] for k in ('lines', 'frames', 'scatter', 'v', 'h', 'form', 'format', 'coords', + 'ports_geom', 'punctured')), 'geometry or scatter changed') + res['frame_closure_memberships'] = geo.closure_checks() + res['frames'] = len(geo.frames) + + # Controls and composition, built literally from selected #589 + node = r438['A'][1985:1995] + c464, d464, ren464, k464 = apply(w589, node, do464=True) + c470, d470, ren470, k470 = apply(w589, node, do470=True) + comp, dcomp, rencomp, kcomp = apply(w589, node, do464=True, do470=True) + strip = lambda w: {k: x for k, x in w.items() if k != 'stats'} + res['composition'] = dict( + e464_node=node, + c464_equals_pr_R438_except_stats=strip(c464) == strip(r438), + composed_equals_pr_R437_except_stats=strip(comp) == strip(r437), + stats_589=w589['stats'], stats_pr_R438=r438['stats'], stats_pr_R437=r437['stats'], + canonical_sha256=dict( + w589=hashlib.sha256(canonical(w589)).hexdigest(), + pr_R438=hashlib.sha256(canonical(r438)).hexdigest(), + pr_R437=hashlib.sha256(canonical(r437)).hexdigest(), + c470_rebuilt=hashlib.sha256(canonical(c470)).hexdigest()), + edit_windows_589_A=dict(e464=[compose.E464_DEL, list(compose.E464_NODE_AT)], + e470=[compose.E470_DEL, compose.E470_READ])) + + words = [('selected589', w589), ('C464_pr_R438', r438), ('C470_rebuilt_1043', c470), ('R437_pr', r437)] + res['words'] = {} + side = {} + for name, w in words: + res['words'][name], side[name] = word_checks(name, w, geo) + _, cl589, _ = side['selected589'] + # second frame method: exact rational projectors for every climb of the R437 word; the changed + # paths (receiver 444, SOURCE77, GL node roles 340/241/349) also get the address-exchange identity + _, cl437, _ = side['R437_pr'] + focus = sorted({(a, b) for r, a, b, _ in cl437 if r in (444, 77, 340, 241, 349)}) + res['native'] = native.check(r437, cl437, geo, focus) + _, cl470, _ = side['C470_rebuilt_1043'] + res['frame_paths_1043'] = dict( + selected589_equals_baseline=[p for _, p in sorted(paths(w589, cl589).items())] == fp['baseline'], + c470_equals_candidate=[p for _, p in sorted(paths(c470, cl470).items())] == fp['candidate']) + prof = {k: res['words'][k]['profile'] for k, _ in words} + delta = lambda a, b: {r: prof[a].get(r, 0) - prof[b].get(r, 0) for r in sorted(set(prof[a]) | set(prof[b])) + if prof[a].get(r, 0) != prof[b].get(r, 0)} + d1, d2, d3 = (delta('C464_pr_R438', 'selected589'), delta('C470_rebuilt_1043', 'selected589'), + delta('R437_pr', 'selected589')) + res['profile_delta'] = dict(e464=d1, e470=d2, composed=d3, + additive={r: d1.get(r, 0) + d2.get(r, 0) for r in set(d1) | set(d2) + if d1.get(r, 0) + d2.get(r, 0)} == d3, + composed_vs_C464=delta('R437_pr', 'C464_pr_R438')) + + # Aligned traces: what each edit changes, and whether the edits interact + T589, C589 = trace(w589, [('A', i) for i in range(len(w589['A']))]) + T464, C464 = trace(c464, k464) + T470, C470 = trace(c470, k470) + T437, C437 = trace(r437, kcomp) + res['traces'] = dict( + e464_vs_589=compare(T589, T464, d464, ren464, v), + e470_vs_589=compare(T589, T470, d470, ren470, v), + composed_vs_589=compare(T589, T437, dcomp, rencomp, v), + composed_vs_C464=compare(T464, T437, [469], lambda r: r - (r > 469), v), + composed_vs_C470=compare(T470, T437, [464], lambda r: r - (r > 464), v)) + # Helper-dirt census of the retained totals at the scatter (the COPY sources), for scale: how + # much arbitrary dirt each capture already carries in #589, and which columns the edits swap. + def capture_dirt(w): + val = forward(w, geo, sections=('D', 'A'), frames_on=False)[0] + return [(q, [b for b in bits(val[q]) if b >= 2 * v]) for q in w['ret']] + cd589, cd437 = capture_dirt(w589), capture_dirt(r437) + need([rencomp(q) for q, _ in cd589] == [q for q, _ in cd437], 'retained totals do not correspond') + res['capture_dirt'] = dict( + selected589_columns={q: len(c) for q, c in cd589}, + R437_pr_columns={q: len(c) for q, c in cd437}, + selected589_totals_carrying_deleted_helpers={q: [b for b in c if b in dcomp] for q, c in cd589 + if any(b in dcomp for b in c)}, + changes_vs_589=[dict(total_589=q0, total_R437=q1, deleted_helper_columns_dropped=[b for b in c0 if b in dcomp], + removed=sorted(set(rencomp(b) for b in c0 if b not in dcomp) - set(c1)), + added=sorted(set(c1) - set(rencomp(b) for b in c0 if b not in dcomp))) + for (q0, c0), (q1, c1) in zip(cd589, cd437) + if [rencomp(b) for b in c0 if b not in dcomp] != c1]) + # SOURCE77 late read and source chronology + h589, sc589 = source_history(T589, C589, v) + h437, sc437 = source_history(T437, C437, v) + k_new = ('A470', 0) + d, f, after, (x77,), regs = T437[k_new] + res['source77'] = dict( + new_read=dict(frame=f, frame_lines=geo.frames[f], frame_dim=geo.dim[f], receiver=d, + source_value_is_clean_input=x77 == 1 << 77), + source77_climbs_589=[(str(k), a, b) for r, a, b, k in C589 if r == 77], + source77_climbs_R437=[(str(k), a, b) for r, a, b, k in C437 if r == 77], + receiver444_climbs_589=[(str(k), a, b) for r, a, b, k in C589 if r == 444], + receiver444_climbs_R437=[(str(k), a, b) for r, a, b, k in C437 if r == 444]) + res['source_chronology'] = dict( + all_source_climbs_identical=sc589 == {s: sc437[s] for s in range(v)}, + access_history_differences=history_diff(h589, h437, v)) + # Records consumed by PR #3647's hosting/invoice stage: byte equality with an independent + # lowering of the audited word, then record replay in both orientations. + with open(os.path.join(ROOT, RECORDS), 'rb') as fh: + raw = gzip.decompress(fh.read()) + mine = records.lower(r437, geo) + theirs = list(struct.iter_unpack('<6i', raw)) + fwd = records.replay(r437, geo, theirs, False) + rev = records.replay(r437, geo, theirs, True) + res['records'] = dict( + pr_stream_sha256=hashlib.sha256(raw).hexdigest(), pr_stream_bytes=len(raw), records=len(theirs), + independent_lowering_byte_equal=records.pack(mine) == raw, + kinds={k: x for k, x in sorted(collections.Counter(r[0] for r in theirs).items())}, + forward=dict(bad_columns=len(fwd[0]), profile=fwd[1], adds=fwd[2], copies=fwd[3], + cancellation_free_row_l1=fwd[4], bits=fwd[4].bit_length()), + reverse=dict(bad_columns=len(rev[0]), profile=rev[1], adds=rev[2], copies=rev[3], + cancellation_free_row_l1=rev[4], bits=rev[4].bit_length())) + res['mutants'] = mutants(w589, node, geo) + + # Stretch: hosted template -> whole paid profile -> price bracket (bounded; see README) + with open(os.path.join(ROOT, TEMPLATE), 'rb') as fh: + tpl = json.loads(gzip.decompress(fh.read())) + hres = hosting.check(tpl, r437, geo, theirs, res['words']['R437_pr']['profile']) + hres['template_canonical_sha256'] = hashlib.sha256(canonical(tpl)).hexdigest() + hres['template_source_record_sha256'] = tpl['source_record_sha256'] + res['hosting'] = hres + # hosting controls (each must break at least one hosting check) + hk = ('windows_rederived_equal', 'every_occurrence_once', 'stage_inside_window', 'offsets_disjoint_within_rank', + 'remainders_equal_published', 'owners_match_slots_and_blocks') + hmut = [] + slots0 = tpl['hosting']['slots'] + def overlap(sl): + first = {} + for i, x in enumerate(sl): + if (x[0], x[1]) in first: + sl[i] = x[:2] + [sl[first[x[0], x[1]]][2]] + x[3:] + return + first[x[0], x[1]] = i + for label, edit in ( + ('slot_moved_outside_window', lambda sl: sl.__setitem__(0, [6] + sl[0][1:])), + ('slot_offsets_overlap', overlap), + ('slot_dropped', lambda sl: sl.pop()), + ('idle_rank_changed', None)): + t2 = dict(tpl) + t2['hosting'] = dict(tpl['hosting'], slots=[list(x) for x in slots0]) + if edit: + edit(t2['hosting']['slots']) + else: + t2['schedule'] = [dict(e, rank=e['rank'] + 1) if e.get('idx') == 6 else e for e in tpl['schedule']] + try: + r2 = hosting.check(t2, r437, geo, theirs, res['words']['R437_pr']['profile']) + broken = [k for k in hk if not r2[k]] + (['whole_profile'] if r2['whole_profile'] != hres['whole_profile'] else []) + except Reject as e: + broken = ['rejected: %s' % e] + hmut.append(dict(mutant=label, rejected=bool(broken), broken=broken)) + res['hosting_mutants'] = hmut + need(tpl['m'] == 64 and tpl['live'] == 28416, 'template m/W differ from the inherited 64/28416') + F = price.Q + res['price'] = dict(R437=price.bracket(hres['whole_profile'], tpl['m'], tpl['live'], F(*C_R437))) + wp = hres['whole_profile'] + # price controls: relabel a single child of the whole profile; a worse child must break the + # bound at c, a better one the bound at the next grid point + res['price_mutants'] = [] + for label, src, dst, side in (('one_rank2_child_as_rank3', 2, 3, 'moment_upper_at_c_below_one'), + ('one_rank42_child_as_rank34', 42, 34, 'moment_lower_at_next_grid_above_one')): + bad = dict(wp) + bad[src] -= 1 + bad[dst] = bad.get(dst, 0) + 1 + b2 = price.bracket(bad, tpl['m'], tpl['live'], F(*C_R437)) + res['price_mutants'].append(dict(mutant=label, rejected=not (b2['moment_upper_at_c_below_one'] and + b2['moment_lower_at_next_grid_above_one']), + failing_bound=[k for k in ('moment_upper_at_c_below_one', + 'moment_lower_at_next_grid_above_one') + if not b2[k]], expected_failing_bound=side)) + local_adds = res['words']['R437_pr']['scalar_adds']['total'] + need(local_adds == res['records']['forward']['adds'] == 24208, 'local ADD count') + res['precision_R437'] = price.precision(res['records']['forward']['cancellation_free_row_l1'], + res['records']['reverse']['cancellation_free_row_l1'], + sum(wp.values()), max(wp), r437['R'], local_adds=local_adds) + res['precision_R437']['children'] = sum(wp.values()) + # positive control 1: selected #589 from main only (word -> local profile; selection9-p111.json + # patterns -> idle remainders on the same nine windows) must give the selected bit value + sel = json.load(open(os.path.join(ROOT, SEL589)))['bit'] + win = hosting.windows(hosting.nine_stage_schedule()) + idle589 = collections.Counter() + per_stage = collections.Counter() + legal = True + for idx, pat, copies in sel['patterns']: + idle589[win[idx][1] - sum(pat)] += copies + cover = collections.Counter() + capacity = collections.Counter() + for idx, pat, copies in sel['patterns']: + cover[idx] += copies + capacity[idx] += copies * len(pat) + for idx, w, st, cnt in sel['stages']: + legal &= st in win[idx][2] and w == 8 + per_stage[st] += cnt + capacity[idx] -= cnt + legal &= all(cover[idx] == 2 * v for idx, (p, r, st) in win.items() if r) and not +capacity and not -capacity + idle589 = {k: x for k, x in idle589.items() if k} + whole589 = collections.Counter() + for k, x in res['words']['selected589']['profile'].items(): + whole589[int(k)] += 288 * x + for k, x in idle589.items(): + whole589[k] += 32 * x + res['price']['selected589_control'] = dict( + idle_children_per_replica=dict(sorted(idle589.items())), stages_legal=legal, + every_stage_hosts_all_helpers=all(per_stage[st] == w589['R'] for st in range(9)), + whole_profile=dict(sorted(whole589.items())), + bracket=price.bracket(dict(whole589), 64, 28416, F(*C_589))) + # positive control 2: #1043's published hosted profile splits over the rebuilt E470 local profile + certj = json.load(open(os.path.join(ROOT, CERT1043))) + cert = certj['hosted']['candidate']['invoice']['bit_profile'] + lc = certj['hosted']['candidate']['parent']['local_checks']['forward'] + c470w = res['words']['C470_rebuilt_1043'] + res['c1043_certificate_vs_rebuilt'] = dict( + local_profile_equal={int(k): x for k, x in lc['profile'].items()} == {int(k): x for k, x in c470w['profile'].items()}, + adds_equal=lc['adds'] == c470w['scalar_adds']['total'], + gates_equal=certj['native']['candidate']['interface']['gates'] == c470w['gates']) + cert = {int(k): x for k, x in cert.items()} + loc470 = {int(k): x for k, x in res['words']['C470_rebuilt_1043']['profile'].items()} + idle470 = {k: cert.get(k, 0) - 288 * loc470.get(k, 0) for k in set(cert) | set(loc470)} + res['price']['c1043_control'] = dict( + idle_children_per_replica={k: x // 32 for k, x in sorted(idle470.items()) if x}, + split_exact=all(x >= 0 and x % 32 == 0 for x in idle470.values()), + bracket=price.bracket(cert, 64, 28416, F(*C_1043))) + # Arithmetic split of the profile published in PR #3647's README/COMPOSED-PROOF into 288 local + # calls plus a per-replica idle remainder; hosting.check above rederives the remainder itself. + claimed = {1: 380160, 2: 400864, 3: 22176, 4: 26592, 5: 29376, 6: 17376, 7: 26496, 34: 64, 42: 352} + loc = {int(k): x for k, x in res['words']['R437_pr']['profile'].items()} + calls, replicas = 9 * 32, 32 + idle = {r: claimed.get(r, 0) - calls * loc.get(r, 0) for r in sorted(set(claimed) | set(loc))} + need(all(x >= 0 and x % replicas == 0 for x in idle.values()), 'claimed profile does not split') + res['whole_profile_split'] = dict( + claimed=claimed, local_calls=calls, replicas=replicas, + idle_children_per_replica={r: x // replicas for r, x in idle.items() if x}, + rank_mass=sum(r * x for r, x in claimed.items()), live_data=28416, + deficit=64 * 28416 - sum(r * x for r, x in claimed.items()), + helper_occurrences=calls * r437['R']) + drop = lambda gates, q: [[f, d - (d > q), [x - (x > q) for x in srcs if x != q]] for f, d, srcs in gates] + res['compensation_facts'] = dict( + e470_D0_is_C464_D0_with_column_deleted=drop(c464['D'], 469) == r437['D'], + e464_D0_is_589_D0_with_column_deleted=drop(w589['D'], 464) == c464['D'], + e470_D0_is_589_D0_with_column_deleted=drop(w589['D'], 470) == c470['D']) + res['cpu_seconds_note'] = 'not recorded (platform dependent)' + ok = (all(x['forward_bad_columns'] == 0 and x['pullback_bad_columns'] == 0 and x['methods_agree_entrywise'] + and x['reverse_orientation_bad_columns'] == 0 and all(x['interface'].values()) + for x in res['words'].values()) + and res['composition']['c464_equals_pr_R438_except_stats'] + and res['composition']['composed_equals_pr_R437_except_stats'] + and all(res['frame_paths_1043'].values()) and res['profile_delta']['additive'] + and all(t['clean_value_differences'] == 0 for t in res['traces'].values()) + and res['traces']['composed_vs_C464']['full_value_differences'] == [] + and res['traces']['e470_vs_589']['full_value_differences'] == [] + and res['traces']['composed_vs_C470']['full_value_differences'] == res['traces']['e464_vs_589']['full_value_differences'] + and res['source_chronology']['all_source_climbs_identical'] + and res['source77']['new_read']['frame'] == 186 and res['source77']['new_read']['source_value_is_clean_input'] + and res['source77']['source77_climbs_589'] == res['source77']['source77_climbs_R437'] + and all(m['rejected'] == m['expect_rejected'] for m in res['mutants']) + and res['whole_profile_split']['rank_mass'] == 1808352 and res['whole_profile_split']['deficit'] == 10272 + and res['whole_profile_split']['helper_occurrences'] == 125856 + and res['records']['independent_lowering_byte_equal'] + and res['records']['pr_stream_sha256'] == 'caeb2eb0e417992788c32c1f5812ada60b46d1dfdba9f4ac376299b2dede13cb' + and all(res['records'][o]['bad_columns'] == 0 and res['records'][o]['profile'] == res['words']['R437_pr']['profile'] + for o in ('forward', 'reverse')) + and all(res['hosting'][k] for k in ('windows_rederived_equal', 'every_occurrence_once', 'stage_inside_window', + 'width_matches_word', 'copy_in_range', 'offsets_disjoint_within_rank', + 'remainders_equal_published', 'owners_match_slots_and_blocks', + 'local_programs_equal_records', 'calls_bound_to_local_programs')) + and res['hosting']['banks'] == 0 and res['hosting']['hosted_occurrences'] == 125856 + and res['hosting']['whole_profile'] == res['whole_profile_split']['claimed'] + and res['hosting']['template_source_record_sha256'] == res['records']['pr_stream_sha256'] + # canonical template content digest published in PR #3647's EXPECTED.json + and res['hosting']['template_canonical_sha256'] == '2e868ff427654e47df34779299545c53aa05b8c96697ee126e80e7bc6a50990a' + and all(b['moment_upper_at_c_below_one'] and b['moment_lower_at_next_grid_above_one'] + for b in (res['price']['R437'], res['price']['selected589_control']['bracket'], + res['price']['c1043_control']['bracket'])) + and res['price']['selected589_control']['stages_legal'] + and res['price']['selected589_control']['every_stage_hosts_all_helpers'] + and res['price']['c1043_control']['split_exact'] + and res['hosting']['schedule_equals_main_recipe'] + and all(res['native'][k] for k in ('projector_rank_equals_dim', 'nested_projector_identity', + 'address_exchange_identity_on_focus')) + and all(m['rejected'] and m['failing_bound'] == [m['expected_failing_bound']] for m in res['price_mutants']) + and all(res['c1043_certificate_vs_rebuilt'].values()) + and all(m['rejected'] for m in res['hosting_mutants']) + and res['precision_R437']['prefix_bits'] == 177 and res['precision_R437']['coefficient_bits'] == [177, 177] + and res['precision_R437']['two_level_bits'] == [393, 393] and res['precision_R437']['charged_two_level_bits'] == 512 + and res['precision_R437']['row_coefficient'] == 18355 and res['precision_R437']['halving_depth'] == 2 + and res['precision_R437']['row_below_inherited_cap_20161'] and res['precision_R437']['payload_below_2_104']) + res['status'] = 'PASS_INDEPENDENT_R437_WORD_AUDIT' if ok else 'FAIL' + return res, time.process_time() - t0 + + +def mutants(w589, node, geo): + out = [] + v = w589['v'] + T589, C589 = trace(w589, [('A', i) for i in range(len(w589['A']))]) + sc589 = source_history(T589, C589, v)[1] + + def judge(label, w, keys, expect, note): + reason, ident = None, None + try: + r, _ = word_checks(label, w, geo) + ident = r['forward_bad_columns'] == 0 + if r['forward_bad_columns'] or r['pullback_bad_columns']: + reason = 'identity fails on %d columns' % r['forward_bad_columns'] + elif not all(r['interface'].values()): + reason = 'interface fails: ' + ','.join(k for k, x in r['interface'].items() if not x) + else: + T, C = trace(w, keys) + sc = source_history(T, C, v)[1] + if sc != {s: sc589[s] for s in range(v)}: + moved = [s for s in range(v) if sc[s] != sc589[s]] + reason = 'source chronology changed for sources %s' % moved + except Reject as e: + reason = 'legality: ' + str(e) + out.append(dict(mutant=label, rejected=reason is not None, reason=reason, expect_rejected=expect, note=note, + legal_and_f2_identity=ident)) + + comp, dead, ren, keys = apply(w589, node, do464=True, do470=True) + m = copy.deepcopy(comp) + m['D'] = [] + judge('drop_D0', m, keys, True, 'no frame-zero dirt compensation') + m = copy.deepcopy(comp) + m['C'] = [] + judge('drop_cleanup_C', m, keys, True, 'no literal reverse cleanup') + # stale compensation/cleanup: selected #589's D0 and C with the two deleted helpers' operands + # and gates removed and the survivors renamed (what reuse of the old D0/C would give) + def project_gates(gates): + g2 = [] + for f, d, srcs in gates: + if d in dead: + continue + ss = [ren(x) for x in srcs if x not in dead] + if ss: + g2.append([f, ren(d), ss]) + return g2 + m = copy.deepcopy(comp) + m['D'] = project_gates(w589['D']) + judge('stale_D0_from_589', m, keys, True, 'selected D0 reused with the deleted helpers dropped') + m = copy.deepcopy(comp) + m['C'] = project_gates(w589['C']) + judge('stale_C_from_589', m, keys, True, 'selected C reused with the deleted helpers dropped') + m, _, _, k = apply(w589, node, do464=True, do470=True, read=[79, 444, [77]]) + judge('late_read_at_frame79', m, k, True, 'replacement read at the removed carrier frame 79 (descends SOURCE77)') + m, _, _, k = apply(w589, node, do464=True, do470=True, read_at=compose.E470_DEL - 1) + judge('early_read_at_birth', m, k, True, 'replacement read moved to the removed birth position (before A[426])') + m, _, _, k = apply(w589, node, do464=True, do470=True, read=[186, 444, [77]], read_at=None) + judge('positive_control_composed', m, k, False, 'the composed word itself') + # revert one deletion: E470 read removed outright (receiver never gets SOURCE77) + m, _, _, k = apply(w589, node, do464=True, do470=True, read='drop') + judge('drop_replacement_read', m, k, True, 'helper470 deleted without the replacement read') + # naive helper464 deletion: old node with the 464 operand dropped instead of the GL node + naive = [[f, d, [s for s in srcs if s != 464]] for f, d, srcs in compose.E464_OLD_NODE] + m, _, _, k = apply(w589, naive, do464=True, do470=True) + judge('naive_464_deletion', m, k, True, 'old node kept, helper464 operand dropped (no GL re-synthesis)') + for j in range(len(node)): + m, _, _, k = apply(w589, node[:j] + node[j + 1:], do464=True, do470=True) + judge('gl_node_drop_gate_%d' % j, m, k, True, 'one of the ten GL node gates removed') + return out + + +def main(): + res, cpu = run() + path = os.path.join(HERE, 'RESULT.json') + text = json.dumps(res, indent=1, sort_keys=True, default=list) + '\n' + if '--write' in sys.argv: + open(path, 'w').write(text) + else: + need(os.path.exists(path) and open(path).read() == text, 'computed result differs from RESULT.json') + print(res['status'], 'cpu %.1fs' % cpu) + return 0 if res['status'].startswith('PASS') else 1 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/research/r437-composed-bit-independent-audit/wordsem.py b/research/r437-composed-bit-independent-audit/wordsem.py new file mode 100644 index 0000000000..e3076362e6 --- /dev/null +++ b/research/r437-composed-bit-independent-audit/wordsem.py @@ -0,0 +1,308 @@ +"""Independent stdlib semantics of a bitE8/1+mut word (format of selected #589). + +Written from scratch for this audit from the format description in the selected +#589 package on main (research/e8-bit-p111-tuned/code/xcheck_p.py docstring, +code/pwordl.py builder); no code is imported from any audited package. + +Registers: sources 0..v-1, targets v..2v-1, helpers 2v..2v+R-1. A gate +[f, d, srcs] first moves every operand to frame f (a strict, nested climb when +it is elsewhere) and then sets d <- d + sum(srcs) over F2. The scatter +snapshots the retained helpers `ret` and adds the listed snapshots to targets. +Frames are spans over Q of their listed E8 lines (ham coordinates, form dot/2). +""" +import gzip +import json +import math +from collections import Counter +from fractions import Fraction + + +class Reject(Exception): + pass + + +def need(ok, msg): + if not ok: + raise Reject(msg) + + +def load(path): + with open(path, 'rb') as fh: + return json.loads(gzip.decompress(fh.read())) + + +def canonical(word): + return json.dumps(word, sort_keys=True, separators=(',', ':')).encode() + + +def perp_basis(vectors, dim=8): + """Integer basis of {u : u.x = 0 for all x in vectors} (Euclidean dot).""" + rows = [[Fraction(a) for a in x] for x in vectors] + piv, r = [], 0 + for col in range(dim): + p = next((i for i in range(r, len(rows)) if rows[i][col]), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + inv = 1 / rows[r][col] + rows[r] = [a * inv for a in rows[r]] + for i in range(len(rows)): + if i != r and rows[i][col]: + f = rows[i][col] + rows[i] = [a - f * b for a, b in zip(rows[i], rows[r])] + piv.append(col) + r += 1 + out = [] + for free in (c for c in range(dim) if c not in piv): + vec = [Fraction(0)] * dim + vec[free] = Fraction(1) + for row, pc in zip(rows[:r], piv): + vec[pc] = -row[free] + den = 1 + for a in vec: + den = den * a.denominator // math.gcd(den, a.denominator) + out.append([int(a * den) for a in vec]) + return r, out + + +class Geometry: + """Rational frame dimensions, nesting and closure computed from the lines.""" + + def __init__(self, word): + self.lines = [list(map(int, x)) for x in word['lines']] + self.frames = [list(f) for f in word['frames']] + self.dim, self.perp = [], [] + for f in self.frames: + d, pb = perp_basis([self.lines[i] for i in f]) + self.dim.append(d) + self.perp.append(pb) + self._nest = {} + + def inside(self, line, k): + x = self.lines[line] + return all(sum(a * b for a, b in zip(x, u)) == 0 for u in self.perp[k]) + + def nested(self, a, b): + key = (a, b) + if key not in self._nest: + self._nest[key] = all(self.inside(i, b) for i in self.frames[a]) + return self._nest[key] + + def closure_checks(self): + v = len(self.lines) + n = 0 + for k, f in enumerate(self.frames): + inside = [i for i in range(v) if self.inside(i, k)] + need(inside == sorted(f), 'frame %d is not closed in the live lines' % k) + n += v + return n + + +def bits(mask): + while mask: + b = mask & -mask + yield b.bit_length() - 1 + mask ^= b + + +def forward(word, geo, sections=('D', 'A', 'scatter', 'B', 'C'), frames_on=True, trace=None): + """Forward symbolic replay over F2. Register r starts as the column bitset 1 << r, so one + pass covers every input column, including arbitrary (dirty) helper contents. Returns final + values, final frames, every frame climb (register, old, new, position) and the COPY frames. + trace(event, values, frames) is called after every gate when given.""" + v, R = word['v'], word['R'] + n = 2 * v + R + need(len(word['start']) == n and len(word['final']) == n, 'start/final length') + cur = list(word['start']) + val = [1 << r for r in range(n)] + climbs = [] # (register, old frame, new frame, position) + copies = [] + pos = 0 + if frames_on: + for s in range(v): + need(geo.frames[cur[s]] == [s] and geo.dim[cur[s]] == 1, 'source %d does not start at its line' % s) + for r in range(v, n): + need(geo.dim[cur[r]] == 0, 'register %d does not start at the zero frame' % r) + + def move(r, f, where): + if cur[r] == f: + return + need(geo.nested(cur[r], f) and geo.dim[cur[r]] < geo.dim[f], + 'illegal climb of register %d from frame %d to %d at %s' % (r, cur[r], f, where)) + climbs.append((r, cur[r], f, where)) + cur[r] = f + + for sec in sections: + if sec == 'scatter': + need(len(word['scatter']) == v, 'scatter rows') + if frames_on: + need(all(geo.dim[cur[v + t]] == 0 for t in range(v)), 'a target left the zero frame before the scatter') + snap = [val[q] for q in word['ret']] + for k, q in enumerate(word['ret']): + need(2 * v <= q < n, 'retained register is not a helper') + copies.append((q, cur[q], geo.dim[cur[q]])) + for t, row in enumerate(word['scatter']): + for k in row: + val[v + t] ^= snap[k] + if trace: + trace(('scatter', None, None, None), val, cur) + continue + for i, g in enumerate(word[sec]): + need(len(g) == 3, 'malformed gate') + f, d, srcs = g + regs = [d] + list(srcs) + need(srcs and len(set(regs)) == len(regs) and all(0 <= r < n for r in regs), 'bad operands %s[%d]' % (sec, i)) + need(0 <= f < len(word['frames']), 'frame id') + if frames_on: + for r in regs: + move(r, f, (sec, i)) + acc = 0 + for s in srcs: + acc ^= val[s] + val[d] ^= acc + if trace: + trace((sec, i, f, d, tuple(srcs)), val, cur) + if frames_on: + for r in range(n): + move(r, word['final'][r], ('final', r)) + return val, cur, climbs, copies + + +def check_identity(word, val): + v, R = word['v'], word['R'] + n = 2 * v + R + bad = [r for r in range(n) if val[r] != ((1 << r) | ((1 << (r - v)) if v <= r < 2 * v else 0))] + return bad + + +def check_final_frames(word, geo): + v, R = word['v'], word['R'] + n = 2 * v + R + full = [k for k, d in enumerate(geo.dim) if d == 8] + need(len(full) == 1, 'exactly one full frame') + for r in list(range(v)) + list(range(2 * v, n)): + need(geo.dim[word['final'][r]] == 8, 'final frame of %d is not full' % r) + for t in range(v): + lt = geo.lines[t] + perp = [i for i in range(v) if sum(a * b for a, b in zip(geo.lines[i], lt)) == 0] + need(geo.frames[word['final'][v + t]] == perp, 'target %d final frame is not t-perp' % t) + return full[0] + + +def pullback(word, sections=('D', 'A', 'scatter', 'B', 'C')): + """Second method: transpose action in reverse order. col[j] = set of outputs + depending on input j (bitset over registers).""" + v, R = word['v'], word['R'] + n = 2 * v + R + col = [1 << r for r in range(n)] + for sec in reversed(sections): + if sec == 'scatter': + for t, row in enumerate(word['scatter']): + for k in row: + q = word['ret'][k] + col[q] ^= col[v + t] + continue + for f, d, srcs in reversed(word[sec]): + cd = col[d] + for s in srcs: + col[s] ^= cd + return col + + +def check_pullback(word, col): + v, R = word['v'], word['R'] + n = 2 * v + R + return [j for j in range(n) if col[j] != ((1 << j) | ((1 << (v + j)) if j < v else 0))] + + +def reverse_orientation(word, geo): + """Literal reverse orientation: gates in reverse order, starting at the final frames; + every move is a nested strict descent (a climb of the orthogonal complement).""" + v, R = word['v'], word['R'] + n = 2 * v + R + cur = list(word['final']) + val = [1 << r for r in range(n)] + + def move(r, f, where): + if cur[r] == f: + return + need(geo.nested(f, cur[r]) and geo.dim[f] < geo.dim[cur[r]], + 'illegal reverse move of %d from %d to %d at %s' % (r, cur[r], f, where)) + cur[r] = f + + for sec in ('C', 'B', 'scatter', 'A', 'D'): + if sec == 'scatter': + # mirror of the forward scatter: targets descend to the zero frame, each retained + # helper to the frame of its last A gate (where the forward COPY reads it) + zero = [k for k, d in enumerate(geo.dim) if d == 0][0] + for t in range(v): + move(v + t, zero, ('scatter', t)) + for q in word['ret']: + last = [g[0] for g in word['A'] if q == g[1] or q in g[2]] + need(last, 'retained helper %d is never written in A' % q) + move(q, last[-1], ('scatter', q)) + snap = [val[q] for q in word['ret']] + for t, row in enumerate(word['scatter']): + for k in row: + val[v + t] ^= snap[k] + continue + for i in range(len(word[sec]) - 1, -1, -1): + f, d, srcs = word[sec][i] + for r in [d] + list(srcs): + move(r, f, (sec, i)) + acc = 0 + for s in srcs: + acc ^= val[s] + val[d] ^= acc + for r in range(n): + move(r, word['start'][r], ('start', r)) + return val + + +def profile(geo, climbs, copies): + h = Counter() + for r, a, b, _ in climbs: + h[geo.dim[b] - geo.dim[a]] += 1 + for q, f, d in copies: + h[d] += 1 + return dict(sorted(h.items())) + + +def paths(word, climbs): + n = 2 * word['v'] + word['R'] + p = {r: [word['start'][r]] for r in range(n)} + for r, a, b, where in climbs: + p[r].append(b) + return p + + +def rebuild_DC(word): + """D0 from the raw word's helper part of each target; C as the literal reverse of the + source/helper-destination A/B gates at the full frame (pwordl.build convention).""" + v, R = word['v'], word['R'] + n = 2 * v + R + val = [1 << r for r in range(n)] + for sec in ('A', 'scatter', 'B'): + if sec == 'scatter': + snap = [val[q] for q in word['ret']] + for t, row in enumerate(word['scatter']): + for k in row: + val[v + t] ^= snap[k] + continue + for f, d, srcs in word[sec]: + acc = 0 + for s in srcs: + acc ^= val[s] + val[d] ^= acc + hmask = ((1 << R) - 1) << (2 * v) + zero = [k for k, f in enumerate(word['frames']) if not f] + full = [k for k, f in enumerate(word['frames']) if len(f) == v] + need(len(zero) == 1 and len(full) == 1, 'zero/full frame ids') + D = [] + for t in range(v): + m = val[v + t] & hmask + if m: + D.append([zero[0], v + t, list(bits(m))]) + # literal reverse of A then B, restricted to source/helper destinations + C = [[full[0], d, list(s)] for f, d, s in reversed(word['A'] + word['B']) if not (v <= d < 2 * v)] + return D, C