diff --git a/research/staged544-moved-add-pair/PROOF.md b/research/staged544-moved-add-pair/PROOF.md new file mode 100644 index 0000000000..8e57baa295 --- /dev/null +++ b/research/staged544-moved-add-pair/PROOF.md @@ -0,0 +1,118 @@ +# Commuting moves cannot retarget a staged544 line + +This is a finite obstruction on two pinned words, plus one scalar identity. +It is not a supplier, a kappa bound, or a theorem about every circuit. + +The move contract is `apply_move` from the vendored tracer: one ADD stays in +its section, crosses only gates accepted by `crosses`, and may replace its +common frame. Entrances, warps, and every other gate's frame stay fixed. +`crosses` is the scalar normal form: an ADD crosses another ADD when neither +destination is the other's source, and it crosses a nonzero scale on a +touched register. It does not cross a warp. + +## 1. Witness for every rank-1 ADD + +On each provider, 735 ADD gates have a rank-1 common frame `M`. For each such +gate `g` the checker finds an operand register `r` whose incoming frame is +already `M`, and an event that first put `M` into `r`: + +| Witness | Gates | What creates `M` on `r` | +|---|---:|---| +| Entrance | 653 | `r` starts inside `M` | +| Map | 70 | A warp map, earlier in the same section or in an earlier section | +| Dependence | 12 | An earlier rank-1 ADD that does not commute with `g` | + +These three classes partition the 735 gates. Both providers give the same +counts and the same twelve dependence pairs. The two provider files are not +equal. + +The twelve pairs are adjacent ADDs in section `A`. The later gate reads the +register written by the earlier gate, so `crosses` fails in both directions: + +| Producer | Consumer | Register | +|---:|---:|---:| +| 2027 | 2028 | 240 | +| 2029 | 2030 | 242 | +| 2181 | 2182 | 256 | +| 2183 | 2184 | 258 | +| 2335 | 2336 | 272 | +| 2337 | 2338 | 274 | +| 2489 | 2490 | 288 | +| 2491 | 2492 | 290 | +| 2643 | 2644 | 304 | +| 2645 | 2646 | 306 | +| 3569 | 3570 | 400 | +| 3723 | 3724 | 416 | + +## 2. The witness survives every commuting move + +**Persistence.** `tracing` accepts a word only when every non-map event's +frame contains that register's incoming state. A map may replace the state. +Its frame belongs to a warp, and `apply_move` neither relocates a warp nor +edits frame. Thus, once register `r` contains a subspace `M`, every later +non-map event on `r` still contains `M`, up to the next map. An ADD whose +incoming state contains `M` can be given only a frame that contains `M`. +A gate that commutes past `g` and lands on `r` while `r` already contains `M` +is under the same restriction, so it does not erase `M`. + +**Finite hypotheses.** On both providers, for every rank-1 ADD and its witness +register, every frame from the witness source through that register's incoming +state contains `M`. An entrance or dependence window contains no map. A map +window starts at the witness warp and contains no second map. The checker +tests these facts; it does not enumerate move sequences. + +**Theorem.** After any finite sequence of `apply_move` steps, every originally +rank-1 ADD still has a common frame containing its original line. + +The proof is induction on the original index in the section. The witness +source still supplies `M` before the gate, and no warp on the witness register +can enter the open interval after that source: warps do not move, and +`crosses` rejects passing a warp. + +- **Entrance.** The start frame is immutable and contains `M`. The window has + no map, so every event on the register before the gate is a climb or a + check. Persistence keeps `M`. +- **Map.** The witness warp is immutable, fails `crosses` with the gate, and + sits earlier in the section or in an earlier section. Its map frame contains + `M`. Persistence keeps `M` from that map until the gate. +- **Dependence.** The producer is an earlier rank-1 ADD and neither order + commutes, so the order is invariant. By induction its frame still contains + `M`. The window has no map. Persistence keeps `M` until the consumer. + +In each case the incoming state contains `M`, so every legal frame of the gate +contains `M`. No legal image is a line disjoint from `M`. In particular, no +sequence of commuting moves realizes the crossed-line pattern on these words: +that pattern replaces `M` by a disjoint line on both gates. + +## 3. The crossed-line identity has histogram delta zero + +The pattern left open by PR #3964 is still a real scalar identity. It just +does not occur under this move contract, and it does not improve the bill. +PR #4122 already invoices a richer swap-and-restore identity at delta zero +and explicitly does not search these providers. The calculation below is the +#3964 synthetic control, not a second claim on that invoice. + +On helpers `h = 300` and `s = 301`, with fixed terminal frame `span(e1, e2)`: + +```text +h += 1 * s frame span(e1) +h += 1 * s frame span(e1) +``` + +Replacing both frames by `span(e2)` keeps every opcode, operand, and +coefficient. Each helper climbs `0 → line → line → plane`: two rank-1 children +per helper, four rank-1 children altogether, before and after. The histogram +delta is zero. Either one-edit intermediate is illegal, because `span(e1)` and +`span(e2)` are incomparable. The same rejection is reproduced by the vendored +tracer; its fixed target-register epilogue is identical on both words, so the +full tracer bill is unchanged as well. + +An unchanged histogram is not a kappa gain. The favorable exchange +`H1 - 2 H2 + H3` is a different signed row and is not this delta. + +## 4. What is not claimed + +Noncommuting rewrites are outside `apply_move`. Frames that properly contain +the old line are outside the theorem. Cleanup, native phases, owners, and +all-size transfer are not repriced, because no disjoint-line move exists to +price. The selected conditional kappa stays `0.001672660197076918`. diff --git a/research/staged544-moved-add-pair/README.md b/research/staged544-moved-add-pair/README.md new file mode 100644 index 0000000000..c52b2af037 --- /dev/null +++ b/research/staged544-moved-add-pair/README.md @@ -0,0 +1,87 @@ +# Commuting moved-ADD pairs do not retarget a staged544 line + +**Negative result. No new kappa.** Selected kappa stays `0.001672660197076918`. + +On both pinned PR3734 providers, every rank-1 ADD frame has a witness operand +whose line is created by an entrance, a warp map, or an earlier rank-1 ADD +that does not commute with it. Those witnesses are invariant under +`apply_move`. No finite sequence of commuting ADD moves can put that frame on +a disjoint line. The crossed-line pattern asked for by PR #3964 therefore does +not occur in this contract. + +The same pattern, written as two scalar ADDs, keeps its opcodes and +coefficients. Each of the two helpers contributes two rank-1 climbs before and +after the retarget, so the child-histogram delta is zero. Either single-frame +intermediate is illegal. An unchanged histogram is not a paid-profile gain. + +The argument and the twelve dependence pairs are in [PROOF.md](PROOF.md). + +PR #4122 prices a different scalar identity for the same open question: a +swap of `y += x` with `y += z`, plus restoration, also at histogram delta 0. +That package does not search these providers. The obstruction above is the +provider half it leaves open. The two-ADD identity in section 3 of the proof +is the synthetic control already named by PR #3964, recomputed here only to +show that its bill is zero and that it is not an occurrence. + +## Scope and evidence + +Original card: `scalar-to-moment`, scope **refined**. The card asks for one +scalar simplification and its histogram. This package takes the released +moved-ADD question: a frame edit that does not change the scalar program. +Details, the stop rule, and the bottleneck link are in [TASK.json](TASK.json). + +| Provider | SHA-256 | Rank-1 ADDs | Entrance | Map | Dependence | +|---|---|---:|---:|---:|---:| +| `BORROW-WORD-43base.json.gz` | `5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699` | 735 | 653 | 70 | 12 | +| `BORROW-WORD-43extra.json.gz` | `965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e` | 735 | 653 | 70 | 12 | + +The gzip bytes and `vendor/retiming.py` +(`591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d`) are +unmodified copies of PR #3964 at `8a8bfb8d36cf5c9f7681b9e7f5d7876a4ba0f5a0`, +paths `research/staged544-stationary-pairs/inputs/` and +`vendor/retiming.py`. That commit is not an ancestor of this package's base +`bb4bccbf42844d2801487450727c2f63e10d1d0f`, so [SOURCES.json](SOURCES.json) pins +only the catalogue and selected record. `verify.py` checks the three SHA-256 +values directly. + +## Reproduce + +Python 3.12, standard library, from the repository root: + +```sh +python3.12 -B research/staged544-moved-add-pair/verify.py +python3.12 -B scripts/research_package.py --package research/staged544-moved-add-pair +``` + +Expected marker: + +```text +PASS_MOVED_ADD_PAIR providers=2 rank1=735 entrance=653 map=70 dependence=12 disjoint_line_moves=0 toy_helper_bill=4xrank1 toy_delta=0 no_new_kappa +``` + +The direct command also passes under `-O`. No Lean, Docker, or selected cold +replay was run. + +## Open next questions + +1. Can one explicit noncommuting transposition, with a scalar correction, put + a rank-1 ADD on a disjoint line and strictly lower the histogram for every + real `0> 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-moved-add-pair/verify.py b/research/staged544-moved-add-pair/verify.py new file mode 100644 index 0000000000..3878657957 --- /dev/null +++ b/research/staged544-moved-add-pair/verify.py @@ -0,0 +1,282 @@ +#!/usr/bin/env python3 +"""No commuting moved-ADD pair retargets a staged544 line onto a disjoint line. + +The scalar program of the crossed-line pattern is unchanged and its child +histogram delta is zero. Selected kappa is not changed. +""" +import gzip +import hashlib +import json +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT / "vendor")) +import retiming as R # noqa: E402 + +SHA256 = { + "inputs/BORROW-WORD-43base.json.gz": + "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699", + "inputs/BORROW-WORD-43extra.json.gz": + "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e", + "vendor/retiming.py": + "591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d", +} + + +def need(ok, message): + if not ok: + raise SystemExit(message) + + +def crosses(g, h): + """Independent copy of the scalar commutation normal form.""" + if h[0] == "add": + return g[1] != h[2] and h[1] != g[2] + return h[0] == "scale" and h[2] != 0 + + +def authenticate(): + for name, digest in SHA256.items(): + blob = (ROOT / name).read_bytes() + need(hashlib.sha256(blob).hexdigest() == digest, "sha256 mismatch: " + name) + need(SHA256["inputs/BORROW-WORD-43base.json.gz"] + != SHA256["inputs/BORROW-WORD-43extra.json.gz"], "providers identical") + + +def load(name): + with gzip.open(ROOT / name, "rt", encoding="utf-8") as handle: + return json.load(handle) + + +def witness(word): + """One forcing operand for every rank-1 ADD, or None when the line is free.""" + nodes, where, _bill = R.tracing(word) + rows = [] + for section in ("A", "B", "restore"): + gates = word[section] + for index, gate in enumerate(gates): + if gate[0] != "add" or not gate[-1]: + continue + old = R.span(tuple(gate[-1])) + if R.rank(old) != 1: + continue + found = None + for register in R.touched(gate): + sequence = nodes[register] + position = where[((section, index), register)] + incoming = sequence[position][2] + if R.rank(incoming) == 0 or not R.contained(incoming, old): + continue + intro = None + for cursor in range(position - 1, -1, -1): + if (R.contained(incoming, sequence[cursor][3]) + and not R.contained(incoming, sequence[cursor][2])): + intro = sequence[cursor] + break + if intro is None: + found = {"kind": "entrance", "section": section, "index": index, + "register": register} + break + address = intro[0] + if not (isinstance(address, tuple) and address[0] == section + and gates[address[1]][0] == "add"): + found = {"kind": "map", "section": section, "index": index, + "register": register, "event": intro[1], + "source": address if isinstance(address, tuple) else None} + break + producer = address[1] + forward = crosses(gates[producer], gate) + backward = crosses(gate, gates[producer]) + need(forward == R.crosses(gates[producer], gate) + and backward == R.crosses(gate, gates[producer]), + "commutation normal form diverged") + if forward and backward: + continue + found = {"kind": "dependence", "section": section, + "producer": producer, "index": index, "register": register, + "producer_rank": R.rank(R.span(tuple(gates[producer][-1])))} + break + rows.append(found) + return rows + + +def check_windows(word, rows): + """Finite hypotheses for the persistence argument. + + From the witness source through the consumer, every recorded frame contains + the original line. Entrance and dependence windows contain no map, so no + warp on that register sits in the interval. A map window starts at the + witness warp and contains no later map. + """ + nodes, where, _bill = R.tracing(word) + for row in rows: + section, index, register = row["section"], row["index"], row["register"] + old = R.span(tuple(word[section][index][-1])) + sequence = nodes[register] + position = where[((section, index), register)] + prior = sequence[:position] + intro_at = None + for cursor in range(len(prior) - 1, -1, -1): + outgoing = prior[cursor][3] + incoming = prior[cursor][2] + if R.contained(old, outgoing) and not R.contained(old, incoming): + intro_at = cursor + break + window = prior if intro_at is None else prior[intro_at:] + for event in window: + need(R.contained(old, event[3]), "witness window drops the original line") + maps = [event for event in window if event[1] == "map"] + if row["kind"] == "entrance": + start = window[0][2] if window else sequence[position][2] + need(R.contained(old, start), "entrance start misses the original line") + need(maps == [], "entrance window contains a map") + elif row["kind"] == "dependence": + need(window and window[0][0] == (section, row["producer"]), + "dependence window does not start at the producer") + need(maps == [], "dependence window contains a map") + else: + need(len(maps) == 1 and maps[0][0] == row["source"], + "map window is not exactly the witness warp") + need(window[0][1] == "map", "map window does not start at the warp") + + +def check_provider(name): + word = load(name) + rows = witness(word) + need(all(row is not None for row in rows), name + " has a free rank-1 ADD") + check_windows(word, rows) + counts = {} + for row in rows: + counts[row["kind"]] = counts.get(row["kind"], 0) + 1 + need(counts == {"entrance": 653, "map": 70, "dependence": 12}, + name + " witness counts " + str(counts)) + dependence = [row for row in rows if row["kind"] == "dependence"] + for row in dependence: + gates = word[row["section"]] + consumer = gates[row["index"]] + producer = gates[row["producer"]] + need(row["producer"] < row["index"], "producer is not earlier") + need(row["producer_rank"] == 1, "dependence producer is not rank 1") + need(not crosses(producer, consumer) and not crosses(consumer, producer), + "dependence pair commutes") + need(consumer[2] == producer[1] or producer[2] == consumer[1], + "dependence pair has no read-after-write") + need(row["section"] == "A", "dependence pair is not in section A") + order = {"A": 0, "B": 1, "restore": 2} + maps = [row for row in rows if row["kind"] == "map"] + need({row["event"] for row in maps} == {"map"}, "map witness is not a map event") + for row in maps: + source = row["source"] + need(isinstance(source, tuple) and isinstance(source[0], str) + and source[0].startswith("map-"), "map witness has no gate") + warp_section = source[0].split("-", 1)[1] + warp = word[warp_section][source[1]] + need(warp[0] == "warp", "map witness is not a warp gate") + consumer = word[row["section"]][row["index"]] + need(not crosses(consumer, warp) and not R.crosses(consumer, warp), + "an ADD can cross its map witness") + if warp_section == row["section"]: + need(source[1] < row["index"], "map witness is not earlier in the section") + else: + need(order[warp_section] < order[row["section"]], + "map witness is not in an earlier section") + return counts, [(row["section"], row["producer"], row["index"], row["register"]) + for row in dependence] + + +def local_children(frames): + """Rank climbs on the two helper registers, without the target epilogue.""" + start = {0} + end = {0, 1, 2, 3} + + def span(vectors): + points = {0} + for vector in vectors: + points |= {point ^ vector for point in points} + return points + + def rank(points): + return (len(points).bit_length() - 1) + + bill = [0] * 10 + current = {300: set(start), 301: set(start)} + for frame in frames: + image = span(frame) + for register in (300, 301): + before = current[register] + need(before <= image, "independent intermediate accepted a bad nest") + bill[rank(image) - rank(before)] += 1 + current[register] = image + for register in (300, 301): + before = current[register] + need(before <= end, "terminal frame does not contain the line") + bill[rank(end) - rank(before)] += 1 + bill[0] = 0 + return bill + + +def check_toy(): + old = local_children(([1], [1])) + new = local_children(([2], [2])) + need(old == new == [0, 4] + [0] * 8, "toy helper bill " + str((old, new))) + for frames in (([2], [1]), ([1], [2])): + try: + local_children(frames) + except SystemExit: + continue + raise SystemExit("toy intermediate was legal") + keep = set(range(112, 224)) | {300, 301} + removed = [register for register in range(704) if register not in keep] + + def programmed(frames): + return { + "A": [["add", 300, 301, 1, 1, list(frame)] for frame in frames], + "B": [], "restore": [], "removed": removed, "ports": [1] * 112, + "start_extra": {}, "helper_final": {"300": [1, 2], "301": [1, 2]}, + "target_levels": {}, "centers": [], "center_frames": [], "cut": [], + "prelude_events": 0, "warps": [], "cleanup": [], + } + + original = programmed(([1], [1])) + retargeted = programmed(([2], [2])) + scalar = lambda word: [(gate[0], gate[1], gate[2], gate[3], gate[4]) for gate in word["A"]] + need(scalar(original) == scalar(retargeted), "scalar program changed") + bill_old = R.tracing(original)[2] + bill_new = R.tracing(retargeted)[2] + need(bill_old == bill_new, "tracer bill changed: " + str((bill_old, bill_new))) + for frames in (([2], [1]), ([1], [2])): + try: + R.tracing(programmed(frames)) + except ValueError: + continue + raise SystemExit("tracer accepted a one-edit intermediate") + + +def main(): + authenticate() + reports = {} + pairs = None + for name in ("inputs/BORROW-WORD-43base.json.gz", + "inputs/BORROW-WORD-43extra.json.gz"): + counts, dependence = check_provider(name) + reports[name] = counts + if pairs is None: + pairs = dependence + else: + need(dependence == pairs, "providers disagree on the dependence pairs") + check_toy() + print("PASS_MOVED_ADD_PAIR", + "providers=2", + "rank1=735", + "entrance=653", + "map=70", + "dependence=12", + "disjoint_line_moves=0", + "toy_helper_bill=4xrank1", + "toy_delta=0", + "no_new_kappa") + + +if __name__ == "__main__": + main()