diff --git a/research/bit589-boundary-adaptive-r659-seed05/EXPECTED.json b/research/bit589-boundary-adaptive-r659-seed05/EXPECTED.json new file mode 100644 index 0000000000..07f7f7c5e8 --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/EXPECTED.json @@ -0,0 +1,282 @@ +{ + "A_slots": [ + 2070, + 2071 + ], + "B_slots": [ + 65, + 819, + 820, + 822, + 823 + ], + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "c": "1733427039589844234749/1000000000000000000000000", + "candidate_assignments": 20, + "examples": { + "better": [], + "illegal": [ + [ + 2070, + 598, + 819, + 598, + "A_upper_boundary" + ], + [ + 2070, + 598, + 820, + 598, + "A_upper_boundary" + ], + [ + 2070, + 598, + 822, + 598, + "A_upper_boundary" + ], + [ + 2070, + 598, + 823, + 598, + "A_upper_boundary" + ], + [ + 2071, + 598, + 819, + 598, + "A_upper_boundary" + ], + [ + 2071, + 598, + 820, + 598, + "A_upper_boundary" + ], + [ + 2071, + 598, + 822, + 598, + "A_upper_boundary" + ], + [ + 2071, + 598, + 823, + 598, + "A_upper_boundary" + ] + ], + "tie": [ + [ + 2070, + 501, + 819, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ], + [ + 2070, + 501, + 820, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ], + [ + 2070, + 501, + 822, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ], + [ + 2070, + 501, + 823, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ], + [ + 2071, + 501, + 819, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ], + [ + 2071, + 501, + 820, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ], + [ + 2071, + 501, + 822, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ], + [ + 2071, + 501, + 823, + 598, + "-3/3906250000000000000000000000", + "3/3906250000000000000000000000" + ] + ], + "unresolved": [], + "worse": [ + [ + 2070, + 501, + 819, + 501, + "30336009189840886151104061/15625000000000000000000000000", + "6067201837968177230220817/3125000000000000000000000000" + ], + [ + 2070, + 501, + 820, + 501, + "30336009189840886151104061/15625000000000000000000000000", + "6067201837968177230220817/3125000000000000000000000000" + ], + [ + 2071, + 501, + 819, + 501, + "30336009189840886151104061/15625000000000000000000000000", + "6067201837968177230220817/3125000000000000000000000000" + ], + [ + 2071, + 501, + 820, + 501, + "30336009189840886151104061/15625000000000000000000000000", + "6067201837968177230220817/3125000000000000000000000000" + ] + ] + }, + "home_control_profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "illegal_A_upper_boundary": 8, + "joint_only_assignments": 0, + "literal_replay": [ + { + "A": [ + 2070, + 501 + ], + "B": [ + 819, + 501 + ], + "profile": { + "1": 1322, + "2": 1343, + "3": 79, + "4": 45, + "5": 101, + "6": 11, + "7": 19 + } + }, + { + "A": [ + 2070, + 501 + ], + "B": [ + 819, + 598 + ], + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + } + }, + { + "A": [ + 2070, + 501 + ], + "B": [ + 820, + 501 + ], + "profile": { + "1": 1322, + "2": 1343, + "3": 79, + "4": 45, + "5": 101, + "6": 11, + "7": 19 + } + } + ], + "literal_replay_count": 12, + "object": "PR589 fixed word; jointly boundary-adaptive A[2071] and B[820] at r=659", + "predecessor_fixed_pair_pr1382_head": "cf17b06c00c50a22315f210c5f6b5197c860abdd", + "predecessor_pr1345_head": "b54a856aa79857d91cd5d65f8f7144e26c8c084f", + "registers_touched": [ + 184, + 290, + 659 + ], + "relaxed_boundary_negative_control": [ + 2070, + 1, + 65, + 0, + "A_upper_boundary" + ], + "relaxed_boundary_negative_control_frames": [ + { + "index": 1, + "mask_hex": "0x7fffffffffffffffffffffffffff", + "rank": 8 + }, + { + "index": 0, + "mask_hex": "0x0", + "rank": 0 + } + ], + "seed": 5, + "static_fixed_boundary_assignments": 12, + "tie": 8, + "track": "bit supplier", + "valid_assignments": 12, + "worse": 4 +} diff --git a/research/bit589-boundary-adaptive-r659-seed05/README.md b/research/bit589-boundary-adaptive-r659-seed05/README.md new file mode 100644 index 0000000000..f954bc8024 --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/README.md @@ -0,0 +1,98 @@ +# PR589 jointly boundary-adaptive pair at register 659 (seed 5) + +**Status: scoped negative-result audit. No new kappa or stronger bound is claimed.** + +## Scope and result + +The assigned OS-random seed was `5` (bit supplier). The three candidates and +selection rule are recorded in [SELECTION.md](SELECTION.md). Seed mapping chose +the third register among the top three ranked by `dim(firstB)-dim(lastA)` and +then register ID descending: shared register `r=659`, with A[2071] +`(frame 501, target 290, source 659)` and B[820] +`(frame 598, target 184, source 659)`. + +This extends the exact fixed-option pair census in PR #1382 by restoring the +reciprocal boundary dependency for these two moves. For every exact commutation +slot region, the enumerator first relaxes the opposite-stage boundary to form a +finite candidate superset, then recomputes B's lower frame from the moved A +schedule, recomputes A's upper frame from the moved B schedule, and checks COPY +retention and the full D/A/B/C frame chain for registers 184, 290 and 659. + +The exact census produced 20 candidate frame assignments. Eight fail the +reciprocal A upper boundary. Twelve are legal: 8 preserve the complete paid +profile and 4 are strictly worse; none improve and none remain unresolved. The +fixed-original-boundary control also yields 12 legal pairs, so the census found +no joint-only pair for this cut. All 12 legal pairs are replayed literally through `wlib.rebuild_C` and +`wlib.paid`; the baseline/home control reproduces the pinned word's paid +profile. Destination slots are gaps before original operation indices; the +literal replayer adjusts the insertion index after a pop for later moves. Exact witnesses and rational interval deltas +are in [EXPECTED.json](EXPECTED.json). + +This is evidence only for one pair of operations in the pinned PR589 word. It +does not establish that boundary-adaptive options are redundant for other cuts, +other words, larger move sets or recursive constructions. The accepted selected +result remains #1094 and the current assembly remains complex-limited; this +result changes neither the selected certificate nor its inherited assumptions. + +## Reproduce + +From repository root, with Python 3.12 and the pinned source files in +[SOURCES.json](SOURCES.json), run the package verifier: + +```sh +python3 research/bit589-boundary-adaptive-r659-seed05/verify.py +``` + +Expected result: + +```text +PASS_BIT589_BOUNDARY_ADAPTIVE_R659 seed=5 candidates=20 valid=12 joint_only=0 +``` + +For registered package metadata and source-pin validation: + +```sh +python3 scripts/research_package.py --package research/bit589-boundary-adaptive-r659-seed05 --check-only +``` + +Expected result: + +```text +PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check) +``` + +The verifier takes about 15 seconds on the recorded environment. It uses only +the standard library and pinned PR589 word, `wlib.py`, and exact base-two moment +engine; `C=1733427039589844234749/10^24`. The atlas checks a deliberately +relaxed candidate rejected by the restored A boundary and confirms the +fixed-boundary domain is contained in the jointly legal set. The finite replay +is not a proof for unenumerated moves or other registers. + +## Open next questions + +The next scoped question is whether the same reciprocal-boundary enumeration +finds joint-only choices for the next seed-ranked high-gap register (r=660 or +r=67). First recheck overlap and derive its exact boundary operations. This +extension is not included here. + +## Provenance and assumptions + +The selected source is the PR589 bit supplier on PR #555, within the accepted +#1094 result. The exact move/price method follows the transport audit in +[PR #1345](https://github.com/CrocSwap/integer-mult-bounds/pull/1345); this +scoped extension follows the open next question recorded by +[PR #1382](https://github.com/CrocSwap/integer-mult-bounds/pull/1382). The +selection, current state and source pins are recorded in [TASK.json](TASK.json) +and [SOURCES.json](SOURCES.json). The selected certificate and task catalogue +are provenance; the listed word, `wlib.py`, and moment engine are live pinned +inputs. + + +## Credit and license + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. The verifier +adapts and credits the exact transport infrastructure developed in PR #1345 +(Qwen3.8-Flash) and extends the fixed-option census contributed in PR #1382 +(OpenAI Codex assisted). PR #589/#555 supply the bit word and its construction; +the selected #1094 result and the word's inherited assumptions remain unchanged. +New package material is Apache-2.0, consistent with repository policy. diff --git a/research/bit589-boundary-adaptive-r659-seed05/SELECTION.md b/research/bit589-boundary-adaptive-r659-seed05/SELECTION.md new file mode 100644 index 0000000000..9d34e9cd02 --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/SELECTION.md @@ -0,0 +1,38 @@ +# Seed 5 task selection + +- OS-random seed: `5` (0–59); bit supplier track. +- Exact base: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. +- Candidate selection: `seed mod 3 = 2` chooses the third narrow task below. +- Within that task, sort shared PR589 registers by `dim(firstB)-dim(lastA)` descending, then register ID descending; `seed mod 3 = 2` chooses the third register from the top three. + +## Three candidates + +1. **Larger/nonabelian register relaxation.** The task card `bit-new-register-model` asks for a target-specific relaxation beyond the three-register abelian alphabet. PR #1333 already supplies an exact paid-cost theorem for binary affine register words; a fresh contribution here would need a materially different explicit alphabet and complete price. +2. **One helper-star interface contract.** The task card `bit-helper-contract` asks for a precise H2/K replacement. PRs #1307 and #1311 and nearby helper-star work already examine hosting and semantic-D bridges; another scalar-count-only case would not close the interface. +3. **Jointly boundary-adaptive A/B transport.** PR #1382's fixed-option census identifies a direct open question: the moved A/B pair can change the boundary that determines each other's feasible frames. The task is to solve this joint feasibility question for one seed-selected high-gap register and its boundary operations. This is selected. + +## Seed-selected object and price + +The shared-register source contains 336 A/B registers. Their largest baseline boundary rank gaps are `(gap 2, register 67)`, `(gap 1, register 660)`, `(gap 1, register 659)`. The seed-selected third object is register 659 (boundary rank gap 1), with last-A op 2071 `(501,290,659)` and first-B op 820 `(598,184,659)`. + +Exact commutation-window slot regions are A: `[2070,2071]` (2 regions), B: `[65,819,820,822,823]` (5 regions). Ignoring only the counterpart boundary gives 8 A frame choices and 16 B frame choices. For each of 8 A choices and 5 B slot regions, the dynamic lower bound can add at most one closure frame to the B catalog set, so the conservative complete search cap is `8*(16+5)=168` frame pairs before full-chain filtering. The actual domain will be counted by the verifier. + +## Overlap and current-state checks + +- The selected certificate remains #1094, κ `836330098538459/500000000000000000`, on the #589 bit supplier. Its inherited assumptions and review remain unchanged; this task does not touch the selected record. +- PR #1382 is open at head `cf17b06c00c50a22315f210c5f6b5197c860abdd`. It exhausts fixed-boundary options and explicitly lists joint boundary-adaptive options as the next question. This task is a one-register extension, not a re-run of its fixed-option census. +- Fresh overlap scan at 2026-10-14 00:04 UTC covered 862 open PRs and 109 discussions. The query `PR589 boundary-adaptive register 659`, `last-A first-B joint frame`, `paired boundary adaptive options` returned zero possible matches; the scanner warns this is not a novelty certificate. +- Latest bit-supplier claim is seed 0 on the independent PR1363 R420 block-4 replay, a different object. No active claim covers register 659's A2071/B820 joint boundary. +- Coordination claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18911738. + + +## Completed result + +The exhaustive two-slot by five-slot joint pass generated 20 assignments after +applying the moved A frame to B's dynamic lower bound. Restoring the reciprocal +A upper bound rejected 8; 12 passed both directions and the complete register +chains on registers 184, 290 and 659. Their paid profiles were 8 ties and 4 +strictly worse outcomes, with no improvement or unresolved interval. The fixed +original-boundary control also has 12 valid assignments, so this cut exposes no +joint-only pair. This is finite evidence for this one pair of operations, not a +general boundary theorem. See EXPECTED.json and `atlas.py` for exact witnesses. diff --git a/research/bit589-boundary-adaptive-r659-seed05/SOURCES.json b/research/bit589-boundary-adaptive-r659-seed05/SOURCES.json new file mode 100644 index 0000000000..21928d3c08 --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", + "usage": "input", + "git_blob": "14a90fa0e788217856f070382c9e61bd7c603c61", + "sha256": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098" + }, + { + "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/tune/wlib.py", + "usage": "input", + "git_blob": "0e5f9a26f68cc415b793aa903cf6d105acbc8f03", + "sha256": "a37fdf3cdf5f62945c2a90193401c0e9edc9dd3cda8d8cb36a3b9c329ebe4dbc" + } + ] +} diff --git a/research/bit589-boundary-adaptive-r659-seed05/TASK.json b/research/bit589-boundary-adaptive-r659-seed05/TASK.json new file mode 100644 index 0000000000..2be52fa7e0 --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 2, + "base_commit": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "For seed 5, exhaustively test jointly boundary-adaptive frame choices for PR589 A operation 2071 and B operation 820 at shared register 659, then price every legal pair.", + "scope_change_reason": "No catalogue card names this transport follow-up. The bit-helper-contract card is retained as the nearest bit-track catalogue anchor only; the actual investigation is the independent PR #1382 open question on reciprocal A/B boundary adaptation.", + "bottleneck_link": "A cheaper A/B transport pair could reduce the bit supplier cost in the selected assembly, but the current accepted result is complex-limited; this is a scoped side result and does not alter the selected kappa.", + "budget_minutes": 24, + "stop_rule": "Stop after exhausting every exact commutation slot region for the two named operations and every stage-local catalog/closure frame candidate; restore both reciprocal stage boundaries, COPY constraints and full touched-register chains for each pair.", + "outcome": "negative-result", + "evidence": "Exact rational census on the pinned PR589 word: 20 dynamically generated assignments, 12 pass both boundaries and complete chains, 8 fail the reciprocal A upper bound; passing profiles are 8 ties and 4 strict losses, with no improvements/unresolved cases. The fixed-boundary control has the same 12 valid pairs; all 12 legal pairs is replayed through wlib.rebuild_C and wlib.paid.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance: seed-based scope selection, adaptation of the PR #1345 transport enumeration, exact census implementation, controls, replay and documentation.", + "open_questions": [ + { + "question": "Does the same reciprocal-boundary enumeration produce joint-only frame pairs on the next seed-ranked high-gap register, r=660 or r=67?", + "why_it_matters": "A positive result would identify whether fixed-boundary option catalogs systematically miss feasible transport combinations beyond this single cut.", + "first_step": "Apply the same two-operation procedure to r=660, first rechecking current PR overlap and deriving its exact last-A/first-B operation indices and slot regions.", + "blocked_by": "This package proves coverage only for r=659; other register pairs may have different operation counts and COPY constraints." + } + ] +} diff --git a/research/bit589-boundary-adaptive-r659-seed05/VERIFY.json b/research/bit589-boundary-adaptive-r659-seed05/VERIFY.json new file mode 100644 index 0000000000..1cfa998507 --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/tune/wlib.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rebuild the exact joint frame census, compare against EXPECTED.json, and exercise baseline literal replay, strict-loss/tie controls, reciprocal-boundary rejection, and fixed-boundary subset check." + } + ] +} diff --git a/research/bit589-boundary-adaptive-r659-seed05/atlas.py b/research/bit589-boundary-adaptive-r659-seed05/atlas.py new file mode 100644 index 0000000000..d065a5633d --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/atlas.py @@ -0,0 +1,446 @@ +"""Exact reciprocal-boundary census for one PR589 A/B move pair (seed 5). + +Enumerate canonical commutation slots and catalogue/closure frames for +A[2071] and B[820] at shared register 659. Recompute both stage boundaries, +preserve COPY frames, check complete touched-register chains, and price with +outward rational bounds from the pinned moment engine. Every legal candidate +is replayed through the literal word builder. No float decides a comparison. + +Move and price methods adapt PR #1345 at b54a856aa79857d91cd5d65f8f7144e26c8c084f; +this narrow extension addresses the joint-boundary question left open by PR #1382. +Substantial OpenAI Codex assistance; Apache-2.0. +""" +import json, sys, importlib.util +from bisect import bisect_left +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +sys.path.insert(0, str(ROOT / 'research/e8-bit-p111-tuned/tune')) +import wlib + +WORD = sys.argv[1] if len(sys.argv) > 1 else \ + str(ROOT / 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz') +C = Q(1733427039589844234749, 10**24) +w = wlib.load(WORD) +V, R = w['v'], w['R'] +N, NL = 2 * V + R, len(w['lines']) +ret = set(w['ret']) +lines = w['lines'] + +masks = [sum(1 << i for i in f) for f in w['frames']] +dim = [len(wlib.basis(lines[i] for i in f)) for f in w['frames']] +idx = {m: i for i, m in enumerate(masks)} +_cl = {} +def closure(mask): + if mask in _cl: + return _cl[mask] + sel = [lines[i] for i in range(NL) if mask >> i & 1] + rk = len(wlib.basis(sel)) + cl = mask + for i in range(NL): + if mask >> i & 1: + continue + if len(wlib.basis(sel + [lines[i]])) == rk: + cl |= 1 << i + if cl not in idx: + idx[cl] = len(masks) + masks.append(cl) + dim.append(rk) + _cl[mask] = idx[cl] + return idx[cl] + +ep = ROOT / 'research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py' +assert sha256(ep.read_bytes()).hexdigest() == 'aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098' +spec = importlib.util.spec_from_file_location('atlas_engine', ep) +engine = importlib.util.module_from_spec(spec) +spec.loader.exec_module(engine) +P = {0: (Q(0), Q(0))} +for d in range(1, 17): + P[d] = tuple(64 * x for x in engine.moment(64, 1, [(d, 1)], C)) + +def chain_cost(seq): + lo = hi = Q(0) + for a, b in zip(seq, seq[1:]): + da, db = dim[a], dim[b] + if db < da or masks[a] & ~masks[b]: + return None + if db > da: + lo += P[db - da][0] + hi += P[db - da][1] + return lo, hi + +def dedup(seq): + out = [] + for f in seq: + if not out or out[-1] != f: + out.append(f) + return out + +SEG = {r: {'D': [], 'A': [], 'B': [], 'C': []} for r in range(N)} +for sec in 'DABC': + for f, t, ss in w[sec]: + for r in [t, *ss]: + s = SEG[r][sec] + if not s or s[-1] != f: + s.append(f) +def full_chain(r, sec=None, ev=None): + segs = [SEG[r]['D']] + if sec == 'A': + segs += [ev, SEG[r]['B'], SEG[r]['C']] + elif sec == 'B': + segs += [SEG[r]['A'], ev, SEG[r]['C']] + else: + segs += [SEG[r]['A'], SEG[r]['B'], SEG[r]['C']] + return [w['start'][r], *dedup(sum(segs, [])), w['final'][r]] +base_cost = {} +for r in range(N): + c = chain_cost(full_chain(r)) + assert c is not None + base_cost[r] = c +tops = Counter() +for q in ret: + fa = w['start'][q] + for sec in 'DA': + for f, t, ss in w[sec]: + if q in (t, *ss): + fa = f + tops[dim[fa]] += 1 +assert dict(tops) == {7: 9}, tops + +def steps(seq): + return Counter(dim[b] - dim[a] for a, b in zip(seq, seq[1:]) if dim[b] > dim[a]) +H0 = Counter() +for r in range(N): + H0.update(steps(full_chain(r))) +H0.update(tops) +assert dict(sorted(H0.items())) == wlib.paid(w) + +def ops_of(sec): + return [(f, t, s) for f, t, ss in w[sec] for s in ss] +A_ops, B_ops = ops_of('A'), ops_of('B') +lastA = list(w['start']) +for f, t, s in A_ops: + lastA[t] = lastA[s] = f +firstB = list(w['final']) +seen = set() +for f, t, s in B_ops: + for r in (t, s): + if r not in seen: + firstB[r] = f + seen.add(r) +CTX = {'A': (list(w['start']), firstB), 'B': (lastA, list(w['final']))} +cp = {} +for r in ret: + lf = w['start'][r] + for f, t, s in A_ops: + if r in (t, s): + lf = f + cp[r] = lf +commute = lambda a, b: a[1] != b[2] and b[1] != a[2] +_feas = {} +def feasible(low, high): + if (low, high) in _feas: + return _feas[(low, high)] + out = [f for f in range(len(masks)) if masks[f] & ~high == 0 and low & ~masks[f] == 0] + F0 = closure(low) + if masks[F0] & ~high == 0 and F0 not in out: + out.append(F0) + _feas[(low, high)] = out + return out + +# Seed-5 scope: jointly move only A[2071] and B[820] on their shared +# boundary register r=659. Slot regions are exact commutation-equivalence +# classes; opposite-stage bounds are relaxed for candidate generation and +# restored jointly below. +AI, BI = 2071, 820 +assert A_ops[AI] == (501, 290, 659), A_ops[AI] +assert B_ops[BI] == (598, 184, 659), B_ops[BI] +FULL = (1 << NL) - 1 + +def slot_regions(sec, i): + ops = A_ops if sec == 'A' else B_ops + tl = [[] for _ in range(N)] + for k, (_, t, s) in enumerate(ops): + tl[t].append(k) + tl[s].append(k) + f0, t, s = ops[i] + lo = i + while lo > 0 and commute((f0, t, s), ops[lo - 1]): + lo -= 1 + hi = i + while hi < len(ops) - 1 and commute((f0, t, s), ops[hi + 1]): + hi += 1 + touches = [k for r in (t, s) for k in tl[r] if k != i] + starts = sorted({lo, i} | {k + 1 for k in touches if lo <= k + 1 <= hi}) + out = [] + for p, st in enumerate(starts): + en = starts[p + 1] - 1 if p + 1 < len(starts) else hi + out.append((min(max(i, st), en), st, en)) + return ops, tl, out + +A_ops2, A_tl2, A_slots = slot_regions('A', AI) +B_ops2, B_tl2, B_slots = slot_regions('B', BI) +assert [q for q, _, _ in A_slots] == [2070, 2071], A_slots +assert [q for q, _, _ in B_slots] == [65, 819, 820, 822, 823], B_slots + +def local_bounds(sec, i, q, tl): + ops = A_ops if sec == 'A' else B_ops + pre, post = CTX[sec] + _, t, s = ops[i] + ctx = [] + for r in (t, s): + lst = [k for k in tl[r] if k != i] + kk = bisect_left(lst, q) + before = ops[lst[kk - 1]][0] if kk else pre[r] + after = ops[lst[kk]][0] if kk < len(lst) else post[r] + ctx.append((r, before, after, kk, lst)) + low = masks[ctx[0][1]] | masks[ctx[1][1]] + high = masks[ctx[0][2]] & masks[ctx[1][2]] + if sec == 'A': + # Only remove the B-stage cap where this moved event is last in A. + for z, (r, _, _, kk, lst) in enumerate(ctx): + if kk == len(lst): + ctx[z] = (r, ctx[z][1], None, kk, lst) + high &= FULL + else: + # Only remove the A-stage floor where this moved event is first in B. + for z, (r, _, _, kk, lst) in enumerate(ctx): + if kk == 0: + ctx[z] = (r, None, ctx[z][2], kk, lst) + low &= FULL + return low, high, ctx + +def section_frames(sec, r, i, q, frame): + ops = A_ops if sec == 'A' else B_ops + tl = A_tl2 if sec == 'A' else B_tl2 + ev = [] + for k in tl[r]: + if k == i: + ev.append((q - 0.5, k, frame)) + else: + ev.append((k, k, ops[k][0])) + ev.sort() + return [x[2] for x in ev] + +def stage_edge(sec, r, moved_i, q, frame, first): + ops = A_ops if sec == 'A' else B_ops + tl = A_tl2 if sec == 'A' else B_tl2 + ev = [] + for k in tl[r]: + ev.append((q - 0.5, k, frame) if k == moved_i else (k, k, ops[k][0])) + if not ev: + return w['start'][r] if sec == 'A' else w['final'][r] + ev.sort() + return ev[0][2] if first else ev[-1][2] + +def local_low_high(sec, i, q): + ops, tl, _ = (A_ops2, A_tl2, A_slots) if sec == 'A' else (B_ops2, B_tl2, B_slots) + _, _, ctx = local_bounds(sec, i, q, tl) + low = 0 + high = FULL + for r, before, after, kk, lst in ctx: + if sec == 'A': + low |= masks[before] + if after is not None: + high &= masks[after] + else: + if before is not None: + low |= masks[before] + if after is not None: + high &= masks[after] + return low, high, ctx + +def candidate_frames(sec, i, q): + low, high, _ = local_low_high(sec, i, q) + return feasible(low, high) + +def chain_for(r, fa, qa, fb, qb): + af = section_frames('A', r, AI, qa, fa) + bf = section_frames('B', r, BI, qb, fb) + segs = [SEG[r]['D'], af, bf, SEG[r]['C']] + return [w['start'][r], *dedup(sum(segs, [])), w['final'][r]] + +def pair_score(qa, fa, qb, fb): + moved_a = {AI: (qa, fa)} + moved_b = {BI: (qb, fb)} + touched = {A_ops[AI][1], A_ops[AI][2], B_ops[BI][1], B_ops[BI][2]} + # COPY outputs retain the selected A access frame. + for r in (A_ops[AI][1], A_ops[AI][2]): + af = section_frames('A', r, AI, qa, fa) + if r in ret and (af[-1] if af else w['start'][r]) != cp[r]: + return None, None, 'copy' + # Check both dynamically updated stage boundaries, including the + # reciprocal B-first/A-last dependency for each operand. + for r in (A_ops[AI][1], A_ops[AI][2]): + _, _, ctx = local_low_high('A', AI, qa) + slot = next(x for x in ctx if x[0] == r) + if slot[2] is None: + bfirst = stage_edge('B', r, BI, qb, fb, True) + if masks[fa] & ~masks[bfirst]: + return None, None, 'A_upper_boundary' + for r in (B_ops[BI][1], B_ops[BI][2]): + _, _, ctx = local_low_high('B', BI, qb) + slot = next(x for x in ctx if x[0] == r) + if slot[1] is None: + alast = stage_edge('A', r, AI, qa, fa, False) + if masks[alast] & ~masks[fb]: + return None, None, 'B_lower_boundary' + low = high = Q(0) + same = True + for r in touched: + now = chain_for(r, fa, qa, fb, qb) + c = chain_cost(now) + if c is None: + return None, None, 'frame_chain' + old = chain_cost(full_chain(r)) + low += c[0] - old[1] + high += c[1] - old[0] + same &= steps(now) == steps(full_chain(r)) + return (low, high), same, None + +def literal_replay(qa, fa, qb, fb): + import copy + w2 = copy.deepcopy(w) + for sec, index, q, frame in (('A', AI, qa, fa), ('B', BI, qb, fb)): + ops = [(f, t, s) for f, t, ss in w2[sec] for s in ss] + op = ops.pop(index) + # q is a gap before original operation q. Removal shifts that gap + # left by one precisely when the destination is later than the source. + ops.insert(q if q <= index else q - 1, (frame, op[1], op[2])) + w2[sec] = [[f, t, [s]] for f, t, s in ops] + while len(w2['frames']) < len(masks): + w2['frames'].append([j for j in range(NL) if masks[len(w2['frames'])] >> j & 1]) + w2['C'] = wlib.rebuild_C(w2) + return dict(sorted(wlib.paid(w2).items())) + +stats = Counter() +examples = {'tie': [], 'worse': [], 'better': [], 'unresolved': [], 'illegal': []} +valid_rows = [] +all_assignments = 0 +for qa, _, _ in A_slots: + a_low, a_high, actx = local_low_high('A', AI, qa) + a_frames = feasible(a_low, a_high) + for qb, _, _ in B_slots: + b_low0, b_high, bctx = local_low_high('B', BI, qb) + # For each candidate A frame, rebuild B's lower bound from the + # actual last-A frames; the closure is recomputed at that exact bound. + for fa in a_frames: + dyn_low = b_low0 + for r, before, _, _, _ in bctx: + if before is None: + dyn_low |= masks[stage_edge('A', r, AI, qa, fa, False)] + for fb in feasible(dyn_low, b_high): + all_assignments += 1 + delta, same, why = pair_score(qa, fa, qb, fb) + if why: + stats['illegal_' + why] += 1 + if len(examples['illegal']) < 8: + examples['illegal'].append([qa, fa, qb, fb, why]) + continue + valid_rows.append((qa, fa, qb, fb, delta, same)) + if same: + label = 'tie' + elif delta[1] < 0: + label = 'better' + elif delta[0] > 0: + label = 'worse' + else: + label = 'unresolved' + stats[label] += 1 + if len(examples[label]) < 8: + examples[label].append([qa, fa, qb, fb, str(delta[0]), str(delta[1])]) + +# The base/base assignment must be legal, profile-identical, and replay exactly. +base_row = next((x for x in valid_rows if x[:4] == (AI, A_ops[AI][0], BI, B_ops[BI][0])), None) +assert base_row is not None and base_row[5] and base_row[4][0] <= 0 <= base_row[4][1] +base_literal = literal_replay(AI, A_ops[AI][0], BI, B_ops[BI][0]) +assert base_literal == dict(sorted(wlib.paid(w).items())) + +# Replay every legal joint assignment, including destinations after the +# original operation index. The latter checks the pop/insert gap adjustment. +replay = [] +for qa, fa, qb, fb, _, _ in valid_rows: + predicted = Counter(tops) + for r in range(N): + predicted.update(steps(chain_for(r, fa, qa, fb, qb))) + observed = literal_replay(qa, fa, qb, fb) + assert observed == dict(sorted(predicted.items())), (qa, fa, qb, fb, observed, predicted) + if len(replay) < 3: + replay.append({'A': [qa, fa], 'B': [qb, fb], 'profile': observed}) + +# Boundary negative control: at least one candidate drawn from the relaxed +# superset must fail when the actual opposing frame is restored. +relaxed_invalid = None +for qa, _, _ in A_slots: + af = candidate_frames('A', AI, qa) + for qb, _, _ in B_slots: + bl, bh, _ = local_low_high('B', BI, qb) + for fa in af: + for fb in feasible(bl, bh): + _, _, why = pair_score(qa, fa, qb, fb) + if why in ('A_upper_boundary', 'B_lower_boundary'): + relaxed_invalid = [qa, fa, qb, fb, why] + break + if relaxed_invalid: + break + if relaxed_invalid: + break + if relaxed_invalid: + break +assert relaxed_invalid is not None + +# Fixed-option negative control: enforce the original external A/B bounds and +# confirm the resulting domain is a subset of the joint dynamic domain. +static_rows = [] +for qa, _, _ in A_slots: + al, ah, actx = local_low_high('A', AI, qa) + for r, before, after, _, _ in actx: + if after is None: + ah &= masks[firstB[r]] + afs = feasible(al, ah) + for qb, _, _ in B_slots: + bl, bh, bctx = local_low_high('B', BI, qb) + for r, before, _, _, _ in bctx: + if before is None: + bl |= masks[lastA[r]] + bfs = feasible(bl, bh) + for fa in afs: + for fb in bfs: + _, _, why = pair_score(qa, fa, qb, fb) + if why is None: + static_rows.append((qa, fa, qb, fb)) +valid_set = {x[:4] for x in valid_rows} +static_set = set(static_rows) +assert static_set <= valid_set, (static_set - valid_set) + +result = { + 'base_commit': 'bce54fb3f895cbe5cd4c0eb477c3afeed100190f', + 'predecessor_pr1345_head': 'b54a856aa79857d91cd5d65f8f7144e26c8c084f', + 'predecessor_fixed_pair_pr1382_head': 'cf17b06c00c50a22315f210c5f6b5197c860abdd', + 'seed': 5, + 'track': 'bit supplier', + 'object': 'PR589 fixed word; jointly boundary-adaptive A[2071] and B[820] at r=659', + 'c': str(C), + 'registers_touched': sorted({A_ops[AI][1], A_ops[AI][2], B_ops[BI][1], B_ops[BI][2]}), + 'A_slots': [q for q, _, _ in A_slots], + 'B_slots': [q for q, _, _ in B_slots], + 'candidate_assignments': all_assignments, + 'valid_assignments': len(valid_rows), + 'static_fixed_boundary_assignments': len(static_rows), + 'joint_only_assignments': len(valid_set - static_set), + **dict(stats), + 'examples': examples, + 'home_control_profile': base_literal, + 'literal_replay': replay, + 'literal_replay_count': len(valid_rows), + 'relaxed_boundary_negative_control': relaxed_invalid, + 'relaxed_boundary_negative_control_frames': [ + {'index': relaxed_invalid[1], 'mask_hex': hex(masks[relaxed_invalid[1]]), 'rank': dim[relaxed_invalid[1]]}, + {'index': relaxed_invalid[3], 'mask_hex': hex(masks[relaxed_invalid[3]]), 'rank': dim[relaxed_invalid[3]]}, + ], +} +if __name__ == '__main__': + print(json.dumps(result, sort_keys=True)) diff --git a/research/bit589-boundary-adaptive-r659-seed05/verify.py b/research/bit589-boundary-adaptive-r659-seed05/verify.py new file mode 100755 index 0000000000..8f6ab7a090 --- /dev/null +++ b/research/bit589-boundary-adaptive-r659-seed05/verify.py @@ -0,0 +1,27 @@ +#!/usr/bin/env python3 +"""Replay the seed-5 r659 joint-boundary census and its controls.""" +import json +from pathlib import Path +import subprocess +import sys + +ROOT = Path(__file__).resolve().parents[2] +PKG = Path(__file__).resolve().parent +run = subprocess.run( + [sys.executable, "-B", str(PKG / "atlas.py")], cwd=ROOT, + text=True, capture_output=True, check=True, +) +actual = json.loads(run.stdout) +expected = json.loads((PKG / "EXPECTED.json").read_text()) +assert actual == expected, "exact census differs from EXPECTED.json" +assert actual["candidate_assignments"] == 20 +assert actual["valid_assignments"] == 12 +assert actual["static_fixed_boundary_assignments"] == 12 +assert actual["joint_only_assignments"] == 0 +assert actual["tie"] == 8 and actual["worse"] == 4 +assert actual.get("better", 0) == 0 and actual.get("unresolved", 0) == 0 +assert actual["illegal_A_upper_boundary"] == 8 +assert actual["relaxed_boundary_negative_control"][-1] == "A_upper_boundary" +assert actual["literal_replay_count"] == 12 +assert len(actual["literal_replay"]) == 3 +print("PASS_BIT589_BOUNDARY_ADAPTIVE_R659 seed=5 candidates=20 valid=12 joint_only=0")