From dcfe5a6933c5dc48b1260a24e771e006e4431d9d Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Wed, 16 Sep 2026 18:33:04 +0300 Subject: [PATCH] Pass exclude_rules through the plugin-facing prover runner WrappedProverRunner.run is the ProverRunner a plugin gets through CVLAuthorState. setup_prover_config_in requires exclude_rule, so every plugin prover call raised a TypeError before anything was staged. The runner and the ProverRunner protocol now take exclude_rules next to rules, the way verify_spec scopes its own runs, and a unit test drives the runner against a mocked run_prover. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01CMrKc9bciyU9yKag4wH4Ev --- composer/spec/source/author.py | 2 + composer/spec/source/plugin.py | 7 ++- tests/test_wrapped_prover_runner.py | 84 +++++++++++++++++++++++++++++ 3 files changed, 91 insertions(+), 2 deletions(-) create mode 100644 tests/test_wrapped_prover_runner.py diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index 3810e453..92f6d7d4 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -692,6 +692,7 @@ async def run( callbacks: ProverCallbacks, tool_call_id: str, rules: list[str] | None = None, + exclude_rules: list[str] | None = None, **config, ) -> ProverReport | str: # The spec/conf staging only has to outlive the run itself, so one call @@ -703,6 +704,7 @@ async def run( spec_contents=curr_spec, config=self.config, rule=rules, + exclude_rule=exclude_rules, **config ) as (conf_path, _): return await run_prover( diff --git a/composer/spec/source/plugin.py b/composer/spec/source/plugin.py index b54eac1d..500e1e33 100644 --- a/composer/spec/source/plugin.py +++ b/composer/spec/source/plugin.py @@ -23,8 +23,10 @@ class ProverRunner(Protocol): """One ad-hoc prover run: stages the spec/conf into ``working_dir`` for the - duration of the call and forwards to ``run_prover``. ``config`` entries - override the author's current prover config for this run only.""" + duration of the call and forwards to ``run_prover``. ``rules`` and + ``exclude_rules`` scope the run the way ``verify_spec`` scopes its own runs + (at most one of them); ``config`` entries override the author's current + prover config for this run only.""" async def __call__( self, *, @@ -34,6 +36,7 @@ async def __call__( callbacks: ProverCallbacks, tool_call_id: str, rules: list[str] | None = None, + exclude_rules: list[str] | None = None, **config, ) -> ProverReport | str: ... diff --git a/tests/test_wrapped_prover_runner.py b/tests/test_wrapped_prover_runner.py new file mode 100644 index 00000000..e09e7d7b --- /dev/null +++ b/tests/test_wrapped_prover_runner.py @@ -0,0 +1,84 @@ +"""``WrappedProverRunner`` is the ``ProverRunner`` handed to plugins through +``CVLAuthorState``: one ad-hoc prover run that stages the spec and conf into the +working directory, forwards to ``run_prover``, and cleans up. + +The prover core is mocked at ``composer.spec.source.author.run_prover``; the conf +the runner staged is read back from the path it passed on. +""" +from pathlib import Path + +import pytest + +from composer.prover.core import CexHandler, ProverCallbacks, ProverOptions, ProverReport +from composer.spec.source.author import WrappedProverRunner + +from .conftest import conf_of_prover_call + + +class _NoCex(CexHandler): + """The mocked prover never reports a violation, so this is never reached.""" + + async def analyze(self, all_results, tool_call_id, callbacks, report_dir) -> str: + raise AssertionError("no violation was reported") + + +def _runner() -> WrappedProverRunner: + return WrappedProverRunner( + config={"files": ["src/Foo.sol"]}, + prover_options=ProverOptions(), + main_contract="Foo", + ) + + +@pytest.fixture +def staged_confs(monkeypatch) -> list[dict]: + """Every conf the runner handed to ``run_prover``, in call order.""" + confs: list[dict] = [] + + async def fake_run_prover(folder: Path, args: list[str], *_rest, **_kw) -> ProverReport: + confs.append(conf_of_prover_call(folder, args)) + return ProverReport( + result_str="ok", link="local://test", raw_rule_status={}, certora_run_stdout="" + ) + + monkeypatch.setattr("composer.spec.source.author.run_prover", fake_run_prover) + return confs + + +async def _run(tmp_path: Path, **selection) -> ProverReport | str: + return await _runner().run( + curr_spec="rule a { assert true; }", + working_dir=str(tmp_path), + cex_handler=_NoCex(), + callbacks=ProverCallbacks(), + tool_call_id="tc", + **selection, + ) + + +@pytest.mark.asyncio +class TestWrappedProverRunner: + async def test_runs_with_a_rule_selection(self, tmp_path, staged_confs): + # The shape every plugin call has (dz-strategy's ``lemma_prover`` included): + # a rule list and nothing about exclusions. + await _run(tmp_path, rules=["a"]) + [conf] = staged_confs + assert conf["rule"] == ["a"] + assert "exclude_rule" not in conf + + async def test_runs_with_no_selection(self, tmp_path, staged_confs): + await _run(tmp_path) + [conf] = staged_confs + assert "rule" not in conf + assert "exclude_rule" not in conf + + async def test_exclusions_reach_the_conf(self, tmp_path, staged_confs): + await _run(tmp_path, exclude_rules=["b"]) + [conf] = staged_confs + assert conf["exclude_rule"] == ["b"] + assert "rule" not in conf + + async def test_per_run_config_overrides_reach_the_conf(self, tmp_path, staged_confs): + await _run(tmp_path, rules=["a"], compilation_steps_only=True) + [conf] = staged_confs + assert conf["compilation_steps_only"] is True