diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml new file mode 100644 index 00000000..199d29e1 --- /dev/null +++ b/.github/workflows/certora-stata.yml @@ -0,0 +1,89 @@ +name: certora-stata + +on: + push: + branches: + - main certora + pull_request: + branches: + - main certora + + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v2 + with: + submodules: recursive + + - name: Install python + uses: actions/setup-python@v2 + with: { python-version: 3.9 } + + - name: Install java + uses: actions/setup-java@v1 + with: { java-version: "11", java-package: jre } + + - name: Install certora cli + run: pip install certora-cli==7.10.2 + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc8.20 + + - name: Verify rule ${{ matrix.rule }} + run: | + cd certora + touch applyHarness.patch + make munged + cd .. + certoraRun certora/conf/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - verifyERC4626.conf --rule previewMintIndependentOfAllowance previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawIndependentOfMaxWithdraw previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance + - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay + #The following seem to be incorrect: + # verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert + # # Timeout + # - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 + - verifyERC4626DepositSummarization.conf --rule depositCheckIndexERayAssert1 + - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint + #The following seem to be incorrect: + # verifyERC4626Extended.conf --rule maxDepositConstant + - verifyERC4626Extended.conf --rule redeemSum + - 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 rewardsTotalDeclinesOnlyByClaim + - verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim_timedout_methods + - verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim_redeem_methods + - verifyStaticATokenLM.conf --rule solvency_positive_total_supply_only_if_positive_asset + - verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply + - verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply_CASE_SPLIT_redeem + - verifyStaticATokenLM.conf --rule singleAssetAccruedRewards + - verifyStaticATokenLM.conf --rule totalAssets_stable + - verifyStaticATokenLM.conf --rule totalAssets_stable_after_collectAndUpdateRewards + - verifyStaticATokenLM.conf --rule reward_balance_stable_after_collectAndUpdateRewards + - verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT + # - verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT_redeem + # # Timeout + - verifyStaticATokenLM.conf --rule getClaimableRewards_stable + - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_deposit + - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_redeem + - verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT_deposit + - verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_refreshRewardTokens + - verifyStaticATokenLM.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf + - 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/Makefile b/certora/stata/Makefile new file mode 100644 index 00000000..f71caf35 --- /dev/null +++ b/certora/stata/Makefile @@ -0,0 +1,32 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../src +LIBS_DIR = ../lib +MUNGED_SRC = munged/src +MUNGED_LIB = munged/lib + +help: + @echo "usage:" + @echo " make clean: remove all generated files (those ignored by git)" + @echo " make $(MUNGED_DIR): create $(MUNGED_DIR) directory by applying the patch file to $(CONTRACTS_DIR)" + @echo " make record: record a new patch file capturing the differences between $(CONTRACTS_DIR) and $(MUNGED_DIR)" + +munged: $(wildcard $(CONTRACTS_DIR)/*.sol) $(PATCH) + rm -rf $@ + mkdir $@ + cp -r ../lib $@ + cp -r ../src $@ + patch -p0 -d $@ < $(PATCH) + +record: + mkdir tmp + cp -r ../lib tmp + cp -r ../src tmp + diff -ruN tmp $(MUNGED_DIR) | sed 's+tmp/++g' | sed 's+$(MUNGED_DIR)/++g' > $(PATCH) + rm -rf tmp + +clean: + git clean -fdX + touch $(PATCH) + diff --git a/certora/stata/applyHarness.patch b/certora/stata/applyHarness.patch new file mode 100644 index 00000000..6357986f --- /dev/null +++ b/certora/stata/applyHarness.patch @@ -0,0 +1,7 @@ +diff -ruN .gitignore .gitignore +--- .gitignore 1970-01-01 02:00:00 ++++ .gitignore 2023-04-01 01:24:40 +@@ -0,0 +1,2 @@ ++* ++!.gitignore +\ No newline at end of file \ No newline at end of file diff --git a/certora/stata/conf/verifyAToken.conf b/certora/stata/conf/verifyAToken.conf new file mode 100644 index 00000000..531f2ac9 --- /dev/null +++ b/certora/stata/conf/verifyAToken.conf @@ -0,0 +1,39 @@ +{ + "files": [ + "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/pool/SymbolicLendingPool.sol", + "certora/stata/harness/rewards/RewardsControllerHarness.sol", + "certora/stata/harness/rewards/TransferStrategyHarness.sol", + "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", + "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", + "src/core/instances/ATokenInstance.sol", + ], + "link": [ + "SymbolicLendingPool:aToken=ATokenInstance", + "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", + "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "TransferStrategyHarness:REWARD=DummyERC20_rewardToken", + "ATokenInstance:POOL=SymbolicLendingPool", + "ATokenInstance:_incentivesController=RewardsControllerHarness", + "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StaticATokenLMHarness:POOL=SymbolicLendingPool", + "StaticATokenLMHarness:_aToken=ATokenInstance", + "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + ], + "loop_iter": "1", + "msg": "aToken properties", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "aave-v3-core/=src/core", + "aave-v3-periphery/=src/periphery", + "solidity-utils/=lib/solidity-utils/src", + "forge-std/=lib/forge-std/src", + ], + "solc": "solc8.20", + "smt_timeout": "1400", + "verify": "StaticATokenLMHarness:certora/stata/specs/staticATokenLM/aTokenProperties.spec", + "build_cache": true, +} \ No newline at end of file diff --git a/certora/stata/conf/verifyDoubleClaim.conf b/certora/stata/conf/verifyDoubleClaim.conf new file mode 100644 index 00000000..807e7dcb --- /dev/null +++ b/certora/stata/conf/verifyDoubleClaim.conf @@ -0,0 +1,39 @@ +{ + "files": [ + "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/pool/SymbolicLendingPool.sol", + "certora/stata/harness/rewards/RewardsControllerHarness.sol", + "certora/stata/harness/rewards/TransferStrategyHarness.sol", + "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", + "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", + "src/core/instances/ATokenInstance.sol", + ], + "link": [ + "SymbolicLendingPool:aToken=ATokenInstance", + "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", + "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "TransferStrategyHarness:REWARD=DummyERC20_rewardToken", + "ATokenInstance:POOL=SymbolicLendingPool", + "ATokenInstance:_incentivesController=RewardsControllerHarness", + "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StaticATokenLMHarness:POOL=SymbolicLendingPool", + "StaticATokenLMHarness:_aToken=ATokenInstance", + "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=src/core", + "aave-v3-periphery/=src/periphery", + "solidity-utils/=lib/solidity-utils/src", + "forge-std/=lib/forge-std/src", + ], + "verify":"StaticATokenLMHarness:certora/stata/specs/staticATokenLM/double_claim.spec", + "solc": "solc8.20", + "msg": "Multi rewards - double claim properties", + "optimistic_loop": true, + "smt_timeout": "2000", + "loop_iter": "2", + "optimistic_hashing": true, + "build_cache": true, +} \ No newline at end of file diff --git a/certora/stata/conf/verifyERC4626.conf b/certora/stata/conf/verifyERC4626.conf new file mode 100644 index 00000000..1583b01a --- /dev/null +++ b/certora/stata/conf/verifyERC4626.conf @@ -0,0 +1,39 @@ +{ + "files": [ + "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/pool/SymbolicLendingPool.sol", + "certora/stata/harness/rewards/RewardsControllerHarness.sol", + "certora/stata/harness/rewards/TransferStrategyHarness.sol", + "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", + "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", + "src/core/instances/ATokenInstance.sol", + ], + "link": [ + "SymbolicLendingPool:aToken=ATokenInstance", + "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", + "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "TransferStrategyHarness:REWARD=DummyERC20_rewardToken", + "ATokenInstance:POOL=SymbolicLendingPool", + "ATokenInstance:_incentivesController=RewardsControllerHarness", + "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StaticATokenLMHarness:POOL=SymbolicLendingPool", + "StaticATokenLMHarness:_aToken=ATokenInstance", + "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=src/core", + "aave-v3-periphery/=src/periphery", + "solidity-utils/=lib/solidity-utils/src", + "forge-std/=lib/forge-std/src", + ], + "verify":"StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626.spec", + "solc": "solc8.20", + "msg": "ERC4626 properties", + "optimistic_loop": true, + "smt_timeout": "1000", + "loop_iter": "1", + "optimistic_hashing": true, + "build_cache": true, +} \ No newline at end of file diff --git a/certora/stata/conf/verifyERC4626DepositSummarization.conf b/certora/stata/conf/verifyERC4626DepositSummarization.conf new file mode 100644 index 00000000..c0b6d885 --- /dev/null +++ b/certora/stata/conf/verifyERC4626DepositSummarization.conf @@ -0,0 +1,39 @@ +{ + "files": [ + "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/pool/SymbolicLendingPool.sol", + "certora/stata/harness/rewards/RewardsControllerHarness.sol", + "certora/stata/harness/rewards/TransferStrategyHarness.sol", + "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", + "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", + "src/core/instances/ATokenInstance.sol", + ], + "link": [ + "SymbolicLendingPool:aToken=ATokenInstance", + "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", + "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "TransferStrategyHarness:REWARD=DummyERC20_rewardToken", + "ATokenInstance:POOL=SymbolicLendingPool", + "ATokenInstance:_incentivesController=RewardsControllerHarness", + "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StaticATokenLMHarness:POOL=SymbolicLendingPool", + "StaticATokenLMHarness:_aToken=ATokenInstance", + "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=src/core", + "aave-v3-periphery/=src/periphery", + "solidity-utils/=lib/solidity-utils/src", + "forge-std/=lib/forge-std/src", + ], + "verify": "StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626DepositSummarization.spec", + "solc": "solc8.20", + "msg": "ERC4626 summarized properties depositCheckIndexGRayAssert1", + "optimistic_loop": true, + "loop_iter": "1", + "optimistic_hashing": true, + "build_cache": true, +// "rule":["depositCheckIndexGRayAssert1"], +} \ No newline at end of file diff --git a/certora/stata/conf/verifyERC4626Extended.conf b/certora/stata/conf/verifyERC4626Extended.conf new file mode 100644 index 00000000..52766658 --- /dev/null +++ b/certora/stata/conf/verifyERC4626Extended.conf @@ -0,0 +1,39 @@ +{ + "files": [ + "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/pool/SymbolicLendingPool.sol", + "certora/stata/harness/rewards/RewardsControllerHarness.sol", + "certora/stata/harness/rewards/TransferStrategyHarness.sol", + "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", + "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", + "src/core/instances/ATokenInstance.sol", + ], + "link": [ + "SymbolicLendingPool:aToken=ATokenInstance", + "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", + "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "TransferStrategyHarness:REWARD=DummyERC20_rewardToken", + "ATokenInstance:POOL=SymbolicLendingPool", + "ATokenInstance:_incentivesController=RewardsControllerHarness", + "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StaticATokenLMHarness:POOL=SymbolicLendingPool", + "StaticATokenLMHarness:_aToken=ATokenInstance", + "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=src/core", + "aave-v3-periphery/=src/periphery", + "solidity-utils/=lib/solidity-utils/src", + "forge-std/=lib/forge-std/src", + ], + "verify":"StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626Extended.spec", + "solc": "solc8.20", + "msg": "ERC4626 Extended properties", + "optimistic_loop": true, + "smt_timeout": "1000", + "loop_iter": "1", + "optimistic_hashing": true, + "build_cache": true, +} \ No newline at end of file diff --git a/certora/stata/conf/verifyERC4626MintDepositSummarization.conf b/certora/stata/conf/verifyERC4626MintDepositSummarization.conf new file mode 100644 index 00000000..9b1ce314 --- /dev/null +++ b/certora/stata/conf/verifyERC4626MintDepositSummarization.conf @@ -0,0 +1,40 @@ +{ + "files": [ + "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/pool/SymbolicLendingPool.sol", + "certora/stata/harness/rewards/RewardsControllerHarness.sol", + "certora/stata/harness/rewards/TransferStrategyHarness.sol", + "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", + "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", + "src/core/instances/ATokenInstance.sol", + ], + "link": [ + "SymbolicLendingPool:aToken=ATokenInstance", + "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", + "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "TransferStrategyHarness:REWARD=DummyERC20_rewardToken", + "ATokenInstance:POOL=SymbolicLendingPool", + "ATokenInstance:_incentivesController=RewardsControllerHarness", + "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StaticATokenLMHarness:POOL=SymbolicLendingPool", + "StaticATokenLMHarness:_aToken=ATokenInstance", + "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=src/core", + "aave-v3-periphery/=src/periphery", + "solidity-utils/=lib/solidity-utils/src", + "forge-std/=lib/forge-std/src", + ], + "verify": + "StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626MintDepositSummarization.spec", + "solc": "solc8.20", + "msg": "ERC4626 Summarized no transferFrom properties", + "optimistic_loop": true, + "smt_timeout": "5000", + "loop_iter": "1", + "optimistic_hashing": true, + "build_cache": true, +} \ No newline at end of file diff --git a/certora/stata/conf/verifyStaticATokenLM.conf b/certora/stata/conf/verifyStaticATokenLM.conf new file mode 100644 index 00000000..5d6fc72d --- /dev/null +++ b/certora/stata/conf/verifyStaticATokenLM.conf @@ -0,0 +1,39 @@ +{ + "files": [ + "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/pool/SymbolicLendingPool.sol", + "certora/stata/harness/rewards/RewardsControllerHarness.sol", + "certora/stata/harness/rewards/TransferStrategyHarness.sol", + "certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol", + "certora/stata/harness/tokens/DummyERC20_rewardToken.sol", + "src/core/instances/ATokenInstance.sol", + ], + "link": [ + "SymbolicLendingPool:aToken=ATokenInstance", + "SymbolicLendingPool:underlyingToken=DummyERC20_aTokenUnderlying", + "TransferStrategyHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "TransferStrategyHarness:REWARD=DummyERC20_rewardToken", + "ATokenInstance:POOL=SymbolicLendingPool", + "ATokenInstance:_incentivesController=RewardsControllerHarness", + "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StaticATokenLMHarness:POOL=SymbolicLendingPool", + "StaticATokenLMHarness:_aToken=ATokenInstance", + "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", + "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=src/core", + "aave-v3-periphery/=src/periphery", + "solidity-utils/=lib/solidity-utils/src", + "forge-std/=lib/forge-std/src", + ], + "verify":"StaticATokenLMHarness:certora/stata/specs/staticATokenLM/StaticATokenLM.spec", + "solc": "solc8.20", + "msg": "Rewards related properties", + "optimistic_loop": true, + "smt_timeout": "1400", + "loop_iter": "1", + "optimistic_hashing": true, + "build_cache": true, +} \ No newline at end of file diff --git a/certora/stata/harness/StaticATokenLMHarness.sol b/certora/stata/harness/StaticATokenLMHarness.sol new file mode 100644 index 00000000..ecd932be --- /dev/null +++ b/certora/stata/harness/StaticATokenLMHarness.sol @@ -0,0 +1,98 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.10; + +import {StaticATokenLM, StaticATokenErrors, IPool, IRewardsController, IERC20} from 'aave-v3-periphery/contracts/static-a-token/StaticATokenLM.sol'; +import {SymbolicLendingPool} from './pool/SymbolicLendingPool.sol'; + + + +contract StaticATokenLMHarness is StaticATokenLM{ + + address internal _reward_A; + address internal _reward_B; + + constructor( + IPool pool, + IRewardsController rewardsController + ) StaticATokenLM(pool, rewardsController){} + + // returns the address of the underlying asset of the static aToken + function getStaticATokenUnderlying() public view returns (address){ + return _aTokenUnderlying; + } + + // returns the address of the i-th reward token in the reward tokens list maintained by the static aToken + function getRewardToken(uint256 i) external view returns (address) { + return _rewardTokens[i]; + } + + // returns the length of the reward tokens list maintained by the static aToken + function getRewardTokensLength() external view returns (uint256) { + return _rewardTokens.length; + } + + // returns a user's reward index on last interaction for a given reward + function getRewardsIndexOnLastInteraction(address user, address reward) + external view returns (uint128) { + UserRewardsData memory currentUserRewardsData = _userRewardsData[user][reward]; + return currentUserRewardsData.rewardsIndexOnLastInteraction; + } + + // claims rewards for a user on the static aToken. + // the method builds the rewards array with a single reward and calls the internal claim function with it + function claimSingleRewardOnBehalf( + address onBehalfOf, + address receiver, + address reward + ) external + { + require (reward == _reward_A); + address[] memory rewards = new address[](1); + rewards[0] = _reward_A; + + // @MM - think of the best way to get rid of this require + require( + msg.sender == onBehalfOf || + msg.sender == INCENTIVES_CONTROLLER.getClaimer(onBehalfOf), + StaticATokenErrors.INVALID_CLAIMER + ); + _claimRewardsOnBehalf(onBehalfOf, receiver, rewards); + } + + // claims rewards for a user on the static aToken. + // the method builds the rewards array with 2 identical rewards and calls the internal claim function with it + function claimDoubleRewardOnBehalfSame( + address onBehalfOf, + address receiver, + address reward + ) external + { + require (reward == _reward_A); + address[] memory rewards = new address[](2); + rewards[0] = _reward_A; + rewards[1] = _reward_A; + + require( + msg.sender == onBehalfOf || + msg.sender == INCENTIVES_CONTROLLER.getClaimer(onBehalfOf), + StaticATokenErrors.INVALID_CLAIMER + ); + _claimRewardsOnBehalf(onBehalfOf, receiver, rewards); + + } + + // wrapper function for the erc20 _mint function. Used to reduce running times + function _mintWrapper(address to, uint256 amount) external { + _mint(to, amount); + } + + function getUserRewardsData(address user, address reward) + external view + returns (uint128) { + UserRewardsData memory currentUserRewardsData = _userRewardsData[user][ + reward + ]; + return currentUserRewardsData.rewardsIndexOnLastInteraction; + } + +} diff --git a/certora/stata/harness/pool/SymbolicLendingPool.sol b/certora/stata/harness/pool/SymbolicLendingPool.sol new file mode 100644 index 00000000..fda7f324 --- /dev/null +++ b/certora/stata/harness/pool/SymbolicLendingPool.sol @@ -0,0 +1,85 @@ +pragma solidity ^0.8.10; +pragma experimental ABIEncoderV2; + +import {IERC20} from 'aave-v3-core/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {IAToken} from "aave-v3-core/contracts/interfaces/IAToken.sol"; +import {DataTypes} from 'aave-v3-core/contracts/protocol/libraries/types/DataTypes.sol'; + +contract SymbolicLendingPool { + // an underlying asset in the pool + IERC20 public underlyingToken; + // the aToken associated with the underlying above + IAToken public aToken; + // This index is used to convert the underlying token to its matching + // AToken inside the pool, and vice versa. + uint256 public liquidityIndex; + + /** + * @dev Deposits underlying token in the Atoken's contract on behalf of the user, + and mints Atoken on behalf of the user in return. + * @param asset The underlying sent by the user and to which Atoken shall be minted + * @param amount The amount of underlying token sent by the user + * @param onBehalfOf The recipient of the minted Atokens + * @param referralCode A unique code (unused) + **/ + function deposit( + address asset, + uint256 amount, + address onBehalfOf, + uint16 referralCode + ) external { + require(asset == address(underlyingToken)); + underlyingToken.transferFrom( + msg.sender, + address(aToken), + amount + ); + aToken.mint( + msg.sender, + onBehalfOf, + amount, + liquidityIndex + ); + } + + /** + * @dev Burns Atokens in exchange for underlying asset + * @param asset The underlying asset to which the Atoken is connected + * @param amount The amount of underlying tokens to be burned + * @param to The recipient of the burned Atokens + * @return The `amount` of tokens withdrawn + **/ + function withdraw( + address asset, + uint256 amount, + address to + ) external returns (uint256) { + require(asset == address(underlyingToken)); + aToken.burn( + msg.sender, + to, + amount, + liquidityIndex + ); + return amount; + } + + /** + * @dev A simplification returning a constant + * @param asset The underlying asset to which the Atoken is connected + * @return liquidityIndex the `liquidityIndex` of the asset + **/ + function getReserveNormalizedIncome(address asset) + external + view + virtual + returns (uint256) + { + return liquidityIndex; + } + + DataTypes.ReserveData reserve; + function getReserveData(address asset) external view returns (DataTypes.ReserveData memory) { + return reserve; + } +} diff --git a/certora/stata/harness/rewards/RewardsControllerHarness.sol b/certora/stata/harness/rewards/RewardsControllerHarness.sol new file mode 100644 index 00000000..0cd97b2d --- /dev/null +++ b/certora/stata/harness/rewards/RewardsControllerHarness.sol @@ -0,0 +1,48 @@ + +pragma solidity ^0.8.10; + +import {RewardsController, RewardsDataTypes} from 'aave-v3-periphery/contracts/rewards/RewardsController.sol'; + +contract RewardsControllerHarness is RewardsController{ + + constructor(address emissionManager) RewardsController(emissionManager) {} + + // returns the available rewardscount of a given asset in the rewards controller + function getAvailableRewardsCount(address asset) + external + view + returns (uint128) + { + return _assets[asset].availableRewardsCount; + } + + // returns the i-th available reward of a given asset in the rewards controller + /// @dev assume i < availableRewardsCount + function getRewardsByAsset(address asset, uint128 i) external view returns (address) { + return _assets[asset].availableRewards[i]; + } + + // returns the i-th asset in the reward controller + function getAssetByIndex(uint256 i) external view returns (address) { + return _assetsList[i]; + } + + // returns the length of the asset list in the reward controller + function getAssetListLength() external view returns (uint256) { + return _assetsList.length; + } + + // returns the a user's accrued rewards for a given reward baring asset and a specified reward + function getUserAccruedReward( + address user, + address asset, + address reward + ) external view returns (uint256) { + return _assets[asset].rewards[reward].usersData[user].accrued; + } + + // returns the a user's reward index for a given reward baring asset and a specified reward + function getRewardsIndex(address asset, address reward) external view returns (uint256){ + return _assets[asset].rewards[reward].index; + } +} diff --git a/certora/stata/harness/rewards/TransferStrategyHarness.sol b/certora/stata/harness/rewards/TransferStrategyHarness.sol new file mode 100644 index 00000000..2007e418 --- /dev/null +++ b/certora/stata/harness/rewards/TransferStrategyHarness.sol @@ -0,0 +1,22 @@ + +pragma solidity ^0.8.10; + +import {IERC20} from 'aave-v3-core/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {TransferStrategyBase} from 'aave-v3-periphery/contracts/rewards/transfer-strategies/TransferStrategyBase.sol'; + +contract TransferStrategyHarness is TransferStrategyBase{ + +constructor(address incentivesController, address rewardsAdmin) TransferStrategyBase(incentivesController, rewardsAdmin) {} + + IERC20 public REWARD; + + // executes the actual transfer of the reward to the receiver + function performTransfer( + address to, + address reward, + uint256 amount + ) external override(TransferStrategyBase) returns (bool){ + require(reward == address(REWARD)); + return REWARD.transfer(to, amount); + } +} diff --git a/certora/stata/harness/rewards/TransferStrategyMultiRewardHarness.sol b/certora/stata/harness/rewards/TransferStrategyMultiRewardHarness.sol new file mode 100644 index 00000000..251d618d --- /dev/null +++ b/certora/stata/harness/rewards/TransferStrategyMultiRewardHarness.sol @@ -0,0 +1,31 @@ + +pragma solidity ^0.8.10; + +import {IERC20} from '../../munged/lib/aave-v3-core/contracts/dependencies/openzeppelin/contracts/IERC20.sol'; +import {TransferStrategyBase} from '../../munged/lib/aave-v3-periphery/contracts/rewards/transfer-strategies/TransferStrategyBase.sol'; + +contract TransferStrategyMultiRewardHarness is TransferStrategyBase{ + +constructor(address incentivesController, address rewardsAdmin) TransferStrategyBase(incentivesController, rewardsAdmin) {} + + IERC20 public REWARD; + IERC20 public REWARD_B; + + // executes the actual transfer of the rewards to the receiver + function performTransfer( + address to, + address reward, + uint256 amount + ) external override(TransferStrategyBase) returns (bool){ + + require(reward == address(REWARD) || reward == address(REWARD_B)); + + if (reward == address(REWARD)){ + return REWARD.transfer(to, amount); + } + else if (reward == address(REWARD_B)){ + return REWARD_B.transfer(to, amount); + } + return false; + } +} \ No newline at end of file diff --git a/certora/stata/harness/tokens/DummyERC20Impl.sol b/certora/stata/harness/tokens/DummyERC20Impl.sol new file mode 100644 index 00000000..a4822551 --- /dev/null +++ b/certora/stata/harness/tokens/DummyERC20Impl.sol @@ -0,0 +1,57 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.10; + +// with mint +contract DummyERC20Impl { + uint256 t; + mapping (address => uint256) b; + mapping (address => mapping (address => uint256)) a; + + string public name; + string public symbol; + uint public decimals; + + function myAddress() public returns (address) { + return address(this); + } + + function add(uint a, uint b) internal pure returns (uint256) { + uint c = a +b; + require (c >= a); + return c; + } + function sub(uint a, uint b) internal pure returns (uint256) { + require (a>=b); + return a-b; + } + + function totalSupply() external view returns (uint256) { + return t; + } + function balanceOf(address account) external view returns (uint256) { + return b[account]; + } + function transfer(address recipient, uint256 amount) external returns (bool) { + b[msg.sender] = sub(b[msg.sender], amount); + b[recipient] = add(b[recipient], amount); + return true; + } + function allowance(address owner, address spender) external view returns (uint256) { + return a[owner][spender]; + } + function approve(address spender, uint256 amount) external returns (bool) { + a[msg.sender][spender] = amount; + return true; + } + + function transferFrom( + address sender, + address recipient, + uint256 amount + ) external returns (bool) { + b[sender] = sub(b[sender], amount); + b[recipient] = add(b[recipient], amount); + a[sender][msg.sender] = sub(a[sender][msg.sender], amount); + return true; + } +} \ No newline at end of file diff --git a/certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol b/certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol new file mode 100644 index 00000000..06460386 --- /dev/null +++ b/certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.10; +import "./DummyERC20Impl.sol"; + +contract DummyERC20_aTokenUnderlying is DummyERC20Impl {} \ No newline at end of file diff --git a/certora/stata/harness/tokens/DummyERC20_rewardToken.sol b/certora/stata/harness/tokens/DummyERC20_rewardToken.sol new file mode 100644 index 00000000..8b8f7e8a --- /dev/null +++ b/certora/stata/harness/tokens/DummyERC20_rewardToken.sol @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; +import "./DummyERC20Impl.sol"; + +contract DummyERC20_rewardToken is DummyERC20Impl {} diff --git a/certora/stata/harness/tokens/DummyERC20_rewardTokenB.sol b/certora/stata/harness/tokens/DummyERC20_rewardTokenB.sol new file mode 100644 index 00000000..e5072788 --- /dev/null +++ b/certora/stata/harness/tokens/DummyERC20_rewardTokenB.sol @@ -0,0 +1,5 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.10; +import "./DummyERC20Impl.sol"; + +contract DummyERC20_rewardTokenB is DummyERC20Impl {} diff --git a/certora/stata/munged/.gitignore b/certora/stata/munged/.gitignore new file mode 100644 index 00000000..c96a04f0 --- /dev/null +++ b/certora/stata/munged/.gitignore @@ -0,0 +1,2 @@ +* +!.gitignore \ No newline at end of file diff --git a/certora/stata/scripts/run-all.sh b/certora/stata/scripts/run-all.sh new file mode 100644 index 00000000..cf5e50e9 --- /dev/null +++ b/certora/stata/scripts/run-all.sh @@ -0,0 +1,118 @@ +#CMN="--compilation_steps_only" + + + +echo "******** Running: 1 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule previewMintIndependentOfAllowance previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawIndependentOfMaxWithdraw previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance \ +--msg "1: verifyERC4626.conf" +# maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert + +echo "******** Running: 2 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay \ +--msg "2: verifyERC4626MintDepositSummarization.conf" + +echo "******** Running: 3 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626DepositSummarization.conf --rule depositCheckIndexERayAssert1 \ +--msg "3: " + +echo "******** Running: 4 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint \ +--msg "4: " + # maxDepositConstant \ + +echo "******** Running: 5 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626Extended.conf --rule redeemSum \ +--msg "5: " + +echo "******** Running: 6 ***************" +certoraRun $CMN certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf \ +--msg "6: " + +echo "******** Running: 7 ***************" +certoraRun $CMN certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf \ +--msg "7: " + +echo "******** Running: 8 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsConsistencyWhenSufficientRewardsExist \ +--msg "8: " + +echo "******** Running: 9 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsConsistencyWhenInsufficientRewards \ +--msg "9: " + +echo "******** Running: 10 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim \ +--msg "10: " + +echo "******** Running: 11 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim_timedout_methods \ +--msg "11: " + +echo "******** Running: 12 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule rewardsTotalDeclinesOnlyByClaim_redeem_methods \ +--msg "12: " + +echo "******** Running: 13 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule solvency_positive_total_supply_only_if_positive_asset \ +--msg "13: " + +echo "******** Running: 14 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply \ +--msg "14: " + +echo "******** Running: 15 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule solvency_total_asset_geq_total_supply_CASE_SPLIT_redeem \ +--msg "15: " + +echo "******** Running: 16 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule singleAssetAccruedRewards \ +--msg "16: " + +echo "******** Running: 17 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule totalAssets_stable \ +--msg "17: " + +echo "******** Running: 18 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule totalAssets_stable_after_collectAndUpdateRewards \ +--msg "18: " + +echo "******** Running: 19 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule reward_balance_stable_after_collectAndUpdateRewards \ +--msg "19: " + +echo "******** Running: 20 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT \ +--msg "20: " + +echo "******** Running: 21 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewards_stable \ +--msg "21: " + +echo "******** Running: 22 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_deposit \ +--msg "22: " + +echo "******** Running: 23 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_redeem \ +--msg "23: " + +echo "******** Running: 24 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule totalClaimableRewards_stable_CASE_SPLIT_deposit \ +--msg "24: " + +echo "******** Running: 25 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewards_stable_after_refreshRewardTokens \ +--msg "25: " + +echo "******** Running: 26 ***************" +certoraRun $CMN certora/stata/conf/verifyStaticATokenLM.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf \ +--msg "26: " + +echo "******** Running: 27 ***************" +certoraRun $CMN certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient \ +--msg "27: " + +echo "******** Running: 28 ***************" +certoraRun $CMN certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient \ +--msg "28: " + diff --git a/certora/stata/specs/erc4626/erc4626.spec b/certora/stata/specs/erc4626/erc4626.spec new file mode 100644 index 00000000..1a99d6ec --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626.spec @@ -0,0 +1,702 @@ +import "../methods/methods_base.spec"; + +methods { + function balanceOf(address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; +} +///////////////// Properties /////////////////////// + /**************************** + * previewDeposit * + *****************************/ + + /*** + * rule to check the following for the previewDeposit function: + * _1. MUST return as close to and no more than the exact amount of Vault shares that would + * be minted in a deposit call in the same transaction. I.e. deposit should return the same or more shares as previewDeposit if called in the same transaction. + */ + // STATUS: Verified, that the amount returned by previewDeposit is exactly equal to that returned by the deposit function. + // This is a stronger property than the one required by the EIP. + // https://vaas-stg.certora.com/output/11775/1488de4bb1e24d37a7972b0c2785df65/?anonymousKey=6f68dd14376fa7d0109ef2687f72d1ef1903dda8 + + ///@title previewDeposit returns the right value + ///@notice EIP4626 dictates that previewDeposit must return as close to and no more than the exact amount of Vault shares that would be minted in a deposit call in the same transaction. The previewDeposit function in staticAToken contract returns a value exactly equal to that returned by the deposit function. + rule previewDepositAmountCheck(){ + env e1; + env e2; + uint256 assets; + address receiver; + uint256 previewShares; + uint256 shares; + + previewShares = previewDeposit(e1, assets); + shares = deposit(e2, assets, receiver); + + assert previewShares == shares,"preview shares should be equal to actual shares"; + } + + // The EIP4626 spec requires that the previewDeposit function must not account for maxDeposit limit or the allowance of asset tokens. + // The following rule checks that the value returned by the previewDeposit function is independent of allowance that the contract might have + // for transferring assets from any user. + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/05df2a231ec74da28ed10f627d3c7f72/?anonymousKey=70c692cbbf781597e0dc0b53a7d4ed6968bb467a + + ///@title previewDeposit independent of Allowance + ///@notice This rule checks that the value returned by the previewDeposit function is independent of allowance that the contract might have for transferring assets from any user. The value retunred is the same regardless of the specified asset amount being more than, equal to or less than the allowance. + rule previewDepositIndependentOfAllowanceApprove() + { + env e1; + env e2; + env e3; + env e4; + env e5; + address user; + uint256 ATokAllowance1 = _AToken.allowance(currentContract, user); + uint256 assets1; + require assets1 < ATokAllowance1; + uint256 previewShares1 = previewDeposit(e1, assets1); + + uint256 amount1; + _AToken.approve(e2, currentContract, amount1); + + uint256 ATokAllowance2 = _AToken.allowance(currentContract, user); + require assets1 == ATokAllowance2; + uint256 previewShares2 = previewDeposit(e3, assets1); + + uint256 amount2; + _AToken.approve(e4, currentContract, amount2); + + uint256 ATokAllowance3 = _AToken.allowance(currentContract, user); + require assets1 > ATokAllowance3; + uint256 previewShares3 = previewDeposit(e5, assets1); + + assert previewShares1 == previewShares2,"previewDeposit should not change regardless of assets > or = allowance"; + assert previewShares2 == previewShares3,"previewDeposit should not change regardless of assets < or = allowance"; + } + + /**************************** + * previewMint * + *****************************/ + + /*** + * rule to check the following for the previewMint function: + * _1. MUST return as close to and no fewer than the exact amount of assets that would be deposited in a mint call in the same transaction. + * I.e. mint should return the same or fewer assets as previewMint if called in the same transaction. + */ + // STATUS: Verified, that the amount returned by previewMint is exactly equal to that returned by the deposit function. + // This is a stronger property than the one required by the EIP. + // https://vaas-stg.certora.com/output/11775/97ed98809a464668b0bfbfb6f6a6277b/?anonymousKey=e8f91f54cebea2f42d809068cf55511670b817d4 + ///@title previewMint returns the right value + ///@notice EIP4626 dictates that previewMint must return as close to and no more than the exact amount of assets that would be deposited in a mint call in the same transaction. The previewMint function in staticAToken contract returns a value exactly equal to that returned by the mint function. + rule previewMintAmountCheck(env e){ + uint256 shares; + address receiver; + uint256 previewAssets; + uint256 assets; + + previewAssets = previewMint(shares); + assets = mint(e, shares, receiver); + assert previewAssets == assets,"preview should be equal to actual"; + } + + + // The EIP4626 spec requires that the previewMint function must not account for mint limits like those returned from maxMint + // and should always act as though the mint would be accepted, regardless whether the user has approved the contract to transfer + // the specified amount of assets + + // The following rule checks that the previewMint returned value is independent of allowance of assets. The value returned by + // previewMind under three conditions a. amount < allowance from any user b. amount = allowance from any user c. amount > allowance + // from any user. The returned value is the same in all cases thus making it independent of the allowance from any user + // STATUS: Verified + + // https://vaas-stg.certora.com/output/11775/937cb9bc984947de98c9bf759b483017/?anonymousKey=db3080cc2ddcf91fe3e7dab4d4a56dad24e6bbce + ///@title previewMint independent of Allowance + ///@notice This rule checks that the value returned by the previewMint function is independent of allowance that the contract might have for transferring assets from any user. The value returned is the same regardless of the equivalent asset amount being more than, equal to or less than the allowance. + rule previewMintIndependentOfAllowance(){ + // allowance of currentContract for asset transfer from msg.sender to + address user; + uint256 ATokAllowance1 = _AToken.allowance(currentContract, user); + uint256 shares1; + uint256 assets1; + uint256 assets2; + env e1; + require convertToAssets(e1, shares1) < ATokAllowance1; + uint256 previewAssets1 = previewMint(shares1); + + env e2; + address receiver1; + deposit(e2, assets1, receiver1); + + uint256 ATokAllowance2 = _AToken.allowance(currentContract, user); + env e3; + require convertToAssets(e3, shares1) == ATokAllowance2; + uint256 previewAssets2 = previewMint(shares1); + + env e4; + address receiver2; + deposit(e2, assets2, receiver2); + + env e5; + uint256 ATokAllowance3 = _AToken.allowance(currentContract, user); + require convertToAssets(e4, shares1) > ATokAllowance3; + uint256 previewAssets3 = previewMint(shares1); + + assert previewAssets1 == previewAssets2,"previewMint should not change regardless of C2A(shares) > or = allowance"; + assert previewAssets2 == previewAssets3,"previewMint should not change regardless of C2A(shares) < or = allowance"; + } + + /******************************** + * previewWithdraw * + *********************************/ + + /*** + * rule to check the following for the previewWithdraw function: + * _1. MUST return as close to and no fewer than the exact amount of Vault shares that would be burned in a withdraw call in the + * same transaction. I.e. withdraw should return the same or fewer shares as previewWithdraw if called in the same transaction + */ + // STATUS: Verified, that the amount returned by previewWithdraw is exactly equal to that returned by the withdraw function. + // This is a stronger property than the one required by the EIP. + // https://vaas-stg.certora.com/output/11775/444832541b5f4f22ab7373f6de1ee782/?anonymousKey=86856741d701630321afe5bc573fc258bbd99739 + ///@title previewWithdraw returns the right value + ///@notice EIP4626 dictates that previewWithdraw must return as close to and no more than the exact amount of shares that would be burned in a withdraw call in the same transaction. The previewWithdraw function in staticAToken contract returns a value exactly equal to that returned by the withdraw function. + rule previewWithdrawAmountCheck(env e){ + uint256 assets; + address receiver; + address owner; + uint256 shares; + uint256 previewShares; + + previewShares = previewWithdraw(assets); + shares = withdraw(e, assets, receiver, owner); + + assert previewShares == shares,"preview should be equal to actual shares"; + } + + // The EIP4626 spec requires that the previewWithdraw function must not account for withdrawal limits like those returned + // from maxWithdraw and should always act as though the withdrawal would be accepted, regardless of whether or not the user + // has enough shares, etc. + // This rules checks that the previewWithdraw function return value is independent of any level of maxWithdraw (relative to + // the asset amount) for any user + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/50abf537cd134084ab309788a0d4b95a/?anonymousKey=c9cbb863531b85f4a877260997f0acfb770e7e99 + + ///@title previewWithdraw independent of maxWithdraw + ///@notice This rule checks that the value returned by previewWithdraw is independent of the value returned by maxWithdraw. + rule previewWithdrawIndependentOfMaxWithdraw(env e){ + env e1; + env e2; + address user; + uint256 maxWithdraw1 = maxWithdraw(user); + uint256 assets1; + uint256 shares1; + uint256 shares2; + + require assets1 > maxWithdraw1; + uint256 previewShares1 = previewWithdraw(assets1); + + mint(e1, shares1, user); + + uint256 maxWithdraw2 = maxWithdraw(user); + require assets1 == maxWithdraw2; + uint256 previewShares2 = previewWithdraw(assets1); + + mint(e2, shares2, user); + + uint256 maxWithdraw3 = maxWithdraw(user); + require assets1 < maxWithdraw3; + uint256 previewShares3 = previewWithdraw(assets1); + + assert previewShares1 == previewShares2 && previewShares2 == previewShares3,"preview withdraw should be independent of allowance"; + } + + // The EIP4626 spec requires that the previewWithdraw function must not account for withdrawal limits like those returned by + // maxWithdraw and should always act as though the withdrawal would be accepted, regardless if the user has enough shares, etc. + // The following two rules checks that the previewWithdraw function is independent of any level of share balance(relative to asset amount) of + // any user + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/8e8fd50a3fba4018b924eb6d8764d77f/?anonymousKey=3fee78908151c06e470add0ed2a9f4479f9bea7b + + ///@title previewWithdraw independent of any user's share balance + ///@notice This rule checks that the value returned by the previewWithdraw function is independent of any user's share balance. The value retunred is the same regardless it being >, = or < any user's balance. + rule previewWithdrawIndependentOfBalance1(){ + env e1; + env e2; + env e3; + + address user; + uint256 shareBal1 = balanceOf(user); + uint256 assets1; + uint256 shares1; + uint256 shares2; + + require assets1 > convertToAssets(e1, shareBal1);//asset amount greater than what the user is entitled to on account of his share balance + uint256 previewShares1 = previewWithdraw(assets1); + + _mintWrapper(e2, user, shares1); + + uint256 shareBal2 = balanceOf(user); + require assets1 == convertToAssets(e3, shareBal2); //asset amount equal to what the user is entitled to on account of his share balance + uint256 previewShares2 = previewWithdraw(assets1); + + assert previewShares1 == previewShares2, + "preview withdraw should be independent of allowance"; + } + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/c686d90f1baf4a77a093d5902125f08f/?anonymousKey=da2ce2f7098c87d89abb767139e689017bd618b1 + + rule previewWithdrawIndependentOfBalance2(){ + env e1; + env e2; + env e3; + + address user; + uint256 shareBal1 = balanceOf(user); + uint256 assets1; + uint256 shares1; + uint256 shares2; + + require assets1 == convertToAssets(e1, shareBal1);//asset amount greater than what the user is entitled to on account of his share balance + uint256 previewShares1 = previewWithdraw(assets1); + + _mintWrapper(e2, user, shares1); + + uint256 shareBal2 = balanceOf(user); + require assets1 < convertToAssets(e3, shareBal2); //asset amount equal to what the user is entitled to on account of his share balance + uint256 previewShares2 = previewWithdraw(assets1); + + assert previewShares1 == previewShares2, + "preview withdraw should be independent of allowance"; + } + + /****************************** + * previewRedeem * + *******************************/ + + /*** + * rule to check the following for the previewRedeem function: + * _1. MUST return as CLOSE to and no more than the exact amount of assets that would be withdrawn in a redeem call in the same transaction. I.e. redeem should return the same or more assets as previewRedeem if called in the same transaction. + */ + // STATUS: Verified, that the amount returned by previewRedeem is exactly equal to that returned by the redeem function. + // This is a stronger property than the one required by the EIP. + // https://vaas-stg.certora.com/output/11775/24e2fe4d485a42618e4e38f0d4376dd2/?anonymousKey=a117a61d3d1dea53fbc875be84292f27af3afd6a + + ///@title previewRedeem returns the right value + ///@notice EIP4626 dictates that previewRedeem must return as close to and no more than the exact amount of assets that would be returned in a redeem call in the same transaction. The previewRedeem function in staticAToken contract returns a value exactly equal to that returned by the redeem function. + rule previewRedeemAmountCheck(env e){ + uint256 shares; + address receiver; + address owner; + uint256 previewAssets; + uint256 assets; + + previewAssets = previewRedeem(shares); + assets = redeem(e, shares, receiver, owner); + + assert previewAssets == assets,"preview should the same as the actual assets received"; + } + + // The EIP4626 spec requires that the previewRedeem function must not account for redemption limits like those returned by + // the maxRedeem function and should always act as though the redemption would be accepted, regardless if the user has enough + // shares, etc. + // + // The following two rules checks that the previewRedeem return value is independent of any level of maxRedeem (relative to the share amount) for any user. + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/e1d9f84456b04e3caa0c4495f3022bb8/?anonymousKey=d82a8ae9fd795f8206f8c117bf5698079c2239cb + + ///@title previewRedeem independent of maxRedeem + ///@notice This rule checks that the value returned by the previewRedeem function is independent of the value returned by maxRedeem. The value retunred is the same regardless of it being >, = or < the value returned by maxRedeem. + rule previewRedeemIndependentOfMaxRedeem1(){ + env e1; + env e2; + address user; + uint256 shares1; + uint256 shares2; + + uint256 maxRedeemableShares1 = maxRedeem(user); + require shares1 == maxRedeemableShares1; + uint256 previewAssets1 = previewRedeem(shares1); + + _mintWrapper(e1, user, shares2); + + uint256 maxRedeemableShares2 = maxRedeem(user); + require shares1 < maxRedeemableShares2; + uint256 previewAssets2 = previewRedeem(shares1); + + assert previewAssets1 == previewAssets2,"previewRedeem should be independent of maxRedeem"; + } + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/16a4a248207b4ae28d778b0f405a3161/?anonymousKey=5efc898c58a75e7fa35d104b23ea3ef4ffe7ecf3 + rule previewRedeemIndependentOfMaxRedeem2(){ + env e1; + env e2; + address user; + uint256 shares1; + uint256 shares2; + + uint256 maxRedeemableShares1 = maxRedeem(user); + require shares1 > maxRedeemableShares1; + uint256 previewAssets1 = previewRedeem(shares1); + + _mintWrapper(e1, user, shares2); + + uint256 maxRedeemableShares2 = maxRedeem(user); + require shares1 == maxRedeemableShares2; + uint256 previewAssets2 = previewRedeem(shares1); + + assert previewAssets1 == previewAssets2,"previewRedeem should be independent of maxRedeem"; + } + + // The EIP4626 spec requires that the previewRedeem function must not account for redemption limits like those returned by maxRedeem + // and should always act as though the redemption would be accepted, regardless of whether the user has enough shares, etc. + // The following rule checks that the previewRedeem return value is independent of any level of share balance (relative to the redemption + // share amount) for any user. + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/de8e4742dbc44945b94e3a9b8e4375ae/?anonymousKey=65bd53e6365d5dd66f76004a80f45de06f088359 + + ///@title previewRedeem independent of any user's balance + ///@notice This rule checks that the value returned by the previewRedeem function is independent of any user's share balance. The value retunred is the same regardless of it being >, = or < any user's balance. + rule previewRedeemIndependentOfBalance(){ + env e1; + env e2; + env e3; + uint256 shares1; + uint256 shares2; + uint256 shares3; + address user1; + uint256 balance1 = balanceOf(user1); + require shares1 > balance1; + uint256 previewAssets1 = previewRedeem(shares1); + + mint(e1, shares2, user1); + uint256 balance2 = balanceOf(user1); + require shares1 == balance2; + uint256 previewAssets2 = previewRedeem(shares1); + + mint(e1, shares3, user1); + uint256 balance3 = balanceOf(user1); + require shares1 < balance3; + uint256 previewAssets3 = previewRedeem(shares1); + + assert previewAssets1 == previewAssets2 && previewAssets2 == previewAssets3,"previewRedeem should be independent of balance"; + } + + /**************************** + * withdraw * + ****************************/ + + /*** + * rule to check the following for the withdraw function: + * 1. SHOULD check msg.sender can spend owner funds, assets needs to be converted to shares and shares should be checked for allowance. + * 2. MUST revert if all of assets cannot be withdrawn (due to withdrawal limit being reached, slippage, the owner not having enough shares, etc). + */ + // STATUS: VERIFIED + // violates #2 above. For any asset amount worth less than 1/2 AToken, the function will not withdrawn anything and not revert. EIP 4626 non compliant for assets < 1/2 AToken. + // For assets amount worth less than 1/2 AToken 0 assets will be withdrawn. Asset amount worth 1/2 AToken and more the final withdrawn amount would be assets +- 1/2AToken. + // https://vaas-stg.certora.com/output/11775/a2ff16b9d15d405cb11572afd0ea9413/?anonymousKey=2d51005a275559a456558660e33de6870aa19846 + ///@title Allowance and withdrawn amount check for withdraw function + ///@notice This rules checks that the withdraw function burns shares upto the allowance for the msg.sender and that the assets withdrawn are within the specified asset amount +- 1/2ATokens range + rule withdrawCheck(env e){ + address owner; + address receiver; + uint256 assets; + + uint256 allowed = allowance(e, owner, e.msg.sender); + uint256 balBefore = _AToken.balanceOf(receiver); + uint256 shareBalBefore = balanceOf(owner); + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS(); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + require e.msg.sender != currentContract; + require receiver != currentContract; + require owner != currentContract; + + require index >= RAY(); + + uint256 sharesBurnt = withdraw(e, assets, receiver, owner); + + uint256 balAfter = _AToken.balanceOf(receiver); + uint256 shareBalAfter = balanceOf(owner); + + // checking for allowance in case msg.sender is not the owner + assert e.msg.sender != owner => allowed >= sharesBurnt,"msg.sender should have allowane to spend owner's shares"; + + // lower bound. First part means atleast 1/2 AToken worth of UL is being deposited + assert assets * 2 * RAY() >= to_mathint(index) => balAfter - balBefore > assets - index/2*RAY(), + "withdrawn amount should be no less than 1/2 AToken worth of UL less than the assets amount"; + + //upper bound + assert balAfter - balBefore <= assets + index/2*RAY(), + "withdrawn amount should be no more than 1/2 AToken worth of UL more than the number of assets "; + } + + /************************** + * redeem * + **************************/ + + /*** + * rule to check the following for the withdraw function: + * 1. SHOULD check msg.sender can spend owner funds using allowance. + * 2. MUST revert if all of shares cannot be redeemed (due to withdrawal limit being reached, slippage, the owner not having enough shares, etc). + */ + // STATUS: VERIFIED + // https://vaas-stg.certora.com/output/11775/ff8f93d3158f40a5bb27ba35b15e771d/?anonymousKey=c0e02f130ff0d31552c6741d3b1751bda5177bfd + ///@title allowance and minted share amount check for redeem function + ///@notice This rules checks that the redeem function burns shares upto the allowance for the msg.sender and that the shares burned are exactly equal to the specified share amount + rule redeemCheck(env e){ + uint256 shares; + address receiver; + address owner; + uint256 assets; + mathint allowed = allowance(e, owner, e.msg.sender); + uint256 balBefore = balanceOf(owner); + + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS(); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + require index > RAY(); + require e.msg.sender != currentContract; + require receiver != currentContract; + + assets = redeem(e, shares, receiver, owner); + + uint256 balAfter = balanceOf(owner); + + assert e.msg.sender != owner => allowed >= (balBefore - balAfter),"msg.sender should have allowance for transferring owner's shares"; + assert to_mathint(shares) == balBefore - balAfter,"exactly the specified amount of shares must be burnt"; + } + + /***************************** + * convertToAssets * + *****************************/ + + /*** + * rule to check the following for the covertToAssets function: + * 1. MUST NOT show any variations depending on the caller. + * 2. MUST round down towards 0. + */ + // STATUS: VERIFIED + // https://vaas-stg.certora.com/output/11775/52075caad70145798090e1038b16e6d0/?anonymousKey=b79fa800a2885356277ca6690c723fece38c7b40 + ///@title convert to assets function check + ///@notice This rule checks that the convertToAssets function will return the same amount for assets for the given number of shares under all conditions and the calculation will always round down. + rule convertToAssetsCheck(){ + env e1; + env e2; + env e3; + uint256 shares1; + uint256 shares2; + storage before = lastStorage; + + mathint assets1 = convertToAssets(e1, shares1) at before; + mathint assets2 = convertToAssets(e2, shares1) at before; + mathint assets3 = convertToAssets(e2, shares2) at before; + mathint combinedAssets = convertToAssets(e3, require_uint256(shares1 +shares2)) at before; + + // assert !lastReverted,"should not revert except for overflow"; + assert assets1 == assets2,"conversion to assets should be independent of env such as msg.sender"; + assert shares1 + shares2 <= max_uint256 => assets1 + assets3 <= combinedAssets,"conversion should round down and not up"; + } + + /// @title Converting amount to shares is properly rounded down + rule amountConversionRoundedDown(uint256 amount) { + env e; + uint256 shares = convertToShares(e, amount); + assert convertToAssets(e, shares) <= amount, "Too many converted shares"; + + /* The next assertion shows that the rounding in `convertToAssets` is tight. This + * protects the user. For example, a function `convertToAssets` that always returns + * zero would have passed the previous assertion, but not the next one. + */ + assert convertToAssets(e, require_uint256(shares + 1)) >= amount, "Too few converted shares"; + } + + /** + * @title ConvertToAssets must not revert unless due to integer overflow + * From EIP4626: + * > MUST NOT revert unless due to integer overflow caused by an unreasonably large input. + * We define large input as 10^45. To be precise we need that `shares * rate < 2^256 ~= 10^77`, + * hence we require that: + * - `shares < 10^45` + * - `rate < 10^32` + */ + rule toAssetsDoesNotRevert(uint256 shares) { + require shares < 10^45; + env e; + require e.msg.value == 0; + + // Prevent revert due to overflow. + // Roughly speaking ConvertToAssets returns shares * rate() / RAY. + mathint ray_math = to_mathint(RAY()); + mathint rate_math = to_mathint(rate()); + mathint shares_math = to_mathint(shares); + require rate_math < 10^32; + + uint256 assets = convertToAssets@withrevert(e, shares); + bool reverted = lastReverted; + + assert !reverted, "Conversion to assets reverted"; + } + + /***************************** + * convertToShares * + *****************************/ + + /*** + * rule to check the following for the convertToShares function: + * 1. MUST NOT show any variations depending on the caller. + * 2. MUST round down towards 0. + */ + // STATUS: VERIFIED + // https://vaas-stg.certora.com/output/11775/a75adca8d9914e80bf09bbaeb168f0f8/?anonymousKey=34ac3fe43e28e4722c7d4211af6e3e1077dc3b22 + ///@title convert to shares function check + ///@notice This rule checks that the convertToShares function will return the same amount for shares for the given number of assets under all conditions and the calculation will always round down. + rule convertToSharesCheck(){ + env e1; + env e2; + env e3; + uint256 assets1; + uint256 assets2; + storage before = lastStorage; + + + mathint shares1 = convertToShares(e1, assets1) at before; + mathint shares2 = convertToShares(e2, assets1) at before; + mathint shares3 = convertToShares(e2, assets2) at before; + mathint combinedShares = convertToShares(e3, assert_uint256(assets1 + assets2)) at before; + + assert shares1 == shares2,"conversion to shares should be independent of env variables including msg.sender"; + assert shares1 + shares3 <= combinedShares,"conversion should round down and not up"; + } + + /// @title Converting shares to amount is properly rounded down + rule sharesConversionRoundedDown(uint256 shares) { + env e; + uint256 amount = convertToAssets(e, shares); + assert convertToShares(e, amount) <= shares, "Amount converted is too high"; + + /* The next assertion shows that the rounding in `convertToShares` is tight. + * For example, a function `convertToShares` that always returns zero + * would have passed the previous assertion, but not the next one. + */ + assert convertToShares(e, require_uint256(amount + 1)) >= shares, "Amount converted is too low"; + } + + /** + * @title ConvertToShares must not revert except for overflow + * From EIP4626: + * > MUST NOT revert unless due to integer overflow caused by an unreasonably large input. + * We define large input as `10^50`. To be precise, we need that `RAY * assets < 2^256`, since + * `2^256~=10^77` and `RAY=10^27` we get that `assets < 10^50`. + * + * Note. *We also require that:* **`rate > 0`**. + */ + rule toSharesDoesNotRevert(uint256 assets) { + require assets < 10^50; + env e; + require e.msg.value == 0; + + // Prevent revert due to overflow. + // Roughly speaking ConvertToShares returns assets * RAY / rate(). + mathint ray_math = to_mathint(RAY()); + mathint rate_math = to_mathint(rate()); + mathint assets_math = to_mathint(assets); + require rate_math > 0; + + uint256 shares = convertToShares@withrevert(e, assets); + bool reverted = lastReverted; + + assert !reverted, "Conversion to shares reverted"; + } + +/************************ + * maxWithdraw * + *************************/ + +// maxWithdraw must not revert +// Nissan remark Aug-2025: this rule doesn't hold due to (a theoretical) possible arithmetical overflow +// in the functions rayDivRoundUp/Down +rule maxWithdrawMustntRevert(address user){ + // This assumption subject to correct configuration of the pool, aToken and statAToken. + // The assumption was ran by and approved by BGD + require rate() > 0; + maxWithdraw@withrevert(user); + assert !lastReverted; +} + +/// @title Ensure `maxWithdraw` conforms to conversion functions +rule maxWithdrawConversionCompliance(address owner) { + env e; + uint256 shares = balanceOf(owner); + uint256 amountConverted = convertToAssets(e, shares); + + assert maxWithdraw(e, owner) <= amountConverted, "Can withdraw more than converted amount"; +} + +/********************** + * maxRedeem * + ***********************/ + +// maxRedeem must not revert +// Nissan remark Aug-2025: this rule doesn't hold due to (a theoretical) possible arithmetical overflow +// in the functions rayDivRoundUp/Down +rule maxRedeemMustntRevert(address user) { + // This assumption subject to correct configuration of the pool, aToken and statAToken. + // The assumption was ran by and approved by BGD + require rate() > 0; + maxRedeem@withrevert(user); + assert !lastReverted; +} + +/// @title Ensure `maxRedeem` is not higher than balance +rule maxRedeemCompliance(address owner) { + uint256 shares = balanceOf(owner); + assert maxRedeem(owner) <= shares, "Can redeem more than available shares)"; +} + +/************************ + * maxDeposit * + *************************/ + +// maxDeposit must not revert +// Nissan remark Aug-2025: this rule doesn't hold due to (a theoretical) possible arithmetical overflow +// in the functions rayDivRoundUp/Down +rule maxDepositMustntRevert(address user) { + env e; + require e.msg.value ==0; + // This assumption subject to correct configuration of the pool, aToken and statAToken. + // The assumption was ran by and approved by BGD + require rate() > 0; + maxDeposit@withrevert(e, user); + assert !lastReverted; +} + +/************************ + * maxMint * + *************************/ + +// maxMint must not revert +// Nissan remark Aug-2025: this rule doesn't hold due to (a theoretical) possible arithmetical overflow +// in the functions rayDivRoundUp/Down +rule maxMintMustntRevert(address user) { + env e; + require e.msg.value ==0; + // This assumption subject to correct configuration of the pool, aToken and statAToken. + // The assumption was ran by and approved by BGD + require rate() > 0; + maxMint@withrevert(e,user); + assert !lastReverted; +} + + /************************* + * totalAssets * + **************************/ + + // totalAssets must not revert + rule totalAssetsMustntRevert(address user){ + // This assumption subject to correct configuration of the pool, aToken and statAToken. + // The assumption was ran by and approved by BGD + require rate() > 0; + totalAssets@withrevert(); + assert !lastReverted; + } diff --git a/certora/stata/specs/erc4626/erc4626DepositSummarization.spec b/certora/stata/specs/erc4626/erc4626DepositSummarization.spec new file mode 100644 index 00000000..2d6f8613 --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626DepositSummarization.spec @@ -0,0 +1,71 @@ +import "../methods/methods_base.spec"; + +/////////////////// Methods //////////////////////// + +methods{ + // static aToken + // ------------- + function previewDeposit(uint256) external returns(uint256) envfree => NONDET; + function ERC20._mint(address, uint256) internal => NONDET; + + // rewards controller + // ------------------ + function _.handleAction(address, uint256, uint128) external => NONDET; +} + +///////////////// Properties /////////////////////// + + /********************* + * deposit * + **********************/ + + /*** + * rule to check the following for the deposit function: + * 1. MUST revert if all of assets cannot be deposited + */ + + // The function doesn't always deposit exactly the asset amount specified by the user due to rounding. The amount deposited is within 1/2AToken of the + // amount specified by the user. The amount of shares minted would be zero for less than 1AToken worth of assets. + // STATUS: Verified + // https://prover.certora.com/output/11775/0c902c255ba748e99e9f7c2f50395706/?anonymousKey=aeb7ec100e687a415dd05c0eb9a45f823ceaeb25 + ///@title Deposit amount check for Index > RAY + ///@notice This rule checks that, for index > RAY, the deposit function will deposit upto 1 AToken more than the specified deposit amount + rule depositCheckIndexGRayAssert1(env e){ + uint256 assets; + address receiver; + uint256 contractAssetBalBefore = _AToken.balanceOf(currentContract); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS();//Without this a different index will be used for conversions in the Atoken contract compared to the one used in StaticAToken + require e.msg.sender != currentContract; + require index > RAY();//since the index is initiated as RAY and only increases after that. index < RAY gives strange behaviors causing wildly inaccurate amounts being deposited and minted + + uint256 shares = deposit(e, assets, receiver); + + uint256 contractAssetBalAfter = _AToken.balanceOf(currentContract); + + // upper bound for deposited assets + assert contractAssetBalAfter - contractAssetBalBefore <= assets + index/RAY(); + } + + // STATUS: Verified + // https://prover.certora.com/output/11775/c149a926d08e44b98b05cec42ff97c0c/?anonymousKey=3a094dbfe8370e0ce3242e97cabd57a6df75a8c8 + ///@title Deposit amount check for Index == RAY + ///@notice This rule checks that, for index == RAY, the deposit function will deposit upto 1/2AToken more than the amount specified deposit amount + rule depositCheckIndexERayAssert1(env e){ + uint256 assets; + address receiver; + uint256 contractAssetBalBefore = _AToken.balanceOf(currentContract); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS();//Without this a different index will be used for conversions in the Atoken contract compared to the one used in StaticAToken + require e.msg.sender != currentContract; + require index == RAY();//since the index is initiated as RAY and only increases after that. index < RAY gives strange behaviors causing wildly inaccurate amounts being deposited and minted + + uint256 shares = deposit(e, assets, receiver); + + uint256 contractAssetBalAfter = _AToken.balanceOf(currentContract); + + // upper bound for deposited assets + assert contractAssetBalAfter - contractAssetBalBefore <= assets + index/(2 * RAY()); + } diff --git a/certora/stata/specs/erc4626/erc4626Extended.spec b/certora/stata/specs/erc4626/erc4626Extended.spec new file mode 100644 index 00000000..581c9d9f --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626Extended.spec @@ -0,0 +1,237 @@ +import "../methods/methods_base.spec"; + +///////////////// Properties /////////////////////// + + /*** + * #### A note on the conversion functions + * The conversion functions are: + * - assets to shares = `S(a) = (a * R) // r` + * - shares to assets = `A(s) = (s * r) // R` + * where a=assets, s=shares, R=RAY, r=rate. + * + * These imply: + * - `a * R - r < S(a) * r <= a * R a*R/r - 1 < S(a) <= a*R/r` + * - `s * r - R < A(s) * R <= s * r s*r/R - 1 < A(s) <= s*r/R` + * + * Hence: + * - `A(S(a)) > S(a)*r/R - 1 > (a*R/r - 1)*r/R - 1 = (a*R - r)/R - 1 = a - r/R - 1` + * - `S(A(s)) > A(s)*R/r - 1 > (s*r/R - 1)*R/r - 1 = (s*r - R)/r - 1 = s - R/r - 1` + */ + + /***************************** + * rounding range * + ******************************/ + + /** + * @title Ensure `previewWithdraw` tightly rounds up shares + * The lower bound (i.e. `previewWithdraw >= convertToShares`) follows from ERC4626. The upper bound + * is based on the current implementation. + */ + rule previewWithdrawRoundingRange(uint256 assets) { + env e; + uint256 shares = convertToShares(e, assets); + + assert previewWithdraw(assets) >= shares, "Preview withdraw takes less shares than converted"; + assert to_mathint(previewWithdraw(assets)) <= shares + 1, "Preview withdraw costs too many shares"; + } + + /** + * @title Ensure `previewRedeem` tightly rounds down assets + * The upper bound (i.e. `previewRedeem <= convertToAssets`) follows from ERC4626. The lower bound + * is based on the current implementation. + */ + rule previewRedeemRoundingRange(uint256 shares) { + env e; + uint256 assets = convertToAssets(e,shares); + + assert previewRedeem(shares) <= assets, "Preview redeem yields more assets than converted"; + assert previewRedeem(shares) + 1 + rate() / RAY() >= to_mathint(assets), "Preview redeem yields too few assets"; + } + + /** + * @title Inequality for conversion of amount to shares and back + * Note the precision depends on the ratio **`rate / RAY`**. + */ + rule amountConversionPreserved(uint256 amount) { + env e; + mathint mathamount = to_mathint(amount); + mathint converted = to_mathint(convertToAssets(e, convertToShares(e, amount))); + + // That `converted <= mathamount` was proved in `amountConversionRoundedDown` + assert mathamount - converted <= 1 + rate() / RAY(), "Too few converted assets"; + } + + /** + * @title Inequality for conversion of shares to amount and back + * Note the precision depends on the ratio **`RAY / rate`**. + */ + rule sharesConversionPreserved(uint256 shares) { + env e; + mathint mathshares = to_mathint(shares); + uint256 amount = convertToAssets(e, shares); + mathint converted = to_mathint(convertToShares(e, amount)); + + // That `converted <= mathshare` was proved in `sharesConversionRoundedDown` + assert mathshares - converted <= 1 + RAY() / rate(), "Too few converted shares"; + } + + /** + * @title Joining and splitting shares provides limited advantage + * This rule verifies that joining accounts (by combining shares), and splitting accounts + * (by splitting shares between accounts) provides limited advantage when converting to + * asset amounts. + */ + rule accountsJoiningSplittingIsLimited(uint256 shares1, uint256 shares2) { + env e; + uint256 amount1 = convertToAssets(e, shares1); + uint256 amount2 = convertToAssets(e, shares2); + uint256 jointShares = require_uint256(shares1 + shares2); + //require jointShares >= shares1 + shares2; // Prevent overflow + mathint jointAmount = convertToAssets(e, jointShares); + + assert jointAmount >= amount1 + amount2, "Found advantage in combining accounts"; + + /* Example as to why the following assertion should be true. Suppose conversion of shares + * to assets is division by 2 rounded down, and suppose shares1 = shares2 = 11. + * Then amount1 + amount2 = 5 + 5 = 10, but jointAmount = 22 // 2 = 11. + */ + assert jointAmount < amount1 + amount2 + 2, "Found advantage in splitting accounts"; + + /* The following assertion fails (as expected): + * assert jointAmount < amount1 + amount2 + 1, "Found advantage in splitting accounts"; + */ + } + + /** + * @title Joining and splitting assets provides limited advantage + * Similar to `accountsJoiningSplittingIsLimited` rule. + */ + rule convertSumOfAssetsPreserved(uint256 assets1, uint256 assets2) { + env e; + uint256 shares1 = convertToShares(e, assets1); + uint256 shares2 = convertToShares(e, assets2); + uint256 sumAssets = require_uint256(assets1 + assets2); + //require sumAssets >= assets1 + assets2; // Prevent overflow + mathint jointShares = convertToShares(e, sumAssets); + + assert jointShares >= shares1 + shares2, "Convert sum of assets bigger than parts"; + assert jointShares < shares1 + shares2 + 2, "Convert sum of assets far smaller than parts"; + } + + /// @title Redeeming sum of assets is nearly equal to sum of redeeming + rule redeemSum(uint256 shares1, uint256 shares2) { + env e; + address owner = e.msg.sender; // Handy alias + + uint256 assets1 = redeem(e, shares1, owner, owner); + uint256 assets2 = redeem(e, shares2, owner, owner); + mathint assetsSum = redeem(e, require_uint256(shares1 + shares2), owner, owner); + + assert assetsSum >= assets1 + assets2, "Redeemed sum smaller than parts"; + + /* See `accountsJoiningSplittingIsLimited` rule for why the following assertion + * is correct. + */ + assert assetsSum < assets1 + assets2 + 2, "Redeemed sum far larger than parts"; + } + + /* The commented out rule below (withdrawSum) timed out after 6994 seconds (see link below). + * However, we can deduce worse bounds from previous rules, here is the proof. + * TODO: should we try for better bounds? + * Let w = withdraw(assets), p = previewWithdraw(assets), s = convertToShares(assets), + * then: + * p - 1 <= w <= p -- by previewWithdrawNearlyWithdraw + * s <= p <= s + 1 -- by previewWithdrawRedeemCompliance + * Hence: s - 1 <= w <= s + 1 + * + * Let w1 = withdraw(assets1), s1 = convertToShares(assets1) + * w2 = withdraw(assets2), s2 = convertToShares(assets2) + * w = withdraw(assets1 + assets2), s = convertToShares(assets1 + assets2) + * By convertSumOfAssetsPreserved: + * s1 + s2 <= s <= s1 + s2 + 1 + * Therefore: + * w1 + w2 - 3 <= s1 + s2 - 1 <= s - 1 <= w <= s + 1 <= s1 + s2 + 2 <= w1 + w2 + 4 + * w1 + w2 - 3 <= w <= w1 + w2 + 4 + * + * The following run of withdrawSum timed out: + * https://vaas-stg.certora.com/output/98279/8f5d36ea63ba4a4ca1d23f781ec8dfa6?anonymousKey=11d8393da339881d925ad4e087252951d1da512d + */ + //rule withdrawSum(uint256 assets1, uint256 assets2) { + // env e; + // address owner = e.msg.sender; // Handy alias + // + // // Additional requirement to speed up calculation + // require balanceOf(owner) > convertToShares(2 * (assets1 + assets2)); + // + // uint256 shares1 = withdraw(e, assets1, owner, owner); + // uint256 shares2 = withdraw(e, assets2, owner, owner); + // uint256 sharesSum = withdraw(e, assets1 + assets2, owner, owner); + // + // assert sharesSum <= shares1 + shares2, "Withdraw sum larger than its parts"; + // assert sharesSum + 2 > shares1 + shares2, "Withdraw sum far smaller than it sparts"; + //} + + /* + * Preview functions rules + * ----------------------- + * The rules below prove that preview functions (e.g. `previewDeposit`) return the same + * values as their non-preview counterparts (e.g. `deposit`). + * The rules below passed with rule sanity: job-id=`2b196ea03b8c408dae6c79ae128fc516` + */ + + /***************************** + * previewDeposit * + *****************************/ + + /// Number of shares returned by `previewDeposit` is the same as `deposit`. + rule previewDepositSameAsDeposit(uint256 assets, address receiver) { + env e; + uint256 previewShares = previewDeposit(e, assets); + uint256 shares = deposit(e, assets, receiver); + assert previewShares == shares, "previewDeposit is unequal to deposit"; + } + + /***************************** + * previewMint * + *****************************/ + + /// Number of assets returned by `previewMint` is the same as `mint`. + rule previewMintSameAsMint(uint256 shares, address receiver) { + env e; + uint256 previewAssets = previewMint(shares); + uint256 assets = mint(e, shares, receiver); + assert previewAssets == assets, "previewMint is unequal to mint"; + } + +/*************************** + * maxDeposit * + ***************************/ +// The EIP4626 spec requires that the previewDeposit function must not account for maxDeposit limit or the allowance of asset tokens. +// Since maxDeposit is a constant, it cannot have any impact on the previewDeposit value. +// STATUS: Verified for all f except metaDeposit which has a reachability issue +// https://vaas-stg.certora.com/output/11775/044c54bdf1c0414898e88d9b03dda5a5/?anonymousKey=aaa9c0c1c413cd1fd3cbb9fdfdcaa20a098274c5 + +///@title maxDeposit is constant +///@notice This rule verifies that maxDeposit returns a constant value and therefore it cannot have any impact on the previewDeposit value. + +// Remark (by Nissan on Aug-2025): Currently this rule fails for several functions, like mint, deposit, redeem and more: +// https://prover.certora.com/output/66114/571e3b8d94884f9594d59efacba86999/?anonymousKey=4ffc80fdbcce585966830513ec609dfdcbe37807 +// It looks likr it is supposed to fail since maxDeposit depends on the scaled-total-suuply of the aToken which may be changed +// by the above functions. +rule maxDepositConstant(method f) + filtered { + f -> + f.contract == currentContract && + f.selector != sig:metaDeposit(address,address,uint256,uint16,bool,uint256,IStaticATokenLM.PermitParams calldata, IStaticATokenLM.SignatureParams calldata).selector + } + { + env e; + address receiver; + uint256 maxDep1 = maxDeposit(e, receiver); + calldataarg args; + f(e, args); + uint256 maxDep2 = maxDeposit(e, receiver); + + assert maxDep1 == maxDep2,"maxDeposit should not change"; + } + diff --git a/certora/stata/specs/erc4626/erc4626MintDepositSummarization.spec b/certora/stata/specs/erc4626/erc4626MintDepositSummarization.spec new file mode 100644 index 00000000..05409d5a --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626MintDepositSummarization.spec @@ -0,0 +1,156 @@ +import "../methods/erc20.spec"; + +using SymbolicLendingPool as _SymbolicLendingPool; +using ATokenInstance as _AToken; + +/////////////////// Methods //////////////////////// + +methods{ + // static aToken harness + // --------------------- + function getStaticATokenUnderlying() external returns (address) envfree; + + // erc20 + // ----- + function _.transferFrom(address,address,uint256) external => NONDET; + + // pool + function _SymbolicLendingPool.getReserveNormalizedIncome(address) external returns (uint256) envfree; + + // aToken + // ------ + function _AToken.UNDERLYING_ASSET_ADDRESS() external returns (address) envfree; +} + +///////////////// DEFINITIONS ////////////////////// + + definition RAY() returns uint256 = 10^27; + +///////////////// Properties /////////////////////// + + /******************** + * deposit * + *********************/ + + // The deposit function does not always deposit exactly the amount of assets specified by the user during the function call due to rounding error + // The following two rules check that the user gets an non-zero amount of shares if the specified amount of assets to be deposited is at least + // equivalent of 1 AToken. Refer to the erc4626DepositSummarization spec for rules asserting the upper bound of the amount of assets + // deposited in a deposit function call + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/b10cd30ab6fb400baeff6b61c07bb375/?anonymousKey=ccba22e832b7549efea9f0d4b1288da2c1377ccb + ///@title Deposit function mint amount check for index > RAY + ///@notice This rule checks that, for index > RAY, the deposit function will mint atleast 1 share as long as the specified deposit amount is worth atleast 1 AToken + rule depositCheckIndexGRayAssert2(env e){ + uint256 assets; + address receiver; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS();//Without this a different index will be used for conversions in the Atoken contract compared to the one used in StaticAToken + require e.msg.sender != currentContract; + require index > RAY();//since the index is initiated as RAY and only increases after that. index < RAY gives strange behaviors causing wildly inaccurate amounts being deposited and minted + + uint256 shares = deposit(e, assets, receiver); + + assert assets * RAY() >= to_mathint(index) => shares != 0; //if the assets amount is worth at least 1 Atoken then receiver will get atleast 1 share + } + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/2e162e12cafb49e688a7959a1d7dd4ca/?anonymousKey=d23ad1899e6bfa4e14fbf79799d008fa003dd633 + ///@title Deposit function mint amount check for index == RAY + ///@notice This rule checks that, for index == RAY, the deposit function will mint atleast 1 share as long as the specified deposit amount is worth atleast 1 AToken + + rule depositCheckIndexERayAssert2(env e){ + uint256 assets; + address receiver; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS();//Without this a different index will be used for conversions in the Atoken contract compared to the one used in StaticAToken + require e.msg.sender != currentContract; + require index == RAY();//since the index is initiated as RAY and only increases after that. index < RAY gives strange behaviors causing wildly inaccurate amounts being deposited and minted + + uint256 shares = deposit(e, assets, receiver); + + assert assets * RAY() >= to_mathint(index) => shares != 0; //if the assets amount is worth at least 1 Atoken then receiver will get atleast 1 share + } + + /***************** + * mint * + ******************/ + + /*** + * rule to check the following for the mint function: + * 1. MUST revert if all of shares cannot be minted + */ + // The mint function doesn't always mint exactly the number of shares specified in the function call due to rounding off. + // The following two rules check that the user will at least get as many shares they wanted to mint and upto one extra share + // over the specified amount + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/b6f6335e770b42ffa280e40d6f82906d/?anonymousKey=ed369d98039f29134aa774592c533ec0c4a9c08e + ///@title mint function check for upper bound of shares minted + ///@notice This rules checks that the mint function, for index > RAY, mints upto 1 extra share over the amount specified by the caller + rule mintCheckIndexGRayUpperBound(env e){ + uint256 shares; + address receiver; + uint256 assets; + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS(); + require e.msg.sender != currentContract; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + + uint256 receiverBalBefore = balanceOf(e, receiver); + require receiverBalBefore + shares <= max_uint256;//avoiding overflow + require index > RAY(); + + assets = mint(e, shares, receiver); + + uint256 receiverBalAfter = balanceOf(e, receiver); + // upperbound + assert to_mathint(receiverBalAfter) <= receiverBalBefore + shares + 1,"receiver should get no more than the 1 extra share"; + } + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/d794a47fa37c4c1e9f9fcb45f33ec6c5/?anonymousKey=8a280f8c9ba94d2c0ce98a7240969c02828ad17b + ///@title mint function check for lower bound of shares minted + ///@notice This rules checks that the mint function, for index > RAY, mints atleast the amount of shares specified by the caller + rule mintCheckIndexGRayLowerBound(env e){ + uint256 shares; + address receiver; + uint256 assets; + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS(); + require e.msg.sender != currentContract; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + + uint256 receiverBalBefore = balanceOf(e, receiver); + require receiverBalBefore + shares <= max_uint256;//avoiding overflow + require index > RAY(); + + assets = mint(e, shares, receiver); + + uint256 receiverBalAfter = balanceOf(e, receiver); + // lowerbound + assert to_mathint(receiverBalAfter) >= receiverBalBefore + shares,"receiver should get no less than the amount of shares requested"; + } + + // STATUS: Verified + // https://vaas-stg.certora.com/output/11775/bdf1ff3daa8542ebaac08c1950fdb89e/?anonymousKey=c5b77c1b715310da8f355d2b27bdb4008e70d519 + ///@title mint function check for index == RAY + ///@notice This rule checks that, for index == RAY, the mind function will mint atleast the specifed amount of shares and upto 1 extra share over the specified amount + rule mintCheckIndexEqualsRay(env e){ + uint256 shares; + address receiver; + uint256 assets; + require getStaticATokenUnderlying() == _AToken.UNDERLYING_ASSET_ADDRESS(); + require e.msg.sender != currentContract; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(getStaticATokenUnderlying()); + + uint256 receiverBalBefore = balanceOf(e, receiver); + require receiverBalBefore + shares <= max_uint256;//avoiding overflow + require index == RAY(); + + assets = mint(e, shares, receiver); + + uint256 receiverBalAfter = balanceOf(e, receiver); + + assert to_mathint(receiverBalAfter) <= receiverBalBefore + shares + 1,"receiver should get no more than the 1 extra share"; + assert to_mathint(receiverBalAfter) >= receiverBalBefore + shares,"receiver should get no less than the amount of shares requested"; + } diff --git a/certora/stata/specs/methods/erc20.spec b/certora/stata/specs/methods/erc20.spec new file mode 100644 index 00000000..bab7e156 --- /dev/null +++ b/certora/stata/specs/methods/erc20.spec @@ -0,0 +1,12 @@ +// erc20 methods +methods { + function _.name() external => DISPATCHER(true); + function _.symbol() external => DISPATCHER(true); + function _.decimals() external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address,address) external => DISPATCHER(true); + function _.approve(address,uint256) external => DISPATCHER(true); + function _.transfer(address,uint256) external => DISPATCHER(true); + // transferFrom(address,address,uint256) returns (bool) => DISPATCHER(true) +} diff --git a/certora/stata/specs/methods/methods_base.spec b/certora/stata/specs/methods/methods_base.spec new file mode 100644 index 00000000..1678f706 --- /dev/null +++ b/certora/stata/specs/methods/methods_base.spec @@ -0,0 +1,160 @@ +import "erc20.spec"; + +using StaticATokenLMHarness as _StaticATokenLM; +using SymbolicLendingPool as _SymbolicLendingPool; +using RewardsControllerHarness as _RewardsController; +using TransferStrategyHarness as _TransferStrategy; +using DummyERC20_aTokenUnderlying as _DummyERC20_aTokenUnderlying; +using ATokenInstance as _AToken; +using DummyERC20_rewardToken as _DummyERC20_rewardToken; + +/////////////////// Methods //////////////////////// + +methods { + // static aToken + // ------------- + function asset() external returns (address) envfree; + function totalAssets() external returns (uint256) envfree; + function maxWithdraw(address owner) external returns (uint256) envfree; + function maxRedeem(address owner) external returns (uint256) envfree; + function previewWithdraw(uint256) external returns (uint256) envfree; + function previewRedeem(uint256) external returns (uint256) envfree; + function maxDeposit(address) external returns (uint256); + function previewMint(uint256) external returns (uint256) envfree; + function maxMint(address) external returns (uint256); + function rate() external returns (uint256) envfree; + function getUnclaimedRewards(address, address) external returns (uint256) envfree; + function rewardTokens() external returns (address[]) envfree; + function isRegisteredRewardToken(address) external returns (bool) envfree; + + // static aToken harness + // --------------------- + function getStaticATokenUnderlying() external returns (address) envfree; + function getRewardsIndexOnLastInteraction(address, address) external returns (uint128) envfree; + function getRewardTokensLength() external returns (uint256) envfree; + function getRewardToken(uint256) external returns (address) envfree; + + // erc20 + // ----- + function _.transferFrom(address,address,uint256) external => DISPATCHER(true); + + // pool + // ---- + function _SymbolicLendingPool.getReserveNormalizedIncome(address) external returns (uint256) envfree; + function _SymbolicLendingPool.getReserveData(address) external returns (DataTypes.ReserveData) => CONSTANT; + + // rewards controller + // ------------------ + // In RewardsDistributor.sol called by RewardsController.sol + function _.getAssetIndex(address, address) external=> DISPATCHER(true); + // In ScaledBalanceTokenBase.sol called by getAssetIndex + function _.scaledTotalSupply() external => DISPATCHER(true); + // Called by RewardsController._transferRewards() + // Defined in TransferStrategyHarness as simple transfer() + function _.performTransfer(address,address,uint256) external => DISPATCHER(true); + + // harness methods of the rewards controller + function _RewardsController.getRewardsIndex(address,address) external returns (uint256) envfree; + function _RewardsController.getAvailableRewardsCount(address) external returns (uint128) envfree; + function _RewardsController.getRewardsByAsset(address, uint128) external returns (address) envfree; + function _RewardsController.getAssetListLength() external returns (uint256) envfree; + function _RewardsController.getAssetByIndex(uint256) external returns (address) envfree; + function _RewardsController.getDistributionEnd(address, address) external returns (uint256) envfree; + function _RewardsController.getUserAccruedRewards(address, address) external returns (uint256) envfree; + function _RewardsController.getUserAccruedReward(address, address, address) external returns (uint256) envfree; + function _RewardsController.getAssetDecimals(address) external returns (uint8) envfree; + function _RewardsController.getRewardsData(address,address) external returns (uint256,uint256,uint256,uint256) envfree; + function _RewardsController.getUserAssetIndex(address,address, address) external returns (uint256) envfree; + + // underlying token + // ---------------- + function _DummyERC20_aTokenUnderlying.balanceOf(address) external returns(uint256) envfree; + + // aToken + // ------ + function _AToken.balanceOf(address) external returns (uint256) envfree; + function _AToken.totalSupply() external returns (uint256) envfree; + function _AToken.allowance(address, address) external returns (uint256) envfree; + function _AToken.UNDERLYING_ASSET_ADDRESS() external returns (address) envfree; + function _AToken.scaledBalanceOf(address) external returns (uint256) envfree; + function _AToken.scaledTotalSupply() external returns (uint256) envfree; + + // called in aToken + function _.finalizeTransfer(address, address, address, uint256, uint256, uint256) external => NONDET; + // Called by rewardscontroller.sol + // Defined in scaledbalancetokenbase.sol + function _.getScaledUserBalanceAndSupply(address) external => DISPATCHER(true); + + // reward token + // ------------ + function _DummyERC20_rewardToken.balanceOf(address) external returns (uint256) envfree; + function _DummyERC20_rewardToken.totalSupply() external returns (uint256) envfree; + + function _.UNDERLYING_ASSET_ADDRESS() external => CONSTANT UNRESOLVED; +} + +///////////////// DEFINITIONS ////////////////////// + + definition RAY() returns uint256 = 10^27; + + /// @notice Claim rewards methods + definition claimFunctions(method f) returns bool = + (f.selector == sig:claimRewardsToSelf(address[]).selector || + f.selector == sig:claimRewards(address, address[]).selector || + f.selector == sig:claimRewardsOnBehalf(address, address,address[]).selector); + + definition collectAndUpdateFunction(method f) returns bool = + f.selector == sig:collectAndUpdateRewards(address).selector; + + definition harnessOnlyMethods(method f) returns bool = + (harnessMethodsMinusHarnessClaimMethods(f) || + f.selector == sig:claimSingleRewardOnBehalf(address, address, address).selector || + f.selector == sig:claimDoubleRewardOnBehalfSame(address, address, address).selector); + + definition harnessMethodsMinusHarnessClaimMethods(method f) returns bool = + (f.selector == sig:getStaticATokenUnderlying().selector || + f.selector == sig:getRewardTokensLength().selector || + f.selector == sig:getRewardToken(uint256).selector || + f.selector == sig:getRewardsIndexOnLastInteraction(address, address).selector || + f.selector == sig:getUserRewardsData(address, address).selector || + f.selector == sig:_mintWrapper(address, uint256).selector); + +////////////////// FUNCTIONS ////////////////////// + + /** + * @title Single reward setup + * Setup the `StaticATokenLM`'s rewards so they contain a single reward token + * which is` _DummyERC20_rewardToken`. + */ + function single_RewardToken_setup() { + require getRewardTokensLength() == 1; + require getRewardToken(0) == _DummyERC20_rewardToken; + } + + /** + * @title Single reward setup in RewardsController + * Sets (in `_RewardsController`) the first reward for `_AToken` as + * `_DummyERC20_rewardToken`. + */ + function rewardsController_reward_setup() { + require _RewardsController.getAvailableRewardsCount(_AToken) > 0; + require _RewardsController.getRewardsByAsset(_AToken, 0) == _DummyERC20_rewardToken; + } + + /// @title Assumptions that should hold in any run + /// @dev Assume that RewardsController.configureAssets(RewardsDataTypes.RewardsConfigInput[] memory rewardsInput) was called + function setup(env e, address user) { + require getRewardTokensLength() > 0; + require _RewardsController.getAvailableRewardsCount(_AToken) > 0; + require _RewardsController.getRewardsByAsset(_AToken, 0) == _DummyERC20_rewardToken; + require currentContract != e.msg.sender; + require currentContract != user; + + require _AToken != user; + require _RewardsController != user; + require _DummyERC20_aTokenUnderlying != user; + require _DummyERC20_rewardToken != user; + require _SymbolicLendingPool != user; + require _TransferStrategy != user; + require _TransferStrategy != user; + } diff --git a/certora/stata/specs/methods/methods_multi_reward.spec b/certora/stata/specs/methods/methods_multi_reward.spec new file mode 100644 index 00000000..5bea0e34 --- /dev/null +++ b/certora/stata/specs/methods/methods_multi_reward.spec @@ -0,0 +1,75 @@ +import "erc20.spec"; + +using SymbolicLendingPool as _SymbolicLendingPool; +using RewardsControllerHarness as _RewardsController; +using DummyERC20_aTokenUnderlying as _DummyERC20_aTokenUnderlying; +using ATokenInstance as _AToken; +using DummyERC20_rewardToken as _DummyERC20_rewardToken; + +/////////////////// Methods //////////////////////// + +/// @dev Using mostly `NONDET` in the methods block, to speed up verification. + +methods { + // static aToken + // ------------- + function _.getCurrentRewardsIndex(address reward) external => CONSTANT; + function getUnclaimedRewards(address, address) external returns (uint256) envfree; + function rewardTokens() external returns (address[]) envfree; + function isRegisteredRewardToken(address) external returns (bool) envfree; + + // static aToken harness + // --------------------- + function getRewardTokensLength() external returns (uint256) envfree; + function getRewardToken(uint256) external returns (address) envfree; + + // pool + // ---- + // In RewardsDistributor.sol called by RewardsController.sol + function _.getAssetIndex(address, address) external => NONDET; + + // In RewardsDistributor.sol called by RewardsController.sol + function _.finalizeTransfer(address, address, address, uint256, uint256, uint256) external => NONDET; + + // In ScaledBalanceTokenBase.sol called by getAssetIndex + function _.scaledTotalSupply() external => NONDET; + + // rewards controller + // ------------------ + function _RewardsController.getAvailableRewardsCount(address) external returns (uint128) envfree; + function _RewardsController.getRewardsByAsset(address, uint128) external returns (address) envfree; + // Called by IncentivizedERC20.sol and by StaticATokenLM.sol + function _.handleAction(address,uint256,uint256) external => NONDET; + // Called by rewardscontroller.sol + // Defined in scaledbalancetokenbase.sol + function _.getScaledUserBalanceAndSupply(address) external => NONDET; + // Called by RewardsController._transferRewards() + // Defined in TransferStrategyHarness as simple transfer() + function _.performTransfer(address,address,uint256) external => NONDET; + + // aToken + // ------ + function _AToken.UNDERLYING_ASSET_ADDRESS() external returns (address) envfree; + function _.mint(address,address,uint256,uint256) external => NONDET; + function _.burn(address,address,uint256,uint256) external => NONDET; + + // reward token + // ------------ + function _DummyERC20_rewardToken.balanceOf(address) external returns (uint256) envfree; + + function _.permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external => NONDET; +} + +///////////////// Definition /////////////////////// + + /// @title Set up a single reward token + function single_RewardToken_setup() { + require isRegisteredRewardToken(_DummyERC20_rewardToken); + require getRewardTokensLength() == 1; + } + + /// @title Set up a single reward token for `_AToken` in the `INCENTIVES_CONTROLLER` + function rewardsController_arbitrary_single_reward_setup() { + require _RewardsController.getAvailableRewardsCount(_AToken) == 1; + require _RewardsController.getRewardsByAsset(_AToken, 0) == _DummyERC20_rewardToken; + } diff --git a/certora/stata/specs/staticATokenLM/StaticATokenLM.spec b/certora/stata/specs/staticATokenLM/StaticATokenLM.spec new file mode 100644 index 00000000..49dbd95e --- /dev/null +++ b/certora/stata/specs/staticATokenLM/StaticATokenLM.spec @@ -0,0 +1,876 @@ +import "../methods/methods_base.spec"; + +/////////////////// Methods //////////////////////// + +methods { + function _.permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external => NONDET; + function _.getIncentivesController() external => CONSTANT; + function _.getRewardsList() external => NONDET; + //call by RewardsController.IncentivizedERC20.sol and also by StaticATokenLM.sol + function _.handleAction(address,uint256,uint256) external => DISPATCHER(true); + + function balanceOf(address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; +} + +////////////////// FUNCTIONS ////////////////////// + + /// @title Reward hook + /// @notice allows a single reward + //todo: allow 2 or 3 rewards + hook Sload address reward _rewardTokens[INDEX uint256 i] { + require reward == _DummyERC20_rewardToken; + } + + /// @title Sum of balances of StaticAToken + ghost sumAllBalance() returns mathint { + init_state axiom sumAllBalance() == 0; + } + + hook Sstore balanceOf[KEY address a] uint256 balance (uint256 old_balance) { + havoc sumAllBalance assuming sumAllBalance@new() == sumAllBalance@old() + balance - old_balance; + } + +///////////////// Properties /////////////////////// + + /** + * @title Rewards claiming when sufficient rewards exist + * Ensures rewards are updated correctly after claiming, when there are enough + * reward funds. + * + * @dev Passed in job-id=`655ba8737ada43efab71eaabf8d41096` + */ + rule rewardsConsistencyWhenSufficientRewardsExist() { + // Assuming single reward + single_RewardToken_setup(); + + // Create a rewards array + address[] _rewards; + require _rewards[0] == _DummyERC20_rewardToken; + require _rewards.length == 1; + + env e; + require e.msg.sender != currentContract; // Cannot claim to contract + uint256 rewardsBalancePre = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + uint256 claimablePre = getClaimableRewards(e, e.msg.sender, _DummyERC20_rewardToken); + + // Ensure contract has sufficient rewards + require _DummyERC20_rewardToken.balanceOf(currentContract) >= claimablePre; + + claimRewardsToSelf(e, _rewards); + + uint256 rewardsBalancePost = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + uint256 unclaimedPost = getUnclaimedRewards(e.msg.sender, _DummyERC20_rewardToken); + uint256 claimablePost = getClaimableRewards(e, e.msg.sender, _DummyERC20_rewardToken); + + assert rewardsBalancePost >= rewardsBalancePre, "Rewards balance reduced after claim"; + mathint rewardsGiven = rewardsBalancePost - rewardsBalancePre; + assert to_mathint(claimablePre) == rewardsGiven + unclaimedPost, "Rewards given unequal to claimable"; + assert claimablePost == unclaimedPost, "Claimable different from unclaimed"; + assert unclaimedPost == 0; // Left last as this is an implementation detail + } + + /** + * @title Rewards claiming when rewards are insufficient + /* Ensures rewards are updated correctly after claiming, when there aren't + * enough funds. + * + * @dev Failed in previous version of the code: job-id=`274946aa85a247149c025df228c71bc1`. + * Failure reported in: `https://github.com/bgd-labs/static-a-token-v3/issues/23`. + * Passed after fix with rule-sanity in job-id=`32b981560c2c41eab24606daa7d38694`. + */ + rule rewardsConsistencyWhenInsufficientRewards() { + // Assuming single reward + single_RewardToken_setup(); + + env e; + require e.msg.sender != currentContract; // Cannot claim to contract + require e.msg.sender != _TransferStrategy; + + uint256 rewardsBalancePre = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + uint256 claimablePre = getClaimableRewards(e, e.msg.sender, _DummyERC20_rewardToken); + + // Ensure contract does not have sufficient rewards + require _DummyERC20_rewardToken.balanceOf(currentContract) < claimablePre; + + claimSingleRewardOnBehalf(e, e.msg.sender, e.msg.sender, _DummyERC20_rewardToken); + + uint256 rewardsBalancePost = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + uint256 unclaimedPost = getUnclaimedRewards(e.msg.sender, _DummyERC20_rewardToken); + uint256 claimablePost = getClaimableRewards(e, e.msg.sender, _DummyERC20_rewardToken); + + assert rewardsBalancePost >= rewardsBalancePre, "Rewards balance reduced after claim"; + mathint rewardsGiven = rewardsBalancePost - rewardsBalancePre; + // Note, when `rewardsGiven` is 0 the unclaimed rewards are not updated + assert ( + ( (rewardsGiven > 0) => (to_mathint(claimablePre) == rewardsGiven + unclaimedPost) ) && + ( (rewardsGiven == 0) => (claimablePre == claimablePost) ) + ), "Claimable rewards changed unexpectedly"; + } + + + /** + * @title Only claiming rewards should reduce contract's total rewards balance + * Only "claim reward" methods should cause the total rewards balance of + * `StaticATokenLM` to decline. Note that `initialize`, `metaDeposit` + * and `metaWithdraw` are filtered out. To avoid timeouts the rest of the + * methods were split between several versions of this rule. + * + * WARNING: `metaDeposit` seems to be vacuous, i.e. **always** fails on a + * require statement. + * + * @dev Passed with rule-sanity in job-id=`98beb842d5b94278ac4a9222249fb564` + * + */ + rule rewardsTotalDeclinesOnlyByClaim(method f) filtered { + // Filter out initialize + f -> ( + f.contract == currentContract && + !harnessOnlyMethods(f) && + f.selector != sig:initialize(address, string, string).selector) && + // Exclude meta functions + (f.selector != sig:metaDeposit( + address,address,uint256,uint16,bool,uint256, + IStaticATokenLM.PermitParams calldata,IStaticATokenLM.SignatureParams calldata).selector) && + (f.selector != sig:metaWithdraw( + address,address,uint256,uint256,bool,uint256,IStaticATokenLM.SignatureParams calldata + ).selector) && + // Exclude methods that time out + (f.selector != sig:deposit(uint256,address).selector) && + (f.selector != sig:deposit(uint256,address,uint16,bool).selector) && + (f.selector != sig:redeem(uint256,address,address).selector) && + (f.selector != sig:redeem(uint256,address,address,bool).selector) && + (f.selector != sig:mint(uint256,address).selector) + } { + // Assuming single reward + single_RewardToken_setup(); + rewardsController_reward_setup(); + + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + + env e; + require e.msg.sender != currentContract; + uint256 preTotal = getTotalClaimableRewards(e, _DummyERC20_rewardToken); + + calldataarg args; + f(e, args); + + uint256 postTotal = getTotalClaimableRewards(e, _DummyERC20_rewardToken); + + assert (postTotal < preTotal) => ( + (f.selector == sig:claimRewardsOnBehalf(address, address, address[]).selector) || + (f.selector == sig:claimRewards(address, address[]).selector) || + (f.selector == sig:claimRewardsToSelf(address[]).selector) || + (f.selector == sig:claimSingleRewardOnBehalf(address,address,address).selector) + ), "Total rewards decline not due to claim"; + } + + /// @dev Passed with rule-sanity in job-id=`f71cabe338614768af9e119dea55b00e` + rule rewardsTotalDeclinesOnlyByClaim_timedout_methods(method f) filtered { + // Include only the timed out methods, excluding redeem + f -> (f.selector == sig:deposit(uint256,address).selector) || + (f.selector == sig:deposit(uint256,address,uint16,bool).selector) || + (f.selector == sig:mint(uint256,address).selector) + } { + // Assuming single reward + single_RewardToken_setup(); + rewardsController_reward_setup(); + + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + + env e; + require e.msg.sender != currentContract; + uint256 preTotal = getTotalClaimableRewards(e, _DummyERC20_rewardToken); + + calldataarg args; + f(e, args); + + uint256 postTotal = getTotalClaimableRewards(e, _DummyERC20_rewardToken); + + assert (postTotal < preTotal) => ( + (f.selector == sig:claimRewardsOnBehalf(address, address, address[]).selector) || + (f.selector == sig:claimRewards(address, address[]).selector) || + (f.selector == sig:claimRewardsToSelf(address[]).selector) || + (f.selector == sig:claimSingleRewardOnBehalf(address,address,address).selector) + ), "Total rewards decline not due to claim"; + } + + /** + * @dev Passed in job-id=`06a3d30b577b4a8a8d26182e7486b065` + * using `--settings -t=7200,-mediumTimeout=40,-depth=7` + */ + rule rewardsTotalDeclinesOnlyByClaim_redeem_methods(method f) filtered { + // Include only the redeem timed out methods + f -> (f.selector == sig:redeem(uint256,address,address).selector) || + (f.selector == sig:redeem(uint256,address,address,bool).selector) + } { + // Assuming single reward + single_RewardToken_setup(); + rewardsController_reward_setup(); + + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + + env e; + require e.msg.sender != currentContract; + uint256 preTotal = getTotalClaimableRewards(e, _DummyERC20_rewardToken); + + calldataarg args; + f(e, args); + + uint256 postTotal = getTotalClaimableRewards(e, _DummyERC20_rewardToken); + + assert (postTotal < preTotal) => ( + (f.selector == sig:claimRewardsOnBehalf(address, address, address[]).selector) || + (f.selector == sig:claimRewards(address, address[]).selector) || + (f.selector == sig:claimRewardsToSelf(address[]).selector) || + (f.selector == sig:claimSingleRewardOnBehalf(address,address,address).selector) + ), "Total rewards decline not due to claim"; + } + + //fail. todo: check if property should hold + //https://vaas-stg.certora.com/output/99352/5521be2ec21640feb23be9d8b1faa08a/?anonymousKey=e2a56ad93292b812fb66afa29a0ae8fcf53b4f37 + //https://vaas-stg.certora.com/output/99352/c288ca4de50e4f7ab76bfa70fac1c7ff/?anonymousKey=9cf2d1fb28a3b4f47b952eae91f3d330ea346181 + // invariant solvency_user_balance_leq_total_asset_CASE_SPLIT_redeem_in_shares_4(address user) + // balanceOf(user) <= _AToken.scaledBalanceOf(currentContract) + // filtered { f -> f.selector == sig:redeem(uint256,address,address,bool).selector} + // { + // preserved redeem(uint256 shares, address receiver, address owner, bool toUnderlying) with (env e1) { + // requireInvariant solvency_total_asset_geq_total_supply(); + // require balanceOf(owner) <= totalSupply(); //todo: replace with requireInvariant + // require receiver != _AToken; + // require user != _SymbolicLendingPool; // TODO: review !!! + // } + // } + + + //pass -t=1400,-mediumTimeout=800,-depth=10 + /// @notice Total supply is non-zero only if total assets is non-zero +invariant solvency_positive_total_supply_only_if_positive_asset() + ((_AToken.scaledBalanceOf(currentContract) == 0) => (totalSupply() == 0)) + filtered { f -> + f.contract == currentContract && + f.selector != sig:metaWithdraw(address,address,uint256,uint256,bool,uint256,IStaticATokenLM.SignatureParams).selector + && !harnessMethodsMinusHarnessClaimMethods(f) + && !claimFunctions(f) + && f.selector != sig:claimDoubleRewardOnBehalfSame(address, address, address).selector + } + { + preserved redeem(uint256 shares, address receiver, address owner, bool toUnderlying) with (env e1) { + requireInvariant solvency_total_asset_geq_total_supply(); + require balanceOf(owner) <= totalSupply(); //todo: replace with requireInvariant + } + preserved redeem(uint256 shares, address receiver, address owner) with (env e2) { + requireInvariant solvency_total_asset_geq_total_supply(); + require balanceOf(owner) <= totalSupply(); + } + preserved withdraw(uint256 assets, address receiver, address owner) with (env e3) { + requireInvariant solvency_total_asset_geq_total_supply(); + require balanceOf(owner) <= totalSupply(); + } + + } + + + + //fail on deposit if e1.msg.sender == currentContract + //https://vaas-stg.certora.com/output/99352/83c1362989b540658dd72714c68f4f6a/?anonymousKey=00b5efbeb76fc09cbb12b5c0a53248703a16f5fe + //https://vaas-stg.certora.com/output/99352/a929ada034a5437ca001dd11b221038b/?anonymousKey=a90c16f056686fdd38110f16f6ec8f72a8d2062b + + //pass with -t=1400,-mediumTimeout=800,-depth=15 + //https://vaas-stg.certora.com/output/99352/7252b6b75144419c825fb00f1f11acc8/?anonymousKey=8cb67238d3cb2a14c8fbad5c1c8554b00221de95 + //pass with -t=1400,-mediumTimeout=800,-depth=10 + + /// @nitce Total asseta is greater than or equal to total supply. +invariant solvency_total_asset_geq_total_supply() + (_AToken.scaledBalanceOf(currentContract) >= totalSupply()) + filtered { f -> + f.contract == currentContract && + f.selector != sig:metaWithdraw(address,address,uint256,uint256,bool,uint256,IStaticATokenLM.SignatureParams calldata).selector + && f.selector != sig:redeem(uint256,address,address).selector + && f.selector != sig:redeem(uint256,address,address,bool).selector + && !harnessMethodsMinusHarnessClaimMethods(f) + && !claimFunctions(f) + && f.selector != sig:claimDoubleRewardOnBehalfSame(address, address, address).selector } + { + preserved withdraw(uint256 assets, address receiver, address owner) with (env e3) { + require balanceOf(owner) <= totalSupply(); + } + preserved deposit(uint256 assets, address receiver) with (env e4) { + require balanceOf(receiver) <= totalSupply(); //todo: replace with requireInvariant + require e4.msg.sender != currentContract; //todo: review + } + preserved deposit(uint256 assets, address receiver,uint16 referralCode, bool fromUnderlying) with (env e5) { + require balanceOf(receiver) <= totalSupply(); //todo: replace with requireInvariant + require e5.msg.sender != currentContract; //todo: review + } + preserved mint(uint256 shares, address receiver) with (env e6) { + require balanceOf(receiver) <= totalSupply(); //todo: replace with requireInvariant + require e6.msg.sender != currentContract; //todo: review + } + + } + + //timeout + //https://vaas-stg.certora.com/output/99352/cf6f23d546ed4834ae27bc4de2df81d7/?anonymousKey=a0ab74898224e42db0ef4770909848880d61abaa + //timeout with -t=1200,-mediumTimeout=800,-depth=10 + invariant solvency_total_asset_geq_total_supply_CASE_SPLIT_redeem() + (_AToken.scaledBalanceOf(currentContract) >= totalSupply()) + filtered { f -> f.selector == sig:redeem(uint256,address,address).selector} + { + preserved redeem(uint256 shares, address receiver, address owner) with (env e2) { + require balanceOf(owner) <= totalSupply(); + } + } + + //pass + /// @title correct accrued value is fetched + /// @notice assume a single asset + //pass with rule_sanity basic except metaDeposit() + //https://vaas-stg.certora.com/output/99352/ab6c92a9f96d4327b52da331d634d3ab/?anonymousKey=abb27f614a8656e6e300ce21c517009cbe0c4d3a + //https://vaas-stg.certora.com/output/99352/d8c9a8bbea114d5caad43683b06d8ba0/?anonymousKey=a079d7f7dd44c47c05c866808c32235d56bca8e8 +invariant singleAssetAccruedRewards(env e0, address _asset, address reward, address user) + ((_RewardsController.getAssetListLength() == 1 && _RewardsController.getAssetByIndex(0) == _asset) + => (_RewardsController.getUserAccruedReward(_asset, reward, user) == _RewardsController.getUserAccruedRewards(reward, user))) + filtered {f -> + f.contract == currentContract && + !harnessOnlyMethods(f) + } { + preserved with (env e1){ + setup(e1, user); + require _asset != _RewardsController; + require _asset != _TransferStrategy; + require reward != _StaticATokenLM; + require reward != _AToken; + require reward != _TransferStrategy; + } +} + + + + //pass with --rule_sanity basic + //https://vaas-stg.certora.com/output/99352/4df615c845e2445b8657ece2db477ce5/?anonymousKey=76379915d60fc1056ed4e5b391c69cd5bba3cce0 + /// @title Claiming rewards should not affect totalAssets() + rule totalAssets_stable(method f) + filtered { f -> f.selector == sig:claimSingleRewardOnBehalf(address, address, address).selector + || f.selector == sig:collectAndUpdateRewards(address).selector } + { + env e; + calldataarg args; + mathint totalAssetBefore = totalAssets(); + f(e, args); + mathint totalAssetAfter = totalAssets(); + assert totalAssetAfter == totalAssetBefore; + } + + //fail + //https://vaas-stg.certora.com/output/99352/2104ed63c44845c2a8a793007224cb2a/?anonymousKey=f2e12ee6154f8b707b21fb62d1cc12a46a6c03b1 + rule totalAssets_stable_after_collectAndUpdateRewards() + { + env e; + address reward; + mathint totalAssetBefore = totalAssets(); + collectAndUpdateRewards(e, reward); + mathint totalAssetAfter = totalAssets(); + assert totalAssetAfter == totalAssetBefore; + } + + + //pass + //https://vaas-stg.certora.com/output/99352/7d2ce2bb69ad4d71b4a179daa08633e4/?anonymousKey=7446e8a015ea9aa79cbc542c10b932e04169a0ab + /// @title Receiving ATokens does not affect the amount of rewards fetched by collectAndUpdateRewards() + rule reward_balance_stable_after_collectAndUpdateRewards() + { + uint256 totalAccrued = _RewardsController.getUserAccruedRewards(_AToken, currentContract); + require (totalAccrued == 0); + + env e; + address reward; + + mathint totalAssetBefore = totalAssets(); + + collectAndUpdateRewards(e, reward); + mathint totalAssetAfter = totalAssets(); + + assert totalAssetAfter == totalAssetBefore; + } + + // //timeout + // /// @title getTotalClaimableRewards() is stable unless rewards were claimed + // rule totalClaimableRewards_stable(method f) + // filtered { f -> !f.isView && !claimFunctions(f) && f.selector != sig:initialize(address,string,string).selector } + // { + // env e; + // require e.msg.sender != currentContract; + // setup(e, 0); + // calldataarg args; + // address reward; + // require e.msg.sender != reward ; + // require currentContract != e.msg.sender; + // require _AToken != e.msg.sender; + // require _RewardsController != e.msg.sender; + // require _DummyERC20_aTokenUnderlying != e.msg.sender; + // require _DummyERC20_rewardToken != e.msg.sender; + // require _SymbolicLendingPool != e.msg.sender; + // require _TransferStrategy != e.msg.sender; + + // require currentContract != reward; + // require _AToken != reward; + // require _RewardsController != reward; + // require _DummyERC20_aTokenUnderlying != reward; + // require _SymbolicLendingPool != reward; + // require _TransferStrategy != reward; + // require _TransferStrategy != reward; + + + // mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward); + // f(e, args); + // mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward); + // assert totalClaimableRewardsAfter == totalClaimableRewardsBefore; + // } + + //pass with -t=1400,-mediumTimeout=800,-depth=10 + rule totalClaimableRewards_stable_CASE_SPLIT(method f) + filtered { f -> !f.isView && !claimFunctions(f) + && !collectAndUpdateFunction(f) + && f.selector != sig:initialize(address,string,string).selector + && f.selector != sig:redeem(uint256,address,address,bool).selector + && f.selector != sig:redeem(uint256,address,address).selector + && f.selector != sig:withdraw(uint256,address,address).selector + && f.selector != sig:deposit(uint256,address).selector + && f.selector != sig:mint(uint256,address).selector + && f.selector != sig:metaWithdraw(address,address,uint256,uint256,bool,uint256,IStaticATokenLM.SignatureParams calldata).selector + && f.selector != sig:claimSingleRewardOnBehalf(address,address,address).selector + } + { + require _RewardsController.getAssetByIndex(0) != _RewardsController; + require _RewardsController.getAssetListLength() > 0; + + uint256 totalAccrued = _RewardsController.getUserAccruedRewards(_AToken, currentContract); + require (totalAccrued == 0); + + + + env e; + address reward; + + mathint totalAssetBefore = totalAssets(); + + collectAndUpdateRewards(e, reward); + mathint totalAssetAfter = totalAssets(); + + assert totalAssetAfter == totalAssetBefore; + } + + + //timeout -t=1400,-mediumTimeout=800,-depth=10 =10 + //pass with -t=1200,-mediumTimeout=1200,-depth=10 + // 16 minutes + //https://vaas-stg.certora.com/output/99352/12829795cff241098f304ce49f73051e/?anonymousKey=739f53463e398ed7d5b2eec101f254b6095e0841 + // 40 minutes + //https://vaas-stg.certora.com/output/99352/5a29622bc18c438ba016a27162a82c84/?anonymousKey=130051cfba518c2cdf7f0e86ecc71ea05d98367b + rule totalClaimableRewards_stable_CASE_SPLIT_redeem() + { + env e; + require e.msg.sender != currentContract; + setup(e, 0); + address reward; + require e.msg.sender != reward; + require currentContract != e.msg.sender; + require _AToken != e.msg.sender; + require _RewardsController != e.msg.sender; + require _DummyERC20_aTokenUnderlying != e.msg.sender; + require _DummyERC20_rewardToken != e.msg.sender; + require _SymbolicLendingPool != e.msg.sender; + require _TransferStrategy != e.msg.sender; + + require currentContract != reward; + require _AToken != reward; + require _RewardsController != reward; + require _DummyERC20_aTokenUnderlying != reward; + require _SymbolicLendingPool != reward; + require _TransferStrategy != reward; + require _TransferStrategy != reward; + + //todo: run with different settings + mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward); + uint256 shares; + address receiver; + address owner; + redeem(e, shares, receiver, owner); + mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward); + assert totalClaimableRewardsAfter == totalClaimableRewardsBefore; + } + + //timeout with -t=1000,-mediumTimeout=100,-depth=10 + //timeout no SMT run: -t=1200,-mediumTimeout=1000,-depth=6 -t=1200,-mediumTimeout=1200,-depth=10 + rule totalClaimableRewards_stable_CASE_SPLIT_deposit() + { + env e; + require e.msg.sender != currentContract; + setup(e, 0); + address reward; + require e.msg.sender != reward; + require currentContract != e.msg.sender; + require _AToken != e.msg.sender; + require _RewardsController != e.msg.sender; + require _DummyERC20_aTokenUnderlying != e.msg.sender; + require _DummyERC20_rewardToken != e.msg.sender; + require _SymbolicLendingPool != e.msg.sender; + require _TransferStrategy != e.msg.sender; + + require currentContract != reward; + require _AToken != reward; + require _RewardsController != reward; + require _DummyERC20_aTokenUnderlying != reward; + require _SymbolicLendingPool != reward; + require _TransferStrategy != reward; + require _TransferStrategy != reward; + + + mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward); + uint256 assets; + address receiver; + deposit(e, assets, receiver); + mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward); + assert totalClaimableRewardsAfter == totalClaimableRewardsBefore; + } + + // //timeout + // rule totalClaimableRewards_stable_less_requires_6(method f) + // filtered { f -> !f.isView && !claimFunctions(f) && f.selector != sig:initialize(address,string,string).selector } + // { + // env e; + // require e.msg.sender != currentContract; + // setup(e, 0); + // calldataarg args; + // address reward; + // require _DummyERC20_aTokenUnderlying != reward; + // require e.msg.sender != reward; + // require currentContract != e.msg.sender; + // require _RewardsController != e.msg.sender; + + // require currentContract != reward; + // require _DummyERC20_aTokenUnderlying != reward; + + + // mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward); + // f(e, args); + // mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward); + // assert totalClaimableRewardsAfter == totalClaimableRewardsBefore; + // } + + // //pass with -t=1400,-mediumTimeout=800,-depth=10 + // //https://vaas-stg.certora.com/output/99352/34ccc167c8d84d1985e3b0f75a5d41a6/?anonymousKey=e6f31abf1c7bb0cb66702a218b84b2830fde8928 + // rule totalClaimableRewards_stable_less_requires_7(method f) + // filtered { f -> !f.isView && !claimFunctions(f) + // && f.selector != sig:initialize(address,string,string).selector + // && f.selector != sig:redeem(uint256,address,address,bool).selector + // && f.selector != sig:redeem(uint256,address,address).selector + // && f.selector != sig:withdraw(uint256,address,address).selector + // && f.selector != sig:deposit(uint256,address).selector + // && f.selector != sig:mint(uint256,address).selector + // && f.selector != metaWithdraw(address,address,uint256,uint256,bool,uint256,(uint8,bytes32,bytes32)).selector + // && f.selector !=sig:claimSingleRewardOnBehalf(address,address,address).selector + // } + // { + // env e; + // require e.msg.sender != currentContract; + // setup(e, 0); + // calldataarg args; + // address reward; + // require _DummyERC20_aTokenUnderlying != reward; + // require _AToken != reward; + // require e.msg.sender != reward; + // require _AToken != e.msg.sender; + // require _RewardsController != e.msg.sender; + + // require currentContract != reward; + + // mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward); + // f(e, args); + // mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward); + // assert totalClaimableRewardsAfter == totalClaimableRewardsBefore; + // } + + + // //timeout + // //https://vaas-stg.certora.com/output/99352/e755cdb34d84406ab17a782c4ffd6954/?anonymousKey=2efcab1e1dd4ea504c315b148b42ef3cec8acaa7 + // rule totalClaimableRewards_stable_less_requires_7_CASE_SPLIT_redeem() + // { + // env e; + // require e.msg.sender != currentContract; + // setup(e, 0); + // address reward; + // require _DummyERC20_aTokenUnderlying != reward; + // require _AToken != reward; + // require e.msg.sender != reward; + // require _AToken != e.msg.sender; + // require _RewardsController != e.msg.sender; + + // require currentContract != reward; + + // mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward); + // uint256 shares; + // address receiver; + // address owner; + // redeem(e, shares, receiver, owner); + // mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward); + // assert totalClaimableRewardsAfter == totalClaimableRewardsBefore; + // } + + + // //timeout + // //https://vaas-stg.certora.com/output/99352/bee8d3a583c549e195c0f755bb804b34/?anonymousKey=4b9e6f6791ede0049659d54a07db5e0f146b4a42 + // rule totalClaimableRewards_stable_less_requires_7_CASE_SPLIT_deposit() + // { + // env e; + // require e.msg.sender != currentContract; + // setup(e, 0); + // address reward; + // require _DummyERC20_aTokenUnderlying != reward; + // require _AToken != reward; + // require e.msg.sender != reward; + // require _AToken != e.msg.sender; + // require _RewardsController != e.msg.sender; + + // require currentContract != reward; + + // mathint totalClaimableRewardsBefore = getTotalClaimableRewards(e, reward); + // uint256 assets; + // address receiver; + // deposit(e, assets, receiver); + // mathint totalClaimableRewardsAfter = getTotalClaimableRewards(e, reward); + // assert totalClaimableRewardsAfter == totalClaimableRewardsBefore; + // } + + + //todo: add separate rules for redeem, mint + //pass with rule_sanity basic, except metaDeposit, timeout withdraw(uint256,address,address) + //https://vaas-stg.certora.com/output/99352/ee42e7f2603740de96a8a0aaf7c676ff/?anonymousKey=f7aaa1b8ed030a8f600136ec0b94ae0bc81a0e0c + //pass + //https://vaas-stg.certora.com/output/99352/109a4a815a9a4c3abcee760bf77c5f7d/?anonymousKey=f215580ed8e698028fdedecf096752c7a3e9363c + //timeout + + /// @notice At a given block, getClaimableRewards() is unchanged unless rewards were claimed. + // rule getClaimableRewards_stable(method f) + // filtered { f -> !f.isView + // && !claimFunctions(f) + // && f.selector != sig:initialize(address,string,string).selector + // && f.selector != sig:deposit(uint256,address,uint16,bool).selector + // && f.selector != sig:redeem(uint256,address,address).selector + // && f.selector != sig:redeem(uint256,address,address,bool).selector + // && f.selector != sig:mint(uint256,address).selector + // && f.selector != metaWithdraw(address,address,uint256,uint256,bool,uint256,(uint8,bytes32,bytes32)).selector + // && f.selector !=sig:claimSingleRewardOnBehalf(address,address,address).selector + // } + // { + // env e; + // calldataarg args; + // address user; + // address reward; + + // require user != 0; + + // require currentContract != user; + // require _AToken != user; + // require _RewardsController != user; + // require _DummyERC20_aTokenUnderlying != user; + // require _DummyERC20_rewardToken != user; + // require _SymbolicLendingPool != user; + // require _TransferStrategy != user; + + // require currentContract != reward; + // require _AToken != reward; + // require _RewardsController != reward; // + // require _DummyERC20_aTokenUnderlying != reward; + // require _SymbolicLendingPool != reward; + // require _TransferStrategy != reward; + + // //require isRegisteredRewardToken(reward); //todo: review the assumption + + // mathint claimableRewardsBefore = getClaimableRewards(e, user, reward); + + // require getRewardTokensLength() > 0; + // require getRewardToken(0) == reward; //todo: review + // require _RewardsController.getAvailableRewardsCount(_AToken) > 0; //todo: review + // require _RewardsController.getRewardsByAsset(_AToken, 0) == reward; //todo: review + // f(e, args); + // mathint claimableRewardsAfter = getClaimableRewards(e, user, reward); + // assert claimableRewardsAfter == claimableRewardsBefore; + // } + // //timeout + // //should pass after excluding claimSingleRewardOnBehalf + // rule getClaimableRewards_stable_6(method f) + // filtered { f -> !f.isView + // && !claimFunctions(f) + // && f.selector != sig:initialize(address,string,string).selector + // && f.selector != sig:deposit(uint256,address,uint16,bool).selector + // && f.selector != sig:redeem(uint256,address,address).selector + // && f.selector != sig:redeem(uint256,address,address,bool).selector + // && f.selector != sig:mint(uint256,address).selector + // && f.selector != metaWithdraw(address,address,uint256,uint256,bool,uint256,(uint8,bytes32,bytes32)).selector + // && f.selector !=sig:claimSingleRewardOnBehalf(address,address,address).selector + // } + // { + // env e; + // calldataarg args; + // address user; + // address reward; + + // require user != 0; + + + // mathint claimableRewardsBefore = getClaimableRewards(e, user, reward); + + // require getRewardTokensLength() > 0; + // require getRewardToken(0) == reward; //todo: review + // require _RewardsController.getAvailableRewardsCount(_AToken) > 0; //todo: review + // require _RewardsController.getRewardsByAsset(_AToken, 0) == reward; //todo: review + // f(e, args); + // mathint claimableRewardsAfter = getClaimableRewards(e, user, reward); + // assert claimableRewardsAfter == claimableRewardsBefore; + // } + + //pass with -t=1400,-mediumTimeout=800,-depth=15 + //https://vaas-stg.certora.com/output/99352/a10c05634b4342d6b31f777826444616/?anonymousKey=67bb71ebd716ef5d10be8743ded7b466f699e32c + //pass with -t=1400,-mediumTimeout=800,-depth=10 +rule getClaimableRewards_stable(method f) + filtered { f -> + f.contract == currentContract && + !f.isView + && !claimFunctions(f) + && !collectAndUpdateFunction(f) + && f.selector != sig:initialize(address,string,string).selector + && f.selector != sig:deposit(uint256,address,uint16,bool).selector + && f.selector != sig:redeem(uint256,address,address).selector + && f.selector != sig:redeem(uint256,address,address,bool).selector + && f.selector != sig:mint(uint256,address).selector + && f.selector != sig:metaWithdraw(address,address,uint256,uint256,bool,uint256,IStaticATokenLM.SignatureParams calldata).selector + && !harnessOnlyMethods(f) + } + { + env e; + calldataarg args; + address user; + address reward; + + require user != 0; + + require currentContract != reward; + require _AToken != reward; + require _RewardsController != reward; // + require _DummyERC20_aTokenUnderlying != reward; + require _SymbolicLendingPool != reward; + require _TransferStrategy != reward; + + //require isRegisteredRewardToken(reward); //todo: review the assumption + + mathint claimableRewardsBefore = getClaimableRewards(e, user, reward); + + require getRewardTokensLength() > 0; + require getRewardToken(0) == reward; //todo: review + require _RewardsController.getAvailableRewardsCount(_AToken) > 0; //todo: review + require _RewardsController.getRewardsByAsset(_AToken, 0) == reward; //todo: review + f(e, args); + mathint claimableRewardsAfter = getClaimableRewards(e, user, reward); + assert claimableRewardsAfter == claimableRewardsBefore; + } + + //pass with -t=1400,-mediumTimeout=800,-depth=10 + rule getClaimableRewards_stable_after_redeem() + { + env e; + address user; + address reward; + + require user != 0; + + require currentContract != reward; + require _AToken != reward; + require _RewardsController != reward; // + require _DummyERC20_aTokenUnderlying != reward; + require _SymbolicLendingPool != reward; + require _TransferStrategy != reward; + + //require isRegisteredRewardToken(reward); //todo: review the assumption + + mathint claimableRewardsBefore = getClaimableRewards(e, user, reward); + + require getRewardTokensLength() > 0; + require getRewardToken(0) == reward; //todo: review + require _RewardsController.getAvailableRewardsCount(_AToken) > 0; //todo: review + require _RewardsController.getRewardsByAsset(_AToken, 0) == reward; //todo: review + uint256 shares; + address receiver; + address owner; + bool toUnderlying; + + redeem(e, shares, receiver, owner, toUnderlying); + + mathint claimableRewardsAfter = getClaimableRewards(e, user, reward); + assert claimableRewardsAfter == claimableRewardsBefore; + } + + + //pass + rule getClaimableRewards_stable_after_deposit() + { + env e; + address user; + address reward; + + uint256 assets; + address recipient; + uint16 referralCode; + bool fromUnderlying; + + require user != 0; + + + mathint claimableRewardsBefore = getClaimableRewards(e, user, reward); + require getRewardTokensLength() > 0; + require getRewardToken(0) == reward; //todo: review + + require _RewardsController.getAvailableRewardsCount(_AToken) > 0; //todo: review + require _RewardsController.getRewardsByAsset(_AToken, 0) == reward; //todo: review + deposit(e, assets, recipient,referralCode,fromUnderlying); + mathint claimableRewardsAfter = getClaimableRewards(e, user, reward); + assert claimableRewardsAfter == claimableRewardsBefore; + } + + + + //todo: remove + //pass with --loop_iter=2 --rule_sanity basic + //https://vaas-stg.certora.com/output/99352/290a1108baa64316ac4f20b5501b4617/?anonymousKey=930379a90af5aa498ec3fed2110a08f5c096efb3 + /// @title getClaimableRewards() is stable unless rewards were claimed + rule getClaimableRewards_stable_after_refreshRewardTokens() + { + env e; + address user; + address reward; + + mathint claimableRewardsBefore = getClaimableRewards(e, user, reward); + refreshRewardTokens(e); + + mathint claimableRewardsAfter = getClaimableRewards(e, user, reward); + assert claimableRewardsAfter == claimableRewardsBefore; + } + + + /// @title The amount of rewards that was actually received by claimRewards() cannot exceed the initial amount of rewards + rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf(method f) + { + env e; + address onBehalfOf; + address receiver; + require receiver != currentContract; + + mathint balanceBefore = _DummyERC20_rewardToken.balanceOf(receiver); + mathint claimableRewardsBefore = getClaimableRewards(e, onBehalfOf, _DummyERC20_rewardToken); + claimSingleRewardOnBehalf(e, onBehalfOf, receiver, _DummyERC20_rewardToken); + mathint balanceAfter = _DummyERC20_rewardToken.balanceOf(receiver); + mathint deltaBalance = balanceAfter - balanceBefore; + + assert deltaBalance <= claimableRewardsBefore; + } diff --git a/certora/stata/specs/staticATokenLM/aTokenProperties.spec b/certora/stata/specs/staticATokenLM/aTokenProperties.spec new file mode 100644 index 00000000..e8ff929a --- /dev/null +++ b/certora/stata/specs/staticATokenLM/aTokenProperties.spec @@ -0,0 +1,370 @@ + +import "../methods/methods_base.spec"; + +/////////////////// Methods //////////////////////// + + methods + { + function _.permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external => NONDET; + } + +////////////////// FUNCTIONS ////////////////////// + + /// @title Sum of scaled balances of AToken + ghost mathint sumAllATokenScaledBalance { + init_state axiom sumAllATokenScaledBalance == 0; + } + + + /// @dev sample struct UserState {uint128 balance; uint128 additionalData; } + hook Sstore _AToken._userState[KEY address a] .(offset 0) uint128 balance (uint128 old_balance) { + sumAllATokenScaledBalance = sumAllATokenScaledBalance + balance - old_balance; + // havoc sumAllATokenScaledBalance() assuming sumAllATokenScaledBalance()@new() == sumAllATokenScaledBalance()@old() + balance - old_balance; + } + + hook Sload uint128 balance _AToken._userState[KEY address a] .(offset 0) { + require to_mathint(balance) <= sumAllATokenScaledBalance; + } + +///////////////// Properties /////////////////////// + + /** + * @title User AToken balance is fixed + * Interaction with `StaticAtokenLM` should not change a user's AToken balance, + * except for the following methods: + * - `withdraw` + * - `deposit` + * - `redeem` + * - `mint` + * - `metaDeposit` + * - `metaWithdraw` + * + * Note. Rewards methods are special cases handled in other rules below. + * + * Rules passed (with rule sanity): job-id=`5fdaf5eeaca249e584c2eef1d66d73c7` + * + * Note. `UNDERLYING_ASSET_ADDRESS()` was unresolved! + */ + rule aTokenBalanceIsFixed(method f) filtered { + // Exclude balance changing methods + f -> (f.selector != sig:deposit(uint256,address).selector) && + (f.selector != sig:deposit(uint256,address,uint16,bool).selector) && + (f.selector != sig:withdraw(uint256,address,address).selector) && + (f.selector != sig:redeem(uint256,address,address).selector) && + (f.selector != sig:redeem(uint256,address,address,bool).selector) && + (f.selector != sig:mint(uint256,address).selector) && + (f.selector != sig:metaDeposit(address,address,uint256,uint16,bool,uint256, + IStaticATokenLM.PermitParams,IStaticATokenLM.SignatureParams).selector) && + (f.selector != sig:metaWithdraw(address,address,uint256,uint256,bool,uint256, + IStaticATokenLM.SignatureParams).selector) && + // Exclude reward related methods - these are handled below + (f.selector != sig:collectAndUpdateRewards(address).selector) && + (f.selector != sig:claimRewardsOnBehalf(address,address,address[]).selector) && + (f.selector != sig:claimSingleRewardOnBehalf(address,address,address).selector) && + (f.selector != sig:claimRewardsToSelf(address[]).selector) && + (f.selector != sig:claimRewards(address,address[]).selector) + } { + require _AToken == asset(); + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + + env e; + + // Limit sender + require e.msg.sender != currentContract; + require e.msg.sender != _AToken; + + uint256 preBalance = _AToken.balanceOf(e.msg.sender); + + calldataarg args; + f(e, args); + + uint256 postBalance = _AToken.balanceOf(e.msg.sender); + assert preBalance == postBalance, "aToken balance changed by static interaction"; + } + + rule aTokenBalanceIsFixed_for_collectAndUpdateRewards() { + require _AToken == asset(); + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + require _AToken != _DummyERC20_rewardToken; + + env e; + + // Limit sender + require e.msg.sender != currentContract; + require e.msg.sender != _AToken; + require e.msg.sender != _DummyERC20_rewardToken; + + uint256 preBalance = _AToken.balanceOf(e.msg.sender); + + collectAndUpdateRewards(e, _DummyERC20_rewardToken); + + uint256 postBalance = _AToken.balanceOf(e.msg.sender); + assert preBalance == postBalance, "aToken balance changed by collectAndUpdateRewards"; + } + + + rule aTokenBalanceIsFixed_for_claimRewardsOnBehalf(address onBehalfOf, address receiver) { + require _AToken == asset(); + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + require _AToken != _DummyERC20_rewardToken; + + // Create a rewards array + address[] _rewards; + require _rewards[0] == _DummyERC20_rewardToken; + require _rewards.length == 1; + + env e; + + // Limit sender + require ( + (e.msg.sender != currentContract) && + (onBehalfOf != currentContract) && + (receiver != currentContract) + ); + require ( + (e.msg.sender != _DummyERC20_rewardToken) && + (onBehalfOf != _DummyERC20_rewardToken) && + (receiver != _DummyERC20_rewardToken) + ); + require (e.msg.sender != _AToken) && (onBehalfOf != _AToken) && (receiver != _AToken); + + uint256 preBalance = _AToken.balanceOf(e.msg.sender); + + claimRewardsOnBehalf(e, onBehalfOf, receiver, _rewards); + + uint256 postBalance = _AToken.balanceOf(e.msg.sender); + assert preBalance == postBalance, "aToken balance changed by claimRewardsOnBehalf"; + } + + + rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf(address onBehalfOf, address receiver) { + require _AToken == asset(); + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + require _AToken != _DummyERC20_rewardToken; + + env e; + + // Limit sender + require ( + (e.msg.sender != currentContract) && + (onBehalfOf != currentContract) && + (receiver != currentContract) + ); + require ( + (e.msg.sender != _DummyERC20_rewardToken) && + (onBehalfOf != _DummyERC20_rewardToken) && + (receiver != _DummyERC20_rewardToken) + ); + require (e.msg.sender != _AToken) && (onBehalfOf != _AToken) && (receiver != _AToken); + + uint256 preBalance = _AToken.balanceOf(e.msg.sender); + + claimSingleRewardOnBehalf(e, onBehalfOf, receiver, _DummyERC20_aTokenUnderlying); + + uint256 postBalance = _AToken.balanceOf(e.msg.sender); + assert preBalance == postBalance, "aToken balance changed by claimSingleRewardOnBehalf"; + } + + + rule aTokenBalanceIsFixed_for_claimRewardsToSelf() { + require _AToken == asset(); + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + require _AToken != _DummyERC20_rewardToken; + + // Create a rewards array + address[] _rewards; + require _rewards[0] == _DummyERC20_rewardToken; + require _rewards.length == 1; + + env e; + + // Limit sender + require e.msg.sender != currentContract; + require e.msg.sender != _AToken; + require e.msg.sender != _DummyERC20_rewardToken; + + uint256 preBalance = _AToken.balanceOf(e.msg.sender); + + claimRewardsToSelf(e, _rewards); + + uint256 postBalance = _AToken.balanceOf(e.msg.sender); + assert preBalance == postBalance, "aToken balance changed by claimRewardsToSelf"; + } + + + rule aTokenBalanceIsFixed_for_claimRewards(address receiver) { + require _AToken == asset(); + require _AToken.UNDERLYING_ASSET_ADDRESS() == _DummyERC20_aTokenUnderlying; + require _AToken != _DummyERC20_rewardToken; + + // Create a rewards array + address[] _rewards; + require _rewards[0] == _DummyERC20_rewardToken; + require _rewards.length == 1; + + env e; + + // Limit sender + require (e.msg.sender != currentContract) && (receiver != currentContract); + require ( + (e.msg.sender != _DummyERC20_rewardToken) && (receiver != _DummyERC20_rewardToken) + ); + require (e.msg.sender != _AToken) && (receiver != _AToken); + + uint256 preBalance = _AToken.balanceOf(e.msg.sender); + + claimRewards(e, receiver, _rewards); + + uint256 postBalance = _AToken.balanceOf(e.msg.sender); + assert preBalance == postBalance, "aToken balance changed by claimRewards"; + } + + /// @title Sum of balances=totalSupply() + //fail without Sload require balance <= sumAllBalance(); + //https://vaas-stg.certora.com/output/99352/1ada6d42ed4c4c03bb85b34d1da92be2/?anonymousKey=d27e10c2ac7220d8571d6374b4618b9e24f1a8a0 + // invariant sumAllBalance_eq_totalSupply() + // sumAllBalance() == totalSupply() + + //fail without Sload require balance <= sumAllBalance(); + //https://vaas-stg.certora.com/output/99352/57f284feabc84b6ca392b781de221e9f/?anonymousKey=3554c35d0a060196775a71fdff3a14a6d2177861 + //todo: add presreved blocks and enable the invariant + // invariant inv_balanceOf_leq_totalSupply(address user) + // balanceOf(user) <= totalSupply() + // { + // preserved { + // requireInvariant sumAllBalance_eq_totalSupply(); + // } + // } + + /// @title AToken balancerOf(user) <= AToken totalSupply() + //timeout on redeem metaWithdraw + //error when running with rule_sanity + //https://vaas-stg.certora.com/output/99352/509a56a1d46348eea0872b3a57c4d15a/?anonymousKey=3e15ac5a5b01e689eb3f71580e3532d8098e71b5 + invariant inv_atoken_balanceOf_leq_totalSupply(address user) + _AToken.balanceOf(user) <= _AToken.totalSupply() + filtered { f -> !f.isView && f.selector != sig:redeem(uint256,address,address,bool).selector && !harnessOnlyMethods(f)} + { + preserved with (env e){ + requireInvariant sumAllATokenScaledBalance_eq_totalSupply(); + } + } + + /// @title AToken balancerOf(user) <= AToken totalSupply() + /// @dev case split of inv_atoken_balanceOf_leq_totalSupply + //pass, times out with rule_sanity basic + invariant inv_atoken_balanceOf_leq_totalSupply_redeem(address user) + _AToken.balanceOf(user) <= _AToken.totalSupply() + filtered { f -> f.selector == sig:redeem(uint256,address,address,bool).selector} + { + preserved with (env e){ + requireInvariant sumAllATokenScaledBalance_eq_totalSupply(); + } + } + + //timeout when running with rule_sanity + //https://vaas-stg.certora.com/output/99352/7840410509f94183bbef864770193ed9/?anonymousKey=b1a13994a4e51f586db837cc284b39c670532f50 + /// @title AToken sum of 2 balancers <= AToken totalSupply() + // invariant inv_atoken_balanceOf_2users_leq_totalSupply(address user1, address user2) + // (_AToken.balanceOf(user1) + _AToken.balanceOf(user2))<= _AToken.totalSupply() + // { + // preserved with (env e1){ + // setup(e1, user1); + // setup(e1, user2); + // } + // preserved redeem(uint256 shares, address receiver, address owner) with (env e2){ + // require user1 != user2; + // require _AToken.balanceOf(currentContract) + _AToken.balanceOf(user1) + _AToken.balanceOf(user2) <= _AToken.totalSupply(); + // } + // preserved redeem(uint256 shares, address receiver, address owner, bool toUnderlying) with (env e3){ + // require user1 != user2; + // requireInvariant sumAllATokenScaledBalance_eq_totalSupply(); + // require _AToken.balanceOf(e3.msg.sender) + _AToken.balanceOf(user1) + _AToken.balanceOf(user2) <= _AToken.totalSupply(); + // require _AToken.balanceOf(currentContract) + _AToken.balanceOf(user1) + _AToken.balanceOf(user2) <= _AToken.totalSupply(); + // } + // preserved withdraw(uint256 assets, address receiver,address owner) with (env e4){ + // require user1 != user2; + // requireInvariant sumAllATokenScaledBalance_eq_totalSupply(); + // require _AToken.balanceOf(e4.msg.sender) + _AToken.balanceOf(user1) + _AToken.balanceOf(user2) <= _AToken.totalSupply(); + // require _AToken.balanceOf(currentContract) + _AToken.balanceOf(user1) + _AToken.balanceOf(user2) <= _AToken.totalSupply(); + // } + + // preserved metaWithdraw(address owner, address recipient,uint256 staticAmount,uint256 dynamicAmount,bool toUnderlying,uint256 deadline,_StaticATokenLM.SignatureParams sigParams) + // with (env e5){ + // require user1 != user2; + // requireInvariant sumAllATokenScaledBalance_eq_totalSupply(); + // require _AToken.balanceOf(e5.msg.sender) + _AToken.balanceOf(user1) + _AToken.balanceOf(user2) <= _AToken.totalSupply(); + // require _AToken.balanceOf(currentContract) + _AToken.balanceOf(user1) + _AToken.balanceOf(user2) <= _AToken.totalSupply(); + // } + + // } + + /// @title Sum of AToken scaled balances = AToken scaled totalSupply() + //pass with rule_sanity basic except metaDeposit() + //https://vaas-stg.certora.com/output/99352/4f91637a96d647baab9accb1093f1690/?anonymousKey=53ccda4a9dd8988205d4b614d9989d1e4148533f + invariant sumAllATokenScaledBalance_eq_totalSupply() + sumAllATokenScaledBalance == to_mathint(_AToken.scaledTotalSupply()) + filtered { f -> !harnessOnlyMethods(f) } + + + /// @title AToken scaledBalancerOf(user) <= AToken scaledTotalSupply() + //pass with rule_sanity basic except metaDeposit() + //https://vaas-stg.certora.com/output/99352/6798b502f97a4cd2b05fce30947911c0/?anonymousKey=c5808a8997a75480edbc45153165c8763488cd1e + invariant inv_atoken_scaled_balanceOf_leq_totalSupply(address user) + _AToken.scaledBalanceOf(user) <= _AToken.scaledTotalSupply() + filtered { f -> !harnessOnlyMethods(f) } + { + preserved { + requireInvariant sumAllATokenScaledBalance_eq_totalSupply(); + } + } + + // //from unregistered_atoken.spec + // // fail + // //todo: remove + // rule claimable_leq_total_claimable() { + // require _RewardsController.getAvailableRewardsCount(_AToken) == 1; + + // require _RewardsController.getRewardsByAsset(_AToken, 0) == _DummyERC20_rewardToken; + + // env e; + // address user; + + // require currentContract != user; + // require _AToken != user; + // require _RewardsController != user; + // require _DummyERC20_aTokenUnderlying != user; + // require _DummyERC20_rewardToken != user; + // require _SymbolicLendingPoolL1 != user; + // require _TransferStrategy != user; + // require _ScaledBalanceToken != user; + // require _TransferStrategy != user; + + // requireInvariant inv_atoken_balanceOf_leq_totalSupply(currentContract); + // requireInvariant inv_atoken_scaled_balanceOf_leq_totalSupply(currentContract); + + + // require getRewardsIndexOnLastInteraction(user, _DummyERC20_rewardToken) == 0; + // require getUnclaimedRewards(e, user, _DummyERC20_rewardToken) == 0; + + // uint256 total = getTotalClaimableRewards(e, _DummyERC20_rewardToken); + // uint256 claimable = getClaimableRewards(e, user, _DummyERC20_rewardToken); + // assert claimable <= total, "Too much claimable"; + // } + + + + + + //The invariant fails, as suspected, with loop_iter=2. + //The invariant is remove. + //requireInvaraint are replaced with require in rules getClaimableRewards_stable* + // invariant registered_reward_exists_in_controller(address reward) + // (isRegisteredRewardToken(reward) => + // (_RewardsController.getAvailableRewardsCount(_AToken) > 0 + // && _RewardsController.getRewardsByAsset(_AToken, 0) == reward)) + // filtered { f -> f.selector != sig:initialize(address,string,string).selector }//Todo: remove filter and use preserved block when CERT-1706 is fixed + // { + // //preserved initialize(address newAToken,string staticATokenName, string staticATokenSymbol) { + // // require newAToken == _AToken; + // // } + // } diff --git a/certora/stata/specs/staticATokenLM/double_claim.spec b/certora/stata/specs/staticATokenLM/double_claim.spec new file mode 100644 index 00000000..e7c120a5 --- /dev/null +++ b/certora/stata/specs/staticATokenLM/double_claim.spec @@ -0,0 +1,65 @@ +import "../methods/methods_multi_reward.spec"; + +///////////////// Properties /////////////////////// + +/// @dev Broke the rule into two cases to speed up verification + + /** + * @title Claiming the same reward twice assuming sufficient rewards + * Using an array with the same reward twice does not give more rewards, + * assuming the contract has sufficient rewards. + * + * @dev Passed in job-id=`54de623f62eb4c95a343ee38834c6d16` + */ + rule prevent_duplicate_reward_claiming_single_reward_sufficient() { + single_RewardToken_setup(); + rewardsController_arbitrary_single_reward_setup(); + + env e; + require e.msg.sender != currentContract; // Cannot claim to contract + + uint256 initialBalance = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + mathint claimable = getClaimableRewards(e, e.msg.sender,_DummyERC20_rewardToken); + + // Ensure contract has sufficient rewards + require to_mathint(_DummyERC20_rewardToken.balanceOf(currentContract)) >= claimable; + + // Duplicate claim + claimDoubleRewardOnBehalfSame(e, e.msg.sender, e.msg.sender, _DummyERC20_rewardToken); + + uint256 duplicateClaimBalance = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + mathint diff = duplicateClaimBalance - initialBalance; + uint256 unclaimed = getUnclaimedRewards(e.msg.sender, _DummyERC20_rewardToken); + + assert diff + unclaimed <= claimable, "Duplicate claim changes rewards"; + } + + /** + * @title Claiming the same reward twice assuming insufficient rewards + * Using an array with the same reward twice does not give more rewards, + * assuming the contract does not have sufficient rewards. + * + * @dev Passed in job-id=`54de623f62eb4c95a343ee38834c6d16` + */ + rule prevent_duplicate_reward_claiming_single_reward_insufficient() { + single_RewardToken_setup(); + rewardsController_arbitrary_single_reward_setup(); + + env e; + require e.msg.sender != currentContract; // Cannot claim to contract + + uint256 initialBalance = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + mathint claimable = getClaimableRewards(e, e.msg.sender,_DummyERC20_rewardToken); + + // Ensure contract does not have sufficient rewards + require to_mathint(_DummyERC20_rewardToken.balanceOf(currentContract)) < claimable; + + // Duplicate claim + claimDoubleRewardOnBehalfSame(e, e.msg.sender, e.msg.sender, _DummyERC20_rewardToken); + + uint256 duplicateClaimBalance = _DummyERC20_rewardToken.balanceOf(e.msg.sender); + mathint diff = duplicateClaimBalance - initialBalance; + uint256 unclaimed = getUnclaimedRewards(e.msg.sender, _DummyERC20_rewardToken); + + assert diff + unclaimed <= claimable, "Duplicate claim changes rewards"; + }