autosetup: keep the named main contract in the scene - #165
Conversation
Two upstream steps can drop the contract the caller named. Auto-detection skips every file under a dependency directory (node_modules/, lib/, dependencies/, ...) — which is where per-address verification bundles and vendored sub-projects keep real, deployed code — and deduplication prefers the shortest path when two files declare the same contract name. The main contract then never reaches the compilation conf, and the run dies much later inside setup_prover with "'X' is not among the compiled contracts in the prover scene", a compilation message for what is really a scoping decision. with_main_contract() guarantees its presence, displacing a same-named handle from another file: the caller said which file it meant, and keeping both would put back the ambiguity dedup exists to remove. The main contract now also goes through the same artifact-backed name resolution as --contract-files-and-name, so a bare `path.sol` spec gets the contract the file really declares rather than the filename stem. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Full-corpus verification (313 projects, 569 contracts)Cloud sweep
The nested-project corpus entry that motivated both PRs passes end-to-end through the ordinary 3 regressions, none attributable to either PR:
Caveat on attribution: the baseline image is two weeks older, so #114, #116, #83, PreAudit master and Separately worth pinning: the fleet image should fix a Foundry version, or every rebuild introduces |
| return result | ||
|
|
||
|
|
||
| def with_main_contract( |
There was a problem hiding this comment.
Please rename the function to something like with_contract_handle and params handles and to_add. The functionality of this function is not specific to a "main" contract. Also, the comment should just describe what the functions does, i.e. adds handle if not already presented, and that it drops other handles that shared the .contract_name.
There was a problem hiding this comment.
Claude answers: Done in 1f1771f. It is now with_contract_handle(handles, to_add), and the docstring only describes behaviour: it returns the list with to_add appended if it is not already there, and drops any handle carrying the same contract_name but a different source file, so the returned list names each contract once. The reasoning about auto-detection skipping dependency directories and dedup preferring the shortest path moved to the call site in cli.py, which is the place that is actually about the main contract.
| f"— adding it to the scene", | ||
| "INFO", "Autosetup", | ||
| ) | ||
| contract_handles = with_main_contract(contract_handles, main_contract_handle) |
There was a problem hiding this comment.
tiny optimisation, but also more logical code - shouldn't we call with_main_contract only in the above if branch? i.e. when main_contract_handle not in contract_handles
There was a problem hiding this comment.
Claude answers: Moved inside the if. Same result either way, since the helper returns the list untouched when the handle is already present, but the call now sits next to the condition that explains it. 1f1771f
…lies The helper never depended on the handle being the main contract, so it is now with_contract_handle(handles, to_add) and its docstring says what it does: append the handle if it is missing, and drop any other handle carrying the same contract_name. Why the main contract can go missing belongs at the call site, where the main contract is what we are talking about, so that reasoning moved into cli.py. The call moved into the branch that already tests for absence: the helper returns the list untouched otherwise. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
2 participants
The bug
certora-autosetup --main-contract <path>:<Name>can fail withfor a contract that is neither abstract nor an interface, and that the build compiled
perfectly well. The message describes compilation, but the decision was made much earlier,
in scoping:
auto_detect_contractsfilters out every file whose path contains a dependency segment(
node_modules/,lib/,forge-std/,dependencies/,.git/—solidity_utils.py:13).That is right for third-party code and wrong for a repo that keeps deployed sources inside
a bundle directory, e.g. a soldeer-style
src/<Component>/dependencies/<pkg>/src/Foo.sol.deduplicate_contract_handleskeeps the shortest path per contract name, so a same-namedcontract elsewhere in the tree can displace the file the caller named.
cli.mainnever reconciled the two:contract_handlescame from detection,main_contract_handlewas parsed separately, and nothing guaranteed the second was in the first. Only the whole-scene
conf reached setup_prover, so the main contract was simply absent from
files.The fix
with_main_contract(handles, main_handle)— a contract the caller named is in scope bydefinition. It displaces a same-named handle from another file rather than sitting beside it:
the caller said which file it meant, and keeping both restores exactly the ambiguity dedup
exists to remove.
Also: the main contract now goes through the same artifact-backed name resolution as
--contract-files-and-name, so a barepath.solspec resolves to the contract the file reallydeclares instead of the filename stem — previously that mismatch produced the same late failure.
Tests
Three cases in
tests/test_contract_utils_nested_project.py: a main contract detection missed,a same-named handle displaced, and an already-detected main contract left untouched.
pytest -m "not expensive": 698 passed, 9 skipped.pyright: 0 errors.Found while running a repo with a nested Foundry project through the mass-test rig, where the
main contract lives under a bundle's
dependencies/directory. Independent of #164, which fixesa remapping-context defect in the same repo shape; both are needed for that layout to work.