Merge pull request #137 from euler-xyz/Certora_CI_fix_8Apr

Certora ci fix 8 apr
Tvenus · May 20, 2024 · 72754d6 · 72754d6
2 parents 38fb9aa + 3f9bf86
commit 72754d6
Show file tree

Hide file tree

Showing 16 changed files with 27 additions and 23 deletions.
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.0.7
+          pip install certora-cli==7.6.3
           echo "`pwd`/.github/executables" >> $GITHUB_PATH
 
       - name: run certora prover on conf files

diff --git a/certora/conf/CER-1-Owner/CER-59-Owner-override.conf b/certora/conf/CER-1-Owner/CER-59-Owner-override.conf
@@ -17,5 +17,6 @@
     "solc_optimize" :  "10000",
     "msg": "CER-1-Owner/CER-59-Owner-addressPrefix",
     "solc": "solc8.20",
-    "rule_sanity": "basic"
+    "rule_sanity": "basic",
+    "hashing_length_bound": "256"
 }
diff --git a/certora/conf/CER-11-Controllers/CER-12-Controllers-number.conf b/certora/conf/CER-11-Controllers/CER-12-Controllers-number.conf
@@ -9,5 +9,6 @@
   "msg": "CER-11-Controllers/CER-12-Controllers-number",
   "optimistic_loop": true,
   "optimistic_hashing": true,
-  "rule_sanity": "basic"
+  "rule_sanity": "basic",
+  "hashing_length_bound": "256"
 }
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,5 +13,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-15-Permit/CER-65-Permit-onBehalfOfAccount",
-    "solc": "solc8.20"
+    "solc": "solc8.20",
+    "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
@@ -10,5 +10,6 @@
   "msg": "CER-2-Operator/CER-52-Operator-deauthorization",
   "optimistic_loop": true,
   "optimistic_hashing": true,
-  "prover_args": ["-smt_bitVectorTheory", "true"]
+  "prover_args": ["-smt_bitVectorTheory", "true"],
+  "hashing_length_bound": "256"
 }
diff --git a/certora/conf/CER-2-Operator/CER-68-Operator-authorization.conf b/certora/conf/CER-2-Operator/CER-68-Operator-authorization.conf
@@ -10,5 +10,6 @@
   "msg": "CER-2-Operator/CER-68-Operator-authorization",
   "optimistic_loop": true,
   "optimistic_hashing": true,
-  "prover_args": ["-smt_bitVectorTheory", "true"]
+  "prover_args": ["-smt_bitVectorTheory", "true"],
+  "hashing_length_bound": "256"
 }
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,5 +10,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "CER-27-ExecutionContext/CER-38-ExecutionContext-restored",
-    "solc": "solc8.20"
+    "solc": "solc8.20",
+    "hashing_length_bound": "256"
 }
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,5 +12,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg" : "CER-44-VaultStatusCheck/CER-78-VaultStatusCheck-scheduling",
-    "solc": "solc8.20"
+    "solc": "solc8.20",
+    "hashing_length_bound": "256"
 }
diff --git a/certora/conf/misc/MustRevertFunctions.conf b/certora/conf/misc/MustRevertFunctions.conf
@@ -13,5 +13,6 @@
     "optimistic_hashing": true,
     "solc_optimize" :  "10000",
     "msg": "misc/MustRevertFunctions",
-    "solc": "solc8.20"
+    "solc": "solc8.20",
+    "hashing_length_bound": "256"
 }
diff --git a/certora/harness/EthereumVaultConnectorHarness.sol b/certora/harness/EthereumVaultConnectorHarness.sol
@@ -11,7 +11,7 @@ contract EthereumVaultConnectorHarness is EthereumVaultConnector {
     using Set for SetStorage;
 
     function getExecutionContextDefault() external view returns (uint256) {
-        return ExecutionContext.STAMP_DUMMY_VALUE << ExecutionContext.STAMP_OFFSET;
+        return 1 << ExecutionContext.STAMP_OFFSET;
     }
 
     function getExecutionContextAreChecksDeferred() external view returns (bool) {

diff --git a/certora/specs/CER-11-Controllers/CER-12-Controllers-number.spec b/certora/specs/CER-11-Controllers/CER-12-Controllers-number.spec
@@ -72,6 +72,6 @@ rule enableControllerEnequeusStatusCheckWhenDeferred {
 rule checkAccountStatusForcesNumControllersLEOne {
     env e;
     address account;
-    checkAccountStatus(e, account);
-    assert numOfController(account) <= 1;
+    bool status = checkAccountStatus(e, account);
+    assert numOfController(account) > 1 => !status;
 }
diff --git a/certora/specs/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.spec b/certora/specs/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.spec
@@ -42,6 +42,7 @@ invariant topLevelFunctionDontChangeTransientStorage()
     getRawExecutionContext() == getExecutionContextDefault()
     filtered { f ->
         !isMustRevertFunction(f) &&
+        !f.isFallback &&            // certora plans to deprecate certora tool-generated function from sanity checks
         f.selector != sig:getCurrentOnBehalfOfAccount(address).selector
     }
 
@@ -55,4 +56,4 @@ rule getCurrentOnBehalfOfAccountAlwaysReverts() {
     address controllerToCheck;
     getCurrentOnBehalfOfAccount@withrevert(controllerToCheck);
     assert(lastReverted);
-}
+}
diff --git a/certora/specs/CER-40-AccountStatusCheck/CER-41-AccountStatusCheck-OnlyOne.spec b/certora/specs/CER-40-AccountStatusCheck/CER-41-AccountStatusCheck-OnlyOne.spec
@@ -1,6 +1,5 @@
 methods {
     function numOfController(address account) external returns (uint8) envfree;
-    function checkAccountStatus(address account) external returns (bool) envfree;
 }
 
 // CER-41: Account Status Check more than one controller.
@@ -10,8 +9,6 @@ rule account_status_only_one_controller {
     env e;
     address account;
     require numOfController(account) > 1;
-    bool isValid = checkAccountStatus@withrevert(account);
-    // Note: writing the rule as follows is actually a counterexample. checkAccountStatus reverts rather than returning false in this case.
-    // assert !isValid;
-    assert lastReverted;
+    bool isValid = checkAccountStatus(e, account);
+    assert !isValid;
 }
diff --git a/certora/specs/CER-40-AccountStatusCheck/CER-42-AccountStatusCheck-NoController.spec b/certora/specs/CER-40-AccountStatusCheck/CER-42-AccountStatusCheck-NoController.spec
@@ -1,6 +1,5 @@
 methods {
     function numOfController(address account) external returns (uint8) envfree;
-    function checkAccountStatus(address account) external returns (bool) envfree;
 }
 
 // CER-42: Account Status Check no controller
@@ -11,6 +10,6 @@ rule account_status_no_controller {
     env e;
     address account;
     require numOfController(account) == 0;
-    bool isValid = checkAccountStatus(account);
+    bool isValid = checkAccountStatus(e, account);
     assert isValid;
 }
diff --git a/certora/specs/utils/IsLowLevelCallFunction.spec b/certora/specs/utils/IsLowLevelCallFunction.spec
@@ -3,8 +3,8 @@
  * that do not always revert (e.g. batchRevert is omitted)
  */
 definition isLowLevelCallFunction(method f) returns bool =
-    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.call(
         address,address,uint256,bytes).selector ||
     f.selector == sig:EthereumVaultConnectorHarness.batch(

diff --git a/certora/specs/utils/IsMustRevertFunction.spec b/certora/specs/utils/IsMustRevertFunction.spec
@@ -5,5 +5,4 @@
  * generic rules or invariants if automatic sanity checks are enabled.
  */
 definition isMustRevertFunction(method f) returns bool =
-    f.selector == sig:EthereumVaultConnectorHarness.batchSimulation(IEVC.BatchItem[]).selector ||
     f.selector == sig:EthereumVaultConnectorHarness.batchRevert(IEVC.BatchItem[]).selector;