autosetup: never emit a conf with both solc and compiler_map#88
autosetup: never emit a conf with both solc and compiler_map#88shellygr wants to merge 2 commits into
Conversation
certoraRun rejects a conf carrying a per-contract map next to its scalar
counterpart ("compiler map flags cannot be set with other compiler flags"),
and the rejection happens before any solc invocation, so no compilation
workaround can detect it — every retry resends the same invalid conf.
Add ConfigManager.drop_scalars_superseded_by_maps (all four scalar/map
pairs) and call it at each conf mutation boundary:
- _precompute_compiler_settings, after building compiler_map from build
artifacts (previously the build system's scalar solc survived next to it)
- _seed_compile_maps, which now always folds a scalar into the map as the
default for uncovered contracts instead of only when the map is absent
- get_build_system_config_dict_with_updates, replacing its hand-rolled
solc_via_ir/solc_optimize pops
Workaround-loop gates made map-aware accordingly:
- solc_not_found_fallback arms on a compiler_map pin, not only scalar solc
- yul_exception_add_optimizer skips when a project solc_optimize_map is
present (the scalar cannot legally sit next to it); the escalation rung
treats the map as "optimizer already tried"
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
| # solc_optimize_map counts as "optimizer already tried": it is | ||
| # project-configured, and the add rung never fires next to it. | ||
| detect_fn=lambda output: ( |
There was a problem hiding this comment.
i'm worried about this change as we could have it misconfigured for one of the contracts in the map.
There was a problem hiding this comment.
Claude answers: Valid concern — an entry in the map can be missing or "0" (optimizer off for that contract), and the previous revision would have skipped straight to relaxing the autofinder assertion without ever trying to enable it. Reworked in 9424974: the add-optimizer rung is now per-contract-aware — with a solc_optimize_map present it enables exactly the entries whose optimizer is off (missing/"0"), keeping explicit project runs values untouched and never setting the scalar next to the map. The escalation rung fires only once the optimizer is on globally or for every scene contract; one predicate (_yul_optimizer_pending) drives both rungs as complements, so there is no gap or overlap between them. Regression tests cover both the all-entries-on case (escalate) and the misconfigured-entry case (fill "0"→"200", keep "1", then escalate only if the error persists).
| # convert_to_compiler_map for solc/compiler_map, check_map_attributes for | ||
| # the rest), so a map always supersedes its scalar counterpart. | ||
| SCALAR_TO_MAP_KEYS = ( | ||
| ("solc", "compiler_map"), |
There was a problem hiding this comment.
may make sense to import names from certora-cli package
There was a problem hiding this comment.
Claude answers: I looked into importing them: the names live in certora_cli.CertoraProver.certoraContextAttributes (EvmProverAttributes.SOLC.get_conf_key() etc.), but that module isn't cleanly importable from library code — certora_cli's internals use flat imports (from Shared import ...), so reaching it requires inserting the certora_cli package dir into sys.path (shadow risk for generic top-level names like Shared) and calling Attrs.set_attribute_class(EvmProverAttributes), a process-global. I didn't want either as a runtime side effect of importing enhanced_config_manager. Compromise in 9424974: the pairs stay literal, and a new test (test_scalar_to_map_keys_match_certora_cli) resolves every name against the installed CLI's attribute definitions in a subprocess — an upstream rename/removal fails the suite instead of silently desyncing. If you'd rather have the runtime import anyway, say the word and I'll wire it with the sys.path shim.
… certora-cli A solc_optimize_map entry that is missing or "0" means the optimizer is off for that contract — exactly what the add-optimizer rung exists to fix. It now enables those entries in the map (keeping explicit project runs values, never setting the scalar next to the map) instead of skipping the whole rung; the escalation rung fires only once the optimizer is on globally or for every scene contract. One predicate (_yul_optimizer_pending) drives both rungs as complements. SCALAR_TO_MAP_KEYS stays literal — importing the names from certora_cli needs its package dir on sys.path (its modules use flat internal imports) plus the set_attribute_class() global, both unwanted at runtime — and is instead pinned against the installed CLI's attribute definitions by a subprocess test. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
1 participant
Problem
Autosetup can generate certoraRun confs that carry BOTH a scalar
solcand a per-contractcompiler_map. certora-cli hard-rejects the pair:Observed on foundry projects whose build artifacts were produced with a different solc than the
foundry.tomlpin (_precompute_compiler_settingsmaps every contract to the artifact version while the build system's scalarsolcstays in the conf).🤖 Generated with Claude Code