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..222decbe1f --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/README.md @@ -0,0 +1,315 @@ +# 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}`. 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-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 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. + +Each rebuilt ledger equals the assembly it is compared with. + +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): 43 tests, about 10 s) + +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. + +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 start is chain-broken: a same-dimension nested from-frame (L5). +- A centre's direction is flipped (L7). +- 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). + +**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 ledger. +- A call is duplicated (L1). +- W is changed (L9). +- 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). + +**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 (L19). +- A mass-preserving hosted/rank shift is applied (L19). +- A remainder frame is duplicated (L20). +- 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 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). + +## Reproduce + +```sh +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 +``` + +- **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 and credit for shared checks + +- **Open #1209** (akiva8201-dotcom, head `d1ba2631`, `research/selected1094-pending-axis-audit`) + 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. + + 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. +- **#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.** 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. + 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?** 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 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 that charts are checked on exactly the priced routes. + +## Credit + +- 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. +- PR1005, NewBArch PR869, and the retained PR799/741/685/645/589 lineage. +- The PR552/PR559 review, the PR558 data phases, and the PR514/PR433 local replay. +- Josie Elliston: #1091. +- akiva8201-dotcom: #1209. +- 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, 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 new file mode 100644 index 0000000000..0a7743f9b2 --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/RESULT.json @@ -0,0 +1,364 @@ +{ + "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", + "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 + }, + "live_families_per_call": { + "N": 144, + "W": 14336, + "per_replica": 896, + "stages": 9 + }, + "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, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "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", + "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 + }, + "live_families_per_call": { + "N": 144, + "W": 14336, + "per_replica": 896, + "stages": 9 + }, + "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, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "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", + "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 + }, + "live_families_per_call": { + "N": 72, + "W": 7168, + "per_replica": 896, + "stages": 9 + }, + "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, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "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", + "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 + }, + "live_families_per_call": { + "N": 72, + "W": 7168, + "per_replica": 896, + "stages": 9 + }, + "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, + "owner_families_per_call": { + "data": 224, + "distinct_owners": 704, + "helper": 480 + }, + "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..fd32c217da --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/SOURCES.json @@ -0,0 +1,126 @@ +{ + "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-batch1099-audit/check_frontier1094.py", + "usage": "provenance", + "git_blob": "1c171898e4f58fbdeca81424c9932ec2c6bbb9c8", + "sha256": "2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51" + }, + { + "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-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", + "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" + }, + { + "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 new file mode 100644 index 0000000000..33c633e4b4 --- /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 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 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 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 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." + }, + { + "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..e830090dfd --- /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 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": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_package.py" + ], + "timeout_seconds": 300, + "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 new file mode 100644 index 0000000000..7553d70020 --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/test_package.py @@ -0,0 +1,418 @@ +# 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 10 s; 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 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) + 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, 'L11 every owner-map slot') + + 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') + + 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() + 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_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) + 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_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'}) + + 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..f85c283be4 --- /dev/null +++ b/research/frontier1094-emitted-ledger-seed78/verify.py @@ -0,0 +1,472 @@ +# 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, 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 +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 io +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'} +# 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): + """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(fileobj=io.BytesIO(raw), mode='r:gz') as tar: # parse exactly the hashed bytes + 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']) + 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'] + 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] + 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') + 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') + 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(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 + + +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') + schedule = T['execution_schedule'] + for e in schedule: + need(e['kind'] in SCHEDULE_EVENTS, 'L4 closed schedule vocabulary') + 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 + 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) + 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') + 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) 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']:] + 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())), + 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, + 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') + else: + print('PASS_PARTIAL', ' '.join(names), '(RESULT.json not compared)') + return + print('PASS_FRONTIER1094_EMITTED_LEDGER') + + +if __name__ == '__main__': + main()