#!/usr/bin/env python3
"""Verify the saved quorum proof package and optionally rerun Lean."""

from __future__ import annotations

import argparse
import hashlib
import json
import re
import subprocess
import sys
from pathlib import Path


ROOT = Path(__file__).resolve().parent
MANIFEST_PATH = ROOT / "outputs" / "manifest.json"


def sha256(path: Path) -> str:
    digest = hashlib.sha256()
    with path.open("rb") as handle:
        for chunk in iter(lambda: handle.read(1024 * 1024), b""):
            digest.update(chunk)
    return digest.hexdigest()


def fail(message: str) -> None:
    raise SystemExit(f"FAIL: {message}")


def check_saved_package(manifest: dict) -> None:
    for relative, metadata in manifest["files"].items():
        path = ROOT / relative
        if not path.is_file():
            fail(f"missing file: {relative}")
        actual = sha256(path)
        if actual != metadata["sha256"]:
            fail(f"SHA-256 mismatch for {relative}: {actual}")

    source = (ROOT / "QuorumSandwich.lean").read_text(encoding="utf-8")
    forbidden = {
        r"\bsorry\b": "sorry",
        r"\baxiom\b": "axiom declaration",
        r"\bunsafe\b": "unsafe declaration",
        r"\bnative_decide\b": "native_decide compiler trust path",
        r"\bsorryAx\b": "sorryAx",
        r"\bLean\.trustCompiler\b": "Lean.trustCompiler",
    }
    for pattern, label in forbidden.items():
        if re.search(pattern, source):
            fail(f"forbidden proof escape found: {label}")

    expected_names = [item["name"] for item in manifest["theorems"]]
    for name in expected_names:
        if not re.search(rf"\b(?:theorem|example)\s+{re.escape(name)}\b", source):
            fail(f"missing named declaration: {name}")

    saved_output = (ROOT / "outputs" / "lean-check.txt").read_text(encoding="utf-8")
    if "Lean (version 4.30.0" not in saved_output:
        fail("saved output does not identify Lean 4.30.0")
    for name in expected_names:
        expected = f"'{name}' does not depend on any axioms"
        if expected not in saved_output:
            fail(f"saved output is missing: {expected}")

    model = manifest["model"]
    if model["boolean_assignments"] != 2 ** model["signature_variables"]:
        fail("manifest assignment count does not match the Boolean model")


def rerun_lean(manifest: dict, executable: str) -> None:
    completed = subprocess.run(
        [executable, "QuorumSandwich.lean"],
        cwd=ROOT,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.STDOUT,
        check=False,
    )
    if completed.returncode != 0:
        sys.stderr.write(completed.stdout)
        fail(f"Lean exited with {completed.returncode}")

    for item in manifest["theorems"]:
        expected = f"'{item['name']}' does not depend on any axioms"
        if expected not in completed.stdout:
            fail(f"live Lean output is missing: {expected}")

    print("Live Lean kernel check: PASS")


def main() -> None:
    parser = argparse.ArgumentParser()
    parser.add_argument(
        "--run-lean",
        action="store_true",
        help="Rerun the proof with the Lean executable on PATH.",
    )
    parser.add_argument("--lean", default="lean", help="Lean executable to use.")
    args = parser.parse_args()

    manifest = json.loads(MANIFEST_PATH.read_text(encoding="utf-8"))
    check_saved_package(manifest)
    print("Saved artifact hashes and claims: PASS")
    print("Static verification is provenance checking, not a replacement for Lean.")

    if args.run_lean:
        rerun_lean(manifest, args.lean)


if __name__ == "__main__":
    main()