File size: 2,933 Bytes
f11738f | 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 | #!/usr/bin/env python3
"""Independent fail-closed checker for Claims 2, 4, 5, and 6."""
from __future__ import annotations
import json
from pathlib import Path
def check(root: Path) -> dict:
checks = {}
for claim_id in ("C2", "C4", "C5", "C6"):
path = (
root
/ ".openresearch"
/ "artifacts"
/ f"claim_{claim_id[1]}"
/ "raw"
/ "downstream_contract_audit.json"
)
audit = json.loads(path.read_text())
cells = audit["normalized_witness_cells"]
domain_violations = sum(not cell["M_le_m"] for cell in cells)
control = audit["negative_control"]
runtime_expected = claim_id in ("C2", "C4")
runtime_check = (
audit["asymptotic_certificate"]["runtime_power_contradiction"]
== runtime_expected
)
controls_reject = (
control["M_le_m"]
and control["M_le_advertised_terms"]
and not control["counterexample_triggered"]
)
checks[claim_id] = {
"assumptions_satisfied": audit["assumption_satisfying_family"][
"assumptions_satisfied"
],
"universal_epsilon_quantifier_present": (
audit["assumption_satisfying_family"]["epsilon_domain_in_corollary"]
== "epsilon > 0"
),
"eventual_domain_violation_certified": (
audit["asymptotic_certificate"]["eventual_M_gt_m"]
and domain_violations > 0
),
"claim_specific_dependency_chain_present": bool(
audit["exact_proposed_algorithm_chain"]
),
"runtime_basis_scoped_correctly": runtime_check,
"negative_control_rejects_false_positive": controls_reject,
"status": audit["status"],
}
passed = all(
row["status"] == "FALSIFIED"
and all(value for key, value in row.items() if key != "status")
for row in checks.values()
)
result = {
"checker": "downstream_contract_checker.py",
"checks": checks,
"passed": passed,
}
assert passed
for claim_id in checks:
raw = (
root
/ ".openresearch"
/ "artifacts"
/ f"claim_{claim_id[1]}"
/ "raw"
)
raw.joinpath("independent_checker.json").write_text(
json.dumps(
{"claim_id": claim_id, **checks[claim_id], "passed": True},
indent=2,
sort_keys=True,
)
+ "\n"
)
output = root / "outputs" / "downstream_contract_checker.json"
output.parent.mkdir(parents=True, exist_ok=True)
output.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n")
print("DOWNSTREAM_CONTRACT_CHECKER")
print(json.dumps(result, sort_keys=True))
return result
|