Spaces:
Restarting
Restarting
File size: 3,019 Bytes
a6a5d8e 04ad3df a6a5d8e 04ad3df a6a5d8e | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 | #!/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())
|