diff --git a/research/r437-parent-blank-cursor/PROOF.md b/research/r437-parent-blank-cursor/PROOF.md new file mode 100644 index 0000000000..243e9a499b --- /dev/null +++ b/research/r437-parent-blank-cursor/PROOF.md @@ -0,0 +1,81 @@ +# Cursor meter for one parent-packet blank-return + +No new κ. The selected conditional exponent stays `781451/250000000`. + +## Machine + +The packet tape is `Tape` in +`research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py`. +The alphabet constants in the sibling `words.py` are `ZERO, ONE, LEFT, RIGHT, BLANK = 0, 1, 2, 3, 4`. +A fresh tape has `cells = [LEFT]` and `head = 1`. `read` at `head >= len(cells)` returns `BLANK` and does not extend the tape. `append` reads a `BLANK`, writes one symbol and steps right. `rewind` steps left until it reads `LEFT`, then steps right once. `clear` is + +```text +rewind +while read() != BLANK: + write(BLANK) + step(+1) +rewind +``` + +After `n` appends the tape is `cells = [LEFT] + payload` of length `n + 1`, and the head sits at `n + 1`. Both payload symbols `0` and `1` differ from `LEFT` and from `BLANK`, so the scan length does not depend on the bit. + +## Call that erases a completed packet + +In `packet_engine.py` the success path, after `copy_bits` has consumed a packet, is + +```text +current.read() == BLANK +current.rewind() +current.clear() +``` + +The comparison read is the completeness check. It leaves the head on the trailing blank and is not part of the erasure meter below. `directory.rewind()` on the same source line is a different tape. The blank-return traced here is the following `rewind` and `clear` on `current`. + +`changed.clear()` and `local.clear()` in the same loop are not this call. Their heads depend on `action`, which this note does not price. The failure-path `current.clear()` at the generator's `finally` is likewise not this call: it has no preceding rewind. + +## Meter from the trailing blank + +Write `R(h)` for `rewind` starting at head `h`, and `C` for `clear` starting at head `1` on a tape whose payload cells are exactly positions `1..n`. + +**Rewind from `h = n + 1`.** One left step lands on cell `n`. The loop then reads cells `n, ..., 1` and steps left, then reads `LEFT` at cell `0` and steps right onto cell `1`. That is `n + 1` reads, `0` writes and `n + 2` moves. The `n = 0` case is the same arithmetic: the head is already at `1`, the left step lands on `LEFT`, and the loop body does not run. + +**Clear from head `1`.** Its opening rewind costs `1` read and `2` moves and returns to head `1`. The loop then reads, blanks and steps through cells `1..n`, and one further read sees the virtual blank at `n + 1`. That is `n + 1` reads, `n` writes and `n` moves. The closing rewind is the rewind already counted, from head `n + 1`: `n + 1` reads and `n + 2` moves. Adding these gives + +```text +reads = 2n + 3 +writes = n +moves = 2n + 4 +``` + +and restores head `1` with `cells = [LEFT] + [BLANK] * n`. + +**Sum, the success-path blank-return.** + +```text +reads = (n + 1) + (2n + 3) = 3n + 4 +writes = n +moves = (n + 2) + (2n + 4) = 3n + 6 +``` + +The success-path rewind, the blanking scan and `clear`'s closing rewind each walk every payload cell. None of them jumps. `clear` also opens with its own rewind. On this call the head is already on cell `1`, so that rewind only steps onto `LEFT` and back. It does not walk the payload a fourth time. Its `1` read and `2` moves are included in the `2n + 3` and `2n + 4` figures above. + +## Parent length + +`PHYSICAL.md` states the unexecuted parent geometry + +```text +B = 2, G = 3 * 3^124, S = 2, U = 9475, +n = U * B * G * S * 3^4 = 9475 * 12 * 3^128. +``` + +The same product is `972 * 9475 * 3^124`, because the executed fibre is `2 * 3 * 2 * 3^4 = 972` and the two omitted factors are the `9475` unused rows and the `124` atom coordinates inside `G`. Those coordinates are a factor of `n`, not a side path. Each of the three walks above steps across them. + +Substituting this `n` is the cursor invoice of one success-path blank-return of a single packet of that length. It is not an execution of the parent: the published child bridge allocates the `972`-bit fibre and does not allocate this tape. The model is the predecessor's one-payload comparison, with the executed `Tape` operations in place of the one-visit lower bound. + +Under that bound the parent write count was only `≥ n` and the executed packet's write count was only `≤ 972`. The machine meets both bounds exactly, and only as write counts. The parent move count `3n + 6` is strictly larger than `n` for this `n`. The same call on the executed fibre has writes `972` and moves `3 * 972 + 6 = 2922`, which is not the parent invoice. + +A model that blanks only one executed fibre, or that divides `n` by `3^124` before counting, is a different machine. `clear` writes once per stored payload cell. + +## What this does not sign + +Gather, routing, parking, checkpointing, table setup and the reverse-row coefficient stay unpriced. `BILL.md`'s `G`, `C` and `F` terms are not set to zero. Splitting the parent into `9475` separate tapes would replace one sentinel pair by `9475` sentinel pairs; that layout is not the packet engine's one `current` tape, and it is not claimed here. No carrier admission and no selected-frontier change follows. diff --git a/research/r437-parent-blank-cursor/README.md b/research/r437-parent-blank-cursor/README.md new file mode 100644 index 0000000000..4112949019 --- /dev/null +++ b/research/r437-parent-blank-cursor/README.md @@ -0,0 +1,114 @@ +# Cursor meter for one R437 parent blank-return + +**Partial certificate. No new κ.** The selected conditional exponent stays +`781451/250000000`. + +## Result + +On the success path of `packet_engine.py`, a completed packet is erased by +`rewind` followed by `Tape.clear`, starting from the trailing blank. For a +payload of `n` symbols that call has meter + +```text +reads = 3n + 4, writes = n, moves = 3n + 6. +``` + +The parent geometry in `research/r437-carrier-integration/PHYSICAL.md` is one +payload of length + +```text +n = 9475 * 12 * 3^128 = 972 * 9475 * 3^124. +``` + +The same call on that length is the parent blank-return invoice. The factor +`3^124` is the 124 omitted atom coordinates inside the gap. The opening +rewind, the blanking scan and the closing rewind each step across every +payload cell, so those coordinates are crossed three times. They are not +skipped. + +The write count is exactly the one-visit lower bound from +`research/r437-parent-spectator-blank`. The move count is strictly larger. +The same call on the executed 972-bit fibre has moves `2922`, which does not +pay the parent. + +The argument is in [PROOF.md](PROOF.md). `verify.py` runs the pinned +`records.Tape` on every length through 48, on the 972-bit fibre, and on the +two miniature parents `9475 * 12 * 3^k` for `k = 0, 1`. It does not allocate +the `3^128` parent. + +## What stays open + +`changed.clear()` and `local.clear()` still depend on where `action` leaves +the head. Gather, routing, parking, checkpointing and table setup are not +priced. One tape of length `n` is the predecessor's payload model; `9475` +separate tapes would add extra sentinel walks and are not this call. No +supplier and no new exponent is claimed. + +## Task and overlap + +- Task: `r437-carrier-integration`, scope **refined**. +- Base: canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. +- Selected record SHA-256 `9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`. + +Session r85, item 8 of the ordered eligible list. The 19 October handoffs +(discussion comments 19030045, 19030047, 19030049, and 19030053) are already +delivered or closed. Later handoffs whose canonical artifact is an open pull +request, including the H25 requests and the 2026-11-02 audits of #6348 +through #6361, are excluded. The revision-8 next-decision table then supplies +six rows, naming `p104-side-correction`, `coverage-law-change` and +`bit-helper-contract`. Catalogue cards not named by those rows follow, in +catalogue order. Item 8 is `r437-carrier-integration`. + +The card's reverse coefficient, child-constructor tapes, SOURCE87 fibre +multiplicity and payload-ratio lower bound are already delivered by this +account (#4147, #4160, #5277, #5276). This package answers open question 1 of +`research/r437-parent-spectator-blank`: the exact fixed-tape visit count, +including cursor motion across the 124 omitted coordinates. It does not +rederive the coefficient or rerun the pooled compiler. + +Checked on 2026-11-02: no open pull request states this `3n+6` move count. +The merged predecessor #5276 stops at the payload ratio. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -B scripts/research_selected_baseline.py +python3 -B research/r437-parent-blank-cursor/verify.py +python3 -B research/r437-parent-blank-cursor/test_verify.py +python3 -B scripts/research_package.py --package research/r437-parent-blank-cursor +``` + +`verify.py` prints `PASS_R437_PARENT_BLANK_CURSOR` with `writes` equal to the +parent payload and `moves = 3 * writes + 6`. `test_verify.py` prints +`PASS_R437_PARENT_BLANK_CURSOR_CONTROLS`. + +Not run: `physical.py`, the pooled compiler, Lean, Docker, and +`make frontier6030-verify`. The universal statement for every `n` is the +control-flow count in `PROOF.md`; the checker executes the machine on the +lengths named above. + +## Open next questions + +1. Where does `action` leave the head of `changed` and `local` before their + `clear` calls? Those blank-returns are not the success-path `current` + call priced here. First step: one source-bound postcondition for `action` + on a fibre of length `n`. Blocker: `action` is outside this package. +2. Can one of `G`, `C` or `F` in `BILL.md` be instantiated on both arms + without setting the others to zero? A blank-return meter still does not + sign the whole C/D inequality. First step: pin one tariff. Blocker: those + tariffs are not inputs here. + +## Credit + +The parent extents, the constants `9475` and `972`, and the statement that a +one-visit lower bound is not the machine invoice are Chris R / Clear1nsight, +`research/r437-carrier-integration` and the open question in +`research/r437-parent-spectator-blank` (unpaidmoon #5276). The tape operations +are the retained predecessor `records.Tape` loaded by the selected physical +caller. The carrier lineage remains ai-nanachi / PR #3647, Ali Romman / +PR #1043, and Sagar Thakrar / PR #3700 and PR #2423. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human or formal-kernel review is claimed. diff --git a/research/r437-parent-blank-cursor/SOURCES.json b/research/r437-parent-blank-cursor/SOURCES.json new file mode 100644 index 0000000000..24294ab8f4 --- /dev/null +++ b/research/r437-parent-blank-cursor/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/r437-carrier-integration/PHYSICAL.md", + "usage": "provenance", + "git_blob": "ec85739460fb61c6505f9b1179f3bb3dc86cc079", + "sha256": "c7689d458e03853f5487a27707003698d04cbca086a503af47cd95d78cb14864" + }, + { + "path": "research/r437-parent-spectator-blank/README.md", + "usage": "provenance", + "git_blob": "ad16671a4cb45d13cd7c4d97b709bc53b8d89607", + "sha256": "009860adc553a14ad5f1f41a0e65fb0d05e6eef5cb219979e1b453513c1516d9" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/packet_engine.py", + "usage": "input", + "git_blob": "72543f684f38fefeacc2ee66d81661f1a2439cf7", + "sha256": "c80fc3aa9092f91cc309b2fb2dbc3618bf96bdb9b8498503993ea161f0ae2134" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "usage": "input", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py", + "usage": "input", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + } + ] +} diff --git a/research/r437-parent-blank-cursor/TASK.json b/research/r437-parent-blank-cursor/TASK.json new file mode 100644 index 0000000000..8e3b22b8d6 --- /dev/null +++ b/research/r437-parent-blank-cursor/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "r437-carrier-integration", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "r437-carrier-integration", + "question": "Can the paid R437 two-window carrier improvement be admitted by the actual pooled compiler and physical caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/r437-two-window-carrier/README.md", + "research/r437-reverse-row-coefficient/README.md" + ], + "methods": [ + "Close one compiler/request, caller or precision/stock implication for the pinned paid exchange.", + "Falsify that exact interface with an arbitrary-dirty-state or chronology counterexample." + ], + "acceptance_gate": "Pin the complete source and destination contracts, exact paid and scalar deltas, and all remaining assumptions. A local moment gain is not a physical or all-size supplier admission.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Choose one unclaimed obligation: pooled compiler codebook/request alignment, actual physical caller, or precision/stock envelope using the already reported reverse coefficient. Pin the input and receiver, preserve dirty/source windows, and test one binding with a rejection control. Stop at unresolved dependencies; do not rederive the coefficient or quote the local moment as a completed bound.", + "bottleneck_link": "The exchange changes the paid profile; integration must establish that its gain survives the complete caller.", + "allowed_variations": [ + "One compiler rebind, one actual caller boundary, or one precision/stock implication." + ], + "scope_change_triggers": [ + "Ignoring added ADDs, retaining an obsolete reverse coefficient, or declaring global admission from the local histogram." + ], + "overlap_terms": [ + "R437", + "two-window carrier", + "4067", + "4147", + "pooled compiler", + "request alignment", + "reverse row coefficient" + ], + "existing_checks": [ + { + "scope": "PR #4067: source-bound two-window carrier with (2,2) to (1,3) paid exchange and fixed OQ4 host.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Pooled compiler/request rebind, physical caller and precision/stock admission.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4147: reverse row coefficient follow-up.", + "evidence": "research/r437-reverse-row-coefficient/README.md", + "remaining": "Use the exact coefficient in a caller-bound precision/stock proof rather than repeat the arithmetic.", + "status": "author-checked", + "source_commit": "72e7bb797adf82aeb525a399f56ab8adbab8e93c", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "On the pinned packet-engine success path, certify the exact Tape rewind-then-clear meter of one parent payload of length 9475*12*3^128, including the cursor walks across the 124 omitted atom coordinates.", + "scope_change_reason": "The card asks for one unclaimed physical-caller obligation of the paid R437 exchange and says not to rederive the reverse coefficient. Open question 1 of research/r437-parent-spectator-blank asks for this cursor invoice. The payload ratio, fibre multiplicity and constructor tapes are already delivered and are not repeated.", + "bottleneck_link": "The paid R437 exchange cannot be admitted until the parent blank-return is an exact charge rather than a one-visit lower bound. This prices that cursor. It does not sign the rest of the C/D inequality or raise selected kappa.", + "budget_minutes": 60, + "stop_rule": "Stop when the success-path meter reads=3n+4, writes=n, moves=3n+6 is certified for the parent length, or when the pinned Tape or call site disagrees with that count. Do not allocate the 3^128 parent or rerun the pooled compiler.", + "outcome": "partial", + "evidence": "verify.py prints PASS_R437_PARENT_BLANK_CURSOR with writes equal to 9475*12*3^128 and moves=3*writes+6. test_verify.py prints PASS_R437_PARENT_BLANK_CURSOR_CONTROLS. PROOF.md counts the three walks. No new kappa.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Where does action leave the head of changed and local before their clear calls?", + "why_it_matters": "Those blank-returns are a different cursor start from the success-path current tape priced here, so their meters are not yet the same formula.", + "first_step": "Pin one source-bound postcondition for action on a fibre of length n, then rerun rewind and clear from that head.", + "blocked_by": "action is outside this package." + }, + { + "question": "Can one of BILL.md's G, C or F terms be instantiated on both arms without setting the others to zero?", + "why_it_matters": "An exact blank-return meter still does not sign the whole C/D inequality, and the selected supplier remains complex-bound.", + "first_step": "Name one of gather/route, checkpoint/disposal or table-setup and pin its tariff on C and D.", + "blocked_by": "Those tariffs are not inputs of this package." + } + ] +} diff --git a/research/r437-parent-blank-cursor/VERIFY.json b/research/r437-parent-blank-cursor/VERIFY.json new file mode 100644 index 0000000000..625343f8a7 --- /dev/null +++ b/research/r437-parent-blank-cursor/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/selected-bit-physical-caller/inputs/pr2753/packet_engine.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "The pinned Tape success-path rewind-then-clear meter is reads=3n+4, writes=n, moves=3n+6 for every n through 48, for both payload bits, for the 972-bit fibre, and for miniature parents 9475*12*3^k at k=0 and k=1. The parent length 9475*12*3^128 equals 972*9475*3^124, and the fibre move count 2922 is strictly smaller." + }, + { + "argv": ["{python}", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "An independent transcription of rewind, clear's opening rewind, the blanking scan and the closing rewind agrees with Tape for n through 40. Payload-only moves, a 972-bit write count, dropping 3^124, and clear without the opening rewind are rejected for the parent length." + } + ] +} diff --git a/research/r437-parent-blank-cursor/test_verify.py b/research/r437-parent-blank-cursor/test_verify.py new file mode 100644 index 0000000000..8f73d6754a --- /dev/null +++ b/research/r437-parent-blank-cursor/test_verify.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python3 +"""Rejection controls for the parent blank-return cursor meter.""" + +from __future__ import annotations + +import importlib.util +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("blank_cursor", HERE / "verify.py") +verify = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(verify) + + +def transcribed(n: int): + """Success-path rewind, then clear, counted without records.Tape. + + clear always opens with its own rewind, including when the head is + already on the first payload cell. + """ + reads = writes = moves = 0 + head = n + 1 + + def step(direction): + nonlocal head, moves + head += direction + if head < 0: + raise AssertionError(head) + moves += 1 + + def rewind(): + nonlocal reads + step(-1) + while head != 0: + reads += 1 + step(-1) + reads += 1 + step(1) + + rewind() + rewind() + while head != n + 1: + reads += 1 + writes += 1 + step(1) + reads += 1 + rewind() + return reads, writes, moves + + +def reject(name, bad_model_matches): + if bad_model_matches: + raise AssertionError(name + " matched the measured meter") + + +def main(): + tape_type, words = verify.load_tape() + for n in range(0, 41): + for bit in (0, 1): + _, _, total = verify.success_path(tape_type, words.BLANK, n, bit) + if total != transcribed(n): + raise AssertionError((n, bit, total, transcribed(n))) + if n: + reject("payload-only moves", total[2] == n) + reject("clear-without-opening-rewind", total[2] == 3 * n + 4) + + parent = verify.parent_payload() + reject("executed fibre pays the parent", parent == verify.EXECUTED_BITS) + reject("dropped omitted coordinates", parent == 9475 * 12 * 3 ** (128 - 124)) + reject("one visit is the whole meter", verify.success_moves(parent) == parent) + result = verify.certify() + if result["writes"] != parent or result["moves"] != verify.success_moves(parent): + raise AssertionError(result) + if result["reads"] != verify.success_reads(parent): + raise AssertionError(result) + print( + "PASS_R437_PARENT_BLANK_CURSOR_CONTROLS" + f" checked_n=0..40" + f" parent_moves_minus_writes={result['moves'] - result['writes']}" + " rejected=payload_only,fibre_only,gap_omitted,clear_without_opening_rewind" + ) + + +if __name__ == "__main__": + main() diff --git a/research/r437-parent-blank-cursor/verify.py b/research/r437-parent-blank-cursor/verify.py new file mode 100644 index 0000000000..8b36539bf4 --- /dev/null +++ b/research/r437-parent-blank-cursor/verify.py @@ -0,0 +1,159 @@ +#!/usr/bin/env python3 +"""Exact success-path blank-return meter for the R437 parent payload. + +The tape is the pinned predecessor records.Tape. The call is packet_engine's +success-path rewind followed by clear, starting from the trailing blank. +This checker does not allocate the parent and does not run physical.py. +""" + +from __future__ import annotations + +import importlib.util +import sys +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +VENDOR = ROOT / "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor" +ENGINE = ROOT / "research/selected-bit-physical-caller/inputs/pr2753/packet_engine.py" + +UNUSED_ROWS = 9475 +OMITTED_COORDINATES = 124 +EXECUTED_BITS = 972 + + +def success_reads(n: int) -> int: + return 3 * n + 4 + + +def success_writes(n: int) -> int: + return n + + +def success_moves(n: int) -> int: + return 3 * n + 6 + + +def load_tape(): + sys.path.insert(0, str(VENDOR)) + spec = importlib.util.spec_from_file_location("r437_blank_records", VENDOR / "records.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + words = importlib.import_module("words") + return module.Tape, words + + +def parent_payload() -> int: + return UNUSED_ROWS * 12 * 3**128 + + +def meter(tape): + counted = tape.meter + return (counted.reads, counted.writes, counted.moves) + + +def delta(before, after): + return tuple(after[i] - before[i] for i in range(3)) + + +def success_path(tape_type, blank, n: int, bit: int, left: int = 2): + """n appends, completeness read, then rewind and clear.""" + tape = tape_type() + for _ in range(n): + tape.append(bit) + if tape.head != n + 1 or tape.read() != blank or tape.head != n + 1: + raise AssertionError((n, tape.head)) + start = meter(tape) + tape.rewind() + middle = meter(tape) + tape.clear() + end = meter(tape) + if tape.head != 1 or list(tape.cells) != [left] + [blank] * n: + raise AssertionError((n, tape.head, list(tape.cells[:4]), len(tape.cells))) + return delta(start, middle), delta(middle, end), delta(start, end) + + +def certify(): + tape_type, words = load_tape() + if (words.ZERO, words.ONE, words.LEFT, words.RIGHT, words.BLANK) != (0, 1, 2, 3, 4): + raise AssertionError("alphabet moved") + blank = words.BLANK + source = ENGINE.read_text(encoding="utf-8") + call = ( + 'need(current.read()==directory.read()==BLANK,"complete shared packet and directory")\n' + " current.rewind();directory.rewind()\n" + " if current is not source:current.clear()\n" + ) + if call not in source: + raise AssertionError("success-path blank-return call site moved") + clear_source = (VENDOR / "records.py").read_text(encoding="utf-8") + if "def clear(self):\n self.rewind()\n while self.read() != BLANK:\n" not in clear_source: + raise AssertionError("Tape.clear control flow moved") + + for n in list(range(0, 49)) + [EXECUTED_BITS]: + for bit in (0, 1): + rewind, clear, total = success_path(tape_type, blank, n, bit, words.LEFT) + if rewind != (n + 1, 0, n + 2): + raise AssertionError((n, bit, rewind)) + if clear != (2 * n + 3, n, 2 * n + 4): + raise AssertionError((n, bit, clear)) + if total != (success_reads(n), success_writes(n), success_moves(n)): + raise AssertionError((n, bit, total)) + + # The omitted-coordinate factor is inside the length. A miniature parent + # with 3^k in place of 3^128 still writes every cell, including that factor. + for exponent in (0, 1): + miniature = UNUSED_ROWS * 12 * 3**exponent + _, _, total = success_path(tape_type, blank, miniature, 1, words.LEFT) + if total[1] != miniature or total != ( + success_reads(miniature), + miniature, + success_moves(miniature), + ): + raise AssertionError((exponent, total)) + skipped = miniature // 3**exponent + if exponent and total[1] == skipped: + raise AssertionError("gap cells were not written") + + child = 2 * 3 * 2 * 3**4 + if child != EXECUTED_BITS: + raise AssertionError(child) + parent = parent_payload() + if parent != UNUSED_ROWS * EXECUTED_BITS * 3**OMITTED_COORDINATES: + raise AssertionError(parent) + if parent != UNUSED_ROWS * 2 * (3 * 3**OMITTED_COORDINATES) * 2 * 3**4: + raise AssertionError(parent) + executed = (success_reads(EXECUTED_BITS), EXECUTED_BITS, success_moves(EXECUTED_BITS)) + full = (success_reads(parent), parent, success_moves(parent)) + if executed[1] >= full[1] or executed[2] >= full[2]: + raise AssertionError((executed, full)) + return { + "rows": UNUSED_ROWS, + "omitted_coordinates": OMITTED_COORDINATES, + "executed_bits": EXECUTED_BITS, + "parent_payload": parent, + "reads": full[0], + "writes": full[1], + "moves": full[2], + "executed_moves": executed[2], + } + + +def main(): + result = certify() + print( + "PASS_R437_PARENT_BLANK_CURSOR" + f" rows={result['rows']}" + f" omitted_coordinates={result['omitted_coordinates']}" + f" executed_bits={result['executed_bits']}" + f" parent_payload={result['parent_payload']}" + f" reads={result['reads']}" + f" writes={result['writes']}" + f" moves={result['moves']}" + f" executed_fibre_moves={result['executed_moves']}" + " call=rewind_then_clear" + " no_new_kappa" + ) + + +if __name__ == "__main__": + main()