Fix report generation when using local Prover runs

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]:

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)
 # ---------------------------------------------------------------------------