Implement a local continuation stack with exact linear cost

research/delimited-continuation-stack/PROOF.md

@@ -0,0 +1,135 @@
+# Sequential stack proof and invoice
+
+## Alphabet and entry state
+
+The alphabet has binary symbols 0 and 1, LEFT, SEP, END, BASE and BLANK.
+Payload tapes use only binary data, LEFT and BLANK. The control tape uses
+BASE at its initial top boundary. A complete older frame ends in END. The
+descriptor tape has BASE immediately before its word. The initial dirty
+prefixes may be arbitrary; none of the routines must inspect them.
+
+Fix k. Role i has word x_i of length s_i and head h_i, with 0<=h_i<=s_i.
+If its presence bit is zero, x_i is empty and h_i=0. The entry head is
+immediately after the first h_i data cells. The payload is contiguous and
+the first cell after it is BLANK. Let H=sum h_i, S=sum s_i and let A count
+absent roles. The parent descriptor has length d. The child descriptor has
+length q when pop begins. Recursive work must retire its payloads and put
+their heads at their current origins before pop. That retirement is child
+work; the source adapter executes and charges it explicitly.
+
+## Push invariant
+
+Push first emits LEFT on the control tape. For each role it emits its presence
+bit, moves the payload head left until LEFT, and emits one unary 1 for each
+crossed binary cell. It then emits 0. There are exactly h_i such binary cells.
+The payload head moves right to the origin, scans the unchanged word to BLANK,
+writes LEFT at that end, and moves right once. The child segment is empty.
+No prefix cell to the left of the previous LEFT is read or written.
+
+The role record is therefore `presence 1^h_i 0`. Push emits SEP, copies each
+descriptor bit to the control tape while clearing the descriptor tape, returns
+its descriptor head to the origin, and emits END. The control head is now at
+the blank cell after END. The frame length is
+
+    L = H + 2k + d + 3.
+
+No extent, origin, frame length or parent reference is saved. The unary header
+is produced by the payload head's actual unit moves. Empty head offsets have
+an explicit 0 terminator; zero never has a missing representation.
+
+## Pop invariant
+
+Pop clears the current child descriptor and rewinds that tape to BASE. From
+the free control top, it moves left, checks END, and continues left to LEFT.
+Neither a role record nor a descriptor can contain LEFT, so this is exactly
+the current frame start. SEP is distinct from all binary header/descriptor
+symbols. BASE before a frame start is rejected; it is not crossed.
+
+Pop clears the frame as it parses it. For each role, it checks the empty child
+origin, moves left to the child delimiter and erases it. It moves left through
+the unchanged parent word until its previous LEFT, then right to its origin.
+For each 1 in the saved unary offset it checks a binary payload cell and moves
+right once. The terminating 0 ends the offset. Thus the final physical head
+is exactly the old head. An excessive offset reaches BLANK and is rejected.
+The parsed presence bit restores the finite role bitmap. An absent role must
+be empty. The recorded size and offset counters in the simulator are observers;
+the physical motion does not depend on those integer values.
+
+After k roles, pop checks SEP. It copies the saved descriptor back to its tape
+and clears each control cell. END terminates that copy. After clearing END,
+pop walks left across the now blank frame until the preceding END or BASE,
+then moves right once. This returns the control head to its exact old free top.
+It rewinds the descriptor head to its BASE. All current frame cells are blank.
+Older complete frames, all parent words and every earlier prefix remain exact.
+
+Push and pop use finite branches on the current symbol and a fixed k-role
+index. Their returned integer observer counts can be omitted without changing
+any tape action. The hardware simulator's absolute head index is a tape-model
+implementation detail; the routines cannot read it or the backing array.
+
+## Composition
+
+The child entry has the same form as the parent entry, with one extra delimiter
+per payload tape and one complete older control frame. Apply the same argument
+at each child. At a leaf, retirement establishes pop's entry condition. Pop
+restores its immediate parent exactly. Induction on any finite properly nested
+call tree gives complete restoration at every return. This proof has no bound
+on depth, ancestor size, descriptor lengths or binary contents. It does require
+the stated lexical ownership and successful child-retirement contract.
+
+## Exact operation count
+
+Every read, write and unit move costs one. Symbol tests and the fixed role
+index are finite control. The following counts refer to the literal routines
+in stack.py, including their explicit checks. H is the sum of offsets from the
+left end, not the sum of distances to the right end.
+
+| Component | Cost |
+| --- | ---: |
+| Push control: L writes, L moves, one initial read | 2L+1 |
+| Push payload sweeps and delimiters | 2H+2S+6k+A |
+| Push descriptor copy, clear and rewind | 5d+4 |
+| Pop child descriptor clear and rewind | 5q+4 |
+| Pop control: find, parse, clear and return | 7L |
+| Pop payload return and head replay | 2S+2H+7k+A |
+| Pop saved descriptor write and rewind | 4d+3 |
+
+For pop control, location takes L reads and L moves. Forward parsing takes
+L-1 reads and L-1 moves. The final backward scan takes L+1 reads and L+1 moves;
+the repeated boundary check is included. Exactly L control cells are cleared.
+These counts give 7L. The descriptor lengths are unrestricted and may differ.
+
+Substitute L to obtain the two exact formulas in README.md. Since H<=S and
+A<=k, their sum is at most 17S+33k+18d+5q+39. No term contains the ancestor
+extent or depth. A frame retains L control cells and k payload delimiters.
+The descriptor tape is reused at every level. The deepest live prefix therefore
+uses the sum of the live frame lengths, with no per-depth tape allocation.
+
+This result supplies a local linear boundary, not a full recursion-space
+theorem. To absorb it into a concrete caller one must still prove bounds for
+the sum of active payload and descriptor sizes. No geometric reserve estimate
+can be substituted for those implementation premises without proof.
+
+## Retained source boundary
+
+The source adapter implements the retained local Tape operations by actual
+unit reads, writes and moves. Its byte snapshot is used only by checkers.
+The local size and head counters are obtained from current operations and
+from the observer counts of the just-decoded physical frame. They do not save
+an ancestor origin or choose a return address. A weak-reference registry models the predecessor's lexical lifetime premise.
+Its live-handle keys are depth and slot. It is consulted only for allocation,
+never for push/pop, and is neither serialized nor recovered by pop. The registry
+is a simulator oracle for allocation, not a proved physical allocator. This interface is for properly scoped source
+handles, not arbitrary stale-handle reuse or a new dynamic allocator.
+
+Each source primitive's sequential call trace is therefore interpreted on the
+current segment. Its new delimiter checks add constant work per crossed cell.
+Its original mathematical endpoint and physical controller premises remain
+inherited. The finite source tests exercise compact repair, ordinary fallback,
+radix work and the actual right-recipe phase under nested suspension. They do
+not establish the general allocation schedule, full affine payload rectangle,
+recursive C output, or a selected supplier admission.
+
+The new proof and code are by Ali Romman with substantial OpenAI Codex
+assistance. The source interface and all predecessor mathematics retain the
+credit and limitations in README.md and the unchanged source notices.

research/delimited-continuation-stack/README.md

@@ -0,0 +1,130 @@
+# Delimited continuation without a saved-frame oracle
+
+This package replaces the missing control-stack operation in
+`research/complex-segment-boundary`. A fixed set of sixteen payload tapes,
+one control tape and one descriptor tape supports every finite nesting depth.
+The return routine finds the frame and the parent payload delimiters by unit
+moves. It does not read a saved frame length, parent pointer or absolute origin.
+The generic stack uses a seven-symbol alphabet. Its tape count is eighteen
+at every depth.
+
+This is a constructive interface result, not a complete recursive caller or
+a new kappa. The selected value remains 60403/20000000. The physical child C,
+delivery of its designated output, descriptor producer and source role
+allocation remain separate obligations. The new result closes Open next
+question 3 of the retained segment package. It does not close its other three
+questions.
+
+## Contract and result
+
+Each payload tape has an arbitrary untouched ancestor prefix, a left delimiter,
+a contiguous binary current word and a head within that word or at its right
+end. An absent role is empty. The descriptor is an arbitrary finite binary word
+on its own tape. The control head is at its free top. These are entry conditions,
+not a promise to locate a remote initial origin for free.
+
+Push writes a frame containing a presence bit and a unary head offset for each
+role, then a separator, the opaque descriptor and an end marker. It discovers
+the current extent by scanning that word. It inserts one payload delimiter at
+each current end and clears the descriptor tape. Pop requires child payloads
+to be empty at their new origins. It clears the current child descriptor,
+finds the frame start, decodes it, removes each child delimiter, finds each
+parent delimiter, restores the saved heads and reconstructs the descriptor.
+It erases the entire current frame and finds the preceding control top.
+
+Let k be the fixed payload-role count, S the sum of current payload extents,
+H the sum of current head offsets, d the parent descriptor length, q the child
+descriptor length at pop, and A the number of absent roles. In the stated
+unit model, every read, write and unit move costs one. The exact boundary bill is
+
+    push = 4H + 2S + 10k + 7d + A + 11
+    pop  = 9H + 2S + 21k + 11d + 5q + A + 28
+    total = 13H + 4S + 31k + 18d + 5q + 2A + 39
+          <= 17S + 33k + 18d + 5q + 39.
+
+The live control frame has H+2k+d+3 symbols. Thus both time and live additional
+space are O(S+d+q+k), independent of ancestor extent and nesting depth. Unary
+headers trade compact metadata for a linear current-volume bound. If the
+actual caller proves S,d,q=O(V polylog(p)), this boundary fits its proposed
+O(V e^(1-a2) polylog(p)) node allowance for e>=1 and 0<a2<1, with the polynomial
+log factor adjusted as needed. This conditional absorption does not prove
+that caller's descriptor-size or payload-volume premises.
+
+`PROOF.md` gives the invariant, induction and full count. `stack.py` is the
+sequential routine. Its only persistent fields are the physical tapes.
+The sizes and heads returned by pop are observer counts for the source adapter:
+they do not choose a branch, address or movement in the return routine.
+
+## Source use and evidence
+
+`adapter.py` lets the unchanged retained `streams.py`, `compact.py` and
+`monomial.py` execute through current segments. Push and pop never consult its weak-reference allocation registry. The registry
+records live handles by depth and slot so an empty role can be released after
+return. It supplies no payload bytes, head, origin, descriptor or frame length.
+A resumed source handle names its fixed slot. This is not a new physical allocator or a
+general API for stale handles. The source's proper lexical lifetimes and fixed
+sixteen-role bound remain premises. Array snapshots and byte views belong only
+to the test oracle; the source algorithms use the local size and sequential
+read/write/rewind/erase interface.
+
+All inputs are pinned to canonical main
+`7c472563474e60185e6ca101a17622133d047e56` in `SOURCES.json`. The predecessor
+retains the earlier PR2250 source and the provisional event8814/family65689
+descriptor. That historical descriptor is used as opaque payload here; this
+package does not recertify the full dispatcher/cover/rho chain.
+
+The checker covers 1,452 complete small push/pop invoices, with absent roles,
+empty heads and unequal descriptors. It constructs a new Stack object before
+return, so the push object cannot supply saved return state. Twelve nested
+cases cover depths 1,2,7,31 and ancestor lengths 0,17,4096. Six source cases
+park all sixteen parent roles, execute unchanged compact calls at two nested
+levels in both source layouts, and compare exact outputs to an independent
+address oracle. Ancestor lengths 16,257,4096 have identical cost. The actual
+right-recipe phase is checked on 1,024 addresses against Gaussian arithmetic,
+including its inverse. Six controls reject a missing end, missing start,
+bad unary terminator, out-of-range head, unretired child and false absence.
+
+From the repository root, with Python 3.12 and the standard library:
+
+```sh
+python3 -I -W error -B research/delimited-continuation-stack/verify.py
+python3 -I -O -W error -B research/delimited-continuation-stack/verify.py
+python3 -B scripts/research_package.py --package research/delimited-continuation-stack
+```
+
+Expected marker: `PASS_DELIMITED_CONTINUATION_STACK`. The committed receipt
+must match the full calculated result. Source byte hashes are checked before
+import. A generated package export supports replay without Git.
+
+The written induction covers arbitrary finite properly nested successful
+calls in the stated ABI. The finite tests corroborate that proof; they do not
+replace it. The adapter's reduced f=2 compact rectangles and phase fibre are
+not full e=147 production payloads. Initial tape setup, descriptor construction,
+arbitrary stale-handle behavior, complete allocation control, recursive C,
+output delivery, native phase admission, precision, full stock and the complete
+multiplication theorem remain outside scope. No selected cold replay, Lean or
+Docker build is required by this isolated result.
+
+## Open next questions
+
+1. Bind the actual packet's output role to a sequential return transfer before
+   child retirement. This is the remaining data-delivery boundary. Start with
+   the pinned event8814 recipe and one complete reduced active rectangle; its
+   full physical packet order and child contract remain dependencies.
+2. Compile the retained lexical allocation into a finite slot schedule. Start
+   at repair/radix's maximum live cut and remove the weak-reference allocation
+   simulator. The stack proof supplies no new allocation theorem.
+3. Bind an actual descriptor producer and its bit-length bound. The stack treats
+   its bits as input and charges all transport. A general node invoice needs the
+   producer and source-size bounds as well.
+
+## Credit
+
+JoyboyBrian supplied PR5329's segment refinement and explicit stack-oracle gap,
+and PR5041's locality invoice. Jose Manuel/jmbarrancoml supplied PR2250's
+sequential compact/monomial source. Douglas Colkitt supplied the guard and
+repair construction. Cinna Davis supplied the PR4100/4088 caller; Matarener
+supplied the cover/stock lineage. All source notices remain unchanged and are
+declared replay inputs. Ali Romman prepared this stack construction, proof,
+adapter and checks with substantial OpenAI Codex assistance. Apache-2.0.
+This is author-checked evidence, subject to independent review.

research/delimited-continuation-stack/RESULT.json

@@ -0,0 +1,75 @@
+{
+  "status": "PASS_DELIMITED_CONTINUATION_STACK",
+  "exact_invoice_cases": 1452,
+  "nested": [
+    {
+      "depth": 1,
+      "steps": 1246
+    },
+    {
+      "depth": 2,
+      "steps": 2606
+    },
+    {
+      "depth": 7,
+      "steps": 10458
+    },
+    {
+      "depth": 31,
+      "steps": 66355
+    }
+  ],
+  "source": [
+    {
+      "prefix": 16,
+      "late": false,
+      "steps": 1649322,
+      "boundary_steps": 219205,
+      "peak_roles": 16
+    },
+    {
+      "prefix": 257,
+      "late": false,
+      "steps": 1649322,
+      "boundary_steps": 219205,
+      "peak_roles": 16
+    },
+    {
+      "prefix": 4096,
+      "late": false,
+      "steps": 1649322,
+      "boundary_steps": 219205,
+      "peak_roles": 16
+    },
+    {
+      "prefix": 16,
+      "late": true,
+      "steps": 2454050,
+      "boundary_steps": 219205,
+      "peak_roles": 16
+    },
+    {
+      "prefix": 257,
+      "late": true,
+      "steps": 2454050,
+      "boundary_steps": 219205,
+      "peak_roles": 16
+    },
+    {
+      "prefix": 4096,
+      "late": true,
+      "steps": 2454050,
+      "boundary_steps": 219205,
+      "peak_roles": 16
+    }
+  ],
+  "phase": {
+    "records": 1024,
+    "steps": 583318,
+    "boundary_sha256": "41374b4ecf3169b9a205d340eca97e36969e16d1eaf403afe4b13832b243c8e5"
+  },
+  "rejection_controls": 6,
+  "empty_role_lifetime_cases": 32,
+  "push_plus_pop": "13H+4S+31k+18d+5q+2A+39",
+  "scope": "Fixed alphabet control stack and scoped retained-source adapter; source lexical allocation and recursive output delivery remain separate."
+}