From 5a277c1e173b48cfa01ab67a59579c7645142bcc Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 14:40:36 -0500 Subject: [PATCH 1/3] Deliver child output through the physical continuation boundary --- research/continuation-output-return/PROOF.md | 127 +++++++++++++ research/continuation-output-return/README.md | 59 ++++++ .../continuation-output-return/RESULT.json | 75 ++++++++ .../continuation-output-return/SOURCES.json | 62 +++++++ research/continuation-output-return/TASK.json | 80 +++++++++ .../continuation-output-return/VERIFY.json | 40 +++++ .../return_output.py | 43 +++++ .../vendor/adapter.py | 153 ++++++++++++++++ .../vendor/stack.py | 170 ++++++++++++++++++ research/continuation-output-return/verify.py | 148 +++++++++++++++ 10 files changed, 957 insertions(+) create mode 100644 research/continuation-output-return/PROOF.md create mode 100644 research/continuation-output-return/README.md create mode 100644 research/continuation-output-return/RESULT.json create mode 100644 research/continuation-output-return/SOURCES.json create mode 100644 research/continuation-output-return/TASK.json create mode 100644 research/continuation-output-return/VERIFY.json create mode 100644 research/continuation-output-return/return_output.py create mode 100644 research/continuation-output-return/vendor/adapter.py create mode 100644 research/continuation-output-return/vendor/stack.py create mode 100644 research/continuation-output-return/verify.py diff --git a/research/continuation-output-return/PROOF.md b/research/continuation-output-return/PROOF.md new file mode 100644 index 0000000000..9beb018238 --- /dev/null +++ b/research/continuation-output-return/PROOF.md @@ -0,0 +1,127 @@ +# Designated child-output return + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +## Contract and retained stack + +Use the seven-symbol tape alphabet and physical push/pop of +[PR #5356](https://github.com/CrocSwap/integer-mult-bounds/pull/5356), at +[the exact source](https://github.com/aliromman/integer-mult-bounds/blob/ef1cc26e1e9a08c11cf382de948ee433bebab16d/research/delimited-continuation-stack/stack.py). +That result restores k=16 payload roles, their presence bits, heads and an +opaque binary descriptor. It requires every child segment empty at return. +The unchanged stack and source adapter are retained in vendor/. Their source +bytes and notices are checked. This PR adds output delivery, not a new stack. + +Reserve one occupied empty parent output role before push. Its head is at its +segment origin. All other parent segments and heads are arbitrary under the +retained ABI. The child leaves one designated binary output of length L on +one fixed role, with its head anywhere in that segment. The child may leave +other binary work on its roles. Slots are compile-time control labels; the +child and parent labels may be equal. Descriptors are arbitrary finite binary +words. All calls succeed and are properly nested. + +Add one relay tape with a BASE marker and an empty current segment at its +origin. It is distinct from all payload, control and descriptor tapes. Its +arbitrary ancestor prefix is preserved. There are nineteen tapes in total, +independent of nesting depth. The source API's logical counters and lexical +allocation remain a separate calibration facade; the return routine never +reads them, a saved origin, a saved length or a parent object. + +## Schedule and invariant + +First check that the relay head is immediately after BASE and reads blank. +Rewind the child output to its nearest LEFT marker by unit moves. Copy its +binary symbols, in order, to the relay until blank. Rewind the relay to BASE. +This preserves the output in relay cells before any child cell is erased. + +For each of the fixed payload roles, rewind to LEFT, erase each current +binary symbol while moving right, then rewind to LEFT. No ancestor cell is +read or changed. Invoke the unchanged physical pop. It erases its frame and +returns each parent payload, head, presence bit and descriptor exactly. +The relay is outside this bank, so pop cannot erase it. + +Check that the reserved target is blank immediately after LEFT. Copy relay +symbols to that role in order. Erase each relay symbol after copying it. +Rewind both tapes to their markers. The target now contains exactly the +child output, with head zero. The relay is empty at its original head. +All other parent roles and the descriptor have the exact pre-push state. + +These assertions prove a matched boundary by loop induction. The copy loop +preserves the copied prefix and unread suffix. The erase loops affect only +current segments. The retained pop theorem restores the parent. The final +copy loop preserves the delivered prefix and the unread relay suffix. Its +postcondition restores the entry condition of the shared relay. Induction +on a finite call tree therefore reuses the same relay for arbitrary finite +proper nesting. At an outer return, a previously delivered inner result is +an ordinary child output. No recursion frame stores return data in host state. + +## Complete bill + +Count each current-symbol read, write and unit move as one action. Let Sp be +the sum of parent extents and Hp the sum of parent head offsets. Let A be the +number of absent parent roles. Let d and q be the parent and child descriptor +lengths. Let W and Hc be the sums of child extents and head offsets immediately +before return. Thus L<=W and Hc<=W. All these symbols are analysis variables; +the routine does not receive their values. + +The retained push costs + +```text +4Hp + 2Sp + 10k + 7d + A + 11. +``` + +The retained pop, after payload retirement, costs + +```text +9Hp + 2Sp + 21k + 11d + 5q + A + 28. +``` + +Rewinding from offset h to its marker costs 2h+3. Erasing a current segment +of size s from offset h costs 2h+5s+7. If the original output head is h0, +checking the relay and copying the output costs 2h0+6L+11. It leaves that +source at offset L. Retiring all roles then costs +2(Hc-h0+L)+5W+7k. Checking the target and installing the output while erasing +the relay costs 9L+11. Thus the complete matched push/return boundary costs +exactly + +```text +13Hp + 4Sp + 38k + 18d + 5q + 2A + 2Hc + 5W + 17L + 61. +``` + +Child computation and its input/descriptor production are separate costs. +They are not hidden in this formula. Output copying, child cleanup, frame +cleanup, descriptor return and relay cleanup are included. Since Hp<=Sp, +Hc<=W, L<=W and A<=k, the boundary is at most + +```text +17Sp + 40k + 18d + 5q + 24W + 61. +``` + +There is no ancestor-length or nesting-depth factor. If Sp,W,d,q=O(V), this +is O(V) and fits the retained per-node allowance. Those actual volume and +descriptor bounds are explicit premises, not established production facts. + +The relay visits L cells in one boundary and is empty at its end. Across +successful calls its retained backing needs at most the maximum output +length seen so far, not a sum over nesting depths. The parent output owns L +cells in its reserved role. During the first copy the child and relay both +hold the result; neither this duplicate nor the parent output is free stock. +All inherited continuation frames and parked payload backing remain charged. + +## Evidence and scope + +The verifier checks 1800 exact small return bills, including zero-length +outputs and every head position through length three. Twelve nested cases +use depths 1,2,7,31 and ancestor lengths 16,257,4096. Six actual compact-source +cases run both retained layouts and deliver all 1024 output bits to the +parent. An independent direct record permutation checks their values. All +six returns cost 24388 actions. Six malformed-state controls reject. Errors +outside the ABI need not restore a partially executed boundary. + +The source calibration still uses the predecessor's weak-reference allocator +and host logical counters. This result does not compile those facilities. +It does not implement recursive C, packet reorder, a general descriptor +producer, the full production rectangle, native admission, stock matching, +precision or outer recovery. It closes the physical output-return boundary +under a reserved-slot ABI. It does not change kappa or prove the complete +multiplication theorem. Independent human and proof-kernel review remain open. diff --git a/research/continuation-output-return/README.md b/research/continuation-output-return/README.md new file mode 100644 index 0000000000..aa30be07a4 --- /dev/null +++ b/research/continuation-output-return/README.md @@ -0,0 +1,59 @@ +# Physical output return through a continuation + +This package closes the designated child-output return question left by +[PR #5329](https://github.com/CrocSwap/integer-mult-bounds/pull/5329) and +[PR #5356](https://github.com/CrocSwap/integer-mult-bounds/pull/5356). +One added relay tape preserves the result through child cleanup and physical +pop, delivers it into a reserved empty parent role, and returns empty. +All other parent bytes, heads, presence bits and descriptors are restored. +The fixed nineteen-tape bank works for arbitrary finite proper nesting. + +[PROOF.md](PROOF.md) gives the contract, nesting proof, exact linear bill and +space charge. [return_output.py](return_output.py) uses only current-symbol +operations and unit moves. [RESULT.json](RESULT.json) records 1800 exact +invoice cases, nested returns through depth31, six unchanged compact-source +endpoints and six rejecting ABI controls. Both source layouts deliver1024 +bits in24388 return actions for dirty ancestor lengths16,257,4096. + +```sh +python3.12 -B scripts/research_package.py --package research/continuation-output-return +``` + +Both registered isolated, warning-strict normal and optimized modes print +`PASS_CONTINUATION_OUTPUT_RETURN`. Source bytes and the complete receipt are +checked. No third-party package is needed. The all-size claim rests on the +written induction, not the finite tests. + +The complete kappa calculation is unchanged. A reserved empty parent output +role is required. Actual packet order, recursive C, physical source allocation, +logical-counter compilation, full supplier/stock/precision and outer recovery +remain open. Lean, Docker, selected cold replay and full-history validation +were not run. The source calibration retains its explicit Python facade. + +## Open next questions + +Bind this returned stream to the actual FOUR/base packet order and its left +map. First show where the caller reserves the output role and how its child +width determines the stream grammar. Separately compile the source's logical +counters and lexical slots at the repair/stable_radix maximum-live cut. +Neither obligation is discharged by successful byte delivery alone. + +## Credit and coordination + +Base7c472563474e60185e6ca101a17622133d047e56, priority7. The live stack handoff +was already complete, so this package takes only its remaining output-return +boundary. Current PR and Discussion bodies and main notes were checked; +arbitrary historical diffs and unpublished work remain outside coverage. + +The byte-exact stack and adapter in vendor/ are consumed from Ali Romman's +pending PR5356, head ef1cc26e1e9a08c11cf382de948ee433bebab16d. They are pinned +explicitly in [SOURCES.json](SOURCES.json); they are not claimed as main-branch +or independently accepted results. The complete linear theorem is conditional +on that retained stack contract. JoyboyBrian supplied the segment refinement +and locality invoice. Jose Manuel/jmbarrancoml supplied the retained sequential +compact source. Douglas Colkitt supplied guard/repair, Cinna Davis the caller, +and Matarener the cover/stock lineage. Original notices remain unchanged. + +New work: Ali Romman with substantial OpenAI Codex assistance in proof, +implementation, review and verification. Apache-2.0. No independent human or +proof-kernel acceptance is claimed. diff --git a/research/continuation-output-return/RESULT.json b/research/continuation-output-return/RESULT.json new file mode 100644 index 0000000000..816abefec0 --- /dev/null +++ b/research/continuation-output-return/RESULT.json @@ -0,0 +1,75 @@ +{ + "controls": 6, + "matched_boundary": "13Hp+4Sp+38k+18d+5q+2A+2Hc+5W+17L+61", + "nested": [ + { + "depth": 1, + "steps": 2859 + }, + { + "depth": 2, + "steps": 5911 + }, + { + "depth": 7, + "steps": 22133 + }, + { + "depth": 31, + "steps": 118414 + } + ], + "return_sha256": "fbf3167da26c7887b769689075e5dc3afcea2ef668496975bc9e6afec8c85751", + "small_cases": 1800, + "source": [ + { + "late": false, + "output_bits": 1024, + "prefix": 16, + "records": 128, + "return_steps": 24388, + "sha256": "4af9929ff7e3d8e72146e260c7e007e975b7c17ef26c0271355333fe64072a48" + }, + { + "late": false, + "output_bits": 1024, + "prefix": 257, + "records": 128, + "return_steps": 24388, + "sha256": "4af9929ff7e3d8e72146e260c7e007e975b7c17ef26c0271355333fe64072a48" + }, + { + "late": false, + "output_bits": 1024, + "prefix": 4096, + "records": 128, + "return_steps": 24388, + "sha256": "4af9929ff7e3d8e72146e260c7e007e975b7c17ef26c0271355333fe64072a48" + }, + { + "late": true, + "output_bits": 1024, + "prefix": 16, + "records": 128, + "return_steps": 24388, + "sha256": "9b6381e2a8cffec1c0d499b50909c409c9dc178584321a9a6e73fafbdbfaf547" + }, + { + "late": true, + "output_bits": 1024, + "prefix": 257, + "records": 128, + "return_steps": 24388, + "sha256": "9b6381e2a8cffec1c0d499b50909c409c9dc178584321a9a6e73fafbdbfaf547" + }, + { + "late": true, + "output_bits": 1024, + "prefix": 4096, + "records": 128, + "return_steps": 24388, + "sha256": "9b6381e2a8cffec1c0d499b50909c409c9dc178584321a9a6e73fafbdbfaf547" + } + ], + "status": "PASS_CONTINUATION_OUTPUT_RETURN" +} diff --git a/research/continuation-output-return/SOURCES.json b/research/continuation-output-return/SOURCES.json new file mode 100644 index 0000000000..f6aac79c27 --- /dev/null +++ b/research/continuation-output-return/SOURCES.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/complex-segment-boundary/README.md", + "usage": "input", + "git_blob": "0e2e520e4a9ade9cc1d2708419b1918b99e9302b", + "sha256": "94d652b8891f8f41442959d02bd0ca641fe1b3a99f32ba95812353e6d21344e2" + }, + { + "path": "research/complex-segment-boundary/source/NOTICE.md", + "usage": "input", + "git_blob": "e82bfef53054bd753ba0aa8a966f84427faa2293", + "sha256": "74a9f03e9ce467c75f5f7cf1b8465d349ea38ef114afad261824c3bcf13da00f" + }, + { + "path": "research/complex-segment-boundary/source/compact.py", + "usage": "input", + "git_blob": "60bc206c78150f23563a4775800b0dd32025843d", + "sha256": "0e1027a60f38c21cfd808c8ce44dcc2423810efdab0e15f02b07f261ad48fc3c" + }, + { + "path": "research/complex-segment-boundary/source/monomial.py", + "usage": "input", + "git_blob": "5fa4494167c4ba668993a2b1c902969518728a4c", + "sha256": "394f9a465ac9148af0c20844d375e4befbef17d92b2fcc840d83419480dd4740" + }, + { + "path": "research/complex-segment-boundary/source/streams.py", + "usage": "input", + "git_blob": "61542ce4c9eb51bfc113475b4f98649cb90a853e", + "sha256": "718a582a50aee8f1f04945ed942be1d4162962fe47dbf05c6ff37b7fb8c61257" + }, + { + "path": "research/delimited-continuation-stack/stack.py", + "usage": "provenance", + "pin": "head:ef1cc26e1e9a08c11cf382de948ee433bebab16d:research/delimited-continuation-stack/stack.py", + "git_blob": "a5d6753b901901a5b2d1a4dd72134e53af70c666", + "sha256": "21a2213aa850c55e5eace4cd10b72b958d7ee84d83a014567902ce8ee9b3f4f2" + }, + { + "path": "research/delimited-continuation-stack/adapter.py", + "usage": "provenance", + "pin": "head:ef1cc26e1e9a08c11cf382de948ee433bebab16d:research/delimited-continuation-stack/adapter.py", + "git_blob": "d860b58c603fc600f95e3413f9230398e9b957b3", + "sha256": "e13823e4124caa4b25050ddd9ac960db59c81e2db369b9ec7b201aca7efbebb8" + } + ] +} diff --git a/research/continuation-output-return/TASK.json b/research/continuation-output-return/TASK.json new file mode 100644 index 0000000000..9d259eee9e --- /dev/null +++ b/research/continuation-output-return/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Deliver a designated child output across the retained physical continuation stack into a reserved empty parent role with exact cleanup and time.", + "scope_change_reason": "The live stack handoff is complete in PR5356 and PR5364. Their child-output return obligation remains open.", + "bottleneck_link": "Destructive child retirement currently loses the result. A complete call boundary must preserve and install it before the relay is retired.", + "budget_minutes": 60, + "stop_rule": "One complete output-return ABI and actual compact endpoint. No packet reorder, recursive C or physical source allocation claim.", + "outcome": "completed", + "evidence": "PROOF.md, return_output.py, verify.py, RESULT.json", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, review and verification; no independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Can the actual FOUR/base caller reserve the output slot and consume this returned stream in its required order?", + "why_it_matters": "Delivered bytes alone do not establish the packet ABI.", + "first_step": "Bind the selected child width and physical packet order before applying the left map.", + "blocked_by": "Actual packet reorder and recursive C remain separate." + }, + { + "question": "Can the source logical counters and lexical slots be compiled into an explicit physical controller?", + "why_it_matters": "The retained source calibration uses a Python allocation facade.", + "first_step": "Use the repair/stable_radix maximum-live cut.", + "blocked_by": "No external dependency; retain the existing stream endpoints." + } + ] +} diff --git a/research/continuation-output-return/VERIFY.json b/research/continuation-output-return/VERIFY.json new file mode 100644 index 0000000000..4c776f7450 --- /dev/null +++ b/research/continuation-output-return/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-segment-boundary/README.md", + "research/complex-segment-boundary/source/NOTICE.md", + "research/complex-segment-boundary/source/compact.py", + "research/complex-segment-boundary/source/monomial.py", + "research/complex-segment-boundary/source/streams.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact complete tape bills, all parent and output state, nested fixed-bank returns, unchanged compact-source endpoints, local cost, rejecting ABI controls, source bytes and typed receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact complete tape bills, all parent and output state, nested fixed-bank returns, unchanged compact-source endpoints, local cost, rejecting ABI controls, source bytes and typed receipt." + } + ] +} diff --git a/research/continuation-output-return/return_output.py b/research/continuation-output-return/return_output.py new file mode 100644 index 0000000000..cdfdd8ea2f --- /dev/null +++ b/research/continuation-output-return/return_output.py @@ -0,0 +1,43 @@ +"""Deliver a child output through the retained physical continuation stack. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from stack import BASE, BLANK, LEFT, Stack, emit, need, rewind + + +def retire(tape): + rewind(tape, LEFT) + while (symbol := tape.read()) != BLANK: + need(symbol in (0, 1), 'binary child payload') + emit(tape, BLANK) + rewind(tape, LEFT) + + +def return_output(payloads, control, descriptor, relay, child_slot, parent_slot): + """Slots are fixed control labels. The parent output is reserved and empty.""" + need(relay.read() == BLANK, 'empty relay') + relay.move(-1) + need(relay.read() == BASE, 'relay at origin') + relay.move(1) + source = payloads[child_slot] + rewind(source, LEFT) + while (symbol := source.read()) != BLANK: + need(symbol in (0, 1), 'binary child output') + emit(relay, symbol) + source.move(1) + rewind(relay, BASE) + for tape in payloads: + retire(tape) + state = Stack(payloads, control, descriptor).pop() + target = payloads[parent_slot] + need(target.read() == BLANK, 'empty reserved parent output') + target.move(-1) + need(target.read() == LEFT, 'reserved output at origin') + target.move(1) + while (symbol := relay.read()) != BLANK: + need(symbol in (0, 1), 'binary relay output') + emit(target, symbol) + emit(relay, BLANK) + rewind(relay, BASE) + rewind(target, LEFT) + return state diff --git a/research/continuation-output-return/vendor/adapter.py b/research/continuation-output-return/vendor/adapter.py new file mode 100644 index 0000000000..d860b58c60 --- /dev/null +++ b/research/continuation-output-return/vendor/adapter.py @@ -0,0 +1,153 @@ +"""Bind retained sequential source calls to the delimited stack. + +The source's fixed lexical role schedule remains an inherited premise. +Weak references simulate allocation; push/pop never consult that registry. +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from contextlib import contextmanager +import weakref +from stack import BASE, BLANK, LEFT, Counts, Stack, Tape, clear_descriptor, emit, need, rewind + + +class View: + def __init__(self, role): + self.role = role + + def __len__(self): + return self.role.arena.sizes[self.role.slot] + + def __bytes__(self): + # Test oracle only. The retained algorithms use len(data), never this. + role = self.role + tape = role.arena.payloads[role.slot] + start = tape.head - role.head + return bytes(tape.cells[start:start + len(self)]) + + +class Arena: + slots = 16 + + def __init__(self, ancestors, control_prefix=()): + need(len(ancestors) == self.slots, 'sixteen payload roles') + self.counts = Counts() + self.payloads = [Tape(x, counts=self.counts) for x in ancestors] + self.control = Tape(control_prefix, BASE, self.counts) + self.descriptor = Tape((), BASE, self.counts) + self.stack = Stack(self.payloads, self.control, self.descriptor) + self.present = [False] * self.slots + self.sizes = [0] * self.slots + self.heads = [0] * self.slots + self.owners = weakref.WeakValueDictionary() + self.depth = 0 + self.peak = 0 + self.boundary_steps = 0 + + def tape(self, meter, data=b''): + for i in range(self.slots): + if self.present[i] and (self.depth, i) not in self.owners: + need(self.sizes[i] == 0, 'retired source role is empty') + self.present[i] = False + slot = next((i for i, occupied in enumerate(self.present) if not occupied), None) + need(slot is not None, 'fixed role inventory') + need(self.sizes[slot] == 0, 'free role is empty') + self.present[slot] = True + self.peak = max(self.peak, sum(self.present)) + role = Role(self, slot, self.depth, meter) + self.owners[self.depth, slot] = role + role.write(data) + role.rewind() + return role + + def set_descriptor(self, bits): + clear_descriptor(self.descriptor) + for bit in bits: + need(bit in (0, 1), 'binary descriptor input') + emit(self.descriptor, bit) + rewind(self.descriptor, BASE) + + def erase_slot(self, slot): + tape = self.payloads[slot] + rewind(tape, LEFT) + while (symbol := tape.read()) != BLANK: + need(symbol in (0, 1), 'binary current payload') + emit(tape, BLANK) + rewind(tape, LEFT) + self.sizes[slot] = self.heads[slot] = 0 + + @contextmanager + def child(self): + before = self.counts.total + self.stack.push(self.present) + self.boundary_steps += self.counts.total - before + self.present = [False] * self.slots + self.sizes = [0] * self.slots + self.heads = [0] * self.slots + self.depth += 1 + try: + yield + finally: + # Child retirement is charged separately from stack operations. + for slot in range(self.slots): + self.erase_slot(slot) + before = self.counts.total + state = self.stack.pop() + self.boundary_steps += self.counts.total - before + self.present = [x[0] for x in state] + self.sizes = [x[1] for x in state] + self.heads = [x[2] for x in state] + self.depth -= 1 + + +class Role: + def __init__(self, arena, slot, depth, meter): + self.arena, self.slot, self.depth, self.meter = arena, slot, depth, meter + + @property + def data(self): + return View(self) + + @property + def head(self): + return self.arena.heads[self.slot] + + def active(self): + need(self.depth == self.arena.depth and self.arena.present[self.slot], 'active role') + + def read(self, size): + self.active() + a = self.arena + need(0 <= size <= a.sizes[self.slot] - self.head, 'sequential read boundary') + out = bytearray() + tape = a.payloads[self.slot] + for _ in range(size): + bit = tape.read() + need(bit in (0, 1), 'binary current payload') + out.append(bit) + tape.move(1) + a.heads[self.slot] += size + return out + + def write(self, value): + self.active() + a = self.arena + need(self.head == a.sizes[self.slot], 'append-only role') + tape = a.payloads[self.slot] + for bit in value: + need(bit in (0, 1), 'binary current payload') + need(tape.read() == BLANK, 'append at free cell') + emit(tape, bit) + a.sizes[self.slot] += 1 + a.heads[self.slot] += 1 + + def rewind(self): + self.active() + rewind(self.arena.payloads[self.slot], LEFT) + self.arena.heads[self.slot] = 0 + + def finish(self): + self.active() + need(self.head == self.arena.sizes[self.slot], 'complete sequential consumption') + + def erase(self): + self.active() + self.arena.erase_slot(self.slot) diff --git a/research/continuation-output-return/vendor/stack.py b/research/continuation-output-return/vendor/stack.py new file mode 100644 index 0000000000..a5d6753b90 --- /dev/null +++ b/research/continuation-output-return/vendor/stack.py @@ -0,0 +1,170 @@ +"""Delimited continuation on a fixed number of sequential tapes. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The source interface follows JoyboyBrian and Jose Manuel's tape packages. +""" +from dataclasses import dataclass + +ZERO, ONE, LEFT, SEP, END, BASE, BLANK = range(7) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +@dataclass +class Counts: + reads: int = 0 + writes: int = 0 + moves: int = 0 + + @property + def total(self): + return self.reads + self.writes + self.moves + + +class Tape: + """Hardware model. Only read, write and unit move are algorithm operations.""" + def __init__(self, prefix=(), marker=LEFT, counts=None): + self.cells = list(prefix) + [marker] + self.head = len(self.cells) + self.floor = self.head - 1 + self.minimum = self.head + self.counts = counts if counts is not None else Counts() + + def read(self): + self.counts.reads += 1 + self.minimum = min(self.minimum, self.head) + need(self.head >= self.floor, 'ancestor prefix accessed') + return self.cells[self.head] if self.head < len(self.cells) else BLANK + + def write(self, value): + need(value in range(7), 'finite tape alphabet') + need(self.head >= self.floor, 'ancestor prefix overwritten') + self.counts.writes += 1 + while len(self.cells) <= self.head: + self.cells.append(BLANK) + self.cells[self.head] = value + + def move(self, direction): + need(direction in (-1, 1), 'unit move') + self.counts.moves += 1 + self.head += direction + need(self.head >= self.floor, 'ancestor prefix crossed') + + +def emit(tape, symbol): + tape.write(symbol) + tape.move(1) + + +def rewind(tape, marker): + tape.move(-1) + while tape.read() != marker: + tape.move(-1) + tape.move(1) + + +def clear_descriptor(tape): + """Entry and exit are at the descriptor origin.""" + while (symbol := tape.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary descriptor') + emit(tape, BLANK) + rewind(tape, BASE) + + +class Stack: + """No saved frame, parent pointer, frame size or origin is stored here.""" + def __init__(self, payloads, control, descriptor): + self.payloads = tuple(payloads) + self.control = control + self.descriptor = descriptor + + def push(self, present): + need(len(present) == len(self.payloads), 'fixed role bitmap') + c = self.control + need(c.read() == BLANK, 'control at free top') + emit(c, LEFT) + for tape, occupied in zip(self.payloads, present): + need(type(occupied) is bool, 'role presence bit') + emit(c, int(occupied)) + tape.move(-1) + while (symbol := tape.read()) != LEFT: + need(symbol in (ZERO, ONE), 'binary prefix before current head') + emit(c, ONE) + tape.move(-1) + emit(c, ZERO) + tape.move(1) + if not occupied: + need(tape.read() == BLANK, 'absent role is empty') + while (symbol := tape.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary parent payload') + tape.move(1) + emit(tape, LEFT) + emit(c, SEP) + d = self.descriptor + while (symbol := d.read()) != BLANK: + need(symbol in (ZERO, ONE), 'binary descriptor') + emit(c, symbol) + emit(d, BLANK) + rewind(d, BASE) + emit(c, END) + + def pop(self): + """Child payloads are empty at their origins; clear its descriptor. + + Returned sizes/heads are observer counts for the source API adapter. + No branch or tape move uses those counts. + """ + clear_descriptor(self.descriptor) + c = self.control + c.move(-1) + need(c.read() == END, 'complete control frame') + c.move(-1) + while (symbol := c.read()) != LEFT: + need(symbol in (ZERO, ONE, SEP), 'frame start before ancestor boundary') + c.move(-1) + emit(c, BLANK) + state = [] + for tape in self.payloads: + present = c.read() + need(present in (ZERO, ONE), 'role presence bit') + emit(c, BLANK) + need(tape.read() == BLANK, 'child payload is retired') + tape.move(-1) + need(tape.read() == LEFT, 'child delimiter') + tape.write(BLANK) + tape.move(-1) + size = 0 + while (symbol := tape.read()) != LEFT: + need(symbol in (ZERO, ONE), 'parked parent payload') + size += 1 + tape.move(-1) + tape.move(1) + if not present: + need(tape.read() == BLANK, 'absent parent role is empty') + head = 0 + while (symbol := c.read()) == ONE: + need(tape.read() in (ZERO, ONE), 'saved head is within payload') + tape.move(1) + head += 1 + emit(c, BLANK) + need(symbol == ZERO, 'terminated unary head') + emit(c, BLANK) + state.append((bool(present), size, head)) + need(c.read() == SEP, 'complete fixed-role header') + emit(c, BLANK) + d = self.descriptor + while (symbol := c.read()) != END: + need(symbol in (ZERO, ONE), 'binary saved descriptor') + emit(d, symbol) + emit(c, BLANK) + c.write(BLANK) + c.move(-1) + while c.read() == BLANK: + c.move(-1) + need(c.read() in (BASE, END), 'previous control top') + c.move(1) + rewind(d, BASE) + return state diff --git a/research/continuation-output-return/verify.py b/research/continuation-output-return/verify.py new file mode 100644 index 0000000000..3fbe454cee --- /dev/null +++ b/research/continuation-output-return/verify.py @@ -0,0 +1,148 @@ +"""Check output delivery, exact tape bills and unchanged source endpoints. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import sys + +P=Path(__file__).resolve().parent +ROOT=P.parents[1] +for row in json.loads((P/'SOURCES.json').read_text())['files']: + if row['usage']=='input':path=ROOT/row['path'] + elif row.get('pin'):path=P/'vendor'/Path(row['path']).name + else:continue + if hashlib.sha256(path.read_bytes()).hexdigest()!=row['sha256']:raise ValueError('source hash') +sys.path[:0]=[str(P),str(P/'vendor'),str(ROOT/'research/complex-segment-boundary/source')] +from stack import BASE, BLANK, LEFT, Counts, Stack, Tape, emit, need, rewind +from return_output import return_output +from adapter import Arena +import streams,compact,monomial + + +def bits(n,salt=0):return tuple((i*17+i//3+salt)%2 for i in range(n)) + + +def snapshot(t): + cells=t.cells[:] + while cells and cells[-1]==BLANK:cells.pop() + return cells,t.head + + +def load(t,data,head=0,marker=LEFT): + for bit in data:emit(t,bit) + rewind(t,marker) + for _ in range(head):t.move(1) + + +def bank(k,prefix): + m=Counts();p=[Tape(bits(prefix,i),counts=m) for i in range(k)] + c=Tape(bits(prefix+3),BASE,m);d=Tape((),BASE,m);relay=Tape(bits(prefix+5),BASE,m) + return m,p,c,d,relay + + +def expect_return(payload,c,d,relay,before,output,target): + expected=list(before) + old,head=expected[target];expected[target]=(old+list(output),head) + need([snapshot(t) for t in (*payload,c,d,relay)]==expected,'complete delivered state') + + +def small(): + count=0 + for s in range(4): + for h in range(s+1): + for dlen,qlen,length,ch,extra in itertools.product(range(3),range(2),range(4),range(4),range(3)): + if ch>length:continue + m,p,c,d,r=bank(2,17);load(p[1],bits(s),h);load(d,bits(dlen),marker=BASE) + before=[snapshot(t) for t in (*p,c,d,r)];start=m.total + Stack(p,c,d).push([True,True]) + need(m.total-start==4*h+2*s+20+7*dlen+11,'exact push invoice') + load(d,bits(qlen,1),marker=BASE) + load(p[0],bits(length,1),ch);load(p[1],bits(extra),extra) + # Setup and child work are excluded from the boundary-only meter. + push=4*h+2*s+20+7*dlen+11 + start=m.total + return_output(p,c,d,r,0,0) + pop=9*h+2*s+28*2+11*dlen+5*qlen+2*(ch+extra)+5*(length+extra)+17*length+50 + need(m.total-start==pop,'exact return invoice') + need(push+pop==13*h+4*s+38*2+18*dlen+5*qlen+2*(ch+extra)+5*(length+extra)+17*length+61,'matched invoice') + expect_return(p,c,d,r,before,bits(length,1),0);count+=1 + return count + + +def nested(depth,prefix): + m,p,c,d,r=bank(16,prefix);expected=[] + for level in range(depth): + for j in range(1,16):load(p[j],bits((j+level)%7,j),(j+level)%7//2) + if level==0:load(d,bits(17),marker=BASE) + else:load(d,bits(17+2*level),marker=BASE) + expected.append([snapshot(t) for t in (*p,c,d,r)]) + Stack(p,c,d).push([True]*16) + output=bits(43,1);load(p[0],output,17) + for before in reversed(expected): + return_output(p,c,d,r,0,0) + expect_return(p,c,d,r,before,output,0) + return m.total + + +def direct(raw,layout,word): + out=bytearray(len(raw));w=layout.record_bits + for i in range(layout.records): + j=layout.encode(word.ideal(layout.decode(i),True));out[j*w:(j+1)*w]=raw[i*w:(i+1)*w] + return bytes(out) + + +def source_case(prefix,late): + a=Arena([bits(prefix,j) for j in range(16)],bits(prefix+3)) + relay=Tape(bits(prefix+5),BASE,a.counts) + for mod in (streams,compact,monomial):mod.Tape=a.tape + parents=[a.tape(streams.Meter(),b'' if j==0 else bits(j+2,j)) for j in range(16)] + for j,role in enumerate(parents):role.read(0 if j==0 else j//2) + a.set_descriptor(bits(43));before=[snapshot(t) for t in (*a.payloads,a.control,a.descriptor,relay)] + a.stack.push(a.present);a.present=[False]*16;a.sizes=[0]*16;a.heads=[0]*16;a.depth+=1 + fields=(('u',1),('t',1))+((('y',2),('x',2)) if late else (('x',2),('y',2)))+(('b',1),) + layout=compact.Layout(fields,8);word=compact.Compact(1,1,1,0,'x','y',late) + raw=bytes(bit for i in range(layout.records) for bit in streams.bit_key(i,8)) + child=a.tape(streams.Meter(),raw);out=compact.execute(child,layout,word) + expected=direct(raw,layout,word);need(bytes(out.data)==expected,'independent compact endpoint') + a.set_descriptor(bits(17));start=a.counts.total + state=return_output(a.payloads,a.control,a.descriptor,relay,out.slot,0) + need(state==[(True,0 if j==0 else j+2,0 if j==0 else j//2) for j in range(16)],'physical parent metadata') + expect_return(a.payloads,a.control,a.descriptor,relay,before,expected,0) + return dict(prefix=prefix,late=late,records=layout.records,output_bits=len(expected),return_steps=a.counts.total-start,sha256=hashlib.sha256(expected).hexdigest()) + + +def controls(): + count=0 + for fault in ('relay_dirty','relay_head','parent_nonempty','parent_head','output_symbol','frame_end'): + m,p,c,d,r=bank(2,9) + if fault in ('parent_nonempty','parent_head'):load(p[0],(1,),int(fault=='parent_head')) + Stack(p,c,d).push([True,True]);load(p[1],(0,1,1),1) + if fault=='relay_dirty':r.write(1) + if fault=='relay_head':r.move(1) + if fault=='output_symbol':p[1].cells[p[1].head]=BASE + if fault=='frame_end':c.cells[c.head-1]=BLANK + try:return_output(p,c,d,r,1,0) + except ValueError:count+=1 + else:raise ValueError('accepted control: '+fault) + return count + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--write-result',action='store_true');args=ap.parse_args() + n=small();nested_rows=[] + for depth in (1,2,7,31): + costs=[nested(depth,prefix) for prefix in (16,257,4096)] + need(len(set(costs))==1,'nested locality');nested_rows.append(dict(depth=depth,steps=costs[0])) + source=[source_case(prefix,late) for late in (False,True) for prefix in (16,257,4096)] + for late in (False,True):need(len({r['return_steps'] for r in source if r['late']==late})==1,'source return locality') + result=dict(status='PASS_CONTINUATION_OUTPUT_RETURN',small_cases=n,nested=nested_rows,source=source,controls=controls(),matched_boundary='13Hp+4Sp+38k+18d+5q+2A+2Hc+5W+17L+61',return_sha256=hashlib.sha256((P/'return_output.py').read_bytes()).hexdigest()) + if args.write_result:(P/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:need(result==json.loads((P/'RESULT.json').read_text()),'complete typed receipt') + print(json.dumps(result,sort_keys=True)) + + +if __name__=='__main__':main() From 1362d9350b733af1c8a8822e0a013c1ff7de64dc Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 14:42:20 -0500 Subject: [PATCH 2/3] Clarify output-return replay and source wording --- research/continuation-output-return/README.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/research/continuation-output-return/README.md b/research/continuation-output-return/README.md index aa30be07a4..426fe0ddde 100644 --- a/research/continuation-output-return/README.md +++ b/research/continuation-output-return/README.md @@ -11,9 +11,9 @@ The fixed nineteen-tape bank works for arbitrary finite proper nesting. [PROOF.md](PROOF.md) gives the contract, nesting proof, exact linear bill and space charge. [return_output.py](return_output.py) uses only current-symbol operations and unit moves. [RESULT.json](RESULT.json) records 1800 exact -invoice cases, nested returns through depth31, six unchanged compact-source -endpoints and six rejecting ABI controls. Both source layouts deliver1024 -bits in24388 return actions for dirty ancestor lengths16,257,4096. +invoice cases, nested returns through depth 31, six unchanged compact-source +endpoints and six rejecting ABI controls. Both source layouts deliver 1024 +bits in 24388 return actions for dirty ancestor lengths 16,257,4096. ```sh python3.12 -B scripts/research_package.py --package research/continuation-output-return @@ -40,13 +40,13 @@ Neither obligation is discharged by successful byte delivery alone. ## Credit and coordination -Base7c472563474e60185e6ca101a17622133d047e56, priority7. The live stack handoff +Base 7c472563474e60185e6ca101a17622133d047e56, priority7. The live stack handoff was already complete, so this package takes only its remaining output-return boundary. Current PR and Discussion bodies and main notes were checked; arbitrary historical diffs and unpublished work remain outside coverage. The byte-exact stack and adapter in vendor/ are consumed from Ali Romman's -pending PR5356, head ef1cc26e1e9a08c11cf382de948ee433bebab16d. They are pinned +pending PR #5356, head ef1cc26e1e9a08c11cf382de948ee433bebab16d. They are pinned explicitly in [SOURCES.json](SOURCES.json); they are not claimed as main-branch or independently accepted results. The complete linear theorem is conditional on that retained stack contract. JoyboyBrian supplied the segment refinement From c4ad9a4063eba8c3e0ccd800301812c58fe71d14 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 15:25:02 -0500 Subject: [PATCH 3/3] Bind continuation sources to retained publication history --- research/continuation-output-return/README.md | 8 +++++--- research/continuation-output-return/SOURCES.json | 14 ++++++++------ 2 files changed, 13 insertions(+), 9 deletions(-) diff --git a/research/continuation-output-return/README.md b/research/continuation-output-return/README.md index 426fe0ddde..1b17891d7b 100644 --- a/research/continuation-output-return/README.md +++ b/research/continuation-output-return/README.md @@ -47,9 +47,11 @@ arbitrary historical diffs and unpublished work remain outside coverage. The byte-exact stack and adapter in vendor/ are consumed from Ali Romman's pending PR #5356, head ef1cc26e1e9a08c11cf382de948ee433bebab16d. They are pinned -explicitly in [SOURCES.json](SOURCES.json); they are not claimed as main-branch -or independently accepted results. The complete linear theorem is conditional -on that retained stack contract. JoyboyBrian supplied the segment refinement +in [SOURCES.json](SOURCES.json). Replay pins resolve to the byte-exact copies +in this PR history. Each upstream_pin retains the original pending source. +Thus a clean checkout does not need an unmerged predecessor commit. They are +not claimed as main-branch or independently accepted results. The complete +linear theorem is conditional on that retained stack contract. JoyboyBrian supplied the segment refinement and locality invoice. Jose Manuel/jmbarrancoml supplied the retained sequential compact source. Douglas Colkitt supplied guard/repair, Cinna Davis the caller, and Matarener the cover/stock lineage. Original notices remain unchanged. diff --git a/research/continuation-output-return/SOURCES.json b/research/continuation-output-return/SOURCES.json index f6aac79c27..96b6abd075 100644 --- a/research/continuation-output-return/SOURCES.json +++ b/research/continuation-output-return/SOURCES.json @@ -45,18 +45,20 @@ "sha256": "718a582a50aee8f1f04945ed942be1d4162962fe47dbf05c6ff37b7fb8c61257" }, { - "path": "research/delimited-continuation-stack/stack.py", + "path": "research/continuation-output-return/vendor/stack.py", "usage": "provenance", - "pin": "head:ef1cc26e1e9a08c11cf382de948ee433bebab16d:research/delimited-continuation-stack/stack.py", + "pin": "head:1362d9350b733af1c8a8822e0a013c1ff7de64dc:research/continuation-output-return/vendor/stack.py", "git_blob": "a5d6753b901901a5b2d1a4dd72134e53af70c666", - "sha256": "21a2213aa850c55e5eace4cd10b72b958d7ee84d83a014567902ce8ee9b3f4f2" + "sha256": "21a2213aa850c55e5eace4cd10b72b958d7ee84d83a014567902ce8ee9b3f4f2", + "upstream_pin": "head:ef1cc26e1e9a08c11cf382de948ee433bebab16d:research/delimited-continuation-stack/stack.py" }, { - "path": "research/delimited-continuation-stack/adapter.py", + "path": "research/continuation-output-return/vendor/adapter.py", "usage": "provenance", - "pin": "head:ef1cc26e1e9a08c11cf382de948ee433bebab16d:research/delimited-continuation-stack/adapter.py", + "pin": "head:1362d9350b733af1c8a8822e0a013c1ff7de64dc:research/continuation-output-return/vendor/adapter.py", "git_blob": "d860b58c603fc600f95e3413f9230398e9b957b3", - "sha256": "e13823e4124caa4b25050ddd9ac960db59c81e2db369b9ec7b201aca7efbebb8" + "sha256": "e13823e4124caa4b25050ddd9ac960db59c81e2db369b9ec7b201aca7efbebb8", + "upstream_pin": "head:ef1cc26e1e9a08c11cf382de948ee433bebab16d:research/delimited-continuation-stack/adapter.py" } ] }