Spaces:
Running
Running
| #!/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", | |
| # staged-advisory: honest, NOT-proven status (SZL Doctrine v11). The gate | |
| # ships enforced:false/severity:warning while its Lean proof is pending, so | |
| # it must never be counted as proven. Honesty semantics enforced below. | |
| "staged-advisory", | |
| } | |
| 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 status == "staged-advisory": | |
| # Honesty guard (SZL Doctrine v11): staged-advisory entries are NOT | |
| # proven. They must self-identify as advisory and carry a caveat so | |
| # they can never be silently promoted into a proven claim. | |
| if entry.get("stagedAdvisory") is not True: | |
| errors.append( | |
| f"{entry_id}: staged-advisory requires stagedAdvisory: true" | |
| ) | |
| if not entry.get("caveat"): | |
| errors.append( | |
| f"{entry_id}: staged-advisory requires a caveat" | |
| ) | |
| if entry.get("leanStatus") in {"proven", "verified", "lean-proven"}: | |
| errors.append( | |
| f"{entry_id}: staged-advisory cannot have leanStatus " | |
| f"{entry.get('leanStatus')!r} (not yet proven)" | |
| ) | |
| 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()) | |