diff --git a/composer/spec/natspec/pipeline.py b/composer/spec/natspec/pipeline.py index da353913..4d9123f4 100644 --- a/composer/spec/natspec/pipeline.py +++ b/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: diff --git a/composer/spec/natspec/registry.py b/composer/spec/natspec/registry.py index 7ed6d52f..dcf687d4 100644 --- a/composer/spec/natspec/registry.py +++ b/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 diff --git a/composer/spec/natspec/task_description.py b/composer/spec/natspec/task_description.py index bb337d6a..c310d322 100644 --- a/composer/spec/natspec/task_description.py +++ b/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): diff --git a/tests/test_file_registry_non_units.py b/tests/test_file_registry_non_units.py new file mode 100644 index 00000000..c2f85a09 --- /dev/null +++ b/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] diff --git a/tests/test_natspec_conf_path.py b/tests/test_natspec_conf_path.py new file mode 100644 index 00000000..f5b2f436 --- /dev/null +++ b/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" diff --git a/tests/test_stub_yields_bytecode.py b/tests/test_stub_yields_bytecode.py new file mode 100644 index 00000000..7514cc09 --- /dev/null +++ b/tests/test_stub_yields_bytecode.py @@ -0,0 +1,111 @@ +"""A stub that compiles but yields no bytecode must be rejected. + +`_compile_stub` gates every stub update. It used to trust solc's exit status, +which an `abstract contract` satisfies happily — solc returns 0 and emits no +bytecode. Certora's scene assembly then rejects the verification unit: + + Contract StreamShareSplitter has no bytecode. It may be caused because the + contract is abstract, or is missing constructor code. + +Every later typecheck in that session fails, `publish` is gated on the +typecheck, and nothing the CVL author does can recover it — the bad stub is +already in the VFS. A registry agent asked for storage fields, got back an +`abstract contract`, and the run produced four judge-approved specs that could +never be published. + +Implicit abstractness — inheriting a function you don't implement — has the +same effect and is covered here too, since it is easier to write by accident. +""" + +import contextlib +import pathlib +import shutil +import tempfile + +import pytest + +from composer.spec.natspec.registry import _compile_stub +from composer.spec.natspec.task_description import Assembler + +SOLC_VERSION = "8.29" +STUB_PATH = "Foo.sol" + +INTERFACE = """// SPDX-License-Identifier: MIT +pragma solidity ^0.8.29; + +interface IFoo { + function a() external view returns (uint256); + function b() external view returns (uint256); +} +""" + +CONCRETE = """// SPDX-License-Identifier: MIT +pragma solidity ^0.8.29; + +import "IFoo.sol"; + +contract Foo is IFoo { + function a() external view returns (uint256) { return 0; } + function b() external view returns (uint256) { return 0; } +} +""" + +# Compiles, emits no bytecode. +ABSTRACT = CONCRETE.replace("contract Foo", "abstract contract Foo") + +# Also compiles, also emits no bytecode: `b` is inherited but never implemented, +# which makes Foo implicitly abstract. +INCOMPLETE = """// SPDX-License-Identifier: MIT +pragma solidity ^0.8.29; + +import "IFoo.sol"; + +contract Foo is IFoo { + function a() external view returns (uint256) { return 0; } +} +""" + +pytestmark = pytest.mark.skipif( + shutil.which(f"solc{SOLC_VERSION}") is None, + reason=f"solc{SOLC_VERSION} not on PATH", +) + + +class InterfaceOnlyAssembler(Assembler): + """Project tree holding just the interface; the stub is written by the validator.""" + + @contextlib.asynccontextmanager + async def _dir(self): + with tempfile.TemporaryDirectory() as td: + root = pathlib.Path(td) + (root / "IFoo.sol").write_text(INTERFACE) + yield root + + def project_directory(self): + return self._dir() + + +@pytest.mark.asyncio +async def test_concrete_stub_is_accepted() -> None: + assert await _compile_stub(CONCRETE, InterfaceOnlyAssembler(), SOLC_VERSION, STUB_PATH) is None + + +@pytest.mark.asyncio +async def test_abstract_stub_is_rejected() -> None: + """The regression: solc exits 0 here and emits nothing, so only the + bytecode check catches it.""" + error = await _compile_stub(ABSTRACT, InterfaceOnlyAssembler(), SOLC_VERSION, STUB_PATH) + + assert error is not None, "an abstract stub was accepted" + # The message has to tell the agent what to change; it gets one retry loop. + assert "no bytecode" in error and "abstract" in error + + +@pytest.mark.asyncio +async def test_stub_with_an_unimplemented_member_is_rejected() -> None: + """Rejected by solc itself ("should be marked as abstract", non-zero exit) + rather than by the bytecode check — pinned so the two paths stay distinct.""" + error = await _compile_stub(INCOMPLETE, InterfaceOnlyAssembler(), SOLC_VERSION, STUB_PATH) + + assert error is not None, "a stub with an unimplemented member was accepted" + assert "should be marked as abstract" in error