diff --git a/research/t74-2322-move-prices/README.md b/research/t74-2322-move-prices/README.md new file mode 100644 index 0000000000..0182fc40d8 --- /dev/null +++ b/research/t74-2322-move-prices/README.md @@ -0,0 +1,182 @@ +# 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**. + +## 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: + +```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 +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` +- `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, +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. +- **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. + +## 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..99adf1193c --- /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. 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": [ + { + "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 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?", + "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..9f7e79f802 --- /dev/null +++ b/research/t74-2322-move-prices/VERIFY.json @@ -0,0 +1,41 @@ +{ + "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." + }, + { + "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/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/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" +} 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())