Formal verification of Account (7702+7579) (#5872)

Author: Amxx

certora/diff/account_extensions_draft-AccountERC7579.sol.patch

@@ -0,0 +1,25 @@
+--- account/extensions/draft-AccountERC7579.sol	2025-07-22 11:18:42.944504471 +0200
++++ account/extensions/draft-AccountERC7579.sol	2025-07-22 13:57:03.670277084 +0200
+@@ -60,8 +60,8 @@
+     using EnumerableSet for *;
+     using Packing for bytes32;
+ 
+-    EnumerableSet.AddressSet private _validators;
+-    EnumerableSet.AddressSet private _executors;
++    EnumerableSet.AddressSet internal _validators; // private → internal for FV
++    EnumerableSet.AddressSet internal _executors; // private → internal for FV
+     mapping(bytes4 selector => address) private _fallbacks;
+ 
+     /// @dev The account's {fallback} was called with a selector that doesn't have an installed handler.
+@@ -308,8 +308,9 @@
+      * the ERC-2771 format.
+      */
+     function _fallback() internal virtual returns (bytes memory) {
+-        address handler = _fallbackHandler(msg.sig);
+-        require(handler != address(0), ERC7579MissingFallbackHandler(msg.sig));
++        bytes4 selector = bytes4(msg.data[0:4]);
++        address handler = _fallbackHandler(selector);
++        require(handler != address(0), ERC7579MissingFallbackHandler(selector));
+ 
+         // From https://eips.ethereum.org/EIPS/eip-7579#fallback[ERC-7579 specifications]:
+         // - MUST utilize ERC-2771 to add the original msg.sender to the calldata sent to the fallback handler

certora/harnesses/AccountHarness.sol

@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.26;
+
+import {AccountERC7702WithModulesMock} from "../patched/mocks/account/AccountMock.sol";
+import {EIP712} from "../patched/utils/cryptography/EIP712.sol";
+import {EnumerableSet} from "../patched/utils/structs/EnumerableSet.sol";
+
+contract AccountHarness is AccountERC7702WithModulesMock {
+    using EnumerableSet for EnumerableSet.AddressSet;
+
+    constructor(string memory name, string memory version) EIP712(name, version) {}
+
+    function getFallbackHandler(bytes4 selector) external view returns (address) {
+        return _fallbackHandler(selector);
+    }
+
+    function getDataSelector(bytes memory data) external pure returns (bytes4) {
+        return bytes4(data);
+    }
+
+    function _validatorContains(address module) external view returns (bool) {
+        return _validators.contains(module);
+    }
+
+    function _validatorLength() external view returns (uint256) {
+        return _validators.length();
+    }
+
+    function _validatorAt(uint256 index) external view returns (address) {
+        return _validators.at(index);
+    }
+
+    function _validatorAtFull(uint256 index) external view returns (bytes32) {
+        return _validators._inner._values[index];
+    }
+
+    function _validatorPositionOf(address module) external view returns (uint256) {
+        return _validators._inner._positions[bytes32(uint256(uint160(module)))];
+    }
+
+    function _executorContains(address module) external view returns (bool) {
+        return _executors.contains(module);
+    }
+
+    function _executorLength() external view returns (uint256) {
+        return _executors.length();
+    }
+
+    function _executorAt(uint256 index) external view returns (address) {
+        return _executors.at(index);
+    }
+
+    function _executorAtFull(uint256 index) external view returns (bytes32) {
+        return _executors._inner._values[index];
+    }
+
+    function _executorPositionOf(address module) external view returns (uint256) {
+        return _executors._inner._positions[bytes32(uint256(uint160(module)))];
+    }
+}

certora/specs/Account.conf

@@ -0,0 +1,9 @@
+{
+    "files": [
+        "certora/harnesses/AccountHarness.sol"
+    ],
+    "optimistic_loop": true,
+    "process": "emv",
+    "url_visibility": "public",
+    "verify": "AccountHarness:certora/specs/Account.spec"
+}