Let console-codegen take several spec files

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 DOCUMENT_SUFFIXES, FileUploader
@@ -142,7 +143,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)
@@ -153,25 +158,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")

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
 

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_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)