code/current_verifier.py

"""Evaluator-visible cumulative verifier. Exits nonzero on any failed contract."""

from __future__ import annotations

import csv
import json
import math
import sys
from pathlib import Path


ROOT = Path(__file__).resolve().parents[1]


def read_csv(path: str) -> list[dict[str, str]]:
    with (ROOT / path).open(newline="") as handle:
        return list(csv.DictReader(handle))


def read_json(path: str) -> dict:
    return json.loads((ROOT / path).read_text())


def claim1() -> bool:
    rows = read_csv("evidence/claim1/results.csv")
    primary = [row for row in rows if row["scale_floor"] != "control_constant_step"]
    control = [row for row in rows if row["scale_floor"] == "control_constant_step"]
    checks = read_json("evidence/claim1/checks.json")
    return (
        len(primary) == 12
        and len(control) == 4
        and all(row["bound_satisfied"] == "true" for row in primary)
        and all(float(row["log_log_slope"]) < -0.8 for row in primary)
        and all(float(row["log_log_slope"]) > -1.3 for row in primary)
        and float(control[-1]["mean_mse"]) > 0.1
        and abs(float(control[-1]["log_log_slope"])) < 0.25
        and checks["independent_checker"]["absolute_z_score"] < 5.0
        and checks["negative_control"]["passed_as_control"] is True
        and checks["compute"]["gpu_used"] is False
    )


def claim2() -> bool:
    data = read_json("evidence/claim2/results.json")
    omega = data["omega"]
    eta = data["eta0"]
    return (
        data["verdict"] == "VERIFIED"
        and all(abs(eta[i] / eta[i + 1] - omega[i] / omega[i + 1]) < 1e-12 for i in range(2))
        and data["negative_control"] == {"mutation": "delete omega", "rejections": 2, "tests": 2, "passed": True}
    )


def claim3() -> bool:
    data = read_json("evidence/claim3/results.json")
    return (
        data["verdict"] == "VERIFIED"
        and max(data["eta0"]) == min(data["eta0"])
        and data["omega_reachable_in_data_flow"] is False
        and data["negative_control"]["distinct_outputs"] == 3
        and data["negative_control"]["passed"] is True
    )


def claim4() -> bool:
    rows = read_csv("evidence/claim4/results.csv")
    factors = [float(row["log10_bound_factor"]) for row in rows]
    taus = [int(row["tau_0.05"]) for row in rows]
    return len(rows) == 13 and all(a < b for a, b in zip(factors, factors[1:])) and all(a < b for a, b in zip(taus, taus[1:]))


def claim5() -> bool:
    rows = read_csv("evidence/claim5/results.csv")
    checker = read_json("evidence/claim5/checker.json")
    control = read_json("evidence/claim5/control.json")
    return (
        len(rows) == 60
        and all(row["tau_definition"] == row["tau_direct_tv"] for row in rows)
        and checker["max_abs_closed_form_tv_error"] < 1e-12
        and checker["passed"] is True
        and control["rejections"] == control["tests"] == 60
        and control["passed_as_control"] is True
    )


def main() -> int:
    results = {"claim1": claim1(), "claim2": claim2(), "claim3": claim3(), "claim4_blocked_evidence": claim4(), "claim5": claim5()}
    print(json.dumps(results, indent=2, sort_keys=True))
    return 0 if all(results.values()) else 1


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