diff --git a/research/staged544-two-add-reduction-review/README.md b/research/staged544-two-add-reduction-review/README.md new file mode 100644 index 0000000000..ac5eb4e1e2 --- /dev/null +++ b/research/staged544-two-add-reduction-review/README.md @@ -0,0 +1,87 @@ +# Independent review of the staged544 new-gap reduction + +**Negative result.** No new κ. The selected conditional κ stays +`0.001672660197076918`. This is an audit of one reduction, not a supplier +and not a universal two-ADD obstruction. + +## Scope and evidence + +PR #3942 certifies that a radius-one first ADD, followed by any legal second +ADD, does not improve the raw rank moment on either pinned PR #3734 provider. +Its released handoff asks for an independent challenge of the +interaction/new-gap reduction and of exhaustive first-frame coverage. +`verify.py` does not import `search.py`. + +On both providers the checker establishes: + +- Every radius-one first-move interval has quotient rank at most 3. A closed + quotient basis spans the upper frame, and a separate one-vector walk finds + exactly the Gaussian number of intermediate subspaces. There are 1292 + intervals: 1078, 186, 3 and 25 of quotient ranks 0, 1, 2 and 3. +- Every fixed-frame adjacent pair that shares a register has equal declared + frames. The 181 unequal shared pairs are nested on the trace: the later + gate's incoming frame is the earlier gate's frame, so they are not + fixed-frame swaps. +- For every scalar-legal third ADD at the swapped interior cut: + - if it meets both swapped gates, its price list equals a separately coded + bridge formula; + - if it meets only the right gate, only the left gate, or neither, that + price equals the original-word price at the cut named in PROOF.md §3 + (after both, before both, or the same cut). +- The bridge rows that are not identically zero are exactly the four published + restore rows `(section=restore, pair=182/191/192/193, third=178, dimension=8)` + with delta `(0, 2, -1, 0, ...)`. Each passes the predecessor nonnegative + curvature certificate, so none is a raw-moment saving. +- Counts tied to the published census: 4709 fixed pairs, 14966 scalar-legal + bridge gates, 14693 bridge dimensions. + +One published nonzero row was recomputed from `apply_move` plus a fresh trace. +Replacing the predicted cut of an only-left gate by the interior cut changes +the price, so the localisation test is not vacuous. Two disjoint ADDs cross +exactly when their endpoint pairs are disjoint; that is the interaction +reduction's crossing hypothesis, checked as algebra on `crosses`, not as the +11.9-million-row variable census. + +The variable-frame second-move census and same-gate collapse are not replayed. +Longer first displacements, illegal intermediate words, and changed native +boundaries stay outside PR #3942 and outside this review. + +## Reproduce + +From the repository root, CPython 3.12: + +```sh +python3.12 -B research/staged544-two-add-reduction-review/verify.py +python3.12 -B scripts/research_package.py --package research/staged544-two-add-reduction-review +``` + +Expected marker: + +```text +PASS_STAGED544_TWO_ADD_GAP_REVIEW +``` + +The two provider words and `vendor/retiming.py` are the bytes of PR #3942 at +`1416f8cd6bfb2f2eb9aa5cc22f0388a85fdbac91`. `verify.py` checks their SHA256 +before use. Recorded local runtime is about 30 seconds. Not run: the +predecessor's 11.9-million-row variable census, Lean, Docker, and the selected +cold replay. + +## Open next questions + +1. **Disjoint second moves.** Prove or price the section-2 claim that a second + ADD on registers missed by the first moved gate has delta equal to its + original single-move delta. The crossing algebra is checked here; the + summed histograms are not. The blocker is the size of that census. +2. **Same-gate collapse.** Show that choosing the moved ADD again undoes every + radius-one first move, not only a sample. A failed undo would be a word the + reduction never prices. + +## Credit + +The reduction, trace, and both provider words are Chris R / Clear1nsight, PR +#3942, with the PR #3886 single-move rules and the PR #3734 providers from +dataisfire. Jeremy Kothe's retiming line, Dugongue's rank-two exchange, and +the frame-contract auditors credited in that package are unchanged. New review +code by unpaidmoon, with substantial assistance from Cursor Grok 4.7. +Apache-2.0. No independent human or formal-kernel review is claimed. diff --git a/research/staged544-two-add-reduction-review/SOURCES.json b/research/staged544-two-add-reduction-review/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/staged544-two-add-reduction-review/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/staged544-two-add-reduction-review/TASK.json b/research/staged544-two-add-reduction-review/TASK.json new file mode 100644 index 0000000000..64057ef3d5 --- /dev/null +++ b/research/staged544-two-add-reduction-review/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "scalar-to-moment", + "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Derive the changed legal frame itinerary and exact child histogram.", + "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract." + ], + "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.", + "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.", + "allowed_variations": [ + "One existing scalar simplification and one proposed frame-path change." + ], + "scope_change_triggers": [ + "Submitting only another scalar count as completion of a paid-profile task." + ], + "overlap_terms": [ + "scalar simplification", + "paid profile", + "R439" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently check the interaction and new-gap reductions for the radius-one fixed-frame two-ADD class on both pinned PR3734 providers, including exhaustive first-frame coverage.", + "scope_change_reason": "The card asks for one scalar simplification's paid histogram. PR #3942 already certifies that this two-ADD class does not improve the raw rank moment, and its released handoff asks for an independent challenge of the reduction rather than another census. This package answers that review. A missed legal interior price would be a scalar move whose histogram was never tested.", + "bottleneck_link": "A two-ADD retiming changes the exponent only if its rank histogram improves. Confirming that every legal fixed-frame interior price is either an old single-move price or one of the four losing bridge rows blocks that scalar route from being recounted as a paid-profile gain.", + "budget_minutes": 60, + "stop_rule": "Stop after both providers' fixed-frame interior prices and radius-one frame intervals are checked. Do not replay the 11917718 variable-frame second-move rows or search a longer first displacement.", + "outcome": "negative-result", + "evidence": "Both providers: 4709 fixed pairs, 14966 scalar-legal bridge gates, 14693 bridge dimensions, max quotient rank 3, and the same four losing restore rows published by PR #3942. No omitted interior price and no bridge-formula mismatch. One-vector subspace counts match the Gaussian binomials on all 1292 intervals.", + "author": "unpaidmoon", + "ai_assistance": "Cursor Grok 4.7 wrote the independent checker and the package text. The predecessor trace oracle and both provider words are unchanged bytes from PR #3942.", + "open_questions": [ + { + "question": "Does every changed-frame first ADD, followed by every legal second ADD on a disjoint register set, have combined raw-moment delta equal to the sum of two original single-move deltas?", + "why_it_matters": "PROOF.md section 2 uses that identity to skip the disjoint pairs. This package checks only the crossing algebra, not the summed histograms.", + "first_step": "Reprice one changed-frame first word against the frozen single-move receipt, restricted to ADDs whose touched sets miss the moved gate.", + "blocked_by": "The variable-frame census is about 11.9 million rows and is outside this review's stop rule." + }, + { + "question": "Does selecting the same ADD twice always collapse to an original single-ADD candidate on every radius-one first move?", + "why_it_matters": "That is the other half of the interaction reduction. A failed undo would be a word the census does not price.", + "first_step": "Apply one radius-one move and its inverse on every changed first frame, and compare the restored gate list.", + "blocked_by": "Needs the variable first-move list. The fixed-frame class checked here does not move a frame, so the same-gate case is a different branch." + } + ] +} diff --git a/research/staged544-two-add-reduction-review/VERIFY.json b/research/staged544-two-add-reduction-review/VERIFY.json new file mode 100644 index 0000000000..8ec8890363 --- /dev/null +++ b/research/staged544-two-add-reduction-review/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Both PR3734 providers: fixed-frame interior localisation, bridge-formula agreement, published nonzero rows, quotient-rank Gaussian counts, nesting of unequal shared pairs, trace oracle, and a wrong-cut sensitivity control." + } + ] +} diff --git a/research/staged544-two-add-reduction-review/inputs/BORROW-WORD-43base.json.gz b/research/staged544-two-add-reduction-review/inputs/BORROW-WORD-43base.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/staged544-two-add-reduction-review/inputs/BORROW-WORD-43base.json.gz differ diff --git a/research/staged544-two-add-reduction-review/inputs/BORROW-WORD-43extra.json.gz b/research/staged544-two-add-reduction-review/inputs/BORROW-WORD-43extra.json.gz new file mode 100644 index 0000000000..b17e2be67e Binary files /dev/null and b/research/staged544-two-add-reduction-review/inputs/BORROW-WORD-43extra.json.gz differ diff --git a/research/staged544-two-add-reduction-review/vendor/retiming.py b/research/staged544-two-add-reduction-review/vendor/retiming.py new file mode 100644 index 0000000000..c33d7bbcdf --- /dev/null +++ b/research/staged544-two-add-reduction-review/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-two-add-reduction-review/verify.py b/research/staged544-two-add-reduction-review/verify.py new file mode 100644 index 0000000000..1a99346a12 --- /dev/null +++ b/research/staged544-two-add-reduction-review/verify.py @@ -0,0 +1,472 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent check of the PR #3942 fixed-frame new-gap reduction. + +This file does not import search.py. vendor/retiming.py is the predecessor +scalar-trace oracle, authenticated by SHA256 before it is loaded. The +interaction and new-gap claims are re-derived from that trace. +""" +from bisect import bisect_left +from collections import Counter, defaultdict +from fractions import Fraction +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +HEAD = "1416f8cd6bfb2f2eb9aa5cc22f0388a85fdbac91" +DIGESTS = { + "inputs/BORROW-WORD-43base.json.gz": + "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699", + "inputs/BORROW-WORD-43extra.json.gz": + "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e", + "vendor/retiming.py": + "591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d", +} +# Published nonzero bridge rows of both RESULT-*.json files at HEAD. +PUBLISHED_NONZERO = ( + ("restore", 182, 178, 8, (0, 2, -1, 0, 0, 0, 0, 0, 0, 0)), + ("restore", 191, 178, 8, (0, 2, -1, 0, 0, 0, 0, 0, 0, 0)), + ("restore", 192, 178, 8, (0, 2, -1, 0, 0, 0, 0, 0, 0, 0)), + ("restore", 193, 178, 8, (0, 2, -1, 0, 0, 0, 0, 0, 0, 0)), +) +PHASES = ("A", "B", "restore") + + +def require(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def gauss(n, k): + if k < 0 or k > n: + return 0 + num = den = 1 + for i in range(k): + num *= (1 << n) - (1 << i) + den *= (1 << k) - (1 << i) + return num // den + + +def load_retiming(): + path = HERE / "vendor/retiming.py" + spec = importlib.util.spec_from_file_location("pinned_retiming", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def load_word(name): + raw = (HERE / name).read_bytes() + require(hashlib.sha256(raw).hexdigest() == DIGESTS[name], "word digest " + name) + return json.loads(gzip.decompress(raw)) + + +def span_bit(mask, v): + """Subspace join of a characteristic mask with the line through v.""" + added = 0 + points = mask + while points: + b = points & -points + points -= b + added |= 1 << ((b.bit_length() - 1) ^ v) + return mask | added + + +def quotient_basis(low, high): + """Closed F2 basis of high/low. Independent of one-vector frame walks.""" + covered = {x for x in range(512) if low >> x & 1} + reps = [] + for v in range(512): + if (high >> v) & 1 and v not in covered: + reps.append(v) + covered.update(v ^ x for x in tuple(covered)) + return reps, covered + + +def one_vector_counts(low, high, rank): + """Fresh one-vector extension. Not the predecessor search.frames walker.""" + current = {low} + counts = {rank(low): 1} + guard = 0 + while True: + expanded = set() + for frame in current: + for v in range(512): + if (high >> v) & 1 and not (frame >> v) & 1: + expanded.add(span_bit(frame, v)) + if not expanded: + break + guard += 1 + require(guard <= 4, "one-vector walk exceeded quotient rank 4") + current = expanded + counts[rank(low) + guard] = len(current) + return counts + + +def analyze(R, word): + report = Counter() + problems = [] + nonzero = [] + trace_case = None + sensitive = None + max_q = 0 + seen_intervals = set() + for section in PHASES: + gates = word[section] + nodes, where, _bill = R.tracing(word) + for lo, hi in R.segments(word, section): + occ = defaultdict(list) + for i in range(lo, hi): + for r in R.touched(gates[i]): + occ[r].append(i) + entries, exits = {}, {} + for r, idxs in occ.items(): + entries[r] = nodes[r][where[((section, idxs[0]), r)]][2] + last = where[((section, idxs[-1]), r)] + require(nodes[r][last + 1][1] != "map", "missing exit") + exits[r] = nodes[r][last + 1][3] + removal = {} + corridor = {} + touched = {} + adds = [] + for i in range(lo, hi): + if gates[i][0] != "add": + continue + regs = tuple(R.touched(gates[i])) + touched[i] = set(regs) + delta = [0] * 10 + for r in regs: + seq = nodes[r] + pos = where[((section, i), r)] + before, frame = seq[pos][2], seq[pos][3] + require(seq[pos + 1][1] != "map", "missing successor") + after = seq[pos + 1][3] + delta[R.rank(frame) - R.rank(before)] -= 1 + delta[R.rank(after) - R.rank(frame)] -= 1 + delta[R.rank(after) - R.rank(before)] += 1 + removal[i] = delta + lower, upper = i, i + 1 + g = gates[i] + while lower > lo and R.crosses(g, gates[lower - 1]): + lower -= 1 + while upper < hi and R.crosses(g, gates[upper]): + upper += 1 + corridor[i] = (lower, upper) + adds.append(i) + cuts = [c for c in (i - 1, i, i + 2) if lower <= c <= upper and c != i + 1] + reduced = {r: tuple(x for x in occ[r] if x != i) for r in regs} + for cut in cuts: + pair = [] + for r in regs: + idxs = reduced[r] + k = bisect_left(idxs, cut) + before = R.span(tuple(gates[idxs[k - 1]][-1])) if k else entries[r] + after = R.span(tuple(gates[idxs[k]][-1])) if k < len(idxs) else exits[r] + pair.append((before, after)) + low = R.join(pair[0][0], pair[1][0]) + high = pair[0][1] & pair[1][1] + if not R.contained(low, high): + continue + q = R.rank(high) - R.rank(low) + max_q = max(max_q, q) + if q > 3: + problems.append(("quotient", section, i, cut, q)) + key = (low, high) + if key not in seen_intervals: + seen_intervals.add(key) + reps, covered = quotient_basis(low, high) + require(len(reps) == q, "quotient basis rank") + require(sum(1 << x for x in covered) == high, "quotient basis misses high") + walked = one_vector_counts(low, high, R.rank) + for kdim in range(q + 1): + require(walked.get(R.rank(low) + kdim, 0) == gauss(q, kdim), + "one-vector coverage") + report["intervals"] += 1 + report["quotient_" + str(q)] += 1 + report["first_dimensions"] += R.rank(high) - R.rank(low) + 1 + + def bounds_at(j, cut, frame_of, index_of): + packed = [] + for r in touched[j]: + idxs = [index_of(x) for x in occ[r] if x != j] + idxs.sort() + k = bisect_left(idxs, cut) + before = R.span(tuple(frame_of(idxs[k - 1]))) if k else entries[r] + after = R.span(tuple(frame_of(idxs[k]))) if k < len(idxs) else exits[r] + packed.append((before, after, R.rank(before), R.rank(after))) + low = R.join(packed[0][0], packed[1][0]) + high = packed[0][1] & packed[1][1] + if not R.contained(low, high): + return None + return packed, R.rank(low), R.rank(high) + + def delta_list(j, packed, lo_rank, hi_rank): + base = removal[j] + out = [] + for dimension in range(lo_rank, hi_rank + 1): + delta = base.copy() + for _before, _after, a, b in packed: + delta[b - a] -= 1 + delta[dimension - a] += 1 + delta[b - dimension] += 1 + delta[0] = 0 + require(sum(r * n for r, n in enumerate(delta)) == 0, "rank mass") + out.append((dimension, tuple(delta))) + return out + + def original_price(j, cut): + packed = bounds_at(j, cut, lambda pos: gates[pos][-1], lambda x: x) + if packed is None: + return None + return delta_list(j, *packed) + + # Disjoint ADDs cross exactly when touched sets are the endpoint pairs. + # Checked on every ADD, not by an n^2 search: crosses(g, h) for two + # ADDs is g[1] != h[2] and h[1] != g[2]. + for i in adds: + gi = gates[i] + require(touched[i] == {gi[1], gi[2]}, "ADD touched set") + report["adds"] += 1 + + for p in range(lo, hi - 1): + g, h = gates[p], gates[p + 1] + if g[0] != "add" and h[0] != "add": + continue + left_ok = g[0] == "add" and R.crosses(g, h) + right_ok = h[0] == "add" and R.crosses(h, g) + if not left_ok and not right_ok: + continue + share = set(R.touched(g)) & set(R.touched(h)) + if share and R.span(tuple(g[-1])) != R.span(tuple(h[-1])): + report["unequal_shared"] += 1 + for r in share: + pos = where[((section, p + 1), r)] + before = nodes[r][pos][2] + if before != R.span(tuple(g[-1])): + problems.append(("nesting", section, p, r)) + continue + report["fixed_pairs"] += 1 + tg, th = set(R.touched(g)), set(R.touched(h)) + + def frame_sw(pos, p=p, g=g, h=h): + if pos == p: + return h[-1] + if pos == p + 1: + return g[-1] + return gates[pos][-1] + + def index_sw(x, p=p): + if x == p: + return p + 1 + if x == p + 1: + return p + return x + + for j in adds: + if j in (p, p + 1): + continue + lower_j, upper_j = corridor[j] + if j > p + 1: + legal = lower_j <= p + 2 and R.crosses(gates[j], g) + else: + legal = upper_j >= p and R.crosses(gates[j], h) + if section == "restore" or report["fixed_pairs"] <= 40: + if j > p + 1: + crossed = (g, *gates[p + 2:j]) + else: + crossed = (*gates[j + 1:p], h) + require(legal == all(R.crosses(gates[j], e) for e in crossed), + "fast corridor disagrees") + report["legality_oracle"] += 1 + if not legal: + continue + report["legal_interior"] += 1 + tj = touched[j] + both = bool(tj & tg) and bool(tj & th) + if not both: + if (tj & th) and not (tj & tg): + pred, label = p + 2, "only_right" + elif (tj & tg) and not (tj & th): + pred, label = p, "only_left" + else: + pred, label = p + 1, "neither" + # Neither gate meets this ADD, so the interior cut + # has the same neighbours before and after the swap. + if any(p in occ[r] or p + 1 in occ[r] for r in tj): + problems.append(("neither_seen", section, p, j)) + report[label] += 1 + continue + lower, upper = corridor[j] + if not lower <= pred <= upper: + problems.append(("pred_illegal", section, p, j, label)) + continue + swapped = bounds_at(j, p + 1, frame_sw, index_sw) + original = bounds_at(j, pred, lambda pos: gates[pos][-1], lambda x: x) + if delta_list(j, *swapped) != delta_list(j, *original) if swapped and original else swapped != original: + problems.append(("localise", section, p, j, label)) + else: + report[label] += 1 + if sensitive is None and label == "only_left" and original is not None: + other = original_price(j, p + 1) + if other != delta_list(j, *original): + sensitive = (section, p, j) + continue + report["bridge"] += 1 + swapped = bounds_at(j, p + 1, frame_sw, index_sw) + packed = [] + for r in tj: + idxs = [x for x in occ[r] if x != j] + left = bisect_left(idxs, p) - 1 + before = R.span(tuple(gates[idxs[left]][-1])) if left >= 0 else entries[r] + right = bisect_left(idxs, p + 2) + after = R.span(tuple(gates[idxs[right]][-1])) if right < len(idxs) else exits[r] + if r in th: + before = R.span(tuple(h[-1])) + if r in tg: + after = R.span(tuple(g[-1])) + packed.append((before, after, R.rank(before), R.rank(after))) + low = R.join(packed[0][0], packed[1][0]) + high = packed[0][1] & packed[1][1] + if not R.contained(low, high): + bridged = None + else: + bridged = (packed, R.rank(low), R.rank(high)) + left_rows = None if swapped is None else delta_list(j, *swapped) + right_rows = None if bridged is None else delta_list(j, *bridged) + if left_rows != right_rows: + problems.append(("bridge", section, p, j)) + continue + report["bridge_dimensions"] += 0 if left_rows is None else len(left_rows) + if left_rows: + for dimension, delta in left_rows: + if any(delta): + nonzero.append((section, p, j, dimension, delta)) + if trace_case is None and left_ok: + trace_case = (section, p, j, dimension, delta, g[-1]) + report["max_quotient"] = max_q + report["nonzero"] = len(nonzero) + return report, problems, nonzero, trace_case, sensitive + + +def trace_oracle(R, word, case): + """One published nonzero row, priced from apply_move plus a fresh trace.""" + section, p, j, dimension, delta, frame = case + require(word[section][p][0] == "add", "trace witness is not an ADD") + middle = R.apply_move(word, section, p, p + 2, frame) + nodes, where, _bill = R.tracing(middle) + gates = middle[section] + lo = hi = None + for a, b in R.segments(middle, section): + if a <= p < b: + lo, hi = a, b + occ = defaultdict(list) + for i in range(lo, hi): + for r in R.touched(gates[i]): + occ[r].append(i) + removal = [0] * 10 + regs = tuple(R.touched(gates[j])) + for r in regs: + seq = nodes[r] + pos = where[((section, j), r)] + before, fr = seq[pos][2], seq[pos][3] + after = seq[pos + 1][3] + removal[R.rank(fr) - R.rank(before)] -= 1 + removal[R.rank(after) - R.rank(fr)] -= 1 + removal[R.rank(after) - R.rank(before)] += 1 + masks = [] + for r in regs: + idxs = [x for x in occ[r] if x != j] + k = bisect_left(idxs, p + 1) + if k: + before = R.span(tuple(gates[idxs[k - 1]][-1])) + else: + before = nodes[r][where[((section, occ[r][0]), r)]][2] + if k < len(idxs): + after = R.span(tuple(gates[idxs[k]][-1])) + else: + last = occ[r][-1] + after = nodes[r][where[((section, last), r)] + 1][3] + masks.append((before, after)) + low = R.join(masks[0][0], masks[1][0]) + high = masks[0][1] & masks[1][1] + require(R.contained(low, high), "trace witness interval empty") + require(R.rank(low) <= dimension <= R.rank(high), "trace witness dimension") + row = removal + for before, after in masks: + a, b = R.rank(before), R.rank(after) + row[b - a] -= 1 + row[dimension - a] += 1 + row[b - dimension] += 1 + row[0] = 0 + require(tuple(row) == delta, "trace oracle delta " + repr(tuple(row))) + + +def synthetic_controls(R): + """Known lattice and a crossing identity that does not use the big words.""" + zero = 1 + cube = R.span((1, 2, 4)) + require([one_vector_counts(zero, cube, R.rank)[d] for d in range(4)] == [1, 7, 7, 1], + "F2^3 frame lattice") + line = R.span((1,)) + reps, covered = quotient_basis(line, cube) + require(len(reps) == 2 and sum(1 << x for x in covered) == cube, "quotient basis") + require([gauss(2, k) for k in range(3)] == [1, 3, 1], "gauss F2^2") + # Two disjoint ADDs cross; two ADDs sharing a destination/source do not. + def add(d, s): + return ["add", d, s, 1, 1, [1]] + require(R.crosses(add(1, 2), add(3, 4)) and R.crosses(add(3, 4), add(1, 2)), + "disjoint cross") + require(not R.crosses(add(1, 2), add(2, 3)), "shared register blocks") + # Every disjoint ADD pair crosses, because touched sets are the two endpoints. + for d1, s1, d2, s2 in ((1, 2, 3, 4), (7, 7, 8, 9), (0, 5, 5, 0)): + left, right = add(d1, s1), add(d2, s2) + disjoint = {d1, s1}.isdisjoint({d2, s2}) + require(disjoint == (R.crosses(left, right) and R.crosses(right, left)), + "disjoint crossing algebra") + # A rightward scale crossing multiplies the coefficient. + word_gate = ["add", 0, 1, 3, 2, [1]] + scale = ["scale", 0, 2, 1, [1]] + coefficient = Fraction(word_gate[3], word_gate[4]) * Fraction(scale[2], scale[3]) + require(coefficient == Fraction(3, 1), "scale factor") + + +def main(): + for name, digest in DIGESTS.items(): + raw = (HERE / name).read_bytes() + require(hashlib.sha256(raw).hexdigest() == digest, name) + R = load_retiming() + synthetic_controls(R) + summaries = {} + for tag, name in (("base", "inputs/BORROW-WORD-43base.json.gz"), + ("extra", "inputs/BORROW-WORD-43extra.json.gz")): + word = load_word(name) + report, problems, nonzero, trace_case, sensitive = analyze(R, word) + require(not problems, tag + " " + repr(problems[:6])) + require(report["fixed_pairs"] == 4709, tag + " fixed pair count") + require(report["bridge"] == 14966, tag + " bridge count") + require(report["bridge_dimensions"] == 14693, tag + " bridge dimensions") + require(report["max_quotient"] == 3, tag + " quotient") + require(report["unequal_shared"] == 181, tag + " unequal shared") + got = tuple(nonzero) + require(got == PUBLISHED_NONZERO, tag + " nonzero rows " + repr(got)) + for _section, _p, _j, _dimension, delta in got: + require(R.all_power_nonnegative(delta), tag + " bridge row improves") + require(sensitive is not None, tag + " localisation control was vacuous") + require(trace_case is not None, tag + " no trace witness") + trace_oracle(R, word, trace_case) + # Dropping the touch-both overwrite must move the published nonzero row. + require(trace_case[4] != (0,) * 10, "witness delta is zero") + summaries[tag] = {k: report[k] for k in ( + "fixed_pairs", "bridge", "bridge_dimensions", "legal_interior", + "only_left", "only_right", "neither", "unequal_shared", + "intervals", "max_quotient", "nonzero", "quotient_0", + "quotient_1", "quotient_2", "quotient_3", "adds", + "legality_oracle")} + print("PASS_STAGED544_TWO_ADD_GAP_REVIEW", json.dumps(summaries, sort_keys=True)) + + +if __name__ == "__main__": + main()