verify_local_fringe_certificates.py

#!/usr/bin/env python3
"""Check the authored constructor-rule IR, not OCaml or Rocq source.

The companion note proves soundness of this finite procedure. This program
does not prove its own soundness and is not a proof-assistant development.
No finite-word sampling is used to accept an equation.
"""
import hashlib
import itertools
import json
from pathlib import Path


class Rejected(Exception):
    def __init__(self, stage, reason):
        self.stage, self.reason = stage, reason


def require(ok, stage, reason):
    if not ok:
        raise Rejected(stage, reason)


def cat(parts):
    return tuple(itertools.chain.from_iterable(parts))


class Checker:
    def __init__(self, data):
        self.alphabet = set(data["alphabet"])
        self.sorts = data["sorts"]
        self.cons = data["constructors"]
        require(all(isinstance(n, int) and n > 0 for n in self.sorts.values()),
                "signature", "component counts must be positive integers")
        for name, c in self.cons.items():
            require(c["sort"] in self.sorts and
                    all(s in self.sorts for s in c["children"]),
                    "signature", f"unknown sort in {name}")
            require(len(c["meaning"]) == self.sorts[c["sort"]],
                    "signature", f"wrong component count in {name}")
            # Validate interpretation references with distinct symbolic children.
            xs = [tuple((("signature", i, j),) for j in range(self.sorts[s]))
                  for i, s in enumerate(c["children"])]
            self.interpret(name, xs)
        self.productive = set()
        while True:
            new = {c["sort"] for c in self.cons.values()
                   if all(s in self.productive for s in c["children"])}
            if new <= self.productive:
                break
            self.productive |= new
        self.q = max((len(c["children"]) for c in self.cons.values()), default=0)

    def interpret(self, name, xs):
        out = []
        for expr in self.cons[name]["meaning"]:
            pieces = []
            for t in expr:
                if isinstance(t, str):
                    require(t in self.alphabet, "signature", "unknown letter")
                    pieces.append((("letter", t),))
                else:
                    require(isinstance(t, list) and len(t) == 2 and
                            all(type(i) is int and i >= 0 for i in t) and
                            t[0] < len(xs) and t[1] < len(xs[t[0]]),
                            "signature", "invalid child-component reference")
                    pieces.append(xs[t[0]][t[1]])
            out.append(cat(pieces))
        return tuple(out)

    def pattern(self, p, sort, env, depth=0):
        """Return symbolic components, maximum old address, constructor height."""
        require(sort in self.productive, "shape", f"uninhabited sort {sort}")
        if "var" in p:
            require(set(p) == {"var", "sort"} and p["sort"] == sort,
                    "shape", "ill-sorted frontier variable")
            name = p["var"]
            require(name not in env, "shape", "nonlinear/repeated variable")
            v = tuple((("variable", name, j),) for j in range(self.sorts[sort]))
            env[name] = (sort, v)
            return v, depth, 0
        require(set(p) <= {"ctor", "args", "as"} and
                p.get("ctor") in self.cons, "shape", "unknown pattern constructor")
        c = self.cons[p["ctor"]]
        require(c["sort"] == sort and len(p.get("args", [])) == len(c["children"]),
                "shape", "ill-sorted constructor pattern")
        vals, radius, height = [], depth, 1
        for child, s in zip(p["args"], c["children"]):
            v, r, h = self.pattern(child, s, env, depth + 1)
            vals.append(v)
            radius, height = max(radius, r), max(height, h + 1)
        v = self.interpret(p["ctor"], vals)
        if "as" in p:
            require(p["as"] not in env, "shape", "repeated internal-node binding")
            env[p["as"]] = (sort, v)
        return v, radius, height

    def shapes(self, sort, height):
        if height == 0:
            return [("*", sort)]
        ans = []
        for name, c in self.cons.items():
            if c["sort"] != sort or not all(s in self.productive for s in c["children"]):
                continue
            for children in itertools.product(
                    *(self.shapes(s, height - 1) for s in c["children"])):
                ans.append((name, children))
        return ans

    def matches(self, p, shape):
        if "var" in p:
            return True
        return (p["ctor"] == shape[0] and
                all(self.matches(x, y) for x, y in zip(p["args"], shape[1])))

    def spec_expr(self, expr, pre, post):
        out = []
        for t in expr:
            if isinstance(t, str):
                require(t in self.alphabet, "specification", "unknown letter")
                out.append((("letter", t),))
                continue
            require(isinstance(t, dict) and len(t) == 1 and
                    next(iter(t)) in {"pre", "post"},
                    "specification", "invalid specification token")
            kind, ij = next(iter(t.items()))
            vals = pre if kind == "pre" else post
            require(isinstance(ij, list) and len(ij) == 2 and
                    all(type(i) is int and i >= 0 for i in ij) and
                    ij[0] < len(vals) and ij[1] < len(vals[ij[0]]),
                    "specification", "invalid specification reference")
            out.append(vals[ij[0]][ij[1]])
        return cat(out)

    def check(self, op):
        require(all(s in self.productive for s in op["inputs"] + op["outputs"]),
                "shape", "operation uses an uninhabited/unknown sort")
        require(op["rules"], "shape", "no rules")
        prepared, height, radius, allocation = [], 0, 0, 0
        for rule in op["rules"]:
            require(len(rule["patterns"]) == len(op["inputs"]),
                    "shape", "wrong number of input patterns")
            env, pre = {}, []
            for p, s in zip(rule["patterns"], op["inputs"]):
                v, r, h = self.pattern(p, s, env)
                pre.append(v)
                radius, height = max(radius, r), max(height, h)
            for slot in rule["fresh"]:
                require(slot["id"] not in env and slot["ctor"] in self.cons,
                        "shape", "unknown constructor or reused fresh-slot name")
                c = self.cons[slot["ctor"]]
                require(len(slot["args"]) == len(c["children"]),
                        "shape", "wrong fresh arity")
                for a, s in zip(slot["args"], c["children"]):
                    require(a in env and env[a][0] == s, "shape",
                            "ill-sorted, cyclic, or forward fresh reference")
                env[slot["id"]] = (
                    c["sort"], self.interpret(slot["ctor"],
                                              [env[a][1] for a in slot["args"]]))
            require(len(rule["roots"]) == len(op["outputs"]),
                    "shape", "wrong output arity")
            for root, s in zip(rule["roots"], op["outputs"]):
                require(root in env and env[root][0] == s,
                        "shape", "ill-sorted/unknown output root")
            require(rule["tag"] in op["contracts"],
                    "specification", "undeclared output tag")
            post = [env[x][1] for x in rule["roots"]]
            allocation = max(allocation, len(rule["fresh"]))
            prepared.append((rule, pre, post))
        cells = 0
        for roots in itertools.product(*(self.shapes(s, height) for s in op["inputs"])):
            matches = sum(all(self.matches(p, t) for p, t in zip(r["patterns"], roots))
                          for r in op["rules"])
            require(matches == 1, "coverage",
                    f"truncated input cell matches {matches} rules")
            cells += 1
        for key, actual in (("r", radius), ("A", allocation)):
            budget = op["budget"][key]
            require(type(budget) is int and budget >= actual, "resource",
                    f"{key} needs {actual}, declared {budget}")
        equations = []
        for rule, pre, post in prepared:
            for index, equation in enumerate(op["contracts"][rule["tag"]]):
                require(len(equation) == 2, "specification", "not an equation pair")
                lhs = self.spec_expr(equation[0], pre, post)
                rhs = self.spec_expr(equation[1], pre, post)
                require(lhs == rhs, "equation",
                        f'{rule["name"]} equation {index}: {lhs!r} != {rhs!r}')
                equations.append({"rule": rule["name"], "index": index,
                                  "normal_form": lhs})
        return {"status": "accepted", "q_signature": self.q,
                "r": radius, "A": allocation, "coverage_cells": cells,
                "equations": equations}


def main():
    path = Path(__file__).with_name("local-fringe-certificates.json")
    data = json.loads(path.read_text())
    checker = Checker(data)
    reports = []
    for op in data["operations"]:
        try:
            result = checker.check(op)
        except Rejected as exc:
            result = {"status": "rejected", "stage": exc.stage, "reason": exc.reason}
        expected = op["expected"]
        require(result["status"] == expected["status"] and
                ("stage" not in expected or result.get("stage") == expected["stage"]),
                "regression", f'{op["name"]}: {result}, expected {expected}')
        reports.append({"name": op["name"], **result})
    print(json.dumps({
        "scope": "Exact symbolic normalization and finite shape/resource checks "
                 "for the authored constructor-rule JSON only. No OCaml extraction, "
                 "Rocq proof, or complete catenable-deque certificate.",
        "input_sha256": hashlib.sha256(path.read_bytes()).hexdigest(),
        "checker_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
        "reports": reports
    }, indent=2))


if __name__ == "__main__":
    main()