From 6d7692875457f7c1506bd15e839350a3bb896f72 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 02:42:13 +0530 Subject: [PATCH 1/2] Independent verification: rebuild the selected frontier1094 complex rank ledger from its emitted program (no new kappa) --- .../CASES.json | 101 +++++ .../README.md | 284 ++++++++++++ .../RESULT.json | 340 ++++++++++++++ .../SOURCES.json | 108 +++++ .../TASK.json | 71 +++ .../VERIFY.json | 52 +++ .../test_package.py | 347 ++++++++++++++ .../verify.py | 428 ++++++++++++++++++ 8 files changed, 1731 insertions(+) create mode 100644 research/frontier1094-emitted-ledger-seed78/CASES.json create mode 100644 research/frontier1094-emitted-ledger-seed78/README.md create mode 100644 research/frontier1094-emitted-ledger-seed78/RESULT.json create mode 100644 research/frontier1094-emitted-ledger-seed78/SOURCES.json create mode 100644 research/frontier1094-emitted-ledger-seed78/TASK.json create mode 100644 research/frontier1094-emitted-ledger-seed78/VERIFY.json create mode 100644 research/frontier1094-emitted-ledger-seed78/test_package.py create mode 100644 research/frontier1094-emitted-ledger-seed78/verify.py diff --git a/research/frontier1094-emitted-ledger-seed78/CASES.json b/research/frontier1094-emitted-ledger-seed78/CASES.json new file mode 100644 index 0000000000..cce82c3dd7 --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/CASES.json @@ -0,0 +1,101 @@ +{ + "cases": { + "frontier1094": { + "role": "selected record (certificates/selected-result.json)", + "record": [ + "certificates/checkpoints/frontier1094.json", + "certificates/selected-result.json" + ], + "archive": { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "pinned_by": "docs/research/community-batch1099-integration.json" + }, + "prefix": "candidate/strict/", + "assembly": "research/community-frontier1094-audit/ASSEMBLY.json", + "owners": "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", + "owners_listed_in": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "full_word_pin": [ + "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json", + "word_sha256" + ], + "independent_profile": [ + "research/community-frontier1094-audit/INDEPENDENT1094.json", + "owner", + "profile" + ] + }, + "frontier1042": { + "role": "previous selected checkpoint (certificates/checkpoints/frontier1042.json)", + "record": [ + "certificates/checkpoints/frontier1042.json", + "certificates/selected-result.json" + ], + "archive": { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "pinned_by": "docs/research/community-batch1047-integration.json" + }, + "prefix": "t16/", + "assembly": "research/community-frontier1042-audit/ASSEMBLY.json", + "owners": "research/gauge44-slots-t16/data/OWNERS.json.gz", + "owners_listed_in": "research/community-frontier1042-audit/SELECTED-SOURCE.json", + "full_word_pin": [ + "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json", + "word_sha256" + ], + "independent_profile": null + }, + "slots-t8": { + "role": "T8 slot ancestor replayed inside the frontier1042 capsule (slots/global)", + "record": null, + "archive": { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "pinned_by": "docs/research/community-batch1047-integration.json" + }, + "prefix": "slots/global/", + "assembly": null, + "owners": "research/gauge44-slots-t16/data/T8/OWNERS.json.gz", + "owners_listed_in": "research/community-frontier1042-audit/SELECTED-SOURCE.json", + "full_word_pin": [ + "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json", + "word_sha256" + ], + "independent_profile": null + }, + "leaver-t8": { + "role": "T8 leaver ancestor replayed inside the frontier1042 capsule (leaver-global)", + "record": null, + "archive": { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "pinned_by": "docs/research/community-batch1047-integration.json" + }, + "prefix": "leaver-global/", + "assembly": null, + "owners": "research/gauge44-leaver8/data/OWNERS.json.gz", + "owners_listed_in": "research/community-frontier1042-audit/SELECTED-SOURCE.json", + "full_word_pin": null, + "independent_profile": null + } + }, + "members": { + "assembly": "ASSEMBLY.json", + "template": "global/hosted/GLOBAL-TEMPLATE.json.gz", + "remainder_frames": "global/hosted/IDLE-REMAINDER-FRAMES.json.gz", + "remainder_receipt": "global/audit/IDLE-REMAINDER-FRAMES.json", + "owner_audit": "global/audit/OWNERS-AND-PROFILE.json", + "local_programs": "global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz", + "canonical_word": "global/base/providers/gauge44/CANONICAL-WORD.json.gz", + "full_word": "global/base/providers/gauge44/FULL-WORD.json.gz", + "data_phases": "global/base/work/complex-nine-native/DATA-PHASES.json", + "local_replay": "global/base/providers/gauge44/INDEPENDENT-LOCAL-REPLAY.json" + }, + "source_artifact_keys": { + "local_programs": "providers/gauge44/LOCAL-PROGRAMS.json.gz", + "canonical_word": "providers/gauge44/CANONICAL-WORD.json.gz", + "data_phases": "work/complex-nine-native/DATA-PHASES.json", + "local_replay": "providers/gauge44/INDEPENDENT-LOCAL-REPLAY.json" + } +} diff --git a/research/frontier1094-emitted-ledger-seed78/README.md b/research/frontier1094-emitted-ledger-seed78/README.md new file mode 100644 index 0000000000..e6130045df --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/README.md @@ -0,0 +1,284 @@ +# The selected complex rank ledger, rebuilt from the emitted program it certifies + +**Independent verification. No new κ, and no check is changed or weakened.** +- Card: `independent-moment` (ledger method), with the scope refined in [TASK.json](TASK.json). +- Track 75–84, assignment seed 78 (OS CSPRNG via Python `secrets`). +- Base commit `dadfea6e8a78ff6ba901705f87532a71c6f5bbb8`. At that base the selected record is + frontier1094, κ = 0.001672660197076918. + +## The obligation + +The selected certificate `research/community-frontier1094-audit/ASSEMBLY.json` (`1122cb3a…`) prices +the complex profile `{1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866}`. This is +the aggregate that the authors' controller audit (`OWNERS-AND-PROFILE.json`) derived from the +emitted hosted program `GLOBAL-TEMPLATE`, whose digest the certificate records. + +The selected κ uses the native complex recurrence, with no bad-class surcharge. The +[PR552 review](../native-complex-moment552/PROOF.md) allows that only because the emitted controller +has an "exact exhaustive recursive-child profile": +- every positive-rank frame climb and centre descent is a recursive child; +- the profile is the sum over all complete local invocations plus every nonempty idle remainder; +- all other work is finite work paid by the invoice. + +This package closes one link of that argument: **the emitted recursive children equal the priced +profile**, under the review's classification rule (line 17). It does **not** discharge the review's +"no good/bad q-adic selector" argument (line 24), nor the whole-owner hosting semantics. The selected +record pins the review as `research/complex-multicold/vendor/pr559/PROOF.md` (`d5d498ed…`, in +`proof_supplements`), which is byte-identical to `native-complex-moment552/PROOF.md`. + +For #1094, only author code had checked that link: +- the authors' ASYNC audit (`audit_allcold`), which counts declared ranks; +- the in-package #858 `indep16`, which replays the canonical frames but binds the backward profile to + the author-provided local replay receipt. +- The maintainers' `INDEPENDENT1094.json` comes from + `research/community-batch1099-audit/check_frontier1094.py`. It audits the owner map and prices + the profile. It takes the local factor (804384 of the 1041408 rank mass) from the word's + self-reported `local_profile` (line 21), and it hard-codes `live=14336, calls=144` (line 32). +- Open #1209 audits the pending axes and the owner map against package inputs and a parent + template. + +Neither reads the emitted template or the dispatched programs. + +## What only this package does + +`verify.py` uses only the standard library. It reads the committed replay capsule's members in +memory, imports nothing from the repository and executes no package code. + +**Byte binding (B1–B9).** Members are resolved by their full bound path. The capsule also holds +decoy copies (`split-centres/`, `global8/`), and the controls show that they are rejected. +- The capsule digest equals its integration pin. Its tar members are regular, unique and + non-traversing. +- The repository certificate equals the capsule certificate. Both equal the record's + `certificate_sha256`: a checkpoint once the frontier moves on, otherwise the selected record. +- The template digest equals `ASSEMBLY.template_sha256`, and the owner audit digest equals + `ASSEMBLY.input_sha256.owner_audit`. +- `LOCAL-PROGRAMS`, `CANONICAL-WORD`, `DATA-PHASES` and `INDEPENDENT-LOCAL-REPLAY` equal the owner + audit's `source_artifacts`. The data phases also equal the template's own pin. +- The literal remainder frames equal their receipt. +- The owner map equals `owner_map_sha256` and is listed in `SELECTED-SOURCE.json`. +- `FULL-WORD` equals the `SLOT-PINS-k8.json` word. + +**The emitted calls (L1–L13).** +- Every `(local stage, replica)` is called exactly once. +- Orientation and pair follow the recipe. +- Each call is bound to its dispatched program by compact-JSON sha256. +- The program and schedule vocabularies are closed: program events are only `scalar`, `climb`, + `adapter`, `residual_adapter`, `phase` and `center`, and the schedule has seven kinds. This is what + makes "every positive-rank climb/centre, and nothing else" exhaustive. +- Every register's frame is **replayed** in both orientations, from the word's `start` to its + `final` frames: + - each climb must leave the register's current frame for a strictly larger frame containing it; + - its rank is recomputed by F2 elimination, and declared ranks are only compared; + - centre *i* must run from `center_frames[i]` to the empty frame (forward), or back (backward), + with its carrier register sitting at that frame. + + This is the first non-author, frame-derived recount of the dispatched `LOCAL-PROGRAMS` events bound + to the selected template. The programs are also checked to equal those embedded in the template + itself. +- The data routes are the active pair's 224 families, and all 704 owners of a call are distinct. +- Each helper route equals its hosted slot: family, child, offset, width and the structural + spectator count. +- Each helper's climb total equals its hosted width and the template's width vector. +- W, N and m are read from the program. + +**The emitted remainders (L19–L20).** +- The template's `idle_children` equal, one for one, the recount: each idle cover sweep's + `DATA-PHASES` pending child minus its contiguous hosted prefix. +- Every literal `IDLE-REMAINDER-FRAMES` entry is the exact suffix of its pending axes, with full + F2 rank. This checks the consistency of an auxiliary output that does not feed the ledger. +- The pending axes of sibling children are checked to be jointly **F2-orthonormal** on every + `(pair, side, port)`, by pairwise dot products. That implies the direct sum. + +**The chain to the certificate (L21–L25).** +- Every live family carries exactly m−1 = 72 data or pending units, so rank mass = (m−1)W + 64N. + This is a checked accounting identity that pins any error to a single family. It also explains + why D is invariant under repacking. +- The rebuilt ledger equals `ASSEMBLY.complex_profile`, the owner audit's `paid_profile` and + `INDEPENDENT1094.owner.profile`. +- Helper climb totals equal the width vector of the `SLOT-PINS`-pinned `FULL-WORD`. This is a + width-vector match, not a frame-by-frame comparison. +- The per-call ledgers equal the in-lineage local replay receipt. + +The receipt also provides the fields requested in discussion #1200 (item 3), derived from the +emitted program: `local_profile_per_call`, `idle_histogram`, `families_per_call` and +`calls_per_family_by_pair`. + +## Results ([RESULT.json](RESULT.json), reproduced byte for byte on every run) + +The same unchanged code checks four records in the T16/T8 gauge44 layout: + +| Case | W | N | Rebuilt ledger | Idle remainders | Rank mass | D = W − 64N | +|---|---:|---:|---|---:|---:|---:| +| **frontier1094 (selected)** | 14336 | 144 | {1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866} | 7526 | 1041408 | 5120 | +| frontier1042 (previous checkpoint) | 14336 | 144 | {1:349577, 2:60193, 3:62608, 4:20448, 5:11808, 7:3, 8:1152, 16:47, 48:4850} | 7550 | 1041408 | 5120 | +| slots T8 (in the 1042 capsule) | 7168 | 72 | {1:174763, 2:30105, 3:31283, 4:10224, 5:5904, 7:54, 8:576, 16:23, 48:2419} | 3783 | 520704 | 2560 | +| leaver T8 (in the 1042 capsule) | 7168 | 72 | {1:174763, 2:30105, 3:30275, 4:12240, 5:4896, 7:54, 8:576, 16:23, 48:2419} | 3783 | 520704 | 2560 | + +For the selected record: +- The per-call ledger is `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` in both orientations, with 80 + forward and 64 backward calls. +- Families of pairs 0/1/2/3 are called 3/2/2/2 times each. +- Rank mass 1041408 = 144 × (1792 data + 3730 hosted-helper + 64 centre units) + 237024 + idle-remainder units. Equivalently, the pending mass 774144 = 537120 hosted + 237024 remainder. + +In each of the four records, the profile the certificate prices is exactly the recursive-child +ledger of the program it binds. + +The frontier1042 case shares its programs, word and phases with #1094, so it mainly exercises the +hosting and idle layer. The T8 cases change W and N, and the leaver case also has a different word +and programs. The constants are read from the data (`v`, `h`, `R`, the pairs in the recipe, `m`, +`live`), not hard-coded. + +## Controls ([test_package.py](test_package.py): 33 tests, about 10 s) + +Each control mutates the decoded inputs and must be rejected **by the named check**. Program edits +are consistent forgeries: the template's embedded copy and every call hash follow the edit. + +**Frame replay:** +- A climb's declared rank is relabelled (L6). +- A climb is retargeted to a non-nested frame (L5). +- A climb is moved to another register, with the same rank and mass (L5). +- A climb is made descending (L5). +- A climb's from-frame is replaced by a different frame of the same dimension that is still nested + (L5 chain). +- A centre's direction is flipped (L7). +- An unknown program event, or an unknown schedule kind, is added (L4). + +**Calls:** +- The embedded programs differ from the dispatched ones (L3). +- A program hash is swapped (L3). +- An orientation is swapped and rehashed (L2). This is a consistency check only, since both + orientations have the same per-call ledger. +- A call is duplicated (L1). +- W is changed (L9). +- A data route's family is duplicated (L10). +- A helper route is moved to another family (L11). +- Spectators are shortened (L12). +- **A whole pair-0 local stage is dropped consistently**, together with its recipe, calls and sweeps. + Every structural check passes, and only per-family conservation sees it (L21). + +**Hosting and remainders:** +- A label-disjoint but F2-dependent pending axis is introduced (L15). +- **A rank-0 child is made pending with an axis that keeps every sibling union orthonormal**. Only + the recount against the emitted remainders sees it (L19). +- A slot gap is introduced and kept consistent across the owner map, template and route (L18). +- An owner-map field that no other check reads is changed (L16). +- An idle child is dropped, or a mass-preserving hosted/rank shift is applied (L19). +- A remainder frame is made dependent (L20). + +**Certificate:** +- The certificate profile is tampered with (L23). +- The independent profile is tampered with (L23). + +**Packaging:** +- The decoy `split-centres` programs (B6) or template (B4) are substituted. +- Another record's owner map is substituted (B7). +- One capsule byte is flipped (B1). +- Duplicate or `..` tar members are added (B2). + +**Positives:** the four records, plus invariance under reordering the idle children and the +remainder frames at the decoded level. + +## Reproduce + +```sh +python3 -I -B research/frontier1094-emitted-ledger-seed78/verify.py # ~2 s; PASS_FRONTIER1094_EMITTED_LEDGER +python3 -I -B -m unittest discover -s research/frontier1094-emitted-ledger-seed78 -p test_package.py +python3 scripts/research_package.py --package research/frontier1094-emitted-ledger-seed78 --check-only +python3.12 scripts/research_package.py --package research/frontier1094-emitted-ledger-seed78 +``` + +The checks need only standard-library Python 3.10 or later; the generic replay uses 3.12. They need +no network, and they pass under `-O` because they use `need()`, not `assert`. Source commits, Git +blobs and SHA256 pins are in [SOURCES.json](SOURCES.json), and the case configuration is in +[CASES.json](CASES.json). No Makefile target is added, because the batch1099 audit pins the Makefile +by digest. + +## Overlap, prior work and credit for shared checks + +- **Open #1209** (akiva8201-dotcom, head `d1ba2631`, `research/selected1094-pending-axis-audit`) + already checks these: + - the cross-child F2 direct sum on all 896 pending bases, with an XOR-dependent-axis control; + - frame-derived helper widths and contiguous prefixes; + - the idle suffix profile and the complete profile. + + Our L15, L13, L18, the idle recount and the L15 control **replicate these as cross-checks**; they + are not claimed as new. #1209 works from package inputs and a parent template. It does not read + the capsule, the emitted template, the programs or the certificate. +- **The authors' in-lineage local replay** (`hpe_audit_local.py`, the "PR514/PR433 independent + replay", pinned in `SELECTED-SOURCE.json`; capsule receipt `INDEPENDENT-LOCAL-REPLAY.json`) already + recounts both dispatched programs. Open **#1184** (woklerx, head `2f1c9e0e`) ports that checker. + - Our recount is **code-disjoint**. L25 compares against that receipt, which is never used as + input. + - That the scalar operations inside the programs respect their frames is covered by that + in-lineage replay and by #1198, not here. +- **The per-family coverage identity** 8k_f + 1 + hosted_f + idle_f = 73, giving mass = 72W + 64N, + is from our open **#1012**, where it is shown on T37/T21. + - Our merged **#1069** observed D = W − 64N on 16 claims. + - Open **#1240** (Mister-Meeseeks) uses the identity as the premise of its packing ceiling and + re-checks it arithmetically on the #1094 profile. Its #1042 idle histogram matches our second + case. + - L21 is the T16 source-level check of that identity on the emitted #1094 and #1042 programs, so + it provides source-level evidence for the premise #1240 assumes. +- **The maintainers' `INDEPENDENT1094.json`** recounts the idle remainders from the owner map. Our + recount is a cross-check of it. +- **#1091** (Josie Elliston, seed67) audits the owner map and excludes the emitted controller. +- **Open #1255** (bitplane, head `add1e267`, `research/selected1094-chart-phase`; claimed in + discussion #1237) audits the exact phase of #1094's residual charts. Our L11–L12 bind only the + route structure and spectator counts. Spectator charts and phases are **not** validated here. +- **Complementary work:** #1112 checks the PR1042 invoice, guards, bootstrap and outer slacks; + #1142 checks PR1042 capsule closure; #1149 checks the canonical-frame rank identity. + +## Trusted, and not checked here + +- **Event classification.** That positive-rank climb and centre events are recursive children, and + that scalar, adapter, phase and residual-adapter events are finite work, is PR552's semantics. + Closed vocabularies make the classification exhaustive; they do not re-prove it. +- **Pending axes.** The `DATA-PHASES` pending axes are taken as the inherited PR558 idle-child + subspaces. They are checked for rank, port independence and direct sum. +- **Family layout.** The layout `replica·896 + (2·pair+side)·112 + port` follows #1091's rule R3. + Per-family conservation holds only if this layout is right. +- **Capsule provenance.** The capsule bytes are bound by hash, not re-executed. +- **Downstream pricing.** Moments, the κ reduction, the invoice, guards, bootstrap and the 47 outer + inequalities are not checked. #1069 prices this profile, and #1112 covers the #1042 invoice. +- **Inherited assumptions.** The all-size/compiler, hosting, precision/tape, analytic-transfer and + PR589 H1–H5 assumptions are untouched. + +## Open next questions + +1. **Does the rebuild hold for the mixed-provider T37 templates of the open claims at + 0.0016756–0.0016758?** + - Why it matters: those claims would replace the selected record, and their layout differs from + the T16/T8 gauge44 layout assumed here. + - First step: generalize the provider-dispatch and family-layout bindings, then run the checker + on one claim's maintainer capsule. + - Blocked by: no such capsule exists on main yet. +2. **Can the event-kind semantics be checked from the compiler rules, rather than only their + exhaustiveness? Can the review's no-q-adic-selector argument (line 24) and the whole-owner + hosting semantics be checked?** + - First step: state each kind's operator from `notes/general-clifford-frames.tex` and test its + fixed-frame action on a toy word. +3. **Do the 73-axis spectator charts and residual phases match the routes bound here?** + - First step: combine #1255's chart-phase criterion with this package's call and route + bindings, so the charts are checked on exactly the routes that are priced. + +## Credit + +- Rohan Arun, with OpenAI Codex assistance: #1094. +- jeremykothe2, with Claude assistance: PR1087 and the T16 owner-packing lineage. +- FanPUYen: PR858. +- rohanarun: PR987/PR1018. +- PR1005, NewBArch PR869, and the retained PR799/741/685/645/589 lineage. +- The PR552 native-complex review, the PR558 data phases and the PR514/PR433 local replay. +- Josie Elliston: seed67 (#1091). +- akiva8201-dotcom: #1209. +- woklerx: #1184 and #1149. +- Mister-Meeseeks: #1240. +- bitplane: #1237/#1255. +- Douglas Colkitt, with OpenAI Codex assistance: the maintainer replay capsules and the independent + pass. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via +Claude Code. Parallel read-only scout and judge subagents selected and designed the check. Two +adversarial judges and a live Discussions sweep found the overlaps above. New material is +Apache-2.0. diff --git a/research/frontier1094-emitted-ledger-seed78/RESULT.json b/research/frontier1094-emitted-ledger-seed78/RESULT.json new file mode 100644 index 0000000000..089272538b --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/RESULT.json @@ -0,0 +1,340 @@ +{ + "cases": { + "frontier1042": { + "N": 144, + "W": 14336, + "binding": { + "archive": "research/community-frontier1042-audit/selected-replay.tar.gz", + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "canonical_word_gz_sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "certificate": "research/community-frontier1042-audit/ASSEMBLY.json", + "certificate_sha256": "093f35445812ea96fe1bfe6a3af7d769cb7f274e08f4fb30f71a17ed1161e54e", + "data_phases_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "local_programs_gz_sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "member_prefix": "t16/", + "owner_audit_sha256": "888d63e292eed39215fe9f1440b15018f71507e13132f0e02bf0c636d56908e6", + "owner_map": "research/gauge44-slots-t16/data/OWNERS.json.gz", + "owner_map_sha256": "fe4f65082d12adfc412ac8cc041fde26b9caadfaa84d524140dc1dbc92a22ee7", + "record": "certificates/checkpoints/frontier1042.json", + "remainder_frames_sha256": "c06d94ce1c030a4230ee9c37cc3fae0a2f1831238364046a5baf778e8195363c", + "template_sha256": "8abaa0b526b17e3816d5250542c56f2a7074f58aa03dd07e606ec93d940a9048" + }, + "calls_per_family_by_pair": { + "0": 3, + "1": 2, + "2": 2, + "3": 2 + }, + "centre_mass_per_call": 64, + "deficit": 5120, + "deficit_identity": "D = W - 64 N", + "families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "family_units": 72, + "helpers": 480, + "hosted_mass": 537120, + "idle_histogram": { + "1": 2249, + "2": 1, + "3": 400, + "7": 3, + "16": 47, + "48": 4850 + }, + "ledger": { + "1": 349577, + "2": 60193, + "3": 62608, + "4": 20448, + "5": 11808, + "7": 3, + "8": 1152, + "16": 47, + "48": 4850 + }, + "local_calls": { + "backward": 64, + "forward": 80 + }, + "local_profile_per_call": { + "backward": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "forward": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "m": 73, + "pending_children": 32256, + "pending_mass": 774144, + "ports": 112, + "rank_mass": 1041408, + "remainder_mass": 237024, + "remainders": 7550, + "replicas": 16 + }, + "frontier1094": { + "N": 144, + "W": 14336, + "binding": { + "archive": "research/community-frontier1094-audit/selected-replay.tar.gz", + "archive_sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "canonical_word_gz_sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "data_phases_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "local_programs_gz_sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "member_prefix": "candidate/strict/", + "owner_audit_sha256": "30bafff060afcfb3644e951214d66cfaffe58242881c652e28003958b42127cc", + "owner_map": "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", + "owner_map_sha256": "87902c528dfab7d503dcf8a784260e3ab6fb7424c418a1820f7261f25be7b6bc", + "record": "certificates/selected-result.json", + "remainder_frames_sha256": "aa0df607a7f8f1804c3972703556000ebee5a5f4e3b3b76c27e570ed7ce17860", + "template_sha256": "9c4c51425251389ee9a747c465814cd07c64812c15b7aeef704dad7d65395a74" + }, + "calls_per_family_by_pair": { + "0": 3, + "1": 2, + "2": 2, + "3": 2 + }, + "centre_mass_per_call": 64, + "deficit": 5120, + "deficit_identity": "D = W - 64 N", + "families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "family_units": 72, + "helpers": 480, + "hosted_mass": 537120, + "idle_histogram": { + "1": 2276, + "3": 377, + "7": 7, + "48": 4866 + }, + "ledger": { + "1": 349604, + "2": 60192, + "3": 62585, + "4": 20448, + "5": 11808, + "7": 7, + "8": 1152, + "48": 4866 + }, + "local_calls": { + "backward": 64, + "forward": 80 + }, + "local_profile_per_call": { + "backward": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "forward": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "m": 73, + "pending_children": 32256, + "pending_mass": 774144, + "ports": 112, + "rank_mass": 1041408, + "remainder_mass": 237024, + "remainders": 7526, + "replicas": 16 + }, + "leaver-t8": { + "N": 72, + "W": 7168, + "binding": { + "archive": "research/community-frontier1042-audit/selected-replay.tar.gz", + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "canonical_word_gz_sha256": "99b5e2898e2a11b9d674b9c359e4bd2bccf93dfa941878f8e395361cbfd454a6", + "data_phases_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "local_programs_gz_sha256": "32487d23f80e50efb073ca12b6d5decbab1978e3680f20a13112d8f9b19a1b3f", + "member_prefix": "leaver-global/", + "owner_audit_sha256": "2e15564e5424e21c958b134090cd2389d925656f61037c0e9151d248813cce4b", + "owner_map": "research/gauge44-leaver8/data/OWNERS.json.gz", + "owner_map_sha256": "32ca30cd1c652ef6ad43657273a08a157e1df3545e759ab36306a0d0b516fb4a", + "remainder_frames_sha256": "ecb6c2aebf7e5ae8aae08206f01d485a73d3af0bf40c35e905f1b27dd53e79ec", + "template_sha256": "3c4adc53be51d72764cd580462cd290134d5826232656c5dec1a20488b1f07d8" + }, + "calls_per_family_by_pair": { + "0": 3, + "1": 2, + "2": 2, + "3": 2 + }, + "centre_mass_per_call": 64, + "deficit": 2560, + "deficit_identity": "D = W - 64 N", + "families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "family_units": 72, + "helpers": 480, + "hosted_mass": 268560, + "idle_histogram": { + "1": 1099, + "2": 9, + "3": 179, + "7": 54, + "16": 23, + "48": 2419 + }, + "ledger": { + "1": 174763, + "2": 30105, + "3": 30275, + "4": 12240, + "5": 4896, + "7": 54, + "8": 576, + "16": 23, + "48": 2419 + }, + "local_calls": { + "backward": 32, + "forward": 40 + }, + "local_profile_per_call": { + "backward": { + "1": 2412, + "2": 418, + "3": 418, + "4": 170, + "5": 68, + "8": 8 + }, + "forward": { + "1": 2412, + "2": 418, + "3": 418, + "4": 170, + "5": 68, + "8": 8 + } + }, + "m": 73, + "pending_children": 16128, + "pending_mass": 387072, + "ports": 112, + "rank_mass": 520704, + "remainder_mass": 118512, + "remainders": 3783, + "replicas": 8 + }, + "slots-t8": { + "N": 72, + "W": 7168, + "binding": { + "archive": "research/community-frontier1042-audit/selected-replay.tar.gz", + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "canonical_word_gz_sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "data_phases_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "local_programs_gz_sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "member_prefix": "slots/global/", + "owner_audit_sha256": "09d9e24c6961b84b461b8d0bd855d9490ee0d785fd414b9d28f6339cb8ac427a", + "owner_map": "research/gauge44-slots-t16/data/T8/OWNERS.json.gz", + "owner_map_sha256": "32ca30cd1c652ef6ad43657273a08a157e1df3545e759ab36306a0d0b516fb4a", + "remainder_frames_sha256": "ecb6c2aebf7e5ae8aae08206f01d485a73d3af0bf40c35e905f1b27dd53e79ec", + "template_sha256": "941206da6a73fc8344b06bfda6b6e1c031d73e82ae970ded3e17c7b1180589a7" + }, + "calls_per_family_by_pair": { + "0": 3, + "1": 2, + "2": 2, + "3": 2 + }, + "centre_mass_per_call": 64, + "deficit": 2560, + "deficit_identity": "D = W - 64 N", + "families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "family_units": 72, + "helpers": 480, + "hosted_mass": 268560, + "idle_histogram": { + "1": 1099, + "2": 9, + "3": 179, + "7": 54, + "16": 23, + "48": 2419 + }, + "ledger": { + "1": 174763, + "2": 30105, + "3": 31283, + "4": 10224, + "5": 5904, + "7": 54, + "8": 576, + "16": 23, + "48": 2419 + }, + "local_calls": { + "backward": 32, + "forward": 40 + }, + "local_profile_per_call": { + "backward": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + }, + "forward": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "m": 73, + "pending_children": 16128, + "pending_mass": 387072, + "ports": 112, + "rank_mass": 520704, + "remainder_mass": 118512, + "remainders": 3783, + "replicas": 8 + } + }, + "status": "PASS_FRONTIER1094_EMITTED_LEDGER" +} diff --git a/research/frontier1094-emitted-ledger-seed78/SOURCES.json b/research/frontier1094-emitted-ledger-seed78/SOURCES.json new file mode 100644 index 0000000000..ecb99ef2c6 --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/SOURCES.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "files": [ + { + "path": "certificates/checkpoints/frontier1042.json", + "usage": "input", + "git_blob": "f451ced6626a1f03aba6915ce23a136b01ebe51d", + "sha256": "207d1f49f113c585024b9d3c17eadbb8b1be17c1321e3d190aabe2f18ce1c5b7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "docs/research/community-batch1047-integration.json", + "usage": "provenance", + "git_blob": "c5c3afd989bdd15bd73c4b9c3fa476159fa98ace", + "sha256": "b04623d39df453804f327a203f07882554b138e6b322b9d1f674d84d94a14a8c" + }, + { + "path": "docs/research/community-batch1099-integration.json", + "usage": "provenance", + "git_blob": "9d60e86c0e494d17bec5e28eda41b275c9ede64e", + "sha256": "684c50d1ac69863e1fcc0a34bf76c54bac576f6bbde79b3c67d8432a495c8c1c" + }, + { + "path": "research/community-frontier1042-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "4e308dc23da97373d66e5d8d4a68b0661caea8e9", + "sha256": "093f35445812ea96fe1bfe6a3af7d769cb7f274e08f4fb30f71a17ed1161e54e" + }, + { + "path": "research/community-frontier1042-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "ab596b9f914f3ea0766b508e267582ec03a17edb", + "sha256": "f2c1594a39facf5d634d02e8a684677831e97f41ab2e609e8c35b52c1fec814b" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/INDEPENDENT1094.json", + "usage": "input", + "git_blob": "009a385e26858058a18188364078d162aa6f9519", + "sha256": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", + "usage": "input", + "git_blob": "d3ba33d7e703a3229d9fb8a360f69d2f318bbb70", + "sha256": "87902c528dfab7d503dcf8a784260e3ab6fb7424c418a1820f7261f25be7b6bc" + }, + { + "path": "research/gauge44-leaver8/data/OWNERS.json.gz", + "usage": "input", + "git_blob": "8eda84ea0c0f57ca4c14ecb11426874ec2e42886", + "sha256": "32ca30cd1c652ef6ad43657273a08a157e1df3545e759ab36306a0d0b516fb4a" + }, + { + "path": "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json", + "usage": "input", + "git_blob": "2702c368f4de0b671577aee9a0e2df41c1b27658", + "sha256": "55dd229684febecb80638eff9c6b3986623e8539c6c956753b350209c3e0efe2" + }, + { + "path": "research/gauge44-slots-t16/data/OWNERS.json.gz", + "usage": "input", + "git_blob": "03062b0ae23d4ca94a47f1ff66742943de5ac646", + "sha256": "fe4f65082d12adfc412ac8cc041fde26b9caadfaa84d524140dc1dbc92a22ee7" + }, + { + "path": "research/gauge44-slots-t16/data/T8/OWNERS.json.gz", + "usage": "input", + "git_blob": "8eda84ea0c0f57ca4c14ecb11426874ec2e42886", + "sha256": "32ca30cd1c652ef6ad43657273a08a157e1df3545e759ab36306a0d0b516fb4a" + } + ] +} diff --git a/research/frontier1094-emitted-ledger-seed78/TASK.json b/research/frontier1094-emitted-ledger-seed78/TASK.json new file mode 100644 index 0000000000..36ecc8065c --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/TASK.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 2, + "base_commit": "dadfea6e8a78ff6ba901705f87532a71c6f5bbb8", + "original_card": { + "id": "independent-moment", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "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." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "refined", + "actual_scope": "Rebuild the selected frontier1094 complex rank ledger (and, unchanged, the frontier1042 checkpoint and two T8 ancestors) from the emitted hosted GLOBAL-TEMPLATE and the dispatched LOCAL-PROGRAMS, CANONICAL-WORD and DATA-PHASES that the certificate binds, by code-disjoint standard-library code, and require it to equal the certificate's complex_profile.", + "scope_change_reason": "The card's ledger method applied to the one link that INDEPENDENT1094 and #1091/#1209 leave to author code: the emitted program versus the priced aggregate. That link is the 'exact exhaustive recursive-child profile' premise (research/native-complex-moment552/PROOF.md) behind the surcharge-free native complex recurrence of the selected kappa. The moment-enclosure method is not repeated (already triply covered for this record).", + "bottleneck_link": "The selected kappa omits the complex bad-class surcharge because the emitted controller's paid profile is claimed to be exactly the sum of all positive-rank climb/centre children over the local invocations plus every nonempty idle remainder. If the priced aggregate differed from the emitted program, the selected kappa would be mispriced even though the owner-map and pricing checks pass. This package checks that link at source level under the PR552 classification rule; it does not discharge the no-q-adic-selector argument or the hosting semantics, and it does not change kappa.", + "budget_minutes": 180, + "stop_rule": "Stop when the rebuilt ledger equals the certificate for the selected record and the unchanged code reproduces the frontier1042 checkpoint, with every semantic and packaging control rejected by its named check; or stop and report a mismatch with its first failing check.", + "outcome": "completed", + "evidence": "RESULT.json: frontier1094 ledger {1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866} rebuilt from 144 bound calls (80 forward, 64 backward; per call {1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}) plus 7526 emitted remainders {1:2276, 3:377, 7:7, 48:4866}; all 14336 families carry 72 units; mass 1041408 = 72W + 64N, D = 5120; equals ASSEMBLY, OWNERS-AND-PROFILE and INDEPENDENT1094; frontier1042 and T8 slots/leaver ancestors pass unchanged. test_package.py: 33 tests pass (27 semantic controls including frame-chain, centre-binding and consistent-forgery controls, 5 packaging controls, positives).", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents selected and designed the check; two adversarial judges and a live Discussions sweep found the overlaps documented in README.md.", + "open_questions": [ + { + "question": "Does the same emitted-program ledger rebuild hold for the mixed-provider T37 templates of the open claims at 0.0016756-0.0016758 (#1178-#1239)?", + "why_it_matters": "Those claims would replace the selected record; their template and provider layout differ from the T16/gauge44 family layout this checker assumes.", + "first_step": "Generalize the family-layout and provider-dispatch bindings (provider_dispatch, per-provider LOCAL-PROGRAMS) and run the checker on one such claim's archived replay once a maintainer capsule exists.", + "blocked_by": "No maintainer replay capsule for those claims on main yet." + }, + { + "question": "Can the paid-child semantics themselves (that exactly the positive-rank climb/centre events are recursive children) be proved from the compiler rules rather than taken from the PR552 review?", + "why_it_matters": "This package proves exhaustiveness relative to closed event vocabularies; the classification of each event kind is still an inherited premise of the surcharge-free recurrence.", + "first_step": "State the per-event-kind operator semantics from notes/general-clifford-frames.tex and check that scalar/adapter/phase events act within a fixed frame on a toy word.", + "blocked_by": "None; needs a careful reading of the pinned notes." + }, + { + "question": "Do the 73-axis spectator charts and residual phases match the routes bound here?", + "why_it_matters": "This package checks route structure and counts only; chart/phase semantics are a separate obligation (discussion #1237).", + "first_step": "Combine #1255's chart-phase criterion with this package's call/route bindings so charts are checked on exactly the priced routes.", + "blocked_by": "None; #1255 is open." + } + ] +} diff --git a/research/frontier1094-emitted-ledger-seed78/VERIFY.json b/research/frontier1094-emitted-ledger-seed78/VERIFY.json new file mode 100644 index 0000000000..f468bf50a7 --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/checkpoints/frontier1042.json", + "certificates/selected-result.json", + "docs/research/community-batch1047-integration.json", + "docs/research/community-batch1099-integration.json", + "research/community-frontier1042-audit/ASSEMBLY.json", + "research/community-frontier1042-audit/SELECTED-SOURCE.json", + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/INDEPENDENT1094.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", + "research/gauge44-leaver8/data/OWNERS.json.gz", + "research/gauge44-slots-t16/construction/slots/SLOT-PINS-k8.json", + "research/gauge44-slots-t16/data/OWNERS.json.gz", + "research/gauge44-slots-t16/data/T8/OWNERS.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Byte binding (capsule pins, certificate, template, owner audit, dispatched programs/word/phases, owner map, literal remainder frames, FULL-WORD) and the independent ledger rebuild from the emitted program for the selected frontier1094 record, the frontier1042 checkpoint and two T8 ancestors; every rebuilt ledger must equal its certificate; RESULT.json must be reproduced byte for byte." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 300, + "checks": "Positive and order-invariance fixtures, 27 semantic failure controls (frame replay, centre binding, consistent forgeries) and 5 packaging controls, each rejected by its named check." + } + ] +} diff --git a/research/frontier1094-emitted-ledger-seed78/test_package.py b/research/frontier1094-emitted-ledger-seed78/test_package.py new file mode 100644 index 0000000000..74c36fdcbb --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/test_package.py @@ -0,0 +1,347 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Semantic and packaging controls for verify.py: every mutation must be rejected by its named check. + +Run: python3 -I -B -m unittest discover -s research/frontier1094-emitted-ledger-seed78 -p test_package.py -v +(about a minute; the selected frontier1094 capsule is decoded once and copied per control) +""" +import gzip +import io +import json +import pickle +import random +import shutil +import sys +import tarfile +import tempfile +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as v # noqa: E402 + +BASE, _ = v.load('frontier1094') +BLOB = pickle.dumps(BASE, protocol=5) + + +def fresh(): + return pickle.loads(BLOB) + + +def rehash(d): + # a consistent forgery: the template's embedded programs and every call hash follow the edit + d['template']['local_providers']['gauge44']['local_programs'] = pickle.loads(pickle.dumps(d['programs'])) + hashes = {o: v.sha(v.compact(p)) for o, p in d['programs'].items()} + for c in d['template']['calls']: + c['local_program_sha256'] = hashes[c['orientation']] + + +def dim(vectors): + return len(v.basis(vectors)) + + +def odd_orthogonal(rows, n): + """A vector of odd weight orthogonal (mod 2) to every row, or None.""" + pivots = {} # pivot column -> fully reduced row + for r in rows: + for c, p in pivots.items(): + if r >> c & 1: + r ^= p + if r: + c = r.bit_length() - 1 + for k in list(pivots): + if pivots[k] >> c & 1: + pivots[k] ^= r + pivots[c] = r + for f in range(n): + if f in pivots: + continue + x = 1 << f + for c, p in pivots.items(): + if p >> f & 1: + x |= 1 << c + if x.bit_count() & 1: + return x + return None + + +class Controls(unittest.TestCase): + def rejects(self, d, label): + with self.assertRaises(v.Reject) as ctx: + v.check(d) + self.assertTrue(str(ctx.exception).startswith(label), 'rejected by %r, expected %r' % (str(ctx.exception), label)) + + # --- positives + def test_selected_positive_and_order_invariance(self): + self.assertEqual(v.check(fresh())['ledger'], {int(k): n for k, n in BASE['assembly']['complex_profile'].items()}) + d = fresh() + random.Random(78).shuffle(d['template']['idle_children']) + random.Random(79).shuffle(d['frames']) + self.assertEqual(v.check(d)['deficit'], 5120) + + # --- the local programs + def test_climb_rank_relabel(self): + d = fresh() + e = next(e for e in d['programs']['forward'] if e[0] == 'climb' and e[5] == 1) + e[5] = 2 + rehash(d) + self.rejects(d, 'L6') + + def test_non_nested_climb_same_rank(self): + d = fresh() + F = d['word']['frames'] + for e in d['programs']['forward']: + if e[0] == 'climb' and dim(F[e[3]]) > 0: + alt = next((j for j, f in enumerate(F) if dim(f) == dim(F[e[4]]) and not v.nested(F[e[3]], f)), None) + if alt is not None: + e[4] = alt # same dimension difference, frames no longer nested + break + rehash(d) + self.rejects(d, 'L5') + + def test_unknown_program_event(self): + d = fresh() + d['programs']['backward'].append(['child', 1]) + rehash(d) + self.rejects(d, 'L4 closed program vocabulary') + + def test_unknown_schedule_event(self): + d = fresh() + d['template']['execution_schedule'].append({'kind': 'recursive_child', 'replica': 0}) + self.rejects(d, 'L4 closed schedule vocabulary') + + def test_climb_moved_to_another_register(self): + # same rank, same histogram and mass: the frame replay sees the register's chain break + d = fresh() + e = next(e for e in d['programs']['forward'] if e[0] == 'climb' and e[2] < 224 and e[5] == 1) + e[2] = (e[2] + 1) % 224 + rehash(d) + self.rejects(d, 'L5') + + def test_descending_climb(self): + d = fresh() + e = next(e for e in d['programs']['forward'] if e[0] == 'climb' and e[5] == 1) + e[3], e[4] = e[4], e[3] + rehash(d) + self.rejects(d, 'L5') + + def test_broken_chain_same_dimension_nested(self): + # from-frame replaced by a different frame of the same dimension that still lies in the to-frame + d = fresh() + F = d['word']['frames'] + done = False + for e in d['programs']['forward']: + if e[0] == 'climb' and dim(F[e[3]]) > 0: + for j, f in enumerate(F): + if j != e[3] and dim(f) == dim(F[e[3]]) and v.nested(f, F[e[4]]): + e[3] = j + done = True + break + if done: + break + self.assertTrue(done) + rehash(d) + self.rejects(d, 'L5 climb leaves its register') + + def test_centre_direction_flipped(self): + d = fresh() + e = next(e for e in d['programs']['forward'] if e[0] == 'center') + e[2], e[3] = e[3], e[2] + rehash(d) + self.rejects(d, 'L7') + + def test_whole_local_stage_dropped_consistently(self): + # recipe, calls and local sweeps of one pair-0 stage removed together: coverage, bindings, + # hosting and remainders stay consistent; only per-family conservation sees the missing units + d = fresh() + T = d['template'] + stage = next(x['stage'] for x in T['recipe'] if x['kind'] == 'local' and x['pair'] == 0) + T['recipe'] = [x for x in T['recipe'] if not (x['kind'] == 'local' and x['stage'] == stage)] + T['calls'] = [c for c in T['calls'] if c['stage'] != stage] + T['execution_schedule'] = [e for e in T['execution_schedule'] + if not (e['kind'] == 'local_cover_sweep' and e.get('stage') == stage)] + self.rejects(d, 'L21') + + def test_data_route_family_duplicated(self): + d = fresh() + owners = d['template']['calls'][0]['owners'] + owners[0][0] = owners[1][0] + self.rejects(d, 'L10') + + def test_embedded_programs_differ(self): + d = fresh() + d['template']['local_providers']['gauge44']['local_programs']['forward'].append(['scalar']) + self.rejects(d, 'L3 dispatched programs') + + # --- calls + def test_program_hash_swapped(self): + d = fresh() + c = d['template']['calls'][0] + c['local_program_sha256'] = v.sha(v.compact(d['programs']['backward' if c['orientation'] == 'forward' else 'forward'])) + self.rejects(d, 'L3') + + def test_orientation_swap_rehashed(self): + d = fresh() + c = d['template']['calls'][0] + c['orientation'] = 'backward' if c['orientation'] == 'forward' else 'forward' + rehash(d) + self.rejects(d, 'L2') + + def test_duplicate_call(self): + d = fresh() + d['template']['calls'][-1] = pickle.loads(pickle.dumps(d['template']['calls'][-2])) + self.rejects(d, 'L1') + + def test_live_families_changed(self): + d = fresh() + d['template']['cover_final_correction']['charged_calls_per_cover'] -= 1 + self.rejects(d, 'L9') + + def test_extra_bank_padding_child(self): + d = fresh() + d['template']['bank_padding']['children'].append({'rank': 1}) + self.rejects(d, 'L8') + + def test_helper_route_moved_to_another_family(self): + d = fresh() + d['template']['calls'][0]['owners'][224][0] += 1 + self.rejects(d, 'L11') + + def test_short_spectators(self): + d = fresh() + for c in d['template']['calls']: + route = next((desc for _, desc in c['owners'] if desc[0] == 4), None) + if route: + route[4] = route[4][:-1] + break + self.rejects(d, 'L12') + + # --- pending children and hosting + def test_dependent_pending_axis_with_fresh_label(self): + # label-disjoint (a new integer) but F2-dependent on a sibling child's axes + d = fresh() + place = {} + for e in d['template']['execution_schedule']: + if e['kind'] == 'idle_cover_sweep': + for side, ch in enumerate(e['child_indices']): + place[ch] = (e['pair'], side) + rec = d['phases']['recipes'][0] + groups = {} + for ch, ps in place.items(): + if rec['idle_children'][ch]['rank'] >= 2: + groups.setdefault(ps, []).append(ch) + a, b = next(g[:2] for g in groups.values() if len(g) >= 2) + axes_a, axes_b = rec['idle_children'][a]['orthogonal_axes'], rec['idle_children'][b]['orthogonal_axes'] + new = axes_b[0] ^ axes_b[1] + self.assertNotIn(new, axes_a + axes_b) + self.assertEqual(dim(axes_a[1:] + [new]), len(axes_a)) # child a alone stays full rank + axes_a[0] = new + self.rejects(d, 'L15') + + def test_rank0_child_made_pending(self): + # a consistent forgery of DATA-PHASES: a rank-0 child gets one axis that keeps every sibling + # union F2-orthonormal, so only the recount against the emitted remainders sees it + d = fresh() + place = {} + for e in d['template']['execution_schedule']: + if e['kind'] == 'idle_cover_sweep': + for side, ch in enumerate(e['child_indices']): + place[ch] = (e['pair'], side) + recipes = d['phases']['recipes'] + zero = next(ch for ch in place if all(r['idle_children'][ch]['rank'] == 0 for r in recipes)) + for rec in recipes: + union = [x for ch, ps in place.items() if ps == place[zero] for x in rec['idle_children'][ch]['orthogonal_axes']] + axis = odd_orthogonal(union, 73) + self.assertIsNotNone(axis) + rec['idle_children'][zero] = dict(rec['idle_children'][zero], rank=1, orthogonal_axes=[axis]) + self.rejects(d, 'L19') + + def test_slot_gap_kept_consistent(self): + d = fresh() + z = next(z for z in d['owners'] if z['offset'] > 0) + idx = d['owners'].index(z) + z['offset'] += 1 + d['template']['hosting']['pooled_slots'][idx]['offset'] += 1 + for c in d['template']['calls']: + if (c['stage'], c['replica']) == (z['stage'], z['replica']): + c['owners'][224 + z['helper']][1][2] += 1 + self.rejects(d, 'L18') + + def test_owner_map_differs_from_template(self): + d = fresh() + d['owners'][0]['copy'] += 1 # a field no other check reads: only the identity sees it + self.rejects(d, 'L16') + + def test_drop_idle_child(self): + d = fresh() + x = d['template']['idle_children'].pop() + d['frames'] = [f for f in d['frames'] if (f['family'], f['child']) != (x['family'], x['child'])] + self.rejects(d, 'L19') + + def test_idle_hosted_inflated(self): + d = fresh() + x = next(x for x in d['template']['idle_children'] if x['rank'] == 3) + x['hosted'] += 1 + x['pending_offset'] += 1 + x['rank'] -= 1 + self.rejects(d, 'L19') + + def test_dependent_remainder_frame(self): + d = fresh() + f = next(f for f in d['frames'] if len(f['orthogonal_axes']) == 3) + f['orthogonal_axes'][2] = f['orthogonal_axes'][0] ^ f['orthogonal_axes'][1] + self.rejects(d, 'L20') + + # --- the certificate + def test_assembly_profile_tamper(self): + d = fresh() + p = d['assembly']['complex_profile'] + p['48'] -= 1 + p['47'] = 1 + self.rejects(d, 'L23') + + def test_independent_profile_tamper(self): + d = fresh() + d['independent']['1'] += 1 + self.rejects(d, 'L23 ledger equals INDEPENDENT1094') + + +class Packaging(unittest.TestCase): + def rejects(self, label, **kw): + with self.assertRaises(v.Reject) as ctx: + v.load('frontier1094', **kw) + self.assertTrue(str(ctx.exception).startswith(label), str(ctx.exception)) + + def test_decoy_local_programs(self): + self.rejects('B6', members={'local_programs': 'global/base/split-centres/LOCAL-PROGRAMS.json.gz'}) + + def test_decoy_template(self): + self.rejects('B4', members={'template': 'global/base/split-centres/GLOBAL-TEMPLATE.json.gz'}) + + def test_other_owner_map(self): + self.rejects('B7', overrides={'owners': 'research/gauge44-slots-t16/data/OWNERS.json.gz'}) + + def test_flipped_archive_byte(self): + with tempfile.TemporaryDirectory() as tmp: + bad = Path(tmp) / 'capsule.tar.gz' + raw = bytearray((v.ROOT / v.SOURCES['cases']['frontier1094']['archive']['path']).read_bytes()) + raw[len(raw) // 2] ^= 1 + bad.write_bytes(bytes(raw)) + self.rejects('B1', archive_path=bad) + + def test_unsafe_tar_members(self): + for names in (['a.json', 'a.json'], ['../escape.json']): + buf = io.BytesIO() + with tarfile.open(fileobj=buf, mode='w:gz') as tar: + for n in names: + info = tarfile.TarInfo(n) + info.size = 2 + tar.addfile(info, io.BytesIO(b'{}')) + buf.seek(0) + with tarfile.open(fileobj=buf, mode='r:gz') as tar, self.assertRaises(v.Reject) as ctx: + v.safe_members(tar) + self.assertTrue(str(ctx.exception).startswith('B2')) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/frontier1094-emitted-ledger-seed78/verify.py b/research/frontier1094-emitted-ledger-seed78/verify.py new file mode 100644 index 0000000000..619ed1fefb --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/verify.py @@ -0,0 +1,428 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Rebuild a selected complex rank ledger from the emitted program it certifies (independent check). + +Usage: python3 -I -B research/frontier1094-emitted-ledger-seed78/verify.py [--case NAME ...] [--write] + +The selected frontier1094 certificate (ASSEMBLY.json) prices an aggregate complex_profile that its +authors' controller audit derived from the emitted hosted GLOBAL-TEMPLATE. The surcharge-free native +recurrence relies on that profile being the *exact exhaustive recursive-child profile* of the emitted +program (research/native-complex-moment552/PROOF.md). This script rebuilds the profile from the +operations themselves, using only the standard library, reading the committed replay capsule's +members in memory and importing nothing from the repository: + + * every positive-rank climb and centre event of the two dispatched LOCAL-PROGRAMS (equal to the copy + embedded in the template), replayed register by register from the word's start to its final + frames with F2 ranks and nesting recomputed (declared ranks only compared) and centres bound to + their frames and carriers, summed over the calls bound to them by local_program_sha256; + * every nonempty idle remainder, recounted from the DATA-PHASES pending axes of every idle cover + sweep minus the hosted owner-map slices, and matched one for one with the emitted idle_children + and their literal remainder frames; + * with closed event and schedule vocabularies, so nothing else can be a paid child. + +It derives W, N, m and the layout from the program, checks per-family rank conservation (every live +family carries m-1 data/pending units, so rank mass = (m-1)W + (centre mass)N and D = W - 64N), and +requires the rebuilt ledger to equal the certificate's complex_profile. This closes the link +'emitted recursive children = priced profile' under the PR552 classification rule; it does not +re-prove that rule, the no-q-adic-selector argument or the hosting semantics. Aggregates (ASSEMBLY.complex_profile, +OWNERS-AND-PROFILE.paid_profile, INDEPENDENT1094.owner.profile, the word's local_profile) are only +comparison targets. Every check raises Reject(label) through need(), so it also holds under -O. +Expected last line: PASS_FRONTIER1094_EMITTED_LEDGER +""" +import argparse +import gzip +import hashlib +import json +import sys +import tarfile +import time +from collections import Counter, defaultdict +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCES = json.loads((HERE / 'CASES.json').read_text()) +PROGRAM_EVENTS = {'scalar', 'climb', 'adapter', 'residual_adapter', 'phase', 'center'} +SCHEDULE_EVENTS = {'idle_cover_sweep', 'local_cover_sweep', 'bridge', 'terminal', 'terminal_Y_translations', + 'bank_padding_cover_sweep', 'translate_every_live_family'} + + +class Reject(Exception): + """A check failed; the argument is the label of the check.""" + + +def need(ok, label): + if not ok: + raise Reject(label) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def compact(value): + return json.dumps(value, separators=(',', ':')).encode() + + +# ---------------------------------------------------------------- F2 linear algebra on int bitmasks +def basis(vectors): + piv = {} + for v in vectors: + while v: + top = v.bit_length() - 1 + if top not in piv: + piv[top] = v + break + v ^= piv[top] + return piv + + +def inside(v, piv): + while v: + top = v.bit_length() - 1 + if top not in piv: + return False + v ^= piv[top] + return True + + +def nested(small, large): + """dim small < dim large and span(small) is contained in span(large).""" + pl = basis(large) + return all(inside(v, pl) for v in small) + + +# ---------------------------------------------------------------- binding: bytes -> decoded objects +def safe_members(tar): + names = Counter() + for info in tar.getmembers(): + names[info.name] += 1 + need(info.isreg() or info.isdir(), 'B2 archive members are regular files') + need(not info.name.startswith('/') and '..' not in Path(info.name).parts, 'B2 archive member paths') + need(all(n == 1 for n in names.values()), 'B2 archive member names are unique') + return {info.name: info for info in tar.getmembers()} + + +def find_pin(obj, key, value): + if isinstance(obj, dict): + return any((k == key and v == value) or find_pin(v, key, value) for k, v in obj.items()) + if isinstance(obj, list): + return any(find_pin(v, key, value) for v in obj) + return False + + +def load(name, members=None, archive_path=None, overrides=None): + """Check the byte binding of one case and return its decoded inputs. + + members, archive_path and overrides exist for the packaging controls in test_package.py. + """ + case = dict(SOURCES['cases'][name], **(overrides or {})) + members = dict(SOURCES['members'], **(members or {})) + arc = case['archive'] + path = Path(archive_path) if archive_path else ROOT / arc['path'] + raw = path.read_bytes() + need(sha(raw) == arc['sha256'], 'B1 archive digest') + need(find_pin(json.loads((ROOT / arc['pinned_by']).read_text()), arc['path'], arc['sha256']), 'B1 archive pin') + with tarfile.open(path, 'r:gz') as tar: + index = safe_members(tar) + + def member(key): + full = case['prefix'] + members[key] + need(full in index, 'B2 archive member present: ' + key) + return tar.extractfile(index[full]).read() + got = {k: member(k) for k in members} + asm = json.loads(got['assembly']) + binding = dict(archive=arc['path'], archive_sha256=arc['sha256'], member_prefix=case['prefix']) + if case['assembly']: + repo_asm = (ROOT / case['assembly']).read_bytes() + need(repo_asm == got['assembly'], 'B3 repository certificate equals the capsule certificate') + binding['certificate'] = case['assembly'] + binding['certificate_sha256'] = sha(repo_asm) + if case['record']: + # a checkpoint record if the frontier has moved on, otherwise the selected record + for record in case['record']: + rec = json.loads((ROOT / record).read_text()) if (ROOT / record).is_file() else {} + if rec.get('certificate') == case['assembly'] and rec.get('certificate_sha256') == sha(got['assembly']): + binding['record'] = record + break + need('record' in binding, 'B3 record binds the certificate') + template_raw = gzip.decompress(got['template']) + need(sha(template_raw) == asm['template_sha256'], 'B4 template digest') + need(sha(got['owner_audit']) == asm['input_sha256']['owner_audit'], 'B5 owner audit digest') + audit = json.loads(got['owner_audit']) + need(audit['template_sha256'] == asm['template_sha256'], 'B5 owner audit template') + src = audit['source_artifacts'] + for key, art in SOURCES['source_artifact_keys'].items(): + need(sha(got[key]) == src[art], 'B6 dispatched input digest: ' + key) + template = json.loads(template_raw) + need(template['exact_data_phase_recipe_sha256'] == sha(got['data_phases']), 'B6 data phases bound by the template') + receipt = json.loads(got['remainder_receipt']) + frames_raw = gzip.decompress(got['remainder_frames']) + need(receipt['template_sha256'] == asm['template_sha256'] and receipt['uncompressed_frames_sha256'] == sha(frames_raw) + and receipt['source_data_phase_sha256'] == sha(got['data_phases']), 'B8 literal remainder frames') + owners_raw = (ROOT / case['owners']).read_bytes() + need(sha(owners_raw) == template['hosting']['owner_map_sha256'], 'B7 owner map digest') + need(sha(owners_raw) in (ROOT / case['owners_listed_in']).read_text(), 'B7 owner map in the source manifest') + local_replay = json.loads(got['local_replay']) + full_word = None + if case['full_word_pin']: + pin_path, pin_key = case['full_word_pin'] + fw_raw = gzip.decompress(got['full_word']) + need(find_pin(json.loads((ROOT / pin_path).read_text()), pin_key, sha(fw_raw)), 'B9 full word pinned') + full_word = json.loads(fw_raw) + independent = None + if case['independent_profile']: + ind_path, *fields = case['independent_profile'] + independent = json.loads((ROOT / ind_path).read_text()) + for f in fields: + independent = independent[f] + binding.update(template_sha256=asm['template_sha256'], owner_audit_sha256=asm['input_sha256']['owner_audit'], + owner_map=case['owners'], owner_map_sha256=template['hosting']['owner_map_sha256'], + local_programs_gz_sha256=sha(got['local_programs']), canonical_word_gz_sha256=sha(got['canonical_word']), + data_phases_sha256=sha(got['data_phases']), remainder_frames_sha256=sha(frames_raw)) + return dict(template=template, programs=json.loads(gzip.decompress(got['local_programs'])), + word=json.loads(gzip.decompress(got['canonical_word'])), phases=json.loads(got['data_phases']), + frames=json.loads(frames_raw), owners=json.loads(gzip.decompress(owners_raw)), assembly=asm, + audit=audit, local_replay=local_replay, full_word=full_word, independent=independent), binding + + +# ---------------------------------------------------------------- the ledger, from operations +def dot(a, b): + return (a & b).bit_count() & 1 + + +def orthonormal(vectors): + """Pairwise F2 dot products are the identity: implies linear independence (and so a direct sum).""" + return all(dot(a, b) == (i == j) for i, a in enumerate(vectors) for j, b in enumerate(vectors) if j >= i) + + +def program_ledger(program, word, orientation): + """Replay one dispatched program over the canonical frames. + + Every register starts at word['start'], each climb must leave the register's current frame for a + strictly larger frame containing it, and every register must end at word['final']. Centre i goes + from word['center_frames'][i] to the empty frame (forward) or back (backward), with its carrier + register word['centers'][i] sitting at that centre frame. Returns the rank histogram of paid + children, per-register climb units and the centre mass. + """ + frames = word['frames'] + dims = [len(basis(f)) for f in frames] + current = list(word['start']) + hist, per_register, centre_mass, centres_seen = Counter(), Counter(), 0, [] + for e in program: + need(e[0] in PROGRAM_EVENTS, 'L4 closed program vocabulary') + if e[0] == 'climb': + _, _, reg, a, b, declared = e + need(a == current[reg], 'L5 climb leaves its register\'s current frame') + rank = dims[b] - dims[a] + need(rank > 0 and nested(frames[a], frames[b]), 'L5 climbs ascend through nested frames') + need(rank == declared, 'L6 frame-derived climb rank') + current[reg] = b + hist[rank] += 1 + per_register[reg] += rank + elif e[0] == 'center': + _, i, a, b, declared = e + cf, carrier = word['center_frames'][i], word['centers'][i] + need((a, b) == ((cf, b) if orientation == 'forward' else (a, cf)) and dims[b if orientation == 'forward' else a] == 0 + and current[carrier] == cf, 'L7 centre bound to its frame and carrier') + rank = dims[cf] + need(rank > 0 and rank == declared, 'L6 frame-derived centre rank') + centres_seen.append(i) + hist[rank] += 1 + centre_mass += rank + need(current == list(word['final']), 'L5 every register ends at its final frame') + need(sorted(centres_seen) == list(range(len(word['centers']))), 'L7 every centre exactly once') + return hist, per_register, centre_mass + + +def check(d): + T, P, CW, DP = d['template'], d['programs'], d['word'], d['phases'] + provider = T['local_providers']['gauge44'] + V, R, H = CW['v'], CW['R'], CW['h'] + need(provider['local_programs'] == P and provider['v'] == DP['ports'] == V and provider['R'] == R, + 'L3 dispatched programs are the ones embedded in the template') + m, W = T['m'], T['live'] + locals_ = {x['stage']: x for x in T['recipe'] if x['kind'] == 'local'} + pairs = len({x['pair'] for x in locals_.values()}) + F = 2 * pairs * V # live families per replica + cover = T['cover_final_correction'] + need(cover['charged_calls_per_cover'] == W and cover['families'] == [0, W] and W % F == 0, + 'L9 live families W from the program') + replicas = W // F + calls = T['calls'] + N = len(calls) + need(sorted((c['stage'], c['replica']) for c in calls) == [(s, r) for s in sorted(locals_) for r in range(replicas)], + 'L1 call coverage: every (local stage, replica) exactly once') + for e in T['execution_schedule']: + need(e['kind'] in SCHEDULE_EVENTS, 'L4 closed schedule vocabulary') + need(sum(e['kind'] == 'local_cover_sweep' for e in T['execution_schedule']) == N, 'L9 one local sweep per call') + need(not T['bank_padding']['children'], 'L8 no bank-padding children') + + programs = {} + for o, program in P.items(): + programs[sha(compact(program))] = (o, *program_ledger(program, CW, o)) + need(len({c for (_, _, _, c) in programs.values()}) == 1, 'L7 equal centre mass in every orientation') + local_hist, data_units = Counter(), Counter() + slots_at = defaultdict(dict) + for z in d['owners']: + slots_at[(z['stage'], z['replica'])][z['helper']] = z + for c in calls: + need(c['local_program_sha256'] in programs and programs[c['local_program_sha256']][0] == c['orientation'] + and c['provider_id'] == 'gauge44', 'L3 call bound to its dispatched program') + need(c['orientation'] == ('backward' if locals_[c['stage']]['reverse'] else 'forward') + and c['pair'] == locals_[c['stage']]['pair'], 'L2 orientation and pair follow the recipe') + _, hist, per, _ = programs[c['local_program_sha256']] + local_hist.update(hist) + owners = c['owners'] + need(len(owners) == 2 * V + R and len({fam for fam, _ in owners}) == len(owners), + 'L10 one route per owner family in every call') + active = {c['replica'] * F + (2 * c['pair'] + side) * V + port for side in (0, 1) for port in range(V)} + need({fam for fam, desc in owners[:2 * V]} == active and all(desc[0] == 1 for _, desc in owners[:2 * V]), + 'L10 data routes are the active pair families') + for i in range(2 * V): + data_units[owners[i][0]] += per[i] + for i in range(R): + fam, desc = owners[2 * V + i] + z = slots_at[(c['stage'], c['replica'])].get(i) + need(z is not None and fam == z['family'] and desc[0] in (3, 4) and desc[1] == z['child'] and desc[2] == z['offset'] + and (desc[0] == 3) == (z['width'] == 9), 'L11 helper route equals its hosted slot') + if desc[0] == 4: + need(desc[3] == z['width'] and len(desc[4]) == len(set(desc[4])) == 9 - z['width'], 'L12 spectators') + need(per[2 * V + i] == z['width'] == provider['widths'][i], 'L13 helper climb total equals hosted and template width') + + # pending children of every idle cover sweep + place, sweeps = {}, set() + for e in T['execution_schedule']: + if e['kind'] == 'idle_cover_sweep': + for side, ch in enumerate(e['child_indices']): + need(place.setdefault(ch, (e['pair'], side)) == (e['pair'], side), 'L14 child placement is consistent') + sweeps.add((e['replica'], ch)) + axes = defaultdict(dict) + for rec in DP['recipes']: + for ch, item in enumerate(rec['idle_children']): + need(len(item['orthogonal_axes']) == item['rank'], 'L14 pending axes count equals rank') + axes[ch][rec['port']] = item['orthogonal_axes'] + need(set(next(iter(axes.values()))) == set(range(V)), 'L14 every port has a recipe') + rank = {} + for ch, per_port in axes.items(): + ranks = {len(a) for a in per_port.values()} + need(len(ranks) == 1, 'L14 child rank is port independent') + rank[ch] = ranks.pop() + need(sweeps == {(r, ch) for r in range(replicas) for ch in place}, 'L14 every replica sweeps every placed child') + pending = {} + for port in range(V): + by_slot = defaultdict(list) + for ch, (p, s) in place.items(): + by_slot[(p, s)] += axes[ch][port] + for key, vectors in by_slot.items(): + need(orthonormal(vectors), 'L15 sibling pending children are jointly F2-orthonormal') + pending[key + (port,)] = len(vectors) + + need(T['hosting']['pooled_slots'] == d['owners'], 'L16 template slots equal the owner map') + occupied = defaultdict(list) + for z in d['owners']: + p, s = place.get(z['child'], (None, None)) + need(p is not None and rank[z['child']] > 0 and + z['family'] == z['owner_replica'] * F + (2 * p + s) * V + z['port'], 'L17 slot lies in a pending child') + occupied[(z['owner_replica'], z['child'], z['port'])].append((z['offset'], z['width'])) + expect = {} + for (rep, ch), port in ((k, q) for k in sorted(sweeps) for q in range(V)): + if not rank[ch]: + continue + pos = 0 + for off, w in sorted(occupied.get((rep, ch, port), [])): + need(off == pos, 'L18 hosted slices form a contiguous prefix') + pos += w + need(pos <= rank[ch], 'L18 hosted slices fit the pending child') + if pos < rank[ch]: + p, s = place[ch] + expect[(rep * F + (2 * p + s) * V + port, ch)] = dict(replica=rep, port=port, hosted=pos, rank=rank[ch] - pos) + emitted = {} + for x in T['idle_children']: + key = (x['family'], x['child']) + need(key not in emitted and x['replicas'] == 1 and x['pending_offset'] == x['hosted'], 'L19 idle child records') + emitted[key] = dict(replica=x['replica'], port=x['port'], hosted=x['hosted'], rank=x['rank']) + need(emitted == expect, 'L19 emitted idle remainders equal the recount') + need(len(d['frames']) == len(expect), 'L20 one literal frame per remainder') + for f in d['frames']: + e = expect.get((f['family'], f['child'])) + need(e is not None and f['orthogonal_axes'] == axes[f['child']][e['port']][e['hosted']:] + and len(f['orthogonal_axes']) == len(basis(f['orthogonal_axes'])) == e['rank'], 'L20 literal remainder frames') + + for f in range(W): + rep, rest = divmod(f, F) + ps, port = divmod(rest, V) + p, s = divmod(ps, 2) + need(data_units[f] + pending[(p, s, port)] == m - 1, 'L21 per-family rank conservation') + idle = Counter(e['rank'] for e in expect.values()) + ledger = local_hist + idle + mass = sum(r * n for r, n in ledger.items()) + centre = next(iter(programs.values()))[3] + need(mass == (m - 1) * W + centre * N, 'L22 rank mass identity') + need(d['audit']['rank_mass'] == mass and d['audit']['deficit'] == m * W - mass, 'L22 owner audit mass and deficit') + profile = {int(k): v for k, v in d['assembly']['complex_profile'].items()} + need(dict(ledger) == profile, 'L23 ledger equals the certificate complex_profile') + need({int(k): v for k, v in d['audit']['paid_profile'].items()} == profile and d['audit']['live'] == W, + 'L23 ledger equals the owner-audit paid_profile') + if d['independent'] is not None: + need({int(k): v for k, v in d['independent'].items()} == profile, 'L23 ledger equals INDEPENDENT1094') + if d['full_word'] is not None: + fw = d['full_word'] + full = [1 << i for i in range(H)] + for i in range(R): + q = 2 * V + i + width = len(basis(fw['helper_final'].get(str(q), full))) - len(basis(fw['start_extra'].get(str(q), []))) + for program in programs.values(): + need(program[2][q] == width, 'L24 helper climb totals equal the pinned FULL-WORD widths') + per_orientation = {o: dict(sorted(h.items())) for (o, h, _, _) in programs.values()} + replayed = {o: {int(k): n for k, n in p.items()} for o, p in d['local_replay']['paid_profiles'].items()} + need(replayed == per_orientation, 'L25 per-call ledgers equal the in-lineage local replay receipt') + calls_per_family = Counter() + for c in calls: + calls_per_family[c['pair']] += 1 + calls_per_family = {p: n // replicas for p, n in sorted(calls_per_family.items())} + return dict(W=W, N=N, m=m, replicas=replicas, ports=V, helpers=R, centre_mass_per_call=centre, + local_profile_per_call=per_orientation, idle_histogram=dict(sorted(idle.items())), + families_per_call=dict(data=2 * V, helper=R, distinct_owners=2 * V + R), + calls_per_family_by_pair=calls_per_family, local_calls=dict(sorted(Counter(c['orientation'] for c in calls).items())), + pending_children=sum(1 for (rep, ch) in sweeps for _ in range(V) if rank[ch]), + pending_mass=sum(pending[(p, s, q)] for (p, s, q) in pending) * replicas, + hosted_mass=sum(z['width'] for z in d['owners']), remainders=len(expect), + remainder_mass=sum(r * n for r, n in idle.items()), ledger=dict(sorted(ledger.items())), rank_mass=mass, deficit=m * W - mass, + deficit_identity='D = W - %d N' % centre, family_units=m - 1) + + +def run(names): + out = {} + for name in names: + t = time.monotonic() + data, binding = load(name) + result = check(data) + out[name] = dict(binding=binding, **result) + print('PASS', name, 'ledger', result['ledger'], 'mass', result['rank_mass'], 'D', result['deficit'], + '%.1f s' % (time.monotonic() - t), flush=True) + return out + + +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n\n')[0]) + ap.add_argument('--case', action='append', choices=sorted(SOURCES['cases'])) + ap.add_argument('--write', action='store_true', help='write RESULT.json instead of comparing with it') + a = ap.parse_args() + names = a.case or list(SOURCES['cases']) + try: + out = run(names) + except Reject as e: + raise SystemExit('FAIL ' + str(e)) + text = json.dumps(dict(status='PASS_FRONTIER1094_EMITTED_LEDGER', cases=out), indent=1, sort_keys=True) + '\n' + target = HERE / 'RESULT.json' + if a.write: + target.write_text(text) + elif names == list(SOURCES['cases']): + if text != target.read_text(): + raise SystemExit('FAIL RESULT.json differs from this run') + print('PASS RESULT.json reproduced byte for byte') + print('PASS_FRONTIER1094_EMITTED_LEDGER') + + +if __name__ == '__main__': + main() From 4b196b40dcac3ec40f62ec285babac53a1b5a3c5 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 03:15:38 +0530 Subject: [PATCH 2/2] Address soundness review: bind sweeps to calls, slots to executed routes, event payloads to the frame replay; correct claims and credits --- .../README.md | 435 ++++++++++-------- .../RESULT.json | 64 ++- .../SOURCES.json | 18 + .../TASK.json | 8 +- .../VERIFY.json | 4 +- .../test_package.py | 79 +++- .../verify.py | 74 ++- 7 files changed, 435 insertions(+), 247 deletions(-) diff --git a/research/frontier1094-emitted-ledger-seed78/README.md b/research/frontier1094-emitted-ledger-seed78/README.md index e6130045df..222decbe1f 100644 --- a/research/frontier1094-emitted-ledger-seed78/README.md +++ b/research/frontier1094-emitted-ledger-seed78/README.md @@ -9,276 +9,307 @@ ## The obligation The selected certificate `research/community-frontier1094-audit/ASSEMBLY.json` (`1122cb3a…`) prices -the complex profile `{1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866}`. This is -the aggregate that the authors' controller audit (`OWNERS-AND-PROFILE.json`) derived from the -emitted hosted program `GLOBAL-TEMPLATE`, whose digest the certificate records. - -The selected κ uses the native complex recurrence, with no bad-class surcharge. The -[PR552 review](../native-complex-moment552/PROOF.md) allows that only because the emitted controller -has an "exact exhaustive recursive-child profile": -- every positive-rank frame climb and centre descent is a recursive child; -- the profile is the sum over all complete local invocations plus every nonempty idle remainder; -- all other work is finite work paid by the invoice. - -This package closes one link of that argument: **the emitted recursive children equal the priced -profile**, under the review's classification rule (line 17). It does **not** discharge the review's -"no good/bad q-adic selector" argument (line 24), nor the whole-owner hosting semantics. The selected -record pins the review as `research/complex-multicold/vendor/pr559/PROOF.md` (`d5d498ed…`, in -`proof_supplements`), which is byte-identical to `native-complex-moment552/PROOF.md`. - -For #1094, only author code had checked that link: -- the authors' ASYNC audit (`audit_allcold`), which counts declared ranks; -- the in-package #858 `indep16`, which replays the canonical frames but binds the backward profile to - the author-provided local replay receipt. -- The maintainers' `INDEPENDENT1094.json` comes from - `research/community-batch1099-audit/check_frontier1094.py`. It audits the owner map and prices - the profile. It takes the local factor (804384 of the 1041408 rank mass) from the word's - self-reported `local_profile` (line 21), and it hard-codes `live=14336, calls=144` (line 32). -- Open #1209 audits the pending axes and the owner map against package inputs and a parent - template. - -Neither reads the emitted template or the dispatched programs. - -## What only this package does - -`verify.py` uses only the standard library. It reads the committed replay capsule's members in -memory, imports nothing from the repository and executes no package code. - -**Byte binding (B1–B9).** Members are resolved by their full bound path. The capsule also holds -decoy copies (`split-centres/`, `global8/`), and the controls show that they are rejected. -- The capsule digest equals its integration pin. Its tar members are regular, unique and - non-traversing. -- The repository certificate equals the capsule certificate. Both equal the record's - `certificate_sha256`: a checkpoint once the frontier moves on, otherwise the selected record. -- The template digest equals `ASSEMBLY.template_sha256`, and the owner audit digest equals - `ASSEMBLY.input_sha256.owner_audit`. -- `LOCAL-PROGRAMS`, `CANONICAL-WORD`, `DATA-PHASES` and `INDEPENDENT-LOCAL-REPLAY` equal the owner - audit's `source_artifacts`. The data phases also equal the template's own pin. -- The literal remainder frames equal their receipt. -- The owner map equals `owner_map_sha256` and is listed in `SELECTED-SOURCE.json`. -- `FULL-WORD` equals the `SLOT-PINS-k8.json` word. - -**The emitted calls (L1–L13).** -- Every `(local stage, replica)` is called exactly once. -- Orientation and pair follow the recipe. -- Each call is bound to its dispatched program by compact-JSON sha256. -- The program and schedule vocabularies are closed: program events are only `scalar`, `climb`, - `adapter`, `residual_adapter`, `phase` and `center`, and the schedule has seven kinds. This is what - makes "every positive-rank climb/centre, and nothing else" exhaustive. -- Every register's frame is **replayed** in both orientations, from the word's `start` to its - `final` frames: - - each climb must leave the register's current frame for a strictly larger frame containing it; - - its rank is recomputed by F2 elimination, and declared ranks are only compared; - - centre *i* must run from `center_frames[i]` to the empty frame (forward), or back (backward), - with its carrier register sitting at that frame. - - This is the first non-author, frame-derived recount of the dispatched `LOCAL-PROGRAMS` events bound - to the selected template. The programs are also checked to equal those embedded in the template - itself. -- The data routes are the active pair's 224 families, and all 704 owners of a call are distinct. -- Each helper route equals its hosted slot: family, child, offset, width and the structural - spectator count. -- Each helper's climb total equals its hosted width and the template's width vector. -- W, N and m are read from the program. - -**The emitted remainders (L19–L20).** -- The template's `idle_children` equal, one for one, the recount: each idle cover sweep's - `DATA-PHASES` pending child minus its contiguous hosted prefix. -- Every literal `IDLE-REMAINDER-FRAMES` entry is the exact suffix of its pending axes, with full - F2 rank. This checks the consistency of an auxiliary output that does not feed the ledger. -- The pending axes of sibling children are checked to be jointly **F2-orthonormal** on every - `(pair, side, port)`, by pairwise dot products. That implies the direct sum. - -**The chain to the certificate (L21–L25).** -- Every live family carries exactly m−1 = 72 data or pending units, so rank mass = (m−1)W + 64N. - This is a checked accounting identity that pins any error to a single family. It also explains - why D is invariant under repacking. -- The rebuilt ledger equals `ASSEMBLY.complex_profile`, the owner audit's `paid_profile` and - `INDEPENDENT1094.owner.profile`. -- Helper climb totals equal the width vector of the `SLOT-PINS`-pinned `FULL-WORD`. This is a - width-vector match, not a frame-by-frame comparison. -- The per-call ledgers equal the in-lineage local replay receipt. - -The receipt also provides the fields requested in discussion #1200 (item 3), derived from the -emitted program: `local_profile_per_call`, `idle_histogram`, `families_per_call` and -`calls_per_family_by_pair`. - -## Results ([RESULT.json](RESULT.json), reproduced byte for byte on every run) - -The same unchanged code checks four records in the T16/T8 gauge44 layout: +the complex profile `{1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866}`. That +profile is the aggregate that the authors' controller audit (`OWNERS-AND-PROFILE.json`) derived from +the emitted hosted program `GLOBAL-TEMPLATE`, whose digest the certificate records. + +The selected κ uses the native complex recurrence, which has no bad-class surcharge. The review that +allows this is pinned by the selected record as `research/complex-multicold/vendor/pr559/PROOF.md` +(`d5d498ed…`, byte-identical to [native-complex-moment552/PROOF.md](../native-complex-moment552/PROOF.md)). +The review rests on two premises: + +- **(a)** The emitted controller has an *exact exhaustive recursive-child profile* (lines 17 and + 24). Every positive-rank frame climb and centre descent is a recursive child, and the profile is + their sum over all local invocations plus every nonempty idle remainder. +- **(b)** There is *no good/bad q-adic selector* (lines 9 and 24). + +**This package checks part of (a) at source level: the priced aggregate equals the emitted recursive +children of the program the certificate binds.** It does not address (b). It also does not re-prove +the classification rule or the whole-owner hosting semantics. + +### Existing checks of this link + +Author and in-lineage checks: +- `audit_allcold` (the authors' ASYNC audit) reads the template and programs but counts declared + ranks. +- The in-package #858 `indep16` replays the word and binds the backward profile to the receipt. +- `hpe_audit_local.py`, the "PR514/PR433 independent replay" pinned in `SELECTED-SOURCE.json`, + replays both programs' frames. Its receipt `INDEPENDENT-LOCAL-REPLAY.json` is in the capsule. + +Non-author checks: +- The maintainers' `INDEPENDENT1094.json`, produced by + `research/community-batch1099-audit/check_frontier1094.py`, audits the owner map and prices the + profile. It takes the local factor (804384 of the 1041408 rank mass) from the word's self-reported + `local_profile` (line 21) and hard-codes `live=14336, calls=144` (line 32). +- Open #1209 audits the pending axes and the owner map against package inputs and a parent template. + +Neither non-author check reads the emitted template or the dispatched programs. + +## What this package checks + +`verify.py` uses the standard library only. It reads the committed replay capsule's members in +memory, parsing exactly the hashed bytes. It imports nothing from the repository and executes no +package code. + +**New in this package:** +- **Byte binding (B1–B9).** + - The capsule digest matches the integration pin, and the tar members are safe. + - The repository certificate equals the capsule certificate and the record's + `certificate_sha256`. The record is a checkpoint once the frontier moves; otherwise it is the + selected record. + - The template digest equals `ASSEMBLY.template_sha256`, and the owner-audit digest equals + `ASSEMBLY.input_sha256.owner_audit`. + - `LOCAL-PROGRAMS`, `CANONICAL-WORD`, `DATA-PHASES` and `INDEPENDENT-LOCAL-REPLAY` equal the owner + audit's `source_artifacts`. The replay receipt names the same programs and word. + - The literal remainder frames match their receipt. + - The owner map matches the template and the source manifest, and `FULL-WORD` is `SLOT-PINS`-pinned. + - Members are resolved by full path. The `split-centres` copies under `global/` and `global8/` are + decoys, and the controls reject the `global/` ones. `global8/base/providers` holds byte-identical + copies of the bound members. +- **The template's dispatch (L1–L3, L9–L12).** + - Every `(local stage, replica)` is called exactly once. + - The local sweeps of the schedule dispatch exactly those calls (stage, replica and provider), and + every schedule event acts on one replica. + - `gauge44` is the only provider, and each idle sweep occurs once. + - Orientation and pair follow the recipe. + - Each call is bound to its program by compact-JSON sha256, and the programs equal the copy + embedded in the template. + - In every call, the routes are 704 distinct live families, and the data routes are the active + pair's families. + - **Every owner-map slot is executed by exactly one call route** in a live replica, and each + helper route equals its slot. +- **A code-disjoint frame replay of the dispatched programs, bound to those calls (L4–L7).** + - Every register runs from `start` to `final`. + - Each climb leaves the register's current frame for a strictly larger frame that contains it, in + its own phase. Its F2 rank is recomputed, and declared ranks are only compared. + - Centre *i* runs from `center_frames[i]` to the empty frame (forward) or back (backward), in the + `centers` phase, with its carrier register at that frame. + - Adapters and residual adapters sit at their registers' start or final frames, and every scalar + operand is at the scalar's frame tag. + - The phase sequence is fixed, and the program and schedule vocabularies are closed. +- **The chain to the certificate (L23).** The rebuilt ledger equals `ASSEMBLY.complex_profile`, + the owner audit's `paid_profile` and `INDEPENDENT1094.owner.profile`. + +**Cross-checks of existing work (not claimed as new):** +- Against #1209: helper widths (L13); joint F2-orthonormality of sibling pending axes, which implies + the direct sum (L15); contiguous hosted prefixes (L18); and the idle-remainder recount, matched one + for one with the emitted `idle_children` and literal frames (L19–L20). +- Against the in-lineage replay: the per-call ledgers equal its receipt (L25). +- Against #1091 rule R7 and `INDEPENDENT1094`: the mass and deficit identity (L22). +- Per-family conservation (L21): every live family carries m−1 = 72 data or pending units. This is + #1012's coverage identity, checked per family on the emitted T16 programs. It pins any rank-mass + error to a single family. Errors that change the histogram's shape are caught by L23 and L25 + instead. +- The helper climb totals equal the width vector of the pinned `FULL-WORD` (L24). + +The receipt carries `local_profile_per_call` and `idle_histogram` as discussion #1200 item 3 asked. +It also carries `live_families_per_call` (W, N, 896 live families per replica, 9 stages), which +matches #1200's "2·pairs·V/stages", and `owner_families_per_call` (224 data + 480 helper routes). All +four are derived from the emitted program. A package receipt is not the per-record field #1200 asked +for, but it supplies the same values. + +## Results ([RESULT.json](RESULT.json), reproduced byte for byte on every full run) + +The same unchanged code checks the selected record, the previous checkpoint, and two in-capsule +ancestor assemblies. The ancestors are bound only through the capsule pin. All four use the T16/T8 +gauge44 layout. | Case | W | N | Rebuilt ledger | Idle remainders | Rank mass | D = W − 64N | |---|---:|---:|---|---:|---:|---:| | **frontier1094 (selected)** | 14336 | 144 | {1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866} | 7526 | 1041408 | 5120 | | frontier1042 (previous checkpoint) | 14336 | 144 | {1:349577, 2:60193, 3:62608, 4:20448, 5:11808, 7:3, 8:1152, 16:47, 48:4850} | 7550 | 1041408 | 5120 | -| slots T8 (in the 1042 capsule) | 7168 | 72 | {1:174763, 2:30105, 3:31283, 4:10224, 5:5904, 7:54, 8:576, 16:23, 48:2419} | 3783 | 520704 | 2560 | -| leaver T8 (in the 1042 capsule) | 7168 | 72 | {1:174763, 2:30105, 3:30275, 4:12240, 5:4896, 7:54, 8:576, 16:23, 48:2419} | 3783 | 520704 | 2560 | +| slots T8 (in-capsule ancestor assembly) | 7168 | 72 | {1:174763, 2:30105, 3:31283, 4:10224, 5:5904, 7:54, 8:576, 16:23, 48:2419} | 3783 | 520704 | 2560 | +| leaver T8 (in-capsule ancestor assembly) | 7168 | 72 | {1:174763, 2:30105, 3:30275, 4:12240, 5:4896, 7:54, 8:576, 16:23, 48:2419} | 3783 | 520704 | 2560 | For the selected record: - The per-call ledger is `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` in both orientations, with 80 forward and 64 backward calls. -- Families of pairs 0/1/2/3 are called 3/2/2/2 times each. -- Rank mass 1041408 = 144 × (1792 data + 3730 hosted-helper + 64 centre units) + 237024 - idle-remainder units. Equivalently, the pending mass 774144 = 537120 hosted + 237024 remainder. +- Families of pairs 0, 1, 2 and 3 are called 3, 2, 2 and 2 times. +- Rank mass is 1041408 = 144 × (1792 data + 3730 hosted-helper + 64 centre units) + 237024 + idle-remainder units. The pending mass is 774144 = 537120 hosted + 237024 remainder. -In each of the four records, the profile the certificate prices is exactly the recursive-child -ledger of the program it binds. +Each rebuilt ledger equals the assembly it is compared with. -The frontier1042 case shares its programs, word and phases with #1094, so it mainly exercises the -hosting and idle layer. The T8 cases change W and N, and the leaver case also has a different word -and programs. The constants are read from the data (`v`, `h`, `R`, the pairs in the recipe, `m`, -`live`), not hard-coded. +How much each case tests: +- The frontier1042 case shares its programs, word and phases with #1094, so it mainly exercises + hosting and the idle layer. +- The T8 cases change W and N. The leaver case also has a different word and different programs. +- Constants are read from the data (`v`, `h`, `R`, the recipe's pairs, `m`, `live`), not + hard-coded. -## Controls ([test_package.py](test_package.py): 33 tests, about 10 s) +## Controls ([test_package.py](test_package.py): 43 tests, about 10 s) -Each control mutates the decoded inputs and must be rejected **by the named check**. Program edits -are consistent forgeries: the template's embedded copy and every call hash follow the edit. +The four-record positives come from `verify.py`. The test suite runs the frontier1094 positive, plus +a check that the result does not depend on the order of the idle children and remainder frames. -**Frame replay:** -- A climb's declared rank is relabelled (L6). -- A climb is retargeted to a non-nested frame (L5). -- A climb is moved to another register, with the same rank and mass (L5). +Each control mutates the decoded inputs. The test asserts the **first** check that rejects it. +Program edits are consistent forgeries: the template's embedded copy and every call hash follow the +edit. + +**Frame replay** +- A climb's rank is relabelled (L6). +- A climb is given a non-nested target (L5). +- A climb is moved to another register (L5). - A climb is made descending (L5). -- A climb's from-frame is replaced by a different frame of the same dimension that is still nested - (L5 chain). +- A climb's start is chain-broken: a same-dimension nested from-frame (L5). - A centre's direction is flipped (L7). -- An unknown program event, or an unknown schedule kind, is added (L4). +- An adapter is placed at the wrong frame (L5). +- A scalar is placed at the wrong frame (L5). +- An extra phase marker is added (L4). +- An unknown program event or schedule kind is added (L4). -**Calls:** +**Dispatch** - The embedded programs differ from the dispatched ones (L3). - A program hash is swapped (L3). - An orientation is swapped and rehashed (L2). This is a consistency check only, since both - orientations have the same per-call ledger. + orientations have the same ledger. - A call is duplicated (L1). - W is changed (L9). -- A data route's family is duplicated (L10). +- A local sweep is repointed, so one call runs twice and one never (L9). +- A foreign provider is added (L9). +- A sweep acts on several replicas (L9). +- A bank sweep reads the idle children (L8). +- An extra bank-padding child is added (L8). +- A data-route family is duplicated (L10). - A helper route is moved to another family (L11). +- A slot is parked in a phantom replica, leaving a ghost copy (L11). +- A whole pair-0 stage is dropped together with its recipe, calls and sweeps (L11). L21 to L23 would + also reject it. - Spectators are shortened (L12). -- **A whole pair-0 local stage is dropped consistently**, together with its recipe, calls and sweeps. - Every structural check passes, and only per-family conservation sees it (L21). - -**Hosting and remainders:** -- A label-disjoint but F2-dependent pending axis is introduced (L15). -- **A rank-0 child is made pending with an axis that keeps every sibling union orthonormal**. Only - the recount against the emitted remainders sees it (L19). -- A slot gap is introduced and kept consistent across the owner map, template and route (L18). + +**Hosting and remainders** +- A pending axis is made label-disjoint but F2-dependent (L15). +- A rank-0 child is made pending with an axis that keeps every sibling union orthonormal (L19). + L20 to L23 also reject it. +- A slot gap is kept consistent across the map, template and route (L18). - An owner-map field that no other check reads is changed (L16). -- An idle child is dropped, or a mass-preserving hosted/rank shift is applied (L19). +- An idle child is dropped (L19). +- A mass-preserving hosted/rank shift is applied (L19). +- A remainder frame is duplicated (L20). - A remainder frame is made dependent (L20). -**Certificate:** +**Certificate** - The certificate profile is tampered with (L23). - The independent profile is tampered with (L23). -**Packaging:** -- The decoy `split-centres` programs (B6) or template (B4) are substituted. +**Packaging** +- The decoy `split-centres` programs are substituted (B6). +- The decoy `split-centres` template is substituted (B4). +- A foreign local-replay receipt is substituted (B6). - Another record's owner map is substituted (B7). - One capsule byte is flipped (B1). - Duplicate or `..` tar members are added (B2). -**Positives:** the four records, plus invariance under reordering the idle children and the -remainder frames at the decoded level. - ## Reproduce ```sh -python3 -I -B research/frontier1094-emitted-ledger-seed78/verify.py # ~2 s; PASS_FRONTIER1094_EMITTED_LEDGER +python3 -I -B research/frontier1094-emitted-ledger-seed78/verify.py # ~3 s; PASS_FRONTIER1094_EMITTED_LEDGER python3 -I -B -m unittest discover -s research/frontier1094-emitted-ledger-seed78 -p test_package.py python3 scripts/research_package.py --package research/frontier1094-emitted-ledger-seed78 --check-only python3.12 scripts/research_package.py --package research/frontier1094-emitted-ledger-seed78 ``` -The checks need only standard-library Python 3.10 or later; the generic replay uses 3.12. They need -no network, and they pass under `-O` because they use `need()`, not `assert`. Source commits, Git -blobs and SHA256 pins are in [SOURCES.json](SOURCES.json), and the case configuration is in -[CASES.json](CASES.json). No Makefile target is added, because the batch1099 audit pins the Makefile -by digest. +- **Requirements.** Standard-library Python 3.10+; the generic replay uses 3.12. No network is + needed. +- **Checks.** They use `need()`, not `assert`, so they also pass under `-O`. +- **`--case`.** A run limited with `--case` prints `PASS_PARTIAL` and does not compare + `RESULT.json`. +- **Source pins.** Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json), + and the case configuration is in [CASES.json](CASES.json). +- **Records and pins read live.** `certificates/selected-result.json` and the batch integration + JSONs are tagged as provenance. They are read live only to find the record and the archive pin, + so a later frontier move or integration update that keeps the pin does not invalidate the package. +- **No Makefile target.** The batch1099 audit pins the Makefile by digest, so none is added. -## Overlap, prior work and credit for shared checks +## Overlap and credit for shared checks - **Open #1209** (akiva8201-dotcom, head `d1ba2631`, `research/selected1094-pending-axis-audit`) - already checks these: - - the cross-child F2 direct sum on all 896 pending bases, with an XOR-dependent-axis control; - - frame-derived helper widths and contiguous prefixes; + already checks: + - the cross-child pending-axis independence on all 896 bases, with an XOR-dependent control; + - helper widths; + - prefixes; - the idle suffix profile and the complete profile. - Our L15, L13, L18, the idle recount and the L15 control **replicate these as cross-checks**; they - are not claimed as new. #1209 works from package inputs and a parent template. It does not read - the capsule, the emitted template, the programs or the certificate. -- **The authors' in-lineage local replay** (`hpe_audit_local.py`, the "PR514/PR433 independent - replay", pinned in `SELECTED-SOURCE.json`; capsule receipt `INDEPENDENT-LOCAL-REPLAY.json`) already - recounts both dispatched programs. Open **#1184** (woklerx, head `2f1c9e0e`) ports that checker. - - Our recount is **code-disjoint**. L25 compares against that receipt, which is never used as - input. - - That the scalar operations inside the programs respect their frames is covered by that - in-lineage replay and by #1198, not here. -- **The per-family coverage identity** 8k_f + 1 + hosted_f + idle_f = 73, giving mass = 72W + 64N, - is from our open **#1012**, where it is shown on T37/T21. - - Our merged **#1069** observed D = W − 64N on 16 claims. - - Open **#1240** (Mister-Meeseeks) uses the identity as the premise of its packing ceiling and - re-checks it arithmetically on the #1094 profile. Its #1042 idle histogram matches our second + Those are cross-checks here. +- **The in-lineage `hpe_audit_local.py`** replay, ported by open **#1184** (woklerx, head + `2f1c9e0e`), already frame-replays both programs, including their scalar and wrapper frames + (receipt status `PASS_INDEPENDENT_LOCAL_SCALAR_FRAME_AND_WRAPPER_REPLAY`). This package's replay + is code-disjoint and adds the binding to the template's calls, sweeps and owner map. It checks + scalar *frame tags*, not scalar arithmetic. Open **#1149** (woklerx) checks the + canonical-frame rank identity. +- **The coverage identity** is from our open **#1012**. + - Our merged #1069's pricing code, applied to this profile by `INDEPENDENT1094`, records D = W − 64N. + - Open **#1240** (Douglas Colkitt / Mister-Meeseeks) uses the identity as the premise of its + packing ceiling and re-checks it arithmetically. Its #1042 idle histogram matches our second case. - - L21 is the T16 source-level check of that identity on the emitted #1094 and #1042 programs, so - it provides source-level evidence for the premise #1240 assumes. -- **The maintainers' `INDEPENDENT1094.json`** recounts the idle remainders from the owner map. Our - recount is a cross-check of it. -- **#1091** (Josie Elliston, seed67) audits the owner map and excludes the emitted controller. -- **Open #1255** (bitplane, head `add1e267`, `research/selected1094-chart-phase`; claimed in - discussion #1237) audits the exact phase of #1094's residual charts. Our L11–L12 bind only the - route structure and spectator counts. Spectator charts and phases are **not** validated here. -- **Complementary work:** #1112 checks the PR1042 invoice, guards, bootstrap and outer slacks; - #1142 checks PR1042 capsule closure; #1149 checks the canonical-frame rank identity. +- **#1091** (Josie Elliston, seed67) audits the owner map, including rule R7. It excludes the + emitted controller. +- **Open #1255** (bitplane, head `add1e267`; claimed in discussion #1237) audits the exact phase of + the residual charts. L11–L12 bind only route structure and spectator counts. Charts and phases are + **not** validated here. +- **Complementary checks:** + - #1112 (Wronskode): the PR1042 invoice, guards, bootstrap and outer slacks. + - #1142 (martinxxx9): PR1042 capsule closure. + - #1198 (Scratch-net): the scalar macro map and omissions; it excludes frames. ## Trusted, and not checked here -- **Event classification.** That positive-rank climb and centre events are recursive children, and - that scalar, adapter, phase and residual-adapter events are finite work, is PR552's semantics. - Closed vocabularies make the classification exhaustive; they do not re-prove it. -- **Pending axes.** The `DATA-PHASES` pending axes are taken as the inherited PR558 idle-child - subspaces. They are checked for rank, port independence and direct sum. +- **Event classification.** These classifications are the PR552/PR559 semantics: + - positive-rank climb and centre events are recursive children; + - scalar, adapter, phase and residual-adapter events are finite work; + - the non-sweep schedule kinds (`bridge`, `terminal`, `terminal_Y_translations`, + `translate_every_live_family`, `bank_padding_cover_sweep`) are not recursive-child work. + + Closed vocabularies make the classification exhaustive but do not re-prove it. Only + `execution_schedule` is vocabulary-checked, and `async_schedule.source_schedule` is not read. +- **Scalar arithmetic.** It is not re-executed. Only frame tags are bound. +- **Pending axes.** The `DATA-PHASES` axes are taken as the inherited PR558 idle-child subspaces. They + are checked for rank, port independence and joint orthonormality. - **Family layout.** The layout `replica·896 + (2·pair+side)·112 + port` follows #1091's rule R3. - Per-family conservation holds only if this layout is right. -- **Capsule provenance.** The capsule bytes are bound by hash, not re-executed. -- **Downstream pricing.** Moments, the κ reduction, the invoice, guards, bootstrap and the 47 outer - inequalities are not checked. #1069 prices this profile, and #1112 covers the #1042 invoice. -- **Inherited assumptions.** The all-size/compiler, hosting, precision/tape, analytic-transfer and - PR589 H1–H5 assumptions are untouched. + Conservation holds only if it is right. +- **Capsule bytes.** They are bound by hash, not re-executed. +- **Downstream pricing.** Moments, the κ reduction, invoice, guards, bootstrap and the 47 outer + inequalities are not checked. +- **Premise (b) and inherited assumptions.** The review's premise (b), and the all-size/compiler, + hosting, precision/tape, analytic-transfer and PR589 H1–H5 assumptions, are untouched. ## Open next questions -1. **Does the rebuild hold for the mixed-provider T37 templates of the open claims at - 0.0016756–0.0016758?** - - Why it matters: those claims would replace the selected record, and their layout differs from - the T16/T8 gauge44 layout assumed here. - - First step: generalize the provider-dispatch and family-layout bindings, then run the checker - on one claim's maintainer capsule. +1. **Does the rebuild hold for the mixed-provider T37 templates of the open claims?** These include + #1183, #1192, #1193, #1201, #1207, #1218 and #1239. + - Why it matters: they would replace the selected record, and their layout differs from the + T16/T8 gauge44 layout assumed here. + - First step: generalize the provider-dispatch and family-layout bindings, then run the checker on + one claim's maintainer capsule. - Blocked by: no such capsule exists on main yet. -2. **Can the event-kind semantics be checked from the compiler rules, rather than only their - exhaustiveness? Can the review's no-q-adic-selector argument (line 24) and the whole-owner - hosting semantics be checked?** +2. **Can the event-kind classification, premise (b) and the hosting semantics be checked from the + compiler rules?** - First step: state each kind's operator from `notes/general-clifford-frames.tex` and test its fixed-frame action on a toy word. 3. **Do the 73-axis spectator charts and residual phases match the routes bound here?** - - First step: combine #1255's chart-phase criterion with this package's call and route - bindings, so the charts are checked on exactly the routes that are priced. + - First step: combine #1255's chart-phase criterion with this package's call and route bindings, + so that charts are checked on exactly the priced routes. ## Credit -- Rohan Arun, with OpenAI Codex assistance: #1094. -- jeremykothe2, with Claude assistance: PR1087 and the T16 owner-packing lineage. +- Rohan Arun (rohanarun), with OpenAI Codex assistance: #1094. Also the PR987 slot search. +- jeremykothe2, with Claude assistance: PR1087, PR1018 (built on PR987) and the T16 owner-packing + lineage. - FanPUYen: PR858. -- rohanarun: PR987/PR1018. - PR1005, NewBArch PR869, and the retained PR799/741/685/645/589 lineage. -- The PR552 native-complex review, the PR558 data phases and the PR514/PR433 local replay. -- Josie Elliston: seed67 (#1091). +- The PR552/PR559 review, the PR558 data phases, and the PR514/PR433 local replay. +- Josie Elliston: #1091. - akiva8201-dotcom: #1209. -- woklerx: #1184 and #1149. -- Mister-Meeseeks: #1240. +- woklerx: #1184, #1149. +- Douglas Colkitt (Mister-Meeseeks): #1240. - bitplane: #1237/#1255. +- Wronskode: #1112. +- martinxxx9: #1142. +- Scratch-net: #1198. - Douglas Colkitt, with OpenAI Codex assistance: the maintainer replay capsules and the independent pass. Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents selected and designed the check. Two -adversarial judges and a live Discussions sweep found the overlaps above. New material is -Apache-2.0. +adversarial judges, a live Discussions sweep and a post-PR soundness review found the overlaps and +holes fixed above. New material is Apache-2.0. diff --git a/research/frontier1094-emitted-ledger-seed78/RESULT.json b/research/frontier1094-emitted-ledger-seed78/RESULT.json index 089272538b..0a7743f9b2 100644 --- a/research/frontier1094-emitted-ledger-seed78/RESULT.json +++ b/research/frontier1094-emitted-ledger-seed78/RESULT.json @@ -28,11 +28,6 @@ "centre_mass_per_call": 64, "deficit": 5120, "deficit_identity": "D = W - 64 N", - "families_per_call": { - "data": 224, - "distinct_owners": 704, - "helper": 480 - }, "family_units": 72, "helpers": 480, "hosted_mass": 537120, @@ -55,6 +50,12 @@ "16": 47, "48": 4850 }, + "live_families_per_call": { + "N": 144, + "W": 14336, + "per_replica": 896, + "stages": 9 + }, "local_calls": { "backward": 64, "forward": 80 @@ -78,6 +79,11 @@ } }, "m": 73, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, "pending_children": 32256, "pending_mass": 774144, "ports": 112, @@ -114,11 +120,6 @@ "centre_mass_per_call": 64, "deficit": 5120, "deficit_identity": "D = W - 64 N", - "families_per_call": { - "data": 224, - "distinct_owners": 704, - "helper": 480 - }, "family_units": 72, "helpers": 480, "hosted_mass": 537120, @@ -138,6 +139,12 @@ "8": 1152, "48": 4866 }, + "live_families_per_call": { + "N": 144, + "W": 14336, + "per_replica": 896, + "stages": 9 + }, "local_calls": { "backward": 64, "forward": 80 @@ -161,6 +168,11 @@ } }, "m": 73, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, "pending_children": 32256, "pending_mass": 774144, "ports": 112, @@ -194,11 +206,6 @@ "centre_mass_per_call": 64, "deficit": 2560, "deficit_identity": "D = W - 64 N", - "families_per_call": { - "data": 224, - "distinct_owners": 704, - "helper": 480 - }, "family_units": 72, "helpers": 480, "hosted_mass": 268560, @@ -221,6 +228,12 @@ "16": 23, "48": 2419 }, + "live_families_per_call": { + "N": 72, + "W": 7168, + "per_replica": 896, + "stages": 9 + }, "local_calls": { "backward": 32, "forward": 40 @@ -244,6 +257,11 @@ } }, "m": 73, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, "pending_children": 16128, "pending_mass": 387072, "ports": 112, @@ -277,11 +295,6 @@ "centre_mass_per_call": 64, "deficit": 2560, "deficit_identity": "D = W - 64 N", - "families_per_call": { - "data": 224, - "distinct_owners": 704, - "helper": 480 - }, "family_units": 72, "helpers": 480, "hosted_mass": 268560, @@ -304,6 +317,12 @@ "16": 23, "48": 2419 }, + "live_families_per_call": { + "N": 72, + "W": 7168, + "per_replica": 896, + "stages": 9 + }, "local_calls": { "backward": 32, "forward": 40 @@ -327,6 +346,11 @@ } }, "m": 73, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, "pending_children": 16128, "pending_mass": 387072, "ports": 112, diff --git a/research/frontier1094-emitted-ledger-seed78/SOURCES.json b/research/frontier1094-emitted-ledger-seed78/SOURCES.json index ecb99ef2c6..fd32c217da 100644 --- a/research/frontier1094-emitted-ledger-seed78/SOURCES.json +++ b/research/frontier1094-emitted-ledger-seed78/SOURCES.json @@ -32,6 +32,12 @@ "git_blob": "9d60e86c0e494d17bec5e28eda41b275c9ede64e", "sha256": "684c50d1ac69863e1fcc0a34bf76c54bac576f6bbde79b3c67d8432a495c8c1c" }, + { + "path": "research/community-batch1099-audit/check_frontier1094.py", + "usage": "provenance", + "git_blob": "1c171898e4f58fbdeca81424c9932ec2c6bbb9c8", + "sha256": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + }, { "path": "research/community-frontier1042-audit/ASSEMBLY.json", "usage": "input", @@ -74,6 +80,12 @@ "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" }, + { + "path": "research/complex-multicold/vendor/pr559/PROOF.md", + "usage": "provenance", + "git_blob": "9adf304048b62c6db9250a611a8d4b0b60ed8276", + "sha256": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453" + }, { "path": "research/complex-t16-rare-pattern-exchanges/data/OWNERS.json.gz", "usage": "input", @@ -103,6 +115,12 @@ "usage": "input", "git_blob": "8eda84ea0c0f57ca4c14ecb11426874ec2e42886", "sha256": "32ca30cd1c652ef6ad43657273a08a157e1df3545e759ab36306a0d0b516fb4a" + }, + { + "path": "research/native-complex-moment552/PROOF.md", + "usage": "provenance", + "git_blob": "9adf304048b62c6db9250a611a8d4b0b60ed8276", + "sha256": "d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453" } ] } diff --git a/research/frontier1094-emitted-ledger-seed78/TASK.json b/research/frontier1094-emitted-ledger-seed78/TASK.json index 36ecc8065c..33c633e4b4 100644 --- a/research/frontier1094-emitted-ledger-seed78/TASK.json +++ b/research/frontier1094-emitted-ledger-seed78/TASK.json @@ -41,22 +41,22 @@ "scope_status": "refined", "actual_scope": "Rebuild the selected frontier1094 complex rank ledger (and, unchanged, the frontier1042 checkpoint and two T8 ancestors) from the emitted hosted GLOBAL-TEMPLATE and the dispatched LOCAL-PROGRAMS, CANONICAL-WORD and DATA-PHASES that the certificate binds, by code-disjoint standard-library code, and require it to equal the certificate's complex_profile.", "scope_change_reason": "The card's ledger method applied to the one link that INDEPENDENT1094 and #1091/#1209 leave to author code: the emitted program versus the priced aggregate. That link is the 'exact exhaustive recursive-child profile' premise (research/native-complex-moment552/PROOF.md) behind the surcharge-free native complex recurrence of the selected kappa. The moment-enclosure method is not repeated (already triply covered for this record).", - "bottleneck_link": "The selected kappa omits the complex bad-class surcharge because the emitted controller's paid profile is claimed to be exactly the sum of all positive-rank climb/centre children over the local invocations plus every nonempty idle remainder. If the priced aggregate differed from the emitted program, the selected kappa would be mispriced even though the owner-map and pricing checks pass. This package checks that link at source level under the PR552 classification rule; it does not discharge the no-q-adic-selector argument or the hosting semantics, and it does not change kappa.", + "bottleneck_link": "The surcharge-free complex recurrence of the selected kappa rests on two premises of the PR552/PR559 review: (a) an exact exhaustive recursive-child profile (PROOF.md lines 17, 24) and (b) no good/bad q-adic selector (lines 9, 24). This package checks, at source level, that the priced aggregate equals the emitted recursive children of the program the certificate binds, which is part of (a). It does not address (b), the classification rule or the hosting semantics, and it does not change kappa.", "budget_minutes": 180, "stop_rule": "Stop when the rebuilt ledger equals the certificate for the selected record and the unchanged code reproduces the frontier1042 checkpoint, with every semantic and packaging control rejected by its named check; or stop and report a mismatch with its first failing check.", "outcome": "completed", - "evidence": "RESULT.json: frontier1094 ledger {1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866} rebuilt from 144 bound calls (80 forward, 64 backward; per call {1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}) plus 7526 emitted remainders {1:2276, 3:377, 7:7, 48:4866}; all 14336 families carry 72 units; mass 1041408 = 72W + 64N, D = 5120; equals ASSEMBLY, OWNERS-AND-PROFILE and INDEPENDENT1094; frontier1042 and T8 slots/leaver ancestors pass unchanged. test_package.py: 33 tests pass (27 semantic controls including frame-chain, centre-binding and consistent-forgery controls, 5 packaging controls, positives).", + "evidence": "RESULT.json: frontier1094 ledger {1:349604, 2:60192, 3:62585, 4:20448, 5:11808, 7:7, 8:1152, 48:4866} rebuilt from 144 calls dispatched by 144 bound local sweeps (80 forward, 64 backward; per call {1:2412, 2:418, 3:432, 4:142, 5:82, 8:8} by a code-disjoint frame replay) plus 7526 emitted remainders {1:2276, 3:377, 7:7, 48:4866}; every owner-map slot executed by exactly one call route; all 14336 families carry 72 units; mass 1041408, D = 5120; equals ASSEMBLY, OWNERS-AND-PROFILE and INDEPENDENT1094. The frontier1042 checkpoint and two in-capsule T8 ancestor assemblies pass unchanged. test_package.py: 43 tests (36 semantic controls including consistent forgeries found by a post-PR soundness review, 6 packaging controls, positives).", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Substantial: Claude (Anthropic) via Claude Code. Parallel read-only scout and judge subagents selected and designed the check; two adversarial judges and a live Discussions sweep found the overlaps documented in README.md.", "open_questions": [ { - "question": "Does the same emitted-program ledger rebuild hold for the mixed-provider T37 templates of the open claims at 0.0016756-0.0016758 (#1178-#1239)?", + "question": "Does the same emitted-program ledger rebuild hold for the mixed-provider T37 templates of open claims such as #1183, #1192, #1193, #1201, #1207, #1218 and #1239?", "why_it_matters": "Those claims would replace the selected record; their template and provider layout differ from the T16/gauge44 family layout this checker assumes.", "first_step": "Generalize the family-layout and provider-dispatch bindings (provider_dispatch, per-provider LOCAL-PROGRAMS) and run the checker on one such claim's archived replay once a maintainer capsule exists.", "blocked_by": "No maintainer replay capsule for those claims on main yet." }, { - "question": "Can the paid-child semantics themselves (that exactly the positive-rank climb/centre events are recursive children) be proved from the compiler rules rather than taken from the PR552 review?", + "question": "Can the event-kind classification, the review's no-q-adic-selector premise (b) and the whole-owner hosting semantics be checked from the compiler rules rather than taken from the PR552/PR559 review?", "why_it_matters": "This package proves exhaustiveness relative to closed event vocabularies; the classification of each event kind is still an inherited premise of the surcharge-free recurrence.", "first_step": "State the per-event-kind operator semantics from notes/general-clifford-frames.tex and check that scalar/adapter/phase events act within a fixed frame on a toy word.", "blocked_by": "None; needs a careful reading of the pinned notes." diff --git a/research/frontier1094-emitted-ledger-seed78/VERIFY.json b/research/frontier1094-emitted-ledger-seed78/VERIFY.json index f468bf50a7..e830090dfd 100644 --- a/research/frontier1094-emitted-ledger-seed78/VERIFY.json +++ b/research/frontier1094-emitted-ledger-seed78/VERIFY.json @@ -30,7 +30,7 @@ "{package}/verify.py" ], "timeout_seconds": 120, - "checks": "Byte binding (capsule pins, certificate, template, owner audit, dispatched programs/word/phases, owner map, literal remainder frames, FULL-WORD) and the independent ledger rebuild from the emitted program for the selected frontier1094 record, the frontier1042 checkpoint and two T8 ancestors; every rebuilt ledger must equal its certificate; RESULT.json must be reproduced byte for byte." + "checks": "Byte binding (capsule pins, certificate and record, template, owner audit, dispatched programs/word/phases and the local replay receipt, owner map, literal remainder frames, FULL-WORD) and the independent ledger rebuild from the emitted program (dispatch and slot bindings, code-disjoint frame replay, idle recount, conservation) for the selected frontier1094 record, the frontier1042 checkpoint and two in-capsule T8 ancestor assemblies; every ledger must equal its assembly; RESULT.json must be reproduced byte for byte." }, { "argv": [ @@ -46,7 +46,7 @@ "test_package.py" ], "timeout_seconds": 300, - "checks": "Positive and order-invariance fixtures, 27 semantic failure controls (frame replay, centre binding, consistent forgeries) and 5 packaging controls, each rejected by its named check." + "checks": "frontier1094 positive and order invariance, 36 semantic failure controls (frame replay, dispatch, hosting, remainders, certificate; consistent forgeries) and 6 packaging controls, each rejected by the first check it reaches as named." } ] } diff --git a/research/frontier1094-emitted-ledger-seed78/test_package.py b/research/frontier1094-emitted-ledger-seed78/test_package.py index 74c36fdcbb..7553d70020 100644 --- a/research/frontier1094-emitted-ledger-seed78/test_package.py +++ b/research/frontier1094-emitted-ledger-seed78/test_package.py @@ -2,7 +2,7 @@ """Semantic and packaging controls for verify.py: every mutation must be rejected by its named check. Run: python3 -I -B -m unittest discover -s research/frontier1094-emitted-ledger-seed78 -p test_package.py -v -(about a minute; the selected frontier1094 capsule is decoded once and copied per control) +(about 10 s; the selected frontier1094 capsule is decoded once and copied per control) """ import gzip import io @@ -151,8 +151,9 @@ def test_centre_direction_flipped(self): self.rejects(d, 'L7') def test_whole_local_stage_dropped_consistently(self): - # recipe, calls and local sweeps of one pair-0 stage removed together: coverage, bindings, - # hosting and remainders stay consistent; only per-family conservation sees the missing units + # recipe, calls and local sweeps of one pair-0 stage removed together: coverage and dispatch stay + # consistent; the dropped calls' owner-map slots are now executed by no route (conservation, + # mass and the certificate comparison reject it as well) d = fresh() T = d['template'] stage = next(x['stage'] for x in T['recipe'] if x['kind'] == 'local' and x['pair'] == 0) @@ -160,7 +161,7 @@ def test_whole_local_stage_dropped_consistently(self): T['calls'] = [c for c in T['calls'] if c['stage'] != stage] T['execution_schedule'] = [e for e in T['execution_schedule'] if not (e['kind'] == 'local_cover_sweep' and e.get('stage') == stage)] - self.rejects(d, 'L21') + self.rejects(d, 'L11 every owner-map slot') def test_data_route_family_duplicated(self): d = fresh() @@ -173,6 +174,66 @@ def test_embedded_programs_differ(self): d['template']['local_providers']['gauge44']['local_programs']['forward'].append(['scalar']) self.rejects(d, 'L3 dispatched programs') + def test_adapter_at_wrong_frame(self): + d = fresh() + e = next(e for e in d['programs']['forward'] if e[0] == 'adapter' and e[1] == 'old_to_new') + e[3] = 1 if e[3] != 1 else 2 + rehash(d) + self.rejects(d, 'L5 adapter') + + def test_scalar_at_wrong_frame(self): + d = fresh() + e = next(e for e in d['programs']['forward'] if e[0] == 'scalar' and e[1][0] == 'add') + e[2] = e[2] + 1 + rehash(d) + self.rejects(d, 'L5 scalar') + + def test_extra_phase_marker(self): + d = fresh() + d['programs']['forward'].insert(5, ['phase', 'extra_child_rank_48']) + rehash(d) + self.rejects(d, 'L4 phase sequence') + + # --- schedule + def test_local_sweep_repointed(self): + # no program edit: one call is dispatched twice and another never + d = fresh() + e = next(e for e in d['template']['execution_schedule'] + if e['kind'] == 'local_cover_sweep' and e['stage'] == 3 and e['replica'] == 0) + e['stage'] = 0 + self.rejects(d, 'L9 local sweeps dispatch') + + def test_foreign_provider(self): + d = fresh() + T = d['template'] + T['local_providers']['evil'] = pickle.loads(pickle.dumps(T['local_providers']['gauge44'])) + self.rejects(d, 'L9 one local provider') + + def test_multi_replica_sweep(self): + d = fresh() + e = next(e for e in d['template']['execution_schedule'] if e['kind'] == 'local_cover_sweep') + e['replicas'] = [e['replica'], (e['replica'] + 1) % 16] + self.rejects(d, 'L9 schedule events act on one replica') + + def test_bank_sweep_reads_idle_children(self): + d = fresh() + e = next(e for e in d['template']['execution_schedule'] if e['kind'] == 'bank_padding_cover_sweep') + e['children_source'] = 'idle_children' + self.rejects(d, 'L8') + + def test_slot_parked_in_phantom_replica(self): + # one slot moved to a nonexistent replica (route follows), with a ghost copy of the original left + # in the owner map: the idle recount would subtract slices that no call executes + d = fresh() + idx, z = next((i, z) for i, z in enumerate(d['owners']) if z['stage'] == 0 and z['replica'] == 0 and z['helper'] == 0) + ghost = dict(z, stage=99) + for slots in (d['owners'], d['template']['hosting']['pooled_slots']): + slots[idx] = dict(slots[idx], owner_replica=16, family=z['family'] + 16 * 896 - z['owner_replica'] * 896) + slots.append(dict(ghost)) + call = next(c for c in d['template']['calls'] if (c['stage'], c['replica']) == (0, 0)) + call['owners'][224][0] = d['owners'][idx]['family'] + self.rejects(d, 'L11 every owner-map slot') + # --- calls def test_program_hash_swapped(self): d = fresh() @@ -286,6 +347,13 @@ def test_idle_hosted_inflated(self): x['rank'] -= 1 self.rejects(d, 'L19') + def test_duplicate_remainder_frame(self): + d = fresh() + one = next(i for i, f in enumerate(d['frames']) if len(f['orthogonal_axes']) == 1) + big = next(f for f in d['frames'] if len(f['orthogonal_axes']) == 48) + d['frames'][one] = pickle.loads(pickle.dumps(big)) + self.rejects(d, 'L20') + def test_dependent_remainder_frame(self): d = fresh() f = next(f for f in d['frames'] if len(f['orthogonal_axes']) == 3) @@ -318,6 +386,9 @@ def test_decoy_local_programs(self): def test_decoy_template(self): self.rejects('B4', members={'template': 'global/base/split-centres/GLOBAL-TEMPLATE.json.gz'}) + def test_foreign_local_replay_receipt(self): + self.rejects('B6', members={'local_replay': 'global/base/split-centres/INDEPENDENT-LOCAL-REPLAY.json'}) + def test_other_owner_map(self): self.rejects('B7', overrides={'owners': 'research/gauge44-slots-t16/data/OWNERS.json.gz'}) diff --git a/research/frontier1094-emitted-ledger-seed78/verify.py b/research/frontier1094-emitted-ledger-seed78/verify.py index 619ed1fefb..f85c283be4 100644 --- a/research/frontier1094-emitted-ledger-seed78/verify.py +++ b/research/frontier1094-emitted-ledger-seed78/verify.py @@ -17,7 +17,10 @@ * every nonempty idle remainder, recounted from the DATA-PHASES pending axes of every idle cover sweep minus the hosted owner-map slices, and matched one for one with the emitted idle_children and their literal remainder frames; - * with closed event and schedule vocabularies, so nothing else can be a paid child. + * with closed event and schedule vocabularies, every non-paid event (adapters, residual adapters, + scalar operands, phase markers) bound to its register's replayed frame, the local sweeps bound to + the calls and every owner-map slot executed by exactly one call route, so that under the PR552/559 + classification nothing else can be a paid child. It derives W, N, m and the layout from the program, checks per-family rank conservation (every live family carries m-1 data/pending units, so rank mass = (m-1)W + (centre mass)N and D = W - 64N), and @@ -31,6 +34,7 @@ import argparse import gzip import hashlib +import io import json import sys import tarfile @@ -44,6 +48,9 @@ PROGRAM_EVENTS = {'scalar', 'climb', 'adapter', 'residual_adapter', 'phase', 'center'} SCHEDULE_EVENTS = {'idle_cover_sweep', 'local_cover_sweep', 'bridge', 'terminal', 'terminal_Y_translations', 'bank_padding_cover_sweep', 'translate_every_live_family'} +# the program phase markers, in order (both orientations); climbs carry their phase, centres sit in 'centers' +PHASES = ['zero_frame_precondition', 'entry_adapters', 'A', 'centers', 'B', 'cleanup_tail', 'final', + 'exit_adapters', 'full_frame_cleanup', 'done'] class Reject(Exception): @@ -122,7 +129,7 @@ def load(name, members=None, archive_path=None, overrides=None): raw = path.read_bytes() need(sha(raw) == arc['sha256'], 'B1 archive digest') need(find_pin(json.loads((ROOT / arc['pinned_by']).read_text()), arc['path'], arc['sha256']), 'B1 archive pin') - with tarfile.open(path, 'r:gz') as tar: + with tarfile.open(fileobj=io.BytesIO(raw), mode='r:gz') as tar: # parse exactly the hashed bytes index = safe_members(tar) def member(key): @@ -163,6 +170,8 @@ def member(key): need(sha(owners_raw) == template['hosting']['owner_map_sha256'], 'B7 owner map digest') need(sha(owners_raw) in (ROOT / case['owners_listed_in']).read_text(), 'B7 owner map in the source manifest') local_replay = json.loads(got['local_replay']) + need(local_replay['local_programs_sha256'] == sha(got['local_programs']) + and local_replay['canonical_word_sha256'] == sha(got['canonical_word']), 'B6 local replay receipt binds the same programs and word') full_word = None if case['full_word_pin']: pin_path, pin_key = case['full_word_pin'] @@ -206,12 +215,17 @@ def program_ledger(program, word, orientation): """ frames = word['frames'] dims = [len(basis(f)) for f in frames] - current = list(word['start']) - hist, per_register, centre_mass, centres_seen = Counter(), Counter(), 0, [] + start, final = list(word['start']), list(word['final']) + current = list(start) + hist, per_register, centre_mass, centres_seen, phases = Counter(), Counter(), 0, [], [] for e in program: need(e[0] in PROGRAM_EVENTS, 'L4 closed program vocabulary') - if e[0] == 'climb': - _, _, reg, a, b, declared = e + phase = phases[-1] if phases else None + if e[0] == 'phase': + phases.append(e[1]) + elif e[0] == 'climb': + _, tag, reg, a, b, declared = e + need(0 <= reg < len(current) and tag == phase, 'L5 climb is in its phase on a real register') need(a == current[reg], 'L5 climb leaves its register\'s current frame') rank = dims[b] - dims[a] need(rank > 0 and nested(frames[a], frames[b]), 'L5 climbs ascend through nested frames') @@ -222,13 +236,28 @@ def program_ledger(program, word, orientation): elif e[0] == 'center': _, i, a, b, declared = e cf, carrier = word['center_frames'][i], word['centers'][i] - need((a, b) == ((cf, b) if orientation == 'forward' else (a, cf)) and dims[b if orientation == 'forward' else a] == 0 - and current[carrier] == cf, 'L7 centre bound to its frame and carrier') + need(phase == 'centers' and (a, b) == ((cf, b) if orientation == 'forward' else (a, cf)) + and dims[b if orientation == 'forward' else a] == 0 and current[carrier] == cf, + 'L7 centre bound to its frame and carrier') rank = dims[cf] need(rank > 0 and rank == declared, 'L6 frame-derived centre rank') centres_seen.append(i) hist[rank] += 1 centre_mass += rank + elif e[0] == 'adapter': + reg = e[2] + need(e[1] in ('old_to_new', 'new_to_old') and 0 <= reg < len(current) + and e[3] == current[reg] == (start if e[1] == 'old_to_new' else final)[reg], 'L5 adapter at its register\'s frame') + elif e[0] == 'residual_adapter': + reg = e[2] + need(0 <= reg < len(current) and e[3] == start[reg] and e[4:] in ([], [final[reg]]), + 'L5 residual adapter at its register\'s frames') + elif e[0] == 'scalar': + op = e[1] + for operand in op[1:]: + if isinstance(operand, list) and operand and operand[0] == 'L': + need(0 <= operand[1] < len(current) and current[operand[1]] == e[2], 'L5 scalar acts at its registers\' frames') + need(phases == PHASES, 'L4 phase sequence') need(current == list(word['final']), 'L5 every register ends at its final frame') need(sorted(centres_seen) == list(range(len(word['centers']))), 'L7 every centre exactly once') return hist, per_register, centre_mass @@ -252,16 +281,26 @@ def check(d): N = len(calls) need(sorted((c['stage'], c['replica']) for c in calls) == [(s, r) for s in sorted(locals_) for r in range(replicas)], 'L1 call coverage: every (local stage, replica) exactly once') - for e in T['execution_schedule']: + schedule = T['execution_schedule'] + for e in schedule: need(e['kind'] in SCHEDULE_EVENTS, 'L4 closed schedule vocabulary') - need(sum(e['kind'] == 'local_cover_sweep' for e in T['execution_schedule']) == N, 'L9 one local sweep per call') - need(not T['bank_padding']['children'], 'L8 no bank-padding children') + need('replica' not in e or e.get('replicas', [e['replica']]) == [e['replica']], 'L9 schedule events act on one replica') + need(Counter((e['stage'], e['replica'], e['provider_id']) for e in schedule if e['kind'] == 'local_cover_sweep') + == Counter((c['stage'], c['replica'], c['provider_id']) for c in calls), 'L9 local sweeps dispatch exactly the calls') + need(list(T['local_providers']) == ['gauge44'], 'L9 one local provider') + idle_sweeps = Counter((e['replica'], e['pair'], tuple(e['child_indices'])) for e in schedule if e['kind'] == 'idle_cover_sweep') + need(all(n == 1 for n in idle_sweeps.values()), 'L9 every idle sweep once') + need(not T['bank_padding']['children'] and all(e['children_source'] == 'bank_padding.children' for e in schedule + if e['kind'] == 'bank_padding_cover_sweep'), 'L8 no bank-padding children') programs = {} for o, program in P.items(): programs[sha(compact(program))] = (o, *program_ledger(program, CW, o)) need(len({c for (_, _, _, c) in programs.values()}) == 1, 'L7 equal centre mass in every orientation') local_hist, data_units = Counter(), Counter() + slot_keys = Counter((z['stage'], z['replica'], z['helper']) for z in d['owners']) + need(slot_keys == Counter((c['stage'], c['replica'], i) for c in calls for i in range(R)) + and all(0 <= z['owner_replica'] < replicas for z in d['owners']), 'L11 every owner-map slot is executed by exactly one call route') slots_at = defaultdict(dict) for z in d['owners']: slots_at[(z['stage'], z['replica'])][z['helper']] = z @@ -273,8 +312,8 @@ def check(d): _, hist, per, _ = programs[c['local_program_sha256']] local_hist.update(hist) owners = c['owners'] - need(len(owners) == 2 * V + R and len({fam for fam, _ in owners}) == len(owners), - 'L10 one route per owner family in every call') + need(len(owners) == 2 * V + R and len({fam for fam, _ in owners}) == len(owners) + and all(0 <= fam < W for fam, _ in owners), 'L10 one route per live owner family in every call') active = {c['replica'] * F + (2 * c['pair'] + side) * V + port for side in (0, 1) for port in range(V)} need({fam for fam, desc in owners[:2 * V]} == active and all(desc[0] == 1 for _, desc in owners[:2 * V]), 'L10 data routes are the active pair families') @@ -342,7 +381,8 @@ def check(d): need(key not in emitted and x['replicas'] == 1 and x['pending_offset'] == x['hosted'], 'L19 idle child records') emitted[key] = dict(replica=x['replica'], port=x['port'], hosted=x['hosted'], rank=x['rank']) need(emitted == expect, 'L19 emitted idle remainders equal the recount') - need(len(d['frames']) == len(expect), 'L20 one literal frame per remainder') + need(len(d['frames']) == len(expect) and {(f['family'], f['child']) for f in d['frames']} == set(expect), + 'L20 one literal frame per remainder') for f in d['frames']: e = expect.get((f['family'], f['child'])) need(e is not None and f['orthogonal_axes'] == axes[f['child']][e['port']][e['hosted']:] @@ -382,7 +422,8 @@ def check(d): calls_per_family = {p: n // replicas for p, n in sorted(calls_per_family.items())} return dict(W=W, N=N, m=m, replicas=replicas, ports=V, helpers=R, centre_mass_per_call=centre, local_profile_per_call=per_orientation, idle_histogram=dict(sorted(idle.items())), - families_per_call=dict(data=2 * V, helper=R, distinct_owners=2 * V + R), + owner_families_per_call=dict(data=2 * V, helper=R, distinct_owners=2 * V + R), + live_families_per_call=dict(W=W, N=N, per_replica=F, stages=len(locals_)), calls_per_family_by_pair=calls_per_family, local_calls=dict(sorted(Counter(c['orientation'] for c in calls).items())), pending_children=sum(1 for (rep, ch) in sweeps for _ in range(V) if rank[ch]), pending_mass=sum(pending[(p, s, q)] for (p, s, q) in pending) * replicas, @@ -421,6 +462,9 @@ def main(): if text != target.read_text(): raise SystemExit('FAIL RESULT.json differs from this run') print('PASS RESULT.json reproduced byte for byte') + else: + print('PASS_PARTIAL', ' '.join(names), '(RESULT.json not compared)') + return print('PASS_FRONTIER1094_EMITTED_LEDGER')