diff --git a/research/staged-644-660-independent-audit/README.md b/research/staged-644-660-independent-audit/README.md new file mode 100644 index 0000000000..bfc15a07ca --- /dev/null +++ b/research/staged-644-660-independent-audit/README.md @@ -0,0 +1,408 @@ +# Independent audit of PR3605's staged 644/660 words + +PR3605 replaces eight early raw helper writes with four later donor releases, +so that helpers 644 and 660 drop from width 8 to width 7. This package checks +that change with a separately written exact interpreter, using the unchanged +parent words as the single-change control. **The changed words pass at head +`3efbb5de` for both providers**: they are exact identities, their cleanup is the +literal inverse, and their binary frames give exactly the claimed profile and +widths. A pass makes these words an independently checked local input for the +open staged-width chain that reuses them unchanged. It does not cover the +retimed words of #3642/#3653/#3682, the native phases of the new entrance +frame, or any owner journal. Those remain load-bearing. + +Reproduce (standard library, about 1–2 min): +`python3 -I -B research/staged-644-660-independent-audit/verify.py && python3 -I -B research/staged-644-660-independent-audit/root.py` + +In detail, the changed `base` and `extra` words are exact arbitrary-dirty +identities in both orientations, with 632 independent inputs and 91 private +buffers. Their chronological binary frames give the local profile +`{1:2433,2:724,3:228,4:102,5:20,8:8} -> {1:2439,2:726,3:224,4:102,5:20,8:8}` +and the helper widths `8:99 -> 97`, `7:50 -> 52`. For PR3605's fourth claim, +the root, the check is narrower: exact arithmetic confirms the published +PR3605 and PR3148 root brackets **on their published histograms**, and recounts +PR3605's idle histogram from its aggregate owner witness, with the witness's +windows taken as published. + +This is a finite exact **audit** of one local supplier change. It makes no κ +claim and no frontier change, and it admits none of the PRs named below. It +does not check native Gaussian phases, owner journals, complete admission or +the inherited all-size hypotheses (see Scope). The selected record stays +`0.001672660197076918`. + +## What was audited + +Audited object: RossRichardson's +[PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), head +`3efbb5de06a49ffeea6684482f2d3fe48cdca3fb`, package +`research/staged-644-660-width-reduction`. In its two words, eight early raw +helper-to-target writes (old `B184..187` for helper 644, `B216..219` for 660) +are replaced by four donor releases at `span(429,30)`: `640 += 2*644` and +`496 -= 2*644` before old B599, and `656 -= 660` and `520 -= 2*660` before +old B647. Helpers 644 and 660 then enter at `span(429,30)` instead of `span(30)` +and keep FULL terminals. The single-change control is dcharb78's unchanged +[PR3133](https://github.com/CrocSwap/integer-mult-bounds/pull/3133) parent words +(`51eb9c4e`, byte-identical on main). The root control is Jeremy Diviney's merged +[PR3148](https://github.com/CrocSwap/integer-mult-bounds/pull/3148) (`f2927a4b`). + +**Who consumes these words** (GitHub API, 2026-10-18, heads re-checked before +submission): + +- *Unchanged reuse.* #3624 `515a7c44`, #3626 `659fd5e7` and #3633 `72c268f1` add + word blobs `dc6d321b`/`78e7b2bb` and record blobs `042dbc69`/`67f04ae3`. The + same blobs sit inside #3638 `d62e1acd`'s vendored `PR3624-SOURCE.tar.gz` and + #3630 `bcac7fe0`'s `PR3605-SOURCES.tar.gz`. For these PRs, the audited words + are the supplier words. +- *Parent only.* #3642 `044d24f1` (roger-sato, T530) and #3653 + `607a09ff` (rohanarun, T488, vendoring #3642) carry the same STAGED blobs, but + their claims run `RETIMED644-660` words (`d69125e0`/`f3c580b0`). #3682 + `431e6c60` (zxv, T360) also vendors the STAGED blobs and runs its own + `DELAYED` words (`7ccd0962`/`3f1fb471`), which apply the same two commuting + release retimings to different bytes. **None of these retimed words is + checked here**; only their STAGED parent is. #3653 and #3682 report the same + endpoint, the highest among these staged-width claims. + +PR3605's own semantic check runs the pinned inherited interpreter +(`audit_local.py`). This package supplies a separately implemented check of +the STAGED words. It does not check any of these PRs' own owner journals or +roots. Concurrent work, none of which re-implements the word semantics: + +- #3659 (jwr404) adds the published PR3605 T740 histogram and compares its + root with 0.00173 and the selected κ; #3661 does the same for the T450 + allocation. +- #3677 (jwr404) checks only the arithmetic of the published RETIMED profile + (rank mass 5,135, lower moment), not the RETIMED words. +- #3681 (roger-sato, `9f781394`) replays the complete PR3605 wrapper with a + fresh retained bootstrap. It runs the inherited code, native chain included, + so it is a full replay but not an independent check. It is not reviewed here. + +This package's distinct parts are the independent word semantics, the PR3148 +delta attribution, the aggregate-witness recount and the sensitivity analysis. + +| Quantity (each provider) | PR3133 parent (control) | PR3605 changed word | +|---|---|---| +| Local profile | `1:2433, 2:724, 3:228, 4:102, 5:20, 8:8` | `1:2439, 2:726, 3:224, 4:102, 5:20, 8:8` | +| Helper widths | `4:26, 5:2, 6:18, 7:50, 8:99, 9:213` | `4:26, 5:2, 6:18, 7:52, 8:97, 9:213` | +| Inputs / private buffers | 632 / 91 | 632 / 91 | +| Forward (dirty buffers), dual, reverse pull-back | PASS | PASS | +| Cleanup equals the literal inverse | yes | yes | + +Per call, the profile changes by +6 rank-1, +2 rank-2 and −4 rank-3 children +(local rank mass −2). The change is confined to exactly six registers, and +each register's change equals PROOF.md's written invoice: + +- pivots 644/660: +1 rank-2, −1 rank-3; +- first donors 640/656: +1 rank-1, +1 rank-2, −1 rank-3; +- second donors 496/520: +2 rank-1, −1 rank-2. + +Applying either helper's edit alone keeps the identity and moves the profile by ++3 rank-1, +1 rank-2 and −2 rank-3 children. The two helpers' shares are +therefore separable and additive. + +## Method and independence + +The registered verifiers (`audit_core.py`, `verify.py`, `root.py`) import only +the standard library. Nothing is imported or copied from the audited authors' +code (the PR3133/PR3605 producers, cleanup generators or the inherited +`audit_local.py`). The word format and contract were read from those pinned +sources. `root.py`'s aggregate legality checks re-implement, without importing +it, every check of PR3605's `owners/verify_aggregate.py` except the two derived +from the source template (the literal T37 order, and the window classes and bin +counts computed by `owner.windows`). + +The checks are not independent of every earlier audit, though. +`audit_core.py`'s frame bill and free-word structure re-implement, without +importing, Arham Tahir's merged `coupled-carrier-independent-audit/verify.py`. +That includes the point-set spans, the warp-frame and lifted-frame checks, +target levels keyed by register, and the dual symbol naming. The two audits +therefore share a reading of the contract. The optional cross-check below +imports the inherited auditor on purpose. + +- **Identity, algorithm 1 (forward values).** Each register's value is + propagated as exact rational combinations of `(input, reduced free-group word)`. + Warps are independent invertible free symbols. All 632 live inputs **and the + 91 private buffers** are independent symbols, so the buffers are dirty. + - The check requires `y_t -> y_t + x_t` with every other live input restored, + and no buffer contribution in any live register. + - With dirty buffers, every buffer is returned unchanged in both orientations. + - At the cleanup boundary, targets are sheared, and the 91 restored helpers + equal their own inputs and are read nowhere else. +- **Dual.** The contragredient circuit is run separately with independent `K^-T` + symbols and must give `x_s -> x_s - y_s` with clean buffers. +- **Identity, algorithm 2 (reverse pull-back).** The program is processed + backwards on covectors, with words growing on the right. The resulting + 723 × 723 symbolic matrix at return must equal algorithm 1 entry for entry. + A separate pull-back of the pre-cleanup program must satisfy the same + boundary contract. +- **Frames.** Subspaces of `F_2^9` are stored as 512-point masks. Each gate's + frame must contain the current frame of every register it touches. The checks + also cover: + - the frame maps of all 72 warps; + - centre descents, target levels and end frames; + - the inherited structural rules: dyadic scalars, power-of-two scales, and + wrapper and correction access. + + The lifted-Lagrangian action is also computed for every warp. For an + invertible warp it follows from the frame-map check, so it only checks the + implementation and adds no evidence. The profile and widths are derived from + the frame chains; report fields are compared only afterwards. +- **Reconstruction.** Each changed word is rebuilt from the parent using only + PROOF.md's prose. + - Every field except cleanup must equal the shipped word. + - Cleanup must equal the independently derived literal inverse. + - Canonical and compressed digests must match PR3605's records. + - The declared edit record must equal the prose. +- **Second method (written argument).** Two parts of PROOF.md are checked + symbolically: + - `P_new = P_old S1 S2` holds on **every register** at the boundary after the + old-B647 releases, and the S matrices change exactly the four donors and the + eight tabled targets; + - the two four-row target tables hold exactly at old B599 and B647, every + other target has zero columns, and each table kills its `v`. + + A per-register frame invoice is also computed and compared with PROOF.md's + written per-pivot histograms. +- **Contract fidelity (optional; not in the registered replay).** + `crosscheck_inherited.py SEED TRIALS` compares this package's forward and dual + verdicts with the inherited interpreter on random mutants of the `base` word. + That interpreter is pinned by SHA256 in the script and in SOURCES.json. The + mutants flip, drop or swap B gates, change coefficients, flip or drop cleanup + gates, drop or flip corrections, and shift warps. Seeds `3605 40` and `44 60` + gave 200 of 200 agreeing verdicts. This script imports the inherited auditor, + so it checks that the contract was read correctly. It is not independent + evidence. + +## Required-failing mutants (19 per provider, all as predicted) + +| Mutant | Outcome | +|---|---| +| Omit one of the four releases (cleanup regenerated) | identity fails at targets: 644→640 `135,162`; 644→496 `135,220`; 660→656 `141,196`; 660→520 `141,171` | +| Flip one release sign, or both signs of one helper | identity fails at targets | +| Add releases but keep the raw target writes | frame containment fails at B184; identity fails at `162,171,196,220` | +| Entrance `span(429,30)` alone on the parent | frame containment fails at B184 (helper 644) | +| Releases at frame `[30]` | frame containment fails at the first release | +| Parent cleanup on the changed word | identity fails at donors `496,520,640,656` (no buffer is left dirty) | +| First 644 cleanup gate removed | identity fails at 19 helper registers `225…644` (no buffer is left dirty) | +| Keep the old `[30]` entrance | identity holds; profile = changed word + 2 rank-1 children (`{1:2441,…}`); rank mass and widths return to the parent's `8:99, 7:50` | +| Drop the restore-210 frame edit | identity and bill unchanged (that edit is bill-neutral) | +| 644-only or 660-only edit (restore-210 edit not applied; bill-neutral) | identity holds; profile `{1:2436,2:725,3:226,…}`, widths `7:51, 8:98` | + +The old-entrance mutant shows that, within these words, the entire rank-mass +saving of 2 comes from the entrance frame. With the old entrance, the staged +releases leave local rank mass unchanged. The physical legitimacy of the +`span(429,30)` entrance therefore rests on the native wrapper identity +`L^-1 T_F T_P^-1 R^-1 = C_[7] ⊗ I_[2]` (PR3605 `check_residual.py`, pinned in +SOURCES.json but not run). Every consumer above shares that identity, and it is +not independently checked here (open question 1). + +## Root brackets and attribution + +`root.py` uses `M(b) = Σ_r r·H[r]·(73/r)^b / (73·663040)` (PR3605 DERIVATION.md) +on the published complete histograms. + +- **Primary engine:** outward-rounded exact rational interval arithmetic, using + atanh/Taylor series with explicit remainders on a `2^-320` grid. +- **Second engine:** 70-digit decimal Newton iteration. +- **Third check, preparation only:** python-flint 0.9.0 arb at 400 bits + reproduced both `M(C)-1` and `M(D)-1` to all printed digits. It is not part + of the shipped replay. + +| Histogram | Published bracket | Confirmed 30-digit bracket | +|---|---|---| +| PR3605 | `[0.001730006549538841847005, …006]` | `[0.001730006549538841847005854305, …306]` | +| PR3148 | `[0.0017297774946785970118869, …870]` | `[0.001729777494678597011886903656, …657]` | + +The root delta is `+2.29054860244835118950648e-7` to `…650e-7`. Both +histograms have the same rank mass, `48,165,120 = 65088·740`. The +decomposition is `H = 6660·L + I`. The local change is +6 rank-1, +2 rank-2 +and −4 rank-3 children per call. The idle change is +`{1:+996, 3:−617, 4:+1, 5:−3083, 6:+3, 48:+616}`. + +Swapping one component at a time moves the root by about ±9.7e-5 (hybrids +0.0018266 and 0.0016331). Both hybrids violate the coverage law below (rank +mass 48,165,120 ∓ 13,320), so this split is bookkeeping, not a measure of +fragility. + +**Recount from the aggregate owner witness.** `root.py` recounts PR3605's +published aggregate integer witness +(`owners/AGGREGATE-INTEGER-FLOW.json.gz`, vendored). + +- Over its 1,491,840 bins, `idle = capacity − pattern width` reproduces `I` + exactly. +- Its role flow meets the per-call demand + `20 × {4:26, 5:2, 6:18, 7:52, 8:97, 9:213}` (the audited widths) for all 333 + macro-calls. +- It passes every check of PR3605's `verify_aggregate.py` (reimplemented) + except the two derived from the source template: record types and ranges, + no duplicate records, pattern records filling every declared bin (S × bins), + open/closed windows, supply equal to flow, per-call demand, the per-copy + group capacity, the complete paid rank mass, and its own inventory and + profile fields. Not reimplemented: the literal T37 order, and whether the + declared window classes and bin counts equal those `owner.windows` derives + from the template. +- The capacity balance `35,804,160 = mass(I) + 6660·3279` holds, so + `mass(I) = 13,966,020`. +- Six controls are rejected, each for its expected reason (asserted, as + `verify_aggregate.py` does): + - the parent widths, against the witness's inventory field; + - the parent widths with that field also set to them, rejected by the + per-call width demand; + - a deleted pattern record, and a duplicated one; + - a deleted role-flow record; + - a role on an excluded lower window endpoint. + +The witness's source windows are taken as published. The literal journal of +2,717,280 helper roles (6660 × 408) and its chronology are not re-derived here. + +**How fragile is the gain?** + +- *Coverage law.* Every complete histogram here obeys `Σ r·H[r] = 72W + 64N` + (W = 663,040, N = 6,660; inherited, see Scope). `root.py` checks both + histograms meet it at 48,165,120, and that both words have the same per-call + constant (local rank mass − helper width units = 1,856), which forces total + owner capacity 54W = 35,804,160, the witness's. So a wrong capacity, bin + count or added/dropped child breaks the law; the ±1-child shifts in + `ROOT-RESULT.json` (rank-48: `∓3.498e-7`) are slopes of law-violating + histograms only. +- *Mass-conserving errors.* Let `m = Σ_{ΔH[r] > 0} r·ΔH[r]` be the rank mass + an error moves. If the removed mass sits at published ranks (at most 48, + checked by `root.py`) and every true rank is at least 1, linearity and + `(73/48)^b ≤ (73/r)^b ≤ 73^b` give `ΔM(b) ≤ m·c(b)`, with + `c(b) = (73^b − (73/48)^b)/(73·663040)`; since `M` increases in `b`, + `m < (1 − M(b0))/c(b0)` keeps the root above `b0`. This inequality is a + written argument; its thresholds are exact-interval computations: an error + can **cancel the gain over PR3148 only if it moves more than 4,678 units**, + and take the root below 0.00173 only above 133. Both are nearly attained: + 98 rank-48 → 48 × rank-1 relabels (4,704 units) and 3 relabels (144 units) + are the fewest that do. Smaller errors still change the gain's size (one + relabel: `∓2.35e-9`; one width-8 role moved to an empty capacity-48 bin: + `−2.73e-10`). +- *Where the risk is.* PR3605 and PR3148 differ by 97,186 moved units: + 66,600 from the per-call word change and 30,586 from idle/owner repacking, + including 616 extra empty capacity-48 bins (29,568 units). So small + accounting slips cannot cancel the gain, but a window or journal legality + failure could, because the idle/owner repacking the gain depends on moves + 6.5 times the threshold. The open risks are the native residual (open + question 1) and window and journal legality (questions 3 and 4), not more + digits of the root. + +## Scope, inherited assumptions and unrun obligations + +Checked here: + +- the finite free-operator identity for arbitrary independent inputs, with + warps as free invertible symbols; +- the binary-frame chronology and bill; +- the cleanup; +- the PROOF.md factorization, tables and invoice; +- arithmetic on two published histograms, and the aggregate-witness recount. + +The free-operator proof uses inverse cancellation only, so it applies to the +actual invertible warps. + +Not checked: + +- native Gaussian/Clifford phases and the rank-7 residual `C_[7]⊗I_[2]` on 512 columns; +- the `RETIMED644-660` words of #3642/#3653 and the `DELAYED` words of #3682; +- the owner source windows and the literal T740 owner journal (the idle profile is recounted only from the aggregate witness), and every consumer's own owner journal and root; +- the PR3605 conditional release and full fresh-bootstrap wrapper replay requested in Ross's #1166 handoff (#3681 claims this replay with the inherited code; not reviewed here); +- physical/prefix/outer release, precision, the inherited all-size hypotheses H1–H5 and the formal kernel. + +The binary-frame contract is taken from the inherited format. It is not +derived from first principles. The coverage law `Σ r·H[r] = 72W + 64N` for +this template (the PR1012 deficit form, as used in +`research/complex-queue-ceiling-census`) is likewise inherited and cited, not +re-derived: `root.py` only checks that the published histograms meet it, and +the mass-changing/mass-conserving classification above depends on it. Gzip streams are not compared; payloads and +pinned byte digests are. + +## Reproduce + +From the repository root, with Python 3.12 or later and the standard library only: + +```sh +python3 -I -B research/staged-644-660-independent-audit/verify.py +python3 -I -B research/staged-644-660-independent-audit/root.py +``` + +Expected output: + +- `verify.py`: two `CHECKED` lines, then + `PASS_INDEPENDENT_STAGED_644_660_WORD_AUDIT`; +- `root.py`: `PASS_EXACT_MOMENT_BRACKETS`. + +Together they take about 1–2 min, depending on machine load. + +Both compare against the committed receipts `RESULT.json` and +`ROOT-RESULT.json`; `--write` regenerates a receipt deliberately. Failures +raise explicit exceptions, also under `-O`. + +Both commands passed directly on CPython 3.14.4 under `-I -B` and `-I -O -B`, +and `research_package.py --check-only` passed. The generic runner +(`python3.12 scripts/research_package.py --package +research/staged-644-660-independent-audit`) needs Python 3.12. That version +was not available here, so the runner has not been executed. + +## Sources + +Base main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. + +- **Snapshots.** PR3605 is unmerged, so its two words, two edit records, its + conditional-release `CLAIM.json` and its aggregate owner witness are + byte-preserved in `inputs/`. [SOURCES.json](SOURCES.json) records their + source path, commit, Git blob and SHA256, which `verify.py` checks. +- **Main inputs.** The PR3133 parent words and PR3148 `CLAIM.json` are read + from main; their blobs equal those at the predecessor heads. +- **Read, not executed.** These PR3605 files are pinned the same way: + PROOF.md, staged_pair.py, check_scope.py, verify.py, DERIVATION.md, + check_residual.py and owners/verify_aggregate.py. +- **Provenance rows.** Arham Tahir's audit `verify.py` and the inherited + `audit_local.py` are also pinned. + +## Open next questions + +The structured list is in [TASK.json](TASK.json). + +1. **Do the native phases of the paired `span(429,30)` entrance hold?** Every + consumer shares this obligation, and the whole width saving rests on it. It + needs an independent check of the rank-7 residual on all 512 Gaussian + columns, without the `bw_*` lineage code. #3681's full wrapper replay runs + the inherited native chain, so independence is the open part. +2. **Are the retimed words correct?** These are the `RETIMED644-660` words of + #3642/#3653 and the separately built `DELAYED` words of #3682. First step: + run this package's interpreter on each, with the audited STAGED words as the + single-change control. Check the identity, the claimed per-invocation change + (−2 rank-1, −2 rank-2, +2 rank-3 children), unchanged widths and + release-retiming mutants. This is cheap and is now the most + decision-relevant local check. +3. **Is each live consumer's own owner journal legal?** These are T450 + (#3624), T530 (#3626), T488 (#3633), T360 (#3638), the retimed T530/T488 + (#3642/#3653) and the retimed T360 (#3682); #3630 is a ceiling bound, not + an allocation. Where a consumer's histogram is checked against the coverage + law, as here, the same argument applies: the window bounds and literal + chronology decide legality, and an owner error can cancel that consumer's + gain only by moving more rank mass than its own threshold. +4. **Are PR3605's own T740 owner windows legal?** PR3605's own κ is already + superseded by its consumers, so this is lower priority. The remaining check + is the 333 source windows of the aggregate witness. First step: derive the window classes from the T37 + source template without the retained `owner.windows` routine, and compare + them with the witness's `groups`. +5. **Is the restore-210 frame edit needed?** It is bill- and identity-neutral + here. Does any native stage require it? + +## Credit and provenance + +- **Construction:** RossRichardson's PR3605. +- **Parent words and coupled folds:** dcharb78's PR3133. +- **T740 owner/cap root control:** Jeremy Diviney's PR3148. +- **Word lineage:** the credited predecessors are retained as recorded in those + packages: PR2857, PR2908/2917, Marius-Paul Dumitrean's PR2979, Jeremy + Kothe's PR3015 and PR3042. +- **Frame-bill and free-word structure:** Arham Tahir's + `coupled-carrier-independent-audit/verify.py` (Apache-2.0). `audit_core.py` + re-implements it without importing it (see Method). +- **Root model:** the PR3531 arithmetic lineage, as credited in PR3605. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). No human or formal-kernel review is claimed. +Apache-2.0. diff --git a/research/staged-644-660-independent-audit/RESULT.json b/research/staged-644-660-independent-audit/RESULT.json new file mode 100644 index 0000000000..10eb174029 --- /dev/null +++ b/research/staged-644-660-independent-audit/RESULT.json @@ -0,0 +1,1330 @@ +{ + "providers": { + "base": { + "changed_word": { + "canonical_sha256": "94d33db98720483f57efcd7bf50657f29f710554474e4f6b4b90617ad4500263", + "cleanup_literal_inverse": true, + "declared_record_equals_PROOF_prose": true, + "entrance_frame_points": { + "644": [ + 0, + 30, + 429, + 435 + ], + "660": [ + 0, + 30, + 429, + 435 + ] + }, + "inherited_hygiene": true, + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "reconstructed_from_PROOF_prose": true, + "release_positions_new_B": [ + 591, + 641 + ], + "semantics": { + "boundary_defects": [], + "buffer_to_live_leaks": [], + "dirty_buffers_returned_unchanged": true, + "dual_bad_registers": [], + "dual_buffer_to_live_leaks": [], + "dual_dirty_buffers": [], + "dual_dirty_buffers_returned_unchanged": true, + "final_terms": 835, + "forward_bad_registers": [], + "forward_dirty_buffers": [], + "independent_inputs": 632, + "private_buffers": 91, + "reverse_boundary_defects": [], + "reverse_pullback_equals_forward": true + }, + "terminal_frames_full": true, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "mutants": { + "644-only staged edit": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2436, + "2": 725, + "3": 226, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 51, + "8": 98, + "9": 213 + } + }, + "660-only staged edit": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2436, + "2": 725, + "3": 226, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 51, + "8": 98, + "9": 213 + } + }, + "entrance change only, on the parent": { + "frames": "FAIL: frame containment fails ('B', 184) 644" + }, + "first 644 cleanup gate removed": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [ + 225, + 241, + 244, + 245, + 247, + 248, + 252, + 253, + 254, + 384, + 388, + 390, + 391, + 392, + 397, + 496, + 641, + 642, + 644 + ], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip both releases of 644": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 162, + 220 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip both releases of 660": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 171, + 196 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 644->496": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 220 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 644->640": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 162 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 660->520": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 171 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 660->656": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 196 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "old [30] entrance kept": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2441, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 50, + "8": 99, + "9": 213 + } + }, + "omit release 644->496": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 220 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2437, + "2": 727, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "omit release 644->640": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 162 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2438, + "2": 725, + "3": 225, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "omit release 660->520": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 171 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2437, + "2": 727, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "omit release 660->656": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 196 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2438, + "2": 725, + "3": 225, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "parent cleanup on the changed word": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [ + 496, + 520, + 640, + 656 + ], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "releases added but raw target writes kept": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 162, + 171, + 196, + 220 + ], + "forward_dirty_buffers": [], + "frames": "FAIL: frame containment fails ('B', 184) 644" + }, + "releases at frame [30]": { + "frames": "FAIL: frame containment fails ('B', 591) 644" + }, + "restore-210 frame edit dropped": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + } + }, + "parent_control": { + "canonical_sha256": "49bdc172f1f53253c15fa4bf5be2d5741701d2fe9d18943f8b79c3ded0b96a3e", + "cleanup_literal_inverse": true, + "inherited_hygiene": true, + "profile": { + "1": 2433, + "2": 724, + "3": 228, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "boundary_defects": [], + "buffer_to_live_leaks": [], + "dirty_buffers_returned_unchanged": true, + "dual_bad_registers": [], + "dual_buffer_to_live_leaks": [], + "dual_dirty_buffers": [], + "dual_dirty_buffers_returned_unchanged": true, + "final_terms": 835, + "forward_bad_registers": [], + "forward_dirty_buffers": [], + "independent_inputs": 632, + "private_buffers": 91, + "reverse_boundary_defects": [], + "reverse_pullback_equals_forward": true + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 50, + "8": 99, + "9": 213 + } + }, + "second_method": { + "per_register_bill_delta": { + "496": { + "1": 2, + "2": -1 + }, + "520": { + "1": 2, + "2": -1 + }, + "640": { + "1": 1, + "2": 1, + "3": -1 + }, + "644": { + "2": 1, + "3": -1 + }, + "656": { + "1": 1, + "2": 1, + "3": -1 + }, + "660": { + "2": 1, + "3": -1 + } + }, + "prefix_identity_all_registers": true, + "register_96_bill_unchanged": true, + "registers_moved_by_S": [ + 135, + 141, + 146, + 162, + 171, + 185, + 196, + 220, + 496, + 520, + 640, + 656 + ], + "roles": { + "496": "second donor", + "520": "second donor", + "640": "first donor", + "644": "pivot", + "656": "first donor", + "660": "pivot" + }, + "sum": { + "1": 6, + "2": 2, + "3": -4 + }, + "target_tables_before_old_B599_and_B647": { + "644": { + "135": [ + "1/2", + "-1/4", + "0" + ], + "146": [ + "-1/2", + "1/4", + "0" + ], + "162": [ + "1/2", + "-1/4", + "0" + ], + "220": [ + "1/2", + "1/4", + "1/2" + ] + }, + "660": { + "141": [ + "1/2", + "1/2", + "0" + ], + "171": [ + "1/2", + "-1/2", + "1/2" + ], + "185": [ + "-1/2", + "-1/2", + "0" + ], + "196": [ + "1/2", + "1/2", + "0" + ] + } + } + } + }, + "extra": { + "changed_word": { + "canonical_sha256": "ec4b2e15beaf99be4a96a6056fd6e92d09ea2382a4d0e8ab321f10bb2fc1dd10", + "cleanup_literal_inverse": true, + "declared_record_equals_PROOF_prose": true, + "entrance_frame_points": { + "644": [ + 0, + 30, + 429, + 435 + ], + "660": [ + 0, + 30, + 429, + 435 + ] + }, + "inherited_hygiene": true, + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "reconstructed_from_PROOF_prose": true, + "release_positions_new_B": [ + 591, + 641 + ], + "semantics": { + "boundary_defects": [], + "buffer_to_live_leaks": [], + "dirty_buffers_returned_unchanged": true, + "dual_bad_registers": [], + "dual_buffer_to_live_leaks": [], + "dual_dirty_buffers": [], + "dual_dirty_buffers_returned_unchanged": true, + "final_terms": 835, + "forward_bad_registers": [], + "forward_dirty_buffers": [], + "independent_inputs": 632, + "private_buffers": 91, + "reverse_boundary_defects": [], + "reverse_pullback_equals_forward": true + }, + "terminal_frames_full": true, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "mutants": { + "644-only staged edit": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2436, + "2": 725, + "3": 226, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 51, + "8": 98, + "9": 213 + } + }, + "660-only staged edit": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2436, + "2": 725, + "3": 226, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 51, + "8": 98, + "9": 213 + } + }, + "entrance change only, on the parent": { + "frames": "FAIL: frame containment fails ('B', 184) 644" + }, + "first 644 cleanup gate removed": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [ + 225, + 241, + 244, + 245, + 247, + 248, + 252, + 253, + 254, + 384, + 388, + 390, + 391, + 392, + 397, + 496, + 641, + 642, + 644 + ], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip both releases of 644": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 162, + 220 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip both releases of 660": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 171, + 196 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 644->496": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 220 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 644->640": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 162 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 660->520": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 171 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "flip release 660->656": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 196 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "old [30] entrance kept": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2441, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 50, + "8": 99, + "9": 213 + } + }, + "omit release 644->496": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 220 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2437, + "2": 727, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "omit release 644->640": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 135, + 162 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2438, + "2": 725, + "3": 225, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "omit release 660->520": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 171 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2437, + "2": 727, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "omit release 660->656": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 141, + 196 + ], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2438, + "2": 725, + "3": 225, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "parent cleanup on the changed word": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [ + 496, + 520, + 640, + 656 + ], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + }, + "releases added but raw target writes kept": { + "dual": "FAIL", + "forward": "FAIL", + "forward_bad_other": [], + "forward_bad_targets": [ + 162, + 171, + 196, + 220 + ], + "forward_dirty_buffers": [], + "frames": "FAIL: frame containment fails ('B', 184) 644" + }, + "releases at frame [30]": { + "frames": "FAIL: frame containment fails ('B', 591) 644" + }, + "restore-210 frame edit dropped": { + "dual": "PASS", + "forward": "PASS", + "forward_bad_other": [], + "forward_bad_targets": [], + "forward_dirty_buffers": [], + "frames": "PASS", + "profile": { + "1": 2439, + "2": 726, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 52, + "8": 97, + "9": 213 + } + } + }, + "parent_control": { + "canonical_sha256": "34af6f955bf8d95f68868cc282fa739532a5a6117df50d753fd996d44cea6731", + "cleanup_literal_inverse": true, + "inherited_hygiene": true, + "profile": { + "1": 2433, + "2": 724, + "3": 228, + "4": 102, + "5": 20, + "8": 8 + }, + "semantics": { + "boundary_defects": [], + "buffer_to_live_leaks": [], + "dirty_buffers_returned_unchanged": true, + "dual_bad_registers": [], + "dual_buffer_to_live_leaks": [], + "dual_dirty_buffers": [], + "dual_dirty_buffers_returned_unchanged": true, + "final_terms": 835, + "forward_bad_registers": [], + "forward_dirty_buffers": [], + "independent_inputs": 632, + "private_buffers": 91, + "reverse_boundary_defects": [], + "reverse_pullback_equals_forward": true + }, + "widths": { + "4": 26, + "5": 2, + "6": 18, + "7": 50, + "8": 99, + "9": 213 + } + }, + "second_method": { + "per_register_bill_delta": { + "496": { + "1": 2, + "2": -1 + }, + "520": { + "1": 2, + "2": -1 + }, + "640": { + "1": 1, + "2": 1, + "3": -1 + }, + "644": { + "2": 1, + "3": -1 + }, + "656": { + "1": 1, + "2": 1, + "3": -1 + }, + "660": { + "2": 1, + "3": -1 + } + }, + "prefix_identity_all_registers": true, + "register_96_bill_unchanged": true, + "registers_moved_by_S": [ + 135, + 141, + 146, + 162, + 171, + 185, + 196, + 220, + 496, + 520, + 640, + 656 + ], + "roles": { + "496": "second donor", + "520": "second donor", + "640": "first donor", + "644": "pivot", + "656": "first donor", + "660": "pivot" + }, + "sum": { + "1": 6, + "2": 2, + "3": -4 + }, + "target_tables_before_old_B599_and_B647": { + "644": { + "135": [ + "1/2", + "-1/4", + "0" + ], + "146": [ + "-1/2", + "1/4", + "0" + ], + "162": [ + "1/2", + "-1/4", + "0" + ], + "220": [ + "1/2", + "1/4", + "1/2" + ] + }, + "660": { + "141": [ + "1/2", + "1/2", + "0" + ], + "171": [ + "1/2", + "-1/2", + "1/2" + ], + "185": [ + "-1/2", + "-1/2", + "0" + ], + "196": [ + "1/2", + "1/2", + "0" + ] + } + } + } + } + }, + "scope": "Finite exact local audit of PR3605 head 3efbb5de words against the PR3133 parent words: free-operator dirty-input identity (forward with symbolic private buffers, contragredient dual, reverse pull-back), literal inverse cleanup, binary-frame chronology/profile/widths, PROOF.md prefix factorization, tables and invoice, and mutants. No native Gaussian phase, owner journal, complete admission, kappa or frontier claim.", + "status": "PASS_INDEPENDENT_STAGED_644_660_WORD_AUDIT" +} diff --git a/research/staged-644-660-independent-audit/ROOT-RESULT.json b/research/staged-644-660-independent-audit/ROOT-RESULT.json new file mode 100644 index 0000000000..ac4270bb49 --- /dev/null +++ b/research/staged-644-660-independent-audit/ROOT-RESULT.json @@ -0,0 +1,167 @@ +{ + "aggregate_witness_recount": { + "bins": 1491840, + "capacity_rank_units": 35804160, + "controls_rejected": 6, + "idle": { + "1": 174156, + "3": 48334, + "4": 1, + "48": 283185, + "5": 10792, + "6": 3 + }, + "scope": "arithmetic of the published integer witness with the audited widths; windows as published; no literal journal or chronology" + }, + "attribution": { + "PR3148 idle + PR3605 local": { + "bracket_30_digits": [ + "1826582763822943966796899637/1000000000000000000000000000000", + "913291381911471983398449819/500000000000000000000000000000" + ], + "rank_mass": 48151800, + "shift_from_PR3148_lower": 9.680526914434695e-05 + }, + "PR3148 local + PR3605 idle": { + "bracket_30_digits": [ + "65325438777578337491804849/40000000000000000000000000000", + "816567984719729218647560613/500000000000000000000000000000" + ], + "rank_mass": 48178440, + "shift_from_PR3148_lower": -9.664152523913857e-05 + } + }, + "coverage_law": { + "forced_capacity_54W": 35804160, + "per_call_mass_minus_width_units": 1856, + "rank_mass_72W_plus_64N": 48165120, + "rank_mass_moved_PR3148_to_PR3605": 97186 + }, + "histograms": { + "PR3148": { + "M_lower_at_D_minus_1": 2.7336604517475374e-25, + "M_upper_at_C_minus_1": -1.0375926953082e-26, + "bracket_30_digits": [ + "216222186834824626485862957/125000000000000000000000000000", + "1729777494678597011886903657/1000000000000000000000000000000" + ], + "decimal_engine_root_70_digits": "0.001729777494678597011886903656817803609005754813360929082708328901175575", + "histogram": { + "1": 16376940, + "2": 4821840, + "3": 1567431, + "4": 679320, + "48": 282569, + "5": 147075, + "8": 53280 + }, + "published_bracket": [ + "17297774946785970118869/10000000000000000000000000", + "1729777494678597011887/1000000000000000000000000" + ], + "published_digits": 25 + }, + "PR3605": { + "M_lower_at_D_minus_1": 4.1334262440831736e-25, + "M_upper_at_C_minus_1": -2.4237067270536225e-24, + "bracket_30_digits": [ + "346001309907768369401170861/200000000000000000000000000000", + "865003274769420923502927153/500000000000000000000000000000" + ], + "decimal_engine_root_70_digits": "0.001730006549538841847005854305451473616183688862135324240199051199479098", + "histogram": { + "1": 16417896, + "2": 4835160, + "3": 1540174, + "4": 679321, + "48": 283185, + "5": 143992, + "6": 3, + "8": 53280 + }, + "published_bracket": [ + "346001309907768369401/200000000000000000000000", + "865003274769420923503/500000000000000000000000" + ], + "published_digits": 24 + } + }, + "idle_delta": { + "1": 996, + "3": -617, + "4": 1, + "48": 616, + "5": -3083, + "6": 3 + }, + "local_delta_per_call": { + "1": 6, + "2": 2, + "3": -4 + }, + "mass_changing_sensitivity_PR3605": { + "+1 rank-1 child (rank mass +1)": { + "bracket_30_digits": [ + "1729999212951825119741563069/1000000000000000000000000000000", + "172999921295182511974156307/100000000000000000000000000000" + ], + "shift_from_PR3605_lower": -7.336587016727264e-09 + }, + "+1 rank-48 child (rank mass +48)": { + "bracket_30_digits": [ + "345931348752233296299287263/200000000000000000000000000000", + "432414185940291620374109079/250000000000000000000000000000" + ], + "shift_from_PR3605_lower": -3.4980577767536554e-07 + }, + "-1 rank-1 child (rank mass -1)": { + "bracket_30_digits": [ + "1730013886126120365249152379/1000000000000000000000000000000", + "86500694306306018262457619/50000000000000000000000000000" + ], + "shift_from_PR3605_lower": 7.336587278518243e-09 + }, + "-1 rank-48 child (rank mass -48)": { + "bracket_30_digits": [ + "865178177482133737937284553/500000000000000000000000000000", + "1730356354964267475874569107/1000000000000000000000000000000" + ], + "shift_from_PR3605_lower": 3.498054254256289e-07 + } + }, + "mass_conserving_sensitivity_PR3605": { + "+1 relabel (rank-48 idle child <-> 48 rank-1 children)": { + "bracket_30_digits": [ + "1730004198960502862962895247/1000000000000000000000000000000", + "108125262435031428935180953/62500000000000000000000000000" + ], + "shift_from_PR3605_lower": -2.350578338984043e-09 + }, + "-1 relabel (rank-48 idle child <-> 48 rank-1 children)": { + "bracket_30_digits": [ + "86500445006178693387823839/50000000000000000000000000000", + "1730008900123573867756476781/1000000000000000000000000000000" + ], + "shift_from_PR3605_lower": 2.3505847320207507e-09 + }, + "least relabels putting the PR3605 root below 0.00173": 3, + "least relabels putting the PR3605 root below the PR3148 root": 98, + "most rank-mass units moved that cannot put the PR3605 root below 0.00173": 133, + "most rank-mass units moved that cannot put the PR3605 root below the PR3148 root": 4678, + "one width-8 role moved from a full bin to an empty capacity-48 bin": { + "bracket_30_digits": [ + "865003138289842471247704021/500000000000000000000000000000", + "1730006276579684942495408043/1000000000000000000000000000000" + ], + "shift_from_PR3605_lower": -2.7295915690451043e-10 + } + }, + "model": "M(b)=sum_r r*H[r]*(73/r)^b/(73*663040)", + "rank_mass": 48165120, + "root_delta_PR3605_minus_PR3148": [ + "28631857530604389868831/125000000000000000000000000000", + "4581097204896702379013/20000000000000000000000000000" + ], + "status": "PASS_EXACT_MOMENT_BRACKETS", + "stock_times_dimension": 48401920 +} diff --git a/research/staged-644-660-independent-audit/SOURCES.json b/research/staged-644-660-independent-audit/SOURCES.json new file mode 100644 index 0000000000..a132cf5787 --- /dev/null +++ b/research/staged-644-660-independent-audit/SOURCES.json @@ -0,0 +1,173 @@ +{ + "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/coupled-carrier-cap740/CLAIM.json", + "usage": "input", + "git_blob": "aa3d8e87fc139d636cd19eaa4cd375fca2c780cf", + "sha256": "338165d75d87a1a576750ec92772640e641bc91076e91b686d8ec7ad6f9d6d19" + }, + { + "path": "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-base.json.gz", + "usage": "input", + "git_blob": "cb4cc24a4545944627ad595c0c5080196952b9f0", + "sha256": "300a9b8ad1d554f0e6f84f43f3f5fd870a5b4e5f81ad856900b6e8999684892e" + }, + { + "path": "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-extra.json.gz", + "usage": "input", + "git_blob": "decc8f26d8aab108baf75f0d8b2d1012eb06d076", + "sha256": "495d030f1e03b90e954dad3043994f03293d41b9ed220a3beaef849df435d3f0" + }, + { + "path": "research/coupled-carrier-independent-audit/verify.py", + "usage": "provenance", + "git_blob": "18044e841b53b3d3779d8f7c15f19d98ba3f00fe", + "sha256": "59d7f658992afbcb0e86b763c07d73f706b3841f177522126cd3def5adffc41d" + }, + { + "path": "research/rank7-coupled-586-588-carrier-fold/vendor/audit_local.py", + "usage": "provenance", + "git_blob": "8224873d0497cf0b4c202f31b145fa273553d978", + "sha256": "a38940094f7d19cd6376aafdd4734fa68eabc9aff4c98c3c4a3e9540328b1c90" + } + ], + "snapshot": [ + { + "local": "inputs/STAGED644-660-base.json.gz", + "source_path": "research/staged-644-660-width-reduction/STAGED644-660-base.json.gz", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "dc6d321b1e8e2a837a1ff7bb60e8f8f78d043db5", + "sha256": "735c540b1fe29d0ceeb4d2f304ec941e5f2bd3bc92bafc8cce2b4f9a67a3b653" + }, + { + "local": "inputs/STAGED644-660-extra.json.gz", + "source_path": "research/staged-644-660-width-reduction/STAGED644-660-extra.json.gz", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "78e7b2bb0653c8dcc0133980a19dd9d97ebdb67e", + "sha256": "886338fc32da14f3389a82c8120a1bcf9c5e2f0ec3e9b2d377fdae809e1d977f" + }, + { + "local": "inputs/STAGED-PAIR-RECORD-base.json.gz", + "source_path": "research/staged-644-660-width-reduction/STAGED-PAIR-RECORD-base.json.gz", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "042dbc69aee653e0a3c66a5910f14c741e5b39a7", + "sha256": "a6ae4188be998990ecb176fef5929e8e1dfce3726e372c0da2a290fe8ea73532" + }, + { + "local": "inputs/STAGED-PAIR-RECORD-extra.json.gz", + "source_path": "research/staged-644-660-width-reduction/STAGED-PAIR-RECORD-extra.json.gz", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "67f04ae395ec5f05586af438eeb2ad2db23c9c82", + "sha256": "33a39d46d4d19bdeb6f0b6abb38cc80c68219e1ae10dd7e1acaccedc14b47236" + }, + { + "local": "inputs/PR3605-CLAIM.json", + "source_path": "research/staged-644-660-conditional-release/CLAIM.json", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "445e6a83a4cdc6e8630e86f20990b50d1311f81d", + "sha256": "2e721209f626d5111142951b1f26383d6746b4f230a4625244b5e5c84d6079d5" + }, + { + "local": "inputs/AGGREGATE-INTEGER-FLOW.json.gz", + "source_path": "research/staged-644-660-conditional-release/owners/AGGREGATE-INTEGER-FLOW.json.gz", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "104962d079d315f3caf5269ff0e8ff0fbae7fee8", + "sha256": "392d9ff80e641a79c9375e71df7f745e9d48f6e0914851a4ed4ecd079e0df2e9" + } + ], + "read_only_references": [ + { + "source_path": "research/staged-644-660-width-reduction/PROOF.md", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "020ab84ae73b04a94d5f49dae77c37d766ceb532", + "sha256": "525b010f3a895bdb11313f9938ad1b742df64bcee0b5671399230b1ded541baf", + "usage": "read for the claims under audit; not imported or executed" + }, + { + "source_path": "research/staged-644-660-width-reduction/staged_pair.py", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "ca3e3effb97f46485ab7ac8c15ce4a92e1f93fbe", + "sha256": "25fc9b025dbb90358032013303adea650a5f19937fd3edf30b6c6fd023e2d747", + "usage": "read for the claims under audit; not imported or executed" + }, + { + "source_path": "research/staged-644-660-width-reduction/check_scope.py", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "cea3481a639a18f13d457c926d7a3db45525797e", + "sha256": "f8eefd425a0d570167e14febcacfbb38a6bb29d820d808be426180cf31b5a947", + "usage": "read for the claims under audit; not imported or executed" + }, + { + "source_path": "research/staged-644-660-width-reduction/verify.py", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "7f2f6170705a77a8ca5e31007d986912373a33f0", + "sha256": "0ef49b725fc132cd5fc26a9a81028739896232d938bae22cef132384c7cbab13", + "usage": "read for the claims under audit; not imported or executed" + }, + { + "source_path": "research/staged-644-660-conditional-release/DERIVATION.md", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "30710a70b9d9e2b8625ba69fcfbf4c2ba736a8e9", + "sha256": "0570b25a98261ed62c9c5709e14a8f6f6c5a921a73286739212c3954c3e7de27", + "usage": "read for the claims under audit; not imported or executed" + }, + { + "source_path": "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-base.json.gz", + "source_commit": "51eb9c4ee9e4722010d308aa3309e039d3940cc2", + "source_pr": 3133, + "git_blob": "cb4cc24a4545944627ad595c0c5080196952b9f0", + "sha256": "300a9b8ad1d554f0e6f84f43f3f5fd870a5b4e5f81ad856900b6e8999684892e", + "usage": "identity of the main-branch input with its predecessor head" + }, + { + "source_path": "research/coupled-carrier-cap740/CLAIM.json", + "source_commit": "f2927a4b8afcf0701a6b945e14f30de1d94f5176", + "source_pr": 3148, + "git_blob": "aa3d8e87fc139d636cd19eaa4cd375fca2c780cf", + "sha256": "338165d75d87a1a576750ec92772640e641bc91076e91b686d8ec7ad6f9d6d19", + "usage": "identity of the main-branch input with its predecessor head" + }, + { + "source_path": "research/staged-644-660-width-reduction/check_residual.py", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "7e75bde5b4c3a0d345b89e71631abeb9994781ec", + "sha256": "e34b06ae725f062d15ad83cbd3ef2f91d3d78c380ccc93c8d2deba1c9e354c70", + "usage": "cited for the native rank-7 residual identity, which this package does not check; not imported or executed" + }, + { + "source_path": "research/staged-644-660-conditional-release/owners/verify_aggregate.py", + "source_commit": "3efbb5de06a49ffeea6684482f2d3fe48cdca3fb", + "source_pr": 3605, + "git_blob": "a5e828b6de7eb691e94eec1ee52ea47fd9a2971f", + "sha256": "c10a0eb62799f73dd577a5bec86e91b0124ec8b2cdf95bd68807299cf1521866", + "usage": "read for the aggregate-witness legality checks that root.py reimplements (all but the literal T37 order and the owner.windows window classes/bin counts); not imported or executed" + } + ], + "snapshot_provenance": "Exact Git blob bytes of PR3605 head 3efbb5de (unmerged at base 20ecf289); verify.py authenticates them by SHA256. The PR3133 parent words and PR3148 claim are read from main and pinned in files. Provenance rows: Arham Tahir's coupled-carrier-independent-audit/verify.py, whose frame-bill and free-word structure audit_core.py re-implements without importing; and the inherited auditor audit_local.py, which only the optional crosscheck_inherited.py executes (it also checks this SHA256 itself)." +} diff --git a/research/staged-644-660-independent-audit/TASK.json b/research/staged-644-660-independent-audit/TASK.json new file mode 100644 index 0000000000..55317f69c7 --- /dev/null +++ b/research/staged-644-660-independent-audit/TASK.json @@ -0,0 +1,90 @@ +{ + "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": "refined", + "actual_scope": "Independently audit PR3605 (head 3efbb5de)'s staged 644/660 width 8->7 change against its single-change control, the unchanged PR3133 parent words: exact dirty-input identity in both orientations by two algorithms, literal inverse cleanup, chronological binary frames, local profile and helper widths, PROOF.md's prefix factorization/tables/invoice, required-failing mutants, and exact root brackets for the published PR3605 and PR3148 complete histograms with their attribution.", + "scope_change_reason": "The card's first experiment names #2979's joint group; PR3605 is the live descendant of that joint-construction lineage (PR2979 -> PR3133 -> PR3605). Open staged-width kappa>0.00173 claims #3624/#3626/#3633/#3638/#3630 reuse its words unchanged, #3642/#3653 build RETIMED644-660 words and #3682 builds DELAYED words on top of them; all rely on author-run inherited-interpreter checks. Auditing one changed group against its single-change control is the card's method applied to the currently decision-relevant group.", + "bottleneck_link": "Independent pricing of the supplier words that the staged-width chain inherits: a failure would invalidate the whole chain; a pass supplies the independent local check for the unchanged reusers (only the STAGED parent of the retimed #3642/#3653/#3682 words); the coverage law (inherited) already excludes mass-changing errors in the root gain, so the gain's sign is robust to owner errors moving at most 4,678 units of rank mass; but the idle repacking behind the gain moves 30,586 units, so window/journal legality and the native residual are the open risks.", + "budget_minutes": 150, + "stop_rule": "Ship (c)+(e) with a handoff if the interpreter could not reproduce the parent control by ~75 min; stop and minimize on any identity/cleanup/profile failure; switch to p104-side-correction if another contributor claimed the words first. None triggered.", + "outcome": "completed", + "evidence": "PASS_INDEPENDENT_STAGED_644_660_WORD_AUDIT (RESULT.json): both providers, parent control {1:2433,2:724,3:228,4:102,5:20,8:8} / widths 7:50,8:99 reproduced; changed words {1:2439,2:726,3:224,4:102,5:20,8:8} / widths 7:52,8:97; 632 inputs, 91 buffers; forward with dirty buffers, dual, and reverse pull-back agree; cleanup literal inverse; PROOF.md factorization P_new=P_old S1 S2 on all registers, target tables and per-register invoice exact; 19 mutants per provider behave as predicted. PASS_EXACT_MOMENT_BRACKETS (ROOT-RESULT.json): on the published histograms, PR3605 [0.001730006549538841847005,...006] and PR3148 [0.0017297774946785970118869,...870] are confirmed by two engines; delta +2.2905486024e-7. The vendored PR3605 aggregate owner witness passes the verify_aggregate.py legality checks (reimplemented) and reproduces I={1:174156,3:48334,4:1,5:10792,6:3,48:283185} with the audited widths, mass(I)=13,966,020 (windows taken as published; literal journal not re-derived). Sensitivity: both histograms meet the coverage law 72W+64N = 48,165,120 (inherited PR1012 deficit form, checked but not re-derived) and both words have per-call constant 1,856, which forces total owner capacity 54W = 35,804,160 (the witness's), so mass-changing errors (e.g. one rank-48 idle child, root shift 3.498e-7) cannot pass undetected. By linear domination with exact-interval thresholds, any mass-conserving error moving at most 4,678 units of rank mass cannot cancel the gain over PR3148 (98 rank-48->48x rank-1 relabels, 4,704 units, are the fewest that do) and any moving at most 133 units cannot take the root below 0.00173 (3 relabels are the fewest that do). PR3605 and PR3148 differ by 97,186 moved units.", + "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. No human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Do the native Gaussian phases of the paired span(429,30) entrance (rank-7 residual C_[7] tensor I_[2]) hold on all 512 columns when checked without the bw_* lineage code?", + "why_it_matters": "The old-entrance mutant shows the whole rank-mass saving comes from this entrance frame; every consumer (#3624/#3626/#3633/#3638/#3630/#3642/#3653/#3682) shares it, and it is certified only by the inherited native chain (also run by #3681's full wrapper replay), so independence is the open part.", + "first_step": "Implement an independent exact monomial/Gaussian product for T_FULL T_P^-1 and compare with PR3605 check_residual.py's recipe (pinned in SOURCES.json) on all 512 columns, including global phase.", + "blocked_by": "Understanding of the native recipe format; no data blocker." + }, + { + "question": "Are the RETIMED644-660 words of #3642/#3653 (blobs d69125e0/f3c580b0) and the separately built DELAYED words of #3682 (blobs 7ccd0962/3f1fb471) exact identities with the claimed per-invocation change -2 rank-1, -2 rank-2, +2 rank-3 and unchanged widths?", + "why_it_matters": "They carry the highest staged-width claims (#3653 and #3682 report the same endpoint) and only their STAGED parent is covered by this audit.", + "first_step": "Run this package's audit_core interpreter on the RETIMED and DELAYED words with the audited STAGED words as the single-change control; add release-retiming mutants.", + "blocked_by": "Nothing; the words are public at #3642 head 044d24f1 and #3682 head 431e6c60." + }, + { + "question": "Is each live consumer's own owner journal (T450 #3624, T530 #3626, T488 #3633, T360 #3638, retimed T530/T488 #3642/#3653, retimed T360 #3682) legal, with window classes derived independently?", + "why_it_matters": "Where a consumer's histogram is checked against the coverage law, mass-changing owner errors are excluded, so the window bounds and literal chronology decide legality; an owner error can cancel that consumer's gain only by moving more rank mass than its own threshold, but idle repacking (30,586 units for PR3605 vs PR3148) can exceed such thresholds.", + "first_step": "For one consumer, derive its window classes from the source template without the retained owner.windows routine and recount its idle histogram.", + "blocked_by": "Per-consumer journal formats." + }, + { + "question": "Are PR3605's own 333 T740 owner source windows legal for the audited widths?", + "why_it_matters": "PR3605's own kappa is superseded by its consumers, so this is lower priority; this package takes the witness windows as published and does not reimplement verify_aggregate.py's template-derived window-class and literal T37 order checks.", + "first_step": "Derive the window classes (capacity, lo, hi, bins) from the T37 source template without the retained owner.windows routine and compare with the witness's groups list.", + "blocked_by": "Requires the T37 source template/order format." + }, + { + "question": "Is the restore-210 frame edit (source 96 sign gate moved from a rank-8 hyperplane to FULL) needed by any native stage?", + "why_it_matters": "It is identity- and bill-neutral in the local audit; if unnecessary it is noise in the declared edit set, if necessary the native contract has an undocumented dependency.", + "first_step": "Run the native transport on the changed word with that single edit reverted and record the first failing stage, if any.", + "blocked_by": "Requires the numpy-based native chain (not run here)." + } + ] +} diff --git a/research/staged-644-660-independent-audit/VERIFY.json b/research/staged-644-660-independent-audit/VERIFY.json new file mode 100644 index 0000000000..7f6ae985c6 --- /dev/null +++ b/research/staged-644-660-independent-audit/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coupled-carrier-cap740/CLAIM.json", + "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-base.json.gz", + "research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Both providers: PR3133 parent control table, PROOF.md-prose reconstruction and record digests, free-operator dirty-input identity (forward with symbolic private buffers, contragredient dual, reverse pull-back), literal inverse cleanup, binary-frame chronology/profile/widths, P_new=P_old S1 S2 on all registers, target tables, per-register invoice, 19 required-outcome mutants, receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/root.py" + ], + "timeout_seconds": 300, + "checks": "Exact interval and decimal-Newton enclosures of the PR3605 and PR3148 complex roots on their published complete histograms, H=6660L+I decompositions, coverage law 72W+64N and the forced owner capacity 54W, recount of I from the vendored aggregate owner witness with the audited widths and the verify_aggregate.py legality checks except the two template-derived ones (six controls, each rejected for its asserted reason), attribution hybrids, law-violating single-child slopes, and mass-conserving sensitivity with exact direct thresholds and least relabel counts, receipt comparison." + } + ] +} diff --git a/research/staged-644-660-independent-audit/audit_core.py b/research/staged-644-660-independent-audit/audit_core.py new file mode 100644 index 0000000000..8b5e1d5f2a --- /dev/null +++ b/research/staged-644-660-independent-audit/audit_core.py @@ -0,0 +1,480 @@ +"""Independent exact semantics and binary-frame bill for the BORROW-WORD format. + +Standard library only. Nothing is imported from the audited authors' code +(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word +format and its semantic contract were read from those pinned sources and are +credited there. The frame-bill and free-word structure (point-set spans, warp +frame and lifted-frame checks, target levels keyed by register, dual symbol +naming) re-implements, without importing, Arham Tahir's +research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its +reading of the contract, so this module is not independent of that audit. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q + +V, N, H = 112, 704, 9 # sources 0..111, targets 112..223, helpers 224..703 +DUAL = 10 ** 6 # offset naming the independent dual symbols D_k = K_k^(-T) + + +class AuditFailure(Exception): + """Explicit failure; never disabled by python -O.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(' '.join(map(str, why))) + + +def is_target(r): + return V <= r < 2 * V + + +def touched(g): + return g[1:3] if g[0] == 'add' else g[1:2] + + +# ---------------------------------------------------------------------------- +# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask +# (bit x set iff x lies in the subspace). Containment is mask inclusion. +# ---------------------------------------------------------------------------- +_SPAN = {} + + +def span(vectors): + key = tuple(vectors) + mask = _SPAN.get(key) + if mask is None: + points = {0} + for u in key: + need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u) + if u not in points: + points |= {p ^ u for p in points} + mask = sum(1 << p for p in points) + _SPAN[key] = mask + return mask + + +def points(mask): + return [x for x in range(512) if mask >> x & 1] + + +def dim(mask): + size = bin(mask).count('1') + need(size and size & (size - 1) == 0, 'not a subspace point set') + return size.bit_length() - 1 + + +FULL = (1 << 512) - 1 +ZERO = 1 + + +def hyperplane(port): + return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0) + + +def warp_images(columns): + """Images of all 512 vectors under the F_2-linear map with columns G e_i.""" + need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns') + images = [0] * 512 + for x in range(1, 512): + low = x & -x + images[x] = images[x ^ low] ^ columns[low.bit_length() - 1] + need(len(set(images)) == 512, 'singular warp') + return images + + +def image_mask(images, mask): + return sum(1 << images[x] for x in points(mask)) + + +def lagrangian_action_ok(images, U, E): + """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves. + + L_U={(x,x+p): x in U, p in U^perp}. This is the binary frame action only; it + is not a Clifford phase or Gaussian-product certificate. For invertible G with + G(U)=E it is implied by the frame-map check ( = ), so it is a + consistency check of the implementation, not extra evidence. + """ + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + # G^{-T} z: bit j of the result is . + git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H)) + lift = lambda x, z: (images[x], images[x] ^ git(x ^ z)) + pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1 + basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)] + lifted = [lift(*b) for b in basis] + if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)): + return False + + def frame(mask): + us = points(mask) + perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)] + return {(u, u ^ p) for u in us for p in perp} + return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E))) + + +# ---------------------------------------------------------------------------- +# Chronological binary-frame bill (BORROW-WORD contract) +# ---------------------------------------------------------------------------- +def frame_bill(w, lagrangian=False): + rep = w['report'] + need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry') + removed = set(w['removed']) + need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers') + live = [r for r in range(N) if r not in removed] + liveset = set(live) + B, warps = w['B'], w['warps'] + for k, (pos, lender, cols, U, E) in enumerate(warps, 1): + need(0 <= pos <= len(B), 'warp position', k) + need(lender in liveset and not is_target(lender), 'warp lender', k) + images = warp_images(cols) + su, se = span(U), span(E) + need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k) + need(image_mask(images, su) == se, 'warp does not map its frame', k) + if lagrangian: + need(lagrangian_action_ok(images, su, se), 'lifted frame action', k) + for name in ('A', 'B', 'restore'): + for g in w[name]: + if g[0] != 'warp': + need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g) + if g[0] == 'add' and not is_target(g[1]): + need(not is_target(g[2]), 'non-target reads a target', name, g) + need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates') + need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes') + need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target') + + ports = w['ports'] + start, end = {}, {} + for r in live: + if r < V: + start[r], end[r] = span((ports[r],)), FULL + elif r < 2 * V: + start[r], end[r] = ZERO, hyperplane(ports[r - V]) + else: + start[r], end[r] = ZERO, FULL + for q, U in w['start_extra'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q) + start[int(q)] = span(U) + for q, U in w['helper_final'].items(): + need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q) + end[int(q)] = span(U) + + current, bill, chain = dict(start), Counter(), {} + + def climb(r, mask, where): + need(current[r] & ~mask == 0, 'frame containment fails', where, r) + d = dim(mask) - dim(current[r]) + if d: + bill[d] += 1 + chain.setdefault(r, []).append((where, d, mask)) + current[r] = mask + + npre = w['prelude_events'] + for i, g in enumerate(w['A']): + if g[0] == 'warp': + need(i < npre and len(g) == 5, 'warp outside the prelude', i) + _, r, op, fr, to = g + need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i) + images = warp_images(warps[abs(op) - 1][2]) + if op < 0: + inverse = [0] * 512 + for x, y in enumerate(images): + inverse[y] = x + images = inverse + need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i) + need(current[r] == span(fr), 'prelude warp entry frame', i, r) + current[r] = span(to) + chain.setdefault(r, []).append((('A', i), 'warp', span(to))) + else: + if i < npre: + need(is_target(g[1]), 'prelude scalar writes a non-target', i) + for r in touched(g): + climb(r, span(g[-1]), ('A', i)) + levels = {V + int(t): span(U) for t, U in w['target_levels'].items()} + need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels') + for q, U in zip(w['centers'], w['center_frames']): + U = span(U) + need(current[q] == U, 'centre entry frame', q) + served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q} + for T in sorted(served, key=lambda m: -dim(m)): + need(T & ~U == 0, 'centre descent not nested', q) + d = dim(U) - dim(T) + if d: + bill[d] += 1 + chain.setdefault(q, []).append((('centre',), d, T)) + U = T + at = {} + for k, rec in enumerate(warps, 1): + at.setdefault(rec[0], []).append(k) + for p in range(len(B) + 1): + for k in at.get(p, ()): + _, lender, _, U, E = warps[k - 1] + need(current[lender] == span(U), 'native warp entry frame', k, lender) + current[lender] = span(E) + chain.setdefault(lender, []).append((('warp', k), 'warp', span(E))) + if p < len(B): + for r in touched(B[p]): + climb(r, span(B[p][-1]), ('B', p)) + for i, g in enumerate(w['restore']): + for r in touched(g): + climb(r, span(g[-1]), ('restore', i)) + for r in live: + climb(r, end[r], ('end',)) + restored = set(map(int, w['helper_final'])) + need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low') + widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V) + return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end + + +def hygiene(w): + """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access.""" + entering = set(map(int, w['start_extra'])) + restored = set(map(int, w['helper_final'])) + live = set(range(N)) - set(w['removed']) + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'): + for g in w[name]: + if g[0] == 'warp': + continue + q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3]) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g) + if g[0] == 'scale': + need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g) + for g in w['precondition'] + w['compensation']: + need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g) + for c in w['initial_corrections']: + word = c['operator_word'] + need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V + and c['source'] not in entering, 'correction access', c) + need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c) + q = Q(c['coefficient']) + need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c) + return True + + +# ---------------------------------------------------------------------------- +# Literal inverse cleanup, derived from the contract +# ---------------------------------------------------------------------------- +def ordinary_forward(w): + """Chronological non-wrapper actions whose inverse forms cleanup.""" + out = [g for g in w['A'][w['prelude_events']:]] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + out += at.get(p, []) + if p < len(w['B']): + out.append(w['B'][p]) + return out + list(w['restore']) + + +def derive_cleanup(w): + restored = set(map(int, w['helper_final'])) + buf = lambda r: r + N if r in restored else r + full = [256, 128, 64, 32, 16, 8, 4, 2, 1] + out = [] + for g in reversed(ordinary_forward(w)): + if g[0] == 'warp': + out.append(['warp', buf(g[1]), -g[2], full]) + elif is_target(g[1]): + continue + elif g[0] == 'add': + out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full]) + else: + need(g[0] == 'scale', 'unknown primitive', g) + out.append(['scale', buf(g[1]), g[3], g[2], full]) + return out + + +def same_cleanup(a, b): + norm = lambda c: [(g[:-1], span(g[-1])) for g in c] + return len(a) == len(b) and norm(a) == norm(b) + + +# ---------------------------------------------------------------------------- +# Exact free-operator semantics. A value is a dict {(input, word): Fraction}; +# word is a reduced tuple of signed operator ids (leftmost = applied last). +# ---------------------------------------------------------------------------- +def program(w, cleanup=None): + """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup.""" + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for k, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], k]) + for p in range(len(w['B']) + 1): + items += at.get(p, []) + if p < len(w['B']): + items.append(w['B'][p]) + items += w['restore'] + return items, list(w['cleanup'] if cleanup is None else cleanup) + + +def dual_op(op): + return (1 if op > 0 else -1) * (abs(op) + DUAL) + + +def _left(op, word): + return word[1:] if word and word[0] == -op else (op,) + word + + +def _right(word, op): + return word[:-1] if word and word[-1] == -op else word + (op,) + + +def _axpy(dst, src, q): + for key, x in src.items(): + y = dst.get(key, 0) + q * x + if y: + dst[key] = y + else: + dst.pop(key, None) + + +def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None): + """Schrodinger pass: every register's value as a combination of initial inputs. + + Live inputs are independent symbols. Private buffers are independent symbols + when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot + callback sees the rows at the cleanup boundary. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live} + for c in restored: + rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {} + prefix, tail = program(w, cleanup) + + def apply(g): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + if dual: + t, s, q = s, t, -q + _axpy(rows[t], rows[s], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + if dual: + q = 1 / q + rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()} + elif kind == 'warp': + op = dual_op(g[2]) if dual else g[2] + rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + if dual: + src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c + else: + src, ops, dst = rows[s], list(reversed(word)), t + moved = {} + for (var, wd), x in src.items(): + for o in ops: + wd = _left(o, wd) + moved[var, wd] = x + _axpy(rows[dst], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + + for g in prefix: + apply(g) + if snapshot is not None: + snapshot(rows) + for g in tail: + apply(g) + return rows + + +def reverse_columns(w, cleanup=None, upto_cleanup=False): + """Heisenberg pull-back: process the forward program backwards. + + cols[s] = {(output, word): coefficient}: the final output register 'output' + contains coefficient*word*x_s. Words grow on the right. Every live input and + every private buffer is an independent symbol. + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + regs = live + [c + N for c in restored] + cols = {r: {(r, ()): Q(1)} for r in regs} + prefix, tail = program(w, cleanup) + seq = prefix if upto_cleanup else prefix + tail + for g in reversed(seq): + kind = g[0] + if kind == 'add': + t, s, q = g[1], g[2], Q(g[3], g[4]) + need(t != s and q, 'add gate', g) + _axpy(cols[s], cols[t], q) + elif kind == 'scale': + q = Q(g[2], g[3]) + need(q != 0, 'zero scale', g) + cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()} + elif kind == 'warp': + op = g[2] + cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()} + elif kind == 'corr': + _, t, s, word, c = g + moved = {} + for (out, wd), x in cols[t].items(): + for o in word: + wd = _right(wd, o) + moved[out, wd] = x + _axpy(cols[s], moved, c) + else: + raise AuditFailure('unknown primitive ' + repr(g)) + return cols + + +def transpose(cols): + rows = {} + for s, col in cols.items(): + for (r, word), x in col.items(): + rows.setdefault(r, {})[s, word] = x + return rows + + +def endpoint_defects(w, rows, dual=False): + """Compare final rows with the contract on the zero-buffer (live-input) domain. + + Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity). + """ + removed = set(w['removed']) + live = [r for r in range(N) if r not in removed] + restored = sorted(map(int, w['helper_final'])) + bad = [] + for r in live: + expect = {(r, ()): Q(1)} + if dual and r < V: + expect[r + V, ()] = Q(-1) + if not dual and is_target(r): + expect[r - V, ()] = Q(1) + got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N} + if got != expect: + bad.append(r) + dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))] + leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N}) + buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)} + for c in restored) + return bad, dirty, leaks, buffer_identity + + +def boundary_defects(w, rows): + """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated.""" + restored = set(map(int, w['helper_final'])) + out = [] + for t in range(V, 2 * V): + if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}: + out.append(('target', t)) + for c in restored: + if rows[c] != {(c, ()): Q(1)}: + out.append(('restored', c)) + for r, row in rows.items(): + if r < N and r not in restored and any(k[0] in restored for k in row): + out.append(('restored input read', r)) + return out diff --git a/research/staged-644-660-independent-audit/crosscheck_inherited.py b/research/staged-644-660-independent-audit/crosscheck_inherited.py new file mode 100644 index 0000000000..7d45364242 --- /dev/null +++ b/research/staged-644-660-independent-audit/crosscheck_inherited.py @@ -0,0 +1,84 @@ +#!/usr/bin/env python3 +"""Optional differential check (not part of the registered replay or of the independent evidence). + +Compares this package's forward/dual endpoint verdicts with the inherited +PR3133 `audit_local.walg_apply` contract on random mutants of the PR3605 base +word, to detect any misreading of the contract. It deliberately imports the +inherited auditor from main, so it is a fidelity check, not an independent one. +Usage: python3 -I -B crosscheck_inherited.py SEED TRIALS (expected: disagree 0). + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +import copy, gzip, json, random, sys, types +from fractions import Fraction as Q +from pathlib import Path +PKG = Path(__file__).resolve().parent +REPO = PKG.parents[1] +sys.path.insert(0, str(PKG)) +import audit_core as C +import hashlib +src = REPO / 'research/rank7-coupled-586-588-carrier-fold/vendor/audit_local.py' +if hashlib.sha256(src.read_bytes()).hexdigest() != 'a38940094f7d19cd6376aafdd4734fa68eabc9aff4c98c3c4a3e9540328b1c90': + raise SystemExit('inherited auditor differs from the PR3605-pinned bytes') +audit = types.ModuleType('inherited'); audit.__file__ = str(src) +exec(compile(src.read_bytes(), str(src), 'exec'), audit.__dict__) + +# Program assembly follows the endpoint driver in PR3605 verify.py (RossRichardson), for a like-for-like comparison. +def inherited_endpoint(word, dual): + live = sorted(set(range(704)) - set(word['removed'])); restored = set(map(int, word['helper_final'])) + rows = {r: {(r, ()): Q(1)} for r in live}; rows.update({r + 704: {} for r in restored}) + program = [['corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])] for c in word['initial_corrections']] + program += word['precondition'] + word['compensation'] + word['A'] + word['cut']; warps = {} + for op, rec in enumerate(word['warps'], 1): warps.setdefault(rec[0], []).append(['warp', rec[1], op]) + for i in range(len(word['B']) + 1): + program += warps.get(i, []) + if i < len(word['B']): program.append(word['B'][i]) + program += word['restore'] + word['cleanup'] + for g in program: audit.walg_apply(g, rows, dual, 10 ** 6) + expected = {r: {(r, ()): Q(1)} for r in live} + for t in range(112): expected[t if dual else 112 + t][(112 + t if dual else t, ())] = Q(-1 if dual else 1) + bad = [r for r in live if rows[r] != expected[r]]; dirty = [r for r in restored if rows[r + 704]] + return not bad and not dirty + +def mine(word, dual): + rows = C.forward_rows(word, dual=dual, symbolic_buffers=False) + bad, dirty, leaks, _ = C.endpoint_defects(word, rows, dual=dual) + return not bad and not dirty and not leaks + +w0 = json.loads(gzip.decompress((PKG / 'inputs/STAGED644-660-base.json.gz').read_bytes())) +rng = random.Random(int(sys.argv[1]) if len(sys.argv) > 1 else 3605) +agree = disagree = 0; kinds = {} +for trial in range(int(sys.argv[2]) if len(sys.argv) > 2 else 40): + w = copy.deepcopy(w0); kind = rng.choice(['flipB', 'dropB', 'swapB', 'coefB', 'flipcleanup', 'dropcorr', 'flipcorr', 'none', 'dropcleanupwarp', 'swapwarppos']) + regen = True + if kind == 'flipB': + i = rng.choice([i for i, g in enumerate(w['B']) if g[0] == 'add']); w['B'][i][3] *= -1 + elif kind == 'dropB': + i = rng.randrange(len(w['B'])); w['B'].pop(i) + for rec in w['warps']: + if rec[0] > i: rec[0] -= 1 + elif kind == 'swapB': + i = rng.randrange(len(w['B']) - 1); w['B'][i], w['B'][i + 1] = w['B'][i + 1], w['B'][i] + elif kind == 'coefB': + i = rng.choice([i for i, g in enumerate(w['B']) if g[0] == 'add']); w['B'][i][4] *= 2 + elif kind == 'flipcleanup': + regen = False; i = rng.choice([i for i, g in enumerate(w['cleanup']) if g[0] == 'add']); w['cleanup'][i][3] *= -1 + elif kind == 'dropcleanupwarp': + regen = False; i = rng.choice([i for i, g in enumerate(w['cleanup']) if g[0] == 'warp']); w['cleanup'].pop(i) + elif kind == 'dropcorr': + w['initial_corrections'].pop(rng.randrange(len(w['initial_corrections']))) + elif kind == 'flipcorr': + c = w['initial_corrections'][rng.randrange(len(w['initial_corrections']))]; c['coefficient'] = str(-Q(c['coefficient'])) + elif kind == 'swapwarppos': + k = rng.randrange(len(w['warps'])); w['warps'][k][0] = max(0, w['warps'][k][0] - 1) + if regen: w['cleanup'] = C.derive_cleanup(w) + for dual in (False, True): + a, b = mine(w, dual), inherited_endpoint(w, dual) + kinds.setdefault(kind, []).append((dual, a, b)) + if a == b: agree += 1 + else: disagree += 1; print('DISAGREE', trial, kind, dual, a, b) +print('agree', agree, 'disagree', disagree) +if disagree: + raise SystemExit('verdicts disagree with the inherited contract') +print({k: sum(1 for d, a, b in v if a) for k, v in kinds.items()}, {k: len(v) for k, v in kinds.items()}) diff --git a/research/staged-644-660-independent-audit/inputs/AGGREGATE-INTEGER-FLOW.json.gz b/research/staged-644-660-independent-audit/inputs/AGGREGATE-INTEGER-FLOW.json.gz new file mode 100644 index 0000000000..104962d079 Binary files /dev/null and b/research/staged-644-660-independent-audit/inputs/AGGREGATE-INTEGER-FLOW.json.gz differ diff --git a/research/staged-644-660-independent-audit/inputs/PR3605-CLAIM.json b/research/staged-644-660-independent-audit/inputs/PR3605-CLAIM.json new file mode 100644 index 0000000000..445e6a83a4 --- /dev/null +++ b/research/staged-644-660-independent-audit/inputs/PR3605-CLAIM.json @@ -0,0 +1,33 @@ +{ + "calls": 6660, + "dimension": 73, + "generated_package_manifest_sha256": "d516ed4734f0d10d99fd157db769d72fe372ca09947e1d2c5ac93a27f0142dda", + "kappa": "17300065495388418470049999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017300065495388418470049999999999999999999998999999999999999999999999", + "live": 663040, + "local_publication_head": "ac92a027c78b0c9bb0ada739b26959afda489d0e", + "owner_payload_sha256": "653085641ff2e9470e25aedfc92861ec34e5cf594d52123e8b28b6f0ec20b9f8", + "physical": 663549, + "profile": { + "1": 16417896, + "2": 4835160, + "3": 1540174, + "4": 679321, + "48": 283185, + "5": 143992, + "6": 3, + "8": 53280 + }, + "release_receipt_sha256": "ce1ce9d9ad3ac9440057534d19e06b7cb4fb8da98ba5e72e01ce538b59eb2f40", + "replicas": 740, + "roles": 2717280, + "root_interval": [ + "346001309907768369401/200000000000000000000000", + "865003274769420923503/500000000000000000000000" + ], + "scope": "Complete fixed T740 source/native/owner/physical/prefix/outer release bound to the stated exact endpoint. All inherited all-size/compiler/uniform-cost/hosting/bootstrap-time/PR559/rounding/tape/recovery/analytic/BIT H1-H5 hypotheses remain. No unconditional or formal-kernel theorem or selected-record update.", + "source_manifest_sha256": "adb145b4f36ca330c34c0dbdb847351dafdc4ca9cd7bb4e1de01ed634d96bfe1", + "status": "CONDITIONAL_RELEASE_BOUND", + "unchanged_bit_endpoint": "0.001733427039589844234749", + "validation_binding": "evidence/FINAL-BINDING.json" +} diff --git a/research/staged-644-660-independent-audit/inputs/STAGED-PAIR-RECORD-base.json.gz b/research/staged-644-660-independent-audit/inputs/STAGED-PAIR-RECORD-base.json.gz new file mode 100644 index 0000000000..042dbc69ae Binary files /dev/null and b/research/staged-644-660-independent-audit/inputs/STAGED-PAIR-RECORD-base.json.gz differ diff --git a/research/staged-644-660-independent-audit/inputs/STAGED-PAIR-RECORD-extra.json.gz b/research/staged-644-660-independent-audit/inputs/STAGED-PAIR-RECORD-extra.json.gz new file mode 100644 index 0000000000..67f04ae395 Binary files /dev/null and b/research/staged-644-660-independent-audit/inputs/STAGED-PAIR-RECORD-extra.json.gz differ diff --git a/research/staged-644-660-independent-audit/inputs/STAGED644-660-base.json.gz b/research/staged-644-660-independent-audit/inputs/STAGED644-660-base.json.gz new file mode 100644 index 0000000000..dc6d321b1e Binary files /dev/null and b/research/staged-644-660-independent-audit/inputs/STAGED644-660-base.json.gz differ diff --git a/research/staged-644-660-independent-audit/inputs/STAGED644-660-extra.json.gz b/research/staged-644-660-independent-audit/inputs/STAGED644-660-extra.json.gz new file mode 100644 index 0000000000..78e7b2bb06 Binary files /dev/null and b/research/staged-644-660-independent-audit/inputs/STAGED644-660-extra.json.gz differ diff --git a/research/staged-644-660-independent-audit/root.py b/research/staged-644-660-independent-audit/root.py new file mode 100644 index 0000000000..79c304c761 --- /dev/null +++ b/research/staged-644-660-independent-audit/root.py @@ -0,0 +1,393 @@ +#!/usr/bin/env python3 +"""Exact moment-root brackets for the published PR3605 and PR3148 complete paid histograms. + +M(b) = sum_r r*H[r]*(73/r)^b / (73*663040); the complex root solves M(b)=1 +(PR3605 DERIVATION.md). Primary engine: outward-rounded exact rational interval +arithmetic (atanh/Taylor series with explicit remainders). Second engine: +decimal floating point at 70 digits with Newton iteration and an explicit error +budget. Standard library only. This re-evaluates published histograms; it does +not certify the owner journals that produce them. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +import decimal +import gzip +from fractions import Fraction as Q +import hashlib +import json +import math +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +M_DIM, STOCK, CALLS = 73, 896 * 740, 6660 +BITS = 320 # outward rounding grid 2^-320 + + +class RootFailure(Exception): + pass + + +def need(ok, *why): + if not ok: + raise RootFailure(' '.join(map(str, why))) + + +def down(x): + return Q(math.floor(x * (1 << BITS)), 1 << BITS) + + +def up(x): + return Q(-math.floor(-x * (1 << BITS)), 1 << BITS) + + +def atanh(y): + """Interval for atanh(y), 0 Q(1, 1 << (BITS + 8)): + total += term / (2 * k + 1) + term *= y2 + k += 1 + return down(total), up(total + term / (2 * k + 1) / (1 - y2)) + + +def scale(c, iv): + return (down(c * iv[0]), up(c * iv[1])) if c >= 0 else (down(c * iv[1]), up(c * iv[0])) + + +def plus(a, b): + return down(a[0] + b[0]), up(a[1] + b[1]) + + +LN2 = scale(2, atanh(Q(1, 3))) +LN3 = plus(LN2, scale(2, atanh(Q(1, 5)))) # ln 3 = ln 2 + ln(3/2) +LN5 = plus(scale(2, LN2), scale(2, atanh(Q(1, 9)))) # ln 5 = 2 ln 2 + ln(5/4) +LN73 = plus(scale(6, LN2), scale(2, atanh(Q(9, 137)))) # ln 73 = 6 ln 2 + ln(73/64) + + +def ln_ratio(r): + """Interval for ln(73/r), r a positive integer below 73 built from 2, 3, 5.""" + exps, rest = [], r + for p in (2, 3, 5): + e = 0 + while rest % p == 0: + rest //= p + e += 1 + exps.append(e) + need(rest == 1 and 0 < r < M_DIM, 'rank outside the stdlib log table', r) + lo = LN73[0] - sum(e * iv[1] for e, iv in zip(exps, (LN2, LN3, LN5))) + hi = LN73[1] - sum(e * iv[0] for e, iv in zip(exps, (LN2, LN3, LN5))) + return down(lo), up(hi) + + +def exp_interval(t_lo, t_hi): + """exp on [t_lo,t_hi] with 0<=t_lo<=t_hi<1: positive Taylor terms, explicit tail.""" + need(0 <= t_lo <= t_hi < 1, 'exp argument range') + + def partial(t): + total, term, k = Q(0), Q(1), 0 + while term > Q(1, 1 << (BITS + 8)): + total += term + k += 1 + term = term * t / k + return total, term, k + lo, _, _ = partial(t_lo) + hi, term, k = partial(t_hi) + return down(lo), up(hi + term / (1 - t_hi / (k + 1))) + + +LOGS = {} + + +def moment(hist, b): + """Interval enclosure of M(b) for a rational b>0.""" + lo = hi = Q(0) + for r, count in hist.items(): + if r not in LOGS: + LOGS[r] = ln_ratio(r) + e = exp_interval(down(b * LOGS[r][0]), up(b * LOGS[r][1])) + lo += r * count * e[0] + hi += r * count * e[1] + return down(lo / (M_DIM * STOCK)), up(hi / (M_DIM * STOCK)) + + +def bracket(hist, digits): + """Adjacent decimal endpoints C 1: + mid = (a + b) // 2 + lo, hi = moment(hist, mid * unit) + if hi < 1: + a = mid + elif lo > 1: + b = mid + else: + raise RootFailure('interval too wide to decide at %s' % (mid * unit)) + return a * unit, b * unit + + +def decimal_root(hist): + """Second engine: Newton in 70-digit decimal arithmetic; returns the root and a safe error radius.""" + D = decimal.Decimal + with decimal.localcontext(decimal.Context(prec=70, rounding=decimal.ROUND_HALF_EVEN)): + logs = {r: (D(M_DIM) / D(r)).ln() for r in hist} + weights = {r: D(r * c) for r, c in hist.items()} + denom = D(M_DIM * STOCK) + b = D('0.00173') + for _ in range(60): + f = sum(weights[r] * (b * logs[r]).exp() for r in hist) / denom - 1 + df = sum(weights[r] * logs[r] * (b * logs[r]).exp() for r in hist) / denom + step = f / df + b -= step + if abs(step) < D('1e-62'): + break + need(abs(step) < D('1e-62') and df > 1, 'decimal Newton did not settle') + # Each of the ~40 operations per evaluation is correctly rounded at 70 digits; + # |f| error < 1e-66 and df > 1, so 1e-55 is a deliberately loose radius. + return b, D('1e-55') + + +def load_hist(obj): + return {int(k): int(v) for k, v in obj.items()} + + +def aggregate_idle(cert, inventory, local): + """Recount PR3605's idle histogram from its published aggregate integer witness. + + Groups are [capacity, lo, hi, bins]; x rows are (group, width pattern, count); + z rows are (group, macro-call, width, roles). Checks record types and ranges, + duplicate records, bin counts, capacities, the open/closed windows as published, + width supply = role flow, the per-call demand S*inventory for all 333 macro-calls, + the per-copy group capacity, the complete paid rank mass 65088*37*S, and the witness's + own inventory and profile fields: every check of PR3605 owners/verify_aggregate.py, + reimplemented, except its two template-derived ones (the literal T37 order, and the + window classes and bin counts from owner.windows). Windows are taken as published. + """ + widths, S, groups = cert['widths'], cert['S'], cert['groups'] + need(widths == [4, 5, 6, 7, 8, 9] and S == 20 and len(cert['order']) == 333, 'aggregate shape') + need({int(w): n for w, n in cert['inventory'].items()} == inventory, 'witness inventory field') + idle, bins, supply, flow, demand, per_copy = (Counter() for _ in range(6)) + seen_x, seen_z = set(), set() + for g, pattern, n in cert['x']: + need(type(g) is int and 0 <= g < len(groups) and len(pattern) == 6 and type(n) is int and n > 0 + and all(type(k) is int and k >= 0 for k in pattern), 'pattern record', g) + need((g, tuple(pattern)) not in seen_x, 'duplicate pattern record', g) + seen_x.add((g, tuple(pattern))) + used = sum(w * k for w, k in zip(widths, pattern)) + need(used <= groups[g][0] and sum(pattern) <= S, 'pattern', g) + bins[g] += n + if used < groups[g][0]: + idle[groups[g][0] - used] += n + for w, k in zip(widths, pattern): + supply[g, w] += n * k + need(all(bins[g] == S * groups[g][3] for g in range(len(groups))), 'bin inventory') + for g, t, w, n in cert['z']: + need(all(type(k) is int for k in (g, t, w, n)) and 0 <= g < len(groups) and 0 <= t < 333 + and w in widths and n > 0, 'role-flow record', g, t) + need((g, t, w) not in seen_z, 'duplicate role-flow record', g, t, w) + seen_z.add((g, t, w)) + need(groups[g][1] < t <= groups[g][2], 'source window', g, t) + flow[g, w] += n + demand[t, w] += n + per_copy[g, t] += n + need(flow == +supply, 'pattern supply differs from role flow') + need(all(demand[t, w] == S * inventory[w] for t in range(333) for w in widths), 'per-call width demand') + need(all(n <= S * groups[g][3] for (g, t), n in per_copy.items()), 'per-copy group capacity') + profile = Counter({r: 333 * S * n for r, n in local.items()}) + idle + need(sum(r * n for r, n in profile.items()) == 65088 * 37 * S, 'complete paid rank mass') + need({int(r): n for r, n in cert['profile'].items()} == profile, 'witness profile field') + return idle, sum(S * g[3] for g in groups), sum(S * g[3] * g[0] for g in groups) + + +def unit_spread(b): + """Interval for c(b) = (73^b - (73/48)^b)/(73*663040), the largest change of M(b) per unit of + rank mass moved between ranks in [1, 48].""" + top, low = moment({1: 1}, b), moment({48: 1}, b) + return down(top[0] - low[1] / 48), up(top[1] - low[0] / 48) + + +def safe_units(hist, point): + """Largest integer m with m*c(point) < 1 - M(point) certified, so that every mass-conserving + change moving at most m units (ranks in [1, 48]) keeps M(point) < 1, i.e. the root above point.""" + gap, spread = 1 - moment(hist, point)[1], unit_spread(point)[1] + need(gap > 0, 'point not below the root', point) + return math.ceil(gap / spread) - 1 + + +def relabel(hist, k): + """k rank-48 idle children relabelled as 48k rank-1 children (k<0: the reverse); rank mass unchanged.""" + out = dict(hist) + out[48] -= k + out[1] += 48 * k + need(min(out.values()) >= 0, 'relabel exceeds the histogram') + return out + + +def min_relabels(hist, lo_point, hi_point): + """Least k>0 proved to put the root below [lo_point, hi_point]: lower M_k(lo_point) > 1 while + upper M_(k-1)(hi_point) < 1. M is linear in the histogram; the float guess is only a start. + """ + base, one = moment(hist, lo_point)[0], moment(relabel(hist, 1), lo_point)[0] + k = max(1, math.ceil((1 - base) / (one - base))) + while moment(relabel(hist, k), lo_point)[0] <= 1: + k += 1 + while k > 1 and moment(relabel(hist, k - 1), lo_point)[0] > 1: + k -= 1 + need(k == 1 or moment(relabel(hist, k - 1), hi_point)[1] < 1, 'relabel threshold undecided', k) + return k + + +def main(): + pr3605 = json.loads((HERE / 'inputs' / 'PR3605-CLAIM.json').read_text(encoding='utf-8')) + pr3148_path = ROOT / 'research/coupled-carrier-cap740/CLAIM.json' + pr3148 = json.loads(pr3148_path.read_text(encoding='utf-8')) + sources = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + pins = {row.get('local', row.get('path')): row['sha256'] for row in sources['files'] + sources['snapshot']} + need(hashlib.sha256((HERE / 'inputs' / 'PR3605-CLAIM.json').read_bytes()).hexdigest() == pins['inputs/PR3605-CLAIM.json'], 'PR3605 claim pin') + need(hashlib.sha256(pr3148_path.read_bytes()).hexdigest() == pins['research/coupled-carrier-cap740/CLAIM.json'], 'PR3148 claim pin') + + new, old = load_hist(pr3605['profile']), load_hist(pr3148['profile']) + local_new, local_old = Counter({1: 2439, 2: 726, 3: 224, 4: 102, 5: 20, 8: 8}), Counter(load_hist(pr3148['local_profile'])) + idle_new = Counter({1: 174156, 3: 48334, 4: 1, 5: 10792, 6: 3, 48: 283185}) # PR3605 DERIVATION.md + idle_old = Counter({1: 173160, 3: 48951, 5: 13875, 48: 282569}) # PR3148 README + times = lambda c: Counter({r: CALLS * x for r, x in c.items()}) + need(times(local_new) + idle_new == Counter(new), 'PR3605 H = 6660 L + I') + need(times(local_old) + idle_old == Counter(old), 'PR3148 H = 6660 L + I') + mass = lambda h: sum(r * c for r, c in h.items()) + # Coverage law mass(H) = 72W + 64N (W = 896*740 live stock, N = 6660 calls; PR1012 deficit form). + need(mass(new) == mass(old) == 72 * STOCK + 64 * CALLS == 65088 * 740, 'coverage law (rank mass invariant)') + cert_path = HERE / 'inputs' / 'AGGREGATE-INTEGER-FLOW.json.gz' + need(hashlib.sha256(cert_path.read_bytes()).hexdigest() == pins['inputs/AGGREGATE-INTEGER-FLOW.json.gz'], 'aggregate pin') + audited_widths = {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213} # derived from frames by verify.py + idle_count, bin_count, capacity = aggregate_idle(json.loads(gzip.decompress(cert_path.read_bytes())), audited_widths, local_new) + need(idle_count == idle_new, 'aggregate witness idle histogram differs from DERIVATION.md', dict(idle_count)) + need(capacity == mass(idle_new) + CALLS * sum(w * c for w, c in audited_widths.items()), 'capacity balance') + # mass(H) = N*(mass(L) - sum w*n_w) + capacity. The per-call constant is 1856 for both audited + # words, so the coverage law forces total owner capacity 54W for PR3605 and PR3148 alike. + parent_widths = {**audited_widths, 7: 50, 8: 99} + per_call = {name: mass(loc) - sum(w * c for w, c in ws.items()) + for name, loc, ws in (('PR3605', local_new, audited_widths), ('PR3148', local_old, parent_widths))} + forced = mass(new) - CALLS * per_call['PR3605'] + need(per_call['PR3605'] == per_call['PR3148'] == 1856 and forced == 54 * STOCK == capacity + == mass(idle_old) + CALLS * sum(w * c for w, c in parent_widths.items()), 'coverage law forces capacity 54W') + cert = json.loads(gzip.decompress(cert_path.read_bytes())) + window_cut = [row[:] for row in cert['z']] + j = next(j for j, row in enumerate(window_cut) if cert['groups'][row[0]][1] >= 0) + window_cut[j][1] = cert['groups'][window_cut[j][0]][1] # role on the excluded lower endpoint + parent_cert = {**cert, 'inventory': {str(w): n for w, n in parent_widths.items()}} + for label, bad_cert, widths, reason in ( + ('parent widths against the witness inventory field', cert, parent_widths, 'witness inventory field'), + ('parent widths, inventory field also set to them', parent_cert, parent_widths, 'per-call width demand'), + ('one pattern record deleted', {**cert, 'x': cert['x'][1:]}, audited_widths, 'bin inventory'), + ('one pattern record duplicated', {**cert, 'x': cert['x'] + cert['x'][:1]}, audited_widths, 'duplicate pattern record'), + ('one role-flow record deleted', {**cert, 'z': cert['z'][1:]}, audited_widths, 'pattern supply differs from role flow'), + ('role on an excluded lower window endpoint', {**cert, 'z': window_cut}, audited_widths, 'source window')): + try: + aggregate_idle(bad_cert, widths, local_new) + except RootFailure as error: + need(str(error).startswith(reason), 'aggregate control rejected for the wrong reason:', label, '/', error) + continue + raise RootFailure('aggregate control accepted: ' + label) + + out = {'status': 'PASS_EXACT_MOMENT_BRACKETS', 'model': 'M(b)=sum_r r*H[r]*(73/r)^b/(73*663040)', + 'rank_mass': mass(new), 'stock_times_dimension': M_DIM * STOCK, 'histograms': {}, + 'aggregate_witness_recount': {'idle': {str(k): v for k, v in sorted(idle_count.items())}, + 'bins': bin_count, 'capacity_rank_units': capacity, + 'controls_rejected': 6, + 'scope': 'arithmetic of the published integer witness with the audited ' + 'widths; windows as published; no literal journal or chronology'}} + published = {'PR3605': (new, [Q(x) for x in pr3605['root_interval']], 24), + 'PR3148': (old, [Q(x) for x in pr3148['root']], 25)} + roots = {} + for name, (hist, (c, d), digits) in published.items(): + lo_c, hi_c = moment(hist, c) + lo_d, hi_d = moment(hist, d) + need(hi_c < 1 < lo_d, 'published bracket fails', name) + own = bracket(hist, 30) + dec, radius = decimal_root(hist) + need(Q(dec) - Q(radius) > own[0] and Q(dec) + Q(radius) < own[1], 'decimal engine disagrees', name) + need(c <= own[0] and own[1] <= d, 'own 30-digit bracket outside the published one', name) + roots[name] = own + out['histograms'][name] = { + 'histogram': {str(k): v for k, v in sorted(hist.items())}, + 'published_bracket': [str(c), str(d)], 'published_digits': digits, + 'M_upper_at_C_minus_1': float(hi_c - 1), 'M_lower_at_D_minus_1': float(lo_d - 1), + 'bracket_30_digits': [str(own[0]), str(own[1])], + 'decimal_engine_root_70_digits': str(dec)} + # Counterfactual arithmetic attribution: swap one component at a time. The hybrid + # histograms are not realized owner journals and do not conserve rank mass. + hybrids = {'PR3148 idle + PR3605 local': times(local_new) + idle_old, + 'PR3148 local + PR3605 idle': times(local_old) + idle_new} + attribution = {} + for name, hist in hybrids.items(): + a, b = bracket(dict(hist), 30) + attribution[name] = {'bracket_30_digits': [str(a), str(b)], 'rank_mass': mass(hist), + 'shift_from_PR3148_lower': float(a - roots['PR3148'][0])} + out['attribution'] = attribution + out['root_delta_PR3605_minus_PR3148'] = [str(roots['PR3605'][0] - roots['PR3148'][1]), + str(roots['PR3605'][1] - roots['PR3148'][0])] + out['coverage_law'] = {'rank_mass_72W_plus_64N': 72 * STOCK + 64 * CALLS, 'per_call_mass_minus_width_units': 1856, + 'forced_capacity_54W': forced, + 'rank_mass_moved_PR3148_to_PR3605': sum(r * (new.get(r, 0) - old.get(r, 0)) + for r in set(new) | set(old) if new.get(r, 0) > old.get(r, 0))} + # Slopes only: one child added or removed changes rank mass by r, so each perturbed histogram + # violates the coverage law checked above and could not pass undetected. They show scale. + sensitivity = {} + for r in (1, 48): + for sign in (1, -1): + hist = dict(new) + hist[r] += sign + a, b = bracket(hist, 30) + sensitivity['%+d rank-%d child (rank mass %+d)' % (sign, r, sign * r)] = { + 'bracket_30_digits': [str(a), str(b)], + 'shift_from_PR3605_lower': float(a - roots['PR3605'][0])} + out['mass_changing_sensitivity_PR3605'] = sensitivity + # Mass-conserving sensitivity (every error the coverage law cannot see). Let m be the + # positive-part rank mass sum_{dH_r>0} r*dH_r of a change dH with sum r*dH_r = 0. If the + # removed mass sits at published ranks (<= 48, checked below) and every true rank is >= 1, + # linearity of M and (73/48)^b <= (73/r)^b <= 73^b give dM(b) <= m*c(b) at every b>0 + # (unit_spread), with equality for relabel(.., m/48). Since M increases in b, + # m <= safe_units(H, b0) keeps the root above b0. + capacities = sorted({g[0] for g in cert['groups']}) + need(capacities == [8, 16, 32, 48] and min(new) >= 1 and max(new) == max(old) == 48, 'ranks within [1,48]') + conserving = {} + for k in (1, -1): + a, b = bracket(relabel(new, k), 30) + conserving['%+d relabel (rank-48 idle child <-> 48 rank-1 children)' % k] = { + 'bracket_30_digits': [str(a), str(b)], 'shift_from_PR3605_lower': float(a - roots['PR3605'][0])} + move8 = dict(new) # one width-8 role: full bin -> empty 48-bin + move8[8] += 1 + move8[48] -= 1 + move8[40] = 1 + need(mass(move8) == mass(new), 'width-8 move conserves mass') + a, b = bracket(move8, 30) + conserving['one width-8 role moved from a full bin to an empty capacity-48 bin'] = { + 'bracket_30_digits': [str(a), str(b)], 'shift_from_PR3605_lower': float(a - roots['PR3605'][0])} + k_gain = min_relabels(new, *roots['PR3148']) + k_threshold = min_relabels(new, Q(173, 100000), Q(173, 100000)) + conserving['least relabels putting the PR3605 root below the PR3148 root'] = k_gain + conserving['least relabels putting the PR3605 root below 0.00173'] = k_threshold + m_gain, m_threshold = safe_units(new, roots['PR3148'][1]), safe_units(new, Q(173, 100000)) + need(48 * (k_gain - 1) <= m_gain < 48 * k_gain and 48 * (k_threshold - 1) <= m_threshold < 48 * k_threshold, + 'direct threshold disagrees with the relabel counts', m_gain, m_threshold) + conserving['most rank-mass units moved that cannot put the PR3605 root below the PR3148 root'] = m_gain + conserving['most rank-mass units moved that cannot put the PR3605 root below 0.00173'] = m_threshold + out['mass_conserving_sensitivity_PR3605'] = conserving + out['local_delta_per_call'] = {str(r): local_new[r] - local_old[r] for r in sorted(set(local_new) | set(local_old)) if local_new[r] != local_old[r]} + out['idle_delta'] = {str(r): idle_new[r] - idle_old[r] for r in sorted(set(idle_new) | set(idle_old)) if idle_new[r] != idle_old[r]} + encoded = json.dumps(out, indent=1, sort_keys=True) + '\n' + if '--write' in sys.argv: + (HERE / 'ROOT-RESULT.json').write_text(encoded, encoding='utf-8', newline='\n') + else: + need((HERE / 'ROOT-RESULT.json').read_text(encoding='utf-8') == encoded, 'ROOT-RESULT.json receipt differs') + print(out['status']) + + +if __name__ == '__main__': + main() diff --git a/research/staged-644-660-independent-audit/verify.py b/research/staged-644-660-independent-audit/verify.py new file mode 100644 index 0000000000..a6f73c7d12 --- /dev/null +++ b/research/staged-644-660-independent-audit/verify.py @@ -0,0 +1,431 @@ +#!/usr/bin/env python3 +"""Independent semantic audit of PR3605's staged 644/660 words against the PR3133 parent words. + +Checks, for both providers: the parent single-change control, an independent +reconstruction of the changed words from PROOF.md's prose, exact dirty-input +identity in both orientations by two different algorithms, literal inverse +cleanup, chronological binary frames, the local profile and widths, PROOF.md's +written prefix factorization and target tables, the per-register invoice, and +required-failing mutants. Standard library only; exact arithmetic throughout. + +`python3 -I -B verify.py` replays and compares with RESULT.json; `--write` +regenerates that receipt deliberately. + +Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude +(Anthropic, Claude Opus 5.5). Apache-2.0. +""" +from collections import Counter +import copy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import audit_core as C # noqa: E402 (package-local; bound by the package and commit-byte checks, not hashed here) +from audit_core import need, AuditFailure # noqa: E402 + +P = [429, 30] # span(429,30): the new entrance and release frame +L = [30] # the old entrance +FULL9 = [256, 128, 64, 32, 16, 8, 4, 2, 1] +RANK8 = [256, 128, 64, 32, 16, 8, 5, 3] +# PROOF.md (PR3605 head 3efbb5de), "Two exact prefix directions": deleted raw +# target writes and the releases inserted before old B599 / old B647. +DELETED = {644: (184, 185, 186, 187), 660: (216, 217, 218, 219)} +RELEASE = {644: (599, ((640, 2), (496, -2))), 660: (647, ((656, -1), (520, -2)))} +TABLE = {644: {135: (Q(1, 2), Q(-1, 4), 0), 146: (Q(-1, 2), Q(1, 4), 0), + 162: (Q(1, 2), Q(-1, 4), 0), 220: (Q(1, 2), Q(1, 4), Q(1, 2))}, + 660: {141: (Q(1, 2), Q(1, 2), 0), 171: (Q(1, 2), Q(-1, 2), Q(1, 2)), + 185: (Q(-1, 2), Q(-1, 2), 0), 196: (Q(1, 2), Q(1, 2), 0)}} +# PROOF.md "Complete local invoice": per pivot, first donor, second donor. +INVOICE = {'pivot': {2: 1, 3: -1}, 'first donor': {1: 1, 2: 1, 3: -1}, 'second donor': {1: 2, 2: -1}} +ROLES = {644: 'pivot', 640: 'first donor', 496: 'second donor', 660: 'pivot', 656: 'first donor', 520: 'second donor'} +OLD_PROFILE = {1: 2433, 2: 724, 3: 228, 4: 102, 5: 20, 8: 8} +NEW_PROFILE = {1: 2439, 2: 726, 3: 224, 4: 102, 5: 20, 8: 8} +OLD_WIDTHS = {4: 26, 5: 2, 6: 18, 7: 50, 8: 99, 9: 213} +NEW_WIDTHS = {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213} +ONE_HELPER_PROFILE = {1: 2436, 2: 725, 3: 226, 4: 102, 5: 20, 8: 8} +ONE_HELPER_WIDTHS = {4: 26, 5: 2, 6: 18, 7: 51, 8: 98, 9: 213} + + +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if raw[:2] == b'\x1f\x8b' else raw) + + +def canonical(word): + return hashlib.sha256(json.dumps(word, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + +def keyed(d): + return {str(k): v for k, v in sorted(d.items())} + + +def authenticate(): + sources = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + for row in sources['files']: + if row['usage'] == 'input': + need(sha(ROOT / row['path']) == row['sha256'], 'input pin drift', row['path']) + for row in sources['snapshot']: + need(sha(HERE / row['local']) == row['sha256'], 'snapshot pin drift', row['local']) + + +# ---------------------------------------------------------------------------- +# Independent reconstruction of the staged words from PROOF.md's prose +# ---------------------------------------------------------------------------- +def stage(parent, helpers=(644, 660), entrance=True, delete=True, release=True, restore210=True, + release_frame=P, omit=(), flip=()): + w = copy.deepcopy(parent) + drop, inserts = set(), {} + for h in helpers: + if delete: + for i in DELETED[h]: + g = parent['B'][i] + need(g[0] == 'add' and g[2] == h and C.is_target(g[1]) and g[-1] == L, 'raw target write', h, i) + drop.add(i) + if release: + cut, gates = RELEASE[h] + for j, (donor, q) in enumerate(gates): + if (h, j) in omit: + continue + q = -q if (h, j) in flip else q + inserts.setdefault(cut, []).append(['add', donor, h, q, 1, list(release_frame)]) + if entrance: + need(w['start_extra'][str(h)] == L and str(h) not in w['helper_final'], 'ordinary L-entering helper', h) + w['start_extra'][str(h)] = list(P) + new_b, cutmap = [], {} + for i in range(len(parent['B']) + 1): + cutmap[i] = len(new_b) # warps recorded at old position i fire before the inserted gates + new_b += inserts.get(i, []) + if i < len(parent['B']) and i not in drop: + new_b.append(copy.deepcopy(parent['B'][i])) + w['B'] = new_b + for rec in w['warps']: + rec[0] = cutmap[rec[0]] + if restore210: + need(w['restore'][210] == ['scale', 96, -1, 1, RANK8], 'restore 210 preimage') + w['restore'][210][-1] = list(FULL9) + w['cleanup'] = C.derive_cleanup(w) + return w, cutmap + + +# ---------------------------------------------------------------------------- +# Semantic checks +# ---------------------------------------------------------------------------- +def semantics(w): + """Forward (dirty private buffers) and dual by the Schrodinger pass; forward again by reverse pull-back.""" + boundary = {} + rows = C.forward_rows(w, symbolic_buffers=True, + snapshot=lambda r: boundary.setdefault('d', C.boundary_defects(w, r))) + bad, dirty, leaks, buffer_identity = C.endpoint_defects(w, rows) + drows = C.forward_rows(w, dual=True, symbolic_buffers=False) + dbad, ddirty, _, _ = C.endpoint_defects(w, drows, dual=True) + _, _, dleaks, dbuffer_identity = C.endpoint_defects(w, C.forward_rows(w, dual=True, symbolic_buffers=True), dual=True) + pulled = C.transpose(C.reverse_columns(w)) + pre = C.transpose(C.reverse_columns(w, upto_cleanup=True)) + pre = {r: pre.get(r, {}) for r in set(pre) | set(range(C.N))} + return {'forward_bad_registers': bad, 'forward_dirty_buffers': dirty, 'buffer_to_live_leaks': leaks, + 'dirty_buffers_returned_unchanged': buffer_identity, 'boundary_defects': boundary['d'], + 'dual_bad_registers': dbad, 'dual_dirty_buffers': ddirty, + 'dual_buffer_to_live_leaks': dleaks, 'dual_dirty_buffers_returned_unchanged': dbuffer_identity, + 'reverse_pullback_equals_forward': pulled == {r: v for r, v in rows.items() if v}, + 'reverse_boundary_defects': C.boundary_defects(w, pre), + 'independent_inputs': C.N - len(w['removed']), 'private_buffers': len(w['helper_final']), + 'final_terms': sum(len(v) for v in rows.values())} + + +def semantic_pass(s): + return (not s['forward_bad_registers'] and not s['forward_dirty_buffers'] and not s['buffer_to_live_leaks'] + and not s['boundary_defects'] and not s['dual_bad_registers'] and not s['dual_dirty_buffers'] + and s['reverse_pullback_equals_forward'] and not s['reverse_boundary_defects'] + and s['dirty_buffers_returned_unchanged'] and s['dual_dirty_buffers_returned_unchanged'] + and not s['dual_buffer_to_live_leaks'] + and s['independent_inputs'] == 632 and s['private_buffers'] == 91) + + +def execute(rows, items): + """Literal forward execution of primitive items on the given symbolic rows.""" + for g in items: + if g[0] == 'corr': + _, t, s, word, c = g + moved = {} + for (var, wd), x in rows[s].items(): + for o in reversed(word): + wd = C._left(o, wd) + moved[var, wd] = x + C._axpy(rows[t], moved, c) + elif g[0] == 'add': + need(g[1] != g[2], 'self add') + C._axpy(rows[g[1]], rows[g[2]], Q(g[3], g[4])) + elif g[0] == 'scale': + q = Q(g[2], g[3]) + rows[g[1]] = {key: q * x for key, x in rows[g[1]].items()} + elif g[0] == 'warp': + rows[g[1]] = {(var, C._left(g[2], wd)): x for (var, wd), x in rows[g[1]].items()} + else: + raise AuditFailure('unknown primitive') + return rows + + +def prefix_rows(w, k, before=()): + """All register rows after the program prefix ending just before B[k] (warps recorded at k included).""" + removed = set(w['removed']) + rows = {r: {(r, ()): Q(1)} for r in range(C.N) if r not in removed} + items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient'])) + for c in w['initial_corrections']] + items += w['precondition'] + w['compensation'] + w['A'] + w['cut'] + at = {} + for op, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], op]) + for p in range(k + 1): + items += at.get(p, []) + if p < k: + items.append(w['B'][p]) + return execute(rows, list(before) + items) + + +def prefix_identity(parent, new, cutmap): + """PROOF.md: P_new = P_old S1 S2 on every register at the boundary after the old-B647 releases.""" + s_gates = [['add', d, h, q, 1, P] for h in (644, 660) for d, q in RELEASE[h][1]] + old = prefix_rows(parent, 647, s_gates) + new_rows = prefix_rows(new, cutmap[647] + len(RELEASE[660][1])) + unchanged = prefix_rows(parent, 647) + moved = sorted(r for r in old if old[r] != unchanged[r]) + return old == new_rows, moved + + +def target_tables(parent, k): + table = {} + rows = prefix_rows(parent, k) + for t in range(C.V, 2 * C.V): + for (var, word), x in rows[t].items(): + if var in ROLES: + need(word == (), 'operator word on a pivot column', t, var, word) + table.setdefault(t, {})[var] = x + return table + + +def check_tables(table): + out = {} + for h, expect in TABLE.items(): + cols = (h, *[d for d, _ in RELEASE[h][1]]) + v = (1, *[q for _, q in RELEASE[h][1]]) + got = {t: tuple(table.get(t, {}).get(c, 0) for c in cols) for t in range(C.V, 2 * C.V) + if any(table.get(t, {}).get(c, 0) for c in cols)} + need(got == expect, 'PROOF.md target table differs', h, got) + need(all(sum(a * b for a, b in zip(row, v)) == 0 for row in got.values()), 'table does not kill v', h) + out[str(h)] = {str(t): [str(x) for x in row] for t, row in sorted(got.items())} + return out + + +def register_bills(chain): + out = {} + for r, events in chain.items(): + c = Counter(d for _, d, _ in events if isinstance(d, int) and d > 0) + if c: + out[r] = c + return out + + +def bill_delta(a, b): + return {k: b.get(k, 0) - a.get(k, 0) for k in sorted(set(a) | set(b)) if b.get(k, 0) != a.get(k, 0)} + + +# ---------------------------------------------------------------------------- +# Mutants +# ---------------------------------------------------------------------------- +def evaluate(word, want_semantics=True): + out = {} + try: + bill, widths, _, _, _ = C.frame_bill(word) + out.update(frames='PASS', profile=keyed(bill), widths=keyed(widths)) + except AuditFailure as e: + out['frames'] = 'FAIL: ' + str(e) + if want_semantics: + rows = C.forward_rows(word, symbolic_buffers=True) + bad, dirty, leaks, _ = C.endpoint_defects(word, rows) + out['forward'] = 'PASS' if not (bad or dirty or leaks) else 'FAIL' + out['forward_bad_targets'] = [r for r in bad if C.is_target(r)] + out['forward_bad_other'] = [r for r in bad if not C.is_target(r)] + out['forward_dirty_buffers'] = dirty + dbad, ddirty, _, _ = C.endpoint_defects(word, C.forward_rows(word, dual=True, symbolic_buffers=False), dual=True) + out['dual'] = 'PASS' if not (dbad or ddirty) else 'FAIL' + return out + + +def mutants(parent, new): + res = {} + for h in (644, 660): + for j in range(2): + donor = RELEASE[h][1][j][0] + res['omit release %d->%d' % (h, donor)] = evaluate(stage(parent, omit={(h, j)})[0]) + res['flip release %d->%d' % (h, donor)] = evaluate(stage(parent, flip={(h, j)})[0]) + res['flip both releases of %d' % h] = evaluate(stage(parent, flip={(h, 0), (h, 1)})[0]) + res['releases added but raw target writes kept'] = evaluate(stage(parent, delete=False)[0]) + res['entrance change only, on the parent'] = evaluate( + stage(parent, delete=False, release=False, restore210=False)[0], want_semantics=False) + res['old [30] entrance kept'] = evaluate(stage(parent, entrance=False)[0]) + res['releases at frame [30]'] = evaluate(stage(parent, release_frame=L)[0], want_semantics=False) + res['restore-210 frame edit dropped'] = evaluate(stage(parent, restore210=False)[0]) + for h in (644, 660): + res['%d-only staged edit' % h] = evaluate(stage(parent, helpers=(h,), restore210=False)[0]) + stale = copy.deepcopy(new) + stale['cleanup'] = copy.deepcopy(parent['cleanup']) + res['parent cleanup on the changed word'] = evaluate(stale) + short = copy.deepcopy(new) + del short['cleanup'][next(i for i, g in enumerate(short['cleanup']) if g[0] == 'add' and 644 in g[1:3])] + res['first 644 cleanup gate removed'] = evaluate(short) + return res + + +def require_mutants(m): + release_mutants = [k for k in m if k.startswith(('omit', 'flip'))] + ['releases added but raw target writes kept'] + for k in release_mutants: + need(m[k]['forward'] == 'FAIL' and m[k]['forward_bad_targets'], 'release mutant not rejected at a target', k) + for k in ('parent cleanup on the changed word', 'first 644 cleanup gate removed'): + need(m[k]['forward'] == 'FAIL', 'cleanup mutant accepted', k) + for k in ('entrance change only, on the parent', 'releases at frame [30]'): + need(m[k]['frames'].startswith('FAIL: frame containment fails'), 'frame mutant accepted', k) + old_entry = m['old [30] entrance kept'] + need(old_entry['forward'] == old_entry['dual'] == 'PASS', 'old-entrance word keeps the identity') + need(old_entry['profile'] == keyed(Counter(NEW_PROFILE) + Counter({1: 2})) + and old_entry['widths'] == keyed(OLD_WIDTHS), 'old-entrance bill') + drop210 = m['restore-210 frame edit dropped'] + need(drop210['forward'] == drop210['dual'] == 'PASS' and drop210['profile'] == keyed(NEW_PROFILE) + and drop210['widths'] == keyed(NEW_WIDTHS), 'restore-210 edit bill-neutral') + for h in (644, 660): + one = m['%d-only staged edit' % h] + need(one['forward'] == one['dual'] == 'PASS', 'single-helper identity', h) + need(one['profile'] == keyed(ONE_HELPER_PROFILE) and one['widths'] == keyed(ONE_HELPER_WIDTHS), + 'single-helper bill', h) + + +# ---------------------------------------------------------------------------- +def provider(tag): + parent_path = ROOT / ('research/rank7-coupled-586-588-carrier-fold/edits/FINAL-WORD-%s.json.gz' % tag) + new_path = HERE / 'inputs' / ('STAGED644-660-%s.json.gz' % tag) + parent, new = load(parent_path), load(new_path) + record = load(HERE / 'inputs' / ('STAGED-PAIR-RECORD-%s.json.gz' % tag)) + out = {} + # (a) single-change control: the unchanged PR3133 parent word + need(canonical(parent) == record['source_canonical_sha256'], 'parent canonical digest') + need(sha(parent_path) == record['source_compressed_sha256'], 'parent compressed digest') + C.hygiene(parent) + pbill, pwidths, pchain, _, _ = C.frame_bill(parent, lagrangian=True) + need(pbill == OLD_PROFILE and pwidths == OLD_WIDTHS, 'parent control table', pbill, pwidths) + need(C.same_cleanup(C.derive_cleanup(parent), parent['cleanup']), 'parent cleanup is not the literal inverse') + psem = semantics(parent) + need(semantic_pass(psem), 'parent control semantics', psem) + out['parent_control'] = {'canonical_sha256': canonical(parent), 'profile': keyed(pbill), 'widths': keyed(pwidths), + 'cleanup_literal_inverse': True, 'inherited_hygiene': True, 'semantics': psem} + # (b) independent reconstruction and full audit of the changed word + rebuilt, cutmap = stage(parent) + declared = {'deleted': [[r['index'], r['old']] for r in record['B_deleted']], + 'inserted': [[r['before'], r['gates']] for r in record['B_inserted']], + 'frames': [record['A_frame_edits'], record['B_frame_edits'], + [[r['index'], r['old'], r['new']] for r in record['restore_frame_edits']]], + 'starts': record['start_frames']} + prose = {'deleted': [[i, parent['B'][i]] for h in (644, 660) for i in DELETED[h]], + 'inserted': [[RELEASE[h][0], [['add', d, h, q, 1, P] for d, q in RELEASE[h][1]]] for h in (644, 660)], + 'frames': [[], [], [[210, RANK8, FULL9]]], + 'starts': {str(h): {'old': L, 'new': P} for h in (644, 660)}} + need(declared == prose, 'declared edit record differs from PROOF.md prose') + need(canonical(new) == record['target_canonical_sha256'], 'changed canonical digest') + need(sha(new_path) == record['target_compressed_sha256'], 'changed compressed digest') + need(set(rebuilt) == set(new), 'field set') + differing = sorted(k for k in new if k not in ('cleanup', 'report') and new[k] != rebuilt[k]) + need(not differing, 'PROOF.md reconstruction differs from the shipped word', differing) + need(C.same_cleanup(rebuilt['cleanup'], new['cleanup']), 'shipped cleanup is not the literal inverse') + C.hygiene(new) + nbill, nwidths, nchain, nstart, nend = C.frame_bill(new, lagrangian=True) + need(nbill == NEW_PROFILE and nwidths == NEW_WIDTHS, 'changed profile/widths', nbill, nwidths) + need({int(k): v for k, v in new['report']['local_profile'].items()} == nbill + and {int(k): v for k, v in new['report']['width_inventory'].items()} == nwidths, 'report fields') + nsem = semantics(new) + need(semantic_pass(nsem), 'changed word semantics', nsem) + out['changed_word'] = {'canonical_sha256': canonical(new), 'reconstructed_from_PROOF_prose': True, + 'declared_record_equals_PROOF_prose': True, 'inherited_hygiene': True, + 'profile': keyed(nbill), 'widths': keyed(nwidths), 'cleanup_literal_inverse': True, + 'semantics': nsem, + 'entrance_frame_points': {str(h): C.points(nstart[h]) for h in (644, 660)}, + 'terminal_frames_full': all(nend[h] == C.FULL for h in (644, 660)), + 'release_positions_new_B': [cutmap[599], cutmap[647]]} + # (c) second method: per-register written invoice, prefix factorization, target tables + pb, nb = register_bills(pchain), register_bills(nchain) + changed = {r: bill_delta(pb.get(r, {}), nb.get(r, {})) for r in sorted(set(pb) | set(nb)) + if bill_delta(pb.get(r, {}), nb.get(r, {}))} + need(set(changed) == set(ROLES), 'registers whose bill changes', sorted(changed)) + need(all(changed[r] == INVOICE[ROLES[r]] for r in ROLES), 'PROOF.md per-register invoice', changed) + total = Counter() + for d in changed.values(): + total.update(d) + need(dict(total) == bill_delta(OLD_PROFILE, NEW_PROFILE), 'invoice sum') + same, moved = prefix_identity(parent, new, cutmap) + need(same, 'P_new != P_old S1 S2 at the old-B647 boundary') + tables = check_tables(target_tables(parent, 599)) + need(tables == check_tables(target_tables(parent, 647)), 'tables move between the cuts') + out['second_method'] = { + 'per_register_bill_delta': {str(r): keyed(d) for r, d in changed.items()}, + 'roles': {str(r): ROLES[r] for r in ROLES}, 'sum': keyed(total), + 'register_96_bill_unchanged': pb.get(96) == nb.get(96), + 'prefix_identity_all_registers': same, 'registers_moved_by_S': moved, + 'target_tables_before_old_B599_and_B647': tables} + # (d) mutants + m = mutants(parent, new) + require_mutants(m) + out['mutants'] = m + return out + + +def self_test(): + """Interpreter sanity on tiny words: operator order, cancellation, dual symbols, pull-back agreement.""" + tiny = {'removed': list(range(226, C.N)), 'helper_final': {}, 'initial_corrections': [], 'precondition': [], + 'compensation': [], 'A': [], 'cut': [], 'warps': [], 'restore': [], 'cleanup': [], + 'B': [['warp', 224, 1], ['warp', 224, 2], ['add', 225, 224, 3, 2, []], ['warp', 224, -2]]} + rows = C.forward_rows(tiny, symbolic_buffers=False) + need(rows[224] == {(224, (1,)): Q(1)} and rows[225] == {(225, ()): Q(1), (224, (2, 1)): Q(3, 2)}, 'free-group order') + need(C.transpose(C.reverse_columns(tiny)) == {r: v for r, v in rows.items() if v}, 'pull-back disagrees on tiny word') + dual = C.forward_rows(tiny, dual=True, symbolic_buffers=False) + # contragredient: 224 <- D1 x224 - 3/2 D2^{-1} x225, with D_k = K_k^{-T} independent symbols + need(dual[224] == {(224, (1 + C.DUAL,)): Q(1), (225, (-(2 + C.DUAL),)): Q(-3, 2)} + and dual[225] == {(225, ()): Q(1)}, 'dual symbols') + need(C.dual_op(-7) == -(7 + C.DUAL) and C._left(5, (-5, 3)) == (3,) and C._right((3, -5), 5) == (3,), 'reduction') + swapped = copy.deepcopy(tiny) + swapped['B'][0][2], swapped['B'][1][2] = 2, 1 + need(C.forward_rows(swapped, symbolic_buffers=False)[225] != rows[225], 'operator order ignored') + + +def main(): + self_test() + authenticate() + result = {'status': 'PASS_INDEPENDENT_STAGED_644_660_WORD_AUDIT', + 'scope': 'Finite exact local audit of PR3605 head 3efbb5de words against the PR3133 parent words: ' + 'free-operator dirty-input identity (forward with symbolic private buffers, contragredient ' + 'dual, reverse pull-back), literal inverse cleanup, binary-frame chronology/profile/widths, ' + 'PROOF.md prefix factorization, tables and invoice, and mutants. No native Gaussian phase, ' + 'owner journal, complete admission, kappa or frontier claim.', + 'providers': {}} + for tag in ('base', 'extra'): + result['providers'][tag] = provider(tag) + print('CHECKED', tag, 'parent control, changed word, second method,', + len(result['providers'][tag]['mutants']), 'mutants', flush=True) + need(result['providers']['base']['changed_word']['profile'] == result['providers']['extra']['changed_word']['profile'], + 'providers disagree') + encoded = json.dumps(result, indent=1, sort_keys=True, default=str) + '\n' + if '--write' in sys.argv: + (HERE / 'RESULT.json').write_text(encoded, encoding='utf-8', newline='\n') + else: + need((HERE / 'RESULT.json').read_text(encoding='utf-8') == encoded, 'RESULT.json receipt differs') + print(result['status']) + + +if __name__ == '__main__': + main()