Formal verification of Account (7702+7579)

.github/workflows/formal-verification.yml

@@ -12,7 +12,7 @@ on:
 env:
   PIP_VERSION: '3.11'
   JAVA_VERSION: '11'
-  SOLC_VERSION: '0.8.20'
+  SOLC_VERSION: '0.8.27'
 
 concurrency: ${{ github.workflow }}-${{ github.ref }}
 

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,52 @@
+// 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 _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 _executorPositionOf(address module) external view returns (uint256) {
+        return _executors._inner._positions[bytes32(uint256(uint160(module)))];
+    }
+}

certora/run.js

@@ -14,7 +14,7 @@ import path from 'path';
 import yargs from 'yargs';
 import { hideBin } from 'yargs/helpers';
 import pLimit from 'p-limit';
-import fs from 'fs/promises';
+import fs from 'fs';
 
 const argv = yargs(hideBin(process.argv))
   .env('')
@@ -123,7 +123,7 @@ async function runCertora(spec, contract, files, options = []) {
   stream.end();
 
   // write results in markdown format
-  writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]);
+  writeEntry(spec, contract, !(code || signal), (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]);
 
   // write all details
   console.error(`+ certoraRun ${args.join(' ')}\n` + (await output));

certora/specs.json

@@ -106,5 +106,11 @@
     "spec": "Nonces",
     "contract": "NoncesHarness",
     "files": ["certora/harnesses/NoncesHarness.sol"]
+  },
+  {
+    "spec": "Account",
+    "contract": "AccountHarness",
+    "files": ["certora/harnesses/AccountHarness.sol"],
+    "options": ["--optimistic_loop"]
   }
 ]