verify_indexed_prefix_repair.py

#!/usr/bin/env python3
"""Symbolic model of the prefix-repair clauses under explicit module contracts.

Ranks below denote n+offset for arbitrary n >= 0. Lengths count elements at
that rank, not letters in their flattened words. This is not OCaml extraction.
"""
from dataclasses import dataclass
from pathlib import Path
import argparse
import hashlib
import json


@dataclass(frozen=True)
class Nat:
    constant: int
    variables: tuple = ()

    def __add__(self, other):
        return Nat(self.constant + other.constant,
                   tuple(sorted(self.variables + other.variables)))

    def at_least(self, k):
        # Every listed variable ranges independently over the natural numbers.
        return self.constant >= k


@dataclass(frozen=True)
class Buffer:
    rank: int
    word: tuple
    length: Nat


@dataclass(frozen=True)
class Chain:
    rank: int
    word: tuple


@dataclass(frozen=True)
class Small:
    prefix: Buffer

    def __post_init__(self):
        assert self.prefix.length.at_least(3)

    @property
    def rank(self):
        return self.prefix.rank + 1

    @property
    def word(self):
        return self.prefix.word


@dataclass(frozen=True)
class Big:
    prefix: Buffer
    child: Chain
    suffix: Buffer

    def __post_init__(self):
        assert self.prefix.rank == self.suffix.rank
        assert self.child.rank == self.prefix.rank + 1
        assert self.prefix.length.at_least(3)
        assert self.suffix.length.at_least(3)

    @property
    def rank(self):
        return self.prefix.rank + 1

    @property
    def word(self):
        return self.prefix.word + self.child.word + self.suffix.word


def semi_push(stored, child):
    assert isinstance(stored, (Small, Big)), "expected stored value, not buffer"
    assert stored.rank == child.rank
    return Chain(child.rank, stored.word + child.word)


def semi_concat(left, right):
    assert left.rank == right.rank
    return Chain(left.rank, left.word + right.word)


def inject(prefix, items):
    assert prefix.rank == items.rank
    return Buffer(prefix.rank, prefix.word + items.word,
                  prefix.length + items.length)


def extract_prefix(stored, child, mutation=None):
    # Direct clause transcription, with primitives interpreted by contracts.
    if isinstance(stored, Small):
        return stored.prefix, child
    child = semi_push(Small(stored.suffix), child)
    child = (semi_concat(child, stored.child) if mutation == "swap_concat"
             else semi_concat(stored.child, child))
    return stored.prefix, child


def make_green_prefix(p, p2, child, three, remainder, short, mutation=None):
    # The has3p contract, including its exhaustive short/long partition.
    assert three.rank == remainder.rank == p2.rank == p.rank
    assert three.length == Nat(3)
    assert p2.word == three.word + remainder.word
    assert p2.length == three.length + remainder.length
    assert p.length.at_least(5)
    if short:
        assert not remainder.length.variables
        assert 0 <= remainder.length.constant < 3
        p = inject(p, three)
        return inject(p, remainder), child
    assert remainder.length.at_least(3)
    p = inject(p, three)
    child = semi_push(remainder if mutation == "omit_small" else Small(remainder),
                      child)
    return p, child


def check_case(kind, short_size=None, mutation=None):
    p = Buffer(0, ("P",), Nat(5, ("p",)))
    three = Buffer(0, ("U",), Nat(3))
    short = short_size is not None
    rest = Buffer(0, (() if short_size == 0 else ("V",)) if short else ("R",),
                  Nat(short_size) if short else Nat(3, ("r",)))
    p2 = inject(three, rest)
    tail = Chain(1, ("D",))
    stored = (Small(p2) if kind == "Small" else
              Big(p2, Chain(1, ("T",)),
                  Buffer(0, ("S",), Nat(3, ("s",)))))
    # Independent pre-state contract of pop_green: old = stored followed by tail.
    expected = p.word + stored.word + tail.word
    extracted, child = extract_prefix(stored, tail, mutation)
    newp, newchild = make_green_prefix(p, extracted, child, three, rest,
                                      short, mutation)
    assert newp.rank == 0 and newchild.rank == 1
    assert newp.length.at_least(8)
    assert newp.word + newchild.word == expected, "fringe equation failed"
    return {"stored": kind, "remainder": short_size if short else "3+r",
            "normal_form": list(expected),
            "output_ranks": ["n", "n+1"],
            "prefix_length_lower_bound": newp.length.constant}


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


def main():
    parser = argparse.ArgumentParser()
    parser.add_argument("--source", type=Path)
    args = parser.parse_args()
    cases = [check_case(kind, size) for kind in ("Small", "Big")
             for size in (0, 1, 2, None)]
    negative = []
    for mutation in ("swap_concat", "omit_small"):
        try:
            check_case("Big", None, mutation)
        except AssertionError as e:
            negative.append({"mutation": mutation, "rejected": str(e)})
        else:
            raise AssertionError(f"mutation escaped: {mutation}")
    try:
        Small(Buffer(0, ("V",), Nat(2)))
    except AssertionError:
        negative.append({"mutation": "repackage_two_items",
                         "rejected": "Small requires at least three entries"})
    else:
        raise AssertionError("undersized Small escaped")
    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
    print(json.dumps({
        "scope": "Symbolic equations and rank/occupancy checks for a handwritten "
                 "model of extract_prefix and make_green_prefix under pop/buffer/"
                 "semi-chain contracts. No executable OCaml refinement, general "
                 "indexed-type checker, or proof-assistant verification.",
        "rank_quantifier": "arbitrary natural n; runtime rank counters are not modeled",
        "word_quantifier": "arbitrary substituted word blocks, not sampled letters",
        "source_commit": "503c5d3ff7f9a20bad1cd7a8f8d7abf4e635d3a0",
        "checked_source_hashes": checked,
        "checker_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
        "cases": cases,
        "negative_controls": negative
    }, indent=2))


if __name__ == "__main__":
    main()