From 38d986ac7c12a676a4e0cf79b8ab00e1283af604 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 22:05:07 +0000 Subject: [PATCH 1/2] feat(research): compress continuation head distances in binary --- .../binary-distance-continuations/PROOF.md | 202 +++++++++++++++ .../binary-distance-continuations/README.md | 124 ++++++++++ .../binary-distance-continuations/RESULT.json | 23 ++ .../SOURCES.json | 36 +++ .../binary-distance-continuations/TASK.json | 83 +++++++ .../binary-distance-continuations/VERIFY.json | 38 +++ .../binary_stack.py | 154 ++++++++++++ .../binary-distance-continuations/verify.py | 233 ++++++++++++++++++ 8 files changed, 893 insertions(+) create mode 100644 research/binary-distance-continuations/PROOF.md create mode 100644 research/binary-distance-continuations/README.md create mode 100644 research/binary-distance-continuations/RESULT.json create mode 100644 research/binary-distance-continuations/SOURCES.json create mode 100644 research/binary-distance-continuations/TASK.json create mode 100644 research/binary-distance-continuations/VERIFY.json create mode 100644 research/binary-distance-continuations/binary_stack.py create mode 100644 research/binary-distance-continuations/verify.py diff --git a/research/binary-distance-continuations/PROOF.md b/research/binary-distance-continuations/PROOF.md new file mode 100644 index 0000000000..61df1236a5 --- /dev/null +++ b/research/binary-distance-continuations/PROOF.md @@ -0,0 +1,202 @@ +# Binary head-distance continuation frames + +New construction and proof produced by Nick Petalas. Apache-2.0. + +## Statement and exact contract + +Use Mihir Srivastava's PR #5364 local segment contract, retained at +`fd74da128f0e5ab702a8fe7b2b00e1a316bb22ad`. There are sixteen disjoint payload +tapes, a control tape, a descriptor tape and reverse scratch. The same nine +symbols suffice. Each parent payload is an arbitrary contiguous binary word +of length s_i after its local marker, with head at h_i in [0,s_i]. Let +H_i=s_i-h_i, H=sum H_i, L=sum bitlength(H_i) and P=sum popcount(H_i), with +bitlength(0)=0. A fixed sixteen-bit mask records presence. Absent roles are +empty, but a present role may be empty. The opaque binary descriptor has +length d and starts at its local beginning. Control is at its blank top; +scratch is blank at its local beginning. Ancestor prefixes are arbitrary and +inaccessible. Markers and tape identities are supplied entry conditions. + +The new push/pop construction has exactly the predecessor's restoration +postcondition, for every finite properly nested successful call tree. Its +control frame has exactly + + d + 35 + L + +symbols, instead of the predecessor's d+35+H. Scratch needs at most +max(d, max_i bitlength(H_i)) working symbols across a matched boundary. +Scratch is empty at every child entry and parent return. During nested +execution the same physical scratch tape is reused, so its historical extent +is the maximum over frames, not a sum over active frames. Parent payload +extents and their historical backing are unchanged by this result. +The scratch interval includes its marker and the terminal blank in addition +to the stated number of working symbols, so it has at most that maximum +plus two cells. Erasure does not deallocate any visited cell. + +Let the seventeen child words, including its descriptor, have lengths t_j +and return head offsets g_j in [0,t_j]. Put W=sum t_j and G=sum g_j. Counting +each read, write and unit move separately, the complete matched boundary is +exactly + + 22d + 24H - 10P + 22L + 613 + 2G + 5W. (1) + +It is therefore at most + + 22d + 46H + 613 + 7W. (2) + +The action bound includes all child and scratch erasure. Child computation, +descriptor production and designated output delivery have separate costs. +Intended output must be delivered before destructive pop, as in #5364. +There is a larger linear action constant in exchange for smaller headers. +This is a local constructive refinement, not a new whole-caller allocation, +binary compilation, supplier admission, exponent saving or multiplication +theorem. No global tape-reserve improvement follows without rebinding the +actual caller and accounting for all payload and historical extents. + +## Binary counter with finite control + +The counter is little endian on reverse scratch, immediately after its local +marker. It starts as an empty word representing zero. For each physical step +right while parking a payload head, increment it by changing the initial run +of ones to zeros and the next zero or blank to one, then rewind to the local +marker and step right. This stores the number of actual head movements; +no numeric payload offset, length or saved pointer is controller state. + +If an increment crosses t trailing ones, its cost is 3t for their +read/write/move actions, two actions for the final read/write, and 2t+3 +for rewind. Thus it costs 5t+5. Among the first h increments from zero, +the sum of trailing-one counts is + + sum_{a>=1} floor(h/2^a) = h-popcount(h). + +The sum counts each carry across each bit position exactly once. Hence the +complete increment cost is 10h-5popcount(h). The counter never exceeds +bitlength(h) cells. + +After parking, scan the counter to its terminal blank, then read it +backward. Emit each bit to control, most significant first, encoding zero +as `u` and one as `:`. Erase each counter bit as it is read, and return to +its local beginning. For ell counter bits, the forward scan costs 2ell+1, +the backward transfers cost 6ell, and the final marker return costs three. +The exact transfer cost is 8ell+4, including the empty counter. + +The frame grammar is + + [ descriptor : b_0 B(H_0) ; ... b_15 B(H_15) ; ] + +where B is the indicated most-significant-first encoding and B(0) is empty. +Positive encodings start with `:`. Presence flags use 0/1, disjoint from +count digits. Although `:` also terminates the descriptor, parsing is +unambiguous: fixed role order and each presence bit separate the contexts. +All thirty-five fixed symbols of the earlier grammar remain; H unary +symbols become L binary symbols. This proves the frame-length formula. + +At pop, consume each role's count backward into scratch. The resulting +word is little endian and has the original fixed width ell. Consuming the +ell count digits costs 6ell, the next presence bit costs three, and rewind +costs 2ell+3. The presence bit is retained in finite control while returning +the corresponding payload head. + +For decrement, change each initial zero to one and move right until a one +or terminal blank is read. If a one is found, replace it with zero and +rewind. This subtracts one in the unchanged fixed-width word. Starting +from a positive integer j, the initial zero-run length is its 2-adic +valuation. Its cost is 5v_2(j)+5. The h positive decrements therefore cost +10h-5popcount(h), by the same floor sum. Each successful decrement also +causes one physical payload step left and a read of that parent bit. + +When the word is zero, all ell digits are temporarily changed to ones. +The terminal blank identifies this case. Walk backward, erasing those +ones, stop at the local marker and step right. Including the forward scan, +this final failed decrement costs exactly 6ell+4. It returns false with +scratch empty. There is no full-width zero test on every decrement; that +would introduce an unnecessary H log H action bound. + +The code's only variable controller data are current symbols, a Boolean +decrement result, fixed role indices and the sixteen-bit mask. Count +arithmetic resides on tape. Helper call depth is fixed; all helpers can +be duplicated at their finitely many call sites. Mathematical nested-call +induction is not runtime recursion. The Python simulator's dictionaries, +integer heads and snapshots belong to the test machine, not the controller. + +## Restoration and nesting + +The descriptor transfer, its two reversals, local child cleanup and parent +suspension markers are the unchanged #5364 recipe. The new role loops +replace only recording and consuming the return distance. After j parking +steps the payload head is h_i+j and the counter represents j. The first +blank occurs at j=H_i. Thus the child marker is placed at the exact parent +end and the saved count is correct. Parent payload symbols are never written. + +After child cleanup, erase that suspension marker. The payload head is now +at the parent end s_i. Each of H_i successful decrements moves it one cell +left. Its final position is exactly h_i, and each visited parent cell is +binary. The final failed decrement erases all counter cells. The saved +presence bit restores that role's mask bit, including occupied empty roles. + +The unchanged descriptor return restores the original opaque word and its +head. Consuming `[` leaves control at the original blank top. All new +control and scratch cells are blank, and older control symbols are untouched. +This proves one matched pair. Induction on any finite properly nested call +tree proves the same assertion at every depth, since each inner matched +pair restores the complete entry state required by its parent's remainder. +No claim is made for malformed storage, failed children or unmatched calls. +Invalid calls need not be transactional. + +## Derivation of the complete invoice + +The inherited `emit` and `take` cost three actions. A local rewind from +offset x costs 2x+3. Clearing a child of length t from head g costs +2g+5t+7, including empty children and all delimiter/blank reads. + +For one role, push costs presence emission three, payload scanning 2h+1, +increments 10h-5popcount(h), counter transfer 8ell+4, suspension-marker +write and movement two, and terminator emission three. Its total is +12h-5popcount(h)+8ell+13. The inherited descriptor/frame setup costs +8d+13, with one added initial scratch-blank read. Consequently + + push = 8d + 12H - 5P + 8L + 13*16 + 14. + +For one role, pop costs six actions for its terminator and payload marker, +8ell+6 for loading its count and presence bit, 10h-5popcount(h) for the +positive decrements, 2h for payload return, and 6ell+4 for the final zero +cleanup. Its total is 12h-5popcount(h)+14ell+16. The inherited descriptor +and frame remainder is 14d+16, including the scratch-blank test. Hence + + pop = 14d + 12H - 5P + 14L + 16*16 + 16 + + sum_j (2g_j+5t_j+7), + +where there are seventeen child segments. Adding the two formulas yields +(1). Since L<=H, P>=0 and G<=W, (2) follows for all nonnegative extents. +These are symbolic tape-action identities, not elapsed-time benchmarks. + +## Verification and implementation boundaries + +The new verifier executes the new controller on the pinned predecessor's +unit-action Tape simulator. It does not execute the predecessor's verifier +or census. Independently computed binary strings, complete nineteen-tape +snapshots and the displayed exact formulas are the oracles. A new controller +object is created before return. Finite cases corroborate the written +all-size proof; they are not a proof-kernel result. + +All loops in the controller are bounded by the declared finite tape segments, +return distances, bit lengths or the fixed sixteen roles. In valid calls +these decrease to a delimiter or a zero count. In the bounded verifier, +payload lengths are at most 4097 in power-boundary cases and 4096 in its +sixteen-role illustration; depth is at most 31 and prefixes at most 4096. +The interpreter necessarily allocates managed Python objects; finite input +bounds limit that test allocation. The finite-control program uses only its +fixed tapes. The inherited simulator and helper implementation are unchanged. +No repository-wide diagnostics or allocation refactor is part of this result. +Dynamic imports are confined to authenticated, explicitly declared source +paths; the four negative controls temporarily replace two named functions +or damage one fixture symbol, and restore the original functions afterward. + +The standard binary carry argument is classical. The new result is this +complete continuation-contract refinement, including the nine-symbol grammar, +shared scratch, explicit restoration and exact space/action tradeoff. +Mihir Srivastava retains #5364's contract, descriptor recipe and simulator; +Ali Romman retains #5356/#5368's related stack/output construction; zxv +retains #5404's complete historical-backing result. JoyboyBrian's segment +boundary, Jose Manuel's sequential primitives, Douglas Colkitt's guard/repair, +Cinna Davis's caller, Matarener's cover/stock and Sagar Thakrar's parent-return +lineage retain their predecessor credit. None is reverified as the deliverable. diff --git a/research/binary-distance-continuations/README.md b/research/binary-distance-continuations/README.md new file mode 100644 index 0000000000..c6229813a2 --- /dev/null +++ b/research/binary-distance-continuations/README.md @@ -0,0 +1,124 @@ +# Binary head-distance continuation frames + +Scoped constructive proof with exact finite corroboration, produced by Nick +Petalas. Apache-2.0. Independent human and formal proof-kernel review are +unclaimed. + +The local continuation contract of Mihir Srivastava's +[PR #5364](https://github.com/CrocSwap/integer-mult-bounds/pull/5364) can use +binary head-return distances with the same nineteen tapes and nine symbols. +Let H_i be each role's head-to-end distance, H their sum, d the opaque binary +descriptor length, and L the sum of bitlength(H_i), with bitlength(0)=0. + +```text +Unary control frame: d + 35 + H symbols +Binary control frame: d + 35 + L symbols +``` + +The new construction records actual head movement with a little-endian +counter on the existing reverse-scratch tape. It clears that counter into +the frame and reconstructs it at return. All parent bytes, physical heads, +role flags, descriptor, older stack symbols and scratch return exactly. +Proper finite nesting is permitted, and child cleanup remains paid. + +With sixteen distances of 4096 and an empty descriptor, the executed frame +uses **243 symbols instead of 65,571**, saving **65,328**. Its complete matched +push/pop costs 1,577,893 read/write/unit-move actions for empty child words. +This is an exact symbolic action invoice, not a runtime benchmark. + +[PROOF.md](PROOF.md) proves restoration, nesting, the grammar and the exact bill + + 22d + 24H - 10P + 22L + 613 + 2G + 5W, + +where P sums popcounts of the distances, W sums all seventeen child-word +lengths, and G sums their return head offsets. Therefore the complete bill +is at most **22d + 46H + 613 + 7W**. This exchanges a larger linear action +constant for smaller headers. Scratch uses at most max(d,max_i bitlength(H_i)) +working symbols, plus its marker and terminal blank. Its historical extent +is reused, and erased cells remain part of physical backing. + +## Evidence and reproduction + +CPython 3.12.15 on macOS 27.0.1 arm64; standard library only. From the repository +root, the exact local interpreter is `/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12`. +Use that interpreter in place of `python3.12` below on the supplied workspace. + +```sh +python3.12 -B scripts/research_package.py --package research/binary-distance-continuations +python3.12 -I -W error -B research/binary-distance-continuations/verify.py +python3.12 -I -O -W error -B research/binary-distance-continuations/verify.py +python3.12 -B scripts/check_research_commit.py --package research/binary-distance-continuations --check-source-history +``` + +Expected markers are `PASS_BINARY_DISTANCE_CONTINUATIONS` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. Both registered commands run the complete +check. [RESULT.json](RESULT.json) is generated by the verifier and binds the +new implementation, verifier and written proof by SHA256. To regenerate it +for an intentional source change, pass `--write-receipt /absolute/scratch/RESULT.json` +and inspect that output before replacing the committed receipt. + +The checks execute 4,816 small matched boundaries, 36 distances immediately +below/at/above powers of two through 4096, and 117 nested returns at depths +1, 7 and 31 with ancestor-prefix lengths 16, 257 and 4096. The small domain +covers every binary parent word of lengths zero through five, every parent +head and every descriptor of lengths zero through three on a rotating role, +plus the completely absent empty mask. Each matched boundary checks the +independently generated frame, all nineteen tape snapshots, mask, exact +action counts and conservative bill. A fresh controller object performs pop. +Four controls reject a wrong top delimiter, omitted increment, omitted +decrement and an absent nonempty role. Explicit exceptions remain active +under optimized Python. No predecessor verifier or mathematical census is run. + +## Scope and limitations + +This original target changes the `uniform-transfer-audit` card to a local +constructive side result relevant to `precision_tape` and `owned_erasure`. +The selected baseline binding check passed. Neither selected assumption is +discharged at its complete caller. The selected frontier is unchanged. + +The caller supplies well-formed contiguous binary segments, separate physical +tapes and local markers. Intended child output must already be delivered +before destructive pop. Malformed/failed calls need not restore state. +Production dispatch, descriptor production, child-output installation, full +historical payload backing, stock and a complete caller invoice remain open. +No flat finite-state transition table, proof-kernel check, selected cold replay, +Lean/Docker run or new kappa is supplied. + +The new controller is the rerunnable construction. Its loops terminate on +finite local segments or counters under the entry contract. Test-side managed +allocation, authenticated imports and narrowly bounded function replacement +controls are documented in the proof. No shared implementation is changed. + +## Sources, overlap and credit + +Canonical base is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +[SOURCES.json](SOURCES.json) binds #5364's exact contract, proof and simulator +as retained on that base. The new code reuses its primitive tape actions and +descriptor/cleanup recipe. Mihir Srivastava retains that credit; this package +adds the binary-distance construction and its exact space/action tradeoff. +The carry-count identity and binary arithmetic are classical. + +Related merged work was read for scope: Ali Romman's #5356 local unary stack +and #5368 output return, and zxv's #5404 historical-backing theorem. Their +contracts are distinct and their results are cited, not audited. JoyboyBrian's +segment boundary, Jose Manuel's sequential primitives, Douglas Colkitt's +guard/repair, Cinna Davis's caller, Matarener's cover/stock and Sagar Thakrar's +parent-return lineage retain their predecessor credit. No source notice changes. + +The overlap check covered live PR titles/bodies, this account's recent work, +latest handoffs, active Discussions, batch reservations, main README text and +merged searches for binary continuations, head distances and compressed +headers. No matching refinement was located in that coverage. Sparse cached +notes, unpublished work and arbitrary historical code diffs remain limits; +no literature-wide priority claim is made. The original target is reserved +as a binary-head-distance continuation question, not as a predecessor audit. +[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228524). + +## Open next questions + +Can an actual selected recursive caller use this frame with a smaller complete +historical tape reserve? First bind one real continuation boundary and complete +nested execution to the changed grammar, counting every tape's high-water +extent. Production descriptor/dispatch semantics, designated output delivery, +allocation and stock are blockers. The structured question is in +[TASK.json](TASK.json). This result stops at the verified local reduction. diff --git a/research/binary-distance-continuations/RESULT.json b/research/binary-distance-continuations/RESULT.json new file mode 100644 index 0000000000..37cd8574ba --- /dev/null +++ b/research/binary-distance-continuations/RESULT.json @@ -0,0 +1,23 @@ +{ + "distance_4096_each_role": { + "binary_frame_symbols": 243, + "matched_actions": 1577893, + "saved_frame_symbols": 65328, + "unary_frame_symbols": 65571 + }, + "negative_controls": [ + "wrong top delimiter", + "omitted increment", + "omitted decrement", + "absent nonempty role" + ], + "nested_returns": 117, + "power_boundaries": 36, + "small_boundaries": 4816, + "source_sha256": { + "PROOF.md": "f7ebf3bfd535cc71587572745701d3acd81e89e6ddfa77a189940571bebafca2", + "binary_stack.py": "2080a526d2991fd04e6953c5f5d1478d771eda7b87172891dc257820f0109c34", + "verify.py": "baad803ce804e5ec185d3dee16e18cd5c1594f051e2c65cf6fc2e5f1b0ab98d3" + }, + "status": "PASS_BINARY_DISTANCE_CONTINUATIONS" +} diff --git a/research/binary-distance-continuations/SOURCES.json b/research/binary-distance-continuations/SOURCES.json new file mode 100644 index 0000000000..997a5765e7 --- /dev/null +++ b/research/binary-distance-continuations/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/segment-continuation-stack/PROOF.md", + "usage": "input", + "git_blob": "4a89021e16e838861f13f19a05df5eb38f7fb3b2", + "sha256": "f171e4181082037533848828da8bc6adba1f95f25e5c5ff4ee53a65fb05c0247" + }, + { + "path": "research/segment-continuation-stack/README.md", + "usage": "input", + "git_blob": "ec62fb3f4457c7b3689b7cafb26a864c109557ec", + "sha256": "8b5c7b3d36ce34dab5bc24102a01e7a78e0aaadeee4a744abda7cb75b4e1474d" + }, + { + "path": "research/segment-continuation-stack/stack.py", + "usage": "input", + "git_blob": "f551aec73ec7ce773adeb44321535316efd3f2e5", + "sha256": "d254d409d695942b4a0a58e54ff3a24da6a8a8b4b7211a19679faae63e76ff60" + } + ] +} diff --git a/research/binary-distance-continuations/TASK.json b/research/binary-distance-continuations/TASK.json new file mode 100644 index 0000000000..f660ce1d2f --- /dev/null +++ b/research/binary-distance-continuations/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "Construct binary head-distance continuation frames with exact restoration and linear sequential action cost.", + "scope_change_reason": "An original local construction reduces the unary header space in PR5364. It targets a precision/tape implementation component; it does not discharge a selected all-size assumption at its full caller.", + "bottleneck_link": "Scoped continuation-space improvement relevant to precision_tape and owned_erasure. Production caller integration and complete reserve remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified header-space reduction; do not extend to a full caller.", + "outcome": "completed", + "evidence": "PROOF.md gives an all-size local construction. RESULT.json is generated by verify.py with full restoration, exact costs, nested returns and negative controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual selected recursive caller use this binary continuation frame with a smaller complete historical tape reserve?", + "why_it_matters": "A local frame reduction is useful only after all payload and workspace high-water extents are included.", + "first_step": "Bind one source continuation boundary and a complete nested execution to the changed grammar and count every physical tape extent.", + "blocked_by": "Production descriptor/dispatch semantics, designated output delivery, and the complete caller allocation and stock contract are not supplied here." + } + ] +} diff --git a/research/binary-distance-continuations/VERIFY.json b/research/binary-distance-continuations/VERIFY.json new file mode 100644 index 0000000000..97fe8c6837 --- /dev/null +++ b/research/binary-distance-continuations/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/segment-continuation-stack/PROOF.md", + "research/segment-continuation-stack/README.md", + "research/segment-continuation-stack/stack.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source authentication, complete restoration and frame grammar, exact action invoices, 4816 small boundaries, 36 power boundaries, 117 nested returns, four negative controls and source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the complete verifier with optimizations; explicit exceptions remain active." + } + ] +} diff --git a/research/binary-distance-continuations/binary_stack.py b/research/binary-distance-continuations/binary_stack.py new file mode 100644 index 0000000000..440c4576a1 --- /dev/null +++ b/research/binary-distance-continuations/binary_stack.py @@ -0,0 +1,154 @@ +"""Binary-distance refinement of Mihir Srivastava's PR5364 contract. + +New construction produced by Nick Petalas. Apache-2.0. +The inherited tape actions and descriptor/cleanup recipe retain PR5364 credit. +Only symbols, fixed role indices and a sixteen-bit mask are controller state. +""" + +from stack import ( + BITS, BLANK, LEFT, ROLES, Controller as UnaryController, + clear, emit, need, rewind, take, +) + + +def increment(counter): + """Increment a little-endian count and return to its local beginning.""" + while True: + symbol = counter.read() + need(symbol in BITS or symbol == BLANK, 'counter alphabet') + if symbol != '1': + counter.write('1') + break + counter.write('0') + counter.move(1) + rewind(counter) + + +def store_count(counter, control): + """Emit most-significant-first u/: digits and erase the counter.""" + while counter.read() != BLANK: + counter.move(1) + while True: + counter.move(-1) + symbol = counter.read() + if symbol == LEFT: + counter.move(1) + return + need(symbol in BITS, 'stored counter alphabet') + emit(control, 'u' if symbol == '0' else ':') + counter.write(BLANK) + + +def load_count(control, counter): + """Consume reversed count digits; return the separate presence bit.""" + leading = BLANK + symbol = take(control) + while symbol in ('u', ':'): + emit(counter, '0' if symbol == 'u' else '1') + leading = symbol + symbol = take(control) + need(leading in (BLANK, ':'), 'canonical binary distance') + need(symbol in BITS, 'role presence flag') + rewind(counter) + return symbol + + +def decrement(counter): + """Subtract one, or erase the fixed-width zero word and return false.""" + while True: + symbol = counter.read() + need(symbol in BITS or symbol == BLANK, 'counter alphabet') + if symbol == '1': + counter.write('0') + rewind(counter) + return True + if symbol == BLANK: + break + counter.write('1') + counter.move(1) + while True: + counter.move(-1) + symbol = counter.read() + if symbol == LEFT: + counter.move(1) + return False + need(symbol == '1', 'zero-count cleanup') + counter.write(BLANK) + + +class Controller(UnaryController): + """The same nineteen tapes and nine symbols, with binary distance fields.""" + + def push(self): + need(self.reverse.read() == BLANK, 'counter scratch empty') + emit(self.control, '[') + while True: + symbol = self.descriptor.read() + if symbol == BLANK: + break + need(symbol in BITS, 'binary descriptor') + emit(self.control, symbol) + self.descriptor.write(BLANK) + self.descriptor.move(1) + rewind(self.descriptor, erased=True) + emit(self.control, ':') + for role in range(ROLES): + present = (self.occupied >> role) & 1 + emit(self.control, '1' if present else '0') + tape = self.payload[role] + while True: + symbol = tape.read() + if symbol == BLANK: + break + need(symbol in BITS, 'binary parent payload') + need(present, 'absent role must be empty') + tape.move(1) + increment(self.reverse) + store_count(self.reverse, self.control) + tape.write(LEFT) + tape.move(1) + emit(self.control, ';') + emit(self.control, ']') + self.occupied = 0 + + def pop(self): + for tape in self.payload: + clear(tape) + clear(self.descriptor) + need(self.reverse.read() == BLANK, 'counter scratch empty') + need(take(self.control) == ']', 'frame top delimiter') + self.occupied = 0 + for role in reversed(range(ROLES)): + need(take(self.control) == ';', 'role terminator') + tape = self.payload[role] + tape.move(-1) + need(tape.read() == LEFT, 'payload suspension delimiter') + tape.write(BLANK) + flag = load_count(self.control, self.reverse) + while decrement(self.reverse): + tape.move(-1) + need(tape.read() in BITS, 'return distance within parent') + if flag == '1': + self.occupied |= 1 << role + need(take(self.control) == ':', 'descriptor terminator') + symbol = take(self.control) + while symbol in BITS: + emit(self.reverse, symbol) + symbol = take(self.control) + need(symbol == '[', 'frame beginning delimiter') + while True: + self.reverse.move(-1) + symbol = self.reverse.read() + if symbol == LEFT: + break + need(symbol in BITS, 'reverse scratch alphabet') + self.reverse.write(BLANK) + emit(self.descriptor, symbol) + self.reverse.move(1) + rewind(self.descriptor) + + +def action_bound(descriptor_bits, return_distance, child_bits): + """Complete matched-boundary bound, including all child cleanup.""" + need(min(descriptor_bits, return_distance, child_bits) >= 0, 'bound domain') + return 22 * descriptor_bits + 46 * return_distance + 613 + 7 * child_bits diff --git a/research/binary-distance-continuations/verify.py b/research/binary-distance-continuations/verify.py new file mode 100644 index 0000000000..a136bbe997 --- /dev/null +++ b/research/binary-distance-continuations/verify.py @@ -0,0 +1,233 @@ +"""Exact finite corroboration. Produced by Nick Petalas. Apache-2.0.""" + +import argparse +import ast +import hashlib +import itertools +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_construction(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + for row in manifest['files']: + if row['usage'] == 'input': + actual = hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() + require(actual == row['sha256'], 'changed source: ' + row['path']) + # Both import locations are explicit; the external code is authenticated. + sys.path.insert(0, str(ROOT / 'research/segment-continuation-stack')) + sys.path.insert(0, str(PACKAGE)) + import binary_stack + import stack + return binary_stack, stack + + +def exact_push(d, distances): + h = sum(distances) + bits = sum(x.bit_length() for x in distances) + ones = sum(x.bit_count() for x in distances) + return 8*d + 12*h - 5*ones + 8*bits + 13*16 + 14 + + +def exact_pop(d, distances, child_lengths, child_heads): + h = sum(distances) + bits = sum(x.bit_length() for x in distances) + ones = sum(x.bit_count() for x in distances) + cleanup = sum(2*g + 5*t + 7 for t, g in zip(child_lengths, child_heads)) + return 14*d + 12*h - 5*ones + 14*bits + 16*16 + 16 + cleanup + + +def frame(descriptor, mask, distances): + rows = [] + for role, distance in enumerate(distances): + digits = format(distance, 'b') if distance else '' + encoded = ''.join('u' if bit == '0' else ':' for bit in digits) + rows.append(str((mask >> role) & 1) + encoded + ';') + return '[' + descriptor + ':' + ''.join(rows) + ']' + + +def fixture(stack, words, heads, descriptor, mask, prefix='101[:;]'): + meter = stack.Meter() + payload = [stack.Tape(meter, prefix, word, head) + for word, head in zip(words, heads)] + control = stack.Tape(meter, prefix) + desc = stack.Tape(meter, prefix, descriptor) + scratch = stack.Tape(meter, prefix) + return meter, payload, control, desc, scratch, mask + + +def snapshots(machine): + _, payload, control, desc, scratch, mask = machine + return tuple(t.snapshot() for t in [*payload, control, desc, scratch]), mask + + +def write_child(tape, word, head, stack): + for symbol in word: + stack.emit(tape, symbol) + for _ in range(len(word) - head): + tape.move(-1) + + +def boundary(module, stack, words, heads, descriptor, mask, children, child_heads): + machine = fixture(stack, words, heads, descriptor, mask) + meter, payload, control, desc, scratch, _ = machine + before = snapshots(machine) + distances = [len(w)-h for w, h in zip(words, heads)] + controller = module.Controller(payload, control, desc, scratch, mask) + start = meter.total + controller.push() + push = meter.total - start + require(push == exact_push(len(descriptor), distances), 'exact push invoice') + actual = ''.join(control._cells.get(i, '_') + for i in range(before[0][-3][0], control._head)) + expected = frame(descriptor, mask, distances) + require(actual == expected, 'binary frame grammar') + require(scratch.snapshot() == before[0][-1], 'scratch after push') + for tape, word, head in zip([*payload, desc], children, child_heads): + write_child(tape, word, head, stack) + # Discard the push controller so the return cannot use hidden saved state. + controller = module.Controller(payload, control, desc, scratch, 0) + start = meter.total + controller.pop() + pop = meter.total - start + lengths = [len(w) for w in children] + require(pop == exact_pop(len(descriptor), distances, lengths, child_heads), + 'exact pop invoice') + restored = (*machine[:-1], controller.occupied) + require(snapshots(restored) == before, 'complete parent restoration') + require(push + pop <= module.action_bound( + len(descriptor), sum(distances), sum(lengths)), 'complete action bound') + return len(expected), push+pop + + +def exhaustive_small(module, stack): + count = 0 + descriptors = [''.join(x) for n in range(4) + for x in itertools.product('01', repeat=n)] + for length in range(6): + for word_tuple in itertools.product('01', repeat=length): + word = ''.join(word_tuple) + for head in range(length+1): + for descriptor in descriptors: + role = count % 16 + words, heads = ['']*16, [0]*16 + words[role], heads[role] = word, head + children = ['']*17 + children[(role+3) % 17] = '01011' + child_heads = [0]*17 + child_heads[(role+3) % 17] = count % 6 + boundary(module, stack, words, heads, descriptor, 1 << role, + children, child_heads) + count += 1 + boundary(module, stack, ['']*16, [0]*16, '', 0, ['']*17, [0]*17) + return count+1 + + +def nested(module, stack, depth, prefix_length): + machine = fixture(stack, ['01011']*16, [3]*16, '10100', 65535, + '1'*prefix_length) + _, payload, control, desc, scratch, mask = machine + saved = [] + for level in range(depth): + before = snapshots((*machine[:-1], mask)) + controller = module.Controller(payload, control, desc, scratch, mask) + controller.push() + saved.append(before) + for role, tape in enumerate(payload): + word = '10100' * (1 + (role+level) % 4) + write_child(tape, word, (role+level) % (len(word)+1), stack) + write_child(desc, '101' * (1 + level % 3), 0, stack) + mask = 65535 + for before in reversed(saved): + controller = module.Controller(payload, control, desc, scratch, mask) + controller.pop() + mask = controller.occupied + require(snapshots((*machine[:-1], mask)) == before, 'nested restoration') + return depth + + +def counter_boundaries(module, stack): + count = 0 + for exponent in range(1, 13): + for distance in ((1 << exponent)-1, 1 << exponent, (1 << exponent)+1): + boundary(module, stack, ['1'*distance]+['']*15, [0]*16, + '00101', 1, ['']*17, [0]*17) + count += 1 + return count + + +def negative_controls(module, stack): + rejected = [] + machine = fixture(stack, ['101']+['']*15, [0]*16, '01', 1) + _, payload, control, desc, scratch, mask = machine + controller = module.Controller(payload, control, desc, scratch, mask) + controller.push() + control._cells[control._head-1] = '[' + try: + controller.pop() + except ValueError: + rejected.append('wrong top delimiter') + for name, replacement in (('increment', lambda counter: None), + ('decrement', lambda counter: False)): + original = getattr(module, name) + try: + setattr(module, name, replacement) + try: + boundary(module, stack, ['101']+['']*15, [0]*16, '01', 1, + ['']*17, [0]*17) + except ValueError: + rejected.append('omitted ' + name) + finally: + setattr(module, name, original) + try: + boundary(module, stack, ['1']+['']*15, [0]*16, '', 0, + ['']*17, [0]*17) + except ValueError: + rejected.append('absent nonempty role') + require(len(rejected) == 4, 'all semantic controls reject') + return rejected + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write-receipt', type=Path) + args = parser.parse_args() + module, stack = load_construction() + tree = ast.parse((PACKAGE / 'binary_stack.py').read_text()) + require(not any(isinstance(n, ast.Attribute) and n.attr.startswith('_') + for n in ast.walk(tree)), 'no simulator metadata access') + result = {'status': 'PASS_BINARY_DISTANCE_CONTINUATIONS'} + result['small_boundaries'] = exhaustive_small(module, stack) + result['power_boundaries'] = counter_boundaries(module, stack) + result['nested_returns'] = sum(nested(module, stack, depth, prefix) + for depth in (1, 7, 31) + for prefix in (16, 257, 4096)) + length, actions = boundary(module, stack, ['1'*4096]*16, [0]*16, '', 65535, + ['']*17, [0]*17) + result['distance_4096_each_role'] = { + 'binary_frame_symbols': length, 'unary_frame_symbols': 16*4096+35, + 'saved_frame_symbols': 16*4096+35-length, 'matched_actions': actions, + } + result['negative_controls'] = negative_controls(module, stack) + result['source_sha256'] = { + name: hashlib.sha256((PACKAGE/name).read_bytes()).hexdigest() + for name in ('binary_stack.py', 'verify.py', 'PROOF.md')} + if args.write_receipt: + args.write_receipt.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + require(result == json.loads((PACKAGE/'RESULT.json').read_text()), + 'generated source-bound receipt') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() From 20ff91f09f67b1ab8b496ca1f80a4e6e7cb19cd2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 22:05:22 +0000 Subject: [PATCH 2/2] docs(research): state continuation construction credit explicitly --- research/binary-distance-continuations/README.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/research/binary-distance-continuations/README.md b/research/binary-distance-continuations/README.md index c6229813a2..ed7d66599e 100644 --- a/research/binary-distance-continuations/README.md +++ b/research/binary-distance-continuations/README.md @@ -1,8 +1,9 @@ # Binary head-distance continuation frames -Scoped constructive proof with exact finite corroboration, produced by Nick -Petalas. Apache-2.0. Independent human and formal proof-kernel review are -unclaimed. +Scoped constructive proof with exact finite corroboration. + +New construction and proof produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. The local continuation contract of Mihir Srivastava's [PR #5364](https://github.com/CrocSwap/integer-mult-bounds/pull/5364) can use @@ -106,7 +107,7 @@ guard/repair, Cinna Davis's caller, Matarener's cover/stock and Sagar Thakrar's parent-return lineage retain their predecessor credit. No source notice changes. The overlap check covered live PR titles/bodies, this account's recent work, -latest handoffs, active Discussions, batch reservations, main README text and +latest handoffs, active Discussions, local reservations, main README text and merged searches for binary continuations, head distances and compressed headers. No matching refinement was located in that coverage. Sparse cached notes, unpublished work and arbitrary historical code diffs remain limits;