#!/usr/bin/env python3
"""
OMEGA_NAUGHT_PROOF/1.0
Self-contained proof-carrying verifier for the finite Omega bridge.

Standard library only.  No floating-point arithmetic is used in any proof.

What this verifier establishes
------------------------------
1. A strict, byte-canonical, SHA-256-pinned manifest.
2. The positive sqrt(5) branch and phi^2-phi-1 = 0 exactly.
3. A rigorous rational interval for the circle constant pi using Machin's
   formula and alternating arctangent-series remainder bounds.
4. A rigorous rational interval for lambda = phi/(phi+pi), and proof that
   the published adjacent 60-decimal endpoints strictly enclose lambda.
5. Exhaustively, for every 0 <= d < 2^15,
       floor(lambda*d) = floor(Q*d/S),
   using only the certified lambda enclosure and exact integer arithmetic.
6. The first mismatch d*=42,189,065, with minimality proved by a
   continued-fraction least-denominator certificate rather than a
   42-million-state brute-force scan.
7. A claim-level dependency DAG, per-claim evidence hashes, a deterministic
   proof-evidence root, and a runtime/source execution commitment.

Trusted mathematical lemmas
---------------------------
The checker intentionally exposes, rather than hides, its small trusted
mathematical base:
  A. Alternating-series enclosure for atan(x), 0 < x <= 1.
  B. Machin identity pi = 16 atan(1/5) - 4 atan(1/239); the exact tangent
     identity is replayed here, while the usual monotonicity/branch theorem
     for atan is treated as standard analysis.
  C. Continued-fraction least-denominator lemma: if two positive rationals
     have canonical simple continued fractions with common prefix P and
     first differing partial quotients a,b, then [P,min(a,b)+1] is a rational
     of minimum denominator strictly between them (non-prefix case).

This is therefore a small exact certificate verifier, not a foundational
proof assistant kernel.
"""

from __future__ import annotations

import argparse
import hashlib
import json
import platform
import sys
from dataclasses import dataclass
from fractions import Fraction
from math import isqrt
from pathlib import Path
from typing import Any, Iterable


# ---------------------------------------------------------------------------
# Frozen contract
# ---------------------------------------------------------------------------

MANIFEST: dict[str, Any] = {
    "contract": "OMEGA_NAUGHT_PROOF/1.0",
    "algebra": "Q(T)[lambda]/(lambda^2-T*lambda-T^2)",
    "embedding": "phi=(1+sqrt(5))/2;pi=circle_constant;T=1/(phi+pi);lambda=phi*T",
    "sqrt5_branch": "positive",
    "pi_certificate": "Machin:pi=16*atan(1/5)-4*atan(1/239)",
    "decimal_scale": "1000000000000000000000000000000000000000000000000000000000000",
    "lambda_lower_60": "339949771344778929576702809321279193551009905014259416689444",
    "lambda_upper_60": "339949771344778929576702809321279193551009905014259416689445",
    "q_num": "339949771344778",
    "q_den": "1000000000000000",
    "width_bits": 15,
    "domain_min": 0,
    "domain_max": 32767,
    "first_mismatch_d": "42189065",
    "first_mismatch_k": "14342163",
}

EXPECTED_MANIFEST_SHA256 = "56693dd0ea48bc0e4015e984a5c0bd63f82dfd537dda63e638cc7707365e8ec9"

TRUSTED_LEMMAS = [
    "alternating_atan_series_remainder",
    "machin_identity_with_standard_atan_branch_theorem",
    "continued_fraction_least_denominator_nonprefix_lemma",
]


class VerificationError(RuntimeError):
    pass


def require(condition: bool, message: str) -> None:
    if not condition:
        raise VerificationError(message)


def canonical_json_bytes(obj: Any) -> bytes:
    return json.dumps(
        obj,
        sort_keys=True,
        separators=(",", ":"),
        ensure_ascii=True,
        allow_nan=False,
    ).encode("ascii")


def sha256_bytes(data: bytes) -> str:
    return hashlib.sha256(data).hexdigest()


def frac_json(x: Fraction) -> dict[str, str]:
    return {"n": str(x.numerator), "d": str(x.denominator)}


def strict_json_loads(raw: bytes) -> Any:
    """Reject duplicate keys and non-standard JSON constants."""

    def pairs_hook(pairs: Iterable[tuple[str, Any]]) -> dict[str, Any]:
        out: dict[str, Any] = {}
        for k, v in pairs:
            if k in out:
                raise VerificationError(f"duplicate JSON key: {k!r}")
            out[k] = v
        return out

    def reject_constant(x: str) -> None:
        raise VerificationError(f"non-finite JSON constant forbidden: {x}")

    try:
        return json.loads(
            raw.decode("ascii"),
            object_pairs_hook=pairs_hook,
            parse_constant=reject_constant,
        )
    except UnicodeDecodeError as exc:
        raise VerificationError("manifest must be canonical ASCII JSON") from exc
    except json.JSONDecodeError as exc:
        raise VerificationError(f"invalid JSON: {exc}") from exc


def verify_manifest_bytes(raw: bytes) -> dict[str, Any]:
    """Require exact schema, exact values, canonical bytes, and pinned digest."""
    obj = strict_json_loads(raw)
    require(isinstance(obj, dict), "manifest root must be an object")
    require(set(obj) == set(MANIFEST), "unknown or missing manifest keys")
    require(obj == MANIFEST, "manifest semantic value differs from frozen contract")
    canonical = canonical_json_bytes(obj)
    require(raw == canonical, "manifest bytes are not canonical JSON")
    digest = sha256_bytes(canonical)
    require(digest == EXPECTED_MANIFEST_SHA256, "manifest SHA-256 mismatch")
    return obj


# ---------------------------------------------------------------------------
# Exact Q(sqrt(5)) fragment for the algebraic branch certificate
# ---------------------------------------------------------------------------

@dataclass(frozen=True)
class Quad5:
    """a + b*sqrt(5), a,b in Q."""

    a: Fraction
    b: Fraction

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

    def __sub__(self, other: "Quad5") -> "Quad5":
        return Quad5(self.a - other.a, self.b - other.b)

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

    def is_zero(self) -> bool:
        return self.a == 0 and self.b == 0

    def as_json(self) -> dict[str, dict[str, str]]:
        return {"a": frac_json(self.a), "b": frac_json(self.b)}


ZERO5 = Quad5(Fraction(0), Fraction(0))
ONE5 = Quad5(Fraction(1), Fraction(0))
PHI5 = Quad5(Fraction(1, 2), Fraction(1, 2))


# ---------------------------------------------------------------------------
# Rigorous real intervals
# ---------------------------------------------------------------------------

@dataclass(frozen=True)
class OpenInterval:
    lo: Fraction
    hi: Fraction

    def __post_init__(self) -> None:
        require(self.lo < self.hi, "invalid interval")

    def as_json(self) -> dict[str, dict[str, str]]:
        return {"lo": frac_json(self.lo), "hi": frac_json(self.hi)}


def sqrt5_interval(decimal_digits: int = 90) -> OpenInterval:
    """Open decimal interval containing the positive sqrt(5)."""
    require(decimal_digits >= 2, "sqrt5 precision too small")
    scale = 10 ** decimal_digits
    target = 5 * scale * scale
    n = isqrt(target)
    require(n * n < target < (n + 1) * (n + 1), "unexpected perfect-square boundary")
    return OpenInterval(Fraction(n, scale), Fraction(n + 1, scale))


def atan_inv_interval(inv_x: int, terms: int) -> OpenInterval:
    """Rigorous interval for atan(1/inv_x) using adjacent alternating sums."""
    require(inv_x >= 1, "inv_x must be positive")
    require(terms >= 1, "terms must be positive")

    s = Fraction(0)
    power = inv_x  # inv_x^(2k+1)
    step = inv_x * inv_x
    for k in range(terms):
        term = Fraction(1, (2 * k + 1) * power)
        s = s - term if (k & 1) else s + term
        power *= step

    k = terms
    next_term = Fraction(1, (2 * k + 1) * power)
    s_next = s - next_term if (k & 1) else s + next_term
    return OpenInterval(min(s, s_next), max(s, s_next))


def verify_machin_tangent_identity() -> dict[str, Any]:
    """Replay the exact rational tangent part of Machin's identity."""
    t = Fraction(1, 5)

    def tan_double(x: Fraction) -> Fraction:
        require(x * x != 1, "tangent doubling singularity")
        return 2 * x / (1 - x * x)

    tan_2a = tan_double(t)
    tan_4a = tan_double(tan_2a)
    b = Fraction(1, 239)
    tan_4a_minus_b = (tan_4a - b) / (1 + tan_4a * b)
    require(tan_2a == Fraction(5, 12), "unexpected tan(2 atan(1/5))")
    require(tan_4a == Fraction(120, 119), "unexpected tan(4 atan(1/5))")
    require(tan_4a_minus_b == 1, "Machin tangent identity failed")
    return {
        "tan_2a": frac_json(tan_2a),
        "tan_4a": frac_json(tan_4a),
        "tan_4a_minus_b": frac_json(tan_4a_minus_b),
    }


def pi_interval(terms_5: int = 70, terms_239: int = 25) -> tuple[OpenInterval, dict[str, Any]]:
    """Rigorous rational interval for pi from Machin's formula."""
    a = atan_inv_interval(5, terms_5)
    b = atan_inv_interval(239, terms_239)
    # pi = 16*a - 4*b; account for monotonicity of interval arithmetic.
    out = OpenInterval(16 * a.lo - 4 * b.hi, 16 * a.hi - 4 * b.lo)
    # A=4 atan(1/5)-atan(1/239) is in (0,1), fixing the tan=1 branch.
    quarter_lo = 4 * a.lo - b.hi
    quarter_hi = 4 * a.hi - b.lo
    require(Fraction(0) < quarter_lo < quarter_hi < Fraction(1), "Machin branch interval failed")
    tangent = verify_machin_tangent_identity()
    return out, {
        "atan_1_5": a.as_json(),
        "atan_1_239": b.as_json(),
        "quarter_angle": OpenInterval(quarter_lo, quarter_hi).as_json(),
        "tangent_certificate": tangent,
        "terms_5": terms_5,
        "terms_239": terms_239,
    }


def lambda_interval_from_phi_pi(sqrt5: OpenInterval, pi: OpenInterval) -> OpenInterval:
    """lambda=phi/(phi+pi), increasing in phi and decreasing in pi."""
    phi_lo = (1 + sqrt5.lo) / 2
    phi_hi = (1 + sqrt5.hi) / 2
    require(phi_lo > 0 and pi.lo > 0, "positive real embedding not established")
    lo = phi_lo / (phi_lo + pi.hi)
    hi = phi_hi / (phi_hi + pi.lo)
    return OpenInterval(lo, hi)


def published_lambda_cell() -> OpenInterval:
    scale = int(MANIFEST["decimal_scale"])
    return OpenInterval(
        Fraction(int(MANIFEST["lambda_lower_60"]), scale),
        Fraction(int(MANIFEST["lambda_upper_60"]), scale),
    )


def floor_certified_by_open_interval(interval: OpenInterval, d: int) -> int:
    """Return floor(x*d) for every x in the open interval, or fail.

    For k=floor(lo*d), it is enough that hi*d <= k+1 because x<hi.
    This correctly handles the case hi*d is exactly an integer.
    """
    require(d >= 0, "d must be nonnegative")
    ld = interval.lo * d
    ud = interval.hi * d
    k = ld.numerator // ld.denominator
    require(Fraction(k) <= ld, "internal floor error")
    require(ud <= k + 1, f"interval does not determine a unique floor at d={d}")
    return k


# ---------------------------------------------------------------------------
# Continued-fraction certificate for first mismatch minimality
# ---------------------------------------------------------------------------


def continued_fraction(x: Fraction) -> list[int]:
    require(x >= 0, "continued_fraction currently expects nonnegative rational")
    a, b = x.numerator, x.denominator
    out: list[int] = []
    while b:
        q, r = divmod(a, b)
        out.append(q)
        a, b = b, r
    # Euclidean expansion is canonical: final term > 1 unless integer/length 1.
    if len(out) > 1:
        require(out[-1] > 1, "noncanonical continued fraction")
    return out


def fraction_from_cf(parts: list[int]) -> Fraction:
    require(parts, "empty continued fraction")
    n = Fraction(parts[-1])
    for a in reversed(parts[:-1]):
        require(n != 0, "invalid continued fraction")
        n = a + 1 / n
    return n


def least_denominator_between_nonprefix(left: Fraction, right: Fraction) -> tuple[Fraction, dict[str, Any]]:
    """Apply the standard common-prefix CF least-denominator lemma.

    This function deliberately accepts only the non-prefix case used by the
    frozen Omega certificate; unsupported edge cases fail closed.
    """
    require(Fraction(0) <= left < right, "invalid CF interval")
    a = continued_fraction(left)
    b = continued_fraction(right)
    i = 0
    while i < min(len(a), len(b)) and a[i] == b[i]:
        i += 1
    require(i < len(a) and i < len(b), "prefix CF case is not accepted by this verifier")
    require(a[i] != b[i], "CF divergence expected")

    candidate_cf = a[:i] + [min(a[i], b[i]) + 1]
    candidate = fraction_from_cf(candidate_cf)
    require(left < candidate < right, "CF candidate is not strictly inside interval")
    return candidate, {
        "left_cf": a,
        "right_cf": b,
        "common_prefix": a[:i],
        "left_next": a[i],
        "right_next": b[i],
        "candidate_cf": candidate_cf,
        "candidate": frac_json(candidate),
        "lemma": "continued_fraction_least_denominator_nonprefix_lemma",
    }


# ---------------------------------------------------------------------------
# Proof ledger
# ---------------------------------------------------------------------------

@dataclass(frozen=True)
class ClaimResult:
    claim_id: str
    dependencies: tuple[str, ...]
    method: str
    evidence: dict[str, Any]

    def record(self) -> dict[str, Any]:
        return {
            "claim_id": self.claim_id,
            "dependencies": list(self.dependencies),
            "method": self.method,
            "result": "PASS",
            "evidence": self.evidence,
        }

    def evidence_sha256(self) -> str:
        return sha256_bytes(canonical_json_bytes(self.record()))


class Ledger:
    def __init__(self) -> None:
        self._claims: dict[str, ClaimResult] = {}

    def add(self, claim: ClaimResult) -> None:
        require(claim.claim_id not in self._claims, f"duplicate claim id {claim.claim_id}")
        for dep in claim.dependencies:
            require(dep in self._claims, f"missing dependency {dep} for {claim.claim_id}")
        self._claims[claim.claim_id] = claim

    def records(self) -> list[dict[str, Any]]:
        out = []
        for c in self._claims.values():
            r = c.record()
            r["evidence_sha256"] = c.evidence_sha256()
            out.append(r)
        return out

    def root_payload(self, manifest_sha256: str) -> dict[str, Any]:
        return {
            "contract": MANIFEST["contract"],
            "manifest_sha256": manifest_sha256,
            "trusted_lemmas": TRUSTED_LEMMAS,
            "claims": [
                {"claim_id": c.claim_id, "evidence_sha256": c.evidence_sha256()}
                for c in self._claims.values()
            ],
            "result": "PASS",
        }


# ---------------------------------------------------------------------------
# Full verification
# ---------------------------------------------------------------------------


def verify_all(manifest_raw: bytes | None = None) -> dict[str, Any]:
    if manifest_raw is None:
        manifest_raw = canonical_json_bytes(MANIFEST)
    verify_manifest_bytes(manifest_raw)
    manifest_sha = sha256_bytes(manifest_raw.strip())
    ledger = Ledger()

    ledger.add(ClaimResult(
        "MANIFEST.FROZEN",
        (),
        "strict canonical JSON + exact schema/value match + SHA-256 pin",
        {"manifest_sha256": manifest_sha},
    ))

    # Exact algebraic branch: phi=(1+sqrt5)/2 is the positive golden root.
    golden_residual = PHI5 * PHI5 - PHI5 - ONE5
    require(golden_residual.is_zero(), "phi^2-phi-1 exact identity failed")
    s5 = sqrt5_interval(90)
    require(s5.lo > 0, "positive sqrt(5) branch not certified")
    ledger.add(ClaimResult(
        "EMBED.PHI.POSITIVE_GOLDEN_ROOT",
        ("MANIFEST.FROZEN",),
        "exact Q(sqrt(5)) arithmetic + positive rational enclosure",
        {
            "phi": PHI5.as_json(),
            "phi2_minus_phi_minus_1": golden_residual.as_json(),
            "sqrt5_interval": s5.as_json(),
            "sqrt5_decimal_digits": 90,
        },
    ))

    # Pi bound and exact Machin tangent certificate.
    pi_int, pi_evidence = pi_interval(70, 25)
    ledger.add(ClaimResult(
        "EMBED.PI.CIRCLE_CONSTANT_BOUND",
        ("MANIFEST.FROZEN",),
        "Machin identity + alternating atan-series rational bounds",
        {"pi_interval": pi_int.as_json(), **pi_evidence},
    ))

    # Bind formal lambda/T relation to the intended real embedding.
    lam = lambda_interval_from_phi_pi(s5, pi_int)
    cell = published_lambda_cell()
    require(cell.lo < lam.lo, "published L60 is not proved below lambda")
    require(lam.hi < cell.hi, "published U60 is not proved above lambda")
    require(int(MANIFEST["lambda_upper_60"]) == int(MANIFEST["lambda_lower_60"]) + 1,
            "published 60-digit endpoints are not adjacent")
    ledger.add(ClaimResult(
        "OMEGA.LAMBDA.CERTIFIED_ENCLOSURE",
        ("EMBED.PHI.POSITIVE_GOLDEN_ROOT", "EMBED.PI.CIRCLE_CONSTANT_BOUND"),
        "monotone rational interval propagation under lambda=phi/(phi+pi)",
        {
            "derived_lambda_interval": lam.as_json(),
            "published_open_cell": cell.as_json(),
            "strictly_inside_published_cell": True,
            "formal_relation_certificate": "lambda^2-T*lambda-T^2 = T^2*(phi^2-phi-1) = 0",
            "real_embedding": MANIFEST["embedding"],
        },
    ))

    # Exhaustive finite bridge using the published cell, now itself certified.
    q = Fraction(int(MANIFEST["q_num"]), int(MANIFEST["q_den"]))
    dmin = int(MANIFEST["domain_min"])
    dmax = int(MANIFEST["domain_max"])
    require(dmin == 0 and dmax == (1 << int(MANIFEST["width_bits"])) - 1,
            "finite domain does not match declared width")

    transcript = hashlib.sha256()
    min_upper_gap: Fraction | None = None
    for d in range(dmin, dmax + 1):
        k_lambda = floor_certified_by_open_interval(cell, d)
        k_q = (int(MANIFEST["q_num"]) * d) // int(MANIFEST["q_den"])
        require(k_lambda == k_q, f"15-bit floor bridge failed at d={d}")
        transcript.update(f"{d}:{k_lambda}\n".encode("ascii"))
        # Margin to next integer from the upper endpoint; nonnegative by certificate.
        gap = Fraction(k_lambda + 1) - cell.hi * d
        if min_upper_gap is None or gap < min_upper_gap:
            min_upper_gap = gap

    ledger.add(ClaimResult(
        "OMEGA.FLOOR_BRIDGE.15BIT",
        ("OMEGA.LAMBDA.CERTIFIED_ENCLOSURE",),
        "exhaustive exact interval-floor proof over all 2^15 states",
        {
            "states_checked": dmax - dmin + 1,
            "domain": [dmin, dmax],
            "q": frac_json(q),
            "floor_transcript_sha256": transcript.hexdigest(),
            "minimum_upper_margin": frac_json(min_upper_gap if min_upper_gap is not None else Fraction(0)),
        },
    ))

    # First mismatch minimality: any earlier mismatch would produce a rational
    # k/d in (q,lambda] subset (q,U60), contradicting the CF denominator lemma.
    candidate, cf_cert = least_denominator_between_nonprefix(q, cell.hi)
    d_star = int(MANIFEST["first_mismatch_d"])
    k_star = int(MANIFEST["first_mismatch_k"])
    expected_candidate = Fraction(k_star, d_star)
    require(candidate == expected_candidate, "CF least-denominator candidate differs from frozen d*,k*")
    require(candidate < cell.lo, "candidate is not proved below lambda")
    q_floor_star = (int(MANIFEST["q_num"]) * d_star) // int(MANIFEST["q_den"])
    require(k_star == q_floor_star + 1, "k* is not the next integer above q*d*")
    lambda_floor_star = floor_certified_by_open_interval(cell, d_star)
    require(lambda_floor_star == k_star, "lambda floor at d* not certified as k*")
    require(q_floor_star != lambda_floor_star, "claimed first mismatch is not a mismatch")

    # Immediate predecessor is included as a diagnostic, not as the minimality proof.
    prev = d_star - 1
    prev_lambda = floor_certified_by_open_interval(cell, prev)
    prev_q = (int(MANIFEST["q_num"]) * prev) // int(MANIFEST["q_den"])
    require(prev_lambda == prev_q, "unexpected mismatch at d*-1")

    ledger.add(ClaimResult(
        "OMEGA.FIRST_MISMATCH.MINIMAL",
        ("OMEGA.LAMBDA.CERTIFIED_ENCLOSURE",),
        "continued-fraction least-denominator certificate + exact boundary floors",
        {
            "d_star": d_star,
            "k_star": k_star,
            "candidate_fraction": frac_json(candidate),
            "candidate_below_L60": candidate < cell.lo,
            "q_floor_at_d_star": q_floor_star,
            "lambda_floor_at_d_star": lambda_floor_star,
            "d_star_minus_1_floor": prev_q,
            "continued_fraction_certificate": cf_cert,
            "minimality_argument": (
                "If d<d_star were a mismatch, k=floor(q*d)+1 would give "
                "q<k/d<=lambda<U60, contradicting the certified minimum "
                "denominator d_star for rationals in (q,U60)."
            ),
        },
    ))

    root_payload = ledger.root_payload(manifest_sha)
    proof_root = sha256_bytes(canonical_json_bytes(root_payload))

    # Per-execution provenance. This is intentionally separate from the
    # deterministic mathematical proof root so other runtimes can reproduce
    # the same proof root while having different source/runtime commitments.
    source_sha = None
    try:
        source_path = Path(__file__).resolve()
        if source_path.is_file():
            source_sha = sha256_bytes(source_path.read_bytes())
    except Exception:
        source_sha = None

    execution_payload = {
        "proof_evidence_root_sha256": proof_root,
        "verifier_source_sha256": source_sha,
        "python_implementation": platform.python_implementation(),
        "python_version": platform.python_version(),
        "result": "PASS",
    }
    execution_commitment = sha256_bytes(canonical_json_bytes(execution_payload))

    return {
        "contract": MANIFEST["contract"],
        "result": "PASS",
        "manifest_sha256": manifest_sha,
        "trusted_lemmas": TRUSTED_LEMMAS,
        "claims": ledger.records(),
        "proof_root_payload": root_payload,
        "proof_evidence_root_sha256": proof_root,
        "execution": execution_payload,
        "execution_commitment_sha256": execution_commitment,
    }


# ---------------------------------------------------------------------------
# CLI
# ---------------------------------------------------------------------------


def main(argv: list[str] | None = None) -> int:
    parser = argparse.ArgumentParser(description="OMEGA_NAUGHT_PROOF/1.0 exact verifier")
    parser.add_argument("--manifest", type=Path, help="verify this canonical frozen manifest instead of embedded bytes")
    parser.add_argument("--emit-manifest", type=Path, help="write canonical frozen manifest and continue verification")
    parser.add_argument("--emit-certificate", type=Path, help="write canonical proof certificate JSON")
    parser.add_argument("--pretty", action="store_true", help="pretty-print certificate to stdout")
    args = parser.parse_args(argv)

    try:
        canonical_manifest = canonical_json_bytes(MANIFEST)
        require(sha256_bytes(canonical_manifest) == EXPECTED_MANIFEST_SHA256,
                "embedded manifest does not match pinned digest")

        if args.emit_manifest:
            args.emit_manifest.write_bytes(canonical_manifest)

        raw = args.manifest.read_bytes() if args.manifest else canonical_manifest
        cert = verify_all(raw)

        if args.emit_certificate:
            args.emit_certificate.write_bytes(canonical_json_bytes(cert))

        if args.pretty:
            print(json.dumps(cert, indent=2, sort_keys=True))
        else:
            print("OMEGA_NAUGHT_PROOF/1.0 PASS")
            print(f"manifest_sha256={cert['manifest_sha256']}")
            print(f"proof_evidence_root_sha256={cert['proof_evidence_root_sha256']}")
            print(f"execution_commitment_sha256={cert['execution_commitment_sha256']}")
            for claim in cert["claims"]:
                print(f"{claim['claim_id']}=PASS {claim['evidence_sha256']}")
        return 0
    except VerificationError as exc:
        print(f"OMEGA_NAUGHT_PROOF/1.0 FAIL: {exc}", file=sys.stderr)
        return 1


if __name__ == "__main__":
    raise SystemExit(main())