diff --git a/research/reverse-record-parking/PROOF.md b/research/reverse-record-parking/PROOF.md new file mode 100644 index 0000000000..2bb9fe7181 --- /dev/null +++ b/research/reverse-record-parking/PROOF.md @@ -0,0 +1,143 @@ +# Reverse-record parking + +This is a scoped construction and written all-size proof. The finite replay +corroborates the proof. It is not a proof-kernel certificate or a complete +multiplication theorem. + +## Contract + +Use ywz65's PR2635 two-tape model. Each transition reads the parking head P +and packet-port head B, optionally writes either cell, and moves each head +by at most one cell. Every issued write counts, including an unchanged write. +The alphabet is `_,0,1,^,$,F,R`, where `_` is blank. A command selects one of +four entry states. All later actions depend only on a finite state and the +two scanned symbols. There is no length, depth, coordinate or floor register. + +At entry P points at the first blank cell above its live suffix. Below that +top are frame delimiters F and records. The new representation of a packet +`b0 ... b(n-1)` is `R b(n-1) ... b0`. At the port, `^` occupies a-1 and B +points at a. A full packet has its bits at a through a+n-1 and `$` at a+n. +An empty packet is `$`. An empty port is blank on the cells the next output +will occupy. Length zero and unequal successive lengths are permitted. + +PUSH requires a full packet and blank parking extension. POP requires a +record in the current frame and a blank destination port. BEGIN/END and +matched whole-packet PUSH/POP commands follow the trusted, well-bracketed +ownership discipline of PR2635. They do not expose arbitrary partial pops. +Every cell outside the described footprints may contain opaque arbitrary +data and must retain its value. The `^` marker and every boundary head return. + +## Finite table + +`controller.py` enumerates all 441 keys of nine states and two seven-symbol +reads. Each key has exactly one action. The nonrejecting rules are below. +An omitted write means no write, and an omitted move means no movement. + +| State and read condition | Writes | Moves P,B | Next state | +| --- | --- | --- | --- | +| begin, P blank | P=F | +1,0 | done | +| end, P blank | none | -1,0 | end_check | +| end_check, P=F | P blank | 0,0 | done | +| push, P blank and B a bit or `$` | P=R | +1,0 | seek | +| seek, P blank and B a bit | none | 0,+1 | seek | +| seek, P blank and B=`$` | B blank | 0,-1 | copy | +| copy, P blank and B a bit b | P=b, B blank | +1,-1 | copy | +| copy, P blank and B=`^` | none | 0,+1 | done | +| pop, both blank | none | -1,0 | deliver | +| deliver, P a bit b and B blank | P blank, B=b | -1,+1 | deliver | +| deliver, P=R and B blank | P blank, B=`$` | 0,-1 | rewind | +| rewind, P blank and B a bit | none | 0,-1 | rewind | +| rewind, P blank and B=`^` | none | 0,+1 | done | + +Two boundary rejection rules restore the initial P head without writes. +In end_check, a non-F cell causes P to move right and reject. In deliver, +P=F and B blank causes the same move and rejection. Other unspecified keys +reject without writing or moving. Every table move is in {-1,0,1}. + +## PUSH invariant + +Let P enter at h and the packet have length n. The entry writes R at h and +advances P to h+1. In seek, after k bit transitions, B is at a+k and every +packet bit is unchanged. Thus seek reaches `$` after exactly n transitions. +Its `$` transition erases the marker and places B at a+n-1. + +After k copy transitions, for 0<=k<=n, the cells h+1 through h+k contain +`b(n-1) ... b(n-k)`, P is at h+k+1, and B is at a+n-1-k. The last k packet +bits are blank and all earlier bits are unchanged. This is immediate for +k=0 and follows for k+1 from the copy rule. At k=n, B sees `^`. Moving B +right terminates at a, with a reversed parked record, a wholly blank consumed +packet and P at h+n+1. No other cell changes. For n=0 the same rules erase +`$`, encounter `^`, and terminate after writing the single R record marker. + +## POP invariant + +Let the top record start at h, so entry P is h+n+1 and B is a. Entry moves +P left. After k deliver-bit transitions, for 0<=k<=n, the first k original +bits `b0 ... b(k-1)` occupy a through a+k-1. P is at h+n-k, B is at a+k, +and the consumed parking cells are blank. The remaining record prefix and +every earlier parking cell are unchanged. The inductive step reads b(k) +from the reversed record and writes it at a+k. + +At k=n, P sees R. Its transition erases R, writes `$` at a+n, and moves B +left. Rewind crosses exactly n bits, then recognizes `^` and moves right. +It terminates with P=h and B=a. The original packet order and extent return, +the entire record is blank, and every other cell is unchanged. This also +holds at n=0. POP is therefore the complete-boundary inverse of PUSH. + +## Frames, rejection scope and physical storage + +BEGIN/END are inverse on an empty frame. POP never traverses an F delimiter. +An empty-frame POP and a nonempty-frame END reject with both entry heads and +every cell unchanged. Structural induction on any finite well-bracketed +command sequence now gives LIFO packet order, complete record/frame erasure, +head return and bit-for-bit opaque ancestor preservation. Nested packets +may have arbitrary finite lengths. No transition reads below the frame it +is allowed to inspect. The one shared packet port is supplied and consumed +by the caller, outside the parking tariff. + +The blank-output precondition matters. Unlike PR2635's preflight scan, this +POP can write an earlier output bit before discovering an occupied later +cell. For example, park `R10`, let the output at a be blank and at a+1 be 1. +POP writes 0 at a and erases its parking copy before rejecting at a+1. +`mutation_checks` executes this exact scope control. No all-malformed-input +rollback or no-write-before-any-occupied-cell guarantee is claimed. A caller +requiring that guarantee needs a separately charged preflight. + +At a valid boundary, the occupied parking suffix has exactly one cell per +live payload bit, one per live record and one per live frame, as in PR2635. +The full port has n bit cells and its two markers. There is no extra tape, +new alphabet symbol, runtime descriptor stack or increased occupied storage. +Erased backing capacity is not claimed to disappear. Existing forward-format +records cannot be read by this controller: all participants in an owned +parking region must use the new format, or pay for a separate conversion. + +## Complete tariff and comparison + +Count the literal table transitions in the preceding invariants. + +| Operation | Steps | Reads | Writes | Unit head moves | +| --- | --- | --- | --- | --- | +| BEGIN | 1 | 2 | 1 | 1 | +| END | 2 | 4 | 1 | 1 | +| PUSH n | 2n+3 | 4n+6 | 2n+2 | 3n+3 | +| POP n | 2n+3 | 4n+6 | 2n+2 | 3n+3 | + +For PUSH the transitions are entry, n seek, marker, n copy, terminal. +For POP they are entry, n delivery, marker, n rewind, terminal. The marker +transition writes twice for POP; every bit transition writes twice. Summing +the stated displacements proves the move counts, including empty packets. + +For d balanced frame pairs, r matched packet pairs and total payload V, +counting each packet pair once, the new totals are + +``` +steps = 4V+6r+3d reads = 8V+12r+6d +writes = 4V+4r+2d moves = 6V+6r+2d. +``` + +PR2635's published totals are cited premises, not replayed here. Subtracting +the new totals from its `5V+7r+3d`, `10V+14r+6d`, `4V+4r+2d`, `8V+8r+2d` +gives exact savings of V+r steps, 2V+2r reads, zero writes and 2V+2r moves. +These quantities concern the valid matched-packet parking contract. They +are not a wall-clock benchmark, shortest-controller theorem, complete caller +invoice, recursive profile improvement or kappa gain. diff --git a/research/reverse-record-parking/README.md b/research/reverse-record-parking/README.md new file mode 100644 index 0000000000..5ec5fc9044 --- /dev/null +++ b/research/reverse-record-parking/README.md @@ -0,0 +1,105 @@ +# Reverse parked records to remove one POP scan + +This contribution was produced by Nick Petalas. Claim type: a new finite +controller with a scoped written all-size proof and exact finite corroboration. +For the valid matched-packet interface of ywz65's +[PR2635](https://github.com/CrocSwap/integer-mult-bounds/pull/2635), storing each +record in reverse order reduces POP from `3n+4` to `2n+3` steps. PUSH remains +`2n+3`. Packet order, returned heads, cleanup and opaque ancestors are preserved. + +For total matched payload V, r packet pairs and d frame pairs: + +| Complete parking charge | PR2635, cited | New controller | Saving | +| --- | --- | --- | --- | +| Steps | 5V+7r+3d | 4V+6r+3d | V+r | +| Reads | 10V+14r+6d | 8V+12r+6d | 2V+2r | +| Writes | 4V+4r+2d | 4V+4r+2d | 0 | +| Unit head moves | 8V+8r+2d | 6V+6r+2d | 2V+2r | + +The new table has nine states and 441 entries over the same two tapes and +seven-symbol alphabet. Occupied storage is unchanged. The construction and +all-size induction are in [PROOF.md](PROOF.md); the compiled finite table and +sparse interpreter are in [controller.py](controller.py). + +## Evidence and reproduction + +Use CPython 3.12 and its standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/reverse-record-parking/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/reverse-record-parking/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/reverse-record-parking +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reverse-record-parking --check-source-history +``` + +Another installed CPython 3.12 may replace that path. Direct replay emits +`PASS_REVERSE_RECORD_PARKING` in a generated JSON receipt, bound to every +package file by SHA256. It writes only stdout. No predecessor executable or +mathematical receipt is consumed. The package launcher checks historical +source pins through Git, so that command requires full repository history. + +The checker enumerates all 2,047 packets through length ten, totaling 18,434 +payload bits. A separate dense-array interpreter agrees with the sparse +interpreter and every expected packet, head, preserved cell and tariff. +There are 21 translated cases through length 16,384, plus unequal and empty +records nested to depths 1, 2, 7, 32 and 129. The largest translated cases +use the sparse interpreter. Thirteen controls cover boundary rejection, +invalid tables, five semantic mutations and the malformed-port scope limit. +Every check remains enabled under optimized Python. + +## Scope and source status + +POP requires a blank destination port. Unlike the predecessor's preflight, +it may modify an earlier cell before rejecting a later occupied output cell. +That stronger malformed-input guarantee is unclaimed and has an executable +counterexample. Commands are trusted and well-bracketed; arbitrary partial +pops and hostile-command isolation are outside the contract. All owners of +one parking region must use the new record format. No free migration of live +forward-format records is claimed. + +This is a physical-interface side result, with an explicit change from the +picker's `portable-replay` card. It can lower a caller's parking subbill after +an actual format-compatible substitution. Packet production, consumption, +invocation dispatch, complete physical reserve, native/frame/precision costs +and the selected supplier's five assumptions remain separate obligations. +No shortest-controller result, selected cold replay, new kappa, complete +multiplication theorem, Lean or Docker run is claimed. + +The scientific base is canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected PR6030. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372174) +precedes construction. Live open PRs, recent account work and handoffs, +distinctive main README terms and merged-PR terms were checked. The overlap +cache covered 539 open PRs and 6,558 Discussion records, with complete remote +pagination and incomplete sparse local notes. Arbitrary diffs, private work +and unpublished work remain outside that coverage. Source hashes in +[SOURCES.json](SOURCES.json) bind cited provenance, not reverified mathematics. + +## Open next questions + +Bind one actual caller's matching whole-packet park/return sequence to this +representation and replace its parking subbill, retaining all serialization, +port production/consumption and backing charges. The first step is to identify +any direct readers of the old forward-format records. A mixed-format live +stack or a caller requiring the predecessor's malformed-port preflight blocks +an automatic substitution. No larger construction search is needed first. + +## Credit and implementation limits + +Credit ywz65 for PR2635's matched-record interface, finite two-tape model, +published invoice and frame induction, and PR2574/2534/2483/2250/2287 and +their retained physical/native/compiler lineage. Reversed stack storage is +a classical technique. The contribution is this format-compatible valid-input +construction, exact improved invoice, proof and standalone checker. No broad +priority claim is made. New work is Apache-2.0. Independent human and formal +proof-kernel review are unclaimed. + +The simulator bounds each tape input at 100,000 occupied cells and each run +at 200,000 transitions. Dense interpretation caps its interval below 500,000 +cells. Fixture loops and mutation inventories are finite, and functions have +at most 60 lines. Dynamic Python allocation and dataclass construction are +managed-runtime deviations from Power of Ten rules 3 and 8. Cell/step/table +bounds constrain live data; the mathematical tape machine itself has no +runtime descriptor and applies to every finite valid packet. Warning-strict +normal/optimized runs and in-memory syntax checks supply diagnostics. No +fixed byte-capacity guarantee or new global analyzer configuration is claimed. diff --git a/research/reverse-record-parking/SOURCES.json b/research/reverse-record-parking/SOURCES.json new file mode 100644 index 0000000000..077b3b85c6 --- /dev/null +++ b/research/reverse-record-parking/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/finite-parking-frames/PROOF.md", + "usage": "provenance", + "git_blob": "15ea512d0f534649b11b4bb78eebf2c2d85f5a6b", + "sha256": "0aeddba71df2fba37ae026ac10585b8ee41dee96e453fd950f12f307f9252090" + }, + { + "path": "research/finite-parking-frames/README.md", + "usage": "provenance", + "git_blob": "b2b1bfc96d17b9ec6739203b7c98fdd3e998fda0", + "sha256": "db87ca92c1401ba58d8f353c1feb338fee44690849602c890050b0ff8d6b8c37" + } + ] +} diff --git a/research/reverse-record-parking/TASK.json b/research/reverse-record-parking/TASK.json new file mode 100644 index 0000000000..f419c6d605 --- /dev/null +++ b/research/reverse-record-parking/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "portable-replay", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "portable-replay", + "question": "Can one reproducible environment or artifact-comparison failure be repaired?", + "starting_points": [ + "research/gzip-container-reproducibility/README.md", + "docs/ci-verification.md" + ], + "methods": [ + "Reproduce one portability failure and add a minimal cross-environment fix.", + "Audit one canonical-payload comparison for omitted proof-relevant fields." + ], + "acceptance_gate": "Preserve immutable source hashes and proof-relevant content; a different compressed byte stream alone is not a mathematical mismatch.", + "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": "Reproduce one specific mismatch or audit one canonical comparison for omitted proof-relevant fields.", + "bottleneck_link": "Portable exact checks prevent environment failures from blocking valid contributions.", + "allowed_variations": [ + "One interpreter/version mismatch or one payload field comparison." + ], + "scope_change_triggers": [ + "Removing immutable-source pins because generated compressed bytes differ." + ], + "overlap_terms": [ + "gzip container", + "reproducibility", + "canonical payload" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct reverse-record two-tape parking with a strictly smaller complete valid-packet tariff.", + "scope_change_reason": "The donor requests original work rather than an audit. The selected baseline passed; a self-posed physical-interface construction replaces the portability task.", + "bottleneck_link": "Side result for precision_tape and owned_erasure: reduce a matched-packet parking subbill while retaining arbitrary ancestor data and complete head/record return. No selected assumption is discharged.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved controller improvement; do not optimize beyond its exact complete tariff.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-size invariants. The standalone verifier enumerates 2047 packets, 21 translated cases and five nesting depths, compares two interpreters and exact charges, and checks 13 rejection/mutation/scope controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a source-bound caller adopt reversed whole-packet records and realize the complete parking subbill reduction?", + "why_it_matters": "A proven local controller saving only affects an actual caller after its representation and full port bill agree.", + "first_step": "Identify every direct reader of the forward record format and one matched park/return path, then price the substitution including port production and consumption.", + "blocked_by": "No actual caller substitution, live-format migration or optional malformed-port preflight has been priced." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372174", + "predecessor": { + "pr": 2635, + "author": "ywz65", + "head": "1662dda699d9ea57b3fb13a23873b087d765149f", + "status": "cited construction and invoice; not audited or replayed" + }, + "framework_assumptions_discharged": [] +} diff --git a/research/reverse-record-parking/VERIFY.json b/research/reverse-record-parking/VERIFY.json new file mode 100644 index 0000000000..abcc622349 --- /dev/null +++ b/research/reverse-record-parking/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New 441-entry finite table; all packets through length ten; translated and nested valid endpoints, exact bills, sparse/dense agreement, semantic mutations and scope controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite controller, endpoint and tariff checks with interpreter optimization enabled." + } + ] +} diff --git a/research/reverse-record-parking/controller.py b/research/reverse-record-parking/controller.py new file mode 100644 index 0000000000..dfd27c2a79 --- /dev/null +++ b/research/reverse-record-parking/controller.py @@ -0,0 +1,124 @@ +"""Finite two-tape controller for reversed parking records. Apache-2.0.""" + +from dataclasses import dataclass +from itertools import product + +ALPHABET = ("_", "0", "1", "^", "$", "F", "R") +STATES = ("begin", "end", "end_check", "push", "seek", "copy", + "pop", "deliver", "rewind") +HALTS = ("done", "reject") +MAX_CELLS = 100_000 +MAX_STEPS = 200_000 + + +@dataclass(frozen=True) +class Action: + next_state: str + write_p: str | None = None + write_b: str | None = None + move_p: int = 0 + move_b: int = 0 + + +def transition(state: str, p: str, b: str) -> Action: + """The only action-selection inputs are a state and two scanned symbols.""" + if state == "begin" and p == "_": + return Action("done", "F", move_p=1) + if state == "end" and p == "_": + return Action("end_check", move_p=-1) + if state == "end_check" and p == "F": + return Action("done", "_") + if state == "end_check": + return Action("reject", move_p=1) + if state == "push" and p == "_" and b in ("0", "1", "$"): + return Action("seek", "R", move_p=1) + if state == "seek" and p == "_" and b in ("0", "1"): + return Action("seek", move_b=1) + if state == "seek" and p == "_" and b == "$": + return Action("copy", write_b="_", move_b=-1) + if state == "copy" and p == "_" and b in ("0", "1"): + return Action("copy", b, "_", 1, -1) + if state == "copy" and p == "_" and b == "^": + return Action("done", move_b=1) + if state == "pop" and p == "_" and b == "_": + return Action("deliver", move_p=-1) + if state == "deliver" and p in ("0", "1") and b == "_": + return Action("deliver", "_", p, -1, 1) + if state == "deliver" and p == "R" and b == "_": + return Action("rewind", "_", "$", move_b=-1) + if state == "deliver" and p == "F" and b == "_": + return Action("reject", move_p=1) + if state == "rewind" and p == "_" and b in ("0", "1"): + return Action("rewind", move_b=-1) + if state == "rewind" and p == "_" and b == "^": + return Action("done", move_b=1) + return Action("reject") + + +def validate_table(table: dict) -> None: + if not isinstance(table, dict) or len(table) != len(STATES) * len(ALPHABET)**2: + raise ValueError("transition table size") + expected = set(product(STATES, ALPHABET, ALPHABET)) + if set(table) != expected: + raise ValueError("incomplete or extra transition keys") + for action in table.values(): + if not isinstance(action, Action): + raise ValueError("action type") + if action.next_state not in STATES + HALTS: + raise ValueError("unknown next state") + if action.write_p not in (None,) + ALPHABET: + raise ValueError("parking write outside alphabet") + if action.write_b not in (None,) + ALPHABET: + raise ValueError("port write outside alphabet") + for move in (action.move_p, action.move_b): + if type(move) is not int or move not in (-1, 0, 1): + raise ValueError("head move must be a unit integer") + + +def compile_table() -> dict: + table = {key: transition(*key) for key in product(STATES, ALPHABET, ALPHABET)} + validate_table(table) + return table + + +def validate_tape(tape: dict) -> None: + if len(tape) > MAX_CELLS: + raise ValueError("finite simulator cell budget") + for position, symbol in tape.items(): + if type(position) is not int or symbol not in ALPHABET[1:]: + raise ValueError("sparse tapes contain integer positions and nonblanks") + + +def run(table: dict, tapes: list[dict], heads: list[int], command: str, + limit: int) -> tuple[str, tuple[int, int, int, int]]: + """Execute a compiled table. Return halt and steps/reads/writes/moves.""" + validate_table(table) + if command not in ("begin", "end", "push", "pop"): + raise ValueError("unknown command") + if type(limit) is not int or not 1 <= limit <= MAX_STEPS: + raise ValueError("step budget") + if len(tapes) != 2 or len(heads) != 2 or tapes[0] is tapes[1]: + raise ValueError("two distinct tapes required") + for tape in tapes: + validate_tape(tape) + if any(type(head) is not int for head in heads): + raise ValueError("integer head positions required") + state = command + writes = moves = 0 + for step in range(1, limit + 1): + p, b = (tape.get(head, "_") for tape, head in zip(tapes, heads)) + action = table[state, p, b] + for i, symbol in enumerate((action.write_p, action.write_b)): + if symbol is not None: + writes += 1 + if symbol == "_": + tapes[i].pop(heads[i], None) + else: + tapes[i][heads[i]] = symbol + heads[0] += action.move_p + heads[1] += action.move_b + moves += abs(action.move_p) + abs(action.move_b) + state = action.next_state + if state in HALTS: + return state, (step, 2 * step, writes, moves) + raise RuntimeError("step budget exhausted") diff --git a/research/reverse-record-parking/verify.py b/research/reverse-record-parking/verify.py new file mode 100644 index 0000000000..fa50b668a1 --- /dev/null +++ b/research/reverse-record-parking/verify.py @@ -0,0 +1,226 @@ +"""Exact new-controller conformance and action counts. Apache-2.0.""" + +import ast +from dataclasses import replace +import hashlib +from itertools import product +import json +from pathlib import Path + +from controller import ALPHABET, Action, compile_table, run, validate_table + +ROOT = Path(__file__).resolve().parent + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def charge(command: str, n: int = 0) -> tuple[int, int, int, int]: + if command == "begin": + return 1, 2, 1, 1 + if command == "end": + return 2, 4, 1, 1 + return 2 * n + 3, 4 * n + 6, 2 * n + 2, 3 * n + 3 + + +def dense_run(table: dict, tapes: list[dict], heads: list[int], command: str, + limit: int) -> tuple[list[dict], list[int], str, tuple]: + """A separate bounded array interpreter; shares the finite table only.""" + low = min(*heads, *(min(t, default=0) for t in tapes)) - limit - 2 + high = max(*heads, *(max(t, default=0) for t in tapes)) + limit + 2 + require(high - low < 500_000, "dense allocation budget") + arrays = [[t.get(i, "_") for i in range(low, high + 1)] for t in tapes] + cursor = [h - low for h in heads] + state, writes, moves = command, 0, 0 + for count in range(1, limit + 1): + action = table[state, arrays[0][cursor[0]], arrays[1][cursor[1]]] + for i, symbol in enumerate((action.write_p, action.write_b)): + if symbol is not None: + arrays[i][cursor[i]] = symbol + writes += 1 + cursor = [cursor[0] + action.move_p, cursor[1] + action.move_b] + moves += abs(action.move_p) + abs(action.move_b) + state = action.next_state + if state in ("done", "reject"): + output = [{i + low: v for i, v in enumerate(a) if v != "_"} + for a in arrays] + return output, [c + low for c in cursor], state, (count, 2*count, writes, moves) + raise RuntimeError("dense step budget exhausted") + + +def base_tapes(h: int = 0, a: int = 0) -> tuple[list[dict], list[int]]: + # Opaque caller data deliberately includes every symbol, except blank. + parking = {h - 12 + i: symbol for i, symbol in enumerate(ALPHABET[1:])} + port = {a - 1: "^", a - 9: "R", a - 8: "1"} + return [parking, port], [h, a] + + +def execute(table: dict, tapes: list[dict], heads: list[int], command: str, + n: int, dense: bool) -> tuple[int, int, int, int]: + limit = 2 * n + 12 + if dense: + other = dense_run(table, tapes, heads, command, limit) + status, bill = run(table, tapes, heads, command, limit) + require(status == "done", "valid command rejected") + require(bill == charge(command, n), "literal action count differs from formula") + if dense: + require((tapes, heads, status, bill) == other, "interpreter disagreement") + return bill + + +def one_packet(table: dict, bits: str, h: int = 0, a: int = 0, + dense: bool = True) -> tuple[int, int, int, int]: + tapes, heads = base_tapes(h, a) + initial = [dict(t) for t in tapes] + n = len(bits) + tapes[1].update({a + i: bit for i, bit in enumerate(bits + "$")}) + bill = list(execute(table, tapes, heads, "begin", 0, dense)) + pushed = execute(table, tapes, heads, "push", n, dense) + expected = dict(initial[0]) + expected[h] = "F" + expected[h + 1] = "R" + expected.update({h + 2 + i: bit for i, bit in enumerate(reversed(bits))}) + require(tapes == [expected, initial[1]], "wrong reversed record or consumed port") + require(heads == [h + n + 2, a], "wrong PUSH boundary heads") + popped = execute(table, tapes, heads, "pop", n, dense) + expected_port = dict(initial[1]) + expected_port.update({a + i: bit for i, bit in enumerate(bits + "$")}) + require(tapes == [initial[0] | {h: "F"}, expected_port], "POP packet/prefix mismatch") + require(heads == [h + 1, a], "wrong POP boundary heads") + ended = execute(table, tapes, heads, "end", 0, dense) + require(tapes == [initial[0], expected_port] and heads == [h, a], "END mismatch") + for item in (pushed, popped, ended): + bill = [x + y for x, y in zip(bill, item)] + require(bill == [4*n+9, 8*n+18, 4*n+6, 6*n+8], "complete pair invoice") + return tuple(bill) + + +def nested(table: dict, depth: int) -> tuple[int, int]: + tapes, heads = base_tapes(-17, 13) + initial = [dict(t) for t in tapes] + records = [] + ledger = [0, 0, 0, 0] + volume = 0 + for level in range(depth): + bills = [execute(table, tapes, heads, "begin", 0, False)] + pair = ("", ("01101" * ((level % 7) + 1))[:level % 23]) + records.append(pair) + for bits in pair: + a = heads[1] + tapes[1].update({a + i: bit for i, bit in enumerate(bits + "$")}) + bills.append(execute(table, tapes, heads, "push", len(bits), False)) + volume += len(bits) + for bill in bills: + ledger = [x + y for x, y in zip(ledger, bill)] + for pair in reversed(records): + for bits in reversed(pair): + bill = execute(table, tapes, heads, "pop", len(bits), False) + a = heads[1] + actual = "".join(tapes[1].get(a + i, "_") for i in range(len(bits) + 1)) + require(actual == bits + "$", "nested LIFO/order/extent") + for i in range(len(bits) + 1): + del tapes[1][a + i] # Caller consumes its returned packet. + ledger = [x + y for x, y in zip(ledger, bill)] + bill = execute(table, tapes, heads, "end", 0, False) + ledger = [x + y for x, y in zip(ledger, bill)] + r = 2 * depth + expected = [4*volume+6*r+3*depth, 8*volume+12*r+6*depth, + 4*volume+4*r+2*depth, 6*volume+6*r+2*depth] + require(ledger == expected, "nested aggregate invoice") + require(tapes == initial and heads == [-17, 13], "nested ancestor/port/head return") + return volume, r + + +def rejection_checks(table: dict) -> int: + count = 0 + for command, contents in (("pop", "F"), ("end", "FR"), ("end", "FR1")): + tapes, heads = base_tapes() + tapes[0].update(enumerate(contents)) + heads[0] = len(contents) + before = [dict(t) for t in tapes], list(heads) + status, bill = run(table, tapes, heads, command, 12) + require(status == "reject" and bill[2] == 0, "boundary rejection wrote data") + require((tapes, heads) == before, "boundary rejection changed heads or cells") + count += 1 + for bad in ({}, table | {("bogus", "_", "_"): Action("done")}, + table | {("begin", "_", "_"): Action("done", move_p=2)}, + table | {("begin", "_", "_"): Action("done", write_p="bad")}): + try: + validate_table(bad) + except ValueError: + count += 1 + else: + raise ValueError("invalid table accepted") + return count + + +def mutation_checks(table: dict) -> int: + mutations = (("copy", "_", "0", {"write_p": "1"}), + ("deliver", "1", "_", {"write_b": "0"}), + ("deliver", "R", "_", {"write_p": None}), + ("rewind", "_", "^", {"move_b": 0}), + ("end_check", "F", "0", {"write_p": None})) + for state, p, b, changes in mutations: + mutant = dict(table) + mutant[state, p, b] = replace(table[state, p, b], **changes) + try: + one_packet(mutant, "010", dense=False) + except (ValueError, RuntimeError): + continue + raise ValueError("semantic mutant survived") + # Deliberately demonstrate the weaker malformed-port guarantee. + tapes, heads = base_tapes() + tapes[0].update(enumerate("FR10")) + heads[0] = 4 + tapes[1][1] = "1" + before = [dict(t) for t in tapes] + status, bill = run(table, tapes, heads, "pop", 20) + require(status == "reject" and bill[2] > 0 and tapes != before, + "malformed-port scope control") + return len(mutations) + 1 + + +def syntax_checks() -> None: + for name in ("controller.py", "verify.py"): + source = (ROOT / name).read_text() + tree = ast.parse(source) + compile(source, str(ROOT / name), "exec") + for node in ast.walk(tree): + if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)): + require(node.end_lineno - node.lineno + 1 <= 60, "function over one page") + + +def main() -> None: + table = compile_table() + syntax_checks() + totals = [0, 0, 0, 0] + cases = volume = 0 + for n in range(11): + for letters in product("01", repeat=n): + bill = one_packet(table, "".join(letters)) + totals = [x + y for x, y in zip(totals, bill)] + cases += 1 + volume += n + translated = 0 + for h, a in ((-103, 37), (71, -89), (0, 0)): + for n in (0, 1, 2, 7, 64, 1024, 16384): + bits = ("0110100" * ((n + 6) // 7))[:n] + one_packet(table, bits, h, a, dense=n <= 1024) + translated += 1 + nesting = [nested(table, d) for d in (1, 2, 7, 32, 129)] + controls = rejection_checks(table) + mutation_checks(table) + require(totals[0] == 4*volume + 9*cases, "enumerated aggregate steps") + hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(ROOT.iterdir()) if p.is_file()} + receipt = {"status": "PASS_REVERSE_RECORD_PARKING", "table_entries": len(table), + "packets": cases, "payload_bits": volume, "complete_pair_bill": totals, + "translated_cases": translated, "nested_volume_records": nesting, + "controls": controls, "sha256": hashes, + "scope": "new finite controller and scoped written all-size proof; no new kappa"} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()