Reduce packed tape read/write access from 30 to 17 instructions (no new κ)

research/packed-tape-fusion/README.md

@@ -0,0 +1,219 @@
+# Packed tape reads and writes in 17 instructions per tape
+
+This contribution is produced by Nick Petalas.
+
+A selected packed tape cell can be read and overwritten in 17 successful RAM
+instructions, including address computation. Read each of k tapes before any
+write, retain four observations per tape, and the access bill is exactly 17k.
+The separately emitted GET and SET macros in Dugongue's
+[PR #4538](https://github.com/CrocSwap/integer-mult-bounds/pull/4538) cost 13k+17k=30k.
+The new local schedule eliminates 13k instructions. This is a scoped construction
+proof with finite executable corroboration. It is neither an optimality theorem
+nor a new multiplication bound.
+
+The contribution isolates a small part of the predecessor's complete-packed-backend
+next question. Its representation and machine semantics are cited premises;
+rechecking those results is not the deliverable. The XOR bit-field identity is
+standard. The new repository result is the retained-read contract, explicit
+instruction schedule and cost reduction at a simultaneous-read boundary.
+
+## Contract
+
+Fix k>=1 tapes, c=2^ell bits per field, B=2^b fields per word, H=2^h>=2k,
+and a data base R above every control/cache register. For tape i with signed
+head z, set u=z if z>=0, otherwise u=-z-1, and tag=2i+[z<0]. Its word address
+and field offset are
+
+```
+a = R + H floor(u/B) + tag
+offset = c (u mod B)
+```
+
+Assume cB<=w, u<2^w, a<2^w, and every register, literal constant and effective
+address fits the w-bit machine. The packed data can contain arbitrary dirty
+words, including arbitrary unused high bits and arbitrary unselected fields.
+The symbol selected for writing satisfies 0<=new<2^c.
+
+The read phase keeps a, offset, the loaded word W, and the old selected field
+s=(W>>offset) AND (2^c-1) in separate registers for each tape. The intervening
+finite dispatcher may read the old symbols and compute new symbols. It must
+preserve these four caches, shared B metadata and all packed data words. Its
+registers must be disjoint from the cache registers. Its actual instructions
+are paid separately. These assumptions permit a usual finite TM dispatcher
+that reads all tapes before writing any tape.
+
+After the dispatch, commit each tape exactly once. Heads can then advance.
+The result has exactly the chosen new symbol at each selected position and
+preserves every other data bit. Cache/scratch registers are clobbered; this is
+not a reversible dirty-workspace restoration claim.
+
+## Four-instruction commit and proof
+
+The emitted commit uses register operands throughout:
+
+```
+xor    delta, old, new
+shiftl delta, delta, offset
+xor    word, word, delta
+store  address, word
+```
+
+Let M=2^c-1. Write W=L+2^offset s+2^(offset+c) U, where
+0<=L<2^offset and 0<=s<=M. The three summands occupy disjoint bit ranges.
+Since both s and new are c-bit values, delta=(s XOR new)<<offset is confined
+to the selected field. Consequently
+
+```
+W XOR ((s XOR new)<<offset)
+    = (W AND NOT(M<<offset)) OR (new<<offset).
+```
+
+This proves replacement and preservation of every other bit. It also proves
+that the shifted delta fits in w bits, so modular word writes introduce no
+additional truncation. All four instructions are successful, with no branch
+or halt instruction in this straight-line block.
+
+Different tapes cannot select the same packed word. If two addresses agree,
+H(t-t')=tag'-tag; the right side has absolute value less than H, hence t=t'
+and tag=tag'. Distinct tapes have distinct tags even when head coordinates
+and sign banks coincide. Thus each commit sees the word retained by its own
+read, and commits cannot invalidate another tape's cache. Applying the
+single-field identity to each tape proves the simultaneous-read contract.
+This argument is valid for arbitrary finite k and every word width meeting
+the stated fit conditions. Finite replay does not establish that quantifier.
+
+For a hand calculation, W=45, c=2, offset=2 has old=3. Replacing it by zero
+uses delta=12 and returns 45 XOR 12=33, preserving the other four bits.
+
+## Read schedule, cost and storage
+
+The [emitter](fusion.py) allocates a 16-register slab per tape, starting at
+r=8+16i. Shared registers 0 and 1 hold b and B-1. The slab has input index,
+tag and new-symbol slots at r,r+1,r+2. The read uses nine instructions to
+compute the address and offset, followed by four to load and extract the
+symbol. The four caches occupy r+8,r+6,r+10,r+13. The commit uses r+14 as its
+delta scratch. The dispatcher reads old symbols directly from r+13 and writes
+new symbols directly into r+2, so the schedule needs no cache-copy instructions.
+
+All reads precede all commits. The complete access count is therefore
+13k+4k=17k, against the predecessor's separately emitted 13k+17k=30k.
+This comparison concerns the stated macros and the same prepared-head ABI.
+It is an exact instruction comparison, not a hardware timing measurement or
+a globally shortest-program claim. For fixed k the new control space is
+constant in input length. The provided layout chooses R to be the smallest
+power of two at least max(128,8+16k), so the cache registers do not alias data.
+
+B initialization, ABI/head preparation, dispatcher instructions, head updates,
+input/output, allocation and full-machine halting remain separately paid.
+For example, the executable two-tape symbol-swap dispatcher uses two additional
+XOR instructions with a supplied zero register. Its complete read/dispatch/write
+fragment executes 36 instructions, rather than the 62 for the separate access
+macros with the same two-instruction dispatcher. This fixture includes actual
+dispatch instructions, rather than an uncharged host-language swap.
+
+The executable emitter intentionally supports 1<=k<=64, c<=16, B<=256 and
+10<=w<=256 with cB<=w and checked address bounds. It does not inspect or obtain
+w at machine runtime; w is a replay parameter. Extending the Python emitter's
+validation limits is distinct from the unrestricted written identity.
+
+## Evidence and reproduction
+
+[RESULT.json](RESULT.json) is generated by the verifier and bound to SHA-256
+hashes of all six proof, metadata and executable source files. It records:
+
+- 592,308 exhaustive scalar field-replacement cases at widths one through ten.
+- 6,000 emitted multi-tape fragments, executing 1,598,000 access instructions.
+- Tape counts 1,2,3,8,16,64, field widths 1,2,4,8,16, word widths
+  16,32,64,128,256, and all fitting power-of-two block sizes through 256.
+- A literal two-tape simultaneous-swap dispatcher with a 36-instruction bill.
+- Twelve invalid-input rejections and four semantic mutation controls.
+
+The fragment oracle uses direct mask-and-replace and an independent signed
+coordinate/address calculation. Every data word present in the fixture,
+including an unrelated spectator word, is compared after execution. Control
+registers begin dirty apart from the prepared ABI. Directed heads include zero,
+minus one and both sides of a block boundary. The other cases are deterministic
+random fixtures, not exhaustive claims about all such configurations.
+
+The mutation controls omit delta preparation, use the wrong shift, clobber the
+cached old symbol, and change the data word after reading. The last control
+shows why the cache-preservation premise is necessary; this construction does
+not permit intervening writes to another field in the cached word.
+
+From the repository root, with the supplied interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/packed-tape-fusion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/packed-tape-fusion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/packed-tape-fusion
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/packed-tape-fusion --check-source-history
+```
+
+On another host, substitute its CPython 3.12 path. The standard library is
+sufficient. The standalone verifier also runs in a Git-free package directory;
+Git is required for the repository metadata and publication preflight. Explicit
+`--write` regenerates the receipt. Normal verification never rewrites it, and
+all correctness checks remain active with optimized Python.
+
+## Scope, sources and code constraints
+
+The base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`, priority
+revision 7. [TASK.json](TASK.json) changes `uniform-transfer-audit` from an audit
+of #4100 to this constructive access improvement. [SOURCES.json](SOURCES.json)
+pins the originating card, selected context, predecessor packed contract,
+macro source and actual RamStd semantics as provenance. None is a runtime input;
+the new emitter/verifier is self-contained. Selected-source orientation passed
+with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. The historical baseline command in
+the old card was replaced by the current selected baseline as directed by the
+current priorities. No predecessor numerical replay is claimed.
+
+The overlap snapshot covered 395 open PRs and 3,895 discussion records, with
+complete remote pagination. Sparse local coverage omitted 6,200 tracked note
+paths. Separate all-main README searches and merged-PR searches covered the
+packed representation, retained fields, read/write fusion and four-instruction
+commit terms. No absent search hit establishes novelty by itself.
+
+Code has no recursion or dynamic evaluation. The emitted blocks have fixed
+length. The replay limits code to 2,048 instructions, k to 64 and words to 256
+bits. Functions are under 60 lines. Explicit contracts remain active under
+`-O`. Managed Python necessarily allocates during execution, a Power of Ten
+rule-3 deviation: each fragment has at most 4,096 memory entries, 2,048
+instructions and 256-bit words, and fragments are processed one at a time.
+The scalar census has explicit finite ranges and retains only a counter.
+No hard-real-time or allocation-free Python execution is claimed. A fixed-array
+backend is the next step only if that execution property is needed. Higher-level
+finite fixture data and receipt serialization are likewise bounded by the
+literal verification ranges. No third-party linter/type checker is required;
+warning-strict normal and optimized runs are registered diagnostics.
+
+A full packed TM compiler, a physical multiplication caller, Lean refinement,
+initialization and IO composition, precise whole-program constants, any RAM
+exponent improvement and a complete multiplication theorem remain unclaimed.
+The selected frontier is unchanged. Research stops at this first local saving.
+
+## Open next questions
+
+1. Install these slabs in one complete packed compiler, including its actual
+   dispatcher, signed head updates, input/output and genuine halt. Start with
+   one transition of Dugongue's unpacked compiler and preserve the four cached
+   observations through its dispatcher. The missing full emitter is the blocker;
+   a local access saving alone does not settle its complete cost.
+2. Determine whether a caller needs multiple selected fields in the same word.
+   Start by specifying all reads, the write order and a live-word versus retained
+   word policy. Cache invalidation is the blocker. The present distinct-tape
+   contract deliberately excludes that aliasing pattern.
+
+The structured versions are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution is produced by Nick Petalas. Dugongue supplies PR #4538's
+packed representation, original GET/SET macros, finite TM compiler and open
+backend question. The retained RamStd/Problem 1.8 formalization supplies the
+machine model; Szymon Torunczyk's compositional simulation and the predecessor's
+credited compiler and physical/native/precision lineage remain predecessor
+credit. PR #4541's Hopcroft, Paul and Valiant logarithmic-window simulation,
+PR #4630's native assembly and PR #4724's portfolio comparison are separate
+context, not results re-established here. All predecessor source notices are
+unchanged. New work is Apache-2.0. Independent human and formal proof-kernel
+review are unclaimed.

research/packed-tape-fusion/RESULT.json

@@ -0,0 +1,22 @@
+{
+  "access_instructions_per_tape": 17,
+  "claim_type": "scoped construction proof with finite corroboration",
+  "commit_instructions_per_tape": 4,
+  "dispatcher_fixture_instructions": 36,
+  "executed_access_instructions": 1598000,
+  "invalid_inputs_rejected": 12,
+  "predecessor_separate_access_instructions_per_tape": 30,
+  "read_instructions_per_tape": 13,
+  "scalar_identity_cases": 592308,
+  "semantic_controls_rejected": 4,
+  "source_sha256": {
+    "README.md": "ab4b1755da02dcb0306a68c5712d6b4e48725b4d501fd89f3675d49576f90a12",
+    "SOURCES.json": "ce82056d77df4b4b9c5fc91d7a9ad36e4e8f2c2ae037e0fbac8280cc53e09aac",
+    "TASK.json": "ac24e100de66e842d6045ace8c905dc7640fdc4533dc6ab84cc1d9b25d11d6bf",
+    "VERIFY.json": "33fa67606c3a30a2d62ce25eb45515b3753ec9b007be1728b7ca436ea17bf1ba",
+    "fusion.py": "01644534f02a303e6f9d2fc89e7b329880e2602f076d54984badc0b7d6e34bf7",
+    "verify.py": "595e404e98e8679a92ca0c1dafd3acd15e1c771fd8c4faa6f09407199437c743"
+  },
+  "status": "PASS_PACKED_TAPE_FUSION",
+  "transition_cases": 6000
+}

research/packed-tape-fusion/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/word-ram-transfer/README.md",
+      "usage": "provenance",
+      "git_blob": "18d6f2682f5760291a1ce5ccb989b5885ae4fc74",
+      "sha256": "4160d820310fb9bcebc359e7108146ea2e1ca9713277feaa4636e820211fabef"
+    },
+    {
+      "path": "research/word-ram-transfer/PACKED-TAPES.md",
+      "usage": "provenance",
+      "git_blob": "9137c0370ac4925907f27a1bc4e9ee1189a72fad",
+      "sha256": "27a1c874f2eae10f3f70758f6f2e5e221e505ec3d5b9fb847f7c5ca3cbe4f10c"
+    },
+    {
+      "path": "research/word-ram-transfer/packed_tape.py",
+      "usage": "provenance",
+      "git_blob": "df8b5553515e0bda6d75f4d9b2aee2f165ab3439",
+      "sha256": "5a4eca73b6043b3b6a2785fd475491a4960caa40b426a5cd0a237434cd295020"
+    },
+    {
+      "path": "research/word-ram-transfer/machine/sources/Mathproof/Meta/RamStd20261007.lean",
+      "usage": "provenance",
+      "git_blob": "4a135d0e646352e0649b3e7fced0c448f42af900",
+      "sha256": "7c9263a14360b7fe485a753bda9c35c408b768612538d092f0dff217aa4f597e"
+    }
+  ]
+}

research/packed-tape-fusion/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Construct a retained-read packed tape access fragment with 13-instruction reads and four-instruction commits, respecting simultaneous tape observations.",
+  "scope_change_reason": "The donor requests original construction rather than predecessor validation. Take the explicit packed-backend next question of Dugongue PR4538 and isolate a local access saving.",
+  "bottleneck_link": "A scoped improvement to fixed-tape execution on the bounded-word RAM route. It changes a local access constant only; no selected TM exponent or complete backend is inferred.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved local access saving; leave compiler integration and aliasing generalizations open.",
+  "outcome": "completed",
+  "evidence": "Written all-width field identity and non-aliasing proof in README.md; emitted instruction replay and generated source-bound RESULT.json.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can these retained-read slabs be installed in a complete packed finite-control TM compiler?",
+      "why_it_matters": "Only whole-program head motion, dispatch, IO and halt composition can price a complete backend.",
+      "first_step": "Adapt one transition of Dugongue PR4538's unpacked compiler and preserve address, offset, word and old symbol through its actual dispatcher.",
+      "blocked_by": "No complete packed emitter is delivered here."
+    },
+    {
+      "question": "What cache policy is required for several selected fields in one packed word?",
+      "why_it_matters": "An intervening write invalidates the retained-word premise, even when it changes another field.",
+      "first_step": "Specify the simultaneous observations and write order for a two-field single-word caller.",
+      "blocked_by": "The present distinct-tape contract excludes shared selected words."
+    }
+  ]
+}