diff --git a/composer/cargo/__init__.py b/composer/cargo/__init__.py new file mode 100644 index 00000000..083d3c5c --- /dev/null +++ b/composer/cargo/__init__.py @@ -0,0 +1 @@ +"""Tools for interacting with Cargo builds and workspaces.""" diff --git a/composer/cargo/features.py b/composer/cargo/features.py new file mode 100644 index 00000000..72558c67 --- /dev/null +++ b/composer/cargo/features.py @@ -0,0 +1,9 @@ +"""The name of a cargo feature.""" + +from typing import TYPE_CHECKING + +# ``CargoFeature``: a feature's name, as ``[features]`` declares it and ``--features`` takes it. +if TYPE_CHECKING: + class CargoFeature(str): ... +else: + CargoFeature = str diff --git a/composer/cargo/manifest.py b/composer/cargo/manifest.py new file mode 100644 index 00000000..0a873feb --- /dev/null +++ b/composer/cargo/manifest.py @@ -0,0 +1,244 @@ +"""Reading and editing a ``Cargo.toml``. + +Only the tables the CVLR scaffold consults are declared. Everything else in a manifest is +accepted and ignored, so a manifest cargo takes is not refused here for a table this module +never reads. + +Parsing is ``tomlkit``'s for reading and editing alike, so what is validated is what is edited. +:class:`ManifestEditor` keeps everything it does not change as it was, comments included. +""" + +from collections.abc import Mapping, Sequence +from dataclasses import dataclass +from pathlib import Path + +import tomlkit +from pydantic import BaseModel, ConfigDict, ValidationError, model_validator +from tomlkit.exceptions import TOMLKitError +from tomlkit.items import InlineTable, Item, Table + +from composer.cargo.features import CargoFeature + + +class MalformedManifest(RuntimeError): + """A ``Cargo.toml`` could not be read, parsed, or does not have cargo's shape.""" + + +class _ManifestModel(BaseModel): + model_config = ConfigDict(frozen=True, extra="ignore") + + +class Dependency(_ManifestModel): + """One dependency entry, from ``[dependencies]``, ``[workspace.dependencies]``, or a patch + table. + + The fields are not exclusive: cargo allows ``version`` beside ``path`` or ``git``, where the + version is what a publish of the dependent uses. + """ + + version: str | None = None + git: str | None = None + path: str | None = None + #: ``workspace = true``: the entry inherits the root's ``[workspace.dependencies]`` one. + workspace: bool = False + + @model_validator(mode="before") + @classmethod + def _bare_requirement(cls, data: object) -> object: + """``foo = "1.0"`` is cargo's shorthand for ``foo = { version = "1.0" }``.""" + return {"version": data} if isinstance(data, str) else data + + +class CertoraMetadata(_ManifestModel): + """``[package.metadata.certora]``, the prover's build settings. Its keys are not read here.""" + + +class PackageMetadata(_ManifestModel): + """``[package.metadata]``. Free-form: cargo passes it to tools without reading it, so only the + tool tables something here consults are declared.""" + + certora: CertoraMetadata | None = None + + +class PackageTable(_ManifestModel): + metadata: PackageMetadata = PackageMetadata() + + +class WorkspaceTable(_ManifestModel): + dependencies: dict[str, Dependency] = {} + + +class Manifest(_ManifestModel): + #: ``None`` for a virtual workspace manifest. + package: PackageTable | None = None + #: ``None`` when the manifest has no ``[workspace]``. An empty ``[workspace]`` still makes + #: the manifest a workspace root. + workspace: WorkspaceTable | None = None + dependencies: dict[str, Dependency] = {} + features: dict[CargoFeature, list[str]] = {} + #: Keyed by the source being patched (``crates-io``, or a registry or git URL), then by crate. + patch: dict[str, dict[str, Dependency]] = {} + + @property + def workspace_dependencies(self) -> dict[str, Dependency]: + return self.workspace.dependencies if self.workspace is not None else {} + + @property + def certora_metadata(self) -> CertoraMetadata | None: + return self.package.metadata.certora if self.package is not None else None + + +_UNPARSEABLE = (TOMLKitError, ValidationError) + + +def _parsed(text: str) -> tuple[tomlkit.TOMLDocument, Manifest]: + document = tomlkit.parse(text) + return document, Manifest.model_validate(document.unwrap()) + + +def parse_manifest(text: str) -> Manifest: + return ManifestEditor(text).manifest + + +def read_manifest(path: Path) -> Manifest: + return ManifestEditor.read(path).manifest + + +#: A table's name, one key per level: ``("package", "metadata", "certora")``. +type TablePath = tuple[str, ...] + +#: A value :class:`ManifestEditor` writes. A mapping is written as an inline table. +type TomlValue = str | bool | Sequence[str] | Mapping[str, str | bool] + + +@dataclass(frozen=True) +class Comment: + """A comment line inside a table :class:`AddTable` creates.""" + + text: str + + +type TableItem = tuple[str, TomlValue] | Comment + + +@dataclass(frozen=True) +class AddEntries: + """Keys added to ``table``, which is created when the manifest has none.""" + + table: TablePath + entries: tuple[tuple[str, TomlValue], ...] + + def describe(self) -> str: + return f"[{'.'.join(self.table)}] {', '.join(key for key, _ in self.entries)}" + + +@dataclass(frozen=True) +class AddTable: + """A table the manifest does not have yet, created with ``body`` in order. The tables above + it are created as needed, without headers of their own.""" + + table: TablePath + body: tuple[TableItem, ...] + + def describe(self) -> str: + return f"[{'.'.join(self.table)}]" + + +type ManifestAddition = AddEntries | AddTable + + +class ManifestConflict(ValueError): + """An addition collides with what the manifest already has.""" + + +class ManifestEditor: + """One ``Cargo.toml``, parsed once, to read and to add to. + + Edits only add. A new table is built whole before it is placed, which is what keeps its keys + together and its spacing like the tables around it. + """ + + def __init__(self, text: str, *, origin: str = "Cargo.toml") -> None: + """``origin`` names the file in a :class:`MalformedManifest`.""" + try: + self._document, self.manifest = _parsed(text) + except _UNPARSEABLE as exc: + raise MalformedManifest(f"{origin}: {exc}") from exc + self._original = text + + @classmethod + def read(cls, path: Path) -> "ManifestEditor": + try: + text = path.read_text() + except OSError as exc: + raise MalformedManifest(f"{path}: {exc}") from exc + return cls(text, origin=str(path)) + + def apply(self, addition: ManifestAddition, *, note: str) -> None: + """Make ``addition``. ``note`` is a comment on each added line, or once on a new table's + header. Raises :class:`ManifestConflict` when a key or table it adds is already there.""" + match addition: + case AddEntries(table=table, entries=entries): + existing = self._find(table) + if existing is None: + self._add_table(table, entries, note=note) + else: + for key, value in entries: + _insert(existing, table, key, value, note=note) + case AddTable(table=table, body=body): + self._add_table(table, body, note=note) + + def text(self) -> str: + """The manifest with the edits, ending in as many newlines as it did.""" + edited = tomlkit.dumps(self._document) + ending = len(self._original) - len(self._original.rstrip("\n")) + return edited.rstrip("\n") + "\n" * ending + + def _add_table(self, table: TablePath, body: Sequence[TableItem], *, note: str) -> None: + if self._find(table) is not None: + raise ManifestConflict(f"[{'.'.join(table)}] already exists") + parent: tomlkit.TOMLDocument | Table = self._document + for name in table[:-1]: + if name not in parent: + parent.add(name, tomlkit.table(is_super_table=True)) + found = parent[name] + if not isinstance(found, Table): + raise ManifestConflict(f"{name} in [{'.'.join(table)}] is not a table") + parent = found + created = tomlkit.table() + created.comment(note) + for item in body: + match item: + case Comment(text=text): + created.add(tomlkit.comment(text)) + case (key, value): + created.add(key, _item(value)) + created.add(tomlkit.nl()) + parent.add(table[-1], created) + + def _find(self, table: TablePath) -> Table | InlineTable | None: + container: object = self._document + for name in table: + if not isinstance(container, tomlkit.TOMLDocument | Table | InlineTable): + return None + if name not in container: + return None + container = container[name] + return container if isinstance(container, Table | InlineTable) else None + + +def _insert( + container: Table | InlineTable, table: TablePath, key: str, value: TomlValue, *, note: str +) -> None: + if key in container: + raise ManifestConflict(f"[{'.'.join(table)}] already has {key}") + container[key] = _item(value) + container[key].comment(note) + + +def _item(value: TomlValue) -> Item: + if isinstance(value, Mapping): + inline = tomlkit.inline_table() + inline.update(value) + return inline + return tomlkit.item(value) diff --git a/composer/cargo/metadata.py b/composer/cargo/metadata.py new file mode 100644 index 00000000..4f9a3abc --- /dev/null +++ b/composer/cargo/metadata.py @@ -0,0 +1,382 @@ +"""Typed ``cargo metadata`` for a Cargo workspace. + +Answers two questions the host has to answer; an agent must not guess them: + +* Which crate owns a source file — the ``source_unit`` half of + :mod:`composer.rustapp.toolchain`, and the package name a build command needs. +* Which version of a dependency this build resolves. ``RUST_FORBIDDEN_READ`` + hides ``Cargo.lock`` from agents. Reading a different CVLR than the build + compiles is worse than reading none. + +``cargo metadata`` runs no build scripts and no proc-macros, so it needs no +confinement — unlike :mod:`composer.cargo.session`. It does resolve the +dependency graph, which needs a warm cache or the network; see +:meth:`Workspace.read`'s ``offline``. +""" + +import asyncio +import shutil +import subprocess +from dataclasses import dataclass +from pathlib import Path +from urllib.parse import parse_qs, urlsplit, urlunsplit + +from pydantic import AliasChoices, BaseModel, ConfigDict, Field, ValidationError + +from composer.cargo.features import CargoFeature + +#: Crate types that make a target the library of its package. Bins, tests, and +#: examples are never the verification target. +_LIB_CRATE_TYPES = frozenset({"lib", "rlib", "dylib", "cdylib", "staticlib", "proc-macro"}) + +#: On a cold cache this resolves (and may download) the whole dependency graph. +METADATA_TIMEOUT_S = 300 + + +class CargoUnavailable(RuntimeError): + """``cargo`` is not on ``PATH``, or could not be started.""" + + +@dataclass(frozen=True) +class CargoFailed: + """``cargo metadata`` exited non-zero. ``stderr`` is cargo's own explanation.""" + + stderr: str + + def describe(self) -> str: + return self.stderr.strip() + + +@dataclass(frozen=True) +class CargoTimedOut: + seconds: int + + def describe(self) -> str: + return ( + f"cargo metadata did not finish within {self.seconds}s; on a first read it may still " + f"have been downloading dependencies" + ) + + +@dataclass(frozen=True) +class UnreadableMetadata: + """``cargo metadata`` succeeded but printed output that does not validate.""" + + error: str + + def describe(self) -> str: + return f"cargo metadata printed output that could not be read: {self.error}" + + +#: Why :meth:`Workspace.read` has no workspace to return. +type MetadataFailure = CargoFailed | CargoTimedOut | UnreadableMetadata + + +class _CargoJson(BaseModel): + """cargo adds fields across releases; only the ones read here are declared.""" + + model_config = ConfigDict(frozen=True, extra="ignore") + + +class CargoTargetJson(_CargoJson): + name: str + src_path: Path + #: Older cargos report only ``kind``. + crate_types: tuple[str, ...] = Field( + default=(), validation_alias=AliasChoices("crate_types", "kind") + ) + + +class CargoPackageJson(_CargoJson): + id: str + name: str + version: str + manifest_path: Path + targets: tuple[CargoTargetJson, ...] = () + features: dict[CargoFeature, list[str]] = {} + source: str | None = None + + +class CargoMetadataJson(_CargoJson): + """The parts of ``cargo metadata --format-version 1`` output this module reads.""" + + packages: tuple[CargoPackageJson, ...] + workspace_root: Path + workspace_members: tuple[str, ...] = () + target_directory: Path | None = None + + +@dataclass(frozen=True) +class LibTarget: + """A package's library target. + + ``name`` is not always the package name; cargo allows them to differ, and + the artifact is named after the target. ``src_path`` comes from cargo, not + the ``src/lib.rs`` convention, because ``[lib] path`` can move it. + """ + + name: str + src_path: Path + crate_types: tuple[str, ...] + + @property + def artifact_stem(self) -> str: + return self.name.replace("-", "_") + + @property + def builds_shared_object(self) -> bool: + """Whether this target produces the loadable object the Solana prover needs. + + An ``rlib``-only package compiles and produces nothing to verify. + """ + return "cdylib" in self.crate_types + + +@dataclass(frozen=True) +class RegistrySource: + """A package from a ``registry+`` index. ``spelling`` is cargo's, verbatim.""" + + spelling: str + + +@dataclass(frozen=True) +class GitBranch: + name: str + + +@dataclass(frozen=True) +class GitTag: + name: str + + +@dataclass(frozen=True) +class GitRev: + rev: str + + +type GitReference = GitBranch | GitTag | GitRev + + +@dataclass(frozen=True) +class GitSource: + """A package from a git repository. + + cargo spells it ``git+[?branch=|?tag=|?rev=][#]``. + """ + + spelling: str + #: The repository URL as the manifest named it, without the reference or the commit. + repository: str + #: ``None`` when the manifest names no reference and cargo follows the default branch. + reference: GitReference | None + #: The commit the build resolved to. + commit: str | None + + @classmethod + def parse(cls, spelling: str) -> "GitSource": + parts = urlsplit(spelling.removeprefix("git+")) + query = parse_qs(parts.query) + reference: GitReference | None = None + if branch := query.get("branch"): + reference = GitBranch(branch[0]) + elif tag := query.get("tag"): + reference = GitTag(tag[0]) + elif rev := query.get("rev"): + reference = GitRev(rev[0]) + return cls( + spelling=spelling, + repository=urlunsplit(parts._replace(query="", fragment="")), + reference=reference, + commit=parts.fragment or None, + ) + + def is_from(self, repository: str) -> bool: + """Whether this is ``repository``, however the two URLs spell it. + + The scheme, a user, a trailing ``.git`` or ``/``, and case are ignored: ``https://`` and + ``ssh://git@`` reach the same repository, and GitHub paths are case-insensitive. + """ + return _repository_key(self.repository) == _repository_key(repository) + + +def _repository_key(url: str) -> tuple[str, str]: + parts = urlsplit(url) + path = parts.path.rstrip("/").removesuffix(".git") + return (parts.hostname or "", path.lower()) + + +@dataclass(frozen=True) +class OtherSource: + """A source kind not distinguished here, such as an alternative registry's + ``sparse+`` index.""" + + spelling: str + + +type PackageSource = RegistrySource | GitSource | OtherSource + + +def _package_source(spelling: str | None) -> PackageSource | None: + if spelling is None: + return None + if spelling.startswith("registry+"): + return RegistrySource(spelling) + if spelling.startswith("git+"): + return GitSource.parse(spelling) + return OtherSource(spelling) + + +@dataclass(frozen=True) +class CratePackage: + name: str + version: str + manifest_path: Path + lib: LibTarget | None + features: tuple[CargoFeature, ...] + #: ``None`` for a workspace member or a path dependency. + source: PackageSource | None + + @property + def root(self) -> Path: + return self.manifest_path.parent + + @property + def is_local(self) -> bool: + return self.source is None + + +@dataclass(frozen=True) +class Workspace: + root: Path + target_directory: Path + members: tuple[CratePackage, ...] + #: Every package the graph resolves, members included. + packages: tuple[CratePackage, ...] + + @classmethod + async def read( + cls, + project_root: Path, + *, + offline: bool = False, + features: tuple[CargoFeature, ...] = (), + timeout_s: int = METADATA_TIMEOUT_S, + ) -> "Workspace | MetadataFailure": + """The workspace containing ``project_root``, or why there is none. + + A failure covers no manifest, an unparseable one, or a graph that will not + resolve, and carries cargo's own explanation; whether that is fatal is the + caller's decision. Missing cargo raises: that is a machine problem, not a + project problem. + + ``offline`` passes ``--offline``. Pass it when a warm cache is guaranteed; + leave it off for the first read of an unseen project. + + ``features`` selects the graph the verification build resolves. Pass it + whenever the answer is about CVLR. A scaffolded project marks CVLR crates + ``optional = true`` behind the ``certora`` feature; a default-feature read + then reports them as absent. Features resolve against the package cargo + considers current, so pass the package directory as ``project_root`` when + naming one. + """ + payload = await asyncio.to_thread( + _cargo_metadata, + project_root, + offline=offline, + features=features, + timeout_s=timeout_s, + ) + return parse_metadata(payload) if isinstance(payload, CargoMetadataJson) else payload + + def owning(self, path: Path) -> CratePackage | None: + """The member whose directory contains ``path``. Deepest match, so a nested + crate wins over the workspace-root package that also contains it.""" + try: + resolved = path.resolve() + except OSError: + return None + containing = [m for m in self.members if resolved.is_relative_to(m.root)] + return max(containing, key=lambda m: len(m.root.parts)) if containing else None + + def member(self, name: str) -> CratePackage | None: + """Unique when present: cargo refuses a workspace with two members of one name.""" + return next((m for m in self.members if m.name == name), None) + + def resolved(self, name: str) -> tuple[CratePackage, ...]: + """Every copy of ``name`` this build compiles against, member or not. + + Usually one. A graph holds several when dependents require semver-incompatible + releases, or the same release from different sources, and cargo builds each. + """ + return tuple(p for p in self.packages if p.name == name) + + def family(self, prefix: str) -> tuple[CratePackage, ...]: + """Every resolved package named ``prefix`` or ``prefix-*``. + + Crate families are a naming convention, not a cargo feature (``cvlr`` + pulls in ``cvlr-asserts``, ``cvlr-log``, …). + """ + return tuple( + p for p in self.packages if p.name == prefix or p.name.startswith(f"{prefix}-") + ) + + +def _lib_target(raw: CargoPackageJson) -> LibTarget | None: + for target in raw.targets: + if _LIB_CRATE_TYPES.intersection(target.crate_types): + return LibTarget( + name=target.name, src_path=target.src_path, crate_types=target.crate_types + ) + return None + + +def _package(raw: CargoPackageJson) -> CratePackage: + return CratePackage( + name=raw.name, + version=raw.version, + manifest_path=raw.manifest_path, + lib=_lib_target(raw), + features=tuple(sorted(raw.features)), + source=_package_source(raw.source), + ) + + +def parse_metadata(payload: CargoMetadataJson) -> Workspace: + """Build a :class:`Workspace` from validated ``cargo metadata --format-version 1`` output.""" + by_id = {raw.id: _package(raw) for raw in payload.packages} + root = payload.workspace_root + return Workspace( + root=root, + target_directory=payload.target_directory or root / "target", + members=tuple(by_id[i] for i in payload.workspace_members if i in by_id), + packages=tuple(by_id.values()), + ) + + +def _cargo_metadata( + project_root: Path, *, offline: bool, features: tuple[CargoFeature, ...], timeout_s: int +) -> CargoMetadataJson | MetadataFailure: + if shutil.which("cargo") is None: + raise CargoUnavailable( + "cargo is not on PATH; a Rust chain's toolchain cannot be resolved without it" + ) + args = ["cargo", "metadata", "--format-version", "1"] + if offline: + args.append("--offline") + if features: + args += ["--features", ",".join(features)] + try: + completed = subprocess.run( + args, cwd=project_root, capture_output=True, text=True, timeout=timeout_s + ) + except subprocess.TimeoutExpired: + return CargoTimedOut(timeout_s) + except OSError as exc: + raise CargoUnavailable(f"cargo could not be started: {exc}") from exc + if completed.returncode != 0: + return CargoFailed(completed.stderr) + try: + return CargoMetadataJson.model_validate_json(completed.stdout) + except ValidationError as exc: + return UnreadableMetadata(str(exc)) + diff --git a/composer/cargo/session.py b/composer/cargo/session.py new file mode 100644 index 00000000..fca9b0d7 --- /dev/null +++ b/composer/cargo/session.py @@ -0,0 +1,223 @@ +"""Reused workdir for a Rust compile loop, and the fast compile gate. + +A compile sits in the authoring inner loop. Each run also gets a private +``CARGO_HOME`` so an untrusted ``build.rs`` cannot poison a later run +(:func:`~composer.sandbox.recipes.sandbox_cargo_home`). Fetching the dependency +graph on every edit is too slow, so the workdir is owned by a session and +:meth:`CargoSession.warm` fetches once. + +Warm vs compile is a trust boundary (``docs/command-sandbox.md`` §5). +``cargo fetch`` downloads and does not execute, so it runs unconfined with the +network. Compile runs confined and offline, using the deps the warm already +fetched. + +The fast tier is a host-target ``cargo check``, not the chain build. +""" + +import logging +import time +from dataclasses import dataclass, field +from pathlib import Path +from typing import Literal + +from composer.cargo.features import CargoFeature +from composer.sandbox.command import CommandResult, run_local_command +from composer.sandbox.config import SandboxConfig +from composer.sandbox.recipes import sandbox_cargo_home + +_log = logging.getLogger(__name__) + +#: ``fast`` runs on every write; ``slow`` only before a prover submission. +type CompileTier = Literal["fast", "slow"] + +#: A cold ``cargo fetch`` of a real program can take several minutes. +WARM_TIMEOUT_S = 900 +#: Long enough for a cold graph; short enough that a stuck compiler times out +#: inside one authoring turn. +CHECK_TIMEOUT_S = 600 + + +@dataclass(frozen=True) +class Compiled: + pass + + +@dataclass(frozen=True) +class CompileFailed: + """``diagnostics`` is rustc's human-format output, unparsed.""" + + diagnostics: str + exit_code: int + + +type CompileVerdict = Compiled | CompileFailed + + +@dataclass(frozen=True) +class CompileRun: + tier: CompileTier + duration_ms: int + verdict: CompileVerdict + #: Copied onto the result so an unconfined verdict is visible. + #: :class:`CargoSession` logs the operator warning. + confined: bool + + @property + def ok(self) -> bool: + return isinstance(self.verdict, Compiled) + + +@dataclass(frozen=True) +class Warmed: + pass + + +@dataclass(frozen=True) +class WarmFailed: + """Logged, not raised: a partial cache still compiles what it has, and the + later build error names the missing crate.""" + + diagnostics: str + exit_code: int + + +type WarmOutcome = Warmed | WarmFailed + + +@dataclass +class CargoSession: + """A workdir reused across an authoring session's compiles. + + ``workdir`` is where every command runs, and the only path the confinement + policy grants read-write. The caller chooses it and cleans it up; the session + does not create or delete it. + """ + + workdir: Path + sandbox: SandboxConfig + #: Keyed by the cargo binary. Two cargos do not share a git cache, so a + #: cache filled by one is not warm for the other. + _warmed: set[str] = field(default_factory=set, repr=False, compare=False) + + def __post_init__(self) -> None: + if not self.sandbox.enabled: + _log.warning( + "cargo session in %s is UNCONFINED (COMPOSER_SANDBOX_PROVIDER=none): build scripts " + "and proc-macros from the analyzed project run with this process's privileges. " + "Development only — every result produced this way is marked unconfined.", + self.workdir, + ) + + @property + def confined(self) -> bool: + return self.sandbox.enabled + + @property + def cargo_home(self) -> Path | None: + """Private per-run home when confined, else the process default. + + Warm runs outside the sandbox, so it has to use the same directory the + confined build will read (:func:`~composer.sandbox.recipes.sandbox_cargo_home`). + """ + return sandbox_cargo_home(self.workdir) if self.sandbox.enabled else None + + async def run_confined( + self, program: str, args: list[str], *, timeout_s: int + ) -> CommandResult: + """Run a command in the workdir under this session's confinement. + + If the configured provider cannot confine, this raises instead of falling + back. + """ + return await run_local_command( + program, + args, + {}, + workdir=self.workdir, + timeout_s=timeout_s, + provider=self.sandbox.resolve_provider() if self.sandbox.enabled else None, + policy=self.sandbox.build_policy(self.workdir), + ) + + async def run_unconfined( + self, program: str, args: list[str], *, timeout_s: int + ) -> CommandResult: + """Run a command in the workdir with the network and no confinement. + + For prep steps only (``docs/command-sandbox.md`` §5). Uses the session's + cargo home so the confined build can read the cache. + """ + home = self.cargo_home + if home is not None: + home.mkdir(parents=True, exist_ok=True) + return await run_local_command( + program, + args, + {}, + workdir=self.workdir, + timeout_s=timeout_s, + env_overlay={"CARGO_HOME": str(home)} if home is not None else None, + ) + + async def warm( + self, + *, + manifest_dirs: tuple[Path, ...] = (), + cargo: Path | str = "cargo", + timeout_s: int = WARM_TIMEOUT_S, + ) -> WarmOutcome: + """Fetch this session's dependency graph, unconfined and online, once. + + ``manifest_dirs`` are directories with a ``Cargo.toml``, relative to the + workdir. Empty means the workdir itself. Pass more than one when the + verification crate sits outside the program's workspace: each root has + its own graph. + + A cache is only warm for the cargo that filled it. The chain build uses + the cargo inside platform-tools, not the one on ``PATH``, and the two + store git dependencies in different places. + """ + dirs = manifest_dirs or (Path("."),) + for d in dirs: + manifest = self.workdir / d / "Cargo.toml" + fetched = await self.run_unconfined( + str(cargo), ["fetch", "--manifest-path", str(manifest)], timeout_s=timeout_s + ) + if fetched.exit_code != 0: + _log.info("cargo fetch for %s failed (%s)", manifest, fetched.exit_code) + return WarmFailed( + diagnostics=fetched.stderr.strip(), exit_code=fetched.exit_code + ) + self._warmed.add(str(cargo)) + return Warmed() + + def already_warmed(self, cargo: Path | str) -> bool: + return str(cargo) in self._warmed + + async def check( + self, + *, + package: str | None = None, + features: tuple[CargoFeature, ...] = (), + manifest_dir: Path | None = None, + timeout_s: int = CHECK_TIMEOUT_S, + ) -> CompileRun: + """Host-target ``cargo check``, confined. Fast enough to run on every write.""" + args = ["check", "--quiet"] + if manifest_dir is not None: + args += ["--manifest-path", str(self.workdir / manifest_dir / "Cargo.toml")] + if package is not None: + args += ["--package", package] + if features: + args += ["--features", ",".join(features)] + started = time.perf_counter() + checked = await self.run_confined("cargo", args, timeout_s=timeout_s) + elapsed = int((time.perf_counter() - started) * 1000) + verdict: CompileVerdict = ( + Compiled() + if checked.exit_code == 0 + else CompileFailed(diagnostics=checked.stderr.strip(), exit_code=checked.exit_code) + ) + return CompileRun( + tier="fast", duration_ms=elapsed, verdict=verdict, confined=self.confined + ) diff --git a/composer/prover/conf.py b/composer/prover/conf.py new file mode 100644 index 00000000..5706ae42 --- /dev/null +++ b/composer/prover/conf.py @@ -0,0 +1,71 @@ +"""Prover confs as data: writing them, and scoping one to a run's rule selection. + +Shared by every ecosystem. What a conf contains is each ecosystem's own policy +(:func:`composer.spec.source.prover.prover_config_overlay` for CVL, +:func:`composer.spec.cvlr.conf.solana_conf` for Solana). +""" + +import json +import re +import string +from dataclasses import dataclass + +#: A conf: the top-level JSON object. +type Conf = dict[str, object] + + +def dump_conf(conf: Conf) -> str: + """Serialize a conf for writing.""" + return json.dumps(conf, indent=2) + "\n" + + +#: Characters ``certoraRun`` accepts in ``msg``. A subset of what the CLI permits today, so a +#: narrower CLI set still accepts these. The CLI raises on anything outside its set before any +#: rule is processed. +_MSG_SAFE = set(string.ascii_letters) | set(string.digits) | set(" ,.:_-()[]'/") + + +def safe_msg(msg: str) -> str: + """``msg`` reduced to what the prover accepts. + + A message built from prose fails on one stray character: ``"Deposit & Balance Tracking"`` + raises ``{'&'} not allowed in 'msg'`` before any rule is read. + + Characters outside the set become spaces, so words do not run together, and runs of whitespace + collapse. Length is left to the CLI, which truncates with a warning. + """ + return re.sub(r"\s+", " ", "".join(c if c in _MSG_SAFE else " " for c in msg)).strip() + + +@dataclass(frozen=True) +class InheritRules: + """Check whatever the base conf selects: its ``rule`` and ``exclude_rule`` entries, or every + rule when it has neither.""" + + def apply_to(self, conf: Conf) -> Conf: + return conf + + +@dataclass(frozen=True) +class SelectRules: + """Check these rules. Names are globs, which is how a parametric rule's instances are named.""" + + names: tuple[str, ...] + + def apply_to(self, conf: Conf) -> Conf: + return {**conf, "rule": list(self.names)} + + +@dataclass(frozen=True) +class ExcludeRules: + """Check every rule the base conf selects except these.""" + + names: tuple[str, ...] + + def apply_to(self, conf: Conf) -> Conf: + return {**conf, "exclude_rule": list(self.names)} + + +#: A run's rule scope. ``apply_to(conf)`` returns ``conf`` scoped to it, writing only the key the +#: selection names. +type RuleSelection = InheritRules | SelectRules | ExcludeRules diff --git a/composer/spec/cvlr/__init__.py b/composer/spec/cvlr/__init__.py new file mode 100644 index 00000000..054f0c31 --- /dev/null +++ b/composer/spec/cvlr/__init__.py @@ -0,0 +1 @@ +"""The CVLR backend — properties formalized as Rust rules and checked by the Certora Solana Prover.""" diff --git a/composer/spec/cvlr/conf.py b/composer/spec/cvlr/conf.py new file mode 100644 index 00000000..49445769 --- /dev/null +++ b/composer/spec/cvlr/conf.py @@ -0,0 +1,118 @@ +"""A Solana submission's prover conf: fixed settings, the ones the author may change, and one run's. + +Every conf is built here, never read from the project. :data:`BASE_CONF` is fixed. +:class:`TunableConf` holds what the author may change, and :func:`tunable_conf` renders it onto +the fixed part. :func:`solana_conf` adds one submission's +keys: the build script, the message, the rule selection, and the summary files. + +``solana_inlining`` is left unset. ``cargo certora-sbf`` reads it from the package's +``[package.metadata.certora]`` and reports it through the build manifest. The prover applies that +declaration only when the conf has none. + +``solana_summaries`` is set when the run passes summary files. A summary is a regex over symbols +and applies to the whole build, so one package-level file would apply one unit's summaries to +every other unit. The run names a per-unit file, composed from the starting layers plus the unit's +own. Naming any value stops the prover from also applying the package's own declaration. +""" + +from dataclasses import dataclass, field +from pathlib import Path + +from composer.cargo.features import CargoFeature +from composer.prover.conf import Conf, InheritRules, RuleSelection, dump_conf, safe_msg +from composer.spec.util import string_hash + +#: Conf keys no author or run changes. +#: +#: ``rule_sanity`` is ``basic``. With the check off, a [3308] inside the generated vacuity rule is +#: reported as verified. +#: +#: ``prover_args`` has none of the ``-solanaOptimistic*`` flags: they are unsound, and they do not +#: fix the [3308] they were meant to. +BASE_CONF: Conf = { + "smt_timeout": "6000", + "rule_sanity": "basic", + "prover_args": [ + "-unsatCoresForAllAsserts true", + "-solanaSkipCallRegInst true", + "-solanaTACOptimize 2", + "-solanaStackSize 8192", + "-solanaTACMathInt true", + ], +} + + +@dataclass(frozen=True) +class TunableConf: + """The conf settings the author may change. The defaults are where every unit starts.""" + + #: 2, not 1. With a bound of 1, a loop inside a handler fails before the rule's property is + #: reached: an Anchor handler comes back violated on "Unwinding condition in a loop" against a + #: loop in its borsh path. + loop_iter: int = 2 + #: Off. The author treats it as a last resort, preferring to bound the inputs that set the trip + #: count first, then summarize or munge the code that holds the loop, then raise ``loop_iter``, + #: and finally turn it on only for a trip count that no bound discharges. Once it is on, every + #: rule in the submission is verified under that assumption. + optimistic_loop: bool = False + + +def tunable_conf(tunable: TunableConf) -> Conf: + """The conf ``tunable`` describes, before any one submission's keys are added.""" + return { + **BASE_CONF, + "loop_iter": str(tunable.loop_iter), + "optimistic_loop": tunable.optimistic_loop, + } + + +def conf_history(tunable: TunableConf) -> tuple[str, ...]: + """The conf as a ``version_history`` token, so a stamp from before a change goes stale. + + A conf decides the loop bound, the solver flags, and whether vacuity is checked. A verdict + under one conf does not apply to another. The token hashes the rendered conf rather than the + ``tunable``, so a change to the fixed part invalidates a stamp too. + """ + return (f"conf:{string_hash(dump_conf(tunable_conf(tunable)))}",) + + +#: The platform-tools release every build uses. The prover does not apply ``cargo_tools_version`` +#: itself: it reaches ``cargo certora-sbf`` only on the CLI's own build path, and this backend owns +#: the build. One release serves every target because the reference set pins one platform +#: generation (:class:`~composer.spec.cvlr.reference.PlatformGeneration`). +PLATFORM_TOOLS_VERSION = "v1.43" + + +#: The cargo feature that compiles the verification module into the program. The scaffold writes +#: this name (``certora = ["no-entrypoint", "dep:cvlr", …]``), and preflight passes it to +#: ``cargo check``. +DEFAULT_FEATURE = CargoFeature("certora") + + +@dataclass(frozen=True) +class RunOverlay: + """What one submission adds to the conf its :class:`TunableConf` describes. + + ``build_script`` is a path as the prover reads it: relative to the directory + ``certoraSolanaProver`` runs in, which is the session's workdir. + """ + + build_script: Path + rules: RuleSelection = field(default_factory=InheritRules) + msg: str = "" + #: Points-to summary files, in the same relative-to-the-workdir spelling as ``build_script``. + #: Empty leaves the key unset, so the package's ``[package.metadata.certora]`` declaration + #: still applies. + summaries: tuple[Path, ...] = () + + +def solana_conf(tunable: TunableConf, run: RunOverlay) -> Conf: + """The conf for one ``certoraSolanaProver`` submission.""" + conf = { + **tunable_conf(tunable), + "build_script": str(run.build_script), + "msg": safe_msg(run.msg), + } + if run.summaries: + conf["solana_summaries"] = [str(s) for s in run.summaries] + return run.rules.apply_to(conf) diff --git a/composer/spec/cvlr/crates.py b/composer/spec/cvlr/crates.py new file mode 100644 index 00000000..4975b616 --- /dev/null +++ b/composer/spec/cvlr/crates.py @@ -0,0 +1,122 @@ +"""Which CVLR crates this build resolves, and the source trees they resolve to. + +The version comes from the resolved graph. ``RUST_FORBIDDEN_READ`` hides ``Cargo.lock`` from +agents, and source for a different version than the build compiles is worse than no source. +:meth:`CvlrSources.of` reports each crate together with the directory it came from. + +:mod:`composer.spec.cvlr.reference` records the one CVLR line this build supports. +:meth:`CvlrSources.gaps` reports where a project's graph and that line disagree, which +:mod:`composer.spec.cvlr.scaffold` refuses over before anything is written. It runs again after the +scaffold as a backstop: a :class:`Mismatched` at that point means a release reached the graph some +way the scaffold's gate does not see, such as a ``[patch]`` table. +""" + +from dataclasses import dataclass +from pathlib import Path +from typing import Self + +from composer.cargo.metadata import CratePackage, Workspace +from composer.spec.cvlr.reference import ChainReference + +#: The crate-name prefix that spells the CVLR family. Its members are not declared anywhere — ``cvlr`` +#: pulls in ``cvlr-asserts``, ``cvlr-log``, ``cvlr-nondet``, ``cvlr-mathint`` and more as ordinary +#: dependencies — so the family is recognized by name, which is also how a reader recognizes it. +CVLR_PREFIX = "cvlr" + + +@dataclass(frozen=True) +class Mismatched: + """The target builds a CVLR release other than the one this build supports. + + A refusal: everything the scaffold writes is :attr:`reference`'s, and pinning those crates + beside :attr:`resolved` puts two CVLR generations in one graph. + """ + + crate: str + #: What the reference set records. + reference: str + #: What this project's build resolves. + resolved: str + + def describe(self) -> str: + return ( + f"{self.crate} {self.resolved} is what this project builds; this build supports " + f"{self.reference}" + ) + + +@dataclass(frozen=True) +class Absent: + """The target does not depend on a reference-set crate at all. + + Not a refusal, and the reason the two are separate types. A project with no ``cvlr-solana`` is + not on an old chain crate, it is on none — the ordinary state of a specialization it has no + use for. Reported so a run can say which reference-set crates this project does not have. + """ + + crate: str + reference: str + + def describe(self) -> str: + return ( + f"{self.crate} is not a dependency of this project, so nothing that uses it " + f"applies here" + ) + + +#: Where a build and the reference set differ. The two cases carry different fields because they +#: ask for different handling: one stops the run, the other is ordinary. +type Divergence = Mismatched | Absent + + +@dataclass(frozen=True) +class CvlrSources: + """The CVLR crates this build resolves, with the source trees they resolve to.""" + + crates: tuple[CratePackage, ...] + + @classmethod + def of(cls, workspace: Workspace) -> Self: + """Every CVLR crate in ``workspace``'s resolved graph, in name order. + + Cargo's order is not stable. This list is written into run metadata, where a shuffle looks + like a change. One version can resolve twice, from two sources or two paths, so the + manifest path, which is unique per package, breaks the tie. + """ + return cls( + tuple( + sorted( + workspace.family(CVLR_PREFIX), + key=lambda c: (c.name, c.version, c.manifest_path), + ) + ) + ) + + def roots(self) -> tuple[Path, ...]: + """The crate directories, one per family member.""" + return tuple(c.root for c in self.crates) + + def gaps(self, reference: ChainReference) -> tuple[Divergence, ...]: + """Where this build and the reference set disagree. + + Only crates the reference set names are compared. A dependency the reference does not + mention is not a disagreement. A capability with no published crate is recorded on the + reference itself, as :class:`~composer.spec.cvlr.reference.UnpublishedCapability`. + A crate the graph resolves more than once is one :class:`Mismatched` per copy off the + reference. + """ + gaps: list[Divergence] = [] + for r in reference.crates(): + versions = [c.version for c in self.crates if c.name == r.name] + if not versions: + gaps.append(Absent(crate=r.name, reference=r.version)) + gaps += [ + Mismatched(crate=r.name, reference=r.version, resolved=v) + for v in versions + if v != r.version + ] + return tuple(gaps) + + def mismatched(self, reference: ChainReference) -> tuple[Mismatched, ...]: + """Only the divergences that stop a run. See :class:`Absent` for why the rest do not.""" + return tuple(g for g in self.gaps(reference) if isinstance(g, Mismatched)) diff --git a/composer/spec/cvlr/env_paths.py b/composer/spec/cvlr/env_paths.py new file mode 100644 index 00000000..ab4b1776 --- /dev/null +++ b/composer/spec/cvlr/env_paths.py @@ -0,0 +1,148 @@ +"""Spell the starting tuning files the way a target's platform generation does. + +The starting tuning files (:mod:`composer.spec.cvlr.tuning`) are written with ``solana_program::`` +paths (``solana_program::account_info::AccountInfo``). From ``solana-program`` 2.2 on those are +re-exports. A demangled symbol carries the path of the crate that defines the item +(``solana_account_info::AccountInfo``), so a directive in the old spelling matches nothing. It +does not fail. It does not apply. + +:class:`~composer.spec.cvlr.reference.PathAlias` pairs a canonical spelling with this generation's +spellings. This module applies those pairs. + +One concept can have more than one spelling. ``solana-program`` kept its own +``invoke_signed_unchecked``, and the one on the call path is ``solana-cpi``'s, so one directive +becomes two. + +An alias is used only when the target resolves the crate it names. The aliases are declared for +the post-split generation. Dropping the ones whose crate is absent keeps them safe on a 1.18 +target, whose paths are already the canonical ones. +""" + +import logging +import re +from dataclasses import dataclass +from collections.abc import Iterable + +from composer.cargo.metadata import Workspace +from composer.spec.cvlr.reference import ChainReference, NamespacePattern, PathAlias + +_log = logging.getLogger(__name__) + +#: An inlining directive: the attribute and the pattern on one line. +_INLINE_LINE = re.compile(r"^(?P#\[inline(?:\(never\))?\]\s+)(?P\S.*?)\s*$") + +#: A points-to summary's type annotation. These *precede* the pattern they belong to, one per line, +#: so a summary whose pattern fans out has to carry its whole annotation block along with it. +_TYPE_LINE = re.compile(r"^#\[type\(.*\)\]\s*$") + + +def _crate_of(path: str) -> str: + return path.split("::", 1)[0].replace("_", "-") + + +@dataclass(frozen=True) +class PathDialect: + """How one target spells the paths in the starting tuning files. + + Built by :func:`dialect_for` from the aliases whose crates this target resolves. + """ + + aliases: tuple[PathAlias, ...] = () + + def spellings(self, pattern: str) -> tuple[str, ...]: + """``pattern`` in this dialect. Unchanged when it names nothing that moved. + + Longest canonical first, so a symbol alias wins over the module alias it sits inside. + ``solana_program::program::invoke_signed_unchecked`` must not be rewritten by an alias for + ``solana_program::program``. + """ + rendered = [pattern] + for alias in sorted(self.aliases, key=lambda a: -len(a.canonical)): + if not any(alias.canonical in p for p in rendered): + continue + rendered = _unique( + p.replace(alias.canonical, actual) for p in rendered for actual in alias.actual + ) + return tuple(rendered) + + def render(self, text: str) -> str: + """One tuning file with every directive spelled for this target. + + Comments, blank lines, and grouping are kept. A second spelling is inserted directly + under the first. + """ + out: list[str] = [] + annotations: list[str] = [] + for line in text.splitlines(): + stripped = line.strip() + if _TYPE_LINE.match(stripped): + annotations.append(line) + continue + inline = _INLINE_LINE.match(stripped) + if inline is not None: + spellings = self.spellings(inline["pattern"]) + # Unchanged lines are copied as they arrived, including trailing whitespace, so + # the composite reads line for line against the starting layer. + out += ( + [line] + if spellings == (inline["pattern"],) + else [f"{inline['lead']}{p}" for p in spellings] + ) + continue + if stripped and not stripped.startswith(";"): + spellings = self.spellings(stripped) + if spellings == (stripped,): + out += [*annotations, line] + annotations = [] + continue + for n, pattern in enumerate(spellings): + # The starting layers separate annotated summary blocks with a blank line. + # Without one, two summaries read as a single block. + if n and annotations: + out.append("") + out += [*annotations, pattern] + annotations = [] + continue + # A comment or a blank line ends the annotation block. Flush it as written + # instead of attaching it to a later pattern. + out += annotations + annotations = [] + out.append(line) + return "\n".join(out + annotations) + "\n" + + +def _unique(patterns: Iterable[str]) -> list[str]: + """``patterns`` with duplicates dropped, first occurrence kept. + + An alias can list its canonical spelling as one of its own replacements, for a symbol that + exists on both sides of a split. Without this that directive would be emitted twice. + + Order matters, which is why this is not a ``set``: the spellings are written into the tuning + file in this order, and the scaffold rewrites that file whenever its text changes. + """ + return list(dict.fromkeys(patterns)) + + +def dialect_for(workspace: Workspace, reference: ChainReference) -> PathDialect: + """The spelling ``workspace`` uses for the platform generation ``reference`` names. + + Aliases whose crate the target does not resolve are dropped. On an older generation this + returns a dialect that changes nothing. + """ + aliases: list[PathAlias] = [] + for alias in reference.platform.path_aliases: + match alias: + case PathAlias(canonical=canonical, actual=actual): + usable = tuple(a for a in actual if workspace.resolved(_crate_of(a))) + if usable: + aliases.append(PathAlias(canonical, usable)) + case NamespacePattern(canonical=canonical, actual=actual): + aliases.append(PathAlias(canonical, (actual,))) + dialect = PathDialect(tuple(aliases)) + _log.debug( + "tuning-path dialect for %s: %d of %d aliases usable", + reference.platform.label, + len(aliases), + len(reference.platform.path_aliases), + ) + return dialect diff --git a/composer/spec/cvlr/envs/cvlr_inlining_anchor.txt b/composer/spec/cvlr/envs/cvlr_inlining_anchor.txt new file mode 100644 index 00000000..2f6839e2 --- /dev/null +++ b/composer/spec/cvlr/envs/cvlr_inlining_anchor.txt @@ -0,0 +1,47 @@ +;; By default we don't inline anything from anchor. +#[inline(never)] ^.*anchor_lang.*$ + +;; except these functions + +#[inline] ^anchor_lang::accounts::account_loader::AccountLoader::load(_[0-9][0-9]*)*$ +#[inline] ^anchor_lang::accounts::account_loader::AccountLoader::load_mut(_[0-9][0-9]*)*$ + +#[inline] ^ as core::clone::Clone>::clone(_[0-9][0-9]*)*$ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; try_from and try_from_unchecked might call to deserialize so we need to check case by case +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#[inline] ^anchor_lang::accounts::account_loader::AccountLoader::try_from(_[0-9][0-9]*)*$ +#[inline] ^anchor_lang::accounts::account_loader::AccountLoader::try_from_unchecked(_[0-9][0-9]*)*$ +#[inline] ^anchor_lang::accounts::account::Account::try_from_unchecked(_[0-9][0-9]*)*$ +#[inline] ^anchor_lang::accounts::account::Account::try_from(_[0-9][0-9]*)*$ +#[inline] ^anchor_lang::accounts::signer::Signer::try_from$ +#[inline] ^ as core::convert::TryFrom<&solana_program::account_info::AccountInfo>>::try_from$ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +#[inline] ^>::as_ref$ +#[inline] ^::to_account_infos$ + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; These are needed to include the code for key() +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#[inline] ^::key$ +#[inline] ^::key$ +#[inline] ^.*::ZeroCopyAccessor>::get$ +#[inline] ^anchor_lang::accounts::account_info::::key$ + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; These do conversion between error codes +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +#[inline] ^>::from$ +#[inline] ^>::from$ +#[inline] ^>::from$ +#[inline] ^anchor_lang::error:: for u32>::from$ +;; Any program's own error enum, not one named project's: this layer is canonical and is copied +;; into every scaffold, so a concrete crate name here is a directive that matches nothing. +#[inline] ^.+ for anchor_lang::error::Error>::from$ +#[inline] ^>::from$ + +#[inline] ^<.+ as anchor_lang::AccountDeserialize>::try_deserialize$ +#[inline] ^<.+ as anchor_lang::AccountDeserialize>::try_deserialize_unchecked$ +#[inline] ^anchor_lang::accounts::interface_account::InterfaceAccount::try_from(_\d+)?$ + diff --git a/composer/spec/cvlr/envs/cvlr_inlining_core.txt b/composer/spec/cvlr/envs/cvlr_inlining_core.txt new file mode 100644 index 00000000..efb11c97 --- /dev/null +++ b/composer/spec/cvlr/envs/cvlr_inlining_core.txt @@ -0,0 +1,154 @@ +; By default we do not inline core, std, alloc, and solana_program +; with some exceptions below with #[inline] + +#[inline(never)] ^core::.*$ +#[inline(never)] ^std::.*$ +#[inline(never)] ^::get$ +#[inline] ^solana_program::poseidon::PoseidonHash::new$ +#[inline] ^solana_program::account_info::AccountInfo::assign$ +#[inline] ^solana_program::incinerator::check_id$ +#[inline] ^solana_program::system_program::check_id$ +#[inline] ^solana_program::system_program::id$ +#[inline] ^solana_program::rent::Rent::minimum_balance$ +#[inline] ^solana_program::sysvar::rent::::get$ +#[inline] ^solana_program::instruction::get_stack_height$ +#[inline] ^solana_program::program::set_return_data$ + +#[inline] ^>::from$ + +#[inline] ^core::cell::RefCell::borrow(_\d+)?$ +#[inline] ^core::cell::RefCell::borrow_mut(_\d+)?$ + + +;; Borsh and common functions used by Borsh +#[inline(never)] ^std::io::error::Error::new(_\d+)?$ +#[inline(never)] ^borsh::de::unexpected_eof_to_unexpected_length_of_input(_\d+)?$ + + +;; We need to inline this function to avoid unsoundness results in +;; NcnOperatorTicket::seeds and others. +#[inline] ^ as alloc::vec::spec_from_iter::SpecFromIter>::from_iter(_\d+)?$ + +#[inline] ^ as core::clone::Clone>::clone$ + diff --git a/composer/spec/cvlr/envs/cvlr_summaries_core.txt b/composer/spec/cvlr/envs/cvlr_summaries_core.txt new file mode 100644 index 00000000..5c86d557 --- /dev/null +++ b/composer/spec/cvlr/envs/cvlr_summaries_core.txt @@ -0,0 +1,108 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; POINTS-TO SUMMARIES +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; if the call returns then (*i64)(r1+0) is always a valid pointer. +;;; 1st call: +;;; - precondition: (*i64)(r1+0) is a Rust dangling pointer +;;; - post-condition: (*i64)(r1+0) points to new allocated memory (malloc) +;;; 2nd call: +;;; - precondition: (*i64)(r1+0) is a valid pointer +;;; - post-condition: (*i64)(r1+0) points to a new allocated memory after resizing the memory object +;;; to which r1 pointed to before the call (realloc). +#[type((*i64)(r1+0):ptr_heap)] +^alloc::raw_vec::RawVec::reserve_for_push(_[0-9][0-9]*)*$ +#[type((*i64)(r1+0):ptr_heap)] +^alloc::raw_vec::RawVec::reserve::do_reserve_and_handle(_[0-9][0-9]*)*$ + +#[type(r0:num)] +^__muldf3$ + +#[type(r0:num)] +^__divdf3$ + +#[type(r0:num)] +^__gedf2$ + +#[type(r0:num)] +^__gtdf2$ + +#[type(r0:num)] +^__floatundidf$ + +;; %"AccountInfo" = type { %"Pubkey"*, i64*, i64*, %"Pubkey"*, i64, i8, i8, i8, [5 x i8] } +#[type((*i64)(r1+0):ptr_external)] +#[type((*i64)(r1+8):ptr_external)] +#[type((*i64)(r1+16):ptr_external)] +#[type((*i64)(r1+24):ptr_external)] +#[type((*i64)(r1+32):num)] +#[type((*i8)(r1+40):num)] +#[type((*i8)(r1+41):num)] +#[type((*i8)(r1+42):num)] +^([^:]+::)*CVT_nondet_account_info$ + +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +^([^:]+::)*CVT_nondet_pubkey$ + +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +^([^:]+::)*CVT_nondet_layout_unchecked$ + +#[type(r0:ptr_external)] +^([^:]+::)*CVT_nondet_pointer_usize$ + +#[type((*i32)(r1+0):num)] +^solana_program::account_info::AccountInfo::realloc$ + +;; Result +#[type((*i8)(r1+0):num)] +#[type((*i64)(r1+1):num)] +#[type((*i64)(r1+9):num)] +#[type((*i64)(r1+17):num)] +#[type((*i64)(r1+25):num)] +^solana_program::pubkey::Pubkey::create_program_address$ + +;; Result +#[type((*i8)(r1+0):num)] +#[type((*i64)(r1+1):num)] +#[type((*i64)(r1+9):num)] +#[type((*i64)(r1+17):num)] +#[type((*i64)(r1+25):num)] +^solana_pubkey::Pubkey::create_program_address$ + +;; (Pubkey, u8) +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +#[type((*i8)(r1+32):num)] +^solana_program::pubkey::Pubkey::find_program_address$ + +;; (Pubkey, u8) +#[type((*i64)(r1+0):num)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +#[type((*i64)(r1+24):num)] +#[type((*i8)(r1+32):num)] +^solana_pubkey::Pubkey::find_program_address$ + +#[type((*i32)(r1+0):num)] +^solana_program::program::invoke_signed_unchecked$ + +;; To silent Solana prover warning about memhavoc_c +^memhavoc_c$ + +;; Return in r1 a String which is Vec +#[type((*i64)(r1+0):ptr_heap)] +#[type((*i64)(r1+8):num)] +#[type((*i64)(r1+16):num)] +^alloc::fmt::format::format_inner$ + +#[type(r0:ptr_heap)] +^std::io::error::Error::new(_\d+)?$ + diff --git a/composer/spec/cvlr/forks.py b/composer/spec/cvlr/forks.py new file mode 100644 index 00000000..003120cd --- /dev/null +++ b/composer/spec/cvlr/forks.py @@ -0,0 +1,376 @@ +"""Build a Solana project against Certora's forks of Anchor and ``fixed``, not the crates.io ones. + +Anchor is the framework most Solana programs are written in. A program uses it through the +``anchor-lang`` crate, and usually ``anchor-spl`` for token accounts, both from crates.io. The +Solana Prover cannot analyze those crates as published. Anchor's error type, +``anchor_lang::error::Error``, moves a struct built on the stack into a heap allocation +(``Box::new``), and the Prover rejects that as [3006], "illegal store of a stack pointer". +Anchor's generated entry point runs that code, and so does any handler that returns an error with +``?``. Against upstream Anchor, in practice, no instruction of the program can be verified. + +``Certora/anchor`` is a copy of the Anchor repository with that fixed. For each Anchor release it +supports, it has one branch, ``certora-v``, holding that release plus Certora's changes: +an ``Error`` that does not box, a simpler ``require!``, an ``emit!`` that does nothing, and public +constructors a harness needs, such as ``new_unchecked`` for ``anchor-spl``'s ``TokenAccount`` and +``Mint``, whose fields upstream keeps private. Otherwise the branch has the same API as the +release, so the program compiles unchanged against the branch for the Anchor version it already +uses. This module reads that version from the resolved dependency graph and adds a +``[patch.crates-io]`` entry to the workspace manifest pointing cargo at the matching branch. + +``Certora/fixed`` is organized the same way, for the ``fixed`` fixed-point crate, for a different +reason: it adds conversions a harness needs to construct values, such as ``From`` for +``FixedU64``, which upstream does not provide. + +The supported versions are listed explicitly (:data:`ANCHOR_FORK`, :data:`FIXED_FORK`) rather than +derived from the version number. A version with no branch blocks the plan with a message saying +which versions are covered. A derived name would send cargo after a branch that does not exist, +and the failure would be a git fetch error that says nothing about coverage. + +A project set up by hand usually stays on the crates.io crates, and hits [3006] with nothing in +the error pointing at the fork. +""" + +import logging +from collections.abc import Mapping +from dataclasses import dataclass + +from composer.cargo.manifest import AddTable, Comment, Manifest, TableItem +from composer.cargo.metadata import ( + CratePackage, + GitSource, + OtherSource, + RegistrySource, + Workspace, +) + +_log = logging.getLogger(__name__) + + +@dataclass(frozen=True) +class ForkOverride: + """A repository of verification-oriented forks, and the crates in it a target may need. + + ``crates`` is more than one name because a fork is a workspace: ``Certora/anchor`` publishes + ``anchor-lang`` and ``anchor-spl`` from one branch. A target has every one of them it uses + redirected, or the ones left out stay upstream. + + ``branches`` maps an exact resolved version to a branch name, listed rather than derived; see + the module docstring. + """ + + repo: str + crates: tuple[str, ...] + branches: Mapping[str, str] + why: str + + def branch_for(self, version: str) -> str | None: + return self.branches.get(version) + + def covered(self) -> str: + return ", ".join(self.branches) + + +@dataclass(frozen=True) +class Blocked: + """Why an override cannot be applied, and what would resolve it.""" + + crate: str + problem: str + resolution: str + + +@dataclass(frozen=True) +class AlreadySourced: + """The target already decides where this crate comes from, so nothing was changed. + + The source is part of the report. A project already on this fork needs nothing. A project on + some other fork is left alone, and if a handler then will not analyze, this is the first place + to look. + """ + + crate: str + #: ``None`` for a path in this workspace. + source: GitSource | OtherSource | None + #: The repository the override would have used. ``points_at_fork`` is derived from this + #: and ``source``. + fork_repo: str + + @property + def points_at_fork(self) -> bool: + return isinstance(self.source, GitSource) and self.source.is_from(self.fork_repo) + + @property + def origin(self) -> str: + return self.source.spelling if self.source is not None else "a path in this workspace" + + def describe(self) -> str: + if self.points_at_fork: + return f"{self.crate} already comes from {self.fork_repo}; nothing to do" + return ( + f"{self.crate} already comes from {self.origin} rather than {self.fork_repo}, so it " + f"was left alone — a source in the manifest is somebody's decision. If a handler will " + f"not analyze, this is the first thing to check." + ) + + +@dataclass(frozen=True) +class AlreadyRedirected: + """This workspace's ``[patch.crates-io]`` table already names the crate. + + Separate from :class:`AlreadySourced` because the table entry has not been resolved to a + source URL. The next graph read is what says whether it points at the fork. + """ + + crate: str + + def describe(self) -> str: + return ( + f"{self.crate} is already redirected in this workspace's [patch.crates-io] table" + ) + + +#: What the planner reports when a crate is already in the manifest's patch table but not yet in the +#: resolved graph — the graph is a snapshot, and it can predate the table. +type LeftAlone = AlreadySourced | AlreadyRedirected + + +@dataclass(frozen=True) +class Override: + """One dependency's replacement, resolved against a particular target.""" + + crate: str + version: str + repo: str + branch: str + why: str + + def redirect(self) -> tuple[TableItem, ...]: + """The ``[patch.crates-io.]`` body that points the graph at the fork. + + A branch, not a commit. The lockfile records the commit, so the build stays reproducible + without editing the manifest every time the fork moves. + """ + return (("git", self.repo), ("branch", self.branch)) + + +@dataclass(frozen=True) +class ForkPlan: + """What redirecting this target at the forks would change. Empty when nothing needs it.""" + + overrides: tuple[Override, ...] = () + #: Crates the target does not resolve. Kept in the plan: "Anchor was not replaced" is what a + #: reader of a [3006] failure needs, and omitting it looks like success. + inapplicable: tuple[str, ...] = () + #: Crates left alone because the target already decides where they come from. See + #: :data:`LeftAlone`. + already: tuple[LeftAlone, ...] = () + + def __bool__(self) -> bool: + return bool(self.overrides) + + def notes(self) -> list[str]: + """What the plan left unchanged, for the scaffold's review output.""" + return [f"{crate} is not a dependency of this project" for crate in self.inapplicable] + [ + a.describe() for a in self.already + ] + + +@dataclass(frozen=True) +class ForkRefused: + """Why this target cannot be redirected at the forks: every reason, not the first. + + Nothing is redirected. Replacing one crate while another stays upstream leaves a build whose + failure has two causes. + """ + + blocked: tuple[Blocked, ...] + + +# --------------------------------------------------------------------------------------------- +# the overrides + + +#: Anchor. Branch names taken from the fork. Listed, not derived, so a release the fork has not +#: been updated for is reported as uncovered. The fork has 0.30.1 and not 0.30.0, and nothing +#: after 0.32.1. +ANCHOR_FORK = ForkOverride( + repo="https://github.com/Certora/anchor.git", + crates=("anchor-lang", "anchor-spl"), + branches={ + "0.26.0": "certora-v0.26.0", + "0.27.0": "certora-v0.27.0", + "0.28.0": "certora-v0.28.0", + "0.29.0": "certora-v0.29.0", + "0.30.1": "certora-v0.30.1", + "0.31.1": "certora-v0.31.1", + "0.32.0": "certora-v0.32.0", + "0.32.1": "certora-v0.32.1", + }, + why=( + "Use the Certora fork of Anchor. It avoids the boxing the official library does, which is " + "hard to analyze." + ), +) + +#: The fixed-point crate. The fork adds conversions verification code needs and upstream does not +#: provide. One branch is listed, ``certora-v1.23.1`` for 1.23.1, because that is the release the +#: fork is known to cover. Any other version blocks instead of inventing a branch name. +FIXED_FORK = ForkOverride( + repo="https://github.com/Certora/fixed.git", + crates=("fixed",), + branches={"1.23.1": "certora-v1.23.1"}, + why=( + "Use the Certora fork of fixed. It adds conversions the official library lacks, such as " + "From for FixedU64, which verification code needs to build fixed-point values." + ), +) + + +# --------------------------------------------------------------------------------------------- +# planning + + +def already_patched(manifest: Manifest) -> frozenset[str]: + """The crates a workspace manifest's ``[patch.crates-io]`` table already redirects. + + Parsed, not searched. Projects write one ``[patch.crates-io]`` header with an inline table + per crate. This module writes a ``[patch.crates-io.]`` sub-table. The two are the same + TOML and share no text, so a search for either misses the other. A second entry for a key + TOML already has is a manifest cargo refuses. + + :func:`plan_overrides` also checks the resolved graph, which is what cargo computed. This covers + the case the graph cannot: a snapshot taken before the patch table was applied. + """ + return frozenset(manifest.patch.get("crates-io", {})) + + +def _copies(copies: tuple[CratePackage, ...]) -> str: + return ", ".join( + f"{c.version} from {c.source.spelling if c.source is not None else 'this workspace'}" + for c in copies + ) + + +def plan_overrides( + workspace: Workspace, + overrides: tuple[ForkOverride, ...], + already_redirected: frozenset[str] = frozenset(), +) -> ForkPlan | ForkRefused: + """What redirecting ``workspace`` at the forks would change, without changing anything. + + Each crate lands in one of four outcomes: + + * inapplicable — not in the resolved graph. + * already sourced — a workspace member, a path dependency, a git dependency, or a crate named + in ``already_redirected``. Overriding it would replace a choice, which may already be this + fork. The graph is what cargo computed. ``already_redirected`` + (:func:`already_patched`) covers a snapshot taken before the patch table was applied. + * blocked — resolved more than once, since one patch entry redirects one of the copies; or + resolved at a version the fork has no branch for, since skipping the fork leaves the + failure it exists to fix. + * overridden — redirected at the fork. + + Any blocked crate makes the whole result a :class:`ForkRefused`. + """ + resolved_overrides: list[Override] = [] + blocked: list[Blocked] = [] + inapplicable: list[str] = [] + already: list[LeftAlone] = [] + + for fork in overrides: + for crate in fork.crates: + copies = workspace.resolved(crate) + if not copies: + inapplicable.append(crate) + continue + if crate in already_redirected: + already.append(AlreadyRedirected(crate=crate)) + continue + resolved, *others = copies + if others: + blocked.append( + Blocked( + crate=crate, + problem=( + f"this project resolves {crate} more than once " + f"({_copies(copies)}), and {fork.repo} can replace only one of them" + ), + resolution=f"move the project onto one {crate} release", + ) + ) + continue + if not isinstance(resolved.source, RegistrySource): + left = AlreadySourced(crate=crate, source=resolved.source, fork_repo=fork.repo) + already.append(left) + _log.info("%s already comes from %s; leaving it alone", crate, left.origin) + continue + branch = fork.branch_for(resolved.version) + if branch is None: + blocked.append( + Blocked( + crate=crate, + problem=( + f"this project resolves {crate} {resolved.version}, which " + f"{fork.repo} has no branch for" + ), + resolution=( + f"move the project to a {crate} release the fork covers: " + f"{fork.covered()}" + ), + ) + ) + continue + resolved_overrides.append( + Override( + crate=crate, + version=resolved.version, + repo=fork.repo, + branch=branch, + why=fork.why, + ) + ) + + if blocked: + return ForkRefused(tuple(blocked)) + return ForkPlan(tuple(resolved_overrides), tuple(inapplicable), tuple(already)) + + +_NOT_DEPLOYED = ( + "Verification-only dependency replacements. These are NOT the deployed program's " + "dependencies: a property proved against a fork is a property of the fork, and whether it " + "carries over is a judgement about the specific difference." +) + + +def patch_tables(plan: ForkPlan) -> tuple[tuple[Override, AddTable], ...]: + """The ``[patch.crates-io.]`` table this plan adds to the workspace manifest for each + override. + + Each fork's reason is written once, in the table of its + first crate: crates from one fork share one reason, and repeating it under each reads like + two unrelated edits. The first table also says what these replacements are. + """ + tables: list[tuple[Override, AddTable]] = [] + preamble = [Comment(line) for line in _wrapped(_NOT_DEPLOYED)] + [Comment("")] + for why in dict.fromkeys(o.why for o in plan.overrides): + first, *rest = [o for o in plan.overrides if o.why == why] + explanation = [Comment(f"{o.crate} {o.version} -> {o.branch}") for o in (first, *rest)] + explanation += [Comment(f" {line}") for line in _wrapped(why)] + body = (*preamble, *explanation, *first.redirect()) + tables.append((first, AddTable(("patch", "crates-io", first.crate), body))) + preamble = [] + tables += [(o, AddTable(("patch", "crates-io", o.crate), o.redirect())) for o in rest] + return tuple(tables) + + +def _wrapped(text: str, width: int = 88) -> list[str]: + words, lines, current = text.split(), [], "" + for word in words: + if current and len(current) + 1 + len(word) > width: + lines.append(current) + current = word + else: + current = f"{current} {word}".strip() + if current: + lines.append(current) + return lines diff --git a/composer/spec/cvlr/harness_files/mod.template.rs b/composer/spec/cvlr/harness_files/mod.template.rs new file mode 100644 index 00000000..65de7115 --- /dev/null +++ b/composer/spec/cvlr/harness_files/mod.template.rs @@ -0,0 +1,5 @@ +//! Certora verification harness. +//! +//! Compiled only under the `certora` feature, which `lib.rs` gates this module on. + +pub mod specs; diff --git a/composer/spec/cvlr/harness_files/specs/mod.template.rs b/composer/spec/cvlr/harness_files/specs/mod.template.rs new file mode 100644 index 00000000..7361c499 --- /dev/null +++ b/composer/spec/cvlr/harness_files/specs/mod.template.rs @@ -0,0 +1 @@ +//! The rules. One module per property group; declare each one here. diff --git a/composer/spec/cvlr/preflight.py b/composer/spec/cvlr/preflight.py new file mode 100644 index 00000000..5ad8c296 --- /dev/null +++ b/composer/spec/cvlr/preflight.py @@ -0,0 +1,245 @@ +"""Scaffold a CVLR project, then check that the scaffold compiles. + +:meth:`composer.pipeline.core.PipelineBackend.preflight` runs in the same task group as system +analysis (``docs/formalization-abstraction.md`` §2), so a failure here cancels the analysis. A +project that cannot compile with the harness in is not handed on. + +:func:`prepare_workspace` writes files. :func:`gate_workspace` compiles. The compile sits on the +run's CPU budget (``PipelineRun.cpu_runner``), the same split as +:mod:`composer.rustapp.adapter`. One function that did both could not be placed on either side +of that line. + +Three outcomes are refusals, all :class:`~composer.spec.cvlr.scaffold.Blocked`: a package that +builds no loadable object, a project on a CVLR release other than the one this build is pinned to, +and a CVLR pin that does not match the platform generation the project is already on. +""" + +import logging +from dataclasses import dataclass +from pathlib import Path + +from composer.cargo.features import CargoFeature +from composer.cargo.metadata import CargoUnavailable, CratePackage, Workspace +from composer.cargo.session import CargoSession, CompileFailed, Compiled, WarmFailed +from composer.sandbox.config import SandboxConfig +from composer.spec.cvlr.conf import DEFAULT_FEATURE +from composer.spec.cvlr.crates import CvlrSources, Divergence +from composer.spec.cvlr.scaffold import ( + ScaffoldBlocked, + ScaffoldPlan, + apply, + plan_scaffold, +) +from composer.spec.cvlr.reference import ChainReference + +_log = logging.getLogger(__name__) + + +class PreflightFailed(RuntimeError): + """The project cannot be prepared for verification, so the run stops. + + Separate from :class:`composer.rustapp.adapter.PreflightFailed`, which says the same thing + for the Rust wheel. The message is what a reader sees, and it names this backend. + """ + + +@dataclass(frozen=True) +class CvlrPreflight: + """What preflight learned. The pipeline carries this to ``prepare_system`` as ``Pre``. + + The scaffold plan is kept with the outcome. It records what was written, including a run + that wrote nothing because the project was already set up. + """ + + workspace_root: Path + package: str + #: The package directory relative to the workspace root. The harness module is written here, + #: and the build names this crate. Taken from the workspace the scaffold already used. + package_dir: Path + #: The library target's file stem. The built ``.so`` is named after it. + artifact_stem: str + scaffold: ScaffoldPlan + #: The files this run wrote, relative to :attr:`workspace_root`, in the order they were + #: written. Empty when the project was already set up. + applied: tuple[Path, ...] + #: The CVLR crates the scaffolded graph resolves. Read after applying. Before that the + #: project may not depend on CVLR at all. + sources: CvlrSources + #: Where the resolved crates and the reference set disagree. Only + #: :class:`~composer.spec.cvlr.crates.Absent` can appear here: the scaffold refuses a project + #: on another CVLR line before anything is written, and :func:`prepare_workspace` checks again + #: afterwards. Kept so a run can say which reference-set crates this project does not have. + gaps: tuple[Divergence, ...] + + def describe(self) -> str: + lines = [self.scaffold.describe()] + versions = ", ".join(f"{c.name} {c.version}" for c in self.sources.crates) + lines.append(f"CVLR resolved: {versions or 'nothing'}") + lines += [f" gap: {g.describe()}" for g in self.gaps] + return "\n".join(lines) + + +def _pick_package(workspace: Workspace, requested: str | None) -> CratePackage: + """The package to verify. + + An explicit name is required when more than one member has a library target. Which program + is under verification is not something the repository layout decides.""" + if requested is not None: + member = workspace.member(requested) + if member is None: + raise PreflightFailed( + f"{requested!r} is not a member of the workspace at {workspace.root} " + f"(members: {', '.join(m.name for m in workspace.members)})" + ) + return member + verifiable = [m for m in workspace.members if m.lib is not None] + if len(verifiable) == 1: + return verifiable[0] + raise PreflightFailed( + f"the workspace at {workspace.root} has {len(verifiable)} packages with a library target " + f"({', '.join(m.name for m in verifiable)}); name the one to verify" + ) + + +@dataclass(frozen=True) +class SelectedPackage: + """Which package will be verified, resolved before any files are written. + + :func:`prepare_workspace` reaches the same package and then scaffolds. This only reads the + workspace, so a workspace that needs a package named fails before anything is written. + """ + + workspace_root: Path + name: str + #: The package directory relative to the workspace root, the same relation as + #: :attr:`CvlrPreflight.package_dir`. Both come from one workspace read. + package_dir: Path + + +async def select_package( + project_root: Path, package: str | None = None, *, main_source: Path | None = None +) -> SelectedPackage: + """Resolve ``package`` against the workspace at ``project_root``. + + An explicit name wins. Otherwise the member that owns the main program's source file wins, + which is cargo's own view of which member a path belongs to. A workspace with several + library crates, which :func:`_pick_package` refuses on its own, needs no second flag. + When neither a name nor a source file is available, the single-library rule applies, + including its refusal. + """ + workspace = await _workspace_at(project_root) + owner = workspace.owning(main_source) if main_source is not None else None + member = ( + owner + if package is None and owner is not None and owner.lib is not None + else _pick_package(workspace, package) + ) + return SelectedPackage( + workspace_root=workspace.root, + name=member.name, + package_dir=member.root.resolve().relative_to(workspace.root.resolve()), + ) + + +async def _workspace_at(root: Path, *, features: tuple[CargoFeature, ...] = ()) -> Workspace: + try: + workspace = await Workspace.read(root, features=features) + except CargoUnavailable as exc: + raise PreflightFailed(str(exc)) from exc + if not isinstance(workspace, Workspace): + raise PreflightFailed( + f"Could not read the Cargo project at {root}:\n{workspace.describe()}" + ) + return workspace + + +async def prepare_workspace( + project_root: Path, *, reference: ChainReference, package: str | None = None +) -> CvlrPreflight: + """Scaffold ``project_root`` and report what a run needs to know about it. + + Writes into the project it is given. For a pipeline run that is the copy the run owns. The + harness files under ``src/certora/`` are replaced by AutoProver's. The project's manifests + and sources are only added to. + + ``reference`` is the set rather than a chain name because every function this calls takes the + set. + """ + workspace = await _workspace_at(project_root) + member = _pick_package(workspace, package) + + plan = plan_scaffold(workspace, member, reference) + _log.info("%s", plan.describe()) + try: + applied = apply(plan, workspace.root) + except ScaffoldBlocked as exc: + raise PreflightFailed(str(exc)) from exc + + # Re-read with the verification feature, from the package directory. The scaffold adds CVLR + # to the manifests, so the graph from before that does not contain those crates. They are + # optional, so a default-feature read still reports them absent + # (:meth:`composer.cargo.metadata.Workspace.read`). Features resolve against the package + # cargo considers current. + resolved_in = await _workspace_at(member.root, features=(DEFAULT_FEATURE,)) + fresh = resolved_in.member(member.name) or member + if fresh.lib is None: + raise PreflightFailed(f"{fresh.name} has no library target to build") + + sources = CvlrSources.of(resolved_in) + # The backstop behind the scaffold's gate. That gate reads the manifests and the pre-scaffold + # graph; this reads what cargo actually resolved with the harness in. A mismatch here is a + # release that arrived some way the gate cannot see — a ``[patch]`` table is the way that + # happens — and it has to stop the run rather than be logged, because the harness this + # scaffold just wrote is the supported line's and will not compile against another. + if mismatched := sources.mismatched(reference): + raise PreflightFailed( + "the scaffolded project does not build the CVLR releases this build supports:\n" + + "\n".join(f" {m.describe()}" for m in mismatched) + + "\nCheck the workspace for a [patch] table redirecting a CVLR crate." + ) + return CvlrPreflight( + workspace_root=resolved_in.root, + package=fresh.name, + package_dir=fresh.root.resolve().relative_to(resolved_in.root.resolve()), + artifact_stem=fresh.lib.artifact_stem, + scaffold=plan, + applied=applied, + sources=sources, + gaps=sources.gaps(reference), + ) + + +async def gate_workspace( + pre: CvlrPreflight, + *, + sandbox: SandboxConfig, + features: tuple[CargoFeature, ...] = (DEFAULT_FEATURE,), +) -> None: + """Check that the scaffolded project compiles with the harness in, or fail the run. + + Host-target ``cargo check`` only. What this has to catch is a scaffold that does not compile. + The SBF build is a later gate, and running it here would cost more than the failure it would + be catching. + """ + session = CargoSession(workdir=pre.workspace_root, sandbox=sandbox) + warmed = await session.warm() + if isinstance(warmed, WarmFailed): + raise PreflightFailed( + f"could not fetch the dependency graph for {pre.workspace_root} " + f"(exit {warmed.exit_code}):\n{warmed.diagnostics}" + ) + run = await session.check(package=pre.package, features=features) + _log.info( + "preflight gate: %s in %dms%s", + "ok" if run.ok else "FAILED", + run.duration_ms, + "" if run.confined else " (UNCONFINED)", + ) + match run.verdict: + case Compiled(): + return + case CompileFailed(diagnostics=diagnostics): + raise PreflightFailed( + f"the scaffolded {pre.package} does not compile with --features " + f"{','.join(features)}:\n{diagnostics}" + ) diff --git a/composer/spec/cvlr/reference.py b/composer/spec/cvlr/reference.py new file mode 100644 index 00000000..1542e440 --- /dev/null +++ b/composer/spec/cvlr/reference.py @@ -0,0 +1,306 @@ +"""Which published CVLR releases count as current, for each chain. + +CVLR is published as several crates, in layers. The core crate, ``cvlr``, is the part that does +not depend on any chain: the specification language, plus the parametric-rule macros it gets from +``cvlr-spec``. A chain crate (``cvlr-solana``, ``cvlr-soroban``) binds the core to one chain and +supplies the helpers that work with that chain's platform types. Specializations are narrower +crates that go with one chain crate. Most of them model a single on-chain program rather than the +whole chain: ``cvlr-spl-token`` models SPL token accounts and ``cvlr-solana-stake`` models the +stake program. Soroban's derive-macro crate is counted here as well. A project declares the core, +its chain's crate, and that chain's specializations. A platform generation is the release line of +the chain's own SDK that a chain crate is built against, such as ``solana-program`` 2.x or +``soroban-sdk`` 22.x. + +Exact versions, not ranges. The core and the chain crates are versioned separately, so "latest" +can pair a new core with an old chain crate. A bump is an edit here, and it moves every project +this build sets up: what is named here is the one CVLR line supported at a time, the way a Prover +release ships one CVL. That is why :mod:`composer.spec.cvlr.scaffold` refuses a project already on +a different line rather than deferring to it. + +A chain crate is bound to one platform generation, and each generation has its own ``AccountInfo``. +``cvlr-solana`` 0.4.x goes with ``solana-program`` 1.18, 0.5.0 with 2.2, and the unreleased 0.6 +line with the ``solana-*`` v3 crates. A helper from one generation cannot be passed an account +from another, so :attr:`ChainReference.platform` is part of the reference, not a detail of one +target. + +``solana-program`` stopped defining the platform types at 2.2, not at 3.0. 1.17 and 1.18 have a +real ``account_info`` module. 2.2.1, 2.3.0, and 3.0.0 re-export ``solana-account-info``. A path +written ``solana_program::account_info::AccountInfo`` then names a re-export. The path a demangled +symbol carries is ``solana_account_info::AccountInfo``. :class:`PathAlias` is that difference, for +the tuning files. +""" + +from dataclasses import dataclass + +from composer.spec.cvlr.forks import ANCHOR_FORK, FIXED_FORK, ForkOverride + + +@dataclass(frozen=True) +class CrateRelease: + """One crate at one published version.""" + + name: str + version: str + + def dependency_line(self) -> str: + """A ``Cargo.toml`` dependency line. Exact (``=version``), not a caret range. + + The reference set says what was compiled, not which later releases are compatible. + """ + return f'{self.name} = "={self.version}"' + + +@dataclass(frozen=True) +class CrateRequirement: + """A crate at a version line, which is how a platform generation is named. + + A CVLR release is the exact crate that was compiled. The platform is a generation, and the + patch level belongs to the target. An exact pin here would claim a patch that was never compiled. + """ + + name: str + line: str + + def dependency_line(self) -> str: + return f'{self.name} = "{self.line}"' + + +@dataclass(frozen=True) +class PathAlias: + """A path prefix as the canonical tuning files spell it, and this generation's spellings of it. + + Matched as a literal substring of a directive's pattern, so a concept is renamed wherever it + appears — several starting directives name two or three of them in one regex. + + ``actual`` is a tuple because a split is not always a rename. ``solana-program`` kept its own + ``invoke_signed_unchecked``, and the one on the call path is ``solana-cpi``'s, so a summary of + the concept is emitted under both spellings. A spelling whose crate the target does not + resolve is dropped, which is what makes these safe on a target that predates the split. + """ + + canonical: str + actual: tuple[str, ...] + + +@dataclass(frozen=True) +class NamespacePattern: + """A blanket over one crate's whole namespace, widened to the family that replaced that crate. + + The canonical spelling is ``::.*``, the pattern the starting layers use for a whole + layer, as in ``#[inline(never)] ^solana_program::.*$``. After the monolith split, that layer + lives in ``solana_account_info``, ``solana_pubkey``, ``solana_cpi``, and others, so the blanket + matches almost nothing and the default stops applying. + + This is not a :class:`PathAlias`, for two reasons. + + It must not rewrite a path that merely starts with the crate. + ``solana_program::instruction::get_stack_height`` is still a function in the monolith, and + rewriting it would name a symbol that does not exist. The literal ``.*`` is what marks a + blanket. + + It is also unconditional. A :class:`PathAlias` is dropped unless the target resolves the crate + it names. This replacement matches crate names, so it covers the canonical spelling and stays + correct on a target that predates the split, and it does not go stale when another crate is + split out. + """ + + canonical: str + actual: str + + +@dataclass(frozen=True) +class PlatformGeneration: + """The chain-platform release line a CVLR chain crate is bound to. + + The CVLR crates the reference set pins work only with this generation. :attr:`witnesses` is + how a target is checked to be on it, :attr:`path_aliases` is how it spells the paths in the + tuning files, and :attr:`sdk_crates` is what a crate built against it declares. + + ``label`` is for people: the platform refusal names it, and so does the tuning-path log line. + ``sdk_crates`` are the chain platform's own crates (``solana-program``, ``soroban-sdk``). + """ + + label: str + sdk_crates: tuple[CrateRequirement, ...] + #: The platform crates that define the types the chain crate's API uses, such as Solana's + #: ``AccountInfo``. When those types have moved between crates across generations, every + #: crate they have lived in is listed, most recent first. + #: + #: These are read from a target's resolved graph, never declared. The scaffold's platform gate + #: takes the first one the target resolves and compares its version against this generation. + witnesses: tuple[CrateRequirement, ...] + #: How this generation spells the paths in the starting tuning files. + #: :mod:`composer.spec.cvlr.env_paths` applies these. Empty when this generation's spelling + #: is already the one the starting layers use, which is the monolith's. + path_aliases: tuple[PathAlias | NamespacePattern, ...] = () + + +@dataclass(frozen=True) +class UnpublishedCapability: + """Something current practice uses that no published crate provides. + + Recorded here rather than left out, so a reader who meets the capability in a project can see + that it is outside what this build can pin: nothing publishes it, so there is no release to + name. Deliberately not a :class:`~composer.spec.cvlr.crates.Mismatched` — that is a + disagreement about *which* release, and this is the absence of one to disagree about. + """ + + #: Every name the capability has gone by. A rename is the case where searching for one + #: name and finding nothing looks like absence. + names: tuple[str, ...] + #: What a project reaching for it therefore finds nothing for. + missing: str + + +@dataclass(frozen=True) +class ChainReference: + """What current CVLR means for one chain.""" + + core: CrateRelease + #: The cvlr chain crate every project on this chain declares. + chain_crate: CrateRelease + platform: PlatformGeneration + #: Certora's forks of crates this chain's programs depend on, which a target is redirected at + #: when it resolves them (:mod:`composer.spec.cvlr.forks`). Empty for a chain with none. + forks: tuple[ForkOverride, ...] + #: Chain crates that model one on-chain program rather than the chain itself: the SPL token + #: account model, the stake program's state. Narrower than :attr:`chain_crate`, and still + #: declared. :meth:`scaffold_crates` includes them. + #: + #: They are optional crates behind the ``certora`` feature, so a project that never calls them + #: pays one extra compile. They are still pinned here. The scaffold is what writes + #: dependencies, and it does not add one later. A dependency changes how the project builds + #: for everyone, which the scaffold does not guess at. A specialization left out of this list + #: is a crate the project cannot name. + specializations: tuple[CrateRelease, ...] = () + unpublished: tuple[UnpublishedCapability, ...] = () + + def line(self) -> str: + """The supported line as a refusal names it to a project author: core and chain crate.""" + return ( + f"{self.core.name} {self.core.version} with " + f"{self.chain_crate.name} {self.chain_crate.version}" + ) + + def crates(self) -> tuple[CrateRelease, ...]: + """Every CVLR crate in the reference set: the line this build supports.""" + return (self.core, self.chain_crate, *self.specializations) + + def scaffold_crates(self) -> tuple[CrateRelease, ...]: + """What a fresh project declares in its ``Cargo.toml``. + + The same crates as :meth:`crates` today. Two names because they answer two questions, and + the questions are asked in different places: :func:`composer.spec.cvlr.scaffold._check_pins` + gates on which releases this build supports, and the manifest planning writes which of them + a project is given. + """ + return self.crates() + + def cargo_dependencies(self) -> str: + """A ``[dependencies]`` body pinning this reference set, for a probe crate. + + The platform crates are included because the chain crate's public types come from them. + Without them a probe cannot name what the helpers return.""" + lines = [c.dependency_line() for c in self.crates()] + lines += [c.dependency_line() for c in self.platform.sdk_crates] + return "\n".join(lines) + + +#: The core line, shared by every chain. ``cvlr-spec`` (``cvlr_spec!``, ``cvlr_rules!``, +#: ``cvlr_lemma!``) is a dependency of ``cvlr``, so a target names one crate and gets the +#: parametric-rule layer with it. +_CORE = CrateRelease("cvlr", "0.6.1") + +SOLANA = ChainReference( + core=_CORE, + chain_crate=CrateRelease("cvlr-solana", "0.5.0"), + specializations=( + CrateRelease("cvlr-solana-stake", "0.5.0"), + # The SPL token account model: nondet token accounts and mints, and the token instruction + # summaries. On crates.io at 0.5.0, the same version as the chain crate it was split from. + CrateRelease("cvlr-spl-token", "0.5.0"), + ), + forks=(ANCHOR_FORK, FIXED_FORK), + platform=PlatformGeneration( + # The last line published as one ``solana-program`` crate. v3 is only the split crates. + label="solana-program 2.x", + sdk_crates=(CrateRequirement("solana-program", "2.2"),), + # ``solana-account-info`` first: it defines ``AccountInfo`` and exists on both 2.x and 3.x. + # ``solana-program`` is the fallback for 1.18, which predates the split and defines the + # type inside the monolith. + witnesses=( + CrateRequirement("solana-account-info", "2.3"), + CrateRequirement("solana-program", "2.2"), + ), + # Checked against a demangled symbol table. ``solana-program`` is a partial facade, so + # which side of the split a symbol lives on is per symbol, not per module. + path_aliases=( + # Modules that became whole-crate aliases (`pub use solana_x as x`), so every path + # under them moved together. + PathAlias("solana_program::account_info", ("solana_account_info",)), + PathAlias("solana_program::pubkey", ("solana_pubkey",)), + PathAlias("solana_program::program_error", ("solana_program_error",)), + PathAlias("solana_program::program_pack", ("solana_program_pack",)), + PathAlias("solana_program::rent", ("solana_rent",)), + PathAlias("solana_program::clock", ("solana_clock",)), + PathAlias("solana_program::sysvar", ("solana_sysvar",)), + PathAlias("solana_program::hash", ("solana_hash",)), + # These two went to one crate that is not named after either of them. + PathAlias("solana_program::system_program", ("solana_sdk_ids::system_program",)), + PathAlias("solana_program::incinerator", ("solana_sdk_ids::incinerator",)), + # `program` is the partial facade. `invoke`, `invoke_signed`, and `set_return_data` + # are real functions there and stay under the canonical spelling. Only the symbol + # that moved is aliased, and it is aliased to both: `solana-program` still defines + # one of that name, and the one on the call path is `solana-cpi`'s. + PathAlias( + "solana_program::program::invoke_signed_unchecked", + ( + "solana_program::program::invoke_signed_unchecked", + "solana_cpi::invoke_signed_unchecked", + ), + ), + # Not aliased: `solana_program::instruction::get_stack_height` is still a function in + # the monolith on this generation, and `solana_program::poseidon` does not exist here + # under any spelling. Rewriting either would hide a directive that does not apply. + # + # The blanket that sets the platform layer's never-inline default. ``solana_program::.*`` + # only matches what stayed in the monolith. The replacement covers the split crates too. + NamespacePattern("solana_program::.*", "solana_[a-z0-9_]*::.*"), + ), + ), +) + +SOROBAN = ChainReference( + core=_CORE, + chain_crate=CrateRelease("cvlr-soroban", "0.4.0"), + # The derive crate is a companion of the chain crate. A target uses it when it writes the + # attribute macros. It is declared the same way as a specialization. + specializations=(CrateRelease("cvlr-soroban-derive", "0.4.0"),), + forks=(), + platform=PlatformGeneration( + label="soroban-sdk 22.x", + sdk_crates=(CrateRequirement("soroban-sdk", "22"),), + # Soroban has one SDK crate, so the declared crate and the witness are the same. Spelled + # out because that is a fact about this platform. On Solana the witness list names a crate + # this generation does not declare. + witnesses=(CrateRequirement("soroban-sdk", "22"),), + ), +) + +#: Keyed by ``composer.pipeline.ecosystem.ChainTag``, minus ``evm``. CVLR is the Rust-side +#: specification language and has no EVM line. +REFERENCE_SET: dict[str, ChainReference] = {"solana": SOLANA, "soroban": SOROBAN} + + +def reference_for(chain: str) -> ChainReference: + """The reference set for ``chain``. + + Raises when ``chain`` has none. Callers need an answer to proceed, and a missing chain is a + registration bug. The error names the chains that have a set. CVLR has no EVM line.""" + try: + return REFERENCE_SET[chain] + except KeyError: + raise ValueError( + f"no CVLR reference set for chain {chain!r} (have: {sorted(REFERENCE_SET)}). CVLR is " + f"the Rust-side language, so EVM has none; a new Rust chain needs an entry here." + ) from None diff --git a/composer/spec/cvlr/scaffold.py b/composer/spec/cvlr/scaffold.py new file mode 100644 index 00000000..1b607c3e --- /dev/null +++ b/composer/spec/cvlr/scaffold.py @@ -0,0 +1,883 @@ +"""The ``certora/`` tree a CVLR project needs before a rule can be written. + +The shape is a harness module behind a cargo feature, two tuning files, and a few ``Cargo.toml`` +stanzas. What to write is read from ``cargo metadata`` and from the reference set. Two cases are +refused (:class:`Blocked`) instead of guessed: a package that builds no loadable object, and a +CVLR pin that does not match the platform generation the project is already on. + +The result, for a program package inside a workspace. Files marked ``*`` are the project's and +are edited. The rest are AutoProver's. Without a ``[workspace]`` the package is the root, and the +root manifest gets no ``[workspace.dependencies]`` pins:: + + / + ├── Cargo.toml * [workspace.dependencies] pins, [patch.crates-io] forks + ├── .gitignore * prover build output + ├── / + │ └── Cargo.toml * a `certora` feature the program's forwards to + └── / + ├── Cargo.toml * `certora` feature, CVLR dependencies, + │ [package.metadata.certora] + └── src/ + ├── lib.rs * #[cfg(feature = "certora")] mod certora; + └── certora/ + ├── mod.rs + ├── specs/mod.rs where authored rules land + └── envs/ + ├── cvlr_inlining.txt generated from the starting configuration + └── cvlr_summaries.txt the same + +What the files under ``envs/`` mean is :mod:`composer.spec.cvlr.tuning`. + +AutoProver's files are rewritten whenever they differ from what the scaffold would write +(:class:`Write`), so a harness left by an earlier run or by hand is replaced, and a newer +starting configuration reaches the build. Nothing else under ``src/certora/`` is touched. + +The project's files are edited, never replaced. Each edit is planned only when what it adds is +missing, so a second run changes nothing. A manifest is edited as a TOML document +(:class:`~composer.cargo.manifest.ManifestEditor`): keys go into the tables that already hold +them, and everything the scaffold does not add comes back as it was, comments included. + +``sources`` includes ``Cargo.toml``. ``.certora_sources`` is what the report and the counterexample +analyzer read, and a source tree with no manifest cannot be rebuilt. CVLR versions come from the +reference set. +""" + +import re +from collections.abc import Mapping, Sequence +from dataclasses import dataclass, replace +from importlib.resources import files +from pathlib import Path + +from composer.cargo.features import CargoFeature +from composer.cargo.manifest import ( + AddEntries, + AddTable, + Comment, + Dependency, + Manifest, + ManifestAddition, + ManifestConflict, + ManifestEditor, + TableItem, + TomlValue, + read_manifest, +) +from composer.cargo.metadata import CratePackage, Workspace +from composer.spec.cvlr.conf import DEFAULT_FEATURE +from composer.spec.cvlr.env_paths import PathDialect, dialect_for +from composer.spec.cvlr import forks +from composer.spec.cvlr.tuning import ENV_FAMILIES, INLINING, SUMMARIES, compose_env +from composer.spec.cvlr.reference import ChainReference + +#: Where the harness module goes in the target package. +HARNESS_DIR = Path("src") / "certora" +SPECS_DIR = HARNESS_DIR / "specs" +ENVS_DIR = HARNESS_DIR / "envs" + +#: Build output the prover leaves in the project, and ``.cvlr_work``, this backend's per-unit work +#: directory. +GITIGNORE_LINES = (".certora", ".certora_internal", "certora_out", ".cvlr_work") + +#: The crate type a Solana program's library target must have. Without it cargo produces no +#: loadable object, and the prover has nothing to read. +SHARED_OBJECT_TYPE = "cdylib" + +#: The Solana convention for compiling a program without its ``entrypoint!``, which exports an +#: ``entrypoint`` symbol and installs a global allocator. Two programs linked into one object +#: collide on both, so a local dependency that is itself a program needs it on. For the verified +#: program it keeps the instruction dispatch, and the allocator and panic handler the macro +#: installs, out of the build. Enabled by ``certora`` when the package already has it. Not added +#: when it does not: a package with no entrypoint to suppress does not need one. The examples' +#: ``first_example`` has ``certora = []``. +NO_ENTRYPOINT_FEATURE = CargoFeature("no-entrypoint") + + +# --------------------------------------------------------------------------------------------- +# what a scaffolding run would change + + +@dataclass(frozen=True) +class Write: + """One of AutoProver's files, planned whenever the file on disk differs from ``contents``. + + Whatever is at the path is replaced. + """ + + path: Path + contents: str + why: str + + +@dataclass(frozen=True) +class AppendSection: + """Text appended at the end of one of the project's files, which is created if absent.""" + + path: Path + contents: str + why: str + + +@dataclass(frozen=True) +class Addition: + """One thing the plan adds to a manifest, and why.""" + + edit: ManifestAddition + why: str + + +@dataclass(frozen=True) +class EditManifest: + """One of the project's manifests, with every addition the plan makes to it, in order. + + :func:`apply` makes them against the file as it is then, so a change to it since planning is + kept. One that already has something the plan adds is :class:`ScaffoldStale`. + """ + + path: Path + additions: tuple[Addition, ...] + + +type Change = Write | AppendSection | EditManifest + + +@dataclass(frozen=True) +class Blocked: + """A decision the scaffold will not make, with what would resolve it. + + A plan that contains one applies nothing. + """ + + path: Path + problem: str + resolution: str + + +@dataclass(frozen=True) +class ScaffoldPlan: + """What scaffolding a project would change, computed without touching it.""" + + package: str + changes: tuple[Change, ...] + #: What was already in place. "Did nothing" and "found everything already there" look the + #: same in a diff. + satisfied: tuple[str, ...] + blocked: tuple[Blocked, ...] + #: How this target spells platform paths. Computed once, with the plan, so a later compose of + #: the same tuning files uses the same spelling. + dialect: PathDialect = PathDialect() + + def describe(self) -> str: + lines = [f"CVLR scaffold for {self.package}:"] + for change in self.changes: + match change: + case Write(path=path, why=why): + lines.append(f" write {path} — {why}") + case AppendSection(path=path, why=why): + lines.append(f" extend {path} — {why}") + case EditManifest(path=path, additions=additions): + lines += [f" edit {path} {a.edit.describe()} — {a.why}" for a in additions] + lines += [f" ok {note}" for note in self.satisfied] + lines += [f" BLOCKED {b.path}: {b.problem} — {b.resolution}" for b in self.blocked] + return "\n".join(lines) + + +class ScaffoldStale(RuntimeError): + """A manifest the plan edits gained, after planning, something the plan adds.""" + + +class ScaffoldBlocked(RuntimeError): + """:func:`apply` was called on a plan that still has :class:`Blocked` entries.""" + + def __init__(self, blocked: tuple[Blocked, ...]) -> None: + self.blocked = blocked + super().__init__( + "the project needs a decision no template can make:\n" + + "\n".join(f" {b.path}: {b.problem}\n {b.resolution}" for b in blocked) + ) + + +# --------------------------------------------------------------------------------------------- +# the content + + +#: What the scaffold writes on every line it adds to a manifest. +_ADDED = "added by AutoProver" + + +def _harness_source(relative: Path) -> str: + """What the scaffold writes at ``relative`` under :data:`HARNESS_DIR`. + + Kept under ``harness_files/`` at the same path, named ``.template.rs``: copied into a + project as it is, never compiled as part of AutoProver. + """ + template = relative.with_name(f"{relative.stem}.template{relative.suffix}") + return files(__package__).joinpath("harness_files", *template.parts).read_text() + + +def _harness_files(dialect: PathDialect) -> tuple[Write, ...]: + """AutoProver's files, with paths relative to the package root. + + ``mod.rs`` declares ``specs`` as ``pub``. ``cvlr::mock_fn(with = crate::certora::specs::…)`` + expands in the program's own file, outside ``certora``, so the path has to be visible from + there. ``certora`` itself stays private. Under the feature gate the module exists only in a + verification build, and it adds nothing to the crate's public API. + + ``specs/mod.rs`` is written empty so the module exists before any rule file does. A module + created later is one a later step can forget to declare. + """ + return ( + Write( + path=HARNESS_DIR / "mod.rs", + contents=_harness_source(Path("mod.rs")), + why="the harness module root", + ), + Write( + path=SPECS_DIR / "mod.rs", + contents=_harness_source(Path("specs") / "mod.rs"), + why="where authored rules land", + ), + *( + Write( + path=ENVS_DIR / family.composite, + contents=compose_env(family, dialect=dialect), + why=f"the {family.kind.lower()} the build reports to the prover", + ) + for family in ENV_FAMILIES + ), + ) + + +def _lib_declaration() -> str: + """The line that pulls the harness into the crate. + + The ``cfg`` is on this declaration, so the harness's submodules need no gate of their own. + """ + return f'\n#[cfg(feature = "{DEFAULT_FEATURE}")]\nmod certora;\n' + + +def _metadata_table(*, inlining: Path, summaries: Path) -> tuple[TableItem, ...]: + """``[package.metadata.certora]``. Tuning-file paths are relative to the package root.""" + return ( + Comment('"Cargo.toml" is included: `.certora_sources` is what the report and the'), + Comment("counterexample analyzer read, and a source tree with no manifest cannot be"), + Comment("rebuilt."), + ("sources", ["Cargo.toml", "src/**/*.rs"]), + ("solana_inlining", [str(inlining)]), + ("solana_summaries", [str(summaries)]), + ) + + +# --------------------------------------------------------------------------------------------- +# planning + + +_MOD_CERTORA = re.compile(r"^[ \t]*(?:pub[ \t]+)?mod[ \t]+certora[ \t]*;", re.MULTILINE) + + +def _project_relative(path: Path, root: Path) -> Path: + """``path`` spelled against ``root``. + + Raises when ``path`` is outside ``root``. Every path here comes from ``cargo metadata``, so + one outside the workspace means the workspace was read from somewhere other than the project + being scaffolded. + """ + try: + return path.resolve().relative_to(root.resolve()) + except ValueError: + raise ScaffoldOutsideProject(f"{path} is not under {root}") from None + + +class ScaffoldOutsideProject(RuntimeError): + """A path in the plan is outside the project root.""" + + +def _dependency(*, inherit: bool, version: str) -> Mapping[str, str | bool]: + """A CVLR dependency entry. ``optional`` is what makes ``dep:`` usable in the feature, and + what keeps CVLR out of a release build.""" + pin: dict[str, str | bool] = {"workspace": True} if inherit else {"version": f"={version}"} + return {**pin, "optional": True} + + +class _PlanBuilder: + """A :class:`ScaffoldPlan` as the planning steps assemble it. + + Each step records into one builder what it would change, what it found already in place, and + what stops the scaffold. Manifests are keyed by project-relative path. Several steps can add + to one file: a package at the workspace root gets the workspace pins, the forks, and its own + entries in one ``Cargo.toml``. Each file becomes one :class:`EditManifest`. + """ + + def __init__(self, root: Path) -> None: + self._root = root + self._read: dict[Path, Manifest] = {} + self._additions: dict[Path, list[Addition]] = {} + self._changes: list[Change] = [] + self._satisfied: list[str] = [] + self._blocked: list[Blocked] = [] + + def read(self, relative: Path) -> Manifest: + if relative not in self._read: + self._read[relative] = read_manifest(self._root / relative) + return self._read[relative] + + def add_manifest_edit(self, relative: Path, edit: ManifestAddition, why: str) -> None: + self._additions.setdefault(relative, []).append(Addition(edit, why)) + + def add_change(self, change: Change) -> None: + self._changes.append(change) + + def add_satisfied(self, note: str) -> None: + self._satisfied.append(note) + + def add_blocked(self, blocked: Blocked) -> None: + self._blocked.append(blocked) + + def build(self, package: str, dialect: PathDialect) -> ScaffoldPlan: + manifest_edits = [ + EditManifest(path=relative, additions=tuple(additions)) + for relative, additions in self._additions.items() + ] + return ScaffoldPlan( + package=package, + changes=tuple(self._changes + manifest_edits), + satisfied=tuple(self._satisfied), + blocked=tuple(self._blocked), + dialect=dialect, + ) + + +def _generation(version: str) -> str: + """The platform generation a version belongs to: its major component. + + ``solana-program`` 2.2 and 2.3 are the same generation. 1.18 and 2.2 are not, and each + generation has its own ``AccountInfo`` type.""" + return version.split(".", maxsplit=1)[0] + + +def _check_platform(workspace: Workspace, reference: ChainReference, plan: _PlanBuilder) -> None: + """Refuse to pin a CVLR release the project's platform generation cannot use. + + A target on ``solana-program`` 1.18 given ``cvlr-solana`` 0.5.0 does not warn. It fails to + compile, because the two generations have different ``AccountInfo`` types and the chain + crate's helpers return the other one. The reference set already records which generation a + chain crate requires (:class:`~composer.spec.cvlr.reference.PlatformGeneration`). This is + where a project that is on a different one is caught, and it has to be caught before the pin + is written. + + The first witness the project resolves decides. Later ones are not consulted. The list is + most-specific first because a target on a newer generation resolves only the specific crate. + Falling through to a broader witness after a specific one has answered would undo that order. + Every copy of that witness has to be on the generation: one that is not still meets CVLR's + types wherever its dependents hand an account to a helper. + """ + for witness in reference.platform.witnesses: + copies = workspace.resolved(witness.name) + if not copies: + continue + off = [c.version for c in copies if _generation(c.version) != _generation(witness.line)] + if off: + builds = ", ".join(off) + plan.add_blocked( + Blocked( + path=Path("Cargo.toml"), + problem=( + f"this project builds {witness.name} {builds}, and the CVLR line this " + f"build supports ({reference.line()}) requires " + f"{reference.platform.label}" + ), + resolution=f"move the project to {witness.name} {witness.line}", + ) + ) + return + + +@dataclass(frozen=True) +class _Pinned: + """The project states a version requirement for a CVLR crate.""" + + requirement: str + + +@dataclass(frozen=True) +class _Unpinned: + """The project names a CVLR crate without a version: a git or path dependency. + + Which release that checkout is cannot be read from the manifest, and the gate cannot pass + something it cannot read. + """ + + #: How the manifest names it, as the phrase that goes in the refusal — "as a git dependency". + how: str + + +def _declaration( + workspace: Workspace, package: CratePackage, crate: str +) -> _Pinned | _Unpinned | None: + """How this project declares ``crate``, or ``None`` when it does not. + + Both manifests that can name a dependency are consulted, and ``workspace = true`` is followed + to the root's ``[workspace.dependencies]``. A crate declared only in that table is still a + declaration: no member depends on it yet, so the resolved graph does not mention it, but the + scaffold is about to make a member inherit it. + """ + spec = read_manifest(package.root / "Cargo.toml").dependencies.get(crate) + if spec is None or spec.workspace: + spec = read_manifest(workspace.root / "Cargo.toml").workspace_dependencies.get(crate) + match spec: + case None: + return None + case Dependency(version=str(version)): + return _Pinned(version) + case Dependency(git=str()): + return _Unpinned("as a git dependency") + case Dependency(path=str()): + return _Unpinned("as a path dependency") + case _: + return _Unpinned("without a version") + + +def _check_pins( + workspace: Workspace, package: CratePackage, reference: ChainReference, plan: _PlanBuilder +) -> None: + """Refuse a project that is on a CVLR release other than the one this build is pinned to. + + One line is supported at a time — the one :mod:`composer.spec.cvlr.reference` names — and + everything this scaffold writes belongs to it: the pins, the specializations added beside + them, and the env files :mod:`composer.spec.cvlr.tuning` composes. A project already on + another line cannot be given those without putting two CVLR generations in one graph, which + does not compile. This scaffold used to resolve that by deferring to the project's pin and + withholding the specializations; a run set up that way is on a configuration nothing else + here is built for, so it is refused instead. + + Two readings, because neither alone covers the project. The resolved graph is exact and + settles a crate some member already depends on. The manifests settle a crate declared in + ``[workspace.dependencies]`` that no member depends on yet — absent from the graph, and about + to be inherited by the member this scaffold is setting up. + + A crate the project does not name at all is not checked. That is + :class:`~composer.spec.cvlr.crates.Absent`, the ordinary state of a specialization the project + has no use for, and refusing it would refuse every project this scaffold exists to set up. + """ + for release in reference.crates(): + supported = f"this build supports only {release.name} {release.version}" + fix = f"move the project to {release.name} {release.version}" + off = [c.version for c in workspace.resolved(release.name) if c.version != release.version] + if off: + builds = ", ".join(off) + plan.add_blocked( + Blocked( + path=Path("Cargo.toml"), + problem=f"this project builds {release.name} {builds}, and {supported}", + resolution=fix, + ) + ) + continue + match _declaration(workspace, package, release.name): + case _Pinned(requirement) if requirement.removeprefix("=") != release.version: + plan.add_blocked( + Blocked( + path=Path("Cargo.toml"), + problem=( + f"this project declares {release.name} {requirement}, and {supported}" + ), + resolution=fix, + ) + ) + case _Unpinned(how): + plan.add_blocked( + Blocked( + path=Path("Cargo.toml"), + problem=( + f"this project declares {release.name} {how}, so its release cannot " + f"be checked, and {supported}" + ), + resolution=( + f"declare {release.name} {release.version} as a registry dependency" + ), + ) + ) + case _: + pass + + +def _plan_workspace_manifest(reference: ChainReference, plan: _PlanBuilder) -> None: + """Pins in ``[workspace.dependencies]``, when the root manifest has a ``[workspace]``.""" + path = Path("Cargo.toml") + root = plan.read(path) + if root.workspace is None: + return + + declared = root.workspace.dependencies + pins: list[tuple[str, TomlValue]] = [] + for crate in reference.scaffold_crates(): + if crate.name in declared: + plan.add_satisfied( + f"{crate.name} is already a workspace dependency, so it is left as it is; its " + f"release is checked on its own" + ) + continue + pins.append((crate.name, {"version": f"={crate.version}"})) + if pins: + plan.add_manifest_edit( + path, + AddEntries(("workspace", "dependencies"), tuple(pins)), + "pin the CVLR releases the reference set names, for the whole workspace", + ) + + +def local_dependencies(workspace: Workspace, package: CratePackage) -> tuple[CratePackage, ...]: + """The workspace crates ``package`` depends on by path, in manifest order. + + Read from the manifest's ``path =`` entries, not from the resolved graph. The question is + which crates this project owns. A registry crate that a patch table resolves to a workspace + member is still somebody else's code. + """ + declared = read_manifest(package.root / "Cargo.toml").dependencies + named = [name for name, spec in declared.items() if spec.path is not None] + return tuple( + found for name in named if (found := workspace.member(name)) is not None + ) + + +def _certora_feature(package: CratePackage, reference: ChainReference) -> list[str]: + """What ``package``'s ``certora`` feature turns on within ``package`` itself: the CVLR + crates, and ``no-entrypoint`` when the package declares it.""" + enables = [f"dep:{c.name}" for c in reference.scaffold_crates()] + if NO_ENTRYPOINT_FEATURE in package.features: + enables.insert(0, NO_ENTRYPOINT_FEATURE) + return enables + + +def _plan_feature_forwarding( + workspace: Workspace, package: CratePackage, reference: ChainReference, plan: _PlanBuilder +) -> None: + """Give each library crate the program depends on its own ``certora`` feature. + + A cargo feature is a named on/off switch that a crate (a Rust package) declares. Code marked + with a feature is compiled only when that feature is on. The libraries in question are the + crates in this project that the program uses by folder path, not ones downloaded from a + registry. + + Sometimes verification needs to change code inside one of those libraries. That change must + not end up in a normal build, so it is marked with a feature, and it has to be a feature that + library declares itself. Turning on the program's ``certora`` feature turns on each library's + ``certora`` feature too. + + Each verification unit also has its own feature (``unit_x``). Those features are empty and + affect only the program's own code (:func:`declare_unit_features`). If they were passed down + to the libraries (``unit_x = ["library/unit_x"]``), every unit would build the libraries with + different switches, so cargo would recompile them for each unit. Passing down only the shared + ``certora`` feature means every unit builds the libraries the same way. The trade-off is that + a library change marked this way is on for every unit, not only the one that needed it. + + This runs at setup, not when the first library change is made. Cargo decides which features + are on when a build starts, so a feature added to a library after that is not seen by that + build. + """ + for dep in local_dependencies(workspace, package): + path = dep.root.resolve().relative_to(workspace.root.resolve()) / "Cargo.toml" + manifest = plan.read(path) + if DEFAULT_FEATURE in manifest.features: + plan.add_satisfied(f"{dep.name} already declares a `{DEFAULT_FEATURE}` feature") + continue + missing = [c for c in reference.scaffold_crates() if c.name not in manifest.dependencies] + plan.add_manifest_edit( + path, + AddEntries(("features",), ((DEFAULT_FEATURE, _certora_feature(dep, reference)),)), + f"so a verification-only edit inside {dep.name} can be gated — the program's " + f"`{DEFAULT_FEATURE}` forwards to it", + ) + if missing: + plan.add_manifest_edit( + path, + AddEntries( + ("dependencies",), + tuple((c.name, _dependency(inherit=False, version=c.version)) for c in missing), + ), + f"the CVLR crates {dep.name}'s `{DEFAULT_FEATURE}` feature enables", + ) + + +def _plan_package_manifest( + workspace: Workspace, + package: CratePackage, + relative: Path, + reference: ChainReference, + plan: _PlanBuilder, + *, + inherit: bool, +) -> None: + """Plan the edits to the scaffolded package's own ``Cargo.toml``. + + Three things go there, each skipped when the manifest already has it: + + - the CVLR crates, as optional dependencies, so a release build does not compile them; + - the ``certora`` feature, which turns those dependencies on, along with ``no-entrypoint`` + when the package declares it and every local dependency's own ``certora`` feature + (:func:`_plan_feature_forwarding`); + - ``[package.metadata.certora]``, which tells the prover where the sources and tuning files + are. + + ``inherit`` writes each dependency as ``workspace = true``. It is set when the root manifest + has a ``[workspace]``, where :func:`_plan_workspace_manifest` puts the pins. + + Two things stop the scaffold here: a package that builds no ``cdylib``, since the prover has + no object to read, and a ``certora`` feature that exists while no CVLR crate is a dependency, + since the name then means something the scaffold should not extend. + """ + manifest_rel = relative / "Cargo.toml" + manifest = plan.read(manifest_rel) + + if package.lib is None or not package.lib.builds_shared_object: + plan.add_blocked( + Blocked( + path=manifest_rel, + problem=( + f"{package.name} builds no {SHARED_OBJECT_TYPE}, so there is no program for " + f"the prover to read" + ), + resolution=( + f'add `crate-type = ["{SHARED_OBJECT_TYPE}"]` to `[lib]` if this package is ' + f"the on-chain program, or scaffold the package that is" + ), + ) + ) + + wanted = reference.scaffold_crates() + missing = [c for c in wanted if c.name not in manifest.dependencies] + for crate in wanted: + if crate not in missing: + plan.add_satisfied(f"{crate.name} is already a dependency of {package.name}") + + features = manifest.features + if DEFAULT_FEATURE in features: + plan.add_satisfied( + f"the `{DEFAULT_FEATURE}` feature already exists as {features[DEFAULT_FEATURE]!r}" + ) + if len(missing) == len(wanted): + plan.add_blocked( + Blocked( + path=manifest_rel, + problem=( + f"`{DEFAULT_FEATURE}` is already a feature but no CVLR crate is a " + f"dependency, so the name means something else in this package" + ), + resolution=( + "rename that feature, or add the CVLR dependencies to it by hand and re-run" + ), + ) + ) + else: + # Cargo features don't cross crate boundaries: the program's `certora` turns on a + # library's only by naming it here. See :func:`_plan_feature_forwarding`. + enables = _certora_feature(package, reference) + [ + f"{dep.name}/{DEFAULT_FEATURE}" for dep in local_dependencies(workspace, package) + ] + plan.add_manifest_edit( + manifest_rel, + AddEntries(("features",), ((DEFAULT_FEATURE, enables),)), + f"the feature that compiles the harness in ({', '.join(enables)})", + ) + + if missing: + plan.add_manifest_edit( + manifest_rel, + AddEntries( + ("dependencies",), + tuple((c.name, _dependency(inherit=inherit, version=c.version)) for c in missing), + ), + "the CVLR dependencies a verification build compiles", + ) + + if manifest.certora_metadata is not None: + plan.add_satisfied("[package.metadata.certora] already declares sources and tuning files") + else: + plan.add_manifest_edit( + manifest_rel, + AddTable( + ("package", "metadata", "certora"), + _metadata_table( + inlining=ENVS_DIR / INLINING.composite, + summaries=ENVS_DIR / SUMMARIES.composite, + ), + ), + "the sources and tuning files the prover reads", + ) + + +def _plan_harness( + package: CratePackage, relative: Path, dialect: PathDialect, plan: _PlanBuilder +) -> None: + for file in _harness_files(dialect): + on_disk = package.root / file.path + if on_disk.is_file() and on_disk.read_text() == file.contents: + plan.add_satisfied(f"{relative / file.path} is current") + else: + plan.add_change(replace(file, path=relative / file.path)) + + if package.lib is not None: + lib_rel = _project_relative(package.lib.src_path, package.root) + # cargo metadata reports a `[lib] path` without checking the file exists. + if not package.lib.src_path.is_file(): + plan.add_blocked( + Blocked( + path=relative / "Cargo.toml", + problem=( + f"{package.name}'s library source, {relative / lib_rel}, does not exist, " + f"so there is no crate to add the harness to" + ), + resolution=( + "point `[lib] path` at the program's source, or scaffold the package that " + "has it" + ), + ) + ) + elif _MOD_CERTORA.search(package.lib.src_path.read_text()): + plan.add_satisfied(f"{relative / lib_rel} already declares the harness module") + else: + plan.add_change( + AppendSection( + path=relative / lib_rel, + contents=_lib_declaration(), + why="pull the harness into the crate, gated on the feature", + ) + ) + + +def _plan_forks(workspace: Workspace, reference: ChainReference, plan: _PlanBuilder) -> None: + """Add ``[patch.crates-io]`` entries for the chain's verification forks. + + The table is workspace-level, so it goes on the workspace manifest with the rest of the plan. + What each fork fixes is on the fork (:mod:`composer.spec.cvlr.forks`). A version the fork + does not cover becomes a + :class:`Blocked` on that manifest. The run stops instead of building a project that later + fails with a pointer-analysis error. + + Crates the manifest already redirects are left alone. :func:`forks.already_patched` reads the + patch table. The resolved graph is checked too, because a redirect shows up there as a git + source. + """ + path = Path("Cargo.toml") + match forks.plan_overrides( + workspace, reference.forks, already_redirected=forks.already_patched(plan.read(path)) + ): + case forks.ForkRefused(blocked): + for b in blocked: + plan.add_blocked(Blocked(path=path, problem=b.problem, resolution=b.resolution)) + case forks.ForkPlan() as overrides: + for override, table in forks.patch_tables(overrides): + plan.add_manifest_edit( + path, + table, + f"verify {override.crate} {override.version} against {override.branch} of " + f"the fork", + ) + for note in overrides.notes(): + plan.add_satisfied(note) + + +def _plan_gitignore(workspace: Workspace, plan: _PlanBuilder) -> None: + path = workspace.root / ".gitignore" + existing = path.read_text() if path.is_file() else None + ignored = {line.strip() for line in (existing or "").splitlines()} + absent = [line for line in GITIGNORE_LINES if line not in ignored] + if not absent: + plan.add_satisfied("prover build output is already gitignored") + return + plan.add_change( + AppendSection( + path=Path(".gitignore"), + contents=("" if existing is None else "\n") + + "# Certora Prover build output\n" + + "".join(f"{line}\n" for line in absent), + why=f"ignore {', '.join(absent)}", + ) + ) + + +def plan_scaffold( + workspace: Workspace, package: CratePackage, reference: ChainReference +) -> ScaffoldPlan: + """What scaffolding ``package`` would change, without changing anything. + + Every path is relative to ``workspace.root``, which is also what :func:`apply` writes under. + """ + relative = _project_relative(package.root, workspace.root) + plan = _PlanBuilder(workspace.root) + inherit = plan.read(Path("Cargo.toml")).workspace is not None + dialect = dialect_for(workspace, reference) + + _plan_workspace_manifest(reference, plan) + _plan_harness(package, relative, dialect, plan) + _plan_gitignore(workspace, plan) + _plan_feature_forwarding(workspace, package, reference, plan) + _plan_forks(workspace, reference, plan) + _plan_package_manifest(workspace, package, relative, reference, plan, inherit=inherit) + # Unconditional, both of them: the scaffold always writes the reference-set pin now, so the + # reference set's platform generation always describes what will be built. + _check_pins(workspace, package, reference, plan) + _check_platform(workspace, reference, plan) + return plan.build(package.name, dialect) + + +# --------------------------------------------------------------------------------------------- +# applying + + +def declare_unit_features( + manifest: Path, features: Sequence[CargoFeature] +) -> tuple[CargoFeature, ...]: + """Declare one empty cargo feature per name, and return the ones this call added. + + ``--features certora,unit_x`` fails with "Package does not contain this feature" unless + ``unit_x`` is declared. The features are empty. A feature that enabled a dependency feature + would change that dependency's resolved feature set and rebuild it per unit. Empty means only + this crate's own code varies with the feature. + + A feature that is already declared is left as it is. + """ + edited = ManifestEditor.read(manifest) + wanted = [f for f in dict.fromkeys(features) if f not in edited.manifest.features] + if not wanted: + return () + edited.apply(AddEntries(("features",), tuple((f, []) for f in wanted)), note=_ADDED) + manifest.write_text(edited.text()) + return tuple(wanted) + + +def apply(plan: ScaffoldPlan, root: Path) -> tuple[Path, ...]: + """Carry out ``plan`` under ``root``, returning the paths it touched, in order. + + Refuses a plan that still has a :class:`Blocked` entry. A partial scaffold leaves the next + build with two possible causes. + """ + if plan.blocked: + raise ScaffoldBlocked(plan.blocked) + + touched: list[Path] = [] + for change in plan.changes: + target = root / change.path + # Every path in a plan comes from constants and from cargo metadata. A path outside the + # project root is a planner bug. Do not write it. + if not target.resolve().is_relative_to(root.resolve()): + raise ScaffoldOutsideProject(f"{target} escapes {root}") + match change: + case Write(contents=contents): + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text(contents) + case AppendSection(contents=contents): + existing = target.read_text() if target.is_file() else "" + target.parent.mkdir(parents=True, exist_ok=True) + target.write_text(existing + contents) + case EditManifest(additions=additions): + edited = ManifestEditor.read(target) + for addition in additions: + try: + edited.apply(addition.edit, note=_ADDED) + except ManifestConflict as exc: + raise ScaffoldStale( + f"{change.path} changed after the scaffold was planned: {exc}" + ) from exc + target.write_text(edited.text()) + touched.append(change.path) + return tuple(touched) diff --git a/composer/spec/cvlr/tuning.py b/composer/spec/cvlr/tuning.py new file mode 100644 index 00000000..99228c2f --- /dev/null +++ b/composer/spec/cvlr/tuning.py @@ -0,0 +1,170 @@ +"""The two tuning files a CVLR build gives the Solana Prover, and how each is assembled. + +The Prover verifies the compiled SBF program. Before it checks a rule, it decides which calls to +analyze through their bodies and what it may assume about the calls it does not analyze. Those +two answers are the inlining file and the summaries file. A package names them in +``[package.metadata.certora]`` (``solana_inlining``, ``solana_summaries``), and ``cargo +certora-sbf`` reports them to the Prover through the build manifest. Every directive in either +file is a regular expression over demangled symbol names. + +Inlining (:data:`INLINING`) + One directive per line, ``#[inline] `` or ``#[inline(never)] ``. An inlined + call is analyzed through its body. Any other call is opaque. The Prover does not look inside + it, and it knows nothing about what the call wrote. The starting configuration leaves + ``core``, ``std``, ``alloc``, ``solana_program`` and ``anchor_lang`` opaque by default. The + exceptions are the functions whose effects a rule depends on: the ``AccountInfo`` accessors, + ``invoke``, error conversions, and Anchor's account loaders. + +Summaries (:data:`SUMMARIES`) + Points-to summaries for opaque calls: one or more ``#[type(:)]`` lines, then + the pattern they describe. A location is a register (``r0``, the return value) or memory at an + offset from one (``(*i64)(r1+8)``, the second word written through the first argument, which + is where an out-pointer return lands). A kind is ``num``, ``ptr_heap`` or ``ptr_external``. + The pointer analysis needs a type for memory an opaque call wrote, and without the body a + summary is the only source of one. + +A pattern that matches nothing is not an error. The directive does not apply, and the Prover runs +with a different configuration than the file appears to describe. Most of the care taken below +is about that failure. + +Each file is split into layers. The starting layers live only under :data:`ENV_DIR`. The rest +are in the target's ``envs/`` directory:: + + _core.txt starting configuration: the Rust runtime and the Solana platform + _anchor.txt starting configuration: the Anchor framework (inlining only) + __run.txt one unit's own directives + .txt generated from the starting layers, named by the package + _.txt generated from those plus the unit's, named by one unit's conf + +When to change which layer: + +- **The starting layers** are the configuration every target begins with, kept under + :data:`ENV_DIR`. A change every target needs, such as a soundness fix, is made there. They are + written with pre-split ``solana_program::`` paths, and :mod:`composer.spec.cvlr.env_paths` + rewrites those into the target's platform generation when a composite is built. They are not + copied into the target. A composite carries their content, spelled for that target. +- **The unit layer** holds the directives one unit's submission needs. A rule may need to see + through a library function the starting layers leave opaque (``#[inline]``). A function may be + too expensive or impossible to analyze, and a rule does better leaving it opaque + (``#[inline(never)]``). An opaque call that the pointer analysis cannot type needs a summary. + The layer is per unit because a pattern applies to the whole build, and no cargo feature can + scope it. It is written against the project's own symbols, so paths in it are not rewritten. +- **The composites are not edited.** :func:`compose_env` builds them from the layers, and the + scaffold rewrites the package composite whenever it differs from that. A directive written into + a composite is not in any layer, and the next composition drops it. +""" + +from dataclasses import dataclass +from importlib.resources import files + +from composer.spec.cvlr.env_paths import PathDialect + +#: The starting layers, shipped in the wheel. Every composite is built from these. +ENV_DIR = files(__package__) / "envs" + + +@dataclass(frozen=True) +class StartingLayer: + """One starting layer of a tuning file.""" + + #: The ```` in ``_.txt``. + name: str + #: What the layer's directives cover, as prose. The composite names its layers by this, since + #: the layer files themselves are not in the target. + covers: str + + +@dataclass(frozen=True) +class EnvFamily: + """One tuning file, split into layers.""" + + stem: str + #: What the file's directives are, as prose. + kind: str + #: The starting layers, in composition order, each named ``_.txt``. + layers: tuple[StartingLayer, ...] + + @property + def starting(self) -> tuple[str, ...]: + """The starting layers' file names, in the order the composite carries them.""" + return tuple(f"{self.stem}_{layer.name}.txt" for layer in self.layers) + + @property + def composite(self) -> str: + """The file the package declares. Generated from the starting layers.""" + return f"{self.stem}.txt" + + def unit_layer(self, unit: str) -> str: + """The file name for one unit's own directives. + + A summary is a symbol pattern the prover applies to the whole build, not something a cargo + feature can scope. Lines added to a file every unit's conf names would apply to every + unit's submission. + """ + return f"{self.stem}_{unit}_run.txt" + + def unit_composite(self, unit: str) -> str: + """The file one unit's conf names. Generated from the starting layers and the unit's.""" + return f"{self.stem}_{unit}.txt" + + +_CORE = StartingLayer("core", "the Rust runtime and the Solana platform") + +#: Which calls the Prover analyzes through their bodies. Declared as ``solana_inlining``. +INLINING = EnvFamily( + "cvlr_inlining", + kind="Inlining directives", + layers=(_CORE, StartingLayer("anchor", "the Anchor framework")), +) +#: What the pointer analysis may assume about the memory an opaque call writes. Declared as +#: ``solana_summaries``. +SUMMARIES = EnvFamily("cvlr_summaries", kind="Points-to summaries", layers=(_CORE,)) +ENV_FAMILIES = (INLINING, SUMMARIES) + +#: The starting layers — one content for every target, as against the per-unit layer. +STARTING_ENVS = tuple(name for f in ENV_FAMILIES for name in f.starting) + + +_GENERATED_HEADER = """;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Generated — this is the file the build reports to the prover. +;;; Rewritten on every run, so an edit made here is lost. Composed, +;;; in order, from AutoProver's starting configuration for: +{layers} +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +""" + + +def starting_env(name: str, dialect: PathDialect = PathDialect()) -> str: + """One starting layer, spelled for the target's platform generation. + + The default dialect changes nothing, so a caller comparing against the file on disk gets that + file. + """ + return dialect.render((ENV_DIR / name).read_text()) + + +def compose_env( + family: EnvFamily, *, unit_layer: str | None = None, dialect: PathDialect = PathDialect() +) -> str: + """The generated composite: header, then the layers, in order. + + The scaffold writes the package-level composite, which has no ``unit_layer``. A unit layer is + one unit's directives, so they are not applied to another unit's submission (see + :meth:`EnvFamily.unit_layer`). Those are the project's own symbols, so the dialect leaves them + alone. + """ + header = _GENERATED_HEADER.format( + layers="\n".join(f";;; {layer.covers}" for layer in family.layers) + ) + parts = [header] + if dialect.aliases: + # Said in the file, so a reader who knows the upstream ``solana_program::`` paths is not + # surprised to find other crates' paths in their place. + parts.append( + f";;; {len(dialect.aliases)} solana_program path prefixes respelled for the " + f"crates this project resolves\n" + ) + parts += [starting_env(name, dialect) for name in family.starting] + if unit_layer is not None: + parts.append(unit_layer) + return "\n".join(p.rstrip("\n") for p in parts) + "\n" diff --git a/composer/spec/natspec/task_description.py b/composer/spec/natspec/task_description.py index 80583ff4..5b62df82 100644 --- a/composer/spec/natspec/task_description.py +++ b/composer/spec/natspec/task_description.py @@ -7,6 +7,7 @@ from graphcore.tools.vfs import GlobalExcludeArg +from composer.prover.conf import dump_conf from composer.spec.gen_types import ITypedTemplate from composer.spec.natspec.models import ( InterfaceDeclModel, @@ -152,9 +153,8 @@ def build_to(self, path: pathlib.Path) -> ContextManager[pathlib.Path]: @contextlib.contextmanager def _build_to(self, path: pathlib.Path) -> Iterator[pathlib.Path]: - import json with temp_certora_file( - content=json.dumps(self.config, indent=2), + content=dump_conf(self.config), root=str(path), ext="conf", prefix="run", diff --git a/composer/spec/source/artifacts.py b/composer/spec/source/artifacts.py index 9d1e52b1..88bbc2f2 100644 --- a/composer/spec/source/artifacts.py +++ b/composer/spec/source/artifacts.py @@ -20,6 +20,7 @@ AP_REPORT_DIR, AUTOPROVE_INTERNAL_DIR, CERTORA_DIR, buffer_spec_path, component_specs_dir, under_project, ) +from composer.prover.conf import dump_conf from composer.spec.source.prover import prover_config_overlay from composer.spec.util import ensure_dir @@ -106,7 +107,7 @@ def write_artifact(self, i: ComponentSpec, artifact: GeneratedCVL) -> Path: main_contract=self._main_contract, verify_target=f"{self._main_contract}:{i.buffer_spec_rel(name)}", ) - _write_checked(confs_root / f"verify_{name}.conf", json.dumps(conf, indent=2)) + _write_checked(confs_root / f"verify_{name}.conf", dump_conf(conf)) else: _log.warning("no base config for %s; skipping conf dump", i.stem) self._write_commentary(i.stem, artifact.commentary) diff --git a/composer/spec/source/author.py b/composer/spec/source/author.py index 8c87b171..6d514698 100644 --- a/composer/spec/source/author.py +++ b/composer/spec/source/author.py @@ -28,7 +28,7 @@ ) 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 setup_prover_config_in +from composer.spec.source.prover import rule_selection, setup_prover_config_in from composer.spec.source.spec_buffers import ( SpecBuffersExtra, buffer_review_text, buffer_state_digest, check_buffer_completion, combined_buffers_view, max_spec_buffers, requireinvariant_citations, run_targets, @@ -838,6 +838,9 @@ async def run( exclude_rules: list[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( @@ -846,8 +849,7 @@ async def run( main_contract=self.main_contract, spec_contents=curr_spec, config=self.config, - rule=rules, - exclude_rule=exclude_rules, + rules=selection, **config ) as (conf_path, _): return await run_prover( diff --git a/composer/spec/source/prover.py b/composer/spec/source/prover.py index f37bc1eb..c6e4a271 100644 --- a/composer/spec/source/prover.py +++ b/composer/spec/source/prover.py @@ -10,7 +10,6 @@ import asyncio import functools -import json import logging import os import time @@ -42,6 +41,9 @@ DefaultCexHandler, ProverReport ) from composer.prover.callbacks import ProverEventCallbacks +from composer.prover.conf import ( + Conf, ExcludeRules, InheritRules, RuleSelection, SelectRules, dump_conf, +) from composer.prover.ptypes import StatusCodes from composer.ui.tool_display import tool_display from composer.diagnostics.stream import ( @@ -77,19 +79,45 @@ from this set, or an "accepted" flag edit would never reach the prover.""" -def prover_config_overlay(base_config: dict, *, main_contract: str, verify_target: str) -> dict: +def prover_config_overlay( + base_config: Conf, + *, + main_contract: str, + verify_target: str, + extra: Conf | None = None, + rules: RuleSelection = InheritRules(), +) -> Conf: """The fixed prover settings the source pipeline layers on top of the base config. Shared by the live prover run and the persisted ``certora/confs`` dump so the two can't drift. ``verify_target`` is the ``:`` the run verifies. """ - return { + conf = { **base_config, "verify": verify_target, "parametric_contracts": main_contract, "optimistic_loop": True, "rule_sanity": "basic", + **(extra or {}), } + return rules.apply_to(conf) + + +BOTH_RULE_SCOPES = "Cannot invoke the prover with both `rules` and `exclude_rules` set to non-none" + + +def rule_selection( + rules: list[str] | None, exclude_rules: list[str] | None +) -> RuleSelection | str: + """The run's scope from a caller's ``rules``/``exclude_rules`` pair, or why the pair is + invalid. Neither leaves the base config's own selection in force.""" + if rules is not None and exclude_rules is not None: + return BOTH_RULE_SCOPES + if rules is not None: + return SelectRules(tuple(rules)) + if exclude_rules is not None: + return ExcludeRules(tuple(exclude_rules)) + return InheritRules() @@ -111,19 +139,19 @@ def _merge_rule_skips(left: dict[str, str], right: dict[str, str]) -> dict[str, to_ret[k] = v return to_ret -class RuleSelection(TypedDict): +class RuleSelectionRecord(TypedDict): sort: Literal["exclude", "include"] selector: list[str] -def _selection_of(rule: list[str] | None, exclude_rules: list[str] | None) -> RuleSelection | None: - """The ``RuleSelection`` a submit_buffer call asks for, or None to run the whole buffer.""" +def _selection_of(rule: list[str] | None, exclude_rules: list[str] | None) -> RuleSelectionRecord | None: + """The ``RuleSelectionRecord`` a submit_buffer call asks for, or None to run the whole buffer.""" if rule is not None: - return RuleSelection(sort="include", selector=rule) + return RuleSelectionRecord(sort="include", selector=rule) if exclude_rules is not None: - return RuleSelection(sort="exclude", selector=exclude_rules) + return RuleSelectionRecord(sort="exclude", selector=exclude_rules) return None -def _selection_key(sel: RuleSelection | None) -> str: +def _selection_key(sel: RuleSelectionRecord | None) -> str: """A stable key distinguishing one buffer's rule selections, so striped runs (different subsets of the same buffer at the same content) coexist as separate jobs instead of deduping each other. The whole-buffer run keys to the empty string.""" @@ -131,17 +159,18 @@ def _selection_key(sel: RuleSelection | None) -> str: return "" return f"{sel['sort']}:{','.join(sorted(sel['selector']))}" -def _apply_selection(config: dict, selection: RuleSelection | None) -> None: - """Write a rule subset onto a prover conf: ``rule`` for an include selection, ``exclude_rule`` for - an exclude one; a None selection leaves the conf running every rule.""" - if selection is not None: - config["rule" if selection["sort"] == "include" else "exclude_rule"] = list(selection["selector"]) +def _scope_of(record: RuleSelectionRecord | None) -> RuleSelection: + """The conf scope a recorded selection runs under; None runs every rule.""" + if record is None: + return InheritRules() + names = tuple(record["selector"]) + return SelectRules(names) if record["sort"] == "include" else ExcludeRules(names) class ProverRunLog(TypedDict): tool_call_id: str prover_results: list[tuple[RulePath, StatusCodes]] spec_digest: str - rules: RuleSelection | None + rules: RuleSelectionRecord | None sort: Literal["run"] declared_rules: list[str] state_digest: str @@ -617,8 +646,7 @@ def setup_prover_config_in( spec_contents: str, spec_stem: str | None = None, main_contract: str, - rule: list[str] | None, - exclude_rule: list[str] | None, + rules: RuleSelection, conf_dir: Path = CERTORA_DIR, **config_extra ): @@ -628,13 +656,15 @@ def setup_prover_config_in( name=spec_stem ) as generated_path: config = prover_config_overlay( - config, main_contract=main_contract, verify_target=f"{main_contract}:{generated_path}" + config, + main_contract=main_contract, + verify_target=f"{main_contract}:{generated_path}", + extra=config_extra, + rules=rules, ) - config.update(config_extra) - _apply_selection(config, _selection_of(rule, exclude_rule)) with temp_certora_file( root=working_dir, - content=json.dumps(config, indent=2), + content=dump_conf(config), ext="conf", name=spec_stem, prefix="verify", @@ -700,19 +730,21 @@ def buffer_conf( buffer_name: str, conf_dir: Path, msg: str, - selection: RuleSelection | None = None, + selection: RuleSelectionRecord | None = None, ) -> 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).""" cfg = prover_config_overlay( - config, main_contract=main_contract, verify_target=f"{main_contract}:{spec_path}" + config, + main_contract=main_contract, + verify_target=f"{main_contract}:{spec_path}", + extra={"msg": msg}, + rules=_scope_of(selection), ) - cfg["msg"] = msg - _apply_selection(cfg, selection) with temp_certora_file( root=working_dir, - content=json.dumps(cfg, indent=2), + content=dump_conf(cfg), ext="conf", name=f"verify_{buffer_name}", prefix="verify", @@ -789,7 +821,7 @@ class _BufJob: task: asyncio.Task[None] #: The rule subset this job runs, or None for the whole buffer. Jobs of one buffer are keyed by #: ``(name, _selection_key(selection))``, so striped runs at the same content coexist. - selection: RuleSelection | None = None + selection: RuleSelectionRecord | None = None @dataclass @@ -802,7 +834,7 @@ class _BufDone: result: ProverReport | str all_rules: list[str] #: The rule subset this run covered, recorded onto the run's ``ProverRunLog.rules``. - selection: RuleSelection | None = None + selection: RuleSelectionRecord | None = None def get_prover_tool( @@ -844,7 +876,7 @@ async def _run_buffer_job( *, name: str, digest: str, label: str, buffers: Mapping[str, NamedBuffer], vfs: dict[str, str], conf: dict, cex_state: StateWithSkips, tool_call_id: str, writer: Callable[[ProverEvents], None], summary: RunSummary, - selection: RuleSelection | None = None, + selection: RuleSelectionRecord | None = None, ) -> None: """Verify one buffer end-to-end against a frozen snapshot (taken at submit time) of the source and all buffers, then push the outcome onto the completion queue. The job runs in its own diff --git a/pyproject.toml b/pyproject.toml index e535654f..b15b8b6a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -60,6 +60,7 @@ dependencies = [ "isodate>=0.6.0", "fsspec>=2023.1.0", "ijson>=3.2.0", + "tomlkit>=0.15.1", ] [project.optional-dependencies] @@ -226,6 +227,7 @@ include = ["composer*", "sanity_analyzer*", "analyzer*", "certora_autosetup*", " composer = [ "templates/**/*.j2", "templates/*.js", "scripts/init-db.sql", "kb/resources/**/*.md", "kb/resources/*.yaml", + "spec/cvlr/envs/*.txt", "spec/cvlr/harness_files/**/*.template.rs", ] # Bundled CVL summaries, spec templates, mocks and conf templates the prover # reads directly off disk; ship them with the wheel. diff --git a/tests/data/vault_sbf_symbols.txt b/tests/data/vault_sbf_symbols.txt new file mode 100644 index 00000000..07172222 --- /dev/null +++ b/tests/data/vault_sbf_symbols.txt @@ -0,0 +1,70 @@ +# Demangled symbols from test_scenarios/solana_vault_idl built for SBF with platform-tools +# v1.43 (anchor-lang 0.31.1, solana-program 2.3.0). Filtered to the platform and Anchor +# layers, which is what the tuning files address. Regenerate with: +# cargo certora-sbf --tools-version v1.43 +# llvm-nm --defined-only target/sbf-solana-solana/release/vault.so \ +# | awk '{ $1=""; $2=""; sub(/^[ \t]+/,""); print }' | rustfilt | sort -u + as anchor_lang::Accounts>::try_accounts +anchor_lang::accounts::account::Account::exit_with_expected_owner +anchor_lang::accounts::account::Account::try_from +anchor_lang::accounts::account::Account::try_from_unchecked + as anchor_lang::Accounts>::try_accounts +>::try_accounts +anchor_lang::accounts::signer::Signer::try_from + as std::io::Write>::write_all +anchor_lang::common::close +anchor_lang::common::is_closed +anchor_lang::error::AnchorError::log +>::from +>::from +>::from +::fmt +anchor_lang::error::ErrorCode::name +anchor_lang::error::Error::log +anchor_lang::error::Error::with_account_name +anchor_lang::error::Error::with_pubkeys +anchor_lang::error::Error::with_values +anchor_lang::error:: for solana_program_error::ProgramError>::from +anchor_lang::error::ProgramErrorWithOrigin::log +anchor_lang::system_program::allocate +anchor_lang::system_program::assign +anchor_lang::system_program::create_account +anchor_lang::system_program::transfer +::clone +solana_account_info::AccountInfo::assign +solana_account_info::AccountInfo::data_is_empty +solana_account_info::AccountInfo::data_len +solana_account_info::AccountInfo::lamports +solana_account_info::AccountInfo::realloc +solana_account_info::AccountInfo::try_borrow_data +solana_account_info::AccountInfo::try_borrow_lamports +solana_account_info::AccountInfo::try_borrow_mut_data +solana_account_info::AccountInfo::try_borrow_mut_lamports +solana_account_info::AccountInfo::try_data_len +solana_cpi::invoke_signed_unchecked +solana_instruction::Instruction::new_with_bincode +solana_program_entrypoint::deserialize +solana_program_error:: for u64>::from +::clone +>::from +::fmt +::fmt +solana_program::program::invoke +solana_program::program::invoke_signed +solana_pubkey::_::::serialize +::deserialize_reader +solana_pubkey::Pubkey::create_program_address +solana_pubkey::Pubkey::create_with_seed +::fmt +solana_pubkey::Pubkey::find_program_address +solana_pubkey::Pubkey::log +solana_rent::Rent::is_exempt +solana_rent::Rent::minimum_balance +solana_sha256_hasher::hashv +>::from +solana_system_interface::instruction::allocate +solana_system_interface::instruction::assign +solana_system_interface::instruction::create_account +solana_system_interface::instruction::create_account_with_seed +solana_system_interface::instruction::transfer +solana_sysvar::rent::::get diff --git a/tests/test_cvlr_env_paths.py b/tests/test_cvlr_env_paths.py new file mode 100644 index 00000000..6c3c9375 --- /dev/null +++ b/tests/test_cvlr_env_paths.py @@ -0,0 +1,439 @@ +"""Spelling the starting tuning files for the platform generation a target is on. + +A directive whose path was renamed matches nothing. It does not raise, log, or fail the build, +and the prover runs with a different configuration than the file appears to describe. The tests +check that a rewrite happens where it must, and does not happen where it must not. + +:func:`test_every_declared_alias_still_names_something_in_the_starting_files` is the one that +goes stale quietly. An alias is written against a starting layer. After that file changes, an +alias whose path no longer appears still looks like coverage. +""" + +from pathlib import Path + +import pytest + +from composer.cargo.metadata import CratePackage, RegistrySource, Workspace +from composer.spec.cvlr.env_paths import PathDialect, dialect_for +from composer.spec.cvlr.tuning import ( + ENV_DIR, + INLINING, + STARTING_ENVS, + compose_env, + starting_env, +) +from composer.spec.cvlr.reference import SOLANA, SOROBAN, NamespacePattern, PathAlias + +#: Every crate the post-split Solana platform layer is spread across, as a target resolves them. +SPLIT_CRATES = ( + "solana-account-info", + "solana-pubkey", + "solana-program-error", + "solana-program-pack", + "solana-rent", + "solana-clock", + "solana-sysvar", + "solana-hash", + "solana-sdk-ids", + "solana-cpi", + "solana-instruction", +) + + +def _workspace(*resolved: str) -> Workspace: + """A ``Workspace`` that resolves exactly ``resolved``, and nothing else. + + Only the resolved-package list matters here: the dialect reads which crates exist and nothing + about the files on disk.""" + packages = tuple( + CratePackage( + name=name, + version="2.3.0", + manifest_path=Path("/nonexistent") / name / "Cargo.toml", + lib=None, + features=(), + source=RegistrySource("registry+https://github.com/rust-lang/crates.io-index"), + ) + for name in resolved + ) + return Workspace( + root=Path("/nonexistent"), + target_directory=Path("/nonexistent/target"), + members=(), + packages=packages, + ) + + +@pytest.fixture +def split() -> PathDialect: + """The dialect a post-split target gets.""" + return dialect_for(_workspace("solana-program", *SPLIT_CRATES), SOLANA) + + +@pytest.fixture +def monolithic() -> PathDialect: + """The dialect a 1.18 target gets, where the canonical paths are already the right ones.""" + return dialect_for(_workspace("solana-program"), SOLANA) + + +# --------------------------------------------------------------------------------------------- +# rewriting + + +@pytest.mark.parametrize( + ("canonical", "expected"), + [ + ( + "^solana_program::account_info::AccountInfo::lamports$", + "^solana_account_info::AccountInfo::lamports$", + ), + ( + "^solana_program::pubkey::Pubkey::find_program_address$", + "^solana_pubkey::Pubkey::find_program_address$", + ), + ( + "^>::from$", + "^>::from$", + ), + ("^solana_program::system_program::id$", "^solana_sdk_ids::system_program::id$"), + ("^solana_program::incinerator::check_id$", "^solana_sdk_ids::incinerator::check_id$"), + ("^solana_program::rent::Rent::minimum_balance$", "^solana_rent::Rent::minimum_balance$"), + # Three concepts in one pattern, which is why aliases are substrings rather than prefixes. + ( + "^solana_program::sysvar::rent::::get$", + "^solana_sysvar::rent::::get$", + ), + ], +) +def test_a_renamed_concept_is_spelled_as_the_defining_crate( + split: PathDialect, canonical: str, expected: str +) -> None: + assert split.spellings(canonical) == (expected,) + + +def test_a_symbol_that_survived_the_split_is_left_alone(split: PathDialect) -> None: + """``solana-program`` is a partial facade. ``invoke``, ``invoke_signed``, + ``set_return_data``, and ``get_stack_height`` are still real functions there, and a target's + symbol table lists them under the canonical spelling.""" + for pattern in ( + "^solana_program::program::invoke$", + "^solana_program::program::invoke_signed$", + "^solana_program::program::set_return_data$", + "^solana_program::instruction::get_stack_height$", + ): + assert split.spellings(pattern) == (pattern,) + + +def test_a_concept_on_both_sides_of_the_split_is_emitted_under_both_spellings( + split: PathDialect, +) -> None: + """``solana-program`` kept its own ``invoke_signed_unchecked``. The one on the call path is + ``solana-cpi``'s. A summary of only one of them leaves the other fully analyzed.""" + assert split.spellings("^solana_program::program::invoke_signed_unchecked$") == ( + "^solana_program::program::invoke_signed_unchecked$", + "^solana_cpi::invoke_signed_unchecked$", + ) + + +def test_a_symbol_level_alias_beats_the_module_it_sits_inside() -> None: + """Longest canonical wins. The module gets one answer, and the symbol that disagrees with it + gets another. Shortest-first would apply the module's answer and leave the specific alias + with nothing to match.""" + dialect = PathDialect( + ( + PathAlias("solana_program::program", ("wholesale",)), + PathAlias("solana_program::program::invoke_signed_unchecked", ("just_this_one",)), + ) + ) + assert dialect.spellings("^solana_program::program::invoke_signed_unchecked$") == ( + "^just_this_one$", + ) + assert dialect.spellings("^solana_program::program::invoke$") == ("^wholesale::invoke$",) + + +# --------------------------------------------------------------------------------------------- +# the blanket + + +def test_the_namespace_blanket_widens_to_the_whole_family(split: PathDialect) -> None: + """``^solana_program::.*$`` sets the never-inline default for the platform layer. On a + post-split target it matches almost nothing that moved out. The widened form has to cover + the split crates and the monolith that remains.""" + import re + + (widened,) = split.spellings("^solana_program::.*$") + for symbol in ( + "solana_account_info::AccountInfo::lamports", + "solana_pubkey::Pubkey::find_program_address", + "solana_cpi::invoke_signed_unchecked", + "solana_program::program::invoke_signed", + ): + assert re.search(widened, symbol), f"{widened} does not cover {symbol}" + + +def test_the_blanket_is_widened_even_on_a_target_that_predates_the_split( + monolithic: PathDialect, +) -> None: + """Unlike a :class:`PathAlias`, the widened blanket is a superset of what it replaces, so it + is correct on either generation and needs no version check. It is a pattern over crate + names, not a list of crates.""" + import re + + (widened,) = monolithic.spellings("^solana_program::.*$") + assert re.search(widened, "solana_program::program::invoke_signed") + + +def test_a_path_that_merely_starts_with_the_split_crate_is_not_widened( + split: PathDialect, +) -> None: + """``^solana_program::instruction::get_stack_height$`` names one function; widening it would + point a directive at symbols that do not exist. The literal ``.*`` is what tells the two + apart.""" + pattern = "^solana_program::instruction::get_stack_height$" + assert split.spellings(pattern) == (pattern,) + + +# --------------------------------------------------------------------------------------------- +# what a target that predates the split gets + + +def test_a_target_without_the_split_crates_keeps_the_canonical_spelling( + monolithic: PathDialect, +) -> None: + """An alias names a crate; if the target does not resolve it, the alias is not merely useless + but wrong — on 1.18 the canonical path is the real one. Dropping unresolvable spellings is what + lets the aliases be declared unconditionally against the newest generation.""" + for pattern in ( + "^solana_program::account_info::AccountInfo::lamports$", + "^solana_program::pubkey::Pubkey::find_program_address$", + "^solana_program::rent::Rent::minimum_balance$", + ): + assert monolithic.spellings(pattern) == (pattern,) + + +def test_a_chain_with_no_split_gets_a_dialect_that_changes_nothing() -> None: + dialect = dialect_for(_workspace("soroban-sdk"), SOROBAN) + assert dialect.aliases == () + assert dialect.spellings("^soroban_sdk::Env::storage$") == ("^soroban_sdk::Env::storage$",) + + +# --------------------------------------------------------------------------------------------- +# rendering a whole file + + +def test_rendering_preserves_comments_blank_lines_and_attributes(split: PathDialect) -> None: + source = ( + "; a comment\n" + "\n" + "#[inline(never)] ^core::.*$\n" + "#[inline] ^solana_program::account_info::AccountInfo::lamports$\n" + ) + assert split.render(source) == ( + "; a comment\n" + "\n" + "#[inline(never)] ^core::.*$\n" + "#[inline] ^solana_account_info::AccountInfo::lamports$\n" + ) + + +def test_a_fanned_out_summary_carries_its_whole_annotation_block(split: PathDialect) -> None: + """A points-to summary's ``#[type(...)]`` lines *precede* its pattern, so a second spelling that + did not repeat them would be a pattern with no summary attached — silently no longer a + summary.""" + source = ( + ";; a summary\n" + "#[type((*i32)(r1+0):num)]\n" + "^solana_program::program::invoke_signed_unchecked$\n" + ) + assert split.render(source) == ( + ";; a summary\n" + "#[type((*i32)(r1+0):num)]\n" + "^solana_program::program::invoke_signed_unchecked$\n" + "\n" + "#[type((*i32)(r1+0):num)]\n" + "^solana_cpi::invoke_signed_unchecked$\n" + ) + + +def test_rendering_twice_is_not_claimed_and_is_not_reachable(split: PathDialect) -> None: + """Rendering rendered output is not the identity. The alias for a symbol that exists on both + sides of the split lists the canonical spelling as one of its own replacements, so a second + pass fans that copy out again. + + Callers render from the starting layer. :func:`starting_env` re-reads ``envs/`` on each + call. This checks that a second pass would duplicate the line, so a caller that starts + feeding rendered text back in fails here. + """ + summaries = starting_env("cvlr_summaries_core.txt", split) + assert summaries.count("^solana_cpi::invoke_signed_unchecked$") == 1 + assert split.render(summaries).count("^solana_cpi::invoke_signed_unchecked$") == 2 + + +def test_recomposing_a_composite_is_stable(split: PathDialect) -> None: + """The composite is built from the starting layers every time, so composing twice gives the + same file.""" + once = compose_env(INLINING, dialect=split) + assert compose_env(INLINING, dialect=split) == once + + +def test_the_starting_files_are_returned_verbatim_without_a_dialect() -> None: + """`starting_env` answers "what is stored", so without a dialect it changes nothing.""" + for name in STARTING_ENVS: + assert starting_env(name) == (ENV_DIR / name).read_text() + + +def test_an_empty_dialect_is_the_identity() -> None: + for name in STARTING_ENVS: + assert PathDialect().render((ENV_DIR / name).read_text()) == (ENV_DIR / name).read_text() + + +# --------------------------------------------------------------------------------------------- +# keeping the aliases honest as the starting layers change + + +def test_every_declared_alias_still_names_something_in_the_starting_files() -> None: + """An alias is written against a starting layer. After that layer changes, one whose canonical + path no longer appears anywhere is dead weight that reads like coverage — and the failure mode it is + supposed to prevent is itself silent, so nothing else would notice.""" + starting = "\n".join((ENV_DIR / name).read_text() for name in STARTING_ENVS) + for alias in SOLANA.platform.path_aliases: + canonical = alias.canonical + assert canonical in starting, ( + f"{canonical} is aliased but appears in none of the starting tuning files; either " + f"the directive was removed or the alias was written against a stale file" + ) + + +def test_the_namespace_blanket_is_declared_for_a_directive_that_exists() -> None: + """Specifically the blanket, because it is the one whose canonical spelling contains a regex + fragment: rewording ``^solana_program::.*$`` to anything else leaves it matching + nothing, and the platform layer loses its default with no other symptom.""" + blankets = [ + a for a in SOLANA.platform.path_aliases if isinstance(a, NamespacePattern) + ] + assert blankets, "the platform layer's never-inline default is no longer widened" + core = (ENV_DIR / "cvlr_inlining_core.txt").read_text() + for blanket in blankets: + assert f"#[inline(never)] ^{blanket.canonical}$" in core + + +# --------------------------------------------------------------------------------------------- +# pinned against a real binary + + +#: Demangled symbols from a real Anchor program built for SBF — the evidence the alias table was +#: derived from. Checked in because it is the only thing that can catch an alias being *wrong*: every +#: other test here can only catch one being stale, and a wrong alias is just as silent. +SYMBOLS_FIXTURE = Path(__file__).parent / "data" / "vault_sbf_symbols.txt" + + +def _measured_symbols() -> tuple[str, ...]: + return tuple( + line.strip() + for line in SYMBOLS_FIXTURE.read_text().splitlines() + if line.strip() and not line.startswith("#") + ) + + +def test_every_alias_rewrites_to_a_path_the_binary_actually_defines(split: PathDialect) -> None: + """The alias table was read off this symbol table. ``solana-program`` is a partial facade: + some symbols moved and some did not, so an alias is per symbol. + + An alias is skipped when the fixture has no symbol under either spelling. The program does + not exercise that concept. Those are checked by the starting-file test above. + """ + symbols = _measured_symbols() + unexercised: list[str] = [] + for alias in SOLANA.platform.path_aliases: + if isinstance(alias, NamespacePattern): + continue + spellings = (alias.canonical, *alias.actual) + if not any(sp in s for s in symbols for sp in spellings): + unexercised.append(alias.canonical) + continue + assert any(a in s for s in symbols for a in alias.actual), ( + f"{alias.canonical} is exercised by the binary but none of its aliases " + f"{alias.actual} names a path it defines — the alias names the wrong crate" + ) + # Stated rather than asserted away: these are the concepts a lamports vault does not touch, and + # the list changing is a signal about the fixture, not a failure. + assert unexercised == [ + "solana_program::program_pack", + "solana_program::clock", + "solana_program::hash", + "solana_program::system_program", + "solana_program::incinerator", + ] + + +def test_the_dialect_measurably_restores_coverage_and_costs_none(split: PathDialect) -> None: + """Two counts against a real binary, because each misses what the other catches. + + Directives that match something: the Anchor error conversion is already inside + ``^.*anchor_lang.*$``, so changing its ``#[inline]`` changes how that symbol is treated + without changing whether anything reaches it. Symbols reached: a rewrite can double a + directive and address no more of the binary, or revive directives while dropping a symbol. + Only the symbol set shows a dropped symbol. + """ + import re + + symbols = _measured_symbols() + + def stats(text: str) -> tuple[int, set[str]]: + live, reached = 0, set() + for line in text.splitlines(): + s = line.strip() + if not s or s.startswith(";") or s.startswith("#[type("): + continue + pattern = re.sub(r"^#\[inline(?:\(never\))?\]\s*", "", s).strip() + hits = {x for x in symbols if re.search(pattern, x)} + if hits: + live += 1 + reached |= hits + return live, reached + + for name, directives, coverage in ( + ("cvlr_inlining_core.txt", (4, 15), (6, 35)), + ("cvlr_inlining_anchor.txt", (6, 7), (26, 26)), + ("cvlr_summaries_core.txt", (2, 6), (2, 4)), + ): + (lb, cb), (la, ca) = stats(starting_env(name)), stats(starting_env(name, split)) + assert (lb, la) == directives, f"{name} directives: {lb} -> {la}" + assert (len(cb), len(ca)) == coverage, f"{name} symbols: {len(cb)} -> {len(ca)}" + assert cb <= ca, f"{name} lost coverage of {sorted(cb - ca)}" + + +def test_a_unit_layer_is_appended_after_the_starting_layers() -> None: + layer = "#[inline] ^prog::handler$\n" + composite = compose_env(INLINING, unit_layer=layer) + assert composite.startswith(compose_env(INLINING).rstrip("\n")) + assert composite.endswith(layer) + + +# --------------------------------------------------------------------------------------------- +# ProgramError::from is inlined + + +def test_program_error_from_is_inlined_in_the_composite() -> None: + """Left opaque with no summary, ``ProgramError::from`` havocs the ``Result`` discriminant a + handler returns, and ``res.is_err()`` cannot be proved. + """ + composite = compose_env(INLINING) + from_u64 = [ln for ln in composite.splitlines() if "From>::from$" in ln and ln.startswith("#[")] + assert from_u64 == [ + "#[inline] ^>::from$" + ] + + +def test_program_error_from_is_inlined_under_the_dialect(split: PathDialect) -> None: + """It has to hold in the spelling that matches. The starting layer names + ``solana_program::program_error::``, which matches nothing on a post-split target. The rewrite + to ``solana_program_error::`` is what makes the directive apply, so an ``inline(never)`` there + would take effect.""" + composite = compose_env(INLINING, dialect=split) + assert ( + "#[inline] ^>::from$" + in composite + ) + assert "#[inline(never)] ^ Workspace: + return Workspace( + root=root, target_directory=root / "target", members=(), packages=resolved + ) + + +def _package(name: str, version: str, source: PackageSource | None = REGISTRY) -> CratePackage: + return CratePackage( + name=name, + version=version, + manifest_path=Path("/nonexistent") / f"{name}-{version}" / "Cargo.toml", + lib=None, + features=(), + source=source, + ) + + +_ROOT = '[workspace]\nmembers = ["."]\n' + + +def _planned(plan: ForkPlan | ForkRefused) -> ForkPlan: + assert isinstance(plan, ForkPlan), plan + return plan + + +def _refused(plan: ForkPlan | ForkRefused) -> ForkRefused: + assert isinstance(plan, ForkRefused), plan + return plan + + +def _added(plan: ForkPlan | ForkRefused) -> str: + """The workspace manifest ``_ROOT`` once ``plan``'s overrides are added to it.""" + plan = _planned(plan) + manifest = ManifestEditor(_ROOT) + for _, table in patch_tables(plan): + manifest.apply(table, note="added by AutoProver") + return manifest.text() + + +# --------------------------------------------------------------------------------------------- +# what it writes + + +def test_a_covered_anchor_version_is_pointed_at_its_branch(tmp_path): + plan = _planned( + plan_overrides(_workspace(tmp_path, _package("anchor-lang", "0.31.1")), SOLANA.forks) + ) + (override,) = plan.overrides + assert override.branch == "certora-v0.31.1" + assert override.repo == "https://github.com/Certora/anchor.git" + + +def test_the_manifest_addition_redirects_the_graph_at_the_fork(tmp_path): + addition = _added( + plan_overrides(_workspace(tmp_path, _package("anchor-lang", "0.31.1")), SOLANA.forks) + ) + assert "[patch.crates-io.anchor-lang]" in addition + assert 'git = "https://github.com/Certora/anchor.git"' in addition + assert 'branch = "certora-v0.31.1"' in addition + + +def test_the_manifest_says_these_are_not_the_deployed_dependencies(tmp_path): + """A property proved against a fork is a property of the fork. The patch section says so, + next to the dependency it replaces.""" + addition = _added( + plan_overrides(_workspace(tmp_path, _package("anchor-lang", "0.31.1")), SOLANA.forks) + ) + assert "NOT the deployed program's" in addition + assert "Certora fork of Anchor" in addition + + +def test_a_branch_is_named_rather_than_a_commit_pinned(tmp_path): + """The lockfile records the commit, so the build stays reproducible without editing this + manifest every time the fork moves.""" + addition = _added( + plan_overrides(_workspace(tmp_path, _package("anchor-lang", "0.31.1")), SOLANA.forks) + ) + assert "rev =" not in addition + + +@pytest.mark.parametrize("version", list(ANCHOR_FORK.branches)) +def test_every_declared_version_maps_to_a_branch(tmp_path, version): + plan = _planned( + plan_overrides(_workspace(tmp_path, _package("anchor-lang", version)), SOLANA.forks) + ) + assert plan.overrides and plan.overrides[0].branch == f"certora-v{version}" + + +# --------------------------------------------------------------------------------------------- +# what it refuses, and what it leaves alone + + +def test_an_uncovered_version_blocks_rather_than_leaving_the_boxing_in(tmp_path): + """The fork covers 0.30.1 and not 0.30.0, which is why versions are listed. A derived name + would send cargo after a branch that does not exist, and the error would be about git.""" + refused = _refused( + plan_overrides(_workspace(tmp_path, _package("anchor-lang", "0.30.0")), SOLANA.forks) + ) + (blocked,) = refused.blocked + assert "0.30.0" in blocked.problem + assert "0.30.1" in blocked.resolution + + +@pytest.mark.parametrize("fork", SOLANA.forks, ids=lambda f: f.crates[0]) +def test_an_uncovered_version_names_the_releases_that_fork_covers(tmp_path, fork): + refused = _refused( + plan_overrides(_workspace(tmp_path, _package(fork.crates[0], "0.0.1")), SOLANA.forks) + ) + (blocked,) = refused.blocked + assert fork.covered() in blocked.resolution + for other in SOLANA.forks: + if other is not fork: + assert other.covered() not in blocked.resolution + + +def test_a_project_that_already_sources_anchor_itself_is_left_alone(tmp_path): + """A path dependency means the project already decided where Anchor comes from. Overriding + it would replace that choice.""" + plan = _planned( + plan_overrides( + _workspace(tmp_path, _package("anchor-lang", "0.31.1", source=None)), SOLANA.forks + ) + ) + assert plan.overrides == () + assert [a.crate for a in plan.already] == ["anchor-lang"] + assert not plan.already[0].points_at_fork + + +def test_a_project_already_patched_to_the_fork_is_recognized_as_such(tmp_path): + """A project already on the fork is recognized from the resolved graph. ``cargo metadata`` + reports the patch as a git source, not as the ``[patch.crates-io.]`` header this + module writes. Projects write ``anchor-lang = { git = … }`` under one shared header. Searching + for either spelling misses the other, and a second entry for a key TOML already has is a + manifest cargo refuses.""" + patched = _package( + "anchor-lang", + "0.31.1", + source=GitSource.parse( + "git+https://github.com/Certora/anchor.git?branch=certora-v0.31.1#3ebe7595" + ), + ) + plan = _planned(plan_overrides(_workspace(tmp_path, patched), SOLANA.forks)) + assert plan.overrides == () + (already,) = plan.already + assert already.points_at_fork + assert "nothing to do" in already.describe() + + +def test_a_project_sourcing_anchor_from_some_other_fork_is_left_alone_and_said_so(tmp_path): + """The two cases read identically from the outside and only one of them is fine. This module + will not override somebody's choice, but a reader of a [3006] failure needs to know it was + made.""" + other = _package( + "anchor-lang", + "0.31.1", + source=GitSource.parse("git+https://github.com/someone/anchor.git?branch=main"), + ) + plan = _planned(plan_overrides(_workspace(tmp_path, other), SOLANA.forks)) + (already,) = plan.already + assert not already.points_at_fork + assert "someone/anchor" in already.describe() + assert "will not analyze" in already.describe() + + +def test_a_crate_resolved_twice_is_blocked_rather_than_half_redirected(tmp_path): + """One ``[patch.crates-io]`` entry replaces one semver-compatible release. The other copy + would stay upstream and keep [3006] in the build.""" + refused = _refused( + plan_overrides( + _workspace( + tmp_path, _package("anchor-lang", "0.29.0"), _package("anchor-lang", "0.31.1") + ), + SOLANA.forks, + ) + ) + (blocked,) = [b for b in refused.blocked if b.crate == "anchor-lang"] + assert "0.29.0" in blocked.problem and "0.31.1" in blocked.problem + + +def test_a_target_that_is_not_an_anchor_program_needs_nothing(tmp_path): + plan = _planned( + plan_overrides(_workspace(tmp_path, _package("solana-program", "2.3.0")), SOLANA.forks) + ) + assert not plan + assert _added(plan) == _ROOT + # Reported rather than dropped: "Anchor was not replaced" is what a reader of a [3006] failure + # needs to know, and silence looks the same as success. + assert set(plan.inapplicable) == {"anchor-lang", "anchor-spl", "fixed"} + + +# --------------------------------------------------------------------------------------------- +# keeping the declaration honest + + +def test_the_branch_list_matches_what_the_fork_publishes(): + """Read from ``Certora/anchor`` on 2026-09-01. The fork also has ``-pad-error`` and + ``-reduce-error`` branches of 0.29.0. Those are experiments and are not in this list.""" + versions = list(ANCHOR_FORK.branches) + assert versions == sorted(versions), "keep the list ordered so a gap is visible" + assert len(set(versions)) == len(versions) + for version, branch in ANCHOR_FORK.branches.items(): + assert branch == f"certora-v{version}" + # The gap that motivates listing rather than deriving. + assert "0.30.0" not in versions + assert "0.30.1" in versions + + +def test_every_override_says_why_it_exists_and_covers_at_least_one_version(): + for fork in SOLANA.forks: + assert fork.crates and fork.branches + assert len(fork.why) > 80, ( + f"{fork.crates}'s reason ends up verbatim in somebody's Cargo.toml, and it is the only " + f"explanation they will get" + ) + + +def test_the_anchor_fork_covers_both_crates_it_publishes(tmp_path): + """Patching only ``anchor-lang`` clears [3006], because the boxing is in + ``anchor_lang::error``, and leaves ``anchor-spl`` upstream. Its ``TokenAccount`` and ``Mint`` + are newtypes with a private field. The fork adds ``new_unchecked`` for those, so a harness + can build a token account. Both crates are redirected to the same branch.""" + assert set(ANCHOR_FORK.crates) == {"anchor-lang", "anchor-spl"} + plan = _planned( + plan_overrides( + _workspace( + tmp_path, _package("anchor-lang", "0.31.1"), _package("anchor-spl", "0.31.1") + ), + SOLANA.forks, + ) + ) + assert {o.crate: o.branch for o in plan.overrides} == { + "anchor-lang": "certora-v0.31.1", + "anchor-spl": "certora-v0.31.1", + } + + +def test_one_forks_two_crates_share_one_reason_in_the_manifest(tmp_path): + """Two crates from one fork share one explanation. Repeating it under each reads like two + unrelated edits.""" + addition = _added( + plan_overrides( + _workspace( + tmp_path, _package("anchor-lang", "0.31.1"), _package("anchor-spl", "0.31.1") + ), + SOLANA.forks, + ) + ) + assert addition.count("Certora fork of Anchor") == 1 + assert "anchor-lang 0.31.1 -> certora-v0.31.1" in addition + assert "anchor-spl 0.31.1 -> certora-v0.31.1" in addition + + +def test_the_fixed_fork_is_planned_from_the_version_the_corpus_pins(tmp_path): + """The known release is ``fixed`` 1.23.1 on ``certora-v1.23.1``. One branch is listed because + that is the release the fork is known to cover.""" + plan = _planned(plan_overrides(_workspace(tmp_path, _package("fixed", "1.23.1")), SOLANA.forks)) + (override,) = plan.overrides + assert override.repo == "https://github.com/Certora/fixed.git" + assert override.branch == "certora-v1.23.1" + + +# --------------------------------------------------------------------------------------------- +# reading a patch table somebody else wrote + + +def test_the_inline_spelling_every_real_project_uses_is_recognized(): + """Projects write one ``[patch.crates-io]`` header with an inline table per crate. This + module writes a ``[patch.crates-io.]`` sub-table. They are the same TOML and share no + text, so a search for either misses the other.""" + inline = """ +[patch.crates-io] +anchor-lang = { git = "https://github.com/Certora/anchor.git", branch = "certora-v0.29.0" } +anchor-spl = { git = "https://github.com/Certora/anchor.git", branch = "certora-v0.29.0" } +spl-token-2022 = { git = "https://github.com/example/solana-program-library.git" } +""" + assert already_patched(parse_manifest(inline)) == frozenset( + {"anchor-lang", "anchor-spl", "spl-token-2022"} + ) + + +def test_the_subtable_spelling_this_module_writes_is_recognized_too(): + subtables = """ +[patch.crates-io.anchor-lang] +git = "https://github.com/Certora/anchor.git" +branch = "certora-v0.31.1" +""" + assert already_patched(parse_manifest(subtables)) == frozenset({"anchor-lang"}) + + +def test_a_manifest_with_no_patch_table_redirects_nothing(): + assert already_patched(parse_manifest('[workspace]\nmembers = ["."]\n')) == frozenset() + assert already_patched(parse_manifest("[patch]\n")) == frozenset() + + +def test_a_crate_the_table_already_names_is_left_alone(tmp_path): + """The graph is what cargo computed, but a snapshot taken before the patch table was applied + still shows the registry. A second entry for a key TOML already has is a manifest cargo + refuses.""" + plan = _planned( + plan_overrides( + _workspace(tmp_path, _package("anchor-lang", "0.31.1")), + SOLANA.forks, + already_redirected=frozenset({"anchor-lang"}), + ) + ) + assert plan.overrides == () + (already,) = plan.already + assert "already redirected" in already.describe() diff --git a/tests/test_cvlr_plumbing.py b/tests/test_cvlr_plumbing.py new file mode 100644 index 00000000..6359f9fc --- /dev/null +++ b/tests/test_cvlr_plumbing.py @@ -0,0 +1,432 @@ +"""CVLR metadata and the prover conf, with no toolchain, network, or LLM. + +Nothing here shells out to cargo or submits a job. What is checked is the parse of +``cargo metadata`` and ``Cargo.toml``, the conf a tunable conf renders to, and the keys one +submission adds. +""" + +import json +import subprocess +from dataclasses import replace +from pathlib import Path + +import pytest + +from composer.cargo.manifest import Dependency, MalformedManifest, parse_manifest +from composer.cargo import metadata +from composer.cargo.metadata import ( + CargoFailed, + CargoMetadataJson, + CargoTimedOut, + CratePackage, + GitBranch, + GitRev, + GitSource, + GitTag, + RegistrySource, + UnreadableMetadata, + Workspace, + parse_metadata, +) +from composer.prover import conf as prover_conf +from composer.spec.cvlr import conf as cvlr_conf +from composer.spec.cvlr.crates import Absent, CvlrSources +from composer.spec.cvlr.reference import SOLANA + + +# -------------------------------------------------------------------------------------------- +# cargo metadata +# -------------------------------------------------------------------------------------------- + +#: A two-member workspace with one published dependency, in cargo's own shape. Hand-written rather +#: than recorded so that every field this codebase reads is visible in the test that reads it. +_METADATA = { + "workspace_root": "/w", + "target_directory": "/w/target", + "workspace_members": ["path+file:///w/programs/lend#0.1.0", "path+file:///w#0.1.0"], + "packages": [ + { + "id": "path+file:///w/programs/lend#0.1.0", + "name": "example-lending", + "version": "0.1.0", + "manifest_path": "/w/programs/lend/Cargo.toml", + "source": None, + "features": {"certora": [], "no-entrypoint": []}, + "targets": [ + { + "name": "example_lending", + "kind": ["cdylib"], + "crate_types": ["cdylib"], + "src_path": "/w/programs/lending/src/lib.rs", + }, + { + "name": "bench", + "kind": ["bench"], + "crate_types": ["bin"], + "src_path": "/w/programs/lending/benches/b.rs", + }, + ], + }, + { + "id": "path+file:///w#0.1.0", + "name": "workspace-root-crate", + "version": "0.1.0", + "manifest_path": "/w/Cargo.toml", + "source": None, + "features": {}, + "targets": [{"name": "root", "kind": ["lib"], "crate_types": ["lib"], "src_path": "/w/src/lib.rs"}], + }, + { + "id": "registry+https://github.com/rust-lang/crates.io-index#cvlr@0.6.1", + "name": "cvlr", + "version": "0.6.1", + "manifest_path": "/home/u/.cargo/registry/src/idx/cvlr-0.6.1/Cargo.toml", + "source": "registry+https://github.com/rust-lang/crates.io-index", + "features": {}, + "targets": [{"name": "cvlr", "kind": ["lib"], "crate_types": ["lib"], "src_path": "/reg/cvlr/src/lib.rs"}], + }, + { + "id": "registry+https://github.com/rust-lang/crates.io-index#cvlr-log@0.6.1", + "name": "cvlr-log", + "version": "0.6.1", + "manifest_path": "/home/u/.cargo/registry/src/idx/cvlr-log-0.6.1/Cargo.toml", + "source": "registry+https://github.com/rust-lang/crates.io-index", + "features": {}, + "targets": [{"name": "cvlr_log", "kind": ["lib"], "crate_types": ["lib"], "src_path": "/reg/cvlr-log/src/lib.rs"}], + }, + ], +} + + +def _workspace(payload: dict) -> Workspace: + return parse_metadata(CargoMetadataJson.model_validate(payload)) + + +def test_the_lib_target_is_the_one_an_artifact_is_named_after(): + """A package's bench and bin targets are not what a verification build produces.""" + lend = _workspace(_METADATA).member("example-lending") + assert lend is not None + assert lend.lib is not None + assert lend.lib.name == "example_lending" + assert lend.lib.artifact_stem == "example_lending" + + +def test_a_dash_in_a_lib_name_becomes_an_underscore_in_the_artifact(): + """Cargo names the file after the target with ``-`` normalized, and the ``.so`` path in the + build manifest follows that, not the package name.""" + payload = json.loads(json.dumps(_METADATA)) + payload["packages"][0]["targets"][0]["name"] = "example-lending" + lend = _workspace(payload).member("example-lending") + assert lend is not None and lend.lib is not None + assert lend.lib.artifact_stem == "example_lending" + + +def test_an_older_cargo_that_reports_only_kind_still_names_the_lib_target(): + payload = json.loads(json.dumps(_METADATA)) + del payload["packages"][0]["targets"][0]["crate_types"] + payload["packages"][0]["targets"][0]["kind"] = ["cdylib"] + lend = _workspace(payload).member("example-lending") + assert lend is not None and lend.lib is not None + assert lend.lib.builds_shared_object + + +def test_a_git_source_is_split_into_repository_reference_and_commit(): + source = GitSource.parse( + "git+https://github.com/Certora/anchor.git?branch=certora-v0.31.1#3ebe7595" + ) + assert source.repository == "https://github.com/Certora/anchor.git" + assert source.reference == GitBranch("certora-v0.31.1") + assert source.commit == "3ebe7595" + + +@pytest.mark.parametrize( + ("query", "reference"), + [("?tag=v1", GitTag("v1")), ("?rev=abc", GitRev("abc")), ("", None)], + ids=["tag", "rev", "default-branch"], +) +def test_every_git_reference_cargo_spells_is_recognized(query, reference): + source = GitSource.parse(f"git+https://github.com/o/r{query}#deadbeef") + assert source.reference == reference + assert source.repository == "https://github.com/o/r" + + +def test_one_repository_is_recognized_across_its_spellings(): + source = GitSource.parse("git+ssh://git@github.com/Certora/Anchor#3ebe7595") + assert source.is_from("https://github.com/certora/anchor.git") + assert source.is_from("https://github.com/Certora/anchor/") + + +def test_a_repository_whose_name_extends_another_is_a_different_repository(): + source = GitSource.parse("git+https://github.com/Certora/anchor-extras.git#3ebe7595") + assert not source.is_from("https://github.com/Certora/anchor.git") + + +def test_the_owning_crate_is_the_deepest_one_containing_the_file(): + """A workspace whose root is itself a package contains every nested crate's files too, so the + shallow match is always available and always wrong.""" + workspace = _workspace(_METADATA) + owner = workspace.owning(Path("/w/programs/lend/src/lib.rs")) + assert owner is not None and owner.name == "example-lending" + + +def test_a_file_in_no_member_has_no_owning_crate(): + workspace = _workspace(_METADATA) + assert workspace.owning(Path("/elsewhere/src/lib.rs")) is None + + +def test_a_crate_family_is_recognized_by_name(): + """``cvlr`` does not declare its family anywhere; the helper crates come in as ordinary + dependencies, and an agent asking what a macro expands to needs all of them.""" + workspace = _workspace(_METADATA) + assert [c.name for c in workspace.family("cvlr")] == ["cvlr", "cvlr-log"] + + +def test_a_published_dependency_is_distinguished_from_a_workspace_member(): + workspace = _workspace(_METADATA) + (cvlr,) = workspace.resolved("cvlr") + (lend,) = workspace.resolved("example-lending") + assert not cvlr.is_local + assert lend.is_local + + +def test_every_copy_of_a_crate_the_graph_resolves_twice_is_reported(): + """A graph holds two releases of one crate when dependents require incompatible ones. A lookup + that returned the first would answer about whichever copy cargo happened to list first.""" + payload = json.loads(json.dumps(_METADATA)) + older = json.loads(json.dumps(payload["packages"][2])) + older.update(id=f"{older['source']}#cvlr@0.4.1", version="0.4.1") + payload["packages"].append(older) + assert [c.version for c in _workspace(payload).resolved("cvlr")] == ["0.6.1", "0.4.1"] + + +def _cargo_answers(monkeypatch, answer): + """``cargo metadata`` as a stub: ``answer`` is returned, or raised if it is an exception.""" + + def run(args, **_kwargs): + if isinstance(answer, BaseException): + raise answer + return answer + + monkeypatch.setattr(metadata.shutil, "which", lambda _name: "/usr/bin/cargo") + monkeypatch.setattr(metadata.subprocess, "run", run) + + +@pytest.mark.asyncio +async def test_a_failed_cargo_metadata_carries_cargos_explanation(monkeypatch): + stderr = ( + "error: failed to parse manifest at `/w/Cargo.toml`\n\nCaused by:\n TOML parse error\n" + ) + _cargo_answers(monkeypatch, subprocess.CompletedProcess([], 101, stdout="", stderr=stderr)) + failure = await Workspace.read(Path("/w")) + assert failure == CargoFailed(stderr) + assert failure.describe().startswith("error: failed to parse manifest") + + +@pytest.mark.asyncio +async def test_a_cargo_metadata_that_runs_out_of_time_says_so(monkeypatch): + _cargo_answers(monkeypatch, subprocess.TimeoutExpired(["cargo"], 7)) + assert await Workspace.read(Path("/w"), timeout_s=7) == CargoTimedOut(7) + + +@pytest.mark.asyncio +async def test_cargo_output_that_does_not_validate_is_a_failure_not_an_exception(monkeypatch): + _cargo_answers(monkeypatch, subprocess.CompletedProcess([], 0, stdout="{}", stderr="")) + failure = await Workspace.read(Path("/w")) + assert isinstance(failure, UnreadableMetadata) + assert "packages" in failure.describe() + + +# -------------------------------------------------------------------------------------------- +# Cargo.toml +# -------------------------------------------------------------------------------------------- + + +def test_a_bare_version_string_is_a_version_requirement(): + """``foo = "1.0"`` is cargo's shorthand for ``foo = { version = "1.0" }``; a reader that kept + the two apart would have to handle both at every use.""" + manifest = parse_manifest( + '[dependencies]\ncvlr = "=0.6.1"\nlocal = { path = "../local", version = "0.1" }\n' + ) + assert manifest.dependencies["cvlr"] == Dependency(version="=0.6.1") + assert manifest.dependencies["local"] == Dependency(path="../local", version="0.1") + + +def test_the_certora_metadata_table_is_read_as_present_or_absent(): + assert parse_manifest('[package]\nname = "p"\n').certora_metadata is None + assert parse_manifest("[workspace]\n").certora_metadata is None + other_tool = '[package]\nname = "p"\n\n[package.metadata.docs.rs]\nall-features = true\n' + assert parse_manifest(other_tool).certora_metadata is None + declared = '[package]\nname = "p"\n\n[package.metadata.certora]\nsources = ["src/**/*.rs"]\n' + assert parse_manifest(declared).certora_metadata is not None + + +def test_an_empty_workspace_table_still_makes_a_workspace_root(): + assert parse_manifest("[workspace]\n").workspace is not None + assert parse_manifest('[package]\nname = "p"\n').workspace is None + + +@pytest.mark.parametrize( + "text", + [ + "[dependencies\nnot toml", + '[features]\ncertora = "dep:cvlr"\n', + "[dependencies]\ncvlr = 6\n", + ], + ids=["unparseable", "feature-not-a-list", "dependency-not-a-spec"], +) +def test_a_manifest_cargo_would_refuse_is_malformed(text): + with pytest.raises(MalformedManifest): + parse_manifest(text) + + +# -------------------------------------------------------------------------------------------- +# CVLR source resolution +# -------------------------------------------------------------------------------------------- + + +def test_the_cvlr_source_roots_are_the_crate_directories_the_build_resolved(): + sources = CvlrSources.of(_workspace(_METADATA)) + assert [(c.name, c.version) for c in sources.crates] == [ + ("cvlr", "0.6.1"), + ("cvlr-log", "0.6.1"), + ] + assert sources.roots() == ( + Path("/home/u/.cargo/registry/src/idx/cvlr-0.6.1"), + Path("/home/u/.cargo/registry/src/idx/cvlr-log-0.6.1"), + ) + + +def test_two_copies_of_one_version_are_ordered_the_same_whatever_order_cargo_lists_them(): + """A registry release and a git checkout of it both resolve as ``cvlr 0.6.1``.""" + registry = CratePackage( + name="cvlr", + version="0.6.1", + manifest_path=Path("/home/u/.cargo/registry/src/idx/cvlr-0.6.1/Cargo.toml"), + lib=None, + features=(), + source=RegistrySource("registry+https://github.com/rust-lang/crates.io-index"), + ) + checkout = replace( + registry, + manifest_path=Path("/home/u/.cargo/git/checkouts/cvlr-1a2b/3c4d/cvlr/Cargo.toml"), + source=GitSource.parse("git+https://github.com/Certora/cvlr.git?branch=main#3c4d5e6f"), + ) + orders = [ + CvlrSources.of( + Workspace(root=Path("/p"), target_directory=Path("/p/target"), members=(), packages=p) + ).crates + for p in ((registry, checkout), (checkout, registry)) + ] + assert orders[0] == orders[1] + + +def test_a_project_on_the_reference_core_but_without_the_chain_crate_reports_that_gap(): + """Two different statements, and only one of them stops a run: an old ``cvlr-solana`` and no + ``cvlr-solana`` at all. They are separate types so a caller cannot conflate them.""" + sources = CvlrSources.of(_workspace(_METADATA)) + gaps = {g.crate: g for g in sources.gaps(SOLANA)} + assert "cvlr" not in gaps, "the fixture pins the reference core, so it is not a gap" + assert isinstance(gaps["cvlr-solana"], Absent) + assert "is not a dependency of this project" in gaps["cvlr-solana"].describe() + assert sources.mismatched(SOLANA) == (), "absence is not something to refuse over" + + +def test_an_older_cvlr_than_the_pin_is_a_mismatch_that_stops_the_run(): + payload = json.loads(json.dumps(_METADATA)) + payload["packages"][2]["version"] = "0.4.1" + sources = CvlrSources.of(_workspace(payload)) + mismatched = {g.crate: g for g in sources.mismatched(SOLANA)} + assert mismatched["cvlr"].resolved == "0.4.1" + assert mismatched["cvlr"].reference == "0.6.1" + + +def test_an_older_cvlr_beside_the_pinned_one_is_still_a_mismatch(): + payload = json.loads(json.dumps(_METADATA)) + older = json.loads(json.dumps(payload["packages"][2])) + older.update(id=f"{older['source']}#cvlr@0.4.1", version="0.4.1") + payload["packages"].append(older) + (mismatch,) = CvlrSources.of(_workspace(payload)).mismatched(SOLANA) + assert (mismatch.crate, mismatch.resolved) == ("cvlr", "0.4.1") + + +# -------------------------------------------------------------------------------------------- +# the conf +# -------------------------------------------------------------------------------------------- + + +def test_loops_are_bounded_soundly_and_the_bound_is_raised_instead(): + """``optimistic_loop`` assumes loops halt instead of proving it, so a violation that needs + more iterations is not found. Bound the inputs that set the trip count, or edit the loop, + before raising ``loop_iter``.""" + conf = cvlr_conf.tunable_conf(cvlr_conf.TunableConf()) + assert conf["optimistic_loop"] is False + assert conf["loop_iter"] == "2" + + +def test_the_base_enables_no_optimistic_solana_flags(): + """None of the ``-solanaOptimistic*`` flags. They are unsound, and they do not fix the [3308] + they were meant to.""" + flags = cvlr_conf.tunable_conf(cvlr_conf.TunableConf())["prover_args"] + assert not [f for f in flags if f.startswith("-solanaOptimistic")] + + +def test_every_conf_checks_vacuity(): + """With ``rule_sanity`` off, a [3308] inside the generated vacuity rule is reported as + verified. No setting turns it off.""" + for tunable in ( + cvlr_conf.TunableConf(), + cvlr_conf.TunableConf(loop_iter=5, optimistic_loop=True), + ): + assert cvlr_conf.tunable_conf(tunable)["rule_sanity"] == "basic" + + +def test_the_loop_bound_is_written_the_way_a_conf_spells_an_integer(): + assert cvlr_conf.tunable_conf(cvlr_conf.TunableConf(loop_iter=4))["loop_iter"] == "4" + + +def test_a_conf_change_invalidates_a_stamp_earned_before_it(): + """A verdict under one loop bound, or with loops assumed to finish, is not a verdict under + another.""" + default = cvlr_conf.conf_history(cvlr_conf.TunableConf()) + assert default != cvlr_conf.conf_history(cvlr_conf.TunableConf(loop_iter=3)) + assert default != cvlr_conf.conf_history(cvlr_conf.TunableConf(optimistic_loop=True)) + assert default == cvlr_conf.conf_history(cvlr_conf.TunableConf()) + + +# --------------------------------------------------------------------------------------------- +# One submission's keys + + +def _submission(**kwargs) -> dict: + return cvlr_conf.solana_conf( + cvlr_conf.TunableConf(), + cvlr_conf.RunOverlay(build_script=Path("/w/.certora_build/confined_build.py"), **kwargs), + ) + + +def test_the_run_names_the_build_script(): + assert _submission()["build_script"] == "/w/.certora_build/confined_build.py" + + +def test_the_message_is_reduced_to_what_the_prover_accepts(): + assert _submission(msg="Deposit & Balance")["msg"] == "Deposit Balance" + + +def test_selecting_rules_names_them(): + assert _submission(rules=prover_conf.SelectRules(("rule_vacuous",)))["rule"] == ["rule_vacuous"] + + +def test_inheriting_rules_checks_every_rule(): + assert "rule" not in _submission() + + +def test_the_env_files_are_left_for_the_build_manifest_to_supply(): + """``cargo certora-sbf`` reads them from ``[package.metadata.certora]``, and the prover + applies that only when the conf has none.""" + conf = _submission() + assert "solana_inlining" not in conf and "solana_summaries" not in conf + + +def test_a_units_summary_file_is_named_when_the_run_passes_one(): + conf = _submission(summaries=(Path("envs/cvlr_summaries_vault.txt"),)) + assert conf["solana_summaries"] == ["envs/cvlr_summaries_vault.txt"] diff --git a/tests/test_cvlr_preflight.py b/tests/test_cvlr_preflight.py new file mode 100644 index 00000000..531d2325 --- /dev/null +++ b/tests/test_cvlr_preflight.py @@ -0,0 +1,112 @@ +"""Resolving a real Cargo project with real cargo, from a bare workspace to one that compiles. + +The other preflight tests build a ``Workspace`` by hand and patch out ``Workspace.read``. That +pins what the planner decides. It cannot pin what cargo decides: + +* which member owns a source file, which is cargo's answer, not a prefix match; +* that the CVLR crates are visible only after the scaffold is applied and the graph is re-read + under the verification feature, from the package directory. A fake graph answers whatever it + was built to answer; +* that the result compiles. + +The workspace has two members with library targets. :func:`_pick_package` refuses that on its +own, so the selection has to come from cargo's view of who owns ``main_source``. A prefix match +fails here. + +Marked ``expensive``: it resolves and compiles a real dependency graph off the network. It skips, +naming what is missing, when cargo is absent. +""" + +import shutil +from pathlib import Path + +import pytest + +from composer.sandbox.config import SandboxConfig +from composer.spec.cvlr.preflight import gate_workspace, prepare_workspace, select_package +from composer.spec.cvlr.reference import SOLANA + +pytestmark = [pytest.mark.expensive, pytest.mark.asyncio] + +WORKSPACE_MANIFEST = """\ +[workspace] +members = ["programs/vault", "programs/other"] +resolver = "2" +""" + +MEMBER_MANIFEST = """\ +[package] +name = "{name}" +version = "0.1.0" +edition = "2021" + +[lib] +crate-type = ["cdylib", "lib"] + +[dependencies] +""" + +PROGRAM = """\ +pub fn deposit(amount: u64) -> u64 { + amount +} +""" + + +@pytest.fixture +def project(tmp_path: Path) -> Path: + if shutil.which("cargo") is None: + pytest.skip("cargo is not on PATH") + (tmp_path / "Cargo.toml").write_text(WORKSPACE_MANIFEST) + for name in ("vault", "other"): + source = tmp_path / "programs" / name / "src" + source.mkdir(parents=True) + (source.parent / "Cargo.toml").write_text(MEMBER_MANIFEST.format(name=name)) + (source / "lib.rs").write_text(PROGRAM) + return tmp_path + + +async def test_a_bare_cargo_workspace_becomes_one_that_compiles_with_a_harness_in(project): + """Select a package, scaffold it, and compile it, in the order a run does. + + The compile is the check that the feature wiring, the manifest edits, and the pinned crate + versions agree. Each of those can look right on its own. Only rustc reads all three. + """ + main_source = project / "programs" / "vault" / "src" / "lib.rs" + + selected = await select_package(project, None, main_source=main_source) + assert selected.name == "vault" + assert selected.package_dir == Path("programs/vault") + + pre = await prepare_workspace(selected.workspace_root, reference=SOLANA, package=selected.name) + assert pre.scaffold.blocked == (), pre.scaffold.blocked + assert pre.artifact_stem == "vault" + # Resolved from the scaffolded graph: before it, this project had no CVLR dependency at all. + assert {crate.name for crate in pre.sources.crates} >= {"cvlr", "cvlr-solana"} + assert (main_source.parent / "certora" / "specs" / "mod.rs").is_file() + + await gate_workspace(pre, sandbox=SandboxConfig(provider="none")) + + +async def test_pointing_it_at_a_project_it_already_scaffolded_replaces_only_the_edited_harness( + project, +): + """The harness files are AutoProver's. A second run puts an edited one back and changes + nothing else, so the manifests it already extended are not extended again.""" + main_source = project / "programs" / "vault" / "src" / "lib.rs" + selected = await select_package(project, None, main_source=main_source) + + first = await prepare_workspace( + selected.workspace_root, reference=SOLANA, package=selected.name + ) + assert first.applied != () + specs = main_source.parent / "certora" / "specs" / "mod.rs" + scaffolded = specs.read_text() + specs.write_text(f"{scaffolded}\n// an author's work\n") + + again = await prepare_workspace( + selected.workspace_root, reference=SOLANA, package=selected.name + ) + + assert again.applied == (specs.relative_to(selected.workspace_root),) + assert specs.read_text() == scaffolded diff --git a/tests/test_cvlr_reference.py b/tests/test_cvlr_reference.py new file mode 100644 index 00000000..096b019e --- /dev/null +++ b/tests/test_cvlr_reference.py @@ -0,0 +1,84 @@ +"""The CVLR reference set (``composer.spec.cvlr.reference``). + +Compiling a probe crate per chain is what checks that the versions resolve. That needs cargo and +a network, so it is not run here. These tests cover what a wrong edit can break without cargo +noticing: the chain names matching the pipeline's, exact pinning, and the platform generation +that travels with the chain crate. +""" + +import pytest + +from composer.spec.cvlr import reference as ref + + +def test_the_chains_are_exactly_the_pipelines_rust_chains(): + """The module repeats the chain names as plain strings so it does not import the pipeline. + This checks that the repetition still matches. EVM is excluded: CVLR is the Rust-side language.""" + from typing import get_args + + from composer.pipeline.ecosystem import ChainTag + + assert set(ref.REFERENCE_SET) == set(get_args(ChainTag)) - {"evm"} + + +def test_every_cvlr_crate_is_pinned_to_an_exact_release(): + # A range would let a resolver move the corpus's ground truth without an edit here, and the + # compile gate would then be testing something nobody chose. + for chain, r in ref.REFERENCE_SET.items(): + for crate in r.crates(): + assert crate.dependency_line().startswith(f'{crate.name} = "='), (chain, crate) + assert crate.version[0].isdigit(), (chain, crate) + + +def test_the_platform_is_a_line_not_a_release(): + # The platform generation is about the target. An exact pin would claim a patch level that + # was never compiled. + for chain, r in ref.REFERENCE_SET.items(): + assert r.platform.sdk_crates, chain + for crate in r.platform.sdk_crates: + assert crate.dependency_line() == f'{crate.name} = "{crate.line}"' + assert "=" not in crate.line + + +def test_the_dependency_block_carries_the_platform_too(): + # Without it a probe cannot name AccountInfo, so an entry that mentions one would fail the + # gate for a missing import rather than for anything about CVLR. + block = ref.SOLANA.cargo_dependencies() + assert 'cvlr = "=0.6.1"' in block + assert 'cvlr-solana = "=0.5.0"' in block + assert 'solana-program = "2.2"' in block + + +def test_the_solana_choice_records_the_platform_it_implies(): + # cvlr-solana 0.5.0 requires solana-program 2.2, and each Solana generation has its own + # AccountInfo. Changing the chain crate without changing this label pairs the wrong types. + assert ref.SOLANA.chain_crate == ref.CrateRelease("cvlr-solana", "0.5.0") + assert "2.x" in ref.SOLANA.platform.label + + +def test_the_spl_token_model_is_part_of_the_reference_set(): + # On crates.io at 0.5.0, the same version as the chain crate it was split from. Leaving it + # off the reference set would keep the scaffold from pinning it. + assert ref.CrateRelease("cvlr-spl-token", "0.5.0") in ref.SOLANA.specializations + assert ref.SOLANA.unpublished == () + + +def test_a_fresh_project_is_pinned_the_whole_reference_set(): + # The scaffold is what writes dependencies, and it does not add one later. A specialization + # left out of this list is a crate the project cannot name. + assert ref.SOLANA.scaffold_crates() == ref.SOLANA.crates() + assert {c.name for c in ref.SOLANA.scaffold_crates()} == { + "cvlr", "cvlr-solana", "cvlr-solana-stake", "cvlr-spl-token", + } + + +def test_an_unknown_chain_raises_and_names_the_ones_that_exist(): + with pytest.raises(ValueError, match="no CVLR reference set for chain 'evm'") as e: + ref.reference_for("evm") + assert "'solana'" in str(e.value) and "'soroban'" in str(e.value) + + +def test_both_chains_share_one_core_release(): + # The core line is chain-independent; two chains drifting apart on it would mean one of them + # is being compiled against a cvlr nobody chose. + assert ref.SOLANA.core == ref.SOROBAN.core diff --git a/tests/test_cvlr_scaffold.py b/tests/test_cvlr_scaffold.py new file mode 100644 index 00000000..e8c335bb --- /dev/null +++ b/tests/test_cvlr_scaffold.py @@ -0,0 +1,852 @@ +"""What the scaffold writes, what it refuses, and what it leaves alone. + +Three failures are quiet. A second run that appends to ``Cargo.toml`` again leaves a manifest +cargo will not parse, and a scaffold gets re-run when nobody is sure it ran. A text edit of a +parsed manifest has to stay valid TOML, because reserializing would rewrite the project's +comments, so every case that touches a manifest re-parses it. A blocked plan has to apply +nothing: a half-scaffolded project makes the next build failure have two causes. + +No cargo and no network. The workspace objects are built in the test. +""" + +import tomllib +from dataclasses import replace +from pathlib import Path + +import pytest + +from composer.cargo.manifest import AddEntries, AddTable, ManifestAddition +from composer.cargo.metadata import ( + CargoFailed, + CargoMetadataJson, + CratePackage, + LibTarget, + MetadataFailure, + RegistrySource, + Workspace, + parse_metadata, +) +from composer.spec.cvlr import preflight, scaffold, tuning +from composer.spec.cvlr.scaffold import ( + HARNESS_DIR, + EditManifest, + ScaffoldBlocked, + Write, + apply, + plan_scaffold, +) +from composer.spec.cvlr.tuning import ENV_FAMILIES, INLINING, SUMMARIES +from composer.spec.cvlr.reference import SOLANA, SOROBAN + +PROGRAM = """\ +use solana_program::account_info::AccountInfo; + +pub fn process(_accounts: &[AccountInfo]) {} +""" + + +def _project( + root: Path, + *, + manifest: str, + workspace_manifest: str | None = None, + package_dir: str = "", + crate_types: tuple[str, ...] = ("cdylib",), + platform: str | None = "2.2.1", + platform_crate: str = "solana-program", + cvlr_resolved: dict[str, str] | None = None, +) -> tuple[Workspace, CratePackage]: + """A project on disk plus the ``Workspace`` cargo would report for it. + + ``platform`` and ``cvlr_resolved`` stand in for the resolved graph, which is what the platform + gate and the version-gap report read; the manifests on disk are what the planner parses. + + ``platform_crate`` is a parameter because which crate carries ``AccountInfo`` is itself a fact + about the generation: Solana's v3 split moved it out of ``solana-program`` and stopped + publishing that crate, so a target on the newest line resolves a platform crate the older line + has never heard of. + """ + package_root = root / package_dir if package_dir else root + # Write-if-absent, so calling this a second time reports the project as the scaffold left it + # rather than as it started. A helper that clobbered `lib.rs` would make the idempotence test + # pass or fail for a reason that has nothing to do with the scaffold. + (package_root / "src").mkdir(parents=True, exist_ok=True) + for path, contents in ( + (package_root / "Cargo.toml", manifest), + (package_root / "src" / "lib.rs", PROGRAM), + *(((root / "Cargo.toml", workspace_manifest),) if workspace_manifest is not None else ()), + ): + if not path.exists(): + path.write_text(contents) + + package = CratePackage( + name="prog", + version="0.1.0", + manifest_path=package_root / "Cargo.toml", + lib=LibTarget( + name="prog", src_path=package_root / "src" / "lib.rs", crate_types=crate_types + ), + features=("no-entrypoint",) if "no-entrypoint" in manifest else (), + source=None, + ) + resolved = [package] + if platform is not None: + resolved.append( + CratePackage( + name=platform_crate, + version=platform, + manifest_path=root / "vendor" / platform_crate / "Cargo.toml", + lib=None, + features=(), + source=RegistrySource("registry+https://github.com/rust-lang/crates.io-index"), + ) + ) + for name, version in (cvlr_resolved or {}).items(): + resolved.append( + CratePackage( + name=name, + version=version, + manifest_path=root / "vendor" / name / "Cargo.toml", + lib=None, + features=(), + source=RegistrySource("registry+https://github.com/rust-lang/crates.io-index"), + ) + ) + workspace = Workspace( + root=root, + target_directory=root / "target", + members=(package,), + packages=tuple(resolved), + ) + return workspace, package + + +STANDALONE = """\ +[package] +name = "prog" +version = "0.1.0" +edition = "2021" + +[lib] +crate-type = ["cdylib"] + +[dependencies] +solana-program = "2.2" +""" + +WITH_FEATURES = """\ +[package] +name = "prog" +version = "0.1.0" + +[lib] +crate-type = ["cdylib"] + +# The project's own comment, which a reserializing writer would move or drop. +[features] +no-entrypoint = [] + +[dependencies] +solana-program = "2.2" +""" + +WORKSPACE_ROOT = """\ +[workspace] +members = ["programs/prog"] +resolver = "2" + +[workspace.dependencies] +solana-program = "2.2" +""" + + +def _plan(root: Path, **kwargs): + workspace, package = _project(root, **kwargs) + return plan_scaffold(workspace, package, SOLANA), workspace + + +def _additions(plan, path: Path = Path("Cargo.toml")) -> list[ManifestAddition]: + """What ``plan`` adds to the manifest at ``path``, in order.""" + return [ + a.edit + for c in plan.changes + if isinstance(c, EditManifest) and c.path == path + for a in c.additions + ] + + +def test_a_fresh_project_gets_the_whole_shape_and_a_second_run_gets_nothing(tmp_path): + # Idempotence is the property, and it has to hold through *apply*, not just through planning: + # the second plan is computed against the files the first one wrote. + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + assert not plan.blocked + touched = apply(plan, workspace.root) + assert touched + + again, _ = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + assert again.changes == () + assert again.satisfied + + +def test_the_manifest_a_fresh_project_ends_up_with_still_parses(tmp_path): + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + parsed = tomllib.loads((tmp_path / "Cargo.toml").read_text()) + + assert parsed["features"]["certora"] == [ + "dep:cvlr", "dep:cvlr-solana", "dep:cvlr-solana-stake", "dep:cvlr-spl-token", + ] + # Optional is what keeps CVLR out of a release build, and what makes `dep:` legal above. + assert parsed["dependencies"]["cvlr"] == {"version": "=0.6.1", "optional": True} + metadata = parsed["package"]["metadata"]["certora"] + assert metadata["sources"] == ["Cargo.toml", "src/**/*.rs"] + assert metadata["solana_inlining"] == ["src/certora/envs/cvlr_inlining.txt"] + + +def test_the_path_a_mock_names_resolves_from_the_programs_own_file(tmp_path): + """``cvlr::mock_fn(with = crate::certora::specs::...)`` expands in the program's own source, + outside ``certora``. The path from there has to be ``pub``. ``pub`` inside a private + ``mod certora`` resolves it without adding to the crate's public API. This checks the + scaffold's ``certora/mod.rs``. + """ + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + root = (tmp_path / HARNESS_DIR / "mod.rs").read_text() + assert "pub mod specs;" in root + + +def test_a_feature_table_that_exists_is_edited_rather_than_reopened(tmp_path): + # Appending `[features]` to a manifest that has one is a duplicate-table error, so this is the + # one change that cannot be an append — and the project's comment must survive it. + plan, workspace = _plan(tmp_path, manifest=WITH_FEATURES, workspace_manifest=WITH_FEATURES) + assert any(isinstance(c, EditManifest) for c in plan.changes) + apply(plan, workspace.root) + + text = (tmp_path / "Cargo.toml").read_text() + assert text.count("[features]") == 1 + assert "The project's own comment" in text + parsed = tomllib.loads(text) + assert parsed["features"]["no-entrypoint"] == [] + # no-entrypoint is enabled only because this package declares it. + assert parsed["features"]["certora"] == [ + "no-entrypoint", "dep:cvlr", "dep:cvlr-solana", "dep:cvlr-solana-stake", + "dep:cvlr-spl-token", + ] + + +def test_a_package_with_no_entrypoint_feature_does_not_get_one_invented(tmp_path): + plan, _ = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + (features,) = [a for a in _additions(plan) if a.table == ("features",)] + assert isinstance(features, AddEntries) + assert "no-entrypoint" not in dict(features.entries)["certora"] + + +def test_a_workspace_gets_the_pins_and_its_member_inherits_them(tmp_path): + plan, workspace = _plan( + tmp_path, + manifest=STANDALONE, + workspace_manifest=WORKSPACE_ROOT, + package_dir="programs/prog", + ) + apply(plan, workspace.root) + + root = tomllib.loads((tmp_path / "Cargo.toml").read_text()) + assert root["workspace"]["dependencies"]["cvlr"] == {"version": "=0.6.1"} + member = tomllib.loads((tmp_path / "programs" / "prog" / "Cargo.toml").read_text()) + assert member["dependencies"]["cvlr"] == {"workspace": True, "optional": True} + + +def test_a_package_that_builds_no_loadable_object_is_refused_rather_than_patched(tmp_path): + # Adding cdylib to somebody's library changes how it builds everywhere, so it is a decision for + # a human. The refusal has to stop the whole plan, not just that one change. + plan, workspace = _plan( + tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE, crate_types=("lib",) + ) + assert [b.problem for b in plan.blocked] == [ + "prog builds no cdylib, so there is no program for the prover to read" + ] + with pytest.raises(ScaffoldBlocked): + apply(plan, workspace.root) + assert not (tmp_path / "src" / "certora").exists() + + +def test_a_library_source_that_does_not_exist_is_refused_rather_than_created(tmp_path): + # cargo metadata reports `[lib] path = "src/missing.rs"` without checking it. Appending the + # harness declaration there would create a lib with no program in it, and it would build. + workspace, package = _project(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + assert package.lib is not None + missing = replace(package, lib=replace(package.lib, src_path=tmp_path / "src" / "missing.rs")) + plan = plan_scaffold(workspace, missing, SOLANA) + assert [b.problem for b in plan.blocked] == [ + "prog's library source, src/missing.rs, does not exist, so there is no crate to add the " + "harness to" + ] + with pytest.raises(ScaffoldBlocked): + apply(plan, workspace.root) + assert not (tmp_path / "src" / "missing.rs").exists() + + +def test_a_certora_feature_that_means_something_else_is_refused(tmp_path): + # A project can legitimately have a feature by that name; extending it would change what their + # build does. Distinguishable from an already-set-up project only by whether CVLR is a dep. + manifest = STANDALONE.replace( + "[dependencies]", '[features]\ncertora = ["some-other-thing"]\n\n[dependencies]' + ) + plan, _ = _plan(tmp_path, manifest=manifest, workspace_manifest=manifest) + assert any("means something else" in b.problem for b in plan.blocked) + + +def test_a_project_already_set_up_is_read_rather_than_refused(tmp_path): + # The same feature name, but with CVLR present: this is a verified project, and the answer is + # "nothing to do" rather than a refusal. + manifest = STANDALONE.replace( + "[dependencies]\nsolana-program", + '[features]\ncertora = ["dep:cvlr"]\n\n[dependencies]\ncvlr = "0.6.1"\nsolana-program', + ) + plan, _ = _plan(tmp_path, manifest=manifest, workspace_manifest=manifest) + assert not plan.blocked + assert any("already exists" in note for note in plan.satisfied) + + +def test_a_platform_generation_the_reference_set_cannot_be_paired_with_is_refused(tmp_path): + # cvlr-solana 0.5.0 is bound to solana-program 2.x, and 1.18's AccountInfo is a different type, + # so this pairing does not warn — it fails to compile. Caught before writing the pin. + plan, _ = _plan( + tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE, platform="1.18.26" + ) + assert any("1.18.26" in b.problem for b in plan.blocked) + + +def test_a_platform_newer_than_the_reference_set_is_refused_though_it_deleted_the_probe(tmp_path): + # Solana v3 moved AccountInfo into solana-account-info and stopped publishing solana-program, + # so a v3 target resolves no solana-program. A gate that only asked about that crate would + # treat the absence as no opinion and pin CVLR 0.5 against it. The scaffold would still + # compile. The mismatch shows up on the first rule that passes an account to a CVLR helper, + # as two different AccountInfo types. + plan, _ = _plan( + tmp_path, + manifest=STANDALONE, + workspace_manifest=STANDALONE, + platform="3.1.1", + platform_crate="solana-account-info", + ) + assert any("3.1.1" in b.problem for b in plan.blocked) + + +def test_a_project_on_the_reference_generation_passes_on_the_specific_witness(tmp_path): + # A 2.x target resolves solana-account-info too, and that witness is first. A match stops + # the check. Continuing on to the next witness would judge the project by a broader crate. + plan, _ = _plan( + tmp_path, + manifest=STANDALONE, + workspace_manifest=STANDALONE, + platform="2.3.0", + platform_crate="solana-account-info", + ) + assert not plan.blocked + + +def test_an_older_platform_copy_beside_the_reference_one_is_refused(tmp_path): + # Both copies build. The old one is what the dependents that pulled it in hand to CVLR. + workspace, package = _project(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + (current,) = workspace.resolved("solana-program") + older = replace(current, version="1.18.26") + workspace = replace(workspace, packages=(*workspace.packages, older)) + plan = plan_scaffold(workspace, package, SOLANA) + assert any("1.18.26" in b.problem for b in plan.blocked) + + +ON_AN_OLDER_LINE = STANDALONE.replace( + "[dependencies]\nsolana-program", + '[dependencies]\ncvlr = "0.4"\ncvlr-solana = "0.4"\nsolana-program', +) + + +def test_a_project_on_a_different_cvlr_line_is_refused(tmp_path): + # One CVLR line is supported at a time, and everything the scaffold writes is that line's. + # It used to defer to a pin like this, withhold the specializations that would collide, and + # report the disagreement for someone to read later; now it stops. + plan, _ = _plan( + tmp_path, + manifest=ON_AN_OLDER_LINE, + workspace_manifest=ON_AN_OLDER_LINE, + cvlr_resolved={"cvlr": "0.4.1", "cvlr-solana": "0.4.5"}, + ) + assert any("0.4.1" in b.problem for b in plan.blocked) + assert any("0.4.5" in b.problem for b in plan.blocked) + + +def test_a_refused_pin_stops_the_plan_before_a_specialization_is_written(tmp_path): + """The refusal has to arrive before the changes, not alongside them. + + A project on the 0.4 line given a 0.5.0 specialization gets two generations of ``AccountInfo`` + in one graph. That used to be avoided by withholding the specializations from such a project; + now the project is refused outright, and :func:`apply` is what must never run. + """ + plan, workspace = _plan( + tmp_path, + manifest=ON_AN_OLDER_LINE, + workspace_manifest=ON_AN_OLDER_LINE, + cvlr_resolved={"cvlr": "0.4.1", "cvlr-solana": "0.4.5"}, + ) + assert plan.blocked + with pytest.raises(ScaffoldBlocked): + apply(plan, workspace.root) + assert 'cvlr = "0.4"' in (tmp_path / "Cargo.toml").read_text() + + +def test_a_cvlr_pin_no_member_depends_on_yet_is_still_refused(tmp_path): + # Declared in [workspace.dependencies] and used by nobody, so cargo has not resolved it and + # the graph says nothing. The scaffold is about to make this member inherit it, which is + # exactly when reading the manifest instead of the graph is the only way to see it. + root = WORKSPACE_ROOT.replace( + "[workspace.dependencies]", '[workspace.dependencies]\ncvlr = "0.4.1"' + ) + plan, _ = _plan( + tmp_path, manifest=STANDALONE, workspace_manifest=root, package_dir="programs/prog" + ) + assert any("0.4.1" in b.problem for b in plan.blocked) + + +def test_a_cvlr_dependency_with_no_readable_version_is_refused(tmp_path): + # A git checkout could be any release. A gate cannot pass a version it cannot see, and + # guessing that a checkout is the pinned one is the mistake the pin exists to prevent. + manifest = STANDALONE.replace( + "[dependencies]\nsolana-program", + '[dependencies]\ncvlr = { git = "https://github.com/Certora/cvlr" }\nsolana-program', + ) + plan, _ = _plan(tmp_path, manifest=manifest, workspace_manifest=manifest) + assert any("git dependency" in b.problem for b in plan.blocked) + + +@pytest.mark.parametrize( + "manifest, overrides", + [ + pytest.param(STANDALONE, {"platform": "1.18.26"}, id="platform"), + pytest.param( + ON_AN_OLDER_LINE, + {"cvlr_resolved": {"cvlr": "0.4.1", "cvlr-solana": "0.4.5"}}, + id="pin", + ), + pytest.param( + STANDALONE.replace( + "[dependencies]\nsolana-program", + '[dependencies]\ncvlr = { git = "https://github.com/Certora/cvlr" }\n' + "solana-program", + ), + {}, + id="unpinned", + ), + ], +) +def test_a_line_refusal_is_put_in_terms_the_project_author_can_act_on( + tmp_path, manifest, overrides +): + """The reader is whoever owns the project. AutoProver's own source is not theirs to edit, so + a refusal names the release this build supports and what to change in the project.""" + plan, _ = _plan(tmp_path, manifest=manifest, workspace_manifest=manifest, **overrides) + assert plan.blocked + for b in plan.blocked: + text = f"{b.problem} {b.resolution}" + assert "composer/" not in text and "reference set" not in text, text + names_a_release = any(f"{c.name} {c.version}" in b.resolution for c in SOLANA.crates()) + names_a_platform = any( + f"{w.name} {w.line}" in b.resolution for w in SOLANA.platform.witnesses + ) + assert names_a_release or names_a_platform, b.resolution + + +def test_a_project_already_on_the_pinned_release_is_not_refused(tmp_path): + # The idempotence case, and the one the gate must not catch: `=0.6.1` is what the scaffold + # itself writes, and a bare `0.6.1` is the same release written by hand. + for requirement in ("=0.6.1", "0.6.1"): + root = tmp_path / requirement + manifest = STANDALONE.replace( + "[dependencies]\nsolana-program", + f'[dependencies]\ncvlr = "{requirement}"\nsolana-program', + ) + plan, _ = _plan( + root, + manifest=manifest, + workspace_manifest=manifest, + cvlr_resolved={"cvlr": "0.6.1"}, + ) + assert not plan.blocked, requirement + + +def test_a_reference_set_crate_the_project_does_not_name_is_not_a_refusal(tmp_path): + # Absent, not mismatched, and the reason the two are separate types. This project is on the + # pinned core and chain crate and names neither specialization; the scaffold adds them. A gate + # that read "not in the graph" as a disagreement would refuse every project it is meant to set + # up, starting with the fresh one. + manifest = STANDALONE.replace( + "[dependencies]\nsolana-program", + '[dependencies]\ncvlr = "=0.6.1"\ncvlr-solana = "=0.5.0"\nsolana-program', + ) + plan, _ = _plan( + tmp_path, + manifest=manifest, + workspace_manifest=manifest, + cvlr_resolved={"cvlr": "0.6.1", "cvlr-solana": "0.5.0"}, + ) + assert not plan.blocked + (dependencies,) = [a for a in _additions(plan) if a.table == ("dependencies",)] + assert isinstance(dependencies, AddEntries) + assert [key for key, _ in dependencies.entries] == ["cvlr-solana-stake", "cvlr-spl-token"] + + +def test_a_partly_pinned_project_is_still_checked(tmp_path): + # One CVLR crate on an old line and one absent: the platform gate has to fire too, because + # the scaffold would write the reference version for the missing one. + manifest = STANDALONE.replace( + "[dependencies]\nsolana-program", '[dependencies]\ncvlr = "0.4"\nsolana-program' + ) + plan, _ = _plan( + tmp_path, + manifest=manifest, + workspace_manifest=manifest, + platform="1.18.26", + cvlr_resolved={"cvlr": "0.4.1"}, + ) + assert any("1.18.26" in b.problem for b in plan.blocked) + assert any("0.4.1" in b.problem for b in plan.blocked) + + +def test_an_existing_harness_declaration_is_not_added_twice(tmp_path): + workspace, package = _project( + tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE + ) + assert package.lib is not None + package.lib.src_path.write_text(PROGRAM + "\npub mod certora;\n") + plan = plan_scaffold(workspace, package, SOLANA) + + assert not any(c.path.name == "lib.rs" for c in plan.changes) + assert any("already declares the harness module" in note for note in plan.satisfied) + + +def test_the_composite_env_file_carries_every_starting_layer_and_says_what_it_covers(tmp_path): + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + + composite = (tmp_path / "src" / "certora" / "envs" / INLINING.composite).read_text() + # The layer files are not in the target, so the composite describes each one by what it covers + # rather than naming a file the reader cannot open. + for layer, name in zip(INLINING.layers, INLINING.starting, strict=True): + assert layer.covers in composite + assert name not in composite + marker = tuning.starting_env(name).strip().splitlines()[-1] + assert marker in composite + + +def test_only_the_generated_files_land_in_the_target(tmp_path): + """The starting layers stay in AutoProver. A copy in the target would be one nothing reads.""" + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + envs = tmp_path / "src" / "certora" / "envs" + assert {p.name for p in envs.iterdir()} == {family.composite for family in ENV_FAMILIES} + + +def test_an_edited_harness_file_is_replaced_and_nothing_else_is_written(tmp_path): + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + specs = tmp_path / HARNESS_DIR / "specs" / "mod.rs" + scaffolded = specs.read_text() + specs.write_text("hand written\n") + + again, _ = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + assert [(type(c), c.path) for c in again.changes] == [(Write, HARNESS_DIR / "specs" / "mod.rs")] + apply(again, workspace.root) + assert specs.read_text() == scaffolded + + +def test_a_generated_file_that_differs_from_the_starting_configuration_is_rewritten(tmp_path): + """What a project scaffolded by an older AutoProver looks like: the composite on disk is not + what today's starting configuration composes to.""" + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + composite = tmp_path / "src" / "certora" / "envs" / SUMMARIES.composite + composite.write_text(";;; composed by an older starting configuration\n") + + again, _ = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + assert [type(c) for c in again.changes] == [Write] + apply(again, workspace.root) + assert composite.read_text() == tuning.compose_env(SUMMARIES, dialect=again.dialect) + + +def test_gitignore_gains_only_what_is_missing(tmp_path): + (tmp_path / ".gitignore").write_text("target/\n.certora_internal\n") + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + + text = (tmp_path / ".gitignore").read_text() + assert text.count(".certora_internal") == 1 + assert ".certora\n" in text and "certora_out" in text + + +def test_a_missing_gitignore_is_created(tmp_path): + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + apply(plan, workspace.root) + + assert (tmp_path / ".gitignore").read_text().splitlines() == [ + "# Certora Prover build output", *scaffold.GITIGNORE_LINES + ] + + +def test_the_projects_manifest_keeps_every_line_it_had(tmp_path): + # The manifest is edited as a document, not reserialized: every line the project wrote is + # still there, in its order, with the additions between them. + plan, workspace = _plan(tmp_path, manifest=WITH_FEATURES, workspace_manifest=WITH_FEATURES) + apply(plan, workspace.root) + edited = iter((tmp_path / "Cargo.toml").read_text().splitlines()) + assert all(line in edited for line in WITH_FEATURES.splitlines()) + + +def test_a_manifest_edited_after_planning_keeps_the_edit(tmp_path): + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + (tmp_path / "Cargo.toml").write_text(STANDALONE + "\n# edited meanwhile\n") + apply(plan, workspace.root) + text = (tmp_path / "Cargo.toml").read_text() + assert "# edited meanwhile" in text + assert "certora = [" in text + + +def test_a_manifest_that_gained_what_the_plan_adds_is_not_written_over(tmp_path): + plan, workspace = _plan(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + meanwhile = STANDALONE + '\n[features]\ncertora = ["dep:something-else"]\n' + (tmp_path / "Cargo.toml").write_text(meanwhile) + with pytest.raises(scaffold.ScaffoldStale, match="already has certora"): + apply(plan, workspace.root) + assert (tmp_path / "Cargo.toml").read_text() == meanwhile + + +def test_the_lib_target_reports_where_cargo_says_its_source_is(tmp_path): + # `[lib] path` can move it, and a scaffold that assumed src/lib.rs would append a module + # declaration to a file nothing compiles. + workspace = parse_metadata( + CargoMetadataJson.model_validate( + { + "workspace_root": str(tmp_path), + "workspace_members": ["prog 0.1.0 (path+file:///prog)"], + "packages": [ + { + "id": "prog 0.1.0 (path+file:///prog)", + "name": "prog", + "version": "0.1.0", + "manifest_path": str(tmp_path / "Cargo.toml"), + "features": {"certora": []}, + "targets": [ + { + "name": "build-script-build", + "kind": ["custom-build"], + "src_path": str(tmp_path / "build.rs"), + }, + { + "name": "prog", + "crate_types": ["cdylib"], + "src_path": str(tmp_path / "program" / "entry.rs"), + }, + ], + } + ], + } + ) + ) + (member,) = workspace.members + assert member.lib is not None + assert member.lib.src_path == tmp_path / "program" / "entry.rs" + assert member.lib.builds_shared_object + assert member.lib.artifact_stem == "prog" + + +# --------------------------------------------------------------------------------------------- +# preflight: the orchestration around the plan + + +class _FakeCargo: + """Stands in for ``cargo metadata`` and records each call. + + Two tests below check which directory and which features were requested. The result does + not show that. + """ + + def __init__(self, workspace: Workspace | MetadataFailure) -> None: + self.workspace = workspace + self.calls: list[tuple[Path, tuple[str, ...]]] = [] + + async def __call__(self, root, *, offline=False, features=(), timeout_s=0): + self.calls.append((Path(root), tuple(features))) + return self.workspace + + +@pytest.fixture +def fake_cargo(monkeypatch): + def install(workspace: Workspace | MetadataFailure) -> _FakeCargo: + fake = _FakeCargo(workspace) + monkeypatch.setattr(Workspace, "read", fake) + return fake + + return install + + +@pytest.mark.asyncio +async def test_preflight_resolves_the_verification_graph_from_the_packages_own_directory( + tmp_path, fake_cargo +): + # CVLR is optional, so a default-feature read reports it absent and the resolved versions + # come back empty. Features also resolve against the package cargo considers current, so + # the directory matters. + workspace, package = _project( + tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE, package_dir="programs/prog" + ) + fake = fake_cargo(workspace) + + result = await preflight.prepare_workspace(tmp_path, reference=SOLANA, package="prog") + + assert fake.calls[0] == (tmp_path, ()) + assert fake.calls[-1] == (package.root, ("certora",)) + assert result.artifact_stem == "prog" + + +@pytest.mark.asyncio +async def test_preflight_reports_what_cargo_said_when_the_project_cannot_be_read( + tmp_path, fake_cargo +): + fake_cargo(CargoFailed("error: failed to parse manifest at `Cargo.toml`\n")) + with pytest.raises(preflight.PreflightFailed, match="failed to parse manifest") as caught: + await preflight.prepare_workspace(tmp_path, reference=SOLANA) + assert str(caught.value).startswith(f"Could not read the Cargo project at {tmp_path}:") + + +@pytest.mark.asyncio +async def test_preflight_refuses_to_choose_between_verifiable_packages(tmp_path, fake_cargo): + # Which program is under verification is a fact about the engagement, not about the layout. + workspace, package = _project(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + second = replace(package, name="other") + fake_cargo(replace(workspace, members=(package, second))) + + with pytest.raises(preflight.PreflightFailed, match="name the one to verify"): + await preflight.prepare_workspace(tmp_path, reference=SOLANA) + + +@pytest.mark.asyncio +async def test_preflight_names_the_members_when_asked_for_one_that_is_not_there( + tmp_path, fake_cargo +): + workspace, _ = _project(tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE) + fake_cargo(workspace) + + with pytest.raises(preflight.PreflightFailed, match="members: prog"): + await preflight.prepare_workspace(tmp_path, reference=SOLANA, package="nope") + + +@pytest.mark.asyncio +async def test_a_blocked_plan_stops_preflight_with_the_resolution_in_the_message( + tmp_path, fake_cargo +): + # Preflight runs in the same task group as system analysis, so this exception cancels that + # work. The message has to carry the fix. It is what the caller sees. + workspace, _ = _project( + tmp_path, manifest=STANDALONE, workspace_manifest=STANDALONE, crate_types=("lib",) + ) + fake_cargo(workspace) + + with pytest.raises(preflight.PreflightFailed, match="crate-type"): + await preflight.prepare_workspace(tmp_path, reference=SOLANA, package="prog") + assert not (tmp_path / "src" / "certora").exists() + + +# --------------------------------------------------------------------------------------------- +# pointing the target at the Anchor fork + + +ANCHOR_MANIFEST = """\ +[package] +name = "prog" +version = "0.1.0" + +[lib] +crate-type = ["cdylib"] + +[dependencies] +anchor-lang = "0.31.1" +""" + + +def test_an_anchor_target_is_redirected_at_the_verification_fork(tmp_path): + """Without the fork, a rule that reaches an Anchor handler cannot be analyzed. Upstream's + boxed ``Error`` trips [3006]. The scaffold is what knows the resolved version, so it is what + picks the branch.""" + workspace, package = _project( + tmp_path, + manifest=ANCHOR_MANIFEST, + workspace_manifest='[workspace]\nmembers = ["."]\n', + cvlr_resolved={"anchor-lang": "0.31.1"}, + ) + plan = plan_scaffold(workspace, package, SOLANA) + assert plan.blocked == () + tables = {a.table: a for a in _additions(plan) if isinstance(a, AddTable)} + patch = tables[("patch", "crates-io", "anchor-lang")] + assert ("branch", "certora-v0.31.1") in patch.body + assert ("git", "https://github.com/Certora/anchor.git") in patch.body + + +def test_redirecting_twice_is_a_no_op(tmp_path): + """A second run must not append the patch table again. Two + ``[patch.crates-io.anchor-lang]`` entries is a manifest cargo will not parse.""" + kwargs = dict( + manifest=ANCHOR_MANIFEST, + workspace_manifest='[workspace]\nmembers = ["."]\n', + cvlr_resolved={"anchor-lang": "0.31.1"}, + ) + workspace, package = _project(tmp_path, **kwargs) + apply(plan_scaffold(workspace, package, SOLANA), tmp_path) + + workspace, package = _project(tmp_path, **kwargs) + again = plan_scaffold(workspace, package, SOLANA) + assert not [a for a in _additions(again) if a.table[0] == "patch"] + assert any("already redirected" in note for note in again.satisfied) + assert (tmp_path / "Cargo.toml").read_text().count("[patch.crates-io.anchor-lang]") == 1 + tomllib.loads((tmp_path / "Cargo.toml").read_text()) + + +def test_an_anchor_version_the_fork_does_not_cover_blocks_the_whole_plan(tmp_path): + """The fork has a branch for 0.30.1 and not 0.30.0. The plan blocks instead of scaffolding a + project that builds and then reports a pointer-analysis error with nothing about Anchor.""" + workspace, package = _project( + tmp_path, + manifest=ANCHOR_MANIFEST.replace("0.31.1", "0.30.0"), + workspace_manifest='[workspace]\nmembers = ["."]\n', + cvlr_resolved={"anchor-lang": "0.30.0"}, + ) + plan = plan_scaffold(workspace, package, SOLANA) + assert any("0.30.0" in b.problem for b in plan.blocked), plan.blocked + with pytest.raises(ScaffoldBlocked): + apply(plan, tmp_path) + # A blocked plan applies nothing at all, including the parts that were fine. + assert not (tmp_path / "src" / "certora").exists() + + +def test_a_non_anchor_target_gets_no_patch_section(tmp_path): + workspace, package = _project( + tmp_path, manifest=STANDALONE, workspace_manifest='[workspace]\nmembers = ["."]\n' + ) + plan = plan_scaffold(workspace, package, SOLANA) + assert not [a for a in _additions(plan) if a.table[0] == "patch"] + assert any("anchor-lang is not a dependency" in note for note in plan.satisfied) + + +def test_the_forks_planned_are_the_reference_chains_own(tmp_path): + """Soroban has no forks, so an Anchor release in its graph is neither redirected nor refused, + even one the Anchor fork does not cover.""" + workspace, package = _project( + tmp_path, + manifest=ANCHOR_MANIFEST.replace("0.31.1", "0.30.0"), + workspace_manifest='[workspace]\nmembers = ["."]\n', + platform="22.0.0", + platform_crate="soroban-sdk", + cvlr_resolved={"anchor-lang": "0.30.0"}, + ) + plan = plan_scaffold(workspace, package, SOROBAN) + assert not [a for a in _additions(plan) if a.table[0] == "patch"] + assert not [b for b in plan.blocked if "anchor-lang" in b.problem], plan.blocked + assert not [note for note in plan.satisfied if "anchor" in note] diff --git a/tests/test_prover_conf.py b/tests/test_prover_conf.py new file mode 100644 index 00000000..047f9050 --- /dev/null +++ b/tests/test_prover_conf.py @@ -0,0 +1,52 @@ +"""The shared conf layering, and the CVL run conf built on it.""" + +import json +from pathlib import Path + +from composer.prover.conf import ExcludeRules, InheritRules, SelectRules, dump_conf +from composer.spec.source.prover import ( + BOTH_RULE_SCOPES, prover_config_overlay, rule_selection, setup_prover_config_in, +) + + +_BASE = {"files": ["C.sol"], "rule": ["base_rule"], "exclude_rule": ["skipped"], "loop_iter": 3} + + +def test_each_rule_selection_writes_only_its_key(): + assert InheritRules().apply_to(_BASE) == _BASE + assert SelectRules(("r",)).apply_to(_BASE) == {**_BASE, "rule": ["r"]} + assert ExcludeRules(("r",)).apply_to(_BASE) == {**_BASE, "exclude_rule": ["r"]} + + +def test_cvl_overlay_forces_its_settings_over_the_base(): + """CVL overrides the base's own sanity and loop settings, whatever they are.""" + base = {**_BASE, "rule_sanity": "advanced", "optimistic_loop": False} + assert prover_config_overlay(base, main_contract="C", verify_target="C:x.spec") == { + **_BASE, + "verify": "C:x.spec", + "parametric_contracts": "C", + "optimistic_loop": True, + "rule_sanity": "basic", + } + + +def test_rule_selection_from_the_tool_arguments(): + assert rule_selection(None, None) == InheritRules() + assert rule_selection(["a"], None) == SelectRules(("a",)) + assert rule_selection(None, ["b"]) == ExcludeRules(("b",)) + assert rule_selection(["a"], ["b"]) == BOTH_RULE_SCOPES + + +def test_cvl_run_conf_on_disk(tmp_path: Path): + """``msg`` and other extras land in the written conf; an exclusion keeps the base's ``rule``.""" + with setup_prover_config_in( + working_dir=str(tmp_path), config=_BASE, spec_contents="rule r { assert true; }", + main_contract="C", rules=ExcludeRules(("r",)), msg="iteration 1", + ) as (conf_path, config): + written = (tmp_path / conf_path).read_text() + assert written == dump_conf(config) + parsed = json.loads(written) + assert parsed["rule"] == ["base_rule"] + assert parsed["exclude_rule"] == ["r"] + assert parsed["msg"] == "iteration 1" + assert parsed["rule_sanity"] == "basic" diff --git a/tests/test_rules_striping.py b/tests/test_rules_striping.py index 72b9ae18..f27d7bbe 100644 --- a/tests/test_rules_striping.py +++ b/tests/test_rules_striping.py @@ -28,7 +28,7 @@ from composer.spec.source.author import ExpectRuleFailure from composer.spec.source.buffer_tools import put_buffer from composer.spec.source.prover import ( - NagMarker, ProverHistoryItem, ProverRunLog, RuleSelection, StateWithSkips, + NagMarker, ProverHistoryItem, ProverRunLog, RuleSelectionRecord, StateWithSkips, VALIDATION_KEY, _executed_rules, _is_completion_history, ) from composer.spec.source.spec_buffers import NamedBuffer, check_buffer_completion @@ -47,18 +47,18 @@ # --------------------------------------------------------------------------- -def _inc(*rules: str) -> RuleSelection: +def _inc(*rules: str) -> RuleSelectionRecord: return {"sort": "include", "selector": list(rules)} -def _exc(*rules: str) -> RuleSelection: +def _exc(*rules: str) -> RuleSelectionRecord: return {"sort": "exclude", "selector": list(rules)} def _log( *results: tuple[RulePath, StatusCodes], digest: str = "d1", - rules: RuleSelection | None = None, + rules: RuleSelectionRecord | None = None, declared: tuple[str, ...] = ("a", "b"), ) -> ProverRunLog: return ProverRunLog( diff --git a/tests/test_stuck_rule_warnings.py b/tests/test_stuck_rule_warnings.py index aa0f26a1..2f998d63 100644 --- a/tests/test_stuck_rule_warnings.py +++ b/tests/test_stuck_rule_warnings.py @@ -15,7 +15,7 @@ from composer.prover.ptypes import RulePath from composer.spec.source.prover import ( - NagMarker, ProverHistoryItem, ProverRunLog, RuleSelection, STUCK_RULE_NAG_THRESHOLD, + NagMarker, ProverHistoryItem, ProverRunLog, RuleSelectionRecord, STUCK_RULE_NAG_THRESHOLD, stuck_rule_reminder, stuck_rule_warnings, ) @@ -26,7 +26,7 @@ def _run( *results: tuple[RulePath, str], tc_id: str = "tc", - rules: RuleSelection | None = None, + rules: RuleSelectionRecord | None = None, declared: tuple[str, ...] = ("r1", "r2"), ) -> ProverHistoryItem: return ProverRunLog( diff --git a/uv.lock b/uv.lock index 8e9bfa07..3536fa8b 100644 --- a/uv.lock +++ b/uv.lock @@ -93,6 +93,7 @@ dependencies = [ { name = "rich" }, { name = "sqlalchemy" }, { name = "textual" }, + { name = "tomlkit" }, { name = "tqdm" }, { name = "wcmatch" }, { name = "websockets" }, @@ -196,6 +197,7 @@ requires-dist = [ { name = "sentence-transformers", marker = "extra == 'ml'", specifier = ">=5.1" }, { name = "sqlalchemy", specifier = ">=2.0.0" }, { name = "textual", specifier = ">=8.1" }, + { name = "tomlkit", specifier = ">=0.15.1" }, { name = "torch", marker = "extra == 'cpu'", index = "https://download.pytorch.org/whl/cpu", conflict = { package = "ai-composer", extra = "cpu" } }, { name = "torch", marker = "extra == 'cuda'", index = "https://download.pytorch.org/whl/cu128", conflict = { package = "ai-composer", extra = "cuda" } }, { name = "tqdm", specifier = ">=4.65.0" }, @@ -5085,6 +5087,15 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/72/f4/0de46cfa12cdcbcd464cc59fde36912af405696f687e53a091fb432f694c/tokenizers-0.22.2-cp39-abi3-win_arm64.whl", hash = "sha256:9ce725d22864a1e965217204946f830c37876eee3b2ba6fc6255e8e903d5fcbc", size = 2612133, upload-time = "2026-01-05T10:45:17.232Z" }, ] +[[package]] +name = "tomlkit" +version = "0.15.1" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/94/96/e07752635b98536177fa1f37671c8f3cdde2e724c6bcf6034b2cfb571565/tomlkit-0.15.1.tar.gz", hash = "sha256:e25bbf38843005246210a12982776f27f99cb9be67160e14434d0c0d21ee1e97", size = 180129, upload-time = "2026-07-17T01:48:04.562Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/13/bc/8c13eb66537dce1d2bd3a57132902f38d0e7f5bb46fa9f4daed9fe9d76ee/tomlkit-0.15.1-py3-none-any.whl", hash = "sha256:177a05aece5a8ca5266fd3c448abb47b8d352f09d477d3ca8332db4d89b24304", size = 49449, upload-time = "2026-07-17T01:48:05.728Z" }, +] + [[package]] name = "torch" version = "2.11.0+cu128"