From 2e2cb4ffa2785e40f6e3443fec8765e4dade7cff Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Thu, 15 Oct 2026 13:05:07 +0530 Subject: [PATCH 1/2] Exact move prices and owner-fill headroom on the T74 PR2322 words Certifies (exact LP dual, 800-bit enclosures) that every legal whole-helper owner fill of the PR2322 words has b < 0.001697195759, so PR2374 is within 8.1e-10 of the cap. Decomposes the realized PR2312->PR2322 handoffs and PR2269->PR2339 aliases into per-register climb reshapes, which add up exactly. Prices each move type by LP re-solve: a PR2322-type handoff gains 4.27e-8, a low alias loses 1.9e-7, a high alias is exactly neutral, and a (1,1)->(2) climb merge gains 1.13e-7. Lists untried handoff sites (block 53; 12 free (5,1,1,1) X registers). An independent recount by a separate subagent confirms the decomposition and the sites. Research note; no kappa claim. Co-Authored-By: Claude Opus 5.5 --- research/t74-2322-move-prices/README.md | 141 ++ research/t74-2322-move-prices/SOURCES.json | 18 + research/t74-2322-move-prices/TASK.json | 76 + research/t74-2322-move-prices/VERIFY.json | 30 + .../independent_recount.py | 227 ++ research/t74-2322-move-prices/move_prices.py | 379 +++ .../move_prices.receipt.json | 2208 +++++++++++++++++ .../vendor/pr2387/ceiling_lp.py | 345 +++ .../vendor/pr2387/fill_check80.py | 1285 ++++++++++ .../vendor/pr2387/vendor/iter3/price_check.py | 880 +++++++ 10 files changed, 5589 insertions(+) create mode 100644 research/t74-2322-move-prices/README.md create mode 100644 research/t74-2322-move-prices/SOURCES.json create mode 100644 research/t74-2322-move-prices/TASK.json create mode 100644 research/t74-2322-move-prices/VERIFY.json create mode 100644 research/t74-2322-move-prices/independent_recount.py create mode 100644 research/t74-2322-move-prices/move_prices.py create mode 100644 research/t74-2322-move-prices/move_prices.receipt.json create mode 100644 research/t74-2322-move-prices/vendor/pr2387/ceiling_lp.py create mode 100644 research/t74-2322-move-prices/vendor/pr2387/fill_check80.py create mode 100644 research/t74-2322-move-prices/vendor/pr2387/vendor/iter3/price_check.py diff --git a/research/t74-2322-move-prices/README.md b/research/t74-2322-move-prices/README.md new file mode 100644 index 0000000000..71ea1b9caf --- /dev/null +++ b/research/t74-2322-move-prices/README.md @@ -0,0 +1,141 @@ +# Exact move prices and owner-fill headroom on the T74 PR2322 words + +**Research note; no κ claim.** This note gives exact local-move prices and a certified packing cap for the +words of [PR2322](https://github.com/CrocSwap/integer-mult-bounds/pull/2322) (Vlado Vojdanovski). Those +words underlie the current open T74 line: #2349, #2363 and #2374, whose claim is +κ = 0.0016971949509. It answers one planning question: after owner fills, where can the next gain on +these words come from, and how large can it be? + +| finding | value | +|---|---| +| **certified cap, any legal whole-helper owner fill of the PR2322 words** | **b < 0.001697195759** | +| headroom above PR2374's claim | ≤ 8.1e-10 | +| one more PR2322-type handoff (same reshapes) | +4.27e-8 each, linear up to 12 (+5.13e-7) | +| one PR2339-type low alias | −1.91e-7 | +| one PR2339-type high alias | exactly 0 | +| one (1,1)→(2) merge of two rank-1 climbs (no width change) | +1.13e-7 | +| the 26 such target merges that come with PR2339's low aliases, on their own | +2.94e-6 | + +All prices are LP-ceiling differences on the PR2322 words, both providers, at a = PR2374's κ. + +**Owner fills on these words are finished.** The width-aware bin-pattern LP of +[PR2387](https://github.com/CrocSwap/integer-mult-bounds/pull/2387) / +[PR2360](https://github.com/CrocSwap/integer-mult-bounds/pull/2360) is certified with an exact rational +dual and 800-bit enclosures. It caps every legal whole-helper fill of these words at b < 0.001697195759, +with a W·mu margin of 1.85e-7 and zero dual repair. The certificate does not reject PR2374's claimed +point. PR2374 therefore sits within 8.1e-10 of the cap, and further owner relocations on these words can +add at most that much. + +## Mechanism + +Under the frame-climb rule, a climb of d dimensions on a register pays one recursive child of rank d. +Local mass equals 1856 plus the sum of helper widths, and the total rank mass is fixed. So a move changes +b only through the **shape** of the children and through the helper widths, which act via the bin +patterns. + +`move_prices.py` recounts which register pays each child in the pinned words. It checks every recount +against the word's own reported profile and width inventory, then decomposes the realized changes +exactly; the reshapes add up to the profile change with nothing left over. + +- **PR2312 → PR2322.** The four handoffs are: + - remove helpers 619/621/622/623, each (1,1,1,1); + - X lenders 1/4/6/12 go (5,1,1,1)→(2,1,1,1,1,1,1); + - partners 616/617/618/620 go (4,1,1,1,1)→(3,2,1,1,1). + + The local change is {1:−2, 2:+2, 3:+1, 4:−1, 5:−1} with one fewer width-4 helper: a net −1.23e-5 per + call in 66304·mu, a small gain. The LP predicts a +1.96e-7 ceiling gain from PR2312 to PR2322; the + realized claims gained +1.69e-7. The underlying prices, LP-ceiling differences, are what this note + reports. +- **PR2269 → PR2339.** + - A low alias's lender takes over the removed helper's climb: (3,2,1,1,1) is removed and the lender + goes (1,1,1,1)→(2,1,1,1,1,1,1,1). The net local change is −h(3), but the width change costs + +0.04137 per call through the bins, a loss of 5.5e-5 per call. Successive low aliases cost more, + because the LP is convex; this is why all 32 cost −9.8e-6 (PR2387). + - A high alias is exactly price-neutral: its local −h(5) equals its bin cost. + - The 26 targets whose climbs changed each gain exactly one (1,1)→(2) merge. That merge has no width + effect and is worth +1.13e-7 by itself. + +The independent recount (`independent_recount.py`) was written by a separate AI reviewer subagent +from a plain statement of the frame rules, with its own GF(2) code and no shared code. It reproduces +both providers' profiles, the exact PR2312→PR2322 change set and the site lists below. + +## Untried sites (leads, not constructions) + +- 33 helpers of the PR2322 words still climb (1,1,1,1). These are the 32 PR2226 low lenders 273..394 + plus 653. +- 12 X registers, 31 33 49 55 68 74 80 83 85 88 98 101, still climb (5,1,1,1) and lend no warp. + These are the shapes of PR2322's four lenders before the handoff. +- Block 53 (registers 648–655) has exactly PR2322's pre-handoff pattern: helper 653 (1,1,1,1) next to + four (4,1,1,1,1) partners 648/649/650/652. Its other three slots were already removed. PR2374 notes + that alias 653 was dropped when 651 moved to lender 530. +- The other blocks pair (1,1,1,1) helpers with (4,1,1,1,1,1) mates. + +If each extra handoff reproduced PR2322's reshapes, k handoffs would add k × 4.27e-8, up to 12 by the +lender count. Whether any of them admits a coherent rank-zero handoff (frame availability, lifetimes, +warp images, native lowering) is **not checked here**. + +## Reproduce + +From the repository root, standard library only: + +```sh +python3 -I -B research/t74-2322-move-prices/move_prices.py --fetch # ~16 s +python3 -I -B research/t74-2322-move-prices/independent_recount.py # ~10 s +``` + +`--fetch` fetches `refs/pull/{2312,2322,2269,2339}/head` from the canonical repository if the pinned +commits are absent. The pinned commits are fb76f799, 002304ef, b479fc55 and bf1742ae; each word file +is blob- and sha256-pinned. + +Expected final lines: +- `PASS_T74_MOVE_PRICES cap=0.001697195759 handoff_db=+4.272e-08 low_alias_db=-1.906e-07 high_alias_net=0 sites=33/12` +- `PASS_T74_INDEPENDENT_RECOUNT` + +`vendor/pr2387/` holds byte copies of this author's PR2387 `ceiling_lp.py` and `fill_check80.py` and the +iteration-3 enclosure code, all pinned. `move_prices.py` patches one line of `local_recount` at load time, +to record the register that pays each child. All results were run on CPython 3.14.4; the registered +Python 3.12 replay was not run locally. + +## Scope and limits + +This is a pricing screen on fixed, pinned words: + +- Moves are priced only by their per-register climb reshapes and width change, through the bin-pattern + LP. Windows, families and ports are dropped, so prices are ceiling differences, not realized gains. +- The cap is a certified relaxation ceiling for unsplit helpers on the unchanged PR2269 bin stock, not + a κ. +- No new handoff or merge is constructed. +- Prices are first-order in the sense that they are measured at the PR2322 operating point. The low- + alias row shows that the LP is convex, so large moves need a re-solve, which the script does for the + ladder. + +## Open next questions + +- **Block 53 handoff.** Does helper 653 admit a PR2322-type coherent handoff to a free (5,1,1,1) X + register, with partners 648/649/650/652? The first step is to rerun PR2322's handoff generator with + 653 as the target role. Its price is +4.27e-8. PR2374 dropped alias 653, so its lender conflict is the + blocker to check. +- **Target merges without low aliases.** The +2.94e-6 from the 26 (1,1)→(2) target merges dwarfs the + owner-fill race. Can those merges be obtained without the width-9 low-lender inventory change? The + first step is to identify which B-gate frames changed on those targets in the PR2339 words, and + whether the anticipatory initial corrections (PR2394 lowers their prefix natively) can be kept with + the original helpers. Note that #1995/#2013 bound frame freedom inside a fixed scalar word, so this + needs a changed premise. +- **More handoff patterns.** Which X shapes other than (5,1,1,1), and which partner shapes, give + positive prices? The first step is to tabulate prices for every (lender shape, partner shape) pair + that occurs in the words. + +## Credits and licence + +- PR2322 (Vlado Vojdanovski): handoffs and words. +- PR2312 and PR2269 (Jeremy Kothe): width exchange and borrow43 words. +- PR2374 and PR2349 (jeremykothe2) and PR2363 (mason-hale): owner fills on PR2322's words. +- PR2226 (Cinna Davis / 1337isnot1337): anticipatory borrowing. +- PR2339 and PR2387 (this author). +- PR2360 (Jeremy Diviney) and PR1129 (Ali Romman): pattern-dual relaxation. +- PR2394 (commdata2338): native anticipatory prefix. +- PR1995 and PR2013: fixed-word frame bounds. +- PR1319 and PR1297: T74 lineage. + +Prepared with substantial AI assistance (Claude Code, Anthropic, Claude Opus 5.5). The independent +recount was written by an AI subagent; no independent human review is claimed. Apache-2.0. diff --git a/research/t74-2322-move-prices/SOURCES.json b/research/t74-2322-move-prices/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/t74-2322-move-prices/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/t74-2322-move-prices/TASK.json b/research/t74-2322-move-prices/TASK.json new file mode 100644 index 0000000000..360623698a --- /dev/null +++ b/research/t74-2322-move-prices/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "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": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "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": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "On the PR2322 T74 words (the base of the open PR2349/PR2363/PR2374 line): what is the certified owner-fill headroom, and what is the exact LP-ceiling price of each realized or candidate local inventory move (PR2322 handoffs, PR2339 low/high aliases, rank-1 climb merges), with a census of untried PR2322-pattern handoff sites?", + "scope_change_reason": "The card asks whether a new local cost interface can beat current packing. For the live T74 line the useful narrowing is to price concrete inventory moves on the actual PR2322 words with the width-aware LP, after showing packing itself is exhausted, so constructors can see which interface changes are worth building.", + "bottleneck_link": "The complex supplier binds. On the PR2322 words, owner fills are within 8.1e-10 of a certified cap, so further T74 gains must come from local inventory or climb-shape changes; this package prices those moves exactly and points to the largest (rank-1 climb merges, +1.13e-7 each).", + "budget_minutes": 90, + "stop_rule": "Stop after the certified cap, exact decomposition of the two realized changes, prices of four move types, an independent recount and the site census; no handoff construction in this session.", + "outcome": "completed", + "evidence": "move_prices.py: per-register recount of 8 pinned words (each equal to its reported profile and inventory), exact decompositions PR2312->PR2322 and PR2269->PR2339, LP prices, calibration (LP +1.96e-7 vs realized +1.69e-7), certified cap b < 0.001697195759 for every legal whole-helper fill of the PR2322 words (PR2374 not rejected). independent_recount.py (separate implementation by an AI reviewer subagent) reproduces profiles, the change set and the site lists.", + "author": "Sagar Thakrar", + "ai_assistance": "Prepared with substantial AI assistance: Claude Code (Anthropic, Claude Opus 5.5) wrote move_prices.py and this text; a separate Claude subagent wrote independent_recount.py from a plain-language rule statement without access to the package code. No independent human review is claimed.", + "open_questions": [ + { + "question": "Does helper 653 of the PR2322 words admit a PR2322-type coherent handoff to a free (5,1,1,1) X register with partners 648/649/650/652?", + "why_it_matters": "Block 53 has exactly PR2322's pre-handoff shape pattern; the move is priced at +4.27e-8, about a third of the whole PR2363->PR2374 owner gain.", + "first_step": "Rerun PR2322's handoff generator with role 653 and each of the 12 free (5,1,1,1) X registers as candidate lenders.", + "blocked_by": "PR2374 dropped alias 653 when moving 651 to lender 530; lender/lifetime conflicts are unchecked here." + }, + { + "question": "Can the 26 (1,1)->(2) target-climb merges that accompany PR2339's low aliases be obtained without the width-9 low-lender inventory change?", + "why_it_matters": "On their own they are worth +2.94e-6 on the PR2322 words, far above any remaining owner-fill gain, while the low-alias inventory change is what makes PR2339 lose.", + "first_step": "Diff the B-gate frames on those 26 targets between the PR2269 and PR2339 words to see whether the merge comes from the anticipatory initial corrections or from the removed helpers.", + "blocked_by": "PR1995/PR2013 bound frame freedom within a fixed scalar word; a changed premise (anticipatory corrections) is needed and its native lowering (PR2394) is only partly done." + }, + { + "question": "Which other (lender shape, partner shape) handoff patterns occurring in the PR2322 words have positive prices?", + "why_it_matters": "Only (5,1,1,1) lenders are priced here; the 12 such registers limit PR2322-type handoffs to +5.1e-7.", + "first_step": "Enumerate per-register shapes of all X registers and helpers and price each feasible-looking reshape pair with move_prices.applied().", + "blocked_by": "Legality of a handoff depends on frame availability and lifetimes that the pricing screen does not model." + } + ] +} diff --git a/research/t74-2322-move-prices/VERIFY.json b/research/t74-2322-move-prices/VERIFY.json new file mode 100644 index 0000000000..b32132930c --- /dev/null +++ b/research/t74-2322-move-prices/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/move_prices.py", + "--fetch" + ], + "timeout_seconds": 300, + "checks": "Fetches pinned PR2312/2322/2269/2339 heads if absent; recounts 8 pinned words against their reports; exact decompositions; prices four move types; certifies the PR2322-word owner-fill cap b < 0.001697195759 and checks PR2374 is not rejected (control). Expect PASS_T74_MOVE_PRICES." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_recount.py" + ], + "timeout_seconds": 300, + "checks": "Separate implementation: both providers' profiles equal the reports; exact PR2312->PR2322 change set; 33 (1,1,1,1) helpers and 12 free (5,1,1,1) X registers. Expect PASS_T74_INDEPENDENT_RECOUNT." + } + ] +} diff --git a/research/t74-2322-move-prices/independent_recount.py b/research/t74-2322-move-prices/independent_recount.py new file mode 100644 index 0000000000..2d90b330c6 --- /dev/null +++ b/research/t74-2322-move-prices/independent_recount.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent recount of per-register paid child ranks of the pinned PR2312 and PR2322 T74 words. + +Written by an independent AI reviewer subagent (Claude Code, Anthropic) from a plain-language statement of the +BORROW-WORD frame-climb rules only; it imports and copies nothing from move_prices.py or its vendored PR2387 code +(own GF(2) span / nesting / orthogonal-complement logic). It re-derives, for both providers: each word's reported +local profile; the exact PR2312 -> PR2322 change set (4 removed (1,1,1,1) helpers, X lenders 1/4/6/12 +(5,1,1,1) -> (2,1,1,1,1,1,1), partners 616/617/618/620 (4,1,1,1,1) -> (3,2,1,1,1), nothing else); the 33 remaining +(1,1,1,1) helpers and the 12 unused (5,1,1,1) X registers. Apache-2.0. + +Usage: python3 -I -B independent_recount.py [--repo PATH] (needs the PR2312 / PR2322 commits; see move_prices.py --fetch) +""" +import argparse +import gzip +import hashlib +import os +import subprocess +import json +import sys +from collections import Counter + +H = 9 +FULL_MASK = (1 << H) - 1 +NX, NY = 112, 112 +Y0 = NX +HELP0 = NX + NY + + +def reduce_basis(vecs): + """Return a canonical reduced row echelon basis (tuple of ints) for span(vecs).""" + piv = {} # leading bit -> vector + for v in vecs: + v &= FULL_MASK + while v: + lb = v.bit_length() - 1 + if lb in piv: + v ^= piv[lb] + else: + piv[lb] = v + break + # full reduction + keys = sorted(piv, reverse=True) + for k in keys: + for k2 in keys: + if k2 != k and (piv[k2] >> k) & 1: + piv[k2] ^= piv[k] + return tuple(sorted(piv.values(), reverse=True)) + + +def span(lst): + return reduce_basis(lst or []) + + +def contains(big, small): + """small subset of big (both reduced bases).""" + return len(reduce_basis(list(big) + list(small))) == len(big) + + +def dot(a, b): + return bin(a & b).count("1") & 1 + + +def orth_complement(basis): + return reduce_basis([w for w in range(1, FULL_MASK + 1) + if all(dot(w, b) == 0 for b in basis)]) + + +FULL = span([1 << i for i in range(H)]) + + +def recount(word): + removed = set(word["removed"]) + ports = word["ports"] + R = word["report"]["R"] + nreg = HELP0 + R + cur = {} + for i in range(NX): + cur[i] = span([ports[i]]) + for i in range(NY): + cur[Y0 + i] = () + for r in range(HELP0, nreg): + cur[r] = () + for k, fr in word.get("start_extra", {}).items(): + cur[int(k)] = span(fr) + paid = {r: [] for r in range(nreg)} + issues = [] + touched_removed = Counter() + + def move(r, F, where): + if r in removed: + touched_removed[r] += 1 + return + c = cur[r] + if not contains(F, c): + issues.append((where, r, c, F)) + return + d = len(F) - len(c) + if d > 0: + paid[r].append(d) + cur[r] = F + + def gate_regs(g): + if g[0] == "add": + return [g[1], g[2]], g[5] + if g[0] == "scale": + return [g[1]], g[4] + raise ValueError(g) + + # precondition / compensation / initial_corrections: pay nothing, but check + # that they do not touch removed registers. + for sec in ("initial_corrections", "precondition", "compensation"): + for g in word.get(sec, []): + regs, fr = gate_regs(g) + for r in regs: + if r in removed: + touched_removed[r] += 1 + for idx, g in enumerate(word["A"]): + regs, fr = gate_regs(g) + F = span(fr) + for r in regs: + move(r, F, ("A", idx)) + # cut: copy reads, ignored for climbs + for g in word["cut"]: + for r in gate_regs(g)[0]: + if r in removed: + touched_removed[r] += 1 + warps_at = {} + for w in word["warps"]: + warps_at.setdefault(w[0], []).append(w) + B = word["B"] + + def apply_warps(pos): + for (p, lender, cols, U, E) in warps_at.get(pos, []): + if lender in removed: + touched_removed[lender] += 1 + continue + if cur[lender] != span(U): + issues.append((("warp", pos), lender, cur[lender], span(U))) + cur[lender] = span(E) + + for pos, g in enumerate(B): + apply_warps(pos) + regs, fr = gate_regs(g) + F = span(fr) + for r in regs: + move(r, F, ("B", pos)) + apply_warps(len(B)) + bad_warp_pos = [p for p in warps_at if not 0 <= p <= len(B)] + for idx, g in enumerate(word["restore"]): + regs, fr = gate_regs(g) + F = span(fr) + for r in regs: + move(r, F, ("restore", idx)) + hf = {int(k): span(v) for k, v in word.get("helper_final", {}).items()} + for r in range(nreg): + if r in removed: + continue + if r < NX: + E = FULL + elif r < HELP0: + E = orth_complement(span([ports[r - Y0]])) + else: + E = hf.get(r, FULL) + move(r, E, ("final", r)) + live = {r: tuple(sorted(paid[r], reverse=True)) for r in range(nreg) if r not in removed} + prof = Counter() + for r, ch in live.items(): + prof.update(ch) + prof[8] += 8 # centre copies + return live, prof, issues, touched_removed, bad_warp_pos + + + +WORDS = { # provider -> {word set: (commit, path, sha256)} + 'base': {'pr2312': ('fb76f799ccf078f51780076ebed3fd26b1db11c0', + 'research/gmx-t74-borrow43-width-exchange/new/borrow/words/BORROW-WORD-43base.json.gz', + '4244149b59b287344b0e91aa50c6fa2a2491ee6c7a76d61cd352684a8182d005'), + 'pr2322': ('002304ef01c4416a127916169ae6d94c1bee052b', 'research/t74-joint-owner-hillclimb/words/base.json.gz', + '93c32c9dc8ca18394b7f3afac2cb4fa8582a6cb77399441b5107b396e63ca0f9')}, + 'extra': {'pr2312': ('fb76f799ccf078f51780076ebed3fd26b1db11c0', + 'research/gmx-t74-borrow43-width-exchange/new/borrow/words/BORROW-WORD-43extra.json.gz', + '01d510cc4ba912567f6b02ea50b6b0e741ed231a3608de9c36e7eeccbdaf6cda'), + 'pr2322': ('002304ef01c4416a127916169ae6d94c1bee052b', 'research/t74-joint-owner-hillclimb/words/extra.json.gz', + 'aae6592eaa4cf8638f21d50c44d09d4f8a6bb079ddcf5e377711a10ee2ddb526')}, +} +H1111 = [273, 275, 277, 282, 289, 291, 293, 298, 305, 307, 309, 314, 321, 323, 325, 330, 337, 339, 341, 346, 353, 355, + 357, 362, 369, 371, 373, 378, 385, 387, 389, 394, 653] +X5111 = [31, 33, 49, 55, 68, 74, 80, 83, 85, 88, 98, 101] + + +def load(repo, commit, path, sha): + data = subprocess.run(['git', '-C', repo, 'show', commit + ':' + path], capture_output=True, check=True).stdout + assert hashlib.sha256(data).hexdigest() == sha, path + return json.loads(gzip.decompress(data)) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--repo', default=os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))) + repo = ap.parse_args().repo + for prov, ws in WORDS.items(): + res = {} + for name, (commit, path, sha) in ws.items(): + word = load(repo, commit, path, sha) + live, prof, issues, touched, badpos = recount(word) + rep = {int(k): v for k, v in word["report"]["local_profile"].items()} + assert dict(prof) == rep, (prov, name, 'profile', dict(prof), rep) + assert not issues and not any(touched.values()) and not badpos, (prov, name, issues[:3], touched, badpos) + res[name] = (live, word) + (la, _wa), (lb, wb) = res['pr2312'], res['pr2322'] + assert sorted(set(la) - set(lb)) == [619, 621, 622, 623] and not set(lb) - set(la) + assert all(la[r] == (1, 1, 1, 1) for r in (619, 621, 622, 623)) + changed = {r: (la[r], lb[r]) for r in set(la) & set(lb) if la[r] != lb[r]} + want = {r: ((5, 1, 1, 1), (2, 1, 1, 1, 1, 1, 1)) for r in (1, 4, 6, 12)} + want.update({r: ((4, 1, 1, 1, 1), (3, 2, 1, 1, 1)) for r in (616, 617, 618, 620)}) + assert changed == want, (prov, changed) + lenders = {w[1] for w in wb["warps"]} + assert [r for r in sorted(lb) if r >= HELP0 and lb[r] == (1, 1, 1, 1)] == H1111 + assert [r for r in sorted(lb) if r < NX and lb[r] == (5, 1, 1, 1) and r not in lenders] == X5111 + print('%s: profiles match reports; PR2312 -> PR2322 change set, 33 (1,1,1,1) helpers and 12 free (5,1,1,1) ' + 'X registers confirmed' % prov) + print('PASS_T74_INDEPENDENT_RECOUNT') + + +if __name__ == "__main__": + main() diff --git a/research/t74-2322-move-prices/move_prices.py b/research/t74-2322-move-prices/move_prices.py new file mode 100644 index 0000000000..4457d421cd --- /dev/null +++ b/research/t74-2322-move-prices/move_prices.py @@ -0,0 +1,379 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact prices of local word moves on the T74 PR2322 words, and a certified owner-fill cap (standard library only). + +Every frame climb of d dimensions on a register pays one recursive child of rank d (frame-climb rule of the vendored +PR2387 fill_check80.py, patched only to also record WHICH register paid each child). So a change of the local words +is a set of per-register climb reshapes plus a change of the helper width inventory. Mass is conserved +(local mass = 1856 + sum of helper widths, idle = bin capacity - hosted width), so only the shape of the +children matters, and the helper widths act through the width-aware bin-pattern LP of PR2387 / PR2360. + +This script + 1. recounts per-register climbs of the pinned words of PR2312 (fb76f799), PR2322 (002304ef), PR2269 (b479fc55) and + PR2339 (bf1742ae) and checks each recount against the word's own reported profile and width inventory; + 2. decomposes the realized changes PR2312 -> PR2322 (four handoffs) and PR2269 -> PR2339 (32 low + 5 high aliases) + into per-register reshapes and checks that they add up exactly to the profile change; + 3. prices each move type at a = PR2374's claimed kappa by exact re-solve of the bin-pattern LP (float simplex) and + by LP-root differences, and calibrates against the realized PR2312 -> PR2322 gain; + 4. certifies (exact rational LP dual, 800-bit enclosures) that every legal whole-helper owner fill of the PR2322 + words has b < 0.001697195759, and that the certificate does not reject PR2374's claimed point; + 5. lists the untried sites with the PR2322 pre-handoff shape pattern and prices k more PR2322-type handoffs. +It is a pricing screen, not a construction: a priced handoff still needs a legal coherent handoff, native lowering, +an owner fill and the outer ledger. + +Credits: PR2322 Vlado Vojdanovski (handoffs, words); PR2312 / PR2269 Jeremy Kothe (width exchange, borrow43 words); +PR2374 / PR2349 jeremykothe2, PR2363 mason-hale (owner fills on PR2322's words); PR2226 Cinna Davis (anticipatory +borrowing); PR2339 / PR2387 this author; PR2360 Jeremy Diviney and PR1129 Ali Romman (pattern-dual relaxation); +PR1319 / PR1297 T74 lineage. Prepared with substantial AI assistance (Claude Code, Anthropic); Apache-2.0. + +Usage: python3 -I -B move_prices.py [--repo PATH] [--fetch] [--remote URL] [--out] +""" + +import argparse +import gzip +import hashlib +import importlib.util +import json +import os +import subprocess +import sys +import time +import types +from collections import Counter, defaultdict +from fractions import Fraction + +if not __debug__: + sys.stdout.write('FAIL_T74_MOVE_PRICES refusing to run under python -O\n') + sys.exit(2) + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO_DEFAULT = os.path.dirname(os.path.dirname(HERE)) +REMOTE_DEFAULT = 'https://github.com/CrocSwap/integer-mult-bounds' +VENDOR = { # byte copies of PR2387 head 20fb6953 (this author): (git blob, sha256) + 'vendor/pr2387/ceiling_lp.py': ('48362358660f74e0e235865df3e172494c191212', + '63e2d35b07342508680e20f4b60c4da888acf4c771cd9b10400c21490f1491be'), + 'vendor/pr2387/fill_check80.py': ('557e0732bfe4c030436a11f5433143c10fa07821', + '1c4d30591969c6502605f239f40505261e99d025aa3b576a804332a6bc479b06'), + 'vendor/pr2387/vendor/iter3/price_check.py': ('708753e7703077a8ce4311293f02e42afb801934', + '19fcfb9f4d766959c599223090142edb03998229459cff1266960ca6b7ed1e0f'), +} +COMMITS = {'pr2312': ('fb76f799ccf078f51780076ebed3fd26b1db11c0', 'refs/pull/2312/head'), + 'pr2322': ('002304ef01c4416a127916169ae6d94c1bee052b', 'refs/pull/2322/head'), + 'pr2269': ('b479fc5567bc09ab9185bffe89b62594f36d74e5', 'refs/pull/2269/head'), + 'pr2339': ('bf1742aee4d855efb8bbd44a8419eddb33a679e5', 'refs/pull/2339/head')} +WORDS = { # (word set, provider) -> (path, git blob, sha256); provider base = gauge44 (249 calls), extra (417 calls) + ('pr2312', 'base'): ('research/gmx-t74-borrow43-width-exchange/new/borrow/words/BORROW-WORD-43base.json.gz', + '40effbbfe9b3664fe051d6e8a03220f09bf76676', + '4244149b59b287344b0e91aa50c6fa2a2491ee6c7a76d61cd352684a8182d005'), + ('pr2312', 'extra'): ('research/gmx-t74-borrow43-width-exchange/new/borrow/words/BORROW-WORD-43extra.json.gz', + '2fe91bd80a6124bece6f80377ea20d1d02561af2', + '01d510cc4ba912567f6b02ea50b6b0e741ed231a3608de9c36e7eeccbdaf6cda'), + ('pr2322', 'base'): ('research/t74-joint-owner-hillclimb/words/base.json.gz', + 'f4dda9147af544ae4fe6d17582b8aa5e9916040b', + '93c32c9dc8ca18394b7f3afac2cb4fa8582a6cb77399441b5107b396e63ca0f9'), + ('pr2322', 'extra'): ('research/t74-joint-owner-hillclimb/words/extra.json.gz', + '471e4819c0c6b256e7b3999649f1391989d92e19', + 'aae6592eaa4cf8638f21d50c44d09d4f8a6bb079ddcf5e377711a10ee2ddb526'), + ('pr2269', 'base'): ('research/gmx-t74-borrow43/new/borrow/words/BORROW-WORD-43base.json.gz', + '448dd795adba29392a90b34aa3f1b1b796c7e0bd', + '9492a5537fb87d9ca98dffcd0230f7625b3789744fa94e2f18acf23d91d998b5'), + ('pr2269', 'extra'): ('research/gmx-t74-borrow43/new/borrow/words/BORROW-WORD-43extra.json.gz', + '2b51ba96256283bbc5578f99b694c50edd8a0e35', + '87d51f5298101d5947f45c43ee02f0ec45d6acbddabb808d0d02db1eaf063734'), + ('pr2339', 'base'): ('research/t74-low-alias-borrowing/words/BORROW-WORD-80base.json.gz', + 'c5953dfdb0ee9ac0c2c73eb29e320582b4569d2b', + '61290abffd8c8225e0abb3958c1506674e256de688fc4cdf358bbe7c981df493'), + ('pr2339', 'extra'): ('research/t74-low-alias-borrowing/words/BORROW-WORD-80extra.json.gz', + '852868543ed36efa799b3ed6dd76a0442b0d6ff1', + '1dd2d6f2ae5b5a27b5f89fb830203f0cca7a78d0323a7845e85e1e80f8f6d1a5'), +} +KAPPA_2312 = Fraction('0.001696891067241618') # PR2312 title / claim +KAPPA_2322 = Fraction('0.001697060296258836') # PR2322 CLAIM.json +KAPPA_2374 = Fraction('0.001697194950901770426594081877309541199782925447437522970580') # PR2374 body (58 digits) +CAP_2322 = '0.001697195759' +CALLS = {'base': 249, 'extra': 417} + + +class Fail(Exception): + pass + + +def need(cond, what): + if not cond: + raise Fail(what) + + +def blob_id(data): + return hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() + + +def load_vendor(): + for rel, (blob, sha) in VENDOR.items(): + data = open(os.path.join(HERE, rel), 'rb').read() + need(blob_id(data) == blob and hashlib.sha256(data).hexdigest() == sha, 'vendored pin ' + rel) + spec = importlib.util.spec_from_file_location('pr2387_ceiling_lp', os.path.join(HERE, 'vendor/pr2387/ceiling_lp.py')) + lp = importlib.util.module_from_spec(spec) + spec.loader.exec_module(lp) + path = os.path.join(HERE, 'vendor/pr2387/fill_check80.py') + src = open(path).read() + old = ' if d:\n paid[d] += 1\n per_reg[r] += d\n' + need(src.count(old) == 1, 'patch anchor in fill_check80.local_recount') + src = src.replace(old, old + ' CHILDREN[r].append(d)\n') # the only change: record the payer + fc = types.ModuleType('pr2387_fill_check80') + fc.__file__ = path + exec(compile(src, path, 'exec'), fc.__dict__) + return lp, fc + + +def git(repo, *args): + return subprocess.run(['git', '-C', repo] + list(args), capture_output=True, check=True).stdout + + +def ensure_commits(repo, fetch, remote): + for name, (commit, ref) in COMMITS.items(): + ok = subprocess.run(['git', '-C', repo, 'cat-file', '-e', commit + '^{commit}'], capture_output=True).returncode == 0 + if not ok and fetch: + subprocess.run(['git', '-C', repo, 'fetch', '-q', remote, ref], check=True) + ok = subprocess.run(['git', '-C', repo, 'cat-file', '-e', commit + '^{commit}'], + capture_output=True).returncode == 0 + need(ok, '%s commit %s absent (rerun with --fetch)' % (name, commit[:8])) + + +def recount(repo, fc, key): + path, blob, sha = WORDS[key] + data = git(repo, 'show', COMMITS[key[0]][0] + ':' + path) + need(blob_id(data) == blob and hashlib.sha256(data).hexdigest() == sha, 'word pin %s/%s' % key) + w = json.loads(gzip.decompress(data)) + fc.CHILDREN = defaultdict(list) + rec = fc.local_recount(w, '%s/%s' % key) + rep = w['report'] + need(dict(rec['paid']) == {int(k): v for k, v in rep['local_profile'].items()}, 'recounted profile %s/%s' % key) + need(dict(Counter(rec['widths'])) == {int(k): v for k, v in rep['width_inventory'].items()}, + 'recounted widths %s/%s' % key) + removed = set(w['removed']) + ch = {r: tuple(sorted(fc.CHILDREN.get(r, []), reverse=True)) for r in range(fc.REGISTERS) if r not in removed} + need(Counter(d for c in ch.values() for d in c) + Counter(rec['copies']) == rec['paid'] or + Counter(d for c in ch.values() for d in c) == rec['paid'] - Counter(rec['copies']), 'per-register sum %s/%s' % key) + return dict(word=w, children=ch, paid=Counter(rec['paid']), widths=dict(zip(rec['live_helpers'], rec['widths'])), + lenders={x[1] for x in w['warps']}, removed=removed) + + +def decompose(a, b): + """Per-register reshapes from word a to word b; checks they add up to the profile change exactly.""" + gone = sorted(r for r in a['children'] if r not in b['children']) + changed = sorted(r for r in b['children'] if r in a['children'] and a['children'][r] != b['children'][r]) + pred = Counter(a['paid']) + for r in gone: + pred.subtract(a['children'][r]) + for r in changed: + pred.subtract(a['children'][r]) + pred.update(b['children'][r]) + need(+pred == b['paid'], 'decomposition does not add up') + return gone, changed + + +def delta(minus=(), plus=()): + c = Counter() + for s in minus: + c.subtract(s) + for s in plus: + c.update(s) + return {k: v for k, v in c.items() if v} + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--repo', default=REPO_DEFAULT) + ap.add_argument('--fetch', action='store_true') + ap.add_argument('--remote', default=REMOTE_DEFAULT) + ap.add_argument('--out', action='store_true') + args = ap.parse_args() + t0 = time.time() + lp, fc = load_vendor() + ensure_commits(args.repo, args.fetch, args.remote) + R = {k: recount(args.repo, fc, k) for k in WORDS} + out = dict(object='PR2322 T74 words: per-register climb decomposition, move prices, owner-fill cap', a_price=str(KAPPA_2374)) + + # ---- 2. realized decompositions ------------------------------------------------------------------------------- + HANDOFF = dict(helper=(1, 1, 1, 1), lender=((5, 1, 1, 1), (2, 1, 1, 1, 1, 1, 1)), + partner=((4, 1, 1, 1, 1), (3, 2, 1, 1, 1))) + for prov in ('base', 'extra'): + a, b = R[('pr2312', prov)], R[('pr2322', prov)] + gone, changed = decompose(a, b) + need(gone == [619, 621, 622, 623] and all(a['children'][r] == HANDOFF['helper'] for r in gone), 'PR2322 removed') + xs = [r for r in changed if r < 112] + need(xs == [1, 4, 6, 12] and all((a['children'][r], b['children'][r]) == HANDOFF['lender'] for r in xs), + 'PR2322 lenders') + parts = [r for r in changed if r >= 224] + need(parts == [616, 617, 618, 620] and all((a['children'][r], b['children'][r]) == HANDOFF['partner'] + for r in parts), 'PR2322 partners') + need(len(changed) == 8 and set(xs) <= b['lenders'] and not set(xs) & a['lenders'], 'PR2322 change set') + out['pr2312_to_pr2322'] = dict(removed=[619, 621, 622, 623], lenders=[1, 4, 6, 12], partners=[616, 617, 618, 620], + shapes={k: [list(x) for x in v] if k != 'helper' else list(v) + for k, v in HANDOFF.items()}, both_providers=True) + low = Counter() + for prov in ('base', 'extra'): + a, b = R[('pr2269', prov)], R[('pr2339', prov)] + gone, changed = decompose(a, b) + newl = sorted(b['lenders'] - a['lenders']) + need(len(gone) == 37 and len(newl) == 37, 'PR2339 alias count') + kinds = Counter() + for r in newl: + kinds[(a['children'][r], b['children'][r])] += 1 + tgt = Counter((a['children'][r], b['children'][r]) for r in changed if 112 <= r < 224) + need(set(changed) - set(newl) == {r for r in changed if 112 <= r < 224}, 'PR2339 change set') + low[prov] = dict(removed=Counter(a['children'][r] for r in gone), lenders=kinds, targets=tgt) + out['pr2269_to_pr2339'] = {p: {k: [[list(x) if isinstance(x, tuple) else [list(y) for y in x], n] + for x, n in sorted(v.items())] for k, v in d.items()} for p, d in low.items()} + + # ---- 3. move prices at a = PR2374 kappa ---------------------------------------------------------------------- + a0 = float(KAPPA_2374) + h = lambda r: lp.h_float(r, a0) + base = lp.CASES['pr2322_control'] + for prov, key in (('base', 'pg'), ('extra', 'pe')): + need(dict(R[('pr2322', prov)]['paid']) == base[key], 'PR2387 pr2322_control case == recounted profile') + need(dict(Counter(R[('pr2322', 'extra')]['widths'].values())) == base['inv'], 'PR2387 pr2322 inventory') + lp.CASES['pr2312'] = dict(inv=dict(Counter(R[('pr2312', 'extra')]['widths'].values())), + pg=dict(R[('pr2312', 'base')]['paid']), pe=dict(R[('pr2312', 'extra')]['paid'])) + moves = { + 'pr2322_handoff': dict(inv={4: -1}, local=delta([HANDOFF['helper'], HANDOFF['lender'][0], HANDOFF['partner'][0]], + [HANDOFF['lender'][1], HANDOFF['partner'][1]])), + 'pr2339_low_alias': dict(inv={4: -1, 8: -1, 9: 1}, local=delta([(3, 2, 1, 1, 1), (1, 1, 1, 1)], + [(2, 1, 1, 1, 1, 1, 1, 1)])), + 'pr2339_high_alias': dict(inv={5: -1}, local=delta([(2, 1, 1, 1), (5, 1, 1, 1)], [(2, 1, 1, 1, 1, 1, 1)])), + 'target_merge_1_1_to_2': dict(inv={}, local={1: -2, 2: 1}), + } + v0, _s, _d = lp.simplex([h(Rr - sum(p)) for Rr, p in lp.COLS], lp.rhs_of('pr2322_control')) + root0 = lp.lp_root_float('pr2322_control')[0] + + def applied(k, mv): + inv = dict(base['inv']) + for w_, d_ in mv['inv'].items(): + inv[w_] += k * d_ + pg, pe = Counter(base['pg']), Counter(base['pe']) + for r_, d_ in mv['local'].items(): + pg[r_] += k * d_ + pe[r_] += k * d_ + need(min(inv.values()) >= 0 and min(pg.values()) >= 0 and min(pe.values()) >= 0, 'move not applicable') + return dict(inv=inv, pg=dict(+pg), pe=dict(+pe)) + + def lp_root_wide(case): + lo, hi = 0.0015, 0.0020 + for _ in range(50): + mid = (lo + hi) / 2 + if lp.lp_mu_float(case, mid)[0] < 1: + lo = mid + else: + hi = mid + return lo + + out['move_prices'] = {} + for name, mv in moves.items(): + lp.CASES['t'] = applied(1, mv) + v1, _s, _d = lp.simplex([h(Rr - sum(p)) for Rr, p in lp.COLS], lp.rhs_of('t')) + dlp = (v1 - v0) / 666 + dloc = sum(n * h(r) for r, n in mv['local'].items()) + db = lp_root_wide('t') - root0 + out['move_prices'][name] = dict(inventory_change=mv['inv'], local_change=mv['local'], + mass_change=sum(r * n for r, n in mv['local'].items()), + dLP_per_call=dlp, dlocal_per_call=dloc, net_per_call=dlp + dloc, db_one_move=db) + print('%-24s inv %-22s local %-36s net/call %+.3e db(one move, both providers) %+.3e' + % (name, json.dumps(mv['inv']), json.dumps(mv['local']), dlp + dloc, db)) + mp = out['move_prices'] + need(mp['pr2322_handoff']['db_one_move'] > 0 and mp['pr2339_low_alias']['db_one_move'] < 0, 'move signs') + need(abs(mp['pr2339_high_alias']['net_per_call']) < 1e-12, 'high alias is exactly price-neutral') + for name in moves: + need(mp[name]['mass_change'] == sum(w_ * d_ for w_, d_ in moves[name]['inv'].items()), + 'mass identity: local mass change = helper width change (%s)' % name) + + # calibration against realized claims + r12 = lp.lp_root_float('pr2312')[0] + out['calibration'] = dict(lp_root_pr2312=r12, lp_root_pr2322=root0, lp_predicted_gain=root0 - r12, + realized_gain=float(KAPPA_2322 - KAPPA_2312), + realized_fraction_pr2312=float(KAPPA_2312) / r12, + realized_fraction_pr2322=float(KAPPA_2322) / root0, + realized_fraction_pr2374=float(KAPPA_2374) / root0) + print('calibration: LP ceiling gain PR2312 -> PR2322 = %.4e, realized claim gain = %.4e' % + (root0 - r12, float(KAPPA_2322 - KAPPA_2312))) + + # ---- 4. certified owner-fill cap for the PR2322 words ----------------------------------------------------------- + ok, cert = lp.certify('pr2322_control', CAP_2322) + need(ok, 'cap certificate for the PR2322 words') + ok2, cert2 = lp.certify('pr2322_control', KAPPA_2374) + need(not ok2, 'control: the certificate must not reject PR2374 (a legal fill is claimed there)') + ok3, cert3 = lp.certify('pr2322_control', Fraction(KAPPA_2374) + Fraction(1, 10**12)) + out['owner_fill_cap'] = dict(case='PR2322 words (inventory and both profiles recounted here)', cap=CAP_2322, + certificate=cert, control_pr2374_not_rejected=cert2, + headroom_above_pr2374=float(Fraction(CAP_2322) - KAPPA_2374), + lp_root_float=root0) + print('certified: every legal whole-helper owner fill of the PR2322 words has b < %s (margin %.3g); ' + 'PR2374 is not rejected; headroom <= %.3e' % (CAP_2322, cert['margin'], float(Fraction(CAP_2322) - KAPPA_2374))) + + # ---- 5. untried PR2322-pattern sites ------------------------------------------------------------------------------ + sites = {} + for prov in ('base', 'extra'): + w = R[('pr2322', prov)] + ch = w['children'] + w4 = [r for r in w['widths'] if ch[r] == HANDOFF['helper']] + xfree = [r for r in range(112) if ch[r] == HANDOFF['lender'][0] and r not in w['lenders']] + blocks = defaultdict(list) + for r in w4: + blocks[(r - 224) // 8].append(r) + rows = [] + for blk, regs in sorted(blocks.items()): + mates = [(r, list(ch[r])) for r in range(224 + 8 * blk, 232 + 8 * blk) if r in ch] + partners = [r for r, s in mates if s and s[0] == 4 and all(x == 1 for x in s[1:])] + rows.append(dict(block=blk, width4_helpers=regs, partners_4_then_1s=partners, + removed_in_block=[r for r in range(224 + 8 * blk, 232 + 8 * blk) if r in w['removed']], + mates=mates)) + sites[prov] = dict(width4_1111_helpers=w4, free_x_5111_registers=xfree, blocks=rows) + need(sites['base']['width4_1111_helpers'] == sites['extra']['width4_1111_helpers'] and + sites['base']['free_x_5111_registers'] == sites['extra']['free_x_5111_registers'], 'sites differ by provider') + s = sites['extra'] + exact = [r for r in s['blocks'] if r['partners_4_then_1s'] and + all(len(m[1]) == 5 for m in r['mates'] if m[0] in r['partners_4_then_1s'])] + kmax = min(len(s['width4_1111_helpers']), len(s['free_x_5111_registers'])) + ladder = [] + for k in (1, 2, 4, 8, kmax): + lp.CASES['t'] = applied(k, moves['pr2322_handoff']) + ladder.append([k, lp_root_wide('t') - root0]) + out['untried_sites'] = dict(width4_1111_helpers=s['width4_1111_helpers'], + free_x_5111_registers=s['free_x_5111_registers'], + blocks=s['blocks'], blocks_matching_pr2322_partner_shape=[r['block'] for r in exact], + lender_limited_kmax=kmax, db_for_k_more_pr2322_handoffs=ladder) + print('untried: %d width-4 (1,1,1,1) helpers, %d unused (5,1,1,1) X registers; block(s) %s carry the exact PR2322 ' + 'partner shape (4,1,1,1,1)' % (len(s['width4_1111_helpers']), len(s['free_x_5111_registers']), + [r['block'] for r in exact])) + for k, db in ladder: + print(' %2d more PR2322-type handoffs (same reshapes): LP ceiling db = %+.3e' % (k, db)) + # the target-climb merges that accompany the PR2339 low aliases, priced on their own (no inventory change) + for prov in ('base', 'extra'): + need(all(delta([x], [y]) == {1: -2, 2: 1} for x, y in low[prov]['targets']), + 'PR2339 target changes are all one (1,1) -> (2) merge (%s)' % prov) + nmerge = sum(low['extra']['targets'].values()) + need(nmerge == sum(low['base']['targets'].values()), 'PR2339 target merges per provider') + lp.CASES['t'] = applied(nmerge, moves['target_merge_1_1_to_2']) + out['pr2339_target_merges_alone'] = dict(count_per_word=nmerge, db_on_pr2322_words=lp_root_wide('t') - root0) + print('the %d target merges (one (1,1)->(2) each) that accompany the PR2339 low aliases, alone on the PR2322 ' + 'words: LP ceiling db = %+.3e' % (nmerge, out['pr2339_target_merges_alone']['db_on_pr2322_words'])) + out['scope'] = ('Pricing screen on fixed pinned words: moves are priced by their per-register climb reshapes and ' + 'width change only, through the PR2387 bin-pattern LP (windows, families, ports dropped). A priced ' + 'move is not a construction; the cap is a relaxation ceiling, not a kappa.') + out['python'] = sys.version.split()[0] + out['seconds'] = round(time.time() - t0, 1) + if args.out: + with open(os.path.join(HERE, 'move_prices.receipt.json'), 'w') as f: + f.write(json.dumps(out, indent=1, sort_keys=True, default=str) + '\n') + print('runtime %.1fs' % (time.time() - t0)) + print('PASS_T74_MOVE_PRICES cap=%s handoff_db=%+.3e low_alias_db=%+.3e high_alias_net=0 sites=%d/%d' + % (CAP_2322, mp['pr2322_handoff']['db_one_move'], mp['pr2339_low_alias']['db_one_move'], + len(s['width4_1111_helpers']), len(s['free_x_5111_registers']))) + return 0 + + +if __name__ == '__main__': + try: + sys.exit(main()) + except Fail as e: + sys.stdout.write('FAIL_T74_MOVE_PRICES %s\n' % e) + sys.exit(1) diff --git a/research/t74-2322-move-prices/move_prices.receipt.json b/research/t74-2322-move-prices/move_prices.receipt.json new file mode 100644 index 0000000000..90955fdf18 --- /dev/null +++ b/research/t74-2322-move-prices/move_prices.receipt.json @@ -0,0 +1,2208 @@ +{ + "a_price": "84859747545088521329704093865477059989146272371876148529/50000000000000000000000000000000000000000000000000000000000", + "calibration": { + "lp_predicted_gain": 1.9625624370013701e-07, + "lp_root_pr2312": 0.0016969995017889746, + "lp_root_pr2322": 0.0016971957580326747, + "realized_fraction_pr2312": 0.9999361021925803, + "realized_fraction_pr2322": 0.9999201849443722, + "realized_fraction_pr2374": 0.9999995244326411, + "realized_gain": 1.69229017218e-07 + }, + "move_prices": { + "pr2322_handoff": { + "dLP_per_call": 0.055006775319084954, + "db_one_move": 4.271643083871013e-08, + "dlocal_per_call": -0.05501907191079801, + "inventory_change": { + "4": -1 + }, + "local_change": { + "1": -2, + "2": 2, + "3": 1, + "4": -1, + "5": -1 + }, + "mass_change": -4, + "net_per_call": -1.2296591713055471e-05 + }, + "pr2339_high_alias": { + "dLP_per_call": 0.0688055194626744, + "db_one_move": 1.734723475976807e-18, + "dlocal_per_call": -0.06880551946267438, + "inventory_change": { + "5": -1 + }, + "local_change": { + "5": -1 + }, + "mass_change": -5, + "net_per_call": 1.3877787807814457e-17 + }, + "pr2339_low_alias": { + "dLP_per_call": 0.04137399660015529, + "db_one_move": -1.9061134770353635e-07, + "dlocal_per_call": -0.041319118617507256, + "inventory_change": { + "4": -1, + "8": -1, + "9": 1 + }, + "local_change": { + "3": -1 + }, + "mass_change": -3, + "net_per_call": 5.4877982648034174e-05 + }, + "target_merge_1_1_to_2": { + "dLP_per_call": 0.0, + "db_one_move": 1.1271960476295917e-07, + "dlocal_per_call": -3.244675888916526e-05, + "inventory_change": {}, + "local_change": { + "1": -2, + "2": 1 + }, + "mass_change": 0, + "net_per_call": -3.244675888916526e-05 + } + }, + "object": "PR2322 T74 words: per-register climb decomposition, move prices, owner-fill cap", + "owner_fill_cap": { + "cap": "0.001697195759", + "case": "PR2322 words (inventory and both profiles recounted here)", + "certificate": { + "W": 66304, + "a0": "1697195759/1000000000000", + "certified_b_below_a0": true, + "dual_repair": { + "16": 0.0, + "32": 0.0, + "48": 0.0, + "8": 0.0 + }, + "lower_bound_of_W_mu": 66304.00000018545, + "margin": 1.8544766141121287e-07 + }, + "control_pr2374_not_rejected": { + "W": 66304, + "a0": "84859747545088521329704093865477059989146272371876148529/50000000000000000000000000000000000000000000000000000000000", + "certified_b_below_a0": false, + "dual_repair": { + "16": 0.0, + "32": 0.0, + "48": 0.0, + "8": 0.0 + }, + "lower_bound_of_W_mu": 66303.99984525406, + "margin": -0.00015474593906241753 + }, + "headroom_above_pr2374": 8.080982295734059e-10, + "lp_root_float": 0.0016971957580326747 + }, + "pr2269_to_pr2339": { + "base": { + "lenders": [ + [ + [ + [ + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + 4 + ], + [ + [ + [ + 1, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + 28 + ], + [ + [ + [ + 5, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + 5 + ] + ], + "removed": [ + [ + [ + 2, + 1, + 1, + 1 + ], + 5 + ], + [ + [ + 3, + 2, + 1, + 1, + 1 + ], + 28 + ], + [ + [ + 4, + 1, + 1, + 1, + 1 + ], + 4 + ] + ], + "targets": [ + [ + [ + [ + 3, + 2, + 1, + 1, + 1 + ], + [ + 3, + 2, + 2, + 1 + ] + ], + 1 + ], + [ + [ + [ + 4, + 1, + 1, + 1, + 1 + ], + [ + 4, + 2, + 1, + 1 + ] + ], + 24 + ], + [ + [ + [ + 5, + 1, + 1, + 1 + ], + [ + 5, + 2, + 1 + ] + ], + 1 + ] + ] + }, + "extra": { + "lenders": [ + [ + [ + [ + 1, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + 32 + ], + [ + [ + [ + 5, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + 5 + ] + ], + "removed": [ + [ + [ + 2, + 1, + 1, + 1 + ], + 5 + ], + [ + [ + 3, + 2, + 1, + 1, + 1 + ], + 32 + ] + ], + "targets": [ + [ + [ + [ + 3, + 2, + 1, + 1, + 1 + ], + [ + 3, + 2, + 2, + 1 + ] + ], + 1 + ], + [ + [ + [ + 4, + 1, + 1, + 1, + 1 + ], + [ + 4, + 2, + 1, + 1 + ] + ], + 24 + ], + [ + [ + [ + 5, + 1, + 1, + 1 + ], + [ + 5, + 2, + 1 + ] + ], + 1 + ] + ] + } + }, + "pr2312_to_pr2322": { + "both_providers": true, + "lenders": [ + 1, + 4, + 6, + 12 + ], + "partners": [ + 616, + 617, + 618, + 620 + ], + "removed": [ + 619, + 621, + 622, + 623 + ], + "shapes": { + "helper": [ + 1, + 1, + 1, + 1 + ], + "lender": [ + [ + 5, + 1, + 1, + 1 + ], + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + "partner": [ + [ + 4, + 1, + 1, + 1, + 1 + ], + [ + 3, + 2, + 1, + 1, + 1 + ] + ] + } + }, + "pr2339_target_merges_alone": { + "count_per_word": 26, + "db_on_pr2322_words": 2.9356014541476877e-06 + }, + "python": "3.14.4", + "scope": "Pricing screen on fixed pinned words: moves are priced by their per-register climb reshapes and width change only, through the PR2387 bin-pattern LP (windows, families, ports dropped). A priced move is not a construction; the cap is a relaxation ceiling, not a kappa.", + "seconds": 16.1, + "untried_sites": { + "blocks": [ + { + "block": 6, + "mates": [ + [ + 272, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 273, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 274, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 275, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 276, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 277, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 278, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 279, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 272 + ], + "removed_in_block": [], + "width4_helpers": [ + 273, + 275, + 277 + ] + }, + { + "block": 7, + "mates": [ + [ + 280, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 281, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 282, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 283, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 284, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 285, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 286, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 287, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 282 + ] + }, + { + "block": 8, + "mates": [ + [ + 288, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 289, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 290, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 291, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 292, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 293, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 294, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 295, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 288 + ], + "removed_in_block": [], + "width4_helpers": [ + 289, + 291, + 293 + ] + }, + { + "block": 9, + "mates": [ + [ + 296, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 297, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 298, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 299, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 300, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 301, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 302, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 303, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 298 + ] + }, + { + "block": 10, + "mates": [ + [ + 304, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 305, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 306, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ], + [ + 307, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 308, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ], + [ + 309, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 310, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ], + [ + 311, + [ + 3, + 2, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 304 + ], + "removed_in_block": [], + "width4_helpers": [ + 305, + 307, + 309 + ] + }, + { + "block": 11, + "mates": [ + [ + 312, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 313, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 314, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 315, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 316, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 317, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 318, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 319, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 314 + ] + }, + { + "block": 12, + "mates": [ + [ + 320, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 321, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 322, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ], + [ + 323, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 324, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ], + [ + 325, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 326, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ], + [ + 327, + [ + 3, + 2, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 320 + ], + "removed_in_block": [], + "width4_helpers": [ + 321, + 323, + 325 + ] + }, + { + "block": 13, + "mates": [ + [ + 328, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 329, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 330, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 331, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 332, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 333, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 334, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 335, + [ + 3, + 2, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 330 + ] + }, + { + "block": 14, + "mates": [ + [ + 336, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 337, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 338, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 339, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 340, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 341, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 342, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 343, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 336 + ], + "removed_in_block": [], + "width4_helpers": [ + 337, + 339, + 341 + ] + }, + { + "block": 15, + "mates": [ + [ + 344, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 345, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 346, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 347, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 348, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 349, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 350, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 351, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 346 + ] + }, + { + "block": 16, + "mates": [ + [ + 352, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 353, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 354, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 355, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 356, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 357, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 358, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 359, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 352 + ], + "removed_in_block": [], + "width4_helpers": [ + 353, + 355, + 357 + ] + }, + { + "block": 17, + "mates": [ + [ + 360, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 361, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 362, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 363, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 364, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 365, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 366, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 367, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 362 + ] + }, + { + "block": 18, + "mates": [ + [ + 368, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 369, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 370, + [ + 3, + 3, + 1, + 1, + 1 + ] + ], + [ + 371, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 372, + [ + 3, + 3, + 1, + 1, + 1 + ] + ], + [ + 373, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 374, + [ + 3, + 3, + 1, + 1, + 1 + ] + ], + [ + 375, + [ + 3, + 3, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 368 + ], + "removed_in_block": [], + "width4_helpers": [ + 369, + 371, + 373 + ] + }, + { + "block": 19, + "mates": [ + [ + 376, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 377, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 378, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 379, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 380, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 381, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 382, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 383, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 378 + ] + }, + { + "block": 20, + "mates": [ + [ + 384, + [ + 4, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 385, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 386, + [ + 3, + 3, + 1, + 1, + 1 + ] + ], + [ + 387, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 388, + [ + 3, + 3, + 1, + 1, + 1 + ] + ], + [ + 389, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 390, + [ + 3, + 3, + 1, + 1, + 1 + ] + ], + [ + 391, + [ + 3, + 3, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 384 + ], + "removed_in_block": [], + "width4_helpers": [ + 385, + 387, + 389 + ] + }, + { + "block": 21, + "mates": [ + [ + 392, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 393, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 394, + [ + 1, + 1, + 1, + 1 + ] + ], + [ + 395, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 396, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 397, + [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 398, + [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ] + ], + [ + 399, + [ + 3, + 1, + 1, + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [], + "removed_in_block": [], + "width4_helpers": [ + 394 + ] + }, + { + "block": 53, + "mates": [ + [ + 648, + [ + 4, + 1, + 1, + 1, + 1 + ] + ], + [ + 649, + [ + 4, + 1, + 1, + 1, + 1 + ] + ], + [ + 650, + [ + 4, + 1, + 1, + 1, + 1 + ] + ], + [ + 652, + [ + 4, + 1, + 1, + 1, + 1 + ] + ], + [ + 653, + [ + 1, + 1, + 1, + 1 + ] + ] + ], + "partners_4_then_1s": [ + 648, + 649, + 650, + 652 + ], + "removed_in_block": [ + 651, + 654, + 655 + ], + "width4_helpers": [ + 653 + ] + } + ], + "blocks_matching_pr2322_partner_shape": [ + 53 + ], + "db_for_k_more_pr2322_handoffs": [ + [ + 1, + 4.271643083871013e-08 + ], + [ + 2, + 8.543502827635177e-08 + ], + [ + 4, + 1.708787240612547e-07 + ], + [ + 8, + 3.417921234944582e-07 + ], + [ + 12, + 5.127402089594862e-07 + ] + ], + "free_x_5111_registers": [ + 31, + 33, + 49, + 55, + 68, + 74, + 80, + 83, + 85, + 88, + 98, + 101 + ], + "lender_limited_kmax": 12, + "width4_1111_helpers": [ + 273, + 275, + 277, + 282, + 289, + 291, + 293, + 298, + 305, + 307, + 309, + 314, + 321, + 323, + 325, + 330, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394, + 653 + ] + } +} diff --git a/research/t74-2322-move-prices/vendor/pr2387/ceiling_lp.py b/research/t74-2322-move-prices/vendor/pr2387/ceiling_lp.py new file mode 100644 index 0000000000..4836235866 --- /dev/null +++ b/research/t74-2322-move-prices/vendor/pr2387/ceiling_lp.py @@ -0,0 +1,345 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Width-aware packing ceiling for whole-helper owner fills on the T74 template (certified LP dual). + +Statement (for a fixed local word pair and the PR #2269 T74 template). Let n_w be the number of live helpers +of width w per call, N_R the number of idle bins of rank R (T*112*#children of rank R: N_8 = 49728, +N_16 = N_32 = N_48 = 33152), and P_g, P_e the local paid profiles. ANY legal whole-helper owner fill puts +each of the 666*400 roles whole into one bin; so for each bin the multiset of hosted widths is a pattern p +with sum(p) <= R, and the bin's idle remainder R - sum(p) is a child of the global profile (if nonzero). +For fixed a the moment mu(a) = sum_r n_r (r/73)^(1-a) / 66304 is linear in the counts, hence + + 66304 * mu(a) >= sum_r (249 P_g + 417 P_e)_r h_a(r) + LP(a), + LP(a) = min sum_p x_p h_a(R_p - sum p) s.t. sum_{p of rank R} x_p = N_R, sum_p x_p cnt_w(p) = 666 n_w, + x >= 0, h_a(r) = (r/73)^(1-a), h_a(0) = 0, + +the LP relaxation of the pattern counts of the fill (time windows, families and ports are dropped). By weak +duality LP(a) >= sum_R N_R y_R + sum_w 666 n_w z_w for every (y, z) with y_R + sum_w cnt_w(p) z_w <= h_a(rem p) +for all patterns p. A float simplex supplies (y, z); they are converted to exact rationals and repaired to +exact feasibility against certified LOWER bounds of h_a (800-bit directed rounding, vendored iteration-3 +price_check.py). If the resulting exact lower bound of 66304*mu(a0) exceeds 66304, then mu(a0) > 1 for every +legal fill, so every fill has b < a0 (mu is increasing in a). This is a ceiling, not a construction. + +Cases: ext80 = PR2339 80-alias words (widths re-derived by check_fill.py); high43 = PR2269 words (positive +control: PR2269's realized b must lie below its ceiling); high48 / low75 = the PR2339 README variants +"+5 high only" / "+32 low only" (profiles as reported in PR2339's README table; width inventories follow from +the alias definitions: a high alias removes a width-5 helper, a low alias removes a width-8 helper and turns a +width-4 lender into width 9). Negative control: the ext80 certificate must FAIL at a0 below the b of our own +legal fill (OWNERS-80), otherwise the machinery would be unsound. + +Prior and concurrent work. The pattern-LP relaxation is not new: PR1129 (Ali Romman) and the R480 pattern-dual audit +use it on an older inventory, and PR2360 (Jeremy Diviney, head 16d4ea6c, opened while this package was in progress) +certifies b < 0.0016870 for the same PR2339 words with the same 1163 patterns (all-extra envelope). This file was +written independently; it gives the tighter b < 0.0016867 (actual 249/417 dispatch), the variant and control cases, +and re-checks PR2360's DUAL.json (inputs/PR2360-DUAL.json, byte copy, blob/sha256 pinned) against its own pattern +enumeration and enclosures, with a tampered-dual negative control. + +Prepared with substantial AI assistance (Claude Code, Anthropic); Apache-2.0. Credits as in build_fill.py. +Usage: python3 -I -B ceiling_lp.py [--out] +""" + +import argparse +import hashlib +import importlib.util +import json +import os +import sys +import time +from fractions import Fraction + +if not __debug__: + sys.exit('refusing to run under python -O') + +HERE = os.path.dirname(os.path.abspath(__file__)) +M, W_LIVE, CALLS = 73, 66304, 666 +NB = {8: 49728, 16: 33152, 32: 33152, 48: 33152} +WID = (4, 5, 7, 8, 9) +CASES = { + 'ext80': dict(inv={4: 4, 5: 4, 7: 36, 8: 84, 9: 272}, + pg={1: 2303, 2: 527, 3: 386, 4: 125, 5: 37, 8: 8}, pe={1: 2287, 2: 535, 3: 386, 4: 125, 5: 37, 8: 8}), + 'high43': dict(inv={4: 36, 5: 9, 7: 36, 8: 116, 9: 240}, + pg={1: 2351, 2: 501, 3: 414, 4: 129, 5: 42, 8: 8}, pe={1: 2339, 2: 509, 3: 418, 4: 125, 5: 42, 8: 8}), + 'high48_5high_only': dict(inv={4: 36, 5: 4, 7: 36, 8: 116, 9: 240}, + pg={1: 2351, 2: 501, 3: 414, 4: 129, 5: 37, 8: 8}, + pe={1: 2339, 2: 509, 3: 418, 4: 125, 5: 37, 8: 8}), + # positive control from PR2322's README (head 002304ef): widths {4:33,5:9,7:38,8:114,9:240}, 434 helpers, + # profile {1:2335,2:512,3:426,4:120,5:38,8:8} in both providers (its own fill is on the same template ranks). + 'pr2322_control': dict(inv={4: 33, 5: 9, 7: 38, 8: 114, 9: 240}, + pg={1: 2335, 2: 512, 3: 426, 4: 120, 5: 38, 8: 8}, + pe={1: 2335, 2: 512, 3: 426, 4: 120, 5: 38, 8: 8}), + 'low75_32low_only': dict(inv={4: 4, 5: 9, 7: 36, 8: 84, 9: 272}, + pg={1: 2303, 2: 527, 3: 386, 4: 125, 5: 42, 8: 8}, + pe={1: 2287, 2: 535, 3: 386, 4: 125, 5: 42, 8: 8}), +} +CLAIM_2269 = Fraction('0.0016962471390584742207696225394800943861') +CLAIM_2322 = Fraction('0.001697060296258836') +VENDOR_PRICE = ('708753e7703077a8ce4311293f02e42afb801934', + '19fcfb9f4d766959c599223090142edb03998229459cff1266960ca6b7ed1e0f') + + +def load_price(): + path = os.path.join(HERE, 'vendor', 'iter3', 'price_check.py') + data = open(path, 'rb').read() + assert hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() == VENDOR_PRICE[0] + assert hashlib.sha256(data).hexdigest() == VENDOR_PRICE[1] + spec = importlib.util.spec_from_file_location('iter3_price_check', path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +P = load_price() + + +def patterns(): + out = [] + for R in NB: + def rec(i, rem, cur): + if i == len(WID): + out.append((R, tuple(cur))) + return + for k in range(rem // WID[i] + 1): + rec(i + 1, rem - k * WID[i], cur + [WID[i]] * k) + rec(0, R, []) + return out + + +COLS = patterns() + + +def h_float(r, a): + return 0.0 if r == 0 else (r / M) ** (1.0 - a) + + +def h_lower(r, a): + """Certified lower bound of (r/73)^(1-a) = (r/73) exp(a log(73/r)) (exact rational).""" + if r == 0: + return Fraction(0) + a = Fraction(a) + ll, lu = P.log_enclosure(M, r) + el, eu = P.exp_enclosure((a.numerator * ll) // a.denominator, P.cdiv(a.numerator * lu, a.denominator)) + return Fraction(r * el, M * P.ONE) + + +def simplex(cost, rhs): + """Dense two-phase simplex (floats). Returns objective, primal {col: x} and duals (one per row).""" + m, n = len(rhs), len(COLS) + A = [[1.0 if R == RR else 0.0 for RR in NB] + [float(p.count(w)) for w in WID] for R, p in COLS] + T = [[A[j][i] for j in range(n)] + [1.0 if k == i else 0.0 for k in range(m)] + [float(rhs[i])] for i in range(m)] + basis = [n + i for i in range(m)] + + def pivot(r, c): + pv = T[r][c] + T[r] = [x / pv for x in T[r]] + for i in range(m): + if i != r and T[i][c] != 0.0: + f = T[i][c] + T[i] = [x - f * y for x, y in zip(T[i], T[r])] + basis[r] = c + + def run(cv, allowed): + for _ in range(10000): + cb = [cv[basis[i]] for i in range(m)] + best = None + for j in allowed: + rc = cv[j] - sum(cb[i] * T[i][j] for i in range(m)) + if rc < -1e-12 * (1 + abs(cv[j])) and (best is None or rc < best[0]): + best = (rc, j) + if best is None: + return + j = best[1] + rat = None + for i in range(m): + if T[i][j] > 1e-12: + q = T[i][-1] / T[i][j] + if rat is None or q < rat[0] - 1e-12: + rat = (q, i) + assert rat is not None, 'unbounded' + pivot(rat[1], j) + raise RuntimeError('simplex iteration limit') + + run([0.0] * n + [1.0] * m, range(n + m)) + assert all(basis[i] < n or abs(T[i][-1]) < 1e-6 for i in range(m)), 'infeasible LP' + cv = list(cost) + [1e12] * m + run(cv, range(n)) + sol = {basis[i]: T[i][-1] for i in range(m) if basis[i] < n} + duals = [sum(cv[basis[k]] * T[k][n + i] for k in range(m)) for i in range(m)] + return sum(cost[j] * x for j, x in sol.items()), sol, duals + + +def rhs_of(case): + inv = CASES[case]['inv'] + return [NB[R] for R in NB] + [CALLS * inv[w] for w in WID] + + +def local_counts(case): + c = CASES[case] + out = {} + for r in set(c['pg']) | set(c['pe']): + out[r] = 249 * c['pg'].get(r, 0) + 417 * c['pe'].get(r, 0) + return out + + +def lp_mu_float(case, a): + v, sol, duals = simplex([h_float(R - sum(p), a) for R, p in COLS], rhs_of(case)) + loc = sum(n * h_float(r, a) for r, n in local_counts(case).items()) + return (loc + v) / W_LIVE, sol, duals + + +def lp_root_float(case): + lo, hi = 0.0015, 0.0018 + for _ in range(45): + mid = (lo + hi) / 2 + if lp_mu_float(case, mid)[0] < 1: + lo = mid + else: + hi = mid + return lo, hi + + +def certify(case, a0): + """Exact lower bound of 66304*mu(a0) valid for every legal fill; True if it exceeds 66304.""" + a0 = Fraction(a0) + _mu, sol, duals = lp_mu_float(case, float(a0)) + y = {R: Fraction(duals[i]) for i, R in enumerate(NB)} + z = {w: Fraction(duals[len(NB) + i]) for i, w in enumerate(WID)} + L = {r: h_lower(r, a0) for r in range(0, 49)} + worst = {R: Fraction(0) for R in NB} + for R, p in COLS: + slack = L[R - sum(p)] - y[R] - sum(z[w] for w in p) + if slack < worst[R]: + worst[R] = slack + y = {R: y[R] + worst[R] for R in NB} # exact dual feasibility + for R, p in COLS: + assert y[R] + sum(z[w] for w in p) <= L[R - sum(p)] + rhs = rhs_of(case) + dual_bound = sum(NB[R] * y[R] for R in NB) + sum(rhs[len(NB) + i] * z[w] for i, w in enumerate(WID)) + local_lower = sum(n * h_lower(r, a0) for r, n in local_counts(case).items()) + total = local_lower + dual_bound + return total > W_LIVE, dict(a0=str(a0), dual_repair={str(R): float(worst[R]) for R in NB}, + lower_bound_of_W_mu=float(total), W=W_LIVE, margin=float(total - W_LIVE), + certified_b_below_a0=total > W_LIVE) + + +PR2360_DUAL = ('inputs/PR2360-DUAL.json', '78c68d193cb0fe9d6ff6183596f34893602422f3', + 'b7fa099301a15fc063bab2250c6df6fc7d013cfabefabd47d3952544738559b5') + + +def check_pr2360_dual(tamper=None): + """Independent re-check of PR2360's nine dual coefficients (head 16d4ea6c, Jeremy Diviney) with this file's + pattern enumeration and 800-bit h enclosures. PR2360 states z_R + sum_s n_s y_s <= f_b(r), f_b(r) = + (73 h_b(r) - r)/b; in this file's normalisation that is the dual Y_R = (b z_R + R)/73, Z_s = (b y_s - s)/73. + Returns the exact lower bound of 66304*mu(b) for (i) the actual 249 gauge44 / 417 extra dispatch and (ii) + PR2360's all-extra envelope; raises AssertionError if any of the 1163 pattern inequalities fails.""" + path = os.path.join(HERE, PR2360_DUAL[0]) + data = open(path, 'rb').read() + assert hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() == PR2360_DUAL[1] + assert hashlib.sha256(data).hexdigest() == PR2360_DUAL[2] + d = json.loads(data) + assert tuple(d['widths']) == WID and tuple(d['bin_ranks']) == tuple(NB) + b = Fraction(d['threshold']) + y = {s: Fraction(v) for s, v in zip(d['widths'], d['width_dual'])} + z = {R: Fraction(v) for R, v in zip(d['bin_ranks'], d['bin_dual'])} + if tamper: + z[tamper[0]] += Fraction(tamper[1]) + Y = {R: (b * z[R] + R) / M for R in NB} + Z = {s: (b * y[s] - s) / M for s in WID} + L = {r: h_lower(r, b) for r in range(0, 49)} + slack = {R: None for R in NB} + for R, p in COLS: + s_ = L[R - sum(p)] - Y[R] - sum(Z[s] for s in p) + assert s_ >= 0, ('PR2360 dual infeasible', R, p) + slack[R] = s_ if slack[R] is None else min(slack[R], s_) + inv = CASES['ext80']['inv'] + dual_bound = sum(NB[R] * Y[R] for R in NB) + sum(CALLS * inv[s] * Z[s] for s in WID) + actual = sum(n * h_lower(r, b) for r, n in local_counts('ext80').items()) + dual_bound + envelope = CALLS * sum(n * h_lower(r, b) for r, n in CASES['ext80']['pe'].items()) + dual_bound + assert envelope <= actual + return dict(threshold=str(b), pins=dict(path=PR2360_DUAL[0], git_blob=PR2360_DUAL[1], sha256=PR2360_DUAL[2], + pr2360_head='16d4ea6c26cd45ebb9301ab90f33a73615627f8d'), + patterns_checked=len(COLS), lower_bound_of_W_mu_actual_dispatch=float(actual), + lower_bound_of_W_mu_all_extra_envelope=float(envelope), + certified_b_below_threshold=envelope > W_LIVE, + min_slack_in_pr2360_units={str(R): float(M * slack[R] / b) for R in NB}, + _tamper_to_violate_48=M * slack[48] / b + Fraction(1, 10**12)) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--out', action='store_true') + args = ap.parse_args() + t0 = time.time() + for case, c in CASES.items(): + assert sum(r * n for r, n in c['pg'].items()) == sum(r * n for r, n in c['pe'].items()) == \ + 1856 + sum(w * n for w, n in c['inv'].items()), case + out = dict(model=__doc__.split('\n\n')[1], patterns=len(COLS), bins=NB, cases={}) + certs = {'ext80': '0.0016867', 'high43': '0.0016965', 'high48_5high_only': '0.0016965', + 'low75_32low_only': '0.0016867', 'pr2322_control': '0.0016973'} + for case in CASES: + lo, hi = lp_root_float(case) + mu, sol, _d = lp_mu_float(case, lo) + basis = sorted(([R, list(p), R - sum(p), round(x, 4)] for j, x in sol.items() + for (R, p) in [COLS[j]] if x > 1e-9), key=lambda z: (z[0], z[1])) + ok, cert = certify(case, certs[case]) + assert ok, ('certificate failed', case, cert) + out['cases'][case] = dict(inventory={str(k): v for k, v in CASES[case]['inv'].items()}, + lp_root_float=[lo, hi], lp_optimal_patterns=basis, certificate=cert) + print('%-18s LP ceiling (float) b_LP = %.13f certified: every legal fill has b < %s (margin %.3g)' + % (case, lo, certs[case], cert['margin'])) + # controls + hi43 = Fraction(certs['high43']) + assert CLAIM_2269 < hi43, 'positive control: PR2269 realized b lies below its own certified ceiling' + ok, cert = certify('high43', CLAIM_2269) + assert not ok, 'control: PR2269 has a legal fill at its claimed b, the certificate must not reject it' + out['controls'] = dict(pr2269_claim_below_high43_ceiling=True, high43_not_rejected_at_pr2269_claim=cert) + assert CLAIM_2322 < Fraction(certs['pr2322_control']), 'positive control: PR2322 claim below its own ceiling' + ok, cert = certify('pr2322_control', CLAIM_2322) + assert not ok, 'control: PR2322 reports a legal fill at its claimed kappa; the certificate must not reject it' + out['controls']['pr2322_not_rejected_at_its_claim'] = cert + out['controls']['pr2322_fraction_of_its_ceiling'] = float(CLAIM_2322 / Fraction(out['cases']['pr2322_control']['lp_root_float'][1])) + x2360 = check_pr2360_dual() + assert x2360['certified_b_below_threshold'], ('PR2360 dual does not certify', x2360) + dz = x2360.pop('_tamper_to_violate_48') + try: + check_pr2360_dual(tamper=(48, dz)) + raise RuntimeError('negative control: a tampered PR2360 dual (z_48 + min slack + 1e-12) was accepted') + except AssertionError: + pass + x2360['tampered_z48_by_min_slack_plus_1e-12_rejected'] = True + out['controls']['pr2360_dual_independent_recheck'] = x2360 + print('PR2360 DUAL.json (b < %s) re-checked independently: 1163/1163 pattern inequalities hold; ' + 'lower bound of 66304*mu = %.6f (all-extra envelope) / %.6f (actual dispatch) > 66304' + % (x2360['threshold'], x2360['lower_bound_of_W_mu_all_extra_envelope'], + x2360['lower_bound_of_W_mu_actual_dispatch'])) + fill_b = None + rec = os.path.join(HERE, 'check_fill.receipt.json') + if os.path.exists(rec): + fill_b = Fraction(json.load(open(rec))['price']['root_bracket'][0]) + ok, cert = certify('ext80', fill_b) + assert not ok, 'negative control: OWNERS-80 is a legal fill with this b; certificate must fail here' + out['controls']['ext80_not_rejected_at_owners80_b'] = cert + out['owners80_b_floor'] = str(fill_b) + out['owners80_fraction_of_ext80_ceiling'] = float(fill_b / Fraction(out['cases']['ext80']['lp_root_float'][1])) + ext = Fraction(certs['ext80']) + assert ext < CLAIM_2269 < CLAIM_2322 + out['conclusion'] = ('Every legal whole-helper owner fill of the PR2339 80-alias words on the PR2269 T74 template ' + 'has b < %s < PR2269 claim %s < PR2322 claim %s.' % (certs['ext80'], P.dec(CLAIM_2269, 40), + P.dec(CLAIM_2322, 18))) + out['credits'] = ('PR2339 (this author); PR2360 Jeremy Diviney (concurrent, independent certificate b < 0.0016870 for ' + 'the same words with the same 1163-pattern relaxation; its DUAL.json re-checked here); PR1129 Ali ' + 'Romman (R480 pattern-dual relaxation, the method); PR2269 Jeremy Kothe; PR2322 Vlado Vojdanovski; ' + 'PR2312/PR2302 jeremykothe2; PR2226 Cinna Davis; PR1319/PR1297 T74 lineage. Prepared with ' + 'substantial AI assistance (Claude Code, Anthropic); Apache-2.0.') + if args.out: + with open(os.path.join(HERE, 'ceiling_lp.receipt.json'), 'w') as h: + h.write(json.dumps(out, indent=1, sort_keys=True) + '\n') + print(out['conclusion']) + if fill_b is not None: + print('OWNERS-80 realizes %.6f of the ext80 LP ceiling' % out['owners80_fraction_of_ext80_ceiling']) + print('runtime %.1fs' % (time.time() - t0)) + print('PASS_T74_WIDTH_AWARE_CEILING') + return 0 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/research/t74-2322-move-prices/vendor/pr2387/fill_check80.py b/research/t74-2322-move-prices/vendor/pr2387/fill_check80.py new file mode 100644 index 0000000000..557e0732bf --- /dev/null +++ b/research/t74-2322-move-prices/vendor/pr2387/fill_check80.py @@ -0,0 +1,1285 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Standalone independent recount of the 80-alias T74 whole-helper owner fill (OWNERS-80.json.gz). + +Object: OWNERS-80.json.gz of this package (research/t74-80alias-owner-fill/, sha256 pinned below): 266,400 +literal roles hosting the 400 live helpers of the two 80-alias T74 borrow words of PR #2339 +(BORROW-WORD-80base = provider gauge44, BORROW-WORD-80extra = provider extra; commit bf1742ae) in the idle +children of PR #2269's unchanged T74 template (head b479fc55: 74 replicas, nine stages, 666 calls). + +This file is an adaptation of our own iteration-3 independent checker (fill_check.py and the frame recount of +words_check.py, research/t74-borrow43-independent-check/ at commit 4a2f20ea, Apache-2.0, same author). It is +standalone: standard library only, it imports no module of this package (not build_fill.py, not +check_fill.py, not vendor/), and no code of PR #2269 / #2322 / #2339 is imported or run. Every input is a git +blob read with `git cat-file` at a pinned commit and is pinned by git blob id *and* sha256. The PR #2339 files +are read from commit bf1742ae when it is present; otherwise from the byte-identical copies in inputs/, which +must match the same blob ids and sha256 pins. The recount does not read PROFILE-80.json or BUILD-RECEIPT.json; +those, and the builder's reported numbers (CLAIMS below), are only compared with the recount at the end. +All accepted facts are integer or GF(2) facts. The script refuses `python -O`. + +Hosting rules (PR858 / complex-double-replica-owners PROOF.md lineage; T16 owner audit rules R1-R7/X1): + R-a one role per (call, live helper): 666 calls x 400 helpers; helper i = i-th live helper register of the + word (224..703 minus the 80 `removed`, increasing); width = dim(final frame) - dim(start frame) over + GF(2), re-derived from both words (they have equal live registers and ordered widths, asserted). + R-e family = owner*896 + (2*pair(child)+side(child))*112 + port, copy = 112*owner + port; family inside the + data namespace [0, W), W = 896*74 = 66304; not the caller's active pair; at most one helper per family + per call. + R-d the call lies strictly inside the owner's actual window, rebuilt from the template's 30 per-replica + source events expanded in ORDER (bridge-aware). X1: rebuilt windows == PR #2269 new/PLAN.json windows. + R-b slices [offset, offset+width) lie in [0, rank(child)), are disjoint per bin (owner, child, port) and + form an occupied prefix. + R-c idle remainders (rank - occupied, per bin) and the global profile sum_calls P_provider + idle are + recounted here; P_provider is recounted from the word by the frame-climb rule (nested climbs + COPY + charges) and compared with the word report and PR #2339's AUDIT receipts; rank-mass, deficit, capacity + and halving identities. + R-f private namespace, stated as PR #2322 does (README "complete physical stock" and + evidence/PRIVATE-NAMESPACE-INJECTION.json): physical = W + 8 centres + R reserved tableau + 2 + coefficient work; centres [W, W+8), reserved tableau [W+8, W+8+R), coefficient [P-2, P); the NZ + private cleanup zero buffers (buffer register r + 704 for every hyperplane-ended live helper r) are + injected in increasing order into [W+8, W+8+NZ), which must lie inside the reserved tableau (NZ <= R); + every hosted helper family is a live data family (< W), hence disjoint from all private names. + The same rule applied to (R, NZ) = (434, 78) must reproduce PR #2322's stated geometry exactly. + R-g X2 and 73-column charts (rule of PR #2269 independent_core.py check_pending_axes / check_roles, Hao Yan + checker lineage): DATA-PHASES.json is read at the PR #2269 commit (blob pinned; its sha256 must equal the + template's exact_data_phase_recipe_sha256) and its 112 port vectors must equal both words' ports. Per + port, the owner 73-frame is orthonormal; every ranked child's pending orthogonal axes are rank-many, + distinct and in that frame, and children sharing a family (pair, side) have disjoint axes (X2). Every + role's slice binds pending[offset:offset+width] to a residual/spectator permutation of the 73 columns; + the distinct charts are counted (positive control: PR #2269's fill gives its SPEC actual_73column_sigmas). + +Positive control: the same pipeline on PR #2269's own fill (OWNERS.json.gz, 437 helpers of the 43-alias +words), including the PLAN per_call_widths comparison, must reproduce its idle {1:23976,3:8673,5:813,7:150, +48:24479} and its global profile. For the 80-alias fill the PLAN per_call_widths comparison (437-helper +lists) is replaced by the word-derived widths; everything else of the static checks, including X1, is kept. +Negative controls: each mutation must be rejected by the check it targets. + +Credits: PR2339 (this author: the 80-alias words); PR2269 Jeremy Kothe (jeremykothe2; T74 template, +windows, dispatch, owner-row format); PR2322 Vlado Vojdanovski (owner exchanges; the private-namespace +statement followed here); PR2312/PR2302 jeremykothe2; PR2226 Cinna Davis (anticipatory dirty borrowing); +PR1319/PR1297 T74 lineage (Rohan Arun et al.); hosting rules of Hao Yan's PR858 / complex-double-replica-owners +PROOF.md and the T16 owner audit (Josie Elliston; icekylinx / Zhihao Chen checker lineage). +Prepared with substantial AI assistance (Claude Code, Anthropic); Apache-2.0. + +Usage: python3 -I -B fill_check80.py [--repo PATH] [--words-from-inputs] [--skip-positive-control] [--out] +The final stdout line starts with PASS_T74_80ALIAS_FILL_INDEPENDENT or FAIL_T74_80ALIAS_FILL_INDEPENDENT. +""" + +import argparse +import bisect +import gzip +import hashlib +import json +import os +import subprocess +import sys +import time +from collections import Counter +from fractions import Fraction + +if not __debug__: + sys.stdout.write('FAIL_T74_80ALIAS_FILL_INDEPENDENT refusing to run under python -O\n') + sys.exit(2) + +HERE = os.path.dirname(os.path.abspath(__file__)) +REPO_DEFAULT = os.path.dirname(os.path.dirname(HERE)) +RECEIPT_NAME = 'fill_check80.receipt.json' +PASS_LINE = 'PASS_T74_80ALIAS_FILL_INDEPENDENT' +FAIL_LINE = 'FAIL_T74_80ALIAS_FILL_INDEPENDENT' + +HEAD_2269 = 'b479fc5567bc09ab9185bffe89b62594f36d74e5' +PKG_2269 = 'research/gmx-t74-borrow43' +HEAD_2322 = '002304ef01c4416a127916169ae6d94c1bee052b' +PKG_2322 = 'research/t74-joint-owner-hillclimb' +HEAD_2339 = 'bf1742aee4d855efb8bbd44a8419eddb33a679e5' +PKG_2339 = 'research/t74-low-alias-borrowing' + +# package-relative path -> (git blob id, sha256) +PINS_2269 = { + 'OWNERS.json.gz': ('fc874cb553af5b984e34c1d8696d2213d7458f8f', '5a8c9a18c21f635563c9a6b6a433bcb1e804175ef23d677459033344aa2bd4e6'), + 'new/PROFILE.json': ('3e103605dd46c8754028056eb9dde9a73b9bfdca', '50fcc0960a47f6d35064d3b55ea6dcb4cebbd305aec215c8034f626718595538'), + 'new/SPEC.json': ('2431d1cebbb2e155356d2da160d60808498bc33d', 'bd091ed9e7f4939d06abb467d0d2c56ce0f34ba800d74132669f7b667e125d2d'), + 'new/PLAN.json': ('7cacd857edd0f29be5bd2ca9590a17fed4da17ba', 'bf1abd33c8ba946371cae37e021747343ef6603a31297bcc962197cc23f535e2'), + 'CONSTRUCTION.json': ('034ec6c6309bd1279661918f2a8706268f9a1200', '37b8605607b2877d82b8403d509f5cd224240064c93fa67ce89a8894acc6b460'), + 'GLOBAL-TEMPLATE.json.gz': ('5327fc2f4e8ea82ed356c94ff040d23fc73c731f', '1d31424c4e27e26a35a9932ca778e43f1f3577589275422cc642aa68b31112db'), + 'ORDER.json': ('7409c4df1092241729739596c7648bda504e6aad', '519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1'), + 'DISPATCH.json': ('20807cc27c82db1f8f9cd47c79713e066d6ad816', '6aad7f628f4c9b510a95c5b34357736303069ecf92a551659900b1ba540bc7e0'), + 'new/borrow/words/BORROW-WORD-43base.json.gz': ('448dd795adba29392a90b34aa3f1b1b796c7e0bd', '9492a5537fb87d9ca98dffcd0230f7625b3789744fa94e2f18acf23d91d998b5'), + 'new/borrow/words/BORROW-WORD-43extra.json.gz': ('2b51ba96256283bbc5578f99b694c50edd8a0e35', '87d51f5298101d5947f45c43ee02f0ec45d6acbddabb808d0d02db1eaf063734'), + 'new/borrow/receipts/AUDIT-43base.json': ('65728eff3ef61c275c873b58f0f8cebc095ef6f9', '9af87b149b8efa58e2454541dd1c5aef86d893c71ec488ae69fb8680c2f7936e'), + 'new/borrow/receipts/AUDIT-43extra.json': ('f9c2401401612b3b0b6e652e142e65bceadc1170', '849fbe9b9267180ba914237d751b118b4539731249c4482e6264d4772932fd2d'), + 'evidence/INDEPENDENT.json': ('16bb558f2472df730076a8163454c6f70b9e9fe3', '78cd00f832ed3c0a4b0e0d202095f7beb6111eaeb4457849d5bb920e983098a0'), +} +# DATA-PHASES.json of the template (outside the PR2269 package dir, present in the b479fc55 tree and on main). +PKG_PHASES = 'research/community-cold617-audit/pr600/replay/mixed-global/base/work/complex-nine-native' +PINS_PHASES = { + 'DATA-PHASES.json': ('d9a4f84211182ca200c081ea061d724c8a2cfb70', 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa'), +} +PINS_2322 = { + 'evidence/PRIVATE-NAMESPACE-INJECTION.json': ('3588cb8991177c10059ce99bd3949220bbe52580', 'fad0f68aa273e39f63904462b7ade93c7c50c29d7278d0c37eee2139bbdcad65'), + 'CLAIM.json': ('e10747182e8bdfa2fea1c8631bf738c15619eccb', '439ded151e7897b8e7d5ef9ad47f3cd8d1daf0b69219ef507a922519c7003530'), +} +# PR #2339 files; inputs/ is a byte-identical copy used when commit bf1742ae is absent. +PINS_2339 = { + 'words/BORROW-WORD-80base.json.gz': ('c5953dfdb0ee9ac0c2c73eb29e320582b4569d2b', '61290abffd8c8225e0abb3958c1506674e256de688fc4cdf358bbe7c981df493'), + 'words/BORROW-WORD-80extra.json.gz': ('852868543ed36efa799b3ed6dd76a0442b0d6ff1', '1dd2d6f2ae5b5a27b5f89fb830203f0cca7a78d0323a7845e85e1e80f8f6d1a5'), + 'receipts/AUDIT-80base.json': ('fc16634cfd3a9c5190e5b97b93cb29ddbd1547ca', 'd65a79658cba82932a9abd2c9af5dd345527141b098130b98850572420166cdd'), + 'receipts/AUDIT-80extra.json': ('b1b0c4d69e4c1a5edc3e9dd968f6f58b5eb8aaf0', '6d05abbc122d72b1eec05e7654a118dd492e55db34b30b718603521231094099'), +} +# The object under test (this package, untracked build output of build_fill.py). +OWNERS_80 = ('OWNERS-80.json.gz', 'b79d678dc8ae685fdecedca994e41b41c8a2930564ec0c58c707d7d13a3870a5') + +# Builder's reported numbers (claims under test, written here from the build report; compared at the end only). +CLAIMS_80 = dict( + roles=266400, cross_replica=251101, idle_remainders=69734, + idle={1: 2644, 3: 10310, 5: 27847, 7: 6114, 41: 33, 48: 22786}, + profile={1: 1529770, 2: 354318, 3: 267386, 4: 83250, 5: 52489, 7: 6114, 8: 5328, 41: 33, 48: 22786}, + local={'gauge44': {1: 2303, 2: 527, 3: 386, 4: 125, 5: 37, 8: 8}, + 'extra': {1: 2287, 2: 535, 3: 386, 4: 125, 5: 37, 8: 8}}, + inventory={4: 4, 5: 4, 7: 36, 8: 84, 9: 272}, zero_buffers=44) +CLAIMS_2269 = dict(idle={1: 23976, 3: 8673, 5: 813, 7: 150, 48: 24479}) + +# Geometry of the nine-stage, four-pair, 112-port controller (template/PLAN): +V = 112 # data ports per (pair, side) +H = 9 # local frame dimension +M = 73 # global dimension m +STAGES = 9 +PAIRS = 4 +FAMILIES_PER_REPLICA = 2 * PAIRS * V # 896 +CENTRES, COEFFICIENT_WORK = 8, 2 +REGISTERS = 2 * V + 480 # n = 704: X, Y and helper registers of a word +ROW_LIMIT = 20161 +ROW_CONSTANTS = 9909 + 252 # retained row formula 2*stock + 9909 + 252 + 2*payload +TAIL_KINDS = ('bank_padding_cover_sweep', 'translate_every_live_family') +ROLE_KEYS = ('child', 'copy', 'family', 'helper', 'offset', 'owner_replica', + 'port', 'replica', 'stage', 'time', 'width') + + +class CheckFailure(Exception): + def __init__(self, check, detail): + Exception.__init__(self, check + ': ' + detail) + self.check = check + self.detail = detail + + +def need(condition, check, detail): + if not condition: + raise CheckFailure(check, detail) + + +# ---------------------------------------------------------------- inputs --- + +def git(repo, *args): + proc = subprocess.run(['git', '-C', repo] + list(args), stdout=subprocess.PIPE, + stderr=subprocess.PIPE, check=False) + need(proc.returncode == 0, 'input.git', 'git ' + ' '.join(args) + ' failed: ' + + proc.stderr.decode('utf-8', 'replace').strip()) + return proc.stdout + + +def commit_present(repo, commit): + proc = subprocess.run(['git', '-C', repo, 'cat-file', '-e', commit + '^{commit}'], + stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False) + return proc.returncode == 0 + + +def blob_id(data): + return hashlib.sha1(('blob %d' % len(data)).encode() + b'\0' + data).hexdigest() + + +def verify(data, oid, sha, what): + need(blob_id(data) == oid, 'input.pin', 'git blob id of ' + what) + need(hashlib.sha256(data).hexdigest() == sha, 'input.pin', 'sha256 of ' + what) + + +def read_pinned(repo, commit, pkg, pins, label): + need(commit_present(repo, commit), 'input.pin', '%s commit %s missing from %s (run run_all.py --fetch)' + % (label, commit, repo)) + blobs, record = {}, {} + for rel in sorted(pins): + oid, sha = pins[rel] + path = pkg + '/' + rel + got = git(repo, 'rev-parse', '--verify', commit + ':' + path).decode().strip() + need(got == oid, 'input.pin', path + ' resolves to ' + got + ', pinned ' + oid) + data = git(repo, 'cat-file', 'blob', oid) + verify(data, oid, sha, path) + blobs[rel] = data + record['%s:%s' % (commit[:12], path)] = dict(git_blob=oid, sha256=sha, bytes=len(data)) + return blobs, record + + +def read_2339(repo, force_inputs=False): + """PR #2339 words/receipts: git blobs at bf1742ae if present (inputs/ copies must then be identical), + else the inputs/ copies (same pins).""" + use_git = commit_present(repo, HEAD_2339) and not force_inputs + blobs, record = {}, {} + for rel in sorted(PINS_2339): + oid, sha = PINS_2339[rel] + copy = os.path.join(HERE, 'inputs', os.path.basename(rel)) + path = PKG_2339 + '/' + rel + if use_git: + got = git(repo, 'rev-parse', '--verify', HEAD_2339 + ':' + path).decode().strip() + need(got == oid, 'input.pin', path + ' resolves to ' + got + ', pinned ' + oid) + data = git(repo, 'cat-file', 'blob', oid) + if os.path.isfile(copy): + with open(copy, 'rb') as handle: + need(handle.read() == data, 'input.pin', 'inputs copy differs from the git blob: ' + copy) + source = 'git %s:%s' % (HEAD_2339[:12], path) + else: + need(os.path.isfile(copy), 'input.pin', 'commit %s absent and inputs copy missing: %s' % (HEAD_2339, copy)) + with open(copy, 'rb') as handle: + data = handle.read() + source = 'inputs/' + os.path.basename(rel) + verify(data, oid, sha, path) + blobs[rel] = data + record['%s:%s' % (HEAD_2339[:12], path)] = dict(git_blob=oid, sha256=sha, bytes=len(data), read_from=source) + return blobs, record, ('git' if use_git else 'inputs') + + +def parse_bytes(data, gz): + if gz: + data = gzip.decompress(data) + return json.loads(data.decode('utf-8'), parse_float=Fraction) + + +def parse(blobs, rel): + return parse_bytes(blobs[rel], rel.endswith('.gz')) + + +def as_profile(mapping, check, what): + out = Counter() + for key, value in mapping.items(): + need(type(value) is int and value >= 0 and str(int(key)) == str(key), check, what + ' profile entry') + if value: + out[int(key)] = value + return out + + +def plain(counter): + return {str(k): counter[k] for k in sorted(counter) if counter[k]} + + +def mass(counter): + return sum(r * n for r, n in counter.items()) + + +# ------------------------------------------------- GF(2) frames and widths --- +# (from our iteration-3 fill_check.py / words_check.py) + +FULL = [1 << i for i in range(H)] + + +def gf2_rank(vectors, check): + pivots = {} + for x in vectors: + need(type(x) is int and 0 <= x < 1 << H, check, 'frame vector outside GF(2)^9') + while x: + top = x.bit_length() - 1 + if top in pivots: + x ^= pivots[top] + else: + pivots[top] = x + break + return len(pivots) + + +def parity(x): + return bin(x).count('1') & 1 + + +def echelon(vectors): + piv = {} + for x in vectors: + x = int(x) + for b in list(piv): + if (x >> b) & 1: + x ^= piv[b] + if x: + lead = x.bit_length() - 1 + for b in list(piv): + if (piv[b] >> lead) & 1: + piv[b] ^= x + piv[lead] = x + return piv + + +def span(vectors): + """Canonical key of a subspace: its reduced echelon basis, sorted decreasingly.""" + return tuple(sorted(echelon(vectors).values(), reverse=True)) + + +def contains(small, big): + piv = echelon(big) + for x in small: + for b, vec in piv.items(): + if (x >> b) & 1: + x ^= vec + if x: + return False + return True + + +def perp(sub, h): + return span([x for x in range(1, 1 << h) if all(parity(x & u) == 0 for u in sub)]) + + +def word_helpers(word, label, removed_count): + """Live helper registers, their residual widths and the hyperplane-ended set (R-a).""" + check = 'R-a.word' + report = word['report'] + need((report.get('v'), report.get('h'), report.get('R')) == (V, H, 480), check, label + ' dimensions') + need(len(word['ports']) == V, check, label + ' port count') + first, end = 2 * V, 2 * V + 480 + removed = list(word.get('removed', [])) + need(all(type(r) is int and first <= r < end for r in removed) and len(set(removed)) == len(removed), + check, label + ' removed registers') + need(len(removed) == removed_count, check, label + ' removed register count') + removed_set = set(removed) + for table in ('helper_final', 'start_extra'): + for key in word[table]: + need(first <= int(key) < end and int(key) not in removed_set, check, + label + ' ' + table + ' names a non-live register ' + key) + live = [r for r in range(first, end) if r not in removed_set] + widths, ended = [], [] + for r in live: + final = word['helper_final'].get(str(r)) + if final is None: + final = FULL + else: + ended.append(r) + start = word['start_extra'].get(str(r), []) + rank_final, rank_start = gf2_rank(final, check), gf2_rank(start, check) + need(rank_final == len(final) and rank_start == len(start), check, label + ' dependent frame list at %d' % r) + need(gf2_rank(list(final) + list(start), check) == rank_final, check, + label + ' start frame not inside final frame at %d' % r) + widths.append(rank_final - rank_start) + return dict(live=live, removed=sorted(removed), widths=widths, hyperplane_ended=ended) + + +# ------------------------------------------------- local paid-profile recount --- +# Frame-climb rule of our iteration-3 words_check.py (frame_check), extended to the anticipatory initial +# corrections of PR2226/PR2339: they run first, at frame 0, and pay nothing. + +def _dyadic(q): + return q.denominator & (q.denominator - 1) == 0 + + +def _gate(g, frame_of, where, allow_warp=False): + check = 'R-c.local_format' + need(isinstance(g, list) and g, check, 'gate is not a list at %s' % where) + op = g[0] + if op == 'add': + need(len(g) == 6 and all(type(x) is int for x in g[1:5]) and g[4] > 0 and g[3] != 0 and g[1] != g[2], + check, 'bad add at %s' % where) + need(_dyadic(Fraction(g[3], g[4])), check, 'non-dyadic coefficient at %s' % where) + return ('add', g[1], g[2], frame_of(g[5])) + if op == 'scale': + need(len(g) == 5 and all(type(x) is int for x in g[1:4]) and g[2] != 0 and g[3] != 0, check, + 'bad scale at %s' % where) + q = Fraction(g[2], g[3]) + need(_dyadic(q) and abs(q.numerator) & (abs(q.numerator) - 1) == 0, check, 'scale not a dyadic unit at %s' % where) + return ('scale', g[1], frame_of(g[4])) + if op == 'warp' and allow_warp: + need(len(g) == 4 and type(g[1]) is int and type(g[2]) is int and g[2] != 0, check, 'bad warp at %s' % where) + return ('warp', g[1], frame_of(g[3])) + raise CheckFailure(check, 'unknown primitive %r at %s' % (op, where)) + + +def _regs(item): + return (item[1], item[2]) if item[0] == 'add' else (item[1],) + + +def local_recount(w, label): + """Paid local profile, helper widths and private zero buffers of one BORROW-WORD, recounted.""" + check = 'R-c.local' + need(w.get('kind') == 'BORROW-WORD', check, label + ' not a BORROW-WORD') + v, h, n = V, H, REGISTERS + full = span(FULL) + + def frame_lit(F): + if F is None: + return None + need(isinstance(F, list) and all(type(x) is int and 0 < x < (1 << h) for x in F), check, 'frame literal') + return span(F) + + ports = w['ports'] + removed = set(w['removed']) + live = [r for r in range(n) if r not in removed] + start, end = {}, {} + for i in range(v): + start[i], end[i] = span([ports[i]]), full + start[v + i], end[v + i] = (), perp(span([ports[i]]), h) + for r in live: + if r >= 2 * v: + start[r], end[r] = (), full + for k, F in w['start_extra'].items(): + need(int(k) in start and int(k) >= 2 * v, check, label + ' start_extra register') + start[int(k)] = frame_lit(F) + restored = set() + for k, F in w['helper_final'].items(): + need(int(k) in end and int(k) >= 2 * v, check, label + ' helper_final register') + end[int(k)] = frame_lit(F) + restored.add(int(k)) + buffers = set(r + n for r in restored) + sec = {name: [_gate(g, frame_lit, '%s[%d]' % (name, i)) for i, g in enumerate(w[name])] + for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore')} + cleanup = [_gate(g, frame_lit, 'cleanup[%d]' % i, allow_warp=True) for i, g in enumerate(w['cleanup'])] + warps = {} + by_pos = {} + for k, rec in enumerate(w['warps'], 1): + need(isinstance(rec, list) and len(rec) == 5, check, 'warp record shape') + pos, lender, _cols, U, E = rec + need(type(pos) is int and 0 <= pos <= len(sec['B']) and lender in start and not (v <= lender < 2 * v), check, + 'warp %d position/lender' % k) + warps[k] = dict(lender=lender, U=span(U), E=span(E)) + need(len(warps[k]['U']) == len(U) == len(E) == len(warps[k]['E']), check, 'warp %d frame dimensions' % k) + by_pos.setdefault(pos, []).append(k) + need(len(set(x['lender'] for x in warps.values())) == len(warps), check, 'a register lends twice') + cur = {r: start[r] for r in live} + paid, copies, per_reg = Counter(), Counter(), Counter() + istarget = lambda r: v <= r < 2 * v + + def climb(r, F, where): + need(r in cur, check, 'register %d is not live (%s)' % (r, where)) + need(contains(cur[r], F), check, 'non-nested climb of %d at %s' % (r, where)) + d = len(F) - len(cur[r]) + if d: + paid[d] += 1 + per_reg[r] += d + cur[r] = F + + # initial (anticipatory) corrections: t += c K_k s, both at frame 0, k a warp lent by s; pay nothing. + for i, c in enumerate(w['initial_corrections']): + t, s, word_k = c['target'], c['source'], c['operator_word'] + q = Fraction(c['coefficient']) + need(istarget(t) and s in cur and not istarget(s) and cur[t] == () and cur[s] == (), check, + 'initial correction %d: target/source not at frame 0' % i) + need(isinstance(word_k, list) and len(word_k) == 1 and word_k[0] in warps and warps[word_k[0]]['lender'] == s + and q != 0 and _dyadic(q), check, 'initial correction %d: operator/coefficient' % i) + for i, g in enumerate(sec['precondition'] + sec['compensation']): + need(g[-1] == () and istarget(g[1]), check, 'precondition/compensation gate %d' % i) + for r in _regs(g): + climb(r, (), 'pre[%d]' % i) + items = [] + for p in range(len(sec['B']) + 1): + items.extend(('warp', k) for k in by_pos.get(p, [])) + if p < len(sec['B']): + items.append(sec['B'][p]) + for i, g in enumerate(list(sec['A']) + [it for it in items if it[0] != 'warp'] + list(sec['restore'])): + need(not (g[0] == 'add' and not istarget(g[1]) and istarget(g[2])), check, + 'a non-target register reads a target (item %d of A+B+restore)' % i) + for i, g in enumerate(sec['A']): + need(g[-1] is not None, check, 'unframed gate in A') + for r in _regs(g): + climb(r, g[-1], 'A[%d]' % i) + levels = {int(k): frame_lit(F) for k, F in w['target_levels'].items()} + for t in range(v): + need(cur[v + t] == levels.get(t, ()), check, 'target %d not at its level after A' % t) + centers, cframes = list(w['centers']), [frame_lit(F) for F in w['center_frames']] + need(len(set(centers)) == len(centers) == len(cframes), check, 'centres') + for q, U in zip(centers, cframes): + need(q in cur and cur[q] == U, check, 'centre %d not at its centre frame after A' % q) + served = {q: set() for q in centers} + for i, g in enumerate(sec['cut']): + need(g[0] == 'add' and g[-1] is None and istarget(g[1]) and g[2] in served, check, 'cut[%d]' % i) + need(cur[g[1]] == levels.get(g[1] - v, ()), check, 'cut[%d] target off its level' % i) + served[g[2]].add(cur[g[1]]) + for q, U in zip(centers, cframes): + prev = U + for T in sorted(served[q], key=lambda S: (-len(S), S)): + need(contains(T, prev), check, 'centre %d copy levels not nested' % q) + if T != prev: + paid[len(prev) - len(T)] += 1 + copies[len(prev) - len(T)] += 1 + prev = T + for i, it in enumerate(items): + if it[0] == 'warp': + wr = warps[it[1]] + need(cur[wr['lender']] == wr['U'], check, 'warp %d: lender frame != U' % it[1]) + cur[wr['lender']] = wr['E'] + else: + need(it[-1] is not None, check, 'unframed gate in B') + for r in _regs(it): + climb(r, it[-1], 'B item %d' % i) + for i, g in enumerate(sec['restore']): + need(g[-1] is not None, check, 'unframed gate after B') + for r in _regs(g): + climb(r, g[-1], 'restore[%d]' % i) + for r in live: + climb(r, end[r], 'end frame') + touched_buffers = set() + for i, it in enumerate(cleanup): + need(it[-1] == full, check, 'cleanup item %d not at FULL' % i) + for r in ((it[1],) if it[0] == 'warp' else _regs(it)): + if r in buffers: + touched_buffers.add(r) + continue + need(r in cur and cur[r] == full, check, 'cleanup item %d touches %d not at FULL / not a buffer' % (i, r)) + need(touched_buffers == buffers, check, label + ' cleanup does not use exactly the declared zero buffers') + for r in live: + need(per_reg[r] == len(end[r]) - len(start[r]), check, 'per-register charge != width for %d' % r) + helpers = [r for r in live if r >= 2 * v] + return dict(paid=+paid, copies=+copies, widths=[len(end[r]) - len(start[r]) for r in helpers], live_helpers=helpers, + buffers=sorted(buffers), mass=mass(paid), corrections=len(w['initial_corrections']), + warps=len(warps)) + + +def load_word(blobs, rel, audit_rel, label, removed_count, claimed_local=None, claimed_inventory=None): + word = parse(blobs, rel) + audit = parse(blobs, audit_rel) if audit_rel else None + info = word_helpers(word, label, removed_count) + rec = local_recount(word, label) + need(rec['live_helpers'] == info['live'] and rec['widths'] == info['widths'], 'R-a.word', + label + ' frame-recount widths != GF(2) rank widths') + inventory = Counter(info['widths']) + need(inventory == as_profile(word['report']['width_inventory'], 'R-a.word', label), 'R-a.word', + label + ' width inventory vs word report') + local = rec['paid'] + need(local == as_profile(word['report']['local_profile'], 'R-c.local', label), 'R-c.local', + label + ' recounted local profile %s != word report %s' % (plain(local), word['report']['local_profile'])) + need(rec['copies'] == Counter({8: 8}), 'R-c.local', label + ' COPY children') + need(rec['buffers'] == sorted(r + REGISTERS for r in info['hyperplane_ended']), 'R-f.zero_buffers', + label + ' buffers = r + 704 for the hyperplane-ended live helpers') + if audit is not None: + need(as_profile(audit['local_profile'], 'R-c.local', 'audit') == local and + as_profile(audit['width_inventory'], 'R-a.word', 'audit') == inventory and + audit['zero_buffers'] == audit['restored_cold'] == len(rec['buffers']), 'R-c.local', + label + ' vs AUDIT receipt') + if claimed_local is not None: + need(local == Counter(claimed_local), 'R-c.local', label + ' local profile vs build report') + if claimed_inventory is not None: + need(inventory == Counter(claimed_inventory), 'R-a.word', label + ' inventory vs build report') + return dict(widths=info['widths'], live=info['live'], removed=info['removed'], local=local, inventory=inventory, + buffers=rec['buffers'], local_mass=rec['mass'], width_sum=sum(info['widths']), + corrections=rec['corrections'], warps=rec['warps']) + + +# --------------------------------------------------------------- context --- + +def derive_schedule(T, template, order): + """Expand the 30 per-replica source events in call order; rebuild windows (verbatim iteration-3 rule).""" + src = template['execution_schedule'] + need([i for i, e in enumerate(src) if e['kind'] in TAIL_KINDS] == [len(src) - 2, len(src) - 1], + 'R-d.schedule', 'global tail events') + per_replica = [i for i, e in enumerate(src) if e['kind'] not in TAIL_KINDS] + need(per_replica == list(range(30)), 'R-d.schedule', 'thirty per-replica source events') + stage_pair = {} + for e in template['recipe']: + if e['kind'] == 'local': + need(e['stage'] not in stage_pair and 0 <= e['pair'] < PAIRS, 'R-d.schedule', 'recipe stage/pair') + stage_pair[e['stage']] = e['pair'] + need(set(stage_pair) == set(range(STAGES)), 'R-d.schedule', 'recipe stages') + blocks, stage = {}, None + for i in per_replica: + e = src[i] + if e['kind'] == 'local_cover_sweep': + stage = e['stage'] + need(stage not in blocks and e['replicas'] == list(range(T)), 'R-d.schedule', 'local sweep block') + blocks[stage] = [] + need(stage is not None, 'R-d.schedule', 'event before first local sweep') + need(e['kind'] in ('local_cover_sweep', 'idle_cover_sweep', 'bridge', 'terminal_Y_translations', 'terminal'), + 'R-d.schedule', 'unknown source event kind ' + str(e['kind'])) + blocks[stage].append((i, e)) + need(set(blocks) == set(range(STAGES)), 'R-d.schedule', 'stage blocks') + rank = {} + for c in template['idle_children']: + need(c['replicas'] == T and 0 <= c['port'] < V and type(c['rank']) is int and c['rank'] > 0, + 'R-d.schedule', 'idle child record') + need(rank.setdefault(c['child'], c['rank']) == c['rank'], 'R-d.schedule', 'child rank depends on port') + need(len(template['idle_children']) == V * len(rank), 'R-d.schedule', 'idle children per port') + seen = Counter((c['child'], c['port']) for c in template['idle_children']) + need(all(n == 1 for n in seen.values()), 'R-d.schedule', 'duplicate idle child record') + events = [] + for t, (s, r) in enumerate(order): + for i, e in blocks[s]: + events.append((i, e, r, t)) + projection = {} + for i, e, r, t in events: + projection.setdefault(r, []).append(i) + need(set(projection) == set(range(T)) and all(p == per_replica for p in projection.values()), + 'R-d.schedule', 'per-replica source-event projection') + last, windows, callpos, child_pair, child_side = {}, {}, {}, {}, {} + rankless = set() + bridges = 0 + for pos, (i, e, r, t) in enumerate(events): + kind = e['kind'] + if kind == 'local_cover_sweep': + callpos[t] = pos + last[r, stage_pair[e['stage']]] = pos + elif kind == 'bridge': + bridges += 1 + last[r, e['src']] = pos + last[r, e['dst']] = pos + elif kind == 'idle_cover_sweep': + for side, child in enumerate(e['child_indices']): + if child not in rank: + rankless.add(child) # a swept child without an idle_children record has no capacity + continue + need((r, child) not in windows, 'R-d.schedule', 'idle sweep child') + need(child_pair.setdefault(child, e['pair']) == e['pair'] and + child_side.setdefault(child, side) == side, 'R-d.schedule', 'child pair/side') + windows[r, child] = (last.get((r, e['pair']), -1), pos) + else: # terminal events touch every pair; they follow every idle sweep of the replica + for p in range(PAIRS): + last[r, p] = pos + need(len(windows) == T * len(rank) and set(callpos) == set(range(len(order))), 'R-d.schedule', 'window inventory') + positions = [callpos[t] for t in range(len(order))] + need(all(a < b for a, b in zip(positions, positions[1:])), 'R-d.schedule', 'call positions increase') + times = {} + for key, (lo, hi) in windows.items(): + times[key] = list(range(bisect.bisect_right(positions, lo), bisect.bisect_left(positions, hi))) + return dict(stage_pair=stage_pair, rank=rank, windows=windows, callpos=positions, child_pair=child_pair, + child_side=child_side, window_times=times, bridges=bridges, events=len(events), + rankless_children=sorted(rankless)) + + +def check_static(ctx, sched): + """Order, dispatch, (optionally) PLAN per-call widths, and X1 (PLAN windows == rebuilt windows).""" + T, order, plan = ctx['T'], ctx['order'], ctx['plan'] + need(len(order) == STAGES * T and set(order) == {(s, r) for s in range(STAGES) for r in range(T)}, + 'R-0.order', 'call inventory') + need(plan['order'] == [list(x) for x in order], 'R-0.order', 'PLAN order') + need(set(ctx['dispatch']) == set(order), 'R-0.dispatch', 'dispatch inventory') + need(len(plan['provider_calls']) == len(order), 'R-0.dispatch', 'PLAN call records') + for t, (s, r) in enumerate(order): + pc = plan['provider_calls'][t] + need((pc['stage'], pc['replica']) == (s, r) and pc.get('time', t) == t and + pc['provider'] == ctx['dispatch'][s, r], 'R-0.dispatch', 'PLAN provider call %d' % t) + if ctx['plan_widths']: + pw = plan['per_call_widths'][t] + need((pw['stage'], pw['replica']) == (s, r) and pw.get('time', t) == t, 'R-0.widths', 'PLAN width call %d' % t) + need(pw['widths'] == ctx['widths'][ctx['dispatch'][s, r]], 'R-0.widths', 'PLAN per-call widths at %d' % t) + pw = plan['windows'] + need(len(pw) == len(sched['windows']), 'R-d.plan_windows', 'window count') + for (r, c), times in sched['window_times'].items(): + key = '%d,%d' % (r, c) + need(key in pw and pw[key] == [sched['rank'][c], times], 'R-d.plan_windows', 'PLAN window ' + key) + + +def check_roles(ctx, sched, rows): + """R-a, R-e, R-d, R-b on the literal roles and the R-c recount (no claim is read here).""" + T, R, W, order = ctx['T'], ctx['R'], ctx['W'], ctx['order'] + at = {key: t for t, key in enumerate(order)} + provider = [ctx['dispatch'][key] for key in order] + # ---- R-a: one role per (call, live helper) at the helper's width + need(len(rows) == len(order) * R, 'R-a.count', '%d roles, expected %d calls x %d helpers' % (len(rows), len(order), R)) + have = [0] * len(order) + seen_helper = set() + for z in rows: + need(type(z) is dict and tuple(sorted(z)) == ROLE_KEYS and all(type(z[k]) is int for k in ROLE_KEYS), + 'R-a.schema', 'role fields') + t = at.get((z['stage'], z['replica'])) + need(t is not None and z['time'] == t, 'R-a.call', 'role call/time') + need(0 <= z['helper'] < R, 'R-a.helper_range', 'helper index') + key = (t, z['helper']) + need(key not in seen_helper, 'R-a.duplicate_helper', 'helper %d twice in call %d' % (z['helper'], t)) + seen_helper.add(key) + need(z['width'] == ctx['widths'][provider[t]][z['helper']], 'R-a.width', 'width of helper %d in call %d' % (z['helper'], t)) + have[t] += 1 + need(all(n == R for n in have), 'R-a.complete', 'per-call helper inventory') + # ---- R-e: physical family identity, namespace, active pair, one helper per family per call + rank, pair, side, stage_pair = sched['rank'], sched['child_pair'], sched['child_side'], sched['stage_pair'] + seen_family = set() + cross = 0 + for z in rows: + need(0 <= z['owner_replica'] < T and z['child'] in rank and 0 <= z['port'] < V, 'R-e.coords', 'owner coordinates') + need(0 <= z['family'] < W, 'R-e.namespace', 'family %d outside data namespace [0,%d)' % (z['family'], W)) + expect = z['owner_replica'] * FAMILIES_PER_REPLICA + (2 * pair[z['child']] + side[z['child']]) * V + z['port'] + need(z['family'] == expect and z['copy'] == V * z['owner_replica'] + z['port'], 'R-e.family_identity', + 'family/copy identity') + need(not (z['owner_replica'] == z['replica'] and pair[z['child']] == stage_pair[z['stage']]), + 'R-e.active_pair', 'helper hosted on the caller active pair') + key = (z['time'], z['family']) + need(key not in seen_family, 'R-e.family_unique_per_call', 'two helpers on family %d in call %d' % key[::-1]) + seen_family.add(key) + cross += z['owner_replica'] != z['replica'] + # ---- R-d: strictly inside the owner's actual (bridge-aware) window + callpos, windows = sched['callpos'], sched['windows'] + for z in rows: + lo, hi = windows[z['owner_replica'], z['child']] + need(lo < callpos[z['time']] < hi, 'R-d.window', 'role outside window of owner %d child %d' % (z['owner_replica'], z['child'])) + # ---- R-b: capacity, disjoint slices per bin, occupied prefix + used = {} + for z in rows: + need(z['offset'] >= 0 and z['width'] >= 1 and z['offset'] + z['width'] <= rank[z['child']], 'R-b.capacity', + 'slice outside child capacity') + b = (z['owner_replica'], z['child'], z['port']) + cells = ((1 << z['width']) - 1) << z['offset'] + old = used.get(b, 0) + need(not old & cells, 'R-b.overlap', 'overlapping slices in bin %s' % (b,)) + used[b] = old | cells + for b, cells in used.items(): + need(cells & (cells + 1) == 0, 'R-b.prefix', 'occupied cells of bin %s are not a prefix' % (b,)) + # ---- R-c: recount idle remainders and the global profile; pure identities + idle = Counter() + for (owner, child) in windows: + for port in range(V): + left = rank[child] - bin(used.get((owner, child, port), 0)).count('1') + if left: + idle[left] += 1 + local = Counter() + for p in provider: + local.update(ctx['local_profiles'][p]) + profile = local + idle + total = mass(profile) + need(M * W - total == 320 * T, 'R-c.mass', 'deficit identity m*W - mass = 320*T') + need(total == (M - 1) * W + 64 * len(order), 'R-c.mass', 'mass = (m-1)W + 64 calls') + capacity = T * V * sum(rank.values()) + hosted_width = sum(z['width'] for z in rows) + need(mass(idle) == capacity - hosted_width, 'R-c.mass', 'idle mass = capacity - hosted width') + need(total == mass(local) + capacity - hosted_width, 'R-c.mass', 'mass decomposition') + need(M * M > 2 * max(profile) ** 2, 'R-c.mass', 'halving guard m^2 > 2*maxchild^2') + family_children = {} + for z in rows: + family_children.setdefault(z['family'], set()).add(z['child']) + return dict(roles=len(rows), calls=len(order), helpers_per_call=R, bins=T * V * len(rank), + occupied_bins=len(used), cross_replica_roles=cross, idle=plain(idle), + hosted_families=len(family_children), max_hosted_family=max(family_children), + idle_remainders=sum(idle.values()), profile=plain(profile), rank_mass=total, + deficit=M * W - total, live=W, idle_capacity=capacity, hosted_width=hosted_width, + idle_mass=mass(idle), local_mass=mass(local), max_child=max(profile), + provider_counts=dict(Counter(provider))) + + +def compare_claims(ctx, rec): + """Compare the recount with the claims (only after the recount).""" + claims = ctx['claims'] + idle = as_profile(rec['idle'], 'R-c.idle', 'recount') + profile = as_profile(rec['profile'], 'R-c.profile', 'recount') + for source, claimed in claims['idle']: + need(idle == claimed, 'R-c.idle', 'recounted idle %s differs from %s %s' % (rec['idle'], source, plain(claimed))) + for source, claimed in claims['profile']: + need(profile == claimed, 'R-c.profile', 'recounted global profile differs from ' + source) + for key, source, value in claims.get('scalars', []): + need(rec[key] == value, 'R-c.counts', '%s %r differs from %s %r' % (key, rec[key], source, value)) + + +def run_pipeline(ctx, sched, rows): + check_static(ctx, sched) + rec = check_roles(ctx, sched, rows) + compare_claims(ctx, rec) + return rec + + +def dispatch_map(records, check): + out = {} + for s, r, p in records: + need((s, r) not in out, check, 'duplicate dispatch') + out[s, r] = p + return out + + +# ------------------------------------------------------------ case setup --- + +def template_2269(blobs): + plan = parse(blobs, 'new/PLAN.json') + spec = parse(blobs, 'new/SPEC.json') + template = parse(blobs, 'GLOBAL-TEMPLATE.json.gz') + order = [tuple(x) for x in parse(blobs, 'ORDER.json')] + dispatch = dispatch_map(parse(blobs, 'DISPATCH.json'), 'R-0.dispatch') + construction = parse(blobs, 'CONSTRUCTION.json') + T = plan['T'] + need(T == 74 and (plan['K'], plan['L'], plan['M']) == (PAIRS, STAGES, M), 'R-0.plan', 'PLAN geometry') + need(order == [tuple(x) for x in plan['order']] == [tuple(x) for x in spec['call_order']], 'R-0.order', + 'ORDER.json = PLAN order = SPEC call_order') + need(dispatch == dispatch_map(spec['dispatch'], 'R-0.dispatch'), 'R-0.dispatch', 'DISPATCH.json = SPEC dispatch') + need(Counter(dispatch.values()) == Counter({'gauge44': 249, 'extra': 417}) == + Counter(construction['dispatch']), 'R-0.dispatch', 'provider call counts 249 gauge44 + 417 extra') + need(spec['expected']['live'] == plan['live'] == FAMILIES_PER_REPLICA * T, 'R-0.plan', 'live data families') + return dict(T=T, plan=plan, spec=spec, template=template, order=order, dispatch=dispatch, construction=construction) + + +def context(name, tpl, helpers, widths, local_profiles, claims, plan_widths): + return dict(name=name, T=tpl['T'], R=helpers, W=FAMILIES_PER_REPLICA * tpl['T'], order=tpl['order'], + dispatch=tpl['dispatch'], widths=widths, local_profiles=local_profiles, plan=tpl['plan'], + claims=claims, plan_widths=plan_widths) + + +def words_80(b2339): + out = {} + for pid, tag in (('gauge44', 'base'), ('extra', 'extra')): + out[pid] = load_word(b2339, 'words/BORROW-WORD-80%s.json.gz' % tag, 'receipts/AUDIT-80%s.json' % tag, + '80' + tag, 80, CLAIMS_80['local'][pid], CLAIMS_80['inventory']) + need(len(out[pid]['live']) == 400 and len(out[pid]['buffers']) == CLAIMS_80['zero_buffers'], 'R-a.word', + pid + ' 400 live helpers / 44 zero buffers') + need(out[pid]['local_mass'] == 1856 + out[pid]['width_sum'], 'R-c.local', pid + ' local mass = 1856 + widths') + need(out['gauge44']['live'] == out['extra']['live'] and out['gauge44']['widths'] == out['extra']['widths'], + 'R-a.word', 'helper map is provider independent (same live registers and ordered widths)') + need(out['gauge44']['removed'] == out['extra']['removed'], 'R-a.word', 'both words remove the same registers') + return out + + +def load_owners80(): + path = os.path.join(HERE, OWNERS_80[0]) + with open(path, 'rb') as handle: + raw = handle.read() + need(hashlib.sha256(raw).hexdigest() == OWNERS_80[1], 'input.pin', 'sha256 of ' + OWNERS_80[0]) + return json.loads(gzip.decompress(raw).decode('utf-8')), raw + + +def claim_files_80(): + """PROFILE-80.json and BUILD-RECEIPT.json (builder outputs): claims only, compared after the recount.""" + out, record = {}, {} + for name in ('PROFILE-80.json', 'BUILD-RECEIPT.json'): + path = os.path.join(HERE, name) + if os.path.isfile(path): + with open(path, 'rb') as handle: + data = handle.read() + out[name] = json.loads(data.decode('utf-8')) + record[name] = hashlib.sha256(data).hexdigest() + return out, record + + +def case_80(repo, force_inputs): + b2269, rec2269 = read_pinned(repo, HEAD_2269, PKG_2269, PINS_2269, 'PR2269') + b2339, rec2339, mode = read_2339(repo, force_inputs) + tpl = template_2269(b2269) + words = words_80(b2339) + rows, raw = load_owners80() + files, file_record = claim_files_80() + claims = dict(idle=[('build report (hard-coded)', Counter(CLAIMS_80['idle']))], + profile=[('build report (hard-coded)', Counter(CLAIMS_80['profile']))], + scalars=[('roles', 'build report', CLAIMS_80['roles']), + ('cross_replica_roles', 'build report', CLAIMS_80['cross_replica']), + ('idle_remainders', 'build report', CLAIMS_80['idle_remainders'])]) + if 'PROFILE-80.json' in files: + claims['profile'].append(('PROFILE-80.json', as_profile(files['PROFILE-80.json'], 'R-c.profile', 'PROFILE-80'))) + if 'BUILD-RECEIPT.json' in files: + b = files['BUILD-RECEIPT.json'] + claims['idle'].append(('BUILD-RECEIPT.json idle', as_profile(b['idle'], 'R-c.idle', 'receipt'))) + claims['profile'].append(('BUILD-RECEIPT.json profile', as_profile(b['profile'], 'R-c.profile', 'receipt'))) + claims['scalars'] += [(k, 'BUILD-RECEIPT.json', b[k]) for k in + ('roles', 'cross_replica_roles', 'idle_remainders', 'rank_mass', 'hosted_width', + 'idle_mass', 'idle_capacity')] + need(b['owners_sha256'] == OWNERS_80[1], 'R-0.pins', 'BUILD-RECEIPT owners sha256') + ctx = context('ext80-T74', tpl, 400, {p: words[p]['widths'] for p in words}, + {p: words[p]['local'] for p in words}, claims, plan_widths=False) + record = dict(rec2269) + record.update(rec2339) + record['package:' + OWNERS_80[0]] = dict(sha256=OWNERS_80[1], git_blob=blob_id(raw), bytes=len(raw)) + return ctx, rows, tpl, words, b2269, dict(inputs=record, pr2339_source=mode, claim_files_sha256=file_record) + + +def case_2269(b2269, tpl): + """Positive control: PR #2269's own 437-helper fill on the same template, PLAN widths included.""" + words = {} + for pid, tag in (('gauge44', 'base'), ('extra', 'extra')): + words[pid] = load_word(b2269, 'new/borrow/words/BORROW-WORD-43%s.json.gz' % tag, + 'new/borrow/receipts/AUDIT-43%s.json' % tag, '43' + tag, 43) + spec, construction = tpl['spec'], tpl['construction'] + exp = spec['expected'] + claims = dict(idle=[('hard-coded #2269 idle', Counter(CLAIMS_2269['idle'])), + ('CONSTRUCTION.json idle', as_profile(construction['idle'], 'R-c.idle', 'construction')), + ('new/SPEC.json idle_remainder_profile', as_profile(exp['idle_remainder_profile'], 'R-c.idle', 's'))], + profile=[('new/PROFILE.json', as_profile(parse(b2269, 'new/PROFILE.json'), 'R-c.profile', 'p')), + ('new/SPEC.json global_profile', as_profile(exp['global_profile'], 'R-c.profile', 's'))], + scalars=[('roles', 'new/SPEC.json hosted_residuals', exp['hosted_residuals']), + ('cross_replica_roles', 'new/SPEC.json', exp['cross_replica_helper_roles']), + ('idle_remainders', 'new/SPEC.json', exp['idle_remainders']), + ('rank_mass', 'new/SPEC.json', exp['rank_mass'])]) + ctx = context('pr2269-borrow43-T74', tpl, 437, {p: words[p]['widths'] for p in words}, + {p: words[p]['local'] for p in words}, claims, plan_widths=True) + return ctx, parse(b2269, 'OWNERS.json.gz'), words + + +# ------------------------------------------------------- R-f: private namespace --- + +def private_namespace(W, R, buffers, hosted_max): + """Rule as stated by PR #2322: physical = W + 8 + R + 2; centres [W, W+8), reserved tableau [W+8, W+8+R), + coefficient [P-2, P); zero buffers injected in increasing order into [W+8, W+8+NZ); NZ <= R; every hosted + family is live (< W). Returns the geometry in PR #2322's PRIVATE-NAMESPACE-INJECTION field names.""" + check = 'R-f.namespace' + NZ = len(buffers) + P = W + CENTRES + R + COEFFICIENT_WORK + need(0 < NZ <= R, check, '%d zero buffers do not fit the %d-field reserved tableau' % (NZ, R)) + zp = {z: W + CENTRES + j for j, z in enumerate(sorted(buffers))} + centres = set(range(W, W + CENTRES)) + work = {P - 2, P - 1} + aux = set(zp.values()) | centres | work + need(len(aux) == NZ + CENTRES + COEFFICIENT_WORK and min(aux) == W and max(aux) == P - 1, check, 'private names') + need(max(zp.values()) < W + CENTRES + R and not set(zp.values()) & (work | centres), check, + 'buffer fields outside the reserved tableau') + need(hosted_max < W, check, 'a hosted helper family is not a live data family') + return dict(live=W, centers=[W, W + CENTRES], reserved_tableau=[W + CENTRES, W + CENTRES + R], + coefficient=[P - 2, P], physical=P, buffer_fields=[W + CENTRES, W + CENTRES + NZ], + remaining_reserve=R - NZ, native_helpers=R, zero_buffers=NZ) + + +def stock_group(): + """The retained 73-dimensional group factor 2^(36*36) * prod_{i=1}^{36} (2^(2i) - 1).""" + g = 2 ** (36 * 36) + for i in range(1, 37): + g *= 2 ** (2 * i) - 1 + return g + + +def physical_rows(b2269, W, calls, physicals): + """Stock bits and row coefficient (iteration-3 R-f formula, re-derived against PR #2269 INDEPENDENT.json).""" + independent = parse(b2269, 'evidence/INDEPENDENT.json') + g = stock_group() + payload = 1 << (192 + (M + 1) // 2 + 2 * calls + 4).bit_length() + + def charge(physical): + bits = (g * physical).bit_length() + return dict(physical=physical, stock_bits=bits, row_coefficient=2 * bits + ROW_CONSTANTS + 2 * payload) + + ref = charge(independent['physical']) + need((ref['stock_bits'], ref['row_coefficient'], independent['charged_prefix_bits']) == + (independent['physical_stock_bits'], independent['physical_row_coefficient'], payload), + 'R-f.formula', 'stock/row formula does not reproduce PR2269 evidence/INDEPENDENT.json') + rows = {name: charge(p) for name, p in physicals.items()} + for name, row in rows.items(): + need(row['row_coefficient'] < ROW_LIMIT, 'R-f.row', name + ' row coefficient') + return dict(payload_bits=payload, row_limit=ROW_LIMIT, rows=rows, + formula_reproduces=dict(physical=independent['physical'], stock_bits=ref['stock_bits'], + row=ref['row_coefficient'])) + + +# ------------------------------------------- R-g: X2 pending axes and 73-column charts --- + +def load_phases(repo, template, port_lists): + """DATA-PHASES.json at the PR2269 commit, bound to the template's data-phase pin and to the word ports.""" + blobs, record = read_pinned(repo, HEAD_2269, PKG_PHASES, PINS_PHASES, 'PR2269 tree') + need(PINS_PHASES['DATA-PHASES.json'][1] == template['exact_data_phase_recipe_sha256'], 'R-g.phases', + 'DATA-PHASES sha256 != GLOBAL-TEMPLATE exact_data_phase_recipe_sha256') + phases = parse(blobs, 'DATA-PHASES.json') + ports = [x['q'] for x in phases['recipes']] + need(phases['ports'] == V and [x['port'] for x in phases['recipes']] == list(range(V)), 'R-g.phases', 'port records') + need(all(p == ports for p in port_lists), 'R-g.phases', 'DATA-PHASES port vectors != word ports') + return phases, ports, record + + +def owner_bases(ports): + """Orthonormal 73-column owner frame per port (PR2269 independent_core.py make_context, verbatim rule).""" + bases = [] + for q in ports: + zero = next(i for i in range(H) if not (q >> i & 1)) + correction = q ^ (1 << zero) + axes = list(range(H)) + axes[0], axes[zero] = axes[zero], axes[0] + frame = [(1 << i) ^ (correction if correction >> i & 1 else 0) for i in axes] + [1 << i for i in range(H, M)] + need(all(bin(x & y).count('1') % 2 == int(i == j) for i, x in enumerate(frame) for j, y in enumerate(frame)), + 'R-g.pending_axes', 'non-orthonormal owner basis') + bases.append(frame) + return bases + + +def pending_axes_and_charts(sched, phases, bases, rows): + """X2 (disjoint pending axes of children sharing a family) and one 73-column chart per role slice.""" + rank, pair, side = sched['rank'], sched['child_pair'], sched['child_side'] + checked = 0 + for port, frame in enumerate(bases): + used, fset = {}, set(frame) + for child in sorted(rank): + axes = [int(x) for x in phases['recipes'][port]['idle_children'][child]['orthogonal_axes']] + need(len(axes) == rank[child] == len(set(axes)) and set(axes) <= fset, 'R-g.pending_axes', + 'pending axes of child %d at port %d' % (child, port)) + fam = used.setdefault((pair[child], side[child]), set()) + need(not fam & set(axes), 'R-g.pending_axes', 'overlapping pending children on one family (X2)') + fam.update(axes) + checked += 1 + charts, cache = set(), {} + for z in rows: + key = (z['port'], z['child'], z['offset'], z['width']) + if key not in cache: + frame = bases[z['port']] + pending = [int(x) for x in phases['recipes'][z['port']]['idle_children'][z['child']]['orthogonal_axes']] + need(z['offset'] + z['width'] <= len(pending) and z['width'] <= H, 'R-g.chart', 'slice beyond pending axes') + occupied = [frame.index(x) for x in pending[z['offset']:z['offset'] + z['width']]] + spectators = [i for i in range(M) if i not in occupied][:H - z['width']] + perm = occupied + spectators + [i for i in range(M) if i not in occupied and i not in spectators] + need(len(set(occupied + spectators)) == H and sorted(perm) == list(range(M)) and + [frame[i] for i in perm[:z['width']]] == pending[z['offset']:z['offset'] + z['width']], + 'R-g.chart', 'residual/spectator permutation') + cache[key] = tuple(frame[i] for i in perm) + charts.add(cache[key]) + return dict(pending_axis_checks=checked, chart_keys=len(cache), actual_73column_charts=len(charts)) + + +# ------------------------------------------------------- negative controls --- + +def controls(ctx, sched, rows, words, b2339, phases=None, bases=None): + T, W, order = ctx['T'], ctx['W'], ctx['order'] + pair, side, stage_pair, rank = sched['child_pair'], sched['child_side'], sched['stage_pair'], sched['rank'] + by_call = {} + for i, z in enumerate(rows): + by_call.setdefault(z['time'], []).append(i) + family_index = {(z['time'], z['family']): i for i, z in enumerate(rows)} + helper_index = {(z['time'], z['helper']): i for i, z in enumerate(rows)} + out = [] + + def replaced(changes): + new = list(rows) + for i, z in changes.items(): + new[i] = z + return new + + def expect(name, expected, fn): + try: + fn() + except CheckFailure as exc: + need(exc.check == expected, 'control', name + ' rejected by ' + exc.check + ' (' + exc.detail + + '), expected ' + expected) + out.append(dict(name=name, rejected_by=exc.check, detail=exc.detail[:200])) + return + raise CheckFailure('control', 'negative control accepted: ' + name) + + def run(name, expected, mutant_rows, mutant_ctx=None): + expect(name, expected, lambda: run_pipeline(mutant_ctx or ctx, sched, mutant_rows)) + + call0 = by_call[0] + a, b = next((i, j) for i in call0 for j in call0 if i < j and rows[i]['width'] == rows[j]['width']) + run('duplicate_role (helper twice in one call)', 'R-a.duplicate_helper', + replaced({b: dict(rows[b], helper=rows[a]['helper'])})) + run('dropped_role', 'R-a.count', rows[1:]) + i = next(k for k, z in enumerate(rows) if z['width'] > 1) + run('narrowed_width', 'R-a.width', replaced({i: dict(rows[i], width=rows[i]['width'] - 1)})) + run('family_in_private_namespace', 'R-e.namespace', replaced({0: dict(rows[0], family=W + CENTRES)})) + z = rows[0] + active = stage_pair[z['stage']] + child = next(c for c in sorted(rank) if pair[c] == active) + fam = z['replica'] * FAMILIES_PER_REPLICA + (2 * active + side[child]) * V + z['port'] + run('caller_active_pair', 'R-e.active_pair', replaced({0: dict(z, owner_replica=z['replica'], child=child, offset=0, + family=fam, copy=V * z['replica'] + z['port'])})) + a, b = call0[0], call0[1] + host = {k: rows[a][k] for k in ('owner_replica', 'child', 'port', 'family', 'copy', 'offset')} + run('two_helpers_one_family', 'R-e.family_unique_per_call', replaced({b: dict(rows[b], **host)})) + # role moved outside its owner's window: swap the hosts of one helper between two calls (R-a/R-e still hold) + swap = None + for i, z in enumerate(rows): + lo, hi = sched['windows'][z['owner_replica'], z['child']] + for t2 in range(len(order) - 1, -1, -1): + if lo < sched['callpos'][t2] < hi: + continue + j = helper_index[t2, z['helper']] + y = rows[j] + s2, r2 = order[t2] + zz = dict(z, stage=s2, replica=r2, time=t2) + yy = dict(y, stage=z['stage'], replica=z['replica'], time=z['time']) + if ctx['widths'][ctx['dispatch'][s2, r2]][z['helper']] != z['width']: + continue + if ctx['widths'][ctx['dispatch'][z['stage'], z['replica']]][y['helper']] != y['width']: + continue + if family_index.get((t2, z['family']), j) != j or family_index.get((z['time'], y['family']), i) != i: + continue + if (zz['owner_replica'] == r2 and pair[zz['child']] == stage_pair[s2]) or \ + (yy['owner_replica'] == z['replica'] and pair[yy['child']] == stage_pair[z['stage']]): + continue + swap = {i: zz, j: yy} + break + if swap: + break + need(swap is not None, 'control', 'no window control could be built') + run('out_of_window_role', 'R-d.window', replaced(swap)) + bins = {} + for k, z in enumerate(rows): + bins.setdefault((z['owner_replica'], z['child'], z['port']), []).append(k) + pick = None + for bkey, members in sorted(bins.items()): + if len(members) >= 2: + members = sorted(members, key=lambda k: rows[k]['offset']) + if rows[members[0]]['offset'] + rows[members[1]]['width'] <= rank[bkey[1]]: + pick = (members[0], members[1]) + break + need(pick is not None, 'control', 'no overlap control could be built') + run('overlapping_slices', 'R-b.overlap', replaced({pick[1]: dict(rows[pick[1]], offset=rows[pick[0]]['offset'])})) + gap = None + for bkey, members in sorted(bins.items()): + last = max(members, key=lambda k: rows[k]['offset']) + if rows[last]['offset'] + rows[last]['width'] + 1 <= rank[bkey[1]]: + gap = last + break + need(gap is not None, 'control', 'no prefix control could be built') + run('gap_in_prefix', 'R-b.prefix', replaced({gap: dict(rows[gap], offset=rows[gap]['offset'] + 1)})) + over = next(k for k, z in enumerate(rows) if z['offset'] + z['width'] == rank[z['child']]) + run('slice_beyond_child_capacity', 'R-b.capacity', replaced({over: dict(rows[over], offset=rows[over]['offset'] + 1)})) + claims = dict(ctx['claims']) + src, claimed = claims['idle'][0] + tampered = Counter(claimed) + tampered[48] -= 1 + tampered[47] += 1 + claims['idle'] = [(src, +tampered)] + claims['idle'][1:] + run('tampered_idle (one 48 claimed as 47)', 'R-c.idle', rows, dict(ctx, claims=claims)) + claims = dict(ctx['claims']) + src, claimed = claims['profile'][-1] + tampered = Counter(claimed) + tampered[1] += 1 + claims['profile'] = claims['profile'][:-1] + [(src, tampered)] + run('tampered_global_profile (%s)' % src, 'R-c.profile', rows, dict(ctx, claims=claims)) + plan = dict(ctx['plan']) + windows = dict(plan['windows']) + key = next(k for k in sorted(windows) if windows[k][1]) + windows[key] = [windows[key][0], windows[key][1][:-1]] + plan['windows'] = windows + run('truncated_plan_window (X1)', 'R-d.plan_windows', rows, dict(ctx, plan=plan)) + # namespace: one more zero buffer than reserved-tableau fields + expect('zero_buffers_exceed_reserve (NZ = R + 1)', 'R-f.namespace', + lambda: private_namespace(W, ctx['R'], list(range(ctx['R'] + 1)), 0)) + # local profile: the word report claims one rank-1 child moved to rank 2 + word = parse(b2339, 'words/BORROW-WORD-80base.json.gz') + lp = dict(word['report']['local_profile']) + lp['1'] -= 1 + lp['2'] += 1 + word['report'] = dict(word['report'], local_profile=lp) + mutant = dict(b2339) + mutant['words/BORROW-WORD-80base.json.gz'] = gzip.compress(json.dumps(word).encode()) + expect('tampered_word_local_profile', 'R-c.local', + lambda: load_word(mutant, 'words/BORROW-WORD-80base.json.gz', None, '80base-mutant', 80)) + if phases is not None: + # X2: one pending axis of a child copied into another child of the same family (PR2269 control) + bad = json.loads(json.dumps(phases)) + a, b = next((a, b) for a in sorted(rank) for b in sorted(rank) + if a < b and (pair[a], side[a]) == (pair[b], side[b])) + kids = bad['recipes'][0]['idle_children'] + kids[b]['orthogonal_axes'][0] = kids[a]['orthogonal_axes'][0] + expect('cross_child_pending_axis_alias (X2)', 'R-g.pending_axes', + lambda: pending_axes_and_charts(sched, bad, bases, [])) + return out + + +# -------------------------------------------------------------------- API --- + +def recount(repo=REPO_DEFAULT, force_inputs=False): + """Main recount only (no controls): used by price80.py.""" + ctx, rows, tpl, words, b2269, meta = case_80(repo, force_inputs) + sched = derive_schedule(ctx['T'], tpl['template'], ctx['order']) + rec = run_pipeline(ctx, sched, rows) + return dict(recount=rec, ctx=ctx, words=words, meta=meta, sched=sched, rows=rows, tpl=tpl, b2269=b2269) + + +# -------------------------------------------------------------------- main --- + +def main(): + ap = argparse.ArgumentParser(description=__doc__.split('\n')[0]) + ap.add_argument('--repo', default=REPO_DEFAULT) + ap.add_argument('--words-from-inputs', action='store_true', + help='read the PR2339 files from inputs/ even if commit bf1742ae is present') + ap.add_argument('--skip-positive-control', action='store_true') + ap.add_argument('--out', action='store_true', help='write ' + RECEIPT_NAME + ' next to this script') + args = ap.parse_args() + started = time.time() + try: + R = recount(args.repo, args.words_from_inputs) + ctx, rec, words, sched, rows = R['ctx'], R['recount'], R['words'], R['sched'], R['rows'] + print('windows: %d rebuilt from %d expanded events (%d bridges) = PR2269 new/PLAN.json windows (X1)' % ( + len(sched['windows']), sched['events'], sched['bridges']), flush=True) + print('R-a..R-e PASS: roles=%d = %d x %d; cross-replica %d; occupied bins %d of %d' % ( + rec['roles'], rec['calls'], rec['helpers_per_call'], rec['cross_replica_roles'], rec['occupied_bins'], + rec['bins']), flush=True) + print('R-c recount: idle=%s' % rec['idle'], flush=True) + print('R-c recount: profile=%s mass=%d deficit=%d' % (rec['profile'], rec['rank_mass'], rec['deficit']), flush=True) + # ---- R-f: private namespace (rule as PR2322 states it) + its positive control on PR2322's numbers + b2322, rec2322 = read_pinned(args.repo, HEAD_2322, PKG_2322, PINS_2322, 'PR2322') + inj = parse(b2322, 'evidence/PRIVATE-NAMESPACE-INJECTION.json') + claim2322 = parse(b2322, 'CLAIM.json') + geo2322 = private_namespace(inj['geometry']['live'], claim2322['native_helpers'], + list(range(inj['geometry']['zero_buffers'])), 0) + need(all(inj['geometry'][k] == geo2322[k] for k in geo2322), 'R-f.namespace', + 'rule does not reproduce PR2322 PRIVATE-NAMESPACE-INJECTION.json geometry') + need(words['gauge44']['buffers'] == words['extra']['buffers'], 'R-f.zero_buffers', + 'both words use the same buffer registers') + geo = private_namespace(ctx['W'], ctx['R'], words['gauge44']['buffers'], rec['max_hosted_family']) + need(geo['physical'] == 66714 and geo['buffer_fields'] == [66312, 66356] and geo['remaining_reserve'] == 356, + 'R-f.namespace', 'expected geometry 66714 = 66304 + 400 + 8 + 2') + phys = physical_rows(R['b2269'], ctx['W'], rec['calls'], + {'ext80_this_fill': geo['physical'], + 'pr2269_43alias': ctx['W'] + CENTRES + 437 + COEFFICIENT_WORK, + 'pr2322': geo2322['physical']}) + print('R-f namespace: physical %d = %d + %d + 8 + 2; centres %s, reserved tableau %s, %d zero buffers -> %s, ' + 'coefficient %s; remaining reserve %d (PR2322 rule reproduces its own geometry %d)' % ( + geo['physical'], ctx['W'], ctx['R'], geo['centers'], geo['reserved_tableau'], geo['zero_buffers'], + geo['buffer_fields'], geo['coefficient'], geo['remaining_reserve'], geo2322['physical']), flush=True) + print('R-f stock bits: %s' % {k: v['stock_bits'] for k, v in phys['rows'].items()}, flush=True) + # ---- R-g: X2 pending-axis disjointness and 73-column charts (template DATA-PHASES) + b2339, _rec, _mode = read_2339(args.repo, args.words_from_inputs) + word_ports = [parse(b2339, 'words/BORROW-WORD-80%s.json.gz' % t)['ports'] for t in ('base', 'extra')] + phases, pports, recph = load_phases(args.repo, R['tpl']['template'], word_ports) + bases = owner_bases(pports) + xg = pending_axes_and_charts(sched, phases, bases, rows) + print('R-g X2: %d (port, child) pending-axis sets disjoint per family; %d distinct 73-column charts ' + '(%d slice keys)' % (xg['pending_axis_checks'], xg['actual_73column_charts'], xg['chart_keys']), flush=True) + # ---- negative controls + rejected = controls(ctx, sched, rows, words, b2339, phases, bases) + print('negative controls rejected: %d (%s)' % (len(rejected), ', '.join( + c['name'].split(' ')[0] + '->' + c['rejected_by'] for c in rejected)), flush=True) + # ---- positive control: PR2269's own fill + presult = None + if not args.skip_positive_control: + pctx, prows, pwords = case_2269(R['b2269'], R['tpl']) + presult = run_pipeline(pctx, sched, prows) + pxg = pending_axes_and_charts(sched, phases, bases, prows) + need(pxg['actual_73column_charts'] == R['tpl']['spec']['expected']['actual_73column_sigmas'], 'R-g.chart', + 'positive control: PR2269 chart count != its SPEC actual_73column_sigmas') + presult['pending_axes_and_charts'] = pxg + print('positive control PR2269 fill: roles=%d idle=%s (PLAN per_call_widths checked); charts %d = SPEC ' + 'actual_73column_sigmas' % (presult['roles'], presult['idle'], pxg['actual_73column_charts']), + flush=True) + except CheckFailure as exc: + print('%s %s' % (FAIL_LINE, exc)) + return 1 + except Exception as exc: # malformed input: report, never pass + print('%s unexpected %s: %s' % (FAIL_LINE, type(exc).__name__, exc)) + return 1 + meta = R['meta'] + meta['inputs'].update(rec2322) + meta['inputs'].update(recph) + receipt = dict( + status=PASS_LINE, + object=dict(owners=OWNERS_80[0], sha256=OWNERS_80[1], template='PR2269 head %s %s' % (HEAD_2269, PKG_2269), + words='PR2339 commit %s %s/words' % (HEAD_2339, PKG_2339)), + inputs=meta['inputs'], pr2339_files_read_from=meta['pr2339_source'], + claim_files_sha256=meta['claim_files_sha256'], + windows=dict(rebuilt=len(sched['windows']), equal_to_pr2269_plan=True, expanded_events=sched['events'], + bridges=sched['bridges'], child_ranks={str(c): sched['rank'][c] for c in sorted(sched['rank'])}, + swept_children_without_capacity=sched['rankless_children']), + words={pid: dict(removed_registers=w['removed'], width_inventory=plain(w['inventory']), + width_per_call=w['width_sum'], local_profile_recount=plain(w['local']), + local_mass=w['local_mass'], zero_buffers=len(w['buffers']), + buffer_registers=w['buffers'], initial_corrections=w['corrections'], warps=w['warps']) + for pid, w in words.items()}, + recount=rec, + claims_compared=dict(idle=[s for s, _ in ctx['claims']['idle']], profile=[s for s, _ in ctx['claims']['profile']], + scalars=[(k, s) for k, s, _ in ctx['claims']['scalars']], all_equal=True), + private_namespace=dict( + rule='As PR2322 states it (README "complete physical stock"; evidence/PRIVATE-NAMESPACE-INJECTION.json): ' + 'physical = W + 8 centres + R reserved tableau + 2 coefficient work; centres [W,W+8), reserved ' + 'tableau [W+8,W+8+R), coefficient [P-2,P); the NZ zero buffers (r + 704 for each hyperplane-ended ' + 'live helper r) are injected in increasing order into [W+8,W+8+NZ) and must fit (NZ <= R); all ' + 'hosted helper families are live (< W). Calls are serial and every buffer is allocated and freed ' + 'inside one call, so the same NZ fields serve every call.', + this_fill=geo, pr2322_reproduced=geo2322, stock=phys), + pending_axes_and_charts=dict( + rule='R-g: PR2269 independent_core.py check_pending_axes (X2) and the per-role 73-column chart binding, on ' + 'DATA-PHASES.json read at the PR2269 commit (sha256 = GLOBAL-TEMPLATE exact_data_phase_recipe_sha256)', + this_fill=xg), + controls_rejected=rejected, + positive_control=None if presult is None else dict( + object='PR2269 OWNERS.json.gz (437 helpers, 43-alias words) on the same template; PLAN per_call_widths ' + 'compared; claims of new/SPEC.json, CONSTRUCTION.json and new/PROFILE.json reproduced', **presult), + adaptation='For the 400-helper fill the PR2269 PLAN per_call_widths (437-helper lists) are not compared; ' + 'per-call widths come from the 80-alias words (positive control checks the PLAN widths for 437).', + not_checked=['warp algebra and exact free-operator replay of the 80-alias words (PR2339 check_ext.py)', + 'native lowering in both orientations of the 64 anticipatory initial corrections (the 43-alias ' + 'words have none) and the 37 new warps (80 lenders: 74 hosted helpers, 6 X fields)', + 'X-field lender ownership and frame-zero read lifetimes of hosted correction sources in the ' + 'whole-call map; physical lowering of the 44 zero buffers (R-f only follows PR2322 statement)', + 'native local prefix bits (needed for prefix < payload), controller emission, physical Clifford ' + 'phases, invoice; PLAN/SPEC refreeze for 400 helpers; assembly and outer ledger'], + scope='Finite recount of OWNERS-80.json.gz under the stated hosting rules on PR2269\'s unchanged template; ' + 'not a kappa claim.', + credits='PR2339 (this author); PR2269 Jeremy Kothe; PR2322 Vlado Vojdanovski; PR2312/PR2302 jeremykothe2; ' + 'PR2226 Cinna Davis; PR1319/PR1297 T74 lineage (Rohan Arun et al.); PR858 / T16 owner-audit rules. ' + 'Adapted from our iteration-3 fill_check.py/words_check.py (commit 4a2f20ea). Prepared with ' + 'substantial AI assistance (Claude Code, Anthropic); Apache-2.0.', + python=sys.version.split()[0]) + if args.out: + with open(os.path.join(HERE, RECEIPT_NAME), 'w', encoding='utf-8') as handle: + handle.write(json.dumps(receipt, indent=1, sort_keys=True) + '\n') + print('runtime_s=%.1f' % (time.time() - started)) + print('%s roles=%d idle=%s physical=%d buffers=%d/%d charts=%d controls=%d positive_control=%s' % ( + PASS_LINE, rec['roles'], json.dumps(rec['idle'], separators=(',', ':')), geo['physical'], geo['zero_buffers'], + ctx['R'], xg['actual_73column_charts'], len(rejected), 'PASS' if presult is not None else 'skipped')) + return 0 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/research/t74-2322-move-prices/vendor/pr2387/vendor/iter3/price_check.py b/research/t74-2322-move-prices/vendor/pr2387/vendor/iter3/price_check.py new file mode 100644 index 0000000000..708753e770 --- /dev/null +++ b/research/t74-2322-move-prices/vendor/pr2387/vendor/iter3/price_check.py @@ -0,0 +1,880 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent price check (task C) of PR #2269: global profile and an exact moment-root bracket. + +Object: CrocSwap/integer-mult-bounds PR #2269 (jeremykothe2), head +b479fc5567bc09ab9185bffe89b62594f36d74e5, package research/gmx-t74-borrow43/. +The package's complex saving is b = (certified native complex endpoint) - 1e-100 += 0.0016962471390584742207696... (outer/B.json). The claimed conditional kappa +(outer/OUTER-CLAIM.json) is derived from b by the inherited PR1673/PR1786 outer +ledger. + +Credit: PR2269 (jeremykothe2) for the borrow43 package, its profile, endpoints +and ledger; PR2226 (Cinna Davis / 1337isnot1337, with OpenAI Codex) for +anticipatory dirty borrowing; PR2260 (Dugongue) for concurrent application of +PR2226; the T74 lineage PR1319/PR1297 (Rohan Arun), PR1625 (mdumitrean), the +pivot-554 kernel (PR1672 lineage); the retained PR547/PR548/PR559 moment +engines and the icekylinx (Zhihao Chen) / eumemic exact-assembly and +independent-checker lineage. This file shares no code with any of them. It was +written from their written specification (package README, new/SPEC.json, +outer/RETUNED-SLACKS.md, outer/FINE-PADDING-COMPOSITION.md and the moment +formula as stated in code/assemble.py); no package code is imported or run. + +The only imported code is our own: words_check.py (task A) and fill_check.py +(task B), loaded from this directory by explicit file path. + +Prepared with substantial AI assistance (Claude Code, Anthropic); Apache-2.0. + +Usage: python3 -I -B price_check.py [--repo PATH | --blob-dir DIR] [--out [RECEIPT.json]] +--blob-dir DIR: an exported copy of the package, DIR/ +(for example `git archive research/gmx-t74-borrow43 | tar -x`, then +DIR = /research/gmx-t74-borrow43). The receipt (default +price_check.receipt.json) must be next to this script. The final stdout line +starts with PASS_T74_BORROW43_PRICE_INDEPENDENT or FAIL_T74_BORROW43_PRICE_INDEPENDENT. + +MODEL (stated precisely; also written to the receipt field "model"). + 1. Local paid profiles P_gauge44 = profile of BORROW-WORD-43base and + P_extra = profile of BORROW-WORD-43extra, recounted by words_check.frame_check + (nested frame climbs + COPY charges; warps checked by words_check.check_all_warps). + 2. Idle remainders: recounted by the fill_check pipeline from OWNERS.json.gz + (rank minus occupied cells for every (owner replica, child, port) bin). + 3. Composition (new/SPEC.json expected.global_profile; code/assemble.py sums the + dispatched providers' paid profiles over the 666 calls and adds the idle + remainders): H = sum over calls of P_dispatch(call) + idle + = 249 P_gauge44 + 417 P_extra + idle, with the counts taken from DISPATCH.json. + 4. Moment (m = 73, W = 66304 live data families): + mu(a) = sum_r n_r (r/m)^(1-a) / W = sum_r n_r r/(m W) exp(a log(m/r)). + Native complex side (evidence/ASSEMBLY.json surcharge_model complex = false; + code/assemble.py checks complex_lower with surcharge off): no surcharge. + This is the side of new/SPEC.json complex_lower and of outer/B.json b. + Conservative complex side (surcharge on): mu(a) + 32 m N m^a / (10^16 W), + N = sum_r n_r (number of children). It prices conservative_complex_lower. + Every rank satisfies 0 < r < m, so each term is strictly increasing in a; + the root rho is the unique a > 0 with mu(a) = 1 (mu(0) = mass/(mW) < 1). + 'accept a' means mu(a) < 1 is certified; 'reject a' means mu(a) > 1 is certified. + 5. Certified evaluation (exact integers on the grid 2^-PREC, PREC = 800 bits, + every rounding directed): log x = k log 2 + 2 atanh(z) with 2^k <= x < 2^(k+1), + z = (x - 2^k)/(x + 2^k) in [0, 1/3), log 2 = 2 atanh(1/3); atanh(z) by its + positive series plus the remainder bound z^(2N+1)/((2N+1)(1-z^2)); exp(x) for + 0 <= x < 1 by its positive Taylor series (lower: truncated sum) plus the + remainder bound x^N/N! (N+1)/(N+1-x) (upper). mu(a) is then enclosed by an + exact rational interval; comparisons with 1 are exact. Self-tests: log 2 by a + second formula (18 atanh(1/26) - 2 atanh(1/4801) + 8 atanh(1/8749)), log(m/r) + against log m - log r, and exp(log 2) must enclose 2. + 6. Root bracket: bisection on the decimal grid 10^-130 starting from [0, 1/100], + using only certified accept/reject decisions; it does not use any claimed value. +""" + +import sys + +if sys.flags.optimize: + sys.stdout.write('refusing to run under python -O\nFAIL_T74_BORROW43_PRICE_INDEPENDENT\n') + sys.exit(2) + +import argparse +import hashlib +import importlib.util +import json +import os +import subprocess +import time +from collections import Counter +from fractions import Fraction + +PASS_LINE = 'PASS_T74_BORROW43_PRICE_INDEPENDENT' +FAIL_LINE = 'FAIL_T74_BORROW43_PRICE_INDEPENDENT' +COMMIT = 'b479fc5567bc09ab9185bffe89b62594f36d74e5' +PKG = 'research/gmx-t74-borrow43/' +HERE = os.path.dirname(os.path.abspath(__file__)) +DEFAULT_REPO = os.path.dirname(os.path.dirname(HERE)) +RECEIPT_NAME = 'price_check.receipt.json' + +# package-relative path -> (git blob id, sha256 of the blob bytes); asserted at run time +PINS = { + 'PROFILE.json': ('48249b94604daccf0552c0c3b2489716344f7ff2', + '7012a58b4078d41e3b4412204d7dfdf9eb401bfe7da5429002150bdfc3558865'), + 'new/PROFILE.json': ('3e103605dd46c8754028056eb9dde9a73b9bfdca', + '50fcc0960a47f6d35064d3b55ea6dcb4cebbd305aec215c8034f626718595538'), + 'new/SPEC.json': ('2431d1cebbb2e155356d2da160d60808498bc33d', + 'bd091ed9e7f4939d06abb467d0d2c56ce0f34ba800d74132669f7b667e125d2d'), + 'outer/B.json': ('a66501df3178012477b4c54fb6888e986b52a25e', + '631d89563be62a156c2b0119f9d4ba5a31cbf36380768bf8748825cf361bb525'), + 'outer/OUTER-CLAIM.json': ('f1feaefc27028e590fa7992d273c137897b379eb', + 'ffa05de3c8d7cb7de0114d25df7250909581f4a2c0ce68c8d20eb821bf67f0e5'), + 'outer/LEDGER.json': ('3644673ab40b7b3595e94bbb7e118924a1cc48a1', + 'eab3f0cbd5b5c45c76cee3e2daefd73c994bf7cfa80be118c67e6fab6106a05b'), + 'README.md': ('b555bc54dc661658e4d5fcbc5e3bd6503d7af4bd', + '2bf8d14e32ea03c614107eccfcce2422287a3a0552ab90f926b464d55767afcf'), + 'CLAIM.json': ('214e02514d2aba5c3977dae6285bf925c685db3e', + 'bbcb4b72c86e4ca668256f8bfa6e35c1830a6e0edd77b7ab6230d8a3a7d7d31e'), + 'evidence/ASSEMBLY.json': ('6e9debfd552d18846fe55e4cbe6c59a37447b035', + '5d9eb1ce551386024b5b6894836f81ed03a83d2e0c0bd0e02e3f6410a596bb2c'), + 'PRICE.json': ('c41b950145014912b2b2d176cb4972408c95e23e', + 'c5ec535fd9edbdec7b64edd5a8b862edb1a7f173d411dacb279172659573e16a'), +} + +# Claims under test, written here from the README / scout notes (not read from the files). +CLAIMS = dict( + local={'gauge44': {1: 2351, 2: 501, 3: 414, 4: 129, 5: 42, 8: 8}, + 'extra': {1: 2339, 2: 509, 3: 418, 4: 125, 5: 42, 8: 8}}, + local_mass=5385, + counts={'gauge44': 249, 'extra': 417}, + idle={1: 23976, 3: 8673, 5: 813, 7: 150, 48: 24479}, + mass=4816512, m=73, W=66304, T=74, calls=666, max_child=48, + b_decimal_prefix='0.0016962471390584742207696', +) +WORD_OF = {'gauge44': 'base', 'extra': 'extra'} # provider id -> BORROW-WORD-43 + +ONE_Q = Fraction(1) + + +class Reject(Exception): + def __init__(self, check, msg): + Exception.__init__(self, '[%s] %s' % (check, msg)) + self.check = check + self.msg = msg + + +def need(cond, check, msg): + if not cond: + raise Reject(check, msg) + + +# ---------------------------------------------------------------------------- +# Inputs +# ---------------------------------------------------------------------------- + +def git_blob_id(data): + h = hashlib.sha1() + h.update(b'blob %d\0' % len(data)) + h.update(data) + return h.hexdigest() + + +def verify_pin(rel, data): + blob, sha = PINS[rel] + need(git_blob_id(data) == blob, 'pin', 'git blob id mismatch for ' + rel) + need(hashlib.sha256(data).hexdigest() == sha, 'pin', 'sha256 mismatch for ' + rel) + + +def read_inputs(repo, blob_dir): + raw, record = {}, {} + for rel in sorted(PINS): + blob, sha = PINS[rel] + if blob_dir is None: + got = subprocess.run(['git', '-C', repo, 'rev-parse', '--verify', COMMIT + ':' + PKG + rel], + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + need(got.returncode == 0, 'pin', 'cannot resolve %s at %s in %s' % (PKG + rel, COMMIT, repo)) + need(got.stdout.decode().strip() == blob, 'pin', PKG + rel + ' does not resolve to the pinned blob') + got = subprocess.run(['git', '-C', repo, 'cat-file', 'blob', blob], + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + need(got.returncode == 0, 'pin', 'cannot read blob ' + blob) + data = got.stdout + else: + src = os.path.join(blob_dir, rel) + need(os.path.isfile(src), 'pin', 'exported blob missing: ' + src) + with open(src, 'rb') as fh: + data = fh.read() + verify_pin(rel, data) + raw[rel] = data + record[PKG + rel] = dict(git_blob=blob, sha256=sha, bytes=len(data)) + return raw, record + + +def as_json(raw, rel): + return json.loads(raw[rel].decode('utf-8')) + + +def load_sibling(name): + """Load our own task A/B module from this directory by explicit path (python -I drops the script dir).""" + path = os.path.join(HERE, name + '.py') + spec = importlib.util.spec_from_file_location('t74b43_' + name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + with open(path, 'rb') as fh: + digest = hashlib.sha256(fh.read()).hexdigest() + return mod, digest + + +def int_profile(mapping, check, what): + out = {} + for k, v in mapping.items(): + need(type(v) is int and v > 0 and str(int(k)) == str(k), check, what + ': bad profile entry') + out[int(k)] = v + return out + + +def plain(prof): + return dict((str(r), prof[r]) for r in sorted(prof) if prof[r]) + + +def mass_of(prof): + return sum(r * n for r, n in prof.items()) + + +# ---------------------------------------------------------------------------- +# Certified rational enclosures (integers on the grid 2^-PREC, directed rounding) +# ---------------------------------------------------------------------------- + +PREC = 800 +ONE = 1 << PREC +MAX_TERMS = 4 * PREC + + +def cdiv(a, b): + """ceil(a / b) for integers, b > 0.""" + return -((-a) // b) + + +def atanh_enclosure(p, q, terms=None, tail=True): + """Integers (lo, hi) with lo <= 2^PREC atanh(p/q) <= hi, for 0 <= p/q <= 1/3. + atanh(z) = sum_j z^(2j+1)/(2j+1) (positive terms). Lower: floored partial sum. + Upper: ceiled partial sum of N terms + z^(2N+1)/((2N+1)(1-z^2)) >= the remainder. + terms/tail exist only for the negative controls (fixed truncation, remainder dropped).""" + need(q > 0 and 0 <= 3 * p <= q, 'evaluator', 'atanh argument outside [0, 1/3]') + if p == 0: + return 0, 0 + p2, q2 = p * p, q * q + pl, pu = (ONE * p) // q, cdiv(ONE * p, q) # bounds of 2^PREC z^(2j+1), j = 0 + sl = su = 0 + j = 0 + while (pl > 0) if terms is None else (j < terms): + need(j < MAX_TERMS, 'evaluator', 'atanh series did not terminate') + sl += pl // (2 * j + 1) + su += cdiv(pu, 2 * j + 1) + pl = (pl * p2) // q2 + pu = cdiv(pu * p2, q2) + j += 1 + if tail: # pu >= 2^PREC z^(2j+1): remainder <= pu / ((2j+1)(1 - z^2)) = pu q^2 / ((2j+1)(q^2 - p^2)) + su += cdiv(pu * q2, (2 * j + 1) * (q2 - p2)) + return sl, su + + +_LOG2 = [] + + +def log2_enclosure(): + if not _LOG2: + lo, hi = atanh_enclosure(1, 3) + _LOG2.append((2 * lo, 2 * hi)) + return _LOG2[0] + + +def log_enclosure(p, q): + """Integers (lo, hi) enclosing 2^PREC log(p/q) for p/q >= 1.""" + need(p >= q > 0, 'evaluator', 'log argument below 1') + k = (p // q).bit_length() - 1 # 2^k <= p/q < 2^(k+1) + a, b = p, q << k # y = a/b in [1, 2) + zl, zu = atanh_enclosure(a - b, a + b) + l2l, l2u = log2_enclosure() + return k * l2l + 2 * zl, k * l2u + 2 * zu + + +def exp_enclosure(xl, xu, terms=None, tail=True): + """Integers (lo, hi) with lo <= 2^PREC exp(x) <= hi for every x in [xl, xu] / 2^PREC, 0 <= xl <= xu < 2^PREC. + Lower: floored Taylor partial sum at xl (positive terms). Upper: ceiled partial sum at xu of N terms plus + t_N (N+1)/(N+1-x) with t_N >= 2^PREC x^N/N!, which bounds sum_{i>=N} x^i/i! for 0 <= x < N+1. + terms/tail exist only for the negative controls (fixed truncation of both sums, remainder dropped).""" + need(0 <= xl <= xu < ONE, 'evaluator', 'exp argument outside [0, 1)') + t = s = ONE + j = 1 + while (t > 0) if terms is None else (j < terms): + need(j < MAX_TERMS, 'evaluator', 'exp series did not terminate') + t = ((t * xl) >> PREC) // j + s += t + j += 1 + lo = s + t = s = ONE + j = 1 + while True: + need(j < MAX_TERMS, 'evaluator', 'exp series did not terminate') + t = cdiv(cdiv(t * xu, ONE), j) # >= 2^PREC x^j / j! + if (t <= 1) if terms is None else (j >= terms): + break + s += t + j += 1 + if tail: + s += cdiv(t * (j + 1) * ONE, (j + 1) * ONE - xu) + return lo, s + + +class Evaluator(object): + """mu(a) enclosures for one profile; logs are computed once per rank.""" + + def __init__(self, profile, m, W, surcharge=False): + need(all(type(r) is int and 0 < r < m and type(n) is int and n > 0 for r, n in profile.items()), + 'moment', 'every child must have 0 < rank < m') + self.profile = dict(profile) + self.m, self.W, self.surcharge = m, W, surcharge + self.N = sum(profile.values()) + self.logs = dict((r, log_enclosure(m, r)) for r in sorted(profile)) + self.logm = log_enclosure(m, 1) + + def bounds(self, a): + """Exact rationals lo <= mu(a) <= hi (plus the surcharge if enabled).""" + a = Fraction(a) + need(a >= 0, 'moment', 'negative saving') + an, ad = a.numerator, a.denominator + slo = shi = 0 + for r in sorted(self.profile): + ll, lu = self.logs[r] + el, eu = exp_enclosure((an * ll) // ad, cdiv(an * lu, ad)) + n = self.profile[r] + slo += n * r * el + shi += n * r * eu + lo = Fraction(slo, self.m * self.W * ONE) + hi = Fraction(shi, self.m * self.W * ONE) + if self.surcharge: + ll, lu = self.logm + el, eu = exp_enclosure((an * ll) // ad, cdiv(an * lu, ad)) + c = 32 * self.m * self.N + lo += Fraction(c * el, 10 ** 16 * self.W * ONE) + hi += Fraction(c * eu, 10 ** 16 * self.W * ONE) + need(lo <= hi, 'evaluator', 'empty enclosure') + return lo, hi + + def side(self, a): + lo, hi = self.bounds(a) + if hi < 1: + return -1 + if lo > 1: + return 1 + return 0 + + def root_bracket(self, digits): + """Bisection on the 10^-digits grid from [0, 1/100] with certified decisions only.""" + scale = 10 ** digits + lo, hi = 0, scale // 100 + need(self.side(Fraction(lo, scale)) < 0, 'moment', 'mu(0) >= 1: no positive saving') + need(self.side(Fraction(hi, scale)) > 0, 'moment', 'mu(1/100) <= 1') + steps, undecided = 0, None + while hi - lo > 1: + mid = (lo + hi) // 2 + s = self.side(Fraction(mid, scale)) + steps += 1 + if s < 0: + lo = mid + elif s > 0: + hi = mid + else: + undecided = mid + break + return Fraction(lo, scale), Fraction(hi, scale), steps, undecided + + +# ---------------------------------------------------------------------------- +# Display helpers (display only; never used for a decision) +# ---------------------------------------------------------------------------- + +def sci(x, sig=22, up=False): + """x rounded to `sig` significant digits toward +inf (up) or -inf; display only.""" + x = Fraction(x) + if x == 0: + return '0' + neg = x < 0 + ax = -x if neg else x + e = len(str(ax.numerator)) - len(str(ax.denominator)) + while ax < Fraction(10) ** e: + e -= 1 + while ax >= Fraction(10) ** (e + 1): + e += 1 + y = ax * Fraction(10) ** (sig - 1 - e) + toward_larger_magnitude = (up and not neg) or (neg and not up) + k = cdiv(y.numerator, y.denominator) if toward_larger_magnitude else y.numerator // y.denominator + ds = str(k) + e += len(ds) - sig + return '%s%s.%sE%+d' % ('-' if neg else '', ds[0], ds[1:sig], e) + + +def dec(x, digits): + """Exact decimal string of a rational with denominator dividing 10^digits.""" + x = Fraction(x) + y = x * 10 ** digits + need(y.denominator == 1, 'display', 'not on the decimal grid') + n = y.numerator + s = str(abs(n)).rjust(digits + 1, '0') + return ('-' if n < 0 else '') + s[:-digits] + '.' + s[-digits:] + + +def interval(lo, hi): + return [sci(lo, up=False), sci(hi, up=True)] + + +# ---------------------------------------------------------------------------- +# Composition +# ---------------------------------------------------------------------------- + +def compose(local, counts, idle): + H = Counter() + for pid in sorted(counts): + for r, n in local[pid].items(): + H[r] += counts[pid] * n + for r, n in idle.items(): + H[r] += n + return dict((r, H[r]) for r in sorted(H) if H[r]) + + +def check_composition(H, sources): + for name, prof in sources: + need(H == prof, 'compose.profile', 'composed profile %s != %s %s' % (plain(H), name, plain(prof))) + + +def check_mass(H, m, W, T, calls, deficit_claim): + mass = mass_of(H) + need(W == 896 * T, 'compose.mass', 'W != 896 T (live data families)') + need(calls == 9 * T, 'compose.mass', 'calls != 9 T') + need(m * W - mass == deficit_claim == 320 * T, 'compose.mass', 'deficit m W - mass != 320 T') + need(mass == (m - 1) * W + 64 * calls, 'compose.mass', 'mass != (m-1) W + 64 calls') + need(m * m > 2 * max(H) ** 2, 'compose.mass', 'halving guard m^2 > 2 maxchild^2') + return mass + + +# ---------------------------------------------------------------------------- +# Negative-control harness +# ---------------------------------------------------------------------------- + +def expect_reject(name, target, fn, results): + try: + detail = fn() + except Reject as e: + ok = e.check == target + results.append(dict(name=name, target=target, rejected_by=e.check, ok=ok, detail=e.msg[:300])) + return ok + results.append(dict(name=name, target=target, rejected_by=None, ok=False, detail=str(detail)[:300])) + return False + + +def require_accept(ev, a, what): + lo, hi = ev.bounds(a) + need(hi < 1, 'moment.accept', '%s: mu - 1 in %s is not certified < 0' % (what, interval(lo - 1, hi - 1))) + return lo, hi + + +def require_reject(ev, a, what): + lo, hi = ev.bounds(a) + need(lo > 1, 'moment.reject', '%s: mu - 1 in %s is not certified > 0' % (what, interval(lo - 1, hi - 1))) + return lo, hi + + +# ---------------------------------------------------------------------------- +# Main +# ---------------------------------------------------------------------------- + +def run(args, receipt): + t0 = time.time() + raw, record = read_inputs(args.repo, args.blob_dir) + receipt['pins'] = record + print('pins: %d package blobs verified (sha256 + git blob id)' % len(record), flush=True) + W_mod, w_sha = load_sibling('words_check') + F_mod, f_sha = load_sibling('fill_check') + receipt['imported_own_modules'] = {'words_check.py': w_sha, 'fill_check.py': f_sha} + + # ---- 1. local profiles recounted by task A code + js, wpins, _ = W_mod.load_inputs(args.repo, args.blob_dir) + local, local_mass, canon, word_widths = {}, {}, {}, {} + for pid in ('gauge44', 'extra'): + tag = WORD_OF[pid] + P = W_mod.parse_borrow(js['word_' + tag]) + W_mod.check_all_warps(P) + fr = W_mod.frame_check(P) + local[pid] = dict((r, n) for r, n in sorted(fr['paid'].items()) if n) + need(dict((r, n) for r, n in fr['copies'].items() if n) == {8: 8} and not fr['climbs'].get(8), 'local', + pid + ': the rank-8 entries must be exactly the 8 COPY children') + local_mass[pid] = fr['mass'] + word_widths[pid] = list(fr['widths']) + C = W_mod.parse_canonical(js['canon_' + tag]) + frC = W_mod.frame_check(C) + canon[pid] = dict((r, n) for r, n in sorted(frC['paid'].items()) if n) + need(local[pid] == CLAIMS['local'][pid], 'local', '%s recount %s != claimed %s' % ( + pid, plain(local[pid]), plain(CLAIMS['local'][pid]))) + need(local_mass[pid] == mass_of(local[pid]) == CLAIMS['local_mass'], 'local', pid + ' local mass') + print('local profiles (words_check recount): gauge44 %s extra %s, mass %d each' % ( + plain(local['gauge44']), plain(local['extra']), CLAIMS['local_mass']), flush=True) + + # ---- 2. idle remainders recounted by task B code + try: + fblobs, frecord = F_mod.load_blobs(args.repo, args.blob_dir) + ctx, rows, helpers_info, extra = F_mod.borrow_case(fblobs) + sched = F_mod.derive_schedule(ctx) + fres = F_mod.run_pipeline(ctx, sched, rows) + except F_mod.CheckFailure as e: + raise Reject('fill', 'fill_check pipeline failed: ' + str(e)) + idle = dict((int(r), n) for r, n in fres['idle'].items()) + counts = dict(Counter(ctx['dispatch'].values())) + T, W, calls = ctx['T'], fres['live'], fres['calls'] + need(idle == CLAIMS['idle'], 'idle', 'recounted idle %s != claimed %s' % (plain(idle), plain(CLAIMS['idle']))) + need(counts == CLAIMS['counts'] and sum(counts.values()) == calls == CLAIMS['calls'], 'dispatch', + 'provider call counts %r' % counts) + need((T, W) == (CLAIMS['T'], CLAIMS['W']), 'geometry', 'T/W') + for pid in word_widths: # cross-module consistency: both recounts see the same 437 helper widths + need(word_widths[pid] == list(ctx['widths'][pid]), 'cross', pid + ' helper widths differ between A and B') + print('idle remainders (fill_check recount): %s; dispatch %s' % (plain(idle), counts), flush=True) + + # ---- 3. composition and mass identities + spec = as_json(raw, 'new/SPEC.json') + Bj = as_json(raw, 'outer/B.json') + ledger = as_json(raw, 'outer/LEDGER.json') + m = spec['geometry']['dimension'] + need(m == CLAIMS['m'] == ledger['m'], 'geometry', 'm') + need(spec['expected']['live'] == W == Bj['live'] == ledger['W'], 'geometry', 'W') + H = compose(local, counts, idle) + sources = [('PROFILE.json', int_profile(as_json(raw, 'PROFILE.json'), 'compose.profile', 'PROFILE.json')), + ('new/PROFILE.json', int_profile(as_json(raw, 'new/PROFILE.json'), 'compose.profile', 'new/PROFILE')), + ('new/SPEC.json expected.global_profile', + int_profile(spec['expected']['global_profile'], 'compose.profile', 'SPEC')), + ('outer/B.json profile', int_profile(Bj['profile'], 'compose.profile', 'B.json')), + ('outer/LEDGER.json profile', int_profile(ledger['profile'], 'compose.profile', 'LEDGER'))] + check_composition(H, sources) + deficit = 320 * T + mass = check_mass(H, m, W, T, calls, m * W - spec['expected']['rank_mass']) + need(mass == CLAIMS['mass'] == spec['expected']['rank_mass'], 'compose.mass', 'rank mass') + need(max(H) == CLAIMS['max_child'], 'compose.mass', 'max child') + need(H.get(8, 0) == 8 * calls and 8 not in idle and all(local[p].get(8) == 8 for p in local), 'compose.mass', + 'rank-8 children are exactly the 8 COPY children of each call') + receipt['composition'] = dict( + rule='H = sum over the %d dispatched calls of P_provider + idle = %d P_gauge44 + %d P_extra + idle' % ( + calls, counts['gauge44'], counts['extra']), + local_profiles=dict((p, plain(local[p])) for p in sorted(local)), local_mass=CLAIMS['local_mass'], + provider_counts=counts, idle=plain(idle), global_profile=plain(H), children=sum(H.values()), + equal_to=[s for s, _ in sources], mass=mass, live_W=W, m=m, T=T, calls=calls, deficit=deficit, + identities=['mass = m W - D = 73*66304 - 23680 = %d, D = 320 T' % mass, + 'mass = (m-1) W + 64 calls = 72*66304 + 64*666 = %d; the second term 42624 = W - D = 576 T ' + 'equals the mass of the 5328 = 8*666 rank-8 children, which are exactly the 8 COPY children ' + '(rank 8) of each call: mass - (COPY mass) = (m-1) W' % mass, + 'local: 666*5385 = %d; idle mass = %d' % (calls * CLAIMS['local_mass'], mass_of(idle)), + 'halving guard 73^2 = 5329 > 2*48^2 = 4608']) + print('composition: %s = PROFILE.json = new/PROFILE.json = SPEC = B.json = LEDGER; mass %d = 72W + 64*666' % ( + plain(H), mass), flush=True) + + # ---- 4. evaluator self-tests + l2 = log2_enclosure() + a1, a2, a3 = atanh_enclosure(1, 26), atanh_enclosure(1, 4801), atanh_enclosure(1, 8749) + l2b = (18 * a1[0] - 2 * a2[1] + 8 * a3[0], 18 * a1[1] - 2 * a2[0] + 8 * a3[1]) + + def log2_crosscheck(first, second): + need(max(first[0], second[0]) <= min(first[1], second[1]), 'evaluator.log2_crosscheck', + 'two enclosures of log 2 are disjoint') + return 'overlap' + + log2_crosscheck(l2, l2b) + need(l2[1] - l2[0] < 2 ** 12 and l2b[1] - l2b[0] < 2 ** 12, 'evaluator', 'log 2 enclosure too wide') + + def exp_log2_check(e): + need(e[0] <= 2 * ONE <= e[1], 'evaluator.exp_log2', 'exp(log 2) enclosure %s misses 2' % ( + interval(Fraction(e[0], ONE), Fraction(e[1], ONE)),)) + return 'contains 2' + + exp_log2_check(exp_enclosure(l2[0], l2[1])) + ranks = sorted(set(H) | {47}) + for r in ranks: + direct = log_enclosure(m, r) + lm, lr = log_enclosure(m, 1), log_enclosure(r, 1) + diff = (lm[0] - lr[1], lm[1] - lr[0]) + need(max(direct[0], diff[0]) <= min(direct[1], diff[1]), 'evaluator.log_crosscheck', + 'log(m/%d) disagrees with log m - log %d' % (r, r)) + need(direct[1] - direct[0] < 2 ** 16, 'evaluator', 'log enclosure too wide') + receipt['evaluator'] = dict( + grid_bits=PREC, log2=interval(Fraction(l2[0], ONE), Fraction(l2[1], ONE)), + log2_width_ulps=l2[1] - l2[0], + self_tests=['log 2 = 2 atanh(1/3) overlaps 18 atanh(1/26) - 2 atanh(1/4801) + 8 atanh(1/8749)', + 'exp(log 2) encloses 2', + 'log(73/r) overlaps log 73 - log r for r in %s' % ranks]) + print('evaluator: PREC=%d bits; self-tests PASS' % PREC, flush=True) + + # ---- 5. native moment: root bracket and the package endpoints + native = Evaluator(H, m, W, surcharge=False) + DIG = 130 + r_lo, r_hi, steps, undecided = native.root_bracket(DIG) + need(undecided is None and r_hi - r_lo == Fraction(1, 10 ** DIG), 'moment.bracket', 'bisection stalled') + X = spec['expected'] + complex_lower = Fraction(X['complex_lower']) + b = Fraction(Bj['b']) + b_above = Fraction(Bj['b_above_endpoint']) + + def b_identity(bb, bab): + need(bb == complex_lower - Fraction(1, 10 ** 100), 'claims.b_identity', 'b != complex_lower - 1e-100') + need(bab == complex_lower + Fraction(1, 10 ** 90), 'claims.b_identity', 'b_above != complex_lower + 1e-90') + return 'identity holds' + + b_identity(b, b_above) + need(Fraction(ledger['complex_lower_pinned']['rational']) == complex_lower and + Fraction(ledger['complex_lower_short']['rational']) == b, 'claims.b_identity', 'LEDGER endpoints') + need(dec(b, 100).startswith(CLAIMS['b_decimal_prefix']), 'claims.b_identity', 'b decimal prefix') + cl_acc = require_accept(native, complex_lower, 'complex_lower') + cl_rej = require_reject(native, complex_lower + Fraction(1, 10 ** 90), 'complex_lower + 1e-90') + b_acc = require_accept(native, b, 'b') + ba_rej = require_reject(native, b_above, 'b_above_endpoint') + coarse = Fraction((complex_lower * 10 ** 24).__floor__(), 10 ** 24) + co_acc = require_accept(native, coarse, 'coarse 1e-24 endpoint') + co_rej = require_reject(native, coarse + Fraction(1, 10 ** 24), 'coarse 1e-24 endpoint + 1e-24') + # task bracket: decimal 1e-21 cell containing b + b_lo = Fraction((b * 10 ** 21).__floor__(), 10 ** 21) + b_hi = b_lo + Fraction(1, 10 ** 21) + need(b_lo <= b <= b_hi and b_hi - b_lo <= Fraction(1, 10 ** 20), 'moment.bracket', 'task bracket shape') + tb_lo = require_accept(native, b_lo, 'b_lo') + tb_hi = require_reject(native, b_hi, 'b_hi') + # consistency of the independent root bracket with the claims (monotone mu) + need(complex_lower <= r_lo and r_hi <= complex_lower + Fraction(1, 10 ** 90), 'moment.bracket', + 'root bracket not inside (complex_lower, complex_lower + 1e-90)') + need(b_lo <= r_lo and r_hi <= b_hi, 'moment.bracket', 'root bracket not inside the task bracket') + # the package's own enclosure of mu(b) (outer/LEDGER.json native_moment) must overlap ours + led = [Fraction(v['rational']) for v in ledger['native_moment']] + need(max(led[0], b_acc[0]) <= min(led[1], b_acc[1]), 'moment.ledger', 'LEDGER native_moment(b) disjoint from ours') + gap_lo, gap_hi = r_lo - b, r_hi - b + receipt['native'] = dict( + model='mu(a) = sum_r n_r (r/73)^(1-a) / 66304, no surcharge (native complex side)', + root_bracket=[dec(r_lo, DIG), dec(r_hi, DIG)], root_bracket_width='1E-%d' % DIG, bisection_steps=steps, + complex_lower=dict(value=X['complex_lower'], accept=True, mu_minus_one=interval(cl_acc[0] - 1, cl_acc[1] - 1), + plus_1e90_reject=True, mu_minus_one_plus_1e90=interval(cl_rej[0] - 1, cl_rej[1] - 1)), + b=dict(value=Bj['b'], decimal=dec(b, 100), equals='complex_lower - 1e-100', accept=True, + mu_minus_one=interval(b_acc[0] - 1, b_acc[1] - 1), + ledger_native_moment_overlaps=True, + root_minus_b=interval(gap_lo, gap_hi)), + b_above_endpoint=dict(value=Bj['b_above_endpoint'], reject=True, + mu_minus_one=interval(ba_rej[0] - 1, ba_rej[1] - 1)), + coarse_1e24=dict(endpoint=dec(coarse, 24), accept=True, plus_1e24_reject=True), + task_bracket=dict(b_lo=dec(b_lo, 21), b_hi=dec(b_hi, 21), width='1E-21', b_lo_le_b_le_b_hi=True, + mu_minus_one_at_b_lo=interval(tb_lo[0] - 1, tb_lo[1] - 1), + mu_minus_one_at_b_hi=interval(tb_hi[0] - 1, tb_hi[1] - 1))) + print('native root in [%s, %s]' % (dec(r_lo, DIG)[:60] + '...', dec(r_hi, DIG)[:60] + '...'), flush=True) + print(' complex_lower accepted, complex_lower+1e-90 rejected; b accepted (root - b in %s); task bracket ' + '[%s, %s] PASS' % (interval(gap_lo, gap_hi), dec(b_lo, 21), dec(b_hi, 21)), flush=True) + + # ---- 6. conservative side (surcharge) and the model control of code/assemble.py + cons = Evaluator(H, m, W, surcharge=True) + c_lo, c_hi, c_steps, c_und = cons.root_bracket(DIG) + need(c_und is None, 'moment.bracket', 'conservative bisection stalled') + ccl = Fraction(X['conservative_complex_lower']) + cc_acc = require_accept(cons, ccl, 'conservative_complex_lower') + cc_rej = require_reject(cons, ccl + Fraction(1, 10 ** 90), 'conservative_complex_lower + 1e-90') + need(ccl <= c_lo and c_hi <= ccl + Fraction(1, 10 ** 90), 'moment.bracket', 'conservative bracket') + sur_b = require_reject(cons, b, 'native b under the conservative surcharge') + receipt['conservative'] = dict( + model='mu(a) + 32 m N m^a / (10^16 W), N = %d children' % sum(H.values()), + root_bracket=[dec(c_lo, DIG), dec(c_hi, DIG)], + conservative_complex_lower=dict(value=X['conservative_complex_lower'], accept=True, + mu_minus_one=interval(cc_acc[0] - 1, cc_acc[1] - 1), plus_1e90_reject=True), + native_b_rejected_with_surcharge=dict(reject=True, mu_minus_one=interval(sur_b[0] - 1, sur_b[1] - 1)), + native_minus_conservative_root=interval(r_lo - c_hi, r_hi - c_lo)) + print('conservative root in [%s...]; SPEC conservative_complex_lower accepted, +1e-90 rejected; native b ' + 'rejected under the surcharge (model control)' % dec(c_lo, DIG)[:40], flush=True) + + # ---- 7. claimed kappa as an arithmetic function of b (outer lemmas NOT checked) + oc = as_json(raw, 'outer/OUTER-CLAIM.json') + kappa = Fraction(oc['kappa_rational']) + need(Fraction(oc['kappa']) == kappa, 'claims.kappa', 'OUTER-CLAIM decimal != rational') + + def kappa_identity(kap, bb): + q = bb - Fraction(1, 10 ** 100) + eq = (1 - Fraction(2, 10 ** 100)) * q + floor136 = Fraction((eq * 10 ** 136).__floor__(), 10 ** 136) + need(kap == floor136 - Fraction(1, 10 ** 112), 'claims.kappa', + 'kappa != floor_1e-136((1-2e-100)(b-1e-100)) - 1e-112') + return 'identity holds' + + kappa_identity(kappa, b) + need(Fraction(ledger['rows']['struct_boundary_radix_union']['kappa']['rational']) == kappa, 'claims.kappa', + 'LEDGER kappa') + readme = raw['README.md'].decode('utf-8') + need(('**' + oc['kappa'] + '**') in readme, 'claims.kappa', 'README kappa string') + strict = Fraction(as_json(raw, 'CLAIM.json')['kappa']) + need(strict == Fraction(X['kappa']) == Fraction(ledger['online_final_kappa']['rational']), 'claims.kappa', + 'strict-assembly kappa') + need(0 < strict < kappa < b < r_lo, 'claims.kappa', 'ordering strict kappa < kappa < b < root') + claim = as_json(raw, 'CLAIM.json') + baseline = Fraction(claim['baseline_kappa']) + stated_gain = Fraction(claim['gain_over_claimed_leader']) + half_unit = Fraction(5, 10 ** 11) # half a unit of the 6th significant digit of 1.28346E-5 + need(abs(kappa - baseline - stated_gain) <= half_unit < abs(strict - baseline - stated_gain), 'claims.kappa', + 'CLAIM.json gain field') + doc_notes = [ + 'CLAIM.json kappa (%s...) is the strict-assembly kappa, while its gain_over_claimed_leader %s is the gain of ' + 'the outer-ledger kappa over baseline_kappa (outer: %s; strict: %s).' % ( + claim['kappa_decimal'][:22], claim['gain_over_claimed_leader'], sci(kappa - baseline, 12), + sci(strict - baseline, 12))] + receipt['kappa'] = dict( + claimed=oc['kappa'], identity='kappa = floor_1e-136((1 - 2e-100)(b - 1e-100)) - 1e-112 (exact)', + b_minus_kappa=interval(b - kappa, b - kappa), root_minus_kappa=interval(r_lo - kappa, r_hi - kappa), + strict_assembly_kappa=claim['kappa_decimal'], documentation_notes=doc_notes, + scope='arithmetic link only; the PR1673/PR1786/PR1758 outer lemmas, the bit endpoint and the 47/62 outer ' + 'inequalities are not checked here') + print('kappa: OUTER-CLAIM kappa = floor_136((1-2e-100)(b-1e-100)) - 1e-112 exactly; strict < kappa < b < root', + flush=True) + + # ---- 8. positive control: the pre-borrow assembly (evidence/ASSEMBLY.json = PRICE.json) endpoints + asm = as_json(raw, 'evidence/ASSEMBLY.json') + price = as_json(raw, 'PRICE.json') + old = int_profile(asm['complex_profile'], 'control', 'ASSEMBLY profile') + need(asm['surcharge_model'] == {'complex': False, 'bit': True}, 'control', 'surcharge model') + need(mass_of(old) == mass, 'control', 'old profile mass') + old_native, old_cons = Evaluator(old, m, W), Evaluator(old, m, W, surcharge=True) + oc_l = Fraction(asm['complex_lower']) + occ_l = Fraction(asm['conservative_complex_lower']) + need(Fraction(price['prices']['native']['root']['lower']) == oc_l and + Fraction(price['prices']['conservative']['root']['lower']) == occ_l, 'control', + 'PRICE.json and evidence/ASSEMBLY.json endpoints differ') + require_accept(old_native, oc_l, 'old complex_lower') + require_reject(old_native, oc_l + Fraction(1, 10 ** 24), 'old complex_lower + 1e-24') + require_accept(old_cons, occ_l, 'old conservative_complex_lower') + require_reject(old_cons, occ_l + Fraction(1, 10 ** 24), 'old conservative_complex_lower + 1e-24') + o_lo, o_hi, _, _ = old_native.root_bracket(40) + receipt['positive_control'] = dict( + what='stale evidence/ASSEMBLY.json profile (an older pre-borrow T74 profile, H5 = 54612 = 82*666; the ' + 'top-level PRICE.json carries the same endpoints): its certified 1e-24 native and conservative ' + 'endpoints are reproduced (accept at the endpoint, reject at +1e-24)', + profile=plain(old), native_endpoint=asm['complex_decimal'], conservative_endpoint=asm['conservative_complex_decimal'], + old_root_bracket=[dec(o_lo, 40), dec(o_hi, 40)], + root_minus_stale_assembly_root=interval(r_lo - o_hi, r_hi - o_lo)) + print('positive control: stale-assembly (older pre-borrow) endpoints %s / %s reproduced' % (asm['complex_decimal'], + asm['conservative_complex_decimal']), flush=True) + + # ---- 9. negative controls + results = [] + ok = True + ok &= expect_reject('mu at claimed b + 1e-15 must exceed 1', 'moment.accept', + lambda: require_accept(native, b + Fraction(1, 10 ** 15), 'b + 1e-15'), results) + lo15, hi15 = native.bounds(b + Fraction(1, 10 ** 15)) + need(lo15 > 1, 'moment.reject', 'mu(b + 1e-15) not certified > 1') + split = dict(H) + split[48] -= 1 + split[47] = split.get(47, 0) + 1 + split[1] += 1 + split = dict((r, split[r]) for r in sorted(split)) + need(mass_of(split) == mass, 'control', 'split keeps the mass') + ok &= expect_reject('one idle 48 replaced by 47 + 1: composition', 'compose.profile', + lambda: check_composition(split, sources[:1]), results) + ev_split = Evaluator(split, m, W) + ok &= expect_reject('one idle 48 replaced by 47 + 1: claimed b no longer admissible', 'moment.accept', + lambda: require_accept(ev_split, b, 'b under the split profile'), results) + s_lo, s_hi, _, s_und = ev_split.root_bracket(40) + need(s_und is None, 'moment.bracket', 'split bisection stalled') + moved = s_hi < r_lo or s_lo > r_hi + results.append(dict(name='one idle 48 replaced by 47 + 1: root moves', target='moment.root', ok=moved, + rejected_by='moment.root' if moved else None, + detail='split root in [%s, %s]; original root - split root in %s' % ( + dec(s_lo, 40), dec(s_hi, 40), interval(r_lo - s_hi, r_hi - s_lo)))) + ok &= moved + ok &= expect_reject('provider counts swapped (417 gauge44 + 249 extra)', 'compose.profile', + lambda: check_composition(compose(local, {'gauge44': counts['extra'], 'extra': counts['gauge44']}, + idle), sources[:1]), results) + ok &= expect_reject('pre-borrow (canonical) local profiles with the same idle', 'compose.profile', + lambda: check_composition(compose(canon, counts, idle), sources[:1]), results) + ok &= expect_reject('idle remainders omitted', 'compose.profile', + lambda: check_composition(compose(local, counts, {}), sources[:1]), results) + ok &= expect_reject('W off by one (66305)', 'compose.mass', + lambda: check_mass(H, m, W + 1, T, calls, m * (W + 1) - mass), results) + ok &= expect_reject('b tampered by +1e-80 (B.json identity)', 'claims.b_identity', + lambda: b_identity(b + Fraction(1, 10 ** 80), b_above), results) + ok &= expect_reject('kappa tampered by +1e-130', 'claims.kappa', + lambda: kappa_identity(kappa + Fraction(1, 10 ** 130), b), results) + ok &= expect_reject('surcharge charged on native b (model control of code/assemble.py)', 'moment.accept', + lambda: require_accept(cons, b, 'b with surcharge'), results) + ok &= expect_reject('complex_lower + 1e-90 claimed admissible', 'moment.accept', + lambda: require_accept(native, complex_lower + Fraction(1, 10 ** 90), 'endpoint + 1e-90'), + results) + ok &= expect_reject('log 2 by 10 atanh terms without the remainder bound', 'evaluator.log2_crosscheck', + lambda: log2_crosscheck(tuple(2 * v for v in atanh_enclosure(1, 3, terms=10, tail=False)), l2b), + results) + # same truncation with the remainder bound is accepted (the remainder is what makes it sound) + log2_crosscheck(tuple(2 * v for v in atanh_enclosure(1, 3, terms=10, tail=True)), l2b) + ok &= expect_reject('exp(log 2) by 3 Taylor terms without the remainder bound', 'evaluator.exp_log2', + lambda: exp_log2_check(exp_enclosure(l2[0], l2[1], terms=3, tail=False)), results) + exp_log2_check(exp_enclosure(l2[0], l2[1], terms=3, tail=True)) + bad = bytearray(raw['PROFILE.json']) + bad[2] ^= 1 + ok &= expect_reject('one flipped bit in PROFILE.json', 'pin', lambda: verify_pin('PROFILE.json', bytes(bad)), + results) + receipt['negative_controls'] = results + receipt['positive_mutations_accepted'] = [ + 'log 2 by the same 10 atanh terms WITH the remainder bound overlaps the reference enclosure', + 'exp(log 2) by the same 3 Taylor terms WITH the remainder bound encloses 2'] + receipt['controls_ok'] = bool(ok) + print('negative controls: %d/%d rejected by their targeted checks' % ( + sum(1 for x in results if x['ok']), len(results)), flush=True) + for x in results: + print(' %s %s -> %s' % ('OK ' if x['ok'] else 'BAD ', x['name'], x['rejected_by']), flush=True) + need(ok, 'controls', 'a negative control was not rejected by its targeted check') + + receipt['findings'] = [ + 'Global profile recomposed from the task-A recounted local profiles and the task-B recounted idle ' + 'remainders: 249 P_gauge44 + 417 P_extra + idle = %s; equal to PROFILE.json, new/PROFILE.json, ' + 'new/SPEC.json, outer/B.json and outer/LEDGER.json. Mass %d = 72*66304 + 64*666; the second term is the ' + 'mass of the 8 rank-8 COPY children per call (W - D = 576 T).' % (plain(H), mass), + 'Native moment root (no surcharge, as the T74 assembly prices the complex endpoint) lies in [%s, %s] ' + '(width 1e-%d), inside (complex_lower, complex_lower + 1e-90): the package endpoint certificate is ' + 'reproduced. b = complex_lower - 1e-100 is admissible (mu(b) < 1, root - b in %s) and agrees with the ' + 'package enclosure of mu(b) in outer/LEDGER.json.' % (dec(r_lo, DIG), dec(r_hi, DIG), DIG, + interval(gap_lo, gap_hi)), + 'Task bracket: mu(%s) < 1 < mu(%s), width 1e-21, contains b.' % (dec(b_lo, 21), dec(b_hi, 21)), + 'Conservative side (surcharge 32 m N m^a / (10^16 W)): root in [%s...], SPEC conservative_complex_lower ' + 'accepted and +1e-90 rejected; native b is rejected under the surcharge.' % dec(c_lo, DIG)[:45], + 'Claimed kappa = floor_1e-136((1 - 2e-100)(b - 1e-100)) - 1e-112 exactly (arithmetic only).', + 'Top-level PRICE.json and evidence/ASSEMBLY.json carry an older pre-borrow price (native endpoint %s); they ' + 'do not price the borrowed profile (their endpoints are reproduced here as a positive control).' % ( + asm['complex_decimal'],), + ] + receipt['not_checked'] = [ + 'The outer lemmas (PR1673 capped phase-cell fusion, PR1786 fine primes, PR1758 interiors, union schedule), ' + 'the bit endpoint and its PR589 supplier, and the bootstrap: only the arithmetic link kappa(b) is checked.', + 'Where the 76 private zero buffers per call live. The moment uses only the rank profile, m and W; under ' + 'task B\'s dedicated-family charge for the buffers none of these changes. If the buffers instead had to be ' + 'hosted inside idle children, the idle remainders and hence the root would change; that model is not ' + 'evaluated here.', + 'Native lowering / invoice / precision-tape obligations; the all-size assumptions of the package.', + ] + receipt['summary'] = dict(root_lo=dec(r_lo, DIG), root_hi=dec(r_hi, DIG), b=dec(b, 100), + b_lo=dec(b_lo, 21), b_hi=dec(b_hi, 21)) + return dict(r_lo=r_lo, r_hi=r_hi, b=b, controls=len(results), t=time.time() - t0) + + +def main(): + ap = argparse.ArgumentParser(description='Independent price check of PR2269 (global profile + moment root)') + ap.add_argument('--repo', default=DEFAULT_REPO, help='git checkout containing commit %s' % COMMIT) + ap.add_argument('--blob-dir', default=None, help='exported package copy, DIR/') + ap.add_argument('--out', nargs='?', const=os.path.join(HERE, RECEIPT_NAME), default=None, + help='write the JSON receipt (default %s next to this script)' % RECEIPT_NAME) + args = ap.parse_args() + if args.out is not None and os.path.dirname(os.path.abspath(args.out)) != HERE: + print('--out must name a file next to this script (%s)' % HERE) + print(FAIL_LINE) + return 2 + receipt = dict(checker='price_check.py', object=dict(pr=2269, commit=COMMIT, package=PKG), + python=sys.version.split()[0], + scope='task C: global profile composition and exact moment-root bracket of the native complex ' + 'saving b', + credits='PR2269 jeremykothe2; PR2226 Cinna Davis / 1337isnot1337; PR2260 Dugongue; T74 lineage ' + 'PR1319/PR1297 (Rohan Arun), PR1625 (mdumitrean), pivot-554 kernel; PR547/548/559 moment ' + 'engines; icekylinx (Zhihao Chen) / eumemic checker lineage. Prepared with substantial AI ' + 'assistance (Claude Code, Anthropic); Apache-2.0.') + ok = True + info = None + t0 = time.time() + try: + info = run(args, receipt) + except Reject as e: + ok = False + receipt['failure'] = str(e) + print('FAILED: %s' % e, flush=True) + except Exception as e: # task A/B failures and malformed input: report, never pass + ok = False + receipt['failure'] = '%s: %s' % (type(e).__name__, e) + print('FAILED: %s: %s' % (type(e).__name__, e), flush=True) + receipt['model'] = __doc__.split('MODEL (stated precisely; also written to the receipt field "model").')[1].strip() + receipt['result'] = PASS_LINE if ok else FAIL_LINE + print('elapsed %.1f s' % (time.time() - t0)) + if args.out is not None: + with open(args.out, 'w') as fh: + json.dump(receipt, fh, indent=1, sort_keys=True) + fh.write('\n') + print('receipt written: %s' % args.out) + if ok: + print('%s root=[%s..., %s...] b_admissible=1 task_bracket=[%s,%s] controls=%d' % ( + PASS_LINE, receipt['summary']['root_lo'][:34], receipt['summary']['root_hi'][:34], + receipt['summary']['b_lo'], receipt['summary']['b_hi'], info['controls'])) + return 0 + print(FAIL_LINE) + return 1 + + +if __name__ == '__main__': + sys.exit(main()) From a419c9966ccff084dc0907c6476752fb8d8d6f08 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Thu, 15 Oct 2026 13:16:43 +0530 Subject: [PATCH 2/2] Follow-up: mechanism and lender prices of the PR2339 target-climb merges merge_mechanism.py checks all 26 merged targets in both providers. Each skips one intermediate frame whose gates all come from helpers that PR2339 removes, and each is fed instead by frame-0 anticipatory corrections. The frame-0 lender census on the PR2322 words is {4:32, 7:8, 8:8, 9:240}; the 32 ending at dimension 4 are the PR2226 lenders. Under rank-zero borrowing the merges therefore come only with width-4 -> 9 lenders, and every such alias loses (-7.8e-8 even with a merge credited). Lender take-overs ending at dimension 7-8, which are outside rank-zero, are priced at up to +1.43e-6 each before frame-raising costs. This answers open question 2 and replaces it. Co-Authored-By: Claude Opus 5.5 --- research/t74-2322-move-prices/README.md | 53 +- research/t74-2322-move-prices/TASK.json | 10 +- research/t74-2322-move-prices/VERIFY.json | 11 + .../t74-2322-move-prices/merge_mechanism.py | 215 +++ .../merge_mechanism.receipt.json | 1533 +++++++++++++++++ 5 files changed, 1811 insertions(+), 11 deletions(-) create mode 100644 research/t74-2322-move-prices/merge_mechanism.py create mode 100644 research/t74-2322-move-prices/merge_mechanism.receipt.json diff --git a/research/t74-2322-move-prices/README.md b/research/t74-2322-move-prices/README.md index 71ea1b9caf..0182fc40d8 100644 --- a/research/t74-2322-move-prices/README.md +++ b/research/t74-2322-move-prices/README.md @@ -74,6 +74,45 @@ If each extra handoff reproduced PR2322's reshapes, k handoffs would add k × 4. lender count. Whether any of them admits a coherent rank-zero handoff (frame availability, lifetimes, warp images, native lowering) is **not checked here**. +## Follow-up: where the target merges come from (`merge_mechanism.py`) + +**Mechanism.** Checked on all 26 merged targets in both providers: + +- In the PR2269 words each merged target climbs through exactly one intermediate frame that the PR2339 + words skip. For example, target 114 goes through dims [1,2,6,7,8] in PR2269 and [2,6,7,8] in PR2339. +- Every gate on the target at that skipped frame comes from a helper that PR2339 removes (608/609/610/612 + for target 114). +- Each merged target receives PR2339's anticipatory initial corrections, which run at frame 0 and pay + nothing. In all, 26 of the 32 corrected targets merge. + +So a merge is the removed helper's early interaction, replaced by a free frame-0 correction from a frame-0 +lender. + +**Lenders.** A frame-0 lender that takes over a FULL-ending role must climb to FULL (dimension 9 = H). +Its width therefore becomes 9, and widths can never exceed 9. + +On the PR2322 words, the frame-0 helpers end at dimensions {4: 32, 7: 8, 8: 8, 9: 240}. The 32 that end +at dimension 4 are exactly the PR2226 lenders 273..394, which are PR2339's lenders. The 8 + 8 that end at +7 or 8 would hand off at dimension 7–8 into first frames of dimension 4–5. PR2339's handoff screen found +that this fails the rank-zero condition; that finding is inherited here, not re-proved. + +Prices on the PR2322 words (LP-ceiling differences): + +| lender take-over | status | db per alias | with one merge credited | +|---|---|---|---| +| width-4 → 9 (PR2339 pattern) | rank-zero, realizable | −1.91e-7 | −7.8e-8 | +| width-5 → 9 | no such frame-0 lender | −1.91e-7 | −7.8e-8 | +| width-7 (end dim 7) → 9 | outside rank-zero | +8.5e-7 | +9.6e-7 | +| width-8 (end dim 8) → 9 | outside rank-zero | **+1.43e-6** | +1.54e-6 | + +**Answer to the second open question.** Under rank-zero anticipatory borrowing, the target merges come +only with the width-4 → 9 lender change, and every such alias loses even with a full merge credited. The +merges cannot be separated from that change by choosing a different lender. The positive rows are a price +tag on a *changed handoff premise*: lenders ending at dimension 7–8, with 16 frame-0 candidates +(572–575, 580–583, 311, 327, 498, 500, 501, 510, 512, 513). Those prices are optimistic. They omit any +cost of raising the borrowed role's gate frames to contain the lender's frame, which also moves partner +climbs. + ## Reproduce From the repository root, standard library only: @@ -81,6 +120,7 @@ From the repository root, standard library only: ```sh python3 -I -B research/t74-2322-move-prices/move_prices.py --fetch # ~16 s python3 -I -B research/t74-2322-move-prices/independent_recount.py # ~10 s +python3 -I -B research/t74-2322-move-prices/merge_mechanism.py # ~11 s ``` `--fetch` fetches `refs/pull/{2312,2322,2269,2339}/head` from the canonical repository if the pinned @@ -90,6 +130,7 @@ is blob- and sha256-pinned. Expected final lines: - `PASS_T74_MOVE_PRICES cap=0.001697195759 handoff_db=+4.272e-08 low_alias_db=-1.906e-07 high_alias_net=0 sites=33/12` - `PASS_T74_INDEPENDENT_RECOUNT` +- `PASS_T74_MERGE_MECHANISM merged=26 lenders_end4=32 pr2339_alias_db=-7.792e-08 takeover8_db=+1.427e-06` `vendor/pr2387/` holds byte copies of this author's PR2387 `ceiling_lp.py` and `fill_check80.py` and the iteration-3 enclosure code, all pinned. `move_prices.py` patches one line of `local_recount` at load time, @@ -115,12 +156,12 @@ This is a pricing screen on fixed, pinned words: register, with partners 648/649/650/652? The first step is to rerun PR2322's handoff generator with 653 as the target role. Its price is +4.27e-8. PR2374 dropped alias 653, so its lender conflict is the blocker to check. -- **Target merges without low aliases.** The +2.94e-6 from the 26 (1,1)→(2) target merges dwarfs the - owner-fill race. Can those merges be obtained without the width-9 low-lender inventory change? The - first step is to identify which B-gate frames changed on those targets in the PR2339 words, and - whether the anticipatory initial corrections (PR2394 lowers their prefix natively) can be kept with - the original helpers. Note that #1995/#2013 bound frame freedom inside a fixed scalar word, so this - needs a changed premise. +- **Higher-rank lender take-over.** *(This replaces the earlier "target merges without low aliases" + question; the answer above closes it for rank-zero borrowing.)* Can a lender that ends at dimension 7 + or 8 take over a removed width-8 helper's role if the role's gate frames are raised to contain the + lender's frame? There are 16 frame-0 candidates on the PR2322 words, priced at up to +1.43e-6 each + before frame-raising costs. The first step is to build one such word with the PR2339 builder, + relaxing condition (d), then recount it with `move_prices.py`'s recount to get the real reshape cost. - **More handoff patterns.** Which X shapes other than (5,1,1,1), and which partner shapes, give positive prices? The first step is to tabulate prices for every (lender shape, partner shape) pair that occurs in the words. diff --git a/research/t74-2322-move-prices/TASK.json b/research/t74-2322-move-prices/TASK.json index 360623698a..99adf1193c 100644 --- a/research/t74-2322-move-prices/TASK.json +++ b/research/t74-2322-move-prices/TASK.json @@ -50,7 +50,7 @@ "budget_minutes": 90, "stop_rule": "Stop after the certified cap, exact decomposition of the two realized changes, prices of four move types, an independent recount and the site census; no handoff construction in this session.", "outcome": "completed", - "evidence": "move_prices.py: per-register recount of 8 pinned words (each equal to its reported profile and inventory), exact decompositions PR2312->PR2322 and PR2269->PR2339, LP prices, calibration (LP +1.96e-7 vs realized +1.69e-7), certified cap b < 0.001697195759 for every legal whole-helper fill of the PR2322 words (PR2374 not rejected). independent_recount.py (separate implementation by an AI reviewer subagent) reproduces profiles, the change set and the site lists.", + "evidence": "move_prices.py: per-register recount of 8 pinned words (each equal to its reported profile and inventory), exact decompositions PR2312->PR2322 and PR2269->PR2339, LP prices, calibration (LP +1.96e-7 vs realized +1.69e-7), certified cap b < 0.001697195759 for every legal whole-helper fill of the PR2322 words (PR2374 not rejected). independent_recount.py (separate implementation by an AI reviewer subagent) reproduces profiles, the change set and the site lists. merge_mechanism.py: all 26 PR2339 target merges come from removed helpers' early gates replaced by frame-0 initial corrections; frame-0 lender census {4:32, 7:8, 8:8, 9:240}; rank-zero aliases lose even with merge credit; higher-rank take-overs priced.", "author": "Sagar Thakrar", "ai_assistance": "Prepared with substantial AI assistance: Claude Code (Anthropic, Claude Opus 5.5) wrote move_prices.py and this text; a separate Claude subagent wrote independent_recount.py from a plain-language rule statement without access to the package code. No independent human review is claimed.", "open_questions": [ @@ -61,10 +61,10 @@ "blocked_by": "PR2374 dropped alias 653 when moving 651 to lender 530; lender/lifetime conflicts are unchecked here." }, { - "question": "Can the 26 (1,1)->(2) target-climb merges that accompany PR2339's low aliases be obtained without the width-9 low-lender inventory change?", - "why_it_matters": "On their own they are worth +2.94e-6 on the PR2322 words, far above any remaining owner-fill gain, while the low-alias inventory change is what makes PR2339 lose.", - "first_step": "Diff the B-gate frames on those 26 targets between the PR2269 and PR2339 words to see whether the merge comes from the anticipatory initial corrections or from the removed helpers.", - "blocked_by": "PR1995/PR2013 bound frame freedom within a fixed scalar word; a changed premise (anticipatory corrections) is needed and its native lowering (PR2394) is only partly done." + "question": "Can a frame-0 lender ending at dimension 7 or 8 take over a removed width-8 helper's role (higher-rank handoff), with the role's gate frames raised to contain the lender's frame?", + "why_it_matters": "Rank-zero anticipatory aliases (width-4 -> 9 lenders) lose even with the target merges credited; the 16 frame-0 lenders ending at dimension 7-8 are priced at up to +1.43e-6 per take-over on the PR2322 words before frame-raising costs.", + "first_step": "Build one such word with the PR2339 builder relaxing its condition (d), then recount it with move_prices.py's recount to price the actual reshape of the role and its partners.", + "blocked_by": "The handoff is outside the rank-zero K_G contract of PR2226/PR2339; legality, frame raising and native lowering are unproven." }, { "question": "Which other (lender shape, partner shape) handoff patterns occurring in the PR2322 words have positive prices?", diff --git a/research/t74-2322-move-prices/VERIFY.json b/research/t74-2322-move-prices/VERIFY.json index b32132930c..9f7e79f802 100644 --- a/research/t74-2322-move-prices/VERIFY.json +++ b/research/t74-2322-move-prices/VERIFY.json @@ -25,6 +25,17 @@ ], "timeout_seconds": 300, "checks": "Separate implementation: both providers' profiles equal the reports; exact PR2312->PR2322 change set; 33 (1,1,1,1) helpers and 12 free (5,1,1,1) X registers. Expect PASS_T74_INDEPENDENT_RECOUNT." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/merge_mechanism.py", + "--fetch" + ], + "timeout_seconds": 300, + "checks": "Mechanism of the 26 PR2339 target merges (both providers), frame-0 lender census on the PR2322 words, and LP prices of lender take-over variants. Expect PASS_T74_MERGE_MECHANISM." } ] } diff --git a/research/t74-2322-move-prices/merge_mechanism.py b/research/t74-2322-move-prices/merge_mechanism.py new file mode 100644 index 0000000000..ee7d0a2042 --- /dev/null +++ b/research/t74-2322-move-prices/merge_mechanism.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Where the PR2339 target-climb merges come from, which lenders can produce them, and what a lender is worth. + +Follow-up to move_prices.py, answering its open question "can the 26 (1,1)->(2) target merges be obtained without +the losing low-lender inventory change?". Standard library only; reuses move_prices.py's pinned loaders. + + 1. Mechanism (both providers, all 26 merged targets). In the PR2269 words each merged target climbs through one + intermediate frame dimension that disappears in the PR2339 words. Every gate that touches the target at + that skipped frame has a partner register that PR2339 removes (a low-alias helper). Every merged target + receives PR2339 anticipatory initial corrections, which run at frame 0 and pay nothing. So the merge is the + helper's early interaction with the target, replaced by a free frame-0 correction from a frame-0 lender. + 2. Lender capacity on the PR2322 words. A frame-0 lender that takes over a FULL-ending role must climb to FULL + (dimension 9 = H). Its width therefore becomes 9 and it absorbs 9 - end_dim. The census of helper end + dimensions shows that only the 32 PR2226 lenders end below FULL with room for a 5-dimension take-over + (end_dim 4). The only other frame-0 helpers ending below FULL (8 ending at 7, 8 ending at 8) hand off at + dimension 7-8 into first frames of dimension 4-5, which fails the rank-zero handoff condition (PR2339 README). + 3. Prices on the PR2322 words (LP-ceiling differences, PR2387 bin-pattern LP, both providers). The PR2339 + pattern (width-4 lender -> 9) loses -1.91e-7 per alias, and still -7.8e-8 with a full merge credited to every + alias. A width-5 lender is no better. The hypothetical higher-rank take-overs (8 -> 9, 7 -> 9) would be worth + about +1.4e-6 and +0.85e-6 each, before any frame-raising cost. This is the price tag on changing the + rank-zero premise; nothing here constructs one. + +Prepared with substantial AI assistance (Claude Code, Anthropic); Apache-2.0. Credits as in move_prices.py. +Usage: python3 -I -B merge_mechanism.py [--repo PATH] [--fetch] [--out] +""" + +import argparse +import gzip +import importlib.util +import json +import os +import sys +import time +from collections import Counter + +if not __debug__: + sys.stdout.write('FAIL_T74_MERGE_MECHANISM refusing to run under python -O\n') + sys.exit(2) + +HERE = os.path.dirname(os.path.abspath(__file__)) +_spec = importlib.util.spec_from_file_location('move_prices', os.path.join(HERE, 'move_prices.py')) +MP = importlib.util.module_from_spec(_spec) +_spec.loader.exec_module(MP) +need = MP.need + + +def span_dim(F): + basis = [] + for v in F: + for b in basis: + v = min(v, v ^ b) + if v: + basis.append(v) + return len(basis) + + +def load_word(repo, key): + path, blob, sha = MP.WORDS[key] + data = MP.git(repo, 'show', MP.COMMITS[key[0]][0] + ':' + path) + need(MP.blob_id(data) == blob, 'word pin %s/%s' % key) + return json.loads(gzip.decompress(data)) + + +def target_gates(w, t): + """(section, index, frame dimension, partner) for every framed gate on t in A, B and restore.""" + out = [] + for sec in ('A', 'B', 'restore'): + for i, g in enumerate(w[sec]): + if g[0] == 'add' and t in (g[1], g[2]) and g[-1] is not None: + out.append((sec, i, span_dim(g[-1]), g[2] if g[1] == t else g[1])) + elif g[0] == 'scale' and g[1] == t and g[-1] is not None: + out.append((sec, i, span_dim(g[-1]), None)) + return out + + +def climb_dims(gates): + seq = [] + for _s, _i, d, _p in gates: + if d and (not seq or d > seq[-1]): + seq.append(d) + return seq + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--repo', default=MP.REPO_DEFAULT) + ap.add_argument('--fetch', action='store_true') + ap.add_argument('--remote', default=MP.REMOTE_DEFAULT) + ap.add_argument('--out', action='store_true') + args = ap.parse_args() + t0 = time.time() + lp, fc = MP.load_vendor() + MP.ensure_commits(args.repo, args.fetch, args.remote) + out = dict(object='PR2339 target-climb merges: mechanism, lender capacity and prices on the PR2322 words') + + # ---- 1. mechanism ------------------------------------------------------------------------------------------ + mech = {} + for prov in ('base', 'extra'): + a = MP.recount(args.repo, fc, ('pr2269', prov)) + b = MP.recount(args.repo, fc, ('pr2339', prov)) + w43, w80 = a['word'], b['word'] + merged = sorted(r for r in b['children'] if 112 <= r < 224 and a['children'][r] != b['children'][r]) + need(len(merged) == 26, 'expected 26 merged targets (%s)' % prov) + removed80 = set(w80['removed']) - set(w43['removed']) + corrected = Counter(c['target'] for c in w80['initial_corrections']) + rows = [] + for t in merged: + g43, g80 = target_gates(w43, t), target_gates(w80, t) + d43, d80 = climb_dims(g43), climb_dims(g80) + skipped = sorted(set(d43) - set(d80)) + need(len(skipped) == 1 and set(d80) <= set(d43), 'target %d: one skipped frame (%s %s)' % (t, d43, d80)) + partners = sorted({p for _s, _i, d, p in g43 if d == skipped[0]}) + need(partners and all(p in removed80 for p in partners), + 'target %d: gates at the skipped frame all come from removed low-alias helpers' % t) + need(corrected[t] >= 1, 'target %d receives anticipatory initial corrections' % t) + rows.append(dict(target=t, dims_pr2269=d43, dims_pr2339=d80, skipped_dim=skipped[0], + partners_at_skipped_frame=partners, initial_corrections=corrected[t])) + mech[prov] = dict(merged_targets=merged, corrected_targets=len(corrected), rows=rows) + need([r['target'] for r in mech['base']['rows']] == [r['target'] for r in mech['extra']['rows']], 'providers') + out['mechanism'] = mech + print('mechanism: all 26 merged targets (both providers) skip exactly one intermediate frame; every gate at that ' + 'frame in PR2269 comes from a helper PR2339 removes; each receives frame-0 initial corrections ' + '(%d of %d corrected targets merge)' % (len(mech['extra']['rows']), mech['extra']['corrected_targets'])) + + # ---- 2. lender capacity census on the PR2322 words ---------------------------------------------------------- + cen = {} + for prov in ('base', 'extra'): + w = load_word(args.repo, ('pr2322', prov)) + rec = MP.recount(args.repo, fc, ('pr2322', prov)) + end = {int(k): span_dim(F) for k, F in w['helper_final'].items()} + start = {int(k): span_dim(F) for k, F in w['start_extra'].items()} + helpers = rec['widths'] + frame0 = {r: end.get(r, 9) for r in helpers if r not in start} + by_end = Counter(frame0.values()) + need(all(rec['widths'][r] == frame0[r] for r in frame0), 'frame-0 helper width = end dimension') + need(max(helpers.values()) <= 9, 'helper widths are bounded by the frame dimension H = 9') + cen[prov] = dict(frame0_helpers_by_end_dim=dict(sorted(by_end.items())), + end4=sorted(r for r, e in frame0.items() if e == 4), + end7=sorted(r for r, e in frame0.items() if e == 7), + end8=sorted(r for r, e in frame0.items() if e == 8)) + need(cen['base']['frame0_helpers_by_end_dim'] == cen['extra']['frame0_helpers_by_end_dim'], 'census providers') + pr2226 = sorted(r for r in cen['extra']['end4'] if 273 <= r <= 394) # the PR2226 low lenders + need(cen['extra']['end4'] == pr2226 and len(pr2226) == 32 and min(pr2226) == 273 and max(pr2226) == 394, + 'the frame-0 end-dimension-4 helpers are exactly the 32 PR2226 lenders in 273..394') + c = cen['extra']['frame0_helpers_by_end_dim'] + need(c.get(4) == 32 and c.get(7) == 8 and c.get(8) == 8 and set(c) == {4, 7, 8, 9}, 'census %s' % c) + out['lender_census'] = cen + print('lender census (PR2322 words, frame-0 helpers by end dimension): %s; the 32 at dimension 4 are the PR2226 ' + 'lenders 273..394' % c) + + # ---- 3. prices ----------------------------------------------------------------------------------------------- + base = lp.CASES['pr2322_control'] + + def root(inv, pg, pe): + lp.CASES['t'] = dict(inv=inv, pg=pg, pe=pe) + lo, hi = 0.0015, 0.0020 + for _ in range(45): + mid = (lo + hi) / 2 + if lp.lp_mu_float('t', mid)[0] < 1: + lo = mid + else: + hi = mid + return lo + + r0 = root(dict(base['inv']), base['pg'], base['pe']) + removed_shape = (3, 2, 1, 1, 1) # the width-8 helper every PR2339 low alias removes + variants = [('PR2339 pattern: width-4 lender ending dim 4 -> 9', 4, (1, 1, 1, 1), (2, 1, 1, 1, 1, 1, 1, 1), 'rank-zero'), + ('width-5 lender -> 9 (2+1+1 absorbed)', 5, (2, 1, 1, 1), (2, 2, 1, 1, 1, 1, 1), 'no such frame-0 lender'), + ('width-7 lender ending dim 7 -> 9', 7, (3, 2, 1, 1), (3, 2, 1, 1, 1, 1), 'fails rank-zero'), + ('width-8 lender ending dim 8 -> 9', 8, (3, 2, 1, 1, 1), (3, 2, 1, 1, 1, 1), 'fails rank-zero')] + prices = [] + for name, lw, old, new, status in variants: + need(sum(new) == 9 and sum(old) == lw, 'variant widths') + row = dict(variant=name, lender_width=lw, lender_old=list(old), lender_new=list(new), status=status) + for merges in (0, 1): + inv = dict(base['inv']) + inv[8] -= 1 + inv[lw] -= 1 + inv[9] += 1 + pg, pe = Counter(base['pg']), Counter(base['pe']) + for P in (pg, pe): + P.subtract(removed_shape) + P.subtract(old) + P.update(new) + if merges: + P.subtract({1: 2}) + P.update({2: 1}) + row['db_merges_%d' % merges] = root(inv, dict(+pg), dict(+pe)) - r0 + prices.append(row) + print('%-48s [%s] db = %+.3e (no merge), %+.3e (one merge credited)' + % (name, status, row['db_merges_0'], row['db_merges_1'])) + need(prices[0]['db_merges_1'] < 0 and prices[1]['db_merges_1'] < 0, 'realizable lender patterns lose') + need(prices[2]['db_merges_0'] > 0 and prices[3]['db_merges_0'] > 0, 'higher-rank take-overs priced positive') + out['prices_on_pr2322_words'] = prices + out['conclusion'] = ('Under the rank-zero anticipatory handoff, the target merges come only with width-4 -> 9 ' + 'lenders and every such alias loses even with full merge credit; separating them requires a ' + 'changed handoff premise (lenders ending at dimension 7-8), priced at up to +1.4e-6 each ' + 'before frame-raising costs.') + out['python'] = sys.version.split()[0] + if args.out: + with open(os.path.join(HERE, 'merge_mechanism.receipt.json'), 'w') as f: + f.write(json.dumps(out, indent=1, sort_keys=True) + '\n') + print('runtime %.1fs' % (time.time() - t0)) + print('PASS_T74_MERGE_MECHANISM merged=26 lenders_end4=32 pr2339_alias_db=%+.3e takeover8_db=%+.3e' + % (prices[0]['db_merges_1'], prices[3]['db_merges_0'])) + return 0 + + +if __name__ == '__main__': + try: + sys.exit(main()) + except MP.Fail as e: + sys.stdout.write('FAIL_T74_MERGE_MECHANISM %s\n' % e) + sys.exit(1) diff --git a/research/t74-2322-move-prices/merge_mechanism.receipt.json b/research/t74-2322-move-prices/merge_mechanism.receipt.json new file mode 100644 index 0000000000..5a589d664e --- /dev/null +++ b/research/t74-2322-move-prices/merge_mechanism.receipt.json @@ -0,0 +1,1533 @@ +{ + "conclusion": "Under the rank-zero anticipatory handoff, the target merges come only with width-4 -> 9 lenders and every such alias loses even with full merge credit; separating them requires a changed handoff premise (lenders ending at dimension 7-8), priced at up to +1.4e-6 each before frame-raising costs.", + "lender_census": { + "base": { + "end4": [ + 273, + 275, + 277, + 282, + 289, + 291, + 293, + 298, + 305, + 307, + 309, + 314, + 321, + 323, + 325, + 330, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394 + ], + "end7": [ + 572, + 573, + 574, + 575, + 580, + 581, + 582, + 583 + ], + "end8": [ + 311, + 327, + 498, + 500, + 501, + 510, + 512, + 513 + ], + "frame0_helpers_by_end_dim": { + "4": 32, + "7": 8, + "8": 8, + "9": 240 + } + }, + "extra": { + "end4": [ + 273, + 275, + 277, + 282, + 289, + 291, + 293, + 298, + 305, + 307, + 309, + 314, + 321, + 323, + 325, + 330, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394 + ], + "end7": [ + 572, + 573, + 574, + 575, + 580, + 581, + 582, + 583 + ], + "end8": [ + 311, + 327, + 498, + 500, + 501, + 510, + 512, + 513 + ], + "frame0_helpers_by_end_dim": { + "4": 32, + "7": 8, + "8": 8, + "9": 240 + } + } + }, + "mechanism": { + "base": { + "corrected_targets": 32, + "merged_targets": [ + 114, + 121, + 123, + 126, + 133, + 137, + 149, + 153, + 155, + 159, + 164, + 166, + 173, + 175, + 177, + 183, + 188, + 190, + 193, + 199, + 202, + 204, + 211, + 216, + 218, + 222 + ], + "rows": [ + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 114 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 121 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 123 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 126 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 133 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 137 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 149 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 153 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 155 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 159 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 164 + }, + { + "dims_pr2269": [ + 1, + 2, + 4, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 4, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 624, + 625, + 626, + 628 + ], + "skipped_dim": 1, + "target": 166 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 173 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 175 + }, + { + "dims_pr2269": [ + 1, + 2, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 672, + 673, + 674, + 676 + ], + "skipped_dim": 1, + "target": 177 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 183 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 188 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 190 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 193 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 199 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 202 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 204 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 211 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 216 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 218 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 222 + } + ] + }, + "extra": { + "corrected_targets": 32, + "merged_targets": [ + 114, + 121, + 123, + 126, + 133, + 137, + 149, + 153, + 155, + 159, + 164, + 166, + 173, + 175, + 177, + 183, + 188, + 190, + 193, + 199, + 202, + 204, + 211, + 216, + 218, + 222 + ], + "rows": [ + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 114 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 121 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 123 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 126 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 133 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 137 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 149 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 153 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 155 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 159 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 164 + }, + { + "dims_pr2269": [ + 1, + 2, + 4, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 4, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 624, + 625, + 626, + 628 + ], + "skipped_dim": 1, + "target": 166 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 608, + 609, + 610, + 612 + ], + "skipped_dim": 1, + "target": 173 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 175 + }, + { + "dims_pr2269": [ + 1, + 2, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 672, + 673, + 674, + 676 + ], + "skipped_dim": 1, + "target": 177 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 183 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 188 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 190 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 193 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 199 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 600, + 601, + 602, + 604 + ], + "skipped_dim": 1, + "target": 202 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 592, + 593, + 594, + 596 + ], + "skipped_dim": 1, + "target": 204 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 211 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 688, + 689, + 690, + 692 + ], + "skipped_dim": 1, + "target": 216 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 680, + 681, + 682, + 684 + ], + "skipped_dim": 1, + "target": 218 + }, + { + "dims_pr2269": [ + 1, + 2, + 6, + 7, + 8 + ], + "dims_pr2339": [ + 2, + 6, + 7, + 8 + ], + "initial_corrections": 2, + "partners_at_skipped_frame": [ + 696, + 697, + 698, + 700 + ], + "skipped_dim": 1, + "target": 222 + } + ] + } + }, + "object": "PR2339 target-climb merges: mechanism, lender capacity and prices on the PR2322 words", + "prices_on_pr2322_words": [ + { + "db_merges_0": -1.9061134770440372e-07, + "db_merges_1": -7.79170536871314e-08, + "lender_new": [ + 2, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "lender_old": [ + 1, + 1, + 1, + 1 + ], + "lender_width": 4, + "status": "rank-zero", + "variant": "PR2339 pattern: width-4 lender ending dim 4 -> 9" + }, + { + "db_merges_0": -1.9061134770440372e-07, + "db_merges_1": -7.79170536871314e-08, + "lender_new": [ + 2, + 2, + 1, + 1, + 1, + 1, + 1 + ], + "lender_old": [ + 2, + 1, + 1, + 1 + ], + "lender_width": 5, + "status": "no such frame-0 lender", + "variant": "width-5 lender -> 9 (2+1+1 absorbed)" + }, + { + "db_merges_0": 8.501276828102276e-07, + "db_merges_1": 9.6296049413515e-07, + "lender_new": [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + "lender_old": [ + 3, + 2, + 1, + 1 + ], + "lender_width": 7, + "status": "fails rank-zero", + "variant": "width-7 lender ending dim 7 -> 9" + }, + { + "db_merges_0": 1.427425214260529e-06, + "db_merges_1": 1.5403349115108121e-06, + "lender_new": [ + 3, + 2, + 1, + 1, + 1, + 1 + ], + "lender_old": [ + 3, + 2, + 1, + 1, + 1 + ], + "lender_width": 8, + "status": "fails rank-zero", + "variant": "width-8 lender ending dim 8 -> 9" + } + ], + "python": "3.14.4" +}