diff --git a/research/bit-ledger-frame-ranks-seedfeb2/README.md b/research/bit-ledger-frame-ranks-seedfeb2/README.md new file mode 100644 index 0000000000..70702479aa --- /dev/null +++ b/research/bit-ledger-frame-ranks-seedfeb2/README.md @@ -0,0 +1,129 @@ +# bit-ledger-frame-ranks-seedfeb2 + +**Scoped partial audit of the selected bit supplier's paid-rank accounting. No new +kappa; the selected record, the certificate and the suppliers are unchanged.** + +Contributor: Aaron Wang (with help from opencode). Apache-2.0. +Task card: [TASK-CARD.md](TASK-CARD.md); structured metadata: [TASK.json](TASK.json); +machine-readable result: [RESULT.json](RESULT.json). + +## Question + +[research/selected-suppliers-de-diagnostic](../selected-suppliers-de-diagnostic/README.md) +prices both selected ledgers but takes the paid profiles from the published +aggregates, and names as open question 2: can `nine.profile` be rebuilt from the +original gate operations of the pinned +`research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz` word rather than +taken from `EXPECTED.json`? Its stated first step is: compute the per-frame +transition ranks of the word file and compare against `word.local_histogram` and +`nine.profile`. This package closes that first step up to the emitter boundary +(below): the paid-rank **mass** aggregate is re-derived from the word geometry; +the paid-record **histogram** is not. + +This matters for the bit-side coverage identity `D = T(2Kv - L*cst) = W - 63N = +10272`, which the discussion-1587 coverage finding states with the hosted bit +template step marked inferred. + +## What is established + +All numbers below are recomputed by +[verify.py](verify.py) from the pinned word file and `tune/EXPECTED.json`, with +frame dimensions computed here by exact rational rank (no import of the +supplier's checker chain). + +1. **Frame dimensions from operations.** The 636 label frames (live line sets: + closures of the 120 labelled E8 lines, punctured to 111, per `pwordl.py`) have + exact rank spectrum `dim 0:1, 1:111, 2:153, 4:70, 6:180, 7:120, 8:1`. +2. **Per-register net frame climbs.** With each register's recorded start and + final frame ids: every X slot climbs 7 (111 registers), every Y slot climbs 7 + (111 registers), every helper climbs 8 (439 registers). Total net climb is + **5066 = 8R + 14v** for `R = 439`, `v = 111`. +3. **Copy block.** The nine retained totals (`word.ret`, nine distinct helper + registers) carry the recorded copy ranks 7 each: 63 = 9 x 7, equal to the + recorded decoder constant 63. +4. **Paid-rank mass from operations.** 5066 + 63 = **5129 = 8R + 63 + 14v**, + matching `word.legality.rank_mass` and the identity asserted by the supplier's + `verify.sh`. The decomposition (which register class contributes what) is + word-geometric and did not exist outside the checker before this package. +5. **Aggregate cross-consistency.** `word.local_histogram` has weighted sum + `sum(r n_r) = 5129` equal to the re-derived mass; `nine.profile` has weighted + sum 1,808,352 = 64W - (W - 63N) with `W = 32*8*111 = 28416` and + `N = 32*9 = 288`, i.e. the recorded deficit `W - 63N = 10272`. + +Five semantic mutation controls must each be rejected: collapsing the full frame +to one label; setting one register's start frame to its final frame; mutating one +copy rank to 6; a one-count mutation of `local_histogram`; a one-count mutation +of `nine.profile`. + +## Method and independence + +Standard-library Python only, exact `fractions.Fraction` arithmetic. The +verifier reads the pinned gzip word and `tune/EXPECTED.json` directly and checks +their recorded `file_sha256`/`content_sha256` first. It imports nothing from the +supplier's pipeline (`code/gen_p3.py`, `code/xcheck_p.py`, +`e8-bit-carrier-skeleton` checkers, `stage_cohort.py`, `legality_h.cpp`, +`global_k.py`), and it does not run that pipeline. The frame-dimension +convention is derived from `code/pwordl.py`'s word format documentation (frames +are live line sets, closures of the labelled E8 lines) and is validated by the +independent identity 5066 = 8R + 14v across 661 registers. + +## Limits (what is NOT established) + +- The 2920-record `word.local_histogram` is **not** decomposed into per-record + MOVE prices. That decomposition lives in the emitter's register-level event + stream (`COHORT249-RECORDS.bin` via `stage_cohort.py`, priced by + `legality_h.cpp`, needing a C++17 compiler and Boost), which is out of this + session's budget. The histogram is only cross-checked at aggregate level. +- The nine copy ranks (7 each) are the recorded block from `word.copy_ranks`; + they are not re-derived from the word file's gate stream here. +- `nine.profile` is checked at aggregate level only, not rebuilt from the + 32-replica template expansion. +- Nothing here re-checks the moment acceptance, the H1-H5 interface obligations, + hosting/precision admission, or the complex ledger. This is not a + multiplication theorem. + +## Reproduce + +From the repository root (Python 3.10+, standard library only, seconds): + +```sh +python3 -B research/bit-ledger-frame-ranks-seedfeb2/verify.py +python3 scripts/research_package.py --package research/bit-ledger-frame-ranks-seedfeb2 --check-only +``` + +Observed: `PASS_BIT_LEDGER_FRAME_RANKS`, 13 checks plus 5 rejected controls. + +## Open next questions + +- **Record-level histogram from gate operations.** Question: can the 2920-record + `word.local_histogram` be decomposed into per-record MOVE prices and the nine + COPY ranks directly from the A/B/C/D gate streams and the frame menu? Why it + matters: it completes the from-operations rebuild of `nine.profile`'s inputs. + First step: reconstruct each register's frame trajectory from the serialized + gate lists using `pwordl.py`'s `gate`/`climb` convention and compare the + induced MOVE-price histogram with `word.local_histogram`. Blocker: the paid + charging convention is defined by the emitter's event stream + (`stage_cohort.py` + `legality_h.cpp`); free ADDs carry no frames in the word + file. See [TASK.json](TASK.json) for both recorded next questions. +- **Copy ranks from punctured-hyperplane geometry.** Question: is the nine-element + copy-rank block derivable as exact frame dimensions of the nine punctured + hyperplanes? Why it matters: it would make the 63 term of + `rank_mass = 8R + 63 + 14v` fully from-operations. First step: compute the + exact rank of each punctured-hyperplane closure and compare with the recorded + copy rank 7. Blocker: the label-to-copy-frame mapping is defined in the + supplier's emitter/xcheck. + +## Credit + +Prepared by Aaron Wang, with help from opencode (substantial AI assistance; no +independent human review claimed). Predecessor credit: the open question and the +pricing model are from Navinor's +`research/selected-suppliers-de-diagnostic` (itself building on Douglas +Colkitt's pricing model in `autoresearch.md` and +`research/pending-claims-independent-pricing`); the pinned bit word, its format +and its checker chain are the PR589/PR555 lineage (eumemic and predecessors, +retained unchanged by the selected record); the bit-side coverage identity +`mass = 63W + 63N` and the port-direction analysis are ctoth's discussion-1587 +finding with the disclosed reviewing models. An independently corroborated or +superseded contribution still deserves credit; this package adds the +word-geometric decomposition of the mass aggregate that none of those record. diff --git a/research/bit-ledger-frame-ranks-seedfeb2/RESULT.json b/research/bit-ledger-frame-ranks-seedfeb2/RESULT.json new file mode 100644 index 0000000000..12e0d51177 --- /dev/null +++ b/research/bit-ledger-frame-ranks-seedfeb2/RESULT.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "PASS_BIT_LEDGER_FRAME_RANKS", + "frame_dim_spectrum": { + "0": 1, + "1": 111, + "2": 153, + "4": 70, + "6": 180, + "7": 120, + "8": 1 + }, + "net_climb": { + "x_ports": 7, + "y_ports": 7, + "helpers": 8, + "total": 5066 + }, + "copy_mass": 63, + "rank_mass": 5129, + "controls_rejected": 5 +} diff --git a/research/bit-ledger-frame-ranks-seedfeb2/SOURCES.json b/research/bit-ledger-frame-ranks-seedfeb2/SOURCES.json new file mode 100644 index 0000000000..fc403c50a4 --- /dev/null +++ b/research/bit-ledger-frame-ranks-seedfeb2/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e112d71c8d7bb32435debcc54df932593dd8223a", + "files": [ + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ] +} diff --git a/research/bit-ledger-frame-ranks-seedfeb2/TASK-CARD.md b/research/bit-ledger-frame-ranks-seedfeb2/TASK-CARD.md new file mode 100644 index 0000000000..94cf8ec33c --- /dev/null +++ b/research/bit-ledger-frame-ranks-seedfeb2/TASK-CARD.md @@ -0,0 +1,69 @@ +# TASK CARD — agent-39 + +Task ID / proposed scope key: bit-ledger-frame-ranks-seedfeb2 (drawer card: coverage-law-change, +track recursive-interfaces, chooser OS nonce feb25c49413fb33710658d2618c9ea58; scope refined) + +Base commit; exact predecessor and dependency heads: +- Base: e112d71c8d7bb32435debcc54df932593dd8223a (origin/main at session start). +- Predecessor artifact: research/selected-suppliers-de-diagnostic/ (TASK.json open question 2, + "Ledger reconstruction for the bit supplier"), predecessor author Navinor with help from opencode. +- Pinned source: research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz, + content_sha256 5642fd0e35a1acc11acff8d0c08350c1617e95f310d4d35ad63a651f9eeeba0b, + file_sha256 e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f; + tune/EXPECTED.json (word.local_histogram, word.legality, nine.profile). + +Concrete object and question: +Rebuild, code-disjoint, the paid-rank accounting of the pinned PR589/PR555-lineage bit word +directly from its gate operations (A/B/C/D lists, label frames, per-register start/final frame +ids) and check it against the recorded aggregates: word.legality.rank_mass = 5129 = 8R + 63 + 14v, +word.local_histogram, and (if reachable) nine.profile. This is the first step of the open +question above: "compute the per-frame transition ranks of the word file and compare against +word.local_histogram and nine.profile". + +Scope status: refined (a narrowing of the drawn coverage-law-change card). +Reason: the drawn card's headline objects (plane-port coverage law, two-unpaid-coordinate +templates) are saturated with fresh claims and PRs (threads 1516/1587, PR1825/PR1808/PR1900); +agent-37 just closed connector-alphabet-change (PR2056). This object is the unclaimed +precondition the repository itself names for the bit-side coverage law (mass = 63W + 63N, +deficit = W - 63N), which ctoth's thread-1587 finding explicitly leaves "inferred" because the +hosted bit template is not in the tree. + +Existing restriction being changed (or exact claim being audited): +Audited claim: EXPECTED.json aggregates (rank_mass = 8R + 63 + 14v = 5129; local_histogram with +sum of r*n_r = 5129; nine.profile with rank_mass 1808352 = 64W - 10272) hold as a from-operations +fact of the pinned word, not only as outputs of the supplier's own checker chain +(stage_cohort.py + legality_h.cpp + global_k.py). + +Method; explicit parameter ranges/candidate alphabet: +Standard-library Python only. Exact F2/integer linear algebra. Parse the pinned gz word; compute +per-register frame transitions from start/final frame ids and the label-frame menu (rank over F2 +of label vectors), decompose paid mass per register class (ports vs helpers vs retained totals), +and compare every derived aggregate to EXPECTED.json. No import of the supplier's checkers. + +Nearest overlapping PRs and why this adds something: +- research/selected-suppliers-de-diagnostic (merged): prices the aggregates but takes + nine.profile and local_histogram from EXPECTED.json; names this reconstruction as open. +- ctoth's thread-1587 FINDING: derives the bit coverage identity but marks the bit template step + "inferred". +No open PR or fresh claim (last 4 hours, discussions 1166/1167/1317/1516/1587) works on a +from-operations rebuild of the bit ledger. + +Optimistic full cost budget; required observable improvement: +This is an audit, not a construction: no moment change. Budget: exact recomputation reproduces +(contradicts nothing) the recorded aggregates, or isolates the first field that does not follow +from the gate operations. + +Success evidence; falsification test; time/compute cap: +Success: verify.py prints PASS with per-aggregate equality to EXPECTED.json plus semantic failure +controls (mutated word must fail). Falsification: any aggregate mismatch is reported exactly. +Cap: 30 minutes of computation; the emitter-level event-stream rebuild +(COHORT249-RECORDS.bin via stage_cohort.py + legality_h.cpp + C++/Boost) is out of budget and is +recorded as the exact obstruction if the word-level accounting cannot close. + +Predecessor authors; intended artifact and reproduction command: +Predecessors: Navinor (selected-suppliers-de-diagnostic open question), eumemic and predecessors +(PR555/PR589 bit word and checkers), Douglas Colkitt (pricing model). Artifact: +research/bit-ledger-frame-ranks-seedfeb2/ with verify.py and README. Reproduce: +PYTHONUTF8=1 python3 -B research/bit-ledger-frame-ranks-seedfeb2/verify.py + +Attribution: Aaron Wang, with help from opencode. diff --git a/research/bit-ledger-frame-ranks-seedfeb2/TASK.json b/research/bit-ledger-frame-ranks-seedfeb2/TASK.json new file mode 100644 index 0000000000..137ed539a2 --- /dev/null +++ b/research/bit-ledger-frame-ranks-seedfeb2/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 3, + "base_commit": "e112d71c8d7bb32435debcc54df932593dd8223a", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "refined", + "actual_scope": "Code-disjoint reconstruction of the pinned PR589/PR555-lineage bit word's paid-rank mass accounting from its gate operations: frame dimensions by exact rational rank of the live line closures, per-register net frame climbs (X 7, Y 7, helpers 8) summing to 8R + 14v = 5066, plus the recorded nine copy ranks (63) reproducing word.legality.rank_mass = 5129 = 8R + 63 + 14v, with cross-consistency of word.local_histogram and nine.profile at aggregate level.", + "scope_change_reason": "The drawn coverage-law-change card's headline objects (plane-port coverage law, two-unpaid-coordinate templates) are saturated with fresh claims and PRs (discussions 1516/1587; https://github.com/CrocSwap/integer-mult-bounds/pull/1825, https://github.com/CrocSwap/integer-mult-bounds/pull/1808, https://github.com/CrocSwap/integer-mult-bounds/pull/1900), and the sibling agent completed connector-alphabet-change (https://github.com/CrocSwap/integer-mult-bounds/pull/2056). This object is the unclaimed first step the repository itself names for the bit-side coverage law (research/selected-suppliers-de-diagnostic open question 2): ctoth's discussion-1587 finding derives the bit identity mass = 63W + 63N but marks the hosted bit template step inferred, and the aggregates it uses have no from-operations audit. Question and method are a narrowing of the card's coverage-identity audit to the bit word's deficit accounting.", + "bottleneck_link": "The bit side supplies the binding supplier's required budget multiplier; the coverage identity D = 64W - rank_mass = W - 63N = 10272 and every bit-side coverage-law or repacking argument rests on the paid-rank mass aggregate. Re-deriving that aggregate from operations removes the last un-audited input of research/selected-suppliers-de-diagnostic's pricing and pins down which part of the accounting is word-geometric and which part remains emitter-level.", + "budget_minutes": 60, + "stop_rule": "30 minutes of computation; stop at the first aggregate that cannot be re-derived from the word file without the supplier's emitter (stage_cohort.py + legality_h.cpp + C++/Boost), and record that boundary as the exact obstruction instead of restating the checker.", + "outcome": "partial", + "evidence": "research/bit-ledger-frame-ranks-seedfeb2/verify.py prints PASS_BIT_LEDGER_FRAME_RANKS: pinned word file/content sha256; frame dimension spectrum {0:1, 1:111, 2:153, 4:70, 6:180, 7:120, 8:1} over the 636 label frames; X-slot and Y-slot net climbs all 7 (111 each), helper net climbs all 8 (439); total net climb 5066 = 8R + 14v; nine retained totals with recorded copy ranks 7 each giving 63; rank_mass 5129 = 8R + 63 + 14v matching word.legality.rank_mass; local_histogram weighted sum 5129; nine.profile weighted sum 1808352 = 64W - (W - 63N). Five semantic mutation controls are rejected. The 2920-record local_histogram refinement and the emitter-level record stream are not re-derived (see README limits).", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial AI assistance: with help from opencode. No model is cited per donor instruction.", + "open_questions": [ + { + "question": "Can the 2920-record paid histogram word.local_histogram be decomposed into per-record MOVE prices and the nine COPY ranks directly from the A/B/C/D gate streams and the frame menu, without the emitter's register-level expansion?", + "why_it_matters": "It would complete the from-operations rebuild of nine.profile's inputs and turn the recorded histogram into a checkable consequence of the word file.", + "first_step": "Read the gate-frame convention in research/e8-bit-carrier-skeleton/code/ pwordl.py (gate(F, dst, srcs), climb(r, F)) and reconstruct each register's frame trajectory from the serialized A/B/C/D lists, then compare the induced MOVE-price histogram with word.local_histogram.", + "blocked_by": "The paid-rank charging convention is defined by the emitter's event stream (COHORT249-RECORDS.bin via stage_cohort.py) and legality_h.cpp; the word file does not carry per-record frames for free ADDs, so the trajectory reconstruction is a substantial piece of work (the original blocker of research/selected-suppliers-de-diagnostic open question 2)." + }, + { + "question": "Is the nine-element copy-rank block (7 each) derivable from the punctured-hyperplane geometry of the nine punctured labels, as exact frame dimensions, rather than taken from the recorded xcheck block?", + "why_it_matters": "It would make the 63 term of rank_mass = 8R + 63 + 14v fully from-operations and tighten the link between the decoder constant 63 and the label geometry.", + "first_step": "For each punctured label p in word.punctured, form the closed live line set of the p-punctured hyperplane and compute its exact rank; compare with the recorded copy rank 7.", + "blocked_by": "The mapping from punctured labels to the nine retained totals' copy frames is defined in the supplier's emitter/xcheck, not spelled out in the word file." + } + ] +} diff --git a/research/bit-ledger-frame-ranks-seedfeb2/VERIFY.json b/research/bit-ledger-frame-ranks-seedfeb2/VERIFY.json new file mode 100644 index 0000000000..2d58c83120 --- /dev/null +++ b/research/bit-ledger-frame-ranks-seedfeb2/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "research/bit-ledger-frame-ranks-seedfeb2/verify.py" + ], + "checks": "Source binding (file/content sha256), exact frame-dimension spectrum, per-register net climbs 7/7/8 and 8R + 14v = 5066, retained-total copy block, rank_mass = 8R + 63 + 14v = 5129, local_histogram and nine.profile cross-consistency, and five semantic mutation controls that must be rejected.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/tune/EXPECTED.json" + ] +} diff --git a/research/bit-ledger-frame-ranks-seedfeb2/verify.py b/research/bit-ledger-frame-ranks-seedfeb2/verify.py new file mode 100644 index 0000000000..08f4fa9820 --- /dev/null +++ b/research/bit-ledger-frame-ranks-seedfeb2/verify.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +"""Code-disjoint reconstruction of the pinned bit word's paid-rank mass accounting. + +Reads research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz and tune/EXPECTED.json +directly and re-derives, from the gate-operations file alone (frames as live line sets, +per-register start/final frame ids) plus the recorded copy-rank block, the aggregate + + word.legality.rank_mass = 5129 = 8R + 63 + 14v, + +including its per-class decomposition, and cross-checks the recorded histograms against it. +No code is imported from the supplier's checker chain (stage_cohort.py, legality_h.cpp, +global_k.py); frame dimensions are computed here by exact rational rank. + +Usage: python3 -B research/bit-ledger-frame-ranks-seedfeb2/verify.py +Prints PASS_BIT_LEDGER_FRAME_RANKS on success. + +Task card: TASK-CARD.md. Prepared by Aaron Wang, with help from opencode. Apache-2.0. +""" +import copy +import gzip +import hashlib +import json +import os +import sys +from fractions import Fraction + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.abspath(os.path.join(HERE, "..", "..")) +TUNE = os.path.join(ROOT, "research", "e8-bit-p111-tuned", "tune") +WORD_PATH = os.path.join(TUNE, "bitE8mut-p111-tuned.json.gz") +EXP_PATH = os.path.join(TUNE, "EXPECTED.json") + +# Expected frame-dimension spectrum of the 636 label frames (counts by exact rank). +EXPECTED_DIM_SPECTRUM = {0: 1, 1: 111, 2: 153, 4: 70, 6: 180, 7: 120, 8: 1} + + +def qrank(vecs): + """Exact rank over Q of integer row vectors (Gauss-Jordan with fractions).""" + rows = [[Fraction(x) for x in vr] for vr in vecs] + rank = 0 + ncol = len(rows[0]) if rows else 0 + for c in range(ncol): + piv = None + for i in range(rank, len(rows)): + if rows[i][c] != 0: + piv = i + break + if piv is None: + continue + rows[rank], rows[piv] = rows[piv], rows[rank] + pv = rows[rank][c] + rows[rank] = [x / pv for x in rows[rank]] + for i in range(len(rows)): + if i != rank and rows[i][c] != 0: + f = rows[i][c] + rows[i] = [a - f * b for a, b in zip(rows[i], rows[rank])] + rank += 1 + return rank + + +def analyse(w): + """Recompute frame dimensions and per-register net frame climbs from the word.""" + lines = [tuple(x) for x in w["lines"]] + dims = [qrank([lines[i] for i in fset]) for fset in w["frames"]] + net = [dims[w["final"][i]] - dims[w["start"][i]] for i in range(len(w["start"]))] + return dims, net + + +def core_checks(w, exp, silent=False): + ew = exp["word"] + v, R = w["v"], w["R"] + say = (lambda m: print(" ok:", m)) if not silent else (lambda m: None) + + dims, net = analyse(w) + spectrum = {d: dims.count(d) for d in sorted(set(dims))} + if spectrum != EXPECTED_DIM_SPECTRUM: + raise AssertionError("FAIL: frame dimension spectrum " + str(spectrum)) + say("frame dimension spectrum") + + X, Y, H = net[:v], net[v:2 * v], net[2 * v:] + if not (set(X) == {7} and len(X) == v): + raise AssertionError("FAIL: X-slot net climbs " + str(set(X))) + if not (set(Y) == {7} and len(Y) == v): + raise AssertionError("FAIL: Y-slot net climbs " + str(set(Y))) + if not (set(H) == {8} and len(H) == R): + raise AssertionError("FAIL: helper net climbs " + str(set(H))) + total_net = sum(net) + if total_net != 8 * R + 14 * v: + raise AssertionError("FAIL: total net climb %d != 8R + 14v" % total_net) + say("per-register net climbs 7/7/8; 8R + 14v = %d" % total_net) + + # Copy ranks of the nine retained totals: recorded block, 63 = 9 * 7. The + # from-operations term is the climb mass above; the per-copy rank is the + # recorded pin (see README limits). + copy_ranks = ew["copy_ranks"] + if not (len(w["ret"]) == 9 and len(copy_ranks) == 9 + and len(set(w["ret"])) == 9 and all(2 * v <= r < 2 * v + R for r in w["ret"])): + raise AssertionError("FAIL: retained-total shape") + if set(copy_ranks) != {7}: + raise AssertionError("FAIL: copy ranks " + str(set(copy_ranks))) + say("nine retained totals; copy ranks all 7") + + mass = total_net + sum(copy_ranks) + if not (mass == 8 * R + 63 + 14 * v == 5129): + raise AssertionError("FAIL: rank_mass identity " + str(mass)) + if mass != ew["legality"]["rank_mass"]: + raise AssertionError("FAIL: rank_mass != recorded %d" % ew["legality"]["rank_mass"]) + say("rank_mass = 8R + 63 + 14v = %d matches the record" % mass) + + hist = {int(k): n for k, n in ew["local_histogram"].items()} + if sum(r * n for r, n in hist.items()) != mass: + raise AssertionError("FAIL: local_histogram weighted sum") + if not all(0 < r < 8 for r in hist): + raise AssertionError("FAIL: local_histogram ranks") + say("local_histogram weighted sum equals rank_mass") + + # Aggregate cross-consistency of nine.profile with the bit coverage identity + # deficit = W - 63N, W = 32 * 8 * 111, N = 32 * 9 (aggregate level only). + nb, profile = exp["nine"]["bit"], exp["nine"]["profile"] + W, N = nb["live"], 32 * 9 + if W != 32 * 8 * v: + raise AssertionError("FAIL: W != 32 * 8 * v") + if sum(int(r) * n for r, n in profile.items()) != 64 * W - (W - 63 * N): + raise AssertionError("FAIL: nine.profile weighted sum") + if ew["decoder_constant"] != sum(copy_ranks): + raise AssertionError("FAIL: decoder_constant") + say("nine.profile weighted sum = 64W - (W - 63N); decoder_constant = 63") + + +def expect_reject(name, mutate, w, exp): + w2, exp2 = copy.deepcopy(w), copy.deepcopy(exp) + mutate(w2, exp2) + try: + core_checks(w2, exp2, silent=True) + except AssertionError: + print(" ok: control rejected:", name) + return + raise AssertionError("FAIL: control not rejected: " + name) + +def main(): + with gzip.open(WORD_PATH, "rt", encoding="utf-8") as f: + w = json.load(f) + with open(EXP_PATH, encoding="utf-8") as f: + exp = json.load(f) + ew = exp["word"] + + # Source binding: the analysed file is exactly the pinned word. + file_sha = hashlib.sha256(open(WORD_PATH, "rb").read()).hexdigest() + content_sha = hashlib.sha256( + json.dumps(w, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + if file_sha != ew["file_sha256"]: + raise AssertionError("FAIL: word file_sha256 " + file_sha) + if content_sha != ew["content_sha256"]: + raise AssertionError("FAIL: word content_sha256 " + content_sha) + if not ((w["v"], w["R"], w["h"]) == (111, 439, 8) and len(w["frames"]) == 636 + and len(w["start"]) == len(w["final"]) == 2 * w["v"] + w["R"]): + raise AssertionError("FAIL: word shape") + print(" ok: pinned word file/content sha256 and shape") + + core_checks(w, exp) + + # Semantic failure controls: each mutation must be rejected (source binding + # is exercised separately in main; these are the geometric/aggregate checks). + expect_reject( + "full frame collapsed to one label", + lambda w2, e2: w2["frames"].__setitem__(1, [0]), w, exp) + expect_reject( + "one register start frame set to its final frame", + lambda w2, e2: w2["start"].__setitem__(5, w2["final"][5]), w, exp) + expect_reject( + "copy rank mutated to 6", + lambda w2, e2: e2["word"]["copy_ranks"].__setitem__(0, 6), w, exp) + expect_reject( + "local histogram one-count mutation", + lambda w2, e2: e2["word"]["local_histogram"].__setitem__("1", e2["word"]["local_histogram"]["1"] + 1), + w, exp) + expect_reject( + "nine.profile one-count mutation", + lambda w2, e2: e2["nine"]["profile"].__setitem__("1", e2["nine"]["profile"]["1"] - 288), + w, exp) + + print("PASS_BIT_LEDGER_FRAME_RANKS") + + +if __name__ == "__main__": + try: + main() + except AssertionError as e: + print(e) + sys.exit(1)