diff --git a/.github/workflows/checkrules.yml b/.github/workflows/checkrules.yml index 1410077..acc18d2 100644 --- 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 index bec3955..39da62f 100644 --- 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" } \ No newline at end of file diff --git a/certora/conf/CER-11-Controllers/CER-12-Controllers-number.conf b/certora/conf/CER-11-Controllers/CER-12-Controllers-number.conf index 97eb06e..0202a28 100644 --- 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" } \ No newline at end of file diff --git a/certora/conf/CER-15-Permit/CER-65-Permit-onBehalfOfAccount.conf b/certora/conf/CER-15-Permit/CER-65-Permit-onBehalfOfAccount.conf index 068fc6e..0d3c6ef 100644 --- 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 index f0d2b82..c162e6f 100644 --- 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" } \ No newline at end of file diff --git a/certora/conf/CER-2-Operator/CER-68-Operator-authorization.conf b/certora/conf/CER-2-Operator/CER-68-Operator-authorization.conf index 3608625..5a036a3 100644 --- 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" } \ No newline at end of file diff --git a/certora/conf/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.conf b/certora/conf/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.conf index 3fa605c..ee6e370 100644 --- 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 index 19de5ee..258d56f 100644 --- 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" } \ No newline at end of file diff --git a/certora/conf/misc/MustRevertFunctions.conf b/certora/conf/misc/MustRevertFunctions.conf index 36c5571..af53667 100644 --- 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 index 8f3c2e6..5147499 100644 --- 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 index e47b8ee..7249297 100644 --- 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; } \ No newline at end of file diff --git a/certora/specs/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.spec b/certora/specs/CER-27-ExecutionContext/CER-38-ExecutionContext-restored.spec index e4e02db..b677720 100644 --- 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); -} \ No newline at end of file +} diff --git a/certora/specs/CER-40-AccountStatusCheck/CER-41-AccountStatusCheck-OnlyOne.spec b/certora/specs/CER-40-AccountStatusCheck/CER-41-AccountStatusCheck-OnlyOne.spec index 5a82389..52155bc 100644 --- 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; } \ No newline at end of file diff --git a/certora/specs/CER-40-AccountStatusCheck/CER-42-AccountStatusCheck-NoController.spec b/certora/specs/CER-40-AccountStatusCheck/CER-42-AccountStatusCheck-NoController.spec index f0fede6..d1e6735 100644 --- 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; } \ No newline at end of file diff --git a/certora/specs/utils/IsLowLevelCallFunction.spec b/certora/specs/utils/IsLowLevelCallFunction.spec index 5499392..53443d6 100644 --- 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 index 3d5d29a..09c4a23 100644 --- 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;