autosetup: converge the compilation-workaround loop instead of timing out

[shellygr]

The incident

A corpus project mixing pragma solidity 0.6.4; (37 files) and 0.8.17 (16 files) burned a full
60-minute job timeout in the compilation-workaround loop without ever converging:

compiler_version_mismatch:  X requires 0.6.4              -> compiler_map[X] = solc6.4
solc_not_found_fallback:    Detected missing solc binary  -> falls back to solc8.34
compiler_version_mismatch:  X requires 0.6.4              -> compiler_map[X] = solc6.4
... 240 rounds, one certoraRun each

solc6.4 is not installed. The fallback was version-blind — it rewrote every contract pinned to the
missing binary to whatever compiler was default, with no reference to the pragma — so the
substitution could never compile and the mismatch detector re-pinned it every pass.

The existing guard could not see this: it compares a pass against its own starting state, so it
only catches a pass that changed nothing. Two workarounds that undo each other each change the conf
relative to their own baseline, and they alternate across passes.

The fixes

1. The fallback is a per-contract plan. Each contract pinned to the missing binary is offered
only compilers its pragma admits (pragma_admits -> True / False / None, where None means
the spec could not be parsed and is treated as no evidence). When a contract has no viable
substitute the run raises UnsatisfiableSolcPinError naming the contract, its pragma and the binary
to install, rather than retrying a substitution that cannot work.

2. A change ledger, as the general backstop. Every apply records (workaround, conf delta) for
the run. A pass whose changes have all been made before means something is undoing them, so the loop
stops and names them; a pass that also lands a new change is still converging. The delta deliberately
excludes the previous value — otherwise each half of an A-undoes-B cycle looks novel forever.

The regression test drives the real shape — missing pin, substitute, re-pin — with the pragma
unreadable so the pragma guard deliberately does not apply: 3 compiles instead of 273.

Review

An adversarial review of the first two commits confirmed six defects, all fixed in 311ea7e and
covered by tests: candidate ordering preferring an unrelated PATH solc over the project default; a
UnicodeDecodeError crash on a non-UTF-8 source; =X.Y.Z / ~X.Y.Z / disjunction pragma spellings;
the terminal raise firing on a pin autosetup seeded itself; certora-fixconf exiting on a traceback
and losing the fixes it had already written; and the ledger persisting across the two loop runs
fixconf makes on one manager.

Known, not fixed here

missing_library_harness cascades into nested FooHarnessHarness... harnesses when a link error
recurs, because its _harnessed_libs guard is keyed on the consumer name and the same apply replaces
that name with the harness's. It is bounded only by max_retries. Pre-existing and independent of
these commits (reproduced with the ledger disabled); the comment no longer claims that guard bounds
it. Worth its own change.

517 passed, 9 skipped; pyright clean.

🤖 Generated with Claude Code