add setup and rules about modules

certora/.gitignore

@@ -0,0 +1 @@
+munged

certora/Makefile

@@ -0,0 +1,25 @@
+default: help
+
+PATCH         = applyHarness.patch
+CONTRACTS_DIR = ../contracts
+MUNGED_DIR    = munged
+
+help:
+	@echo "usage:"
+	@echo "  make clean:  remove all generated files (those ignored by git)"
+	@echo "  make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)"
+	@echo "  make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)"
+
+munged:  $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH)
+	rm -rf $@
+	cp -r $(CONTRACTS_DIR) $@
+	patch -p0 -d $@ < $(PATCH)
+
+record:
+	diff -druN $(CONTRACTS_DIR) $(MUNGED_DIR) | sed 's+../contracts/++g' | sed 's+munged/++g' > $(PATCH)
+
+refresh: munged record
+
+clean:
+	git clean -fdX
+	touch $(PATCH)

certora/applyHarness.patch

@@ -0,0 +1,24 @@
+diff -druN Safe.sol Safe.sol
+--- Safe.sol	2023-02-08 21:35:44
++++ Safe.sol	2023-02-09 12:55:35
+@@ -60,7 +60,7 @@
+         // By setting the threshold it is not possible to call setup anymore,
+         // so we create a Safe with 0 owners and threshold 1.
+         // This is an unusable Safe, perfect for the singleton
+-        threshold = 1;
++        // threshold = 1; // MUNGED: remove and add to constructor of the harness
+     }
+
+     /// @dev Setup function sets initial storage of contract.
+diff -druN base/Executor.sol base/Executor.sol
+--- base/Executor.sol	2023-01-31 17:25:15
++++ base/Executor.sol	2023-02-09 13:44:38
+@@ -18,6 +18,8 @@
+         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;
+         if (operation == Enum.Operation.DelegateCall) {
+             // solhint-disable-next-line no-inline-assembly
+             assembly {

certora/harnesses/SafeHarness.sol

@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: LGPL-3.0-only
+import "../munged/Safe.sol";
+
+contract SafeHarness is Safe {
+
+    constructor(address[] memory _owners,
+        uint256 _threshold,
+        address to,
+        bytes memory data,
+        address fallbackHandler,
+        address paymentToken,
+        uint256 payment,
+        address payable paymentReceiver
+    ) {
+            this.setup(_owners, _threshold, to, data, fallbackHandler, paymentToken, payment, paymentReceiver);
+    }
+
+    // harnessed getters
+    function getModule(address module) public view returns (address) {
+        return modules[module];
+    }
+}

certora/scripts/base/verifySafe.sh

@@ -0,0 +1,12 @@
+solc-select use 0.8.9
+
+certoraRun  certora/harnesses/SafeHarness.sol ComplexityCheck/DummyERC20A.sol ComplexityCheck/DummyERC20B.sol \
+    --verify SafeHarness:certora/specs/Safe.spec \
+    --staging master \
+    --optimistic_loop \
+    --settings -optimisticFallback=true \
+    --loop_iter 3 \
+    --optimistic_hashing \
+    --rule_sanity \
+    --send_only \
+    --msg "Safe $1 "

certora/specs/Safe.spec

@@ -0,0 +1,79 @@
+methods {
+    // 
+    getThreshold() returns (uint256) envfree
+    disableModule(address,address)
+    nonce() returns (uint256) envfree
+
+    // harnessed
+    getModule(address) returns (address) envfree
+}
+
+definition noHavoc(method f) returns bool =
+    f.selector != execTransactionFromModuleReturnData(address,uint256,bytes,uint8).selector
+    && f.selector != execTransactionFromModule(address,uint256,bytes,uint8).selector 
+    && f.selector != execTransaction(address,uint256,bytes,uint8,uint256,uint256,uint256,address,address,bytes).selector;
+
+definition reachableOnly(method f) returns bool =
+    f.selector != setup(address[],uint256,address,bytes,address,address,uint256,address).selector
+    && f.selector != simulateAndRevert(address,bytes).selector;
+
+/// Nonce must never decrease
+rule nonceMonotonicity(method f) filtered {
+    f -> noHavoc(f)
+} {
+    uint256 nonceBefore = nonce();
+
+    calldataarg args; env e;
+    f(e, args);
+
+    uint256 nonceAfter = nonce();
+
+    assert nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1;
+}
+
+
+/// The sentinel must never point to the zero address.
+/// @notice It should either point to itself or some nonzero value
+invariant liveSentinel()
+    getModule(1) != 0
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+    { preserved {
+        requireInvariant noDeadEnds(getModule(1), 1);
+    }}
+
+/// Threshold must always be nonzero.
+invariant nonzeroThreshold()
+    getThreshold() > 0
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+
+/// Two different modules must not point to the same module/
+invariant uniquePrevs(address prev1, address prev2)
+    prev1 != prev2 && getModule(prev1) != 0 => getModule(prev1) != getModule(prev2)
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+    { 
+        preserved {
+            requireInvariant noDeadEnds(getModule(prev1), prev1);
+            requireInvariant noDeadEnds(getModule(prev2), prev2);
+            requireInvariant uniquePrevs(prev1, 1);
+            requireInvariant uniquePrevs(prev2, 1);
+            requireInvariant uniquePrevs(prev1, getModule(prev2));
+            requireInvariant uniquePrevs(prev2, getModule(prev1));
+        }
+    }
+
+/// A module that points to the zero address must not have another module pointing to it.
+invariant noDeadEnds(address dead, address lost)
+    dead != 0 && getModule(dead) == 0 => getModule(lost) != dead
+    filtered { f -> noHavoc(f) && reachableOnly(f) }
+    {
+        preserved {
+            requireInvariant liveSentinel();
+            requireInvariant noDeadEnds(getModule(1), 1);
+        }
+        preserved disableModule(address prevModule, address module) with (env e) {
+            requireInvariant uniquePrevs(prevModule, lost);
+            requireInvariant uniquePrevs(prevModule, dead);
+            requireInvariant noDeadEnds(dead, module);
+            requireInvariant noDeadEnds(module, dead);
+        }
+    }

certora/specs/properties.md

@@ -0,0 +1,29 @@
+
+only permissioned address can do permissioned activities.
+    who can swap owner?
+    who should be able to?
+
+
+who should be allowed to make contract do delegate calls?
+    contract creator
+    address specified by contract creator
+
+setup only be done once
+
+check signature validation?
+    can't sign a signature that isn't yours...
+    not really something we can prove
+
+module states
+    enabled
+    cancelled
+    always circular
+    checkNSignatures same as checkSignature N times
+
+properties about approved hashes
+    who can approve hashes?
+    Can hashes do more than one thing?
+
+getStorageAt gets storage at
+
+execTransactionFromModuleReturnData