diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 323c82bc..3d5dc74d 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -67,6 +67,6 @@ jobs: - verifyGhoVariableDebtToken.sh user_index_after_mint accumulated_interest_increase_after_mint user_index_ge_one_ray nonzeroNewDiscountToken - verifyGhoVariableDebtToken.sh discountCantExceed100Percent disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease userCantNullifyItsDebt integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation onlyMintForUserCanIncreaseUsersBalance integrityOfMint_cantDecreaseInterestWithMint integrityMint_atoken integrityOfBurn_updateDiscountRate integrityOfBurn_updateIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance burnAllDebtReturnsZeroDebt integrityOfUpdateDiscountRateStrategy discountCantExceedDiscountRate - verifyGhoVariableDebtToken_summarized.sh accrueAlwaysCaleldBeforeRefresh - - verifyGhoVariableDebtTokenIntenal.sh + - verifyGhoVariableDebtTokenInternal.sh - verifyGhoVariableDebtToken_specialBranch.sh sendersDiscountPercentCannotIncrease - verifyGhoVariableDebtToken-rayMulDiv-summarization.sh diff --git a/certora/scripts/verifyFlashMinter.sh b/certora/scripts/verifyFlashMinter.sh index 31f36457..8511a690 100644 --- a/certora/scripts/verifyFlashMinter.sh +++ b/certora/scripts/verifyFlashMinter.sh @@ -12,7 +12,7 @@ certoraRun certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol: --solc solc8.10 \ --optimistic_loop \ --prover_args "-contractRecursionLimit 1" \ - --rules "${@}" + --rule "${@}" --msg "flashMinter check, rules ${@}" else certoraRun certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol:GhoFlashMinter \ diff --git a/certora/scripts/verifyGhoAToken.sh b/certora/scripts/verifyGhoAToken.sh index a66741bc..1b540b4b 100644 --- a/certora/scripts/verifyGhoAToken.sh +++ b/certora/scripts/verifyGhoAToken.sh @@ -13,7 +13,7 @@ certoraRun certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol \ --link GhoVariableDebtToken:_ghoAToken=GhoAToken \ --solc solc8.10 \ --optimistic_loop \ - --rules "${@}" \ + --rule "${@}" \ --msg "GhoAToken, rules ${@}" else certoraRun certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol \ diff --git a/certora/scripts/verifyGhoDiscountRateStrategy.sh b/certora/scripts/verifyGhoDiscountRateStrategy.sh index 05605099..8877803a 100644 --- a/certora/scripts/verifyGhoDiscountRateStrategy.sh +++ b/certora/scripts/verifyGhoDiscountRateStrategy.sh @@ -1,5 +1,5 @@ -#if (($# > 0)) -#then +if (($# > 0)) +then certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness \ --verify GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec \ --solc solc8.10 \ @@ -7,15 +7,15 @@ certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStr --optimistic_loop \ --prover_args "-mediumTimeout 20 -depth 10" \ --smt_timeout 500 \ - --rules "$2" \ - --msg "GhoDiscountRateStrategy, rules $2." -# else -# certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness \ -# --verify GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec \ -# --solc solc8.10 \ -# --loop_iter 2 \ -# --optimistic_loop \ -# --prover_args "-mediumTimeout 20 -depth 10" \ -# --smt_timeout 500 \ -# --msg "GhoDiscountRateStrategy, all rules." -# fi + --rule "${@}" \ + --msg "GhoDiscountRateStrategy rules ${@}" +else +certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness \ + --verify GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec \ + --solc solc8.10 \ + --loop_iter 2 \ + --optimistic_loop \ + --prover_args "-mediumTimeout 20 -depth 10" \ + --smt_timeout 500 \ + --msg "GhoDiscountRateStrategy, all rules." +fi diff --git a/certora/scripts/verifyGhoToken.sh b/certora/scripts/verifyGhoToken.sh index 68705052..72ad9445 100644 --- a/certora/scripts/verifyGhoToken.sh +++ b/certora/scripts/verifyGhoToken.sh @@ -7,13 +7,13 @@ certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/co --solc solc8.10 \ --loop_iter 3 \ --optimistic_loop \ - --rules "${@}" \ - --msg "GhoToken workaround for CERT-1060, rules ${@}" + --rule "${@}" \ + --msg "GhoToken rules ${@}" else certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/contracts/gho/GhoToken.sol \ --verify GhoTokenHarness:certora/specs/ghoToken.spec \ --solc solc8.10 \ --loop_iter 3 \ --optimistic_loop \ - --msg "GhoToken, all rules. workaround for CERT-1060" + --msg "GhoToken, all rules." fi \ No newline at end of file diff --git a/certora/scripts/verifyGhoVariableDebtToken-rayMulDiv-summarization.sh b/certora/scripts/verifyGhoVariableDebtToken-rayMulDiv-summarization.sh index f7c77d2a..ffd7b4b9 100644 --- a/certora/scripts/verifyGhoVariableDebtToken-rayMulDiv-summarization.sh +++ b/certora/scripts/verifyGhoVariableDebtToken-rayMulDiv-summarization.sh @@ -19,7 +19,6 @@ certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenH --solc solc8.10 \ --optimistic_loop \ --smt_timeout 900 \ - --fe_version latest \ --prover_args "-mediumTimeout 30 -depth 15" \ $RULE \ --msg "$1 $2"