diff --git a/research/complex-k492-frame-bound/README.md b/research/complex-k492-frame-bound/README.md new file mode 100644 index 0000000000..0e1b71fa51 --- /dev/null +++ b/research/complex-k492-frame-bound/README.md @@ -0,0 +1,67 @@ +# Fixed-order A/B frame exclusion for the selected PR626 complex providers + +**Scoped negative result; no new κ.** Base `66849e1475c930fd7732b1a0067ffee7e1e95f60`. Sprint track: complex supplier (OS seed 23). + +## Claim + +Take the emitted programs of the two selected #626 complex providers: **jp8**, used in 64 of the 72 calls, and **ck**, used in 8. Use both orientations. The macro list, order and operands stay fixed, as do every start frame, final frame and target level, each centre chain, and the frame of every macro outside phases A and B. Any frame in F_2^9 may then be assigned to any A or B scalar macro, simultaneously. No assignment that is legal under `hpe_audit_local.py`'s frame rules yields a native complex moment below one at + + b_next = 102387919519255428911/62500000000000000000000 + +This is the next 10^-24 grid point above #626's accepted endpoint. With owners, widths, the bit supplier and the outer assembly unchanged, frame-only reassignment therefore cannot raise the binding complex endpoint, and so cannot raise the selected κ. + +## Proof (finite, exact) + +1. **Domains.** Forward joins from the fixed starts and pins give `lo_i`, and backward meets from the finals and pins give `hi_i`. Every legal frame satisfies `lo_i <= G_i <= hi_i`. In these words `dim(hi/lo) <= 3`. The verifier enumerates every subspace in each interval and checks completeness: 2, 5 or 16 choices per macro (`model.py`). +2. **LP.** For each component of free macros, the local-polytope LP uses variables x(i,G), plus nested pair variables y on consecutive macros of a register (counted with multiplicity). Every legal assignment is a 0/1 point of this LP. Each register's total climb is fixed, so the paid local moment equals sum n_k c_k plus a constant, where c_k = k^(1-b) - k. The common positive factor m^b/(mW) is dropped. +3. **Duals.** Each component has a rational dual whose entries are linear forms in c_2..c_9. The verifier checks two things. First, every reduced cost is >= 0 at b_next, using two rational engines: its own atanh/alternating-series engine, and the pinned repository `moment.py`. Second, the dual objective equals the literal #626 baseline as an exact coefficient-vector identity. By weak duality, every legal assignment costs at least as much as the baseline. +4. **Global step.** Using the pinned #626 `ASSEMBLY.json` profile, both engines put the baseline global moment minus one at about +6.49e-25 at b_next. Every child term increases with b. So for each call, each reassignment has a local moment at least the baseline's at b_next, and the reassigned supplier is rejected at b_next and above. + +Small components (63 for jp8 and 96 for ck, per orientation) are also brute-forced over all legal assignments as an independent cross-check. + +## Reproduce + +```sh +python3 -B research/complex-k492-frame-bound/verify.py # committed inputs, ~30 s, stdlib only +python3 -B research/complex-k492-frame-bound/verify.py --controls # six controls must be rejected +``` + +Expected: `PASS_FIXED_ORDER_AB_FRAME_EXCLUSION_PR626` and `PASS_CONTROLS 6 of 6 rejected`. `--work DIR` checks fresh outputs of `research/complex-k492-owner-repair/verify.sh DIR` instead. + +The inputs are the jp8/ck `CANONICAL-WORD` and `LOCAL-PROGRAMS` files. Their gzip SHA-256 equals the hashes recorded in `research/community-k492-audit/pr626/replay/mixed-global/base/providers/*/INDEPENDENT-LOCAL-REPLAY.json`, and the decompressed payload hashes are pinned in `SOURCES.json`. + +This was validated in two ways: the full #626 provider replay was run fresh on macOS with Python 3.12, and its outputs matched; and the verifier was run on Python 3.11 and 3.15. Running with `-O` is refused. + +The six controls are: +- a dropped component +- an inflated dual +- an incomplete domain +- the accepted (rather than next) endpoint +- a legal but worse baseline, which the duals must not certify +- the wrong word + +`gen_duals.py` (needs highspy/scipy) nominates the duals; it is deterministic, reproducing the pinned payload hash. `explore/exact.py` (needs ortools) solves the same exact model with CP-SAT and reports the baseline objective as optimal for both words. It is a solver cross-check, not part of the proof. + +## Exploratory findings (not shipped as checks) + +- A per-register rank-path relaxation, which drops shared geometry, leaves gaps on 410 jp8 registers. +- A coupled dimension-only relaxation claims a large spurious gain, which shrinks after pair-span cuts but does not vanish. +- Greedy and annealed block moves and a flag-structured frame family all found no improvement. + +So the geometric subspace constraints are what close the gap, which is why the full subspace LP is needed. + +## Scope + +Not covered: +- scalar rewrites, reordering, or changed cuts or centres +- frames of zero-frame precondition, cleanup-tail and full-frame-cleanup macros +- changed starts or finals (and so widths), owners, hosting or the invoice +- the bit supplier, other words (for example the open #645/#659/#685 lineages), or other outer theorems + +The result holds at the fixed exponent b_next, not for all exponents. All inherited all-size, compiler, realization, hosting, precision, tape and analytic assumptions remain. This is a finite certificate, not a Lean proof. + +## Credit + +The method follows chafreaky's #557 (`research/frame-domain-ceiling`, PR551 word): complete F_2 domains, an LP relaxation and symbolic exact duals. This package is a new implementation against the emitted #626 programs. Concurrent #698 (thakrarsagar) proves ck B-phase optimality at fixed end-of-B frames for all exponents; this result independently corroborates it at b_next and adds jp8, joint A/B freedom and the global next-tick exclusion. #661 (yuj1r0) is the bit analogue. + +The suppliers and their lineage are Jeremy Kothe (#622), Chafik Boukhalfa (#626), DreamingOfClouds, icekylinx and the selected-record contributors. Prepared with substantial AI assistance (Anthropic Claude). Apache-2.0. diff --git a/research/complex-k492-frame-bound/RESULT.json b/research/complex-k492-frame-bound/RESULT.json new file mode 100644 index 0000000000..9b0edbae36 --- /dev/null +++ b/research/complex-k492-frame-bound/RESULT.json @@ -0,0 +1,102 @@ +{ + "accepted_complex_endpoint": "65528268492323474503/40000000000000000000000", + "excluded_complex_endpoint": "102387919519255428911/62500000000000000000000", + "global_moment_minus_one_at_excluded": { + "engine_a": [ + "0.0000000000000000000000006493109174788603", + "0.0000000000000000000000006493109174788604" + ], + "repo_engine": [ + "0.0000000000000000000000006493109174788603", + "0.0000000000000000000000006493109174788604" + ] + }, + "programs": { + "ck/backward": { + "brute_forced_components": 96, + "brute_forced_legal_assignments": 629, + "components": 114, + "distinct_reduced_cost_forms": 543, + "domain_frames": 2694, + "free_macros_with_choices": 884, + "local_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "lp_columns": 9713, + "lp_rows": 7288, + "macros": 22748, + "register_rank_mass": 5650 + }, + "ck/forward": { + "brute_forced_components": 96, + "brute_forced_legal_assignments": 629, + "components": 114, + "distinct_reduced_cost_forms": 543, + "domain_frames": 2694, + "free_macros_with_choices": 884, + "local_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "lp_columns": 9713, + "lp_rows": 7288, + "macros": 22748, + "register_rank_mass": 5650 + }, + "jp8/backward": { + "brute_forced_components": 63, + "brute_forced_legal_assignments": 133, + "components": 81, + "distinct_reduced_cost_forms": 432, + "domain_frames": 3518, + "free_macros_with_choices": 1296, + "local_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "lp_columns": 12433, + "lp_rows": 10228, + "macros": 23505, + "register_rank_mass": 5694 + }, + "jp8/forward": { + "brute_forced_components": 63, + "brute_forced_legal_assignments": 133, + "components": 81, + "distinct_reduced_cost_forms": 432, + "domain_frames": 3518, + "free_macros_with_choices": 1296, + "local_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "lp_columns": 12433, + "lp_rows": 10228, + "macros": 23505, + "register_rank_mass": 5694 + } + }, + "scope": "Every simultaneous reassignment of A/B scalar-macro frames of the emitted PR626 jp8 and ck provider programs, with macro list/order/operands, starts, finals, target levels, centre chains and all non-A/B macro frames fixed. No scalar rewrite, reordering, width/owner/hosting change, other supplier or outer theorem is covered.", + "status": "PASS_FIXED_ORDER_AB_FRAME_EXCLUSION_PR626" +} diff --git a/research/complex-k492-frame-bound/SOURCES.json b/research/complex-k492-frame-bound/SOURCES.json new file mode 100644 index 0000000000..3e06410474 --- /dev/null +++ b/research/complex-k492-frame-bound/SOURCES.json @@ -0,0 +1,44 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "selected_record": { + "path": "certificates/selected-result.json", + "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "assembly": { + "path": "research/community-k492-audit/pr626/replay/ASSEMBLY.json", + "sha256": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e" + }, + "duals_payload_sha256": "de05d858cb1670712847f6618752a08cb320cb55149c47d87dfe044e8aae6b4d", + "inputs": { + "jp8": { + "CANONICAL-WORD": { + "payload_sha256": "fb4a8d14ed2a8048698bea6ae16f86163a1aa6c80f2eb622222eee5cdbce9b3b", + "gzip_sha256": "7a3fec1022d3b2b1bd986302a327735ec521d17b043f4a5acb96253a56f6193c" + }, + "LOCAL-PROGRAMS": { + "payload_sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b", + "gzip_sha256": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98" + }, + "pr626_receipt": { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/INDEPENDENT-LOCAL-REPLAY.json", + "canonical_word_sha256": "7a3fec1022d3b2b1bd986302a327735ec521d17b043f4a5acb96253a56f6193c", + "local_programs_sha256": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98" + } + }, + "ck": { + "CANONICAL-WORD": { + "payload_sha256": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7", + "gzip_sha256": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45" + }, + "LOCAL-PROGRAMS": { + "payload_sha256": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900", + "gzip_sha256": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3" + }, + "pr626_receipt": { + "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/INDEPENDENT-LOCAL-REPLAY.json", + "canonical_word_sha256": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45", + "local_programs_sha256": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3" + } + } + } +} diff --git a/research/complex-k492-frame-bound/data/DUALS.json.gz b/research/complex-k492-frame-bound/data/DUALS.json.gz new file mode 100644 index 0000000000..381f587eee Binary files /dev/null and b/research/complex-k492-frame-bound/data/DUALS.json.gz differ diff --git a/research/complex-k492-frame-bound/data/ck/CANONICAL-WORD.json.gz b/research/complex-k492-frame-bound/data/ck/CANONICAL-WORD.json.gz new file mode 100644 index 0000000000..58cd1be8f2 Binary files /dev/null and b/research/complex-k492-frame-bound/data/ck/CANONICAL-WORD.json.gz differ diff --git a/research/complex-k492-frame-bound/data/ck/LOCAL-PROGRAMS.json.gz b/research/complex-k492-frame-bound/data/ck/LOCAL-PROGRAMS.json.gz new file mode 100644 index 0000000000..61ef73c1f9 Binary files /dev/null and b/research/complex-k492-frame-bound/data/ck/LOCAL-PROGRAMS.json.gz differ diff --git a/research/complex-k492-frame-bound/data/jp8/CANONICAL-WORD.json.gz b/research/complex-k492-frame-bound/data/jp8/CANONICAL-WORD.json.gz new file mode 100644 index 0000000000..7fd7cd1fef Binary files /dev/null and b/research/complex-k492-frame-bound/data/jp8/CANONICAL-WORD.json.gz differ diff --git a/research/complex-k492-frame-bound/data/jp8/LOCAL-PROGRAMS.json.gz b/research/complex-k492-frame-bound/data/jp8/LOCAL-PROGRAMS.json.gz new file mode 100644 index 0000000000..e22169a163 Binary files /dev/null and b/research/complex-k492-frame-bound/data/jp8/LOCAL-PROGRAMS.json.gz differ diff --git a/research/complex-k492-frame-bound/engine.py b/research/complex-k492-frame-bound/engine.py new file mode 100644 index 0000000000..ba0b796e38 --- /dev/null +++ b/research/complex-k492-frame-bound/engine.py @@ -0,0 +1,115 @@ +"""Two rational enclosures of the adjusted child cost c_k(b) = k^(1-b) - k (standard library only). + +For the complex recurrence the width-k child contributes M_k = (k/(mW)) (m/k)^b, so +M_k - k M_1 = (m^b/(mW)) c_k with a positive common factor. Since every register's +total climb is fixed, minimising sum n_k M_k is minimising sum n_k c_k (c_0 = c_1 = 0). + +Engine A: own atanh logarithm series and alternating exponential series. +Engine B: the pinned repository engine (research/complex-k492-owner-repair/vendor/multicold/engines/moment.py), + via its exact moment() enclosures of M_k and M_1. +""" +import hashlib, importlib.util +from functools import lru_cache +from fractions import Fraction as Q +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +REPO_ENGINE = ROOT / 'research/complex-k492-owner-repair/vendor/multicold/engines/moment.py' +REPO_ENGINE_SHA256 = '81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482' +B_ACCEPTED = Q('65528268492323474503/40000000000000000000000') # PR626 native complex endpoint +B_NEXT = Q('102387919519255428911/62500000000000000000000') # next 10^-24 grid point, rejected by PR626 +M_DIM, W_LIVE = 73, 7168 +DEN = Q(1, 2 ** 200) + + +@lru_cache(None) +def _ln_bounds(k): + """ln k = 2 atanh(z), z=(k-1)/(k+1): positive odd series; tail <= next term / (1 - z^2).""" + if k == 1: return Q(0), Q(0) + z = Q(k - 1, k + 1); s = Q(0); t = z; j = 1 + while True: + s += t / j; t *= z * z; j += 2 + tail = t / j / (1 - z * z) + if tail < DEN: return 2 * s, 2 * (s + tail) + + +def _down(x, bits=256): + return Q((x.numerator << bits) // x.denominator, 1 << bits) + + +def _up(x, bits=256): + return -_down(-x, bits) + + +def _exp_neg_bounds(x): + """bounds of exp(-x) for 0 <= x < 1: alternating series with decreasing terms. + Callers pass dyadic x; exp(-x) is decreasing, so outward rounding of x is done by the caller.""" + assert 0 <= x < 1 + s = Q(1); t = Q(1); j = 1; lo = hi = None + while True: + t = t * x / j; s = s - t if j % 2 else s + t + if j % 2: lo = s + else: hi = s + if lo is not None and hi is not None and t < DEN: return lo, hi + j += 1 + + +def engine_a(b): + out = {} + for k in range(0, 10): + if k < 2: out[k] = (Q(0), Q(0)); continue + l, u = _ln_bounds(k) + e_lo, _ = _exp_neg_bounds(_up(b * u)); _, e_hi = _exp_neg_bounds(_down(b * l)) + out[k] = (k * e_lo - k, k * e_hi - k) + return out + + +def _repo(): + spec = importlib.util.spec_from_file_location('repo_moment', REPO_ENGINE) + m = importlib.util.module_from_spec(spec); spec.loader.exec_module(m); return m + + +def engine_b(b): + """c_k scaled by (mW)/m^b: uses M_k enclosures; returns enclosures of (mW) (M_k - k M_1) / m^b.""" + R = _repo(); out = {} + l1, u1 = R.moment({1: 1}, M_DIM, W_LIVE, b) + # m^b bounds from the same engine: M_1 = (1/(mW)) m^b + mb_lo, mb_hi = l1 * M_DIM * W_LIVE, u1 * M_DIM * W_LIVE + for k in range(0, 10): + if k < 2: out[k] = (Q(0), Q(0)); continue + lk, uk = R.moment({k: 1}, M_DIM, W_LIVE, b) + lo = (lk - k * u1) * M_DIM * W_LIVE; hi = (uk - k * l1) * M_DIM * W_LIVE + # divide by m^b > 0 (both bounds are negative for k >= 2) + assert hi < 0 + out[k] = (lo / mb_lo, hi / mb_hi) + return out + + +def adjusted_bounds(b=B_NEXT): + A = engine_a(b) + return {k: A[k][0] for k in A}, {k: A[k][1] for k in A} + + +def nonnegative(v, engines): + """sum_{k=2..9} v[k-2] c_k >= 0, proved by every engine (zero form accepted symbolically)""" + if not any(v): return True + for E in engines: + s = Q(0) + for k in range(2, 10): + x = v[k - 2] + if x: s += x * (E[k][0] if x > 0 else E[k][1]) + if s < 0: return False + return True + + +def moment_a(H, b, m=M_DIM, W=W_LIVE): + """engine-A enclosure of the native moment sum_r (r n/(mW)) (m/r)^b""" + lo = hi = Q(0) + lm_lo, lm_hi = _ln_bounds(m) + for r, n in H.items(): + lr_lo, lr_hi = _ln_bounds(r) + x_lo, x_hi = b * (lm_lo - lr_hi), b * (lm_hi - lr_lo) # b ln(m/r) >= 0 + # exp(x) = 1/exp(-x) + e1_lo, e1_hi = _exp_neg_bounds(_up(x_hi)); e2_lo, e2_hi = _exp_neg_bounds(_down(x_lo)) + p = Q(r * n, m * W); lo += p / e2_hi; hi += p / e1_lo + return lo, hi diff --git a/research/complex-k492-frame-bound/explore/exact.py b/research/complex-k492-frame-bound/explore/exact.py new file mode 100644 index 0000000000..e15d7a5742 --- /dev/null +++ b/research/complex-k492-frame-bound/explore/exact.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +"""Discovery cross-check: exact fixed-order A/B frame model solved by CP-SAT (needs ortools). + +Not used by verify.py; CP-SAT optimality is a solver report, not a certificate. +Every free macro picks one subspace of its complete interval [lo, hi]; consecutive +free macros on a register must be nested. Objective: maximise -sum c_k(b) over +register climbs (c_k = k^(1-b) - k), scaled to integers. + +usage: explore/exact.py DATA_WORD_DIR forward|backward SECONDS +""" +import sys +from collections import Counter +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parents[1])) +import model as Mo +import engine as E +from ortools.sat.python import cp_model + +lo_, hi_ = E.adjusted_bounds() +W = {k: round(-float(lo_[k]) * 10 ** 9) for k in range(10)} + + +def solve(c, F, nodes, lo, hi, seconds): + m = cp_model.CpModel(); n = 2 * c['v'] + c['R']; seq = Mo.chains(c, nodes) + free = [i for i, nd in enumerate(nodes) if nd[1] is None and len(lo[i]) < len(hi[i])] + dom = {i: Mo.between(lo[i], hi[i]) for i in free}; x = {}; dv = {} + for i in free: + x[i] = m.NewIntVar(0, len(dom[i]) - 1, ''); dims = [len(g) for g in dom[i]] + dv[i] = m.NewIntVar(min(dims), max(dims), ''); m.AddElement(x[i], dims, dv[i]); m.AddHint(x[i], dom[i].index(nodes[i][2])) + D = lambda i: dv[i] if i in dv else len(nodes[i][2]) + obj = []; done = set() + for r in range(n): + s = seq[r] + for a, b in zip(s, s[1:]): + if a in x and b in x and (a, b) not in done: + done.add((a, b)) + m.AddAllowedAssignments([x[a], x[b]], [(p, q) for p, g in enumerate(dom[a]) for q, h in enumerate(dom[b]) if Mo.contains(h, g)]) + chain = [len(F[c['start'][r]])] + [D(i) for i in s] + [len(F[c['final'][r]])] + for u, w in zip(chain, chain[1:]): + if isinstance(u, int) and isinstance(w, int): obj.append(W[w - u]); continue + zs = [(t, m.NewBoolVar('')) for t in range(10)] + m.AddExactlyOne(z for t, z in zs); m.Add(w - u == sum(t * z for t, z in zs)); obj.extend(W[t] * z for t, z in zs) + m.Maximize(sum(obj)) + s = cp_model.CpSolver(); s.parameters.max_time_in_seconds = seconds; s.parameters.num_workers = 8; st = s.Solve(m) + fr = [nd[2] for nd in nodes] + for i in free: fr[i] = dom[i][s.Value(x[i])] + return s.StatusName(st), s.ObjectiveValue(), s.BestObjectiveBound(), fr + + +if __name__ == '__main__': + c, ev = Mo.load(sys.argv[1], sys.argv[2]); F, nodes, climbs, center = Mo.extract(c, ev); lo, hi = Mo.intervals(c, F, nodes) + H0 = Mo.profile(c, F, nodes, [nd[2] for nd in nodes]); base = sum(W[k] * z for k, z in H0.items()) + st, val, bd, fr = solve(c, F, nodes, lo, hi, float(sys.argv[3])) + H1 = Mo.profile(c, F, nodes, fr) + print(st, 'objective', val, 'bound', bd, 'baseline', base, 'solution profile', dict(sorted(H1.items())), + 'changed frames', sum(fr[i] != nd[2] for i, nd in enumerate(nodes))) diff --git a/research/complex-k492-frame-bound/gen_duals.py b/research/complex-k492-frame-bound/gen_duals.py new file mode 100644 index 0000000000..9acd742885 --- /dev/null +++ b/research/complex-k492-frame-bound/gen_duals.py @@ -0,0 +1,67 @@ +#!/usr/bin/env python3 +"""Nominate exact symbolic LP duals for every component (discovery only; uses highspy/scipy). + +The verifier (verify.py) uses only the standard library and the shipped rational duals. +""" +import argparse, gzip, json, sys +from fractions import Fraction as Q +from pathlib import Path +import numpy as np +import highspy +from scipy.sparse import csc_matrix +from scipy.sparse.linalg import splu +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import model as Mo +from engine import adjusted_bounds + + +def solve_component(comp, cnum): + cols, rhs = comp['cols'], comp['rhs']; nr, nc = len(rhs), len(cols) + cost = np.array([sum(v * cnum[k] for k, v in enumerate(col[1])) for col in cols]) + starts = [0]; idx = []; val = [] + for col in cols: + for r, a in col[2]: idx.append(r); val.append(float(a)) + starts.append(len(idx)) + lp = highspy.HighsLp(); lp.num_col_ = nc; lp.num_row_ = nr + lp.col_cost_ = cost; lp.col_lower_ = np.zeros(nc); lp.col_upper_ = np.full(nc, highspy.kHighsInf) + lp.row_lower_ = np.array(rhs, float); lp.row_upper_ = np.array(rhs, float) + lp.a_matrix_.format_ = highspy.MatrixFormat.kColwise; lp.a_matrix_.start_ = np.array(starts, np.int32) + lp.a_matrix_.index_ = np.array(idx, np.int32); lp.a_matrix_.value_ = np.array(val) + h = highspy.Highs(); h.setOptionValue('output_flag', False); h.setOptionValue('primal_feasibility_tolerance', 1e-10) + h.setOptionValue('dual_feasibility_tolerance', 1e-10); h.passModel(lp); h.run() + assert h.getModelStatus() == highspy.HighsModelStatus.kOptimal + b = h.getBasis(); basic_cols = [j for j in range(nc) if b.col_status[j] == highspy.HighsBasisStatus.kBasic] + basic_rows = [i for i in range(nr) if b.row_status[i] == highspy.HighsBasisStatus.kBasic] + assert len(basic_cols) + len(basic_rows) == nr + # Equations on q: A_j^T q = c_j for basic columns j; q_i = 0 for basic (redundant) rows i. + R = []; C = []; V = []; eq = 0 + for j in basic_cols: + for r, a in cols[j][2]: R.append(eq); C.append(r); V.append(float(a)) + eq += 1 + for i in basic_rows: R.append(eq); C.append(i); V.append(1.0); eq += 1 + Msys = csc_matrix((V, (R, C)), shape=(nr, nr)); lu = splu(Msys) + duals = [] + for k in range(8): + rhs_k = np.array([float(cols[j][1][k]) for j in basic_cols] + [0.0] * len(basic_rows)) + duals.append(lu.solve(rhs_k)) + D = [[Q(float(duals[k][i])).limit_denominator(10 ** 6) for k in range(8)] for i in range(nr)] + return D, h.getInfo().objective_function_value + + +if __name__ == '__main__': + ap = argparse.ArgumentParser(); ap.add_argument('--work', type=Path, required=True); ap.add_argument('--out', type=Path, required=True) + a = ap.parse_args(); out = {} + lower, upper = adjusted_bounds() + cnum = [float((lower[k] + upper[k]) / 2) for k in range(2, 10)] + for word in ('jp8', 'ck'): + for prog in ('forward', 'backward'): + c, ev = Mo.load(a.work / (word + '-local'), prog) + F, nodes, climbs, center = Mo.extract(c, ev); lo, hi = Mo.intervals(c, F, nodes) + comps, const, base, free = Mo.lp(c, F, nodes, lo, hi) + certs = [] + for comp in comps: + D, val = solve_component(comp, cnum) + certs.append([[str(x) for x in row] for row in D]) + out['%s/%s' % (word, prog)] = certs + print(word, prog, 'components', len(comps), 'rows', sum(len(x['rhs']) for x in comps), flush=True) + a.out.write_bytes(gzip.compress(json.dumps(out, separators=(',', ':'), sort_keys=True).encode(), mtime=0)) diff --git a/research/complex-k492-frame-bound/model.py b/research/complex-k492-frame-bound/model.py new file mode 100644 index 0000000000..51ac5ef897 --- /dev/null +++ b/research/complex-k492-frame-bound/model.py @@ -0,0 +1,236 @@ +"""Exact fixed-order frame model of one emitted complex provider program (standard library only). + +Prepared for the CrocSwap integer-mult-bounds sprint with substantial AI assistance (Anthropic Claude). Apache-2.0. + +Input: CANONICAL-WORD.json.gz and LOCAL-PROGRAMS.json.gz written by +research/complex-k492-owner-repair (hpe_emit_local.py). The emitted program is the +object audited by that package's hpe_audit_local.py, whose frame rules are: + * an L-register operand of a scalar macro is exactly at the macro frame; + * frames change only through climb events, which are strictly nested; + * a private C register keeps one frame between centre events; + * targets sit at their levels when phase 'centers' opens; every register sits at + its final frame when 'full_frame_cleanup' opens; starts are fixed. +Class: every scalar macro of phases A and B may take any frame; the frames of all +other macros, all start/final frames, target levels and private-centre frames stay +fixed, as do the macro list, order and operands. Climbs are then determined. +""" +import gzip, hashlib, itertools, json +from collections import Counter, defaultdict +from functools import lru_cache +from pathlib import Path + +H = 9 +FREE_PHASES = ('A', 'B') + + +def basis(vs): + b = {} + for x in vs: + for p in sorted(b, reverse=True): + if x >> p & 1: x ^= b[p] + if x: + p = x.bit_length() - 1 + for q in list(b): + if b[q] >> p & 1: b[q] ^= x + b[p] = x + return tuple(b[p] for p in sorted(b, reverse=True)) + + +def contains(A, B): + """B is a subspace of A (both reduced bases)""" + return len(basis(list(A) + list(B))) == len(A) + + +@lru_cache(None) +def perp(U): + return basis([z for z in range(1, 1 << H) if all(not (z & u).bit_count() % 2 for u in U)]) + + +@lru_cache(None) +def meet(A, B): + return perp(basis(list(perp(tuple(A))) + list(perp(tuple(B))))) + + +def payload_sha(path): + return hashlib.sha256(gzip.decompress(Path(path).read_bytes())).hexdigest() + + +def load(directory, program): + d = Path(directory) + c = json.load(gzip.open(d / 'CANONICAL-WORD.json.gz')) + ev = json.load(gzip.open(d / 'LOCAL-PROGRAMS.json.gz'))[program] + return c, ev + + +def extract(c, events): + """Replay the emitted program; return frames, macro nodes (ops, pin, baseline frame, phase), climbs, centre steps.""" + v, R = c['v'], c['R']; n = 2 * v + R + F = [basis(f) for f in c['frames']] + levels = {int(t): F[f] for t, f in c.get('target_levels', {}).items()} + cur = [F[f] for f in c['start']] + nodes = []; climbs = defaultdict(list); center = Counter(); private = {}; phase = None + for e in events: + tag = e[0] + if tag == 'phase': + phase = e[1] + if phase == 'centers': + for t in range(v): nodes.append(((v + t,), levels.get(t, ()), cur[v + t], 'pin:centers')) + if phase == 'full_frame_cleanup': + for r in range(n): nodes.append(((r,), F[c['final'][r]], cur[r], 'pin:final')) + elif tag == 'climb': + _, part, r, a, b, rank = e + assert cur[r] == F[a] and contains(F[b], F[a]) and len(F[b]) - len(F[a]) == rank > 0 + climbs[r].append(rank); cur[r] = F[b] + elif tag == 'center': + _, k, a, b, rank = e + assert rank == abs(len(F[a]) - len(F[b])) > 0 + private[('C', k)] = F[b]; center[rank] += 1 + elif tag == 'scalar': + _, op, f = e; f = F[f] + regs = [tuple(op[1])] + ([tuple(op[2])] if op[0] in ('add', 'copy') else []) + ops = tuple(r[1] for r in regs if r[0] == 'L'); pin = None + for r in regs: + if r[0] == 'C': + if op[0] == 'clear': private.pop(r, None); continue + private.setdefault(r, f); assert private[r] == f; pin = f + for r in ops: assert cur[r] == f + if phase not in FREE_PHASES: pin = f + if ops: nodes.append((ops, pin, f, phase)) + elif tag in ('adapter', 'residual_adapter'): + pass # boundary wrappers: frame-independent of macro frames, unchanged + else: + raise AssertionError(tag) + assert all(cur[r] == F[c['final'][r]] for r in range(n)) + return F, nodes, climbs, center + + +def chains(c, nodes): + n = 2 * c['v'] + c['R']; seq = defaultdict(list) + for i, nd in enumerate(nodes): + for r in nd[0]: seq[r].append(i) + return [seq[r] for r in range(n)] + + +def intervals(c, F, nodes): + """lo_i (forward joins) and hi_i (backward meets): every legal assignment has lo_i <= G_i <= hi_i.""" + low = [F[f] for f in c['start']]; lo = [] + for ops, pin, f, ph in nodes: + L = basis([x for r in ops for x in low[r]]) + if pin is not None: assert contains(pin, L); L = pin + for r in ops: low[r] = L + lo.append(L) + up = [F[f] for f in c['final']]; hi = [None] * len(nodes) + for i in range(len(nodes) - 1, -1, -1): + ops, pin, f, ph = nodes[i]; U = up[ops[0]] + for r in ops[1:]: U = meet(U, up[r]) + if pin is not None: assert contains(U, pin); U = pin + for r in ops: up[r] = U + hi[i] = U + for i, nd in enumerate(nodes): + assert contains(nd[2], lo[i]) and contains(hi[i], nd[2]) + return lo, hi + + +def between(L, U): + """every subspace G with L <= G <= U (lift of all subspaces of the quotient U/L)""" + comp = [] + for x in U: + if not contains(basis(list(L) + comp), (x,)): comp.append(x) + g = len(comp); assert g <= 3 + def lift(s): + z = 0 + for j in range(g): + if s >> j & 1: z ^= comp[j] + return z + out = {basis(list(L) + [lift(s) for s in sub]) for sub in itertools.product(range(1 << g), repeat=g)} + return sorted(out, key=lambda b: (len(b), b)) + + +def profile(c, F, nodes, frames): + """paid L-register climbs implied by a frame assignment, with full legality check""" + n = 2 * c['v'] + c['R']; cur = [F[x] for x in c['start']]; Hc = Counter() + for i, nd in enumerate(nodes): + G = frames[i] + if nd[1] is not None: assert G == nd[1] + for r in nd[0]: + assert contains(G, cur[r]), ('not nested', i, r) + k = len(G) - len(cur[r]) + if k: Hc[k] += 1 + cur[r] = G + for r in range(n): + fin = F[c['final'][r]]; assert contains(fin, cur[r]); k = len(fin) - len(cur[r]) + if k: Hc[k] += 1 + return Hc + + +def vec(k, mult=1): + """symbolic cost: coefficient vector over C_2..C_9 (C_0 = C_1 = 0)""" + v = [0] * 8 + if k >= 2: v[k - 2] = mult + return tuple(v) + + +def add(a, b): return tuple(x + y for x, y in zip(a, b)) + + +ZERO = (0,) * 8 + + +def lp(c, F, nodes, lo, hi): + """Local-polytope LP of the exact model, split into independent components. + + Vertices: free macros (lo < hi). Edges: consecutive macros on a register (with + multiplicity). Columns: x(i,G) for G in [lo_i,hi_i]; y(e,G,G') for nested pairs. + Rows: sum_G x(i,G) = 1 and both marginal equalities of every free-free edge. + Costs are symbolic vectors over C_2..C_9. Every legal assignment is a 0/1 point. + Returns components, the constant symbolic cost and the baseline symbolic cost. + """ + n = 2 * c['v'] + c['R']; seq = chains(c, nodes) + free = {i for i, nd in enumerate(nodes) if nd[1] is None and len(lo[i]) < len(hi[i])} + dom = {i: between(lo[i], hi[i]) for i in free} + for i in free: assert nodes[i][2] in dom[i] + edges = Counter(); unary = defaultdict(lambda: ZERO); const = ZERO; base = ZERO + def frame(tag, x): + return F[c['start'][x]] if tag == 'S' else F[c['final'][x]] if tag == 'E' else nodes[x][2] + for r in range(n): + ch = [('S', r)] + [('N', i) for i in seq[r]] + [('E', r)] + for (ta, a), (tb, b) in zip(ch, ch[1:]): + fa, fb = frame(ta, a), frame(tb, b) + base = add(base, vec(len(fb) - len(fa))) + va, vb = ta == 'N' and a in free, tb == 'N' and b in free + if va and vb: edges[(a, b)] += 1 + elif va: + for G in dom[a]: unary[(a, G)] = add(unary[(a, G)], vec(len(fb) - len(G))) + elif vb: + for G in dom[b]: unary[(b, G)] = add(unary[(b, G)], vec(len(G) - len(fa))) + else: + const = add(const, vec(len(fb) - len(fa))) + parent = {i: i for i in free} + def find(x): + while parent[x] != x: parent[x] = parent[parent[x]]; x = parent[x] + return x + for a, b in edges: parent[find(a)] = find(b) + groups = defaultdict(list) + for i in free: groups[find(i)].append(i) + comps = [] + for key in sorted(groups, key=lambda k: min(groups[k])): + vs = sorted(groups[key]); S = set(vs) + cols = []; rows = [] # cols: (name, cost, [(row, coef)]); rows: rhs + xid = {} + for i in vs: + r0 = len(rows); rows.append(1) + for G in dom[i]: + xid[(i, G)] = len(cols); cols.append([('x', i, G), unary[(i, G)], [(r0, 1)]]) + for (a, b), m in sorted(edges.items()): + if a not in S: continue + ra = {G: len(rows) + j for j, G in enumerate(dom[a])}; rows += [0] * len(dom[a]) + rb = {G: len(rows) + j for j, G in enumerate(dom[b])}; rows += [0] * len(dom[b]) + for G in dom[a]: cols[xid[(a, G)]][2].append((ra[G], -1)) + for G2 in dom[b]: cols[xid[(b, G2)]][2].append((rb[G2], -1)) + for G in dom[a]: + for G2 in dom[b]: + if contains(G2, G): + cols.append([('y', (a, b), (G, G2)), vec(len(G2) - len(G), m), [(ra[G], 1), (rb[G2], 1)]]) + comps.append({'nodes': vs, 'domains': {i: dom[i] for i in vs}, 'cols': cols, 'rhs': rows, + 'edges': {e: m for e, m in edges.items() if e[0] in S}}) + return comps, const, base, free diff --git a/research/complex-k492-frame-bound/verify.py b/research/complex-k492-frame-bound/verify.py new file mode 100644 index 0000000000..5e609d2486 --- /dev/null +++ b/research/complex-k492-frame-bound/verify.py @@ -0,0 +1,216 @@ +#!/usr/bin/env python3 +"""Verify the fixed-order A/B frame exclusion for the PR626 jp8 and ck complex providers. + +Standard library only; no optimizer. Prepared with substantial AI assistance (Anthropic Claude). Apache-2.0. + +usage: python3 -B verify.py [--work K492_REPLAY_DIR] [--control NAME] +Without --work the committed copies in data/ are used; with --work the freshly +replayed jp8-local/ck-local outputs of research/complex-k492-owner-repair/verify.sh +are used. Either way the decompressed payloads must match the pinned hashes. +""" +import argparse, copy, gzip, hashlib, itertools, json, sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +HERE = Path(__file__).resolve().parent; sys.path.insert(0, str(HERE)) +import model as Mo +import engine as E + +if not __debug__: raise SystemExit('assertions are the proof checks: run without -O') +PINS = json.loads((HERE / 'SOURCES.json').read_text()) +GAUSS = {0: 1, 1: 2, 2: 5, 3: 16} # number of subspaces of F_2^g +CONTROLS = ('drop_component', 'inflate_dual', 'alter_domain', 'accepted_endpoint', 'suboptimal_baseline', 'wrong_word') + + +def dec(x, direction, digits=40): + """outward-rounded decimal string (direction -1: floor, +1: ceil)""" + s = 10 ** digits; n = (x.numerator * s) // x.denominator + if direction > 0 and Q(n, s) < x: n += 1 + return '%s%d.%0*d' % ('-' if n < 0 else '', abs(n) // s, digits, abs(n) % s) + + +def sha(b): return hashlib.sha256(b).hexdigest() + + +def check_component(comp, dual, baseline_frames, engines): + cols, rhs = comp['cols'], comp['rhs'] + assert len(dual) == len(rhs) and all(len(r) == 8 for r in dual), 'dual shape' + q = [tuple(Q(x) for x in r) for r in dual] + forms = set() + for name, cost, entries in cols: + v = list(cost) + for r, a in entries: + for k in range(8): v[k] -= a * q[r][k] + forms.add(tuple(v)) + for v in forms: assert E.nonnegative(v, engines), ('negative reduced cost', v) + obj = tuple(sum((rhs[i] * q[i][k] for i in range(len(rhs))), Q(0)) for k in range(8)) + # literal baseline point: x(i, baseline) = 1 and y(e, baseline pair) = 1 + base = Mo.ZERO + for name, cost, entries in cols: + if name[0] == 'x' and baseline_frames[name[1]] == name[2]: base = Mo.add(base, cost) + if name[0] == 'y' and (baseline_frames[name[1][0]], baseline_frames[name[1][1]]) == name[2]: base = Mo.add(base, cost) + assert obj == tuple(Q(x) for x in base), ('dual objective differs from the literal baseline', obj, base) + return len(forms), base + + +def worse_block(c, F, nodes, free): + """a legal, strictly different-profile assignment: move one same-frame block of free macros to span(in)/meet(out)""" + seq = Mo.chains(c, nodes); pos = {(i, r): k for r, ch in enumerate(seq) for k, i in enumerate(ch)} + H0 = Mo.profile(c, F, nodes, [nd[2] for nd in nodes]) + for i0 in sorted(free): + f = nodes[i0][2]; B = {i0}; st = [i0] + while st: + j = st.pop() + for r in nodes[j][0]: + k = pos[(j, r)] + for q in (k - 1, k + 1): + if 0 <= q < len(seq[r]) and seq[r][q] not in B and nodes[seq[r][q]][2] == f: B.add(seq[r][q]); st.append(seq[r][q]) + if not B <= free: continue + ins = []; outs = [] + for j in B: + for r in nodes[j][0]: + k = pos[(j, r)] + if k == 0 or seq[r][k - 1] not in B: ins.append(nodes[seq[r][k - 1]][2] if k else F[c['start'][r]]) + if k + 1 == len(seq[r]) or seq[r][k + 1] not in B: outs.append(nodes[seq[r][k + 1]][2] if k + 1 < len(seq[r]) else F[c['final'][r]]) + L = Mo.basis([x for g in ins for x in g]); U = outs[0] + for g in outs[1:]: U = Mo.meet(U, g) + for G in (L, U): + if G == f: continue + trial = [nd[2] for nd in nodes] + for j in B: trial[j] = G + if Mo.profile(c, F, nodes, trial) != H0: return {j: G for j in B} + raise AssertionError('no alternative block found') + + +def brute(c, F, nodes, comp, engines, limit=4096): + """independent exhaustive check of small components: all legal assignments, exact symbolic cost difference""" + vs = comp['nodes']; doms = [comp['domains'][i] for i in vs] + total = 1 + for d in doms: total *= len(d) + if total > limit: return None + seq = Mo.chains(c, nodes); S = set(vs); count = 0 + regs = sorted({r for i in vs for r in nodes[i][0]}) + def cost(assign): + v = Mo.ZERO + for r in regs: + ch = seq[r]; prev = F[c['start'][r]] + for i in ch + [None]: + G = F[c['final'][r]] if i is None else assign.get(i, nodes[i][2]) + if not Mo.contains(G, prev): return None + v = Mo.add(v, Mo.vec(len(G) - len(prev))); prev = G + return v + b = cost({i: nodes[i][2] for i in vs}) + for choice in itertools.product(*doms): + v = cost(dict(zip(vs, choice))) + if v is None: continue + count += 1 + diff = tuple(x - y for x, y in zip(v, b)) + assert E.nonnegative(diff, engines), ('brute force found a cheaper legal assignment', vs, choice) + return count + + +def main(): + ap = argparse.ArgumentParser(); ap.add_argument('--work', type=Path); ap.add_argument('--controls', action='store_true') + ap.add_argument('--out', type=Path) + a = ap.parse_args() + if a.controls: + rejected = [] + for ctl in CONTROLS: + try: run(a.work, ctl, None) + except AssertionError as e: + rejected.append(ctl); print('REJECTED control', ctl, '-', str(e)[:120], flush=True) + else: raise SystemExit('control accepted: ' + ctl) + print('PASS_CONTROLS', len(rejected), 'of', len(CONTROLS), 'rejected'); return + run(a.work, None, a.out) + + +def run(work, ctl, out): + class a: pass + a.work = work + assert sha(E.REPO_ENGINE.read_bytes()) == E.REPO_ENGINE_SHA256, 'repository moment engine pin' + endpoint = E.B_ACCEPTED if ctl == 'accepted_endpoint' else E.B_NEXT + engA = E.engine_a(endpoint); engB = E.engine_b(endpoint); engines = (engA, engB) + duals = json.loads(gzip.decompress((HERE / 'data/DUALS.json.gz').read_bytes())) + assert sha(gzip.decompress((HERE / 'data/DUALS.json.gz').read_bytes())) == PINS['duals_payload_sha256'] + report = {'programs': {}} + local = {} + for word in ('jp8', 'ck'): + d = (a.work / (word + '-local')) if a.work else HERE / 'data' / word + if ctl == 'wrong_word' and word == 'jp8': d = (a.work / 'ck-local') if a.work else HERE / 'data/ck' + rec = json.loads((HERE.parents[1] / PINS['inputs'][word]['pr626_receipt']['path']).read_text()) + assert rec['canonical_word_sha256'] == PINS['inputs'][word]['CANONICAL-WORD']['gzip_sha256'] + assert rec['local_programs_sha256'] == PINS['inputs'][word]['LOCAL-PROGRAMS']['gzip_sha256'] + for f in ('CANONICAL-WORD', 'LOCAL-PROGRAMS'): + got = Mo.payload_sha(d / (f + '.json.gz')) + assert got == PINS['inputs'][word][f]['payload_sha256'], ('input payload pin', word, f) + for prog in ('forward', 'backward'): + key = '%s/%s' % (word, prog) + c, ev = Mo.load(d, prog) + F, nodes, climbs, center = Mo.extract(c, ev) + Hc = Counter(center) + for r, l in climbs.items(): Hc.update(l) + assert dict(Hc) == {int(k): z for k, z in c['local_profile'].items()}, 'emitted climbs + centre steps = local profile' + lo, hi = Mo.intervals(c, F, nodes) + assert Mo.profile(c, F, nodes, [nd[2] for nd in nodes]) + Counter(center) == Hc + comps, const, base, free = Mo.lp(c, F, nodes, lo, hi) + if ctl == 'alter_domain': + comp = next(x for x in comps if any(len(v) > 2 for v in x['domains'].values())) + i = next(i for i, v in comp['domains'].items() if len(v) > 2) + G = next(g for g in comp['domains'][i] if g != nodes[i][2]) + comp['domains'][i].remove(G) + drop = {j for j, col in enumerate(comp['cols']) if (col[0][0] == 'x' and col[0][1:] == (i, G)) or (col[0][0] == 'y' and ((col[0][1][0] == i and col[0][2][0] == G) or (col[0][1][1] == i and col[0][2][1] == G)))} + comp['cols'] = [col for j, col in enumerate(comp['cols']) if j not in drop] + assert len(comp['domains'][i]) < GAUSS[len(hi[i]) - len(lo[i])] + for comp in comps: # completeness: every subspace of every interval is a choice + for i in comp['nodes']: + g = len(hi[i]) - len(lo[i]); dom = comp['domains'][i] + assert len(set(dom)) == len(dom) == GAUSS[g], ('incomplete domain', i) + assert all(Mo.contains(G, lo[i]) and Mo.contains(hi[i], G) for G in dom) + cert = duals[key] + if ctl == 'drop_component': cert = cert[:-1] + if ctl == 'inflate_dual': + cert = copy.deepcopy(cert); k0 = max(range(len(cert)), key=lambda j: len(cert[j])) + cert[k0][0][0] = str(Q(cert[k0][0][0]) + 1) + assert len(cert) == len(comps), 'one certificate per component' + bf = {i: nodes[i][2] for i in free} + if ctl == 'suboptimal_baseline': + bf.update(worse_block(c, F, nodes, free)) + forms = 0; total = const; brute_assignments = 0; brute_components = 0 + for comp, dual in zip(comps, cert): + nf, cb = check_component(comp, dual, bf, engines); forms += nf; total = Mo.add(total, cb) + bc = brute(c, F, nodes, comp, engines) if ctl is None else None + if bc is not None: brute_assignments += bc; brute_components += 1 + assert total == base, 'components and constants recompose the literal baseline' + mass = sum(len(F[c['final'][r]]) - len(F[c['start'][r]]) for r in range(2 * c['v'] + c['R'])) + report['programs'][key] = {'macros': len(nodes), 'free_macros_with_choices': len(free), + 'domain_frames': sum(len(x['domains'][i]) for x in comps for i in x['nodes']), + 'components': len(comps), 'lp_rows': sum(len(x['rhs']) for x in comps), 'lp_columns': sum(len(x['cols']) for x in comps), + 'distinct_reduced_cost_forms': forms, 'brute_forced_components': brute_components, + 'brute_forced_legal_assignments': brute_assignments, 'register_rank_mass': mass, + 'local_profile': {str(k): v for k, v in sorted(Hc.items())}} + local[key] = Hc + print('PASS', key, json.dumps(report['programs'][key]), flush=True) + # global consequence at the endpoint + assembly = HERE.parents[1] / PINS['assembly']['path'] + assert sha(assembly.read_bytes()) == PINS['assembly']['sha256'] + A = json.loads(assembly.read_text()); Hg = {int(k): v for k, v in A['complex_profile'].items()} + assert Q(A['complex_lower']) == E.B_ACCEPTED and A['binding'] == 'complex' + calls = A['provider_counts']; assert calls == {'ck': 8, 'jp8': 64} + for prog in ('forward', 'backward'): + rem = {k: Hg.get(k, 0) - 64 * local['jp8/' + prog].get(k, 0) - 8 * local['ck/' + prog].get(k, 0) for k in set(Hg) | set(local['jp8/' + prog]) | set(local['ck/' + prog])} + assert all(v >= 0 for v in rem.values()), 'local profiles are contained in the global profile' + la, ua = E.moment_a(Hg, endpoint); R = E._repo(); lb, ub = R.moment(Hg, E.M_DIM, E.W_LIVE, endpoint) + assert la > 1 and lb > 1, 'baseline global moment must exceed one at the excluded endpoint' + la0, ua0 = E.moment_a(Hg, E.B_ACCEPTED); lb0, ub0 = R.moment(Hg, E.M_DIM, E.W_LIVE, E.B_ACCEPTED) + assert ua0 < 1 and ub0 < 1 + report.update(status='PASS_FIXED_ORDER_AB_FRAME_EXCLUSION_PR626', excluded_complex_endpoint=str(endpoint), + accepted_complex_endpoint=str(E.B_ACCEPTED), global_moment_minus_one_at_excluded={'engine_a': [dec(la - 1, -1), dec(ua - 1, 1)], 'repo_engine': [dec(lb - 1, -1), dec(ub - 1, 1)]}, + scope='Every simultaneous reassignment of A/B scalar-macro frames of the emitted PR626 jp8 and ck provider programs, ' + 'with macro list/order/operands, starts, finals, target levels, centre chains and all non-A/B macro frames fixed. ' + 'No scalar rewrite, reordering, width/owner/hosting change, other supplier or outer theorem is covered.') + if out: out.write_text(json.dumps(report, indent=2, sort_keys=True) + '\n') + print(report['status'], 'excluded b =', endpoint, flush=True) + + +if __name__ == '__main__': + main()