#!/usr/bin/env python3
"""OMEGA proof-certificate checker, Python 3.10+, standard library only.

Usage: python python/verify.py certificates.json
Checks exact polynomial certificates in Q(phi)[x_1,...,x_n], then independently
recomputes the canonical floor-prefix certificate, every 15-bit ledger, and
Boolean-circuit examples. Written analytic proofs live in omega_proofs.json.
This is a custom checker, NOT a Lean proof-kernel or an external-paper audit.
"""
from __future__ import annotations
from dataclasses import dataclass
from fractions import Fraction as F
from math import isqrt, gcd
from pathlib import Path
import hashlib
import json
import re
import sys

CERTIFICATE_SHA256 = "daaee23b3c27bbb320d0f8db2c8d00a4a077f08e5fe0056864323873ddf71b19"
EXPECTED_CASE_COUNTS = {'G01_SIMILARITY': 21, 'G02_GRAM_AND_DIMENSION': 58, 'C01_SYMBOLIC_INTERPOLATION': 2, 'C02_EXACT_DECODERS': 183, 'C03_CODE_DISTANCE_MINORS': 94, 'C04_INVISIBLE_PROFILE': 8, 'V01_CONVEX_POLARS': 12, 'T01_TENSOR_RECONSTRUCTION': 1296, 'H01_ICOSAHEDRAL_CUBATURE': 163, 'O01_MOMENT_AND_PULLBACK': 8, 'O02_OPERATOR_ALGEBRA': 19, 'O03_BLOCH_ELLIPSE': 8, 'S01_SYMPLECTIC': 8, 'I01_BOUNDARY_AND_COMPRESSION': 14, 'I02_CHART_METRIC': 1, 'F01_FORCED_FLOW': 10, 'B01_QUANTIZED_LINEAR_LAYER': 397, 'A01_TELESCOPING_SYMBOLIC': 3, 'U01_COMPOSITION_EXAMPLE': 9}  # Filled after the immutable certificate is built.
Q, S, N, LIMIT = 339949771344778, 10**15, 23, 32768


def require(ok: bool, message: str) -> None:
    if not ok:
        raise ValueError(message)


def fraction(text: str) -> F:
    require(isinstance(text, str) and re.fullmatch(r"-?(0|[1-9][0-9]*)(/[1-9][0-9]*)?", text) is not None,
            "noncanonical exact rational")
    return F(text)


@dataclass(frozen=True)
class Golden:
    """a+b*phi, where phi^2=phi+1; a and b are arbitrary-precision rationals."""
    a: F = F(0)
    b: F = F(0)

    def __add__(self, other: Golden) -> Golden:
        return Golden(self.a+other.a, self.b+other.b)

    def __neg__(self) -> Golden:
        return Golden(-self.a, -self.b)

    def __sub__(self, other: Golden) -> Golden:
        return self + -other

    def __mul__(self, other: Golden) -> Golden:
        return Golden(self.a*other.a+self.b*other.b,
                      self.a*other.b+self.b*other.a+self.b*other.b)

    def inverse(self) -> Golden:
        norm = self.a*self.a+self.a*self.b-self.b*self.b
        require(norm != 0, "zero field denominator")
        return Golden((self.a+self.b)/norm, -self.b/norm)

    def __truediv__(self, other: Golden) -> Golden:
        return self * other.inverse()

    def sign(self) -> int:
        # a+b*phi = (a+b/2)+(b/2)*sqrt(5); compare exactly, without floats.
        a, b = self.a+self.b/2, self.b/2
        sg = lambda x: (x > 0)-(x < 0)
        if b == 0:
            return sg(a)
        if a == 0 or sg(a) == sg(b):
            return sg(b)
        return sg(a)*sg(a*a-5*b*b)


ZERO, ONE = Golden(), Golden(F(1))
Monomial = tuple[int, ...]
Polynomial = dict[Monomial, Golden]


def clean(p: Polynomial) -> Polynomial:
    return {m: c for m, c in p.items() if c != ZERO}


def p_add(p: Polynomial, q: Polynomial) -> Polynomial:
    out = p.copy()
    for m, c in q.items():
        out[m] = out.get(m, ZERO)+c
    return clean(out)


def p_neg(p: Polynomial) -> Polynomial:
    return {m: -c for m, c in p.items()}


def p_mul(p: Polynomial, q: Polynomial) -> Polynomial:
    out: Polynomial = {}
    for m, a in p.items():
        for n, b in q.items():
            key = tuple(x+y for x, y in zip(m, n))
            out[key] = out.get(key, ZERO)+a*b
    return clean(out)


def p_pow(p: Polynomial, n: int, dimensions: int) -> Polynomial:
    require(type(n) is int and 0 <= n <= 64, "invalid polynomial exponent")
    out, base = {(0,)*dimensions: ONE}, p
    while n:
        if n & 1:
            out = p_mul(out, base)
        base = p_mul(base, base)
        n //= 2
    return out


def p_derivative(p: Polynomial, variable: int) -> Polynomial:
    out = {}
    for m, c in p.items():
        if m[variable]:
            n = list(m)
            n[variable] -= 1
            out[tuple(n)] = c*Golden(F(m[variable]))
    return out


def audit_algebra(data: dict, enforce_inventory: bool = True) -> dict[str, int]:
    require(data.get("format") == "OMEGA_EXACT_CERTIFICATES/1.0", "unknown certificate format")
    cases = data.get("algebra_cases")
    require(isinstance(cases, list) and len(cases) > 0, "empty algebra certificate")
    counts = {}
    for case in cases:
        name, variables = case["id"], case["variables"]
        require(name not in counts, "duplicate case ID")
        require(len(set(variables)) == len(variables), "duplicate variables")
        dimensions = len(variables)
        zero_monomial = (0,)*dimensions
        registers: list[Polynomial] = []
        for inst in case["program"]:
            require(isinstance(inst, list) and len(inst) > 0, "invalid instruction")
            op = inst[0]
            def get(index: int) -> Polynomial:
                require(type(index) is int and 0 <= index < len(registers), "forward or invalid register reference")
                return registers[index]
            if op == "q":
                require(len(inst) == 3, "bad constant arity")
                value = clean({zero_monomial: Golden(fraction(inst[1]), fraction(inst[2]))})
            elif op == "v":
                require(len(inst) == 2 and type(inst[1]) is int and 0 <= inst[1] < dimensions, "bad variable")
                m = [0]*dimensions
                m[inst[1]] = 1
                value = {tuple(m): ONE}
            elif op in ("+", "*"):
                require(len(inst) == 3, "bad binary arity")
                value = (p_add if op == "+" else p_mul)(get(inst[1]), get(inst[2]))
            elif op == "-":
                require(len(inst) == 2, "bad negation arity")
                value = p_neg(get(inst[1]))
            elif op == "^":
                require(len(inst) == 3, "bad power arity")
                value = p_pow(get(inst[1]), inst[2], dimensions)
            elif op == "D":
                require(len(inst) == 3 and type(inst[2]) is int and 0 <= inst[2] < dimensions, "bad derivative")
                value = p_derivative(get(inst[1]), inst[2])
            else:
                raise ValueError("unsupported polynomial instruction: "+str(op))
            registers.append(value)
        checks = case["checks"]
        require(len(checks) > 0, "case has no checks")
        ids = set()
        for check in checks:
            require(check["id"] not in ids, "duplicate check ID")
            ids.add(check["id"])
            left, right = get(check["lhs"]), get(check["rhs"])
            difference = p_add(left, p_neg(right))
            relation = check["relation"]
            if relation == "eq":
                require(not difference, "identity failed: "+check["id"])
            elif relation in ("ne_constant", "positive_constant"):
                require(set(difference) == {zero_monomial}, "counterexample is not a nonzero constant: "+check["id"])
                if relation == "positive_constant":
                    require(difference[zero_monomial].sign() > 0, "positivity failed: "+check["id"])
            else:
                raise ValueError("unsupported relation")
        counts[name] = len(checks)
    if enforce_inventory:
        require(counts == EXPECTED_CASE_COUNTS, "certificate coverage inventory mismatch")
    return counts


def floor_sum(n: int, m: int, a: int, b: int = 0) -> int:
    require(all(type(x) is int for x in (n, m, a, b)) and n >= 0 and m > 0 and a >= 0 and b >= 0,
            "floor_sum requires nonnegative integers and positive modulus")
    out = 0
    while True:
        qa, a = divmod(a, m)
        qb, b = divmod(b, m)
        out += (n-1)*n*qa//2+n*qb
        y = a*n+b
        if y < m:
            return out
        n, b = divmod(y, m)
        m, a = a, m


def atan_interval(inv: int, terms: int) -> tuple[F, F]:
    p = sum((F((-1)**k, (2*k+1)*inv**(2*k+1)) for k in range(terms)), F(0))
    q = p+F((-1)**terms, (2*terms+1)*inv**(2*terms+1))
    return min(p, q), max(p, q)


def prefix_certificate() -> dict:
    small_count = 0
    for n in range(9):
        for m in range(1, 9):
            for a in range(9):
                for b in range(3):
                    require(floor_sum(n,m,a,b) == sum((a*i+b)//m for i in range(n)), "floor-sum recurrence mismatch")
                    small_count += 1
    l5, u5 = atan_interval(5, 50)
    l239, u239 = atan_interval(239, 18)
    pi_l, pi_u = 16*l5-4*u239, 16*u5-4*l239
    scale = 10**80
    root = isqrt(5*scale*scale)
    require(root*root < 5*scale*scale < (root+1)**2, "sqrt5 bracket")
    phi_l, phi_u = (1+F(root,scale))/2, (1+F(root+1,scale))/2
    lower, upper = phi_l/(phi_l+pi_u), phi_u/(phi_u+pi_l)
    q = F(Q,S)
    require(0 < q < lower < upper < F(1,2), "lambda interval order")
    stop, target = 42189065, 302541195258184
    sums = [floor_sum(stop, v.denominator, v.numerator) for v in (q,lower,upper)]
    require(sums == [target]*3, "whole-prefix floor certificate")
    real_floor_l, real_floor_u = (lower*stop).__floor__(), (upper*stop).__floor__()
    rational_floor = Q*stop//S
    require(real_floor_l == real_floor_u == 14342163 and rational_floor == 14342162, "first disagreement certificate")
    return {"floor_sum_small_cases": small_count, "first_disagreement": str(stop),
            "prefix_common_sum": str(target), "rational_floor": str(rational_floor),
            "real_floor": str(real_floor_l), "lambda_lower": str(lower), "lambda_upper": str(upper)}


def encode(seed: int, steps: int = N) -> tuple[int, list[int]]:
    require(type(seed) is int and seed >= 0 and type(steps) is int and steps >= 0, "invalid nonnegative seed/horizon")
    d, residues = seed, []
    for _ in range(steps):
        d, r = divmod(Q*d, S)
        residues.append(r)
    return d, residues


def decode(terminal: int, residues: list[int], expected_steps: int | None = None) -> int:
    require(type(terminal) is int and terminal >= 0 and isinstance(residues,list), "invalid ledger types")
    require(expected_steps is None or (type(expected_steps) is int and expected_steps >= 0 and len(residues) == expected_steps), "ledger length mismatch")
    d = terminal
    for r in reversed(residues):
        require(type(r) is int and 0 <= r < S, "invalid Euclidean remainder")
        numerator = S*d+r
        require(numerator % Q == 0, "invalid reverse divisibility")
        previous = numerator//Q
        require(divmod(Q*previous,S) == (d,r), "failed forward consistency")
        d = previous
    return d


def ledger_audit() -> dict:
    maximum, transitions = 0, 0
    qn, sn = Q**N, S**N
    inverse_q = pow(Q//2, -1, S//2)
    require(gcd(Q,S) == 2 and (Q//2)*inverse_q % (S//2) == 1, "first residue inverse")
    for seed in range(LIMIT):
        terminal, ledger = encode(seed)
        require(terminal == 0 and decode(terminal,ledger,N) == seed, "canonical ledger inversion")
        require((ledger[0]//2)*inverse_q % (S//2) == seed, "first-residue seed inversion")
        # Streaming form of the telescoping polynomial, avoiding repeated large exponentiation.
        weighted, spow = 0, 1
        for r in ledger:
            weighted = Q*weighted+spow*r
            spow *= S
        require(qn*seed == sn*terminal+weighted, "whole-ledger telescoping identity")
        d, steps = seed, 0
        while d:
            d = Q*d//S
            steps += 1
        maximum = max(maximum,steps)
        transitions += N
    require(maximum == 10, "extinction maximum")
    def rejected(fn) -> None:
        try:
            fn()
        except (ValueError, TypeError):
            return
        raise ValueError("malformed input incorrectly accepted")
    terminal, good = encode(399)
    changed = good.copy(); changed[0] += 1
    rejected(lambda: decode(terminal,changed,N))
    rejected(lambda: decode(-1,good,N))
    rejected(lambda: decode(0,[S],1))
    rejected(lambda: decode(0,[-1],1))
    rejected(lambda: decode(terminal,good[:-1],N))
    rejected(lambda: decode(0,[True],1))
    rejected(lambda: encode(-1))
    rejected(lambda: encode(True))
    a, b = 32767, 32768
    require(Q*a//S == Q*b//S and (Q*a)%S != (Q*b)%S, "discarded witness collision example")
    return {"seeds": LIMIT, "horizon": N, "transitions": transitions, "max_extinction": maximum,
            "telescoping_checks": LIMIT, "first_residue_checks": LIMIT, "malformed_inputs_rejected": 8}


def bits(n: int, width: int) -> list[int]:
    require(type(n) is int and n >= 0 and n < 1 << width, "bit word overflow")
    return [(n >> k) & 1 for k in range(width)]


def unbits(word: list[int]) -> int:
    return sum(v << k for k,v in enumerate(word))


def bit_add(a: list[int], b: list[int]) -> list[int]:
    require(len(a) == len(b), "bit widths differ")
    out, carry = [], 0
    for x,y in zip(a,b):
        out.append(x ^ y ^ carry)
        carry = (x & y) | (carry & (x ^ y))
    require(carry == 0, "bit addition overflow")
    return out


def bit_ge(a: list[int], b: list[int]) -> bool:
    for x,y in zip(reversed(a),reversed(b)):
        if x != y:
            return x > y
    return True


def bit_sub(a: list[int], b: list[int]) -> list[int]:
    out, borrow = [], 0
    for x,y in zip(a,b):
        out.append(x ^ y ^ borrow)
        borrow = ((1-x) & (y | borrow)) | (y & borrow)
    require(borrow == 0, "bit subtraction underflow")
    return out


def bit_floor_transition(d: int) -> tuple[int,int]:
    width = 65  # Q*(2^15-1) < 2^64; one spare bit for restoring division.
    require(type(d) is int and 0 <= d < LIMIT, "15-bit input required")
    product, multiplier = [0]*width, bits(Q,width)
    for i,x in enumerate(bits(d,15)):
        shifted = [0]*i+multiplier[:width-i]
        product = bit_add(product,[v & x for v in shifted])
    divisor, quotient, remainder = bits(S,width), [0]*width, [0]*width
    for k in range(width-1,-1,-1):
        require(remainder[-1] == 0, "restoring divider overflow")
        remainder = [product[k]]+remainder[:-1]
        if bit_ge(remainder,divisor):
            remainder = bit_sub(remainder,divisor)
            quotient[k] = 1
    return unbits(quotient),unbits(remainder)


def bit_audit() -> dict:
    for a in (0,1):
        for b in (0,1):
            for c in (0,1):
                total = a+b+c
                require((a ^ b ^ c)+2*((a & b) | (c & (a ^ b))) == total, "full-adder truth table")
                require((c ^ (a & b)) ^ (a & b) == c, "Toffoli reversibility")
    seeds = list(range(256))+[511,1023,4095,16383,32767]
    for d in seeds:
        require(bit_floor_transition(d) == divmod(Q*d,S), "Boolean floor circuit")
    messages = [b"",b"\0",b"\0\0",b"OMEGA",b"OMEGA\0\xffNAUGHT",bytes(range(256))]
    for message in messages:
        for byte_order in ("little","big"):
            value = int.from_bytes(message,byte_order)
            require(value.to_bytes(len(message),byte_order) == message, "length-preserving byte tower")
    require(int.from_bytes(b"\0","big") == int.from_bytes(b"\0\0","big"), "length metadata is necessary")
    return {"full_adder_rows": 8, "toffoli_rows": 8, "boolean_floor_cases": len(seeds), "byte_roundtrips": 12}


def end_to_end_audit() -> dict:
    # Exact auxiliary seed s=1/2; NOT a replacement for canonical sin(pi/1296000).
    phi, seed = Golden(F(0),F(1)), Golden(F(1,2))
    A, B = seed+phi*phi, seed+ONE
    nodes = [-A,-B,-seed,seed,B,A]
    values = [Golden(F(3))-Golden(F(2))*z for z in nodes]
    packet = ";".join(str(v.a)+","+str(v.b) for v in values).encode("ascii")
    recovered = bytes(decode(*encode(octet),expected_steps=N) for octet in packet)
    require(recovered == packet, "exact measurement packet replay")
    fields = [part.split(",") for part in recovered.decode("ascii").split(";")]
    require(len(fields) == 6 and all(len(part)==2 for part in fields), "measurement packet shape")
    restored = [Golden(fraction(a),fraction(b)) for a,b in fields]
    slope = (restored[-1]-restored[0])/(nodes[-1]-nodes[0])
    intercept = restored[0]-slope*nodes[0]
    require(slope == Golden(F(-2)) and intercept == Golden(F(3)), "end-to-end affine field recovery")
    return {"auxiliary_seed":"1/2", "point_measurements":6,"packet_bytes":len(packet),
            "byte_ledgers":len(packet),"recovered_intercept":"3","recovered_slope":"-2"}


def audit_runtime() -> dict:
    cyclotomic_order = 2**8*3**4*5**3
    totient = cyclotomic_order
    for p in (2,3,5):
        totient = totient//p*(p-1)
    require(cyclotomic_order == 2592000 and totient == 691200, "cyclotomic arithmetic")
    return {"cyclotomic_ambient_real_degree": totient//2,
            "floor_prefix": prefix_certificate(), "ledger": ledger_audit(), "binary": bit_audit(), "end_to_end":end_to_end_audit()}


def main() -> int:
    path = Path(sys.argv[1]) if len(sys.argv) == 2 else Path(__file__).resolve().parents[1]/"certificates.json"
    require(len(sys.argv) <= 2, "usage: verify.py [certificates.json]")
    raw = path.read_bytes()
    require(hashlib.sha256(raw).hexdigest() == CERTIFICATE_SHA256, "certificate hash mismatch")
    data = json.loads(raw, parse_float=lambda _: (_ for _ in ()).throw(ValueError("floating JSON number forbidden")))
    counts = audit_algebra(data)
    report = {"format":"OMEGA_EXECUTION_REPORT/1.0", "engine":"Python", "runtime":sys.version.split()[0],
              "status":"CHECKS_PASSED", "certificate_sha256":CERTIFICATE_SHA256,
              "algebra_case_counts":counts, "algebra_checks":sum(counts.values()),
              "finite_audit":audit_runtime(), "formal_proof_kernel":"NOT_RUN",
              "external_manuscript_proofs":"NOT_VERIFIED", "neural_performance_claims":"NOT_ESTABLISHED"}
    print(json.dumps(report,indent=2,sort_keys=True))
    return 0


if __name__ == "__main__":
    try:
        raise SystemExit(main())
    except (ValueError,TypeError,KeyError,IndexError,OSError,ZeroDivisionError) as exc:
        print(json.dumps({"format":"OMEGA_EXECUTION_REPORT/1.0","engine":"Python","status":"FAIL","error":str(exc)}),file=sys.stderr)
        raise SystemExit(1)