Formal verification of Account (7702+7579)

certora/diff/account_extensions_draft-AccountERC7579.sol.patch

@@ -0,0 +1,14 @@
+--- account/extensions/draft-AccountERC7579.sol	2025-07-07 12:07:22.042739166 +0200
++++ account/extensions/draft-AccountERC7579.sol	2025-07-08 18:43:59.413714889 +0200
+@@ -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,13 @@
+// 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";
+
+contract AccountHarness is AccountERC7702WithModulesMock {
+    constructor(string memory name, string memory version) EIP712(name, version) {}
+
+    function getFallbackHandler(bytes4 selector) external view returns (address) {
+        return _fallbackHandler(selector);
+    }
+}

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"]
   }
 ]

certora/specs/Account.spec

@@ -0,0 +1,182 @@
+import "helpers/helpers.spec";
+import "methods/IAccount.spec";
+
+methods {
+    function getFallbackHandler(bytes4) external returns (address) envfree;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│                                                  Module management                                                  │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule moduleManagementRule(
+    env e,
+    method f,
+    calldataarg args,
+    uint256 moduleTypeId,
+    address module,
+    bytes additionalContext
+) {
+    bytes context;
+    require context.length == 0;
+
+    bool isEntryPoint = e.msg.sender == entryPoint();
+    bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract;
+    bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context);
+
+    bool isModuleInstalledBefore = isModuleInstalled(moduleTypeId, module, additionalContext);
+    f(e, args);
+    bool isModuleInstalledAfter = isModuleInstalled(moduleTypeId, module, additionalContext);
+
+    assert (
+        isModuleInstalledBefore != isModuleInstalledAfter
+    ) => (
+        (
+            f.selector == sig:execute(bytes32,bytes).selector  &&
+            isEntryPointOrSelf
+        ) || (
+            f.selector == sig:executeFromExecutor(bytes32,bytes).selector &&
+            isExecutionModule
+        ) || (
+            f.selector == sig:installModule(uint256,address,bytes).selector &&
+            isEntryPointOrSelf
+        ) || (
+            f.selector == sig:uninstallModule(uint256,address,bytes).selector &&
+            isEntryPointOrSelf
+        )
+    );
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│                                                     CALL OPCODE                                                     │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost bool    call;
+ghost address call_target;
+ghost uint32  call_selector;
+ghost uint256 call_value;
+ghost uint256 call_argsLength;
+
+hook CALL(uint256 gas, address target, uint256 value, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc {
+    if (executingContract == currentContract) {
+        call            = true;
+        call_target     = target;
+        call_selector   = selector;
+        call_value      = value;
+        call_argsLength = argsLength;
+    }
+}
+
+rule callOpcodeRule(env e, method f, calldataarg args) {
+    require !call;
+
+    bytes context;
+    require context.length == 0;
+
+    bool isEntryPoint = e.msg.sender == entryPoint();
+    bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract;
+    bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context);
+
+    f(e, args);
+
+    assert call => (
+        (
+            f.selector == sig:execute(bytes32,bytes).selector &&
+            isEntryPointOrSelf
+        ) || (
+            f.selector == sig:executeFromExecutor(bytes32,bytes).selector &&
+            isExecutionModule
+        ) || (
+            // Note: rule callInstallModule checks that the call target is the module being installed
+            f.selector == sig:installModule(uint256,address,bytes).selector &&
+            isEntryPointOrSelf &&
+            call_value == 0
+        ) || (
+            // Note: rule callUninstallModule checks that the call target is the module being uninstalled
+            f.selector == sig:uninstallModule(uint256,address,bytes).selector &&
+            isEntryPointOrSelf &&
+            call_value == 0
+        ) || (
+            f.selector == sig:validateUserOp(Account.PackedUserOperation,bytes32,uint256).selector &&
+            isEntryPoint &&
+            (
+                (
+                    // payPrefund (target is entryPoint and argsLength is 0)
+                    call_target == entryPoint() &&
+                    call_value > 0 &&
+                    call_argsLength == 0
+                ) || (
+                    // isValidSignatureWithSender (target is as validation module)
+                    isModuleInstalled(1, call_target, context) &&
+                    call_value == 0
+                )
+            )
+        ) || (
+            f.isFallback &&
+            call_target == getFallbackHandler(to_bytes4(call_selector)) &&
+            call_value == e.msg.value
+        )
+    );
+}
+
+rule callInstallModule(env e, uint256 moduleTypeId, address module, bytes initData) {
+    installModule(e, moduleTypeId, module, initData);
+
+    assert call        == true;
+    assert call_target == module;
+    assert call_value  == 0;
+}
+
+rule callUninstallModule(env e, uint256 moduleTypeId, address module, bytes deInitData) {
+    uninstallModule(e, moduleTypeId, module, deInitData);
+
+    assert call        == true;
+    assert call_target == module;
+    assert call_value  == 0;
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│                                                 DELEGATECALL OPCODE                                                 │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+ghost bool    delegatecall;
+ghost address delegatecall_target;
+ghost uint256 delegatecall_argsLength;
+
+hook DELEGATECALL(uint256 gas, address target, uint256 argsOffset, uint256 argsLength, uint256 retOffset, uint256 retLength) uint256 rc {
+    if (executingContract == currentContract) {
+        delegatecall = true;
+        delegatecall_target = target;
+        delegatecall_argsLength = argsLength;
+    }
+}
+
+rule delegatecallOpcodeRule(
+    env e,
+    method f,
+    calldataarg args
+) {
+    require !delegatecall;
+
+    bytes context;
+    require context.length == 0;
+
+    bool isEntryPoint = e.msg.sender == entryPoint();
+    bool isEntryPointOrSelf = e.msg.sender == entryPoint() || e.msg.sender == currentContract;
+    bool isExecutionModule = isModuleInstalled(2, e.msg.sender, context);
+
+    f(e, args);
+
+    assert delegatecall => (
+        (
+            f.selector == sig:execute(bytes32,bytes).selector &&
+            isEntryPointOrSelf
+        ) || (
+            f.selector == sig:executeFromExecutor(bytes32,bytes).selector &&
+            isExecutionModule
+        )
+    );
+}

certora/specs/methods/IAccount.spec

@@ -0,0 +1,34 @@
+methods {
+    // Account
+    function entryPoint()                                                      external returns (address) envfree;
+    function getNonce()                                                        external returns (uint256) envfree;
+    function getNonce(uint192)                                                 external returns (uint256) envfree;
+    function validateUserOp(Account.PackedUserOperation,bytes32,uint256)       external returns (uint256);
+
+    // IERC1271
+    function isValidSignature(bytes32,bytes)                                   external returns (bytes4);
+
+    // IERC7579AccountConfig
+    function accountId()                                                       external returns (string)  envfree;
+    function supportsExecutionMode(bytes32)                                    external returns (bool)    envfree;
+    function supportsModule(uint256)                                           external returns (bool)    envfree;
+
+    // IERC7579ModuleConfig
+    function installModule(uint256,address,bytes)                              external;
+    function uninstallModule(uint256,address,bytes)                            external;
+    function isModuleInstalled(uint256,address,bytes)                          external returns (bool)    envfree;
+
+    // IERC7579Execution
+    function execute(bytes32,bytes)                                            external;
+    function executeFromExecutor(bytes32,bytes)                                external returns (bytes[]);
+
+    // IERC721Receiver
+    function onERC721Received(address,address,uint256,bytes)                   external returns (bytes4)  envfree;
+
+    // IERC1155Receiver
+    function onERC1155Received(address,address,uint256,uint256,bytes)          external returns (bytes4)  envfree;
+    function onERC1155BatchReceived(address,address,uint256[],uint256[],bytes) external returns (bytes4)  envfree;
+
+    // IERC165
+    function supportsInterface(bytes4)                                         external returns (bool)    envfree;
+}

fv-requirements.txt

@@ -1,4 +1,4 @@
-certora-cli==4.13.1
+certora-cli==7.31.0
 # File uses a custom name (fv-requirements.txt) so that it isn't picked by Netlify's build
 # whose latest Python version is 0.3.8, incompatible with most recent versions of Halmos
 halmos==0.3.0