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