More rules

certora/L1TokenBridge.conf

@@ -3,14 +3,16 @@
         "src/L1TokenBridge.sol",
         "certora/harness/Auxiliar.sol",
         "test/mocks/MessengerMock.sol",
-        "test/mocks/GemMock.sol"
+        "test/mocks/GemMock.sol",
+        "certora/harness/ImplementatioNMock.sol"
     ],
     "solc": "solc-0.8.21",
     "solc_optimize_map": {
         "L1TokenBridge": "200",
         "Auxiliar": "0",
         "MessengerMock": "0",
-        "GemMock": "0"
+        "GemMock": "0",
+        "ImplementatioNMock": "0"
     },
     "link": [
         "L1TokenBridge:messenger=MessengerMock"
@@ -22,5 +24,8 @@
     "build_cache": true,
     "optimistic_hashing": true,
     "hashing_length_bound": "512",
+    "prover_args": [
+        "-enableStorageSplitting false"
+    ],
     "msg": "L1TokenBridge"
 }

certora/L1TokenBridge.spec

@@ -13,6 +13,8 @@ methods {
     // immutables
     function otherBridge() external returns (address) envfree;
     function messenger() external returns (address) envfree;
+    // getter
+    function getImplementation() external returns (address) envfree;
     //
     function gem.allowance(address,address) external returns (uint256) envfree;
     function gem.totalSupply() external returns (uint256) envfree;
@@ -23,15 +25,62 @@ methods {
     function l1messenger.lastMessageHash() external returns (bytes32) envfree;
     function l1messenger.lastMinGasLimit() external returns (uint32) envfree;
     //
+    function _.proxiableUUID() external => DISPATCHER(true);
     function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
 }
 
+definition INITIALIZABLE_STORAGE() returns uint256 = 0xf0c57e16840df040f15088dc2f81fe391c3923bec73e23a9662efc9c229c6a00;
+definition IMPLEMENTATION_SLOT() returns uint256 = 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc;
+
+persistent ghost bool firstRead;
+persistent ghost mathint initializedBefore;
+persistent ghost bool initializingBefore;
+persistent ghost mathint initializedAfter;
+persistent ghost bool initializingAfter;
+hook ALL_SLOAD(uint256 slot) uint256 val {
+    if (slot == INITIALIZABLE_STORAGE() && firstRead) {
+        firstRead = false;
+        initializedBefore = val % (max_uint64 + 1);
+        initializingBefore = (val / 2^64) % (max_uint8 + 1) != 0;
+    } else if (slot == INITIALIZABLE_STORAGE()) {
+        initializedAfter = val % (max_uint64 + 1);
+        initializingAfter = (val / 2^64) % (max_uint8 + 1) != 0;
+    }
+}
+hook ALL_SSTORE(uint256 slot, uint256 val) {
+    if (slot == INITIALIZABLE_STORAGE()) {
+        initializedAfter = val % (max_uint64 + 1);
+        initializingAfter = (val / 2^64) % (max_uint8 + 1) != 0;
+    }
+}
+
+// Verify no more entry points exist
+rule entryPoints(method f) filtered { f -> !f.isView } {
+    env e;
+
+    calldataarg args;
+    f(e, args);
+
+    assert f.selector == sig:initialize().selector ||
+           f.selector == sig:upgradeToAndCall(address,bytes).selector ||
+           f.selector == sig:rely(address).selector ||
+           f.selector == sig:deny(address).selector ||
+           f.selector == sig:file(bytes32,address).selector ||
+           f.selector == sig:close().selector ||
+           f.selector == sig:registerToken(address,address).selector ||
+           f.selector == sig:bridgeERC20(address,address,uint256,uint32,bytes).selector ||
+           f.selector == sig:bridgeERC20To(address,address,address,uint256,uint32,bytes).selector ||
+           f.selector == sig:finalizeBridgeERC20(address,address,address,address,uint256,bytes).selector;
+}
+
 // Verify that each storage layout is only modified in the corresponding functions
 rule storageAffected(method f) filtered { f -> f.selector != sig:upgradeToAndCall(address, bytes).selector } {
     env e;
 
     address anyAddr;
 
+    initializedAfter = initializedBefore;
+
     mathint wardsBefore = wards(anyAddr);
     address l1ToL2TokenBefore = l1ToL2Token(anyAddr);
     mathint isOpenBefore = isOpen();
@@ -45,10 +94,86 @@ rule storageAffected(method f) filtered { f -> f.selector != sig:upgradeToAndCal
     mathint isOpenAfter = isOpen();
     address escrowAfter = escrow();
 
-    assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector || f.selector == sig:initialize().selector, "Assert 1";
-    assert l1ToL2TokenAfter != l1ToL2TokenBefore => f.selector == sig:registerToken(address,address).selector, "Assert 2";
-    assert isOpenAfter != isOpenBefore => f.selector == sig:close().selector || f.selector == sig:initialize().selector, "Assert 3";
-    assert escrowAfter != escrowBefore => f.selector == sig:file(bytes32,address).selector, "Assert 4";
+    assert initializedAfter != initializedBefore => f.selector == sig:initialize().selector, "Assert 1";
+    assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector || f.selector == sig:initialize().selector, "Assert 2";
+    assert l1ToL2TokenAfter != l1ToL2TokenBefore => f.selector == sig:registerToken(address,address).selector, "Assert 3";
+    assert isOpenAfter != isOpenBefore => f.selector == sig:close().selector || f.selector == sig:initialize().selector, "Assert 4";
+    assert escrowAfter != escrowBefore => f.selector == sig:file(bytes32,address).selector, "Assert 5";
+}
+
+// Verify correct storage changes for non reverting initialize
+rule initialize() {
+    env e;
+
+    address other;
+    require other != e.msg.sender;
+
+    mathint wardsOtherBefore = wards(other);
+
+    initialize(e);
+
+    mathint wardsSenderAfter = wards(e.msg.sender);
+    mathint wardsOtherAfter = wards(other);
+    mathint isOpenAfter = isOpen();
+
+    assert initializedAfter == 1, "Assert 1";
+    assert !initializingAfter, "Assert 2";
+    assert wardsSenderAfter == 1, "Assert 3";
+    assert wardsOtherAfter == wardsOtherBefore, "Assert 4";
+    assert isOpenAfter == 1, "Assert 5";
+}
+
+// Verify revert rules on initialize
+rule initialize_revert() {
+    env e;
+
+    firstRead = true;
+    mathint bridgeCodeSize = nativeCodesize[currentContract]; // This should actually be always > 0
+
+    initialize@withrevert(e);
+
+    bool initialSetup = initializedBefore == 0 && !initializingBefore;
+    bool construction = initializedBefore == 1 && bridgeCodeSize == 0;
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = !initialSetup && !construction;
+
+    assert lastReverted <=> revert1 || revert2, "Revert rules failed";
+}
+
+// Verify correct storage changes for non reverting initialize
+rule upgradeToAndCall(address newImplementation, bytes data) {
+    env e;
+
+    require data.length == 0; // Avoid evaluating the delegatecCall part
+
+    upgradeToAndCall(e, newImplementation, data);
+
+    address implementationAfter = getImplementation();
+
+    assert implementationAfter == newImplementation, "Assert 1";
+}
+
+// Verify revert rules on upgradeToAndCall
+rule upgradeToAndCall_revert(address newImplementation, bytes data) {
+    env e;
+
+    require data.length == 0; // Avoid evaluating the delegatecCall part
+
+    address self = currentContract.__self;
+    address implementation = getImplementation();
+    mathint wardsSender = wards(e.msg.sender);
+    bytes32 newImplementationProxiableUUID = newImplementation.proxiableUUID(e);
+
+    upgradeToAndCall@withrevert(e, newImplementation, data);
+
+    bool revert1 = e.msg.value > 0;
+    bool revert2 = self == currentContract || implementation != self;
+    bool revert3 = wardsSender != 1;
+    bool revert4 = newImplementationProxiableUUID != to_bytes32(IMPLEMENTATION_SLOT());
+
+    assert lastReverted <=> revert1 || revert2 || revert3 ||
+                            revert4, "Revert rules failed";
 }
 
 // Verify correct storage changes for non reverting rely
@@ -205,7 +330,7 @@ rule bridgeERC20(address _localToken, address _remoteToken, uint256 _amount, uin
     mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
     mathint localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
     // ERC20 assumption
-    require gem.totalSupply >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;
+    require gem.totalSupply() >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;
 
     bridgeERC20(e, _localToken, _remoteToken, _amount, _minGasLimit, _extraData);
 
@@ -265,7 +390,7 @@ rule bridgeERC20To(address _localToken, address _remoteToken, address _to, uint2
     mathint localTokenBalanceOfSenderBefore = gem.balanceOf(e.msg.sender);
     mathint localTokenBalanceOfEscrowBefore = gem.balanceOf(escrow);
     // ERC20 assumption
-    require gem.totalSupply >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;
+    require gem.totalSupply() >= localTokenBalanceOfSenderBefore + localTokenBalanceOfEscrowBefore;
 
     bridgeERC20To(e, _localToken, _remoteToken, _to, _amount, _minGasLimit, _extraData);
 

certora/L2TokenBridge.conf

@@ -3,14 +3,16 @@
         "src/L2TokenBridge.sol",
         "certora/harness/Auxiliar.sol",
         "test/mocks/MessengerMock.sol",
-        "test/mocks/GemMock.sol"
+        "test/mocks/GemMock.sol",
+        "certora/harness/ImplementatioNMock.sol"
     ],
     "solc": "solc-0.8.21",
     "solc_optimize_map": {
         "L2TokenBridge": "200",
         "Auxiliar": "0",
         "MessengerMock": "0",
-        "GemMock": "0"
+        "GemMock": "0",
+        "ImplementatioNMock": "0"
     },
     "link": [
         "L2TokenBridge:messenger=MessengerMock"
@@ -22,5 +24,8 @@
     "build_cache": true,
     "optimistic_hashing": true,
     "hashing_length_bound": "512",
+    "prover_args": [
+        "-enableStorageSplitting false"
+    ],
     "msg": "L2TokenBridge"
 }