Add an optimistic assumption about DELEGATECALL, update nonce monoton…

…icity rule (#574)

certora/applyHarness.patch

@@ -1,6 +1,6 @@
 diff -druN Safe.sol Safe.sol
---- Safe.sol	2023-04-11 15:01:13
-+++ Safe.sol	2023-04-11 15:01:55
+--- Safe.sol	2023-05-16 15:08:39
++++ Safe.sol	2023-05-25 16:23:56
 @@ -76,7 +76,7 @@
           * so we create a Safe with 0 owners and threshold 1.
           * This is an unusable Safe, perfect for the singleton
@@ -11,14 +11,19 @@ diff -druN Safe.sol Safe.sol
 
      /**
 diff -druN base/Executor.sol base/Executor.sol
---- base/Executor.sol	2023-04-11 15:01:13
-+++ base/Executor.sol	2023-04-11 15:01:18
-@@ -25,6 +25,8 @@
+--- base/Executor.sol	2023-05-16 15:08:39
++++ base/Executor.sol	2023-05-25 16:23:31
+@@ -25,11 +25,9 @@
          Enum.Operation operation,
          uint256 txGas
      ) internal returns (bool success) {
-+        // MUNGED lets just be a bit more optimistic, `execute` does nothing and always returns true
-+        return true;
++        // MUNGED lets just be a bit more optimistic, `execute` does nothing for `DELEGATECALL` and always returns true
          if (operation == Enum.Operation.DelegateCall) {
+-            // solhint-disable-next-line no-inline-assembly
+-            assembly {
+-                success := delegatecall(txGas, to, add(data, 0x20), mload(data), 0, 0)
+-            }
++            return true;
+         } else {
              // solhint-disable-next-line no-inline-assembly
              assembly {

certora/specs/Safe.spec

@@ -23,20 +23,25 @@ definition reachableOnly(method f) returns bool =
     f.selector != sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector
     && f.selector != sig:simulateAndRevert(address,bytes).selector;
 
+definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffff;
 
 /// Nonce must never decrease
 rule nonceMonotonicity(method f) filtered {
-    f -> noHavoc(f) && reachableOnly(f) &&
+    f -> reachableOnly(f) &&
          f.selector != sig:getStorageAt(uint256,uint256).selector
 } {
     uint256 nonceBefore = nonce();
 
+    // The nonce may overflow, but since it's increased only by 1 with each transaction, it is not realistically possible to overflow it.
+    require nonceBefore < MAX_UINT256();
+
     calldataarg args; env e;
     f(e, args);
 
     uint256 nonceAfter = nonce();
 
-    assert nonceAfter == nonceBefore || to_mathint(nonceAfter) == nonceBefore + 1;
+    assert nonceAfter != nonceBefore =>
+        to_mathint(nonceAfter) == nonceBefore + 1 && f.selector == sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector;
 }
 
 
@@ -129,7 +134,7 @@ rule fallbackHandlerAddressChange(method f) filtered {
 
     address fbHandlerAfter = fallbackHandlerAddress;
 
-    assert fbHandlerBefore != fbHandlerAfter => 
+    assert fbHandlerBefore != fbHandlerAfter =>
         f.selector == sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector || f.selector == sig:setFallbackHandler(address).selector;
 }
 
@@ -145,6 +150,6 @@ rule guardAddressChange(method f) filtered {
 
     address guardAfter = getSafeGuard();
 
-    assert guardBefore != guardAfter => 
+    assert guardBefore != guardAfter =>
         f.selector == sig:setGuard(address).selector;
 }