From 36560b9fab8c119e5ef2ab3262409718742c5afe Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Tue, 11 Aug 2026 02:00:29 +0300 Subject: [PATCH 1/5] Fix doubled certora/ segment in the natspec typecheck conf path `temp_certora_file` yields a path already relative to the project root, so it carries the `certora/` segment (its docstring: "callers use it verbatim (no `certora/` prefixing)"). `ConfigurationBuilder._build_to` prefixed it a second time and yielded `/certora/certora/run_.conf`, a path nothing ever wrote to, so every natspec typecheck died with: read_from_conf_file: /tmp/tmpXXXXXXXX/certora/certora/run_YYYY.conf: not found `publish` is gated on a passing typecheck, so greenfield natspec runs could never emit a spec: the authoring agents produced complete, judge-approved CVL, burned their remaining turns retrying, and gave up. The pipeline still wrote the interface and the stub, which made the failure look like missing specs rather than a broken backend. The sibling call in the same `with` block, `with_verify(spec_file=...)`, already uses the yielded path verbatim. Adds a regression test asserting `build_to` yields a path that exists and sits under exactly one `certora` segment. Co-Authored-By: Claude Opus 5 --- composer/spec/natspec/task_description.py | 6 ++++-- tests/test_natspec_conf_path.py | 26 +++++++++++++++++++++++ 2 files changed, 30 insertions(+), 2 deletions(-) create mode 100644 tests/test_natspec_conf_path.py diff --git a/composer/spec/natspec/task_description.py b/composer/spec/natspec/task_description.py index bb337d6a7..24cf660ce 100644 --- a/composer/spec/natspec/task_description.py +++ b/composer/spec/natspec/task_description.py @@ -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_natspec_conf_path.py b/tests/test_natspec_conf_path.py new file mode 100644 index 000000000..366ce3331 --- /dev/null +++ b/tests/test_natspec_conf_path.py @@ -0,0 +1,26 @@ +"""``ConfigurationBuilder.build_to`` must yield the path it actually wrote to. + +``temp_certora_file`` yields a path already relative to the project root, i.e. +one that carries the ``certora/`` segment. Re-prefixing it produced +``/certora/certora/run_.conf`` — a path nothing ever wrote — and the +Certora CLI failed every natspec typecheck with ``read_from_conf_file: ... not +found``. Since ``publish`` is gated on a passing typecheck, no spec could ever +be published. +""" + +import json +import pathlib + +from composer.spec.natspec.task_description import ConfigurationBuilder + + +def test_build_to_yields_the_written_conf(tmp_path: pathlib.Path) -> None: + builder = ConfigurationBuilder({"solc": "solc8.29"}).with_files(["A.sol"]) + + with builder.build_to(tmp_path) as conf: + assert conf.is_file(), f"conf not written at yielded path: {conf}" + assert json.loads(conf.read_text()) == {"solc": "solc8.29", "files": ["A.sol"]} + # The regression: one `certora` segment, never two. + assert conf.relative_to(tmp_path).parts[:-1] == ("certora",) + + assert not conf.exists(), "conf should be cleaned up on context exit" From 9533f6c61741ee711a3dedeb7e62b2b95df673dc Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Tue, 11 Aug 2026 11:36:32 +0300 Subject: [PATCH 2/5] Fix the same doubled certora/ segment in the verify attribute MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `with_verify` re-prefixed `certora/` onto a spec path that already carried it, so the conf's `verify` attribute read :certora/certora/generated_.spec The Certora CLI validates that path against the process CWD (which typecheck.py sets to the project root), so it rejected every spec with attribute/flag 'verify': file certora/certora/generated_.spec not found This is the same mistake as the conf-location bug in the previous commit, one layer up: fixing only that one moved the failure from "conf not found" to "spec not found" without unblocking publish. Widens the regression test to assert the invariant both bugs broke — every path the conf hands to the CLI must resolve, from the project root, to a file on disk. The test now fails on either bug alone. Co-Authored-By: Claude Opus 5 --- composer/spec/natspec/task_description.py | 2 +- tests/test_natspec_conf_path.py | 43 ++++++++++++++++------- 2 files changed, 31 insertions(+), 14 deletions(-) diff --git a/composer/spec/natspec/task_description.py b/composer/spec/natspec/task_description.py index 24cf660ce..c310d3226 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( diff --git a/tests/test_natspec_conf_path.py b/tests/test_natspec_conf_path.py index 366ce3331..f5b2f4361 100644 --- a/tests/test_natspec_conf_path.py +++ b/tests/test_natspec_conf_path.py @@ -1,26 +1,43 @@ -"""``ConfigurationBuilder.build_to`` must yield the path it actually wrote to. +"""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. Re-prefixing it produced -``/certora/certora/run_.conf`` — a path nothing ever wrote — and the -Certora CLI failed every natspec typecheck with ``read_from_conf_file: ... not -found``. Since ``publish`` is gated on a passing typecheck, no spec could ever -be published. +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_build_to_yields_the_written_conf(tmp_path: pathlib.Path) -> None: - builder = ConfigurationBuilder({"solc": "solc8.29"}).with_files(["A.sol"]) +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",) - with builder.build_to(tmp_path) as conf: - assert conf.is_file(), f"conf not written at yielded path: {conf}" - assert json.loads(conf.read_text()) == {"solc": "solc8.29", "files": ["A.sol"]} - # The regression: one `certora` segment, 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" From 6eaa4f20738c27ea2f107b23e9a9a939145203ed Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Wed, 12 Aug 2026 01:32:45 +0300 Subject: [PATCH 3/5] Keep interfaces out of the Certora conf's files list MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Certora's scene assembly requires every entry in the conf's `files` to compile to bytecode. An interface never does, so one 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 pipeline registers only stubs, but the CVL-authoring agent registered the interface too — reasonably, since its spec references it and `register_verification_file` invited "any contract source the spec references". There is no unregister tool, so a session poisoned itself irrecoverably: the agent's own diagnosis after its sixth rejected publish was "blocking error is scene assembly of the pre-registered interface-only file". The registration also outlived the run that made it. FILES_NS is keyed by document digest and not by cache namespace, so re-running the same document under a fresh `--cache-ns` reused the poisoned entry. Hence two guards: `register` refuses these paths, and `read_all` filters them so entries written before this commit stay out of the conf. The interfaces are in the scene regardless, via the stubs' imports. Verified by running the real typecheck gate against a generated interface + stub with `rule sanity { assert true; }`: with the interface excluded from `files`, the gate passes. Co-Authored-By: Claude Opus 5 --- composer/spec/natspec/pipeline.py | 6 +++ composer/spec/natspec/registry.py | 50 ++++++++++++++++++-- tests/test_file_registry_non_units.py | 68 +++++++++++++++++++++++++++ 3 files changed, 119 insertions(+), 5 deletions(-) create mode 100644 tests/test_file_registry_non_units.py diff --git a/composer/spec/natspec/pipeline.py b/composer/spec/natspec/pipeline.py index f9a496c2f..89713fb3e 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 7ed6d52fc..043987ba5 100644 --- a/composer/spec/natspec/registry.py +++ b/composer/spec/natspec/registry.py @@ -519,19 +519,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 +574,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 +594,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 +658,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/tests/test_file_registry_non_units.py b/tests/test_file_registry_non_units.py new file mode 100644 index 000000000..c2f85a097 --- /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] From eccb7467197ba4e784068e31b6f57943eea16d37 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Wed, 12 Aug 2026 14:56:28 +0300 Subject: [PATCH 4/5] Require stub updates to yield bytecode, not merely to compile MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `_compile_stub` gates every stub update and trusted solc's exit status. An `abstract contract` satisfies that 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. — failing every subsequent typecheck in the session. `publish` is gated on the typecheck, so nothing the CVL author does afterwards can recover: the bad stub is already in the VFS and the spec is not what is wrong. This is not hypothetical. A registry agent asked for storage fields and got back `abstract contract StreamShareSplitter is IStreamShareSplitter`, which the validator accepted. All four components then produced judge-approved specs that could never be published, while the artifact dumped at the end was the pristine concrete stub from generation — so the failure was invisible in the output. Ask solc for the bytecode via --combined-json and require it to be non-empty. The rejection message names the two ways a contract ends up without bytecode so the agent can act on it within its retry loop. Note the neighbouring case is already safe: a contract that inherits a function it does not implement is a hard solc error ("should be marked as abstract"), so the exit-status path catches that one. Only explicit `abstract` slipped through. Both are pinned by tests. Co-Authored-By: Claude Opus 5 --- composer/spec/natspec/registry.py | 24 ++++++- tests/test_stub_yields_bytecode.py | 111 +++++++++++++++++++++++++++++ 2 files changed, 134 insertions(+), 1 deletion(-) create mode 100644 tests/test_stub_yields_bytecode.py diff --git a/composer/spec/natspec/registry.py b/composer/spec/natspec/registry.py index 043987ba5..dcf687d48 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 diff --git a/tests/test_stub_yields_bytecode.py b/tests/test_stub_yields_bytecode.py new file mode 100644 index 000000000..7514cc09b --- /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 From ed1f8d0eac6829e2200fd07955f0af49d3c9d2b4 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Wed, 12 Aug 2026 17:05:18 +0300 Subject: [PATCH 5/5] Let console-codegen take several spec files The workflow is already plumbed for N specs (`InputData.specs`), but the CLI mapped its triad to a one-element list, so there was no way to hand it more than one -- as `upload_input`'s comment noted, no producer needed it at the time. There is one now. Natspec emits one spec per component, four for a modest contract, and each carries its own copy of the shared ERC20 ghost model. Merging them by hand means reconciling duplicate ghosts, definitions and `methods` blocks; running codegen once per spec instead yields four unrelated implementations, each satisfying one component and ignoring the rest. `spec_file` becomes `nargs="+"`. The three-argument form parses exactly as before, so existing invocations are unaffected. `vfs_path` keys the specs downstream (audit's resume artifact indexes by it), so several specs are named after their files while a single spec keeps the conventional `rules.spec` -- recorded artifacts from single-spec runs stay valid. Two specs whose file names collide are refused by name rather than silently sharing a key, which would drop one of them. Co-Authored-By: Claude Opus 5 --- composer/input/parsing.py | 44 +++++++++++-- composer/input/types.py | 4 +- tests/test_codegen_multi_spec_input.py | 88 ++++++++++++++++++++++++++ 3 files changed, 129 insertions(+), 7 deletions(-) create mode 100644 tests/test_codegen_multi_spec_input.py diff --git a/composer/input/parsing.py b/composer/input/parsing.py index a90467ec8..b4a9f16ed 100644 --- a/composer/input/parsing.py +++ b/composer/input/parsing.py @@ -1,4 +1,5 @@ import argparse +import pathlib from typing import TypeVar, Protocol, cast, Annotated, get_type_hints, get_origin, Any, get_args, Union from composer.input.types import CommandLineArgs, ResumeArgs, Arg, OptionalArg, RAGDBOptions, ModelOptions, LanggraphOptions, UploadPaths, InputData, SpecInput from composer.input.files import FileUploader @@ -127,7 +128,11 @@ def _common_options(parser: argparse.ArgumentParser) -> None: def fresh_workflow_argument_parser() -> TypedArgumentParser[CommandLineArgs]: """Configure command line argument parser.""" parser = argparse.ArgumentParser(description="Certora AI Composer for Smart Contract Generation") - parser.add_argument("spec_file", help="Specification file for the smart contract") + parser.add_argument( + "spec_file", nargs="+", + help="One or more specification files for the smart contract. All of them " + "gate the generated code: it must satisfy every rule in every spec.", + ) parser.add_argument("interface_file", help="The interface file for the smart contract") parser.add_argument("system_doc", help="A text document describing the system") _common_options(parser) @@ -138,25 +143,52 @@ def fresh_workflow_argument_parser() -> TypedArgumentParser[CommandLineArgs]: async def upload_input(uploader: FileUploader, args: UploadPaths) -> InputData: """Turn the CLI's spec / interface / system-doc paths into an ``InputData``. - Spec and interface are unconditionally uploaded to the Files API as text + Specs and interface are unconditionally uploaded to the Files API as text (``upload_text_file_if_needed`` → ``UploadedTextFile``, a ``TextDocument``); the system doc goes through ``get_document`` so a PDF is uploaded while a text design doc stays inline. + + Each spec is materialized in the VFS under its own file name, since + ``vfs_path`` keys the specs downstream (audit's resume artifact indexes them + by it). A single spec keeps the conventional ``rules.spec`` name so existing + single-spec runs and their recorded artifacts are unaffected. """ - spec = await uploader.upload_text_file_if_needed(args.spec_file) + specs = [ + SpecInput(file=await uploader.upload_text_file_if_needed(path), vfs_path=vfs_path) + for path, vfs_path in zip(args.spec_file, _spec_vfs_paths(args.spec_file)) + ] intf = await uploader.upload_text_file_if_needed(args.interface_file) system_doc = await uploader.get_document(args.system_doc) if system_doc is None: raise FileNotFoundError(f"System document not found or not a file: {args.system_doc}") - # The legacy CLI triad is single-spec; map it to a one-element specs list at - # the conventional codegen path. The pipeline is plumbed for N specs. return InputData( - specs=[SpecInput(file=spec, vfs_path="rules.spec")], + specs=specs, system_doc=system_doc, intf=intf, ) +def _spec_vfs_paths(spec_files: list[str]) -> list[str]: + """VFS names for the CLI's spec paths: the file names, deduplicated by path. + + Distinct directories can hold same-named specs (``core/vault.spec`` and + ``periphery/vault.spec``), and a collision would silently drop one of them + from anything keyed by ``vfs_path``, so reject it with the offending name + rather than inventing a suffix the user never asked for. + """ + if len(spec_files) == 1: + return ["rules.spec"] + names = [pathlib.PurePath(p).name for p in spec_files] + duplicates = {n for n in names if names.count(n) > 1} + if duplicates: + raise ValueError( + f"Spec file names must be unique; got {len(names)} specs with repeated " + f"name(s): {', '.join(sorted(duplicates))}. Rename or copy them so each " + f"spec has a distinct file name." + ) + return names + + def _common_resume_args(parser: argparse.ArgumentParser) -> None: parser.add_argument("--commentary", default=None, help="Commentary describing the changes to the system. If prefixed with @, assumed to be a filename from which the commentary is read") parser.add_argument("src_thread_id", help="The thread id from which to resume the workflow") diff --git a/composer/input/types.py b/composer/input/types.py index c3eac6d1d..f9aed3125 100644 --- a/composer/input/types.py +++ b/composer/input/types.py @@ -141,7 +141,9 @@ class ExtendedModelOptions(_ModelOptionsCommon, Protocol): )] class UploadPaths(Protocol): - spec_file: str + # One or more specs, all gating the same generated contract (argparse + # ``nargs="+"``), hence a list even for the single-spec invocation. + spec_file: list[str] interface_file: str system_doc: str diff --git a/tests/test_codegen_multi_spec_input.py b/tests/test_codegen_multi_spec_input.py new file mode 100644 index 000000000..79dd899d1 --- /dev/null +++ b/tests/test_codegen_multi_spec_input.py @@ -0,0 +1,88 @@ +"""``console-codegen`` accepts N specs, all gating the same generated contract. + +The workflow has been plumbed for several specs (``InputData.specs``), but the +CLI mapped its triad to a one-element list, so there was no way to hand it more +than one. Natspec emits one spec per component — four for a modest contract — +and merging them by hand means reconciling four copies of the same ERC20 ghost +model, so the CLI is the thing that needed to move. + +``vfs_path`` keys the specs downstream (audit's resume artifact indexes by it), +so these pin the naming: one spec keeps the conventional ``rules.spec``, several +take their file names, and a name collision is refused rather than silently +dropping a spec. +""" + +import pytest + +from composer.input.files import FileUploader +from composer.input.parsing import fresh_workflow_argument_parser, upload_input + + +class FakeUploader(FileUploader): + """Records what it was asked to upload; returns the path as the document.""" + + def __init__(self) -> None: + self.uploaded: list[str] = [] + + async def upload_text_file_if_needed(self, path: str): # type: ignore[override] + self.uploaded.append(path) + return path + + async def get_document(self, path): # type: ignore[override] + return str(path) + + async def _upload_bytes(self, crc_basename: str, file_data: bytes, mime: str) -> str: + raise AssertionError("upload_input should not reach the binary upload path") + + +def _parse(argv: list[str]): + parser = fresh_workflow_argument_parser() + import sys + old, sys.argv = sys.argv, ["console-codegen", *argv] + try: + return parser.parse_args() + finally: + sys.argv = old + + +def test_single_spec_parses_as_before() -> None: + args = _parse(["rules.spec", "IFoo.sol", "design.md"]) + + assert args.spec_file == ["rules.spec"] + assert args.interface_file == "IFoo.sol" + assert args.system_doc == "design.md" + + +def test_several_specs_are_collected() -> None: + args = _parse(["a.spec", "b.spec", "c.spec", "IFoo.sol", "design.md"]) + + assert args.spec_file == ["a.spec", "b.spec", "c.spec"] + assert args.interface_file == "IFoo.sol" + assert args.system_doc == "design.md" + + +@pytest.mark.asyncio +async def test_one_spec_keeps_the_conventional_vfs_name() -> None: + args = _parse(["some/where/views.spec", "IFoo.sol", "design.md"]) + + data = await upload_input(FakeUploader(), args) + + assert [s.vfs_path for s in data.specs] == ["rules.spec"] + + +@pytest.mark.asyncio +async def test_several_specs_are_named_after_their_files() -> None: + args = _parse(["core/views.spec", "core/withdrawal.spec", "IFoo.sol", "design.md"]) + + data = await upload_input(FakeUploader(), args) + + assert [s.vfs_path for s in data.specs] == ["views.spec", "withdrawal.spec"] + assert [s.file for s in data.specs] == ["core/views.spec", "core/withdrawal.spec"] + + +@pytest.mark.asyncio +async def test_colliding_spec_names_are_refused() -> None: + args = _parse(["core/vault.spec", "periphery/vault.spec", "IFoo.sol", "design.md"]) + + with pytest.raises(ValueError, match="vault.spec"): + await upload_input(FakeUploader(), args)