verify_pair_chain_pop.py

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

The model uses free word blocks and handwritten indexed branch inventories.
It pins source files by hash but does not parse OCaml or rerun Rocq.
"""
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)


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

    def minus_one(self) -> "Size":
        assert self.constant > 0
        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",
}


HEAD = ("X0", "X1")
P = ("P",)
CHILD = ("C",)
BOUNDARY = (("B",), ("D",), ("E",), ("F",), ("G",), ("H",))
RIGHT_PAIR = (("I",), ("J",))
RIGHT_CHILD = ("R",)
RIGHT_SUFFIX = ("S",)


def six_word() -> Word:
    return cat(*BOUNDARY)


def check_pop_left_green() -> list[dict]:
    """Check every typed green-left case after splitting finite subcases."""
    b, d, e, f, g, h = BOUNDARY
    cases = [
        {
            "case": "GT/EN/exact4",
            "tc": "GT", "nc": "EN", "child": "Empty",
            "before": Size(5), "after": Size(4),
            "input": cat(HEAD, b, d, e, f, g, h),
            "kind": "Six_elements", "residual": six_word(),
        },
        {
            "case": "GT/EN/at_least5",
            "tc": "GT", "nc": "EN", "child": "Empty",
            "before": Size(6, ("q",)), "after": Size(5, ("q",)),
            "input": cat(HEAD, P, g, h),
            "kind": "Ok_pt", "residual": cat(P, g, h),
        },
        {
            "case": "GT/GN", "tc": "GT", "nc": "GN",
            "child": "Nonempty", "before": Size(8, ("q",)),
            "after": Size(7, ("q",)), "input": cat(HEAD, P, CHILD, g, h),
            "kind": "Ok_pt/YT-YN", "residual": cat(P, CHILD, g, h),
        },
        {
            "case": "YT/YN/Single", "tc": "YT", "nc": "YN",
            "child": "Single", "before": Size(7, ("q",)),
            "after": Size(6, ("q",)), "input": cat(HEAD, P, CHILD, g, h),
            "kind": "Ok_pt/OST-ON", "residual": cat(P, CHILD, g, h),
        },
        {
            "case": "YT/YN/Pair", "tc": "YT", "nc": "YN",
            "child": "Pair", "before": Size(7, ("q",)),
            "after": Size(6, ("q",)), "input": cat(HEAD, P, CHILD, g, h),
            "kind": "Ok_pt/OPT-ON", "residual": cat(P, CHILD, g, h),
        },
        {
            "case": "OST/ON", "tc": "OST", "nc": "ON",
            "child": "Single", "before": Size(6, ("q",)),
            "after": Size(5, ("q",)), "input": cat(HEAD, P, CHILD, g, h),
            "kind": "Ok_pt/RT-RN", "residual": cat(P, CHILD, g, h),
        },
        {
            "case": "OPT/ON", "tc": "OPT", "nc": "ON",
            "child": "Pair", "before": Size(6, ("q",)),
            "after": Size(5, ("q",)), "input": cat(HEAD, P, CHILD, g, h),
            "kind": "Ok_pt/RT-RN", "residual": cat(P, CHILD, g, h),
        },
    ]
    minimum_after = {"GN": 7, "YN": 6, "ON": 5}
    result = []
    for case in cases:
        assert case["after"] == case["before"].minus_one()
        if case["nc"] in minimum_after:
            assert case["after"].at_least(minimum_after[case["nc"]])
        assert case["input"] == cat(HEAD, case["residual"])
        result.append({
            "case": case["case"],
            "input_coloring": f'{case["tc"]}/{case["nc"]}',
            "child_shape": case["child"],
            "result_kind": case["kind"],
            "prefix_min_before": case["before"].constant,
            "prefix_min_after": case["after"].constant,
            "normal_form": list(case["input"]),
        })
    assert [case["case"] for case in cases] == [
        "GT/EN/exact4", "GT/EN/at_least5", "GT/GN",
        "YT/YN/Single", "YT/YN/Pair", "OST/ON", "OPT/ON",
    ]
    return result


def check_only_of_right() -> list[dict]:
    """Check the ending and nonempty right-triple splice cases."""
    i, j = RIGHT_PAIR
    six = six_word()
    typed = [
        ("GT/EN", "Empty", "Only_end"),
        ("GT/GN", "Nonempty", "Only/GN"),
        ("YT/YN/Single", "Single", "Only/YN"),
        ("YT/YN/Pair", "Pair", "Only/YN"),
        ("OST/ON", "Single", "Only/ON"),
        ("OPT/ON", "Pair", "Only/ON"),
    ]
    result = []
    for coloring, child_shape, output in typed:
        if coloring == "GT/EN":
            right = cat(i, j, RIGHT_SUFFIX)
            converted = cat(six, i, j, RIGHT_SUFFIX)
        else:
            right = cat(i, j, RIGHT_CHILD, RIGHT_SUFFIX)
            converted = cat(six, i, j, RIGHT_CHILD, RIGHT_SUFFIX)
        assert converted == cat(six, right)
        result.append({
            "case": coloring,
            "child_shape": child_shape,
            "output_shape": output,
            "prefix_entries_constructed": 8,
            "normal_form": list(converted),
        })
    return result


def check_pair_composition() -> list[dict]:
    """Compose the view equations in the two pop_pair_green result arms."""
    right = cat(*RIGHT_PAIR, RIGHT_CHILD, RIGHT_SUFFIX)
    six = six_word()

    # Boundary arm: left = head + six; fused residual = six + right.
    left_boundary = cat(HEAD, six)
    input_boundary = cat(left_boundary, right)
    output_boundary = cat(HEAD, six, right)
    assert input_boundary == output_boundary

    # Residual arm: left = head + L'; pair the residual left with right.
    left_residual = ("L0", "L1")
    left_ok = cat(HEAD, left_residual)
    input_ok = cat(left_ok, right)
    output_ok = cat(HEAD, left_residual, right)
    assert input_ok == output_ok

    return [
        {
            "case": "Six_elements_then_only_of_right",
            "normal_form": list(input_boundary),
            "returned_head_block": list(HEAD),
            "residual_chain_block": list(cat(six, right)),
        },
        {
            "case": "Ok_pt_then_Pair",
            "normal_form": list(input_ok),
            "returned_head_block": list(HEAD),
            "residual_chain_block": list(cat(left_residual, right)),
        },
    ]


def check_negative_controls() -> list[dict]:
    i, j = RIGHT_PAIR
    six = six_word()
    right = cat(i, j, RIGHT_CHILD, RIGHT_SUFFIX)
    expected_boundary = cat(HEAD, six, right)
    expected_ok = cat(HEAD, ("L0", "L1"), right)
    mutations = {
        "right_before_six": cat(HEAD, right, six),
        "reverse_six": cat(HEAD, *reversed(BOUNDARY), right),
        "swap_residual_left_and_right": cat(HEAD, right, ("L0", "L1")),
        "retain_popped_head": cat(HEAD, HEAD, six, right),
    }
    expected = {
        "right_before_six": expected_boundary,
        "reverse_six": expected_boundary,
        "swap_residual_left_and_right": expected_ok,
        "retain_popped_head": expected_boundary,
    }
    result = []
    for name, actual in mutations.items():
        assert actual != expected[name]
        result.append({"mutation": name, "reason": "word normal forms differ"})

    # After popping a five-entry EN prefix, four entries cannot form another
    # Left node, whose prefix minimum is five.  The six-element boundary is
    # therefore a type obligation, not merely a convenient source branch.
    assert not Size(4).at_least(5)
    result.append({
        "mutation": "keep_Left_EN_after_exact4",
        "reason": "residual prefix has 4 entries, below the Left minimum 5",
    })
    result.append({
        "mutation": "omit_adapt_to_prefix",
        "reason": (
            "the constructed Only prefix has 8 entries, but an arbitrary "
            "Right-node phantom prefix index is not evidence for that size"
        ),
    })
    return result


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

    left = check_pop_left_green()
    splice = check_only_of_right()
    composed = check_pair_composition()
    negative = check_negative_controls()
    print(json.dumps({
        "scope": (
            "Exact free-word equations and handwritten indexed branch closure "
            "for pop_left_green, only_of_right, and the Pair arm of "
            "pop_green, reusing the previously certified sequence-preserving "
            "view conversions. Source files are hash-pinned. This is not "
            "OCaml extraction, buffer verification, or a Rocq rerun."
        ),
        "source_commit": "503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0",
        "checked_source_hashes": checked,
        "checker_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
        "level_quantifier": "every natural nesting level l; erased at runtime",
        "word_quantifier": (
            "every symbol names an arbitrary word block; X0,X1 jointly "
            "represent one stored entry rather than two payload letters"
        ),
        "branch_counts": {
            "pop_left_green_typed_subcases": len(left),
            "only_of_right_typed_subcases": len(splice),
            "pop_pair_green_result_arms": len(composed),
        },
        "pop_left_green": left,
        "only_of_right": splice,
        "pop_pair_green": composed,
        "negative_controls": negative,
    }, indent=2))


if __name__ == "__main__":
    main()