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
 from certora_autosetup.cache.content_cache import ContentCache
 from certora_autosetup.reporting.reporter import Reporter
 from certora_autosetup.setup.sanity_rule_generator import SanityRuleGenerator
@@ -86,6 +87,17 @@ def main():
     main_handles = parse_contract_files([args.main_contract])
     main_contract_handle = main_handles[0]
 
+    # 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).
+    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,
+    )
+
     # 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,89 @@
+"""``python -m certora_autosetup.harnesser`` — generate a library harness.
+
+AutoProver invokes this as a subprocess and reads the JSON record from the file named by
+``--output``, so the Solidity generation stays on the autosetup side while the decision
+to swap the main contract stays with the caller. The result goes to a file rather than
+stdout because the probe build and the logger both write there; this mirrors how
+autosetup already hands its result to composer via ``--composer-setup``.
+"""
+
+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
+
+
+def _split_target(target: str) -> tuple[str, str]:
+    """Split ``path/To/Lib.sol:LibName``, defaulting the name to the file stem."""
+    if ":" in target:
+        path, name = target.rsplit(":", 1)
+        return path, name
+    path = target
+    return path, Path(path).stem
+
+
+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_target(args.library)
+
+    try:
+        result = ensure_library_harness(
+            project_root=Path(args.project_dir),
+            library_file=Path(library_path),
+            library_name=library_name,
+            solc=args.solc,
+            extra_files=args.extra_files,
+            validate=not args.skip_validation,
+        )
+    except LibraryHarnessError 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_name} -> {result.harness_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/cvl_reserved.py

@@ -0,0 +1,116 @@
+"""CVL reserved words that a generated wrapper name must avoid.
+
+A wrapper is only useful if a spec can name it. CVL's grammar reserves words that are
+perfectly legal Solidity function names, so a mechanically-wrapped library hits them
+routinely: ``at`` appears 41 times across OpenZeppelin and Solady, ``sort`` 4, ``exists``
+3. A wrapper called ``at`` compiles and then makes the spec unparseable.
+
+The list is the identifier-shaped terminal set of the CVL grammar, transcribed from
+``TerminalId.kt`` in the Prover repo. It is vendored rather than derived because the
+harnesser has no access to the Prover's sources at runtime; it is a closed grammar, so
+it changes rarely, and an entry that disappears only costs one needless rename.
+
+The escape is a trailing underscore, which is what OpenZeppelin's hand-written Certora
+harness uses (``at_``), so generated specs read like the human-written ones.
+"""
+
+from typing import FrozenSet
+
+#: Identifier-shaped terminals of the CVL grammar. Operators and punctuation are
+#: omitted: they cannot collide with a Solidity function name.
+CVL_RESERVED_WORDS: FrozenSet[str] = frozenset(
+    {
+        "ALL",
+        "ALWAYS",
+        "ASSERT_FALSE",
+        "AUTO",
+        "CONSTANT",
+        "Create",
+        "DELETE",
+        "DISPATCH",
+        "DISPATCHER",
+        "EOF",
+        "HAVOC_ALL",
+        "HAVOC_ECF",
+        "NONDET",
+        "PER_CALLEE_CONSTANT",
+        "STORAGE",
+        "Sload",
+        "Sstore",
+        "Tload",
+        "Tstore",
+        "UNRESOLVED",
+        "as",
+        "assert",
+        "assuming",
+        "at",
+        "axiom",
+        "builtin",
+        "default",
+        "definition",
+        "description",
+        "else",
+        "error",
+        "event",
+        "exists",
+        "expect",
+        "fallback",
+        "false",
+        "filtered",
+        "forall",
+        "function",
+        "ghost",
+        "good_description",
+        "havoc",
+        "hook",
+        "if",
+        "import",
+        "in",
+        "indexed",
+        "invariant",
+        "lastReverted",
+        "lastStorage",
+        "links",
+        "mapping",
+        "methods",
+        "new",
+        "norevert",
+        "old",
+        "onTransactionBoundary",
+        "override",
+        "persistent",
+        "preserved",
+        "require",
+        "requireInvariant",
+        "reset_storage",
+        "return",
+        "returns",
+        "revert",
+        "rule",
+        "satisfy",
+        "sig",
+        "sort",
+        "strong",
+        "sum",
+        "true",
+        "unresolved",
+        "use",
+        "using",
+        "usum",
+        "void",
+        "weak",
+        "with",
+        "withrevert",
+        "xor",
+    }
+)
+
+
+def escape_reserved(name: str) -> str:
+    """Rename ``name`` if CVL reserves it, else return it unchanged.
+
+    Applied before collision mangling: renaming afterwards could turn a distinct name
+    into one already taken (a library declaring both ``at`` and ``at_`` — and ``at_`` is
+    in active use in OpenZeppelin's own harness).
+    """
+    return f"{name}_" if name in CVL_RESERVED_WORDS else name

certora_autosetup/harnesser/detect.py

@@ -0,0 +1,145 @@
+"""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.
+"""
+
+import json
+import shutil
+import subprocess
+from pathlib import Path
+from typing import Dict, Optional
+
+from packaging.version import Version
+
+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,
+)
+
+#: 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[str]:
+    """Return the declared kind of ``contract_name`` — "library", "contract", "interface".
+
+    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 node in ast.get("nodes", []):
+        if node.get("nodeType") == "ContractDefinition" and node.get("name") == contract_name:
+            return node.get("contractKind")
+    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) == "library"