Merge e52e98f into ad9b319

certora/specs/Safe.spec

@@ -81,4 +81,29 @@ invariant noDeadEnds(address dead, address lost)
             requireInvariant noDeadEnds(dead, module);
             requireInvariant noDeadEnds(module, dead);
         }
-    }
+    }
+
+ghost address fallbackHandlerAddress {
+    init_state axiom fallbackHandlerAddress == 0;
+}
+
+// This is Safe's fallback handler storage slot:
+// 0x6c9a6c4a39284e37ed1cf53d337577d14212a4870fb976a4366c693b939918d5
+// converted to decimal because certora doesn't seem to support hex yet.
+hook Sstore SafeHarness.(slot 49122629484629529244014240937346711770925847994644146912111677022347558721749) address newFallbackHandlerAddress STORAGE {
+    fallbackHandlerAddress = newFallbackHandlerAddress;
+}
+
+rule fallbackHandlerAddressChange(method f) filtered {
+    f -> f.selector != sig:simulateAndRevert(address,bytes).selector
+} {
+    address fbHandlerBefore = fallbackHandlerAddress;
+
+    calldataarg args; env e;
+    f(e, args);
+
+    address fbHandlerAfter = fallbackHandlerAddress;
+
+    assert fbHandlerBefore != fbHandlerAfter => 
+        f.selector == sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector || f.selector == sig:setFallbackHandler(address).selector;
+}