Reduce XOR tape travel by at least N-2 crossings (no new κ)

research/nested-xor-scratch-tapes/PROOF.md

@@ -0,0 +1,147 @@
+# Nested swaps for an in-place XOR correction
+
+The construction and proof were produced by Nick Petalas. Apache-2.0.
+The two-tape record interface, R0/L0/W templates and serial comparison
+formula are Dugongue / David Ganz's [PR #3879](https://github.com/CrocSwap/integer-mult-bounds/pull/3879).
+Those are cited premises. This package does not audit that predecessor.
+
+## Contract and theorem
+
+Let h >= 1, N = 2^h and 0 < delta < N. Write delta = m+l, where m is a
+power of two and 0 <= l < m. Let c = N/(2m). Tape zero contains
+
+```
+# w_0 # w_1 # ... # w_(N-1) #
+```
+
+with N arbitrary binary records of the same width B >= 0. Tape one
+contains one arbitrary dirty record of width B, framed by two separators.
+Both heads start at their opening separators, at arbitrary integer origins.
+All tape cells outside these windows are arbitrary and must be preserved.
+The alphabet is {0,1,#,blank}. Each transition reads both scanned symbols,
+writes at most one symbol per tape and moves each head by at most one cell.
+
+There is a finite controller that implements w'_j = w_(j xor delta),
+restores the complete scratch record and both heads, and preserves both
+exteriors. Its exact number of transitions is
+
+```
+H_nested = N*m + 2*(c-1)*(l+1)
+T_nested = (3N/2)*(2B+3) + (B+2)*H_nested.
+```
+
+Its control has 2*H_nested + 9N/2 + 1 states including halt, and
+16*H_nested + 33N/2 defined transition entries. It uses the same B+2
+scratch cells, including separators, as the predecessor. The first tape's
+visited window has N*(B+1)+1 cells. These statements hold for all h and B.
+The executable evidence has explicit expansion bounds described below.
+For delta = 0, the controller is already halted, with zero transitions.
+
+PR #3879's serial schedule has
+
+```
+H_serial = (N-2)*m + 2N-2.
+```
+
+The new schedule saves at least (N-2)*(B+2) transitions for every nonzero
+mask. The saving is strict for N >= 4. This is an exact machine invoice,
+not a wall-clock measurement or a recursive rank saving. No minimum over
+all possible tape machines or all swap orders is asserted.
+
+## Schedule and arbitrary dirty scratch
+
+List a_0 < ... < a_(q-1), q=N/2, with a_i < b_i = a_i xor delta.
+These are exactly the indices whose m bit is zero. In particular a_0=0.
+Let W(v) swap the record at address v with the scratch record and rewind
+both heads to their entry separators. It is the predecessor's three-state
+W template, costing 2B+3 transitions for arbitrary record contents.
+
+Use this visit order, with literal R0/L0 seeks between visits:
+
+```
+a_0, a_1, ..., a_(q-1),
+b_(q-1), a_(q-1), ..., b_1, a_1, b_0, a_0.
+```
+
+There are exactly 3q record swaps. There is no online stack or online
+address arithmetic. The finite compiler unrolls every seek and swap.
+
+For correctness, the subword for pair i is an opening W(a_i), followed
+by all later pairs, followed by W(b_i), W(a_i). Induct on the number of
+enclosed pairs. The enclosed subword acts only on its own disjoint data
+pairs and restores whatever scratch value it receives. Thus it returns
+the scratch value left by the opening W(a_i), even though that value is
+an arbitrary original data record rather than the original scratch dirt.
+The remaining two swaps finish the transposition of a_i,b_i and restore
+the incoming scratch value. The induction proves the desired disjoint
+transpositions, including arbitrary dirt restoration. This is the usual
+star-transposition identity applied to a nested schedule.
+
+Every data address occurs in a W, and the final visit is a_0=0. Each W
+rewinds both heads. The data head therefore returns to its origin and
+the scratch head never leaves its declared record. All seeks stay between
+valid data-record separators. The predecessor templates write no exterior
+cell. This proves the restoration, frame and visited-window statements.
+
+## Exact travel
+
+Put D_i=b_i-a_i>0 and d_i=a_(i+1)-a_i for i<q-1. The opening sweep costs
+a_(q-1). In the closing sweep every b_i to a_i leg costs D_i, the first
+closing entry costs D_(q-1), and each intervening leg costs |D_i-d_i|.
+Since a_(q-1)=sum d_i, the total is
+
+```
+H = 2*sum_i D_i + 2*sum_(i<q-1) max(0,d_i-D_i).
+```
+
+The representatives form c blocks, each containing m consecutive
+addresses. In block t they are 2mt+x, 0<=x<m, with partners
+2mt+m+(x xor l). Since XOR permutes [0,m),
+
+```
+sum_i D_i = c*m^2 = N*m/2.
+```
+
+Inside a block d_i=1 and D_i>=1, so the positive-part term is zero.
+At each of the c-1 block boundaries, the old representative is
+2mt+m-1, its partner is 2mt+2m-1-l, and the next representative is
+2mt+2m. The positive part is exactly l+1. Substitution gives the claimed
+H_nested. No monotonicity of the partner sequence was assumed.
+
+For comparison, the cited serial formula gives
+
+```
+H_serial-H_nested = 2*(N-m-1-(c-1)*(l+1))
+                 >= 2*(N-m-1-(c-1)*m)
+                  = N-2.
+```
+
+There are the same 3N/2 W macros in both constructions. Every seek crosses
+one width-B record and costs B+2. Multiplication gives the exact transition
+saving. Each seek contributes two states and sixteen transition entries;
+each W contributes three states and eleven entries. Add one halt state.
+The compiler also saves twice the crossing reduction in states and sixteen
+times that reduction in transition entries. Control is not treated as free.
+
+## Evidence and limits
+
+The written schedule is uniform for every finite h. The supplied compiler
+allows 0<=h<=9 and at most 250,000 transition entries, before allocation.
+Larger controllers are not silently approximated; expansion fails. The
+schedule and token-permutation checker covers every h<=9 and every mask,
+including controllers too large for literal expansion. The unit-step
+executor covers every mask through h=5, widths 0..3, complete one-bit
+data/scratch basis fixtures through h=3, and two h=9 machines. The complete
+RESULT records the enumerated counts. Its finite evidence corroborates the
+proof; it does not establish the universal quantifiers by enumeration.
+
+No predecessor executable is imported or replayed. Its transition templates
+are reimplemented here with attribution. The independent executor dispatches
+only literal table entries, never an address-seek or record-swap oracle.
+The executable compiler stores a bounded host-side finite table; it does
+not claim an unpriced fixed-control online interpreter for arbitrary h.
+
+Acquiring an actual native return in this record layout, buffer placement,
+representation conversions, the complete caller and its recursive invoice
+remain open. No selected framework assumption, new kappa, complete rounded
+multiplier, human review or formal proof-kernel acceptance is supplied.

research/nested-xor-scratch-tapes/README.md

@@ -0,0 +1,128 @@
+# Fewer head crossings for dirty-scratch XOR correction
+
+The construction, proof and verifier were produced by Nick Petalas.
+Apache-2.0. Claim type: scoped construction and mathematical proof, with
+exact finite machine evidence. No new kappa.
+
+Nesting the scratch swaps in Dugongue / David Ganz's
+[PR #3879](https://github.com/CrocSwap/integer-mult-bounds/pull/3879)
+reduces its in-place XOR correction cost for every nonzero mask on N>=4
+records. Both heads and the arbitrary dirty scratch record still return
+exactly. The alphabet, record representation, scratch capacity and 3N/2
+record swaps are the same.
+
+For N=2^h, delta=m+l, m the highest power of two in delta, and 0<=l<m,
+the exact record-crossing counts are
+
+```
+serial, cited from #3879: (N-2)*m + 2N-2
+nested, proved here:     N*m + 2*(N/(2m)-1)*(l+1).
+```
+
+The saving is at least N-2 record crossings, or (N-2)*(B+2) unit tape
+transitions at record width B. With N=512 and delta=16, crossings fall
+from 9,182 to 8,222, saving 960*(B+2) transitions. At B=2 the new literal
+machine executes 38,264 transitions, saving 3,840 under the cited serial
+invoice. This is an exact operation count, not a measured runtime speedup.
+
+[PROOF.md](PROOF.md) gives the unrestricted h/B theorem, dirty-state
+argument, exact travel formula and finite-control invoice.
+[machine.py](machine.py) emits the new visit order and literal four-symbol
+two-tape transition tables. [verify.py](verify.py) supplies an independent
+unit-step executor and token-permutation oracle. The star-transposition
+identity is classical; the contribution is this nested tape construction
+and its exact all-mask invoice. No global minimum is claimed.
+
+## Reproduce
+
+From the repository root, CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nested-xor-scratch-tapes/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nested-xor-scratch-tapes/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nested-xor-scratch-tapes
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nested-xor-scratch-tapes --check-source-history
+```
+
+Any CPython 3.12 path can replace the local interpreter. Expected markers
+are `PASS_NESTED_XOR_SCRATCH_TAPES`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`. Default replay writes nothing. `--emit-result`
+prints a generated receipt with SHA256 of all eight package files.
+
+[RESULT.json](RESULT.json) records 1,023 complete token schedules through
+h=9, with 1,012 strict improvements; 254 literal payload executions; 100
+complete one-bit data/scratch basis cases; 284,889 unit transitions in those
+accepted machine runs; and twelve rejecting controls. The controls cover
+wrong nesting, omitted scratch restoration, wrong mask, illegal movement
+or write, malformed framing, execution exhaustion and input/expansion bounds.
+The two h=9 literal executions have masks 1 and 16. Larger literal tables
+are not counted as executed. The old machine is not replayed: its published
+invoice is a cited comparison, and no predecessor verification is claimed.
+
+## Scope and implementation bounds
+
+This is a cheaper standalone physical permutation primitive. Native return
+layout, stream acquisition, placement, representation conversion, full
+caller integration, compiler and recursive/outer funding remain open.
+None of the selected record's five framework assumptions is discharged.
+No selected cold replay, Lean proof or complete multiplier is supplied.
+Independent human and formal proof-kernel review are unclaimed.
+
+The written schedule works for every finite h and B. Executable schedules
+are bounded to h<=9; table expansion rejects more than 250,000 entries
+before allocation. The literal executor permits at most 1,000,000 steps.
+Its fixed fixtures have B<=3 and at most 512 records. All loops have these
+finite bounds, and no runtime recursion or generated Python code is used.
+Functions are below sixty lines. Invariants use explicit exceptions and
+remain active under optimized Python.
+
+Power-of-Ten deviations are limited to Python's managed allocation and the
+twelve explicit rejection callbacks. Table entries, operations, fixture
+cells and interpreter steps have the bounds above; callbacks have only the
+twelve local targets listed in `controls`. Direct execution and the normal
+and optimized registered checks exercise these limits. A future larger
+literal replay must first revise the resource caps and evidence. Python
+warning-strict execution, AST parsing and indentation checks provide the
+available diagnostics; no static type-checker configuration is introduced.
+
+## Source and credit
+
+This takes the cost comparison in Open next question 2 of PR #3879 as a
+source, narrowing it to a faster in-place primitive before full native
+placement. Its exact record ABI, W/R0/L0 transition templates and serial
+formula retain Dugongue / David Ganz's credit. The templates are reimplemented
+with attribution; no predecessor executable is imported. Gonzalo Mier's
+PR #3480 supplies the endpoint-correction context, Cinna Davis's PR #2297
+the five-plane operator, and Sagar Thakrar's PR #3876 the scalar-contract
+boundary. Tekalign's permutation-frame compiler and the earlier native
+routing and decoder authors retain the credit recorded in #3879.
+
+The same author's merged [PR #3880](https://github.com/CrocSwap/integer-mult-bounds/pull/3880)
+provides a streamed-chunk space/time tradeoff with larger dirty buffers.
+It explicitly reports that its one-record point is slower than #3879.
+This contribution improves #3879's one-record schedule. It does not replay
+or compare the larger-buffer points of #3880.
+
+[SOURCES.json](SOURCES.json) pins the source README, proof and machine as
+provenance at canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`.
+They are not live replay dependencies. Priority revision 8 is pinned in
+[TASK.json](TASK.json). The source-binding positive control passed after
+materializing its sparse closure. Remote overlap coverage included 401
+open PR bodies and 5,645 Discussion records with complete pagination;
+working local notes were sparse. Separate searches covered merged main,
+merged PRs, this account's recent PRs and concurrent claims. These checks
+do not cover unpublished work or prove exhaustive novelty.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228649)
+states the same schedule and predicted formula. The first verified
+improvement ended construction work.
+
+## Open next questions
+
+1. Can another dirty-scratch swap order reduce head travel further at the
+   same record-swap count? Start with exact shortest paths for four or eight
+   records. A global travel lower bound is missing; this package asserts none.
+2. Which actual native return supplies this framed record bank, and does
+   the saving survive its complete placement/representation bill? Bind one
+   producer's output and charge acquisition, return and ownership. Those
+   physical interfaces remain the blocker to using the primitive in a supplier.

research/nested-xor-scratch-tapes/RESULT.json

@@ -0,0 +1,54 @@
+{
+  "status": "PASS_NESTED_XOR_SCRATCH_TAPES",
+  "schedules": {
+    "cases": 1023,
+    "strict_improvements": 1012,
+    "n512_saved_crossings_min": 510,
+    "n512_saved_crossings_max": 960
+  },
+  "payload_cases": 254,
+  "basis_cases": 100,
+  "executed_unit_transitions": 284889,
+  "rejecting_controls": 12,
+  "examples": [
+    {
+      "records": 4,
+      "mask": 2,
+      "width": 1,
+      "record_swaps": 6,
+      "record_crossings": 8,
+      "serial_record_crossings": 10,
+      "saved_record_crossings": 2,
+      "steps": 54,
+      "saved_steps": 6,
+      "states_including_halt": 35,
+      "table_entries": 194
+    },
+    {
+      "records": 512,
+      "mask": 1,
+      "width": 3,
+      "record_swaps": 768,
+      "record_crossings": 1022,
+      "serial_record_crossings": 1532,
+      "saved_record_crossings": 510,
+      "steps": 12022,
+      "saved_steps": 2550,
+      "states_including_halt": 4349,
+      "table_entries": 24800
+    },
+    {
+      "records": 512,
+      "mask": 16,
+      "width": 2,
+      "record_swaps": 768,
+      "record_crossings": 8222,
+      "serial_record_crossings": 9182,
+      "saved_record_crossings": 960,
+      "steps": 38264,
+      "saved_steps": 3840,
+      "states_including_halt": 18749,
+      "table_entries": 140000
+    }
+  ]
+}

research/nested-xor-scratch-tapes/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/xor-endpoint-tapes/README.md",
+      "usage": "provenance",
+      "git_blob": "d6dae8f5c1a489a62c35ff092d37b5758ec6f363",
+      "sha256": "1121afa87bafae0efe9f3c515d6a19fe087710b01eea3e31c140604d8052335e"
+    },
+    {
+      "path": "research/xor-endpoint-tapes/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e46aefdb54ddd5488812d8eb85e6672b39a0093f",
+      "sha256": "6d3ea54291a65655a373eb170ef86d94f5910b28e4d1f9b6dd5b03ffbf8109d0"
+    },
+    {
+      "path": "research/xor-endpoint-tapes/machine.py",
+      "usage": "provenance",
+      "git_blob": "1710effc98e45c77108030f08d60195ec05c3255",
+      "sha256": "778c5941d16a43406aceed8aa9f0c7d9682c65cf920bfa8a09a735405a2a4fd0"
+    },
+    {
+      "path": "research/dirty-buffer-xor/README.md",
+      "usage": "provenance",
+      "git_blob": "3e135b98989f58ee8ffbaf0bd203b35f8a9e5b4e",
+      "sha256": "2c0433a9f6f7be8193f7122562cd3df12f1f2c24af1714b6522f7b964c86f7c7"
+    }
+  ]
+}