final cleaning of FV specs

Certora · Sep 8, 2024 · 64a0ffd · 64a0ffd
1 parent e9e381c
commit 64a0ffd
Show file tree

Hide file tree

Showing 6 changed files with 30 additions and 30 deletions.
diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml
@@ -51,8 +51,10 @@ jobs:
       max-parallel: 16
       matrix:
         rule:
-          - verifyERC4626.conf --rule previewMintIndependentOfAllowance previewRedeemIndependentOfBalance  previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
+          - verifyERC4626.conf --rule previewRedeemIndependentOfBalance  previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance
           - verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
+          # Timeout
+          # - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
           - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
           - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
           - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint
@@ -61,17 +63,17 @@ jobs:
           - verifyERC4626Extended.conf --rule redeemATokensSum
           - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
           - verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
-          - verifyStaticATokenLM.conf --rule rewardsConsistencyWhenSufficientRewardsExist
-          - verifyStaticATokenLM.conf --rule rewardsConsistencyWhenInsufficientRewards
-          - verifyStaticATokenLM.conf --rule totalClaimableRewards_stable
-          - verifyStaticATokenLM.conf --rule solvency_positive_total_supply_only_if_positive_asset
-          - verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply
-          - verifyStaticATokenLM.conf --rule singleAssetAccruedRewards
-          - verifyStaticATokenLM.conf --rule totalAssets_stable
-          - verifyStaticATokenLM.conf --rule getClaimableRewards_stable
-          - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_deposit
-          - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
-          - verifyStaticATokenLM.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
-          - verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim
+          - verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
+          - verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
+          - verifyStataToken.conf --rule totalClaimableRewards_stable
+          - verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
+          - verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
+          - verifyStataToken.conf --rule singleAssetAccruedRewards
+          - verifyStataToken.conf --rule totalAssets_stable
+          - verifyStataToken.conf --rule getClaimableRewards_stable
+          - verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
+          - verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
+          - verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
+          - verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
           - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
           - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient
diff --git a/certora/stata/conf/verifyStaticATokenLM.conf → certora/stata/conf/verifyStataToken.conf b/certora/stata/conf/verifyStaticATokenLM.conf → certora/stata/conf/verifyStataToken.conf
@@ -29,7 +29,7 @@
      "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts",
      "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts",
   ],
-  "verify":"StataTokenV2Harness:certora/stata/specs/staticATokenLM/StaticATokenLM.spec",
+  "verify":"StataTokenV2Harness:certora/stata/specs/StataToken/StataToken.spec",
   "solc": "solc8.20",
   "msg": "Rewards related properties",
   "optimistic_loop": true,

diff --git a/certora/stata/scripts/run-all.sh b/certora/stata/scripts/run-all.sh
@@ -1,7 +1,7 @@
 #CMN="--compilation_steps_only"
 
 echo "******** Running: 1  ***************"
-certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule previewMintIndependentOfAllowance previewRedeemIndependentOfBalance  previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert  previewDepositAmountCheck maxRedeemCompliance  maxWithdrawConversionCompliance \
+certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule previewRedeemIndependentOfBalance  previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert  previewDepositAmountCheck maxRedeemCompliance  maxWithdrawConversionCompliance \
             maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert \
 --msg "1: verifyERC4626.conf"
 
@@ -34,58 +34,56 @@ echo "******** Running: 7   ***************"
 certoraRun $CMN certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf \
 --msg "7: "
 
-# https://prover.certora.com/output/44289/f0b91e1835a640c88b57e0d7bf165ea4/?anonymousKey=09f94bda02a18efeca1e94c7bedfe6b044277b56
-# fails rule sanity
 echo "******** Running: 8  ***************"
 certoraRun $CMN certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf \
 --msg "8: "
 
 echo "******** Running: 9  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsConsistencyWhenSufficientRewardsExist \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist \
 --msg "9: "
 
 echo "******** Running: 10  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsConsistencyWhenInsufficientRewards \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards \
 --msg "10: "
 
 echo "******** Running: 11  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule totalClaimableRewards_stable \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule totalClaimableRewards_stable \
 --msg "11: "
 
 echo "******** Running: 12  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule solvency_positive_total_supply_only_if_positive_asset \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset \
 --msg "12: "
 
 echo "******** Running: 13  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule solvency_total_asset_geq_total_supply \
 --msg "13: "
 
 echo "******** Running: 14  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule singleAssetAccruedRewards \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule singleAssetAccruedRewards \
 --msg "14: "
 
 echo "******** Running: 15  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule totalAssets_stable \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule totalAssets_stable \
 --msg "15: "
 
 echo "******** Running: 16  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewards_stable \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable \
 --msg "16: "
 
 echo "******** Running: 17  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_deposit \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit \
 --msg "17: "
 
 echo "******** Running: 18  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_refreshRewardTokens \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens \
 --msg "18: "
 
 echo "******** Running: 19  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf \
 --msg "19: "
 
 echo "******** Running: 20  ***************"
-certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim \
+certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim \
 --msg "20: "
 
 echo "******** Running: 21  ***************"

diff --git a/.../specs/staticATokenLM/StaticATokenLM.spec → ...ra/stata/specs/StataToken/StataToken.spec b/.../specs/staticATokenLM/StaticATokenLM.spec → ...ra/stata/specs/StataToken/StataToken.spec
diff --git a/...pecs/staticATokenLM/aTokenProperties.spec → ...ta/specs/StataToken/aTokenProperties.spec b/...pecs/staticATokenLM/aTokenProperties.spec → ...ta/specs/StataToken/aTokenProperties.spec
@@ -131,7 +131,7 @@ import "../methods/methods_base.spec";
 
         uint256 preBalance = _AToken.balanceOf(e.msg.sender);
 
-        claimSingleRewardOnBehalf(e, onBehalfOf, receiver, _DummyERC20_aTokenUnderlying);
+        claimSingleRewardOnBehalf(e, onBehalfOf, receiver, _DummyERC20_rewardToken);
 
         uint256 postBalance = _AToken.balanceOf(e.msg.sender);
         assert preBalance == postBalance, "aToken balance changed by claimSingleRewardOnBehalf";

diff --git a/...ta/specs/staticATokenLM/double_claim.spec → .../stata/specs/StataToken/double_claim.spec b/...ta/specs/staticATokenLM/double_claim.spec → .../stata/specs/StataToken/double_claim.spec