fix script path

Author: mmv08

.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

.gitignore

@@ -15,4 +15,5 @@ yarn-error.log
 
 # Certora Formal Verification related files
 .certora_internal
-.certora_recent_jobs.json
+.certora_recent_jobs.json
+.zip-output-url.txt

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
      }
 
      /**

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];
     }
-}
+}

certora/scripts/base/verifySafe.sh certora/scripts/verifySafe.shcertora/scripts/base/verifySafe.sh renamed to certora/scripts/verifySafe.sh

@@ -1,10 +1,19 @@
+#!/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 \
     --optimistic_loop \
     --settings -optimisticFallback=true \
     --loop_iter 3 \
     --optimistic_hashing \
+    --hashing_length_bound 352 \
     --rule_sanity \
-    --send_only \
+    "${params[@]}" \
     --msg "Safe $1 "

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;