diff --git a/research/segment-continuation-stack/PROOF.md b/research/segment-continuation-stack/PROOF.md new file mode 100644 index 0000000000..4a89021e16 --- /dev/null +++ b/research/segment-continuation-stack/PROOF.md @@ -0,0 +1,203 @@ +# Delimited continuation primitive + +This is a written all-size proof for `Controller` in `stack.py`, with exact +finite corroboration in `verify.py`. It is not a proof-kernel certificate or +a compilation of the entire retained PR2250 source interpreter. + +## Contract and finite control + +Fix k=16 physical payload tapes. Each has an arbitrary inaccessible ancestor +prefix, a local delimiter `|`, a contiguous binary word of length s_i, and +blanks thereafter. Its head is h_i cells after the start, 0 <= h_i <= s_i. +An absent role has s_i=h_i=0; a present role may also be empty. A 16-bit mask +specifies presence. No alias between any two of the nineteen physical tapes +is allowed. The source/caller supplies this well-formed entry state. + +The remaining three tapes are: + +* `control`, whose head is at the blank just after the current stack top; +* `descriptor`, with its own local `|`, an opaque binary word of length d, + and its head at that word's beginning; +* `reverse`, an empty scratch segment with its head just after its local `|`. + +All bodies have no internal blanks. Initial local markers and tape identity +are entry conditions. There is no supplied absolute position, frame length, +parent pointer, numeric h_i or numeric s_i available to the controller. + +`Controller` uses only current-symbol reads, one-symbol writes, and moves +by +1 or -1. Its other variables are a symbol from a nine-symbol alphabet, +a role index in {0,...,15}, and a mask in {0,...,65535}. Fixed `range(16)` +loops can be unrolled. Helper call depth is fixed and independent of nesting; +the helper return labels can be duplicated at their finitely many call sites. +Thus this is a constructive finite-control program, although we do not emit +a flat transition table or formal compiler certificate. The Python `Tape` +dictionary, integer head, meter and visited-set are simulator internals; +no controller method reads those fields. The syntax check is only a regression +guard on that access boundary, not a proof of finite-state expressibility. + +`push` consumes the current descriptor into the control tape, parks the +payload heads, installs child delimiters and sets the mask to zero. The +caller may perform successful local binary child work, including arbitrarily +many properly nested push/pop pairs. It must preserve the stack and its +payload suspension delimiters and leave reverse scratch empty. At `pop`, +each current child payload has finite size t_i and a head g_i in [0,t_i]; +the current child descriptor has size e and head g_D in [0,e]. All intended +child outputs must already have been delivered: pop erases every child body. + +The postcondition is exact restoration of all parent words, parent physical +head positions, descriptor and its head, mask, older control symbols and +control-head position. Every symbol of this new frame and of child/scratch +work is blank. Visited blank cells are not claimed to be deallocated. + +## Frame grammar and push invariant + +Let H_i=s_i-h_i and H=sum H_i. The appended frame is exactly + +``` +[ descriptor : b_0 u^H_0 ; b_1 u^H_1 ; ... b_15 u^H_15 ; ] +``` + +where b_i is the presence bit. Its length is + +``` +F = d + H + 2k + 3 = d + H + 35. +``` + +The delimiter alphabet is disjoint from the descriptor's binary alphabet. +Zero distance is the empty run of `u`, including an occupied empty role. +There is no ambiguous zero-width binary-integer header. + +The descriptor loop copies each bit forward to control, erases it from the +descriptor tape and moves one cell right on both tapes. At its first blank, +the descriptor tape is blank from its marker to that head. The erased-rewind +loop walks left to `|` and one cell right, so descriptor is empty at its entry +head. It never visits the descriptor's ancestor prefix. + +For role i, after j iterations of its scan, the payload head is at h_i+j +and exactly j `u` marks follow b_i. The parent symbols are only read, never +written. The first blank occurs precisely at j=H_i. Writing `|` there and +moving right establishes an empty child segment. The suffix `;` closes that +role. Consequently the grammar and all child entries hold at the end of push. + +Unary H uses more header space than a binary offset. The relevant bound is +H <= sum s_i: the original local suspension already moves H cells to park +the heads. This representation exchanges logarithmic header space for a +fully local linear construction and inverse. It claims no improved constant +over a compiled binary counter implementation. + +## Cleanup and pop invariant + +For a contiguous local binary word of length t and current head g, `clear` +walks left to the nearest `|`, then right to the first blank while erasing +every bit, then left through those erased blanks to the same marker. It +returns one cell right of the marker. No ancestor symbol left of the marker +is visited. This applies also to t=g=0. Therefore the first part of pop +establishes empty child bodies with their heads at their origins. + +`take` moves the control head one cell left, reads that symbol, erases it +and leaves the head at that cell. After checking `]`, pop handles roles in +reverse order. Each `;` is consumed. The corresponding payload head is one +cell right of the child delimiter, so moving left and erasing that delimiter +leaves the head at the parent's end s_i. For each consumed `u`, the payload +head moves one cell left. All H_i such cells belong to the original binary +parent word. The next symbol is b_i, and the head is now s_i-H_i=h_i. +Restoring b_i into the fixed mask restores the complete role state. Roles +are distinct tapes, so one restoration cannot disturb another. + +After all sixteen roles, the next consumed symbol is `:`. Reading and erasing +descriptor bits backwards until `[` writes the reversed descriptor onto +`reverse`. The beginning marker is consumed, leaving the control head at +exactly its old blank top. No older control symbol is even read. Walking +backward on reverse copies bits forward onto descriptor and erases reverse; +both return to their local origins. The two reversals recover the original +descriptor, including empty and nonpalindromic descriptors. + +This proves one matched push/pop. Induction on a finite properly nested call +tree proves the same invariant at every depth: a successful inner pair +restores the state in which its caller resumes, and the outer pair's proof +then applies. The induction is in the proof, not an allocated runtime frame +or a Python recursion stack in the controller. The external caller schedules +push/pop; its program counter and arbitrary object state are not supplied by +this primitive. + +## Complete action invoice + +Count each symbol read, symbol write (including blank erasure), and unit +move as one action. Comparisons and finite-control updates are represented +by a fixed finite expansion; this is an exact tape-action invoice, not an +exact count of Python instructions or a flat multi-tape transition table. + +`emit` uses three actions and `take` uses three. `rewind` on a word with head +h costs 2h+3; erased rewind from its end costs 2t+3. Thus `clear(t,g)` costs +exactly 2g+5t+7. This includes the tests of the terminal blank and local marker. + +Directly counting every loop, delimiter, failed loop test and rewind gives + +``` +push = 8d + 5H + 9k + 13 +pop = 14d + 5H + 9k + 16 + + sum_i (2g_i + 5t_i + 7) + (2g_D + 5e + 7). +``` + +The standalone reverse-scratch blank test is included in pop. Put +W=sum_i t_i+e. Since g_i<=t_i and g_D<=e, the total satisfies + +``` +push + pop <= 22d + 10H + 25k + 36 + 7W + <= 24d + 12H + 32k + 64 + 8W. +``` + +The latter is the exported conservative `action_bound`. The checker also +compares the measured counts to the sharper two exact formulas, so a broken +meter cannot pass merely because the conservative inequality has slack. +Child computation, producing its descriptor, and delivering a useful child +output have their own bills and are excluded; all child erasure performed by +pop is included in W. No claim is made that arbitrary output delivery is free. + +All these costs are independent of ancestor lengths. If the caller separately +establishes d+sum s_i+W=O(V), the primitive costs O(V). For e_node>=1 and +0= 0, 'left tape boundary') + self._head += direction + self._meter.moves += 1 + self._visited.add(self._head) + + def snapshot(self): + return self._head, tuple(sorted(self._cells.items())) + + +def emit(tape, symbol): + need(tape.read() == BLANK, 'append requires blank') + tape.write(symbol) + tape.move(1) + + +def take(stack): + stack.move(-1) + symbol = stack.read() + stack.write(BLANK) + return symbol + + +def rewind(tape, erased=False): + """Return to the nearest local delimiter, paying every backward move.""" + while True: + tape.move(-1) + symbol = tape.read() + if symbol == LEFT: + tape.move(1) + return + need(symbol == BLANK if erased else symbol in BITS, + 'local rewind alphabet') + + +def clear(tape): + """Erase a contiguous local binary segment from any head in its extent.""" + rewind(tape) + while True: + symbol = tape.read() + if symbol == BLANK: + break + need(symbol in BITS, 'local clear alphabet') + tape.write(BLANK) + tape.move(1) + rewind(tape, erased=True) + + +class Controller: + """Nineteen fixed tapes and a 16-bit live-role mask, at every nesting depth. + + No method accesses the simulator's private cells, head, meter or snapshots. + Role indices, symbols and the mask range over fixed finite sets. The caller + supplies well-formed local segments and properly nested successful calls. + """ + + def __init__(self, payload, control, descriptor, reverse, occupied): + need(len(payload) == ROLES, 'sixteen payload roles') + need(0 <= occupied < 1 << ROLES, 'finite occupancy mask') + self.payload = tuple(payload) + self.control = control + self.descriptor = descriptor + self.reverse = reverse + self.occupied = occupied + + def push(self): + # Entry: control at its blank top, descriptor at its local beginning, + # reverse scratch empty. Descriptor is consumed into the new frame. + emit(self.control, '[') + while True: + symbol = self.descriptor.read() + if symbol == BLANK: + break + need(symbol in BITS, 'binary descriptor') + emit(self.control, symbol) + self.descriptor.write(BLANK) + self.descriptor.move(1) + rewind(self.descriptor, erased=True) + emit(self.control, ':') + for role in range(ROLES): + present = (self.occupied >> role) & 1 + emit(self.control, '1' if present else '0') + tape = self.payload[role] + while True: + symbol = tape.read() + if symbol == BLANK: + break + need(symbol in BITS, 'binary parent payload') + need(present, 'absent role must be empty') + tape.move(1) + emit(self.control, 'u') + tape.write(LEFT) + tape.move(1) + emit(self.control, ';') + emit(self.control, ']') + self.occupied = 0 + + def pop(self): + # Retire current child work first. Any designated child result must + # have been delivered by the caller before this destructive cleanup. + for tape in self.payload: + clear(tape) + clear(self.descriptor) + need(self.reverse.read() == BLANK, 'reverse scratch empty') + need(take(self.control) == ']', 'frame top delimiter') + self.occupied = 0 + for role in reversed(range(ROLES)): + need(take(self.control) == ';', 'role terminator') + tape = self.payload[role] + tape.move(-1) + need(tape.read() == LEFT, 'payload suspension delimiter') + tape.write(BLANK) + symbol = take(self.control) + while symbol == 'u': + tape.move(-1) + need(tape.read() in BITS, 'return distance within parent') + symbol = take(self.control) + need(symbol in BITS, 'role presence flag') + if symbol == '1': + self.occupied |= 1 << role + need(take(self.control) == ':', 'descriptor terminator') + symbol = take(self.control) + while symbol in BITS: + emit(self.reverse, symbol) + symbol = take(self.control) + need(symbol == '[', 'frame beginning delimiter') + # Reverse once more by physical movement, reconstructing forward order. + while True: + self.reverse.move(-1) + symbol = self.reverse.read() + if symbol == LEFT: + break + need(symbol in BITS, 'reverse scratch alphabet') + self.reverse.write(BLANK) + emit(self.descriptor, symbol) + self.reverse.move(1) + rewind(self.descriptor) + + +def action_bound(descriptor_bits, return_distance, child_bits): + """Conservative read/write/unit-move bound for one matched push/pop.""" + need(min(descriptor_bits, return_distance, child_bits) >= 0, 'bound domain') + return 24 * descriptor_bits + 12 * return_distance + 32 * ROLES + 64 + 8 * child_bits diff --git a/research/segment-continuation-stack/verify.py b/research/segment-continuation-stack/verify.py new file mode 100644 index 0000000000..0c7f4b533e --- /dev/null +++ b/research/segment-continuation-stack/verify.py @@ -0,0 +1,372 @@ +"""Exact endpoints, action census, failure controls and retained source exercises.""" +import ast +import itertools +import json +import sys +import weakref +from hashlib import sha256 +from pathlib import Path +from types import ModuleType + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +kernel = ModuleType('stack') +sys.modules[kernel.__name__] = kernel +exec(compile((HERE / 'stack.py').read_bytes(), str(HERE / 'stack.py'), 'exec'), kernel.__dict__) + + +def need(value, message): + if not value: + raise ValueError(message) + + +def authenticate(): + manifest = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + sources = {} + for row in manifest['files']: + if row['usage'] == 'input': + raw = (ROOT / row['path']).read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'source hash: ' + row['path']) + sources[row['path']] = raw + return sources + + +def word(length, seed=0): + return ''.join(str((i * i + i // 3 + seed) % 2) for i in range(length)) + + +def fixture(parent, heads, descriptor, prefix=0, occupied=None, module=kernel): + meter = module.Meter() + payload = [module.Tape(meter, word(prefix, i), row, h) + for i, (row, h) in enumerate(zip(parent, heads))] + control = module.Tape(meter, '[u;01:]' * (prefix // 7)) + desc = module.Tape(meter, word(prefix, 1), descriptor) + reverse = module.Tape(meter, word(prefix, 0)) + mask = (1 << 16) - 1 if occupied is None else occupied + machine = module.Controller(payload, control, desc, reverse, mask) + return meter, machine + + +def snapshot(machine): + return (tuple(t.snapshot() for t in machine.payload), machine.control.snapshot(), + machine.descriptor.snapshot(), machine.reverse.snapshot(), machine.occupied) + + +def install(tape, data, head=0, module=kernel): + for symbol in data: + module.emit(tape, symbol) + module.rewind(tape) + for _ in range(head): + tape.move(1) + + +def exact_actions(d, H, child, child_heads, child_desc, desc_head): + # Derived from the loops in the written proof, independently of the meter. + push = 8 * d + 5 * H + 9 * 16 + 13 + cleanup = sum(2 * h + 5 * len(row) + 7 for row, h in zip(child, child_heads)) + cleanup += 2 * desc_head + 5 * len(child_desc) + 7 + pop = 14 * d + 5 * H + 9 * 16 + 16 + cleanup + return push, pop + + +def run_case(parent, heads, descriptor, child, child_heads, child_desc='', desc_head=0, + prefix=0, occupied=None, module=kernel): + meter, machine = fixture(parent, heads, descriptor, prefix, occupied, module) + before = snapshot(machine) + d, H = len(descriptor), sum(len(row) - h for row, h in zip(parent, heads)) + start = meter.total + machine.push() + pushed = meter.total - start + begin = before[1][0] + frame = ''.join(machine.control._cells[i] for i in range(begin, machine.control._head)) + need(frame == '[' + descriptor + ':' + ''.join( + str((before[-1] >> i) & 1) + 'u' * (len(row) - h) + ';' + for i, (row, h) in enumerate(zip(parent, heads))) + ']', 'literal frame grammar') + need(len(frame) == d + H + 35, 'frame size') + for tape, row, h in zip(machine.payload, child, child_heads): + install(tape, row, h, module) + install(machine.descriptor, child_desc, desc_head, module) + start = meter.total + machine.pop() + popped = meter.total - start + need(snapshot(machine) == before, 'complete restoration') + need((pushed, popped) == exact_actions(d, H, child, child_heads, child_desc, desc_head), + 'exact action invoice') + child_volume = sum(map(len, child)) + len(child_desc) + bound = module.action_bound(d, H, child_volume) + need(pushed + popped <= bound, 'complete linear bound') + for tape in machine.payload + (machine.descriptor, machine.reverse): + need(min(tape._visited) >= prefix, 'no dirty ancestor traversal') + need(min(machine.control._visited) >= begin, 'no prior control-frame traversal') + return {'push': pushed, 'pop': popped, 'bound': bound, 'frame_symbols': len(frame)} + + +def finite_cases(): + count, largest = 0, 0 + descriptors = [''.join(bits) for n in range(4) for bits in itertools.product('01', repeat=n)] + for n in range(5): + for bits in itertools.product('01', repeat=n): + for h in range(n + 1): + for desc in descriptors: + slot = count % 16 + parent, heads = [''] * 16, [0] * 16 + parent[slot], heads[slot] = ''.join(bits), h + child = [word((i + count) % 4, i) for i in range(16)] + child_heads = [(i + count) % (len(row) + 1) for i, row in enumerate(child)] + result = run_case(parent, heads, desc, child, child_heads, + child_desc='100', desc_head=count % 4, + occupied=1 << slot, prefix=count % 4) + largest = max(largest, result['push'] + result['pop']) + count += 1 + masks = [0, (1 << 16) - 1, 0x5555, 0xAAAA] + [1 << i for i in range(16)] + for mask in masks: + run_case([''] * 16, [0] * 16, '', [''] * 16, [0] * 16, occupied=mask) + return {'complete_single_role_cases': count, 'empty_mask_cases': len(masks), + 'largest_boundary_action_count': largest} + + +def nested_case(prefix, depth): + parent = [word(i % 7 + 1, i) for i in range(16)] + heads = [i % (len(row) + 1) for i, row in enumerate(parent)] + meter, machine = fixture(parent, heads, word(17, 2), prefix) + expected = [] # Test oracle only; Controller never receives this list. + totals = [] + for level in range(depth): + expected.append(snapshot(machine)) + start = meter.total + machine.push() + pushed = meter.total - start + for i, tape in enumerate(machine.payload): + row = word((level + i) % 9, i) + install(tape, row, (i + level) % (len(row) + 1)) + machine.occupied = 0xFFFF + install(machine.descriptor, word(43 if level % 2 == 0 else 17, level)) + totals.append([pushed, 0]) + for level in reversed(range(depth)): + start = meter.total + machine.pop() + totals[level][1] = meter.total - start + need(snapshot(machine) == expected[level], 'nested full state restoration') + return totals + + +class SourceView: + """Observer/size facade for unchanged PR2250 source, outside Controller.""" + def __init__(self, role): + self.role = role + def __len__(self): + return self.role.size + def __bytes__(self): + r = self.role + start = r.tape._head - r.head + return bytes(int(r.tape._cells[start + i]) for i in range(r.size)) + + +class SourceRole: + """Calibration facade: source integer sizes/handles are not compiled here.""" + def __init__(self, arena, slot, meter): + self.arena, self.slot, self.meter = arena, slot, meter + self.tape = arena.machine.payload[slot] + self.size = self.head = 0 + @property + def data(self): + return SourceView(self) + def read(self, size): + need(self.arena.active and 0 <= size <= self.size - self.head, 'source read boundary') + result = bytearray() + for _ in range(size): + symbol = self.tape.read() + need(symbol in kernel.BITS, 'source read bit') + result.append(int(symbol)) + self.tape.move(1) + self.head += size + return result + def write(self, data): + need(self.arena.active and self.head == self.size, 'source append boundary') + for bit in data: + need(bit in (0, 1), 'source binary payload') + kernel.emit(self.tape, str(bit)) + self.size += 1 + self.head += 1 + def rewind(self): + need(self.arena.active, 'source arena active') + kernel.rewind(self.tape) + self.head = 0 + def finish(self): + need(self.head == self.size, 'source complete consumption') + def erase(self): + need(self.arena.active, 'source arena active') + kernel.clear(self.tape) + self.head = self.size = 0 + + +class SourceArena: + def __init__(self, machine): + self.machine, self.active = machine, True + self.live = [None] * 16 + self.peak = 0 + def release(self, slot): + if self.active: + self.machine.occupied &= ~(1 << slot) + def tape(self, meter, data=b''): + need(self.active, 'source allocator active') + slot = next((i for i in range(16) if not (self.machine.occupied >> i) & 1), None) + need(slot is not None, 'source fixed role inventory') + need(self.machine.payload[slot].read() == kernel.BLANK, 'source empty allocation') + self.machine.payload[slot].move(-1) + need(self.machine.payload[slot].read() == kernel.LEFT, 'source retired role origin') + self.machine.payload[slot].move(1) + self.machine.occupied |= 1 << slot + role = SourceRole(self, slot, meter) + self.live[slot] = weakref.ref(role, lambda _, i=slot: self.release(i)) + self.peak = max(self.peak, self.machine.occupied.bit_count()) + role.write(data) + role.rewind() + return role + + +def source_cases(sources): + source = ROOT / 'research/complex-segment-boundary/source' + for name in ('streams', 'compact', 'monomial'): + module = ModuleType(name) + sys.modules[name] = module + raw = sources['research/complex-segment-boundary/source/' + name + '.py'] + exec(compile(raw, str(source / (name + '.py')), 'exec'), module.__dict__) + streams, compact, monomial = (sys.modules[name] for name in ('streams', 'compact', 'monomial')) + boundary = json.loads(sources['research/complex-segment-boundary/BOUNDARY.json']) + need(boundary['actual_event']['event_index'] == 8814 and + boundary['actual_event']['family'] == 65689, 'source event binding') + recipe = json.loads(sources['research/complex-segment-boundary/RIGHT-RECIPE.json']) + need(recipe['offset'] == 426 and recipe['phase'] == 1, 'source recipe binding') + results = [] + for late in (False, True): + for prefix in (16, 257, 4096): + parent = [word(i + 1, i) for i in range(16)] + heads = [i // 2 for i in range(16)] + meter, machine = fixture(parent, heads, word(17), prefix) + initial = snapshot(machine) + machine.push() + first = SourceArena(machine) + for m in (streams, compact, monomial): + m.Tape = first.tape + fields = (('u', 1), ('t', 1)) + ((('y', 2), ('x', 2)) if late else + (('x', 2), ('y', 2))) + (('b', 1),) + layout = compact.Layout(fields, 8) + op = 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)) + expected = bytearray(len(raw)) + for i in range(layout.records): + j = layout.encode(op.ideal(layout.decode(i), True)) + expected[j*8:(j+1)*8] = raw[i*8:(i+1)*8] + smeter = streams.Meter() + current = first.tape(smeter, raw) + outer = compact.execute(current, layout, op) + need(bytes(outer.data) == bytes(expected), 'outer retained compact endpoint') + outer.read(7) + install(machine.descriptor, word(43, 1)) + saved = snapshot(machine) + first.active = False + start = meter.total + machine.push() + boundary_actions = meter.total - start + second = SourceArena(machine) + for m in (streams, compact, monomial): + m.Tape = second.tape + inner = compact.execute(second.tape(smeter, raw), layout, op) + need(bytes(inner.data) == bytes(expected), 'inner retained compact endpoint') + second.active = False + start = meter.total + machine.pop() + boundary_actions += meter.total - start + need(snapshot(machine) == saved, 'source outer roles restored after inner work') + first.active = True + need(bytes(outer.data) == bytes(expected) and outer.head == 7, 'source handle calibration') + first.active = False + machine.pop() + need(snapshot(machine) == initial, 'all sixteen parent roles restored') + results.append({'late': late, 'prefix': prefix, 'records': layout.records, + 'inner_boundary_actions': boundary_actions, + 'peak_source_roles': max(first.peak, second.peak)}) + for late in (False, True): + counts = {r['inner_boundary_actions'] for r in results if r['late'] == late} + need(len(counts) == 1, 'source boundary independent of dirty prefix length') + return results + + +def rejected(action, label): + try: + action() + except ValueError: + return label + raise ValueError('control was accepted: ' + label) + + +def controls(): + outcomes = [] + for label, old, new in [('top', ']', ':'), ('row', ';', ':'), ('descriptor', ':', ';')]: + _, m = fixture(['1'] * 16, [0] * 16, '100') + m.push() + index = max(i for i, c in m.control._cells.items() if c == old) + m.control._cells[index] = new + outcomes.append(rejected(m.pop, 'malformed_' + label)) + _, m = fixture([''] * 16, [0] * 16, '100') + m.push() + m.control._cells[m.control._head - 3] = 'u' + outcomes.append(rejected(m.pop, 'excess_return_distance')) + _, m = fixture(['1'] * 16, [0] * 16, '100', occupied=0) + outcomes.append(rejected(m.push, 'absent_nonempty_parent')) + _, m = fixture([''] * 16, [0] * 16, '') + m.descriptor._cells[m.descriptor._head] = 'u' + outcomes.append(rejected(m.push, 'nonbinary_descriptor')) + raw = (HERE / 'stack.py').read_text(encoding='utf-8') + mutations = [ + ('omitted_head_return', ' tape.move(-1)\n', ' pass\n'), + ('wrong_descriptor_bit', 'emit(self.descriptor, symbol)', + "emit(self.descriptor, '1' if symbol == '0' else '0')"), + ('unpaid_moves', 'self._meter.moves += 1', 'self._meter.moves += 0'), + ] + for label, old, new in mutations: + need(raw.count(old) == 1, 'unique mutation site') + module = ModuleType('stack_control_' + label) + sys.modules[module.__name__] = module + exec(compile(raw.replace(old, new), '', 'exec'), module.__dict__) + outcomes.append(rejected(lambda: run_case(['101'] * 16, [1] * 16, '100', + ['10'] * 16, [1] * 16, + child_desc='01', module=module), label)) + return outcomes + + +def finite_control_surface(): + tree = ast.parse((HERE / 'stack.py').read_text(encoding='utf-8')) + controller = next(x for x in tree.body if isinstance(x, ast.ClassDef) and x.name == 'Controller') + for node in ast.walk(controller): + if isinstance(node, ast.Attribute): + need(not node.attr.startswith('_'), 'controller cannot inspect simulator state') + need(not isinstance(node, (ast.ListComp, ast.DictComp)), 'no dynamic frame comprehension') + need(not any(isinstance(n, ast.Attribute) and n.attr in ('append', 'pop', 'snapshot') + for n in ast.walk(controller)), 'no frame list or snapshot oracle') + + +def main(): + sources = authenticate() + finite_control_surface() + finite = finite_cases() + nested = {str(prefix): nested_case(prefix, 7) for prefix in (16, 257, 4096)} + need(nested['16'] == nested['257'] == nested['4096'], 'all-depth calibration locality') + descriptor = ''.join(str((byte >> bit) & 1) for name in ('BOUNDARY.json', 'RIGHT-RECIPE.json') + for byte in sources['research/complex-segment-boundary/' + name] for bit in range(8)) + actual_descriptor = run_case(['101'] * 16, [1] * 16, descriptor, + ['10'] * 16, [1] * 16, child_desc=word(43), prefix=257) + actual_descriptor['descriptor_bits'] = len(descriptor) + result = {'status': 'PASS_DELIMITED_CONTINUATION_PRIMITIVE', 'source_pins': len(sources), + 'finite': finite, 'seven_level_boundary_counts': nested['16'], + 'retained_descriptor_round_trip': actual_descriptor, + 'actual_compact_calibrations': source_cases(sources), 'rejecting_controls': controls(), + 'physical_tapes': 19, 'alphabet_symbols': 9, + 'scope': 'Primitive theorem and exact finite corroboration; source handles/sizes remain ' + 'a calibration facade; no recursive C, child-output delivery or supplier admission.'} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()