From ef1cc26e1e9a08c11cf382de948ee433bebab16d Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 14:06:52 -0500 Subject: [PATCH] Implement a delimited local continuation stack with exact cost --- .../delimited-continuation-stack/PROOF.md | 135 +++++++++ .../delimited-continuation-stack/README.md | 130 +++++++++ .../delimited-continuation-stack/RESULT.json | 75 +++++ .../delimited-continuation-stack/SOURCES.json | 66 +++++ .../delimited-continuation-stack/TASK.json | 86 ++++++ .../delimited-continuation-stack/VERIFY.json | 43 +++ .../delimited-continuation-stack/adapter.py | 153 ++++++++++ .../delimited-continuation-stack/stack.py | 170 +++++++++++ .../delimited-continuation-stack/verify.py | 263 ++++++++++++++++++ 9 files changed, 1121 insertions(+) create mode 100644 research/delimited-continuation-stack/PROOF.md create mode 100644 research/delimited-continuation-stack/README.md create mode 100644 research/delimited-continuation-stack/RESULT.json create mode 100644 research/delimited-continuation-stack/SOURCES.json create mode 100644 research/delimited-continuation-stack/TASK.json create mode 100644 research/delimited-continuation-stack/VERIFY.json create mode 100644 research/delimited-continuation-stack/adapter.py create mode 100644 research/delimited-continuation-stack/stack.py create mode 100644 research/delimited-continuation-stack/verify.py diff --git a/research/delimited-continuation-stack/PROOF.md b/research/delimited-continuation-stack/PROOF.md new file mode 100644 index 0000000000..5c9310d77e --- /dev/null +++ b/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. diff --git a/research/delimited-continuation-stack/README.md b/research/delimited-continuation-stack/README.md new file mode 100644 index 0000000000..4ef37dbb9e --- /dev/null +++ b/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= 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/delimited-continuation-stack/verify.py b/research/delimited-continuation-stack/verify.py new file mode 100644 index 0000000000..08d1523611 --- /dev/null +++ b/research/delimited-continuation-stack/verify.py @@ -0,0 +1,263 @@ +"""Check the sequential continuation and its retained source boundary. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib +import itertools +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +for row in json.loads((HERE / 'SOURCES.json').read_text())['files']: + if row['usage'] == 'input': + if hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() != row['sha256']: + raise ValueError('source byte drift: ' + row['path']) +SOURCE = ROOT / 'research/complex-segment-boundary' +sys.path[:0] = [str(HERE), str(SOURCE / 'source')] +from stack import BASE, BLANK, END, LEFT, SEP, Counts, Stack, Tape, emit, need, rewind +from adapter import Arena +import streams +import compact +import monomial + + +def bits(n, salt=0): + return tuple((i * 13 + (i // 3) + salt) % 2 for i in range(n)) + + +def snapshot(tape): + cells = list(tape.cells) + while cells and cells[-1] == BLANK: + cells.pop() + return cells, tape.head + + +def load(tape, data, head=0): + for bit in data: + emit(tape, bit) + rewind(tape, LEFT) + for _ in range(head): + tape.move(1) + + +def descriptor(tape, data): + for bit in data: + emit(tape, bit) + rewind(tape, BASE) + + +def formulas(): + options = [(present, s, h) for s in range(4) for h in range(s + 1) + for present in ((False, True) if s == 0 else (True,))] + count = 0 + for roles in itertools.product(options, repeat=2): + for dlen, qlen in itertools.product(range(4), range(3)): + m = Counts() + payload = [Tape(bits(17, i), counts=m) for i in range(2)] + for t, (_, s, h) in zip(payload, roles): + load(t, bits(s), h) + c, d = Tape(bits(19), BASE, m), Tape((), BASE, m) + descriptor(d, bits(dlen)) + before = [snapshot(t) for t in (*payload, c, d)] + stack = Stack(payload, c, d) + s = sum(x[1] for x in roles) + h = sum(x[2] for x in roles) + absent = sum(not x[0] for x in roles) + start = m.total + stack.push([x[0] for x in roles]) + need(m.total - start == 4*h + 2*s + 20 + 7*dlen + absent + 11, 'exact push invoice') + # No Python object from push supplies the return frame. + del stack + descriptor(d, bits(qlen, 1)) + start = m.total + state = Stack(payload, c, d).pop() + need(m.total - start == 9*h + 2*s + 42 + 11*dlen + 5*qlen + absent + 28, 'exact pop invoice') + need(state == list(roles), 'decoded metadata') + need([snapshot(t) for t in (*payload, c, d)] == before, 'all tapes and heads restored') + count += 1 + return count + + +def nested(depth, prefix): + m = Counts() + payload = [Tape(bits(prefix, i), counts=m) for i in range(16)] + c, d = Tape(bits(prefix + 3), BASE, m), Tape((), BASE, m) + expected = [] + for level in range(depth): + roles = [(i % 3 != 0, (i + level) % 7 if i % 3 != 0 else 0) for i in range(16)] + for i, (t, (present, size)) in enumerate(zip(payload, roles)): + load(t, bits(size, level + i), size // 2) + descriptor(d, bits(1 + 2*level, level)) + expected.append(([snapshot(t) for t in (*payload, c, d)], roles)) + Stack(payload, c, d).push([r[0] for r in roles]) + for old, roles in reversed(expected): + state = Stack(payload, c, d).pop() + need([snapshot(t) for t in (*payload, c, d)] == old, 'arbitrary-depth restoration') + need(state == [(p, s, s//2) for p, s in roles], 'arbitrary-depth observer state') + for t in payload: + rewind(t, LEFT) + while t.read() != BLANK: + emit(t, BLANK) + rewind(t, LEFT) + # The next pop retires this current descriptor itself. + return m.total + + +def direct(raw, layout, word): + out = bytearray(len(raw)) + for i in range(layout.records): + j = layout.encode(word.ideal(layout.decode(i), True)) + width = layout.record_bits + out[j*width:(j+1)*width] = raw[i*width:(i+1)*width] + return bytes(out) + + +def bind(arena): + for module in (streams, compact, monomial): + module.Tape = arena.tape + + +def source_case(prefix, late): + a = Arena([bits(prefix, i) for i in range(16)], bits(prefix + 5)) + bind(a) + fields = (('u', 1), ('t', 1)) + ((('y', 2), ('x', 2)) if late else (('x', 2), ('y', 2))) + (('b', 1),) + layout, word = compact.Layout(fields, 8), compact.Compact(1, 1, 1, 0, 'x', 'y', late) + raw = bytes(b for i in range(layout.records) for b in streams.bit_key(i, 8)) + current = a.tape(streams.Meter(), raw) + current.read(7) + other = [a.tape(streams.Meter(), bits(3 + i, i)) for i in range(15)] + for i, role in enumerate(other): + role.read(i % (len(role.data) + 1)) + outer = tuple(bit for byte in (SOURCE / 'BOUNDARY.json').read_bytes() for bit in streams.bit_key(byte, 8)) + a.set_descriptor(outer) + before = [snapshot(t) for t in (*a.payloads, a.control, a.descriptor)] + with a.child(): + try: + current.rewind() + except ValueError as error: + need(str(error) == 'active role', 'suspended role rejection') + else: + raise ValueError('suspended role was accessible') + child = a.tape(streams.Meter(), raw) + child.read(11) + a.set_descriptor(bits(43, 1)) + nested_before = [snapshot(t) for t in (*a.payloads, a.control, a.descriptor)] + with a.child(): + data = a.tape(streams.Meter(), raw) + out = compact.execute(data, layout, word) + need(bytes(out.data) == direct(raw, layout, word), 'nested source endpoint') + out.erase() + a.set_descriptor(bits(17)) + need([snapshot(t) for t in (*a.payloads, a.control, a.descriptor)] == nested_before, 'nested source return') + out = compact.execute(child, layout, word) + need(bytes(out.data) == direct(raw, layout, word), 'source endpoint') + out.erase() + need([snapshot(t) for t in (*a.payloads, a.control, a.descriptor)] == before, 'sixteen source roles and control restored') + need(bytes(current.data) == raw and current.head == 7, 'caller view restored') + return {'prefix': prefix, 'late': late, 'steps': a.counts.total, + 'boundary_steps': a.boundary_steps, 'peak_roles': a.peak} + + +def phase_case(): + recipe = json.loads((SOURCE / 'RIGHT-RECIPE.json').read_text()) + a = Arena([bits(257, i) for i in range(16)]) + bind(a) + class Fibre: + records, record_bits = 1024, 8 + def decode(self, index): + x, y = divmod(index, 2) + return {'v' + str(i): ((x >> i) & 1) | (((y >> i) & 1) << 1) for i in range(9)} + raw = bytes(b for i in range(1024) for b in streams.bit_key((37*i + 19) % 256, 8)) + a.set_descriptor(bits(43)) + with a.child(): + source = a.tape(streams.Meter(), raw) + output = monomial.phase_pass(source, Fibre(), recipe, 2, 1, 0, 4) + expected = bytearray() + for index in range(1024): + phase = 2 * recipe['phase'] + for value in divmod(index, 2): + for i in range(9): + if value >> i & 1: + phase += recipe['linear_Z4'][i] + for j in range(i + 1, 9): + phase += 2*((recipe['quadratic_rows'][i] >> j) & 1)*((value >> j) & 1) + real = sum(raw[index*8+i] << i for i in range(4)) + imag = sum(raw[index*8+4+i] << i for i in range(4)) + for _ in range(phase % 4): + real, imag = -imag, real + expected.extend(streams.bit_key(real % 16, 4)) + expected.extend(streams.bit_key(imag % 16, 4)) + need(bytes(output.data) == bytes(expected), 'actual recipe independent Gaussian oracle') + restored = monomial.phase_pass(output, Fibre(), recipe, 2, 1, 0, 4, True) + need(bytes(restored.data) == raw, 'source phase inverse') + restored.erase() + return {'records': 1024, 'steps': a.counts.total, 'boundary_sha256': hashlib.sha256((SOURCE/'BOUNDARY.json').read_bytes()).hexdigest()} + + +def controls(): + count = 0 + for fault in ('end', 'start', 'unary', 'head', 'child', 'presence'): + p, c, d = Tape(bits(9)), Tape(bits(11), BASE), Tape((), BASE) + load(p, (0, 1), 1) + stack = Stack((p,), c, d) + stack.push([True]) + start = c.floor + 1 + if fault == 'end': c.cells[c.head-1] = BLANK + if fault == 'start': c.cells[start] = SEP + if fault == 'unary': c.cells[start+3] = SEP + if fault == 'head': + c.cells[start+3:start+3] = [1, 1] + c.head += 2 + if fault == 'child': p.write(1) + if fault == 'presence': c.cells[start+1] = 0 + try: + Stack((p,), c, d).pop() + except ValueError: + count += 1 + else: + raise ValueError('accepted fault: ' + fault) + return count + + +def allocation_cases(): + a = Arena([bits(7, i) for i in range(16)]) + for _ in range(32): + parent = a.tape(streams.Meter()) + with a.child(): + child = a.tape(streams.Meter()) + with a.child(): + pass + del child + replacement = a.tape(streams.Meter()) + need(replacement.slot == 0, 'empty resumed role released') + del replacement + del parent + return 32 + + +def main(): + n = formulas() + nesting = [] + for depth in (1, 2, 7, 31): + costs = [nested(depth, prefix) for prefix in (0, 17, 4096)] + need(len(set(costs)) == 1, 'nested cost independent of ancestors') + nesting.append({'depth': depth, 'steps': costs[0]}) + source = [source_case(p, late) for late in (False, True) for p in (16, 257, 4096)] + for offset in (0, 3): + need(len({x['steps'] for x in source[offset:offset+3]}) == 1, 'source cost independent of ancestors') + need(len({x['boundary_steps'] for x in source[offset:offset+3]}) == 1, 'boundary cost independent of ancestors') + result = {'status': 'PASS_DELIMITED_CONTINUATION_STACK', 'exact_invoice_cases': n, + 'nested': nesting, 'source': source, 'phase': phase_case(), 'rejection_controls': controls(), + 'empty_role_lifetime_cases': allocation_cases(), + '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.'} + expected = HERE / 'RESULT.json' + if expected.exists(): + need(json.loads(expected.read_text()) == result, 'committed receipt mismatch') + print(json.dumps(result, indent=2)) + + +if __name__ == '__main__': + main()