bundle/v0/tests/test_theorem_audit.py

from __future__ import annotations

import copy
import importlib.util
import json
import shutil
from pathlib import Path

import pytest

from loss_aware_dro_repro.core import ContractError


ROOT = Path(__file__).resolve().parents[1]
SPEC = importlib.util.spec_from_file_location(
    "loss_aware_theorem_audit", ROOT / "scripts" / "validate_theorem_audit.py"
)
MODULE = importlib.util.module_from_spec(SPEC)
assert SPEC.loader is not None
SPEC.loader.exec_module(MODULE)


def load_audit() -> dict:
    return json.loads((ROOT / "configs" / "theorem-5.1-audit.json").read_text(encoding="utf-8"))


def test_canonical_audit_validates_and_fails_closed() -> None:
    audit = load_audit()
    MODULE.validate_audit(audit, root=ROOT)
    assert audit["all_assumptions_pass"] is False
    assert audit["executed_algorithm_within_theorem_scope"] is False
    assert audit["recommended_c2_verdict"] == "inconclusive"
    assert audit["falsification_status"] == "not_falsified"
    assert audit["schema_version"] == 2


def test_emitted_artifact_is_deterministic(tmp_path: Path) -> None:
    first = tmp_path / "first.json"
    second = tmp_path / "second.json"
    MODULE.emit_audit(artifact=first)
    MODULE.emit_audit(artifact=second)
    assert first.read_bytes() == second.read_bytes()
    assert first.read_bytes() == MODULE.render_audit(load_audit())


@pytest.mark.parametrize(
    ("mutation", "message"),
    [
        (lambda audit: audit.__setitem__("plan_hash", "sha256:" + "0" * 64), "plan_hash"),
        (lambda audit: audit.__setitem__("all_assumptions_pass", True), "all_assumptions_pass"),
        (lambda audit: audit.__setitem__("all_assumptions_pass", 0), "JSON boolean"),
        (
            lambda audit: audit.__setitem__("executed_algorithm_within_theorem_scope", True),
            "modified recurrences",
        ),
        (lambda audit: audit.__setitem__("recommended_c2_verdict", "verified"), "inconclusive"),
        (lambda audit: audit["source_evidence"]["paper"].__setitem__("citations", []), "non-empty"),
        (
            lambda audit: audit["source_evidence"]["davis"].__setitem__(
                "source_archive_sha256", "0" * 64
            ),
            "recorded source archive hash",
        ),
        (
            lambda audit: audit["assumptions"][3].__setitem__(
                "requirement", "Any unreviewed replacement text"
            ),
            "frozen theorem-audit content",
        ),
    ],
)
def test_forged_audit_is_rejected(mutation, message: str) -> None:
    audit = copy.deepcopy(load_audit())
    mutation(audit)
    with pytest.raises(ContractError, match=message):
        MODULE.validate_audit(audit, root=ROOT)


def test_every_assumption_has_three_way_traceability() -> None:
    audit = load_audit()
    assert {item["id"] for item in audit["assumptions"]} == {
        f"A{index}" for index in range(1, 13)
    }
    for item in audit["assumptions"]:
        assert item["classification"]
        assert item["paper_evidence"]
        assert item["author_code_evidence"]
        assert item["independent_code_evidence"]
        assert item["reason"]


def test_bound_source_artifact_bytes_are_rehashed(tmp_path: Path) -> None:
    (tmp_path / "configs").mkdir()
    shutil.copy2(ROOT / "configs" / "paper_scale.json", tmp_path / "configs" / "paper_scale.json")
    shutil.copy2(ROOT / "paper.json", tmp_path / "paper.json")
    audit = load_audit()
    for source_id in ("paper", "davis", "bolte_v1", "bolte_v2"):
        relative = Path(audit["source_evidence"][source_id]["artifact_path"])
        destination = tmp_path / relative
        destination.parent.mkdir(parents=True, exist_ok=True)
        shutil.copy2(ROOT / relative, destination)
    paper_artifact = tmp_path / audit["source_evidence"]["paper"]["artifact_path"]
    with paper_artifact.open("ab") as handle:
        handle.write(b"tamper")
    with pytest.raises(ContractError, match="bound source artifact hash mismatch"):
        MODULE.validate_audit(audit, root=tmp_path)