From d9bbfb55bcef2d6f0ea93af95b95d37f1e8b9a79 Mon Sep 17 00:00:00 2001 From: Mikhail <16622558+mmv08@users.noreply.github.com> Date: Tue, 21 May 2024 15:06:06 +0200 Subject: [PATCH 1/2] upgrade certora cli/prover to 7.6.3 on the ci --- .github/workflows/certora.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index d60bd2b3f..597f74f8f 100644 --- 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: | From d3f244550fd471a89fd793c4e7d62ceaec85003b Mon Sep 17 00:00:00 2001 From: Mikhail <16622558+mmv08@users.noreply.github.com> Date: Tue, 21 May 2024 15:41:37 +0200 Subject: [PATCH 2/2] fix specs by removing redundant options and keywords --- certora/conf/nativeTokenRefund.conf | 3 ++- certora/conf/run.conf | 3 ++- certora/conf/safe.conf | 3 ++- certora/conf/signatures.conf | 3 ++- certora/scripts/verifyNativeTokenRefund.sh | 10 +--------- certora/specs/ModuleReach.spec | 4 ++-- certora/specs/OwnerReach.spec | 8 ++++---- certora/specs/Safe.spec | 6 +++--- 8 files changed, 18 insertions(+), 22 deletions(-) diff --git a/certora/conf/nativeTokenRefund.conf b/certora/conf/nativeTokenRefund.conf index 1deab7f1e..efc5e2651 100644 --- 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 index 913b78187..c3137e83d 100644 --- 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 index e7b378649..1b4d4c7a1 100644 --- 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 index 3760f2153..6c24a29f2 100644 --- 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 index e969c6e54..25ddc121f 100755 --- 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 " \ No newline at end of file diff --git a/certora/specs/ModuleReach.spec b/certora/specs/ModuleReach.spec index 8032dff59..b5cb9eac4 100644 --- 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 index 17f0f0a43..a9d758f65 100644 --- 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 index ecd55d415..4b15d43ea 100644 --- 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; }