scripts/validate_theorem_runtime_manifest.py

#!/usr/bin/env python3
"""Validate the A11oy theorem-to-runtime manifest."""

from __future__ import annotations

import argparse
import json
from pathlib import Path


REPO_ROOT = Path.cwd()
MANIFEST = REPO_ROOT / "docs" / "theorem-runtime-manifest.json"
VALID_STATUSES = {
    "verified-runtime",
    "lean-backed-current-green",
    "lean-backed-needs-upstream-ci",
    "lean-backed-needs-runtime",
    "historical-roadmap",
    "roadmap",
}


def main() -> int:
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument("--manifest", default=str(MANIFEST))
    args = parser.parse_args()
    path = Path(args.manifest)
    data = json.loads(path.read_text(encoding="utf-8"))
    errors: list[str] = []

    seen = set()
    for entry in data.get("entries", []):
        entry_id = entry.get("id")
        if not entry_id:
            errors.append("entry missing id")
            continue
        if entry_id in seen:
            errors.append(f"duplicate entry id: {entry_id}")
        seen.add(entry_id)

        status = entry.get("claimStatus")
        if status not in VALID_STATUSES:
            errors.append(f"{entry_id}: invalid claimStatus {status}")

        for field in ["runtimeFile", "exportFile", "testFile"]:
            value = entry.get(field)
            if value and not (REPO_ROOT / value).exists():
                errors.append(f"{entry_id}: missing {field} path {value}")

        if status == "verified-runtime" and not entry.get("validationCommand"):
            errors.append(f"{entry_id}: verified-runtime requires validationCommand")

    if errors:
        print("Theorem runtime manifest failed:")
        for error in errors:
            print(f"  - {error}")
        return 1

    print(f"Theorem runtime manifest OK: {len(seen)} entries")
    return 0


if __name__ == "__main__":
    raise SystemExit(main())