From 206a82b73201f5831cd5929b674c8d9ce2b4d419 Mon Sep 17 00:00:00 2001
From: Derek Sorensen <derek-certora@Dereks-MacBook-Pro.local>
Date: Wed, 18 Dec 2024 14:43:32 +0000
Subject: [PATCH] extend some rules, deprecate/remove fixes used because I
 couldn't resolve some CVL issues, filter the invariant
 fallbackHanlderNeverSelf for sanity, etc. overall improvement of rules for
 fallback

---
 certora/harnesses/SafeHarness.sol |  5 ---
 certora/specs/v1.5/Fallback.spec  | 64 ++++++++++++++++++++++++-------
 2 files changed, 50 insertions(+), 19 deletions(-)

diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol
index d94159ff4..402ca86e2 100644
--- a/certora/harnesses/SafeHarness.sol
+++ b/certora/harnesses/SafeHarness.sol
@@ -74,11 +74,6 @@ contract SafeHarness is Safe {
         return handler ;
     }
 
-    // TODO deprecate this with CVL2
-    function addressToBytes32(address addr) public pure returns (bytes32) {
-        return bytes32(uint256(uint160(addr)));
-    }
-
     function getTransactionHashPublic(
         address to,
         uint256 value,
diff --git a/certora/specs/v1.5/Fallback.spec b/certora/specs/v1.5/Fallback.spec
index 2c6a1555b..5836a7a46 100644
--- a/certora/specs/v1.5/Fallback.spec
+++ b/certora/specs/v1.5/Fallback.spec
@@ -9,8 +9,7 @@ using SafeHarness as safe;
 methods {
 
     function getFallbackHandler() external returns (address) envfree;
-    function addressToBytes32(address) external returns (bytes32) envfree;
-
+    
     function _.handle(address _safe, address sender, uint256 value, bytes data) external => DISPATCHER(true);
 }
 
@@ -36,36 +35,73 @@ rule setFallbackIntegrity(address handler) {
 }
 
 /// @dev invariant: the address in fallback handler slot is never self
-/// @status Done (?)s: https://prover.certora.com/output/39601/103eb341ceef481c830e0ba04eb06766?anonymousKey=61cb4fd6726ab3d0fad887f6393865263eecf3f0
-invariant fallbackHanlderNeverSelf()
-    getFallbackHandler() != safe ;
+/// @status Done: https://prover.certora.com/output/39601/edb75f86f23445cdbc7cd7b5c4c420b6?anonymousKey=62191f4f70404bcbce784f5172e3ed7ab323d416
+invariant fallbackHanlderNeverSelf() 
+    getFallbackHandler() != safe
+    filtered { 
+        f -> f.selector != sig:simulateAndRevert(address,bytes).selector 
+    }
+
+// for soundness of fallbackHanlderNeverSelf, we prove a rule that simulateAndRevert always reverts
+rule simulateAndRevertReverts(address caddr, bytes b) {
+    env e;
+    simulateAndRevert@withrevert(e,caddr,b);
+    assert lastReverted;
+}
+
+/// @dev 3 rules for set safe method integrity: sets/modifies/removes handler
+/// @status Done: https://prover.certora.com/output/39601/bab9860cdfc44a83bed82e79d8c06218?anonymousKey=b4c5dbef050bb201ad78b3dd5af5cdca8ffa9f92
+rule setSafeMethodSets(bytes4 selector, address newMethodCaddr) {
+    env e; 
 
+    bytes32 newMethod = to_bytes32(assert_uint256(newMethodCaddr));
+
+    fallbackHandler.setSafeMethod(e,selector,newMethod);
+    bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector);
+
+    assert (thisMethod == thisMethod);
+}
 
-/// @dev set safe method integrity: sets/modifies/removes handler  
-/// @status Done: https://prover.certora.com/output/39601/09912f9691e04917b4c0277e30ad8e38?anonymousKey=61db5fd06c13a287939455e3a531ff841442ee2e
-rule setSafeMethodIntegrity(bytes4 selector, address newMethod_addr) {
+/// @status Done: https://prover.certora.com/output/39601/8591535c4a434f3e826af00b95ea1ca8?anonymousKey=a7b6743a3161a3289883f99014619a9d6e7196e1
+/// note this is a special case of the rule above, but we still include it here for illustration
+rule setSafeMethodRemoves(bytes4 selector) {
     env e; 
 
-    bytes32 newMethod = addressToBytes32(newMethod_addr);
+    bytes32 newMethod = to_bytes32(0); // call setSafeMethod with the zero address
 
     fallbackHandler.setSafeMethod(e,selector,newMethod);
-    bytes32 this_method = fallbackHandler.getSafeMethod(e,e.msg.sender,selector);
+    bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector);
+
+    assert (thisMethod == to_bytes32(0)); // there is nothing stored
+}
+
+/// @status Done: https://prover.certora.com/output/39601/b44efe9ef3bd4ff5a1af710a7d3d7ee4?anonymousKey=7fd15cc355164c803123c27b41660fed34548647 
+rule setSafeMethodChanges(bytes4 selector, address newMethodCaddr) {
+    env e; 
+
+    bytes32 newMethod = to_bytes32(assert_uint256(newMethodCaddr));
+    bytes32 oldMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector);
+    require (newMethod != oldMethod); // we are changing the method address
+
+    fallbackHandler.setSafeMethod(e,selector,newMethod);
+
+    bytes32 thisMethod = fallbackHandler.getSafeMethod(e,e.msg.sender,selector);
 
-    assert (newMethod == this_method);
+    assert (thisMethod == newMethod);
 }
 
 
 /// @dev a handler, once set via setSafeMethod, is possible to call
 /// @status Done: https://prover.certora.com/output/39601/9fcde04ecd434963b9ce788f7ddea8c1?anonymousKey=a7efde58b28ef7c99264424b66984a8d39b78518
-rule hanlderCallableIfSet(bytes4 selector,method f) filtered { f -> f.isFallback } {
+rule hanlderCallableIfSet(method f) filtered { f -> f.isFallback } {
     env e;
 
     // the fallback handler is in the scene
     require (getFallbackHandler() == fallbackHandler);
 
     // the dummy (sub) handler is a valid handler for this safe
-    bytes32 dummy_bytes = addressToBytes32(dummyHandler); // TODO to_bytes32 from CVL2
-    //  bytes4 selector = to_bytes4(00); // 0x00 indicates this is a non-static call
+    bytes32 dummy_bytes = to_bytes32(assert_uint256(dummyHandler));
+    bytes4 selector = to_bytes4(00); // 0x00 indicates this is a non-static call
     fallbackHandler.setSafeMethod(e,selector,dummy_bytes); // we've set the dummy as a handler
 
     // reset the check to see if dummy handler has been called