verify_single_chain_pop.py

#!/usr/bin/env python3
"""Symbolic certificate for the single-chain pop_green route.

This checks a handwritten algebraic model against pinned source hashes.  It
does not parse OCaml, rerun Rocq, or verify the buffer implementation.
"""
from dataclasses import dataclass
from pathlib import Path
import argparse
import hashlib
import json


Word = tuple[str, ...]


def cat(*parts: Word) -> Word:
    return tuple(x for part in parts for x in part)


def context(left: Word, middle: Word, right: Word) -> Word:
    return cat(left, middle, right)


@dataclass(frozen=True)
class Size:
    constant: int
    variables: tuple[str, ...] = ()

    def minus_one(self) -> "Size":
        assert self.constant >= 1
        return Size(self.constant - 1, self.variables)

    def at_least(self, lower: int) -> bool:
        return self.constant >= lower


SOURCE_HASHES = {
    "lib/cadeque_core.ml":
        "2a7e36a50e9cec5f3cc06226922ab26e039e1fa0dc1188e879e594f320ae003e",
    "theory/Cadeque/Core.v":
        "32340da1cedd75eddee2e3205fee4ae4d99f71e347e807b993d528f3e6f1875f",
    "theory/Cadeque/Types.v":
        "4beb995bd9634c6cc275aa053e009065a7ff699e2ad7b04fd2821df97bcd9e23",
    "theory/Cadeque/Models.v":
        "d19612a21f4e506aedb31657393c437a07d1f2f8e5ed4ebcea4e408d6b05402f",
}


def check_triple_of_chain() -> list[dict]:
    """Check the seven source clauses using independent chain/triple forms."""
    h_l, h_r = ("HL",), ("HR",)
    t_l, t_r = ("TL",), ("TR",)
    rest = ("R",)
    left, right = ("L",), ("Q",)

    tail_applied = context(t_l, rest, t_r)
    body_applied = context(("BL",), tail_applied, ("BR",))
    cases = [
        ("G/Hole", tail_applied, context(t_l, rest, t_r)),
        ("Single_child", context(h_l, body_applied, h_r),
         context(h_l, body_applied, h_r)),
        ("Pair_yellow", context(h_l, cat(body_applied, right), h_r),
         context(h_l, cat(body_applied, right), h_r)),
        ("Pair_orange", context(h_l, cat(left, body_applied), h_r),
         context(h_l, cat(left, body_applied), h_r)),
        ("R/Hole/Only", tail_applied, context(t_l, rest, t_r)),
        ("R/Hole/Left", tail_applied, context(t_l, rest, t_r)),
        ("R/Hole/Right", tail_applied, context(t_l, rest, t_r)),
    ]
    out = []
    for name, chain_word, triple_word in cases:
        assert chain_word == triple_word
        out.append({"case": name, "normal_form": list(chain_word)})
    return out


def check_chain_of_triple() -> list[dict]:
    """Check the six inverse-view clauses, again only at word level."""
    h_l, h_r = ("HL",), ("HR",)
    t_l, t_r = ("TL",), ("TR",)
    rest = ("R",)
    left, right = ("L",), ("Q",)
    tail_applied = context(t_l, rest, t_r)
    body_applied = context(("BL",), tail_applied, ("BR",))
    cases = [
        ("GT", context(t_l, rest, t_r), tail_applied),
        ("YT/Single", context(h_l, body_applied, h_r),
         context(h_l, body_applied, h_r)),
        ("YT/Pair", context(h_l, cat(body_applied, right), h_r),
         context(h_l, cat(body_applied, right), h_r)),
        ("OST", context(h_l, body_applied, h_r),
         context(h_l, body_applied, h_r)),
        ("OPT", context(h_l, cat(left, body_applied), h_r),
         context(h_l, cat(left, body_applied), h_r)),
        ("RT", context(t_l, rest, t_r), tail_applied),
    ]
    out = []
    for name, triple_word, chain_word in cases:
        assert chain_word == triple_word
        out.append({"case": name, "normal_form": list(chain_word)})
    return out


def check_pop_cases() -> list[dict]:
    """Check exhaustive typed green-only cases and their size transitions."""
    # X is deliberately a multi-token arbitrary block: one stored value need
    # not flatten to one payload letter.
    x, p, child, suffix = ("X0", "X1"), ("P",), ("C",), ("S",)
    cases = [
        # name, tc, nc, child shape, input prefix, output node coloring,
        # residual components
        ("GT/Only_end/empty", "GT", "Only_end", "Empty",
         Size(1), "empty", ()),
        ("GT/Only_end/nonempty", "GT", "Only_end", "Empty",
         Size(2, ("q",)), "Only_end", p),
        ("GT/GN", "GT", "GN", "Nonempty",
         Size(8, ("qp",)), "YN", cat(p, child, suffix)),
        ("YT/YN/Single", "YT", "YN", "Single",
         Size(7, ("qp",)), "ON/OST", cat(p, child, suffix)),
        ("YT/YN/Pair", "YT", "YN", "Pair",
         Size(7, ("qp",)), "ON/OPT", cat(p, child, suffix)),
        ("OST/ON", "OST", "ON", "Single",
         Size(6, ("qp",)), "RN/RT", cat(p, child, suffix)),
        ("OPT/ON", "OPT", "ON", "Pair",
         Size(6, ("qp",)), "RN/RT", cat(p, child, suffix)),
    ]
    minimum_after = {
        "GN": 7, "YN": 6, "ON": 5,
    }
    out = []
    for name, tc, nc, child_shape, input_size, output_shape, residual in cases:
        after = input_size.minus_one()
        if nc in minimum_after:
            assert after.at_least(minimum_after[nc])
        input_word = cat(x, residual)
        output_word = cat(x, residual)
        assert input_word == output_word
        out.append({
            "case": name,
            "input_coloring": f"{tc}/{nc}",
            "child_shape": child_shape,
            "output_shape": output_shape,
            "prefix_min_before": input_size.constant,
            "prefix_min_after": after.constant,
            "normal_form": list(output_word),
        })

    # This table is the inversion result for triple A l only green.  No RT
    # input is possible because RT's result color is red; OST and OPT force
    # child arity one and two, respectively.
    assert [c[0] for c in cases] == [
        "GT/Only_end/empty", "GT/Only_end/nonempty", "GT/GN",
        "YT/YN/Single", "YT/YN/Pair", "OST/ON", "OPT/ON",
    ]
    return out


def check_composition(pop_cases: list[dict]) -> list[dict]:
    out = []
    for case in pop_cases:
        normal = tuple(case["normal_form"])
        # triple_of_chain supplies chain=t; pop supplies t=X+residual;
        # chain_of_triple supplies residual-triple=residual-chain.
        assert normal[:2] == ("X0", "X1")
        out.append({
            "case": case["case"],
            "chain_equation": list(normal),
            "returned_head_block": ["X0", "X1"],
            "residual_chain_block": list(normal[2:]),
        })
    return out


def check_negative_controls() -> list[dict]:
    rejected = []
    x, p, c, s = ("X0", "X1"), ("P",), ("C",), ("S",)
    expected = cat(x, p, c, s)
    mutations = {
        "retain_popped_head": cat(x, x, p, c, s),
        "swap_child_suffix": cat(x, p, s, c),
        "reverse_pair_yellow_children":
            context(("HL",), cat(("Q",), ("BL", "R", "BR")), ("HR",)),
    }
    mutation_expected = {
        "retain_popped_head": expected,
        "swap_child_suffix": expected,
        "reverse_pair_yellow_children":
            context(("HL",), cat(("BL", "R", "BR"), ("Q",)), ("HR",)),
    }
    for name, actual in mutations.items():
        assert actual != mutation_expected[name]
        rejected.append({"mutation": name, "reason": "word normal forms differ"})

    # A color transition can be semantically invisible yet ill-typed.
    gn_after_pop = Size(7, ("qp",))
    assert not gn_after_pop.at_least(8)
    rejected.append({
        "mutation": "keep_GN_after_pop",
        "reason": "word may agree, but GN requires a prefix of at least 8 entries",
    })
    return rejected


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--source", type=Path)
    args = parser.parse_args()

    checked = {}
    if args.source:
        for name, expected in SOURCE_HASHES.items():
            actual = hashlib.sha256((args.source / name).read_bytes()).hexdigest()
            assert actual == expected, f"source drift: {name}"
            checked[name] = actual

    forward = check_triple_of_chain()
    backward = check_chain_of_triple()
    pop_cases = check_pop_cases()
    composition = check_composition(pop_cases)
    negative = check_negative_controls()
    print(json.dumps({
        "scope": (
            "Exact symbolic word equations and handwritten indexed branch "
            "closure for triple_of_chain, pop_only_green, chain_of_triple, "
            "and the Single arm of pop_green. Source files are hash-pinned. "
            "This is not OCaml extraction, buffer verification, a Rocq rerun, "
            "or a certificate for pop_pair_green."
        ),
        "source_commit": "503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0",
        "checked_source_hashes": checked,
        "checker_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
        "word_quantifier": (
            "formal blocks admit arbitrary word substitutions; X0,X1 jointly "
            "represent one stored value and need not be one payload letter"
        ),
        "level_quantifier": "every natural nesting level l; erased at runtime",
        "branch_counts": {
            "triple_of_chain": len(forward),
            "pop_only_green_typed_subcases": len(pop_cases),
            "chain_of_triple": len(backward),
            "composed_single_pop": len(composition),
        },
        "triple_of_chain": forward,
        "pop_only_green": pop_cases,
        "chain_of_triple": backward,
        "composed_single_pop": composition,
        "negative_controls": negative,
    }, indent=2))


if __name__ == "__main__":
    main()