From 3f94b96e03ea482bb3d5127463001706d44faa3e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 16:18:52 +0000 Subject: [PATCH] feat(research): bound complete root planner backing history --- research/rootplan-backing-envelope/PROOF.md | 190 ++++++++++++++++ research/rootplan-backing-envelope/README.md | 119 ++++++++++ .../rootplan-backing-envelope/SOURCES.json | 48 ++++ research/rootplan-backing-envelope/TASK.json | 100 +++++++++ .../rootplan-backing-envelope/VERIFY.json | 38 ++++ research/rootplan-backing-envelope/verify.py | 211 ++++++++++++++++++ 6 files changed, 706 insertions(+) create mode 100644 research/rootplan-backing-envelope/PROOF.md create mode 100644 research/rootplan-backing-envelope/README.md create mode 100644 research/rootplan-backing-envelope/SOURCES.json create mode 100644 research/rootplan-backing-envelope/TASK.json create mode 100644 research/rootplan-backing-envelope/VERIFY.json create mode 100644 research/rootplan-backing-envelope/verify.py diff --git a/research/rootplan-backing-envelope/PROOF.md b/research/rootplan-backing-envelope/PROOF.md new file mode 100644 index 0000000000..8292fdbc8c --- /dev/null +++ b/research/rootplan-backing-envelope/PROOF.md @@ -0,0 +1,190 @@ +# Complete encoded RootPlan backing envelope + +This result was produced by Nick Petalas. Apache-2.0. + +## Statement and boundary + +Use the unchanged `MinimumRootPlan` in Ali Romman's merged PR #5707, +`research/encoded-minimum-root-prefix/planner.py`, pinned by SOURCES.json. +Its constructor fixes `2 <= m <= 73`, `1 <= r < m`, `F > 1` and integer +guard exponent `g >= 0`. Each successful `compute` borrows canonical, +distinct Counts + +``` +(p, s, left, right, C, B, rho), +p >= 2, C >= 1, B >= 1, 0 <= s <= d, 0 <= rho < K, +d = floor(p^(997/1000)), K = floor(d^(1/500)). +``` + +The seven borrowed tapes are separate from all owned tapes. Calls obey the +source's empty-scratch entry contract. We count `len(Tape.cells)`, including +erased BLANK tails, for its 256 scratch tapes and 29 field tapes. This does +not count Python heap memory, borrowed input backing, payload execution, +tape actions, or storage elsewhere in `RootLayer`. + +For a call define + +``` +b = bitlength(p), u = bitlength(C), v = bitlength(B), +c = ceil(log2 F), h = m - 1, z = left + s*K + right, +E = 8 + max(1994*b, c*h*b, z + u + v + b + g). +``` + +For any finite history of successful calls, let `a_i` be physical tape i's +initial extent. At every instant through call j and its field cleanup, + +``` +len(cells_i) <= max(a_i, E_1, ..., E_j). +``` + +The sum of those 285 maxima bounds the complete owned backing. A cold +planner therefore needs at most `285*max_j E_j` cells throughout its history. +These are sufficient bounds, with no optimality claim for their constants. +The successful-call premise does not assert absence of pool exhaustion on +every input or provide a complete multiplier implementation. + +## Primitive extent rule + +The retained Count implementation represents an L-digit natural by LEFT at +index zero, digits at 1 through L, and RIGHT at L+1. Zero has one digit. +Copies, literal construction, increment and multiplication by a compiled +constant write only through the longest old or resulting digit interval. +Addition copies its right operand, then writes at most the longer input or +the sum's interval. `Count.product` copies both factors and scans multiplier +prefixes. Its result and temporary sums never exceed the final product when +both factors are positive. A zero factor still requires its input copy. + +`encoded.divide` copies the divisor and keeps quotient and remainder. Each +pre-subtraction remainder is less than twice the divisor; quotient prefixes +are bounded by the final quotient. `subtract` copies its left operand. +Normalization and division may leave erased high digits, but never extend +past an already bounded old interval. Counter copies and decrements do not +increase the copied digit interval. `copy_symbols` writes the complete +Count including RIGHT. Clear writes through an existing dense body only. +Add two cells to a digit bound for the markers. + +These rules follow directly from the retained `cardinal_counts`, `counts`, +`cardinality`, `encoded`, `compact_counts`, `stream`, `machine` and `records` +implementations. Their exact transitive bytes are retained in PR5707's +source archive. The new step is applying these rules to the complete caller, +including expressions outside the standalone callee of JoyboyBrian's PR #6098. + +## Parameter calculations + +The largest uncapped power target is `p^997`, used by `floor_power` and +`atom_width`. Exponentiation by squaring constructs powers with exponents +no larger than the requested fixed exponent. Saturated powers return their +cap when a nonzero operand is already at least the cap. Otherwise they +first form the full product of two operands smaller than the cap. Thus +saturation does not justify charging only the cap's length. + +Every target and cap is at most `p^997+1 < 2^(997*b)+1`. Every such full +product has fewer than `1994*b+2` binary digits. Input copies, bisection +sums, `cap=target+1` and the smaller root computations fit this same bound. +The marker allowance in E exceeds the resulting `1994*b+4` extent bound. + +The other parameter fields obey + +``` +1 <= d <= p, 1 <= K <= p, +G = 4 ceil(log2 p)+6 <= 4*b+6 < 2^(b+3), +H = d*G < 2^(2*b+3), delta = d*2^g < 2^(b+g). +``` + +Hence `qF=ceil(2H/K) <= 2H`, `qB <= H`, and their sum, products by K, +and addition of `q0 <= p` use fewer than `2*b+6` digits. The products +`qF*K < 2H+K` and `qB*K < H+K` are bounded before their subtractions. +`input_bits=p+2` and `work_bits=p+2*delta+3` use at most `b+g+3` +digits. Intermediate additions are nonnegative prefixes of those sums. +The fixed literals through m have at most seven digits. All these lengths +fit E after markers. + +## Complete minimum-prefix call + +This part uses the standalone envelope proved in JoyboyBrian's PR #6098 as +a cited input. Its proof gives, for `M=remaining <= p` and spacing `K<=p`, +at most + +``` +2 + max(7, bitlength(M)+bitlength(K)+1, + c*h*bitlength(M)+2) +``` + +cells for every newly reached scratch extent. This is at most E. Other +caller leases remain live during that call, but cannot be acquired again +until closed. Their values are covered by the other rows of this proof. +The callee's free slots are still physical members of the same 256-tape +pool. No standalone aggregate or 14-live-lease bound is substituted for +historical backing of the caller. + +The returned `q0` is at most M-1, every profile depth is at most h*b, and +`stock=F^depth <= 2^(c*h*b)`. These are the cited callee contract. The direct +branch returns constants zero and one instead. + +## Address and row expressions + +Put `a=s*K` and `t=q0*K`. Both are nonnegative, and on the fast branch +`t <= a`, since `q0 < M <= s`. The remaining complete expression ledger is + +| Expression | Digit bound or nonnegative magnitude bound | +| --- | --- | +| `active_bits=s*K`, its input copies | a; numeric digit length <= z+1 | +| `left+active_bits+right` | z; its digit length <= z+1 | +| `addresses=2^z` and its Counter | z+1 digits; the counter is no longer | +| `gaussians=addresses*C*B` | at most z+u+v+1 digits, including both partial products | +| `core_width=s-Q0` | at most p | +| `core_front=qF*K-2H` | less than K | +| `core_back=qB*K-H+right` | less than K+right | +| `row_axes=t`, `original_rows=2^t` | t<=a; at most a+1 digits for the power | +| `prefixes=B*2^left` | at most left+v+1 digits | +| `ceil(original_rows/stock)` | quotient <= original_rows; temporary remainder < 2*stock | +| `padded_rows=ceil(original_rows/stock)*stock` | less than original_rows+stock, hence at most max(a,c*h*b)+2 digits | +| `rectangle=active_bits-row_axes+right` | between zero and a+right, hence at most z | +| `row_gaussians=2^rectangle*C` | at most z+u+1 digits | +| `row_bits=2*row_gaussians*work_bits` | at most z+u+b+g+4 digits, including the partial product | + +The padded-row estimate uses only division arithmetic. It does not need +strict factor-two feasibility or a replay of the predecessor's padding +theorem. Product prefixes are bounded by the final value. Input copies, +sums, subtractions, counters and saved field copies all occur in this +ledger or the preceding parameter/callee ledgers. Borrowed left and right +have digit lengths at most z+1, since each is at most z. C and B have u and +v digits. Every row plus its two markers fits E. The direct branch replaces +the fast-only fields by zero or one, while still constructing addresses +and gaussians; it therefore fits as well. + +## History and consequences + +`Tape.write` extends a tape exactly to `head+1` when necessary. Nothing +reached here truncates `cells`. Thus each tape's extent is exactly the +maximum of its initial extent and every write index plus one so far. The +ledgers show that computation cannot extend it beyond E. Cleanup can write +through an older larger body, already in the prior maximum, and cannot +extend it. Induction over writes and calls proves the history theorem, +even with arbitrary finite initially erased tails. + +For the production law, `a=s*K <= d*K`. Since `K^500 <= d` and +`d^1000 <= p^997`, + +``` +a^500000 <= p^499497. +``` + +For fixed construction constants the cold bound is therefore +`O(left+right+p^(499497/500000)+bitlength(p)+u+v)` cells. In particular it is +`O(p+left+right+u+v)`. + +A bound linear only in encoded input digit lengths is impossible with +unrestricted side widths. Fix p=2, s=right=0 and C=B=1. For every integer +N>=0 set left=N. This direct-branch family has saved `gaussians=2^N`, with +exactly N+3 cells through RIGHT in its cold field. Borrowed left has only +max(1,bitlength(N)) digits. Conditional on successful execution, this lower +bound follows directly from the saved output. The usual Count primitives +terminate and this direct branch uses a fixed number of leases, so this +family also supplies actual successful calls. This explains why the complete +planner cannot inherit the callee's logarithmic bound without a caller +restriction on numeric side widths. + +The proof concerns numerical backing of successful planner calls. The +enclosing root, its payload, precision accuracy, movement costs, arbitrary +exceptional exits and the five framework assumptions remain outside scope. diff --git a/research/rootplan-backing-envelope/README.md b/research/rootplan-backing-envelope/README.md new file mode 100644 index 0000000000..13522d4494 --- /dev/null +++ b/research/rootplan-backing-envelope/README.md @@ -0,0 +1,119 @@ +# Complete encoded RootPlan backing bound + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped written proof with finite source-bound corroboration. The complete +unchanged PR5707 `MinimumRootPlan.compute`, including its 256 scratch tapes +and 29 retained field tapes, has a history-aware numerical backing envelope. +This answers the caller-transfer question in JoyboyBrian's +[PR #6098](https://github.com/CrocSwap/integer-mult-bounds/pull/6098). + +For successful calls with precision p, selected width s, spacing K, +side widths left and right, coefficient count C, outer rows B, and fixed +construction constants m, F, g, define + +``` +b=bitlength(p), u=bitlength(C), v=bitlength(B), +c=ceil(log2 F), h=m-1, z=left+s*K+right, +E=8+max(1994*b, c*h*b, z+u+v+b+g). +``` + +Physical tape i has extent at most `max(initial_i,E_1,...,E_j)` through +call j and cleanup. The total is the sum over all 285 tapes. A cold planner +therefore has the sufficient bound `285*max_j E_j`. The full domain and +complete expression ledger are in [PROOF.md](PROOF.md). + +For the production parameter law, `(s*K)^500000 <= p^499497`. With fixed +construction constants the cold bound is +`O(left+right+p^(499497/500000)+bitlength(p)+u+v)`. +The numeric side widths cannot simply be replaced by their bit lengths: +the direct p=2, s=right=0, C=B=1 family stores `gaussians=2^left`, requiring +left+3 cells through RIGHT. + +## What is new and what is assumed + +JoyboyBrian's PR6098 bounds the standalone minimum-prefix callee on a +32-tape pool and explicitly excludes the enclosing planner. We cite that +mathematical envelope as an input, without auditing or rerunning that +package. The new step accounts for all other live caller expressions, +parameter arithmetic, large saved powers, both caller branches, all 285 +physical histories and erased warm tails. Saturated multiplication is +charged for its uncropped intermediate, before applying the cap. + +Ali Romman supplied PR5707's complete encoded planner and PR5688's minimum +prefix theorem. Jose Manuel supplied the physical RootPlan and Count cohort +in PR3385. The retained sources preserve their complete predecessor notices, +including commdata2338's reached-depth result and the address/geometry lineage. +The per-tape high-water identity is elementary and is also used by PR6098. +The contribution is the complete caller envelope and its explicit dependence, +with no priority claim for that general identity. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/rootplan-backing-envelope/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/rootplan-backing-envelope/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rootplan-backing-envelope +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rootplan-backing-envelope --check-source-history +``` + +Set TMPDIR to a scratch directory to choose where the unchanged source +loaders extract their temporary trees. The verifier removes those trees on +exit and writes its hash-bound receipt to stdout. It changes no source file. +The marker is `PASS_ROOTPLAN_BACKING_ENVELOPE`. + +The checker runs seven complete planner calls and observes every owned +write, checking the exact high-water identity and the new envelope. One +call uses the production parameter law at p=2. Six use the predecessor's +explicit reduced tuple `(d,K,G,H,delta)=(8,1,1,1,32)` to reach both branches, +in cold and reused warm histories. These fast fixtures exercise the caller +body; they are not production-law fast cases. All seven borrowed inputs, +all 29 canonical fields, pool closure and owned cleanup are checked. + +Further controls check 256 parameter substitutions, seven address-power +lower-bound fixtures, rejection of digit-only side-width accounting, and +failure of a fresh-history bound on preexisting erased backing. The finite +checks corroborate the proof. They do not quantify over all inputs. + +## Limits + +The sufficient constants are conservative. The theorem concerns successful +planner calls with the stated ownership contract. It does not prove pool +sufficiency on every input, exceptional-exit cleanup, Python heap bounds, +RootLayer payload storage, movement/time costs, numerical accuracy, any +selected framework assumption in full, or a new kappa. The standalone callee +theorem is a cited mathematical premise. Independent human and proof-kernel +review are unclaimed. No predecessor scientific suite or full selected +supplier replay is required for this scoped addition. + +## Open next questions + +The structured questions are also in [TASK.json](TASK.json). + +- Bind actual root caller restrictions on left, right, C and B to this + envelope. Start with one descriptor producer and include retained backing + outside the planner. The remaining RootLayer storage ledger is a blocker. +- Replace the conservative 1994*b parameter term by a sharper source-bound + bound, or change the capped multiply implementation to avoid full temporary + products. First identify its maximum reached product. A replacement needs + its own physical cost and ownership proof. + +## Verification design decisions + +The write observer delegates to actual complete source execution. Source +binding, caller execution and publication checks are separate. Functions are +under 60 lines. Fixture sets, the 285-slot state and five source-tree owners +are fixed and bounded. + +Power of Ten deviations, rules 3 and 9: Python and the inherited interpreter +allocate dynamically, and observation requires replacing one Tape.write call +with a wrapper. Scope is this bounded checker only. The wrapper has one +original target, delegates each write exactly once, checks the resulting +physical extent, and is restored in finally. Fixed fixture sets bound live +observer state; the finite parameter/word sizes bound the source run. Warning- +strict normal and optimized replays verify this path. The five source loaders +are explicitly cleaned up in finally. The proof does not infer a Python heap +bound from numerical tape extents. A future runtime port must replace these +managed allocations and callback with its own bounded observation mechanism. diff --git a/research/rootplan-backing-envelope/SOURCES.json b/research/rootplan-backing-envelope/SOURCES.json new file mode 100644 index 0000000000..ae5ca5ff7a --- /dev/null +++ b/research/rootplan-backing-envelope/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/encoded-minimum-root-prefix/SOURCE-INDEX.json", + "usage": "input", + "git_blob": "c899b4bda006b247a909751f8e9c51190c111032", + "sha256": "a82d9be25cc5457a0dea248d51558da5b5b68fbde0c342238bc500fab50da4ef" + }, + { + "path": "research/encoded-minimum-root-prefix/SOURCES.json", + "usage": "input", + "git_blob": "edcab2a10cecf01396076b8947017a7f1ae25e46", + "sha256": "acc4f3e5d165b4ba62627fe4465c94dc748109424009b058e7b15bd9dbbd0391" + }, + { + "path": "research/encoded-minimum-root-prefix/planner.py", + "usage": "input", + "git_blob": "7a94b98a8fe4dc6b34c749527a43866ab49b155e", + "sha256": "8a65edc901f95fc24082eea6503309fedef8eb2a0d66701d0daf9dd0e136383f" + }, + { + "path": "research/encoded-minimum-root-prefix/retained.py", + "usage": "input", + "git_blob": "8149c0dbea1b09ccc4a93bccbe318e9cbc2ac5d4", + "sha256": "35f0070900a82164bcb3e570c155d95d0a84d54a62252e33d74dc4848176347c" + }, + { + "path": "research/encoded-minimum-root-prefix/source-snapshot.tar", + "usage": "input", + "git_blob": "991cfca61a091e10168b1647e1ae55c644cdcd85", + "sha256": "3e901efd15eafce0d9b1f11d452a294229e08b0cc06ddb6fc0bef8157dc3c08f" + } + ] +} diff --git a/research/rootplan-backing-envelope/TASK.json b/research/rootplan-backing-envelope/TASK.json new file mode 100644 index 0000000000..5cb851b8f2 --- /dev/null +++ b/research/rootplan-backing-envelope/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "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_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 assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "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": "Explicit numerical backing envelope for the complete unchanged PR5707 MinimumRootPlan.compute, its 256 scratch tapes and 29 fields, through finite successful histories.", + "scope_change_reason": "A scoped caller-level precision_tape lemma, answering PR6098 open next question 1, rather than discharging the complete selected assumption.", + "bottleneck_link": "The numerical setup planner must have a complete historical storage bill before its root caller can be charged. This closes a storage sub-obligation, with no supplier admission or kappa change.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified complete caller envelope; leave tighter constants and surrounding RootLayer storage to follow-up work.", + "outcome": "completed", + "evidence": "PROOF.md and the source-bound verify.py, registered in VERIFY.json", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What complete enclosing RootLayer backing bound follows after binding its actual side-width, coefficient and row producers?", + "why_it_matters": "The planner envelope alone is not a complete physical root storage bill.", + "first_step": "Pin one actual descriptor producer and substitute its bounds for left, right, C and B, while adding all nonplanner retained tapes.", + "blocked_by": "The surrounding payload and historical tape ledger." + }, + { + "question": "Can the 1994*b parameter term be reduced by a sharper reached-product bound or an implementation that avoids uncropped saturated products?", + "why_it_matters": "The current sufficient constant includes a full cap-squared intermediate.", + "first_step": "Identify the largest reached capped product in floor_power and atom_width before choosing a replacement arithmetic contract.", + "blocked_by": "A source-bound physical multiplication and ownership argument for any changed implementation." + } + ], + "source_question": { + "pr": 6098, + "author": "JoyboyBrian", + "question": 1 + }, + "upstream_checkpoint": { + "commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "checked_utc": "2026-10-28T16:04:00Z", + "selected_kappa": "781451/250000000" + } +} diff --git a/research/rootplan-backing-envelope/VERIFY.json b/research/rootplan-backing-envelope/VERIFY.json new file mode 100644 index 0000000000..1a38a8e47c --- /dev/null +++ b/research/rootplan-backing-envelope/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/encoded-minimum-root-prefix/SOURCE-INDEX.json", + "research/encoded-minimum-root-prefix/SOURCES.json", + "research/encoded-minimum-root-prefix/planner.py", + "research/encoded-minimum-root-prefix/retained.py", + "research/encoded-minimum-root-prefix/source-snapshot.tar" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Seven complete caller executions, every owned write and per-tape history, borrowed preservation, 29 canonical fields, both branches, warm backing, parameter and address controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Seven complete caller executions, every owned write and per-tape history, borrowed preservation, 29 canonical fields, both branches, warm backing, parameter and address controls." + } + ] +} diff --git a/research/rootplan-backing-envelope/verify.py b/research/rootplan-backing-envelope/verify.py new file mode 100644 index 0000000000..48b2ba4a39 --- /dev/null +++ b/research/rootplan-backing-envelope/verify.py @@ -0,0 +1,211 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Observe the complete unchanged RootPlan, including retained erased cells.""" +import hashlib +import json +from pathlib import Path +import sys +import tempfile +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/encoded-minimum-root-prefix" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def authenticate(): + rows = json.loads((HERE / "SOURCES.json").read_text())["files"] + live = tuple(row for row in rows if row["usage"] == "input") + need(len(live) == 5, "complete five-file source closure") + for row in live: + raw = (ROOT / row["path"]).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], row["path"]) + return len(live) + + +def envelope(values, dimension, divisor, guard, spacing): + p, selected, left, right, coefficients, rows, _ = values + b, u, v = p.bit_length(), coefficients.bit_length(), rows.bit_length() + c, h = (divisor - 1).bit_length(), dimension - 1 + z = left + selected * spacing + right + return 8 + max(1994 * b, c * h * b, z + u + v + b + guard) + + +def decode(count): + from words import RIGHT + physical = getattr(count.tape, "physical", count.tape) + raw = physical.cells + end = raw.index(RIGHT, 1) + need(end >= 2 and all(bit in (0, 1) for bit in raw[1:end]), "canonical Count") + return sum(bit << i for i, bit in enumerate(raw[1:end])) + + +def snapshot(counts): + return tuple((bytes(count.tape.cells), count.tape.head) for count in counts) + + +class Observation: + def __init__(self, tapes): + need(len(tapes) == 285 and len({id(t) for t in tapes}) == 285, + "256 scratch tapes and 29 distinct fields") + self.tapes = tapes + self.slots = {id(tape): i for i, tape in enumerate(tapes)} + self.initial = [len(tape.cells) for tape in tapes] + self.exact = self.initial[:] + self.bound = self.initial[:] + self.writes = 0 + self.active = False + + def begin(self, capacity): + self.bound = [max(old, capacity) for old in self.bound] + self.active = True + + def write(self, original, tape, symbol): + if not self.active: + return original(tape, symbol) + need(id(tape) in self.slots, "no unaccounted numerical tape writes") + original(tape, symbol) + i = self.slots[id(tape)] + self.exact[i] = max(self.exact[i], tape.head + 1) + self.writes += 1 + need(len(tape.cells) == self.exact[i], "exact per-tape high-water identity") + need(len(tape.cells) <= self.bound[i], "complete caller extent envelope") + + def finish(self): + self.active = False + need([len(tape.cells) for tape in self.tapes] == self.exact, + "physical identities hold after the complete call and clear") + + +def warm(tapes): + from words import BLANK, LEFT + # Prepare erased backing before observation. No execution is changed. + for i in (0, 255, 256, 284): + tape = tapes[i] + for _ in range(9001 + i): + tape.append(0) + tape.clear() + need(tape.cells[0] == LEFT and all(v == BLANK for v in tape.cells[1:]), + "warm backing is entirely erased") + + +def execute(plan, values, spacing, observer): + from cardinal_counts import Count + from words import BLANK + counts = tuple(Count.literal(value) for value in values) + before = snapshot(counts) + capacity = envelope(values, plan.dimension, plan.level_divisor, + plan.guard_exponent, spacing) + observer.begin(capacity) + try: + result = plan.compute(*counts) + need(result is plan and plan.closed and not plan.pool.live, "successful whole planner") + need(snapshot(counts) == before, "all seven borrowed inputs preserved") + need(decode(plan.count("K")) == spacing, "declared spacing is actual output K") + need(all(decode(plan.count(name)) >= 0 for name in plan.roles), "all 29 fields canonical") + record = {"capacity": capacity, "fast": plan.fast, + "max_extent": max(len(t.cells) for t in observer.tapes), + "retained_total": sum(len(t.cells) for t in observer.tapes)} + plan.clear() + need(all(tape.read() == BLANK for tape in observer.tapes), "all owned bodies cleared") + observer.finish() + finally: + observer.active = False + for count in counts: + count.close() + return record + + +def history(reduced, warmed): + import planner + from cardinal_counts import Count + from records import Tape + + class Reduced(planner.MinimumRootPlan): + def parameters(self, precision): + return tuple(Count.literal(value) for value in (8, 1, 1, 1, 32)) + + cls = Reduced if reduced else planner.MinimumRootPlan + plan = cls(2, 1, 6, guard_exponent=2) + tapes = (*plan.pool.tapes, *plan.roles.values()) + if warmed: + warm(tapes) + observer = Observation(tapes) + original = Tape.write + cases = ((9, 8, 0, 0, 1, 1, 0), (9, 8, 7, 3, 13, 5, 0), + (9, 0, 0, 0, 1, 1, 0)) if reduced else ((2, 0, 1, 0, 3, 5, 0),) + records = [] + try: + Tape.write = lambda tape, symbol: observer.write(original, tape, symbol) + for values in cases: + records.append(execute(plan, values, 1, observer)) + finally: + observer.active = False + Tape.write = original + if warmed: + need(records[-1]["max_extent"] > records[-1]["capacity"], + "reject forgetting preexisting erased backing") + if reduced: + need([record["fast"] for record in records] == [True, True, False], + "complete fast and direct branches exercised") + return {"reduced_parameters": reduced, "warm": warmed, "calls": records, + "writes": observer.writes, "peak_leases": plan.pool.peak} + + +def symbolic_controls(): + checks = 0 + for p in range(2, 66): + b = p.bit_length() + need(4 * b + 6 < 2 ** (b + 3), "parameter logarithm envelope") + need((p ** 997 + 1) ** 2 < 2 ** (1994 * b + 2), "uncropped cap product") + for g in (0, 2, 17, 210000): + need((p + 2 * p * (1 << g) + 3).bit_length() <= b + g + 3, + "work precision envelope") + checks += 1 + lower_bounds = 0 + for left in (0, 1, 2, 7, 31, 4096, 65536): + count = 1 << left + need(count.bit_length() + 2 == left + 3, "necessary address-power field extent") + if left >= 4096: + values = (2, 0, left, 0, 1, 1, 0) + wrong = envelope((2, 0, left.bit_length(), 0, 1, 1, 0), 2, 6, 2, 1) + need(count.bit_length() + 2 > wrong, "reject digit-only side-width accounting") + need(count.bit_length() + 2 <= envelope(values, 2, 6, 2, 1), "numeric address bound") + lower_bounds += 1 + return {"parameter_checks": checks, "address_lower_bound_fixtures": lower_bounds} + + +def cleanup_sources(): + # These five authenticated loaders own all extracted source trees. + for name in ("source", "native_sources", "phase_sources", "leaf_sources", "retained"): + module = sys.modules.get(name) + temporary = getattr(module, "_temporary", None) + need(isinstance(temporary, tempfile.TemporaryDirectory), "known source-tree owner") + temporary.cleanup() + + +def main(): + started = time.monotonic() + inputs = authenticate() + sys.path.insert(0, str(SOURCE)) + controls = symbolic_controls() + try: + histories = [history(False, False), history(True, False), history(True, True)] + finally: + cleanup_sources() + need(sum(len(row["calls"]) for row in histories) == 7, "seven complete planner calls") + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + files = tuple(HERE / name for name in names) + receipt = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() for path in files} + print(json.dumps({"status": "PASS_ROOTPLAN_BACKING_ENVELOPE", "source_inputs": inputs, + "controls": controls, "histories": histories, "sha256": receipt, + "elapsed_seconds": round(time.monotonic() - started, 3)}, indent=2)) + + +if __name__ == "__main__": + main()