add rules on hashing

certora/conf/v1.5/safe.conf

@@ -0,0 +1,25 @@
+{
+    "files": [
+        "certora/harnesses/SafeHarness.sol"
+    ],
+    "link": [
+
+    ],
+    "verify": "SafeHarness:certora/specs/v1.5/Safe.spec",
+
+    "assert_autofinder_success": true,
+    "optimistic_summary_recursion": true,
+    "optimistic_contract_recursion": true,
+
+    "summary_recursion_limit": "2",
+    "contract_recursion_limit": "2",
+    "loop_iter": "3",
+    "optimistic_loop": true,
+    "optimistic_hashing": true,
+    "optimistic_fallback": true,
+
+    "rule_sanity": "basic",
+
+    "solc": "solc7.6",
+    "solc_via_ir": false,  
+}

certora/harnesses/SafeHarness.sol

@@ -2,6 +2,8 @@
 import "../munged/Safe.sol";
 import {SafeMath} from "../munged/external/SafeMath.sol";
 import {ISafe, IStaticFallbackMethod, IFallbackMethod, ExtensibleBase} from "../munged/handler/extensible/ExtensibleBase.sol";
+import {IFallbackHandler, FallbackHandler} from "../munged/handler/extensible/FallbackHandler.sol";
+
 
 contract SafeHarness is Safe {
     constructor(
@@ -66,6 +68,10 @@ contract SafeHarness is Safe {
         return getOwners().length;
     }
 
+    function approvedHashVal(address a, bytes32 hashInQuestion) public view returns (uint256) {
+        return approvedHashes[a][hashInQuestion];
+    }
+
     function getFallbackHandler() public view returns (address) {
         address handler;
         assembly{
@@ -74,6 +80,14 @@ contract SafeHarness is Safe {
         return handler ;
     }
 
+    function callSetSafeMethod(bytes4 selector, bytes32 newMethod) public {
+        IFallbackHandler(address(this)).setSafeMethod(selector,newMethod);
+    }
+
+    function callDummyHandler(bytes4 selector) public {
+        address(this).call(abi.encodeWithSelector(selector));
+    }
+
     function getTransactionHashPublic(
         address to,
         uint256 value,

certora/specs/v1.5/Safe.spec

@@ -0,0 +1,47 @@
+/* A specification for the Safe setup function */
+
+
+// ---- Methods block ----------------------------------------------------------
+methods {
+    function getThreshold() external returns (uint256) envfree;
+
+    function SecuredTokenTransfer.transferToken(address token, address receiver, uint256 amount) internal returns (bool) => NONDET ;
+}
+
+// ---- Functions and ghosts ---------------------------------------------------
+
+
+// ---- Invariants -------------------------------------------------------------
+
+
+// ---- Rules ------------------------------------------------------------------
+
+/// @dev approvedHashes[user][hash] can only be changed by msg.sender==user
+/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6 
+
+rule approvedHashesUpdate(method f,bytes32 userHash,address user) filtered {
+    f -> f.selector != sig:simulateAndRevert(address,bytes).selector
+} {
+    env e;
+
+    uint256 hashBefore = approvedHashVal(e,user,userHash);
+
+    calldataarg args;
+    f(e,args);
+
+    uint256 hashAfter = approvedHashVal(e,user,userHash);
+
+    assert (hashBefore != hashAfter =>
+        (e.msg.sender == user)
+    );
+}
+
+
+/// @dev approvedHashes is set when calling approveHash
+/// @status Done: https://prover.certora.com/output/39601/bb515eafa67e4edd99bb5aa51a63877b?anonymousKey=9c42e3105c1c3a3fbc95c8a24fa43b3dd43a05d6
+
+rule approvedHashesSet(bytes32 hashToApprove) {
+    env e;
+    approveHash(e,hashToApprove);
+    assert(approvedHashVal(e,e.msg.sender,hashToApprove) == 1);
+}