= ), so it is a
+ consistency check of the implementation, not extra evidence.
+ """
+ inverse = [0] * 512
+ for x, y in enumerate(images):
+ inverse[y] = x
+ # G^{-T} z: bit j of the result is .
+ git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H))
+ lift = lambda x, z: (images[x], images[x] ^ git(x ^ z))
+ pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1
+ basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)]
+ lifted = [lift(*b) for b in basis]
+ if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)):
+ return False
+
+ def frame(mask):
+ us = points(mask)
+ perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)]
+ return {(u, u ^ p) for u in us for p in perp}
+ return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E)))
+
+
+# ----------------------------------------------------------------------------
+# Chronological binary-frame bill (BORROW-WORD contract)
+# ----------------------------------------------------------------------------
+def frame_bill(w, lagrangian=False):
+ rep = w['report']
+ need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry')
+ removed = set(w['removed'])
+ need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers')
+ live = [r for r in range(N) if r not in removed]
+ liveset = set(live)
+ B, warps = w['B'], w['warps']
+ for k, (pos, lender, cols, U, E) in enumerate(warps, 1):
+ need(0 <= pos <= len(B), 'warp position', k)
+ need(lender in liveset and not is_target(lender), 'warp lender', k)
+ images = warp_images(cols)
+ su, se = span(U), span(E)
+ need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k)
+ need(image_mask(images, su) == se, 'warp does not map its frame', k)
+ if lagrangian:
+ need(lagrangian_action_ok(images, su, se), 'lifted frame action', k)
+ for name in ('A', 'B', 'restore'):
+ for g in w[name]:
+ if g[0] != 'warp':
+ need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g)
+ if g[0] == 'add' and not is_target(g[1]):
+ need(not is_target(g[2]), 'non-target reads a target', name, g)
+ need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates')
+ need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes')
+ need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target')
+
+ ports = w['ports']
+ start, end = {}, {}
+ for r in live:
+ if r < V:
+ start[r], end[r] = span((ports[r],)), FULL
+ elif r < 2 * V:
+ start[r], end[r] = ZERO, hyperplane(ports[r - V])
+ else:
+ start[r], end[r] = ZERO, FULL
+ for q, U in w['start_extra'].items():
+ need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q)
+ start[int(q)] = span(U)
+ for q, U in w['helper_final'].items():
+ need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q)
+ end[int(q)] = span(U)
+
+ current, bill, chain = dict(start), Counter(), {}
+
+ def climb(r, mask, where):
+ need(current[r] & ~mask == 0, 'frame containment fails', where, r)
+ d = dim(mask) - dim(current[r])
+ if d:
+ bill[d] += 1
+ chain.setdefault(r, []).append((where, d, mask))
+ current[r] = mask
+
+ npre = w['prelude_events']
+ for i, g in enumerate(w['A']):
+ if g[0] == 'warp':
+ need(i < npre and len(g) == 5, 'warp outside the prelude', i)
+ _, r, op, fr, to = g
+ need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i)
+ images = warp_images(warps[abs(op) - 1][2])
+ if op < 0:
+ inverse = [0] * 512
+ for x, y in enumerate(images):
+ inverse[y] = x
+ images = inverse
+ need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i)
+ need(current[r] == span(fr), 'prelude warp entry frame', i, r)
+ current[r] = span(to)
+ chain.setdefault(r, []).append((('A', i), 'warp', span(to)))
+ else:
+ if i < npre:
+ need(is_target(g[1]), 'prelude scalar writes a non-target', i)
+ for r in touched(g):
+ climb(r, span(g[-1]), ('A', i))
+ levels = {V + int(t): span(U) for t, U in w['target_levels'].items()}
+ need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels')
+ for q, U in zip(w['centers'], w['center_frames']):
+ U = span(U)
+ need(current[q] == U, 'centre entry frame', q)
+ served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q}
+ for T in sorted(served, key=lambda m: -dim(m)):
+ need(T & ~U == 0, 'centre descent not nested', q)
+ d = dim(U) - dim(T)
+ if d:
+ bill[d] += 1
+ chain.setdefault(q, []).append((('centre',), d, T))
+ U = T
+ at = {}
+ for k, rec in enumerate(warps, 1):
+ at.setdefault(rec[0], []).append(k)
+ for p in range(len(B) + 1):
+ for k in at.get(p, ()):
+ _, lender, _, U, E = warps[k - 1]
+ need(current[lender] == span(U), 'native warp entry frame', k, lender)
+ current[lender] = span(E)
+ chain.setdefault(lender, []).append((('warp', k), 'warp', span(E)))
+ if p < len(B):
+ for r in touched(B[p]):
+ climb(r, span(B[p][-1]), ('B', p))
+ for i, g in enumerate(w['restore']):
+ for r in touched(g):
+ climb(r, span(g[-1]), ('restore', i))
+ for r in live:
+ climb(r, end[r], ('end',))
+ restored = set(map(int, w['helper_final']))
+ need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low')
+ widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V)
+ return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end
+
+
+def hygiene(w):
+ """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access."""
+ entering = set(map(int, w['start_extra']))
+ restored = set(map(int, w['helper_final']))
+ live = set(range(N)) - set(w['removed'])
+ for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'):
+ for g in w[name]:
+ if g[0] == 'warp':
+ continue
+ q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3])
+ need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g)
+ if g[0] == 'scale':
+ need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g)
+ for g in w['precondition'] + w['compensation']:
+ need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g)
+ for c in w['initial_corrections']:
+ word = c['operator_word']
+ need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V
+ and c['source'] not in entering, 'correction access', c)
+ need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c)
+ q = Q(c['coefficient'])
+ need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c)
+ return True
+
+
+# ----------------------------------------------------------------------------
+# Literal inverse cleanup, derived from the contract
+# ----------------------------------------------------------------------------
+def ordinary_forward(w):
+ """Chronological non-wrapper actions whose inverse forms cleanup."""
+ out = [g for g in w['A'][w['prelude_events']:]]
+ at = {}
+ for k, rec in enumerate(w['warps'], 1):
+ at.setdefault(rec[0], []).append(['warp', rec[1], k])
+ for p in range(len(w['B']) + 1):
+ out += at.get(p, [])
+ if p < len(w['B']):
+ out.append(w['B'][p])
+ return out + list(w['restore'])
+
+
+def derive_cleanup(w):
+ restored = set(map(int, w['helper_final']))
+ buf = lambda r: r + N if r in restored else r
+ full = [256, 128, 64, 32, 16, 8, 4, 2, 1]
+ out = []
+ for g in reversed(ordinary_forward(w)):
+ if g[0] == 'warp':
+ out.append(['warp', buf(g[1]), -g[2], full])
+ elif is_target(g[1]):
+ continue
+ elif g[0] == 'add':
+ out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full])
+ else:
+ need(g[0] == 'scale', 'unknown primitive', g)
+ out.append(['scale', buf(g[1]), g[3], g[2], full])
+ return out
+
+
+def same_cleanup(a, b):
+ norm = lambda c: [(g[:-1], span(g[-1])) for g in c]
+ return len(a) == len(b) and norm(a) == norm(b)
+
+
+# ----------------------------------------------------------------------------
+# Exact free-operator semantics. A value is a dict {(input, word): Fraction};
+# word is a reduced tuple of signed operator ids (leftmost = applied last).
+# ----------------------------------------------------------------------------
+def program(w, cleanup=None):
+ """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup."""
+ items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient']))
+ for c in w['initial_corrections']]
+ items += w['precondition'] + w['compensation'] + w['A'] + w['cut']
+ at = {}
+ for k, rec in enumerate(w['warps'], 1):
+ at.setdefault(rec[0], []).append(['warp', rec[1], k])
+ for p in range(len(w['B']) + 1):
+ items += at.get(p, [])
+ if p < len(w['B']):
+ items.append(w['B'][p])
+ items += w['restore']
+ return items, list(w['cleanup'] if cleanup is None else cleanup)
+
+
+def dual_op(op):
+ return (1 if op > 0 else -1) * (abs(op) + DUAL)
+
+
+def _left(op, word):
+ return word[1:] if word and word[0] == -op else (op,) + word
+
+
+def _right(word, op):
+ return word[:-1] if word and word[-1] == -op else word + (op,)
+
+
+def _axpy(dst, src, q):
+ for key, x in src.items():
+ y = dst.get(key, 0) + q * x
+ if y:
+ dst[key] = y
+ else:
+ dst.pop(key, None)
+
+
+def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None):
+ """Schrodinger pass: every register's value as a combination of initial inputs.
+
+ Live inputs are independent symbols. Private buffers are independent symbols
+ when symbolic_buffers is set (dirty), otherwise zero. The optional snapshot
+ callback sees the rows at the cleanup boundary.
+ """
+ removed = set(w['removed'])
+ live = [r for r in range(N) if r not in removed]
+ restored = sorted(map(int, w['helper_final']))
+ rows = {r: {(r, ()): Q(1)} for r in live}
+ for c in restored:
+ rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {}
+ prefix, tail = program(w, cleanup)
+
+ def apply(g):
+ kind = g[0]
+ if kind == 'add':
+ t, s, q = g[1], g[2], Q(g[3], g[4])
+ need(t != s and q, 'add gate', g)
+ if dual:
+ t, s, q = s, t, -q
+ _axpy(rows[t], rows[s], q)
+ elif kind == 'scale':
+ q = Q(g[2], g[3])
+ need(q != 0, 'zero scale', g)
+ if dual:
+ q = 1 / q
+ rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()}
+ elif kind == 'warp':
+ op = dual_op(g[2]) if dual else g[2]
+ rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()}
+ elif kind == 'corr':
+ _, t, s, word, c = g
+ if dual:
+ src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c
+ else:
+ src, ops, dst = rows[s], list(reversed(word)), t
+ moved = {}
+ for (var, wd), x in src.items():
+ for o in ops:
+ wd = _left(o, wd)
+ moved[var, wd] = x
+ _axpy(rows[dst], moved, c)
+ else:
+ raise AuditFailure('unknown primitive ' + repr(g))
+
+ for g in prefix:
+ apply(g)
+ if snapshot is not None:
+ snapshot(rows)
+ for g in tail:
+ apply(g)
+ return rows
+
+
+def reverse_columns(w, cleanup=None, upto_cleanup=False):
+ """Heisenberg pull-back: process the forward program backwards.
+
+ cols[s] = {(output, word): coefficient}: the final output register 'output'
+ contains coefficient*word*x_s. Words grow on the right. Every live input and
+ every private buffer is an independent symbol.
+ """
+ removed = set(w['removed'])
+ live = [r for r in range(N) if r not in removed]
+ restored = sorted(map(int, w['helper_final']))
+ regs = live + [c + N for c in restored]
+ cols = {r: {(r, ()): Q(1)} for r in regs}
+ prefix, tail = program(w, cleanup)
+ seq = prefix if upto_cleanup else prefix + tail
+ for g in reversed(seq):
+ kind = g[0]
+ if kind == 'add':
+ t, s, q = g[1], g[2], Q(g[3], g[4])
+ need(t != s and q, 'add gate', g)
+ _axpy(cols[s], cols[t], q)
+ elif kind == 'scale':
+ q = Q(g[2], g[3])
+ need(q != 0, 'zero scale', g)
+ cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()}
+ elif kind == 'warp':
+ op = g[2]
+ cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()}
+ elif kind == 'corr':
+ _, t, s, word, c = g
+ moved = {}
+ for (out, wd), x in cols[t].items():
+ for o in word:
+ wd = _right(wd, o)
+ moved[out, wd] = x
+ _axpy(cols[s], moved, c)
+ else:
+ raise AuditFailure('unknown primitive ' + repr(g))
+ return cols
+
+
+def transpose(cols):
+ rows = {}
+ for s, col in cols.items():
+ for (r, word), x in col.items():
+ rows.setdefault(r, {})[s, word] = x
+ return rows
+
+
+def endpoint_defects(w, rows, dual=False):
+ """Compare final rows with the contract on the zero-buffer (live-input) domain.
+
+ Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity).
+ """
+ removed = set(w['removed'])
+ live = [r for r in range(N) if r not in removed]
+ restored = sorted(map(int, w['helper_final']))
+ bad = []
+ for r in live:
+ expect = {(r, ()): Q(1)}
+ if dual and r < V:
+ expect[r + V, ()] = Q(-1)
+ if not dual and is_target(r):
+ expect[r - V, ()] = Q(1)
+ got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N}
+ if got != expect:
+ bad.append(r)
+ dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))]
+ leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N})
+ buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)}
+ for c in restored)
+ return bad, dirty, leaks, buffer_identity
+
+
+def boundary_defects(w, rows):
+ """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated."""
+ restored = set(map(int, w['helper_final']))
+ out = []
+ for t in range(V, 2 * V):
+ if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}:
+ out.append(('target', t))
+ for c in restored:
+ if rows[c] != {(c, ()): Q(1)}:
+ out.append(('restored', c))
+ for r, row in rows.items():
+ if r < N and r not in restored and any(k[0] in restored for k in row):
+ out.append(('restored input read', r))
+ return out
diff --git a/research/staged544-losing-first-d2/vendor/audit_verify.py b/research/staged544-losing-first-d2/vendor/audit_verify.py
new file mode 100644
index 0000000000..7f9fc1df42
--- /dev/null
+++ b/research/staged544-losing-first-d2/vendor/audit_verify.py
@@ -0,0 +1,254 @@
+#!/usr/bin/env python3
+"""Whole-word cross-check of published RETIMED and DELAYED supplier words.
+
+Reuses Sagar Thakrar's exact PR3687 audit_core, unchanged and authenticated
+before execution. This is not a new interpreter. No construction/native checker
+is imported. roger-sato with substantial OpenAI Codex assistance; Apache-2.0.
+"""
+from collections import Counter
+from copy import deepcopy
+import gzip
+import hashlib
+import json
+from pathlib import Path
+import sys
+import types
+
+HERE = Path(__file__).resolve().parent
+STAGED = {1: 2439, 2: 726, 3: 224, 4: 102, 5: 20, 8: 8}
+RETIMED = {1: 2437, 2: 724, 3: 226, 4: 102, 5: 20, 8: 8}
+WIDTHS = {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213}
+MOVES = ((591, 1045, 640, 644, 2, [423, 65, 20, 10]),
+ (641, 1085, 656, 660, -1, [427, 96, 24, 6]))
+SOURCE_COMMITS = {
+ 3605: '3efbb5de06a49ffeea6684482f2d3fe48cdca3fb',
+ 3642: '044d24f12e74f228dd462c07ae2d7f3ea35e2be9',
+ 3653: '607a09ff441c79b215a8127a81f4cc70021d0d9b',
+ 3682: '431e6c6023ef352c41696469de7fb614cd4ded8c',
+ 3687: 'f798838eb8ede4178e94f240e7b7e54b3f80c82d',
+}
+
+
+def need(ok, message):
+ if not ok:
+ raise ValueError(message)
+
+
+def authenticate():
+ rows = json.loads((HERE / 'SOURCES.json').read_text())['snapshots']
+ expected = {(3687, 'vendor/audit_core.py')}
+ for provider in ('base', 'extra'):
+ expected.update((number, f'inputs/{kind}-{provider}.json.gz') for number, kind in
+ ((3605, 'STAGED'), (3642, 'RETIMED'), (3653, 'RETIMED'), (3682, 'DELAYED')))
+ keys = [(row['source_pr'], row['local']) for row in rows]
+ need(len(keys) == len(expected) and set(keys) == expected, 'source mapping inventory differs')
+ for row in rows:
+ need(row['source_commit'] == SOURCE_COMMITS[row['source_pr']], 'source commit differs')
+ raw = (HERE / row['local']).read_bytes()
+ need(len(raw) == row['bytes'], 'source byte length: ' + row['local'])
+ need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: ' + row['local'])
+ blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest()
+ need(blob == row['git_blob'], 'source Git blob: ' + row['local'])
+ core = types.ModuleType('retained_audit_core')
+ path = HERE / 'vendor/audit_core.py'
+ # Execute the authenticated source bytes, without accepting a .pyc cache.
+ exec(compile(path.read_bytes(), str(path), 'exec'), core.__dict__)
+ return core
+
+
+def load(kind, provider):
+ return json.loads(gzip.decompress((HERE / 'inputs' / f'{kind}-{provider}.json.gz').read_bytes()))
+
+
+def events(w):
+ result = []
+ for pos in range(len(w['B']) + 1):
+ result += [('warp', k, deepcopy(rec)) for k, rec in enumerate(w['warps']) if rec[0] == pos]
+ if pos < len(w['B']):
+ result.append(('gate', pos, deepcopy(w['B'][pos])))
+ return result
+
+
+def replace_events(w, seq):
+ result = deepcopy(w)
+ body, warps = [], [None] * len(w['warps'])
+ for kind, label, gate in seq:
+ gate = deepcopy(gate)
+ if kind == 'gate':
+ body.append(gate)
+ else:
+ gate[0] = len(body)
+ warps[label] = gate
+ need(all(rec is not None for rec in warps), 'lost warp in reconstruction')
+ result['B'], result['warps'] = body, warps
+ return result
+
+
+def reconstruct(C, staged, kind):
+ """Literal prose recipes: adjacent shear swap, or move before first producer.
+
+ This repeats the credited local structural arguments as an input control;
+ the new evidence is the full word calculation below.
+ """
+ seq = events(staged)
+ for start, stop, donor, pivot, coefficient, frame in MOVES:
+ source = next(x for x in seq if x[:2] == ('gate', start))
+ need(source[2] == ['add', donor, pivot, coefficient, 1, [429, 30]], 'source release')
+ if kind == 'RETIMED':
+ target = next(x for x in seq if x[:2] == ('gate', start + 1))
+ need(target[2][0] == 'add' and target[2][2] == pivot, 'adjacent same-pivot shear')
+ need(not any(rec[0] == start + 1 for rec in staged['warps']), 'unexpected crossed warp')
+ where = seq.index(target) + 1
+ else:
+ target = next(x for x in seq if x[:2] == ('gate', stop))
+ writes = [i for i, g in enumerate(staged['B']) if i > start and g[1] == pivot]
+ need(writes[0] == stop, 'first producer cut')
+ where = seq.index(target)
+ changed = deepcopy(source[2])
+ changed[-1] = frame
+ seq.insert(where, ('gate', -pivot, changed))
+ seq.remove(source)
+ result = replace_events(staged, seq)
+ result['cleanup'] = C.derive_cleanup(result)
+ result['report']['local_profile'] = {str(k): v for k, v in RETIMED.items()}
+ return result
+
+
+def semantics(C, w):
+ """All live and buffer inputs are symbols, with no zero-buffer assumption."""
+ def endpoint(name, result):
+ bad_live, dirty_buffers, leaks, buffer_identity = result
+ need(not bad_live and not dirty_buffers and not leaks and buffer_identity,
+ name + ' endpoint: ' + repr(result))
+ boundary = {}
+ rows = C.forward_rows(w, symbolic_buffers=True,
+ snapshot=lambda values: boundary.setdefault('defects', C.boundary_defects(w, values)))
+ endpoint('forward', C.endpoint_defects(w, rows))
+ dual_rows = C.forward_rows(w, dual=True, symbolic_buffers=True)
+ endpoint('dual', C.endpoint_defects(w, dual_rows, dual=True))
+ need(not boundary['defects'], 'cleanup boundary: ' + repr(boundary['defects']))
+ pulled = C.transpose(C.reverse_columns(w))
+ need(pulled == {r: row for r, row in rows.items() if row}, 'reverse pull-back differs from forward')
+ pre = C.transpose(C.reverse_columns(w, upto_cleanup=True))
+ pre = {r: pre.get(r, {}) for r in set(pre) | set(range(C.N))}
+ need(not C.boundary_defects(w, pre), 'reverse cleanup-boundary contract')
+ live = C.N - len(w['removed'])
+ buffers = len(w['helper_final'])
+ need((live, buffers, len(rows)) == (632, 91, 723), 'complete symbolic domain')
+ # Endpoint expectations are derived by the retained checker: live x,y,h
+ # map to x,y+x,h; all private buffer symbols return unchanged.
+ return {'live_inputs': live, 'dirty_buffers': buffers, 'matrix_dimension': len(rows),
+ 'forward': 'PASS', 'dual': 'PASS', 'reverse_pullback_equals_forward': True,
+ 'cleanup_boundary_forward_and_reverse': 'PASS',
+ 'buffer_to_live_leaks': 0, 'buffer_self_map': 'identity',
+ 'nonzero_endpoint_terms': sum(len(row) for row in rows.values())}
+
+
+def inspect(C, w, profile):
+ C.hygiene(w)
+ bill, widths, chain, _, _ = C.frame_bill(w)
+ need(bill == profile, 'computed profile differs')
+ need(w['report']['local_profile'] == {str(k): v for k, v in bill.items()}, 'declared profile differs')
+ need(widths == WIDTHS, 'helper widths differ')
+ need(w['cleanup'] == C.derive_cleanup(w), 'literal cleanup differs')
+ return {'semantics': semantics(C, w), 'profile': bill, 'widths': widths,
+ 'rank_mass': sum(r * n for r, n in bill.items())}, chain
+
+
+def expect_rejection(C, fn, phrase):
+ try:
+ fn()
+ except (ValueError, C.AuditFailure) as exc:
+ need(phrase in str(exc), 'wrong rejection: ' + str(exc))
+ return phrase
+ raise ValueError('mutant unexpectedly passed: ' + phrase)
+
+
+def negative_controls(C, staged, w, kind):
+ controls = []
+ for _, _, donor, pivot, _, _ in MOVES:
+ seq = events(w)
+ release = next(x for x in seq if x[0] == 'gate' and x[2][0] == 'add' and x[2][1:3] == [donor, pivot])
+ for defect in ('omit', 'flip', 'cross_first_producer'):
+ changed = deepcopy(seq)
+ index = seq.index(release)
+ if defect == 'omit':
+ changed.pop(index)
+ elif defect == 'flip':
+ changed[index][2][3] *= -1
+ else:
+ producer = next(x for x in changed[index + 1:] if x[0] == 'gate' and x[2][1] == pivot)
+ moved = changed.pop(index)
+ changed.insert(changed.index(producer) + 1, moved)
+ bad = replace_events(w, changed)
+ bad['cleanup'] = C.derive_cleanup(bad)
+ # Repair the literal inverse so stale cleanup is not the rejection.
+ reason = expect_rejection(C, lambda: semantics(C, bad), 'forward endpoint')
+ controls.append({'defect': defect, 'pivot': pivot, 'rejected_by': reason})
+ old_cleanup = deepcopy(w)
+ old_cleanup['cleanup'] = staged['cleanup']
+ # The inverse shears commute: this is a format failure, not a wrong operator.
+ semantic_control = semantics(C, old_cleanup)
+ need(old_cleanup['cleanup'] != C.derive_cleanup(old_cleanup), 'old cleanup unexpectedly literal')
+ controls.append({'defect': 'old_cleanup_order', 'semantics': semantic_control,
+ 'rejected_by': expect_rejection(C, lambda: inspect(C, old_cleanup, RETIMED), 'literal cleanup differs')})
+ old_frames = deepcopy(w)
+ for gate in old_frames['B']:
+ if gate[0] == 'add' and gate[1:3] in ([640, 644], [656, 660]):
+ gate[-1] = [429, 30]
+ need(semantics(C, old_frames) == semantic_control, 'frame-only mutation changed operator')
+ if kind == 'RETIMED':
+ need(C.frame_bill(old_frames)[0] == STAGED, 'old frame control does not restore staged bill')
+ controls.append({'defect': 'old_release_frames', 'semantic_operator': 'PASS',
+ 'profile': STAGED, 'rejected_by': expect_rejection(C, lambda: inspect(C, old_frames, RETIMED), 'computed profile differs')})
+ else:
+ # The later release encounters a donor that has already climbed, so
+ # the original rank-2 frame is now illegal, despite the same operator.
+ controls.append({'defect': 'old_release_frames', 'semantic_operator': 'PASS',
+ 'rejected_by': expect_rejection(C, lambda: inspect(C, old_frames, RETIMED), 'frame containment fails')})
+ fake_report = deepcopy(w)
+ fake_report['report']['local_profile']['1'] += 1
+ controls.append({'defect': 'wrong_declared_profile', 'rejected_by':
+ expect_rejection(C, lambda: inspect(C, fake_report, RETIMED), 'declared profile differs')})
+ return controls
+
+
+def run(C):
+ results = {}
+ for provider in ('base', 'extra'):
+ staged = load('STAGED', provider)
+ control, old_chain = inspect(C, staged, STAGED)
+ records = {'STAGED': control}
+ for kind in ('RETIMED', 'DELAYED'):
+ w = load(kind, provider)
+ need(reconstruct(C, staged, kind) == w, 'prose reconstruction differs: ' + kind)
+ record, chain = inspect(C, w, RETIMED)
+ deltas = {}
+ for register in set(chain) | set(old_chain):
+ before = Counter(d for _, d, _ in old_chain.get(register, []) if type(d) is int and d > 0)
+ after = Counter(d for _, d, _ in chain.get(register, []) if type(d) is int and d > 0)
+ delta = {r: after[r] - before[r] for r in set(after) | set(before) if after[r] != before[r]}
+ if delta:
+ deltas[register] = delta
+ need(deltas == {640: {1: -1, 2: -1, 3: 1}, 656: {1: -1, 2: -1, 3: 1}}, 'per-register invoice differs')
+ record['prose_reconstruction'] = 'exact complete JSON equality'
+ record['changed_register_bills'] = deltas
+ record['controls'] = negative_controls(C, staged, w, kind)
+ records[kind] = record
+ print('CHECKED', provider, kind, '723-register forward/dual/pull-back and 9 controls', flush=True)
+ results[provider] = records
+ return {'status': 'PASS_RETIMED_AND_DELAYED_WHOLE_WORD_AUDIT',
+ 'scope': 'Reused PR3687 interpreter; finite exact operator/frame audit only. No native Gaussian, owner, root, or complete supplier claim.',
+ 'providers': results}
+
+
+if __name__ == '__main__':
+ need(sys.argv[1:] in ([], ['--write']), 'usage: verify.py [--write]')
+ C = authenticate()
+ result = run(C)
+ output = json.dumps(result, sort_keys=True, indent=2) + '\n'
+ if sys.argv[1:] == ['--write']:
+ (HERE / 'RESULT.json').write_text(output)
+ else:
+ need((HERE / 'RESULT.json').read_text() == output, 'committed result differs')
+ print(result['status'])
diff --git a/research/staged544-losing-first-d2/vendor/pr3942_PROOF.md b/research/staged544-losing-first-d2/vendor/pr3942_PROOF.md
new file mode 100644
index 0000000000..9c44765e69
--- /dev/null
+++ b/research/staged544-losing-first-d2/vendor/pr3942_PROOF.md
@@ -0,0 +1,162 @@
+# Local-first two-ADD retiming obstruction
+
+## Statement and fixed contract
+
+Fix either literal PR3734 provider retained in `inputs/`. A first existing ADD
+may change its common binary frame in place, or move across exactly one adjacent
+ADD or nonzero SCALE and change that frame. A second existing ADD may then move
+any distance inside its allowed scalar corridor and choose any common binary
+frame. Both the intermediate and final words must satisfy the fixed boundaries.
+Every other gate, gate frame, entrance, target/centre cut, native warp, and exit
+is unchanged. Each move stays within A after its prelude, B between native warp
+cuts, or restore. ADD crossings use the sufficient condition
+`destination(g) != source(h)` and `destination(h) != source(g)`; SCALE crossings
+use exact conjugation. These are the PR3886 move rules, not every possible
+semantics-preserving rewrite. The same ADD may be chosen twice.
+
+**Theorem.** Every word in this class has new-minus-old raw rank moment at least
+zero for every real `0 < a < 1`. The raw moment is `sum n_r r^(1-a)`. This is a
+finite source-bound theorem conditional on the explicitly stated word/frame
+contract, supported by the exact census below. It is not a universal two-gate
+barrier or supplier admission.
+
+The first move need not be neutral. The census also includes every locally
+losing first move in this radius-one class. The second move has no radius bound.
+A simultaneous edit which needs an illegal intermediate, a longer first move,
+a moved SCALE, extra/deleted gates, warp/phase crossings, or another changed
+boundary is outside the statement.
+
+## 1. Reused scalar and single-move facts
+
+The elementary matrix `I+cE_ds` commutes with `I+bE_uv` under the displayed
+sufficient condition. Moving it right across a scale q at d multiplies c by q;
+a scale at s divides c by q. Moving left reverses these factors. The source
+scales are nonzero powers of two, so coefficients remain dyadic. These are
+identities on arbitrary inputs, including dirty helpers. Cleanup is defined as
+the literal inverse of the edited forward programme, with the inherited buffer
+substitution; it does not require zero dirty state.
+
+The PR3886 trace, move applier, complete single-move census, and sign criterion
+are reused verbatim. The primary replay regenerates all 1,776,295 single-move
+cut/dimension cases separately for each provider and compares the entire frozen
+receipt, rather than trusting its old PASS flag. That census proves every
+single-move delta is nonnegative for all real `0 lo and R.crosses(gate, gates[lower - 1]):
+ lower -= 1
+ while upper < hi and R.crosses(gate, gates[upper]):
+ upper += 1
+ if window is not None:
+ lower, upper = max(lower, window[0]), min(upper, window[1])
+ cuts = [c for c in (i - 1, i, i + 2) if lower <= c <= upper] if first else range(lower, upper + 1)
+ reduced = {r: [x for x in occurrences[r] if x != i] for r in R.touched(gate)}
+ for cut in cuts:
+ if cut == i + 1:
+ continue
+ bounds = []
+ for r in R.touched(gate):
+ indices = reduced[r]
+ j = bisect_left(indices, cut)
+ before = R.span(tuple(gates[indices[j - 1]][-1])) if j else entries[r]
+ after = R.span(tuple(gates[indices[j]][-1])) if j < len(indices) else exits[r]
+ bounds.append((before, after))
+ low = R.join(bounds[0][0], bounds[1][0])
+ high = bounds[0][1] & bounds[1][1]
+ if not R.contained(low, high):
+ continue
+ for dimension in range(R.rank(low), R.rank(high) + 1):
+ delta = removal[i].copy()
+ for before, after in bounds:
+ p, q = R.rank(before), R.rank(after)
+ delta[q - p] -= 1
+ delta[dimension - p] += 1
+ delta[q - dimension] += 1
+ delta[0] = 0
+ require(sum(r * n for r, n in enumerate(delta)) == 0, 'rank mass drift')
+ yield i, cut, dimension, low, high, tuple(delta)
+
+@lru_cache(maxsize=None)
+def frames(low, high, dimension):
+ """All intermediate subspaces, not one representative per dimension."""
+ require(R.contained(low, high), 'empty frame interval')
+ require(R.rank(low) <= dimension <= R.rank(high), 'invalid frame dimension')
+ require(R.rank(high) - R.rank(low) <= 4, 'first-frame resource bound exceeded')
+ current = {low}
+ for _ in range(dimension - R.rank(low)):
+ expanded = set()
+ for frame in current:
+ for v in range(1, 512):
+ if high >> v & 1 and not frame >> v & 1:
+ expanded.add(R.join(frame, R.span((v,))))
+ current = expanded
+ return tuple(sorted(current))
+
+def first_moves(word):
+ fixed, variable, seen = {}, [], set()
+ counts = Counter()
+ interval_checks = set()
+ for section in PHASES:
+ gates = word[section]
+ for i, cut, dimension, low, high, delta in candidates(word, section, range(len(gates)), first=True):
+ interval_checks.add((low, high, dimension))
+ for frame in frames(low, high, dimension):
+ if frame == R.span(tuple(gates[i][-1])):
+ if cut == i:
+ continue
+ pair = (section, min(i, cut))
+ if pair in seen:
+ continue
+ seen.add(pair)
+ require(delta == ZERO, 'fixed-frame swap was not neutral')
+ fixed[pair] = (i, cut, frame)
+ counts['fixed_adjacent'] += 1
+ else:
+ kind = ('frame_only' if cut == i else 'adjacent') + ('_neutral' if delta == ZERO else '_losing')
+ require(R.all_power_nonnegative(delta), 'first move unexpectedly improves')
+ variable.append((section, i, cut, frame, delta, kind))
+ counts[kind] += 1
+ # A separate structural enumeration checks completeness of fixed-frame swaps.
+ direct = set()
+ for section in PHASES:
+ gates = word[section]
+ for lo, hi in R.segments(word, section):
+ for p in range(lo, hi - 1):
+ g, h = gates[p:p + 2]
+ if g[0] != 'add' and h[0] != 'add':
+ continue
+ a, b = (g, h) if g[0] == 'add' else (h, g)
+ if not R.crosses(a, b):
+ continue
+ if set(R.touched(g)) & set(R.touched(h)) and R.span(tuple(g[-1])) != R.span(tuple(h[-1])):
+ continue
+ direct.add((section, p))
+ require(set(fixed) == direct, 'fixed-swap enumerators disagree')
+ return fixed, variable, counts, interval_checks
+
+def bridge_census(word, fixed):
+ """Only the newly opened gap can have a new price after a fixed-frame swap."""
+ histogram, counts = Counter(), Counter()
+ nonzero = []
+ for section in PHASES:
+ gates = word[section]
+ touched = [set(R.touched(g)) for g in gates]
+ for lo, hi, occurrences, entries, exits, removal in geometry(word, section):
+ for p in range(lo, hi - 1):
+ if (section, p) not in fixed:
+ continue
+ counts['first_pairs'] += 1
+ g, h = gates[p:p + 2]
+ selected = sorted({j for r in touched[p] for j in occurrences[r]
+ if gates[j][0] == 'add' and j not in (p, p + 1)
+ and touched[j] & touched[p + 1]})
+ for j in selected:
+ counts['bridge_gates'] += 1
+ crossed = gates[j + 1:p] + [h] if j < p else [g] + gates[p + 2:j]
+ if not all(R.crosses(gates[j], e) for e in crossed):
+ continue
+ counts['scalar_legal'] += 1
+ bounds = []
+ for r in R.touched(gates[j]):
+ indices = occurrences[r]
+ left = bisect_left(indices, p) - 1
+ if left >= 0 and indices[left] == j:
+ left -= 1
+ before = R.span(tuple(gates[indices[left]][-1])) if left >= 0 else entries[r]
+ right = bisect_left(indices, p + 2)
+ if right < len(indices) and indices[right] == j:
+ right += 1
+ after = R.span(tuple(gates[indices[right]][-1])) if right < len(indices) else exits[r]
+ if r in touched[p + 1]:
+ before = R.span(tuple(h[-1]))
+ if r in touched[p]:
+ after = R.span(tuple(g[-1]))
+ bounds.append((before, after))
+ low = R.join(bounds[0][0], bounds[1][0])
+ high = bounds[0][1] & bounds[1][1]
+ if not R.contained(low, high):
+ continue
+ for dimension in range(R.rank(low), R.rank(high) + 1):
+ delta = removal[j].copy()
+ for before, after in bounds:
+ a, b = R.rank(before), R.rank(after)
+ delta[b - a] -= 1
+ delta[dimension - a] += 1
+ delta[b - dimension] += 1
+ delta[0] = 0
+ histogram[tuple(delta)] += 1
+ if any(delta):
+ nonzero.append([section, p, j, dimension, delta])
+ counts['candidate_dimensions'] += 1
+ return {'counts': dict(counts), 'profiles': rows(histogram), 'nonzero_cases': nonzero}
+
+def variable_census(word, variable, auditor=None, progress=False):
+ baseline = R.tracing(word)[2]
+ histogram, by_kind = Counter(), {}
+ for number, (section, i, cut, frame, first_delta, kind) in enumerate(variable):
+ middle = R.apply_move(word, section, i, cut, R.basis(frame))
+ intermediate = R.tracing(middle)[2]
+ require(tuple(intermediate.get(r, 0) - baseline.get(r, 0) if r else 0 for r in range(10)) == first_delta,
+ 'first actual invoice differs from relaxation')
+ if auditor is not None:
+ require(auditor.frame_bill(middle)[0] == intermediate, 'retained first-word invoice disagrees')
+ moved = cut - (cut > i)
+ registers = set(R.touched(word[section][i]))
+ counts = by_kind.setdefault(kind, Counter())
+ counts['first_words'] += 1
+ for second_section in PHASES:
+ selected = [j for j, g in enumerate(middle[second_section])
+ if g[0] == 'add' and registers.intersection(R.touched(g))
+ and (second_section, j) != (section, moved)]
+ for _, _, _, _, _, second_delta in candidates(middle, second_section, selected):
+ delta = tuple(a + b for a, b in zip(first_delta, second_delta))
+ histogram[delta] += 1
+ counts['second_cut_dimensions'] += 1
+ if progress and number % 100 == 0:
+ print('Checked first word', number, 'of', len(variable), flush=True)
+ return {'by_kind': {k: dict(v) for k, v in sorted(by_kind.items())}, 'profiles': rows(histogram)}
+
+def compute(word, auditor=None, progress=False):
+ fixed, variable, counts, intervals = first_moves(word)
+ serial = [[s, p, i, c, list(R.basis(f))] for (s, p), (i, c, f) in sorted(fixed.items())]
+ serial += [[s, i, c, list(R.basis(f)), list(d), k] for s, i, c, f, d, k in variable]
+ return {'first_counts': dict(sorted(counts.items())), 'first_digest': digest(serial),
+ 'max_first_quotient_dimension': max(R.rank(h) - R.rank(l) for l, h, _ in intervals),
+ 'fixed_frame': bridge_census(word, fixed),
+ 'variable_frame': variable_census(word, variable, auditor, progress)}
diff --git a/research/staged544-losing-first-d2/vendor/retiming.py b/research/staged544-losing-first-d2/vendor/retiming.py
new file mode 100644
index 0000000000..c33d7bbcdf
--- /dev/null
+++ b/research/staged544-losing-first-d2/vendor/retiming.py
@@ -0,0 +1,269 @@
+# SPDX-License-Identifier: Apache-2.0
+"""Exact, fixed-neighbour single-ADD retiming relaxation.
+
+Chris R / Clear1nsight, with substantial OpenAI assistance. The BORROW-WORD
+frame contract and scalar-retiming mechanism are credited in README.md.
+This module does not import the retained auditor or a numerical optimiser.
+"""
+from bisect import bisect_left
+from collections import Counter
+from copy import deepcopy
+from fractions import Fraction
+from functools import lru_cache
+
+
+def need(ok, message):
+ if not ok:
+ raise ValueError(message)
+
+
+@lru_cache(maxsize=None)
+def span(vectors):
+ points = {0}
+ for v in vectors:
+ need(type(v) is int and 0 <= v < 512, 'invalid frame vector')
+ points |= {x ^ v for x in tuple(points)}
+ return sum(1 << x for x in points)
+
+
+@lru_cache(maxsize=None)
+def basis(mask):
+ answer = []
+ have = 1
+ for v in range(1, 512):
+ if (mask >> v) & 1 and not (have >> v) & 1:
+ answer.append(v)
+ have = span(tuple(answer))
+ need(have == mask, 'not a binary subspace')
+ return tuple(answer)
+
+
+@lru_cache(maxsize=None)
+def join(a, b):
+ return span(basis(a) + basis(b))
+
+
+@lru_cache(maxsize=None)
+def rank(mask):
+ n = mask.bit_count()
+ need(n > 0 and n & (n - 1) == 0, 'invalid subspace cardinality')
+ return n.bit_length() - 1
+
+
+def contained(a, b):
+ return not a & ~b
+
+
+def touched(gate):
+ return gate[1:3] if gate[0] == 'add' else gate[1:2]
+
+
+def tracing(word):
+ """Own chronological trace; centre descent is NOT persistent state.
+
+ A check node is a fixed boundary, not a charged instruction. The census
+ relaxes it to a virtual climb. Every legal witness has zero such charge.
+ """
+ full = (1 << 512) - 1
+ live = set(range(704)) - set(word['removed'])
+ start, end = {}, {}
+ for r in live:
+ if r < 112:
+ start[r], end[r] = span((word['ports'][r],)), full
+ elif r < 224:
+ p = word['ports'][r - 112]
+ start[r] = 1
+ end[r] = sum(1 << x for x in range(512) if (x & p).bit_count() % 2 == 0)
+ else:
+ start[r], end[r] = 1, full
+ for r, fr in word['start_extra'].items():
+ start[int(r)] = span(tuple(fr))
+ for r, fr in word['helper_final'].items():
+ end[int(r)] = span(tuple(fr))
+ current = dict(start)
+ nodes = {r: [] for r in live}
+ where = {}
+ bill = Counter()
+
+ def event(r, frame, address, kind='climb'):
+ before = current[r]
+ if kind != 'map':
+ need(contained(before, frame), 'source frame containment')
+ d = rank(frame) - rank(before)
+ if kind == 'check':
+ need(d == 0, 'source fixed boundary')
+ elif d:
+ bill[d] += 1
+ if kind == 'climb':
+ where[(address, r)] = len(nodes[r])
+ nodes[r].append((address, kind, before, frame))
+ current[r] = frame
+
+ for i, gate in enumerate(word['A']):
+ if gate[0] == 'warp':
+ event(gate[1], span(tuple(gate[3])), ('check-A', i), 'check')
+ event(gate[1], span(tuple(gate[4])), ('map-A', i), 'map')
+ else:
+ for r in touched(gate):
+ event(r, span(tuple(gate[-1])), ('A', i))
+ levels = {112 + int(r): span(tuple(fr)) for r, fr in word['target_levels'].items()}
+ for r in range(112, 224):
+ event(r, levels.get(r, 1), ('target-cut', r), 'check')
+ for r, fr in zip(word['centers'], word['center_frames']):
+ u = span(tuple(fr))
+ event(r, u, ('centre-cut', r), 'check')
+ served = {levels.get(g[1], 1) for g in word['cut'] if g[2] == r}
+ for v in sorted(served, key=lambda x: -rank(x)):
+ need(contained(v, u), 'centre nesting')
+ if rank(u) > rank(v):
+ bill[rank(u) - rank(v)] += 1
+ u = v
+ # The main forward register remains at its declared centre entry.
+ warps = {}
+ for j, rec in enumerate(word['warps']):
+ warps.setdefault(rec[0], []).append((j, rec))
+ for i in range(len(word['B']) + 1):
+ for j, rec in warps.get(i, []):
+ event(rec[1], span(tuple(rec[3])), ('check-B', j), 'check')
+ event(rec[1], span(tuple(rec[4])), ('map-B', j), 'map')
+ if i < len(word['B']):
+ gate = word['B'][i]
+ for r in touched(gate):
+ event(r, span(tuple(gate[-1])), ('B', i))
+ for i, gate in enumerate(word['restore']):
+ for r in touched(gate):
+ event(r, span(tuple(gate[-1])), ('restore', i))
+ for r in live:
+ event(r, end[r], ('end',))
+ return nodes, where, dict(sorted(bill.items()))
+
+
+def crosses(g, h):
+ """Sufficient exact scalar normal form, not all algebraic commutations."""
+ if h[0] == 'add':
+ return g[1] != h[2] and h[1] != g[2]
+ return h[0] == 'scale' and h[2] != 0
+
+
+def segments(word, section):
+ if section == 'A':
+ cuts = [word['prelude_events'], len(word['A'])]
+ elif section == 'B':
+ cuts = sorted({0, len(word['B'])} | {rec[0] for rec in word['warps']})
+ else:
+ cuts = [0, len(word[section])]
+ return list(zip(cuts, cuts[1:]))
+
+
+def caps(delta):
+ return [sum(n * min(r, k) for r, n in enumerate(delta)) for k in range(1, 10)]
+
+
+def all_power_nonnegative(delta):
+ """Sufficient exact certificate using decreasing positive curvatures."""
+ values = caps(delta)
+ prefix = 0
+ for value in values[:-1]:
+ prefix += value
+ if prefix < 0:
+ return False
+ return values[-1] == 0
+
+
+def census(word):
+ nodes, where, bill = tracing(word)
+ deltas = Counter()
+ counts = {}
+ for section in ('A', 'B', 'restore'):
+ gates = word[section]
+ count = 0
+ for lo, hi in segments(word, section):
+ occurrences = {}
+ for i in range(lo, hi):
+ need(gates[i][0] in ('add', 'scale'), 'unexpected scalar segment')
+ for r in touched(gates[i]):
+ occurrences.setdefault(r, []).append(i)
+ for i in range(lo, hi):
+ g = gates[i]
+ if g[0] != 'add':
+ continue
+ lower = i
+ while lower > lo and crosses(g, gates[lower - 1]):
+ lower -= 1
+ upper = i + 1
+ while upper < hi and crosses(g, gates[upper]):
+ upper += 1
+ removal = [0] * 10
+ reduced, entries, exits = {}, {}, {}
+ for r in touched(g):
+ seq = nodes[r]
+ pos = where[((section, i), r)]
+ _, _, p, u = seq[pos]
+ need(pos + 1 < len(seq) and seq[pos + 1][1] != 'map', 'missing successor')
+ q = seq[pos + 1][3]
+ removal[rank(u) - rank(p)] -= 1
+ removal[rank(q) - rank(u)] -= 1
+ removal[rank(q) - rank(p)] += 1
+ indices = occurrences[r]
+ reduced[r] = [x for x in indices if x != i]
+ entries[r] = seq[where[((section, indices[0]), r)]][2]
+ last = where[((section, indices[-1]), r)]
+ need(seq[last + 1][1] != 'map', 'missing exit check')
+ exits[r] = seq[last + 1][3]
+ for cut in range(lower, upper + 1):
+ if cut == i + 1: # Same placement as cut i, counted once.
+ continue
+ boundaries = []
+ for r in touched(g):
+ indices = reduced[r]
+ j = bisect_left(indices, cut)
+ p = span(tuple(gates[indices[j - 1]][-1])) if j else entries[r]
+ q = span(tuple(gates[indices[j]][-1])) if j < len(indices) else exits[r]
+ boundaries.append((p, q))
+ lower_frame = join(boundaries[0][0], boundaries[1][0])
+ upper_frame = boundaries[0][1] & boundaries[1][1]
+ if not contained(lower_frame, upper_frame):
+ continue
+ dims = [(rank(p), rank(q)) for p, q in boundaries]
+ for d in range(rank(lower_frame), rank(upper_frame) + 1):
+ delta = removal.copy()
+ for p, q in dims:
+ delta[q - p] -= 1
+ delta[d - p] += 1
+ delta[q - d] += 1
+ delta[0] = 0
+ need(sum(r * n for r, n in enumerate(delta)) == 0, 'rank mass drift')
+ deltas[tuple(delta)] += 1
+ count += 1
+ counts[section] = count
+ return {'per_section': counts, 'candidates': sum(counts.values()),
+ 'source_profile': bill,
+ 'deltas': [{'delta': {r: n for r, n in enumerate(d) if n}, 'count': n,
+ 'caps': caps(d), 'certificate': all_power_nonnegative(d)}
+ for d, n in sorted(deltas.items())]}
+
+
+def apply_move(word, section, index, cut, frame):
+ """Apply one exact scalar retiming. Caller must rederive cleanup and audit."""
+ need(section in ('A', 'B', 'restore'), 'unknown section')
+ gates = word[section]
+ need(type(index) is int and 0 <= index < len(gates), 'bad source index')
+ need(type(cut) is int and 0 <= cut <= len(gates), 'bad insertion cut')
+ need(any(lo <= index < hi and lo <= cut <= hi for lo, hi in segments(word, section)),
+ 'crosses prelude or native warp boundary')
+ g = deepcopy(gates[index])
+ need(g[0] == 'add', 'only ADD moves are covered')
+ crossed = gates[index + 1:cut] if cut > index else gates[cut:index]
+ need(all(crosses(g, h) for h in crossed), 'noncommuting scalar barrier')
+ coefficient = Fraction(g[3], g[4])
+ for h in crossed:
+ if h[0] == 'scale' and h[1] in touched(g):
+ power = (1 if h[1] == g[1] else -1) * (1 if cut > index else -1)
+ coefficient *= Fraction(h[2], h[3]) ** power
+ g[3:5] = [coefficient.numerator, coefficient.denominator]
+ g[-1] = list(basis(span(tuple(frame))))
+ result = deepcopy(word)
+ result[section].pop(index)
+ result[section].insert(cut - (cut > index), g)
+ # Segment length and all warp cuts are unchanged. No warp is crossed.
+ return result
diff --git a/research/staged544-losing-first-d2/verify.py b/research/staged544-losing-first-d2/verify.py
new file mode 100644
index 0000000000..09a89c879b
--- /dev/null
+++ b/research/staged544-losing-first-d2/verify.py
@@ -0,0 +1,191 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Read-only exact replay; --emit explicitly regenerates an external receipt."""
+import argparse
+import gzip
+import hashlib
+import json
+from pathlib import Path
+import types
+from collections import Counter
+from copy import deepcopy
+import time
+
+P = Path(__file__).resolve().parent
+
+def require(ok, message):
+ if not ok:
+ raise ValueError(message)
+
+def module(name, path):
+ value = types.ModuleType(name)
+ value.__file__ = str(path)
+ exec(compile(path.read_bytes(), str(path), 'exec'), value.__dict__)
+ return value
+
+def authenticate(raw, row):
+ require(len(raw) == row['bytes'], 'source length: ' + row['local'])
+ require(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: ' + row['local'])
+ blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest()
+ require(blob == row['git_blob'], 'source Git blob: ' + row['local'])
+
+def setup():
+ sources = json.loads((P / 'SOURCES.json').read_text())
+ for row in sources['snapshots']:
+ authenticate((P / row['local']).read_bytes(), row)
+ return (module('owned_search', P / 'search.py'),
+ module('retained_auditor', P / 'vendor/audit_core.py'),
+ module('retained_semantics', P / 'vendor/audit_verify.py'))
+
+def load(tag):
+ return json.loads(gzip.decompress((P / 'inputs' / f'BORROW-WORD-43{tag}.json.gz').read_bytes()))
+
+def calculate(tag, progress=False):
+ S, C, A = setup()
+ word = load(tag)
+ C.hygiene(word)
+ bill, inventory, *_ = C.frame_bill(word)
+ require(bill == {int(r): n for r, n in word['report']['local_profile'].items()}, 'source declared invoice')
+ require(S.R.tracing(word)[2] == bill, 'source trace disagreement')
+ require(C.derive_cleanup(word) == word['cleanup'], 'source inverse cleanup')
+ baseline = S.R.census(word)
+ expected = json.loads((P / 'inputs/SINGLE-CENSUS.json').read_text())[tag]
+ require(json.loads(json.dumps(baseline)) == expected, 'predecessor single-move census differs')
+ require(all(row['certificate'] for row in baseline['deltas']), 'single-move premise failed')
+ result = S.compute(word, C, progress)
+ proof_rows=result['variable_frame']['profiles']
+ if not all(row['certificate'] for row in proof_rows):
+ raise ValueError('unresolved combined signs; no obstruction claimed: '+repr(result['variable_frame']['uncertified_witnesses']))
+ result['dirty_validation']=dirty_validation(S,C,A,word,result['variable_frame']['states'])
+ result['ledger']=ledger(S,C,word,result)
+
+ return {'schema_version': 1, 'provider': tag, 'source_canonical': S.digest(word),
+ 'source_profile': bill, 'width_inventory': inventory,
+ 'single_move_candidates': baseline['candidates'],
+ 'single_census_digest': S.digest(baseline),
+ 'source_semantics': A.semantics(C, word), 'pair_census': result}
+
+def normal(value):return json.loads(json.dumps(value,sort_keys=True))
+
+def ledger(S,C,word,result):
+ bill,widths,_,start,end=C.frame_bill(word)
+ primitives={sec:dict(sorted(Counter(g[0] for g in word[sec]).items())) for sec in
+ ('precondition','compensation','A','cut','B','restore','cleanup')}
+ first=result['variable_frame']['states']
+ masses={sum(int(r)*n for r,n in x['profile'].items()) for x in first}
+ require(masses=={sum(r*n for r,n in bill.items())},'first rank masses')
+ return {'baseline_local_profile':bill,'recursive_children':sum(bill.values()),
+ 'rank_mass':sum(r*n for r,n in bill.items()),'helper_width_inventory':widths,
+ 'helper_roles':sum(widths.values()),'dirty_buffers':len(word['helper_final']),
+ 'live_inputs':C.N-len(word['removed']),'primitive_inventory':primitives,
+ 'native_warps':len(word['warps']),'initial_operator_corrections':len(word['initial_corrections']),
+ 'first_recursive_children_range':[min(sum(x['profile'].values()) for x in first),max(sum(x['profile'].values()) for x in first)],
+ 'all_first_profiles_recorded':'pair_census.variable_frame.states',
+ 'all_combined_histograms_recorded':'pair_census.variable_frame.profiles',
+ 'entrance_frames_sha256':S.digest({str(k):str(v) for k,v in start.items()}),
+ 'exit_frames_sha256':S.digest({str(k):str(v) for k,v in end.items()}),
+ 'added_gates_helpers_buffers':0,'source_scalar_coefficient_bound':coefficient_bound(word),
+ 'first_scalar_coefficient_bound':result['dirty_validation']['coefficient_bound'],
+ 'proved':['Local chronological recursive invoices, fixed native maps/cuts and helper widths',
+ 'Exact rational first-block equality for every admitted first move on arbitrary dirty inputs',
+ 'Complete baseline free-operator replay and deterministic first/final replay controls',
+ 'Recomputed inverse cleanup and full first-word resource inventories in sampled whole-word controls'],
+ 'unknown':['Fresh native Gaussian/Clifford realization and phase','Physical hosting/allocation and complete owner chronology',
+ 'Uniform coefficient/precision/stock/tape costs','All-size compiler, outer/supplier admission','Analytic transfer and BIT H1-H5'],
+ 'unknown_costs_are_zero':False,'new_supplier_or_kappa':False}
+
+def coefficient_bound(word):
+ a=[g for sec in ('A','B','restore') for g in word[sec] if g[0]=='add']
+ return {'maximum_numerator_bits':max(abs(g[3]).bit_length() for g in a),
+ 'maximum_denominator_bits':max(g[4].bit_length() for g in a)}
+
+def dirty_validation(S,C,A,word,states):
+ # Local block equality was checked for every first word during the census.
+ # Whole-word samples additionally exercise the retained production interpreter.
+ samples={0,len(states)-1}
+ for sec in S.PHASES:
+ group=[i for i,x in enumerate(states) if x['first'][0]==sec]
+ if group:
+ samples.update((group[0],group[len(group)//2],group[-1]))
+ rows=[];bound=coefficient_bound(word);second_blocks=[]
+ D=module('dirty_oracle',P/'dirty_blocks.py')
+ for ordinal in sorted(samples):
+ sec,i,cut,fr,delta=states[ordinal]['first']
+ middle=S.R.apply_move(word,sec,i,cut,fr)
+ middle['cleanup']=C.derive_cleanup(middle)
+ bill,widths,*_=C.frame_bill(middle)
+ middle['report']['local_profile']={str(r):n for r,n in bill.items()}
+ C.hygiene(middle)
+ semantic=A.semantics(C,middle)
+ b=coefficient_bound(middle)
+ bound={k:max(bound[k],b[k]) for k in bound}
+ moved=cut-(cut>i)
+ restored=S.R.apply_move(middle,sec,moved,i+(moved=d:break
+ if not mask>>v&1:frame.append(v);mask=S.R.span(tuple(frame))
+ require(len(frame)==d,'second frame realization')
+ final=S.R.apply_move(middle,section,j,target,frame)
+ try:fb,fw,*_=C.frame_bill(final)
+ except C.AuditFailure:continue
+ require(fw==widths,'second helper width drift')
+ actual=tuple(fb.get(r,0)-bill.get(r,0) if r else 0 for r in range(10))
+ require(actual==sd,'second real invoice differs')
+ lo,hi=min(j,target),max(j+1,target)
+ check=D.block_equal(middle[section][lo:hi],final[section][lo:hi])
+ final['cleanup']=C.derive_cleanup(final);final['report']['local_profile']={str(r):n for r,n in fb.items()}
+ C.hygiene(final)
+ second={'section':section,'index':j,'cut':target,'frame':frame,'profile':fb,
+ 'block':check,'semantics':A.semantics(C,final)}
+ break
+ if second:break
+ require(second is not None,'no legal second control')
+ rows.append({'first_state':ordinal,'semantics':semantic,'literal_undo':'PASS','second':second})
+ # Meter all first scalar conjugations without replaying complete words.
+ for state in states:
+ sec,i,cut,fr,_=state['first'];g=word[sec][i]
+ from fractions import Fraction
+ coefficient=Fraction(g[3],g[4])
+ crossed=word[sec][i+1:cut] if cut>i else word[sec][cut:i]
+ for h in crossed:
+ if h[0]=='scale' and h[1] in S.R.touched(g):
+ power=(1 if h[1]==g[1] else -1)*(1 if cut>i else -1)
+ coefficient*=Fraction(h[2],h[3])**power
+ bound['maximum_numerator_bits']=max(bound['maximum_numerator_bits'],abs(coefficient.numerator).bit_length())
+ bound['maximum_denominator_bits']=max(bound['maximum_denominator_bits'],coefficient.denominator.bit_length())
+ return {'all_first_dirty_blocks':len(states),'whole_word_samples':rows,'coefficient_bound':bound,
+ 'proof':'Every first scalar block equals its source on independent rational symbols; unchanged surrounding free operators compose with that equality. Inverse cleanup is rederived; baseline and sampled complete words additionally replay all 723 symbolic inputs.'}
+
+def main():
+ parser = argparse.ArgumentParser(description=__doc__)
+ parser.add_argument('--provider', choices=('base', 'extra'), required=True)
+ parser.add_argument('--emit', type=Path)
+ parser.add_argument('--progress', action='store_true')
+ args = parser.parse_args()
+ result = calculate(args.provider, args.progress)
+ if args.emit:
+ require(not args.emit.resolve().is_relative_to(P), 'write regenerated receipt outside the package')
+ args.emit.write_text(json.dumps(result, sort_keys=True, separators=(',', ':')) + '\n')
+ else:
+ expected = json.loads((P / f'RESULT-{args.provider}.json').read_text())
+ require(json.loads(json.dumps(result)) == expected, 'complete pair receipt differs')
+ print(json.dumps({'status': 'PASS_STAGED544_LOSING_FIRST_D2', 'provider': args.provider,
+ 'first_counts': result['pair_census']['first_counts'],
+ 'result_sha256': hashlib.sha256(json.dumps(result, sort_keys=True, separators=(',', ':')).encode()).hexdigest(),
+ 'new_supplier': False}, sort_keys=True))
+
+if __name__ == '__main__':
+ main()