Reduce valid matched-packet parking by V+r steps (no κ)

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.

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.

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"
+    }
+  ]
+}

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": []
+}

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."
+    }
+  ]
+}