Support verifying a library main contract via a generated harness

[shellygr]

Why

The Prover cannot verify a library as the verification target, and fails silently — there is no error anywhere in certora-cli or the JVM. CalculateMethodParamFilters.kt:182 filters libraries out of parametric rules, so the run reaches the prover, instantiates zero methods, and comes back vacuous.

The Prover itself prescribes the fix: "Calling Library functions from spec is not supported. Use a harness function that calls the library one if needed." This automates it.

How

New certora_autosetup/harnesser/ package. Everything completes before Autosetup.run starts:

detect contractKind == library
  → emit a stub harness in certora/harnesses/
  → probe-build it WITH the library in `files`
  → read the library's allMethods
  → refill the harness, drop the placeholder
  → swap the main contract
AutoSetup then runs once, normally.

Three findings shaped this, each verified against real builds:

• The library must be listed in the conf's files. An imported-but-unused library is not compiled as its own contract — the build reports its structs and none of its functions.
• The API comes from allMethods, not internalFunctions. The latter is autofinder instrumentation, and certora-cli skips autofinders for library-hosted functions (certoraBuild.py:2751), so it is systematically empty for libraries. Reading it yields zero wrappers for a library whose surface is all-internal.
• The fill is not re-entrant into autosetup. setup_prover.py:327 re-seeds from the base build-system dict, so a second run_compilation_analysis would discard every workaround from the first; and a swap inside setup_prover cannot propagate (it returns no handle, ContractHandle is frozen).

Detection uses solc --standard-json with stopAfter: "parsing" — real AST, no build, no import resolution, milliseconds. It keys on contractKind, never on a message, since there is no message.

Codegen

Storage receivers become harness-owned state; CVL keywords are escaped before ABI-collision mangling (at → at_, then suffixed); collision suffixes come from the dropped receiver keyed positionally (overloads share a name); storage readers reach through nested structs and mappings; in-place memory mutators get a synthesized return.

Skipped and reported, not silently dropped: private, storage-pointer returns, internal-only types, opaque bytes32 ptr handles. Zero surviving wrappers is a hard error — a method-less target proves nothing.

Coverage

Matches hardhat-exposed's independent counts where they overlap:

Library	Wrapped
OZ Math	14/14
OZ EnumerableSet	18/24	6 private
OZ Checkpoints	20/33	incl. the function-type push
OZ StorageSlot	refused	all 8 return storage pointers
Solady LibBitmap	10/10
Solady LibSort	57/68	in-place mutators
Solady EnumerableSetLib	45/51	both utils/ and g/

Validation

Full local autosetup on OZ EnumerableSet: emits a conf whose verify and parametric_contracts are CertoraLibraryHarness_EnumerableSet, typechecker passes, local prover run succeeds, certoraRun --compilation_steps_only exits 0. A/B against OpenZeppelin's hand-written EnumerableSetHarness.sol — the generated names now read add/remove/contains/at_Bytes32Set/Bytes32Set_inner_indexes against the human's add/remove/contains/at_/_indexOf; the remaining differences are the two extra set types the human harness does not cover.

Tests live in the Autosetup repo (29 unit tests over real trimmed build fixtures); needs a submodule pin bump there once this merges.

Known limitation

Solady's EnumerableSetLib sets are struct { uint256 _spacer; } with assembly-derived slots, so the owned state variable may not model where the data actually lives. Treat its 45/51 as unproven until a prover run confirms it.

🤖 Generated with Claude Code

[shellygr]

to Claude: I'm surprised we don't have such a utility function yet

[jar-ben]

+1 on this question

[jar-ben]

btw, autosetup uses the ContractHandle class

[shellygr]

Claude answers: we do. split_contract_spec in utils/contract_utils.py, and _split_target was a near duplicate of it. The CLI calls it now, and --extra-file goes through parse_contract_files, so a typo fails at parse time instead of as a probe build error minutes later.

[shellygr]

Claude answers: it does exist, split_contract_spec in utils/contract_utils.py. The CLI uses it now.

[shellygr]

Claude answers: done. ContractHandle carries the library and the harness through cli, run, plan, model and swap, so the (file, name) string pairs are gone.

Two places kept their current shape on purpose: the manifest still writes four flat JSON keys, because swap.library_behind_harness reads it back in a later process, and the probe build still spells the explicit :Name, which is what tells apart a file declaring several libraries.

[shellygr]

@jar-ben before I push forward on this - does this conflict with your work on symbolic modeling? if yes maybe we should discuss merging in together

[jar-ben]

Don't talk about AutoProver here. That's just one of the possible consumers of this tool. Just describe what the tool does and how to use it.

[shellygr]

Claude answers: done. The docstring now says what the tool does and shows the invocation, with no consumer named.

[jar-ben]

+1 on this question

[jar-ben]

btw, autosetup uses the ContractHandle class

[jar-ben]

Double check we don't have this defined somewhere in AutoProver yet. I am sure I saw a list like this (perhaps just a sublist, but if yes, it could be good to centralise similar frozen lists / enums to a single location)

[shellygr]

Claude answers: you did see it. CVL_RESERVED_WORDS was already in setup/setup_summaries.py with 60 words, and this branch added a second one of 82 under the same name. Both are gone; there is one list now, in utils/cvl_keywords.py.

The 22 extra words were also wrong. 20 of them are the grammar's usable_keywords, which CVL accepts wherever an identifier is expected. I checked with certoraRun --compilation_steps_only: a contract declaring exists, sum, old, forall and invariant typechecks, the same shape with havoc or rule is a syntax error. No generated name changes as a result, since at and sort are the only escapes real libraries trigger.

[jar-ben]

How about we reuse (or create if not existing) an AST manipulation utils in Autoprover? This seems like a pretty common function.

[shellygr]

Claude answers: moved to solidity_ast/contracts.py. It is now the one place that turns a ContractDefinition into name, kind, abstract and bases, for both the post-build .asts.json stream and this pre-build probe, and setup_prover's private _ContractDeclView / _iter_contract_declarations moved there with it. Kinds come back as ContractKind instead of raw strings.

One thing I could not do is read the probe's AST through the typed models. A stopAfter: "parsing" AST carries no analysis-phase fields (no scope, no linearizedBaseContracts, no fullyImplemented), so SourceUnit.model_validate fails on it with 16 errors on a two-declaration file. That entry point stays on raw nodes, and the module says why.

[jar-ben]

I am almost sure I have seen this somewhere. again seems like a shared util

[shellygr]

Claude answers: you have. That loop was written five times. It is now utils/build_json.py (build_json_path, iter_contracts, contract_source_file), used by setup_prover in four places, by signature_manager, by compile_check and here. The path .certora_internal/latest/.certora_build.json was hardcoded in three of them and is now in one, with compile_check's newest-run-dir fallback folded in.

[jar-ben]

So, I wanted to suggest to use ContractHandle already above (perhaps in cli.py) when you had a separated library name and path, but then thought that "well, it's not a contract so perhaps ContractName is not the right naming". But here, you use it. so use it everywhere perhaps.

[jar-ben]

btw I know you have to use it here because it's the autosetup's interface. but the argument still mostly stands

[shellygr]

Claude answers: done, it is ContractHandle through the harnesser now, starting at the CLI.

[shellygr]

Claude answers: agreed, and the argument held. See the reply above.

[jar-ben]

ContractHandle would solve this? maybe

[shellygr]

Claude answers: yes. The dedup builds handles and compares those, rather than comparing (path, name) tuples.

[jar-ben]

wrongly named parameter. Instead of harnessed_library, we should call it excluded_library or something like that. Or perhaps not even library, just excluded. This seems to be a generic filter; the fact that we apply it on the harness library is just a matter of the consumer of run_setup_summaries. Similarly, drop the "harness" specific naming and comments in certora_autosetup/setup/setup_summaries.py

[shellygr]

Claude answers: renamed to excluded_library, with _excluded_library_keys and _excluded_library_methods, and the harness-specific comments in setup_summaries.py now describe the filter instead of the caller. I kept library in the name because the filter selects curated summary keys by library name.

setup_prover keeps its harness wording at the call site, since that file calls library_behind_harness and legitimately knows what it is excluding and why.

[jar-ben]

how much is this change related to this PR?

[shellygr]

Claude answers: half of it belongs and half did not. parent_name: Optional[str] is needed here: a library cannot be a base contract, so the harness holds it at arm's length and passes None, which without this change renders contract X is None {. extra_pragma_lines was speculative, nothing ever populated it, and it is gone from the branch.

[shellygr]

Claude answers: the review is addressed, in two commits, with a reply on each thread.

c036c786 puts the CVL keyword list in one place. There were two constants named CVL_RESERVED_WORDS, and the harnesser's copy also escaped the 20 usable_keywords terminals, which CVL accepts where an identifier is expected.

71389a8c moves out what the harnesser had written for itself: solidity_ast/contracts.py for reading contract declarations and their kind, utils/build_json.py for the walk over .certora_build.json that was written five times, ContractHandle in place of the (file, name) string pairs, and excluded_library instead of harnessed_library. It also drops extra_pragma_lines, which was plumbed end to end and never populated.

Two things stayed where they are, with the reasoning on the threads: model.py and plan.py hold the harnesser's own plan and decision logic, and nothing else in the repo consumes them; and the pre-build probe reads raw AST nodes rather than the typed models, because a stopAfter: "parsing" AST has none of the analysis-phase fields the models require.

Generated output is unchanged. Regenerating a 65-wrapper harness gives a byte-identical file and the same manifest, and no wrapper name in any fixture is one of the keywords that stopped being escaped.

[shellygr]

Claude answers: also re-ran the feature end to end on the refactored code, on a library main contract. AutoSetup swaps in the generated harness, puts the library in the conf's scene once, drops the curated summary that would have replaced it (Not summarizing BitMaps, it is the library under verification), and the cloud prover job comes back successful.

[shellygr]

Claude answers: checked the other libraries on the refactored code too.

• EnumerableSet as the main contract: AutoSetup exits 0, 60 of 72 functions wrapped (same as before), the library and its two dependencies are in the conf's scene, and the cloud prover job completes.
• SafeCast and ABDKMath64x64: harness regenerated byte-identical, 65/65 and 25/27, same manifests and same plan hashes.

ABDK cannot go through AutoSetup locally, since that repo has no build system for the detector to find. That is not new here.

[jar-ben]

minor comments

[jar-ben]

Five places used to walk
that structure with their own nesting checks and their own idea of where the file
lives, which is one place to get it wrong per caller.

drop that part

[shellygr]

Claude answers: dropped. Only the first paragraph is left, describing the file's shape.

[jar-ben]

(16 errors on a two-declaration file)
seems like particular test specific output, i.e. drop

Also, this whole paragraph seems like it should not be here. Don't discuss users, just say what contracts.py introduces.

[shellygr]

Claude answers: rewritten. It now names what the module offers and stops there:

Contract declarations and their kind, from either shape of solc AST.

ContractDeclView is the uniform view. iter_contract_declarations reads it from the typed models over an AstDump stream. parse_only_declarations reads it from the raw nodes of a stopAfter: "parsing" AST, which the typed models reject: solc emits no analysis-phase fields (scope, linearizedBaseContracts, fullyImplemented) at that stage.

I kept that last clause because it is the only reason there are two entry points instead of one. The error count is gone.

[jar-ben]

What if there is a nested repeated folder structure, e.g. nested .certora_sources? That also applies to strip_sources_anchor. Perhaps if we have get_sources_anchor(path) that either gives us the anchor if presented or None, then we can in same_source_file say that candidate and wanted are the same if either they are string equal or if one of them has anchor and removing the anchor prefix yields the other one?

[shellygr]

Claude answers: good question, and chasing it produced a better answer than the helper. The anchor strip cannot affect same_source_file at all: it removes leading components, and the comparison is on trailing ones. I ran your nested case through it, .certora_sources/vendor/.certora_sources/contracts/A.sol, along with the absolute and instrumented-copy shapes, and the result is the same with and without the strip in every one.

So the fix is subtraction rather than get_sources_anchor: same_source_file keeps only the suffix comparison, and strip_sources_anchor is gone from paths.py. There are now unit tests for those shapes in the Autosetup PR.

I also put compile_check's _strip_anchor back where it was. Merging it into paths.py was my mistake: _is_touched is directional and length-sensitive, so it only resembles same_source_file. That file keeps the one change that is real reuse, build_json_path.

On the equality-modulo-anchor shape you suggested: it would reject the case this function exists for, a build reporting one file as /abs/proj/contracts/A.sol and the other as contracts/A.sol. The suffix rule is loose in the other direction, A.sol matches contracts/A.sol, which the caller bounds by also requiring the contract name to match. Tightening it properly means normalizing both sides to project-relative where the paths are produced. Worth doing, but bigger than this PR.