From b1b8ce5622a01a8e818defc25c836a440568d707 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 11:21:20 +0000 Subject: [PATCH] perf(research): reuse bounded NTT temporary storage --- research/wordram-live-storage/PROOF.md | 116 ++++++++++++ research/wordram-live-storage/README.md | 103 +++++++++++ research/wordram-live-storage/RESULT.json | 97 ++++++++++ research/wordram-live-storage/SOURCES.json | 60 +++++++ research/wordram-live-storage/TASK.json | 123 +++++++++++++ research/wordram-live-storage/VERIFY.json | 42 +++++ research/wordram-live-storage/compact.py | 124 +++++++++++++ research/wordram-live-storage/verify.py | 200 +++++++++++++++++++++ 8 files changed, 865 insertions(+) create mode 100644 research/wordram-live-storage/PROOF.md create mode 100644 research/wordram-live-storage/README.md create mode 100644 research/wordram-live-storage/RESULT.json create mode 100644 research/wordram-live-storage/SOURCES.json create mode 100644 research/wordram-live-storage/TASK.json create mode 100644 research/wordram-live-storage/VERIFY.json create mode 100644 research/wordram-live-storage/compact.py create mode 100644 research/wordram-live-storage/verify.py diff --git a/research/wordram-live-storage/PROOF.md b/research/wordram-live-storage/PROOF.md new file mode 100644 index 0000000000..c9e36abd69 --- /dev/null +++ b/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. diff --git a/research/wordram-live-storage/README.md b/research/wordram-live-storage/README.md new file mode 100644 index 0000000000..0518498c47 --- /dev/null +++ b/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. diff --git a/research/wordram-live-storage/RESULT.json b/research/wordram-live-storage/RESULT.json new file mode 100644 index 0000000000..0eb19271ef --- /dev/null +++ b/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 + } + ] +} diff --git a/research/wordram-live-storage/SOURCES.json b/research/wordram-live-storage/SOURCES.json new file mode 100644 index 0000000000..f0440a7d1f --- /dev/null +++ b/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" + } + ] +} diff --git a/research/wordram-live-storage/TASK.json b/research/wordram-live-storage/TASK.json new file mode 100644 index 0000000000..d239939354 --- /dev/null +++ b/research/wordram-live-storage/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a smaller temporary arena for the fixed PR5466 bounded Word RAM NTT multiplier without adding runtime instructions.", + "scope_change_reason": "The explicit original-contribution assignment excludes predecessor audits. Open next question 2 of David Ganz PR5466 supplies a distinct constructive storage target outside the supplier-admission card.", + "bottleneck_link": "Side result on a complete bounded arithmetic kernel. It reduces owned runtime storage without changing the selected recursive invoice or any selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified reduction and package it. Do not optimize the cleanup suffix or search for a smaller unconstrained arena.", + "outcome": "completed", + "evidence": "PROOF.md, generated RESULT.json, compact.py and verify.py", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can redundant final zeroings be removed safely?", + "why_it_matters": "The present storage gain deliberately preserves all runtime instructions.", + "first_step": "Rewrite cleanup with branch labels preserved, then count the complete new execution.", + "blocked_by": "No label-aware deletion transformation or proof is supplied." + }, + { + "question": "Can split lifetimes or last-use operand consumption reduce the arena below 1282?", + "why_it_matters": "The certified minimum covers only whole closed lifetimes.", + "first_step": "Derive one butterfly allocation under an explicit read-before-write model.", + "blocked_by": "The present interval theorem does not cover these changed allocation rules." + } + ], + "claim_type": "Scoped program-refinement proof with a finite source-bound certificate.", + "source_question": "PR #5466, README Open next question 2", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215580", + "upstream_checkpoint": { + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at": "2026-10-27T11:10:34Z" + }, + "preserved_checkout": { + "branch": null, + "state": "detached HEAD", + "head": "de5ec2e7a6074068452f45b1a191b5c72832df4a" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "local_checks": { + "normal_seconds": 2.39, + "optimized_seconds": 2.29, + "python": "3.12.15", + "command_options": "-I -W error -B; optimized also -O", + "checks": "280 paired dirty executions, nine full static certificates and eight rejection controls" + }, + "result": "17920 logical temporary words mapped to 1282 physical words in the 512-point template, preserving every static instruction and branch path." +} diff --git a/research/wordram-live-storage/VERIFY.json b/research/wordram-live-storage/VERIFY.json new file mode 100644 index 0000000000..d3713e0495 --- /dev/null +++ b/research/wordram-live-storage/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/wordram-ntt-kernel/NOTICE.txt", + "research/wordram-ntt-kernel/PROOF.txt", + "research/wordram-ntt-kernel/README.md", + "research/wordram-ntt-kernel/ntt/exact_ntt.py", + "research/wordram-ntt-kernel/ram/PROOFS.txt", + "research/wordram-ntt-kernel/ram/wordram_kernel.py", + "research/wordram-ntt-kernel/ram_multiplier.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete address-renaming certificate, closed-interval overlap, 280 paired dirty executions and eight rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same full storage-refinement checks with Python assertions disabled." + } + ] +} diff --git a/research/wordram-live-storage/compact.py b/research/wordram-live-storage/compact.py new file mode 100644 index 0000000000..fb0d4fa5c4 --- /dev/null +++ b/research/wordram-live-storage/compact.py @@ -0,0 +1,124 @@ +"""Static temporary-cell reuse for the pinned forward Word RAM template.""" + +from bisect import bisect_left, bisect_right +from dataclasses import dataclass +from heapq import heappop, heappush + +MAX_INSTRUCTIONS = 1_000_000 +MAX_TEMPORARIES = 20_000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def operands(instruction): + """Return destination and semantically required direct-address reads.""" + op, *args = instruction + if op == "accept": + require(not args, "accept arity") + return None, () + if op == "bltz": + require(len(args) == 2, "branch arity") + return None, (args[0],) + require(op in ("one", "add", "sub", "mul"), "unsupported opcode") + require(len(args) == (1 if op == "one" else 3), "arithmetic arity") + reads = () if op == "one" else tuple(args[1:]) + if op == "sub" and args[1] == args[2]: + reads = () # This instruction is zero for every incoming word. + return args[0], reads + + +def lifetimes(program, temporaries, scratch, zero): + require(0 < len(program) <= MAX_INSTRUCTIONS, "instruction capacity") + require(0 < len(temporaries) <= MAX_TEMPORARIES, "temporary capacity") + require(0 < len(scratch) <= 64 and zero in scratch, "scratch contract") + require(not temporaries & scratch, "temporary/scratch overlap") + require(all(type(x) is int for x in temporaries | scratch), "address type") + cleanup = [("sub", x, x, x) for x in sorted(temporaries)] + cleanup += [("sub", x, x, x) for x in sorted(scratch - {zero})] + cleanup += [("accept",)] + end = len(program) - len(cleanup) + require(end > 0 and program[end:] == cleanup, "cleanup suffix") + first, last, branches = {}, {}, [] + for pc in range(end): + ins = program[pc] + require(ins and all(type(x) is int for x in ins[1:]), "operand type") + require(ins[0] != "accept", "early halt") + dst, reads = operands(ins) + for cell in reads: + if cell in temporaries: + require(cell in first, "read before initialization") + last[cell] = pc + if dst in temporaries: + first.setdefault(dst, pc) + last[dst] = pc + if ins[0] == "bltz": + target = ins[2] + require(pc < target < end, "nonforward or escaping branch") + branches.append((pc, target)) + require(first.keys() == temporaries, "unused temporary") + starts = sorted(first.values()) + for pc, target in branches: + require(bisect_left(starts, target) == bisect_right(starts, pc), + "branch skips initialization") + return end, tuple(sorted((first[x], last[x], x) for x in temporaries)) + + +def allocate(intervals, physical_cells): + active, free, mapping = [], [], {} + capacity = 0 + for start, finish, cell in intervals: + require(start <= finish, "reversed lifetime") + # At most one retirement per supplied interval, over the whole run. + for _ in range(len(active)): + if active[0][0] >= start: + break + _, slot = heappop(active) + heappush(free, slot) + if free: + slot = heappop(free) + else: + require(capacity < len(physical_cells), "physical capacity") + slot = physical_cells[capacity] + capacity += 1 + mapping[cell] = slot + heappush(active, (finish, slot)) + return mapping, capacity + + +def check_allocation(intervals, mapping, physical_cells): + require(set(mapping) == {x for _, _, x in intervals}, "mapping domain") + require(set(mapping.values()) <= set(physical_cells), "mapping range") + previous_end = {} + for start, finish, cell in intervals: + slot = mapping[cell] + require(previous_end.get(slot, -1) < start, "overlapping aliases") + previous_end[slot] = finish + + +@dataclass(frozen=True) +class CompactProgram: + program: list + mapping: dict + intervals: tuple + cleanup_start: int + capacity: int + + +def compact(program, temporaries, scratch, zero): + end, intervals = lifetimes(program, temporaries, scratch, zero) + physical = sorted(temporaries) + mapping, capacity = allocate(intervals, physical) + check_allocation(intervals, mapping, physical) + result = [] + for ins in program: + op, *args = ins + if op == "bltz": + args[0] = mapping.get(args[0], args[0]) + else: + args = [mapping.get(x, x) for x in args] + result.append((op, *args)) + require(len(result) == len(program), "instruction count changed") + return CompactProgram(result, mapping, intervals, end, capacity) diff --git a/research/wordram-live-storage/verify.py b/research/wordram-live-storage/verify.py new file mode 100644 index 0000000000..dcace61d57 --- /dev/null +++ b/research/wordram-live-storage/verify.py @@ -0,0 +1,200 @@ +"""Check the new storage refinement, without invoking predecessor verifiers.""" + +import argparse +import hashlib +import json +from pathlib import Path +import random +import sys +import types + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from compact import check_allocation, compact, operands, require + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SOURCE = "research/wordram-ntt-kernel/" + + +def load_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + captured = {} + for row in manifest["files"]: + if row["usage"] == "input": + data = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], + "source hash: " + row["path"]) + captured[row["path"]] = data + for name in ("ram", "ntt"): + module = types.ModuleType(name) + module.__path__ = [] + sys.modules[name] = module + for name, path in (("ram.wordram_kernel", "ram/wordram_kernel.py"), + ("ntt.exact_ntt", "ntt/exact_ntt.py"), + ("ram_multiplier", "ram_multiplier.py")): + module = types.ModuleType(name) + module.__file__ = str(ROOT / (SOURCE + path)) + sys.modules[name] = module + exec(compile(captured[SOURCE + path], module.__file__, "exec"), + module.__dict__) + return sys.modules["ram_multiplier"], sys.modules["ram.wordram_kernel"] + + +def peak_certificate(intervals): + """Independent closed-interval overlap count, before each instruction.""" + events = {} + for start, finish, _ in intervals: + events[start] = events.get(start, 0) + 1 + events[finish + 1] = events.get(finish + 1, 0) - 1 + live = peak = witness = 0 + for pc, delta in sorted(events.items()): + live += delta + if live > peak: + peak, witness = live, pc + require(live == 0, "unclosed interval sweep") + clique = [x for start, finish, x in intervals if start <= witness <= finish] + require(len(clique) == peak, "peak witness") + return peak, witness + + +def check_structure(plan, result, kernel): + peak, witness = peak_certificate(result.intervals) + require(result.capacity == peak, "nonminimal closed-interval allocation") + check_allocation(result.intervals, result.mapping, sorted(plan.temporaries)) + for old, new in zip(plan.program, result.program, strict=True): + require(old[0] == new[0] and len(old) == len(new), "opcode change") + positions = (1,) if old[0] == "bltz" else range(1, len(old)) + for i in positions: + require(new[i] == result.mapping.get(old[i], old[i]), "address change") + if old[0] == "bltz": + require(old[2] == new[2], "branch target change") + protected = set(plan.left + plan.right + plan.output) | kernel.SCRATCH + require(not plan.temporaries & protected, "ABI collision") + allowed = set(result.mapping.values()) | kernel.SCRATCH | set(plan.output) + for ins in result.program: + dst, _ = operands(ins) + require(dst is None or dst in allowed, "static destination outside ABI") + encoded = json.dumps(result.program, separators=(",", ":")).encode() + return {"n": plan.n, "original_temporaries": len(plan.temporaries), + "compact_temporaries": result.capacity, "peak_pc": witness, + "static_instructions": len(result.program), + "program_sha256": hashlib.sha256(encoded).hexdigest()} + + +def execute_pair(plan, result, kernel, left, right, seed): + rng = random.Random(seed) + fixed = set(plan.left + plan.right + plan.output) | kernel.SCRATCH + # Include the old abandoned cells in exterior memory of the compact ABI. + addresses = fixed | plan.temporaries | {-19, 777777} + initial = {x: rng.getrandbits(64) for x in sorted(addresses)} + initial.update(zip(plan.left, left)) + initial.update(zip(plan.right, right)) + old = kernel.run(plan.program, initial) + new = kernel.run(result.program, initial) + require(old is not None and new is not None, "execution budget") + require(old.accepted and new.accepted, "execution rejected") + require(old.steps == new.steps and old.counts == new.counts, "path or cost change") + for cell in fixed: + require(old.memory[cell] == new.memory[cell], "visible endpoint change") + owned = set(result.mapping.values()) | kernel.SCRATCH + require(all(new.memory[x] == 0 for x in owned), "dirty compact return") + allowed = owned | set(plan.output) + require(new.writes <= allowed, "write outside compact ABI") + require(all(new.memory[x] == value for x, value in initial.items() + if x not in allowed), "exterior or input change") + digits = [new.memory[x] for x in plan.output] + require(all(0 <= x < 16 for x in digits), "output digit") + def value(digits): + return sum(x << (4 * i) for i, x in enumerate(digits)) + require(value(digits) == value(left) * value(right), "integer endpoint") + return new.steps + + +def must_reject(action, message): + try: + action() + except ValueError as error: + require(str(error) == message, "wrong rejection: " + str(error)) + return + raise ValueError("missing rejection: " + message) + + +def controls(plan, result, kernel): + broken = dict(result.mapping) + peak, witness = peak_certificate(result.intervals) + clique = [x for a, b, x in result.intervals if a <= witness <= b] + require(peak >= 2, "control needs an overlap") + broken[clique[1]] = broken[clique[0]] + must_reject(lambda: check_allocation(result.intervals, broken, + sorted(plan.temporaries)), "overlapping aliases") + prefix = [("one", 100), ("add", 101, 100, 100)] + suffix = [("sub", 100, 100, 100), ("sub", 101, 101, 101), ("accept",)] + good = prefix + suffix + compact(good, {100, 101}, {10}, 10) + bad = [("add", 100, 100, 100)] + good[1:] + must_reject(lambda: compact(bad, {100, 101}, {10}, 10), + "read before initialization") + bad = [("bltz", 10, 2), ("one", 100), ("one", 101)] + suffix + must_reject(lambda: compact(bad, {100, 101}, {10}, 10), + "branch skips initialization") + bad = [("bltz", 10, 0)] + good + must_reject(lambda: compact(bad, {100, 101}, {10}, 10), + "nonforward or escaping branch") + must_reject(lambda: compact(good[:-1], {100, 101}, {10}, 10), "cleanup suffix") + bad = [("load", 100, 10)] + good[1:] + must_reject(lambda: compact(bad, {100, 101}, {10}, 10), "unsupported opcode") + must_reject(lambda: compact(good, {100, 101, 102}, {10}, 10), "cleanup suffix") + must_reject(lambda: compact(good, {10, 100}, {10}, 10), "temporary/scratch overlap") + return 8 + + +def verify(): + source, kernel = load_sources() + rows, executions = [], 0 + maximal = None + for size in (1, 2, 4, 8, 16, 32, 64, 128, 256): + plan = source.build_multiplier(size, size) + result = compact(plan.program, plan.temporaries, kernel.SCRATCH, kernel.ZERO) + row = check_structure(plan, result, kernel) + cases = [(15, 15), (0, 15), (1, 15)] + if size == 1: + cases = [(a, b) for a in range(16) for b in range(16)] + steps = [] + for a, b in cases: + left = [a] * size + right = [b] * size + steps.append(execute_pair(plan, result, kernel, left, right, executions)) + executions += 1 + row["dynamic_steps_maximal_digits"] = steps[-1] if size == 1 else steps[0] + rows.append(row) + if size == 256: + maximal = plan, result + require(maximal is not None, "missing maximal plan") + count = controls(*maximal, kernel) + require(rows[-1]["original_temporaries"] == 17920, "source template changed") + require(rows[-1]["compact_temporaries"] == 1282, "storage result changed") + return {"claim_type": "scoped program-refinement proof and finite certificate", + "templates": rows, "paired_dirty_executions": executions, + "rejection_controls": count} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + result = verify() + hashes = {} + for path in sorted(HERE.iterdir()): + if path.is_file() and path.name != "RESULT.json": + hashes[path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + result["package_sha256"] = hashes + target = HERE / "RESULT.json" + if args.write_result: + target.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(result == json.loads(target.read_text()), "receipt mismatch") + print("PASS_WORDRAM_LIVE_STORAGE " + json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()