diff --git a/composer/spec/source/report_prover.py b/composer/spec/source/report_prover.py index cabcc4e1..375254b4 100644 --- a/composer/spec/source/report_prover.py +++ b/composer/spec/source/report_prover.py @@ -1,16 +1,23 @@ """Prover-backend adapter for the property-keyed report. -Translates ProverOutputUtility's per-rule `CheckResult`s into the report's backend-agnostic +Translates per-rule prover results into the report's backend-agnostic `Verdict`/`Outcome` vocabulary. This is the only place the report stack touches `prover_output_utility` — the core report package is backend-neutral. + +A run link is either a cloud job URL or a local report directory, mirroring +``run_prover``'s own cloud/local split: ProverOutputUtility speaks only the former, so +a local run is read back with the same parser the run itself used. """ import asyncio import logging from pathlib import Path from prover_output_utility import ProverOutputAPI +from prover_output_utility.exceptions import ProverAPIError from prover_output_utility.models import CheckResult, NodeStatus +from composer.prover.ptypes import StatusCodes +from composer.prover.results import read_and_format_run_result from composer.spec.cvl_generation import GeneratedCVL from composer.spec.source.report.collect import Formalized, Verdict, VerdictFetcher from composer.spec.source.report.schema import Outcome, RuleName @@ -28,12 +35,46 @@ NodeStatus.PENDING: Outcome.UNKNOWN, } +# The local parser's vocabulary. SANITY_FAILED is a real failure of the rule's own +# sanity check; SKIPPED yielded no verdict at all. +_STATUS_TO_OUTCOME: dict[StatusCodes, Outcome] = { + "VERIFIED": Outcome.GOOD, + "VIOLATED": Outcome.BAD, + "ERROR": Outcome.ERROR, + "TIMEOUT": Outcome.TIMEOUT, + "SANITY_FAILED": Outcome.BAD, + "SKIPPED": Outcome.UNKNOWN, +} + + +def _fetch_local(path: Path) -> dict[RuleName, Verdict]: + """rule_name -> rolled-up `Verdict` from a local run's report directory, read with + the parser ``run_prover`` uses on the same directory. No line numbers or + durations: those come from POU, which a local run never went through.""" + parsed = read_and_format_run_result(path) + if isinstance(parsed, str): + _log.warning("report: could not read local prover results at %s: %s", path, parsed) + return {} + verdicts: dict[RuleName, Verdict] = {} + for result in parsed.values(): + name = RuleName(result.path.rule) + cand = Verdict(_STATUS_TO_OUTCOME.get(result.status, Outcome.UNKNOWN)) + verdicts[name] = cand.merge(verdicts.get(name)) + return verdicts + def _fetch(api: ProverOutputAPI, link: str) -> dict[RuleName, Verdict]: - """rule_name -> rolled-up `Verdict` for one prover run. Best-effort: any POU failure -> {}.""" + """rule_name -> rolled-up `Verdict` for one prover run, cloud or local. + + Best-effort: a fetch that fails yields no verdicts, which the report renders as + UNKNOWN. That silence is why the local branch matters — POU rejects a filesystem + path outright, so before it existed a local run reported every rule inconclusive.""" + if (local := Path(link)).is_dir(): + return _fetch_local(local) + try: checks: list[CheckResult] = api.get_all_checks(link) - except Exception: + except ProverAPIError: _log.warning("report: POU get_all_checks failed for %s", link, exc_info=True) return {} verdicts: dict[RuleName, Verdict] = {} @@ -51,9 +92,10 @@ def _fetch(api: ProverOutputAPI, link: str) -> dict[RuleName, Verdict]: def make_prover_fetcher(api: ProverOutputAPI | None = None) -> VerdictFetcher[GeneratedCVL]: - """A `VerdictFetcher` that pulls per-rule verdicts from ProverOutputUtility, keyed by each - component's run link. POU calls run off the event loop (one blocking call per run). Only ever - invoked for delivered results (collect skips gave-up / curtailed inputs).""" + """A `VerdictFetcher` that pulls per-rule verdicts for each component's run link — + from ProverOutputUtility for a cloud job, or off disk for a local one. Both are + blocking and run off the event loop (one call per run). Only ever invoked for + delivered results (collect skips gave-up / curtailed inputs).""" api = api or ProverOutputAPI() async def fetch(formalized: Formalized[GeneratedCVL]) -> dict[RuleName, Verdict]: diff --git a/tests/test_autoprove_report.py b/tests/test_autoprove_report.py index 542a9d49..b5c7a727 100644 --- a/tests/test_autoprove_report.py +++ b/tests/test_autoprove_report.py @@ -28,7 +28,7 @@ from composer.spec.source.artifacts import ProverArtifactStore from composer.spec.source.report import build -from composer.spec.source.report.collect import ReportComponentInput, collect +from composer.spec.source.report.collect import ReportComponentInput, Verdict, collect from composer.spec.source.report.coverage import ValidationError, validate from composer.spec.source.report.grouping import ( FALLBACK_SLUG, GroupingResult, PropertyGroupDraft, aggregate_status, @@ -40,7 +40,7 @@ GaveUpComponent, GroupStatus, ImpactLevel, IssueContent, LikelihoodLevel, Outcome, PropertyGroup, RuleVerdict, SeverityTier, SkippedClaim, ) -from composer.spec.source.report_prover import make_prover_fetcher +from composer.spec.source.report_prover import _fetch, make_prover_fetcher from composer.spec.source.report.collect import RuleEvidence from composer.spec.source.report.findings import FindingDraft, build_findings from composer.spec.source.cex_capture import CexAnalysisStore @@ -151,6 +151,92 @@ def _llm_type(self) -> str: return "structured-stub" +# --------------------------------------------------------------------------- +# prover adapter: cloud link vs local run directory +# --------------------------------------------------------------------------- +# +# `run_prover` runs either against the cloud or locally, and records the link +# accordingly — a job URL or a report directory. ProverOutputUtility only speaks the +# former and rejects a filesystem path outright, so before the local branch existed a +# local run reported every rule UNKNOWN while its verdicts sat on disk. + +class _StubAPI: + """Records what reached POU, so the local path can be shown to bypass it.""" + + def __init__(self, raises: Exception | None = None) -> None: + self.calls: list[str] = [] + self._raises = raises + + def get_all_checks(self, link): + self.calls.append(link) + if self._raises is not None: + raise self._raises + return [] + + +def _local_run(tmp_path: pathlib.Path, monkeypatch, results): + """A directory that looks like a prover report dir, with the run's own parser + stubbed to return ``results`` (a str stands for a parse failure).""" + monkeypatch.setattr( + "composer.spec.source.report_prover.read_and_format_run_result", + lambda path: results, + ) + run_dir = tmp_path / "emv-1-certora" + run_dir.mkdir() + return run_dir + + +def _result(rule: str, status: str): + return SimpleNamespace(path=SimpleNamespace(rule=rule), status=status) + + +@pytest.mark.parametrize(("status", "expected"), [ + # Only the two mappings a reader can't infer from the name. VERIFIED/VIOLATED + # are covered by the roll-up test below; the rest map onto themselves. + ("SANITY_FAILED", Outcome.BAD), # a rule whose own sanity check failed is not a pass + ("SKIPPED", Outcome.UNKNOWN), # ran nothing, so concluded nothing +]) +def test_local_statuses_that_are_not_self_evident(tmp_path, monkeypatch, status, expected): + run_dir = _local_run(tmp_path, monkeypatch, {"r": _result("r", status)}) + api = _StubAPI() + assert _fetch(cast(ProverOutputAPI, api), str(run_dir)) == {"r": Verdict(expected)} + assert api.calls == [] # POU never consulted for a local run + + +def test_local_verdicts_roll_up_the_most_terminal_outcome(tmp_path, monkeypatch): + """Parametric instantiations and invariant induction steps arrive as separate + results under one rule name.""" + run_dir = _local_run(tmp_path, monkeypatch, { + "a": _result("shared", "VERIFIED"), + "b": _result("shared", "VIOLATED"), + "c": _result("shared", "VERIFIED"), + }) + verdicts = _fetch(cast(ProverOutputAPI, _StubAPI()), str(run_dir)) + assert verdicts["shared"].outcome is Outcome.BAD + + +def test_an_unreadable_local_run_yields_no_verdicts(tmp_path, monkeypatch): + run_dir = _local_run(tmp_path, monkeypatch, "malformed tree view data") + assert _fetch(cast(ProverOutputAPI, _StubAPI()), str(run_dir)) == {} + + +def test_a_pou_failure_yields_no_verdicts(): + """Every POU exception derives from ProverAPIError — auth, job-not-found, parse — + so the whole documented surface degrades to UNKNOWN rather than failing the run.""" + from prover_output_utility.exceptions import AuthenticationError + + api = _StubAPI(raises=AuthenticationError("credentials expired")) + assert _fetch(cast(ProverOutputAPI, api), "https://prover.certora.com/output/1/a") == {} + + +def test_a_non_pou_exception_is_not_swallowed(): + """The catch is narrowed deliberately: a bug in our own code must not present as + a report full of inconclusive rules.""" + api = _StubAPI(raises=RuntimeError("bug in the adapter")) + with pytest.raises(RuntimeError): + _fetch(cast(ProverOutputAPI, api), "https://prover.certora.com/output/1/a") + + # --------------------------------------------------------------------------- # collect (async, in-memory) # ---------------------------------------------------------------------------