small fixes for ci

Certora · Nov 22, 2023 · 9b2ebc3 · 9b2ebc3
1 parent 5542ac2
commit 9b2ebc3
Show file tree

Hide file tree

Showing 6 changed files with 20 additions and 21 deletions.
diff --git 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
@@ -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
@@ -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
@@ -1,21 +1,21 @@
-#if (($# > 0))
-#then
+if (($# > 0))
+then
 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 \
-    --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
@@ -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
diff --git 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"