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. The loop remembers the states it has compiled. _retry_state already serializes the command
and both conf dicts, and already carries the invariant that makes this sound: an apply that makes
real progress must change one of them. The loop keeps every state it has run and gives up when one
comes round again, which subsumes the old "this pass changed nothing" guard. One check, not two.

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

What replaced the change ledger, and why

The first version of fix 2 was a change ledger: every apply recorded (workaround, conf delta), and
a pass whose changes had all been made before stopped the loop. @jar-ben asked why the criterion was
not simply "stop when a normalized conf repeats". Investigating that turned up two problems with the
ledger, both measured against the real workaround table:

• It could give up on a conf that compiles. Once compiler_version_mismatch bumps the compiler,
  cancun_opcode_evm_version re-adds an identical delta and the pass looks like pure repetition. The
  ledger stops at 3 compiles; the state memo reaches that conf and compiles it on the 4th. Whether a
  compiler rejects cancun depends on which compiler compiler_map pins, and two other workarounds
  write that field, so this is reachable rather than theoretical.
• Its cost scaled with the contract count on the case it was written for. The fallback replaces
  every entry pinned to the missing binary in one apply, while the mismatch detector re-pins one
  contract per pass, so the fallback's delta differs every pass. For 1, 3 and 6 pinned contracts the
  ledger needs 4, 8 and 14 compiles. The state memo needs 2, 3 and 3.

The state memo has the opposite failure mode: an orthogonal one-way change (a warning flag, an
optimizer rung) makes each state unique and buys the cycle one more pass. There are about eight such
keys, all one-shot, so that cost is a constant, and max_retries still bounds it.

Validation

• uv run --no-sync python -m pytest tests/ -m "not expensive" -q -> 518 passed, 9 skipped; pyright -> 0 errors
• new tests: the fallback plan (blocked pins, per-contract selection, unreadable and non-UTF-8
  pragmas, candidate ordering), the state memo stopping a cycle, an orthogonal change letting the
  loop continue, and the memo being scoped to one loop rather than to the manager
• the missing-library harness workaround now has a test of its own, since dropping the ledger removed
  the exemption it carried and nothing in tests/ exercised it
• the two failure modes above were reproduced end to end against the shipped module: the previously
  abandoned conf now compiles, and the incident converges in 2, 3 and 3 compiles at 1, 3 and 6
  pinned contracts

Known, not fixed here

missing_library_harness never regenerates a harness for a second library, and its _harnessed_libs
guard cannot bound the FooHarnessHarness cascade. Pre-existing and independent of these commits;
filed as #179.

[jar-ben]

Can you rename it e.g. to BlockedSolcPin? BlockedPin is quite generic

[shellygr]

Claude answers: renamed to BlockedSolcPin in e4ee229. UnsatisfiableSolcPinError already owned that spelling in the module, so it is the house form.

[jar-ben]

I don't like the name rewrites - how about compliant or something like that?

[jar-ben]

alright, after reading more of the codebase, rewrites makes some sense, but here it's still confusing, especially in connection with the comment saying:

rewrites covers the contracts an installed compiler can serve

[shellygr]

Claude answers: it is compliant now, in e4ee229, and the class docstring was rewritten so the prose and the field agree — it opens with what the plan is (which installed compiler, if any, stands in for the missing one at each contract pinned to it), then says compliant maps such a contract to an installed compiler its pragma admits and blocked holds the ones no installed compiler can serve. rewrites was describing the edit the apply performs on compiler_map, whereas the field is the decision, computed a stage earlier by a planner that writes nothing.

[jar-ben]

the comment describes more how the function is used rather than describing what the function does. Especially the second paragraph of the comment.

Saying it computes the diff and perhaps providing a particular small example would be better.

[shellygr]

Claude answers: that docstring is gone — _conf_delta and _flatten_conf were deleted along with the change ledger in e4ee229. See the reply on the convergence thread for why.

[jar-ben]

re-setting the same value of a particular conf field might still lead to a convergence assuming some of the other fields also changed, i.e. perhaps it would make sense to simply store all the already seemed "full" conf files (normalized ofc) and stop once we see a conf we have seen before? That's looser stopping criterion.

[shellygr]

Claude answers: you were right, and the ledger is gone as of e4ee229. The loop now keeps every state it has compiled and stops when one comes round again. _retry_state already serialized exactly that (cmd plus both conf dicts), and it already carried the invariant that makes the stop sound: an apply that makes real progress must change one of them. That also folds the old "this pass changed nothing" guard into the same check, so there is one criterion instead of two.

On your specific worry: the ledger did not actually have that hole. A repeat only stops the loop when nothing new landed in the same pass, so a re-set value riding along with other changes kept going. But looking for that scenario turned up two others that are real, both measured against the actual workaround table:

1. The ledger could give up on a conf that compiles. Once compiler_version_mismatch bumps the compiler, cancun_opcode_evm_version re-adds an identical delta and the pass looks like pure repetition. Ledger: gives up at 3 compiles. State memo: reaches that conf and compiles it on the 4th. "This solc rejects cancun" depends on which compiler compiler_map pins, and two other workarounds write that field, so it is reachable rather than theoretical.

2. The ledger's cost scaled with the contract count on the very case it was written for. _apply_solc_fallback_workaround replaces every entry pinned to the missing binary in one apply, while _detect_compiler_version_mismatch re-pins one contract per pass, so the fallback's delta is different every pass and the ledger cannot fire until the same contract comes round again. For 1, 3 and 6 pinned contracts: 4, 8 and 14 compiles. The state memo: 2, 3 and 3. The project that started this mixed pragmas across 53 files.

The looseness you named is real and it is the price: an orthogonal one-way change (a warning flag, an optimizer rung) makes each state unique and buys the cycle one more pass. There are about eight such keys, all one-shot, so it is a constant, and max_retries still bounds it. A false negative that costs a constant number of certoraRuns beats a false positive that abandons a conf which would have compiled.

One consequence worth flagging: dropping the ledger also drops the progress_outside_conf exemption missing_library_harness carried, and nothing in tests/ exercised that workaround at all, so it now has a test of its own. Reviewing it turned up a real defect there, filed separately as #179 — it never regenerates a harness for a second library, because the apply renames the consumer handle it would need to look up on the next firing.

[jar-ben]

I am surprised we did not have a pragma_admits function yet. are you sure it's not already existing somewhere? (I have not checked)

[shellygr]

Claude answers: checked, and no, it did not exist. What existed was the raw expression Version(v) in parse_pragma_constraint(spec) open-coded at four sites: solc_version_resolver.py:277 and :295 inside resolve_pragma_to_version, enhanced_config_manager.py:849, and certoraRunAutoSolc.py:85. Nothing in the installed certora-cli interprets a pragma at all (it only shells out to solc --version), and no semver library is a dependency — packaging is the only thing available.

Naming it is what buys the two things the fallback planner needs and that a caller-side membership test does not give you: None meaning 'spec not understood', never conflated with False, and a guard around Version(version), which raises on a non-PEP440 string. resolve_pragma_to_version cannot serve either, since it returns None both for an unparseable pragma and for 'no matching version found', and it fetches the version list over the network on the way.

parse_pragma_constraint stays public regardless: certoraRunAutoSolc.py:73-85 needs the SpecifierSet objects to intersect many pragmas against many versions. One follow-up worth doing separately: enhanced_config_manager.py:841-851 could drop its own inline membership test and call pragma_admits, which would make it the single entry point.

Unrelated find on the same function, fixed in e4ee229: the third docstring example claimed pragma_admits("~0.6.4", "0.6.4") returns None, but this branch added tilde parsing, so it returns True. It now shows the disjunction case instead, which is the real unknown.