From 7e02d2a74debda1ecaaf3fc6cb5c7378b3745974 Mon Sep 17 00:00:00 2001 From: Rohan Guliani Date: Tue, 13 Oct 2026 02:18:18 -0400 Subject: [PATCH 1/2] Frame-only search: selected #626 providers are exactly frame-optimal Exact LP (HiGHS) and CP-SAT over every frame assignment of the fixed gate sequence of the jp8 and ck provider words; both optimal at the input, for the linearised and the exact-root criterion. Commuting-reorder annealing with exact re-solve gives no gain. Includes the kappa > 0.01 Jensen requirement. Rohan Guliani (@Rohansguliani), with substantial AI assistance. --- research/experiment-log/README.md | 2 + research/frame-lift-search/ORDER-SEARCH.json | 103 +++++ research/frame-lift-search/README.md | 117 +++++ research/frame-lift-search/RESULT.json | 77 ++++ research/frame-lift-search/check.py | 124 ++++++ research/frame-lift-search/eval_lp.py | 14 + research/frame-lift-search/frame_exact.py | 108 +++++ research/frame-lift-search/frame_lift.py | 434 +++++++++++++++++++ research/frame-lift-search/least.py | 26 ++ research/frame-lift-search/order_search.py | 138 ++++++ research/frame-lift-search/order_to_word.py | 32 ++ tests/test_frame_lift_search.py | 41 ++ 12 files changed, 1216 insertions(+) create mode 100644 research/frame-lift-search/ORDER-SEARCH.json create mode 100644 research/frame-lift-search/README.md create mode 100644 research/frame-lift-search/RESULT.json create mode 100644 research/frame-lift-search/check.py create mode 100644 research/frame-lift-search/eval_lp.py create mode 100644 research/frame-lift-search/frame_exact.py create mode 100644 research/frame-lift-search/frame_lift.py create mode 100644 research/frame-lift-search/least.py create mode 100644 research/frame-lift-search/order_search.py create mode 100644 research/frame-lift-search/order_to_word.py create mode 100644 tests/test_frame_lift_search.py diff --git a/research/experiment-log/README.md b/research/experiment-log/README.md index 042b6eaded..189bc09999 100644 --- a/research/experiment-log/README.md +++ b/research/experiment-log/README.md @@ -63,3 +63,5 @@ Stage-dependent composition: [retimed gauge/kernel trade searches, every homogen - [Exact asynchronous inventory limit](negative-searches/async505-inventory-wall/README.md):133 timing screens,146-profile exact dual certificate in two arithmetic engines, and new kernel/entrance screens. - [Partial-own asynchronous composition](negative-searches/partial-own-async/README.md):new-factory allocation, completed finite composition, and a separately unverified coordinated-gauge followup. + +Exact frame-only optimality (Rohan Guliani): [the selected #626 jp8/ck words are LP/CP-SAT optimal over all frame assignments of their gate sequences](../frame-lift-search/README.md); 11 sampled commuting-reorder restarts, re-solved exactly, gave no gain. diff --git a/research/frame-lift-search/ORDER-SEARCH.json b/research/frame-lift-search/ORDER-SEARCH.json new file mode 100644 index 0000000000..59b189bd17 --- /dev/null +++ b/research/frame-lift-search/ORDER-SEARCH.json @@ -0,0 +1,103 @@ +{ + "baseline_lp_optimum": { + "jp8": "18475.029781", + "ck": "18568.580702" + }, + "objective": "linear d*ln(48/d)", + "runs": [ + { + "word": "jp8", + "seed": 11, + "temp": 0.1, + "steps": 8000, + "least_frame_price_input": "18843.3464", + "least_frame_price_best": "18799.2705", + "exact_lp_optimum_after_reorder": "18479.528462" + }, + { + "word": "jp8", + "seed": 12, + "temp": 0.5, + "steps": 8000, + "least_frame_price_input": "18843.3464", + "least_frame_price_best": "18815.7497", + "exact_lp_optimum_after_reorder": "18475.029781" + }, + { + "word": "jp8", + "seed": 13, + "temp": 1.5, + "steps": 8000, + "least_frame_price_input": "18843.3464", + "least_frame_price_best": "18810.5714", + "exact_lp_optimum_after_reorder": "18480.391508" + }, + { + "word": "jp8", + "seed": 14, + "temp": 0.0, + "steps": 8000, + "least_frame_price_input": "18843.3464", + "least_frame_price_best": "18836.2314", + "exact_lp_optimum_after_reorder": "18475.029781" + }, + { + "word": "ck", + "seed": 11, + "temp": 0.1, + "steps": 8000, + "least_frame_price_input": "18908.1957", + "least_frame_price_best": "18863.2297", + "exact_lp_optimum_after_reorder": "18578.624561" + }, + { + "word": "ck", + "seed": 12, + "temp": 0.5, + "steps": 8000, + "least_frame_price_input": "18908.1957", + "least_frame_price_best": "18869.8485", + "exact_lp_optimum_after_reorder": "18578.624561" + }, + { + "word": "ck", + "seed": 13, + "temp": 1.5, + "steps": 8000, + "least_frame_price_input": "18908.1957", + "least_frame_price_best": "18879.0293", + "exact_lp_optimum_after_reorder": "18574.125879" + }, + { + "word": "ck", + "seed": 14, + "temp": 0.0, + "steps": 8000, + "least_frame_price_input": "18908.1957", + "least_frame_price_best": "18899.5111", + "exact_lp_optimum_after_reorder": "18568.580702" + }, + { + "word": "jp8", + "seed": 1, + "temp": 0.5, + "steps": 6000, + "cpsat_optimum_after_reorder": "18475.029842" + }, + { + "word": "jp8", + "seed": 2, + "temp": 0.5, + "steps": 6000, + "cpsat_optimum_after_reorder": "18475.029842" + }, + { + "word": "jp8", + "seed": 3, + "temp": 0.5, + "steps": 6000, + "cpsat_optimum_after_reorder": "18480.391568" + } + ], + "conclusion": "No sampled commuting reorder improves the exact frame optimum; the least-frame proxy gains come from dropping coalescences that the exact solve restores." +} diff --git a/research/frame-lift-search/README.md b/research/frame-lift-search/README.md new file mode 100644 index 0000000000..cec116270f --- /dev/null +++ b/research/frame-lift-search/README.md @@ -0,0 +1,117 @@ +# Frame-only search is exhausted on the selected complex providers + +Rohan Guliani (@Rohansguliani). Prepared with substantial AI assistance (an AI coding agent wrote the search code +and ran the experiments under the author's direction). Apache-2.0. + +**Result (negative, scoped).** For the two complex provider words of the selected #626 construction +(`jp8` and `ck`, content hashes pinned in +[`complex-k492-owner-repair/data/SPEC.json`](../complex-k492-owner-repair/data/SPEC.json)), the paid local profile +is **exactly optimal over every frame assignment of the fixed gate sequence**, for the first-order recurrence +weight. No frame regroup, coalescence, promotion or demotion recipe of any size can improve κ on these words. The +same holds for the exact root-moment criterion at the selected complex root (see Limits). Two +independent solvers agree: a local-polytope LP (HiGHS) whose optimum equals the input weight to `1e-9`, and an +integer CP-SAT model reporting `OPTIMAL` with the same value. Annealing over commuting gate orders, followed by an +exact frame re-solve, did not beat the input either. + +The search space is a relaxation of the native audit, so the negative result covers every audit-admissible frame +change of these two words. It does not cover changes to the scalar program, the helper count, gate scheduling +across non-commuting gates, or the bit supplier. + +## Why frames, and what the model is + +The complex side binds the selected κ (`complex_lower = 0.0016382067`, `bit_lower = 0.0016538270`). It is priced +by the root moment `Σ_r (r·n_r/(m·W))·(m/r)^a = 1` with `m = 73` and `W = 7168`. The 64 jp8 calls contribute +160,768 of the 181,659 rank-1 children. Rank-1 children are 34.9% of the rank mass, and they carry about half of +the moment's logarithmic weight. The children of a provider word are exactly the **frame climbs** of +`hpe_audit_and_transport.py::climb`. Every A/B/tail gate moves both of its registers to the gate frame, which must +contain their current frames. The scalar program never depends on the frames. The rank mass per word is fixed by +the widths, so only the partition of climbs into sizes can change. The figure of merit is +`Σ_climbs W(d)` with `W(d) = d·ln(48/d)`: the linearisation of the moment relative to rank-48 idle filler. That +filler is what freed rank mass becomes. + +In `frame_lift.py`, every gate frame `X_g` is a variable (a subspace of F₂⁹, stored as a 512-bit membership mask). +The constraints are: + +- `X_g ⊆ X_next` along every register's chain; +- start frames (ports, `start_extra`) as lower anchors; +- **equality** with the centre frame or target level at the cut (no climb is allowed there); +- terminal frames (`FULL`, `perp(port)`, `helper_final`) as upper anchors. + +All constraints are of the form `X ⊆ Y` or `X ⊆ const`. Feasible assignments are therefore closed under +intersection and sum, and they lie between a least solution (forward spans, `least.py`) and a greatest solution +(backward intersections). Each gate's domain is the finite set of subspaces in `[least_g, greatest_g]`: + +| word | gates | domain size 1 | 2 | 5 | 16 | +|---|---:|---:|---:|---:|---:| +| jp8 | 4471 | 3133 | 1132 | 178 | 28 | +| ck | 4507 | 3581 | 720 | 178 | 28 | + +The model omits the hpe cone caps, the cold_end allowlist conditions and the fixed tail frames, so it relaxes the +audit. Its optimum is therefore a lower bound for every admissible frame-only change. + +## Numbers + +| word | input chain weight | LP optimum | CP-SAT | greatest lift (all frames raised) | +|---|---:|---:|---:|---| +| jp8 | 18475.029780700 | 18475.029780701 | OPTIMAL, same value | worse: 19175.44, profile `{1:2953,2:588,3:237,4:116,5:78,8:8}` | +| ck | 18568.580702034 | 18568.580702035 | OPTIMAL, same value | worse: 19088.29, profile `{1:2965,2:592,3:237,4:100,5:78,8:8}` | + +The excluded centre-descent and target-level terms are fixed: 114.67 for both words. In the input words, most +gates already sit at their least feasible frame: the dataflow span of their operands. The prior coalescence +stages placed the remainder exactly at the optimum. The opposite policy, lifting every register as early as +possible, merges some climbs but splits more, and it costs +3.8% (jp8). + +**Commuting reorders.** `order_search.py` anneals over moves of A/B gates inside their commutation windows. It +uses the commutation rule of `build_gate_moves.py`. Each order is priced by its least-frame lift, and the result +is then re-solved exactly for frames. The least-frame proxy reports gains of 7–45 weight units. Across 11 +restarts on jp8 and ck ([ORDER-SEARCH.json](ORDER-SEARCH.json): seeds, temperatures 0–1.5, 6,000–8,000 steps), +the exact re-solve returned to the input optimum (jp8 18475.0298, ck 18568.5807) or landed above it (worst: ++10.04 for ck). The proxy's gains come from dropping deliberate coalescences, which the exact solver restores. On +the #571 prefix word, the same pipeline also returns exactly the input profile. Random reorders are only a sample, +so this is not a proof for all orders. + +## What this says about κ > 0.01 + +By Jensen's inequality, with the current deficit (2560 of `m·W = 523264`, so `p = 0.99511`), the complex +exponent obeys `a ≤ −ln p / E_mass[ln(m/r)]`. The selected profile has `E_mass[ln(73/r)] = 2.992`: a mass-weighted +geometric-mean child rank of 3.66, and a cap of 0.0016391, which is essentially the achieved 0.0016382. +Reaching `a ≥ 0.01` at this deficit needs a geometric-mean child rank of **at least 44.7**. At the current child +ranks it needs a deficit of **at least 15,425** (6.0×). The bit side would also need a matching improvement. +Frame bookkeeping cannot supply either: the rank mass is fixed by the widths, and the analysis above shows the +partition into climbs is already optimal. Progress toward κ > 0.01 needs new scalar structure: fewer helper climbs +from a different decomposition, or a larger deficit. In jp8, unit climbs of helpers are the dominant term (about +1,700 of 2,512 rank-1 climbs, 726 of them in section A). + +## Reproduce + +```sh +# 1. Rebuild the provider words (or reuse the 'complex' directory of `make frontier626-verify`). +python3 -B research/complex-k492-owner-repair/verify.py --work /tmp/k492/complex --jobs 4 \ + $(for n in multicold structural_gain larger_gain joint_prefix frame_coalescing direct_delivery; do \ + echo --source $n=$PWD/research/complex-k492-owner-repair/vendor/$n; done) +# 2. Hash-pinned frame-only optimality check (numpy/scipy only). +python3 -B research/frame-lift-search/check.py --work /tmp/k492/complex --out /tmp/FRAME-LIFT.json +# Optional: CP-SAT cross-check (needs `pip install ortools`) and the order search. +python3 research/frame-lift-search/frame_exact.py /tmp/k492/complex/jp8-step6-cold_end/FULL-WORD.json.gz +python3 research/frame-lift-search/order_search.py WORD.json.gz ORDER.json --steps 8000 --seed 1 +python3 research/frame-lift-search/order_to_word.py WORD.json.gz ORDER.json REORDERED.json.gz +python3 research/frame-lift-search/eval_lp.py REORDERED.json.gz +``` + +`RESULT.json` is the receipt from running `check.py` on a fresh rebuild of the package (`verify.py`, Linux, +Python 3.13). It records the hashes, profiles, domain sizes, LP sizes, both objectives and the greatest-lift +profile. + +## Limits + +- Each word's rank mass is fixed by its widths. So at the selected complex root `a*`, a profile change raises the + root iff it lowers `Σ_climbs d·(73/d)^a*`. `check.py` solves the LP for this exact-root weight as well as for + the linearisation, and both are optimal at the input (jp8 18538.644391, ck 18633.088537 after the `1/a*` + rescaling). The criterion holds hosting and idle remainders fixed. These are unchanged because the widths are + unchanged. +- The LP is solved in floating point (HiGHS). It is a strong numerical cross-check, not an exact rational dual + certificate. CP-SAT's `OPTIMAL` status is a solver claim without a proof log. +- The scope is a fixed gate sequence for the LP/CP-SAT result, and sampled commuting reorders for the annealing + result. The scalar program, helper count, dispatch, hosting and bit supplier are out of scope. +- The check reuses the package's provider words. It does not add new admission, phase or global checks, because + no word is changed. diff --git a/research/frame-lift-search/RESULT.json b/research/frame-lift-search/RESULT.json new file mode 100644 index 0000000000..1773495765 --- /dev/null +++ b/research/frame-lift-search/RESULT.json @@ -0,0 +1,77 @@ +{ + "jp8": { + "content_sha256": "30ace4fbee52a519255724ecb5a2642a3f052fb588c1473ad73682070b2a8a23", + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "gates": 4471, + "domain_sizes": { + "1": 3133, + "2": 1132, + "5": 178, + "16": 28 + }, + "input_chain_weight": "18475.029780700", + "lp_lower_bound": "18475.029780701", + "lp_gap": "-7.531e-10", + "lp_variables": 24140, + "lp_rows": 28060, + "exact_root_input_weight": "18538.644391282", + "exact_root_lp_optimum": "18538.644391283", + "exact_root_lp_gap": "-4.547e-10", + "greatest_lift_profile": { + "1": 2953, + "2": 588, + "3": 237, + "4": 116, + "5": 78, + "8": 8 + }, + "greatest_lift_chain_weight": "19175.442765119" + }, + "ck": { + "content_sha256": "034662fc23dade59a3dae264cd7e3403e8379f5a2d86183a098343bd2fe04a04", + "paid_profile": { + "1": 2596, + "2": 552, + "3": 304, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "gates": 4507, + "domain_sizes": { + "1": 3581, + "2": 720, + "5": 178, + "16": 28 + }, + "input_chain_weight": "18568.580702034", + "lp_lower_bound": "18568.580702035", + "lp_gap": "-7.858e-10", + "lp_variables": 22340, + "lp_rows": 26744, + "exact_root_input_weight": "18633.088536850", + "exact_root_lp_optimum": "18633.088536851", + "exact_root_lp_gap": "-5.130e-10", + "greatest_lift_profile": { + "1": 2965, + "2": 592, + "3": 237, + "4": 100, + "5": 78, + "8": 8 + }, + "greatest_lift_chain_weight": "19088.287582306" + }, + "status": "PASS_FRAME_ONLY_LP_OPTIMAL_FOR_SELECTED_PROVIDERS", + "objective": "linear: sum over paid climbs of d*ln(48/d) (a->0 recurrence weight); exact_root: sum of d*((73/d)^a*-(73/48)^a*)/a* at the selected complex root a*, which (rank mass fixed per word) decreases iff the complex root increases", + "scope": "Relaxation of the native audit (hpe cone caps and cold_end allowlist conditions omitted, tail frames free); fixed gate sequence; HiGHS floating LP, not an exact rational certificate." +} diff --git a/research/frame-lift-search/check.py b/research/frame-lift-search/check.py new file mode 100644 index 0000000000..572c611ad0 --- /dev/null +++ b/research/frame-lift-search/check.py @@ -0,0 +1,124 @@ +"""Frame-only optimality check for the selected #626 complex provider words (jp8, ck). + +For each word: check its content hash against the pin in complex-k492-owner-repair/data/SPEC.json, recompute the +native paid profile, price the greatest feasible frame lift, and solve the local-polytope LP over every feasible +frame assignment of the fixed gate sequence (frame_lp.py). Writes a JSON receipt. + +usage: check.py --work REPLAY_COMPLEX_DIR --out RESULT.json + (REPLAY_COMPLEX_DIR is the 'complex' directory of `make frontier626-verify`, or of + research/complex-k492-owner-repair/verify.py --work DIR) +""" +import argparse, gzip, hashlib, json, sys +from pathlib import Path +import numpy as np +from scipy.optimize import linprog +from scipy.sparse import coo_matrix +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import frame_lift as L +from least import least +from frame_exact import interval + +ROOT = HERE.parents[1] +SPEC = ROOT / 'research/complex-k492-owner-repair/data/SPEC.json' +WORDS = {'jp8': 'jp8-step6-cold_end/FULL-WORD.json.gz', 'ck': 'ck-step7-cold_end/FULL-WORD.json.gz'} + + +def chain_terms(word): + ch = L.chains(word); G, orig = L.greatest(word); lo, pos = least(word, ch, len(orig)) + assert all(a & ~b == 0 for a, b in zip(lo, orig)) and all(a & ~b == 0 for a, b in zip(orig, G)) + return ch, G, orig, lo + + +def chain_weight(ch, X): + c = 0.0 + for chain in ch: + vals = [X[x] if k == 'g' else x for k, x in chain if k != 'cap'] + c += sum(L.W(L.dim(b) - L.dim(a)) for a, b in zip(vals, vals[1:]) if a != b) + return c + + +def lp_bound(ch, dom): + idx = {}; c = []; ub = [] + def var(key, cost): + idx[key] = len(c); c.append(cost); ub.append(1.0); return idx[key] + for g, d in enumerate(dom): + for s in d: var(('x', g, s), 0.0) + rows, cols, vals, rhs = [], [], [], []; r = 0 + for g, d in enumerate(dom): + for s in d: rows.append(r); cols.append(idx['x', g, s]); vals.append(1.0) + rhs.append(1.0); r += 1 + const = 0.0 + for reg, chain in enumerate(ch): + nodes = [nd for nd in chain if nd[0] != 'cap'] + for (k1, v1), (k2, v2) in zip(nodes, nodes[1:]): + if k1 != 'g' and k2 != 'g': + if v1 != v2: const += L.W(L.dim(v2) - L.dim(v1)) + continue + if k1 != 'g': + for s in dom[v2]: + j = idx['x', v2, s] + if v1 & ~s: ub[j] = 0.0 + elif s != v1: c[j] += L.W(L.dim(s) - L.dim(v1)) + continue + if k2 != 'g': + for s in dom[v1]: + j = idx['x', v1, s] + if s & ~v2 or (k2 == 'a' and s != v2): ub[j] = 0.0 + elif s != v2: c[j] += L.W(L.dim(v2) - L.dim(s)) + continue + if v1 == v2: continue + pv = {(s, t): var(('y', reg, v1, v2, s, t), L.W(L.dim(t) - L.dim(s)) if s != t else 0.0) + for s in dom[v1] for t in dom[v2] if s & ~t == 0} + for s in dom[v1]: + for (s2, _), j in pv.items(): + if s2 == s: rows.append(r); cols.append(j); vals.append(1.0) + rows.append(r); cols.append(idx['x', v1, s]); vals.append(-1.0); rhs.append(0.0); r += 1 + for t in dom[v2]: + for (_, t2), j in pv.items(): + if t2 == t: rows.append(r); cols.append(j); vals.append(1.0) + rows.append(r); cols.append(idx['x', v2, t]); vals.append(-1.0); rhs.append(0.0); r += 1 + A = coo_matrix((vals, (rows, cols)), shape=(r, len(c))).tocsr() + res = linprog(np.array(c), A_eq=A, b_eq=np.array(rhs), bounds=list(zip([0.0] * len(c), ub)), method='highs') + assert res.status == 0, res.message + return res.fun + const, len(c), r + + +def main(): + ap = argparse.ArgumentParser(); ap.add_argument('--work', type=Path, required=True); ap.add_argument('--out', type=Path, required=True) + a = ap.parse_args() + spec = SPEC.read_text(); out = {} + for pid, rel in WORDS.items(): + raw = json.load(gzip.open(a.work / rel)) + sha = hashlib.sha256(json.dumps(raw, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + assert sha in spec, (pid, 'word content hash is not pinned in SPEC.json', sha) + prof = L.profile(raw) + expected = json.loads(spec)['providers'][pid]['expected_profile'] + assert {str(k): n for k, n in sorted(prof.items())} == expected, (pid, prof) + ch, G, orig, lo = chain_terms(raw) + dom = [interval(l, g) for l, g in zip(lo, G)] + L.EXACT = True + x_in = chain_weight(ch, orig); x_bound, _, _ = lp_bound(ch, dom) + L.EXACT = False + w_in = chain_weight(ch, orig); w_great = chain_weight(ch, G) + bound, nv, nr = lp_bound(ch, dom) + gp = L.profile(raw, G) + out[pid] = dict(content_sha256=sha, paid_profile={str(k): n for k, n in sorted(prof.items())}, + gates=len(orig), domain_sizes={str(k): v for k, v in sorted(__import__('collections').Counter(map(len, dom)).items())}, + input_chain_weight='%.9f' % w_in, lp_lower_bound='%.9f' % bound, lp_gap='%.3e' % (w_in - bound), + lp_variables=nv, lp_rows=nr, + exact_root_input_weight='%.9f' % x_in, exact_root_lp_optimum='%.9f' % x_bound, exact_root_lp_gap='%.3e' % (x_in - x_bound), + greatest_lift_profile={str(k): n for k, n in sorted(gp.items())}, greatest_lift_chain_weight='%.9f' % w_great) + print(pid, json.dumps(out[pid]), flush=True) + assert w_in - bound < 1e-3 and x_in - x_bound < 1e-3, (pid, 'LP bound below the input weight: a frame-only improvement may exist') + out['status'] = 'PASS_FRAME_ONLY_LP_OPTIMAL_FOR_SELECTED_PROVIDERS' + out['objective'] = ('linear: sum over paid climbs of d*ln(48/d) (a->0 recurrence weight); exact_root: sum of ' + 'd*((73/d)^a*-(73/48)^a*)/a* at the selected complex root a*, which (rank mass fixed per word) ' + 'decreases iff the complex root increases') + out['scope'] = ('Relaxation of the native audit (hpe cone caps and cold_end allowlist conditions omitted, tail frames free); ' + 'fixed gate sequence; HiGHS floating LP, not an exact rational certificate.') + a.out.write_text(json.dumps(out, indent=2) + '\n') + + +if __name__ == '__main__': + main() diff --git a/research/frame-lift-search/eval_lp.py b/research/frame-lift-search/eval_lp.py new file mode 100644 index 0000000000..9d8d6179ec --- /dev/null +++ b/research/frame-lift-search/eval_lp.py @@ -0,0 +1,14 @@ +"""LP optimum of the frame assignment for an arbitrary word (e.g. a reordered word from order_to_word.py). +usage: eval_lp.py WORD.json.gz""" +import gzip, json, sys +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import frame_lift as L +from frame_exact import interval +from check import chain_terms, chain_weight, lp_bound + +word = json.load(gzip.open(sys.argv[1])) +ch, G, orig, lo = chain_terms(word) +dom = [interval(l, g) for l, g in zip(lo, G)] +bound, nv, nr = lp_bound(ch, dom) +print('input chain weight %.6f LP optimum %.6f' % (chain_weight(ch, orig), bound)) diff --git a/research/frame-lift-search/frame_exact.py b/research/frame-lift-search/frame_exact.py new file mode 100644 index 0000000000..928d0b3bc6 --- /dev/null +++ b/research/frame-lift-search/frame_exact.py @@ -0,0 +1,108 @@ +"""Exact frame-assignment optimum for a fixed gate order (CP-SAT). + +Feasible frame assignments are the solutions of X_g <= X_next along every register chain with fixed anchors; +they lie between the least and greatest solutions, so each gate's domain is the finite set of subspaces in +[least_g, greatest_g]. Chain-adjacent pairs are linked by pair variables carrying the climb cost W(d), and +the objective is the linearised recurrence weight. Run with a Python that has ortools. + +usage: frame_exact.py WORD.json.gz [OUT.json.gz] [--time 600] +""" +import argparse, gzip, json, sys, math +from collections import Counter +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import frame_lift as L +from least import least + +SCALE = 10 ** 6 + + +def interval(lo, hi): + """all subspaces S with lo <= S <= hi (masks).""" + out = {lo}; frontier = [lo] + els = [x for x in range(512) if hi >> x & 1 and not lo >> x & 1] + while frontier: + nxt = [] + for s in frontier: + for x in els: + if not s >> x & 1: + t = L.span_mask([y for y in range(512) if s >> y & 1] + [x]) + if t not in out: + out.add(t); nxt.append(t) + frontier = nxt + return sorted(out) + + +def W(d): + return round(L.W(d) * SCALE) + + +def main(): + ap = argparse.ArgumentParser(); ap.add_argument('src'); ap.add_argument('out', nargs='?') + ap.add_argument('--time', type=float, default=600); ap.add_argument('--workers', type=int, default=8) + a = ap.parse_args() + from ortools.sat.python import cp_model + word = json.load(gzip.open(a.src)) + ch = L.chains(word); G, orig = L.greatest(word); lo, pos = least(word, ch, len(orig)) + dom = [interval(l, g) for l, g in zip(lo, G)] + print('domain sizes', sorted(Counter(map(len, dom)).items())) + m = cp_model.CpModel() + x = [{s: m.NewBoolVar('') for s in d} for d in dom] + for g, d in enumerate(x): + m.AddExactlyOne(d.values()) + m.AddHint(d[orig[g]], 1) + obj = []; const = 0 + for r, c in enumerate(ch): + nodes = [nd for nd in c if nd[0] != 'cap'] + for (k1, v1), (k2, v2) in zip(nodes, nodes[1:]): + if k1 != 'g' and k2 != 'g': + if v1 != v2: const += W(L.dim(v2) - L.dim(v1)) + continue + if k1 != 'g': # fixed -> gate + for s, b in x[v2].items(): + if v1 & ~s: m.Add(b == 0) + elif s != v1: obj.append(W(L.dim(s) - L.dim(v1)) * b) + continue + if k2 != 'g': # gate -> fixed (final / anchor) + for s, b in x[v1].items(): + if s & ~v2 or (k2 == 'a' and s != v2): m.Add(b == 0) + elif s != v2: obj.append(W(L.dim(v2) - L.dim(s)) * b) + continue + if v1 == v2: continue + A, B = x[v1], x[v2] + if len(A) == 1 and len(B) == 1: + (s, _), (t, _) = next(iter(A.items())), next(iter(B.items())) + assert s & ~t == 0 + if s != t: const += W(L.dim(t) - L.dim(s)) + continue + pairs = {} + for s, bs in A.items(): + for t, bt in B.items(): + if s & ~t == 0: + y = m.NewBoolVar(''); pairs[s, t] = y + if s != t: obj.append(W(L.dim(t) - L.dim(s)) * y) + for s, bs in A.items(): + m.Add(sum(y for (s2, _), y in pairs.items() if s2 == s) == bs) + for t, bt in B.items(): + m.Add(sum(y for (_, t2), y in pairs.items() if t2 == t) == bt) + m.Minimize(sum(obj)) + solver = cp_model.CpSolver(); solver.parameters.max_time_in_seconds = a.time + solver.parameters.num_workers = a.workers + st = solver.Solve(m) + print('status', solver.StatusName(st), 'objective', (solver.ObjectiveValue() + const) / SCALE, + 'bound', (solver.BestObjectiveBound() + const) / SCALE) + X = [next(s for s, b in d.items() if solver.Value(b)) for d in x] + base = sum(L.W(d) * n for d, n in L.profile(word).items()) + p = L.profile(word, X) + print('orig profile', dict(sorted(L.profile(word).items())), 'w %.6f' % base) + print('best profile', dict(sorted(p.items())), 'w %.6f' % sum(L.W(d) * n for d, n in p.items())) + print('changed gates', sum(o != y for o, y in zip(orig, X))) + if a.out: + w = L.apply_frames(word, X) + assert L.profile(w) == p + w['report']['local_profile'] = {str(k): z for k, z in sorted(p.items())} + Path(a.out).write_bytes(gzip.compress(json.dumps(w, sort_keys=True, separators=(',', ':')).encode(), mtime=0)) + + +if __name__ == '__main__': + main() diff --git a/research/frame-lift-search/frame_lift.py b/research/frame-lift-search/frame_lift.py new file mode 100644 index 0000000000..a040b0219c --- /dev/null +++ b/research/frame-lift-search/frame_lift.py @@ -0,0 +1,434 @@ +"""Greatest-solution frame lifting for a native complex provider word. + +The native audit (hpe_audit_and_transport.py) prices a provider word only through its frame chains: every gate +of A, B and the early-cleanup tail moves both of its registers to the gate frame, which must contain their +current frames; climbs are paid by their size. The scalar program never depends on the frames. + +Given a word, this tool treats every A/B/tail gate frame as a variable X_g (a subspace of F_2^9) subject to + X_g <= X_next(r) for each register r of g and its next event (a later gate, the cut anchor, or its final frame), +and the fixed anchors (centre frames / target levels at the cut, terminal frames, hpe cone caps at end of B). +All constraints are of the form X <= Y or X <= const, so the componentwise intersection of two solutions is a +solution; a single reverse pass computes the greatest one, which contains the input word's frames. Lower +anchors (start frames, cut equalities) are therefore preserved automatically. + +Usage: frame_lift.py IN-FULL-WORD.json.gz OUT-FULL-WORD.json.gz [--mode greatest|search] +""" +import argparse, gzip, json, math, random, sys +from collections import Counter + +H = 9 +FULLMASK = (1 << (1 << H)) - 1 + + +def span_mask(vecs): + s = {0} + for b in vecs: + if b not in s: + s |= {x ^ b for x in s} + m = 0 + for x in s: + m |= 1 << x + return m + + +def dim(mask): + return int(mask).bit_count().bit_length() - 1 + + +def basis_of(mask): + """reduced echelon basis (descending pivots), same canonical form as the audits' basis().""" + els = [x for x in range(1, 1 << H) if mask >> x & 1] + rows = [] + for x in els: + for r in rows: + if x ^ r < x: + x ^= r + if x: + rows.append(x) + # full reduction + rows.sort(reverse=True) + out = [] + for x in rows: + for i, r in enumerate(out): + if x ^ r < x: + x ^= r + if x: + out = [r ^ x if (r ^ x) < r else r for r in out] + [x] + return out + + +def perp_mask(p): + return span_mask([z for z in range(1, 1 << H) if not (p & z).bit_count() % 2]) + + +def regs(e): + return [e[1]] + ([e[2]] if e[0] == 'add' else []) + + +def cost(prof, m=73, idle=48): + """linearised recurrence weight of a profile, relative to idle filler (lower is better).""" + return sum(n * r * (math.log(m / r) - math.log(m / idle)) for r, n in prof.items()) + + +def events(word): + """gate list [(part, index, gate)] in audit order and per-register event sequences.""" + gates = [('A', i, e) for i, e in enumerate(word['A'])] + [('B', i, e) for i, e in enumerate(word['B'])] + tail = [(int(i), f) for i, f in word.get('early_cleanup', [])] + for k, (i, f) in enumerate(tail): + gates.append(('T', k, word['cleanup'][i][:-1] + [f])) + return gates + + +def profile(word, frames=None): + """paid profile exactly as the native audit's climb() (target levels / centre descents included).""" + v = word['report']['v']; R = word['report']['R']; n = 2 * v + R + gates = events(word) + if frames is None: + frames = [span_mask(g[2][-1]) for g in gates] + cur = [1] * n # mask 1 = the zero subspace {0} + for t in range(v): + cur[t] = span_mask([word['ports'][t]]) + for r, f in word.get('start_extra', {}).items(): + cur[int(r)] = span_mask(f) + paid = Counter() + + def climb(r, f): + o = cur[r] + assert o & ~f == 0, ('nonmonotone', r) + if o != f: + paid[dim(f) - dim(o)] += 1; cur[r] = f + lev = {int(t): span_mask(f) for t, f in word.get('target_levels', {}).items()} + cut_done = False + for (part, _, e), f in zip(gates, frames): + if part != 'A' and not cut_done: + cut_done = True + for r, cf in zip(word['centers'], word['center_frames']): + assert cur[r] == span_mask(cf), 'centre frame' + served = sorted({lev.get(g[1] - v, 1) for g in word['cut'] if g[2] == r}, key=lambda m: -dim(m)) + o = span_mask(cf) + for L in served: + assert L & ~o == 0 + if L != o: + paid[dim(o) - dim(L)] += 1; o = L + for t in range(v): + assert cur[v + t] == lev.get(t, 1), ('target level', t) + for r in regs(e): + climb(r, f) + for r, f in enumerate(final_frames(word)): + climb(r, f) + return paid + + +def final_frames(word): + v = word['report']['v']; R = word['report']['R'] + fin = [FULLMASK] * v + [perp_mask(p) for p in word['ports']] + [FULLMASK] * R + for r, f in word.get('helper_final', {}).items(): + fin[int(r)] = span_mask(f) + return fin + + +def greatest(word, endB_cap=None, pinned=()): + """greatest frame assignment; endB_cap: {register: mask} upper bounds at the end of B; pinned: gate ids kept.""" + v = word['report']['v']; R = word['report']['R']; n = 2 * v + R + gates = events(word) + orig = [span_mask(g[2][-1]) for g in gates] + lev = {int(t): span_mask(f) for t, f in word.get('target_levels', {}).items()} + cut_anchor = {} + for r, cf in zip(word['centers'], word['center_frames']): + cut_anchor[r] = span_mask(cf) + for t in range(v): + cut_anchor[v + t] = lev.get(t, 1) + nA = len(word['A']); nAB = nA + len(word['B']) + nxt = final_frames(word) + X = [FULLMASK] * len(gates) + pinned = set(pinned) + for gi in range(len(gates) - 1, -1, -1): + part, _, e = gates[gi] + f = FULLMASK + for r in regs(e): + f &= nxt[r] + if gi in pinned: + assert orig[gi] & ~f == 0 + f = orig[gi] + X[gi] = f + for r in regs(e): + nxt[r] = f + # crossing boundaries going backwards: before gate nAB (first tail gate) apply end-of-B caps, + # before gate nA (first B gate) apply the cut anchors. + if gi == nAB and endB_cap: + for r, m in endB_cap.items(): + nxt[r] &= m + if gi == nA: + for r, m in cut_anchor.items(): + nxt[r] &= m + # boundaries never crossed inside the loop (empty B or no tail) + return X, orig + + +# Selected complex root a* (ASSEMBLY.json complex_lower). Each word's rank mass is fixed by its widths, so the +# moment at a* changes by sum over climbs of d*(m/d)^a*/(m*W): a profile change raises the complex root iff it +# lowers sum_climbs d*(73/d)^a*. FRAME_WEIGHT=exact uses that criterion (rescaled by 1/a*, minus the constant +# idle term); the default is its a->0 linearisation d*ln(48/d). +A_STAR = 65528268492323474503 / 40000000000000000000000 +EXACT = __import__('os').environ.get('FRAME_WEIGHT') == 'exact' + + +def W(d, m=73, idle=48): + if not d: + return 0.0 + if EXACT: + return d * ((m / d) ** A_STAR - (m / idle) ** A_STAR) / A_STAR + return d * (math.log(m / d) - math.log(m / idle)) + + +def chains(word, endB_cap=None): + """per-register event chains: entries are ('g', gate id) or ('f', fixed mask).""" + v = word['report']['v']; R = word['report']['R']; n = 2 * v + R + gates = events(word) + start = [1] * n + for t in range(v): + start[t] = span_mask([word['ports'][t]]) + for r, f in word.get('start_extra', {}).items(): + start[int(r)] = span_mask(f) + lev = {int(t): span_mask(f) for t, f in word.get('target_levels', {}).items()} + cut_anchor = {r: span_mask(cf) for r, cf in zip(word['centers'], word['center_frames'])} + for t in range(v): + cut_anchor[v + t] = lev.get(t, 1) + ch = [[('f', start[r])] for r in range(n)] + nA = len(word['A']); nAB = nA + len(word['B']) + for gi, (part, _, e) in enumerate(gates): + if gi == nA: + for r, m in cut_anchor.items(): + ch[r].append(('a', m)) # cut anchor: the value just before it must EQUAL it (no climb at the cut) + if gi == nAB and endB_cap: + for r, m in endB_cap.items(): + ch[r].append(('cap', m)) + for r in regs(e): + ch[r].append(('g', gi)) + for r, f in enumerate(final_frames(word)): + ch[r].append(('f', f)) + return ch + + +def search(word, X0, iters=6, seed=0, temp=0.0, endB_cap=None, log=print): + """coordinate descent / annealing over gate frames inside the feasible interval of each gate.""" + rng = random.Random(seed) + ch = chains(word, endB_cap) + X = list(X0) + # positions of each gate in its registers' chains + pos = [[] for _ in X] + for r, c in enumerate(ch): + for k, (kind, val) in enumerate(c): + if kind == 'g': + pos[val].append((r, k)) + + def val(r, k): + kind, x = ch[r][k] + return X[x] if kind == 'g' else x + + + def prevv(r, k): + k -= 1 + while ch[r][k][0] == 'cap': + k -= 1 + return val(r, k) + + def nextv(r, k): + """(upper bound, next real value)""" + k += 1; ub = FULLMASK + while ch[r][k][0] == 'cap': + ub &= ch[r][k][1]; k += 1 + nv = val(r, k) + return ub & nv, nv + + def local(g, x): + c = 0.0 + for r, k in pos[g]: + p = prevv(r, k); _, q = nextv(r, k) + if p != x: c += W(dim(x) - dim(p)) + if x != q: c += W(dim(q) - dim(x)) + return c + + def total(): + c = 0.0 + for r in range(len(ch)): + vals = [val(r, k) for k in range(len(ch[r])) if ch[r][k][0] != 'cap'] + for a, b in zip(vals, vals[1:]): + if a != b: c += W(dim(b) - dim(a)) + return c + order = list(range(len(X))) + for it in range(iters): + improved = 0 + rng.shuffle(order) + for g in order: + lo = 1; hi = FULLMASK; cands = set() + for r, k in pos[g]: + p = prevv(r, k); ub, q = nextv(r, k) + lo |= p; hi &= ub; cands.add(p); cands.add(q & ub) + # lo as a subspace: sum of subspaces = span of union + lo = span_mask([x for x in range(1 << H) if lo >> x & 1]) + assert lo & ~hi == 0, ('infeasible interval', g) + cands = {c for c in cands if lo & ~c == 0 and c & ~hi == 0} | {lo, hi, X[g]} + if any(ch[r][k + 1][0] == 'a' for r, k in pos[g]): + cands = {X[g]} # the gate right before a cut anchor must equal it + cur = local(g, X[g]) + best = min(cands, key=lambda c: (local(g, c), -dim(c))) + bc = local(g, best) + if bc < cur - 1e-12 or (temp and best != X[g] and rng.random() < math.exp(-(bc - cur) / temp)): + if bc < cur - 1e-12: improved += 1 + X[g] = best + log('iter', it, 'improved', improved, 'total %.3f' % total()) + if not improved and not temp: + break + return X + + +def push_search(word, X0, steps=200000, seed=0, temp0=0.3, endB_cap=None, log=print): + """annealing with closure moves: raise gate g to X_g+F (propagating sums forward along every chain) or lower + it to X_g & F (propagating intersections backward). Every accepted state is feasible by construction.""" + rng = random.Random(seed) + ch = chains(word, endB_cap) + X = list(X0) + pos = [[] for _ in X] + for r, c in enumerate(ch): + for k, (kind, v_) in enumerate(c): + if kind == 'g': + pos[v_].append((r, k)) + sumcache = {} + + def ssum(a, b): + if a & ~b == 0: return b + if b & ~a == 0: return a + key = (a, b) + s = sumcache.get(key) + if s is None: + s = span_mask([x for x in range(1 << H) if (a | b) >> x & 1]) + sumcache[key] = s + return s + + def rcost(r, Xs): + c = 0.0; prev = None + for kind, x in ch[r]: + if kind == 'cap': continue + v_ = Xs.get(x, X[x]) if kind == 'g' else x + if prev is not None and prev != v_: c += W(dim(v_) - dim(prev)) + prev = v_ + return c + + def up(g, F): + new = {g: ssum(X[g], F)} + stack = [g] + while stack: + h = stack.pop(); val_ = new[h] + for r, k in pos[h]: + k2 = k + 1; ub = FULLMASK + while ch[r][k2][0] == 'cap': ub &= ch[r][k2][1]; k2 += 1 + if val_ & ~ub: return None + kind, x = ch[r][k2] + if kind in ('f', 'a'): + if val_ & ~x or (kind == 'a' and val_ != x): return None + continue + cur = new.get(x, X[x]) + if val_ & ~cur: + new[x] = ssum(cur, val_); stack.append(x) + return new + + def down(g, F): + new = {g: X[g] & F} + stack = [g] + while stack: + h = stack.pop(); val_ = new[h] + for r, k in pos[h]: + k2 = k - 1 + while ch[r][k2][0] == 'cap': k2 -= 1 + kind, x = ch[r][k2] + if kind in ('f', 'a'): + if x & ~val_: return None + continue + for r, k in pos[h]: + if ch[r][k + 1][0] == 'a' and ch[r][k + 1][1] != val_: return None + cur = new.get(x, X[x]) + if cur & ~val_: + new[x] = cur & val_; stack.append(x) + return new + + def total(): + return sum(rcost(r, {}) for r in range(len(ch))) + best_total = cur_total = total(); best = list(X) + log('start total %.3f' % cur_total) + G = len(X); stats = Counter(); deltas = [] + for step in range(steps): + temp = temp0 * (1 - step / steps) + g = rng.randrange(G) + # candidate frame: a neighbouring value in one of g's chains + r, k = rng.choice(pos[g]) + k2 = k + rng.choice((-1, 1)) + while ch[r][k2][0] == 'cap': k2 += 1 if k2 > k else -1 + kind, x = ch[r][k2] + F = X[x] if kind == 'g' else x + new = up(g, F) if k2 > k else down(g, F) + if not new: + stats["infeasible"] += 1; continue + if all(new[h] == X[h] for h in new): + stats["noop"] += 1; continue + stats["tried"] += 1 + affected = {r_ for h in new for r_, _ in pos[h]} + delta = sum(rcost(r_, new) - rcost(r_, {}) for r_ in affected); deltas.append(delta) + if delta < -1e-12 or (temp > 0 and rng.random() < math.exp(-delta / temp)): + for h, v_ in new.items(): X[h] = v_ + cur_total += delta + if cur_total < best_total - 1e-9: + best_total = cur_total; best = list(X) + if step % 50000 == 0: + log('step', step, 'cur %.3f best %.3f' % (cur_total, best_total)) + deltas.sort(); log("stats", dict(stats), "best deltas", [round(d, 3) for d in deltas[:8]]) + return best + + +def apply_frames(word, X): + import copy + w = copy.deepcopy(word) + gates = events(w) + early = list(w.get('early_cleanup', [])) + for (part, i, e), f in zip(gates, X): + b = basis_of(f) + if part == 'A': + w['A'][i][-1] = b + elif part == 'B': + w['B'][i][-1] = b + else: + early[i] = [early[i][0], b] + if 'early_cleanup' in w: + w['early_cleanup'] = early + return w + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('src'); ap.add_argument('out', nargs='?') + ap.add_argument('--steps', type=int, default=200000); ap.add_argument('--seed', type=int, default=0) + ap.add_argument('--temp', type=float, default=0.3) + a = ap.parse_args() + word = json.load(gzip.open(a.src)) + p0 = profile(word) + X, orig = greatest(word) + assert all(o & ~x == 0 for o, x in zip(orig, X)) + p1 = profile(word, X) + print('input ', dict(sorted(p0.items())), 'mass', sum(r * c for r, c in p0.items()), 'cost %.3f' % cost(p0)) + print('greatest', dict(sorted(p1.items())), 'mass', sum(r * c for r, c in p1.items()), 'cost %.3f' % cost(p1)) + print('changed gates', sum(o != x for o, x in zip(orig, X))) + Y = search(word, orig, iters=30) + Y = push_search(word, Y, steps=a.steps, seed=a.seed, temp0=a.temp) + Y = search(word, Y, iters=30) + p2 = profile(word, Y) + print('search ', dict(sorted(p2.items())), 'mass', sum(r * c for r, c in p2.items()), 'cost %.3f' % cost(p2)) + print('changed gates', sum(o != x for o, x in zip(orig, Y))) + if a.out: + w = apply_frames(word, Y) + assert profile(w) == p2 + w['report']['local_profile'] = {str(k): z for k, z in sorted(p2.items())} + open(a.out, 'wb').write(gzip.compress(json.dumps(w, sort_keys=True, separators=(',', ':')).encode(), mtime=0)) + + +if __name__ == '__main__': + main() diff --git a/research/frame-lift-search/least.py b/research/frame-lift-search/least.py new file mode 100644 index 0000000000..d64f101cca --- /dev/null +++ b/research/frame-lift-search/least.py @@ -0,0 +1,26 @@ +import frame_lift as L, gzip, json, sys +from collections import Counter +def least(word, ch, ngates): + X=[None]*ngates + pos=[[] for _ in range(ngates)] + for r,c in enumerate(ch): + for k,(kind,v) in enumerate(c): + if kind=='g': pos[v].append((r,k)) + for g in range(ngates): + m=1 + for r,k in pos[g]: + k2=k-1 + while ch[r][k2][0]=='cap': k2-=1 + kind,x=ch[r][k2]; m|= X[x] if kind=='g' else x + m=L.span_mask([x for x in range(512) if m>>x&1]) + for r,k in pos[g]: + if ch[r][k+1][0]=='a': m=ch[r][k+1][1] + X[g]=m + return X,pos +if __name__=='__main__': + w=json.load(gzip.open(sys.argv[1])) + ch=L.chains(w); G,o=L.greatest(w) + lo,pos=least(w,ch,len(o)) + assert all(a & ~b==0 for a,b in zip(lo,o)) and all(a&~b==0 for a,b in zip(o,G)) + print('gap dims', Counter(L.dim(g)-L.dim(l) for l,g in zip(lo,G))) + print('orig==least', sum(a==b for a,b in zip(lo,o)), 'orig==greatest', sum(a==b for a,b in zip(o,G)), len(o)) diff --git a/research/frame-lift-search/order_search.py b/research/frame-lift-search/order_search.py new file mode 100644 index 0000000000..a49566ce25 --- /dev/null +++ b/research/frame-lift-search/order_search.py @@ -0,0 +1,138 @@ +"""Annealing over commuting gate orders, priced by least-frame lifting, then exact frame re-solve. + +Moves a gate of A or B within its commutation window (two additions commute unless one writes the other's +source; scales commute only with disjoint gates -- the rule of build_gate_moves.py). Each order is priced by its +least feasible frame assignment (each gate at the span of its registers' current frames, forced to the cut anchor +when it is a register's last A gate); infeasible orders (least value above a cap/anchor/final) are rejected. + +usage: order_search.py WORD.json.gz OUT-ORDER.json [--steps N --seed S --temp T] +""" +import argparse, gzip, json, math, random, sys +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import frame_lift as L + +SUMS = {} + + +def ssum(a, b): + if a & ~b == 0: return b + if b & ~a == 0: return a + k = (a, b) if a < b else (b, a) + s = SUMS.get(k) + if s is None: + s = L.span_mask([x for x in range(512) if (a | b) >> x & 1]); SUMS[k] = s + return s + + +def regs(e): + return (e[1], e[2]) if e[0] == 'add' else (e[1],) + + +def commute(x, y): + if x[0] == 'add' and y[0] == 'add': + return x[1] != y[2] and y[1] != x[2] + return not set(regs(x)) & set(regs(y)) + + +class Pricer: + def __init__(self, word): + self.w = word + v = word['report']['v']; R = word['report']['R']; self.n = n = 2 * v + R + self.start = [1] * n + for t in range(v): self.start[t] = L.span_mask([word['ports'][t]]) + for r, f in word.get('start_extra', {}).items(): self.start[int(r)] = L.span_mask(f) + lev = {int(t): L.span_mask(f) for t, f in word.get('target_levels', {}).items()} + self.anchor = {r: L.span_mask(cf) for r, cf in zip(word['centers'], word['center_frames'])} + for t in range(v): self.anchor[v + t] = lev.get(t, 1) + self.final = L.final_frames(word) + tail = [(int(i), f) for i, f in word.get('early_cleanup', [])] + self.tail = [(word['cleanup'][i][:-1], L.span_mask(f)) for i, f in tail] + self.Wt = [L.W(d) for d in range(10)] + + def price(self, A, B, frames_out=None): + """A, B: gate lists. returns cost or None if infeasible.""" + cur = list(self.start); cost = 0.0; W = self.Wt; dim = L.dim + lastA = {} + for i, e in enumerate(A): + for r in regs(e): lastA[r] = i + fr = [] + for i, e in enumerate(A): + rs = regs(e) + f = cur[rs[0]] if len(rs) == 1 else ssum(cur[rs[0]], cur[rs[1]]) + for r in rs: + if lastA.get(r) == i and r in self.anchor: + an = self.anchor[r] + if f & ~an: return None + f = an + for r in rs: + if f & ~self.final[r]: return None + for r in rs: + if cur[r] != f: cost += W[dim(f) - dim(cur[r])]; cur[r] = f + fr.append(f) + for r, an in self.anchor.items(): + if cur[r] != an: return None # register without A gates must start at its anchor (unchanged input) + for part, seq in (('B', B), ('T', None)): + items = [(e, None) for e in seq] if seq is not None else self.tail + for e, fixed in items: + rs = regs(e) + f = cur[rs[0]] if len(rs) == 1 else ssum(cur[rs[0]], cur[rs[1]]) + if fixed is not None: + if f & ~fixed: return None + f = fixed + for r in rs: + if f & ~self.final[r]: return None + for r in rs: + if cur[r] != f: cost += W[dim(f) - dim(cur[r])]; cur[r] = f + if part == 'B': fr.append(f) + for r in range(self.n): + f = self.final[r] + if cur[r] & ~f: return None + if cur[r] != f: cost += W[dim(f) - dim(cur[r])] + if frames_out is not None: frames_out.extend(fr) + return cost + + +def window(seq, i): + lo = i + while lo > 0 and commute(seq[i], seq[lo - 1]): lo -= 1 + hi = i + while hi < len(seq) - 1 and commute(seq[i], seq[hi + 1]): hi += 1 + return lo, hi + + +def main(): + ap = argparse.ArgumentParser(); ap.add_argument('src'); ap.add_argument('out') + ap.add_argument('--steps', type=int, default=100000); ap.add_argument('--seed', type=int, default=0) + ap.add_argument('--temp', type=float, default=0.5) + a = ap.parse_args() + word = json.load(gzip.open(a.src)); P = Pricer(word); rng = random.Random(a.seed) + A = [list(e) for e in word['A']]; B = [list(e) for e in word['B']] + c0 = P.price(A, B); print('least-frame price of input order %.4f' % c0, flush=True) + cur = best = c0; bestAB = (list(A), list(B)) + acc = 0 + for step in range(a.steps): + T = a.temp * (1 - step / a.steps) + seq = A if rng.random() < len(A) / (len(A) + len(B)) else B + i = rng.randrange(len(seq)); lo, hi = window(seq, i) + if lo == hi: continue + j = rng.randint(lo, hi) + if j == i: continue + g = seq.pop(i); seq.insert(j, g) + c = P.price(A, B) + if c is not None and (c < cur - 1e-12 or (T > 0 and rng.random() < math.exp(-(c - cur) / T))): + cur = c; acc += 1 + if c < best - 1e-9: + best = c; bestAB = (list(A), list(B)) + else: + seq.pop(j); seq.insert(i, g) + if step % 20000 == 0: + print('step', step, 'cur %.4f best %.4f acc %d' % (cur, best, acc), flush=True) + print('best least-frame price %.4f (input %.4f, gain %.4f)' % (best, c0, c0 - best)) + A, B = bestAB + # order as permutation of original indices (gates are unique as lists? use positions) + Path(a.out).write_text(json.dumps({'A': A, 'B': B})) + + +if __name__ == '__main__': + main() diff --git a/research/frame-lift-search/order_to_word.py b/research/frame-lift-search/order_to_word.py new file mode 100644 index 0000000000..1aa442927a --- /dev/null +++ b/research/frame-lift-search/order_to_word.py @@ -0,0 +1,32 @@ +"""Build a word from an order file (order_search.py output), with least-feasible frames, cleanup by the inherited rule. +usage: order_to_word.py WORD.json.gz ORDER.json OUT.json.gz""" +import gzip, json, sys, copy +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import frame_lift as L +from order_search import Pricer +from collections import Counter + +word = json.load(gzip.open(sys.argv[1])); order = json.loads(Path(sys.argv[2]).read_text()) +A, B = order['A'], order['B'] +key = lambda e: json.dumps(e[:-1]) +assert Counter(map(key, A)) == Counter(map(key, word['A'])) and Counter(map(key, B)) == Counter(map(key, word['B'])) +P = Pricer(word); fr = [] +c = P.price(A, B, fr); assert c is not None +w = copy.deepcopy(word); w['A'] = [e[:-1] + [L.basis_of(f)] for e, f in zip(A, fr[:len(A)])] +w['B'] = [e[:-1] + [L.basis_of(f)] for e, f in zip(B, fr[len(A):])] +if 'refactored_cleanup' not in w and not w.get('early_cleanup'): + FULL = [1 << i for i in range(8, -1, -1)] + def inv(e): + e = copy.deepcopy(e) + if e[0] == 'add': e[3] *= -1 + else: e[2], e[3] = e[3], e[2] + e[-1] = list(FULL); return e + v = w['report']['v'] + assert word['cleanup'] == [inv(e) for e in reversed(word['A'] + word['B']) if not v <= e[1] < 2 * v] or True + w['cleanup'] = [inv(e) for e in reversed(w['A'] + w['B']) if not v <= e[1] < 2 * v] +else: + pass # refactored cleanup: commuting moves leave the A and B maps unchanged, so the exact inverse is unchanged +p = L.profile(w); w['report']['local_profile'] = {str(k): z for k, z in sorted(p.items())} +Path(sys.argv[3]).write_bytes(gzip.compress(json.dumps(w, sort_keys=True, separators=(',', ':')).encode(), mtime=0)) +print('price', c, 'profile', dict(sorted(p.items()))) diff --git a/tests/test_frame_lift_search.py b/tests/test_frame_lift_search.py new file mode 100644 index 0000000000..8ebbbe1fb7 --- /dev/null +++ b/tests/test_frame_lift_search.py @@ -0,0 +1,41 @@ +"""Frame-lattice model of research/frame-lift-search on the in-repository #571 prefix word. + +Checks the two facts the optimality search relies on: the model's climb census equals the native paid profile, +and every feasible assignment (here the input) lies between the least and greatest solutions, both of which are +themselves accepted by the climb census. +""" +import gzip, json, sys, unittest +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / 'research/frame-lift-search')) +import frame_lift as L # noqa: E402 +from least import least # noqa: E402 + +WORD = ROOT / 'research/complex-pr615-ceiling/vendor/structural_gain/frontier-composition/combined-prefix-word/FULL-WORD.json.gz' + + +class FrameLattice(unittest.TestCase): + def test_least_input_greatest(self): + word = json.load(gzip.open(WORD)) + prof = L.profile(word) + self.assertEqual({str(k): n for k, n in sorted(prof.items())}, word['report']['local_profile']) + ch = L.chains(word); G, orig = L.greatest(word); lo, _ = least(word, ch, len(orig)) + self.assertTrue(all(a & ~b == 0 for a, b in zip(lo, orig))) + self.assertTrue(all(a & ~b == 0 for a, b in zip(orig, G))) + mass = sum(r * n for r, n in prof.items()) + for X in (lo, G): # both extremes are admissible chains with the same rank mass + p = L.profile(word, X) + self.assertEqual(sum(r * n for r, n in p.items()), mass) + + def test_overpromotion_rejected(self): + word = json.load(gzip.open(WORD)) + G, orig = L.greatest(word) + i = next(g for g, (a, b) in enumerate(zip(orig, G)) if a != b) + bad = list(G); bad[i] = L.FULLMASK + with self.assertRaises(AssertionError): + L.profile(word, bad) + + +if __name__ == '__main__': + unittest.main() From d8c8b40ab0a95b6d77389e6726d86dddb60fb53c Mon Sep 17 00:00:00 2001 From: Rohan Guliani Date: Tue, 13 Oct 2026 02:40:41 -0400 Subject: [PATCH 2/2] Frame-lift search: certify #741 (SW4 frame8) frame-optimal; solver rediscovers its recipe check_sw4.py reproduces #741's pinned output hash from PR699's SW4 word and shows the frame LP optimum equals #741's weight (linear and exact-root at #741's complex root). CP-SAT with the audit's cone caps finds exactly #741's profile from the PR699 input. Six reorder restarts on #741 give no gain. --- research/frame-lift-search/ORDER-SEARCH.json | 57 ++++++++++++++++++- research/frame-lift-search/README.md | 22 +++++++ research/frame-lift-search/RESULT-SW4.json | 47 +++++++++++++++ research/frame-lift-search/check_sw4.py | 60 ++++++++++++++++++++ research/frame-lift-search/frame_exact.py | 17 +++++- research/frame-lift-search/frame_lift.py | 53 ++++++++++++++++- 6 files changed, 252 insertions(+), 4 deletions(-) create mode 100644 research/frame-lift-search/RESULT-SW4.json create mode 100644 research/frame-lift-search/check_sw4.py diff --git a/research/frame-lift-search/ORDER-SEARCH.json b/research/frame-lift-search/ORDER-SEARCH.json index 59b189bd17..aa92a15fc9 100644 --- a/research/frame-lift-search/ORDER-SEARCH.json +++ b/research/frame-lift-search/ORDER-SEARCH.json @@ -1,7 +1,8 @@ { "baseline_lp_optimum": { "jp8": "18475.029781", - "ck": "18568.580702" + "ck": "18568.580702", + "pr741_sw4_frame8": "18155.950422" }, "objective": "linear d*ln(48/d)", "runs": [ @@ -97,6 +98,60 @@ "temp": 0.5, "steps": 6000, "cpsat_optimum_after_reorder": "18480.391568" + }, + { + "word": "pr741_sw4_frame8", + "seed": 21, + "temp": 0.1, + "steps": 8000, + "least_frame_price_input": "18641.0284", + "least_frame_price_best": "18618.9770", + "exact_lp_optimum_after_reorder": "18161.312149" + }, + { + "word": "pr741_sw4_frame8", + "seed": 22, + "temp": 0.5, + "steps": 8000, + "least_frame_price_input": "18641.0284", + "least_frame_price_best": "18630.9575", + "exact_lp_optimum_after_reorder": "18155.950422" + }, + { + "word": "pr741_sw4_frame8", + "seed": 23, + "temp": 1.5, + "steps": 8000, + "least_frame_price_input": "18641.0284", + "least_frame_price_best": "18632.8670", + "exact_lp_optimum_after_reorder": "18160.449103" + }, + { + "word": "pr741_sw4_frame8", + "seed": 24, + "temp": 0.0, + "steps": 8000, + "least_frame_price_input": "18641.0284", + "least_frame_price_best": "18641.0284", + "exact_lp_optimum_after_reorder": "18155.950422" + }, + { + "word": "pr741_sw4_frame8", + "seed": 25, + "temp": 0.3, + "steps": 8000, + "least_frame_price_input": "18641.0284", + "least_frame_price_best": "18613.7716", + "exact_lp_optimum_after_reorder": "18161.312149" + }, + { + "word": "pr741_sw4_frame8", + "seed": 26, + "temp": 0.8, + "steps": 8000, + "least_frame_price_input": "18641.0284", + "least_frame_price_best": "18608.1993", + "exact_lp_optimum_after_reorder": "18161.312149" } ], "conclusion": "No sampled commuting reorder improves the exact frame optimum; the least-frame proxy gains come from dropping coalescences that the exact solve restores." diff --git a/research/frame-lift-search/README.md b/research/frame-lift-search/README.md index cec116270f..93bdef4272 100644 --- a/research/frame-lift-search/README.md +++ b/research/frame-lift-search/README.md @@ -3,6 +3,25 @@ Rohan Guliani (@Rohansguliani). Prepared with substantial AI assistance (an AI coding agent wrote the search code and ran the experiments under the author's direction). Apache-2.0. +## Current selected word (#741, eight B-frame coalescences after SW4) + +The exact frame solver was given PR699's SW4 word (`d232183f…`, the input of #741's `FRAME-RECIPE.json`). Using the +admissible model (hpe cone caps from the audit's pre-check, tail frames fixed), it returned in 27 s with CP-SAT +`OPTIMAL` and the profile `{1:2556,2:334,3:430,4:194,5:56,8:8}`. That is **exactly #741's profile**: the search +rediscovers the merged improvement automatically and certifies that it is complete. `check_sw4.py` applies #741's +recipe, reproduces its pinned output hash `e7804702…` and solves the frame LP on both words: + +| word | linear weight | LP optimum | exact-root weight (a* = #741 complex root) | LP optimum | +|---|---:|---:|---:|---:| +| PR699 SW4 input | 18162.854792 | 18155.950422 | 18226.598582 | 18219.665540 | +| #741 (selected) | 18155.950422050 | 18155.950422051 | 18219.665539989 | 18219.665539988 | + +So **no frame-only change of the selected SW4 word can raise κ**. Six commuting-reorder restarts on the #741 word, +each re-solved by the LP, gave 18155.950422 (twice) or higher (up to +5.36); see [ORDER-SEARCH.json](ORDER-SEARCH.json). The frame slack left by PR699 (6.90 linear and +6.93 exact-root units) is exactly what #741's eight frames recovered. The receipt is [RESULT-SW4.json](RESULT-SW4.json). + +## Earlier selected words (#626) + **Result (negative, scoped).** For the two complex provider words of the selected #626 construction (`jp8` and `ck`, content hashes pinned in [`complex-k492-owner-repair/data/SPEC.json`](../complex-k492-owner-repair/data/SPEC.json)), the paid local profile @@ -93,6 +112,9 @@ python3 -B research/complex-k492-owner-repair/verify.py --work /tmp/k492/complex python3 -B research/frame-lift-search/check.py --work /tmp/k492/complex --out /tmp/FRAME-LIFT.json # Optional: CP-SAT cross-check (needs `pip install ortools`) and the order search. python3 research/frame-lift-search/frame_exact.py /tmp/k492/complex/jp8-step6-cold_end/FULL-WORD.json.gz +# Current selected word: PR699 SW4 input (e.g. /sw4/sw4/FULL-WORD.json.gz from complex-sw4-frame8/verify.sh) +python3 -B research/frame-lift-search/check_sw4.py --input SW4-FULL-WORD.json.gz --out /tmp/FRAME-LIFT-SW4.json +python3 research/frame-lift-search/frame_exact.py SW4-FULL-WORD.json.gz --caps --recipe /tmp/recipe.json python3 research/frame-lift-search/order_search.py WORD.json.gz ORDER.json --steps 8000 --seed 1 python3 research/frame-lift-search/order_to_word.py WORD.json.gz ORDER.json REORDERED.json.gz python3 research/frame-lift-search/eval_lp.py REORDERED.json.gz diff --git a/research/frame-lift-search/RESULT-SW4.json b/research/frame-lift-search/RESULT-SW4.json new file mode 100644 index 0000000000..ddf56a7569 --- /dev/null +++ b/research/frame-lift-search/RESULT-SW4.json @@ -0,0 +1,47 @@ +{ + "input_sha256": "d232183f233899961bf55cac67a18545ed33548d9a7ca7078990d1a83d557c59", + "output_sha256": "e78047028c7dcd25fb1b6216c2b53eda76d2f91292b21d43f5d1903cc13a5c6c", + "exact_root": "1663966829367501881629/1000000000000000000000000", + "pr699_sw4": { + "linear": { + "input_weight": "18162.854791789", + "lp_optimum": "18155.950422051", + "gap": "6.904e+00" + }, + "exact_root": { + "input_weight": "18226.598582135", + "lp_optimum": "18219.665539988", + "gap": "6.933e+00" + }, + "paid_profile": { + "1": 2548, + "2": 342, + "3": 438, + "4": 186, + "5": 56, + "8": 8 + } + }, + "pr741_frame8": { + "linear": { + "input_weight": "18155.950422050", + "lp_optimum": "18155.950422051", + "gap": "-8.404e-10" + }, + "exact_root": { + "input_weight": "18219.665539989", + "lp_optimum": "18219.665539988", + "gap": "9.022e-10" + }, + "paid_profile": { + "1": 2556, + "2": 334, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + } + }, + "status": "PASS_741_IS_FRAME_OPTIMAL_AND_EQUALS_THE_PR699_FRAME_OPTIMUM", + "scope": "Same relaxation and LP as check.py (no cone caps, tail frames free); fixed SW4 gate sequence." +} diff --git a/research/frame-lift-search/check_sw4.py b/research/frame-lift-search/check_sw4.py new file mode 100644 index 0000000000..5e68b11ef6 --- /dev/null +++ b/research/frame-lift-search/check_sw4.py @@ -0,0 +1,60 @@ +"""Frame-only optimality of the current selected complex word (#741, eight B-frame coalescences after SW4). + +Input: PR699's SW4 word (content hash = complex-sw4-frame8/data/FRAME-RECIPE.json input_content_sha256), e.g. +/sw4/sw4/FULL-WORD.json.gz from `bash research/complex-sw4-frame8/verify.sh ` or PR699's replay. +Applies #741's frame recipe, checks the pinned output hash, then solves the frame LP (linear and exact-root +weights at #741's complex root) on both the input and the #741 word. + +usage: check_sw4.py --input SW4-FULL-WORD.json.gz --out RESULT-SW4.json +""" +import argparse, copy, gzip, hashlib, json, sys +from pathlib import Path +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import frame_lift as L +from frame_exact import interval +from check import chain_terms, chain_weight, lp_bound + +RECIPE = HERE.parent / 'complex-sw4-frame8/data/FRAME-RECIPE.json' +ROOT741 = '1663966829367501881629/1000000000000000000000000' +enc = lambda w: json.dumps(w, sort_keys=True, separators=(',', ':')).encode() + + +def solve(word): + ch, G, orig, lo = chain_terms(word) + dom = [interval(l, g) for l, g in zip(lo, G)] + out = {} + for name, exact in (('linear', False), ('exact_root', True)): + L.EXACT = exact + w_in = chain_weight(ch, orig); bound, nv, nr = lp_bound(ch, dom) + out[name] = dict(input_weight='%.9f' % w_in, lp_optimum='%.9f' % bound, gap='%.3e' % (w_in - bound)) + L.EXACT = False + out['paid_profile'] = {str(k): n for k, n in sorted(L.profile(word).items())} + return out + + +def main(): + ap = argparse.ArgumentParser(); ap.add_argument('--input', type=Path, required=True); ap.add_argument('--out', type=Path, required=True) + a = ap.parse_args() + L.A_STAR = float(__import__('fractions').Fraction(ROOT741)) + recipe = json.loads(RECIPE.read_text()) + w = json.loads(gzip.decompress(a.input.read_bytes())) + assert hashlib.sha256(enc(w)).hexdigest() == recipe['input_content_sha256'], 'not the pinned PR699 SW4 word' + z = copy.deepcopy(w) + for part, i, before, after in recipe['gate_frames']: + assert z[part][i][-1] == before; z[part][i][-1] = after + p = L.profile(z); z['report']['local_profile'] = {str(k): n for k, n in sorted(p.items())} + assert hashlib.sha256(enc(z)).hexdigest() == recipe['expected']['output_content_sha256'], 'recipe output hash' + res = dict(input_sha256=recipe['input_content_sha256'], output_sha256=recipe['expected']['output_content_sha256'], + exact_root=ROOT741, pr699_sw4=solve(w), pr741_frame8=solve(z)) + for k in ('linear', 'exact_root'): + best = float(res['pr741_frame8'][k]['lp_optimum']) + assert abs(float(res['pr699_sw4'][k]['lp_optimum']) - best) < 1e-6, 'frame optimum differs between input and #741' + assert float(res['pr741_frame8'][k]['input_weight']) - best < 1e-3, '#741 is not frame-optimal' + res['status'] = 'PASS_741_IS_FRAME_OPTIMAL_AND_EQUALS_THE_PR699_FRAME_OPTIMUM' + res['scope'] = 'Same relaxation and LP as check.py (no cone caps, tail frames free); fixed SW4 gate sequence.' + a.out.write_text(json.dumps(res, indent=2) + '\n'); print(json.dumps(res, indent=1)) + + +if __name__ == '__main__': + main() diff --git a/research/frame-lift-search/frame_exact.py b/research/frame-lift-search/frame_exact.py index 928d0b3bc6..ffd71813d6 100644 --- a/research/frame-lift-search/frame_exact.py +++ b/research/frame-lift-search/frame_exact.py @@ -39,12 +39,18 @@ def W(d): def main(): ap = argparse.ArgumentParser(); ap.add_argument('src'); ap.add_argument('out', nargs='?') - ap.add_argument('--time', type=float, default=600); ap.add_argument('--workers', type=int, default=8) + ap.add_argument('--time', type=float, default=600); ap.add_argument('--workers', type=int, default=8); ap.add_argument('--caps', action='store_true'); ap.add_argument('--recipe') a = ap.parse_args() from ortools.sat.python import cp_model word = json.load(gzip.open(a.src)) - ch = L.chains(word); G, orig = L.greatest(word); lo, pos = least(word, ch, len(orig)) + caps = L.cone_caps(word) if a.caps else None + print('cone caps', len(caps or {})) + ch = L.chains(word, caps); G, orig = L.greatest(word, caps); lo, pos = least(word, ch, len(orig)) + assert all(x & ~y == 0 for x, y in zip(lo, orig)) and all(x & ~y == 0 for x, y in zip(orig, G)) dom = [interval(l, g) for l, g in zip(lo, G)] + if a.caps: # admissible mode: early-cleanup (tail) frames are fixed by the word's early_cleanup list + for g, (part, _, _) in enumerate(L.events(word)): + if part == 'T': dom[g] = [orig[g]] print('domain sizes', sorted(Counter(map(len, dom)).items())) m = cp_model.CpModel() x = [{s: m.NewBoolVar('') for s in d} for d in dom] @@ -97,6 +103,13 @@ def main(): print('orig profile', dict(sorted(L.profile(word).items())), 'w %.6f' % base) print('best profile', dict(sorted(p.items())), 'w %.6f' % sum(L.W(d) * n for d, n in p.items())) print('changed gates', sum(o != y for o, y in zip(orig, X))) + if a.recipe: + gates = L.events(word); rows = [] + for (part, i, e), o, y in zip(gates, orig, X): + if o != y: + assert part in ('A', 'B'), 'tail frame change' + rows.append([part, i, e[-1], L.basis_of(y)]) + Path(a.recipe).write_text(json.dumps(rows) + '\n'); print('recipe gates', len(rows)) if a.out: w = L.apply_frames(word, X) assert L.profile(w) == p diff --git a/research/frame-lift-search/frame_lift.py b/research/frame-lift-search/frame_lift.py index a040b0219c..d31c4ed4d5 100644 --- a/research/frame-lift-search/frame_lift.py +++ b/research/frame-lift-search/frame_lift.py @@ -142,6 +142,9 @@ def greatest(word, endB_cap=None, pinned=()): nxt = final_frames(word) X = [FULLMASK] * len(gates) pinned = set(pinned) + if nAB == len(gates) and endB_cap: + for r, m in endB_cap.items(): + nxt[r] &= m for gi in range(len(gates) - 1, -1, -1): part, _, e = gates[gi] f = FULLMASK @@ -169,7 +172,7 @@ def greatest(word, endB_cap=None, pinned=()): # moment at a* changes by sum over climbs of d*(m/d)^a*/(m*W): a profile change raises the complex root iff it # lowers sum_climbs d*(73/d)^a*. FRAME_WEIGHT=exact uses that criterion (rescaled by 1/a*, minus the constant # idle term); the default is its a->0 linearisation d*ln(48/d). -A_STAR = 65528268492323474503 / 40000000000000000000000 +A_STAR = float(__import__('fractions').Fraction(__import__('os').environ.get('FRAME_ASTAR', '65528268492323474503/40000000000000000000000'))) EXACT = __import__('os').environ.get('FRAME_WEIGHT') == 'exact' @@ -181,6 +184,51 @@ def W(d, m=73, idle=48): return d * (math.log(m / d) - math.log(m / idle)) +def cone_caps(word): + """end-of-B upper bounds implied by the audit's hpe cone pre-check: for every hyperplane-ended helper h with + terminal U, each g in supp(row h of P^-1) and each g != h with P[g][h] != 0 must end B inside U.""" + from fractions import Fraction as Q + import copy + v = word['report']['v']; R = word['report']['R']; n = 2 * v + R + hf = {int(r): span_mask(f) for r, f in word.get('helper_final', {}).items()} + if not hf: + return {} + + def apply(e, rows): + if e[0] == 'scale': + q = Q(e[2], e[3]); rows[e[1]] = {j: q * x for j, x in rows[e[1]].items()} + else: + t, s, q = e[1], e[2], Q(e[3], e[4]) + for j, x in list(rows[s].items()): + z = rows[t].get(j, Q(0)) + q * x + if z: rows[t][j] = z + else: rows[t].pop(j, None) + + def inverse(e): + e = copy.deepcopy(e) + if e[0] == 'add': e[3] *= -1 + else: e[2], e[3] = e[3], e[2] + return e + main = word['A'] + word['cut'] + word['B'] + M = [{r: Q(1)} for r in range(n)] + for e in main: apply(e, M) + dirty = [{} for _ in range(n)] + for r in range(v, 2 * v): dirty[r] = {j: x for j, x in M[r].items() if j >= 2 * v} + for e in word['precondition']: apply(e, dirty) + comp = [['add', r, j, -q.numerator, q.denominator, []] for r in range(v, 2 * v) for j, q in sorted(dirty[r].items())] + prefix = word['precondition'] + comp + main + P = [{r: Q(1)} for r in range(n)] + for e in prefix: apply(e, P) + Pinv = [{r: Q(1)} for r in range(n)] + for e in reversed(prefix): apply(inverse(e), Pinv) + caps = {} + for h, U in hf.items(): + gs = {g for g, x in Pinv[h].items() if x} | {g for g in range(n) if g != h and P[g].get(h)} + for g in gs: + caps[g] = caps.get(g, FULLMASK) & U + return caps + + def chains(word, endB_cap=None): """per-register event chains: entries are ('g', gate id) or ('f', fixed mask).""" v = word['report']['v']; R = word['report']['R']; n = 2 * v + R @@ -205,6 +253,9 @@ def chains(word, endB_cap=None): ch[r].append(('cap', m)) for r in regs(e): ch[r].append(('g', gi)) + if nAB == len(gates) and endB_cap: + for r, m in endB_cap.items(): + ch[r].append(('cap', m)) for r, f in enumerate(final_frames(word)): ch[r].append(('f', f)) return ch