Fix the three defects blocking natspec spec publication

composer/spec/natspec/pipeline.py

@@ -549,6 +549,12 @@ async def gen_one_stub(
 
     file_registry = await FileRegistry.acreate(
         store, FILES_NS + (doc_digest,), materializer=mat_,
+        # The generated interfaces reach the scene through the stubs' imports
+        # and have no bytecode of their own, so they must never become
+        # compilation units. The registry refuses them and filters any that an
+        # earlier run persisted (this namespace is keyed by document digest,
+        # so registrations outlive a change of cache namespace).
+        non_units=frozenset(v.path for v in interface.name_to_interface.values()),
     )
 
     for c in summary.contract_components:

composer/spec/natspec/registry.py

@@ -9,6 +9,7 @@
 """
 
 import asyncio
+import json
 import logging
 from dataclasses import dataclass, field
 from typing import Callable, NotRequired, override, Iterable
@@ -104,15 +105,24 @@ async def _compile_stub(
     the tmpdir so relative ``import`` statements in the stub resolve the
     same way they will in the real project tree. Returns ``None`` on
     success, an error string on failure.
+
+    Compiling is necessary but not sufficient: an ``abstract contract`` — or
+    one that leaves an inherited function unimplemented, which makes it
+    implicitly abstract — compiles with exit status 0 and emits no bytecode.
+    Certora's scene assembly then rejects the verification unit ("Contract X
+    has no bytecode"), failing every subsequent typecheck with nothing in the
+    spec able to fix it. So ask solc for the bytecode and require it to be
+    non-empty, rather than trusting the exit status alone.
     """
     solc_name = f"solc{solc_version}"
+    identifier = pathlib.Path(stub_path).stem
     async with assembler.project_directory() as tmpdir:
         stub_abs = tmpdir / stub_path
         stub_abs.parent.mkdir(parents=True, exist_ok=True)
         stub_abs.write_text(stub)
         try:
             proc = await asyncio.create_subprocess_exec(
-                solc_name, stub_path,
+                solc_name, "--combined-json", "bin", stub_path,
                 stdout=asyncio.subprocess.PIPE,
                 stderr=asyncio.subprocess.PIPE,
                 cwd=tmpdir,
@@ -123,6 +133,18 @@ async def _compile_stub(
             return f"Solidity compiler {solc_name} not found"
         if proc.returncode != 0:
             return f"stdout:\n{stdout.decode()}\nstderr:\n{stderr.decode()}"
+        try:
+            compiled = json.loads(stdout.decode())["contracts"]
+        except (json.JSONDecodeError, KeyError) as e:
+            return f"Could not read the Solidity compiler's output ({e})"
+        if not compiled.get(f"{stub_path}:{identifier}", {}).get("bin"):
+            return (
+                f"{identifier} compiles but produces no bytecode, so it cannot "
+                f"be verified. A contract yields no bytecode when it is declared "
+                f"`abstract`, or when it inherits a function it does not "
+                f"implement. Declare it as a plain `contract` and give every "
+                f"member of the interface a body."
+            )
         return None
 
 
@@ -519,19 +541,31 @@ class FileRegistry:
     entry under ``_namespace`` keyed by contract name; ``read_all_contracts``
     enumerates via ``asearch``. The lock serializes the read-modify-write that
     backs ``register``'s per-path dedupe within a single contract.
+
+    ``_non_units`` holds paths that must never become compilation units — the
+    generated interfaces. Certora's scene assembly requires every entry in the
+    conf's ``files`` to compile to bytecode, and an interface does not, so one
+    such entry fails the build for every spec in the session. Interfaces reach
+    the scene anyway, via the stub's ``import``. ``register`` refuses them, and
+    ``read_all`` filters them, so entries persisted by an earlier run (this
+    namespace is keyed by document digest, not by cache namespace) can't
+    resurface.
     """
     _store: BaseStore
     _materializer: Materializer
     _lock: asyncio.Lock = field(default_factory=asyncio.Lock)
     _namespace: tuple[str, ...] = ()
+    _non_units: frozenset[str] = frozenset()
 
     @staticmethod
     async def acreate(
         store: BaseStore,
         namespace: tuple[str, ...],
         materializer: Materializer,
+        non_units: frozenset[str] = frozenset(),
     ) -> "FileRegistry":
         return FileRegistry(
+            _non_units=non_units,
             _store=store, _materializer=materializer, _namespace=namespace,
         )
 
@@ -562,8 +596,16 @@ async def read_all(self, contract_identifier: SolidityIdentifier) -> list[str]:
 
         Each entry is either ``path`` or ``path:Identifier`` depending on
         whether a Solidity identifier was supplied at registration.
+
+        Non-compilation units are filtered here as well as refused at
+        registration, so entries written before that guard existed stay out of
+        the conf.
         """
-        return [e.as_prover_arg() for e in await self._read_contract(contract_identifier)]
+        return [
+            e.as_prover_arg()
+            for e in await self._read_contract(contract_identifier)
+            if e.path not in self._non_units
+        ]
 
     async def register(
         self,
@@ -574,14 +616,29 @@ async def register(
         """Register ``path`` as a compilation-unit file for ``contract_identifier``.
 
         Rejects paths that don't exist in the layered FS this registry closes
-        over. If ``path`` is already registered for this contract, the
-        existing entry's ``solidity_identifier`` is overwritten (latest call
-        wins). Each path appears at most once per contract.
+        over, and paths in ``_non_units`` (the generated interfaces). If
+        ``path`` is already registered for this contract, the existing entry's
+        ``solidity_identifier`` is overwritten (latest call wins). Each path
+        appears at most once per contract.
         """
         _log.debug(
             "FileRegistry.register: ns=%r contract=%s path=%s ident=%s",
             self._namespace, contract_identifier, path, solidity_identifier,
         )
+        if path in self._non_units:
+            _log.debug(
+                "FileRegistry.register: REJECTED ns=%r contract=%s "
+                "path=%s (interface, not a compilation unit)",
+                self._namespace, contract_identifier, path,
+            )
+            return (
+                f"{path} is an interface, so it cannot be a compilation unit: "
+                f"Certora requires every registered file to compile to "
+                f"bytecode, and registering this one would fail the build for "
+                f"every spec in this session. It is already part of the scene "
+                f"— the stub that implements it imports it — so the spec can "
+                f"reference it without registration."
+            )
         if self._materializer.get(path) is None:
             _log.debug(
                 "FileRegistry.register: REJECTED ns=%r contract=%s "
@@ -623,9 +680,14 @@ def get_tools(self, contract_identifier: SolidityIdentifier) -> list[BaseTool]:
         class RegisterSpecFile(WithAsyncImplementation[str]):
             """Register a Solidity source file that must be pulled into the
             verification task for the spec you're authoring. Use this for any
-            contract source the spec references, e.g.,
+            *deployable* contract source the spec references, e.g.,
             other stubs, extant code the stubs don't cover (if applicable)
 
+            Do NOT register interfaces. Every registered file must compile to
+            bytecode, which an interface never does. The interfaces your stubs
+            implement are already in the scene through the stubs' ``import``
+            statements, so your spec can reference them without registration.
+
             The path must be project-relative and point to a ``.sol`` file
             already present in the source tree (inspect the tree with the
             source tools if unsure). Registration of a path that does not

composer/spec/natspec/task_description.py

@@ -113,7 +113,7 @@ def with_files(self, files: list[str]) -> Self:
         return self._replace(files=list(files))
 
     def with_verify(self, *, main_contract: SolidityIdentifier, spec_file: str) -> Self:
-        return self._replace(verify=f"{main_contract}:certora/{spec_file}")
+        return self._replace(verify=f"{main_contract}:{spec_file}")
 
     def with_solc(self, version: str) -> Self:
         return self._replace(
@@ -156,8 +156,10 @@ def _build_to(self, path: pathlib.Path) -> Iterator[pathlib.Path]:
             root=str(path),
             ext="conf",
             prefix="run",
-        ) as basename:
-            yield path / "certora" / basename
+        ) as rel_conf:
+            # temp_certora_file yields a project-root-relative path that already
+            # carries the `certora/` segment, so join it to the root verbatim.
+            yield path / rel_conf
 
 
 class Assembler(ABC):

tests/test_file_registry_non_units.py

@@ -0,0 +1,68 @@
+"""Interfaces must never reach the Certora conf's ``files`` list.
+
+Certora's scene assembly requires every entry in ``files`` to compile to
+bytecode. An interface does not, so a single interface entry fails the build
+for *every* spec authored in that session:
+
+    Contract IFoo has no bytecode. It may be caused because the contract is
+    abstract, or is missing constructor code.
+
+The CVL-authoring agent used to register them — the spec references the
+interface, and the tool invited it — with no way to undo. Worse, the registry's
+namespace is keyed by document digest and not by cache namespace, so a bad
+registration outlived every subsequent run on the same document, including runs
+under a fresh ``--cache-ns``. Hence both guards: refuse at registration, and
+filter at read so already-persisted entries stay out of the conf.
+"""
+
+import pytest
+from langgraph.store.memory import InMemoryStore
+
+from composer.spec.natspec.registry import FileEntry, FileRegistry
+from composer.spec.types import SolidityIdentifier
+
+CONTRACT = SolidityIdentifier("Foo")
+STUB = "Foo.sol"
+INTERFACE = "IFoo.sol"
+NS = ("test", "spec_files")
+
+
+class FakeMaterializer:
+    """Composite-FS stand-in: every known path resolves, others don't."""
+
+    def __init__(self, paths: set[str]):
+        self._paths = paths
+
+    def get(self, path: str) -> bytes | None:
+        return b"// solidity" if path in self._paths else None
+
+
+@pytest.fixture
+def registry() -> FileRegistry:
+    return FileRegistry(
+        _store=InMemoryStore(),
+        _materializer=FakeMaterializer({STUB, INTERFACE}),  # type: ignore[arg-type]
+        _namespace=NS,
+        _non_units=frozenset({INTERFACE}),
+    )
+
+
+@pytest.mark.asyncio
+async def test_register_refuses_an_interface(registry: FileRegistry) -> None:
+    await registry.register(CONTRACT, STUB)
+    message = await registry.register(CONTRACT, INTERFACE)
+
+    assert INTERFACE in message and "compilation unit" in message
+    assert await registry.read_all(CONTRACT) == [STUB]
+
+
+@pytest.mark.asyncio
+async def test_read_all_filters_an_interface_persisted_by_an_earlier_run(
+    registry: FileRegistry,
+) -> None:
+    """A registration written before the guard existed must not resurface."""
+    await registry._write_contract(
+        CONTRACT, [FileEntry(path=STUB), FileEntry(path=INTERFACE)]
+    )
+
+    assert await registry.read_all(CONTRACT) == [STUB]

tests/test_natspec_conf_path.py

@@ -0,0 +1,43 @@
+"""Natspec typecheck paths must point at files that were actually written.
+
+``temp_certora_file`` yields a path already relative to the project root, i.e.
+one that carries the ``certora/`` segment. ``ConfigurationBuilder`` prefixed that
+segment a second time in two places — the conf's own location and the ``verify``
+attribute — producing ``certora/certora/...`` paths nothing ever wrote to. The
+Certora CLI then failed every natspec typecheck (``read_from_conf_file: ... not
+found``, then ``attribute/flag 'verify': file ... not found``), and since
+``publish`` is gated on a passing typecheck, no spec could ever be published.
+
+The invariant both cases violated: every path the conf hands to the CLI must
+resolve, from the project root, to a file on disk. ``typecheck.py`` runs the CLI
+with ``cwd`` set to that root, so the CLI resolves them the same way.
+"""
+
+import json
+import pathlib
+
+from composer.spec.natspec.task_description import ConfigurationBuilder
+from composer.spec.types import SolidityIdentifier
+from composer.spec.util import temp_certora_file
+
+
+def test_conf_paths_resolve_from_the_project_root(tmp_path: pathlib.Path) -> None:
+    """Mirrors typecheck.run_typecheck: materialize a spec, build a conf around it."""
+    with temp_certora_file(content="rule sanity { assert true; }", root=str(tmp_path), ext="spec") as spec_file:
+        builder = (
+            ConfigurationBuilder({"solc": "solc8.29"})
+            .with_files(["A.sol"])
+            .with_verify(main_contract=SolidityIdentifier("A"), spec_file=spec_file)
+        )
+        with builder.build_to(tmp_path) as conf:
+            assert conf.is_file(), f"conf not written at yielded path: {conf}"
+            # One `certora` segment in the conf's own location, never two.
+            assert conf.relative_to(tmp_path).parts[:-1] == ("certora",)
+
+            config = json.loads(conf.read_text())
+            verify_path = config["verify"].partition(":")[2]
+            assert (tmp_path / verify_path).is_file(), (
+                f"verify points at a file that was never written: {verify_path}"
+            )
+
+    assert not conf.exists(), "conf should be cleaned up on context exit"