From a845871b139b92e6a08b7b5ab9700c7f46188790 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 23 Oct 2026 13:36:31 +0000 Subject: [PATCH] Price the closed six-tape head moves of L546 -= L561. Once both registers occupy the kernel's six lengths, the coordinatewise subtraction costs 8NW-12 moves and meets the line-tour lower bound. No new kappa. Co-authored-by: unpaidmoon --- research/qq16-l546-head-move/PROOF.md | 78 ++++++ research/qq16-l546-head-move/README.md | 141 +++++++++++ research/qq16-l546-head-move/SOURCES.json | 24 ++ research/qq16-l546-head-move/TASK.json | 96 ++++++++ research/qq16-l546-head-move/VERIFY.json | 20 ++ research/qq16-l546-head-move/verify.py | 279 ++++++++++++++++++++++ 6 files changed, 638 insertions(+) create mode 100644 research/qq16-l546-head-move/PROOF.md create mode 100644 research/qq16-l546-head-move/README.md create mode 100644 research/qq16-l546-head-move/SOURCES.json create mode 100644 research/qq16-l546-head-move/TASK.json create mode 100644 research/qq16-l546-head-move/VERIFY.json create mode 100644 research/qq16-l546-head-move/verify.py diff --git a/research/qq16-l546-head-move/PROOF.md b/research/qq16-l546-head-move/PROOF.md new file mode 100644 index 0000000000..99bba014ce --- /dev/null +++ b/research/qq16-l546-head-move/PROOF.md @@ -0,0 +1,78 @@ +# Closed head-move bill for one six-tape subtraction + +The tape rules are the pinned `Tape` object in +`research/qq16-gaussian-axis-tapes/tapes.py`: a head reads or writes only the +cell it occupies, a move changes that head by exactly one cell, and the cell +one past the owned interval may be occupied but not read or written. Finite +control may hold a borrow in `{0,1}`. No second head, random access, or free +relocation is available. + +## Placement + +Let \(N=2^n\) with \(n\ge 1\) and let \(W\ge 1\). Write \(L=NW\). The six +lengths are the kernel's lengths \((L,L,L/2,L/2,L/2,L/2)\). + +| Tape | Contents | Cells | +| --- | --- | ---: | +| data0 | real part of L546, coordinates \(0..N-1\), little-endian | \(L\) | +| data1 | imaginary part of L546 | \(L\) | +| scratch0 | real part of L561, coordinates \(0..N/2-1\) | \(L/2\) | +| scratch1 | imaginary part of L561, coordinates \(0..N/2-1\) | \(L/2\) | +| scratch2 | real part of L561, coordinates \(N/2..N-1\) | \(L/2\) | +| scratch3 | imaginary part of L561, coordinates \(N/2..N-1\) | \(L/2\) | + +Every cell is a payload bit. The two complex registers occupy \(4L\) cells and +the six tapes have exactly \(4L\) cells, so this is a capacity-tight packing +of those lengths. Heads start at the origin of each interval, which is cell 0. + +## Program + +On each coordinate, subtract the \(W\)-bit two's-complement integer on the +source tape from the integer on the destination tape. The borrow resets at +every coordinate boundary, so it does not cross from scratch0 to scratch2. +Process the first \(N/2\) coordinates, step each data head one cell onto the +second half, process the remaining coordinates, then walk every head back to +its origin. Source cells are read and not written. + +The forward scan of a tape of length \(L_t\) makes \(L_t-1\) moves and finishes +on the last cell. The return makes another \(L_t-1\) moves. Data tapes are one +interval of length \(L\), so the single step between the halves is one of those +\(L-1\) forward moves, not an extra crossing. The move total is + +\[ +\sum_t 2(L_t-1) = 2\bigl(2(L-1)+4(L/2-1)\bigr) = 8L-12 = 8NW-12. +\] + +Each of the \(4L\) payload cells is read once, and each of the \(2L\) +destination cells is written once. So READ \(=4NW\), WRITE \(=2NW\), and the +cell-action total is \(14NW-12\). + +## Matching lower bound + +Work in the model above, with heads required to start and end at cell 0. + +Changing any one payload bit changes the coordinatewise difference in +\((\mathbb{Z}/2^W\mathbb{Z})^2\). A cell that is never read cannot affect a +later write, so every payload cell is read. The output bit string is not a +function of the minuend alone, so every destination cell must be written: +otherwise that cell would keep a bit that is not always the difference bit. +Therefore every cell of every tape is visited. + +On one tape the farthest cell is \(L_t-1\). A unit-step walk from 0 to \(L_t-1\) +and back to 0 has length at least \(2(L_t-1)\), and that shortest walk already +visits every earlier cell. Summing over the six lengths gives at least +\(8NW-12\) moves. The program meets the bound, so the closed-return move count +is sharp for this placement. + +The same counting gives READ at least \(4NW\) and WRITE at least \(2NW\). Both +are achieved. Stepping one past the last cell, as the axis kernel does, would +add two moves per tape and is not required here. + +## What is not charged + +Copying L561 onto the scratch windows, returning those bits to a native home, +zeroing scratch for a later kernel, the preceding axis factor (MOVE \(=20NW\) +in the pinned kernel), frame climbs, and the four scalar-work steps of the +same-frame coefficient count are outside this bill. \(W\) is the component +width of the placement. This note does not claim that event 9895 uses a +particular \(W\), including the \(W=5\) kernel fixture. diff --git a/research/qq16-l546-head-move/README.md b/research/qq16-l546-head-move/README.md new file mode 100644 index 0000000000..0244954ed1 --- /dev/null +++ b/research/qq16-l546-head-move/README.md @@ -0,0 +1,141 @@ +# Sharp six-tape head moves for `L546 -= L561` + +**Scoped tariff. No new κ.** The selected conditional exponent stays +`60403/20000000`. Same-frame legality of this ADD does not make its tape-head +bill zero. + +## Result + +After both complex registers already occupy the six tapes of the pinned axis +kernel, the coordinatewise subtraction `L546 -= L561` has the closed-return +cell-action bill + +| | count | +| --- | ---: | +| READ | \(4NW\) | +| WRITE | \(2NW\) | +| MOVE | \(8NW-12\) | + +Here \(N=2^n\) with \(n\ge 1\), \(W\ge 1\) is the signed component width, and +every head starts and ends at its interval origin. The move count equals +\(\sum 2(L_t-1)\) over the six kernel lengths +\((NW, NW, NW/2, NW/2, NW/2, NW/2)\), so it is sharp for that placement. +L561's cells are unchanged. The argument is in [PROOF.md](PROOF.md). + +data0 and data1 hold L546. The four half-length scratch tapes hold L561, split +after coordinate \(N/2\). Those six lengths have exactly the \(4NW\) cells the +two registers need. Borrow stays in finite control and resets on each +coordinate. The schedule never steps one past the last cell. + +For the kernel fixture size \(N=512\), \(W=5\), the formula gives +MOVE \(=20468\), READ \(=10240\), WRITE \(=5120\). That width is the kernel +fixture's width, not a measured width of native event 9895. + +## Scope + +Task card `joint-query-controller`, priority revision 7, base +`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. Scope status is **refined**. + +This is item 2 of the eligible list below. It answers open question 1 of +`research/qq16-adjacent-add-bill` and the layout half of discussion comment +19030049 that remains after `research/qq16-f0-first-caller` bound event 9894. +It does not repeat #4162's four scalar-work steps, and it does not price the +matched park/restore comparison left by #4166. + +Ordered eligible list for session r24. Dropped first: work this account +already delivered, results closed on current main, questions covered by an +open pull request, and topics already on a fork `cursor/*` branch. Open +handoffs from the 19 October index come first, with a closed smallest task +removed and a still-open remainder kept when it is distinct. Priority-table +rows whose stated next decision is still open come next. Catalogue cards that +are not already one of those rows follow. + +1. A caller that accepts `(w, q, v_N)` without restoring the original source + slots and without repaying the saving (discussion comment 19030045). The + q-field cleanup in `research/p104-residual-consumer` and the 192-transport + return in `research/p104-role-exchange-caller-audit` leave that caller open. + Distinct from the encoded-exit standard-Y consumer and from `(N-P)⊗M`. +2. This package. +3. Four-provider ordinary/outer rebind (`supplier-boundary-audit`; open + question 1 of `research/staged544-mixed-fourth-entry`). The idle-cost block + is recorded; the four-id rebind is not. +4. Matched park/restore bill for the #4166 caller (`joint-query-controller` + as stated in the priority table; open question of + `research/qq16-caller-install`). Open #4167 and #4172 do not price it. +5. R437 fixed-tape preparation and parking bill (open question 1 of + `research/r437-carrier-integration`). The reverse coefficient is already + covered. +6. `#4091` model equivalence on the later 1090-call fill + (`independent-moment`). +7. The PR2809 encoded-stack visited-space bound left by + `research/bit-stock-recurrence-audit`. The algebraic BIT.md induction is + closed there. CRT join, row-field movement, the half-gap budget and the + uniform evaluator are already on fork `cursor/*` branches or in the listed + unpaidmoon PRs. + +Excluded before this cut: the fresh T385 wrapper (comment 19030047), closed +by `research/t385-r437-copy-audit`; the retiming handoff (comment 19030053), +already covered by #4122, #4128 and later shear work; `p104-side-correction` +as its own row, because the slot, chart, encoding, fiber and standard-Y +pieces are already certified; `formal-interface-lemma`, because #4321 audited +the compact-switch contract and a fork branch holds the sharp-window density. + +## Not charged + +- Moving L561 from its native home onto these scratch windows. +- Copying it back, or clearing scratch for a later kernel. +- The preceding axis kernel (MOVE \(=20NW\) on its own contract) and the + frame climb of event 9894. +- A native component width for event 9895. The formula keeps \(W\). +- Park/restore, F17 consumption, and any change to κ. + +Unknown placement cost is not zero. This is a conditional tariff for one +stated packing, not a physical embedding extracted from the native word. + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3 scripts/research_package.py --package research/qq16-l546-head-move --check-only +python3.12 -B scripts/research_package.py --package research/qq16-l546-head-move +``` + +Directly: + +```sh +python3 -B research/qq16-l546-head-move/verify.py +``` + +Expected: + +```text +PASS_QQ16_L546_HEAD_MOVE move=8*N*W-12 read=4*N*W write=2*N*W bound=sum_2(L_t-1) sharp=yes placement=data_full_scratch_halves heads=origin L561=preserved no_new_kappa +``` + +The verifier loads the pinned tape object, checks the bill on every +\(N=2^1..2^7\) and \(W=1..5\), checks signed fixtures including \(N=512\), +\(W=5\), rejects a non-unit move, and flips every payload cell of one +\(N=2\), \(W=2\) instance. + +## Open next questions + +1. What does it cost to place L561 onto the four scratch windows before this + subtraction? The move bill above starts only after that placement. The + first step is to name the intervals that actually hold L561 at event 9895. + PR #3932 leaves those intervals unbound. +2. If the next kernel needs zero scratch, L561 must be copied out before that + clear. The first step is to bind the next tape-using event after 9895 to + these six windows. No such binding is in the forward word's frame bill. + +## Credit + +The six-tape rules and the axis-kernel lengths are Clear1nsight's +`research/qq16-gaussian-axis-tapes` (PR #3884). The first-caller cut at event +9894 is PR #3932. The same-frame scalar price of event 9895 is unpaidmoon's +#4162 (`research/qq16-adjacent-add-bill`), whose open question 1 is the +question answered here. Ali Romman's QQ16 lineage and Nick Petalas's numerical +formats are the retained background; they are not re-proved. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human or formal-kernel review. diff --git a/research/qq16-l546-head-move/SOURCES.json b/research/qq16-l546-head-move/SOURCES.json new file mode 100644 index 0000000000..5aa7c406aa --- /dev/null +++ b/research/qq16-l546-head-move/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/qq16-gaussian-axis-tapes/tapes.py", + "usage": "input", + "git_blob": "661aafb229dbc280bc667fdc0f22b438b85c634b", + "sha256": "a3ad668b94d44ff1b9d7093e95c5af3ea0d80cdb798365ea7631c0e2a3dcae10" + } + ] +} diff --git a/research/qq16-l546-head-move/TASK.json b/research/qq16-l546-head-move/TASK.json new file mode 100644 index 0000000000..cc1a1370d4 --- /dev/null +++ b/research/qq16-l546-head-move/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Once L546 and L561 occupy the six kernel tapes, what is the exact closed-return head-move bill of the coordinatewise subtraction L546 -= L561?", + "scope_change_reason": "The card asks for a matched whole-caller bill or a cheaper demand. Open question 1 of research/qq16-adjacent-add-bill, continuing discussion comment 19030049, asks only for the head moves of this one ADD after the registers are already on the six-tape windows. The same-frame scalar price is already #4162. This package answers that head-move question and stops. It does not compare park/restore protocols or change the demanded observations.", + "bottleneck_link": "The first rank-positive F0 climb is already followed by a legal same-frame ADD. A zero frame delta does not make the physical layout bill zero. The sharp six-tape move count is the missing local charge for that pair; it is not a supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop when the closed-return subtraction matches the line-tour lower bound on the kernel's six lengths. Do not price copying L561 onto those windows, the preceding axis kernel, later cleanup, or the matched parent park/restore bill.", + "outcome": "partial", + "evidence": "verify.py prints PASS_QQ16_L546_HEAD_MOVE with MOVE=8NW-12, READ=4NW, WRITE=2NW. The count meets sum 2(L_t-1) over the six kernel lengths, and random signed fixtures reproduce coordinatewise two's-complement subtraction while restoring every head and leaving L561 unchanged.", + "author": "unpaidmoon", + "ai_assistance": "Cursor Grok 4.7 wrote the scan, the lower-bound note and this card. The tape object is the pinned predecessor module. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "What is the head-move cost of placing L561 onto the four half-length scratch windows from its native home, with heads returned, before this subtraction starts?", + "why_it_matters": "The bill above assumes that placement is already paid. If the copy is longer than the subtraction, it dominates this pair.", + "first_step": "Name the source intervals and origins that actually hold L561 at event 9895, then scan-copy each component into scratch0/scratch2 or scratch1/scratch3 and return those heads.", + "blocked_by": "PR #3932 and research/qq16-f0-first-caller leave L546 and L561 physical intervals unbound." + }, + { + "question": "Does the next kernel on these same six tapes require the scratch windows to be zero, and what extra closed scan does that clear cost?", + "why_it_matters": "This subtraction leaves L561's bits in scratch. A later axis kernel in research/qq16-gaussian-axis-tapes demands scratch it may destroy, but a live L561 cannot be wiped without a copy-out.", + "first_step": "Find the next tape-using event after 9895 that needs these four scratch windows and decide whether L561 still occupies them.", + "blocked_by": "No native event after 9895 is bound to these six physical tapes." + } + ] +} diff --git a/research/qq16-l546-head-move/VERIFY.json b/research/qq16-l546-head-move/VERIFY.json new file mode 100644 index 0000000000..6eef0bf1d8 --- /dev/null +++ b/research/qq16-l546-head-move/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/qq16-gaussian-axis-tapes/tapes.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Closed-return coordinatewise subtraction on the six kernel tape lengths: MOVE=8NW-12 equals the line-tour lower bound, READ=4NW, WRITE=2NW, heads and L561 cells restored, signed fixtures match, and every payload cell on a small instance is necessary." + } + ] +} diff --git a/research/qq16-l546-head-move/verify.py b/research/qq16-l546-head-move/verify.py new file mode 100644 index 0000000000..ac62bf33b3 --- /dev/null +++ b/research/qq16-l546-head-move/verify.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +"""Sharp closed-return head-move bill for L546 -= L561 on six kernel tapes. + +The tape object is research/qq16-gaussian-axis-tapes/tapes.py (Clear1nsight, +Apache-2.0). This file only schedules reads, writes and unit moves. +""" +import importlib.util +import random +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +TAPE_PATH = ROOT / "research" / "qq16-gaussian-axis-tapes" / "tapes.py" + + +def load_tapes(): + spec = importlib.util.spec_from_file_location("qq16_axis_tapes", TAPE_PATH) + if spec is None or spec.loader is None: + raise RuntimeError("cannot load pinned tape module") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +TAPES = load_tapes() +Tape = TAPES.Tape +need = TAPES.need + + +def encode(values, width): + lo = -(1 << (width - 1)) + hi = (1 << (width - 1)) - 1 + need(all(type(v) is int and lo <= v <= hi for v in values), "signed input range") + return [(v >> bit) & 1 for v in values for bit in range(width)] + + +def decode(cells, width): + values = [] + for start in range(0, len(cells), width): + word = sum(cells[start + bit] << bit for bit in range(width)) + values.append(word - ((word >> (width - 1)) << width)) + return values + + +def lengths(n, width): + need(type(n) is int and n >= 2 and (n & (n - 1)) == 0, "N=2^n, n>=1") + need(type(width) is int and width >= 1, "component width") + length = n * width + need(length % 2 == 0, "even bit length") + return [length, length] + [length // 2] * 4 + + +def lower_bound(n, width): + """Closed origin-return tours that visit every cell of each tape.""" + return sum(2 * (length - 1) for length in lengths(n, width)) + + +def subtract_segment(dst, src, nbits, width): + """In-place two's-complement subtraction. Heads finish on the last cell.""" + need(nbits % width == 0 and nbits >= width, "whole coordinates") + coords = nbits // width + for coord in range(coords): + borrow = 0 + for bit in range(width): + incoming = src.read() + resident = dst.read() + diff = resident - incoming - borrow + dst.write(diff & 1) + borrow = 1 if diff < 0 else 0 + if bit != width - 1 or coord != coords - 1: + dst.move(1) + src.move(1) + + +def rewind(tape, steps): + for _ in range(steps): + tape.move(-1) + + +def place(real_a, imag_a, real_b, imag_b, width): + n = len(real_a) + half = n // 2 + bits = [ + encode(real_a, width), + encode(imag_a, width), + encode(real_b[:half], width), + encode(imag_b[:half], width), + encode(real_b[half:], width), + encode(imag_b[half:], width), + ] + need([len(row) for row in bits] == lengths(n, width), "placement lengths") + tapes = [] + for index, row in enumerate(bits): + tapes.append(Tape(row, origin=0, trace=True, discardable=(index >= 2))) + return tapes + + +def closed_subtraction(real_a, imag_a, real_b, imag_b, width): + """L546 (a) -= L561 (b), then return every head to its origin. + + data0/data1 hold L546 real/imag for every coordinate. + scratch0/scratch1 hold L561's first N/2 coordinates. + scratch2/scratch3 hold L561's second N/2 coordinates. + """ + n = len(real_a) + need(len(imag_a) == len(real_b) == len(imag_b) == n, "equal lengths") + tapes = place(real_a, imag_a, real_b, imag_b, width) + data0, data1, s0, s1, s2, s3 = tapes + half_bits = (n // 2) * width + saved = [list(tape.cells) for tape in tapes[2:]] + exteriors = [dict(tape.exterior) for tape in tapes] + + subtract_segment(data0, s0, half_bits, width) + subtract_segment(data1, s1, half_bits, width) + data0.move(1) + data1.move(1) + subtract_segment(data0, s2, half_bits, width) + subtract_segment(data1, s3, half_bits, width) + for tape in (data0, data1): + rewind(tape, n * width - 1) + for tape in (s0, s1, s2, s3): + rewind(tape, half_bits - 1) + + for tape in tapes: + need(tape.head == tape.origin, "head returned") + need(tape.exterior == exteriors[tapes.index(tape)], "exterior untouched") + for tape, before in zip(tapes[2:], saved): + need(tape.cells == before, "L561 preserved") + return tapes + + +def counts(tapes): + read = write = move = 0 + for tape in tapes: + traced = [action for action, _pos in tape.trace] + need(sum(item == "read" for item in traced) == tape.count["read"], "trace reads") + need(sum(item == "write" for item in traced) == tape.count["write"], "trace writes") + need(sum(item == "move" for item in traced) == tape.count["move"], "trace moves") + read += tape.count["read"] + write += tape.count["write"] + move += tape.count["move"] + return read, write, move + + +def expect_bill(n, width, tapes): + length = n * width + read, write, move = counts(tapes) + need(read == 4 * length, "read bill") + need(write == 2 * length, "write bill") + need(move == lower_bound(n, width) == 8 * length - 12, "sharp move bill") + return read, write, move + + +def signed_range(width): + return -(1 << (width - 1)), (1 << (width - 1)) - 1 + + +def check_random(rng, n, width, trials): + lo, hi = signed_range(width) + # Both summands lie in [lo/2, hi/2], so minuend = result + source stays + # inside the signed width. lo = -2^(W-1) is even for W>=2. + need(width >= 2, "half-range fixture needs W>=2") + span_lo, span_hi = lo // 2, hi // 2 + accepted = 0 + for _ in range(trials): + result_r = [rng.randint(span_lo, span_hi) for _ in range(n)] + result_i = [rng.randint(span_lo, span_hi) for _ in range(n)] + source_r = [rng.randint(span_lo, span_hi) for _ in range(n)] + source_i = [rng.randint(span_lo, span_hi) for _ in range(n)] + real_a = [result_r[coord] + source_r[coord] for coord in range(n)] + imag_a = [result_i[coord] + source_i[coord] for coord in range(n)] + need(all(lo <= value <= hi for value in real_a + imag_a), "constructed overflow") + tapes = closed_subtraction(real_a, imag_a, source_r, source_i, width) + expect_bill(n, width, tapes) + need(decode(tapes[0].cells, width) == result_r, "real difference") + need(decode(tapes[1].cells, width) == result_i, "imag difference") + accepted += 1 + need(accepted >= 1, "no in-range random fixture") + + +def check_sensitivity(): + """Every payload cell changes the difference for some one-bit flip.""" + n, width = 2, 2 + real_a, imag_a = [1, -2], [0, 1] + real_b, imag_b = [1, 0], [-1, 1] + base = closed_subtraction(real_a, imag_a, real_b, imag_b, width) + base_r = decode(base[0].cells, width) + base_i = decode(base[1].cells, width) + placed = place(real_a, imag_a, real_b, imag_b, width) + for tape_index, tape in enumerate(placed): + for cell in range(len(tape.cells)): + trial = place(real_a, imag_a, real_b, imag_b, width) + trial[tape_index].cells[cell] ^= 1 + out = rerun_from_cells(trial, width) + # Modulo 2^W the map is a translation in each component, so every + # payload bit changes the written difference. Preservation of a + # flipped L561 cell is not itself the signal. + changed = (decode(out[0].cells, width) != base_r or + decode(out[1].cells, width) != base_i) + need(changed, "silent payload cell") + + +def rerun_from_cells(tapes, width): + """Subtract using cells already placed. Used only by the sensitivity control.""" + nbits = len(tapes[0].cells) + half = nbits // 2 + need(len(tapes[2].cells) == half, "half scratch") + data0, data1, s0, s1, s2, s3 = tapes + subtract_segment(data0, s0, half, width) + subtract_segment(data1, s1, half, width) + data0.move(1) + data1.move(1) + subtract_segment(data0, s2, half, width) + subtract_segment(data1, s3, half, width) + for tape in (data0, data1): + rewind(tape, nbits - 1) + for tape in (s0, s1, s2, s3): + rewind(tape, half - 1) + return tapes + + +def check_machine_contract(): + """The pinned Tape charges unit moves and refuses a non-unit jump.""" + tape = Tape([0, 1, 0], origin=0, trace=False, discardable=False) + need(tape.read() == 0, "read at origin") + tape.move(1) + need(tape.count["move"] == 1 and tape.head == 1, "unit move") + try: + tape.move(2) + except ValueError: + pass + else: + raise AssertionError("non-unit move was accepted") + # One-past the last cell is allowed; reading it is not. + tape.move(1) + tape.move(1) + need(tape.head == 3, "one-past") + try: + tape.read() + except ValueError: + pass + else: + raise AssertionError("read past the owned interval was accepted") + + +def check_formula_grid(): + for exponent in range(1, 8): + n = 1 << exponent + for width in range(1, 6): + tapes = closed_subtraction([0] * n, [0] * n, [0] * n, [0] * n, width) + expect_bill(n, width, tapes) + need(decode(tapes[0].cells, width) == [0] * n, "zero real") + need(decode(tapes[1].cells, width) == [0] * n, "zero imag") + + +def main(): + check_machine_contract() + check_formula_grid() + rng = random.Random(546561) + check_random(rng, 2, 3, 40) + check_random(rng, 4, 5, 20) + check_random(rng, 8, 4, 10) + check_random(rng, 512, 5, 1) + # Hand example: 1 - (-1) = 2 on a signed 3-bit component, both coordinates. + tapes = closed_subtraction([1, 1], [0, -1], [-1, 1], [1, 0], 3) + expect_bill(2, 3, tapes) + need(decode(tapes[0].cells, 3) == [2, 0], "hand real") + need(decode(tapes[1].cells, 3) == [-1, -1], "hand imag") + check_sensitivity() + print( + "PASS_QQ16_L546_HEAD_MOVE " + "move=8*N*W-12 read=4*N*W write=2*N*W " + "bound=sum_2(L_t-1) sharp=yes " + "placement=data_full_scratch_halves heads=origin " + "L561=preserved no_new_kappa" + ) + + +if __name__ == "__main__": + main()