Honor the project-declared EVM version + Yul-steps escalation rung

certora_autosetup/autosetup/autosetup.py

@@ -57,6 +57,36 @@
 COMPONENT = "Autosetup"
 
 
+def _reconcile_evm_version_keys(
+    config: Dict[str, Any],
+    updates: Dict[str, Any],
+    contract_names: List[str],
+) -> None:
+    """Reconcile solc_evm_version / solc_evm_version_map in a merged conf, in place.
+
+    The compilation updates started as a superset of the base build-system conf,
+    so when they carry neither the scalar nor the map, the invalid_evm_version
+    workaround removed the declared version — drop the base-re-emitted scalar
+    rather than resurrect a rejected setting. When the map is present it
+    supersedes the scalar (the prover forbids both), but must cover every
+    contract: extend it with the declared scalar for contracts it misses (e.g. a
+    cancun override plus the project-declared version for the rest).
+    """
+    if (
+        updates
+        and "solc_evm_version" not in updates
+        and "solc_evm_version_map" not in updates
+    ):
+        config.pop("solc_evm_version", None)
+    if "solc_evm_version_map" in config:
+        declared = config.pop("solc_evm_version", None)
+        if declared:
+            config["solc_evm_version_map"] = {
+                **{name: declared for name in contract_names},
+                **config["solc_evm_version_map"],
+            }
+
+
 class Autosetup:
     """Execute the autosetup phase and return an AutosetupResult.
 
@@ -434,6 +464,12 @@ def get_build_system_config_dict_with_updates(self) -> Dict[str, Any]:
         if "solc_optimize_map" in config:
             config.pop("solc_optimize", None)
 
+        _reconcile_evm_version_keys(
+            config,
+            self.compilation_config_updates,
+            [ch.contract_name for ch in self.contract_handles],
+        )
+
         # Filter per-contract maps to only include contracts in self.contract_handles
         contract_names = {ch.contract_name for ch in self.contract_handles}
         for map_key in ("compiler_map", "solc_via_ir_map", "solc_evm_version_map", "solc_optimize_map"):

certora_autosetup/build_systems/base.py

@@ -29,6 +29,9 @@ class BuildSystemConfig(ABC):
     optimizer: Optional[bool] = None
     optimizer_runs: int = 200
     via_ir: Optional[bool] = None
+    # Declared EVM target (foundry `evm_version`, hardhat `settings.evmVersion`);
+    # None means each solc's own default.
+    evm_version: Optional[str] = None
 
     # Common source configuration
     src: Optional[str] = None
@@ -55,6 +58,7 @@ def to_certora_dict(
                 "solc": "solc8.24",  # or "0.8.24" if convert_solc=False
                 "solc_optimize": 200,
                 "solc_via_ir": true,
+                "solc_evm_version": "paris",  # only when the project declares one
                 "packages": [...]
             }
         """
@@ -137,6 +141,16 @@ def _apply_common_solc_settings(
         if self.via_ir:
             result["solc_via_ir"] = True
 
+        # Honor the project's declared EVM target. Unlike the optimizer setting
+        # above, this is not a tuning knob: solc's default EVM version can be
+        # NEWER than the declared one (e.g. shanghai/PUSH0 vs a pinned "paris"),
+        # producing bytecode for the wrong chain and different codegen (which can
+        # even fail where the declared target compiles), and no reactive
+        # workaround could guess the intended version. If the declared version is
+        # rejected by the solc in use, the invalid_evm_version workaround drops it.
+        if self.evm_version:
+            result["solc_evm_version"] = self.evm_version
+
         return result
 
     def _relativize_packages(

certora_autosetup/build_systems/foundry.py

@@ -63,7 +63,7 @@ def __post_init__(self):
         if self.restriction_manager is None:
             # No restrictions → apply_restrictions short-circuits, so the
             # defaults here are never consulted; we still pass optimizer_runs
-            # for consistency. (evm_version isn't a FoundryConfig field.)
+            # for consistency.
             self.restriction_manager = FoundryRestrictionManager(
                 restrictions=[], # No restriction means no effect of apply_restrictions
                 default_via_ir=bool(self.via_ir) if self.via_ir is not None else False,
@@ -221,6 +221,7 @@ def _extract_profile_config(self, foundry_data: Dict[str, Any], profile: str) ->
             optimizer=optimizer_settings["enabled"],
             optimizer_runs=optimizer_settings["runs"],
             via_ir=via_ir,
+            evm_version=profile_data.get("evm_version"),  # Will be None if not specified
             src=profile_data.get("src"),  # Will be None if not specified
             out=profile_data.get("out"),  # Will be None if not specified
             libs=profile_data.get("libs"),  # Will be None if not specified
@@ -278,6 +279,7 @@ def _merge_configs(self, base: FoundryConfig, override: FoundryConfig) -> Foundr
             optimizer=override.optimizer if override.optimizer is not None else base.optimizer,
             optimizer_runs=merged_optimizer_runs,
             via_ir=merged_via_ir,
+            evm_version=override.evm_version or base.evm_version,
             src=override.src or base.src,
             out=override.out or base.out,
             libs=override.libs or base.libs,
@@ -463,13 +465,13 @@ def apply_restrictions(
                 "FoundryRestrictionManager",
             )
 
-        # NOTE: per-path evm_version is intentionally NOT emitted. The prover
-        # requires solc_evm_version_map to be total, so unmatched contracts
-        # would have to be filled with the profile-level evm_version (e.g.
-        # "prague") — which breaks older-solc files that don't support it
-        # (solc 0.8.25 rejects "prague"). Leaving evm_version unset lets each
-        # contract use its solc's own default, which is always compatible — the
-        # behaviour that worked before per-path evm_version was introduced.
+        # NOTE: per-path evm_version from compilation_restrictions is
+        # intentionally NOT emitted. The prover requires solc_evm_version_map to
+        # be total, so unmatched contracts would have to be filled with a
+        # concrete version even where the project relies on each solc's own
+        # default. The PROFILE-level evm_version is honored separately (emitted
+        # as scalar solc_evm_version by _apply_common_solc_settings and dropped
+        # by the invalid_evm_version workaround if a solc rejects it).
 
         # ---------------- solc_optimize map ----------------
         restricted_optimize = self._optimize_map(contracts)

certora_autosetup/build_systems/hardhat.py

@@ -278,6 +278,7 @@ def _extract_config_from_json(self, config_data: Dict[str, Any], config_type: st
             optimizer = False
             optimizer_runs = 200
             via_ir = False
+            evm_version = None
         elif isinstance(solidity, dict):
             # Hardhat config structure: {"compilers": [{"version": "0.8.28", "settings": {...}}], ...}
             # Or simple format: {"version": "0.8.28", "settings": {...}}
@@ -309,11 +310,13 @@ def _extract_config_from_json(self, config_data: Dict[str, Any], config_type: st
             optimizer = optimizer_settings.get("enabled", False)
             optimizer_runs = optimizer_settings.get("runs", 200)
             via_ir = settings.get("viaIR", False)
+            evm_version = settings.get("evmVersion")
         else:
             solc_version = None
             optimizer = False
             optimizer_runs = 200
             via_ir = False
+            evm_version = None
 
         # Extract and process paths
         paths = config_data.get("paths", {})
@@ -340,6 +343,7 @@ def _extract_config_from_json(self, config_data: Dict[str, Any], config_type: st
             optimizer=optimizer,
             optimizer_runs=optimizer_runs,
             via_ir=via_ir,
+            evm_version=evm_version,
             src=src,
             artifacts=artifacts,
             cache=cache,

certora_autosetup/build_systems/hardhat_config_extractor.js

@@ -27,11 +27,16 @@ try {
     if (hasTypeScriptConfig) {
         try {
             // Register ts-node with transpileOnly to skip type checking
-            // This allows loading TypeScript configs even if the project has type errors
+            // This allows loading TypeScript configs even if the project has type errors.
+            // moduleResolution must be overridden together with module: forcing
+            // commonjs while the project's tsconfig pins moduleResolution
+            // "nodenext"/"node16" is rejected by TypeScript (TS5110) even in
+            // transpileOnly mode, losing the whole config.
             require('ts-node').register({
                 transpileOnly: true,
                 compilerOptions: {
-                    module: 'commonjs'
+                    module: 'commonjs',
+                    moduleResolution: 'node'
                 }
             });
         } catch (tsError) {

certora_autosetup/fixconf.py

@@ -33,7 +33,7 @@
 # Build system keys that should be stripped from the output if the user's original conf didn't have them.
 # These are low-priority settings that can break the prover (e.g. solc_optimize with a huge value from foundry.toml).
 # High-priority keys like solc and packages are kept since they're often needed for compilation.
-_LOW_PRIORITY_BS_KEYS = {"solc_optimize", "solc_via_ir"}
+_LOW_PRIORITY_BS_KEYS = {"solc_optimize", "solc_via_ir", "solc_evm_version"}
 
 
 class _AcceptAllScope: