verify_two_sided_catenation.py

#!/usr/bin/env python3
"""Handwritten symbolic obligations, not OCaml extraction or a Rocq rerun."""
import argparse
import hashlib
import json
from pathlib import Path

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


def word(*parts):
    return tuple(x for part in parts for x in part)


def block(name):
    # One stored entry has two formal factors, never implicitly one letter.
    return (name + "0", name + "1")


def push(entry, chain):
    return entry + chain


def inject(chain, entry):
    return chain + entry


def push_vector(v, c):
    for e in reversed(v):
        c = push(e, c)
    return c


def inject_vector(c, v):
    for e in v:
        c = inject(c, e)
    return c


def stored_right(u, a, b, child, suffix, y, z):
    # Transcribes inject2 followed by eject2 and Big construction.
    big_prefix = word(u, a, b)
    big = word(big_prefix, child, suffix)
    return big, (y, z)


def stored_left(x, y, prefix, child, a, b, u):
    big_suffix = word(a, b, u)
    big = word(prefix, child, big_suffix)
    return (x, y), big


def require_stored(prefix_rank, prefix_min, result_rank, child_rank=None, suffix_min=None):
    assert result_rank == prefix_rank + 1, "stored rank must increase by one"
    assert prefix_min >= 3, "stored prefix minimum is three"
    if child_rank is not None:
        assert child_rank == result_rank, "Big child rank mismatch"
        assert suffix_min >= 3, "stored suffix minimum is three"


def require_orange(buffer_min):
    assert buffer_min >= 6, "orange buffer minimum is six"


def run():
    checks = []

    def equation(name, output, expected):
        assert output == expected, name
        checks.append({"case": name, "normal_form": output})

    p, s, c, l, r = map(block, ("P", "S", "C", "L", "R"))
    a, b, x, y, z, u = map(block, ("A", "B", "X", "Y", "Z", "U"))
    for n in range(7):
        v = [block(f"e{i}") for i in range(n)]
        equation(f"small_left_{n}", push_vector(v, r), word(*v, r))
        equation(f"small_right_{n}", inject_vector(l, v), word(l, *v))

    # Only conversions: independent pre-state is P C S' Y Z or X Y P' C S.
    equation("left_of_only", word(p, inject(c, s), y, z), word(p, c, s, y, z))
    equation("right_of_only", word(x, y, push(p, c), s), word(x, y, p, c, s))

    big, tail = stored_right(u, a, b, r, s, y, z)
    equation("stored_of_right", word(big, *tail), word(u, a, b, r, s, y, z))
    front, big = stored_left(x, y, p, l, a, b, u)
    equation("stored_of_left", word(*front, big), word(x, y, p, l, a, b, u))

    for ending in (True, False):
        big, tail = stored_right(z if ending else word(y, z), a, b, r, s, x, u)
        prefix = inject(p, y) if ending else p
        child = big if ending else inject(l, big)
        equation(f"left_pair_{ending}", word(prefix, child, *tail),
                 word(p, () if ending else l, y, z, a, b, r, s, x, u))

        front, big = stored_left(x, y, p, l, z, u, a if ending else word(a, b))
        suffix = push(b, s) if ending else s
        child = big if ending else push(big, r)
        equation(f"right_pair_{ending}", word(*front, child, suffix),
                 word(x, y, p, l, z, u, a, b, () if ending else r, s))

    equation("large_large", word(l, r), word(l, r))

    # Affine minima: all omitted size parameters are arbitrary naturals.
    occupancy = {"Small_after_removing_two": 5-2,
                 "Big_prefix_from_nonempty_plus_pair": 1+2,
                 "Big_suffix_after_removing_two": 5-2,
                 "ending_pair_orange_buffer": 5+1,
                 "side_buffer_after_ending_split": 7-2}
    for key, lower in occupancy.items():
        assert lower >= (6 if "orange" in key else 5 if "ending_split" in key else 3)
    require_stored(0, 5-2, 1)
    require_stored(0, 1+2, 1, 1, 5-2)
    require_orange(5+1)

    failures = []
    bad = r
    for e in (a, b):
        bad = push(e, bad)
    assert bad != word(a, b, r)
    failures.append("left-folding prepend reverses the boundary")
    assert word(r, l) != word(l, r)
    failures.append("swapping large sides changes the word")
    # These are explicit checks of selected typing obligations, not a type checker.
    for label, operation in [
        ("omit stored wrapper", lambda: require_stored(0, 3, 0)),
        ("undersized stored buffer", lambda: require_stored(0, 2, 1)),
        ("omit boundary move to orange buffer", lambda: require_orange(5)),
    ]:
        try:
            operation()
        except AssertionError as error:
            failures.append(label + ": " + str(error))
        else:
            raise AssertionError("negative control accepted: " + label)
    return checks, occupancy, failures


if __name__ == "__main__":
    parser = argparse.ArgumentParser()
    parser.add_argument("source", type=Path)
    args = parser.parse_args()
    for path, digest in HASHES.items():
        assert hashlib.sha256((args.source/path).read_bytes()).hexdigest() == digest, path
    checks, occupancy, failures = run()
    print(json.dumps({
        "scope": "Handwritten symbolic word equations and affine occupancy minima. Written proof supplies exhaustive source branch/color coverage; no automatic OCaml refinement, full type checker, buffer verification or Rocq rerun.",
        "source_commit": "503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0",
        "source_hashes": HASHES,
        "checker_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
        "quantifiers": "Every natural level; arbitrary substituted word blocks; vector lengths zero through six exhaust the fixed shape bound.",
        "word_obligations": checks,
        "affine_occupancy_minima": occupancy,
        "negative_controls": failures,
    }, indent=2))