#!/usr/bin/env python3 """Finite corroboration only; no determinizer, emptiness solver or proof assistant. The paired update uses a finite cap/buffer and the paired top. An independent oracle stores the two ordinary stack words and re-encodes the expected state. Tuple copying here is a testing convenience, not a runtime complexity claim. """ import itertools import json from pathlib import Path from verify_bounded_stack_skew import encode, decode, source_step def words(n): for k in range(n + 1): yield from itertools.product((0, 1), repeat=k) def observer_action(top, letter): if letter in ("0", "1"): return int(letter) if letter == "x": return 0 if top is None else "pop" if top == 0 else "keep" if letter == "z": return "keep" if top is None else 1 if top == 0 else "pop" if letter == "p": return "pop" if top is not None else "keep" assert letter == "k" return "keep" def paired_encode(B, reference, source): cap, buffer, frames = encode(B, len(reference), source) return cap, buffer, tuple(zip(reference, frames)) def paired_decode(state): cap, buffer, pairs = state return decode((cap, buffer, tuple(frame for _, frame in pairs))) def paired_step(B, state, reference_action, source_action): cap, buffer, pairs = state actual_ref = ("keep" if reference_action == "pop" and not pairs else reference_action) change_ref = 1 if actual_ref in (0, 1) else -1 if actual_ref == "pop" else 0 temporary = source_step(buffer, source_action) change_source = len(temporary) - len(buffer) error = len(buffer) - min(cap, B + 1) + change_source - change_ref if abs(error) > B: return None if change_ref == 1: payload = None if cap >= B + 1: assert len(temporary) >= 2 payload, temporary = temporary[0], temporary[1:] pairs = pairs + ((actual_ref, (cap, payload)),) cap = min(cap + 1, B + 2) elif change_ref == -1: _, (cap, payload) = pairs[-1] pairs = pairs[:-1] if payload is not None: temporary = (payload,) + temporary assert len(temporary) <= 2 * B + 1 return cap, temporary, pairs def local_pair_audit(): counts = {"transitions": 0, "inside": 0, "first_exits": 0, "bottom_noops": 0} # Reference stacks all binary words through height 4, source heights # within B, B=0,1,2; six symbol-sensitive reference commands, four P ops. for B in range(3): for reference in words(4): H = len(reference) for h in range(max(0, H - B), H + B + 1): for source in itertools.product((0, 1), repeat=h): old = paired_encode(B, reference, source) for letter, action in itertools.product("01xzpk", (0, 1, "pop", "keep")): ra = observer_action(reference[-1] if reference else None, letter) new_ref = source_step(reference, ra) new_source = source_step(source, action) actual = paired_step(B, old, ra, action) violation = abs(len(new_ref) - len(new_source)) > B assert (actual is None) == violation assert old == paired_encode(B, reference, source) counts["transitions"] += 1 counts["bottom_noops"] += int(letter == "p" and not reference) if violation: counts["first_exits"] += 1 else: counts["inside"] += 1 assert actual == paired_encode(B, new_ref, new_source) assert paired_decode(actual) == new_source assert tuple(symbol for symbol, _ in actual[2]) == new_ref return counts def valley_operation(phase, stack, letter): if letter == "a": if phase != "build": return None return "build", 0 assert letter == "b" if phase == "grow" or not stack: return "grow", 0 return "fall", "pop" def delayed_valley_audit(): checks = runs = 0 zero_failure = None for n in range(7): for m in range(7): operations = "a" * n + "b" * m for delays in itertools.product((False, True), repeat=len(operations)): reference = source = () ref_phase = src_phase = "build" paired = paired_encode(1, reference, source) for letter, delay in zip(operations, delays): next_ref_phase, ra = valley_operation(ref_phase, reference, letter) next_src_phase, sa = valley_operation(src_phase, source, letter) assert ra == sa and next_ref_phase == next_src_phase for ref_action, src_action in ((ra, "keep" if delay else sa), ("keep", sa if delay else "keep")): reference = source_step(reference, ref_action) source = source_step(source, src_action) paired = paired_step(1, paired, ref_action, src_action) assert paired is not None assert paired == paired_encode(1, reference, source) assert paired_decode(paired) == source assert abs(len(reference) - len(source)) <= 1 if zero_failure is None and abs(len(reference) - len(source)): zero_failure = {"prefix": "a", "choice": "delay first push", "reference_height": 1, "source_height": 0} assert paired_step(0, paired_encode(0, (), ()), 0, "keep") is None checks += 1 ref_phase, src_phase = next_ref_phase, next_src_phase assert source == reference assert len(source) == abs(n - m) assert (not source) == (n == m) runs += 1 return {"n_and_m": [0, 6], "runs_with_all_early_late_choices": runs, "prefix_updates": checks, "B1_passed": True, "B0_witness": zero_failure} def spread_audit(): maximum_diameter = maximum_radius = 0 for length in range(9): heights = set(range(min(length, 2) + 1)) selected = 0 if length == 0 else 1 radius = max(abs(h - selected) for h in heights) diameter = max(heights) - min(heights) assert radius <= diameter <= 2 * radius maximum_diameter = max(maximum_diameter, diameter) maximum_radius = max(maximum_radius, radius) assert (maximum_radius, maximum_diameter) == (1, 2) # Complete all-rejecting unary source with push/keep on every letter. for length in range(13): heights = {0} for _ in range(length): heights |= {h + 1 for h in heights} assert heights == set(range(length + 1)) return {"sharp_factor_two_lengths": [0, 8], "radius": 1, "diameter": 2, "unbounded_family_checked_lengths": [0, 12], "unboundedness_status": "induction in the note, not established by this finite check"} def view(stack, depth): top_first = stack[::-1] return top_first[:depth] + (None,) * max(0, depth - len(stack)) def metric_audit(): stacks = list(words(5)) comparisons = updates = 0 for x, y in itertools.product(stacks, repeat=2): for letter in "01xzpk": fx = source_step(x, observer_action(x[-1] if x else None, letter)) fy = source_step(y, observer_action(y[-1] if y else None, letter)) for m in range(7): if view(x, m + 1) == view(y, m + 1): assert view(fx, m) == view(fy, m) updates += 1 # Bit complement preserves first differing padded position exactly. cx, cy = tuple(1 - b for b in x), tuple(1 - b for b in y) for m in range(7): assert (view(x, m) == view(y, m)) == (view(cx, m) == view(cy, m)) comparisons += 1 return {"control_states": 1, "binary_stack_max_height": 5, "view_depths": [0, 6], "local_modulus_implications": updates, "complement_view_comparisons": comparisons} def main(): result = {"status": "passed", "scope": "Finite corroboration; no formal verification.", "local_pairing": local_pair_audit(), "delayed_valley": delayed_valley_audit(), "intrinsic_spread": spread_audit(), "observation_metric": metric_audit(), "not_implemented": ["VPA determinization", "pushdown emptiness", "arbitrary-machine compiler", "scaffold generation", "proof-assistant verification"]} output = Path(__file__).with_name("stack-observer-output.json") output.write_text(json.dumps(result, indent=2) + "\n") print(json.dumps(result, indent=2)) if __name__ == "__main__": main()