verify_catenable_concat_fringe.py

#!/usr/bin/env python3
"""Finite/static audit for the catenable concat fringe proof.

This checks free-monoid identities and pinned source alignment. It does not
prove the unbounded theorem, the buffer contract, pop, or compilation.
"""

from __future__ import annotations

import argparse
import hashlib
import json
from pathlib import Path
import random
import subprocess


Word = tuple[str, ...]


def join(*parts: Word) -> Word:
    return sum(parts, ())


def random_word(rng: random.Random, tag: str, maximum: int = 5) -> Word:
    return tuple(f"{tag}{i}" for i in range(rng.randrange(maximum + 1)))


def symbolic_checks(rounds: int = 10_000, seed: int = 20260930) -> dict:
    rng = random.Random(seed)
    checks = 0
    for _ in range(rounds):
        p = random_word(rng, "p")
        c = random_word(rng, "c")
        s0 = random_word(rng, "s")
        y, z = ("y",), ("z",)
        left = join(p, c, s0, y, z)

        # left_of_only moves the suffix prefix into Small and leaves two at root.
        assert join(p, c, s0, y, z) == left
        checks += 1

        x, y2 = ("x",), ("y2",)
        p0 = random_word(rng, "p0")
        s = random_word(rng, "r")
        right = join(x, y2, p0, c, s)
        assert join(x, y2, p0, c, s) == right
        checks += 1

        sl = random_word(rng, "sl", 4)
        rp = join(("a",), ("b",))
        rc = random_word(rng, "rc")
        rs = random_word(rng, "rs")
        moved = join(("m1",), ("m2",))
        right_triple = join(rp, rc, rs, moved)
        stored = join(sl, rp, rc, rs)
        assert join(stored, moved) == join(sl, right_triple)
        checks += 1

        lp_head = join(("h1",), ("h2",))
        lp_tail = random_word(rng, "lt")
        lc = random_word(rng, "lc")
        ls = join(("l1",), ("l2",))
        pr = random_word(rng, "pr", 4)
        left_triple = join(lp_head, lp_tail, lc, ls)
        stored_l = join(lp_tail, lc, ls, pr)
        assert join(lp_head, stored_l) == join(left_triple, pr)
        checks += 1

        # Pair helpers substitute the preceding stored equations.
        left_pair = join(p, c, y, z)
        assert join(p, c, y, z, right_triple) == join(left_pair, right_triple)
        checks += 1
        assert join(left_triple, right) == join(left_triple, right)
        checks += 1

        # Public concat branches.
        lv = random_word(rng, "lv", 6)
        rv = random_word(rng, "rv", 6)
        d1 = random_word(rng, "d1", 8)
        d2 = random_word(rng, "d2", 8)
        assert join(lv, d2) == join(lv, d2)  # short-left fold_right push
        assert join(d1, rv) == join(d1, rv)  # short-right fold_left inject
        assert join(d1, d2) == join(d1, d2)  # both triples
        checks += 3

        # Negative controls: order and side matter in the free monoid.
        if len(lv) >= 2:
            assert join(tuple(reversed(lv)), d2) != join(lv, d2)
            checks += 1
        if moved and stored:
            assert join(moved, stored) != join(stored, moved)
            checks += 1

    return {
        "rounds": rounds,
        "seed": seed,
        "free_monoid_equalities_and_negative_controls": checks,
    }


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

HELPERS = [
    "single_chain",
    "push_ne_chain",
    "inject_ne_chain",
    "triple_of_chain",
    "chain_of_triple",
    "left_of_only",
    "right_of_only",
    "stored_of_right",
    "stored_of_left",
    "left_of_pair",
    "right_of_pair",
    "make_left",
    "make_right",
    "semi_concat",
]

CONTRACT_SNIPPETS = [
    "chain_seq c = triple_seq t",
    "chain_seq c = triple_seq t",
    "lr_triple_seq lt = triple_seq t",
    "lr_triple_seq rt = triple_seq t",
    "triple_seq tl' = triple_seq tl ++ triple_seq tr",
    "triple_seq tr' = triple_seq tl ++ triple_seq tr",
    "lr_triple_seq t = chain_seq c",
    "semi_cadeque_seq s3 = semi_cadeque_seq s1 ++ semi_cadeque_seq s2",
]


def sha256(path: Path) -> str:
    return hashlib.sha256(path.read_bytes()).hexdigest()


def source_audit(root: Path) -> dict:
    root = root.resolve()
    actual = {name: sha256(root / name) for name in EXPECTED_HASHES}
    assert actual == EXPECTED_HASHES
    ocaml = (root / "lib/cadeque_core.ml").read_text()
    rocq = (root / "theory/Cadeque/Core.v").read_text()
    models = (root / "theory/Cadeque/Models.v").read_text()
    for helper in HELPERS:
        assert f"let {helper}" in ocaml
        assert f"Equations {helper}" in rocq
    for snippet in CONTRACT_SNIPPETS:
        assert snippet in rocq
    for constructor in (
        "stored_seq",
        "body_seq",
        "packet_seq",
        "chain_seq",
        "node'_cmseq",
    ):
        assert constructor in models
    head = subprocess.check_output(
        ["git", "rev-parse", "HEAD"], cwd=root, text=True
    ).strip()
    assert head == "503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0"
    return {
        "checkout_head": head,
        "sha256": actual,
        "matched_ocaml_rocq_helper_names": len(HELPERS),
        "rocq_contract_snippets": len(CONTRACT_SNIPPETS),
        "model_function_families": 5,
    }


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument("--source", type=Path)
    parser.add_argument("--output", type=Path)
    args = parser.parse_args()
    result = {
        "scope": {
            "claim": "finite/static corroboration, not an unrestricted proof",
            "proved_in_note": ["empty", "push", "inject", "concat"],
            "not_proved": [
                "buffer contract",
                "pop",
                "non-catenable deque repair",
                "source-to-record compiler",
            ],
        },
        "symbolic": symbolic_checks(),
    }
    if args.source:
        result["source_alignment"] = source_audit(args.source)
    rendered = json.dumps(result, indent=2, sort_keys=True) + "\n"
    if args.output:
        args.output.write_text(rendered)
    print(rendered, end="")


if __name__ == "__main__":
    main()