diff --git a/research/t74-owner-fill-optimality/README.md b/research/t74-owner-fill-optimality/README.md new file mode 100644 index 0000000000..3ae33ae669 --- /dev/null +++ b/research/t74-owner-fill-optimality/README.md @@ -0,0 +1,124 @@ +# Exact owner-fill optimality on the T74 handoff line: PR2374 is optimal; PR2435's fill leaves +5.8e-10 + +**Audit / independent check; no κ claim.** This package certifies the exact pattern-integer optimum of the +whole-helper owner fill for the two latest T74 claims and compares each claim's published fill with it. + +- **[PR2374](https://github.com/CrocSwap/integer-mult-bounds/pull/2374)** (Jeremy Kothe) claims "an exact + window-free-optimal owner fill" on [PR2322](https://github.com/CrocSwap/integer-mult-bounds/pull/2322)'s + words. + - **Confirmed and strengthened.** Every legal whole-helper owner fill of these words has + **b ≤ κ₂₃₇₄ + 10⁻¹⁵**. + - Its idle multiset `{1:21978, 3:8592, 5:2552, 32:1, 48:24560}` is the only one whose root exceeds + κ₂₃₇₄ − 10⁻¹². + - Owner-map work on the PR2322 words is therefore exactly exhausted. The earlier cap in + [PR2402](https://github.com/CrocSwap/integer-mult-bounds/pull/2402) allowed up to 8.1e-10. +- **[PR2435](https://github.com/CrocSwap/integer-mult-bounds/pull/2435)** (Jeremy Kothe, κ = 0.0016985113437) + raises 24 copy-buffer entrances and adds "an exact owner fill for the new inventory", with idle + `{1:20824, 3:6695, 5:1, 48:25302}`. + - **That fill is not the pattern optimum.** The unique pattern-integer optimum has idle + **`{1:20822, 3:6694, 5:2, 48:25302}`**, with root **0.0016985119240, +5.80e-10 above PR2435's claimed κ**. + - It moves two rank-1 remainders and one rank-3 remainder into one more rank-5 remainder. Its pattern + counts are in the receipt; for example it uses two (32: 9,9,9) bins and 1,156 (48: 4,8,9,9,9,9) bins. + - Every legal fill of the PR2435 words has b ≤ that root + 10⁻¹⁵. + - Whether the optimum can be realized under PR2435's windows and family rules is **not** checked here. + It is a concrete owner-level target worth up to +5.8e-10. + +## Method (`owner_optimum.py`) + +0. **Inputs.** + - PR2322 words: profile and inventory recounted in PR2402. + - PR2435 words: recounted for this audit with the PR2387 frame-climb rule from PR2435 head `324d7d35` + (`BORROW-WORD-43base`, blob 7e382c2d; `BORROW-WORD-43extra`, blob 29fa1b3a). Both providers give + profile {1:2359, 2:632, 3:330, 4:120, 5:38, 8:8} and inventory {4:33, 5:9, 7:62, 8:90, 9:240}, equal to + the published report. + - The idle multisets and κ values are as published in each PR body. +1. **The relaxation.** A legal fill places every helper role whole into one idle bin. The bins have ranks + 8/16/32/48 and counts 49,728 / 33,152 / 33,152 / 33,152. So the fill's idle remainders come from an + integer pattern-count vector x ≥ 0 over the 1,163 width patterns, with the bin and width-inventory row + sums fixed (PR2387 / PR2360 relaxation, after PR1129). Windows, families and ports are dropped. That + makes this a relaxation of every legal fill, and the moment is linear in x. +2. **Root check.** The PR2322 local profile (recounted in PR2402) plus PR2374's idle multiset has its root + certified within ±10⁻¹⁵ of the claimed κ, using 800-bit enclosures. Its rank mass equals 73·66304 − 23680. +3. **Exact dual.** At a₀ = κ₂₃₇₄ + 10⁻¹⁵, a float simplex dual is repaired to an exact rational dual. It is + feasible against 800-bit lower enclosures of h(r) = (r/73)^(1−a₀) on all 1,163 patterns. Every integer + x then satisfies + + 66304·μₓ(a₀) ≥ L_loc + D + Σ_p rc_p xₚ, rc_p ≥ 0 exact, + + and if Σ rc_p xₚ ≥ T := 66304 − L_loc − D, then bₓ ≤ a₀. Here T ≈ 1.5475e-4. +4. **Enumeration.** Every integer x with Σ rc_p xₚ < T is enumerated exactly. + - Only 9 basic and 7 non-basic patterns have rc < T. + - The 2 degenerate patterns, (32: 7,8,8,9) and (32: 7,7,9,9), are checked to swap only zero-remainder + patterns, so they never change the idle multiset. Their basis representation is integral, so their + counts never affect integrality. + - Any solution using them therefore maps to a count-0 representative with the same idle multiset and the + same Σ rc. That representative is checked to be nonnegative for every candidate combination, so the + sweep is complete. + - The other 5 have reduced costs 5.5e-5 … 1.5e-4, which allows counts ≤ 2. + - Basic variables are solved in exact rationals. +5. **Search, then exclusion.** + - Search: at a = κ_claim, enumerate every integer solution that could beat the claim. A budget-pruned + DFS is exact. Rank the distinct idle multisets by certified root. + - Exclusion: at a₀ = (best root) + 10⁻¹⁵, zero integer survivors remain, so every fill has b ≤ a₀. +6. **Control at (best root) − 10⁻¹²:** the optimal fill must survive, and it does. + - For PR2374 there are 25 survivors and for PR2435 there are 1,250. Each set is made of degenerate + copies of one heavy part, and all carry the optimal idle multiset. + - That gives the uniqueness statement. + +An adversarial AI reviewer reviewed the PR2374 part (the PR2435 extension came later) and found it +**not refuted**. Using its own code +(Decimal at 90 digits), it: +- reproduced PR2374's root to 60 digits; +- confirmed with a Gomory group-relaxation shortest path that the only correction within the budget is one + empty 32-bin; +- ran local search over more than 48,000 exchanges of up to 4 bins without finding any improvement. + +Its runner-up fill, `{1:21978, 3:8591, 5:2553, 30:1, 48:24560}`, has a root 5.0e-10 below PR2374's. Its +two wording issues are fixed here: the nonnegativity argument for the degenerate sweep, and the +degenerate-copy count. + +## Reproduce + +From the repository root, standard library only. It needs no network, since all inputs are vendored and +pinned. + +```sh +python3 -I -B research/t74-owner-fill-optimality/owner_optimum.py # ~45 s +``` + +Expected final line: +`PASS_T74_OWNER_OPTIMUM pr2374:claim_is_optimum pr2435:optimum_gain=+5.803e-10 unique_within_1e-12 no_new_kappa` + +All results were run on CPython 3.14.4; the registered Python 3.12 replay was not run locally. + +## Scope and limits + +- **What is not re-checked.** Realization of the fills (windows, families, ports, admission, outer) is not + re-run, for either PR's fill or for the PR2435 pattern optimum. The bound covers every legal fill. + Attaining PR2435's optimum needs a realized owner map. +- **What the statement covers.** It is about owner fills of the fixed PR2322 and PR2435 words, the 249/417 + dispatch and the unchanged PR2269 bin stock. Changed words, inventories or templates are outside it; see PR2402 + and PR2429 for those levers. +- **Exactness.** The enumeration is exact (integer and rational), with an exact dual and enclosures. The + only floating-point step is the simplex that proposes the dual, and its repair is exact. + +## Open next questions + +- **Other inventories.** Do the same exact integer-optimality certificates hold for PR2312's and PR2269's + inventories? That would show whether every recent owner-fill PR on the T74 line was already at the + integer optimum. First step: run `owner_optimum.py` with their inventories and published idle + multisets. +- **Recursive-interface levers.** Since packing on these words is exhausted, which word-level move is + cheapest to realize? Candidates are a block-53 handoff (+4.3e-8, PR2402) and cold-restoring one + end-climb-3 helper (+1.46e-6, PR2429). First step: attempt the PR601-style commutation test on the 64 + end-climb-3 helpers. + +## Credits and licence + +- PR2374 / PR2349 (Jeremy Kothe) and PR2363 (mason-hale): the audited fills. +- PR2322 (Vlado Vojdanovski): the words. +- PR2360 (Jeremy Diviney) and PR1129 (Ali Romman): the pattern-dual relaxation. +- PR2387 / PR2402 (this author): the LP and recount tools, vendored with pins. + +Prepared with substantial AI assistance (Claude Code, Anthropic, Claude Opus 5.5). An adversarial AI +reviewer was used; no independent human review is claimed. Apache-2.0. diff --git a/research/t74-owner-fill-optimality/SOURCES.json b/research/t74-owner-fill-optimality/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/t74-owner-fill-optimality/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-owner-fill-optimality/TASK.json b/research/t74-owner-fill-optimality/TASK.json new file mode 100644 index 0000000000..7aea46ced4 --- /dev/null +++ b/research/t74-owner-fill-optimality/TASK.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "refined", + "actual_scope": "Are the owner fills claimed by PR2374 (PR2322 words) and PR2435 (copy-buffer-raised words) optimal over all legal whole-helper fills (exact bin-pattern integer relaxation), and if not, what is the optimum?", + "scope_change_reason": "Drawn on the adversarial-audit track (seed 71). The specific new implication of PR2374 is its optimality claim, which had no independent check; the bin-pattern integer program gives one by a different method and over a larger class.", + "bottleneck_link": "Shows owner packing on the T74 handoff line is exactly exhausted for PR2322's words and has exactly +5.8e-10 left for PR2435's words, so further gains need word-level changes.", + "budget_minutes": 60, + "stop_rule": "Stop once the exact dual plus integer enumeration either exhibits a better idle multiset or proves none exists above kappa_2374 + 1e-15, with a below-root control.", + "outcome": "completed", + "evidence": "owner_optimum.py: both claimed roots certified within 1e-15 of their kappa; exact dual plus pruned exact enumeration finds the pattern-integer optimum and excludes everything above it + 1e-15. PR2374: optimum = its fill (unique within 1e-12). PR2435: unique optimum idle {1:20822,3:6694,5:2,48:25302}, root 0.0016985119240 (+5.80e-10 over its claim). PR2435 words recounted (profile/inventory equal to report).", + "author": "Sagar Thakrar", + "ai_assistance": "Prepared with substantial AI assistance: Claude Code (Anthropic, Claude Opus 5.5) wrote the certificate and text; a separate Claude subagent adversarially reviewed it. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can PR2435's pattern optimum {1:20822,3:6694,5:2,48:25302} be realized as a legal owner map under its windows and families?", + "why_it_matters": "It is worth +5.80e-10 in kappa on the current top T74 claim and is the exact maximum for those words.", + "first_step": "Start from PR2435's FILL and move helpers into two extra (32: 9,9,9) bins and the (48: 4,8,9,9,9,9) bins listed in the receipt's pattern_counts, re-checking windows and family rules.", + "blocked_by": "Window/family feasibility is not modelled by the pattern relaxation." + }, + { + "question": "Which word-level move on the PR2322 words is cheapest to realize now that packing is exhausted?", + "why_it_matters": "Owner fills cannot add more than 1e-15; word-level moves are priced at +4.3e-8 (handoff) to +1.46e-6 (cold-restoring an end-climb-3 helper).", + "first_step": "Attempt a PR601-style commutation test on the 64 end-climb-3 helpers (PR2429).", + "blocked_by": "Exact cleanup commutation semantics of the T74 words are not modelled here." + } + ] +} diff --git a/research/t74-owner-fill-optimality/VERIFY.json b/research/t74-owner-fill-optimality/VERIFY.json new file mode 100644 index 0000000000..7b4d52fb48 --- /dev/null +++ b/research/t74-owner-fill-optimality/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/owner_optimum.py" + ], + "timeout_seconds": 300, + "checks": "For PR2374 and PR2435: certified root bracket of the published idle multiset; exact search of integer pattern solutions that could beat the claim; certified root of the best; exact dual exclusion at best + 1e-15 (no survivors); control at best - 1e-12 (optimum survives, unique idle multiset). Expect PASS_T74_OWNER_OPTIMUM." + } + ] +} diff --git a/research/t74-owner-fill-optimality/owner_optimum.py b/research/t74-owner-fill-optimality/owner_optimum.py new file mode 100644 index 0000000000..4cc934232a --- /dev/null +++ b/research/t74-owner-fill-optimality/owner_optimum.py @@ -0,0 +1,330 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Certificate that PR2374's owner fill is optimal for the PR2322 T74 words over all whole-helper fills. + +PR2374 (jeremykothe2) claims "an exact window-free-optimal owner fill" on PR2322's words. Its published leftover +idle ranks are I = {1:21978, 3:8592, 5:2552, 32:1, 48:24560} and its claimed kappa is 0.0016971949509017704... +This script audits the optimality claim by a different method and over a larger class: the bin-pattern integer +program of PR2387/PR2360 (after PR1129). + +Every legal whole-helper owner fill puts each helper role whole into one idle bin (ranks 8/16/32/48, counts +49728/33152/33152/33152). So its idle remainders come from an integer pattern-count vector x >= 0 with the bin +and width-inventory row sums. The moment is linear in x for fixed a. + +Steps: + 1. Re-derive PR2374's root from the local profile plus I. The PR2322 profile is recounted in PR2402; both + providers have {1:2335, 2:512, 3:426, 4:120, 5:38, 8:8}, with dispatch 249/417. Certify it lies within 1e-15 + of the claimed kappa. + 2. At a0 = kappa_2374 + 1e-15, take an exact rational dual (y, z) that is feasible against 800-bit LOWER + enclosures of h(r) = (r/73)^(1-a0) for all 1163 patterns. Every integer x then satisfies + 66304 mu_x(a0) >= L_loc + D + sum_p rc_p x_p, rc_p >= 0 exact. + If sum rc_p x_p >= T := 66304 - L_loc - D, then mu_x(a0) >= 1, so b_x <= a0. + 3. Enumerate exactly every integer x with sum rc_p x_p < T. Only patterns with rc_p < T can appear; the LP + basis system is solved in exact rationals. Degenerate patterns (rc ~ 0) are shown to swap only + zero-remainder patterns, so they never change the idle multiset; they enter only through integrality, + residues mod det(B). Each surviving x is shown to have idle multiset I exactly. Its moment at a0 is then + certified >= 66304 directly with lower enclosures. + Conclusion: every legal whole-helper owner fill of the PR2322 words on the unchanged T74 template has + b <= kappa_2374 + 1e-15, and I is the only idle multiset within the dual gap. The negative control repeats the + exclusion at kappa_2374 - 1e-12, where PR2374's own fill must survive. + +Prepared with substantial AI assistance (Claude Code, Anthropic); Apache-2.0. Credits in README.md. +Usage: python3 -I -B owner_optimum.py [--out] +""" + +import argparse +import hashlib +import importlib.util +import itertools +import json +import os +import sys +import time +from collections import Counter +from fractions import Fraction + +if not __debug__: + sys.stdout.write('FAIL_T74_OWNER_OPTIMUM refusing to run under python -O\n') + sys.exit(2) + +HERE = os.path.dirname(os.path.abspath(__file__)) +VENDOR = { # byte copies of PR2387 (this author), as vendored and pinned in PR2402 + 'vendor/pr2387/ceiling_lp.py': ('48362358660f74e0e235865df3e172494c191212', + '63e2d35b07342508680e20f4b60c4da888acf4c771cd9b10400c21490f1491be'), + 'vendor/pr2387/vendor/iter3/price_check.py': ('708753e7703077a8ce4311293f02e42afb801934', + '19fcfb9f4d766959c599223090142edb03998229459cff1266960ca6b7ed1e0f'), +} +CLAIMS = { # published in the PR bodies (owner fills audited here) + 'pr2374': dict(kappa=Fraction('0.001697194950901770426594081877309541199782925447437522970580'), + idle={1: 21978, 3: 8592, 5: 2552, 32: 1, 48: 24560}, + inv={4: 33, 5: 9, 7: 38, 8: 114, 9: 240}, + profile={1: 2335, 2: 512, 3: 426, 4: 120, 5: 38, 8: 8}, + words='PR2322 words (recounted in PR2402)'), + 'pr2435': dict(kappa=Fraction('0.001698511343697629329051733814187744630805511096704593311278'), + idle={1: 20824, 3: 6695, 5: 1, 48: 25302}, + inv={4: 33, 5: 9, 7: 62, 8: 90, 9: 240}, + profile={1: 2359, 2: 632, 3: 330, 4: 120, 5: 38, 8: 8}, + words='PR2435 words (24 copy-buffer entrances raised; profile and inventory as published)'), +} +KAPPA_2374 = CLAIMS['pr2374']['kappa'] +IDLE_2374 = CLAIMS['pr2374']['idle'] +EPS = Fraction(1, 10 ** 15) + + +class Fail(Exception): + pass + + +def need(cond, what): + if not cond: + raise Fail(what) + + +def load_lp(): + for rel, (blob, sha) in VENDOR.items(): + data = open(os.path.join(HERE, rel), 'rb').read() + need(hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() == 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) + return lp + + +def audit(C, P, W, name): + claim = CLAIMS[name] + K, I = claim['kappa'], claim['idle'] + case = 'claim_' + name + C.CASES[case] = dict(inv=dict(claim['inv']), pg=dict(claim['profile']), pe=dict(claim['profile'])) + need(sum(claim['profile'].values()) and sum(r * n for r, n in claim['profile'].items()) == 1856 + sum(w * n for w, n in claim['inv'].items()), + name + ': local mass = 1856 + helper widths') + W = C.W_LIVE + loc = C.local_counts(case) + need(sum(r * n for r, n in I.items()) + sum(r * n for r, n in loc.items()) == 73 * W - 23680, + name + ': idle multiset + local profile = rank mass 73 W - deficit') + + def h_up(r, a): + if r == 0: + return Fraction(0) + ll, lu = P.log_enclosure(C.M, r) + el, eu = P.exp_enclosure((a.numerator * ll) // a.denominator, P.cdiv(a.numerator * lu, a.denominator)) + return Fraction(r * eu, C.M * P.ONE) + + def wmu_idle(idle, a, upper): + f = h_up if upper else C.h_lower + return sum(n * f(r, a) for r, n in loc.items()) + sum(n * f(r, a) for r, n in idle.items()) + + # ---- 1. PR2374's root is within 1e-15 of its claimed kappa ------------------------------------------------- + hi_a, lo_a = K + EPS, K - EPS + need(wmu_idle(I, hi_a, False) > W and wmu_idle(I, lo_a, True) < W, + name + ': idle multiset root is not within 1e-15 of its claimed kappa') + out = dict(object=name + ' owner fill on the ' + claim['words'] + ': optimality over all whole-helper fills', + root_bracket=[str(lo_a), str(hi_a)], inventory=claim['inv'], profile=claim['profile'], idle=I, + kappa=str(K)) + print('[%s] 1. local profile + published idle multiset: root certified in kappa +- 1e-15' % name) + + def exclusion(a0, label): + """Return (T, survivors) for the exact dual at a0.""" + _mu, sol, du = C.lp_mu_float(case, float(a0)) + y = {R: Fraction(du[i]) for i, R in enumerate(C.NB)} + z = {w: Fraction(du[len(C.NB) + i]) for i, w in enumerate(C.WID)} + L = {r: C.h_lower(r, a0) for r in range(0, 49)} + worst = {R: Fraction(0) for R in C.NB} + for R, p in C.COLS: + s = L[R - sum(p)] - y[R] - sum(z[w] for w in p) + worst[R] = min(worst[R], s) + y = {R: y[R] + worst[R] for R in C.NB} + rc = [L[R - sum(p)] - y[R] - sum(z[w] for w in p) for R, p in C.COLS] + need(min(rc) >= 0, 'exact dual feasibility') + rhs = C.rhs_of(case) + D = sum(C.NB[R] * y[R] for R in C.NB) + sum(rhs[len(C.NB) + i] * z[w] for i, w in enumerate(C.WID)) + Lloc = sum(n * C.h_lower(r, a0) for r, n in loc.items()) + T = W - Lloc - D + basis = sorted(j for j, x in sol.items() if x > 1e-9) + need(len(basis) == len(C.NB) + len(C.WID), 'LP basis size') + cand = [j for j in range(len(C.COLS)) if rc[j] < T and j not in basis] + need(all(rc[j] < T for j in basis), 'basic columns inside the budget') + rows = len(C.NB) + len(C.WID) + + def col(j): + R, p = C.COLS[j] + return [Fraction(1 if R == RR else 0) for RR in C.NB] + [Fraction(p.count(w)) for w in C.WID] + + Bm = [[col(j)[i] for j in basis] for i in range(rows)] + + def solve(b): + A = [Bm[i][:] + [Fraction(b[i])] for i in range(rows)] + for c in range(rows): + piv = next(r for r in range(c, rows) if A[r][c] != 0) + A[c], A[piv] = A[piv], A[c] + pv = A[c][c] + A[c] = [v / pv for v in A[c]] + for r in range(rows): + if r != c and A[r][c] != 0: + f = A[r][c] + A[r] = [u - f * v for u, v in zip(A[r], A[c])] + return [A[i][rows] for i in range(rows)] + + # degenerate columns: rc tiny; check they only exchange zero-remainder patterns (idle multiset invariant) + degen = [j for j in cand if rc[j] < T / 10 ** 6] + heavy = [j for j in cand if j not in degen] + for j in degen: + lam = solve(col(j)) + need(C.COLS[j][0] - sum(C.COLS[j][1]) == 0 and + all(l == 0 or C.COLS[b][0] - sum(C.COLS[b][1]) == 0 for l, b in zip(lam, basis)), + 'degenerate column %s changes the idle multiset' % (C.COLS[j],)) + # Completeness of the degenerate sweep: if every degenerate column has an integral basis representation, + # integrality of x_B does not depend on its count, and a feasible x with positive degenerate counts maps + # to the count-0 representative, which has the same idle multiset and sum rc, provided that representative + # is nonnegative. Nonnegativity at count 0 is asserted below for every heavy combination. + lam_integral = all(l.denominator == 1 for j in degen for l in solve(col(j))) + det_den = 1 + for j in degen: + for l in solve(col(j)): + det_den = det_den * l.denominator // __import__('math').gcd(det_den, l.denominator) + xb0 = solve(rhs) + for v in xb0: + det_den = det_den * v.denominator // __import__('math').gcd(det_den, v.denominator) + maxc = {j: int(T // rc[j]) for j in heavy} + survivors = [] + colv = {j: col(j) for j in heavy + degen} + + def visit(counts, b, s): + # complete heavy part: try every degenerate residue + if lam_integral: + need(all(v >= 0 for v in solve(b)), 'count-0 representative negative for heavy part %s' % counts) + for kz in itertools.product(range(det_den), repeat=len(degen)): + bb = list(b) + for c, j in zip(kz, degen): + bb = [bi - c * v for bi, v in zip(bb, colv[j])] + xb = solve(bb) + if all(v.denominator == 1 and v >= 0 for v in xb): + idle = Counter() + for v, j in list(zip(xb, basis)) + [(c, j) for j, c in counts.items()] + list(zip(kz, degen)): + R, p = C.COLS[j] + if v and R - sum(p): + idle[R - sum(p)] += int(v) + full = Counter() + for v, j in list(zip(xb, basis)) + [(c, j) for j, c in counts.items()] + list(zip(kz, degen)): + if v: + full[str(C.COLS[j])] += int(v) + survivors.append(dict(heavy={str(C.COLS[j]): c for j, c in counts.items()}, patterns=dict(full), + degenerate_residues=list(kz), sum_rc=float(s), idle=dict(sorted(idle.items())))) + + def dfs(i, b, s, counts): # exact budget-pruned enumeration of heavy counts with sum rc < T + if i == len(heavy): + visit(counts, b, s) + return + j = heavy[i] + c = 0 + while c <= maxc[j] and s + c * rc[j] < T: + nb = [bi - c * v for bi, v in zip(b, colv[j])] if c else b + if c: + counts[j] = c + dfs(i + 1, nb, s + c * rc[j], counts) + counts.pop(j, None) + c += 1 + + dfs(0, list(rhs), Fraction(0), {}) + info = dict(a0=str(a0), T=float(T), dual_repair={str(R): float(worst[R]) for R in C.NB}, + basis=[str(C.COLS[j]) for j in basis], degenerate=[str(C.COLS[j]) for j in degen], + heavy={str(C.COLS[j]): dict(rc=float(rc[j]), max_count=maxc[j]) for j in heavy}, + det_lcm=det_den, degenerate_representation_integral=lam_integral, survivors=len(survivors), + distinct_heavy_parts=len({json.dumps(s['heavy'], sort_keys=True) for s in survivors}), + survivor_idle_multisets=sorted({json.dumps(s['idle'], sort_keys=True) for s in survivors})) + print('%s: a0 = %s; budget T = %.4e; basis %d, degenerate %d, heavy %d candidate patterns; integer survivors %d' + % ('[%s] %s' % (name, label), '%.19f' % float(a0), float(T), len(basis), + len(degen), len(heavy), len(survivors))) + return T, survivors, info + + # ---- 2. search: every integer pattern solution that could beat the claim at a = K ------------------------------ + _T, cands, _info = exclusion(K, '2. search') + def froot(idle): + lo, hi = float(K) - 1e-7, float(K) + 1e-7 + for _ in range(80): + mid = (lo + hi) / 2 + if sum(n * C.h_float(r, mid) for r, n in loc.items()) + sum(n * C.h_float(r, mid) for r, n in idle.items()) < W: + lo = mid + else: + hi = mid + return lo + multisets = {json.dumps({str(k): v for k, v in sorted(s['idle'].items())}, sort_keys=True): s for s in cands} + ranked = sorted(((froot({int(k): v for k, v in json.loads(m).items()}), m) for m in multisets), reverse=True) + best_root, best_key = ranked[0] if ranked else (float(K), json.dumps({str(k): v for k, v in I.items()}, sort_keys=True)) + best = {int(k): v for k, v in json.loads(best_key).items()} + need(sum(r * n for r, n in best.items()) == sum(r * n for r, n in I.items()), 'best multiset keeps the idle mass') + # certified bracket of the best multiset's root + RB = Fraction(best_root).limit_denominator(10 ** 30) + need(wmu_idle(best, RB + EPS, False) > W and wmu_idle(best, RB - EPS, True) < W, 'best root bracket') + out['pattern_optimum'] = dict(idle={str(k): v for k, v in sorted(best.items())}, root_bracket=[str(RB - EPS), str(RB + EPS)], + gain_over_claim=float(RB - K), candidates_better_than_claim=len(ranked) - 1, + pattern_change_vs_lp_basis=(multisets[best_key]['heavy'] if best_key in multisets else {}), + pattern_counts=(multisets[best_key]['patterns'] if best_key in multisets else {}), + ranked=[dict(root=r, idle=json.loads(m)) for r, m in ranked[:6]]) + print('[%s] 2. pattern-IP optimum %s, root %.19f (%+.3e vs claimed kappa)' % (name, best_key, float(RB), float(RB - K))) + # ---- 3. exclusion at a0 = best root + 1e-15 ----------------------------------------------------------------------- + a0 = RB + EPS + T, surv, info = exclusion(a0, '3. exclusion') + need(not surv, name + ': integer solutions survive above the pattern optimum') + out['exclusion'] = info + I, K = best, RB + print('[%s] 3. no integer pattern solution survives at optimum + 1e-15: every legal whole-helper fill has ' + 'b <= optimum root + 1e-15' % name) + want = {str(k): v for k, v in sorted(I.items())} + + # ---- negative control ----------------------------------------------------------------------------------------- + a1 = K - Fraction(1, 10 ** 12) + T1, surv1, info1 = exclusion(a1, 'control') + need(any({str(k): v for k, v in s['idle'].items()} == want for s in surv1) and wmu_idle(I, a1, True) < W, + name + ': negative control: below its root the claimed fill must survive the exclusion') + norm = lambda d: json.dumps({str(k): v for k, v in d.items()}, sort_keys=True) + others = sorted({norm(s['idle']) for s in surv1} - {norm(want)}) + need(not others, name + ': a different idle multiset survives at kappa - 1e-12: %s' % others) + out['negative_control'] = dict(a=str(a1), survivors=len(surv1), claimed_fill_survives=True, + survivor_idle_multisets=info1['survivor_idle_multisets']) + print('[%s] control: %d survivors at kappa - 1e-12 (degenerate copies of %d heavy part(s)), all with the ' + 'optimal idle multiset (uniqueness within 1e-12)' % (name, len(surv1), info1['distinct_heavy_parts'])) + out['conclusion'] = ('Every legal whole-helper owner fill of the ' + claim['words'] + ' on the unchanged T74 ' + 'template has b <= %s + 1e-15 (pattern-IP optimum, idle %s); the published fill is %s.' + % (float(RB), out['pattern_optimum']['idle'], + 'that optimum' if RB == Fraction(froot(CLAIMS[name]['idle'])).limit_denominator(10 ** 30) or + out['pattern_optimum']['gain_over_claim'] < 1e-15 else + 'below it by %.3e' % out['pattern_optimum']['gain_over_claim'])) + return out, out['pattern_optimum']['gain_over_claim'] + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--out', action='store_true') + args = ap.parse_args() + t0 = time.time() + C = load_lp() + P = C.P + W = C.W_LIVE + base = C.CASES['pr2322_control'] + need(dict(base['inv']) == CLAIMS['pr2374']['inv'] and dict(base['pg']) == CLAIMS['pr2374']['profile'] == + dict(base['pe']), 'PR2374 claim data equals the PR2387/PR2402 recounted PR2322 case') + out = dict(claims={}) + surv = {} + for name in CLAIMS: + out['claims'][name], surv[name] = audit(C, P, W, name) + out['scope'] = ('Pattern relaxation of all whole-helper fills (windows, families and ports dropped), so each bound ' + 'covers every legal fill of that claim\'s words; realization of each fill and the word data ' + '(profile, inventory) are the claimants\' own checks (PR2322 data recounted in PR2402).') + out['python'] = sys.version.split()[0] + if args.out: + with open(os.path.join(HERE, 'owner_optimum.receipt.json'), 'w') as f: + f.write(json.dumps(out, indent=1, sort_keys=True) + '\n') + print('runtime %.1fs' % (time.time() - t0)) + need(surv['pr2374'] < 1e-15, 'PR2374 fill is the pattern optimum') + print('PASS_T74_OWNER_OPTIMUM pr2374:claim_is_optimum pr2435:optimum_gain=%+.3e unique_within_1e-12 no_new_kappa' + % surv['pr2435']) + return 0 + + +if __name__ == '__main__': + try: + sys.exit(main()) + except Fail as e: + sys.stdout.write('FAIL_T74_OWNER_OPTIMUM %s\n' % e) + sys.exit(1) diff --git a/research/t74-owner-fill-optimality/owner_optimum.receipt.json b/research/t74-owner-fill-optimality/owner_optimum.receipt.json new file mode 100644 index 0000000000..6e610faeb6 --- /dev/null +++ b/research/t74-owner-fill-optimality/owner_optimum.receipt.json @@ -0,0 +1,295 @@ +{ + "claims": { + "pr2374": { + "conclusion": "Every legal whole-helper owner fill of the PR2322 words (recounted in PR2402) on the unchanged T74 template has b <= 0.0016971949509017592 + 1e-15 (pattern-IP optimum, idle {'1': 21978, '3': 8592, '5': 2552, '32': 1, '48': 24560}); the published fill is that optimum.", + "exclusion": { + "T": 0.00015474574765232094, + "a0": "933042791560150585892013/549755813888000000000000000", + "basis": [ + "(8, (8,))", + "(16, (8, 8))", + "(16, (7, 9))", + "(32, (9, 9, 9))", + "(32, (8, 8, 8, 8))", + "(32, (5, 9, 9, 9))", + "(32, (4, 9, 9, 9))", + "(48, ())", + "(48, (9, 9, 9, 9, 9))" + ], + "degenerate": [ + "(32, (7, 8, 8, 9))", + "(32, (7, 7, 9, 9))" + ], + "degenerate_representation_integral": true, + "det_lcm": 5, + "distinct_heavy_parts": 0, + "dual_repair": { + "16": 0.0, + "32": 0.0, + "48": -1.0063810643125138e-17, + "8": 0.0 + }, + "heavy": { + "(32, (4, 8, 9, 9))": { + "max_count": 1, + "rc": 0.0001335186657766286 + }, + "(32, (8, 9, 9))": { + "max_count": 1, + "rc": 0.0001027801043596668 + }, + "(48, (4, 8, 9, 9, 9, 9))": { + "max_count": 2, + "rc": 5.487798265415046e-05 + }, + "(48, (8, 9, 9, 9, 9))": { + "max_count": 1, + "rc": 0.0001133684986005809 + }, + "(48, (9,))": { + "max_count": 1, + "rc": 0.00014964300833992533 + } + }, + "survivor_idle_multisets": [], + "survivors": 0 + }, + "idle": { + "1": 21978, + "3": 8592, + "5": 2552, + "32": 1, + "48": 24560 + }, + "inventory": { + "4": 33, + "5": 9, + "7": 38, + "8": 114, + "9": 240 + }, + "kappa": "84859747545088521329704093865477059989146272371876148529/50000000000000000000000000000000000000000000000000000000000", + "negative_control": { + "a": "7464342328078760129521/4398046511104000000000000", + "claimed_fill_survives": true, + "survivor_idle_multisets": [ + "{\"1\": 21978, \"3\": 8592, \"5\": 2552, \"32\": 1, \"48\": 24560}" + ], + "survivors": 25 + }, + "object": "pr2374 owner fill on the PR2322 words (recounted in PR2402): optimality over all whole-helper fills", + "pattern_optimum": { + "candidates_better_than_claim": 0, + "gain_over_claim": -1.1223772586967725e-17, + "idle": { + "1": 21978, + "3": 8592, + "32": 1, + "48": 24560, + "5": 2552 + }, + "pattern_change_vs_lp_basis": { + "(32, ())": 1 + }, + "pattern_counts": { + "(16, (7, 9))": 25296, + "(16, (8, 8))": 7856, + "(32, ())": 1, + "(32, (4, 9, 9, 9))": 21978, + "(32, (5, 9, 9, 9))": 5994, + "(32, (7, 7, 9, 9))": 4, + "(32, (7, 8, 8, 9))": 4, + "(32, (8, 8, 8, 8))": 2619, + "(32, (9, 9, 9))": 2552, + "(48, ())": 24560, + "(48, (9, 9, 9, 9, 9))": 8592, + "(8, (8,))": 49728 + }, + "ranked": [ + { + "idle": { + "1": 21978, + "3": 8592, + "32": 1, + "48": 24560, + "5": 2552 + }, + "root": 0.0016971949509017592 + } + ], + "root_bracket": [ + "933042791559051074264237/549755813888000000000000000", + "933042791560150585892013/549755813888000000000000000" + ] + }, + "profile": { + "1": 2335, + "2": 512, + "3": 426, + "4": 120, + "5": 38, + "8": 8 + }, + "root_bracket": [ + "84859747545038521329704093865477059989146272371876148529/50000000000000000000000000000000000000000000000000000000000", + "84859747545138521329704093865477059989146272371876148529/50000000000000000000000000000000000000000000000000000000000" + ] + }, + "pr2435": { + "conclusion": "Every legal whole-helper owner fill of the PR2435 words (24 copy-buffer entrances raised; profile and inventory as published) on the unchanged T74 template has b <= 0.0016985119240027768 + 1e-15 (pattern-IP optimum, idle {'1': 20822, '3': 6694, '5': 2, '48': 25302}); the published fill is below it by 5.803e-10.", + "exclusion": { + "T": 8.787264375162669e-05, + "a0": "933766805179169140579513/549755813888000000000000000", + "basis": [ + "(8, (8,))", + "(16, (7, 9))", + "(32, (8, 8, 8, 8))", + "(32, (7, 7, 9, 9))", + "(32, (5, 9, 9, 9))", + "(32, (4, 9, 9, 9))", + "(48, ())", + "(48, (9, 9, 9, 9, 9))", + "(48, (4, 8, 9, 9, 9, 9))" + ], + "degenerate": [ + "(16, (8, 8))", + "(32, (7, 8, 8, 9))" + ], + "degenerate_representation_integral": false, + "det_lcm": 50, + "distinct_heavy_parts": 0, + "dual_repair": { + "16": 0.0, + "32": 0.0, + "48": -8.68383704707395e-18, + "8": 0.0 + }, + "heavy": { + "(32, (9, 9, 9))": { + "max_count": 1, + "rc": 4.393641631145471e-05 + } + }, + "survivor_idle_multisets": [], + "survivors": 0 + }, + "idle": { + "1": 20824, + "3": 6695, + "5": 1, + "48": 25302 + }, + "inventory": { + "4": 33, + "5": 9, + "7": 62, + "8": 90, + "9": 240 + }, + "kappa": "849255671848814664525866907093872315402755548352296655639/500000000000000000000000000000000000000000000000000000000000", + "negative_control": { + "a": "7470134437030908567021/4398046511104000000000000", + "claimed_fill_survives": true, + "survivor_idle_multisets": [ + "{\"1\": 20822, \"3\": 6694, \"5\": 2, \"48\": 25302}" + ], + "survivors": 1250 + }, + "object": "pr2435 owner fill on the PR2435 words (24 copy-buffer entrances raised; profile and inventory as published): optimality over all whole-helper fills", + "pattern_optimum": { + "candidates_better_than_claim": 4, + "gain_over_claim": 5.803051475115292e-10, + "idle": { + "1": 20822, + "3": 6694, + "48": 25302, + "5": 2 + }, + "pattern_change_vs_lp_basis": { + "(32, (9, 9, 9))": 2 + }, + "pattern_counts": { + "(16, (7, 9))": 33103, + "(16, (8, 8))": 49, + "(32, (4, 9, 9, 9))": 20822, + "(32, (5, 9, 9, 9))": 5994, + "(32, (7, 7, 9, 9))": 4070, + "(32, (7, 8, 8, 9))": 49, + "(32, (8, 8, 8, 8))": 2215, + "(32, (9, 9, 9))": 2, + "(48, ())": 25302, + "(48, (4, 8, 9, 9, 9, 9))": 1156, + "(48, (9, 9, 9, 9, 9))": 6694, + "(8, (8,))": 49728 + }, + "ranked": [ + { + "idle": { + "1": 20822, + "3": 6694, + "48": 25302, + "5": 2 + }, + "root": 0.0016985119240027768 + }, + { + "idle": { + "1": 20823, + "3": 6695, + "48": 25302, + "6": 1 + }, + "root": 0.0016985116737687211 + }, + { + "idle": { + "1": 20823, + "3": 6694, + "4": 1, + "48": 25302, + "5": 1 + }, + "root": 0.0016985116184565219 + }, + { + "idle": { + "1": 20822, + "2": 1, + "3": 6695, + "48": 25302, + "5": 1 + }, + "root": 0.0016985115131949446 + }, + { + "idle": { + "1": 20824, + "3": 6695, + "48": 25302, + "5": 1 + }, + "root": 0.0016985113436976396 + } + ], + "root_bracket": [ + "933766805178069628951737/549755813888000000000000000", + "933766805179169140579513/549755813888000000000000000" + ] + }, + "profile": { + "1": 2359, + "2": 632, + "3": 330, + "4": 120, + "5": 38, + "8": 8 + }, + "root_bracket": [ + "849255671848314664525866907093872315402755548352296655639/500000000000000000000000000000000000000000000000000000000000", + "849255671849314664525866907093872315402755548352296655639/500000000000000000000000000000000000000000000000000000000000" + ] + } + }, + "python": "3.14.4", + "scope": "Pattern relaxation of all whole-helper fills (windows, families and ports dropped), so each bound covers every legal fill of that claim's words; realization of each fill and the word data (profile, inventory) are the claimants' own checks (PR2322 data recounted in PR2402)." +} diff --git a/research/t74-owner-fill-optimality/vendor/pr2387/ceiling_lp.py b/research/t74-owner-fill-optimality/vendor/pr2387/ceiling_lp.py new file mode 100644 index 0000000000..4836235866 --- /dev/null +++ b/research/t74-owner-fill-optimality/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-owner-fill-optimality/vendor/pr2387/vendor/iter3/price_check.py b/research/t74-owner-fill-optimality/vendor/pr2387/vendor/iter3/price_check.py new file mode 100644 index 0000000000..708753e770 --- /dev/null +++ b/research/t74-owner-fill-optimality/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())