From ece50eb9ac05854e807f5164dd2b42a3af1e5735 Mon Sep 17 00:00:00 2001
From: teryanarmen <61996358+teryanarmen@users.noreply.github.com>
Date: Fri, 10 Feb 2023 07:21:19 -0800
Subject: [PATCH 01/10] add setup and rules about modules

---
 certora/.gitignore                 |  1 +
 certora/Makefile                   | 25 ++++++++++
 certora/applyHarness.patch         | 24 +++++++++
 certora/harnesses/SafeHarness.sol  | 22 +++++++++
 certora/scripts/base/verifySafe.sh | 12 +++++
 certora/specs/Safe.spec            | 79 ++++++++++++++++++++++++++++++
 certora/specs/properties.md        | 29 +++++++++++
 7 files changed, 192 insertions(+)
 create mode 100644 certora/.gitignore
 create mode 100644 certora/Makefile
 create mode 100644 certora/applyHarness.patch
 create mode 100644 certora/harnesses/SafeHarness.sol
 create mode 100644 certora/scripts/base/verifySafe.sh
 create mode 100644 certora/specs/Safe.spec
 create mode 100644 certora/specs/properties.md

diff --git a/certora/.gitignore b/certora/.gitignore
new file mode 100644
index 000000000..284379223
--- /dev/null
+++ b/certora/.gitignore
@@ -0,0 +1 @@
+munged
\ No newline at end of file
diff --git a/certora/Makefile b/certora/Makefile
new file mode 100644
index 000000000..06e8318dc
--- /dev/null
+++ b/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)
diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
new file mode 100644
index 000000000..c98439b5b
--- /dev/null
+++ b/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 {
diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol
new file mode 100644
index 000000000..b8e241083
--- /dev/null
+++ b/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];
+    }
+}
\ No newline at end of file
diff --git a/certora/scripts/base/verifySafe.sh b/certora/scripts/base/verifySafe.sh
new file mode 100644
index 000000000..d063ab32f
--- /dev/null
+++ b/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 "
\ No newline at end of file
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
new file mode 100644
index 000000000..8679bb411
--- /dev/null
+++ b/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);
+        }
+    }
\ No newline at end of file
diff --git a/certora/specs/properties.md b/certora/specs/properties.md
new file mode 100644
index 000000000..7aa529bb1
--- /dev/null
+++ b/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

From 2a99238be41c63db451ffec2bf79f2e10b816464 Mon Sep 17 00:00:00 2001
From: teryanarmen <61996358+teryanarmen@users.noreply.github.com>
Date: Fri, 10 Feb 2023 07:31:19 -0800
Subject: [PATCH 02/10] fix run script

---
 certora/scripts/base/verifySafe.sh | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/certora/scripts/base/verifySafe.sh b/certora/scripts/base/verifySafe.sh
index d063ab32f..c52fc56a7 100644
--- a/certora/scripts/base/verifySafe.sh
+++ b/certora/scripts/base/verifySafe.sh
@@ -1,6 +1,4 @@
-solc-select use 0.8.9
-
-certoraRun  certora/harnesses/SafeHarness.sol ComplexityCheck/DummyERC20A.sol ComplexityCheck/DummyERC20B.sol \
+certoraRun  certora/harnesses/SafeHarness.sol \
     --verify SafeHarness:certora/specs/Safe.spec \
     --staging master \
     --optimistic_loop \

From 6142597480d2ebce5daaf9da05aa925d30e8880e Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Fri, 31 Mar 2023 17:17:46 +0200
Subject: [PATCH 03/10] use solc7.6 for fv

---
 .gitignore                         | 6 +++++-
 certora/scripts/base/verifySafe.sh | 2 +-
 2 files changed, 6 insertions(+), 2 deletions(-)
 mode change 100644 => 100755 certora/scripts/base/verifySafe.sh

diff --git a/.gitignore b/.gitignore
index 18cdf9169..2e9f668b4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -11,4 +11,8 @@ bin/
 solc
 coverage/
 coverage.json
-yarn-error.log
\ No newline at end of file
+yarn-error.log
+
+# Certora Formal Verification related files
+.certora_internal
+.certora_recent_jobs.json
\ No newline at end of file
diff --git a/certora/scripts/base/verifySafe.sh b/certora/scripts/base/verifySafe.sh
old mode 100644
new mode 100755
index c52fc56a7..f477a035d
--- a/certora/scripts/base/verifySafe.sh
+++ b/certora/scripts/base/verifySafe.sh
@@ -1,6 +1,6 @@
 certoraRun  certora/harnesses/SafeHarness.sol \
     --verify SafeHarness:certora/specs/Safe.spec \
-    --staging master \
+    --solc solc7.6 \
     --optimistic_loop \
     --settings -optimisticFallback=true \
     --loop_iter 3 \

From 4d2284c628d05e88969ecc41dd58b8aa618a37e1 Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Tue, 11 Apr 2023 12:59:51 +0900
Subject: [PATCH 04/10] Update makefile

---
 certora/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/certora/Makefile b/certora/Makefile
index 06e8318dc..2afda13d2 100644
--- a/certora/Makefile
+++ b/certora/Makefile
@@ -7,7 +7,7 @@ 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 munged: 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)

From 2253f7e599480e46b94bd714968fe7a32ff53018 Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Tue, 11 Apr 2023 15:02:51 +0900
Subject: [PATCH 05/10] fix the harness patch

---
 certora/applyHarness.patch | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
index c98439b5b..ba642b665 100644
--- a/certora/applyHarness.patch
+++ b/certora/applyHarness.patch
@@ -1,19 +1,19 @@
 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
+--- Safe.sol	2023-04-11 15:01:13
++++ Safe.sol	2023-04-11 15:01:54
+@@ -76,7 +76,7 @@
+          * 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
+++        // 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 @@
+--- base/Executor.sol	2023-04-11 15:01:13
++++ base/Executor.sol	2023-04-11 15:01:18
+@@ -25,6 +25,8 @@
          Enum.Operation operation,
          uint256 txGas
      ) internal returns (bool success) {

From dc0cbf9ed3036f5701a147848b65d014d180deeb Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Wed, 12 Apr 2023 12:56:11 +0900
Subject: [PATCH 06/10] properties doc skeleton

---
 certora/specs/properties.md | 62 +++++++++++++++++++++++++++++--------
 1 file changed, 49 insertions(+), 13 deletions(-)

diff --git a/certora/specs/properties.md b/certora/specs/properties.md
index 7aa529bb1..6c68dac45 100644
--- a/certora/specs/properties.md
+++ b/certora/specs/properties.md
@@ -1,28 +1,64 @@
+# Safe Contract implementation properties
 
-only permissioned address can do permissioned activities.
-    who can swap owner?
-    who should be able to?
+## Reminder on property categories
+
+The categories are based on Certora's workshop [notes](https://github.com/Certora/Tutorials/blob/40ad7970bfafd081f6f416fe36b31981e48c6857/3DayWorkshop/SymbolicPool/properties.md).
+
+1. Valid states
+   Usually, there can be only one valid state at any given time. Such properties ensure the system is always in exactly one of its valid states.
+
+2. State transitions
+   Such properties verify the correctness of transactions between valid states. E.g., confirm valid states change according to their correct order or transitions only occur under the right conditions.
+
+3. Variable transitions
+   Similar to state transitions, but for variables. E.g., verify that Safe nonce is monotonically increasing.
+
+4. High-level properties
+   The most powerful type of properties covering the entire system. E.g., for any given operation, Safe threshold must remain lower or equal to the number of owners.
+
+5. Unit test
+   Such properties target specific function individually to verify their correctness. E.g., verify that a specific function can only be called by a specific address.
+
+6. Risk assessment
+   Such properties verify that worst cases that can happen to the system are handled correctly. E.g., verify that a transaction cannot be replayed.
 
+## Safe Contract Properties
+
+### Valid states
+
+### State transitions
+
+### Variable transitions
+
+### High-level properties
+
+### Unit test
+
+### Risk assessment
+
+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
+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
+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
+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?
+who can approve hashes?
+Can hashes do more than one thing?
 
 getStorageAt gets storage at
 

From 2524f74df35e51201e82a7527fb1fecb10e5a29e Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Thu, 20 Apr 2023 16:58:51 +0200
Subject: [PATCH 07/10] properties notes

---
 certora/specs/properties.md | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/certora/specs/properties.md b/certora/specs/properties.md
index 6c68dac45..bede0aad3 100644
--- a/certora/specs/properties.md
+++ b/certora/specs/properties.md
@@ -24,6 +24,8 @@ The categories are based on Certora's workshop [notes](https://github.com/Certor
 
 ## Safe Contract Properties
 
+Verification doesn't hold for the `DELEGATECALL` operation.
+
 ### Valid states
 
 ### State transitions
@@ -36,30 +38,29 @@ The categories are based on Certora's workshop [notes](https://github.com/Certor
 
 ### Risk assessment
 
-only permissioned address can do permissioned activities.
+- nonce monotonicity, it can only increase by 1 after execTransaction call
+
+- consistency of owner and module lists
+
+verify that `ownerCount` is in sync with the linked list. 
+always circular - each address for which `isModuleEnabled` returns true should be a part of the list
+
+
+- configuration changes to safe can only be done by the safe
 who can swap owner?
+module management
 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
+- setup only be done once
 
 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
+checkNSignatures same as checkSignature N times - ?
 
 execTransactionFromModuleReturnData
+

From e8e9241d83609ee0042d67ad5262b98dd5502f76 Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Tue, 9 May 2023 17:25:36 +0200
Subject: [PATCH 08/10] add certora workflow

---
 .github/workflows/certora.yml | 53 +++++++++++++++++++++++++++++++++++
 certora/specs/properties.md   | 19 ++++++-------
 2 files changed, 61 insertions(+), 11 deletions(-)
 create mode 100644 .github/workflows/certora.yml

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
new file mode 100644
index 000000000..bf570b40c
--- /dev/null
+++ b/.github/workflows/certora.yml
@@ -0,0 +1,53 @@
+name: certora
+
+on:
+    push:
+        branches:
+            - main
+    pull_request:
+        branches:
+            - main
+
+    workflow_dispatch:
+
+jobs:
+    verify:
+        runs-on: ubuntu-latest
+
+        steps:
+            - uses: actions/checkout@v2
+
+            - name: Install python
+              uses: actions/setup-python@v2
+              with: { python-version: 3.11 }
+
+            - name: Install java
+              uses: actions/setup-java@v1
+              with: { java-version: "19", java-package: jre }
+
+            - name: Install certora cli
+              run: pip install certora-cli
+
+            - name: Install solc
+              run: |
+                  wget https://github.com/ethereum/solidity/releases/download/v0.7.6/solc-static-linux
+                  chmod +x solc-static-linux
+                  sudo mv solc-static-linux /usr/local/bin/solc8.10
+
+            - name: Verify rule ${{ matrix.rule }}
+              run: |
+                  cd certora
+                  touch applyHarness.patch
+                  make munged
+                  cd ..
+                  echo "key length" ${#CERTORAKEY}
+                  sh certora/scripts/${{ matrix.rule }}
+              env:
+                  CERTORAKEY: ${{ secrets.CERTORAKEY }}
+
+        strategy:
+            fail-fast: false
+            max-parallel: 16
+            matrix:
+                rule:
+                    - verifySafe.sh
diff --git a/certora/specs/properties.md b/certora/specs/properties.md
index bede0aad3..761112ec0 100644
--- a/certora/specs/properties.md
+++ b/certora/specs/properties.md
@@ -38,29 +38,26 @@ Verification doesn't hold for the `DELEGATECALL` operation.
 
 ### Risk assessment
 
-- nonce monotonicity, it can only increase by 1 after execTransaction call
+-   nonce monotonicity, it can only increase by 1 after execTransaction call
 
-- consistency of owner and module lists
+-   consistency of owner and module lists
 
-verify that `ownerCount` is in sync with the linked list. 
+verify that `ownerCount` is in sync with the linked list.
 always circular - each address for which `isModuleEnabled` returns true should be a part of the list
 
-
-- configuration changes to safe can only be done by the safe
-who can swap owner?
-module management
-who should be able to?
+-   configuration changes to safe can only be done by the safe
+    who can swap owner?
+    module management
+    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
+-   setup only be done once
 
 module states
 enabled
 cancelled
-checkNSignatures same as checkSignature N times - ?
 
 execTransactionFromModuleReturnData
-

From 1c29d232c50c015a7fc835cd32142c0502a43b7e Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Wed, 10 May 2023 12:35:09 +0200
Subject: [PATCH 09/10] fix script path

---
 .github/workflows/certora.yml            | 14 +++++++-------
 .gitignore                               |  3 ++-
 certora/applyHarness.patch               |  4 ++--
 certora/harnesses/SafeHarness.sol        |  8 ++++----
 certora/scripts/{base => }/verifySafe.sh | 11 ++++++++++-
 certora/specs/Safe.spec                  |  4 +---
 6 files changed, 26 insertions(+), 18 deletions(-)
 rename certora/scripts/{base => }/verifySafe.sh (67%)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index bf570b40c..fc1d891b9 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -15,15 +15,15 @@ jobs:
         runs-on: ubuntu-latest
 
         steps:
-            - uses: actions/checkout@v2
+            - uses: actions/checkout@v3
 
             - name: Install python
-              uses: actions/setup-python@v2
+              uses: actions/setup-python@v4
               with: { python-version: 3.11 }
 
             - name: Install java
-              uses: actions/setup-java@v1
-              with: { java-version: "19", java-package: jre }
+              uses: actions/setup-java@v3
+              with: { java-version: "17", java-package: jre, distribution: semeru }
 
             - name: Install certora cli
               run: pip install certora-cli
@@ -32,7 +32,7 @@ jobs:
               run: |
                   wget https://github.com/ethereum/solidity/releases/download/v0.7.6/solc-static-linux
                   chmod +x solc-static-linux
-                  sudo mv solc-static-linux /usr/local/bin/solc8.10
+                  sudo mv solc-static-linux /usr/local/bin/solc7.6
 
             - name: Verify rule ${{ matrix.rule }}
               run: |
@@ -41,9 +41,9 @@ jobs:
                   make munged
                   cd ..
                   echo "key length" ${#CERTORAKEY}
-                  sh certora/scripts/${{ matrix.rule }}
+                  ./certora/scripts/${{ matrix.rule }}
               env:
-                  CERTORAKEY: ${{ secrets.CERTORAKEY }}
+                  CERTORAKEY: ${{ secrets.CERTORA_KEY }}
 
         strategy:
             fail-fast: false
diff --git a/.gitignore b/.gitignore
index 2e9f668b4..3d7b70cca 100644
--- a/.gitignore
+++ b/.gitignore
@@ -15,4 +15,5 @@ yarn-error.log
 
 # Certora Formal Verification related files
 .certora_internal
-.certora_recent_jobs.json
\ No newline at end of file
+.certora_recent_jobs.json
+.zip-output-url.txt
\ No newline at end of file
diff --git a/certora/applyHarness.patch b/certora/applyHarness.patch
index ba642b665..106c4562e 100644
--- a/certora/applyHarness.patch
+++ b/certora/applyHarness.patch
@@ -1,12 +1,12 @@
 diff -druN Safe.sol Safe.sol
 --- Safe.sol	2023-04-11 15:01:13
-+++ Safe.sol	2023-04-11 15:01:54
++++ Safe.sol	2023-04-11 15:01:55
 @@ -76,7 +76,7 @@
           * 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
++        // threshold = 1; MUNGED: remove and add to constructor of the harness
      }
  
      /**
diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol
index b8e241083..db95b3dcd 100644
--- a/certora/harnesses/SafeHarness.sol
+++ b/certora/harnesses/SafeHarness.sol
@@ -2,8 +2,8 @@
 import "../munged/Safe.sol";
 
 contract SafeHarness is Safe {
-
-    constructor(address[] memory _owners,
+    constructor(
+        address[] memory _owners,
         uint256 _threshold,
         address to,
         bytes memory data,
@@ -12,11 +12,11 @@ contract SafeHarness is Safe {
         uint256 payment,
         address payable paymentReceiver
     ) {
-            this.setup(_owners, _threshold, to, data, fallbackHandler, paymentToken, payment, paymentReceiver);
+        this.setup(_owners, _threshold, to, data, fallbackHandler, paymentToken, payment, paymentReceiver);
     }
 
     // harnessed getters
     function getModule(address module) public view returns (address) {
         return modules[module];
     }
-}
\ No newline at end of file
+}
diff --git a/certora/scripts/base/verifySafe.sh b/certora/scripts/verifySafe.sh
similarity index 67%
rename from certora/scripts/base/verifySafe.sh
rename to certora/scripts/verifySafe.sh
index f477a035d..fd14d87fa 100755
--- a/certora/scripts/base/verifySafe.sh
+++ b/certora/scripts/verifySafe.sh
@@ -1,3 +1,11 @@
+#!/bin/bash
+
+params=("--send_only")
+
+if [[ -n "$CI" ]]; then
+    params=()
+fi
+
 certoraRun  certora/harnesses/SafeHarness.sol \
     --verify SafeHarness:certora/specs/Safe.spec \
     --solc solc7.6 \
@@ -5,6 +13,7 @@ certoraRun  certora/harnesses/SafeHarness.sol \
     --settings -optimisticFallback=true \
     --loop_iter 3 \
     --optimistic_hashing \
+    --hashing_length_bound 352 \
     --rule_sanity \
-    --send_only \
+    "${params[@]}" \
     --msg "Safe $1 "
\ No newline at end of file
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
index 8679bb411..bff33983b 100644
--- a/certora/specs/Safe.spec
+++ b/certora/specs/Safe.spec
@@ -18,9 +18,7 @@ definition reachableOnly(method f) returns bool =
     && f.selector != simulateAndRevert(address,bytes).selector;
 
 /// Nonce must never decrease
-rule nonceMonotonicity(method f) filtered {
-    f -> noHavoc(f)
-} {
+rule nonceMonotonicity(method f) {
     uint256 nonceBefore = nonce();
 
     calldataarg args; env e;

From c8932d44a43d26b68d90c00a587f0be8f9809ea4 Mon Sep 17 00:00:00 2001
From: Mikhail <mveehkim@gmail.com>
Date: Mon, 15 May 2023 16:38:37 +0200
Subject: [PATCH 10/10] use cvl2

---
 .github/workflows/certora.yml |  4 ++--
 certora/specs/Safe.spec       | 29 ++++++++++++++++++-----------
 2 files changed, 20 insertions(+), 13 deletions(-)

diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
index fc1d891b9..d51626537 100644
--- a/.github/workflows/certora.yml
+++ b/.github/workflows/certora.yml
@@ -25,8 +25,8 @@ jobs:
               uses: actions/setup-java@v3
               with: { java-version: "17", java-package: jre, distribution: semeru }
 
-            - name: Install certora cli
-              run: pip install certora-cli
+            - name: Install certora cli-beta
+              run: pip install certora-cli-beta
 
             - name: Install solc
               run: |
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
index bff33983b..17950ca02 100644
--- a/certora/specs/Safe.spec
+++ b/certora/specs/Safe.spec
@@ -1,24 +1,31 @@
 methods {
     // 
-    getThreshold() returns (uint256) envfree
-    disableModule(address,address)
-    nonce() returns (uint256) envfree
+    function getThreshold() external returns (uint256) envfree;
+    function disableModule(address,address) external;
+    function nonce() external returns (uint256) envfree;
 
     // harnessed
-    getModule(address) returns (address) envfree
+    function getModule(address) external returns (address) envfree;
+
+    // optional
+    function execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation) external returns (bool, bytes memory);
+    function execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation) external returns (bool);
+    function execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes) external returns (bool);
 }
 
 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;
+    f.selector != sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector
+    && f.selector != sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector 
+    && f.selector != sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,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;
+    f.selector != sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector
+    && f.selector != sig:simulateAndRevert(address,bytes).selector;
 
 /// Nonce must never decrease
-rule nonceMonotonicity(method f) {
+rule nonceMonotonicity(method f) filtered {
+    f -> noHavoc(f) && reachableOnly(f)
+} {
     uint256 nonceBefore = nonce();
 
     calldataarg args; env e;
@@ -26,7 +33,7 @@ rule nonceMonotonicity(method f) {
 
     uint256 nonceAfter = nonce();
 
-    assert nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1;
+    assert nonceAfter == nonceBefore || to_mathint(nonceAfter) == nonceBefore + 1;
 }