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

[shellygr]

What

New module certora_autosetup/amenability/ + CLI certora-fv-amenability: score how amenable a Solidity project is to automatic formal verification with autosetup —

• low — needs a full reference implementation; a small rewrite won't suffice
• medium — scoped configuration/customization needed to get the automatic proof going
• high — expected to pass autosetup as-is

Phase 1 (this PR) is the deterministic static scorer. Phase 2 adds a graphcore-based LLM judge over a versioned rubric data file; phase 3 calibrates the weights against labeled autosetup outcomes. Both follow separately.

Note: branch is based on shelly/solidity-ast-pydantic (#76) — this PR builds on the typed AST package and should land after it.

How

Twelve signals over the typed compact AST (solidity_ast.find_all/walk), each a pure function AnalysisContext -> SignalResult with a score in [0,1] (1 = amenable), raw counters, and evidence carrying project-relative file:line:

signal	catches
asm_density	inline-assembly saturation
asm_fp_manipulation	mstore(0x40, …) — free-memory pointer as a first-class object
asm_trampoline	assembly/low-level delegatecall forwarding layers
bitmask_style	wide-mask bit surgery inline vs behind small internal accessors
function_length	150+-line functions (no divide-and-conquer seams)
unchecked_nonlinear	unchecked nonlinear arithmetic with symbolic operands
mixed_theory	bitvector + nonlinear ops interleaved in one function
curated_summary_hits	hand-rolled mulDiv/sqrt/… vs libraries with curated summaries (reads setup/function_summaries.json)
storage_packing	sload/sstore on computed slots (incl. via Yul locals) — hand-rolled layouts that break storage analysis
external_call_surface	low-level call counts / try-dispatch
dynamic_loops	storage-length- and symbolically-bounded loops
surface_shape	scene-size normalizers (weight 0)

Aggregation = weighted mean + hard rules (high-severity findings from FP-manipulation / trampoline / storage-packing cap the level at medium; N severe signals force low). All weights and thresholds live in weights.yaml — calibration never touches code.

Compiling is a hard precondition: the CLI takes --ast-dump (a certoraRun --dump_asts output) or discovers one under .certora_internal/; with neither it exits 1 with a distinct does-not-compile JSON error. There is deliberately no raw-source fallback.

Testing

• tests/test_amenability.py (19 tests) runs against a committed AST dump of a self-authored bait contract (tests/fixtures/amenability/signals_bait.sol): PackedBook trips every signal on purpose — each per-signal test asserts detection, evidence anchoring, and function attribution — while the CleanVault control (incl. the good accessor-encapsulated bit pattern) must produce zero evidence. Scoring hard rules and both CLI exits are covered end-to-end. Regenerate the dump with tests/fixtures/amenability/generate.py (dev-only).
• Validated on a real protocol of the motivating class (heavy assembly trampolines, hand-rolled packed storage, mixed-theory math, 500+-line functions — empirically un-provable without prover-flag surgery): scores low (0.12) with 87 evidence items pinpointing each pathology; the benign fixture scores high (0.94).
• pyright: 0 errors on the module.

🤖 Generated with Claude Code

[shellygr]

Pushed 562d63d — adds the mutual_recursion signal.

Why it exists. A prod project scored high (0.9766) from this scorer while the Prover could not ingest it at all: a vendored dependency implements a bytecode interpreter with two mutually recursive clusters entered from inside a bounded loop, and the decompiler unfolds each recursive entry to -recursionEntryLimit depth on every path. Confirmed causally — de-recursing that one file, with no other change and no prover flags, turns a job that fails in decompilation at 257s into one that succeeds at 653s with zero ERROR alerts.

What landed. callgraph.py builds the internal call graph per compilation unit (node ids collide across units) over the edges the decompiler actually inlines — internal/private calls, free functions, modifier bodies — and finds recursive clusters with an iterative Tarjan. signals/recursion.py scores each cluster on size, whether a call site into it sits in a loop, reachability from a public entry point, and how many distinct sites enter it. All eight curve constants are in weights.yaml.

Two ways it differs from the existing signals, both deliberate:

• It analyses dependencies. AnalysisContext.iter_* default to include_dependencies=False, so every other signal skipped the hazard — it was 252 SLOC of 9,905 (2.5%), under lib/. That blind spot is now measured, not asserted: the other 11 signals scored 1.000 or near it on a project that cannot be verified.
• It is a structural killer. A weighted mean cannot express "2.5% of the sources is fatal". On the reference project the mean is 0.8762, still above high_min 0.78 — the level moves to medium only because the veto fires.

56 public dump-free tests, pyright clean. Fixture-backed tests are in the private corpus (Certora/fv-amenability-tests#1, also draft, pinned at this commit).

Open before this leaves draft: a false positive that fires the veto on recursion-free code. Virtual dispatch is expanded per compilation unit rather than per deployable contract, so two sibling contracts overriding hooks of a shared abstract base get their edges welded into one graph — the template-method / OZ-hooks shape reads as a cycle. Reproduced and measured. The fix is to resolve each virtual call against one concrete contract's linearization and union the per-contract clusters; I did not do it unilaterally since it changes the module's core structure. It is recorded in the callgraph module's limitations docstring meanwhile.

I also fixed the adjacent false negative in the same area: override expansion was one level deep, so a grandchild override closing a loop-entered cycle was invisible. Now transitive.