change Safe spec to Hash spec for more accurate naming

certora/conf/v1.5/safe.conf → certora/conf/v1.5/hash.conf

@@ -5,7 +5,7 @@
     "link": [
 
     ],
-    "verify": "SafeHarness:certora/specs/v1.5/Safe.spec",
+    "verify": "SafeHarness:certora/specs/v1.5/Hash.spec",
 
     "assert_autofinder_success": true,
     "optimistic_summary_recursion": true,

certora/specs/v1.5/Hash.spec

@@ -0,0 +1,45 @@
+/* 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 setup can only be called if threshold = 0 and setup sets threshold > 0 
+/// @status Done: https://prover.certora.com/output/39601/7849e9a464e042ea89bfe68fc226edbc?anonymousKey=5c1387afecb8bc86f23df3be5eb886a5cd82787f
+
+rule setupThresholdZeroAndSetsPositiveThreshold(
+        address[] _owners,
+        uint256 _threshold,
+        address to,
+        bytes data,
+        address fallbackHandler,
+        address paymentToken,
+        uint256 payment,
+        address paymentReceiver) {
+    env e;
+
+    uint256 old_threshold = getThreshold();
+
+    // a successful call to setup
+    setup(e,_owners,_threshold,to,data,fallbackHandler,
+        paymentToken,payment,paymentReceiver);
+
+    uint256 new_threshold = getThreshold();
+
+    assert (
+        new_threshold >  0 &&
+        old_threshold == 0
+    );
+}