Let a plugin verify one buffer beside the author's others

composer/spec/source/author.py

@@ -1,4 +1,4 @@
-from typing import AsyncIterator, NotRequired, override, Literal, Annotated, Sequence, Protocol, Callable
+from typing import AsyncIterator, Mapping, NotRequired, override, Literal, Annotated, Sequence, Protocol, Callable
 
 from typing_extensions import TypedDict
 from contextlib import asynccontextmanager
@@ -28,9 +28,11 @@
 )
 from composer.prover.core import run_prover, CexHandler, ProverCallbacks, ProverReport
 from composer.spec.source.live_explorer import VersionedHistory, LiveEditTools, WIPE_HISTORY
-from composer.spec.source.prover import rule_selection, setup_prover_config_in
+from composer.spec.source.prover import (
+    buffer_conf, component_slug, materialize_buffers, rule_selection, setup_prover_config_in,
+)
 from composer.spec.source.spec_buffers import (
-    SpecBuffersExtra, buffer_review_text, buffer_state_digest, check_buffer_completion,
+    NamedBuffer, SpecBuffersExtra, buffer_review_text, buffer_state_digest, check_buffer_completion,
     combined_buffers_view, max_spec_buffers, requireinvariant_citations, run_targets,
     skips_review_digest, SKIPS_VALIDATION_KEY, validate_coverage, validate_declared_rules_mapped,
     validate_disjoint_rules, validate_requireinvariant_proved,
@@ -51,6 +53,7 @@
 from langgraph.graph import MessagesState
 from pathlib import Path
 from composer.spec.gen_types import (
+    CERTORA_DIR,
     CVLResource, SPECS_DIR, TypedTemplate, buffer_spec_path, import_statement_for,
 )
 from composer.spec.service_host import ServiceHost, Sort
@@ -825,6 +828,12 @@ class WrappedProverRunner:
     config: dict
     prover_options: ProverOptions
     main_contract: str
+    #: The author's buffers as they stood when the plugin read its state, and the
+    #: component directory they are materialized under. A run on a named buffer
+    #: stages all of them, with that buffer replaced by the text under test, so
+    #: the text's imports resolve to the same files the author's own runs see.
+    buffers: Mapping[str, NamedBuffer] = field(default_factory=dict)
+    slug: str = ""
 
     async def run(
         self,
@@ -836,22 +845,49 @@ async def run(
         tool_call_id: str,
         rules: list[str] | None = None,
         exclude_rules: list[str] | None = None,
+        buffer: str | None = None,
         **config,
     ) -> ProverReport | str:
         selection = rule_selection(rules, exclude_rules)
         if isinstance(selection, str):
             return selection
         # The spec/conf staging only has to outlive the run itself, so one call
         # stages, runs, and cleans up (the CVLAuthorState.prover_runner contract).
-        with setup_prover_config_in(
-            working_dir=working_dir,
-            spec_stem="adhoc_run",
-            main_contract=self.main_contract,
-            spec_contents=curr_spec,
-            config=self.config,
-            rules=selection,
-            **config
-        ) as (conf_path, _):
+        if buffer is None:
+            with setup_prover_config_in(
+                working_dir=working_dir,
+                spec_stem="adhoc_run",
+                main_contract=self.main_contract,
+                spec_contents=curr_spec,
+                config=self.config,
+                rules=selection,
+                **config
+            ) as (conf_path, _):
+                return await run_prover(
+                    pathlib.Path(working_dir),
+                    [conf_path],
+                    tool_call_id,
+                    self.prover_options,
+                    callbacks, cex_handler
+                )
+        if buffer not in self.buffers:
+            raise ValueError(f"no buffer named {buffer!r}; the author has {sorted(self.buffers)}")
+        if not self.slug:
+            raise ValueError("a buffer run needs the component slug its buffers are materialized under")
+        staged = {**self.buffers, buffer: self.buffers[buffer].model_copy(update={"cvl": curr_spec})}
+        with (
+            materialize_buffers(working_dir, staged, self.slug) as paths,
+            buffer_conf(
+                working_dir=working_dir,
+                config=self.config,
+                main_contract=self.main_contract,
+                spec_path=paths[buffer],
+                buffer_name=buffer,
+                conf_dir=CERTORA_DIR / "confs",
+                rules=selection,
+                **config,
+            ) as (conf_path, _),
+        ):
             return await run_prover(
                 pathlib.Path(working_dir),
                 [conf_path],
@@ -978,7 +1014,9 @@ async def propose(
                 prover_runner=WrappedProverRunner(
                     st["config"],
                     prover_tool.options,
-                    source.contract_name
+                    source.contract_name,
+                    buffers=st.get("buffers") or {},
+                    slug=component_slug(spec_stem, source.contract_name),
                 ).run,
                 host=task_host,
                 edit_store=_PluginStore()

composer/spec/source/plugin.py

@@ -27,7 +27,13 @@ class ProverRunner(Protocol):
     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."""
+    prover config for this run only.
+
+    ``buffer`` names the author's buffer that ``curr_spec`` is the (edited) text
+    of. The runner then stages it in that buffer's place, beside the author's
+    other buffers, so the ``import`` statements of the staged text resolve the
+    way they do in the author's own runs. ``None`` stages ``curr_spec`` on its
+    own, as a free-standing spec."""
     async def __call__(
         self,
         *,
@@ -38,6 +44,7 @@ async def __call__(
         tool_call_id: str,
         rules: list[str] | None = None,
         exclude_rules: list[str] | None = None,
+        buffer: str | None = None,
         **config,
     ) -> ProverReport | str:
         ...
@@ -69,7 +76,7 @@ class CVLAuthorState:
     working_dir: pathlib.Path
     # The spec under authoring, as its named buffers — each a self-contained CVL unit (its own rules,
     # methods{}, and imports). Every rule lives in exactly one buffer; ``spec_for_rule`` returns the CVL
-    # for a given rule.
+    # for a given rule, and ``prover_runner`` stages the whole set when asked to verify one buffer.
     buffers: Mapping[str, NamedBuffer]
     prover_runner: ProverRunner
     host: TaskHost

composer/spec/source/prover.py

@@ -701,6 +701,14 @@ def stuck_rule_nag(
     )
 
 
+def component_slug(spec_stem: str | None, main_contract: str) -> str:
+    """The directory a component's buffers are materialized under (``certora/specs/<slug>/``) and the
+    label prefix of its prover runs: the seeded spec stem, or the main contract, with the
+    ``autospec_`` prefix stripped. One definition, so the author's own runs and a plugin's runs on the
+    author's buffers land in the same place and the buffers' relative imports resolve identically."""
+    return (spec_stem or main_contract).removeprefix("autospec_")
+
+
 @contextmanager
 def materialize_buffers(
     working_dir: str, buffers: Mapping[str, NamedBuffer], slug: str
@@ -729,18 +737,22 @@ def buffer_conf(
     spec_path: str,
     buffer_name: str,
     conf_dir: Path,
-    msg: str,
+    msg: str = "",
     selection: RuleSelectionRecord | None = None,
+    rules: RuleSelection | None = None,
+    **config_extra,
 ) -> Iterator[tuple[str, dict]]:
     """Build a conf verifying an already-materialized buffer spec at ``spec_path`` (its imports resolve
-    to the sibling ``.spec`` files written by :func:`materialize_buffers`). ``selection`` restricts the
-    run to a subset of the buffer's rules. Yields (conf_path, config)."""
+    to the sibling ``.spec`` files written by :func:`materialize_buffers`). The run's scope is
+    ``selection`` (a recorded subset of the buffer's rules, as submit_buffer stripes them) or ``rules``
+    (a scope already built by :func:`rule_selection`); ``config_extra`` entries override the conf for
+    this run only, the way :func:`setup_prover_config_in` takes them. Yields (conf_path, config)."""
     cfg = prover_config_overlay(
         config,
         main_contract=main_contract,
         verify_target=f"{main_contract}:{spec_path}",
-        extra={"msg": msg},
-        rules=_scope_of(selection),
+        extra={"msg": msg, **config_extra},
+        rules=rules if rules is not None else _scope_of(selection),
     )
     with temp_certora_file(
         root=working_dir,
@@ -848,9 +860,8 @@ def get_prover_tool(
     stamper = make_validation_stamper(VALIDATION_KEY)
 
     def component_of(state: StateWithSkips) -> str:
-        """The label prefix for this generation's prover runs: its seeded spec stem, or the main
-        contract, with the ``autospec_`` prefix stripped."""
-        return (state.get("spec_stem") or main_contract).removeprefix("autospec_")
+        """The label prefix for this generation's prover runs (:func:`component_slug`)."""
+        return component_slug(state.get("spec_stem"), main_contract)
 
     # ---- Multi-buffer async submit / collect -------------------------------------------------
     # The agent submits each run-target buffer as an independent background job and consumes results

tests/test_wrapped_prover_runner.py

@@ -11,6 +11,8 @@
 
 from composer.prover.core import CexHandler, ProverCallbacks, ProverOptions, ProverReport
 from composer.spec.source.author import WrappedProverRunner
+from composer.spec.source.prover import component_slug
+from composer.spec.source.spec_buffers import NamedBuffer
 
 from .conftest import conf_of_prover_call
 
@@ -22,14 +24,25 @@ async def analyze(self, all_results, tool_call_id, callbacks, report_dir) -> str
         raise AssertionError("no violation was reported")
 
 
-def _runner() -> WrappedProverRunner:
+def _runner(**buffer_set) -> WrappedProverRunner:
     return WrappedProverRunner(
         config={"files": ["src/Foo.sol"]},
         prover_options=ProverOptions(app="evm"),
         main_contract="Foo",
+        **buffer_set,
     )
 
 
+#: An author with a shared buffer and a run-target buffer that imports it and the
+#: summaries a directory up, the way the author is told to write imports.
+SHARED = "ghost mathint total;\n"
+TARGET = 'import "shared.spec";\nimport "../summaries/erc20.spec";\nrule a { assert true; }\n'
+BUFFERS = {
+    "shared": NamedBuffer(name="shared", cvl=SHARED, is_run_target=False),
+    "target": NamedBuffer(name="target", cvl=TARGET, property_rules={"p": ["a"]}),
+}
+
+
 @pytest.fixture
 def staged_confs(monkeypatch) -> list[dict]:
     """Every conf the runner handed to ``run_prover``, in call order."""
@@ -45,8 +58,8 @@ async def fake_run_prover(folder: Path, args: list[str], *_rest, **_kw) -> Prove
     return confs
 
 
-async def _run(tmp_path: Path, **selection) -> ProverReport | str:
-    return await _runner().run(
+async def _run(tmp_path: Path, runner: WrappedProverRunner | None = None, **selection) -> ProverReport | str:
+    return await (runner or _runner()).run(
         curr_spec="rule a { assert true; }",
         working_dir=str(tmp_path),
         cex_handler=_NoCex(),
@@ -59,7 +72,7 @@ async def _run(tmp_path: Path, **selection) -> ProverReport | str:
 @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):
+        # The shape every plugin call has (a plugin's lemma runner included):
         # a rule list and nothing about exclusions.
         await _run(tmp_path, rules=["a"])
         [conf] = staged_confs
@@ -82,3 +95,63 @@ async def test_per_run_config_overrides_reach_the_conf(self, tmp_path, staged_co
         await _run(tmp_path, rules=["a"], compilation_steps_only=True)
         [conf] = staged_confs
         assert conf["compilation_steps_only"] is True
+
+
+@pytest.mark.asyncio
+class TestBufferRuns:
+    """A run on a named buffer stages the author's whole buffer set, with that
+    buffer replaced by the text under test, under the component's spec dir."""
+
+    async def test_the_buffer_set_is_staged_around_the_edited_text(self, tmp_path, monkeypatch):
+        seen: dict = {}
+
+        async def fake_run_prover(folder: Path, args: list[str], *_rest, **_kw) -> ProverReport:
+            conf = conf_of_prover_call(folder, args)
+            specs = folder / "certora" / "specs" / "foo"
+            seen.update(
+                conf=conf,
+                conf_path=args[0],
+                target=(specs / "target.spec").read_text(),
+                shared=(specs / "shared.spec").read_text(),
+            )
+            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)
+        edited = TARGET + "rule lemma_a { assert true; }\n"
+        runner = _runner(buffers=BUFFERS, slug="foo")
+        await runner.run(
+            curr_spec=edited, working_dir=str(tmp_path), cex_handler=_NoCex(), callbacks=ProverCallbacks(),
+            tool_call_id="tc", rules=["a"], buffer="target", msg="lemma run", compilation_steps_only=True,
+        )
+        assert seen["conf"]["verify"] == "Foo:certora/specs/foo/target.spec"
+        assert seen["conf_path"].startswith("certora/confs/verify_target")
+        assert seen["conf"]["rule"] == ["a"]
+        assert seen["conf"]["msg"] == "lemma run"
+        assert seen["conf"]["compilation_steps_only"] is True
+        # The text under test replaces the author's draft; the sibling it imports sits beside it.
+        assert seen["target"] == edited
+        assert seen["shared"] == SHARED
+        # Nothing staged outlives the run.
+        assert not (tmp_path / "certora" / "specs" / "foo").exists() or not any((tmp_path / "certora" / "specs" / "foo").iterdir())
+        assert not list((tmp_path / "certora" / "confs").glob("*.conf"))
+
+    async def test_without_a_buffer_name_the_text_is_staged_alone(self, tmp_path, staged_confs):
+        await _run(tmp_path, runner=_runner(buffers=BUFFERS, slug="foo"), rules=["a"])
+        [conf] = staged_confs
+        assert conf["verify"] == "Foo:certora/specs/adhoc_run.spec"
+
+    async def test_an_unknown_buffer_is_refused(self, tmp_path, staged_confs):
+        with pytest.raises(ValueError, match="no buffer named 'other'"):
+            await _run(tmp_path, runner=_runner(buffers=BUFFERS, slug="foo"), buffer="other")
+        assert staged_confs == []
+
+    async def test_a_buffer_run_needs_the_component_slug(self, tmp_path, staged_confs):
+        with pytest.raises(ValueError, match="component slug"):
+            await _run(tmp_path, runner=_runner(buffers=BUFFERS), buffer="target")
+        assert staged_confs == []
+
+
+def test_component_slug_strips_the_prefix_and_falls_back_to_the_contract():
+    assert component_slug("autospec_vault", "Vault") == "vault"
+    assert component_slug("custom", "Vault") == "custom"
+    assert component_slug(None, "Vault") == "Vault"