certora-fv-amenability: static FV-amenability scorer (phase 1)

certora_autosetup/amenability/__init__.py

@@ -0,0 +1,10 @@
+"""certora-fv-amenability: score how amenable a Solidity project is to automatic
+formal verification (autosetup) — low / medium / high — from deterministic AST
+signals (phase 1) plus an LLM judge over a versioned rubric (phase 2).
+
+See report.py for the output contract and signals/ for the individual metrics.
+"""
+
+from certora_autosetup.amenability.report import AmenabilityReport, Level
+
+__all__ = ["AmenabilityReport", "Level"]

certora_autosetup/amenability/cli.py

@@ -0,0 +1,148 @@
+"""certora-fv-amenability: score how amenable a Solidity project is to
+automatic formal verification with autosetup.
+
+JSON in/out, no side effects: clients (SaaS, CI, humans) call this and read the
+report from stdout. Exit 0 = scored (any level); exit 1 = could not score
+(most importantly: the project does not compile).
+"""
+
+import argparse
+import subprocess
+import sys
+from pathlib import Path
+
+from certora_autosetup.amenability.compile import CannotScoreError, resolve_dumps
+from certora_autosetup.amenability.context import AnalysisContext
+from certora_autosetup.amenability.report import (
+    AmenabilityReport,
+    Level,
+    Recommendation,
+    ScoringErrorReport,
+)
+from certora_autosetup.amenability.scoring import DEFAULT_WEIGHTS, ScoringConfig, aggregate
+from certora_autosetup.amenability.signals import ALL_SIGNALS
+from certora_autosetup.solidity_ast import ContractDefinition, find_all
+
+BASE_CONFIDENCE = 0.6  # static-only scoring; the phase-2 judge raises/lowers this
+
+
+def _tool_version() -> str:
+    try:
+        return subprocess.run(
+            ["git", "describe", "--always", "--dirty"],
+            cwd=Path(__file__).parent, capture_output=True, text=True, timeout=5,
+        ).stdout.strip() or "unknown"
+    except Exception:
+        return "unknown"
+
+
+def _recommendations(report_evidence) -> list[Recommendation]:
+    kinds = {e.signal for e in report_evidence}
+    recs = []
+    if "curated_summary_hits" in kinds:
+        recs.append(Recommendation(
+            kind="summary",
+            detail="Replace hand-rolled math kernels with a standard library "
+                   "(OZ Math / FullMath / prb-math) for which autosetup ships curated summaries.",
+        ))
+    if "asm_trampoline" in kinds:
+        recs.append(Recommendation(
+            kind="reference-impl",
+            detail="Replace manual calldata/delegatecall trampolines with direct calls or a "
+                   "reference implementation without the forwarding layer.",
+        ))
+    if "asm_fp_manipulation" in kinds or "storage_packing" in kinds:
+        recs.append(Recommendation(
+            kind="munge",
+            detail="Move hand-rolled memory/storage layouts behind standard declarations or "
+                   "sanctioned slot patterns (ERC-7201/StorageSlot) so the prover's storage "
+                   "and memory analyses can model them.",
+        ))
+    if "bitmask_style" in kinds or "mixed_theory" in kinds:
+        recs.append(Recommendation(
+            kind="harness",
+            detail="Extract packed-field decoding and nonlinear math into small internal pure "
+                   "functions — each becomes a summarization seam for modular proofs.",
+        ))
+    return recs
+
+
+def main() -> int:
+    parser = argparse.ArgumentParser(prog="certora-fv-amenability", description=__doc__)
+    parser.add_argument("project_root", type=Path)
+    parser.add_argument("--contract", action="append", default=[],
+                        help="restrict the contracts_analyzed listing (repeatable)")
+    parser.add_argument("--ast-dump", action="append", default=[], type=Path,
+                        help="existing certoraRun --dump_asts output (repeatable)")
+    parser.add_argument("--weights", type=Path, default=DEFAULT_WEIGHTS)
+    parser.add_argument("--judge", action="store_true",
+                        help="run the LLM judge over the static report (requires "
+                             "Anthropic credentials); default is static-only")
+    parser.add_argument("--rubric-version", default=None,
+                        help="pin a specific judge rubric version (default: latest)")
+    parser.add_argument("--no-llm", action="store_true",
+                        help="explicitly static-only (the default; kept for interface stability)")
+    parser.add_argument("--output", type=Path, default=None, help="write report here instead of stdout")
+    args = parser.parse_args()
+
+    project_root = args.project_root.resolve()
+
+    try:
+        resolution = resolve_dumps(project_root, args.ast_dump)
+    except CannotScoreError as e:
+        error = ScoringErrorReport(project=str(project_root), error=e.error, detail=e.detail)
+        print(error.model_dump_json(indent=2))
+        return 1
+
+    ctx = AnalysisContext(project_root=project_root, dumps=resolution.dumps)
+
+    config = ScoringConfig.load(args.weights)
+    results = [sig(ctx) for sig in ALL_SIGNALS]
+    static = aggregate(results, config)
+    evidence = [e for r in results for e in r.evidence]
+
+    contracts = sorted({
+        c.name for _, root in ctx.iter_sources()
+        for c in find_all(root, ContractDefinition)
+        if c.contractKind == "contract" and not c.abstract
+    })
+    if args.contract:
+        requested = set(args.contract)
+        contracts = [c for c in contracts if c in requested]
+
+    confidence = BASE_CONFIDENCE
+    if ctx.unparsed_source_count:
+        confidence = max(0.3, confidence - 0.05 * ctx.unparsed_source_count)
+
+    report = AmenabilityReport(
+        tool_version=_tool_version(),
+        project=str(project_root),
+        contracts_analyzed=contracts,
+        level=static.provisional_level,
+        confidence=round(confidence, 2),
+        static=static,
+        evidence=evidence,
+        recommendations=_recommendations(evidence),
+    )
+
+    if args.judge and not args.no_llm:
+        from certora_autosetup.amenability.judge import JudgeError, judge_report
+        try:
+            report.judge = judge_report(report, ctx, rubric_version=args.rubric_version)
+            report.level = Level(report.judge["level"])
+            report.confidence = round(
+                (confidence + report.judge["confidence"]) / 2, 2
+            )
+        except JudgeError as e:
+            print(f"judge failed, keeping static verdict: {e}", file=sys.stderr)
+
+    payload = report.model_dump_json(indent=2)
+    if args.output:
+        args.output.write_text(payload + "\n")
+    else:
+        print(payload)
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())

certora_autosetup/amenability/compile.py

@@ -0,0 +1,63 @@
+"""AST-dump acquisition.
+
+Compiling is the amenability floor: there is no degraded raw-source scoring
+path. The resolution order is (1) dumps passed explicitly, (2) dumps a previous
+certoraRun/autosetup run left under .certora_internal, (3) a distinct
+"cannot score" error telling the caller exactly what to run.
+"""
+
+from dataclasses import dataclass
+from pathlib import Path
+
+from certora_autosetup.solidity_ast import AstDump
+
+DUMP_BASENAMES = ("all_asts.json", ".asts.json")
+
+
+class CannotScoreError(Exception):
+    def __init__(self, error: str, detail: str):
+        super().__init__(detail)
+        self.error = error
+        self.detail = detail
+
+
+@dataclass
+class DumpResolution:
+    dumps: list[AstDump]
+    dump_paths: list[Path]
+
+
+def discover_dumps(project_root: Path) -> list[Path]:
+    """Newest-first AST dumps a previous certoraRun left in the project."""
+    internal = project_root / ".certora_internal"
+    if not internal.is_dir():
+        return []
+    candidates = [
+        p for name in DUMP_BASENAMES for p in internal.rglob(name) if p.is_file()
+    ]
+    return sorted(candidates, key=lambda p: p.stat().st_mtime, reverse=True)
+
+
+def resolve_dumps(project_root: Path, ast_dump_args: list[Path]) -> DumpResolution:
+    if ast_dump_args:
+        missing = [p for p in ast_dump_args if not p.is_file()]
+        if missing:
+            raise CannotScoreError(
+                "no-ast-dump", f"--ast-dump path(s) not found: {', '.join(map(str, missing))}"
+            )
+        return DumpResolution(
+            dumps=[AstDump.load(p) for p in ast_dump_args], dump_paths=list(ast_dump_args)
+        )
+
+    discovered = discover_dumps(project_root)
+    if discovered:
+        newest = discovered[0]
+        return DumpResolution(dumps=[AstDump.load(newest)], dump_paths=[newest])
+
+    raise CannotScoreError(
+        "does-not-compile",
+        "No AST dump found. The project must compile before it can be scored — run "
+        "`certoraRun <files...> --compilation_steps_only --dump_asts` (or a "
+        "certora-autosetup compilation analysis) in the project first, or pass an "
+        "existing dump via --ast-dump.",
+    )

certora_autosetup/amenability/context.py

@@ -0,0 +1,130 @@
+"""AnalysisContext: the one object every signal receives.
+
+Wraps one or more AstDumps (a project may have per-contract dumps), deduplicates
+sources across them, separates project code from dependencies, and maps AST byte
+offsets to source lines for evidence.
+"""
+
+from dataclasses import dataclass, field
+from pathlib import Path
+from typing import Iterator, Optional
+
+from certora_autosetup.solidity_ast import (
+    AstDump,
+    ContractDefinition,
+    FunctionDefinition,
+    SourceUnit,
+    find_all,
+)
+
+# Path fragments that mark a source as a dependency rather than project code.
+# Signals score project code; dependencies still participate where they must
+# (e.g. curated-summary library detection).
+DEPENDENCY_MARKERS = ("node_modules/", "lib/", "dependencies/", ".deps/")
+
+# Dumps produced inside build containers key sources by the container's project
+# mount; strip these so source text resolves against the host project_root.
+CONTAINER_ROOTS = ("/workspace/project/",)
+
+
+def _strip_container_root(source_path: str) -> str:
+    for root in CONTAINER_ROOTS:
+        if source_path.startswith(root):
+            return source_path[len(root):]
+    return source_path
+
+
+def is_dependency_path(source_path: str) -> bool:
+    p = _strip_container_root(source_path).lstrip("./")
+    return any(p.startswith(m) or f"/{m}" in p for m in DEPENDENCY_MARKERS)
+
+
+@dataclass
+class AnalysisContext:
+    project_root: Path
+    dumps: list[AstDump]
+    _sources: dict[str, SourceUnit] = field(default_factory=dict, init=False)
+    _line_tables: dict[str, list[int]] = field(default_factory=dict, init=False)
+    _source_texts: dict[str, Optional[bytes]] = field(default_factory=dict, init=False)
+    unparsed_source_count: int = field(default=0, init=False)
+
+    def __post_init__(self) -> None:
+        for dump in self.dumps:
+            for _, source in dump.iter_sources():
+                if source.root is None:
+                    self.unparsed_source_count += 1
+                elif source.source_path not in self._sources:
+                    self._sources[source.source_path] = source.root
+
+    # ---- source iteration -------------------------------------------------
+
+    def iter_sources(self, *, include_dependencies: bool = False) -> Iterator[tuple[str, SourceUnit]]:
+        for path, root in self._sources.items():
+            if include_dependencies or not is_dependency_path(path):
+                yield path, root
+
+    def iter_contracts(
+        self, *, include_dependencies: bool = False
+    ) -> Iterator[tuple[str, ContractDefinition]]:
+        for path, root in self.iter_sources(include_dependencies=include_dependencies):
+            for contract in find_all(root, ContractDefinition):
+                yield path, contract
+
+    def iter_functions(
+        self, *, implemented_only: bool = True, include_dependencies: bool = False
+    ) -> Iterator[tuple[str, ContractDefinition, FunctionDefinition]]:
+        """(source_path, contract, function) over contract members (not free functions)."""
+        for path, contract in self.iter_contracts(include_dependencies=include_dependencies):
+            for node in contract.nodes:
+                if isinstance(node, FunctionDefinition) and (node.implemented or not implemented_only):
+                    yield path, contract, node
+
+    # ---- source text / line mapping --------------------------------------
+
+    def display_path(self, source_path: str) -> str:
+        """Project-relative path for reports (falls back to the raw dump path)."""
+        stripped = _strip_container_root(source_path)
+        if stripped != source_path:
+            return stripped
+        try:
+            return str(Path(source_path).resolve().relative_to(self.project_root.resolve()))
+        except ValueError:
+            return source_path
+
+    def _text(self, source_path: str) -> Optional[bytes]:
+        if source_path not in self._source_texts:
+            candidate = self.project_root / _strip_container_root(source_path)
+            self._source_texts[source_path] = (
+                candidate.read_bytes() if candidate.is_file() else None
+            )
+        return self._source_texts[source_path]
+
+    def offset_to_line(self, source_path: str, byte_offset: int) -> int:
+        """1-based line for a solc src byte offset; 0 when the source file is
+        unavailable (evidence stays usable, just without a line anchor)."""
+        text = self._text(source_path)
+        if text is None:
+            return 0
+        if source_path not in self._line_tables:
+            starts = [0]
+            for i, b in enumerate(text):
+                if b == 0x0A:
+                    starts.append(i + 1)
+            self._line_tables[source_path] = starts
+        starts = self._line_tables[source_path]
+        # binary search: number of line starts <= offset
+        lo, hi = 0, len(starts)
+        while lo < hi:
+            mid = (lo + hi) // 2
+            if starts[mid] <= byte_offset:
+                lo = mid + 1
+            else:
+                hi = mid
+        return lo
+
+    def line_span(self, source_path: str, byte_offset: int, byte_length: int) -> int:
+        """Number of source lines a node covers (0 when the source is unavailable)."""
+        text = self._text(source_path)
+        if text is None:
+            return 0
+        return text[byte_offset : byte_offset + byte_length].count(b"\n") + 1

certora_autosetup/amenability/judge/__init__.py

@@ -0,0 +1,6 @@
+"""Phase-2 LLM judge: a single structured call over the static report + code
+excerpts, clamped to ±1 level of the static provisional score."""
+
+from certora_autosetup.amenability.judge.agent import JudgeError, judge_report
+
+__all__ = ["judge_report", "JudgeError"]