"""CAIN-A75-011 offline verifier (rules embedded verbatim). CAIN-A75-011 formal-artifact rules. Standard library only, no CAIN imports: embedded verbatim in the offline verifier.

A formal artifact (proof term, model-checking run or certificate) is claimed to establish a statement. The review
recomputes what the supplied artifact evidence supports:

  binding      the artifact hash, the checker name/version, and the statement are present; the statement hash covers the
               formula and assumptions
  checks       every checker result is "pass"; "unknown" and "fail" are not success
  dependencies every named dependency resolves and is itself certified; a missing or uncertified dependency blocks
  trust base   no placeholders ("sorry"/"admit"); every axiom used is declared; every declared axiom is on the allowed
               standard list; the statement does not smuggle an extra assumption
  claims       every boolean the artifact asserts matches what this review computed

Verdict: CERTIFIED, else UNCERTIFIED with every failing check named. Malformed input is UNCERTIFIED.
This reviews the evidence record. It does not run the checker or re-prove the theorem.
"""
from __future__ import annotations

import hashlib
import json
import re

_ID = re.compile(r"^[A-Za-z0-9_.:\-]{1,80}$")
_HEX = re.compile(r"^[0-9a-f]{64}$")
STANDARD_AXIOMS = {"propext", "Quot.sound", "Classical.choice", "choice", "excluded_middle"}


class Bad(ValueError):
    pass


def statement_hash(statement):
    body = {"formula": statement.get("formula"), "assumptions": sorted(statement.get("assumptions") or [])}
    return hashlib.sha256(json.dumps(body, sort_keys=True, separators=(",", ":"), ensure_ascii=True).encode()).hexdigest()


def evaluate(record):
    checks, summary = [], {"check_results": {}, "axioms": []}

    def c(cid, ok, detail=""):
        checks.append({"id": cid, "ok": bool(ok), "detail": detail})
        return ok

    try:
        if not isinstance(record, dict) or record.get("schema") != "cain42.a75.formal.artifact.v1":
            raise Bad("not a cain42.a75.formal.artifact.v1 record")
        art, st = record.get("artifact"), record.get("statement")
        if not all(isinstance(x, dict) for x in (art, st)):
            raise Bad("artifact and statement must be objects")
        checker = art.get("checker") if isinstance(art.get("checker"), dict) else {}
        c("binding.artifact_hash", isinstance(art.get("sha256"), str) and bool(_HEX.match(art["sha256"])),
          f"artifact {art.get('sha256')!r}")
        c("binding.checker", isinstance(checker.get("name"), str) and bool(checker["name"]) and isinstance(checker.get("version"), str) and bool(checker["version"]),
          f"checker {checker.get('name')!r} {checker.get('version')!r}")
        c("binding.statement", isinstance(st.get("id"), str) and _ID.match(st["id"]) is not None and isinstance(st.get("formula"), str) and bool(st["formula"].strip()),
          "the statement has an id and a formula")
        c("binding.statement_hash", st.get("sha256") == statement_hash(st), "the statement hash covers formula and assumptions")

        results = art.get("checks")
        if not isinstance(results, list) or not results or len(results) > 200:
            raise Bad("artifact.checks must be a non-empty list")
        seen = set()
        for r in results:
            if not isinstance(r, dict) or not isinstance(r.get("name"), str) or not _ID.match(r["name"]):
                raise Bad("a check needs a name")
            if r["name"] in seen:
                raise Bad(f"check {r['name']} appears twice")
            seen.add(r["name"])
            if r.get("result") not in ("pass", "fail", "unknown"):
                raise Bad(f"{r['name']}: result must be pass, fail or unknown")
            c(f"checks.{r['name']}", r["result"] == "pass", f"result {r['result']!r}")
            c(f"checks.{r['name']}.bound", r.get("artifact_sha256") == art["sha256"],
              f"bound to {r.get('artifact_sha256')!r}")
            summary["check_results"][r["name"]] = r["result"]

        deps = record.get("dependencies") if isinstance(record.get("dependencies"), list) else []
        for d in deps:
            if not isinstance(d, dict) or not isinstance(d.get("id"), str) or not _ID.match(d["id"]):
                raise Bad("a dependency needs an id")
            c(f"deps.{d['id']}.resolved", isinstance(d.get("artifact_sha256"), str) and bool(_HEX.match(d["artifact_sha256"])),
              "the dependency artifact is named by hash")
            c(f"deps.{d['id']}.certified", d.get("status") == "CERTIFIED", f"status {d.get('status')!r}")

        tb = record.get("trust_base") if isinstance(record.get("trust_base"), dict) else {}
        sorries = tb.get("sorry_count")
        c("trust_base.no_placeholder", isinstance(sorries, int) and not isinstance(sorries, bool) and sorries == 0,
          f"sorry/admit count {sorries!r}")
        axioms = tb.get("axioms")
        if not isinstance(axioms, list) or not all(isinstance(a, str) and a for a in axioms):
            raise Bad("trust_base.axioms must be a list of axiom names")
        c("trust_base.axioms_declared", len(set(axioms)) == len(axioms), f"{len(axioms)} unique axiom(s)")
        bad = sorted(set(axioms) - STANDARD_AXIOMS)
        c("trust_base.axioms_standard", not bad, f"non-standard: {bad}" if bad else "only the allowed standard axioms")
        summary["axioms"] = sorted(axioms)

        assumed = st.get("assumptions") if isinstance(st.get("assumptions"), list) else []
        declared = tb.get("declared_assumptions") if isinstance(tb.get("declared_assumptions"), list) else []
        c("statement.assumptions_declared", set(assumed) <= set(declared), f"statement assumes {sorted(set(assumed) - set(declared))} not declared")

        claims = record.get("claims") if isinstance(record.get("claims"), dict) else {}
        computed = {
            "verified": all(x["ok"] for x in checks),
            "no_placeholder": sorries == 0,
            "axioms_standard": not bad,
        }
        for k in sorted(claims):
            c(f"claims.{k}", k in computed and claims[k] == computed[k], f"claimed {claims[k]!r}, computed {computed.get(k)!r}")
        summary["computed"] = computed
    except Bad as e:
        checks.append({"id": "input.well_formed", "ok": False, "detail": str(e)})
        return "UNCERTIFIED", checks, summary
    except Exception as e:  # noqa: BLE001
        checks.append({"id": "input.error", "ok": False, "detail": f"{type(e).__name__}: {e}"[:200]})
        return "UNCERTIFIED", checks, summary
    return ("CERTIFIED" if all(x["ok"] for x in checks) else "UNCERTIFIED"), checks, summary


# ---------------------------------------------------------------------------- offline verifier (no CAIN imports)
# Every name below is prefixed _kit_verifier_ / _b64 / _hl / _json / _sys so it cannot shadow a name in the rules above.
import base64 as _b64, hashlib as _hl, json as _json, sys as _sys
_KIT_VERIFIER_GENESIS = _hl.sha256(b"cain42.a75.formal.genesis").hexdigest()


def _kit_verifier_canon(o):
    return _json.dumps(o, sort_keys=True, separators=(",", ":"), ensure_ascii=True).encode()


def _kit_verifier_sha(o):
    return _hl.sha256(_kit_verifier_canon(o)).hexdigest()


def _kit_verifier_main(argv):
    from cryptography.hazmat.primitives.asymmetric.ed25519 import Ed25519PublicKey
    if len(argv) < 2:
        print("usage: verify_offline.py run.json --pinned-key BASE64"); return 2
    run = _json.load(open(argv[1]))
    pin = argv[argv.index("--pinned-key") + 1] if "--pinned-key" in argv else None
    problems, prev, recs = [], _KIT_VERIFIER_GENESIS, run.get("records") or []
    for i, r in enumerate(recs):
        body = {k: v for k, v in r.items() if k not in ("record_hash", "signature_b64")}
        if _kit_verifier_sha(body) != r.get("record_hash"): problems.append(f"record {i}: record_hash does not match")
        if body.get("subject_sha256") != _kit_verifier_sha(body.get("subject")): problems.append(f"record {i}: subject_sha256 does not match")
        if pin and r.get("public_key_b64") != pin: problems.append(f"record {i}: different key than the pinned one")
        try:
            Ed25519PublicKey.from_public_bytes(_b64.b64decode(pin or r.get("public_key_b64"))).verify(
                _b64.b64decode(r.get("signature_b64", "")), str(r.get("record_hash")).encode())
        except Exception:
            problems.append(f"record {i}: signature does not verify")
        if r.get("prev_record_hash") != prev: problems.append(f"record {i}: chain link broken")
        v, checks, _ = evaluate(r.get("subject"))
        if v != r.get("verdict") or checks != r.get("checks"):
            problems.append(f"record {i}: re-running the rules gives {v}, the record says {r.get('verdict')}")
        prev = r.get("record_hash")
    if run.get("run_hash") != _kit_verifier_sha([r.get("record_hash") for r in recs]): problems.append("run_hash does not match")
    for p in problems: print("  -", p)
    if not pin: print("WARNING: no --pinned-key given; the signature was checked against the key inside the file")
    print("VERDICT:", "VERIFIED" if not problems else "TAMPERED OR INVALID", f"(CAIN-A75-011, {len(recs)} record(s), verdicts {run.get('verdicts')})")
    return 0 if not problems else 1


if __name__ == "__main__":
    _sys.exit(_kit_verifier_main(_sys.argv))