#!/usr/bin/env python3
"""Stand-alone verifier for the IHVRK evidence bundle. ZERO CAIN/IHVRK imports.

Requires: Python 3.8+ only. Standard library only (Ed25519 is verified with the RFC 8032 reference algorithm below).
Run inside the directory that holds MANIFEST.json:

    python3 verify_ihvrk_evidence.py

Checks (each prints PASS / FAIL / SKIP):
  E1  every file listed in MANIFEST.json exists and matches its sha256
  E2  test_results.json totals are internally consistent and show 0 failed / 0 error
  E3  z3_proofs.json: control case SAT, all 15 invariants UNSAT, every sensitivity mutant SAT
  E4  tlc_summary.json: design run complete with no error; each broken variant behaves as expected
  E5  mutation.json: every applied mutant killed
  E6  sample ledger: chain, digests and signed checkpoint verify, re-implemented here from the spec
  E7  the three tampered ledger copies are each REJECTED by the same check

Exit 0 only if no check FAILs. What this does not show: that the code which produced these results is the code
you would deploy (compare MANIFEST.source_commit with the release), or anything about a production deployment.
"""
import base64
import hashlib
import json
import os
import sys

HERE = os.getcwd()
RESULTS = []


def check(name, ok, detail=""):
    RESULTS.append((name, "PASS" if ok is True else ("SKIP" if ok is None else "FAIL"), detail))


def load(name):
    with open(os.path.join(HERE, name), "rb") as f:
        return json.loads(f.read())


# ---- canonical JSON, integer-only RFC 8785 profile (mirrors ihvrk/crypto/canonical_encoding.py spec) -----------
def _esc(s):
    out = ['"']
    for ch in s:
        o = ord(ch)
        if ch == '"':
            out.append('\\"')
        elif ch == "\\":
            out.append("\\\\")
        elif ch in "\b\f\n\r\t":
            out.append({"\b": "\\b", "\f": "\\f", "\n": "\\n", "\r": "\\r", "\t": "\\t"}[ch])
        elif o < 0x20:
            out.append("\\u%04x" % o)
        else:
            out.append(ch)
    return "".join(out) + '"'


def canon(v):
    if v is None:
        return "null"
    if v is True:
        return "true"
    if v is False:
        return "false"
    if isinstance(v, int):
        if abs(v) > 2 ** 53 - 1:
            raise ValueError("int range")
        return str(v)
    if isinstance(v, str):
        return _esc(v)
    if isinstance(v, list):
        return "[" + ",".join(canon(x) for x in v) + "]"
    if isinstance(v, dict):
        ks = sorted(v, key=lambda k: k.encode("utf-16-be", "surrogatepass"))
        return "{" + ",".join(_esc(k) + ":" + canon(v[k]) for k in ks) + "}"
    raise ValueError("type")


def ddigest(domain, value):
    return hashlib.sha256(domain.encode() + b"\x00" + canon(value).encode()).hexdigest()


# ---- Ed25519 verification, RFC 8032 section 5.1.7 (reference algorithm, standard library only) -------------------
_P = 2 ** 255 - 19
_L = 2 ** 252 + 27742317777372353535851937790883648493
_D = -121665 * pow(121666, _P - 2, _P) % _P
_I = pow(2, (_P - 1) // 4, _P)


def _xrecover(y, sign):
    xx = (y * y - 1) * pow(_D * y * y + 1, _P - 2, _P) % _P
    x = pow(xx, (_P + 3) // 8, _P)
    if (x * x - xx) % _P:
        x = x * _I % _P
    if (x * x - xx) % _P:
        return None
    if x == 0 and sign:
        return None
    return _P - x if x & 1 != sign else x


_B = (_xrecover(4 * pow(5, _P - 2, _P) % _P, 0), 4 * pow(5, _P - 2, _P) % _P, 1,
      _xrecover(4 * pow(5, _P - 2, _P) % _P, 0) * 4 * pow(5, _P - 2, _P) % _P)


def _add(a, b):
    A = (a[1] - a[0]) * (b[1] - b[0]) % _P
    B = (a[1] + a[0]) * (b[1] + b[0]) % _P
    C = 2 * a[3] * b[3] * _D % _P
    Dd = 2 * a[2] * b[2] % _P
    E, F, G, H = B - A, Dd - C, Dd + C, B + A
    return (E * F % _P, G * H % _P, F * G % _P, E * H % _P)


def _mul(s, pt):
    q = (0, 1, 1, 0)
    while s:
        if s & 1:
            q = _add(q, pt)
        pt = _add(pt, pt)
        s >>= 1
    return q


def _eq(a, b):
    return (a[0] * b[2] - b[0] * a[2]) % _P == 0 and (a[1] * b[2] - b[1] * a[2]) % _P == 0


def _decode(b):
    if len(b) != 32:
        return None
    y = int.from_bytes(b, "little")
    sign, y = y >> 255, y & ((1 << 255) - 1)
    if y >= _P:
        return None
    x = _xrecover(y, sign)
    return None if x is None else (x, y, 1, x * y % _P)


def ed25519_verify(pub, msg, sig):
    if len(pub) != 32 or len(sig) != 64:
        return False
    A, R = _decode(pub), _decode(sig[:32])
    s = int.from_bytes(sig[32:], "little")
    if A is None or R is None or s >= _L:
        return False
    h = int.from_bytes(hashlib.sha512(sig[:32] + pub + msg).digest(), "little") % _L
    return _eq(_mul(s, _B), _add(R, _mul(h, A)))


def verify_ledger_bytes(data, checkpoints, keys):
    """Return a list of problems; empty = verified. Spec: ihvrk/ledger/append_only_ledger.py docstring."""
    probs = []
    if data and not data.endswith(b"\n"):
        probs.append("torn tail")
    prev, digests = "0" * 64, []
    for i, line in enumerate(data.splitlines()):
        try:
            rec = json.loads(line)
            if canon(rec).encode() != line:
                probs.append("record %d not canonical" % i)
        except ValueError:
            probs.append("record %d unparseable" % i)
            prev = ""
            digests.append("")
            continue
        body = {k: v for k, v in rec.items() if k != "digest"}
        if ddigest("IHVRK/v1/ledger-record", body) != rec.get("digest"):
            probs.append("record %d digest mismatch" % i)
        if rec.get("prev") != prev or rec.get("seq") != i:
            probs.append("record %d chain/seq break" % i)
        prev = rec.get("digest", "")
        digests.append(prev)
    for cp in checkpoints:
        body = {k: v for k, v in cp.items() if k != "signature"}
        if cp.get("alg") != "Ed25519" or cp.get("kid") not in keys:
            probs.append("checkpoint key/alg not trusted")
            continue
        try:
            ok = ed25519_verify(base64.b64decode(keys[cp["kid"]], validate=True),
                                b"IHVRK/v1/ledger-checkpoint\x00" + canon(body).encode(),
                                base64.b64decode(cp["signature"], validate=True))
        except (ValueError, TypeError):
            ok = False
        if not ok:
            probs.append("checkpoint signature invalid")
            continue
        n = cp["count"]
        if n > len(digests):
            probs.append("ledger shorter than checkpoint (rollback/truncation)")
        elif (digests[n - 1] if n else "0" * 64) != cp["head"]:
            probs.append("ledger differs from checkpointed head (rewrite)")
    return probs


def main():
    try:
        man = load("MANIFEST.json")
    except (OSError, ValueError) as e:
        print("FAIL  cannot read MANIFEST.json: %s" % e)
        return 1
    bad = []
    for rel, meta in man["files"].items():
        p = os.path.join(HERE, rel)
        if not os.path.exists(p):
            bad.append(rel + " missing")
        elif hashlib.sha256(open(p, "rb").read()).hexdigest() != meta["sha256"]:
            bad.append(rel + " hash mismatch")
    check("E1 manifest file hashes (%d files)" % len(man["files"]), not bad, "; ".join(bad[:5]))

    try:
        t = load("test_results.json")
        tot = t["totals"]
        consistent = sum(tot.values()) == t["total"] == len(t["cases"])
        check("E2 test results: %(passed)d passed, %(failed)d failed, %(error)d error, %(skipped)d skipped" % tot,
              consistent and tot["failed"] == 0 and tot["error"] == 0 and t["exit_code"] == 0,
              "" if consistent else "totals do not add up")
    except (OSError, KeyError, ValueError) as e:
        check("E2 test results", False, str(e))

    try:
        z = load("z3_proofs.json")
        rows = z["invariants"]
        ok = (z["control_authorize_reachable"] == "SAT" and len(rows) == 15
              and all(r["observed"] == "UNSAT" and r["sensitivity_observed"] == "SAT" for r in rows))
        check("E3 Z3: control SAT, %d invariants UNSAT, sensitivity SAT" % len(rows), ok)
    except (OSError, KeyError, ValueError) as e:
        check("E3 Z3 proofs", False, str(e))

    try:
        tl = load("tlc_summary.json")
        runs = tl["runs"]
        ok = runs.get("design", {}).get("status") == "NO_ERROR" and all(r.get("as_expected") for r in runs.values())
        check("E4 TLC: design NO_ERROR, broken variants as expected (%d runs)" % len(runs), ok,
              ", ".join("%s=%s" % (k, v.get("status")) for k, v in sorted(runs.items())))
    except (OSError, KeyError, ValueError) as e:
        check("E4 TLC summary", False, str(e))

    try:
        m = load("mutation.json")
        check("E5 mutation: %s killed" % m["score"], m["survived"] == 0 and m["applied"] == m["mutants"])
    except (OSError, KeyError, ValueError) as e:
        check("E5 mutation", False, str(e))

    sd = os.path.join(HERE, "sample_ledger")
    try:
        keys = json.load(open(os.path.join(sd, "checkpoint_keys.json")))
        cps = [json.loads(l) for l in open(os.path.join(sd, "checkpoints.jsonl"), "rb").read().splitlines() if l]
        probs = verify_ledger_bytes(open(os.path.join(sd, "ledger.jsonl"), "rb").read(), cps, keys)
        check("E6 sample ledger + signed checkpoint verify", not probs, "; ".join(probs[:3]))
        for name in ("tampered_modified.jsonl", "tampered_deleted.jsonl", "tampered_truncated.jsonl"):
            probs = verify_ledger_bytes(open(os.path.join(sd, name), "rb").read(), cps, keys)
            check("E7 %s is rejected" % name, bool(probs), "; ".join(probs[:2]))
    except (OSError, ValueError, KeyError) as e:
        check("E6/E7 sample ledger", False, str(e))

    for name, status, detail in RESULTS:
        print("%-4s  %s%s" % (status, name, ("   [" + detail + "]") if detail else ""))
    print("source_commit: %s   tree clean at generation: %s" % (man.get("source_commit"),
                                                                 man.get("ihvrk_tree_clean_at_generation")))
    failed = [r for r in RESULTS if r[1] == "FAIL"]
    print("RESULT: %s (%d checks, %d failed)" % ("PASS" if not failed else "FAIL", len(RESULTS), len(failed)))
    return 1 if failed else 0


if __name__ == "__main__":
    sys.exit(main())