Repository navigation
Implement a local continuation stack with exact linear cost - #5356
Conversation
|
Independent review (James Reed, with Claude Code). Head Verdict: correct. Restoration is exact at every nesting depth, and the README's exact push/pop formulas hold, under an independent randomized nested harness. HarnessI imported only
Result: 1,360 checks (680 frames), 0 failures. My first harness draft measured nested H and S from the tape's original floor and produced spurious mismatches; correcting that to the frame's own delimiter, which is your definition, made every count exact. The registered replay passes locally ( Comparison with #5364 (same handoff)Both PRs solve PR5329's saved-frame-oracle question with a delimited control tape and unary head headers. For maintainers choosing between them:
Neither dominates. The bills differ in what they charge: here child retirement is a caller obligation, in #5364 it is included. A cross-reference in each README would help whichever one becomes canonical. |
This constructive interface result replaces the saved-frame oracle identified by PR #5329. A delimited control tape locates and erases its own frames, restores all sixteen payload heads and role-presence bits, and returns arbitrary unequal descriptors. The stack reads no saved parent pointer, frame length or absolute origin. Its eighteen-tape, seven-symbol construction works for every finite properly nested call tree under the stated retirement ABI. The complete kappa calculation is unchanged; selected kappa remains 60403/20000000.
Proof and exact invoice, sequential implementation, receipt, and source pins are fixed at reviewed head
ef1cc26e1e9a08c11cf382de948ee433bebab16d. Base and consumed source pins are7c472563474e60185e6ca101a17622133d047e56.With k payload roles, parent extents summing to S, parent head offsets summing to H, descriptor lengths d and q, and A absent roles, the literal push/pop total is
13H + 4S + 31k + 18d + 5q + 2A + 39reads, writes and unit moves. Since H<=S and A<=k, this is linear in current volume and descriptor sizes, independent of ancestor length or depth. Unary offsets are produced by actual head movement; zero has an explicit terminator. The control frame occupiesH + 2k + d + 3symbols. Actual descriptor-size and volume bounds remain premises when absorbing this into a specific node invoice.The source adapter and limits execute the unchanged retained compact and monomial primitives. Its weak-reference registry simulates lexical allocation and is never consulted by push/pop; allocation is still a separate physical obligation. Empty resumed-role release has its own regression. This PR does not implement recursive C, designated child-output delivery, the general descriptor producer, a complete physical allocation controller, or full supplier admission.
From the repository root, with Python 3.12 and the standard library:
Expected marker:
PASS_DELIMITED_CONTINUATION_STACK. Registered normal/optimized CPython 3.12.13 and optimized 3.14.7 checks pass. Evidence covers 1,452 exact small invoices, nesting to depth 31, six complete two-level compact-source cases with all sixteen parent roles occupied, 1,024 actual-recipe phase records and inverse checks, six malformed-state controls, and 32 empty-role lifetime cases. Ancestor lengths 16,257,4096 give identical operation counts in both source layouts. The checker discards the push object and constructs a new stack object before return. Committed-byte checks, the official 17-file export and Git-free optimized replay pass; source and receipt corruption reject. Optional full-history verification was unavailable in the shallow checkout. No full production rectangle, selected cold replay, native compiler, Lean or Docker run is claimed. Hosted CI and independent human or proof-kernel review remain separate.The advance claim takes the released control-stack handoff. Final overlap covered 305 open PRs, 4,634 Discussion records and all 7,267 tracked README/TASK notes. A concurrent claimant released the same scope after finding this earlier claim. Canonical main still matched the base; arbitrary diffs and unpublished work remain outside overlap coverage. No successor scope is reserved by this PR.
Credit @JoyboyBrian for the segment refinement and the PR #5041 locality invoice; @jmbarrancoml (Jose Manuel) for PR #2250's sequential primitives; Douglas Colkitt for guard/repair; Cinna Davis for the caller; @Matarener for the cover/stock lineage. Their roles and retained notices are documented in the pinned predecessor. New stack proof, code and checks: @aliromman with substantial OpenAI Codex assistance. Apache-2.0; author-checked, awaiting independent review.