From 2b17d28298838a55c6acbadde997363b55802f6e Mon Sep 17 00:00:00 2001 From: jar-ben Date: Wed, 22 Jul 2026 15:57:12 +0200 Subject: [PATCH 1/4] autosetup: don't inherit via_ir from the build system --- certora_autosetup/build_systems/base.py | 9 +++- certora_autosetup/build_systems/foundry.py | 63 ++-------------------- 2 files changed, 11 insertions(+), 61 deletions(-) diff --git a/certora_autosetup/build_systems/base.py b/certora_autosetup/build_systems/base.py index ae625269..e16085e8 100644 --- a/certora_autosetup/build_systems/base.py +++ b/certora_autosetup/build_systems/base.py @@ -133,9 +133,14 @@ def _apply_common_solc_settings( type(self).__name__, ) - # Apply via_ir + # via_ir is intentionally not inherited: viaIR inlines internal functions, which + # might prevent CVL internal summaries from being applied. if self.via_ir: - result["solc_via_ir"] = True + logger.log( + f"Ignoring {type(self).__name__}'s via_ir setting", + "INFO", + type(self).__name__, + ) return result diff --git a/certora_autosetup/build_systems/foundry.py b/certora_autosetup/build_systems/foundry.py index 7e55b79e..8fd1b18b 100644 --- a/certora_autosetup/build_systems/foundry.py +++ b/certora_autosetup/build_systems/foundry.py @@ -66,7 +66,6 @@ def __post_init__(self): # for consistency. (evm_version isn't a FoundryConfig field.) 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, default_optimizer_runs=self.optimizer_runs, ) @@ -213,7 +212,6 @@ def _extract_profile_config(self, foundry_data: Dict[str, Any], profile: str) -> via_ir = profile_data.get("via_ir") # Will be None if not specified restriction_manager = FoundryRestrictionManager( restrictions=list(profile_data.get("compilation_restrictions", [])), - default_via_ir=bool(via_ir) if via_ir is not None else False, default_optimizer_runs=optimizer_settings["runs"], ) return FoundryConfig( @@ -269,7 +267,6 @@ def _merge_configs(self, base: FoundryConfig, override: FoundryConfig) -> Foundr restriction_manager = FoundryRestrictionManager( restrictions=merged_restrictions, - default_via_ir=bool(merged_via_ir) if merged_via_ir is not None else False, default_optimizer_runs=merged_optimizer_runs, ) # For each field, use override value if it's not None, otherwise use base @@ -411,20 +408,17 @@ def filter_artifacts(self, artifacts_dir: Path) -> List[Path]: class FoundryRestrictionManager: """ This manager keeps information about restrictions from foundry.toml (defined in the section [profile.].compilation_restrictions). - These restrictions modify the `solc_via_ir_map` and `solc_optimize_map` - for specified contracts. (Per-path evm_version is intentionally not applied — - see the note in apply_restrictions.) + These restrictions modify the `solc_optimize_map` for specified contracts. + (Per-path via_ir and evm_version are intentionally not applied.) The manager also provides functionality for applying the restriction to a given certora conf file. """ def __init__( self, restrictions: List[Dict[str, Any]], - default_via_ir: bool = False, default_optimizer_runs: Optional[int] = None, ): self.restrictions = restrictions - self.default_via_ir = default_via_ir self.default_optimizer_runs = default_optimizer_runs def apply_restrictions( @@ -439,29 +433,8 @@ def apply_restrictions( if not self.restrictions: return config_dict - # ---------------- via_ir map ---------------- - restricted_via_ir = self._via_ir_map(contracts) - if restricted_via_ir: - existing_via_ir = config_dict.get("solc_via_ir_map", {}) - merged_via_ir = self._merge_via_ir_maps(existing_via_ir, restricted_via_ir) - uniform = self._uniform_value(merged_via_ir) - if uniform is not None: - # All contracts agree — collapse to the global flag. (solc_via_ir - # is only meaningful when True; all-False just means leave it off.) - config_dict.pop("solc_via_ir_map", None) - config_dict.pop("solc_via_ir", None) - if uniform: - config_dict["solc_via_ir"] = True - else: - config_dict.pop("solc_via_ir", None) - config_dict["solc_via_ir_map"] = merged_via_ir - enabled = sorted(n for n, v in merged_via_ir.items() if v) - logger.log( - f"Applied Foundry compilation_restrictions: viaIR enabled " - f"for {len(enabled)} contract(s): {enabled}", - "INFO", - "FoundryRestrictionManager", - ) + # per-path via_ir is intentionally not applied: viaIR inlines internal functions, + # which might prevent CVL internal summaries from being applied. # NOTE: per-path evm_version is intentionally NOT emitted. The prover # requires solc_evm_version_map to be total, so unmatched contracts @@ -505,18 +478,6 @@ def _uniform_value(mapping: Dict[str, Any]) -> Any: values = set(mapping.values()) return next(iter(values)) if len(values) == 1 else None - def _via_ir_map(self, contracts: List[ContractHandle]) -> Dict[str, bool]: - """Restricts per-contract solc_via_ir map. Empty when no rule addresses via_ir. - """ - matches = self._matching_rules(contracts) - if not any("via_ir" in r for rules in matches.values() for r in rules): - return {} - result: Dict[str, bool] = {} - for c in contracts: - value = self._first_key(matches.get(c.contract_name, []), "via_ir") - result[c.contract_name] = bool(value) if value is not None else self.default_via_ir - return result - def _optimize_map(self, contracts: List[ContractHandle]) -> Dict[str, int]: """Per-contract solc_optimize map. Empty when no rule sets a runs value. @@ -579,19 +540,3 @@ def _first_key(rules: List[Dict[str, Any]], *keys: str) -> Any: return r[k] return None - @staticmethod - def _merge_via_ir_maps( - existing: Dict[str, bool], restricted: Dict[str, bool] - ) -> Dict[str, bool]: - """Merge per-contract solc_via_ir maps with explicit priority. - It marges existing and restricted dir. In the end, it sets - items of existing that were false, to false again since these were - disabled because of old socl version (those compilers literally cannot use viaIR) - """ - merged = dict(existing) - merged.update(restricted) - for name, val in existing.items(): - if val is False: - merged[name] = False - return merged - From dc72fd908fa42760db1b30cf47122ddf6eeb1dc3 Mon Sep 17 00:00:00 2001 From: jar-ben Date: Wed, 22 Jul 2026 16:39:56 +0200 Subject: [PATCH 2/4] autosetup: add curated summaries for OZ Arrays, EIP-712 hashing, camelCase extSload --- .../certora/specs/summaries/EIP712.spec | 22 +++++++++++++++++++ .../summaries/OpenZeppelin/OZ_Arrays.spec | 9 ++++++++ .../specs/summaries/extload.template.spec | 3 +++ .../setup/function_summaries.json | 16 ++++++++++++-- 4 files changed, 48 insertions(+), 2 deletions(-) create mode 100644 certora_autosetup/certora/specs/summaries/EIP712.spec create mode 100644 certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_Arrays.spec diff --git a/certora_autosetup/certora/specs/summaries/EIP712.spec b/certora_autosetup/certora/specs/summaries/EIP712.spec new file mode 100644 index 00000000..a7365efa --- /dev/null +++ b/certora_autosetup/certora/specs/summaries/EIP712.spec @@ -0,0 +1,22 @@ +// EIP-712 typed-data hashing (solady `_hashTypedData`, OpenZeppelin `_hashTypedDataV4`). +// The digest is a keccak over the domain separator and the struct hash, whose assembly +// defeats the points-to analysis. It is modeled as a deterministic, injective +// uninterpreted function of the struct hash: sound, keeps equal struct hashes mapped to +// equal digests, and distinct struct hashes to distinct digests (collision-freedom, +// matching the optimistic-hashing assumption). +// +// Injectivity is encoded via a left-inverse ghost rather than a two-variable forall: +// recovering the struct hash from the digest is equivalent to injectivity (equal digests +// force equal struct hashes through the inverse) but quantifies one variable and applies +// the hash once, so the solver instantiates it linearly instead of over every pair. + +persistent ghost cvlHashTypedDataInv(bytes32) returns bytes32; + +persistent ghost cvlHashTypedData(bytes32) returns bytes32 { + axiom forall bytes32 s. cvlHashTypedDataInv(cvlHashTypedData(s)) == s; +} + +methods { + function EIP712._hashTypedData(bytes32 structHash) internal returns (bytes32) => cvlHashTypedData(structHash); + function EIP712._hashTypedDataV4(bytes32 structHash) internal returns (bytes32) => cvlHashTypedData(structHash); +} diff --git a/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_Arrays.spec b/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_Arrays.spec new file mode 100644 index 00000000..2297c2bc --- /dev/null +++ b/certora_autosetup/certora/specs/summaries/OpenZeppelin/OZ_Arrays.spec @@ -0,0 +1,9 @@ +// OpenZeppelin Arrays.unsafeMemoryAccess: an unchecked (assembly `mload`) memory +// array read whose raw pointer arithmetic defeats the points-to analysis. It reads +// the element at `pos` without a bounds check, so it is modeled as `arr[pos]` (the +// caller is responsible for `pos` being in bounds, matching the function's contract). +methods { + function Arrays.unsafeMemoryAccess(uint256[] memory arr, uint256 pos) internal returns (uint256) => arr[pos]; + function Arrays.unsafeMemoryAccess(bytes32[] memory arr, uint256 pos) internal returns (bytes32) => arr[pos]; + function Arrays.unsafeMemoryAccess(address[] memory arr, uint256 pos) internal returns (address) => arr[pos]; +} diff --git a/certora_autosetup/certora/specs/summaries/extload.template.spec b/certora_autosetup/certora/specs/summaries/extload.template.spec index 01fa6b1e..49c7bdfa 100644 --- a/certora_autosetup/certora/specs/summaries/extload.template.spec +++ b/certora_autosetup/certora/specs/summaries/extload.template.spec @@ -7,6 +7,9 @@ methods { function $CONTRACT_NAME$.exttload(bytes32 slot) external returns (bytes32) => NONDET DELETE; function $CONTRACT_NAME$.exttload(bytes32[] slots) external returns (bytes32[] memory) => ArbBytes32(slots) DELETE; function $CONTRACT_NAME$.exttload(bytes32[] slots) external returns (bytes memory) => ArbBytes(slots) DELETE; + // camelCase naming (e.g. Aave: extSload / extSloads) + function $CONTRACT_NAME$.extSload(bytes32 slot) external returns (bytes32) => NONDET DELETE; + function $CONTRACT_NAME$.extSloads(bytes32[] slots) external returns (bytes32[] memory) => ArbBytes32(slots) DELETE; } function ArbBytes32(bytes32[] slots) returns bytes32[] { diff --git a/certora_autosetup/setup/function_summaries.json b/certora_autosetup/setup/function_summaries.json index 221284b2..a066c2a0 100644 --- a/certora_autosetup/setup/function_summaries.json +++ b/certora_autosetup/setup/function_summaries.json @@ -107,10 +107,22 @@ "description": "OpenZeppelin BitMaps operations", "additional_contracts": ["specs/summaries/OpenZeppelin/harnesses/OZ_BitMaps.sol"] }, + "oz_arrays_unsafeMemoryAccess": { + "names": ["unsafeMemoryAccess"], + "library_names": ["Arrays"], + "summary_file": "specs/summaries/OpenZeppelin/OZ_Arrays.spec", + "description": "OpenZeppelin Arrays.unsafeMemoryAccess (unchecked memory array read)" + }, + "eip712_hashTypedData": { + "names": ["_hashTypedData", "_hashTypedDataV4"], + "library_names": ["EIP712"], + "summary_file": "specs/summaries/EIP712.spec", + "description": "EIP-712 typed-data hashing (solady _hashTypedData / OpenZeppelin _hashTypedDataV4)" + }, "extload": { - "names": ["extsload", "exttload"], + "names": ["extsload", "exttload", "extSload", "extSloads"], "summary_file": "specs/summaries/extload.template.spec", - "description": "External storage load functions (extsload/exttload)" + "description": "External storage load functions (extsload/exttload, incl. camelCase extSload/extSloads)" }, "safeTransfer": { "names": ["safeTransfer"], From 0fceab93db0ffd056358b9755f38844587182bbd Mon Sep 17 00:00:00 2001 From: jar-ben Date: Wed, 22 Jul 2026 22:22:29 +0200 Subject: [PATCH 3/4] autosetup: add curated summaries for the Aave math libraries --- .../specs/summaries/Aave/Aave_Math.spec | 35 +++++++++++++++++++ .../certora/specs/summaries/Math.spec | 19 ++++++++++ .../setup/function_summaries.json | 18 ++++++++++ 3 files changed, 72 insertions(+) create mode 100644 certora_autosetup/certora/specs/summaries/Aave/Aave_Math.spec diff --git a/certora_autosetup/certora/specs/summaries/Aave/Aave_Math.spec b/certora_autosetup/certora/specs/summaries/Aave/Aave_Math.spec new file mode 100644 index 00000000..3bb9a1dc --- /dev/null +++ b/certora_autosetup/certora/specs/summaries/Aave/Aave_Math.spec @@ -0,0 +1,35 @@ +// Curated summaries for the Aave fixed-point math libraries (WadRayMath, PercentageMath, +// MathUtils). All three compute x*y in a single 256-bit word and revert on intermediate +// overflow, so they use the 256-bit-intermediate helpers from Math.spec +// (mulDivDownSummary256 / mulDivUpSummary256), not the full-precision ones. Each op is a +// floor/ceil of x*y/scale (WAD=1e18, RAY=1e27, PERCENTAGE_FACTOR=1e4); e.g. +// rayMulDown(a,b) = mulDivDownSummary256(a, b, 1e27). +import "../Math.spec"; + +methods { + // ---- WadRayMath (WAD = 1e18, RAY = 1e27) ---- + function WadRayMath.wadMulDown(uint256 a, uint256 b) internal returns (uint256) => mulDivDownSummary256(a, b, 10^18); + function WadRayMath.wadMulUp(uint256 a, uint256 b) internal returns (uint256) => mulDivUpSummary256(a, b, 10^18); + function WadRayMath.wadDivDown(uint256 a, uint256 b) internal returns (uint256) => mulDivDownSummary256(a, 10^18, b); + function WadRayMath.wadDivUp(uint256 a, uint256 b) internal returns (uint256) => mulDivUpSummary256(a, 10^18, b); + function WadRayMath.rayMulDown(uint256 a, uint256 b) internal returns (uint256) => mulDivDownSummary256(a, b, 10^27); + function WadRayMath.rayMulUp(uint256 a, uint256 b) internal returns (uint256) => mulDivUpSummary256(a, b, 10^27); + function WadRayMath.rayDivDown(uint256 a, uint256 b) internal returns (uint256) => mulDivDownSummary256(a, 10^27, b); + function WadRayMath.rayDivUp(uint256 a, uint256 b) internal returns (uint256) => mulDivUpSummary256(a, 10^27, b); + function WadRayMath.toWad(uint256 a) internal returns (uint256) => mulDivDownSummary256(a, 10^18, 1); + function WadRayMath.toRay(uint256 a) internal returns (uint256) => mulDivDownSummary256(a, 10^27, 1); + function WadRayMath.fromWadDown(uint256 a) internal returns (uint256) => mulDivDownSummary256(a, 1, 10^18); + function WadRayMath.fromRayUp(uint256 a) internal returns (uint256) => mulDivUpSummary256(a, 1, 10^27); + + // ---- PercentageMath (PERCENTAGE_FACTOR = 1e4) ---- + function PercentageMath.percentMulDown(uint256 value, uint256 percentage) internal returns (uint256) => mulDivDownSummary256(value, percentage, 10^4); + function PercentageMath.percentMulUp(uint256 value, uint256 percentage) internal returns (uint256) => mulDivUpSummary256(value, percentage, 10^4); + function PercentageMath.percentDivDown(uint256 value, uint256 percentage) internal returns (uint256) => mulDivDownSummary256(value, 10^4, percentage); + function PercentageMath.percentDivUp(uint256 value, uint256 percentage) internal returns (uint256) => mulDivUpSummary256(value, 10^4, percentage); + function PercentageMath.fromBpsDown(uint256 value) internal returns (uint256) => mulDivDownSummary256(value, 1, 10^4); + + // ---- MathUtils (generic 256-bit mulDiv / divUp) ---- + function MathUtils.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns (uint256) => mulDivDownSummary256(a, b, c); + function MathUtils.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns (uint256) => mulDivUpSummary256(a, b, c); + function MathUtils.divUp(uint256 a, uint256 b) internal returns (uint256) => mulDivUpSummary256(a, 1, b); +} diff --git a/certora_autosetup/certora/specs/summaries/Math.spec b/certora_autosetup/certora/specs/summaries/Math.spec index 59edf694..e7b8ff3e 100644 --- a/certora_autosetup/certora/specs/summaries/Math.spec +++ b/certora_autosetup/certora/specs/summaries/Math.spec @@ -14,6 +14,25 @@ function mulDivUpSummary(uint256 x, uint256 y, uint256 denominator) returns uint return assert_uint256(result); } +// 256-bit-intermediate variants: model libraries that compute x*y in a single 256-bit +// word (e.g. Aave WadRayMath / PercentageMath / MathUtils, which revert when a > max/b), +// so they revert on intermediate x*y overflow. This differs from mulDivDownSummary above, +// which keeps the full product (matching 512-bit mulDiv like OpenZeppelin Math / Uniswap +// FullMath) and reverts only on result overflow. +function mulDivDownSummary256(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint product = x * y; + if (denominator == 0 || product > max_uint256) revert(); + return require_uint256(product / denominator); +} + +function mulDivUpSummary256(uint256 x, uint256 y, uint256 denominator) returns uint256 { + mathint product = x * y; + if (denominator == 0 || product > max_uint256) revert(); + mathint result = (product + denominator - 1) / denominator; + if (result > max_uint256) revert(); + return require_uint256(result); +} + function averageSummary(uint256 a, uint256 b) returns uint256 { return require_uint256((a+b)/2); } diff --git a/certora_autosetup/setup/function_summaries.json b/certora_autosetup/setup/function_summaries.json index a066c2a0..39055b5c 100644 --- a/certora_autosetup/setup/function_summaries.json +++ b/certora_autosetup/setup/function_summaries.json @@ -159,5 +159,23 @@ "library_names": ["CTHelpers"], "summary_file": "specs/summaries/CTHelpers.spec", "description": "Gnosis Conditional Tokens CTHelpers.getCollectionId (bn128 collection-id derivation)" + }, + "aave_WadRayMath": { + "names": ["wadMulDown", "wadMulUp", "wadDivDown", "wadDivUp", "rayMulDown", "rayMulUp", "rayDivDown", "rayDivUp", "toWad", "toRay", "fromWadDown", "fromRayUp"], + "library_names": ["WadRayMath"], + "summary_file": "specs/summaries/Aave/Aave_Math.spec", + "description": "Aave WadRayMath fixed-point (WAD/RAY) operations" + }, + "aave_PercentageMath": { + "names": ["percentMulDown", "percentMulUp", "percentDivDown", "percentDivUp", "fromBpsDown"], + "library_names": ["PercentageMath"], + "summary_file": "specs/summaries/Aave/Aave_Math.spec", + "description": "Aave PercentageMath operations" + }, + "aave_MathUtils": { + "names": ["mulDivDown", "mulDivUp", "divUp"], + "library_names": ["MathUtils"], + "summary_file": "specs/summaries/Aave/Aave_Math.spec", + "description": "Aave MathUtils generic 256-bit mulDiv / divUp" } } From 6dd837459c77152c5ed9d49befa04081d33e42c7 Mon Sep 17 00:00:00 2001 From: jar-ben Date: Wed, 22 Jul 2026 23:08:26 +0200 Subject: [PATCH 4/4] autosetup: keep solc_optimize_map consistent when files change --- .../utils/enhanced_config_manager.py | 42 +++++++- tests/test_compiler_flag_reconciliation.py | 96 +++++++++++++++---- 2 files changed, 115 insertions(+), 23 deletions(-) diff --git a/certora_autosetup/utils/enhanced_config_manager.py b/certora_autosetup/utils/enhanced_config_manager.py index 61cae9c3..5fc406dc 100644 --- a/certora_autosetup/utils/enhanced_config_manager.py +++ b/certora_autosetup/utils/enhanced_config_manager.py @@ -416,12 +416,14 @@ def _update_compiler_maps_for_new_contracts( contracts_added: List[ContractHandle], ) -> bool: """ - Update compiler_map and solc_via_ir_map when new contracts are added. + Update compiler_map, solc_via_ir_map, and solc_optimize_map when new + contracts are added. Delegates to CompilationWorkaroundManager which handles: - Parsing pragma from source files - Creating/updating compiler_map entries - Creating/updating solc_via_ir_map entries + - Creating/updating solc_optimize_map entries Args: conf_object: The config dict to modify in-place @@ -438,6 +440,7 @@ def _update_compiler_maps_for_new_contracts( for contract in contracts_added: modified |= self.update_compiler_map_for_contract(conf_object, contract, ref_maps) modified |= self.update_via_ir_map_for_contract(conf_object, contract, ref_maps) + modified |= self.update_optimize_map_for_contract(conf_object, contract, ref_maps) return modified @@ -1012,12 +1015,33 @@ def update_via_ir_map_for_contract( return modified + def update_optimize_map_for_contract( + self, + conf_object: Dict[str, Any], + contract: ContractHandle, + reference_maps: Optional[Dict[str, Any]] = None, + ) -> bool: + """Add a solc_optimize_map entry for a newly-added contract. Mirrors + `update_via_ir_map_for_contract` for the optimize map. Only the map form is + extended; a scalar `solc_optimize` already applies to every file.""" + contract_name = contract.contract_name + if "solc_optimize_map" not in conf_object: + return False + if contract_name in conf_object["solc_optimize_map"]: + return False + ref_optimize_map = (reference_maps or {}).get("solc_optimize_map", {}) + optimize_value = ref_optimize_map.get(contract_name, "200") + conf_object["solc_optimize_map"][contract_name] = optimize_value + self.log(f"Added {contract_name} to solc_optimize_map (value={optimize_value})") + return True + def sync_compiler_maps_with_files( self, conf_object: Dict[str, Any], convention: Optional[SolcConvention] = None, ) -> bool: - """Reconcile compiler_map, solc_via_ir_map, and solc_evm_version_map with `files`. + """Reconcile compiler_map, solc_via_ir_map, solc_evm_version_map, and + solc_optimize_map with `files`. Invariant: when `compiler_map` is present, every contract in `files` has a matching entry. Stale entries (no longer in `files`) get trimmed; @@ -1097,6 +1121,20 @@ def sync_compiler_maps_with_files( ) modified = True + if "solc_optimize_map" in conf_object: + original_len = len(conf_object["solc_optimize_map"]) + conf_object["solc_optimize_map"] = { + key: value + for key, value in conf_object["solc_optimize_map"].items() + if self._key_matches_any_contract(key, contracts_in_files) + } + if len(conf_object["solc_optimize_map"]) != original_len: + self.log( + f"Trimmed solc_optimize_map from {original_len}" + f" to {len(conf_object['solc_optimize_map'])} entries" + ) + modified = True + return modified def create_copy_with_prover_args( diff --git a/tests/test_compiler_flag_reconciliation.py b/tests/test_compiler_flag_reconciliation.py index 91292b65..7b3226e8 100644 --- a/tests/test_compiler_flag_reconciliation.py +++ b/tests/test_compiler_flag_reconciliation.py @@ -27,21 +27,21 @@ def test_drops_solc_when_compiler_map_present() -> None: - conf = {"solc": "solc8.30", "compiler_map": {"Vault": "solc8.35"}} + conf = {"solc": "solc8.30", "compiler_map": {"Widget": "solc8.35"}} ConfigManager.drop_scalars_superseded_by_maps(conf) - assert conf == {"compiler_map": {"Vault": "solc8.35"}} + assert conf == {"compiler_map": {"Widget": "solc8.35"}} def test_each_pair_is_dropped_independently() -> None: conf = { "solc": "solc8.30", - "compiler_map": {"Vault": "solc8.35"}, + "compiler_map": {"Widget": "solc8.35"}, "solc_via_ir": True, - "solc_via_ir_map": {"Vault": True}, + "solc_via_ir_map": {"Widget": True}, "solc_optimize": "200", - "solc_optimize_map": {"Vault": "200"}, + "solc_optimize_map": {"Widget": "200"}, "solc_evm_version": "paris", - "solc_evm_version_map": {"Vault": "cancun"}, + "solc_evm_version_map": {"Widget": "cancun"}, } ConfigManager.drop_scalars_superseded_by_maps(conf) assert set(conf) == { @@ -60,9 +60,9 @@ def test_scalars_survive_without_maps() -> None: def test_unrelated_pair_not_affected() -> None: # A via-ir map must not drop the solc scalar and vice versa. - conf = {"solc": "solc8.30", "solc_via_ir_map": {"Vault": True}} + conf = {"solc": "solc8.30", "solc_via_ir_map": {"Widget": True}} ConfigManager.drop_scalars_superseded_by_maps(conf) - assert conf == {"solc": "solc8.30", "solc_via_ir_map": {"Vault": True}} + assert conf == {"solc": "solc8.30", "solc_via_ir_map": {"Widget": True}} # ============================================================================= @@ -116,24 +116,24 @@ def test_precompute_drops_scalar_solc_when_map_is_built( ) monkeypatch.setattr( "certora_autosetup.setup.setup_prover.FoundryContractExtractor", - lambda root: _StubExtractor({"src/Vault.sol": [("Vault", "0.8.35")]}), + lambda root: _StubExtractor({"src/Widget.sol": [("Widget", "0.8.35")]}), ) contracts = [ - ContractHandle(contract_name="Vault", source_file="src/Vault.sol"), + ContractHandle(contract_name="Widget", source_file="src/Widget.sol"), ContractHandle( contract_name="DummyERC20Impl", source_file="certora/mocks/DummyERC20Impl.sol" ), ] config = setup_prover._precompute_compiler_settings( - contracts, {"solc": "solc8.30", "files": ["src/Vault.sol", str(mock_src)]} + contracts, {"solc": "solc8.30", "files": ["src/Widget.sol", str(mock_src)]} ) assert "solc" not in config - # Total over the scene: artifact version for Vault, pragma-resolved + # Total over the scene: artifact version for Widget, pragma-resolved # (biased to the old default) for the injected mock. assert config["compiler_map"] == { - "Vault": "solc8.35", + "Widget": "solc8.35", "DummyERC20Impl": "solc8.30", } @@ -141,11 +141,11 @@ def test_precompute_drops_scalar_solc_when_map_is_built( def test_precompute_keeps_scalar_when_artifacts_agree(setup_prover, monkeypatch) -> None: monkeypatch.setattr( "certora_autosetup.setup.setup_prover.FoundryContractExtractor", - lambda root: _StubExtractor({"src/Vault.sol": [("Vault", "0.8.30")]}), + lambda root: _StubExtractor({"src/Widget.sol": [("Widget", "0.8.30")]}), ) - contracts = [ContractHandle(contract_name="Vault", source_file="src/Vault.sol")] + contracts = [ContractHandle(contract_name="Widget", source_file="src/Widget.sol")] config = setup_prover._precompute_compiler_settings( - contracts, {"solc": "solc8.30", "files": ["src/Vault.sol"]} + contracts, {"solc": "solc8.30", "files": ["src/Widget.sol"]} ) assert config["solc"] == "solc8.30" assert "compiler_map" not in config @@ -163,11 +163,11 @@ def test_precompute_keeps_scalar_when_artifacts_agree(setup_prover, monkeypatch) def test_merge_drops_base_scalar_when_updates_bring_map(monkeypatch) -> None: autosetup = Autosetup.__new__(Autosetup) autosetup.compilation_config_updates = { - "compiler_map": {"Vault": "solc8.35", "Helper": "solc8.30"}, - "solc_via_ir_map": {"Vault": True, "Helper": False}, + "compiler_map": {"Widget": "solc8.35", "Helper": "solc8.30"}, + "solc_via_ir_map": {"Widget": True, "Helper": False}, } autosetup.contract_handles = [ - ContractHandle(contract_name="Vault", source_file="src/Vault.sol"), + ContractHandle(contract_name="Widget", source_file="src/Widget.sol"), ContractHandle(contract_name="Helper", source_file="src/Helper.sol"), ] monkeypatch.setattr( @@ -181,8 +181,8 @@ def test_merge_drops_base_scalar_when_updates_bring_map(monkeypatch) -> None: assert "solc" not in config assert "solc_via_ir" not in config - assert config["compiler_map"] == {"Vault": "solc8.35", "Helper": "solc8.30"} - assert config["solc_via_ir_map"] == {"Vault": True, "Helper": False} + assert config["compiler_map"] == {"Widget": "solc8.35", "Helper": "solc8.30"} + assert config["solc_via_ir_map"] == {"Widget": True, "Helper": False} # ============================================================================= @@ -215,3 +215,57 @@ def test_scalar_to_map_keys_match_certora_cli() -> None: result = sp.run([sys.executable, "-c", probe], capture_output=True, text=True) assert result.returncode == 0, result.stderr assert __import__("json").loads(result.stdout) == conf_keys + + +# ============================================================================= +# ConfigManager: solc_optimize_map stays consistent when files are added/removed +# +# certoraRun rejects a conf whose solc_optimize_map is missing an entry for a +# file ("files are not matched in solc_optimize_map"). When call resolution +# injects new files (e.g. indexed link-harnesses Sample_1.sol), the map +# must gain matching entries; when files shrink, stale entries must be trimmed. +# ============================================================================= + + +def _config_manager(tmp_path: Path) -> ConfigManager: + return ConfigManager(project_root=tmp_path) + + +def test_update_optimize_map_adds_new_contract_with_default(tmp_path: Path) -> None: + mgr = _config_manager(tmp_path) + conf = {"solc_optimize_map": {"Sample": "22300"}} + added = mgr.update_optimize_map_for_contract( + conf, ContractHandle(contract_name="Sample_1", source_file="certora/harnesses/Sample_1.sol") + ) + assert added is True + assert conf["solc_optimize_map"]["Sample_1"] == "200" + + +def test_update_optimize_map_prefers_reference_value(tmp_path: Path) -> None: + mgr = _config_manager(tmp_path) + conf = {"solc_optimize_map": {"Sample": "22300"}} + mgr.update_optimize_map_for_contract( + conf, + ContractHandle(contract_name="Sample_1", source_file="certora/harnesses/Sample_1.sol"), + reference_maps={"solc_optimize_map": {"Sample_1": "22300"}}, + ) + assert conf["solc_optimize_map"]["Sample_1"] == "22300" + + +def test_update_optimize_map_noop_without_map(tmp_path: Path) -> None: + # A scalar solc_optimize already covers every file, so no map to extend. + mgr = _config_manager(tmp_path) + conf = {"solc_optimize": "200"} + assert mgr.update_optimize_map_for_contract( + conf, ContractHandle(contract_name="Sample_1", source_file="certora/harnesses/Sample_1.sol") + ) is False + assert "solc_optimize_map" not in conf + + +def test_update_optimize_map_noop_when_already_present(tmp_path: Path) -> None: + mgr = _config_manager(tmp_path) + conf = {"solc_optimize_map": {"Sample_1": "22300"}} + assert mgr.update_optimize_map_for_contract( + conf, ContractHandle(contract_name="Sample_1", source_file="certora/harnesses/Sample_1.sol") + ) is False + assert conf["solc_optimize_map"] == {"Sample_1": "22300"}