autosetup: keep the named main contract in the scene

[shellygr]

The bug

certora-autosetup --main-contract <path>:<Name> can fail with

Main contract 'X' is not among the compiled contracts in the prover scene: [...].
Most often this means 'X' is abstract or an interface ...

for 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_contracts filters 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_handles keeps the shortest path per contract name, so a same-named
  contract elsewhere in the tree can displace the file the caller named.

cli.main never reconciled the two: contract_handles came from detection, main_contract_handle
was 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 by
definition. 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 bare path.sol spec resolves to the contract the file really
declares 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 fixes
a remapping-context defect in the same repo shape; both are needed for that layout to work.

[shellygr]

Full-corpus verification (313 projects, 569 contracts)

Cloud sweep full-2026-08-14 on master + #164 + this branch, PreAudit master; baseline
full-2026-08-07 (master @ Aug 1 + PreAudit @ Aug 1).

	baseline	this run
contracts ok	378 / 568 (66%)	390 / 569 (68%)
main-not-in-scene	41	0
missing-deps/submodule	28	54

main-not-in-scene is gone as a failure class. Most of those contracts do not turn green — they
move to missing-deps/submodule, which is the point: the main contract now reaches the compilation
conf, so the run fails (when it fails) on the project's actual missing dependencies instead of on a
scoping decision dressed up as a compilation error. 14 rows went failed → ok outright, 8 of them
from main-not-in-scene.

The nested-project corpus entry that motivated both PRs passes end-to-end through the ordinary
autosetup path, main contract included:

[209/569] ok   <entry>:<main contract under a bundle's dependencies/>   (473s)
[481/569] ok   <entry>:<sibling bundle contract>                        (318s)

3 regressions, none attributable to either PR:

• 2 × one project's contracts → missing-deps/submodule. Its import dep/src/contracts/…/Math.sol
  is now rewritten to node_modules/dep/src/contracts/src/contracts/… — a doubled prefix from a
  remapping forge remappings did not emit in the baseline. Cause is toolchain drift: the fleet
  image installs Foundry unpinned, so this image carries forge 1.8.0-nightly (2026-08-13) where the
  baseline image did not. No context-scoped remapping is involved and the contract was already in the
  detected scene, so neither PR is in the path.
• 1 × timeout at the 60-minute cap; a sibling contract in the same project took 58 minutes on this
  run, so it is the cap, not a new failure.

Caveat on attribution: the baseline image is two weeks older, so #114, #116, #83, PreAudit master and
the Foundry bump all ride along with these two PRs. Regressions are the trustworthy signal in that
kind of diff, and the three above are accounted for.

Separately worth pinning: the fleet image should fix a Foundry version, or every rebuild introduces
this class of confound.