From 2b17d28298838a55c6acbadde997363b55802f6e Mon Sep 17 00:00:00 2001 From: jar-ben Date: Wed, 22 Jul 2026 15:57:12 +0200 Subject: [PATCH 1/2] 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/2] 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"],