#!/usr/bin/env python3
"""Recovery revision: explicit exact checks, canonical generators and row ledger.

Based on the recovered verify_classI_f2_f21.py. The historical source is retained.
No numerical optimization or floating arithmetic is used in proof decisions.
"""
import argparse
from datetime import datetime, timezone
from fractions import Fraction
import hashlib
import json
import math
from pathlib import Path
import platform
import sys
import time

ZERO = (Fraction(0), Fraction(0))
ONE = (Fraction(1), Fraction(0))
PHI = (Fraction(1, 2), Fraction(1, 2))
CERT_SHA = "7b3945ad58b76341bbc22e7812a359f64b61a68d413b2668012dc155803edb5e"


def require(ok, message):
    if not ok:
        raise ValueError(message)


def pair(o):
    require(isinstance(o, dict) and set(o) == {"a", "b"}, "Invalid field pair")
    values = []
    for key in ("a", "b"):
        s = o[key]
        require(isinstance(s, str), "Rational coefficients must be strings")
        f = Fraction(s)
        require(str(f) == s, "Rational coefficient is not in reduced canonical form")
        values.append(f)
    return tuple(values)


def encode(v):
    return {"a": str(v[0]), "b": str(v[1])}


def add(u, v): return (u[0] + v[0], u[1] + v[1])
def sub(u, v): return (u[0] - v[0], u[1] - v[1])
def mul(u, v): return (u[0]*v[0] + 5*u[1]*v[1], u[0]*v[1] + u[1]*v[0])
def scale(u, n): return (u[0]*n, u[1]*n)


def inv(u):
    d = u[0]*u[0] - 5*u[1]*u[1]
    require(d != 0, "Division by zero in Q(sqrt(5))")
    return (u[0]/d, -u[1]/d)


def div(u, v): return mul(u, inv(v))


def power(u, n):
    require(type(n) is int and n >= 0, "Invalid exponent")
    a = ONE
    while n:
        if n & 1:
            a = mul(a, u)
        u = mul(u, u)
        n //= 2
    return a


def sign(u):
    a, b = u
    if b == 0: return (a > 0) - (a < 0)
    if a == 0: return (b > 0) - (b < 0)
    if a > 0 and b > 0: return 1
    if a < 0 and b < 0: return -1
    d = a*a - 5*b*b
    require(d != 0, "Unexpected rational equality with sqrt(5)")
    if a > 0: return 1 if d > 0 else -1
    return 1 if d < 0 else -1


def pmul(A, B):
    C = {}
    for ma, ca in A.items():
        for mb, cb in B.items():
            m = tuple(x + y for x, y in zip(ma, mb))
            C[m] = add(C.get(m, ZERO), mul(ca, cb))
    return {m: c for m, c in C.items() if c != ZERO}


def padd(A, B):
    C = A.copy()
    for m, c in B.items():
        C[m] = add(C.get(m, ZERO), c)
    return {m: c for m, c in C.items() if c != ZERO}


def pscale(P, q): return {m: mul(c, q) for m, c in P.items() if mul(c, q) != ZERO}


def ppow(P, n):
    R = {(0, 0, 0): ONE}
    while n:
        if n & 1: R = pmul(R, P)
        n //= 2
        if n: P = pmul(P, P)
    return R


def linpow(v, n):
    P = {}
    for i in range(n + 1):
        for j in range(n - i + 1):
            k = n - i - j
            c = mul(power(v[0], i), mul(power(v[1], j), power(v[2], k)))
            c = scale(c, Fraction(math.factorial(n), math.factorial(i)*math.factorial(j)*math.factorial(k)))
            if c != ZERO: P[(i, j, k)] = c
    return P


def canonical_generators():
    vertices = []
    for u in (1, -1):
        for v in (1, -1):
            U, V = scale(ONE, u), scale(ONE, v)
            vertices.extend([(ZERO, U, scale(PHI, v)), (U, scale(PHI, v), ZERO),
                             (scale(PHI, u), ZERO, V)])
    R2 = add(PHI, scale(ONE, 2))
    raw = {}
    for n in (6, 10):
        poly = {}
        for vertex in vertices: poly = padd(poly, linpow(vertex, n))
        raw[n] = pscale(poly, inv(power(R2, n // 2)))
    norm = {(2, 0, 0): ONE, (0, 2, 0): ONE, (0, 0, 2): ONE}
    # Homogenized Legendre orbit sums in the same orientation as the dossier.
    H6 = pscale(padd(pscale(raw[6], scale(ONE, 231)),
                     pscale(ppow(norm, 3), scale(ONE, -396))), scale(ONE, Fraction(1, 16)))
    H10 = padd(pscale(raw[10], scale(ONE, 46189)),
               pscale(pmul(raw[6], ppow(norm, 2)), scale(ONE, -114114)))
    H10 = pscale(padd(H10, pscale(ppow(norm, 5), scale(ONE, 145236))),
                  scale(ONE, Fraction(1, 256)))
    return H6, H10


def read_poly(entries, degree):
    P = {}
    for entry in entries:
        m = tuple(entry["monomial"])
        require(len(m) == 3 and all(type(x) is int and x >= 0 for x in m), "Invalid monomial")
        require(sum(m) == degree and m not in P, "Wrong degree or duplicate monomial")
        P[m] = pair(entry["coeff"])
    return P


def dfodd(n):
    r = 1
    for k in range(n, 0, -2): r *= k
    return r


def sphere_mean(P):
    out = ZERO
    for (i, j, k), c in P.items():
        if i % 2 or j % 2 or k % 2: continue
        q = Fraction(dfodd(i-1)*dfodd(j-1)*dfodd(k-1), dfodd(i+j+k+1))
        out = add(out, scale(c, q))
    return out


def eval_poly(P, xyz):
    maxdeg = max(max(m) for m in P)
    caches = []
    for q in xyz:
        c = [ONE]
        for _ in range(maxdeg): c.append(mul(c[-1], q))
        caches.append(c)
    out = ZERO
    for (i, j, k), coef in P.items():
        out = add(out, mul(coef, mul(caches[0][i], mul(caches[1][j], caches[2][k]))))
    return out


def inv_values(part, H6, H10):
    a, b, c = part
    xyz = (scale(ONE, c-b), add(scale(ONE, a), scale(PHI, b+c)), scale(PHI, a))
    n2 = add(mul(xyz[0], xyz[0]), add(mul(xyz[1], xyz[1]), mul(xyz[2], xyz[2])))
    return div(eval_poly(H6, xyz), power(n2, 3)), div(eval_poly(H10, xyz), power(n2, 5))


def monoms(t):
    return [(r, s) for d, r, s in sorted((6*r+10*s, r, s)
            for r in range(t//6+1) for s in range(t//10+1) if 6*r+10*s <= t)]


def partitions(f):
    return [(a, b, f-a-b) for a in range(f, -1, -1)
            for b in range(min(a, f-a), -1, -1) if 0 <= f-a-b <= b]


def orbit_size(p):
    a, b, c = p
    if b == 0: return 12
    if c == 0: return 30 if a == b else 60
    if a == b == c: return 20
    return 60 if a == b or b == c else 120


def validate_structure(D):
    require(set(D["frequencies"]) == {str(f) for f in range(2, 22)}, "Expected exactly frequencies 2 through 21")
    H6, H10 = read_poly(D["H6"], 6), read_poly(D["H10"], 10)
    require((H6, H10) == canonical_generators(), "Generator coefficients differ from canonical vertex construction")
    records = {}
    for f in range(2, 22):
        rec = D["frequencies"][str(f)]
        t = 3*f + (2 if f % 2 else 3)
        require(type(rec["tau"]) is int and rec["tau"] == t, f"Wrong target degree at f={f}")
        reps = partitions(f)
        actual = [tuple(w["partition"]) for w in rec["weights"]]
        require(all(all(type(x) is int for x in p) for p in actual), "Invalid partition coordinate")
        require(actual == reps, f"Missing, duplicate or reordered orbit at f={f}")
        require(rec["orbit_count"] == len(reps), f"Wrong orbit count at f={f}")
        require(rec["moment_condition_count"] == len(monoms(t)), f"Wrong row count at f={f}")
        sizes = [orbit_size(p) for p in reps]
        require(sum(sizes) == 10*f*f+2, f"Orbit cardinalities do not cover the grid at f={f}")
        W = [pair(w["weight"]) for w in rec["weights"]]
        require(all(sign(w) == 1 for w in W), f"Nonpositive weight at f={f}")
        require(sum((w[0] for w in W), Fraction(0)) == 1 and
                sum((w[1] for w in W), Fraction(0)) == 0, f"Normalization failed at f={f}")
        records[f] = (rec, reps, sizes, W)
    return H6, H10, records


def unique_object(pairs):
    result = {}
    for key, value in pairs:
        require(key not in result, "Duplicate JSON object key")
        result[key] = value
    return result


def verify(D):
    H6, H10, records = validate_structure(D)
    needed = monoms(65)
    P6, P10 = {0: {(0,0,0): ONE}}, {0: {(0,0,0): ONE}}
    for r in range(1, max(r for r,s in needed)+1): P6[r] = pmul(P6[r-1], H6)
    for s in range(1, max(s for r,s in needed)+1): P10[s] = pmul(P10[s-1], H10)
    rhs = {(r,s): sphere_mean(pmul(P6[r], P10[s])) for r,s in needed}
    result = {"generator_reconstruction": "PASS", "frequencies": {}, "total_moment_rows": 0,
              "total_positive_orbit_masses": 0}
    for f, (rec, reps, sizes, W) in records.items():
        UV = [inv_values(p, H6, H10) for p in reps]
        rows = []
        for r,s in monoms(rec["tau"]):
            lhs = ZERO
            for w,(u6,u10) in zip(W, UV):
                lhs = add(lhs, mul(w, mul(power(u6,r), power(u10,s))))
            residual = sub(lhs, rhs[(r,s)])
            require(residual == ZERO, f"Moment failed at f={f}, (r,s)=({r},{s})")
            rows.append({"r": r, "s": s, "degree": 6*r+10*s,
                         "lhs": encode(lhs), "rhs": encode(rhs[(r,s)]), "residual": encode(residual)})
        minimum = 0
        for j in range(1, len(W)):
            if sign(sub(W[j], W[minimum])) < 0: minimum = j
        canonical = "".join(f"{p[0]},{p[1]},{p[2]}:{w[0].numerator}/{w[0].denominator}:{w[1].numerator}/{w[1].denominator}\n"
                            for p,w in zip(reps,W)).encode()
        result["frequencies"][str(f)] = {
            "degree": rec["tau"], "nodes": sum(sizes), "orbits": len(W), "rows": rows,
            "normalization": encode(ONE), "minimum_orbit": reps[minimum],
            "minimum_mass": encode(W[minimum]), "canonical_weight_text_sha256": hashlib.sha256(canonical).hexdigest(),
            "positivity": [{"partition": p, "nodes": size, "sign": 1} for p,size in zip(reps,sizes)]}
        result["total_moment_rows"] += len(rows)
        result["total_positive_orbit_masses"] += len(W)
        print(f"PASS f={f:2d} degree={rec['tau']:2d} nodes={sum(sizes)} orbits={len(W):2d} rows={len(rows):2d} minimum={reps[minimum]} exact", flush=True)
    require(result["total_moment_rows"] == 383, "Wrong total row count")
    require(result["total_positive_orbit_masses"] == 404, "Wrong total mass count")
    print("ALL PASS: 20 frequencies; 383 exact identities; 404 strictly positive masses; canonical generators and orbit coverage checked.", flush=True)
    return result


def main():
    parser = argparse.ArgumentParser()
    parser.add_argument("certificate", nargs="?", type=Path,
                        default=Path(__file__).resolve().with_name("classI_exact_certificates_f2_f21.json"))
    parser.add_argument("--ledger", type=Path, required=True)
    args = parser.parse_args()
    started = datetime.now(timezone.utc).isoformat()
    start = time.monotonic()
    raw = args.certificate.read_bytes()
    require(hashlib.sha256(raw).hexdigest() == CERT_SHA, "Recovered certificate SHA-256 mismatch")
    data = json.loads(raw, object_pairs_hook=unique_object)
    result = verify(data)
    result.update({"verifier": "verify_classI_f2_f21.r2.py", "certificate_sha256": CERT_SHA,
                   "verifier_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
                   "started_utc": started, "completed_utc": datetime.now(timezone.utc).isoformat(),
                   "duration_seconds": time.monotonic()-start, "python": sys.version,
                   "platform": platform.platform(), "optimization": sys.flags.optimize})
    args.ledger.parent.mkdir(parents=True, exist_ok=True)
    args.ledger.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8")


if __name__ == "__main__":
    try:
        main()
    except (ValueError, OSError, KeyError, TypeError, ZeroDivisionError) as exc:
        raise SystemExit("FAIL: " + str(exc)) from exc