From b07bd2cb008d3601fd1eb03bd1af41b592ea895f Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Thu, 15 Oct 2026 01:51:27 +0000 Subject: [PATCH 1/3] Tooling: wire one-basis close into production frameopt with identical receipts Promote Ross Richardson's proved #1666 bit-frame-closure-basis adapter into research/bit589-frame-optimum/frameopt.py:close. Production verify.sh keeps identical PR589/PR555/degraded receipts; no new kappa. Prepared by Wentao Li with substantial AI assistance. --- .../bit-frame-closure-production/NOTICE.md | 20 ++ .../bit-frame-closure-production/README.md | 92 ++++++++ .../bit-frame-closure-production/SOURCES.json | 66 ++++++ .../bit-frame-closure-production/TASK.json | 70 ++++++ .../bit-frame-closure-production/VERIFY.json | 26 +++ .../bit-frame-closure-production/baseline.py | 210 ++++++++++++++++++ .../bit-frame-closure-production/benchmark.py | 202 +++++++++++++++++ .../bit-frame-closure-production/verify.py | 198 +++++++++++++++++ research/bit589-frame-optimum/frameopt.py | 49 +++- 9 files changed, 930 insertions(+), 3 deletions(-) create mode 100644 research/bit-frame-closure-production/NOTICE.md create mode 100644 research/bit-frame-closure-production/README.md create mode 100644 research/bit-frame-closure-production/SOURCES.json create mode 100644 research/bit-frame-closure-production/TASK.json create mode 100644 research/bit-frame-closure-production/VERIFY.json create mode 100644 research/bit-frame-closure-production/baseline.py create mode 100644 research/bit-frame-closure-production/benchmark.py create mode 100644 research/bit-frame-closure-production/verify.py diff --git a/research/bit-frame-closure-production/NOTICE.md b/research/bit-frame-closure-production/NOTICE.md new file mode 100644 index 0000000000..81a09c46c1 --- /dev/null +++ b/research/bit-frame-closure-production/NOTICE.md @@ -0,0 +1,20 @@ +# Attribution and license + +Prepared by Wentao Li ([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor), wentaol4@illinois.edu) with substantial +AI assistance for orientation, overlap search, profiling, production wiring, +packaging, benchmarking and writing. Not independent human peer review. +Apache-2.0; see the repository root `LICENSE`. + +The one-basis modular closure algorithm and its Hadamard-guard equivalence +argument were introduced by **Ross Richardson** in the opt-in adapter +`research/bit-frame-closure-basis/` (merged as +[CrocSwap/integer-mult-bounds#1666](https://github.com/CrocSwap/integer-mult-bounds/pull/1666); +see that package's NOTICE.md and PROOF.md). This package wires an equivalent +`close` into the production `research/bit589-frame-optimum/frameopt.py` path +used by `research/bit589-frame-optimum/verify.sh`. + +The original PR886 frame-only optimum checker, live-line catalogue and paid +profile accounting are by **Seth Burkart**, as refined during maintainer +integration of the bit589 frame-optimum package. Upstream material retains its +own source notices and license. diff --git a/research/bit-frame-closure-production/README.md b/research/bit-frame-closure-production/README.md new file mode 100644 index 0000000000..ab51448cf4 --- /dev/null +++ b/research/bit-frame-closure-production/README.md @@ -0,0 +1,92 @@ +# Production one-basis closure for the PR886 bit-frame checker + +**Tooling improvement; no new kappa.** At base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, +`research/bit589-frame-optimum/frameopt.py:close` still rebuilt a modular +elimination for every candidate live line. Ross Richardson's opt-in adapter +`research/bit-frame-closure-basis/` (merged [#1666](https://github.com/CrocSwap/integer-mult-bounds/pull/1666)) +already proved an exact one-basis reduction with identical receipts. This +package wires that equivalent `close` into the **production** source used by +`research/bit589-frame-optimum/verify.sh`. + +Every receipt field, all three stdout digests in +`research/bit-frame-closure-basis/EXPECTED.json`, the degraded positive control +and the `PASS_BIT589_FRAME_OPTIMUM` marker are unchanged. Selected frontier +untouched. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/bit-frame-closure-production/verify.py +python3.12 -I -O -B research/bit-frame-closure-production/verify.py +python3.12 -B scripts/research_package.py --package research/bit-frame-closure-production +python3.12 -I -B research/bit-frame-closure-production/benchmark.py --rounds 5 +``` + +Expected: + +```text +PASS_BIT_FRAME_CLOSURE_PRODUCTION cases=['pr589', 'pr555', 'degraded'] corruption=... certs=0 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/bit-frame-closure-production outcome=completed +PASS_IDENTICAL_BIT_FRAME_CLOSURE_PRODUCTION_RECEIPTS +``` + +Default verify is read-only. Timing is host-descriptive and is not a +correctness gate. Samples are retained in [`RESULT.json`](RESULT.json). + +## Why the one-basis close is equivalent + +For a nonempty mask `M` and live lines `L_i`, the historical checker returns + +```text +({i : rank_p(S ∪ {L_i}) = rank_p(S)}, rank_p(S)) where S = {L_i : i ∈ M}. +``` + +The production path builds one increasing-pivot echelon basis of `span_p(S)` +and admits each remaining live line exactly when its residual is zero. That is +the same membership predicate over the fixed prime field +`p = 2147483647`. The module-level Hadamard guard +`B^d < p^2` still justifies that modular rank equals rational rank on this +line table. The empty-mask result remains `(0, 0)`. Full details are in +`research/bit-frame-closure-basis/PROOF.md`. + +## Overlap and credit + +Closest priors: + +- [Ross Richardson / bit-frame-closure-basis](../bit-frame-closure-basis/) — + opt-in one-basis adapter (#1666); this package is the production wiring. +- [CrocSwap/integer-mult-bounds#756](https://github.com/CrocSwap/integer-mult-bounds/pull/756) + — identical-receipt tooling quality bar. +- Open leave-alone tooling on other objects (#1922 joint frames, #2054/#2150 + shared/mixed-point, #2100 ternary, #2117 DisjointTensor.frame_data, #2194 + production verify_factor, #2210 production leech_minor, #2231 sparse-fusion + orbits, #2239 joint-dual replay, #1861 parity-side) was not reopened. Fresh + overlap refresh over 475 open PRs found no competing production rewrite of + `frameopt.close`. + +Seth Burkart authored the PR886 frame-only optimum checker. Ross Richardson +authored the one-basis algorithm. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance, under +Apache-2.0. + +## Open next questions + +1. **Question:** Should `research/bit-frame-closure-basis/` note that production + now ships the same one-basis close? + **Why it matters:** That package's source-admission pins expect the + historical pairwise `frameopt.py` bytes. + **First step:** Add a one-line status note without editing pinned evidence. + **Blocked by:** Maintainer preference on touching incorporated historical + packages. + +2. **Question:** Should `research/r439-resynth-frame-seed10` refresh its + `frameopt.py` SHA-256 after this equivalence-preserving rewrite? + **Why it matters:** That package binds working-tree bytes; leaving the old + pin keeps this tooling PR focused. + **First step:** Dedicated provenance follow-up after confirming receipt + identity. + **Blocked by:** Pin repair outside this tooling change. diff --git a/research/bit-frame-closure-production/SOURCES.json b/research/bit-frame-closure-production/SOURCES.json new file mode 100644 index 0000000000..6fe1f56f3f --- /dev/null +++ b/research/bit-frame-closure-production/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/bit589-frame-optimum/frameopt.py", + "usage": "provenance", + "git_blob": "1622844ff90529c47e539f502c92b4f2371524e9", + "sha256": "d18d5ed96a6d3146b2141b9bdd29900dd612defdcd5ebc7040542064ec89f237" + }, + { + "path": "research/bit589-frame-optimum/verify.sh", + "usage": "input", + "git_blob": "4352170bc26141d630140647c2181f142289dd55", + "sha256": "eb69e2482686dd61f7727d58dc0ecd0aec5d34739b5d9b887f3c0b54c16f1c52" + }, + { + "path": "research/bit-frame-closure-basis/closure.py", + "usage": "input", + "git_blob": "df194142ca53d1d42938ec0525f71aea6b02a109", + "sha256": "febc46cb43be709684bb51e48bc2c849b63f02809e2bf5bb461c62d55953c4fd" + }, + { + "path": "research/bit-frame-closure-basis/PROOF.md", + "usage": "provenance", + "git_blob": "a086311e8af31c8a597c304e88fcff128f577c2b", + "sha256": "9c15c9f57ee3e8950dbc40235a9567d344507fcec9e50a69712150d59c50ae7b" + }, + { + "path": "research/bit-frame-closure-basis/EXPECTED.json", + "usage": "input", + "git_blob": "c8703852e7a02b1daa050ef250b468769ede73a7", + "sha256": "dac0e71d005bf700444f866209f588fef2a276ea6ce2cf17b6279e7881a5647e" + }, + { + "path": "research/bit-frame-closure-basis/README.md", + "usage": "provenance", + "git_blob": "e01fa237b7926fba0e9d94c0acd13ff228cf1490", + "sha256": "f98c95c5e9efc5c2383b459d5053837e72a47a927d36e759be7ad2fc942fc2ba" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz", + "usage": "input", + "git_blob": "bdbb95aa970647bd52895c120b494f0f591f3f87", + "sha256": "1bc3c53d4baf4927c6a00c339ea3975516471a48074d4d97c6addaded2a4d858" + } + ] +} diff --git a/research/bit-frame-closure-production/TASK.json b/research/bit-frame-closure-production/TASK.json new file mode 100644 index 0000000000..0f362fd6a5 --- /dev/null +++ b/research/bit-frame-closure-production/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_seed": "b78166147518e47337ab370b48c628f4", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected reproduction command and choose a single replay stage for profiling.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Can the production PR886 bit-frame checker (research/bit589-frame-optimum/frameopt.py:close, exercised by research/bit589-frame-optimum/verify.sh on the pinned PR589/PR555/degraded words) adopt the exact one-basis modular closure from research/bit-frame-closure-basis/ so the shipped verify path is faster while every receipt field, stdout digest and complete three-case suite stays identical?", + "scope_change_reason": "The catalogue draw suggested portable-replay; expertise override selected verifier-engineering after profiling showed production frameopt.close still rebuilt a modular elimination per candidate live line. Ross Richardson's incorporated #1666 opt-in adapter already proved an identical-receipt one-basis accelerator; production still paid the pairwise path. Leave-alone objects (joint frames, shared/mixed-point, ternary, parity-side, DisjointTensor.frame_data, verify_factor, leech_minor, sparse-fusion, joint-dual replay, quadratic-affine) and deferred micro-opts were not reopened.", + "bottleneck_link": "Side result on review throughput: the PR886 frame-only optimum is a retained historical obstruction replay. Faster identical close ranks do not change kappa or the binding complex supplier.", + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, packaging, benchmarking and writing", + "outcome": "completed", + "evidence": "PASS_BIT_FRAME_CLOSURE_PRODUCTION via research/bit-frame-closure-production/verify.py (also under -O); PASS_IDENTICAL_BIT_FRAME_CLOSURE_PRODUCTION_RECEIPTS via benchmark.py; production verify.sh still prints PASS_BIT589_FRAME_OPTIMUM; EXPECTED.json stdout digests unchanged.", + "author": "Wentao Li", + "email": "wentaol4@illinois.edu", + "github": "VictorLiwentao", + "budget_minutes": 60, + "stop_rule": "Ship an equivalence-preserving production frameopt.close change with frozen baseline, identical three-case receipts and stdout digests, temp-copy corruption rejection, registered replay and a measured before/after median. Do not invent kappa or reopen leave-alone objects.", + "open_questions": [ + { + "question": "Should research/bit-frame-closure-basis/ note that production now ships the same one-basis close?", + "why_it_matters": "That opt-in package's SOURCES.json pins the historical pairwise frameopt.py bytes and will fail source admission after this rewrite.", + "first_step": "Add a one-line status note and either refresh or relax that single pin without editing pinned mathematical evidence.", + "blocked_by": "Maintainer preference on touching incorporated historical packages." + }, + { + "question": "Should research/r439-resynth-frame-seed10 refresh its frameopt.py SHA-256 after this equivalence-preserving rewrite?", + "why_it_matters": "That package's SOURCES.json / CERTIFICATE.json bind working-tree frameopt.py bytes; leaving the old pin keeps this tooling PR focused.", + "first_step": "Dedicated provenance follow-up that only rewrites those pin entries after confirming receipt identity.", + "blocked_by": "Pin repair outside this tooling change." + } + ] +} diff --git a/research/bit-frame-closure-production/VERIFY.json b/research/bit-frame-closure-production/VERIFY.json new file mode 100644 index 0000000000..937b55d6e7 --- /dev/null +++ b/research/bit-frame-closure-production/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit589-frame-optimum/frameopt.py", + "research/bit589-frame-optimum/verify.sh", + "research/bit-frame-closure-basis/EXPECTED.json", + "research/bit-frame-closure-basis/closure.py", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Exact baseline copy of the base-commit frameopt.py; identical receipts and stdout digests for pr589/pr555/degraded against EXPECTED.json; production verify.sh PASS; temp-copy membership-omission corruption rejection; duplicate JSON-key check; read-only default." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Same package require() gates under -O; frameopt children still launch assertion-enabled." + } + ] +} diff --git a/research/bit-frame-closure-production/baseline.py b/research/bit-frame-closure-production/baseline.py new file mode 100644 index 0000000000..1622844ff9 --- /dev/null +++ b/research/bit-frame-closure-production/baseline.py @@ -0,0 +1,210 @@ +"""Exact frame-only optimum of a bitE8/1+mut bit word with its gate sequence fixed. + +Every gate g puts all its operands on one frame f_g; each register's frames must nest from its start to its final +frame. Targets stay at frame 0 until the scatter. Retained totals keep their scatter frames, so the COPY ranks and the +decoder constant do not change. Frames are closed sets of live lines. The paid profile counts each climb by its rank step. + +1. Forward least frames lo_g and backward greatest frames hi_g bound every legal f_g. Every closed frame between + them is enumerated. +2. Free gates (lo_g != hi_g) couple only through consecutive free gates on a register. A fixed gate in between pins + the frame there, so the components are independent in both legality and cost. +3. At z = c the moment sum_d n_d (d/(mW)) (m/d)^z is linear in the profile. A frame change can raise c only if it + lowers sum_d n_d d (m/d)^c. Each component is enumerated exhaustively and its best combination kept. + +Usage: frameopt.py WORD.json.gz C [--degrade] +--degrade is the positive control: every free gate starts at its least frame. +""" +import gzip, itertools, json, sys +from collections import Counter +from fractions import Fraction +from functools import reduce +from operator import or_, and_ + +w = json.load(gzip.open(sys.argv[1], 'rt')) +c = Fraction(sys.argv[2]) +V, N, L = w['v'], 2 * w['v'] + w['R'], w['lines'] +P = 2147483647 +# Hadamard: every nonzero integer minor has absolute value below P. +assert max(sum(x*x for x in line) for line in L) ** len(L[0]) < P**2 + + +def rank(rows): + rows, rk = [[x % P for x in r] for r in rows], 0 + for col in range(len(L[0])): + p = next((i for i in range(rk, len(rows)) if rows[i][col]), None) + if p is None: + continue + rows[rk], rows[p] = rows[p], rows[rk] + inv = pow(rows[rk][col], P - 2, P) + rows[rk] = [x * inv % P for x in rows[rk]] + for i in range(len(rows)): + if i != rk and rows[i][col]: + f = rows[i][col] + rows[i] = [(a - f * b) % P for a, b in zip(rows[i], rows[rk])] + rk += 1 + return rk + + +bits = lambda m: [i for i in range(V) if m >> i & 1] +_close = {} + + +def close(m): + """(closed line set spanned by mask m, its rank)""" + if m not in _close: + sel = [L[i] for i in bits(m)] + rk = rank(sel) if sel else 0 + _close[m] = (sum(1 << i for i in range(V) if m >> i & 1 or (sel and rank(sel + [L[i]]) == rk)), rk) + return _close[m] + + +dim = lambda m: close(m)[1] +FM = [sum(1 << i for i in f) for f in w['frames']] +assert all(close(m)[0] == m for m in FM), 'catalogue frame not closed' +SCATTER = ('S', 0, [], None) +gates = [(s, k, [g[1], *g[2]], FM[g[0]]) for s in 'DA' for k, g in enumerate(w[s])] + [SCATTER] + \ + [(s, k, [g[1], *g[2]], FM[g[0]]) for s in 'BC' for k, g in enumerate(w[s])] +start, final = [FM[f] for f in w['start']], [FM[f] for f in w['final']] +word = {(s, k): f for s, k, _, f in gates if s != 'S'} + +cur = start.copy() +for s, k, regs, f in gates[:gates.index(SCATTER)]: + for r in regs: + cur[r] = f +pin = {q: cur[q] for q in w['ret']} + +# 1. bounds +lo, cur = {}, start.copy() +for s, k, regs, f in gates: + if s == 'S': + assert all(cur[q] & ~pin[q] == 0 for q in pin) + for q in pin: + cur[q] = pin[q] + continue + lo[s, k] = m = close(reduce(or_, (cur[r] for r in regs)))[0] + for r in regs: + cur[r] = m +hi, ub = {}, final.copy() +for s, k, regs, f in reversed(gates): + if s == 'S': + for t in range(V, 2 * V): + ub[t] = 0 + for q in pin: + assert pin[q] & ~ub[q] == 0 + ub[q] = pin[q] + continue + hi[s, k] = m = reduce(and_, (ub[r] for r in regs)) # an intersection of closed sets is closed + for r in regs: + ub[r] = m +assert all(lo[x] & ~word[x] == 0 and word[x] & ~hi[x] == 0 for x in word), 'word frame outside its bounds' + +opts = {} +for x in word: + if lo[x] != hi[x]: + seen, todo = {lo[x]}, [lo[x]] + while todo: + m = todo.pop() + for i in bits(hi[x] & ~m): + n = close(m | 1 << i)[0] + if n & ~hi[x] == 0 and n not in seen: + seen.add(n) + todo.append(n) + opts[x] = sorted(seen, key=dim) + +# 2. components of free gates +parent = {x: x for x in opts} + + +def find(x): + while parent[x] != x: + x = parent[x] + return x + + +last = {} +for s, k, regs, f in gates: + for r in regs: + if (s, k) in opts and last.get(r) in opts: + parent[find(last[r])] = find((s, k)) + last[r] = (s, k) +members = {} +for x in opts: + members.setdefault(find(x), []).append(x) + + +# 3. exact enumeration +def profile(fr): + """paid profile (climbs plus COPY ranks) of a frame assignment, or None if some chain does not nest""" + cur, H = start.copy(), Counter() + for s, k, regs, _ in gates + [('F', 0, range(N), None)]: + if s == 'S': + H.update(dim(cur[q]) for q in pin) + continue + for r in regs: + m = final[r] if s == 'F' else fr[s, k] + if cur[r] != m: + if cur[r] & ~m: + return None + H[dim(m) - dim(cur[r])] += 1 + cur[r] = m + return H + + +# Exact outward rational bounds; no float decides a comparison. +import importlib.util +from pathlib import Path +from hashlib import sha256 +engine_path = Path(__file__).resolve().parents[1] / 'complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py' +assert sha256(engine_path.read_bytes()).hexdigest() == 'aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098' +spec = importlib.util.spec_from_file_location('frameopt_interval', engine_path) +engine = importlib.util.module_from_spec(spec); spec.loader.exec_module(engine) +prices = {d: tuple(64*x for x in engine.moment(64, 1, [(d, 1)], c)) for d in range(1, 9)} +def difference(H, G): + lo = hi = Fraction(0) + for d in set(H) | set(G): + n = H.get(d, 0) - G.get(d, 0) + l, u = prices[d] + lo += n*(l if n >= 0 else u) + hi += n*(u if n >= 0 else l) + assert H == G or hi < 0 or lo > 0, 'Unresolved interval comparison' + return lo, hi +cost = lambda H: sum(n*(prices[d][0]+prices[d][1])/2 for d,n in H.items()) +base = dict(word) +if '--degrade' in sys.argv: + base.update({x: lo[x] for x in opts}) +H0 = profile(base) +best, tried, illegal, ties, margins = dict(base), 0, 0, 0, [] +for xs in members.values(): + deltas = [] + for combo in itertools.product(*(opts[x] for x in xs)): + fr = dict(base) + fr.update(zip(xs, combo)) + H = profile(fr) + tried += 1 + if H is None: + illegal += 1 + elif H == H0: + ties += combo != tuple(base[x] for x in xs) + else: + lo_delta, hi_delta = difference(H, H0) + deltas.append(((lo_delta + hi_delta)/2, combo)) + if deltas: + d, combo = min(deltas) + selected = dict(base); selected.update(zip(xs, combo)); Hselected = profile(selected) + for _, other_combo in deltas: + other = dict(base); other.update(zip(xs, other_combo)); Hother = profile(other) + lo_check, hi_check = difference(Hother, Hselected) + assert Hother == Hselected or lo_check > 0, 'Minimum not certified' + margins.append(d) + if d < 0: + best.update(zip(xs, combo)) +H1 = profile(best) +result = dict( + word=sys.argv[1].rsplit('/', 1)[-1], degraded_start='--degrade' in sys.argv, gates=len(word), + free_gates=len(opts), components=len(members), component_sizes=dict(Counter(map(len, members.values()))), + assignments_enumerated=tried, non_nesting_rejected=illegal, same_profile_alternatives=ties, + start_profile=dict(sorted(H0.items())), optimum_profile=dict(sorted(H1.items())), + improving_components=sum(d < 0 for d in margins), + smallest_alternative_delta=float(min(margins)) if margins else None, weighted_cost_delta=float(cost(H1) - cost(H0)), + exact_interval_comparisons=True, rational_rank_justified_by_hadamard=True) +print(json.dumps(result)) diff --git a/research/bit-frame-closure-production/benchmark.py b/research/bit-frame-closure-production/benchmark.py new file mode 100644 index 0000000000..102c667234 --- /dev/null +++ b/research/bit-frame-closure-production/benchmark.py @@ -0,0 +1,202 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process before/after timings for production one-basis close. + +Timing is descriptive evidence for RESULT.json. Equivalence is enforced by +verify.py; this script fails only on unequal receipts or subprocess errors. +""" +from __future__ import annotations + +import argparse +from hashlib import sha256 +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent + +CASES = ( + ( + "pr589", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "1733427039589844234749/1000000000000000000000000", + False, + ), + ( + "pr555", + "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz", + "1733052823330162099157/1000000000000000000000000", + False, + ), + ( + "degraded", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "1733427039589844234749/1000000000000000000000000", + True, + ), +) + +WORKER = r""" +import json +import sys +import time +from pathlib import Path + +root = Path(sys.argv[1]) +engine = sys.argv[2] +scope = sys.argv[3] +cases = [ + ("pr589", "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "1733427039589844234749/1000000000000000000000000", False), + ("pr555", "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz", + "1733052823330162099157/1000000000000000000000000", False), + ("degraded", "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "1733427039589844234749/1000000000000000000000000", True), +] +if engine == "baseline": + script = root / "research/bit-frame-closure-production/baseline.py" +else: + script = root / "research/bit589-frame-optimum/frameopt.py" +selected = [row for row in cases if scope == "suite" or row[0] == scope] +assert selected, scope +import subprocess, os +env = os.environ.copy() +env.pop("PYTHONOPTIMIZE", None) +env["PYTHONDONTWRITEBYTECODE"] = "1" +receipts = {} +t0 = time.perf_counter() +for name, word, endpoint, degraded in selected: + cmd = [sys.executable, "-I", "-B", str(script), str(root / word), endpoint] + if degraded: + cmd.append("--degrade") + proc = subprocess.run(cmd, cwd=root, env=env, capture_output=True, text=True) + if proc.returncode != 0: + raise SystemExit(proc.stderr + proc.stdout) + receipts[name] = json.loads(proc.stdout) +elapsed = time.perf_counter() - t0 +print(json.dumps({"elapsed": elapsed, "receipts": receipts}, sort_keys=True)) +""" + + +def run_engine(engine: str, scope: str) -> dict: + env = os.environ.copy() + env.pop("PYTHONOPTIMIZE", None) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run( + [sys.executable, "-I", "-B", "-c", WORKER, str(ROOT), engine, scope], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + ) + if proc.returncode != 0: + raise SystemExit(f"engine={engine} scope={scope} failed\n{proc.stderr}\n{proc.stdout}") + return json.loads(proc.stdout.strip().splitlines()[-1]) + + +def measure(scope: str, rounds: int) -> dict: + baseline_samples = [] + optimized_samples = [] + reference = None + samples = [] + for round_index in range(rounds): + order = ("baseline", "optimized") if round_index % 2 == 0 else ("optimized", "baseline") + pair = {} + for engine in order: + payload = run_engine(engine, scope) + if reference is None: + reference = payload["receipts"] + elif payload["receipts"] != reference: + raise SystemExit(f"receipt mismatch scope={scope} round={round_index} engine={engine}") + pair[engine] = payload["elapsed"] + baseline_samples.append(pair["baseline"]) + optimized_samples.append(pair["optimized"]) + samples.append( + { + "round": round_index, + "order": list(order), + "baseline_seconds": pair["baseline"], + "optimized_seconds": pair["optimized"], + "ratio": pair["baseline"] / pair["optimized"] if pair["optimized"] else None, + } + ) + print( + f"scope={scope} round={round_index} order={order[0]}->{order[1]} " + f"baseline={pair['baseline']:.6f}s optimized={pair['optimized']:.6f}s", + flush=True, + ) + base_med = statistics.median(baseline_samples) + opt_med = statistics.median(optimized_samples) + return { + "scope": scope, + "rounds": rounds, + "median_baseline_seconds": base_med, + "median_optimized_seconds": opt_med, + "median_ratio": base_med / opt_med if opt_med else None, + "samples": samples, + } + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--rounds", type=int, default=5) + parser.add_argument("--output", type=Path, default=PACKAGE / "RESULT.json") + args = parser.parse_args(argv) + if args.rounds < 1: + raise SystemExit("--rounds must be >= 1") + + single = measure("pr589", args.rounds) + suite = measure("suite", args.rounds) + result = { + "status": "PASS_IDENTICAL_BIT_FRAME_CLOSURE_PRODUCTION_RECEIPTS", + "ai_assistance": ( + "Substantial AI assistance for orientation, overlap search, profiling, " + "production wiring, packaging, benchmarking and writing. Not independent " + "human peer review." + ), + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "predecessor": "research/bit-frame-closure-basis/", + "engines": { + "baseline": "research/bit-frame-closure-production/baseline.py", + "optimized": "research/bit589-frame-optimum/frameopt.py", + }, + "source_sha256": { + "baseline.py": sha256((PACKAGE / "baseline.py").read_bytes()).hexdigest(), + "research/bit589-frame-optimum/frameopt.py": sha256( + (ROOT / "research/bit589-frame-optimum/frameopt.py").read_bytes() + ).hexdigest(), + "research/bit-frame-closure-basis/closure.py": sha256( + (ROOT / "research/bit-frame-closure-basis/closure.py").read_bytes() + ).hexdigest(), + }, + "environment": { + "python": sys.version, + "executable": sys.executable, + "platform": platform.platform(), + "implementation": platform.python_implementation(), + "os_caches_flushed": False, + "cpu_affinity_set": False, + }, + "pr589_only": single, + "complete_three_case_suite": suite, + "no_new_kappa": True, + } + args.output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print(result["status"]) + print( + f"pr589_median {single['median_baseline_seconds']:.6f} -> " + f"{single['median_optimized_seconds']:.6f} ({single['median_ratio']:.3f}x)" + ) + print( + f"suite_median {suite['median_baseline_seconds']:.6f} -> " + f"{suite['median_optimized_seconds']:.6f} ({suite['median_ratio']:.3f}x)" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/bit-frame-closure-production/verify.py b/research/bit-frame-closure-production/verify.py new file mode 100644 index 0000000000..9ab64f15c0 --- /dev/null +++ b/research/bit-frame-closure-production/verify.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +"""Equivalence, rejection and receipt controls for production one-basis close. + +Read-only by default. Timing is not a pass gate; see benchmark.py / RESULT.json. +""" +from __future__ import annotations + +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +PRODUCTION = ROOT / "research/bit589-frame-optimum/frameopt.py" +BASELINE = PACKAGE / "baseline.py" +EXPECTED = ROOT / "research/bit-frame-closure-basis/EXPECTED.json" + +BASE_COMMIT = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +ORIGINAL_BLOB = "1622844ff90529c47e539f502c92b4f2371524e9" +ORIGINAL_SHA256 = "d18d5ed96a6d3146b2141b9bdd29900dd612defdcd5ebc7040542064ec89f237" +OPTIMIZED_SHA256 = "0cbcda715cfb9f9b17c8e2bd30f90f34fa08e3d467f262e6ba4837b20d17eced" + +CASES = { + "pr589": ( + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "1733427039589844234749/1000000000000000000000000", + False, + ), + "pr555": ( + "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz", + "1733052823330162099157/1000000000000000000000000", + False, + ), + "degraded": ( + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "1733427039589844234749/1000000000000000000000000", + True, + ), +} + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def digest_file(path: Path) -> str: + return sha256(path.read_bytes()).hexdigest() + + +def unique_object(pairs): + out = {} + for key, value in pairs: + require(key not in out, f"duplicate JSON key: {key}") + out[key] = value + return out + + +def load_json_unique(path: Path): + return json.loads(path.read_text(encoding="utf-8"), object_pairs_hook=unique_object) + + +def run_frameopt(script: Path, case: str) -> tuple[dict, str]: + """Run one checker under assertion-enabled -I -B (never inherit -O).""" + word, endpoint, degraded = CASES[case] + cmd = [ + sys.executable, + "-I", + "-B", + str(script), + str(ROOT / word), + endpoint, + ] + if degraded: + cmd.append("--degrade") + env = dict(**{k: v for k, v in __import__("os").environ.items() if k != "PYTHONOPTIMIZE"}) + env["PYTHONDONTWRITEBYTECODE"] = "1" + proc = subprocess.run(cmd, cwd=ROOT, env=env, capture_output=True, text=True) + require(proc.returncode == 0, f"{script.name} case={case} failed\n{proc.stderr}\n{proc.stdout}") + text = proc.stdout + receipt = json.loads(text) + return receipt, text + + +def check_baseline_bytes() -> None: + original = subprocess.check_output( + ["git", "show", f"{BASE_COMMIT}:research/bit589-frame-optimum/frameopt.py"], + cwd=ROOT, + ) + require(sha256(original).hexdigest() == ORIGINAL_SHA256, "base frameopt.py sha256 drift") + blob = ( + subprocess.check_output( + ["git", "rev-parse", f"{BASE_COMMIT}:research/bit589-frame-optimum/frameopt.py"], + cwd=ROOT, + ) + .decode() + .strip() + ) + require(blob == ORIGINAL_BLOB, "base frameopt.py blob drift") + require(BASELINE.read_bytes() == original, "baseline.py must equal the base-commit frameopt.py") + require( + digest_file(PRODUCTION) == OPTIMIZED_SHA256, + "production frameopt.py does not match the claimed optimized digest", + ) + require(PRODUCTION.read_bytes() != original, "production must differ from the pairwise baseline") + + +def check_case_equivalence() -> list[dict]: + expected = load_json_unique(EXPECTED) + rows = [] + for case in CASES: + base_receipt, base_text = run_frameopt(BASELINE, case) + prod_receipt, prod_text = run_frameopt(PRODUCTION, case) + require(base_receipt == prod_receipt, f"receipt mismatch case={case}") + require( + sha256(base_text.encode()).hexdigest() + == sha256(prod_text.encode()).hexdigest() + == expected[case]["stdout_sha256"], + f"stdout digest mismatch case={case}", + ) + require(prod_receipt == expected[case]["receipt"], f"EXPECTED receipt mismatch case={case}") + rows.append( + { + "case": case, + "stdout_sha256": expected[case]["stdout_sha256"], + "improving_components": prod_receipt["improving_components"], + "assignments_enumerated": prod_receipt["assignments_enumerated"], + } + ) + return rows + + +def check_temp_corruption_rejection() -> dict: + """On-disk mutant in a temp copy must diverge from the honest production receipt.""" + honest, _ = run_frameopt(PRODUCTION, "pr589") + with tempfile.TemporaryDirectory(prefix="bit-frame-closure-prod-") as tmp: + stage = Path(tmp) + mutant = stage / "frameopt.py" + text = PRODUCTION.read_text(encoding="utf-8") + # Drop membership admission: closed stays equal to the input mask. + needle = "if not (m >> i & 1) and _in_span(L[i], basis):\n closed |= 1 << i\n" + require(needle in text, "membership block missing for corruption control") + mutant.write_text(text.replace(needle, "if False and _in_span(L[i], basis):\n closed |= 1 << i\n", 1), encoding="utf-8") + require(mutant.read_bytes() != PRODUCTION.read_bytes(), "mutant must differ on disk") + try: + bad, _ = run_frameopt(mutant, "pr589") + except AssertionError as exc: + return {"rejected": True, "mode": "subprocess_failure", "detail": str(exc)[:200]} + require(bad != honest, "membership-omission mutant must change the pr589 receipt") + return {"rejected": True, "mode": "receipt_divergence", "honest_improving": honest["improving_components"], "mutant_improving": bad["improving_components"]} + + +def check_verify_sh() -> None: + env = dict(**{k: v for k, v in __import__("os").environ.items() if k != "PYTHONOPTIMIZE"}) + env["PYTHONDONTWRITEBYTECODE"] = "1" + env["PY"] = sys.executable + proc = subprocess.run( + ["bash", str(ROOT / "research/bit589-frame-optimum/verify.sh")], + cwd=ROOT, + env=env, + capture_output=True, + text=True, + ) + require(proc.returncode == 0, f"verify.sh failed\n{proc.stderr}\n{proc.stdout}") + require(proc.stdout.strip().splitlines()[-1] == "PASS_BIT589_FRAME_OPTIMUM", "verify.sh marker") + + +def main(argv: list[str] | None = None) -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write-result", + action="store_true", + help="unused placeholder; default verify is read-only and never writes certificates", + ) + args = parser.parse_args(argv) + require(not args.write_result, "default verify is read-only; do not pass --write-result") + + check_baseline_bytes() + cases = check_case_equivalence() + corruption = check_temp_corruption_rejection() + check_verify_sh() + + print( + "PASS_BIT_FRAME_CLOSURE_PRODUCTION " + f"cases={[row['case'] for row in cases]} " + f"corruption={corruption['mode']} " + "certs=0 no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/bit589-frame-optimum/frameopt.py b/research/bit589-frame-optimum/frameopt.py index 1622844ff9..f069583a7c 100644 --- a/research/bit589-frame-optimum/frameopt.py +++ b/research/bit589-frame-optimum/frameopt.py @@ -47,14 +47,57 @@ def rank(rows): bits = lambda m: [i for i in range(V) if m >> i & 1] _close = {} +# One-basis closure (Ross Richardson #1666 / research/bit-frame-closure-basis): +# build one echelon basis of span(S) and test remaining live lines for membership. +# Equivalent to the historical per-candidate rank(S ∪ {L_i}) == rank(S) predicate. + + +def _echelon(rows): + """Increasing-pivot, unit-pivot basis over the fixed prime field.""" + basis, width = [], len(L[0]) + for source in rows: + row = [x % P for x in source] + for pivot, vector in basis: + factor = row[pivot] + if factor: + for j in range(pivot, width): + row[j] = (row[j] - factor * vector[j]) % P + pivot = next((j for j, x in enumerate(row) if x), None) + if pivot is not None: + inv = pow(row[pivot], P - 2, P) + row = tuple(x * inv % P for x in row) + basis.append((pivot, row)) + basis.sort(key=lambda item: item[0]) + return basis + + +def _in_span(source, basis): + row = [x % P for x in source] + for pivot, vector in basis: + factor = row[pivot] + if factor: + for j in range(pivot, len(row)): + row[j] = (row[j] - factor * vector[j]) % P + return not any(row) def close(m): """(closed line set spanned by mask m, its rank)""" if m not in _close: - sel = [L[i] for i in bits(m)] - rk = rank(sel) if sel else 0 - _close[m] = (sum(1 << i for i in range(V) if m >> i & 1 or (sel and rank(sel + [L[i]]) == rk)), rk) + if not m: + # Preserve the historical empty-selection convention. + _close[m] = (0, 0) + else: + basis = _echelon(L[i] for i in bits(m)) + rk = len(basis) + if rk == len(L[0]): + closed = (1 << V) - 1 + else: + closed = m + for i in range(V): + if not (m >> i & 1) and _in_span(L[i], basis): + closed |= 1 << i + _close[m] = (closed, rk) return _close[m] From 4d822cc0aeb2170d8650c605c4c42f222291bc37 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Thu, 15 Oct 2026 02:13:15 +0000 Subject: [PATCH 2/3] Tooling: record frameopt production benchmark and corruption control MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five alternating pairs: suite median 47.744→8.904s (5.362×) with identical receipts. Tighten temp-copy foil to always-admit _in_span for bounded rejection. Prepared by Wentao Li with substantial AI assistance. --- .../bit-frame-closure-production/README.md | 5 +- .../bit-frame-closure-production/RESULT.json | 142 ++++++++++++++++++ .../bit-frame-closure-production/VERIFY.json | 2 +- .../bit-frame-closure-production/verify.py | 31 +++- 4 files changed, 170 insertions(+), 10 deletions(-) create mode 100644 research/bit-frame-closure-production/RESULT.json diff --git a/research/bit-frame-closure-production/README.md b/research/bit-frame-closure-production/README.md index ab51448cf4..4e16ea005a 100644 --- a/research/bit-frame-closure-production/README.md +++ b/research/bit-frame-closure-production/README.md @@ -34,7 +34,10 @@ PASS_IDENTICAL_BIT_FRAME_CLOSURE_PRODUCTION_RECEIPTS ``` Default verify is read-only. Timing is host-descriptive and is not a -correctness gate. Samples are retained in [`RESULT.json`](RESULT.json). +correctness gate. On Linux / CPython 3.12.3, five alternating fresh-process +pairs gave median **pr589 17.298 → 3.213 s (5.383×)** and **complete three-case +suite 47.744 → 8.904 s (5.362×)**. Samples are retained in +[`RESULT.json`](RESULT.json). ## Why the one-basis close is equivalent diff --git a/research/bit-frame-closure-production/RESULT.json b/research/bit-frame-closure-production/RESULT.json new file mode 100644 index 0000000000..ae02e9b45e --- /dev/null +++ b/research/bit-frame-closure-production/RESULT.json @@ -0,0 +1,142 @@ +{ + "ai_assistance": "Substantial AI assistance for orientation, overlap search, profiling, production wiring, packaging, benchmarking and writing. Not independent human peer review.", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "complete_three_case_suite": { + "median_baseline_seconds": 47.74427043100013, + "median_optimized_seconds": 8.903693554000256, + "median_ratio": 5.36229938074964, + "rounds": 5, + "samples": [ + { + "baseline_seconds": 50.23534307199998, + "optimized_seconds": 9.116682268999966, + "order": [ + "baseline", + "optimized" + ], + "ratio": 5.51026586095014, + "round": 0 + }, + { + "baseline_seconds": 48.14631975800012, + "optimized_seconds": 9.367295856000055, + "order": [ + "optimized", + "baseline" + ], + "ratio": 5.139831227510642, + "round": 1 + }, + { + "baseline_seconds": 47.708987005000154, + "optimized_seconds": 8.903693554000256, + "order": [ + "baseline", + "optimized" + ], + "ratio": 5.358336595441949, + "round": 2 + }, + { + "baseline_seconds": 47.74427043100013, + "optimized_seconds": 8.554956250000032, + "order": [ + "optimized", + "baseline" + ], + "ratio": 5.580890075387581, + "round": 3 + }, + { + "baseline_seconds": 46.38257842299981, + "optimized_seconds": 8.464688658000341, + "order": [ + "baseline", + "optimized" + ], + "ratio": 5.479537440418632, + "round": 4 + } + ], + "scope": "suite" + }, + "engines": { + "baseline": "research/bit-frame-closure-production/baseline.py", + "optimized": "research/bit589-frame-optimum/frameopt.py" + }, + "environment": { + "cpu_affinity_set": false, + "executable": "/usr/bin/python3.12", + "implementation": "CPython", + "os_caches_flushed": false, + "platform": "Linux-6.12.94+-x86_64-with-glibc2.39", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]" + }, + "no_new_kappa": true, + "pr589_only": { + "median_baseline_seconds": 17.29837664899992, + "median_optimized_seconds": 3.21332176299984, + "median_ratio": 5.383331619069105, + "rounds": 5, + "samples": [ + { + "baseline_seconds": 18.543131178000067, + "optimized_seconds": 3.0485810260001927, + "order": [ + "baseline", + "optimized" + ], + "ratio": 6.082544967594013, + "round": 0 + }, + { + "baseline_seconds": 17.29837664899992, + "optimized_seconds": 3.248697127000014, + "order": [ + "optimized", + "baseline" + ], + "ratio": 5.324712022315845, + "round": 1 + }, + { + "baseline_seconds": 16.61269226399986, + "optimized_seconds": 3.075237322000021, + "order": [ + "baseline", + "optimized" + ], + "ratio": 5.402084627795678, + "round": 2 + }, + { + "baseline_seconds": 17.327575813000067, + "optimized_seconds": 3.21332176299984, + "order": [ + "optimized", + "baseline" + ], + "ratio": 5.39241852855211, + "round": 3 + }, + { + "baseline_seconds": 16.734536901000183, + "optimized_seconds": 3.42617271600011, + "order": [ + "baseline", + "optimized" + ], + "ratio": 4.884323788713413, + "round": 4 + } + ], + "scope": "pr589" + }, + "predecessor": "research/bit-frame-closure-basis/", + "source_sha256": { + "baseline.py": "d18d5ed96a6d3146b2141b9bdd29900dd612defdcd5ebc7040542064ec89f237", + "research/bit-frame-closure-basis/closure.py": "febc46cb43be709684bb51e48bc2c849b63f02809e2bf5bb461c62d55953c4fd", + "research/bit589-frame-optimum/frameopt.py": "0cbcda715cfb9f9b17c8e2bd30f90f34fa08e3d467f262e6ba4837b20d17eced" + }, + "status": "PASS_IDENTICAL_BIT_FRAME_CLOSURE_PRODUCTION_RECEIPTS" +} diff --git a/research/bit-frame-closure-production/VERIFY.json b/research/bit-frame-closure-production/VERIFY.json index 937b55d6e7..ff98a28677 100644 --- a/research/bit-frame-closure-production/VERIFY.json +++ b/research/bit-frame-closure-production/VERIFY.json @@ -15,7 +15,7 @@ { "argv": ["{python}", "-I", "-B", "{package}/verify.py"], "timeout_seconds": 600, - "checks": "Exact baseline copy of the base-commit frameopt.py; identical receipts and stdout digests for pr589/pr555/degraded against EXPECTED.json; production verify.sh PASS; temp-copy membership-omission corruption rejection; duplicate JSON-key check; read-only default." + "checks": "Exact baseline copy of the base-commit frameopt.py; identical receipts and stdout digests for pr589/pr555/degraded against EXPECTED.json; production verify.sh PASS; temp-copy always-admit _in_span corruption rejection; duplicate JSON-key check; read-only default." }, { "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], diff --git a/research/bit-frame-closure-production/verify.py b/research/bit-frame-closure-production/verify.py index 9ab64f15c0..3b75c49ce1 100644 --- a/research/bit-frame-closure-production/verify.py +++ b/research/bit-frame-closure-production/verify.py @@ -136,23 +136,38 @@ def check_case_equivalence() -> list[dict]: def check_temp_corruption_rejection() -> dict: - """On-disk mutant in a temp copy must diverge from the honest production receipt.""" + """On-disk mutant in a temp copy must fail or diverge from the honest receipt. + + The foil forces `_in_span` to accept every live line. Catalogue frames then + fail the inherited `close(m)[0] == m` assertion immediately, so the control + stays bounded (a membership-omission foil can otherwise wander through a + huge illegal search). + """ honest, _ = run_frameopt(PRODUCTION, "pr589") with tempfile.TemporaryDirectory(prefix="bit-frame-closure-prod-") as tmp: stage = Path(tmp) mutant = stage / "frameopt.py" text = PRODUCTION.read_text(encoding="utf-8") - # Drop membership admission: closed stays equal to the input mask. - needle = "if not (m >> i & 1) and _in_span(L[i], basis):\n closed |= 1 << i\n" - require(needle in text, "membership block missing for corruption control") - mutant.write_text(text.replace(needle, "if False and _in_span(L[i], basis):\n closed |= 1 << i\n", 1), encoding="utf-8") + needle = "def _in_span(source, basis):\n row = [x % P for x in source]\n" + require(needle in text, "_in_span header missing for corruption control") + foil = ( + "def _in_span(source, basis):\n" + " return True\n" + " row = [x % P for x in source]\n" + ) + mutant.write_text(text.replace(needle, foil, 1), encoding="utf-8") require(mutant.read_bytes() != PRODUCTION.read_bytes(), "mutant must differ on disk") try: bad, _ = run_frameopt(mutant, "pr589") except AssertionError as exc: - return {"rejected": True, "mode": "subprocess_failure", "detail": str(exc)[:200]} - require(bad != honest, "membership-omission mutant must change the pr589 receipt") - return {"rejected": True, "mode": "receipt_divergence", "honest_improving": honest["improving_components"], "mutant_improving": bad["improving_components"]} + return {"rejected": True, "mode": "subprocess_failure", "detail": str(exc)[:240]} + require(bad != honest, "always-admit mutant must change the pr589 receipt") + return { + "rejected": True, + "mode": "receipt_divergence", + "honest_improving": honest["improving_components"], + "mutant_improving": bad["improving_components"], + } def check_verify_sh() -> None: From e45c48ca6b44b917d8114140a8715352667795ea Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Thu, 15 Oct 2026 02:28:44 +0000 Subject: [PATCH 3/3] Tooling: demote historical frameopt pin in bit-frame-closure-basis to provenance After production one-basis close, keep the pairwise digest as provenance so research-packages CI no longer fails working source drift when frameopt.py changes. Live VERIFY/run inputs drop that path; basis verify still PASSes. Prepared by Wentao Li with substantial AI assistance. --- .../bit-frame-closure-basis/BENCHMARK.json | 336 +++++++++--------- research/bit-frame-closure-basis/README.md | 2 + research/bit-frame-closure-basis/SOURCES.json | 2 +- research/bit-frame-closure-basis/VERIFY.json | 1 - research/bit-frame-closure-basis/run.py | 2 +- 5 files changed, 172 insertions(+), 171 deletions(-) diff --git a/research/bit-frame-closure-basis/BENCHMARK.json b/research/bit-frame-closure-basis/BENCHMARK.json index b81c66186f..2d43a353e3 100644 --- a/research/bit-frame-closure-basis/BENCHMARK.json +++ b/research/bit-frame-closure-basis/BENCHMARK.json @@ -1,251 +1,251 @@ { - "status": "PASS_BIT_FRAME_CLOSURE_BENCHMARK", + "executable": "/opt/homebrew/opt/python@3.12/bin/python3.12", + "finished_at": "2026-10-14T05:45:21.412584+00:00", + "implementation_sha256": { + "EXPECTED.json": "dac0e71d005bf700444f866209f588fef2a276ea6ce2cf17b6279e7881a5647e", + "SOURCES.json": "949964a1d1da371cc2347aba6543f088cc47dbb65392a2aabc3c4e21f930e3bf", + "benchmark.py": "d579af460de5d8b076403714c17ba8595d900ad6a5c51d84f5e63ab28723ade4", + "closure.py": "febc46cb43be709684bb51e48bc2c849b63f02809e2bf5bb461c62d55953c4fd", + "run.py": "82a8d9fdccd7e5c99884d02255ddf4f66657424521e6427d68caeea6b7d3a1f2" + }, + "median_case_seconds": { + "degraded": { + "basis": 2.0303760420065373, + "reference": 11.144659584038891 + }, + "pr555": { + "basis": 1.8459598339395598, + "reference": 10.765563208027743 + }, + "pr589": { + "basis": 2.030974750057794, + "reference": 10.703001499990933 + } + }, + "median_suite_seconds": { + "basis": 5.907537999912165, + "reference": 32.6134802919114 + }, + "platform": "macOS-26.5.2-arm64-arm-64bit", + "python": "3.12.12 (main, Oct 9 2025, 11:07:00) [Clang 17.0.0 (clang-1700.6.3.2)]", "samples": [ { - "pair": 0, - "order": [ - "reference", - "basis" - ], "engines": { - "reference": { - "seconds": 30.93506745796185, + "basis": { "cases": { - "pr589": { - "seconds": 10.3824437080184, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 1.983572750003077 }, "pr555": { - "seconds": 10.024701665970497, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 1.7693556669401005 }, - "degraded": { - "seconds": 10.527642667060718, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 1.9619243339402601 } - } + }, + "seconds": 5.71508595906198 }, - "basis": { - "seconds": 5.71508595906198, + "reference": { "cases": { - "pr589": { - "seconds": 1.9619243339402601, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 10.527642667060718 }, "pr555": { - "seconds": 1.7693556669401005, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 10.024701665970497 }, - "degraded": { - "seconds": 1.983572750003077, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 10.3824437080184 } - } + }, + "seconds": 30.93506745796185 } - } - }, - { - "pair": 1, + }, "order": [ - "basis", - "reference" + "reference", + "basis" ], + "pair": 0 + }, + { "engines": { "basis": { - "seconds": 5.703479459043592, "cases": { - "pr589": { - "seconds": 1.9423902080161497, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 1.9654521669726819 }, "pr555": { - "seconds": 1.7954174579354003, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 1.7954174579354003 }, - "degraded": { - "seconds": 1.9654521669726819, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 1.9423902080161497 } - } + }, + "seconds": 5.703479459043592 }, "reference": { - "seconds": 30.964114416972734, "cases": { - "pr589": { - "seconds": 10.366719332989305, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 10.494463707902469 }, "pr555": { - "seconds": 10.102655207971111, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 10.102655207971111 }, - "degraded": { - "seconds": 10.494463707902469, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 10.366719332989305 } - } + }, + "seconds": 30.964114416972734 } - } - }, - { - "pair": 2, + }, "order": [ - "reference", - "basis" + "basis", + "reference" ], + "pair": 1 + }, + { "engines": { - "reference": { - "seconds": 32.6134802919114, + "basis": { "cases": { - "pr589": { - "seconds": 10.703001499990933, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 2.0303760420065373 }, "pr555": { - "seconds": 10.765563208027743, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 1.8459598339395598 }, - "degraded": { - "seconds": 11.144659584038891, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 2.030974750057794 } - } + }, + "seconds": 5.907537999912165 }, - "basis": { - "seconds": 5.907537999912165, + "reference": { "cases": { - "pr589": { - "seconds": 2.030974750057794, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 11.144659584038891 }, "pr555": { - "seconds": 1.8459598339395598, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 10.765563208027743 }, - "degraded": { - "seconds": 2.0303760420065373, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 10.703001499990933 } - } + }, + "seconds": 32.6134802919114 } - } - }, - { - "pair": 3, + }, "order": [ - "basis", - "reference" + "reference", + "basis" ], + "pair": 2 + }, + { "engines": { "basis": { - "seconds": 6.311234583030455, "cases": { - "pr589": { - "seconds": 2.0816027499968186, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 2.1659246659837663 }, "pr555": { - "seconds": 2.063415333046578, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 2.063415333046578 }, - "degraded": { - "seconds": 2.1659246659837663, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 2.0816027499968186 } - } + }, + "seconds": 6.311234583030455 }, "reference": { - "seconds": 43.282476166961715, "cases": { - "pr589": { - "seconds": 12.81674420798663, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 15.380409959005192 }, "pr555": { - "seconds": 15.084301250055432, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 15.084301250055432 }, - "degraded": { - "seconds": 15.380409959005192, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 12.81674420798663 } - } + }, + "seconds": 43.282476166961715 } - } - }, - { - "pair": 4, + }, "order": [ - "reference", - "basis" + "basis", + "reference" ], + "pair": 3 + }, + { "engines": { - "reference": { - "seconds": 50.12656000000425, + "basis": { "cases": { - "pr589": { - "seconds": 15.884748458047397, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 3.175984041998163 }, "pr555": { - "seconds": 14.376700167078525, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 2.9492821249878034 }, - "degraded": { - "seconds": 19.864370208000764, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 3.2756130000343546 } - } + }, + "seconds": 9.401485707960092 }, - "basis": { - "seconds": 9.401485707960092, + "reference": { "cases": { - "pr589": { - "seconds": 3.2756130000343546, - "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b" + "degraded": { + "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299", + "seconds": 19.864370208000764 }, "pr555": { - "seconds": 2.9492821249878034, - "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab" + "report_sha256": "55c93455cfbdc94a292491bb9f13158e20f0e5bd230402ca86f78cf0629ae5ab", + "seconds": 14.376700167078525 }, - "degraded": { - "seconds": 3.175984041998163, - "report_sha256": "c59410f7506f5338ceaccb778e0e5f5b7185a6353c525bad85a756bb83c3b299" + "pr589": { + "report_sha256": "0d3ee000d192749fdc44f868f075fb92fc6aeff873beebf12fd3cf92433d923b", + "seconds": 15.884748458047397 } - } + }, + "seconds": 50.12656000000425 } - } + }, + "order": [ + "reference", + "basis" + ], + "pair": 4 } ], - "median_suite_seconds": { - "reference": 32.6134802919114, - "basis": 5.907537999912165 - }, - "suite_ratio": 5.520655185357471, - "median_case_seconds": { - "pr589": { - "reference": 10.703001499990933, - "basis": 2.030974750057794 - }, - "pr555": { - "reference": 10.765563208027743, - "basis": 1.8459598339395598 - }, - "degraded": { - "reference": 11.144659584038891, - "basis": 2.0303760420065373 - } - }, - "finished_at": "2026-10-14T05:45:21.412584+00:00", - "python": "3.12.12 (main, Oct 9 2025, 11:07:00) [Clang 17.0.0 (clang-1700.6.3.2)]", - "executable": "/opt/homebrew/opt/python@3.12/bin/python3.12", - "platform": "macOS-26.5.2-arm64-arm-64bit", - "implementation_sha256": { - "closure.py": "febc46cb43be709684bb51e48bc2c849b63f02809e2bf5bb461c62d55953c4fd", - "run.py": "4e40c4497143ee2525028c78fcf527e6690761a984eb132e74d30c50081b8698", - "benchmark.py": "d579af460de5d8b076403714c17ba8595d900ad6a5c51d84f5e63ab28723ade4", - "EXPECTED.json": "dac0e71d005bf700444f866209f588fef2a276ea6ce2cf17b6279e7881a5647e", - "SOURCES.json": "b94b723b5585ec673b82da156b50afa28b9122d441616f4a282754fed8b7dea8" - }, - "scope": "Three complete pinned checker cases in fresh interpreters per engine; same sources, closure inventories and receipts; warm OS caches; no timing acceptance threshold or selected-replay claim." + "scope": "Three complete pinned checker cases in fresh interpreters per engine; same sources, closure inventories and receipts; warm OS caches; no timing acceptance threshold or selected-replay claim.", + "status": "PASS_BIT_FRAME_CLOSURE_BENCHMARK", + "suite_ratio": 5.520655185357471 } diff --git a/research/bit-frame-closure-basis/README.md b/research/bit-frame-closure-basis/README.md index e01fa237b7..0548348521 100644 --- a/research/bit-frame-closure-basis/README.md +++ b/research/bit-frame-closure-basis/README.md @@ -131,3 +131,5 @@ Profile one pinned PR933 or PR1345 transport checker to see whether closure is also a material cost there. Its mutable-state and rank contracts must be checked before reuse. This package supplies no speed or correctness claim for those checkers; `TASK.json` records that first step and its blockers. + +After production promotion of `frameopt.close` (`research/bit-frame-closure-production/`), the historical pairwise `frameopt.py` digest remains pinned as **provenance** only. Live CI inputs no longer include that path; the adapter still loads the working-tree checker and replaces `close` for the basis engine. diff --git a/research/bit-frame-closure-basis/SOURCES.json b/research/bit-frame-closure-basis/SOURCES.json index c2b1c694d9..d777f1608b 100644 --- a/research/bit-frame-closure-basis/SOURCES.json +++ b/research/bit-frame-closure-basis/SOURCES.json @@ -16,7 +16,7 @@ }, { "path": "research/bit589-frame-optimum/frameopt.py", - "usage": "input", + "usage": "provenance", "git_blob": "1622844ff90529c47e539f502c92b4f2371524e9", "sha256": "d18d5ed96a6d3146b2141b9bdd29900dd612defdcd5ebc7040542064ec89f237" }, diff --git a/research/bit-frame-closure-basis/VERIFY.json b/research/bit-frame-closure-basis/VERIFY.json index c73f3068f7..ce56bcc90f 100644 --- a/research/bit-frame-closure-basis/VERIFY.json +++ b/research/bit-frame-closure-basis/VERIFY.json @@ -4,7 +4,6 @@ "python": "3.12", "requirements": [], "inputs": [ - "research/bit589-frame-optimum/frameopt.py", "research/bit589-frame-optimum/verify.sh", "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz", diff --git a/research/bit-frame-closure-basis/run.py b/research/bit-frame-closure-basis/run.py index dd69ab9dcf..d6a285b126 100644 --- a/research/bit-frame-closure-basis/run.py +++ b/research/bit-frame-closure-basis/run.py @@ -17,7 +17,7 @@ TUNED = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" BASE_WORD = "research/e8-bit-p111-tuned/data/bitE8mut-p111.json.gz" INPUTS = { - CHECKER, TUNED, BASE_WORD, + TUNED, BASE_WORD, "research/bit589-frame-optimum/verify.sh", "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", }