Upgrade Certora CLI and Prover to v7.6.3 on the CI (safe-global#761)

Changelog is available here: https://docs.certora.com/en/latest/docs/prover/changelog/prover_changelog.html#may-15-2024 I also fixed the `verifyNativeTokenRefund` ruleset not using the configuration file.
haqq-network · May 28, 2024 · a9e3385 · a9e3385
1 parent f830466
commit a9e3385
Show file tree

Hide file tree

Showing 9 changed files with 19 additions and 23 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -29,7 +29,7 @@ jobs:
               with: { java-version: "17", java-package: jre, distribution: semeru }
 
             - name: Install certora cli
-              run: pip install -Iv certora-cli==6.3.1
+              run: pip install -Iv certora-cli==7.6.3
 
             - name: Install solc
               run: |

diff --git a/certora/conf/nativeTokenRefund.conf b/certora/conf/nativeTokenRefund.conf
@@ -7,9 +7,10 @@
     "msg": "Safe Native Token Refund",
     "optimistic_hashing": true,
     "optimistic_loop": true,
+    "optimistic_fallback": true,
     "process": "emv",
     "prover_args": [
-        " -optimisticFallback true -mediumTimeout 30"
+        "-mediumTimeout 30"
     ],
     "rule_sanity": "basic",
     "solc": "solc7.6",

diff --git a/certora/conf/run.conf b/certora/conf/run.conf
@@ -7,9 +7,10 @@
     "msg": "Safe Mutation",
     "optimistic_hashing": true,
     "optimistic_loop": true,
+    "optimistic_fallback": true,
     "process": "emv",
     "prover_args": [
-        " -optimisticFallback true -s z3 -copyLoopUnroll 5 -mediumTimeout 5 -depth 30"
+        "-s z3 -copyLoopUnroll 5 -mediumTimeout 5 -depth 30"
     ],
     "rule_sanity": "basic",
     "run_source": "MUTATION",

diff --git a/certora/conf/safe.conf b/certora/conf/safe.conf
@@ -7,9 +7,10 @@
     "msg": "Safe General Ruleset",
     "optimistic_hashing": true,
     "optimistic_loop": true,
+    "optimistic_fallback": true,
     "process": "emv",
     "prover_args": [
-        " -optimisticFallback true -s z3 -copyLoopUnroll 5 -mediumTimeout 5 -depth 30"
+        "-s z3 -copyLoopUnroll 5 -mediumTimeout 5 -depth 30"
     ],
     "rule_sanity": "basic",
     "solc": "solc7.6",

diff --git a/certora/conf/signatures.conf b/certora/conf/signatures.conf
@@ -7,9 +7,10 @@
     "msg": "Safe Signatures Rules",
     "optimistic_hashing": true,
     "optimistic_loop": true,
+    "optimistic_fallback": true,
     "process": "emv",
     "prover_args": [
-        "-optimisticFallback true -mediumTimeout 30"
+        "-mediumTimeout 30"
     ],
     "rule_sanity": "basic",
     "solc": "solc7.6",

diff --git a/certora/scripts/verifyNativeTokenRefund.sh b/certora/scripts/verifyNativeTokenRefund.sh
@@ -6,14 +6,6 @@ if [[ -n "$CI" ]]; then
     params=()
 fi
 
-certoraRun  certora/harnesses/SafeHarness.sol \
-    --verify SafeHarness:certora/specs/NativeTokenRefund.spec \
-    --solc solc7.6 \
-    --optimistic_loop \
-    --prover_args '-optimisticFallback true -s z3' \
-    --loop_iter 3 \
-    --optimistic_hashing \
-    --hashing_length_bound 352 \
-    --rule_sanity \
+certoraRun  certora/conf/nativeTokenRefund.conf \
     "${params[@]}" \
     --msg "Safe $1 "
diff --git a/certora/specs/ModuleReach.spec b/certora/specs/ModuleReach.spec
@@ -157,7 +157,7 @@ definition updateSucc(address a, address b) returns bool = forall address X. for
 // hook to update the ghostModules and the reach ghost state whenever the modules field
 // in storage is written. 
 // This also checks that the reach_succ invariant is preserved. 
-hook Sstore currentContract.modules[KEY address key] address value STORAGE {
+hook Sstore currentContract.modules[KEY address key] address value {
     address valueOrNull;
     address someKey;
     require reach_succ(someKey, ghostModules[someKey]);
@@ -171,7 +171,7 @@ hook Sstore currentContract.modules[KEY address key] address value STORAGE {
 
 // Hook to match ghost state and storage state when reading modules from storage. 
 // This also provides the reach_succ invariant. 
-hook Sload address value currentContract.modules[KEY address key] STORAGE {
+hook Sload address value currentContract.modules[KEY address key] {
     require ghostModules[key] == value;
     require reach_succ(key, value);
 }

diff --git a/certora/specs/OwnerReach.spec b/certora/specs/OwnerReach.spec
@@ -202,7 +202,7 @@ definition updateGhostSuccCount(address key, mathint diff) returns bool = forall
 // hook to update the ghostOwners and the reach ghost state whenever the owners field
 // in storage is written.
 // This also checks that the reach_succ invariant is preserved.
-hook Sstore currentContract.owners[KEY address key] address value STORAGE {
+hook Sstore currentContract.owners[KEY address key] address value {
     address valueOrNull;
     address someKey;
     require reach_succ(someKey, ghostOwners[someKey]);
@@ -216,19 +216,19 @@ hook Sstore currentContract.owners[KEY address key] address value STORAGE {
     assert ghostSuccCount(someKey) == count_expected(someKey);
 }
 
-hook Sstore currentContract.ownerCount uint256 value STORAGE {
+hook Sstore currentContract.ownerCount uint256 value {
     ghostOwnerCount = value;
 }
 
 // Hook to match ghost state and storage state when reading owners from storage.
 // This also provides the reach_succ invariant.
-hook Sload address value currentContract.owners[KEY address key] STORAGE {
+hook Sload address value currentContract.owners[KEY address key] {
     require ghostOwners[key] == value;
     require reach_succ(key, value);
     require ghostSuccCount(key) == count_expected(key);
 }
 
-hook Sload uint256 value currentContract.ownerCount STORAGE {
+hook Sload uint256 value currentContract.ownerCount {
     // The prover found a counterexample if the owners count is max uint256,
     // but this is not a realistic scenario.
     require ghostOwnerCount < MAX_UINT256();

diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
@@ -54,14 +54,14 @@ persistent ghost address ghostSingletonAddress {
     init_state axiom ghostSingletonAddress == 0;
 }
 
-hook Sstore SafeHarness.(slot 0) address newSingletonAddress STORAGE {
+hook Sstore SafeHarness.(slot 0) address newSingletonAddress {
     ghostSingletonAddress = newSingletonAddress;
 }
 
 // This is EIP-1967's singleton storage slot:
 // 0x360894a13ba1a3210667c828492db98dca3e2076cc3735a920a3ca505d382bbc
 // converted to decimal because certora doesn't seem to support hex yet.
-hook Sstore SafeHarness.(slot 24440054405305269366569402256811496959409073762505157381672968839269610695612) address newSingletonAddress STORAGE {
+hook Sstore SafeHarness.(slot 24440054405305269366569402256811496959409073762505157381672968839269610695612) address newSingletonAddress {
     ghostSingletonAddress = newSingletonAddress;
 }
 
@@ -76,7 +76,7 @@ persistent ghost address fallbackHandlerAddress {
 // This is Safe's fallback handler storage slot:
 // 0x6c9a6c4a39284e37ed1cf53d337577d14212a4870fb976a4366c693b939918d5
 // converted to decimal because certora doesn't seem to support hex yet.
-hook Sstore SafeHarness.(slot 49122629484629529244014240937346711770925847994644146912111677022347558721749) address newFallbackHandlerAddress STORAGE {
+hook Sstore SafeHarness.(slot 49122629484629529244014240937346711770925847994644146912111677022347558721749) address newFallbackHandlerAddress {
     fallbackHandlerAddress = newFallbackHandlerAddress;
 }