Merge pull request #174 from euler-xyz/update-certora

kasperpawlowski · web-flow · commit 6b9be5cb82ee · 2024-10-16T10:07:59.000+02:00
Update certora
diff --git a/.github/executables/solc b/.github/executables/solc
@@ -1 +1 @@
-solc8.20
+solc8.24
diff --git a/.github/executables/solc8.24 b/.github/executables/solc8.24
diff --git a/.github/workflows/checkrules.yml b/.github/workflows/checkrules.yml
@@ -20,7 +20,7 @@ jobs:
 
       - name: setup cvt
         run: |
-          pip install certora-cli==7.6.3
+          pip install certora-cli
           echo "`pwd`/.github/executables" >> $GITHUB_PATH
 
       - name: run certora prover on conf files
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -34,7 +34,7 @@ jobs:
                 submodules: recursive
           - uses: foundry-rs/foundry-toolchain@v1
             with:
-                version: nightly
+                version: nightly-c99854277c346fa6de7a8f9837230b36fd85850e
 
           - name: Run foundry fmt check
             run: |
diff --git a/certora/conf/CER-1-Owner/CER-59-Owner-override.conf b/certora/conf/CER-1-Owner/CER-59-Owner-override.conf
@@ -7,7 +7,7 @@
         "@openzeppelin=lib/openzeppelin-contracts"
     ],
     "prover_args": [
-        "-useBitVectorTheory"
+        "-useBitVectorTheory true"
     ],
     "function_finder_mode": "relaxed",
     "solc_via_ir" : true,
@@ -16,7 +16,7 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-1-Owner/CER-59-Owner-addressPrefix",
-    "solc": "solc8.20",
+    "solc": "solc8.24",
     "rule_sanity": "basic",
     "hashing_length_bound": "256"
 }
diff --git a/certora/conf/CER-1-Owner/CER-60-Owner-addressPrefix.conf b/certora/conf/CER-1-Owner/CER-60-Owner-addressPrefix.conf
@@ -7,14 +7,14 @@
         "@openzeppelin=lib/openzeppelin-contracts"
     ],
     "prover_args": [
-        "-useBitVectorTheory"
+        "-useBitVectorTheory true"
     ],
     "solc_via_ir" : true,
     "assert_autofinder_success" : true,
     "optimistic_loop": true,
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-1-Owner/CER-60-Owner-addressPrefix",
-    "solc": "solc8.20",
+    "solc": "solc8.24",
     "rule_sanity": "basic"
 }
diff --git a/certora/conf/CER-11-Controllers/CER-12-Controllers-number.conf b/certora/conf/CER-11-Controllers/CER-12-Controllers-number.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-11-Controllers/CER-12-Controllers-number.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "solc_via_ir": true,
   "msg": "CER-11-Controllers/CER-12-Controllers-number",
diff --git a/certora/conf/CER-11-Controllers/CER-56-Controllers-disabling.conf b/certora/conf/CER-11-Controllers/CER-56-Controllers-disabling.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-11-Controllers/CER-56-Controllers-disabling.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "solc_via_ir": true,
   "msg": "CER-11-Controllers/CER-56-Controllers-disabling",
diff --git a/certora/conf/CER-11-Controllers/CER-81-Controllers-restrictions.conf b/certora/conf/CER-11-Controllers/CER-81-Controllers-restrictions.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-11-Controllers/CER-81-Controllers-restrictions.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "solc_via_ir": true,
   "msg": "CER-11-Controllers/CER-81-Controllers-restrictions",
diff --git a/certora/conf/CER-15-Permit/CER-51-Permit-msg-sender.conf b/certora/conf/CER-15-Permit/CER-51-Permit-msg-sender.conf
@@ -13,5 +13,5 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-15-Permit/CER-51-Permit-msg-sender",    
-    "solc": "solc8.20"
+    "solc": "solc8.24"
 }
diff --git a/certora/conf/CER-15-Permit/CER-65-Permit-onBehalfOfAccount.conf b/certora/conf/CER-15-Permit/CER-65-Permit-onBehalfOfAccount.conf
@@ -13,6 +13,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-15-Permit/CER-65-Permit-onBehalfOfAccount",
-    "solc": "solc8.20",
+    "solc": "solc8.24",
     "hashing_length_bound": "256"
 }
diff --git a/certora/conf/CER-2-Operator/CER-52-Operator-deauthorization.conf b/certora/conf/CER-2-Operator/CER-52-Operator-deauthorization.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-2-Operator/CER-52-Operator-deauthorization.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "rule_sanity": "basic",
   "solc_via_ir": true,
diff --git a/certora/conf/CER-2-Operator/CER-54-Operator-owner.conf b/certora/conf/CER-2-Operator/CER-54-Operator-owner.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-2-Operator/CER-54-Operator-owner.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "rule_sanity": "basic",
   "solc_via_ir": true,
diff --git a/certora/conf/CER-2-Operator/CER-62-Operator-setAccountOperator.conf b/certora/conf/CER-2-Operator/CER-62-Operator-setAccountOperator.conf
@@ -10,5 +10,5 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg" : "CER-2-Operator/CER-62-Operator-setAccountOperator",
-    "solc": "solc8.20"
+    "solc": "solc8.24"
 }
diff --git a/certora/conf/CER-2-Operator/CER-68-Operator-authorization.conf b/certora/conf/CER-2-Operator/CER-68-Operator-authorization.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-2-Operator/CER-68-Operator-authorization.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "rule_sanity": "basic",
   "solc_via_ir": true,
diff --git a/certora/conf/CER-20-ChecksDeferrable/CER-22-ChecksDeferrable-controlCollateral.conf b/certora/conf/CER-20-ChecksDeferrable/CER-22-ChecksDeferrable-controlCollateral.conf
@@ -11,5 +11,5 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-20-ChecksDeferrable/CER-22-ChecksDeferrable-controlCollateral",
-    "solc": "solc8.20"
+    "solc": "solc8.24"
 }
diff --git a/certora/conf/CER-20-ChecksDeferrable/CER-23-ChecksDeferrable-callbatch-callback.conf b/certora/conf/CER-20-ChecksDeferrable/CER-23-ChecksDeferrable-callbatch-callback.conf
@@ -13,5 +13,5 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-20-ChecksDeferrable/CER-23-ChecksDeferrable-callbatch-callback",
-    "solc": "solc8.20",
+    "solc": "solc8.24",
 }
diff --git a/certora/conf/CER-27-ExecutionContext/CER-32-ExecutionContext-checksDeferred.conf b/certora/conf/CER-27-ExecutionContext/CER-32-ExecutionContext-checksDeferred.conf
@@ -11,5 +11,5 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-27-ExecutionContext/CER-32-ExecutionContext-checksDeferred",
-    "solc": "solc8.20"
+    "solc": "solc8.24"
 }
diff --git a/certora/conf/CER-27-ExecutionContext/CER-33-ExecutionContext-onBehalfOfAccount.conf b/certora/conf/CER-27-ExecutionContext/CER-33-ExecutionContext-onBehalfOfAccount.conf
@@ -11,5 +11,5 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-27-ExecutionContext/CER-33-ExecutionContext-onBehalfOfAccount",
-    "solc": "solc8.20"
+    "solc": "solc8.24"
 }
diff --git a/certora/conf/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.conf b/certora/conf/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.conf
@@ -10,6 +10,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-27-ExecutionContext/CER-38-ExecutionContext-restored",
-    "solc": "solc8.20",
+    "solc": "solc8.24",
     "hashing_length_bound": "256"
 }
diff --git a/certora/conf/CER-40-AccountStatusCheck/CER-326-checkStatusAll-called.conf b/certora/conf/CER-40-AccountStatusCheck/CER-326-checkStatusAll-called.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-40-AccountStatusCheck/CER-326-checkStatusAll-called.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "rule_sanity": "basic",
   "solc_via_ir": true,
diff --git a/certora/conf/CER-40-AccountStatusCheck/CER-41-AccountStatusCheck-OnlyOne.conf b/certora/conf/CER-40-AccountStatusCheck/CER-41-AccountStatusCheck-OnlyOne.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-40-AccountStatusCheck/CER-41-AccountStatusCheck-OnlyOne.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "rule_sanity": "basic",
   "solc_via_ir": true,
diff --git a/certora/conf/CER-40-AccountStatusCheck/CER-42-AccountStatusCheck-NoController.conf b/certora/conf/CER-40-AccountStatusCheck/CER-42-AccountStatusCheck-NoController.conf
@@ -3,7 +3,7 @@
     "certora/harness/EthereumVaultConnectorHarness.sol"
   ],
   "verify": "EthereumVaultConnectorHarness:certora/specs/CER-40-AccountStatusCheck/CER-42-AccountStatusCheck-NoController.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "rule_sanity": "basic",
   "solc_via_ir": true,
diff --git a/certora/conf/CER-44-VaultStatusCheck/CER-78-VaultStatusCheck-scheduling.conf b/certora/conf/CER-44-VaultStatusCheck/CER-78-VaultStatusCheck-scheduling.conf
@@ -12,6 +12,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg" : "CER-44-VaultStatusCheck/CER-78-VaultStatusCheck-scheduling",
-    "solc": "solc8.20",
+    "solc": "solc8.24",
     "hashing_length_bound": "256"
 }
diff --git a/certora/conf/CER-83-Set.conf b/certora/conf/CER-83-Set.conf
@@ -3,9 +3,18 @@
     "certora/harness/SetHarness.sol"
   ],
   "verify": "SetHarness:certora/specs/CER-83-Set.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "loop_iter" : "6", 
   "msg": "Set properties",
   "optimistic_loop": true,
-  "rule_sanity" : "basic"
+  "rule_sanity" : "basic",
+  "coverage_info" : "advanced", 
+  "mutations": {
+        "gambit": {
+                  "filename" : "src/Set.sol",
+                  "num_mutants": 25,
+                  "functions": ["insert","remove"],
+        },
+        "msg": "Set mutations"
+    }
 }
diff --git a/certora/conf/misc/ExecutionContext.conf b/certora/conf/misc/ExecutionContext.conf
@@ -3,7 +3,7 @@
     "certora/harness/ExecutionContextHarness.sol"
   ],
   "verify": "ExecutionContextHarness:certora/specs/misc/ExecutionContext.spec",
-  "solc": "solc8.20",
+  "solc": "solc8.24",
   "solc_optimize": "10000",
   "solc_via_ir": true,
   "msg": "misc/ExecutionContext",
diff --git a/certora/conf/misc/MustRevertFunctions.conf b/certora/conf/misc/MustRevertFunctions.conf
@@ -13,6 +13,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "misc/MustRevertFunctions",
-    "solc": "solc8.20",
+    "solc": "solc8.24",
     "hashing_length_bound": "256"
 }
diff --git a/certora/harness/EthereumVaultConnectorHarness.sol b/certora/harness/EthereumVaultConnectorHarness.sol
@@ -82,4 +82,7 @@ contract EthereumVaultConnectorHarness is EthereumVaultConnector {
     function ecGetOnBehalfOfAccount(EC context) external pure returns (address result) {
         result = ExecutionContext.getOnBehalfOfAccount(context);
     }
+    function isPhantomAccountContract(bytes19 addressPrefix) external view returns (bool) {
+        return address(uint160(uint152(addressPrefix)) << 8).code.length != 0;
+    }
 }
diff --git a/certora/harness/ExecutionContextHarness.sol b/certora/harness/ExecutionContextHarness.sol
@@ -8,9 +8,7 @@ contract ExecutionContextHarness {
     uint public constant ON_BEHALF_OF_ACCOUNT_MASK = ExecutionContext.ON_BEHALF_OF_ACCOUNT_MASK;
     uint public constant OPERATOR_AUTHENTICATED_MASK = ExecutionContext.OPERATOR_AUTHENTICATED_MASK;
     uint public constant SIMULATION_MASK = ExecutionContext.SIMULATION_MASK;
-    uint public constant STAMP_MASK = ExecutionContext.STAMP_MASK;
     uint public constant STAMP_OFFSET = ExecutionContext.STAMP_OFFSET;
-    uint public constant STAMP_DUMMY_VALUE = ExecutionContext.STAMP_DUMMY_VALUE;
 
     function areChecksDeferred(EC context) external pure returns (bool result) {
         result = ExecutionContext.areChecksDeferred(context);
diff --git a/certora/harness/SetHarness.sol b/certora/harness/SetHarness.sol
@@ -20,23 +20,12 @@ contract SetHarness {
         return Set.remove(setStorage, element);
     }
 
-    function get(uint8 index) external view returns (address ) {
-        if (index==0) return address(0);
-        if (index == 1) return setStorage.firstElement;
-        return setStorage.elements[index-1].value;
-
+    function reorder(uint8 index1, uint8 index2) external  {
+        Set.reorder(setStorage, index1, index2);
     }
 
-    function contains(
-        address element
-    ) external view returns (bool found) {
-        return Set.contains(setStorage, element);
-    }
-
-
-    function length(
-    ) external view returns (uint8) {
-        return setStorage.numElements;
+    function contains(address elem) external view returns (bool) {
+        return Set.contains(setStorage, elem);
     }
 
 }
diff --git a/certora/scripts/rerun_all_confs.sh b/certora/scripts/rerun_all_confs.sh
diff --git a/certora/specs/CER-15-Permit/CER-51-Permit-msg-sender.spec b/certora/specs/CER-15-Permit/CER-51-Permit-msg-sender.spec
@@ -87,7 +87,7 @@ hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, ui
 rule onlyEVCCanCallCriticalMethod(method f, env e, calldataarg args)
   filtered {f -> 
     !isMustRevertFunction(f) &&
-    f.selector != sig:EthereumVaultConnectorHarness.permit(address,uint256,uint256,uint256,uint256,bytes,bytes).selector &&
+    f.selector != sig:EthereumVaultConnectorHarness.permit(address,address,uint256,uint256,uint256,uint256,bytes,bytes).selector &&
     f.selector != sig:EthereumVaultConnectorHarness.controlCollateral(address, address, uint256, bytes).selector
   }{
     //Exclude EVC as being the initiator of the call.
diff --git a/certora/specs/CER-2-Operator/CER-52-Operator-deauthorization.spec b/certora/specs/CER-2-Operator/CER-52-Operator-deauthorization.spec
@@ -23,6 +23,7 @@ rule operatorDeauthorization (method f) filtered { f ->
     address caller = actualCaller(e);
     address account;
     require addressPrefix == getAddressPrefix(account);
+    requireInvariant OwnerIsFromPrefix(addressPrefix);
     address owner = haveCommonOwner(account, caller) ? caller : getAccountOwner(e, account);
     uint256 operatorBefore = getOperator(addressPrefix, operator);
     f(e,args);
@@ -40,6 +41,8 @@ rule operatorDeauthorizationSetOperator {
     uint256 operatorBitField;
 
     address caller = actualCaller(e);
+    
+    requireInvariant OwnerIsFromPrefix(addressPrefix);
 
     // call the setOperator() method giving 0 as the bit field to deauthorize
     setOperator(e, addressPrefix, operator, 0);
diff --git a/certora/specs/CER-2-Operator/CER-54-Operator-owner.spec b/certora/specs/CER-2-Operator/CER-54-Operator-owner.spec
@@ -29,6 +29,8 @@ rule setOperator_owner() {
     address operator;
     uint256 operatorBitField;
 
+    requireInvariant OwnerIsFromPrefix(addressPrefix);
+
     // call the setOperator() method.
     setOperator(e, addressPrefix, operator, operatorBitField);
     // For any address "addr" with prefix "addressPrefix"
diff --git a/certora/specs/CER-2-Operator/CER-68-Operator-authorization.spec b/certora/specs/CER-2-Operator/CER-68-Operator-authorization.spec
@@ -6,6 +6,7 @@ methods {
     function getOperator(bytes19, address) external returns (uint256) envfree;
     function getAddressPrefix(address) external returns (bytes19) envfree;
     function haveCommonOwner(address account, address otherAccount) external returns (bool) envfree;
+    function isPhantomAccountContract(bytes19 addressPrefix) external returns (bool) envfree;
 }
 
 /**
@@ -27,6 +28,8 @@ rule onlyOwnerCanCallSetOperator() {
 
     address caller = actualCaller(e);
 
+    requireInvariant OwnerIsFromPrefix(addressPrefix);
+
     // call the setOperator() method.
     setOperator(e, addressPrefix, operator, operatorBitField);
 
@@ -95,6 +98,10 @@ rule theOwnerCanCallSetOperator() {
         require(getAddressPrefix(e.msg.sender) == addressPrefix);
         // the owner is not set yet (zero) or identical to msg.sender
         require(owner == 0 || owner == e.msg.sender);
+        // if the owner is not set yet, require that its phantom account is not a contract
+        if (owner == 0) {
+            require(!isPhantomAccountContract(addressPrefix));
+        }
     }
 
     // The function will revert if any of these assumptions do not hold:
diff --git a/certora/specs/CER-83-Set.spec b/certora/specs/CER-83-Set.spec

Original file line number	Diff line number	Diff line change
`@@ -13,5 +13,5 @@`
`13`	`13`	`"optimistic_hashing": true,`
`14`	`14`	`"solc_optimize" : "10000",`
`15`	`15`	`"msg": "CER-15-Permit/CER-51-Permit-msg-sender",`
`16`		`- "solc": "solc8.20"`
	`16`	`+ "solc": "solc8.24"`
`17`	`17`	`}`