Spaces:
Running
Running
File size: 3,238 Bytes
ca74b23 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 | """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())
|