Support verifying a library main contract via a generated harness

certora_autosetup/autosetup/cli.py

@@ -15,6 +15,7 @@
 from certora_autosetup.autosetup.cli_args import create_parser
 from certora_autosetup.autosetup.types import AutosetupConfig
 from certora_autosetup.cache.cache_fs import get_fs, init_cache_fs
+from certora_autosetup.harnesser.swap import swap_library_main_contract, with_harnessed_library
 from certora_autosetup.cache.content_cache import ContentCache
 from certora_autosetup.reporting.reporter import Reporter
 from certora_autosetup.setup.sanity_rule_generator import SanityRuleGenerator
@@ -107,6 +108,26 @@ def main():
         )
         contract_handles = with_contract_handle(contract_handles, main_contract_handle)
 
+    # A library cannot be a verification target — the Prover accepts it and instantiates
+    # no parametric methods. Swap in a generated harness before anything downstream keys
+    # on the contract name (sanity spec, base conf, verify target, result keys).
+    harnessed_library = main_contract_handle
+    main_contract_handle, contract_handles, _library_harness = swap_library_main_contract(
+        project_root=cwd,
+        main_contract_handle=main_contract_handle,
+        contract_handles=contract_handles,
+        solc=args.solc_default,
+        certora_run_command=args.certora_run_command,
+    )
+    # AutoProver's pipeline swaps before it invokes us, so on that path the target
+    # arrives already harnessed and only the manifest still names the library.
+    args.additional_contracts = with_harnessed_library(
+        cwd,
+        main_contract_handle,
+        args.additional_contracts or [],
+        swapped_from=harnessed_library if _library_harness is not None else None,
+    )
+
     # TODO: a bare `path.sol` spec drops only the contract whose name matches the file
     # stem. Expand to "drop every concrete contract in the file" for symmetry with
     # auto-detect's emit-all default. Mirror the same expansion for include specs

certora_autosetup/harnesser/__init__.py

@@ -0,0 +1,12 @@
+"""Generate a verifiable contract harness for a library main contract."""
+
+from certora_autosetup.harnesser.detect import contract_kind, is_library_main_contract
+from certora_autosetup.harnesser.model import HarnessPlan, LibraryApi, LibraryHarnessError
+
+__all__ = [
+    "contract_kind",
+    "is_library_main_contract",
+    "HarnessPlan",
+    "LibraryApi",
+    "LibraryHarnessError",
+]

certora_autosetup/harnesser/__main__.py

@@ -0,0 +1,3 @@
+from certora_autosetup.harnesser.cli import main
+
+raise SystemExit(main())

certora_autosetup/harnesser/cli.py

@@ -0,0 +1,103 @@
+"""``python -m certora_autosetup.harnesser`` — generate a library harness.
+
+    python -m certora_autosetup.harnesser --library src/utils/BitMaps.sol:BitMaps \
+        --project-dir . --output harness.json
+
+It compiles a probe build to learn the library's API, writes
+``certora/harnesses/CertoraLibraryHarness_<Library>.sol``, and records what it wrapped.
+The JSON record goes to the file named by ``--output`` rather than to stdout, because
+the probe build and the logger both write there; whoever runs this decides what to do
+with the harness, so nothing here swaps a main contract.
+"""
+
+import argparse
+import json
+import sys
+from pathlib import Path
+
+from certora_autosetup.harnesser.model import LibraryHarnessError
+from certora_autosetup.harnesser.run import ensure_library_harness
+from certora_autosetup.utils.contract_utils import parse_contract_files, split_contract_spec
+from certora_autosetup.utils.types import ContractHandle
+
+
+def _project_relative(handle: ContractHandle, root: Path) -> ContractHandle:
+    """Probe-build file arguments are resolved from the project root, so keep them there.
+
+    ``parse_contract_files`` absolutizes against the root in order to check the file
+    exists; the build wants the path back the way the user wrote it.
+    """
+    path = Path(handle.source_file)
+    if path.is_absolute() and path.is_relative_to(root):
+        path = path.relative_to(root)
+    return ContractHandle(contract_name=handle.contract_name, source_file=path.as_posix())
+
+
+def main(argv: list[str] | None = None) -> int:
+    parser = argparse.ArgumentParser(
+        prog="certora_autosetup.harnesser",
+        description="Generate a verifiable contract harness for a library main contract.",
+    )
+    parser.add_argument(
+        "--library",
+        required=True,
+        help="Library to wrap, as path/To/Lib.sol:LibName (name defaults to the file stem)",
+    )
+    parser.add_argument(
+        "--project-dir", default=".", help="Project root; defaults to the current directory"
+    )
+    parser.add_argument("--solc", default=None, help="solc to build with, e.g. solc8.16")
+    parser.add_argument(
+        "--extra-file",
+        action="append",
+        default=[],
+        dest="extra_files",
+        help="Additional path:Contract to include in the probe build; repeatable",
+    )
+    parser.add_argument(
+        "--skip-validation",
+        action="store_true",
+        help="Do not recompile the filled harness (faster; leaves compile errors to autosetup)",
+    )
+    parser.add_argument(
+        "--output",
+        default=None,
+        help="Write the JSON result here; without it only the human summary is printed",
+    )
+    args = parser.parse_args(argv)
+
+    library_path, library_name = split_contract_spec(args.library)
+    project_root = Path(args.project_dir).resolve()
+
+    try:
+        # Parsed rather than passed through, so a mistyped --extra-file is reported here
+        # instead of as a probe-build failure minutes later.
+        extra_files = [
+            _project_relative(handle, project_root)
+            for handle in parse_contract_files(args.extra_files, project_root)
+        ] if args.extra_files else []
+        result = ensure_library_harness(
+            project_root=project_root,
+            library=ContractHandle(contract_name=library_name, source_file=library_path),
+            solc=args.solc,
+            extra_files=extra_files,
+            validate=not args.skip_validation,
+        )
+    except (LibraryHarnessError, ValueError) as e:
+        print(f"library harness generation failed: {e}", file=sys.stderr)
+        return 1
+
+    if args.output:
+        Path(args.output).write_text(json.dumps(result.to_dict(), indent=2) + "\n")
+
+    coverage = result.coverage
+    print(
+        f"{result.harness.contract_name} -> {result.harness.source_file}: "
+        f"{coverage['wrapped']}/{coverage['total']} function(s) wrapped, "
+        f"{coverage['readers']} storage reader(s), {coverage['skipped']} skipped"
+    )
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

certora_autosetup/harnesser/detect.py

@@ -0,0 +1,150 @@
+"""Decide whether a main contract is a ``library``, before anything is built.
+
+The Certora Prover does not reject a library verification target — it accepts it and
+silently verifies nothing, because parametric rules filter libraries out of the method
+set. There is therefore no error message to key on: detection has to read the
+declaration itself.
+
+It reads it from solc's own AST rather than from the source text. ``solc
+--standard-json`` with ``stopAfter: "parsing"`` returns ``ContractDefinition`` nodes
+carrying ``contractKind`` without resolving imports, type-checking, or generating code,
+so a single unresolved-import-laden library file parses in milliseconds with no build
+and no dependency setup.
+
+``stopAfter`` requires solc >= 0.7. Below that, solc refuses to emit an AST for a file
+whose imports it cannot resolve, which is every real library file, and pre-build
+detection is not possible; such a project keeps today's behavior and logs why.
+
+Reading the declarations out of that AST is shared with the post-build dump path, in
+``solidity_ast.contracts``.
+"""
+
+import json
+import shutil
+import subprocess
+from pathlib import Path
+from typing import Dict, Optional
+
+from packaging.version import Version
+
+from certora_autosetup.solidity_ast import parse_only_declarations
+from certora_autosetup.utils.logger import logger
+from certora_autosetup.utils.solc_version_resolver import (
+    convert_solc_version_to_certora_format,
+    read_pragma_from_source_file,
+    resolve_pragma_to_version,
+)
+from certora_autosetup.utils.types import ContractKind
+
+#: Below this, solc has no ``stopAfter`` and cannot parse a file with unresolved imports.
+MIN_SOLC_FOR_PARSE_ONLY = Version("0.7.0")
+
+
+def _solc_binary(version: str) -> Optional[str]:
+    """Locate an installed solc binary for ``version`` under either naming convention."""
+    for name in (convert_solc_version_to_certora_format(version), f"solc-{version}"):
+        if path := shutil.which(name):
+            return path
+    return None
+
+
+def _parse_only_ast(solc: str, source_file: Path, content: str) -> Optional[Dict]:
+    """Parse a single file and return its AST node dict, or None if solc could not.
+
+    Imports are deliberately left unresolved: ``stopAfter: "parsing"`` never follows
+    them, so the ``sources`` map holds exactly one entry.
+    """
+    request = {
+        "language": "Solidity",
+        "sources": {source_file.name: {"content": content}},
+        "settings": {
+            "stopAfter": "parsing",
+            "outputSelection": {"*": {"": ["ast"]}},
+        },
+    }
+    try:
+        completed = subprocess.run(
+            [solc, "--standard-json"],
+            input=json.dumps(request),
+            capture_output=True,
+            text=True,
+            timeout=60,
+        )
+        response = json.loads(completed.stdout)
+    except (subprocess.SubprocessError, json.JSONDecodeError, OSError) as e:
+        logger.log(f"solc parse-only probe failed for {source_file}: {e}", "DEBUG", "Harnesser")
+        return None
+
+    for error in response.get("errors", []):
+        if error.get("severity") == "error":
+            logger.log(
+                f"solc could not parse {source_file}: {error.get('message', '')}",
+                "DEBUG",
+                "Harnesser",
+            )
+            return None
+
+    sources = response.get("sources", {})
+    entry = sources.get(source_file.name) or next(iter(sources.values()), None)
+    return entry.get("ast") if entry else None
+
+
+def contract_kind(
+    source_file: Path,
+    contract_name: str,
+    project_root: Optional[Path] = None,
+    preferred_solc: Optional[str] = None,
+) -> Optional[ContractKind]:
+    """Return the declared kind of ``contract_name``.
+
+    None means the question could not be answered (no usable solc, unparseable file, or
+    the name is not declared here); callers treat that as "not a library" and proceed
+    unchanged, which is the behavior that predates this feature.
+    """
+    if not source_file.exists():
+        return None
+
+    content = source_file.read_text(errors="replace")
+    pragma = read_pragma_from_source_file(source_file, project_root)
+    version = resolve_pragma_to_version(pragma, preferred_solc) if pragma else preferred_solc
+    if not version:
+        logger.log(
+            f"No solc version resolvable for {source_file}; skipping library detection",
+            "DEBUG",
+            "Harnesser",
+        )
+        return None
+
+    if Version(version) < MIN_SOLC_FOR_PARSE_ONLY:
+        logger.log(
+            f"{source_file} resolves to solc {version}; parse-only AST needs >= "
+            f"{MIN_SOLC_FOR_PARSE_ONLY}, so a library main contract cannot be detected "
+            f"before the build",
+            "WARNING",
+            "Harnesser",
+        )
+        return None
+
+    solc = _solc_binary(version)
+    if not solc:
+        logger.log(f"No installed solc binary for {version}", "DEBUG", "Harnesser")
+        return None
+
+    ast = _parse_only_ast(solc, source_file, content)
+    if not ast:
+        return None
+
+    for decl in parse_only_declarations(ast, str(source_file)):
+        if decl.name == contract_name:
+            return decl.contract_kind
+    return None
+
+
+def is_library_main_contract(
+    source_file: Path,
+    contract_name: str,
+    project_root: Optional[Path] = None,
+    preferred_solc: Optional[str] = None,
+) -> bool:
+    """Whether verifying ``contract_name`` requires a generated harness."""
+    return contract_kind(source_file, contract_name, project_root, preferred_solc) is ContractKind.LIBRARY