Migration Contract FV (#832)

Based on #829 

Some extra changes:
- Adding FV to Certora Workflow
- Remove the unused `data` from the `SafeMock`.
- EOF and some capitalization changes
- Parametric argument to some rules

---------

Co-authored-by: Hristo Grigorov <hristo.grigorov@gmail.com>
Co-authored-by: Nicholas Rodrigues Lordello <nick@safe.global>

.github/workflows/certora.yml

@@ -15,7 +15,7 @@ jobs:
         runs-on: ubuntu-latest
         strategy:
             matrix:
-                rule: ["owner", "safe", "module", "nativeTokenRefund", "signatures"]
+                rule: ["owner", "safe", "module", "nativeTokenRefund", "signatures", "safeMigration", "safeToL2Migration", "safeToL2Setup"]
 
         steps:
             - uses: actions/checkout@v4

certora/conf/safeMigration.conf

@@ -0,0 +1,15 @@
+{
+    "files": [
+        "contracts/libraries/SafeMigration.sol",
+        "certora/mocks/SafeMock.sol",
+    ],
+    "link": [
+		"SafeMock:impl=SafeMigration"
+	],
+    "loop_iter": "3",
+    "msg": "SafeMigration",
+    "optimistic_hashing": true,
+    "process": "emv",
+    "solc": "solc7.6",
+    "verify": "SafeMigration:certora/specs/SafeMigration.spec"
+}

certora/conf/safeToL2Migration.conf

@@ -0,0 +1,16 @@
+{
+    "files": [
+        "contracts/libraries/SafeToL2Migration.sol",
+        "certora/mocks/SafeMock.sol",
+    ],
+    "link": [
+		"SafeMock:impl=SafeToL2Migration"
+	],
+    "loop_iter": "3",
+    "msg": "SafeToL2Migration",
+    "optimistic_hashing": true,
+    "optimistic_loop": true,
+    "process": "emv",
+    "solc": "solc7.6",
+    "verify": "SafeToL2Migration:certora/specs/SafeToL2Migration.spec"
+}

certora/conf/safeToL2Setup.conf

@@ -0,0 +1,15 @@
+{
+    "files": [
+        "contracts/libraries/SafeToL2Setup.sol",
+        "certora/mocks/SafeMock.sol"
+    ],
+    "link": [
+		"SafeMock:impl=SafeToL2Setup"
+	],
+    "loop_iter": "3",
+    "msg": "SafeToL2Setup",
+    "optimistic_hashing": true,
+    "process": "emv",
+    "solc": "solc7.6",
+    "verify": "SafeToL2Setup:certora/specs/SafeToL2Setup.spec"
+}

certora/mocks/SafeMock.sol

@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+pragma solidity >=0.7.0 <0.9.0;
+
+import {SafeStorage} from "../../contracts/libraries/SafeStorage.sol";
+
+contract SafeMock is SafeStorage {
+
+    address public impl;
+    address public fallbackHandler;
+
+    function setFallbackHandler(address a) public {
+        fallbackHandler = a;
+    }
+
+    function getFallbackHandler() public view returns (address) {
+        return fallbackHandler;
+    }
+
+    function getNonce() public view returns (uint256) {
+        return nonce;
+    }
+
+    function getSingleton() public view returns (address) {
+        return singleton;
+    }
+
+    function getChainId() public view returns (uint256 result) {
+        /* solhint-disable no-inline-assembly */
+        /// @solidity memory-safe-assembly
+        assembly {
+            result := chainid()
+        }
+        /* solhint-enable no-inline-assembly */
+    }
+
+    function delegateCallSetupToL2(address l2Singleton) public {
+        (bool success, ) = impl.delegatecall(
+            abi.encodeWithSignature("setupToL2(address)", l2Singleton)
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateSingleton() public {
+        (bool success, ) = impl.delegatecall(
+            abi.encodeWithSignature("migrateSingleton()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateWithFallbackHandler() public {
+        (bool success, ) = impl.delegatecall(
+            abi.encodeWithSignature("migrateWithFallbackHandler()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateL2Singleton() public {
+        (bool success, ) = impl.delegatecall(
+            abi.encodeWithSignature("migrateL2Singleton()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateL2WithFallbackHandler() public {
+        (bool success, ) = impl.delegatecall(
+            abi.encodeWithSignature("migrateL2WithFallbackHandler()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateToL2(address l2Singleton) public {
+        (bool success, ) = impl.delegatecall(
+            abi.encodeWithSignature("migrateToL2(address)", l2Singleton)
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateFromV111(address l2Singleton, address fallbackHandlerAddr) public {
+        (bool success, ) = impl.delegatecall(
+            abi.encodeWithSignature("migrateFromV111(address,address)", l2Singleton, fallbackHandlerAddr)
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+}

certora/specs/ModuleReach.spec

@@ -235,4 +235,4 @@ rule disableModuleDisablesModule {
 
     assert !isModuleEnabled(toRemove), "disableModule should disable module";
     assert isModuleEnabled(other) == isModuleEnabledBefore, "disableModule should not change other modules";
-}
+}

certora/specs/SafeMigration.spec

@@ -0,0 +1,74 @@
+using SafeMigration as SafeMigration;
+using SafeMock as SafeMock;
+
+methods {
+    function _.setFallbackHandler(address) external => DISPATCHER(true);
+}
+
+// MIGRATION_SINGLETON is always the current contract
+invariant MIGRATION_SINGLETONisAlwaysCurrentContract()
+    SafeMigration.MIGRATION_SINGLETON == SafeMigration;
+
+
+// All the function that are not view function will revert (if it is not delegateCall)
+rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } {
+    requireInvariant MIGRATION_SINGLETONisAlwaysCurrentContract;
+    SafeMigration.f@withrevert(e,args);
+    assert lastReverted;
+}
+
+
+// Safe's singleton address update integrity (parametric version)
+rule singletonMigrationIntegrityParametric(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:SafeMock.delegateMigrateSingleton().selector
+      || f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector
+      || f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector
+      || f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector
+    } {
+    address singletonBefore = SafeMock.getSingleton(e);
+
+    SafeMock.f@withrevert(e, args);
+    bool callReverted = lastReverted;
+
+    address singletonAfter = SafeMock.getSingleton(e);
+
+    assert !callReverted && 
+           (f.selector == sig:SafeMock.delegateMigrateSingleton().selector || 
+            f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector) =>
+                                                singletonAfter == SafeMigration.SAFE_SINGLETON(e);
+
+    assert !callReverted && 
+           (f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector || 
+            f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector) =>
+                                                singletonAfter == SafeMigration.SAFE_L2_SINGLETON(e);
+
+    assert callReverted => singletonAfter == singletonBefore;
+}
+
+
+// Safe's fallbackHandler address update integrity (parametric version)
+rule fallbackHandlerMigrationIntegrityParametric(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:SafeMock.delegateMigrateSingleton().selector
+      || f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector
+      || f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector
+      || f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector
+    } {
+    address fallbackHandlerBefore = SafeMock.getFallbackHandler(e);
+
+    SafeMock.f@withrevert(e, args);
+    bool callReverted = lastReverted;
+
+    address fallbackHandlerAfter = SafeMock.getFallbackHandler(e);
+
+    assert !callReverted && 
+           (f.selector == sig:SafeMock.delegateMigrateWithFallbackHandler().selector || 
+            f.selector == sig:SafeMock.delegateMigrateL2WithFallbackHandler().selector) =>
+                                                fallbackHandlerAfter == SafeMigration.SAFE_FALLBACK_HANDLER(e);
+
+    assert !callReverted && 
+           (f.selector == sig:SafeMock.delegateMigrateSingleton().selector || 
+            f.selector == sig:SafeMock.delegateMigrateL2Singleton().selector) =>
+                                                fallbackHandlerAfter == fallbackHandlerBefore;
+
+    assert callReverted => fallbackHandlerAfter == fallbackHandlerBefore;
+}

certora/specs/SafeToL2Migration.spec

@@ -0,0 +1,64 @@
+using SafeToL2Migration as SafeToL2Migration;
+using SafeMock as SafeMock;
+
+methods {
+    function _.setFallbackHandler(address) external => DISPATCHER(true);
+}
+
+// MIGRATION_SINGLETON is always the current contract
+invariant MIGRATION_SINGLETONisAlwaysCurrentContract()
+    SafeToL2Migration.MIGRATION_SINGLETON == SafeToL2Migration;
+
+
+// All the function that are not view function will revert (if it is not delegateCall)
+rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } {
+    requireInvariant MIGRATION_SINGLETONisAlwaysCurrentContract;
+    SafeToL2Migration.f@withrevert(e,args);
+    assert lastReverted;
+}
+
+// Calls to migrateToL2() and migrateFromV111() can succeed only if Safe's nonce is correct
+rule nonceMustBeCorrect(env e, method f, calldataarg args) filtered {
+    f -> f.selector == sig:SafeMock.delegateMigrateToL2(address).selector
+      || f.selector == sig:SafeMock.delegateMigrateFromV111(address,address).selector
+    } {
+    // get current nonce of the Safe contract
+    uint256 currentNonce = SafeMock.getNonce(e);
+
+    SafeMock.f@withrevert(e, args);
+    bool callReverted = lastReverted;
+
+    assert !callReverted => currentNonce == 1;
+}
+
+// Correct update of Safe's singleton address by migrateToL2()
+rule singletonMigrateToL2Integrity(env e, address l2Singleton) {
+    address singletonBefore = SafeMock.getSingleton(e);
+
+    SafeMock.delegateMigrateToL2@withrevert(e, l2Singleton);
+    bool callReverted = lastReverted;
+
+    address singletonAfter = SafeMock.getSingleton(e);
+
+    assert !callReverted => singletonAfter == l2Singleton;
+    assert callReverted => singletonAfter == singletonBefore;
+}
+
+
+// Correct update of Safe's singleton address and fallbackHandler address by migrateFromV111()
+rule singletonMigrateFromV111Integrity(env e, address l2Singleton, address fallbackHandlerAddr) {
+    address singletonBefore = SafeMock.getSingleton(e);
+    address fallbackHandlerBefore = SafeMock.getFallbackHandler(e);
+
+    SafeMock.delegateMigrateFromV111@withrevert(e, l2Singleton, fallbackHandlerAddr);
+    bool callReverted = lastReverted;
+
+    address singletonAfter = SafeMock.getSingleton(e);
+    address fallbackHandlerAfter = SafeMock.getFallbackHandler(e);
+
+    assert !callReverted => singletonAfter == l2Singleton;
+    assert !callReverted => fallbackHandlerAfter == fallbackHandlerAddr;
+
+    assert callReverted => singletonAfter == singletonBefore;
+    assert callReverted => fallbackHandlerAfter == fallbackHandlerBefore;
+}

certora/specs/SafeToL2Setup.spec

@@ -0,0 +1,43 @@
+using SafeToL2Setup as SafeToL2Setup;
+using SafeMock as SafeMock;
+
+// _SELF is always the current contract
+// if the "rule_sanity": "basic" flag is enabled this rule would fail sanity check
+invariant _SELFisAlwaysCurrentContract()
+    SafeToL2Setup.SELF == SafeToL2Setup;
+
+
+// All the non-view functions will revert when called directly (only delegateCall is allowed)
+rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } {
+    requireInvariant _SELFisAlwaysCurrentContract;
+    SafeToL2Setup.f@withrevert(e,args);
+    assert lastReverted;
+}
+
+// The delegateCall to setupToL2() can succeed only if Safe's nonce is zero
+rule nonceMustBeZero(env e, address singletonContract) {
+    // get current nonce of the Safe contract
+    uint256 currentNonce = SafeMock.getNonce(e);
+
+    SafeMock.delegateCallSetupToL2@withrevert(e, singletonContract);
+    bool callReverted = lastReverted;
+
+    assert !callReverted => currentNonce == 0;
+}
+
+
+// The singleton contract can be updated only if the chainId is not 1
+rule theSingletonContractIsUpdatedCorrectly(env e, address newSingletonContract) {
+    // `newSingletonContract` is the singleton we try to assign to the Safe contract
+
+    address singletonBefore = SafeMock.getSingleton(e);
+    uint256 chainId = SafeMock.getChainId(e);
+
+    SafeMock.delegateCallSetupToL2@withrevert(e, newSingletonContract);
+    bool callReverted = lastReverted;
+
+    address singletonAfter = SafeMock.getSingleton(e);
+
+    assert !callReverted && chainId != 1 => singletonAfter == newSingletonContract;
+    assert !callReverted && chainId == 1 => singletonAfter == singletonBefore;
+}