Reduce bounded NTT temporary storage from 17,920 to 1,282 (no new κ)

research/wordram-live-storage/PROOF.md

@@ -0,0 +1,116 @@
+# Address reuse preserves the complete forward program
+
+## Hypotheses checked by the transformation
+
+Let P be a finite direct-address 64-bit Word RAM program. Its body uses only
+`one`, `add`, `sub`, `mul` and `bltz`. Every branch goes forward to a body
+instruction. A straight-line suffix zeros each logical temporary once, then
+zeros each scratch cell except the distinguished zero cell, then accepts.
+The suffix is matched byte for byte as an instruction list.
+
+For a logical temporary t, let f(t) be its first body write and l(t) its last
+body read or write. Every t has a first write. Every semantically required
+read of t follows that first write strictly. The reads of `sub d a a` are
+empty because its result is zero for every a, including arbitrary incoming
+dirt. All other arithmetic operands and branch conditions are required reads.
+No branch skips any first write: for each branch at i to j, no f(t) satisfies
+i < f(t) < j. The scanner checks these conditions before allocation.
+
+Assign each temporary t a physical cell m(t), chosen from the original
+temporary address set, disjoint from every input, output and scratch cell.
+Require m(t) != m(u) whenever the closed intervals [f(t),l(t)] and
+[f(u),l(u)] intersect. Rewrite each temporary address operand using m;
+leave every other address and every branch label unchanged. The source has
+no indirect accesses, so address renaming cannot change an address computed
+at runtime.
+
+## Simulation in the body
+
+Consider any incoming memory for the compact program. Give the original
+program the same incoming values in all non-temporary cells. Incoming logical
+temporary values can be arbitrary and need not equal their physical cells.
+The initialization condition makes those values irrelevant to required reads.
+
+All first writes execute. A forward path could skip one only by a branch
+jumping across it, which the checked condition forbids. Both programs start
+at index zero. Induct on their executed instructions. At each reached index,
+the programs agree in every non-temporary cell and in the represented value
+of every initialized temporary whose interval has not ended.
+
+A required temporary read lies in its own interval and therefore uses a cell
+distinct from every other simultaneously relevant temporary. Its physical
+value equals the original logical value. Non-temporary operands also agree.
+Thus the arithmetic result or branch condition agrees. A zeroing subtraction
+has the same result without needing equality of its two equal-address inputs.
+At the first write of a new interval, its cell can hold irrelevant previous
+dirt, but the result does not depend on that dirt. No write to its physical
+cell can destroy another relevant temporary, because their intervals would
+intersect at that index. The invariant is preserved.
+
+Consequently, both executions take the same branches and have identical
+opcodes and instruction counts through the body. The proof works modulo
+2^64 and covers the ISA's signed branch interpretation, since the condition
+word is identical. Strictly forward control bounds execution by the number
+of static instructions; no termination premise about the operands is needed.
+
+## Cleanup and exterior memory
+
+On entry to the suffix, no temporary has any remaining body use. Each mapped
+instruction `sub m(t) m(t) m(t)` sets its cell to zero. Repeated zeroings are
+harmless. Every cell in the image of m occurs at least once, so all compact
+temporaries finish zero. Scratch cleanup and outputs agree with the original
+program because their addresses have not changed and their incoming suffix
+values agree. The unchanged zero scratch cell inherits its original contract.
+
+The only compact destinations are the mapped temporary cells and original
+non-temporary destinations. In the pinned multiplier, the latter are scratch
+and output cells. Therefore the input cells and every other address retain
+their incoming values. This includes each original temporary address that is
+outside the smaller image of m. Arbitrary exterior memory and arbitrary initial
+owned dirt are allowed. The compact routine owns a smaller arena; it does not
+promise to zero the abandoned addresses of the original ABI.
+
+## Allocation size and the source-bound result
+
+Sort the intervals by start. Retire an active interval only when its end is
+strictly before the next start. Reuse a retired slot if one exists; otherwise
+allocate one new slot. This gives a valid coloring of the closed intervals.
+Whenever a new slot is needed, every earlier slot is active, so that many
+intervals overlap at the new start. Hence the number of slots equals the
+maximum overlap. Any allocation obeying these same closed-interval rules
+needs at least that many cells. A separate difference-event sweep computes
+the maximum and an index attaining it.
+
+For David Ganz's pinned balanced 256-by-256 hexadecimal-digit multiplier,
+the scanner covers all 507,701 instructions, 17,920 logical temporary
+intervals and the exact cleanup suffix. The generated allocation uses 1,282
+cells. Its overlap witness is index 140274. The compact program's canonical
+instruction encoding has SHA256
+`fcf6d3a599ff7c79d939c6c591423888eaca21cc935a810054719ee9b01ce6de`.
+Every one of these counts is regenerated from the pinned source.
+
+The simulation proves preservation for every incoming memory. Applying
+PR #5466's original bounded multiplication theorem therefore gives a
+multiplier for every admitted operand pair, with 16,638 fewer temporary
+words, the same 20 scratch words and 513 output words, and the same dynamic
+instruction count on each input. We do not re-prove the inherited NTT,
+modular arithmetic, carry or integer-recovery theorem. There is no new
+asymptotic exponent or unrestricted storage optimality conclusion.
+
+## Implementation bounds
+
+The new compiler rejects more than 1,000,000 instructions or 20,000
+temporaries. Its loops scan bounded instruction, operand, interval and event
+collections; the heap retirement loop has at most one removal per interval
+over the whole allocation. No recursion is used. Functions are below 60
+physical lines. Contracts use explicit exceptions and remain enabled under
+optimized Python. Captured predecessor source is compiled only after its
+SHA256 pins pass, without consulting bytecode caches.
+
+Managed Python allocation is a deviation from fixed-memory execution for
+the offline compiler and verifier. Their live collections are bounded by
+the instruction and temporary capacities and the nine fixed test fixtures.
+The emitted runtime program introduces no allocation instruction or indirect
+dispatch. The authenticated source loader's dynamic module construction is
+limited to three named, pinned modules. The original source's implementation
+and its proof obligations remain inherited rather than rewritten here.

research/wordram-live-storage/README.md

@@ -0,0 +1,103 @@
+# Reuse 16,638 temporary words in the bounded NTT multiplier
+
+The fixed 512-point Word RAM multiplier of David Ganz's
+[PR #5466](https://github.com/CrocSwap/integer-mult-bounds/pull/5466)
+can use **1,282 temporary words instead of 17,920**. All 507,701 static
+instructions, their opcodes and branch targets remain. Every input follows
+the same branch path and executes the same number of instructions as before.
+The maximal-digit input still takes 391,079 instructions. The 20 fixed scratch
+words and 513 output words are additional in both versions.
+
+This answers that package's Open next question 2 with a new static allocation
+and a written program-refinement proof. The reduction is exactly 16,638 words.
+The contribution is a scoped proof with a finite source-bound certificate.
+It supplies no new kappa or selected-supplier admission. The predecessor's
+bounded multiplication theorem is a cited premise, not a theorem audited here.
+
+## Construction and scope
+
+[compact.py](compact.py) computes each logical temporary's closed interval
+from its first definition to its last access before the final cleanup suffix.
+It assigns disjoint intervals to the same physical cell. Inputs, outputs and
+the fixed scratch cells keep their original addresses. The compact temporary
+arena is exactly addresses 10000 through 11281, inclusive.
+
+The transformation rejects indirect addressing, backward or escaping branches,
+uninitialized reads, branches skipping initialization, and unexpected cleanup.
+It rewrites address operands only. In particular, branch labels are program
+indices and are never renamed. All original cleanup instructions remain,
+including repeated zeroings of a reused physical cell. No load, store, setup,
+arithmetic or clearing instruction is added.
+
+[PROOF.md](PROOF.md) gives a simulation for arbitrary incoming 64-bit memory.
+Every compact temporary and fixed scratch word returns zero. Inputs and all
+memory outside the compact arena, scratch and output cells are preserved.
+Abandoned old temporary addresses are exterior memory under the compact ABI
+and can contain arbitrary dirt. The multiplication conclusion for all pairs of
+256-digit hexadecimal operands follows from the cited original theorem and
+this simulation, rather than from enumeration of all operands.
+
+At program index 140274, exactly 1,282 closed intervals overlap. This is also
+the optimal allocation size under the stated one-cell-per-logical-temporary,
+closed-interval rule. It is not an unrestricted storage lower bound. Splitting
+lifetimes, consuming an operand's last-use cell, rescheduling, recomputation
+or deleting redundant cleanup may change that model.
+
+## Evidence and reproduction
+
+[RESULT.json](RESULT.json) is generated by [verify.py](verify.py) and binds the
+package files and nine compact emitted programs by SHA256. The verifier loads
+captured, hash-authenticated source bytes; it imports no predecessor verifier.
+It checks every instruction's renaming, interval noninterference and a separate
+overlap-sweep lower certificate. It then runs 280 paired dirty-memory executions,
+including every pair of single hexadecimal digits and zero, maximal and unit
+patterns at each larger template. Output digits are compared with direct integer
+multiplication. Eight rejection controls exercise the new transformation.
+
+From the repository root, using the supplied CPython 3.12 interpreter:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/wordram-live-storage
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/wordram-live-storage/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/wordram-live-storage/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/wordram-live-storage --check-source-history
+```
+
+Expected output is `PASS_WORDRAM_LIVE_STORAGE`, followed by
+`PASS_REGISTERED_RESEARCH_PACKAGE` for the registered replay. The certificate
+includes balanced operand lengths 1, 2, 4, 8, 16, 32, 64, 128 and 256. It does
+not certify a census of every asymmetric length pair. The generic simulation
+applies to any supplied template passing the explicit structural gates.
+
+The fixed-template compiler is offline. Its Python memory and running time
+are not charged as runtime Word RAM instructions. Standard interval allocation
+and program simulation are classical. The new result is their checked storage
+refinement of this particular construction, not a new general allocation method.
+
+## Open next questions
+
+1. Can redundant final zeroings be removed while preserving branch indices
+   and the same dirty-memory contract? Start with a label-aware cleanup rewrite
+   and count every removed instruction. This package deliberately retains the
+   original suffix and makes no reduced-time claim.
+2. Can split lifetimes or last-use operand consumption reduce the 1,282-word
+   arena further? Start with one butterfly and a precise read-before-write
+   instruction model. The current closed-interval lower bound does not cover
+   either change.
+
+An asymptotic algorithm, an actual selected consumer, complete machine
+formalization, independent human review and formal proof-kernel review remain
+unclaimed. No Lean, Docker, selected cold replay or approximate FFT backend
+replay is part of this contribution.
+
+## Credit
+
+This contribution was produced by Nick Petalas. David Ganz supplied PR #5466's
+multiplier, its original correctness and cost arguments, and the explicit
+storage question. Shilun-Allan-Li and the tcslib contributors, Thomas Ahle and
+FastPoly, Bas Spitters and the CatCrypt contributors, and Brett Saiki and mpfx
+retain credit for the original interfaces, together with all predecessors in
+the unchanged [source notice](../wordram-ntt-kernel/NOTICE.txt).
+[SOURCES.json](SOURCES.json) pins the retained bytes on canonical main
+`de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8.
+Original package files and attribution remain unchanged. New work is Apache-2.0.

research/wordram-live-storage/RESULT.json

@@ -0,0 +1,97 @@
+{
+  "claim_type": "scoped program-refinement proof and finite certificate",
+  "package_sha256": {
+    "PROOF.md": "db5bf408c49a2a28b13da60f1ef81d2ced2d8aca9ebdda56182e1686e1f30aa1",
+    "README.md": "88c12e1a8b2a4399da0b5b87f609fc1d0b0e0a199f5a2b16d95640f73cba404c",
+    "SOURCES.json": "8a44ed87df58de8490ab9941aa5ed10fb03ce5e4f504d4c10f03f4dfb8ea7ca5",
+    "TASK.json": "8bc8577758ac474e6e7e092f6b6830a854b954173498e0081b10b6254f3bca06",
+    "VERIFY.json": "bcc7543130ff046c1746252c7e8f577526e029089ee7ec85039fcd0c850b1e4f",
+    "compact.py": "dabe2f4464c5731352b60206ea1aee63fd8bf020cae2d669c7aab01376f524da",
+    "verify.py": "20c53b75e77b6629a474f481a874b57b93cb7f8114e0f7abe9b1b23f522dd70f"
+  },
+  "paired_dirty_executions": 280,
+  "rejection_controls": 8,
+  "templates": [
+    {
+      "compact_temporaries": 8,
+      "dynamic_steps_maximal_digits": 319,
+      "n": 1,
+      "original_temporaries": 24,
+      "peak_pc": 243,
+      "program_sha256": "d86e088cb60ae0197a7ba717f48e8b0ae8d9b10879243eccb3dc82e4766dfa5f",
+      "static_instructions": 369
+    },
+    {
+      "compact_temporaries": 22,
+      "dynamic_steps_maximal_digits": 1243,
+      "n": 4,
+      "original_temporaries": 71,
+      "peak_pc": 1354,
+      "program_sha256": "7dde68aa01be9bf95389195af9391d6c3432ff2d8221914f621751833c6110bc",
+      "static_instructions": 1610
+    },
+    {
+      "compact_temporaries": 26,
+      "dynamic_steps_maximal_digits": 2839,
+      "n": 8,
+      "original_temporaries": 149,
+      "peak_pc": 3199,
+      "program_sha256": "6b33f8153b4c49bcd5e17716e720c3211cf8f26f5ed378b3279c3e5e208f0765",
+      "static_instructions": 3737
+    },
+    {
+      "compact_temporaries": 42,
+      "dynamic_steps_maximal_digits": 6582,
+      "n": 16,
+      "original_temporaries": 328,
+      "peak_pc": 2086,
+      "program_sha256": "c6516d806d10736680ec0ad6dedf7f9cb57cee2277e9d2157bd9dd69ed91bc6f",
+      "static_instructions": 8689
+    },
+    {
+      "compact_temporaries": 82,
+      "dynamic_steps_maximal_digits": 15252,
+      "n": 32,
+      "original_temporaries": 736,
+      "peak_pc": 5064,
+      "program_sha256": "fec482c2ea96412a6f893fabdcaab372e9664d31f6a03bca4c8ae0158f489cb9",
+      "static_instructions": 20073
+    },
+    {
+      "compact_temporaries": 162,
+      "dynamic_steps_maximal_digits": 35063,
+      "n": 64,
+      "original_temporaries": 1664,
+      "peak_pc": 11936,
+      "program_sha256": "b2363eb1d3697b626142e6ee7cf11df0f7829691ed53dbef4e290c3480601495",
+      "static_instructions": 45991
+    },
+    {
+      "compact_temporaries": 322,
+      "dynamic_steps_maximal_digits": 79413,
+      "n": 128,
+      "original_temporaries": 3712,
+      "peak_pc": 27627,
+      "program_sha256": "0e7906b140795e7c517b7107c31e49519a1ed789d5e86db1db3c06caa187df08",
+      "static_instructions": 103751
+    },
+    {
+      "compact_temporaries": 642,
+      "dynamic_steps_maximal_digits": 177058,
+      "n": 256,
+      "original_temporaries": 8192,
+      "peak_pc": 62682,
+      "program_sha256": "eacb7a120338fca47c70a58e2c7dd381154ae395d9ce2ab16b47c397bbc52dfd",
+      "static_instructions": 230701
+    },
+    {
+      "compact_temporaries": 1282,
+      "dynamic_steps_maximal_digits": 391079,
+      "n": 512,
+      "original_temporaries": 17920,
+      "peak_pc": 140274,
+      "program_sha256": "fcf6d3a599ff7c79d939c6c591423888eaca21cc935a810054719ee9b01ce6de",
+      "static_instructions": 507701
+    }
+  ]
+}

research/wordram-live-storage/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "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/wordram-ntt-kernel/NOTICE.txt",
+      "usage": "input",
+      "git_blob": "b0dc94cb9d5ed24d2ebddc2eae0f41792a2abe69",
+      "sha256": "c7a35a43ceeca4d0b820c00e5b3c589d119033748a46de91769f284e869ac33b"
+    },
+    {
+      "path": "research/wordram-ntt-kernel/PROOF.txt",
+      "usage": "input",
+      "git_blob": "d0d0d6486e833fb4711fcdd22a5aaa1853815189",
+      "sha256": "f1d6549b55337e6704b575806fb6be6cec8bbc9a761a6bf3a320aec40cbee9df"
+    },
+    {
+      "path": "research/wordram-ntt-kernel/README.md",
+      "usage": "input",
+      "git_blob": "8c24538d69695a816a19b9d2910c4cfb13e5afb1",
+      "sha256": "903f3fd84a09de855dec2a000f4eedab16037c93648d5e8d275475a66c7a9322"
+    },
+    {
+      "path": "research/wordram-ntt-kernel/ntt/exact_ntt.py",
+      "usage": "input",
+      "git_blob": "5982128975472dfeb472dbe848c5d3617076662b",
+      "sha256": "b512200d63c736c5d347247028eb1b1f3431cea44aba01c86f2772910d6b41bf"
+    },
+    {
+      "path": "research/wordram-ntt-kernel/ram/PROOFS.txt",
+      "usage": "input",
+      "git_blob": "21907aa9c4aa4c135a49ff5652bbfa08e722b757",
+      "sha256": "e62d76c0caaa4e24651d2282a7a19cb935c63e16932c90a14cb74182d3934df8"
+    },
+    {
+      "path": "research/wordram-ntt-kernel/ram/wordram_kernel.py",
+      "usage": "input",
+      "git_blob": "f5c6e00699db701f02c23c0d776f6db9d8a28854",
+      "sha256": "b1a6133e505e5faf5832a5274eea23f96b033257c3d16cc24479c4a4c7059a2e"
+    },
+    {
+      "path": "research/wordram-ntt-kernel/ram_multiplier.py",
+      "usage": "input",
+      "git_blob": "09ca74343b741af876043059d0cd0d1db8b393ed",
+      "sha256": "6c3ae23ad90c92741f5a505ae9dd85a4bbaaafb72ebdf50291e07d1ae4c52476"
+    }
+  ]
+}