Upgrade certora spec files and CI to certora-cli v6 (#732)

This PR updates the certora cli to the latest available v6 version. The
main breaking change is that ghosts have to be marked persistent if we
don't want them to be HAVOC'ed on, let's say, an external call.

Author: mmv08

.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==5.0.5
+              run: pip install -Iv certora-cli==6.3.1
 
             - name: Install solc
               run: |

certora/specs/ModuleReach.spec

@@ -21,18 +21,19 @@ methods {
 definition reachableOnly(method f) returns bool =
     f.selector != sig:simulateAndRevert(address,bytes).selector;
 
-ghost reach(address, address) returns bool {
+persistent ghost reach(address, address) returns bool {
     init_state axiom forall address X. forall address Y. reach(X, Y) == (X == Y || to_mathint(Y) == 0);
 }
 
-ghost mapping(address => address) ghostModules {
+persistent ghost mapping(address => address) ghostModules {
     init_state axiom forall address X. to_mathint(ghostModules[X]) == 0;
 }
 
-ghost address SENTINEL {
+persistent ghost address SENTINEL {
     axiom to_mathint(SENTINEL) == 1;    
 }
-ghost address NULL {
+
+persistent ghost address NULL {
     axiom to_mathint(NULL) == 0;    
 }
 

certora/specs/NativeTokenRefund.spec

@@ -7,7 +7,7 @@ methods {
     function getSafeGuard() external returns (address) envfree;
 }
 
-ghost uint256 gasPriceEnv {
+persistent ghost uint256 gasPriceEnv {
     init_state axiom gasPriceEnv == 1;
 }
 

certora/specs/OwnerReach.spec

@@ -24,24 +24,25 @@ definition reachableOnly(method f) returns bool =
 
 definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffff;
 
-ghost reach(address, address) returns bool {
+persistent ghost reach(address, address) returns bool {
     init_state axiom forall address X. forall address Y. reach(X, Y) == (X == Y || to_mathint(Y) == 0);
 }
 
-ghost mapping(address => address) ghostOwners {
+persistent ghost mapping(address => address) ghostOwners {
     init_state axiom forall address X. to_mathint(ghostOwners[X]) == 0;
 }
 
-ghost ghostSuccCount(address) returns mathint {
+persistent ghost ghostSuccCount(address) returns mathint {
     init_state axiom forall address X. ghostSuccCount(X) == 0;
 }
 
-ghost uint256 ghostOwnerCount;
+persistent ghost uint256 ghostOwnerCount;
 
-ghost address SENTINEL {
+persistent ghost address SENTINEL {
     axiom to_mathint(SENTINEL) == 1;
 }
-ghost address NULL {
+
+persistent ghost address NULL {
     axiom to_mathint(NULL) == 0;
 }
 

certora/specs/Safe.spec

@@ -50,7 +50,7 @@ rule nonceMonotonicity(method f) filtered {
 
 
 // The singleton is a private variable, so we need to use a ghost variable to track it.
-ghost address ghostSingletonAddress {
+persistent ghost address ghostSingletonAddress {
     init_state axiom ghostSingletonAddress == 0;
 }
 
@@ -69,7 +69,7 @@ invariant singletonAddressNeverChanges()
     ghostSingletonAddress == 0
     filtered { f -> reachableOnly(f) && f.selector != sig:getStorageAt(uint256,uint256).selector }
 
-ghost address fallbackHandlerAddress {
+persistent ghost address fallbackHandlerAddress {
     init_state axiom fallbackHandlerAddress == 0;
 }
 

certora/specs/Signatures.spec

@@ -33,22 +33,9 @@ methods {
 
 definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff;
 
-ghost mapping(bytes => mapping(uint256 => uint8)) mySigSplitV;
-ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitR;
-ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitS;
-
-// This is needed for the execTransaction <> signatures rule
-ghost transactionHashGhost(
-        address /*to */,
-        uint256 /*value */,
-        bytes,
-        Enum.Operation /*operation*/,
-        uint256 /*safeTxGas */,
-        uint256 /*baseGas*/,
-        uint256 /*gasPrice*/,
-        address /*gasToken*/,
-        address /*refundReceiver*/,
-        uint256 /*_nonce*/ ) returns bytes32 ;
+persistent ghost mapping(bytes => mapping(uint256 => uint8)) mySigSplitV;
+persistent ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitR;
+persistent ghost mapping(bytes => mapping(uint256 => bytes32)) mySigSplitS;
 
 function signatureSplitGhost(bytes signatures, uint256 pos) returns (uint8,bytes32,bytes32) {
     return (mySigSplitV[signatures][pos], mySigSplitR[signatures][pos], mySigSplitS[signatures][pos]);