setup, mock and rules for SafeMigration, SafeToL2Migration and SafeToL2Setup

certora/conf/SafeMigration.conf

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

certora/conf/SafeToL2Migration.conf

@@ -0,0 +1,17 @@
+{
+    "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",
+    // "rule_sanity": "advanced",
+    "solc": "solc7.6",
+    "verify": "SafeToL2Migration:certora/specs/SafeToL2Migration.spec"
+}

certora/conf/SafeToL2Setup.conf

@@ -0,0 +1,16 @@
+{
+    "files": [
+        "contracts/libraries/SafeToL2Setup.sol",
+        "certora/mocks/SafeMock.sol"
+    ],
+    "link": [
+		"SafeMock:impl=SafeToL2Setup"
+	],
+    "loop_iter": "3",
+    "msg": "SafeToL2Setup",
+    "optimistic_hashing": true,
+    "process": "emv",
+    // "rule_sanity": "advanced",
+    "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, bytes memory data) = impl.delegatecall(
+            abi.encodeWithSignature("setupToL2(address)", l2Singleton)
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateSingleton() public {
+        (bool success, bytes memory data) = impl.delegatecall(
+            abi.encodeWithSignature("migrateSingleton()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateWithFallbackHandler() public {
+        (bool success, bytes memory data) = impl.delegatecall(
+            abi.encodeWithSignature("migrateWithFallbackHandler()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateL2Singleton() public {
+        (bool success, bytes memory data) = impl.delegatecall(
+            abi.encodeWithSignature("migrateL2Singleton()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateL2WithFallbackHandler() public {
+        (bool success, bytes memory data) = impl.delegatecall(
+            abi.encodeWithSignature("migrateL2WithFallbackHandler()")
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateToL2(address l2Singleton) public {
+        (bool success, bytes memory data) = impl.delegatecall(
+            abi.encodeWithSignature("migrateToL2(address)", l2Singleton)
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+    function delegateMigrateFromV111(address l2Singleton, address fallbackHandlerAddr) public {
+        (bool success, bytes memory data) = impl.delegatecall(
+            abi.encodeWithSignature("migrateFromV111(address,address)", l2Singleton, fallbackHandlerAddr)
+        );
+
+        if (!success) {
+            revert("Something went wrong");
+        }
+    }
+
+}

certora/specs/SafeMigration.spec

@@ -0,0 +1,84 @@
+// All rules of SafeMigration without sanity check
+// https://prover.certora.com/output/80942/620608f8f84c40e498eeb6e672b27d91?anonymousKey=3b88dbb5a130bb1b7733e9c9ea9f6b84c375864e
+
+// All rules of SafeMigration with sanity check
+// https://prover.certora.com/output/80942/19f6446a292242d4ae7448da7eb3a5ec?anonymousKey=8dba0d1d6a0028d5faa80e7b38bbdb80e1d373f2
+
+using SafeMigration as SafeMigration;
+using SafeMock as SafeMock;
+
+methods {
+    function _.setFallbackHandler(address) external => DISPATCHER(true);
+}
+
+// MIGRATION_SINGLETON is always the current contract
+// passes - https://prover.certora.com/output/80942/1f393e4a9f464500b6ab07e4f1670c70?anonymousKey=cae79ff7b651cc8da032d6cfba5597eacd0918e5
+invariant MIGRATION_SINGLETONisAlwaysCurrentContract()
+    SafeMigration.MIGRATION_SINGLETON == SafeMigration;
+
+
+// all the function that are not view function will revert (if it is not delegateCall)
+// passes - https://prover.certora.com/output/80942/1f393e4a9f464500b6ab07e4f1670c70?anonymousKey=cae79ff7b651cc8da032d6cfba5597eacd0918e5
+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)
+// passes - https://prover.certora.com/output/80942/3518444596b84ae6ae47bd08d8ebfb60?anonymousKey=bc02b2447d81d7762d0b34b2d98a31a8dc225ca6
+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)
+// passes - https://prover.certora.com/output/80942/7fcd95ecf2574139a1ee490f9b6b68c9?anonymousKey=fefdae9e8e8a0aebdd99d5ebd6288b2555b6a86e
+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,75 @@
+// All rules of SafeToL2Migration without sanity check
+// https://prover.certora.com/output/80942/0e6b9696724342b38f978129c826dd46?anonymousKey=fc6f2912ae59d097b105f8458fb7870f08694114
+
+// All rules of SafeToL2Migration with sanity check
+// https://prover.certora.com/output/80942/a95f00eed26c4aa89c3e24fc07c1c574?anonymousKey=a63ab3672b3ae8e42a5af1e6b1f36251227d9ce8
+
+using SafeToL2Migration as SafeToL2Migration;
+using SafeMock as SafeMock;
+
+methods {
+    function _.setFallbackHandler(address) external => DISPATCHER(true);
+}
+
+// MIGRATION_SINGLETON is always the current contract
+// passes - https://prover.certora.com/output/80942/3087ca5a9a27481891e7f84736ec6aaf?anonymousKey=f867049529614ee37a9c573ff1e479834e34ad52
+invariant MIGRATION_SINGLETONisAlwaysCurrentContract()
+    SafeToL2Migration.MIGRATION_SINGLETON == SafeToL2Migration;
+
+
+// all the function that are not view function will revert (if it is not delegateCall)
+// passes - https://prover.certora.com/output/80942/3349cd8b7e9645c1ba89bf874580649c?anonymousKey=5375971a67985c430f00936755857d20e61d3f5f
+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
+// passes - https://prover.certora.com/output/80942/a809db0dd61140bbbbf2b8df6318491c?anonymousKey=71b8fdfdedc8523bda752739c743b8e3202f05a2
+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()
+// passes - https://prover.certora.com/output/80942/2eec3578aa6a434686e6af3c2e08768f?anonymousKey=7df843e6bab53765efa0d2c29597ac1b2474930e
+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()
+// running (extended check) - https://prover.certora.com/output/80942/01b4a45695cb4f83bee86a0f4e9110e0?anonymousKey=b0d04846f6eb35c3037f0983da75aef8980dad28
+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,55 @@
+// All rules of SafeToL2Setup without sanity check
+// https://prover.certora.com/output/80942/0639d6b99acb41ea9939baad4781bfa1?anonymousKey=c279b3bd45442b66b5ecad7a017e5b4ad3be1e4e
+
+// All rules of SafeToL2Setup with sanity check
+// https://prover.certora.com/output/80942/3cbb0c40489045488279deda0cfa9a4a?anonymousKey=f7fd8636ff12c6d589a46ac56d312e394a382004
+
+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
+// passes - https://prover.certora.com/output/80942/a2558c3b8fcf46a8bf3df94600026345?anonymousKey=c168a08554d2c1d9226269a72567e82e0dc1805a
+invariant _SELFisAlwaysCurrentContract()
+    SafeToL2Setup._SELF == SafeToL2Setup;
+
+
+// all the non-view functions will revert when called directly (only delegateCall is allowed)
+// passes - https://prover.certora.com/output/80942/a2558c3b8fcf46a8bf3df94600026345?anonymousKey=c168a08554d2c1d9226269a72567e82e0dc1805a
+rule allNonViewFunctionRevert(env e, method f, calldataarg args) filtered { f -> !f.isView } {
+    requireInvariant _SELFisAlwaysCurrentContract;
+    SafeToL2Setup.f@withrevert(e,args);
+    assert lastReverted;
+}
+
+// delegateCall to setupToL2() can succeed only if Safe's nonce is zero
+// passes - https://prover.certora.com/output/80942/35c91add2768483d92deb5d864e7e5e4?anonymousKey=02d1291b5b390f7ff332b44d9f8465e7d0991651
+rule nonceMustBeZero(env e) {
+    // get current nonce of the Safe contract
+    uint256 currentNonce = SafeMock.getNonce(e);
+    address singletonContract;
+
+    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
+// passes - https://prover.certora.com/output/80942/7dc165e79c724608b79edb5f4b3a8cc3?anonymousKey=d99b351a5d6b09831496ed245f31b54bb8902a16
+rule theSingletonContractIsUpdatedCorrectly(env e) {
+    address newSingletonContract;  // 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;
+}
+