From 7cd25c0d56e9829ea060f0895c700c355d19e459 Mon Sep 17 00:00:00 2001 From: Michael M Date: Tue, 10 Sep 2024 19:52:37 +0300 Subject: [PATCH] Certora adaptation to stata --- .github/workflows/certora-stata.yml | 79 ++ certora/conf/AToken.conf | 1 + certora/conf/NEW-pool-no-summarizations.conf | 1 + certora/conf/NEW-pool-simple-properties.conf | 1 + certora/conf/ReserveConfiguration.conf | 1 + certora/conf/StableDebtToken.conf | 1 + certora/conf/UserConfiguration.conf | 1 + certora/conf/VariableDebtToken.conf | 1 + certora/scripts/run-all.sh | 2 +- certora/specs/NEW-pool-base.spec | 12 +- certora/specs/NEW-pool-no-summarizations.spec | 2 +- certora/stata/Makefile | 33 + certora/stata/applyHarness.patch | 48 ++ certora/stata/conf/verifyAToken.conf | 40 + certora/stata/conf/verifyDoubleClaim.conf | 40 + certora/stata/conf/verifyERC4626.conf | 40 + .../verifyERC4626DepositSummarization.conf | 39 + certora/stata/conf/verifyERC4626Extended.conf | 40 + ...verifyERC4626MintDepositSummarization.conf | 41 + certora/stata/conf/verifyStataToken.conf | 40 + certora/stata/harness/StataTokenV2Harness.sol | 85 ++ .../harness/pool/SymbolicLendingPool.sol | 108 +++ .../rewards/RewardsControllerHarness.sol | 48 ++ .../rewards/TransferStrategyHarness.sol | 22 + .../TransferStrategyMultiRewardHarness.sol | 31 + .../stata/harness/tokens/DummyERC20Impl.sol | 53 ++ .../tokens/DummyERC20_aTokenUnderlying.sol | 5 + .../harness/tokens/DummyERC20_rewardToken.sol | 5 + certora/stata/munged/.gitignore | 2 + certora/stata/scripts/run-all.sh | 95 +++ .../stata/specs/StataToken/StataToken.spec | 399 +++++++++ .../specs/StataToken/aTokenProperties.spec | 246 ++++++ .../stata/specs/StataToken/double_claim.spec | 65 ++ certora/stata/specs/erc4626/erc4626.spec | 754 ++++++++++++++++++ .../erc4626/erc4626DepositSummarization.spec | 163 ++++ .../stata/specs/erc4626/erc4626Extended.spec | 254 ++++++ .../erc4626MintDepositSummarization.spec | 220 +++++ certora/stata/specs/methods/CVLMath.spec | 236 ++++++ certora/stata/specs/methods/erc20.spec | 12 + certora/stata/specs/methods/methods_base.spec | 195 +++++ .../specs/methods/methods_multi_reward.spec | 75 ++ 41 files changed, 3528 insertions(+), 8 deletions(-) create mode 100644 .github/workflows/certora-stata.yml create mode 100644 certora/stata/Makefile create mode 100644 certora/stata/applyHarness.patch create mode 100644 certora/stata/conf/verifyAToken.conf create mode 100644 certora/stata/conf/verifyDoubleClaim.conf create mode 100644 certora/stata/conf/verifyERC4626.conf create mode 100644 certora/stata/conf/verifyERC4626DepositSummarization.conf create mode 100644 certora/stata/conf/verifyERC4626Extended.conf create mode 100644 certora/stata/conf/verifyERC4626MintDepositSummarization.conf create mode 100644 certora/stata/conf/verifyStataToken.conf create mode 100644 certora/stata/harness/StataTokenV2Harness.sol create mode 100644 certora/stata/harness/pool/SymbolicLendingPool.sol create mode 100644 certora/stata/harness/rewards/RewardsControllerHarness.sol create mode 100644 certora/stata/harness/rewards/TransferStrategyHarness.sol create mode 100644 certora/stata/harness/rewards/TransferStrategyMultiRewardHarness.sol create mode 100644 certora/stata/harness/tokens/DummyERC20Impl.sol create mode 100644 certora/stata/harness/tokens/DummyERC20_aTokenUnderlying.sol create mode 100644 certora/stata/harness/tokens/DummyERC20_rewardToken.sol create mode 100644 certora/stata/munged/.gitignore create mode 100644 certora/stata/scripts/run-all.sh create mode 100644 certora/stata/specs/StataToken/StataToken.spec create mode 100644 certora/stata/specs/StataToken/aTokenProperties.spec create mode 100644 certora/stata/specs/StataToken/double_claim.spec create mode 100644 certora/stata/specs/erc4626/erc4626.spec create mode 100644 certora/stata/specs/erc4626/erc4626DepositSummarization.spec create mode 100644 certora/stata/specs/erc4626/erc4626Extended.spec create mode 100644 certora/stata/specs/erc4626/erc4626MintDepositSummarization.spec create mode 100644 certora/stata/specs/methods/CVLMath.spec create mode 100644 certora/stata/specs/methods/erc20.spec create mode 100644 certora/stata/specs/methods/methods_base.spec create mode 100644 certora/stata/specs/methods/methods_multi_reward.spec diff --git a/.github/workflows/certora-stata.yml b/.github/workflows/certora-stata.yml new file mode 100644 index 00000000..81fdf68a --- /dev/null +++ b/.github/workflows/certora-stata.yml @@ -0,0 +1,79 @@ +name: certora-stata + +on: + push: + branches: + - main + pull_request: + branches: + - main + + 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.14.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/stata + touch applyHarness.patch + make munged + cd ../.. + certoraRun certora/stata/conf/${{ matrix.rule }} + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 + matrix: + rule: + - verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance + - verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert + # Timeout + # - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw + - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay + - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1 + - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint + - verifyERC4626Extended.conf --rule maxDepositConstant + - verifyERC4626Extended.conf --rule redeemSum + - verifyERC4626Extended.conf --rule redeemATokensSum + - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf + - verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf + - verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist + - verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards + - verifyStataToken.conf --rule totalClaimableRewards_stable + - verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset + - verifyStataToken.conf --rule solvency_total_asset_geq_total_supply + - verifyStataToken.conf --rule singleAssetAccruedRewards + - verifyStataToken.conf --rule totalAssets_stable + - verifyStataToken.conf --rule getClaimableRewards_stable + - verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit + - verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens + - verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf + - verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim + - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient + - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient diff --git a/certora/conf/AToken.conf b/certora/conf/AToken.conf index 299a8f4e..fcf73ac5 100644 --- a/certora/conf/AToken.conf +++ b/certora/conf/AToken.conf @@ -11,5 +11,6 @@ "process": "emv", "solc": "solc8.19", "verify": "ATokenHarness:certora/specs/AToken.spec", +// "build_cache": true, "msg": "aToken spec" } diff --git a/certora/conf/NEW-pool-no-summarizations.conf b/certora/conf/NEW-pool-no-summarizations.conf index 11f62350..080f07f5 100644 --- a/certora/conf/NEW-pool-no-summarizations.conf +++ b/certora/conf/NEW-pool-no-summarizations.conf @@ -36,6 +36,7 @@ "depositUpdatesUserATokenSuperBalance", "depositCannotChangeOthersATokenSuperBalance" ], +// "build_cache": true, "parametric_contracts": ["PoolHarness"], "msg": "pool-no-summarizations::partial rules", } diff --git a/certora/conf/NEW-pool-simple-properties.conf b/certora/conf/NEW-pool-simple-properties.conf index 96a78c78..6c81b8ad 100644 --- a/certora/conf/NEW-pool-simple-properties.conf +++ b/certora/conf/NEW-pool-simple-properties.conf @@ -38,6 +38,7 @@ "cannotBorrowOnReserveDisabledForBorrowing", "cannotBorrowOnFrozenReserve" ], +// "build_cache": true, "parametric_contracts": ["PoolHarness"], "msg": "pool-simple-properties::ALL", } diff --git a/certora/conf/ReserveConfiguration.conf b/certora/conf/ReserveConfiguration.conf index 2e4e50b6..ed3fc42f 100644 --- a/certora/conf/ReserveConfiguration.conf +++ b/certora/conf/ReserveConfiguration.conf @@ -10,5 +10,6 @@ ], "rule_sanity": "basic", // from time to time, use "advanced" instead of "basic" "solc": "solc8.19", +// "build_cache": true, "verify": "ReserveConfigurationHarness:certora/specs/ReserveConfiguration.spec" } diff --git a/certora/conf/StableDebtToken.conf b/certora/conf/StableDebtToken.conf index 1480d348..0d94747f 100644 --- a/certora/conf/StableDebtToken.conf +++ b/certora/conf/StableDebtToken.conf @@ -14,5 +14,6 @@ "optimistic_loop": true, "process": "emv", "solc": "solc8.19", +// "build_cache": true, "verify": "StableDebtTokenHarness:certora/specs/StableDebtToken.spec" } diff --git a/certora/conf/UserConfiguration.conf b/certora/conf/UserConfiguration.conf index 65b23d05..2d85039b 100644 --- a/certora/conf/UserConfiguration.conf +++ b/certora/conf/UserConfiguration.conf @@ -11,5 +11,6 @@ "-useBitVectorTheory" ], "solc": "solc8.19", +// "build_cache": true, "verify": "UserConfigurationHarness:certora/specs/UserConfiguration.spec" } diff --git a/certora/conf/VariableDebtToken.conf b/certora/conf/VariableDebtToken.conf index 52b9f172..90050b61 100644 --- a/certora/conf/VariableDebtToken.conf +++ b/certora/conf/VariableDebtToken.conf @@ -7,5 +7,6 @@ "optimistic_loop": true, "process": "emv", "solc": "solc8.19", +// "build_cache": true, "verify": "VariableDebtTokenHarness:certora/specs/VariableDebtToken.spec" } diff --git a/certora/scripts/run-all.sh b/certora/scripts/run-all.sh index 9e6c5d05..ab9685d4 100644 --- a/certora/scripts/run-all.sh +++ b/certora/scripts/run-all.sh @@ -1,4 +1,4 @@ -CMN="" +#CMN="--compilation_steps_only" diff --git a/certora/specs/NEW-pool-base.spec b/certora/specs/NEW-pool-base.spec index ac7cfdf0..9a9e86ba 100644 --- a/certora/specs/NEW-pool-base.spec +++ b/certora/specs/NEW-pool-base.spec @@ -30,19 +30,19 @@ methods { function _.transfer(address, uint256) external => DISPATCHER(true); function _.transferFrom(address, address, uint256) external => DISPATCHER(true); function _.approve(address, uint256) external => DISPATCHER(true); - function _.mint(address, uint256) external => DISPATCHER(true); - function _.burn(uint256) external => DISPATCHER(true); + //function _.mint(address, uint256) external => DISPATCHER(true); + //function _.burn(uint256) external => DISPATCHER(true); function _.balanceOf(address) external => DISPATCHER(true); function _.totalSupply() external => DISPATCHER(true); // ATOKEN - function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true); - function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true); + //function _.mint(address user, uint256 amount, uint256 index) external => DISPATCHER(true); + //function _.burn(address user, address receiverOfUnderlying, uint256 amount, uint256 index) external => DISPATCHER(true); function _.mintToTreasury(uint256 amount, uint256 index) external => DISPATCHER(true); function _.transferOnLiquidation(address from, address to, uint256 value) external => DISPATCHER(true); function _.transferUnderlyingTo(address user, uint256 amount) external => DISPATCHER(true); - function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true); + // function _.handleRepayment(address user, uint256 amount) external => DISPATCHER(true); function _.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) external => DISPATCHER(true); function _.ATokenBalanceOf(address user) external => DISPATCHER(true); @@ -62,7 +62,7 @@ methods { function _.getReserveNormalizedIncome(address asset) external => DISPATCHER(true); function _.getReserveNormalizedVariableDebt(address asset) external => DISPATCHER(true); function _.getACLManager() external => DISPATCHER(true); - function _.isBridge(address) external => DISPATCHER(true); + //function _.isBridge(address) external => DISPATCHER(true); // StableDebt function _.mint(address user, address onBehalfOf, uint256 amount, uint256 rate) external => DISPATCHER(true); diff --git a/certora/specs/NEW-pool-no-summarizations.spec b/certora/specs/NEW-pool-no-summarizations.spec index d4dcbe68..aad2c00c 100644 --- a/certora/specs/NEW-pool-no-summarizations.spec +++ b/certora/specs/NEW-pool-no-summarizations.spec @@ -9,7 +9,7 @@ methods { function _.symbol() external => DISPATCHER(true); function _.isFlashBorrower(address a) external => DISPATCHER(true); - function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true); + // function _.executeOperation(address[] a, uint256[]b, uint256[]c, address d, bytes e) external => DISPATCHER(true); function _.getAverageStableRate() external => DISPATCHER(true); function _.isPoolAdmin(address a) external => DISPATCHER(true); diff --git a/certora/stata/Makefile b/certora/stata/Makefile new file mode 100644 index 00000000..215e7440 --- /dev/null +++ b/certora/stata/Makefile @@ -0,0 +1,33 @@ +default: help + +PATCH = applyHarness.patch +CONTRACTS_DIR = ../../src +LIBS_DIR = ../../lib +MUNGED_SRC = munged/src +MUNGED_LIB = munged/lib +MUNGED_DIR = munged + +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..98c12412 --- /dev/null +++ b/certora/stata/applyHarness.patch @@ -0,0 +1,48 @@ +diff -ruN .gitignore .gitignore +--- .gitignore 1970-01-01 02:00:00 ++++ .gitignore 2024-09-04 13:59:46 +@@ -0,0 +1,2 @@ ++* ++!.gitignore +\ No newline at end of file +diff -ruN src/core/instances/ATokenInstance.sol src/core/instances/ATokenInstance.sol +--- src/core/instances/ATokenInstance.sol 2024-09-05 19:01:54 ++++ src/core/instances/ATokenInstance.sol 2024-09-05 11:33:23 +@@ -35,15 +35,15 @@ + + _domainSeparator = _calculateDomainSeparator(); + +- emit Initialized( +- underlyingAsset, +- address(POOL), +- treasury, +- address(incentivesController), +- aTokenDecimals, +- aTokenName, +- aTokenSymbol, +- params +- ); ++ // emit Initialized( ++ // underlyingAsset, ++ // address(POOL), ++ // treasury, ++ // address(incentivesController), ++ // aTokenDecimals, ++ // aTokenName, ++ // aTokenSymbol, ++ // params ++ // ); + } + } +diff -ruN src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol +--- src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 19:01:54 ++++ src/periphery/contracts/static-a-token/ERC20AaveLMUpgradeable.sol 2024-09-05 13:48:31 +@@ -147,7 +147,7 @@ + } + + ///@inheritdoc IERC20AaveLM +- function rewardTokens() external view returns (address[] memory) { ++ function rewardTokens() public view returns (address[] memory) { + ERC20AaveLMStorage storage $ = _getERC20AaveLMStorage(); + return $._rewardTokens; + } diff --git a/certora/stata/conf/verifyAToken.conf b/certora/stata/conf/verifyAToken.conf new file mode 100644 index 00000000..154a46f7 --- /dev/null +++ b/certora/stata/conf/verifyAToken.conf @@ -0,0 +1,40 @@ +{ + "files": [ + "certora/stata/harness/StataTokenV2Harness.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", + "certora/stata/munged/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", + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=certora/stata/munged/src/core", + "aave-v3-periphery/=certora/stata/munged/src/periphery", + "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", + "forge-std/=certora/stata/munged/lib/forge-std/src", + "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", + ], + "loop_iter": "1", + "msg": "aToken properties", + "optimistic_hashing": true, + "optimistic_loop": true, + "solc": "solc8.20", + "smt_timeout": "1400", + "verify": "StataTokenV2Harness:certora/stata/specs/StataToken/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..52cc582d --- /dev/null +++ b/certora/stata/conf/verifyDoubleClaim.conf @@ -0,0 +1,40 @@ +{ + "files": [ + "certora/stata/harness/StataTokenV2Harness.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", + "certora/stata/munged/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", + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=certora/stata/munged/src/core", + "aave-v3-periphery/=certora/stata/munged/src/periphery", + "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", + "forge-std/=certora/stata/munged/lib/forge-std/src", + "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", +], + "verify":"StataTokenV2Harness:certora/stata/specs/StataToken/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..06900f28 --- /dev/null +++ b/certora/stata/conf/verifyERC4626.conf @@ -0,0 +1,40 @@ +{ + "files": [ + "certora/stata/harness/StataTokenV2Harness.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", + "certora/stata/munged/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", + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=certora/stata/munged/src/core", + "aave-v3-periphery/=certora/stata/munged/src/periphery", + "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", + "forge-std/=certora/stata/munged/lib/forge-std/src", + "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", +], + "verify":"StataTokenV2Harness:certora/stata/specs/erc4626/erc4626.spec", + "solc": "solc8.20", + "msg": "ERC4626 properties", + "optimistic_loop": true, + "smt_timeout": "3600", + "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..d2ce588f --- /dev/null +++ b/certora/stata/conf/verifyERC4626DepositSummarization.conf @@ -0,0 +1,39 @@ +{ + "files": [ + "certora/stata/harness/StataTokenV2Harness.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", + "certora/stata/munged/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", + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=certora/stata/munged/src/core", + "aave-v3-periphery/=certora/stata/munged/src/periphery", + "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", + "forge-std/=certora/stata/munged/lib/forge-std/src", + "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", +], + "verify": "StataTokenV2Harness:certora/stata/specs/erc4626/erc4626DepositSummarization.spec", + "solc": "solc8.20", + "msg": "ERC4626 Deposit summarized", + "optimistic_loop": true, + "loop_iter": "1", + "optimistic_hashing": true, + "build_cache": true, +} \ 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..fedbbffe --- /dev/null +++ b/certora/stata/conf/verifyERC4626Extended.conf @@ -0,0 +1,40 @@ +{ + "files": [ + "certora/stata/harness/StataTokenV2Harness.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", + "certora/stata/munged/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", + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=certora/stata/munged/src/core", + "aave-v3-periphery/=certora/stata/munged/src/periphery", + "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", + "forge-std/=certora/stata/munged/lib/forge-std/src", + "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", + ], + "verify":"StataTokenV2Harness:certora/stata/specs/erc4626/erc4626Extended.spec", + "solc": "solc8.20", + "msg": "ERC4626 Extended properties", + "optimistic_loop": true, + "smt_timeout": "6000", + "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..d0c76fba --- /dev/null +++ b/certora/stata/conf/verifyERC4626MintDepositSummarization.conf @@ -0,0 +1,41 @@ +{ + "files": [ + "certora/stata/harness/StataTokenV2Harness.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", + "certora/stata/munged/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", + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=certora/stata/munged/src/core", + "aave-v3-periphery/=certora/stata/munged/src/periphery", + "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", + "forge-std/=certora/stata/munged/lib/forge-std/src", + "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", + ], + "verify": + "StataTokenV2Harness:certora/stata/specs/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/verifyStataToken.conf b/certora/stata/conf/verifyStataToken.conf new file mode 100644 index 00000000..a1406810 --- /dev/null +++ b/certora/stata/conf/verifyStataToken.conf @@ -0,0 +1,40 @@ +{ + "files": [ + "certora/stata/harness/StataTokenV2Harness.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", + "certora/stata/munged/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", + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" + ], + "packages": [ + "aave-v3-core/=certora/stata/munged/src/core", + "aave-v3-periphery/=certora/stata/munged/src/periphery", + "solidity-utils/=certora/stata/munged/lib/solidity-utils/src", + "forge-std/=certora/stata/munged/lib/forge-std/src", + "openzeppelin-contracts-upgradeable/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=certora/stata/munged/lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", + ], + "verify":"StataTokenV2Harness:certora/stata/specs/StataToken/StataToken.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/StataTokenV2Harness.sol b/certora/stata/harness/StataTokenV2Harness.sol new file mode 100644 index 00000000..ce615d08 --- /dev/null +++ b/certora/stata/harness/StataTokenV2Harness.sol @@ -0,0 +1,85 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.10; + +import {IERC20} from 'openzeppelin-contracts/contracts/interfaces/IERC20.sol'; +import {StataTokenV2, IPool, IRewardsController} from 'aave-v3-periphery/contracts/static-a-token/StataTokenV2.sol'; +import {SymbolicLendingPool} from './pool/SymbolicLendingPool.sol'; + + + +contract StataTokenV2Harness is StataTokenV2 { + address internal _reward_A; + + constructor( + IPool pool, + IRewardsController rewardsController + ) StataTokenV2(pool, rewardsController) {} + + function rate() external view returns (uint256) { + return _rate(); + } + + // 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) + ); + _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) + ); + _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); + } + +} diff --git a/certora/stata/harness/pool/SymbolicLendingPool.sol b/certora/stata/harness/pool/SymbolicLendingPool.sol new file mode 100644 index 00000000..ec3b7ef4 --- /dev/null +++ b/certora/stata/harness/pool/SymbolicLendingPool.sol @@ -0,0 +1,108 @@ +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.ReserveDataLegacy reserveLegacy; + DataTypes.ReserveData reserve; + + function getReserveData(address asset) external view returns (DataTypes.ReserveDataLegacy memory) { + DataTypes.ReserveDataLegacy memory res; + + res.configuration = reserve.configuration; + res.liquidityIndex = reserve.liquidityIndex; + res.currentLiquidityRate = reserve.currentLiquidityRate; + res.variableBorrowIndex = reserve.variableBorrowIndex; + res.currentVariableBorrowRate = reserve.currentVariableBorrowRate; + res.currentStableBorrowRate = reserve.currentStableBorrowRate; + res.lastUpdateTimestamp = reserve.lastUpdateTimestamp; + res.id = reserve.id; + res.aTokenAddress = reserve.aTokenAddress; + res.stableDebtTokenAddress = reserve.stableDebtTokenAddress; + res.variableDebtTokenAddress = reserve.variableDebtTokenAddress; + res.interestRateStrategyAddress = reserve.interestRateStrategyAddress; + res.accruedToTreasury = reserve.accruedToTreasury; + res.unbacked = reserve.unbacked; + res.isolationModeTotalDebt = reserve.isolationModeTotalDebt; + return res; + } + + function getReserveDataExtended(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..d6f32d65 --- /dev/null +++ b/certora/stata/harness/tokens/DummyERC20Impl.sol @@ -0,0 +1,53 @@ +// SPDX-License-Identifier: agpl-3.0 +pragma solidity ^0.8.0; + +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() external view returns (address) { + return address(this); + } + + 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] -= amount; + 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] -= amount; + b[recipient] += amount; + 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/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..c00dcb4e --- /dev/null +++ b/certora/stata/scripts/run-all.sh @@ -0,0 +1,95 @@ +#CMN="--compilation_steps_only" + +echo "******** Running: 1 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance \ + maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert \ +--msg "1: verifyERC4626.conf" + +echo "******** Running: 1.5 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw \ +--msg "1.5: verifyERC4626.conf" + +echo "******** Running: 2 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay \ +--msg "2: verifyERC4626MintDepositSummarization.conf" + +echo "******** Running: 3 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1 \ +--msg "3: " + +echo "******** Running: 4 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint \ + maxDepositConstant \ +--msg "4: " + +echo "******** Running: 5 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626Extended.conf --rule redeemSum \ +--msg "5: " + +echo "******** Running: 6 ***************" +certoraRun $CMN certora/stata/conf/verifyERC4626Extended.conf --rule redeemATokensSum \ +--msg "6: " + +echo "******** Running: 7 ***************" +certoraRun $CMN certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf \ +--msg "7: " + +echo "******** Running: 8 ***************" +certoraRun $CMN certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf \ +--msg "8: " + +echo "******** Running: 9 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist \ +--msg "9: " + +echo "******** Running: 10 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards \ +--msg "10: " + +echo "******** Running: 11 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule totalClaimableRewards_stable \ +--msg "11: " + +echo "******** Running: 12 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset \ +--msg "12: " + +echo "******** Running: 13 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule solvency_total_asset_geq_total_supply \ +--msg "13: " + +echo "******** Running: 14 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule singleAssetAccruedRewards \ +--msg "14: " + +echo "******** Running: 15 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule totalAssets_stable \ +--msg "15: " + +echo "******** Running: 16 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable \ +--msg "16: " + +echo "******** Running: 17 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit \ +--msg "17: " + +echo "******** Running: 18 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens \ +--msg "18: " + +echo "******** Running: 19 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf \ +--msg "19: " + +echo "******** Running: 20 ***************" +certoraRun $CMN certora/stata/conf/verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim \ +--msg "20: " + +echo "******** Running: 21 ***************" +certoraRun $CMN certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient \ +--msg "21: " + +echo "******** Running: 22 ***************" +certoraRun $CMN certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient \ +--msg "22: " diff --git a/certora/stata/specs/StataToken/StataToken.spec b/certora/stata/specs/StataToken/StataToken.spec new file mode 100644 index 00000000..479816b3 --- /dev/null +++ b/certora/stata/specs/StataToken/StataToken.spec @@ -0,0 +1,399 @@ +import "../methods/methods_base.spec"; + +/////////////////// Methods //////////////////////// + + methods { + 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; + } + + +///////////////// 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. + */ + 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` and `emergencyEtherTransfer` + * are filtered out. To avoid timeouts the rest of the + * methods were split between several versions of this rule. + * + * @dev Passed with rule-sanity in job-id=`98beb842d5b94278ac4a9222249fb564` + * + */ + rule rewardsTotalDeclinesOnlyByClaim(method f) filtered { + f -> ( + f.contract == currentContract && + !harnessOnlyMethods(f) && + f.selector != sig:initialize(address, string, string).selector) && + f.selector != sig:emergencyEtherTransfer(uint256).selector && + f.selector != sig:emergencyTokenTransfer(address,uint256).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 due to function other than claim or emergency rescue"; + } + + //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 + && !harnessMethodsMinusHarnessClaimMethods(f) + && !claimFunctions(f) + && f.selector != sig:claimDoubleRewardOnBehalfSame(address, address, address).selector + && f.selector != sig:emergencyEtherTransfer(uint256).selector + } + { + preserved redeem(uint256 shares, address receiver, address owner) with (env e1) { + requireInvariant solvency_total_asset_geq_total_supply(); + require balanceOf(owner) <= totalSupply(); + } + preserved redeemATokens(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(); + } + preserved emergencyTokenTransfer(address asset, uint256 amount) with (env e3) { + require rate() >= RAY(); + } + } + + + + //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 assets is greater than or equal to total supply. + invariant solvency_total_asset_geq_total_supply() + (_AToken.scaledBalanceOf(currentContract) >= totalSupply()) + filtered { f -> + f.contract == currentContract + && !harnessMethodsMinusHarnessClaimMethods(f) + && !claimFunctions(f) + && f.selector != sig:emergencyEtherTransfer(uint256).selector + && f.selector != sig:claimDoubleRewardOnBehalfSame(address, address, address).selector } + { + preserved withdraw(uint256 assets, address receiver, address owner) with (env e3) { + require balanceOf(owner) <= totalSupply(); + } + preserved depositWithPermit(uint256 assets, address receiver, uint256 deadline, IERC4626StataToken.SignatureParams signature, bool depositToAave) with (env e4) { + require balanceOf(receiver) <= totalSupply(); + require e4.msg.sender != currentContract; + } + preserved depositATokens(uint256 assets, address receiver) with (env e5) { + require balanceOf(receiver) <= totalSupply(); + require e5.msg.sender != currentContract; + } + preserved deposit(uint256 assets, address receiver) with (env e5) { + require balanceOf(receiver) <= totalSupply(); + require e5.msg.sender != currentContract; + } + preserved mint(uint256 shares, address receiver) with (env e6) { + require balanceOf(receiver) <= totalSupply(); + require e6.msg.sender != currentContract; + } + preserved redeem(uint256 shares, address receiver, address owner) with (env e2) { + require balanceOf(owner) <= totalSupply(); + } + preserved redeemATokens(uint256 shares, address receiver, address owner) with (env e2) { + require balanceOf(owner) <= totalSupply(); + } + preserved emergencyTokenTransfer(address asset, uint256 amount) with (env e1) { + require rate() >= RAY(); + } + } + + + + //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 && + f.selector != sig:emergencyEtherTransfer(uint256).selector && + !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; + } + + /// @title getTotalClaimableRewards() is stable unless rewards were claimed or emergency rescue was applied + rule totalClaimableRewards_stable(method f) + filtered { f -> + f.contract == currentContract + && !f.isView + && !claimFunctions(f) + && !collectAndUpdateFunction(f) + && !harnessOnlyMethods(f) + && f.selector != sig:initialize(address,string,string).selector + && f.selector != sig:emergencyEtherTransfer(uint256).selector + && f.selector != sig:emergencyTokenTransfer(address,uint256).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=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:emergencyEtherTransfer(uint256).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 + 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); + depositATokens(e, assets, recipient); // try depositWithPermit() + 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/StataToken/aTokenProperties.spec b/certora/stata/specs/StataToken/aTokenProperties.spec new file mode 100644 index 00000000..be0f9fad --- /dev/null +++ b/certora/stata/specs/StataToken/aTokenProperties.spec @@ -0,0 +1,246 @@ + +import "../methods/methods_base.spec"; + +////////////////// 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:depositATokens(uint256,address).selector) && + (f.selector != sig:withdraw(uint256,address,address).selector) && + (f.selector != sig:redeemATokens(uint256,address,address).selector) && + (f.selector != sig:mint(uint256,address).selector) && + (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) + } { + + 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() { + 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) { + // 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) { + 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_rewardToken); + + uint256 postBalance = _AToken.balanceOf(e.msg.sender); + assert preBalance == postBalance, "aToken balance changed by claimSingleRewardOnBehalf"; + } + + + rule aTokenBalanceIsFixed_for_claimRewardsToSelf() { + // 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) { + // 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 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).selector && + f.selector != sig:redeemATokens(uint256,address,address).selector && + f.selector != sig:emergencyEtherTransfer(uint256).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).selector } + { + 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_redeemAToken(address user) + _AToken.balanceOf(user) <= _AToken.totalSupply() + filtered { f -> f.selector == sig:redeemATokens(uint256,address,address).selector } + { + preserved with (env e){ + requireInvariant sumAllATokenScaledBalance_eq_totalSupply(); + } + } + + /// @title Sum of AToken scaled balances = AToken scaled totalSupply() + //pass with rule_sanity basic + //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 + //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(); + } + } diff --git a/certora/stata/specs/StataToken/double_claim.spec b/certora/stata/specs/StataToken/double_claim.spec new file mode 100644 index 00000000..466fa3ee --- /dev/null +++ b/certora/stata/specs/StataToken/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"; + } diff --git a/certora/stata/specs/erc4626/erc4626.spec b/certora/stata/specs/erc4626/erc4626.spec new file mode 100644 index 00000000..b790c3fb --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626.spec @@ -0,0 +1,754 @@ +import "../methods/methods_base.spec"; + +methods { + function balanceOf(address) external returns (uint256) envfree; + function totalSupply() external returns (uint256) envfree; + function ReserveConfiguration.getDecimals(DataTypes.ReserveConfigurationMap memory) internal returns (uint256) => limitReserveDecimals(); + function ReserveConfiguration.getSupplyCap(DataTypes.ReserveConfigurationMap memory) internal returns (uint256) => limitReserveSupplyCap(); +} + +///////////////// FUNCTIONS /////////////////////// + + function limitReserveDecimals() returns uint256 { + uint256 dec; + require dec >= 6 && dec <= 18; + return dec; + } + + function limitReserveSupplyCap() returns uint256 { + uint256 cap; + require cap <= 10^36; + return cap; + } + + +///////////////// 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); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + 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); + + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + 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"; + } + + /*** + * 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 redeemATokensCheck(env e){ + uint256 shares; + address receiver; + address owner; + uint256 assets; + mathint allowed = allowance(e, owner, e.msg.sender); + uint256 balBefore = balanceOf(owner); + + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + require index > RAY(); + require e.msg.sender != currentContract; + require receiver != currentContract; + + assets = redeemATokens(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, require_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() > RAY(); + require rate() <= 100 * RAY(); + 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() > RAY(); + require rate() <= 100 * RAY(); + 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 _AToken.scaledTotalSupply() <= 10^36; // arbitrary extremely large sum of tokens. 10^18 of 18 decimals tokens + require rate() > RAY(); + require rate() <= 100 * RAY(); + 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() > RAY(); + require rate() <= 100 * RAY(); + require _AToken.scaledTotalSupply() <= 10^36; // arbitrary extremely large sum of tokens. 10^18 of 18 decimals tokens + 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() > RAY(); + require rate() <= 100 * RAY(); + 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..f6675d10 --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626DepositSummarization.spec @@ -0,0 +1,163 @@ +import "../methods/methods_base.spec"; + +/////////////////// Methods //////////////////////// + +methods{ + // static aToken + // ------------- + function previewDeposit(uint256) external returns(uint256) envfree => NONDET; + function ERC20Upgradeable._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(asset()); + + 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(); + } + + // 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 aTokens 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 depositATokensCheckIndexGRayAssert1(env e){ + uint256 assets; + address receiver; + uint256 contractAssetBalBefore = _AToken.balanceOf(currentContract); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositATokens(e, assets, receiver); + + uint256 contractAssetBalAfter = _AToken.balanceOf(currentContract); + + // upper bound for deposited assets + assert contractAssetBalAfter - contractAssetBalBefore <= assets + index/RAY(); + } + + // 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 with permit 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 depositWithPermitCheckIndexGRayAssert1(env e){ + uint256 assets; + address receiver; + uint256 deadline; + IERC4626StataToken.SignatureParams signature; + bool depositToAave; + uint256 contractAssetBalBefore = _AToken.balanceOf(currentContract); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositWithPermit(e, assets, receiver, deadline, signature, depositToAave); + + 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(asset()); + + 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()); + } + + // STATUS: Verified + // https://prover.certora.com/output/11775/c149a926d08e44b98b05cec42ff97c0c/?anonymousKey=3a094dbfe8370e0ce3242e97cabd57a6df75a8c8 + ///@title Deposit aTokens 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 depositATokensCheckIndexERayAssert1(env e){ + uint256 assets; + address receiver; + uint256 contractAssetBalBefore = _AToken.balanceOf(currentContract); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositATokens(e, assets, receiver); + + uint256 contractAssetBalAfter = _AToken.balanceOf(currentContract); + + // upper bound for deposited assets + assert contractAssetBalAfter - contractAssetBalBefore <= assets + index/(2 * RAY()); + } + + // STATUS: Verified + // https://prover.certora.com/output/11775/c149a926d08e44b98b05cec42ff97c0c/?anonymousKey=3a094dbfe8370e0ce3242e97cabd57a6df75a8c8 + ///@title Deposit with permit 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 depositWithPermitCheckIndexERayAssert1(env e){ + uint256 assets; + address receiver; + uint256 deadline; + IERC4626StataToken.SignatureParams signature; + bool depositToAave; + uint256 contractAssetBalBefore = _AToken.balanceOf(currentContract); + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositWithPermit(e, assets, receiver, deadline, signature, depositToAave); + + 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..cbf95cb6 --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626Extended.spec @@ -0,0 +1,254 @@ +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"; + } + + /// @title Redeeming aTokens sum of assets is nearly equal to sum of redeeming + rule redeemATokensSum(uint256 shares1, uint256 shares2) { + env e; + address owner = e.msg.sender; // Handy alias + + uint256 assets1 = redeemATokens(e, shares1, owner, owner); + uint256 assets2 = redeemATokens(e, shares2, owner, owner); + mathint assetsSum = redeemATokens(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. + * 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. + rule maxDepositConstant(method f) + filtered { + f -> + f.contract == currentContract && + !f.isView && + !harnessOnlyMethods(f) && + f.selector != sig:emergencyEtherTransfer(uint256).selector && + f.selector != sig:deposit(uint256,address).selector && + f.selector != sig:depositWithPermit(uint256,address,uint256,IERC4626StataToken.SignatureParams,bool).selector && + f.selector != sig:withdraw(uint256,address,address).selector && + f.selector != sig:redeem(uint256,address,address).selector && + f.selector != sig:mint(uint256,address).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..16ea48ae --- /dev/null +++ b/certora/stata/specs/erc4626/erc4626MintDepositSummarization.spec @@ -0,0 +1,220 @@ +import "../methods/erc20.spec"; + +using SymbolicLendingPool as _SymbolicLendingPool; +using ATokenInstance as _AToken; + +/////////////////// Methods //////////////////////// + +methods{ + // static aToken + // ------------- + function asset() 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; + function RAY() external returns (uint256) envfree; +} + +///////////////// 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(asset()); + + 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/b10cd30ab6fb400baeff6b61c07bb375/?anonymousKey=ccba22e832b7549efea9f0d4b1288da2c1377ccb + ///@title DepositATokens 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 depositATokensCheckIndexGRayAssert2(env e){ + uint256 assets; + address receiver; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositATokens(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/b10cd30ab6fb400baeff6b61c07bb375/?anonymousKey=ccba22e832b7549efea9f0d4b1288da2c1377ccb + ///@title Deposit with permit 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 depositWithPermitCheckIndexGRayAssert2(env e){ + uint256 assets; + address receiver; + uint256 deadline; + IERC4626StataToken.SignatureParams signature; + bool depositToAave; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositWithPermit(e, assets, receiver, deadline, signature, depositToAave); + + 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(asset()); + + 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 depositATokensCheckIndexERayAssert2(env e){ + uint256 assets; + address receiver; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositATokens(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 depositWithPermitCheckIndexERayAssert2(env e){ + uint256 assets; + address receiver; + uint256 deadline; + IERC4626StataToken.SignatureParams signature; + bool depositToAave; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 = depositWithPermit(e, assets, receiver, deadline, signature, depositToAave); + + 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 e.msg.sender != currentContract; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 e.msg.sender != currentContract; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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 e.msg.sender != currentContract; + uint256 index = _SymbolicLendingPool.getReserveNormalizedIncome(asset()); + + 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/CVLMath.spec b/certora/stata/specs/methods/CVLMath.spec new file mode 100644 index 00000000..ba475be8 --- /dev/null +++ b/certora/stata/specs/methods/CVLMath.spec @@ -0,0 +1,236 @@ +/****************************************** +----------- CVL Math Library -------------- +*******************************************/ + + ///////////////// DEFINITIONS ////////////////////// + + // A restriction on the value of w = x * y / z + // The ratio between x (or y) and z is a rational number a/b or b/a. + // Important : do not set a = 0 or b = 0. + // Note: constRatio(x,y,z,a,b,w) <=> constRatio(x,y,z,b,a,w) + definition constRatio(uint256 x, uint256 y, uint256 z, + uint256 a, uint256 b, uint256 w) + returns bool = + ( a * x == b * z && to_mathint(w) == (b * y) / a ) || + ( b * x == a * z && to_mathint(w) == (a * y) / b ) || + ( a * y == b * z && to_mathint(w) == (b * x) / a ) || + ( b * y == a * z && to_mathint(w) == (a * x) / b ); + + // A restriction on the value of w = x * y / z + // The division quotient between x (or y) and z is an integer q or 1/q. + // Important : do not set q=0 + definition constQuotient(uint256 x, uint256 y, uint256 z, + uint256 q, uint256 w) + + returns bool = + ( to_mathint(x) == q * z && to_mathint(w) == q * y ) || + ( q * x == to_mathint(z) && to_mathint(w) == y / q ) || + ( to_mathint(y) == q * z && to_mathint(w) == q * x ) || + ( q * y == to_mathint(z) && to_mathint(w) == x / q ); + + /// Equivalent to the one above, but with implication + definition constQuotientImply(uint256 x, uint256 y, uint256 z, + uint256 q, uint256 w) + + returns bool = + ( to_mathint(x) == q * z => to_mathint(w) == q * y ) && + ( q * x == to_mathint(z) => to_mathint(w) == y / q ) && + ( to_mathint(y) == q * z => to_mathint(w) == q * x ) && + ( q * y == to_mathint(z) => to_mathint(w) == x / q ); + + definition ONE18() returns uint256 = 1000000000000000000; + // definition RAY() returns uint256 = 10^27; + + definition _monotonicallyIncreasing(uint256 x, uint256 y, uint256 fx, uint256 fy) returns bool = + (x > y => fx >= fy); + + definition _monotonicallyDecreasing(uint256 x, uint256 y, uint256 fx, uint256 fy) returns bool = + (x > y => fx <= fy); + + definition abs(mathint x) returns mathint = + x >= 0 ? x : 0 - x; + + definition min(mathint x, mathint y) returns mathint = + x > y ? y : x; + + definition max(mathint x, mathint y) returns mathint = + x > y ? x : y; + + /// Returns whether y is equal to x up to error bound of 'err' (18 decs). + /// e.g. 10% relative error => err = 1e17 + definition relativeErrorBound(mathint x, mathint y, mathint err) returns bool = + (x != 0 + ? abs(x - y) * ONE18() <= abs(x) * err + : abs(y) <= err); + + /// Axiom for a weighted average of the form WA = (x * y) / (y + z) + /// This is valid as long as z + y > 0 => make certain of that condition in the use of this definition. + definition weightedAverage(mathint x, mathint y, mathint z, mathint WA) returns bool = + ((x > 0 && y > 0) => (WA >= 0 && WA <= x)) + && + ((x < 0 && y > 0) => (WA <= 0 && WA >= x)) + && + ((x > 0 && y < 0) => (WA <= 0 && WA - x <= 0)) + && + ((x < 0 && y < 0) => (WA >= 0 && WA + x <= 0)) + && + ((x == 0 || y == 0) => (WA == 0)); + + + + ////////////////// FUNCTIONS ////////////////////// + + function mulDivDownAbstract(uint256 x, uint256 y, uint256 z) returns uint256 { + require z !=0; + uint256 xy = require_uint256(x * y); + uint256 res; + mathint rem; + require z * res + rem == to_mathint(xy); + require rem < to_mathint(z); + return res; + } + + function mulDivDownAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 { + uint256 res; + require z != 0; + uint256 xy = require_uint256(x * y); + uint256 fz = require_uint256(res * z); + + require xy >= fz; + require fz + z > to_mathint(xy); + return res; + } + + function mulDivUpAbstractPlus(uint256 x, uint256 y, uint256 z) returns uint256 { + uint256 res; + require z != 0; + uint256 xy = require_uint256(x * y); + uint256 fz = require_uint256(res * z); + require xy >= fz; + require fz + z > to_mathint(xy); + + if(xy == fz) { + return res; + } + return require_uint256(res + 1); + } + + function mulDownWad(uint256 x, uint256 y) returns uint256 { + return mulDivDownAbstractPlus(x, y, ONE18()); + } + + function mulUpWad(uint256 x, uint256 y) returns uint256 { + return mulDivUpAbstractPlus(x, y, ONE18()); + } + + function divDownWad(uint256 x, uint256 y) returns uint256 { + return mulDivDownAbstractPlus(x, ONE18(), y); + } + + function divUpWad(uint256 x, uint256 y) returns uint256 { + return mulDivUpAbstractPlus(x, ONE18(), y); + } + + function discreteQuotientMulDiv(uint256 x, uint256 y, uint256 z) returns uint256 + { + uint256 res; + require z != 0 && noOverFlowMul(x, y); + // Discrete quotients: + require( + ((x ==0 || y ==0) && res == 0) || + (x == z && res == y) || + (y == z && res == x) || + constQuotient(x, y, z, 2, res) || // Division quotient is 1/2 or 2 + constQuotient(x, y, z, 5, res) || // Division quotient is 1/5 or 5 + constQuotient(x, y, z, 100, res) // Division quotient is 1/100 or 100 + ); + return res; + } + + function discreteRatioMulDiv(uint256 x, uint256 y, uint256 z) returns uint256 + { + uint256 res; + require z != 0 && noOverFlowMul(x, y); + // Discrete ratios: + require( + ((x ==0 || y ==0) && res == 0) || + (x == z && res == y) || + (y == z && res == x) || + constRatio(x, y, z, 2, 1, res) || // f = 2*x or f = x/2 (same for y) + constRatio(x, y, z, 5, 1, res) || // f = 5*x or f = x/5 (same for y) + constRatio(x, y, z, 2, 3, res) || // f = 2*x/3 or f = 3*x/2 (same for y) + constRatio(x, y, z, 2, 7, res) // f = 2*x/7 or f = 7*x/2 (same for y) + ); + return res; + } + + function noOverFlowMul(uint256 x, uint256 y) returns bool + { + return x * y <= max_uint; + } + + /// @doc Ghost power function that incorporates mathematical pure x^y axioms. + /// @warning Some of these axioms might be false, depending on the Solidity implementation + /// The user must bear in mind that equality-like axioms can be violated because of rounding errors. + ghost _ghostPow(uint256, uint256) returns uint256 { + /// x^0 = 1 + axiom forall uint256 x. _ghostPow(x, 0) == ONE18(); + /// 0^x = 1 + axiom forall uint256 y. _ghostPow(0, y) == 0; + /// x^1 = x + axiom forall uint256 x. _ghostPow(x, ONE18()) == x; + /// 1^y = 1 + axiom forall uint256 y. _ghostPow(ONE18(), y) == ONE18(); + + /// I. x > 1 && y1 > y2 => x^y1 > x^y2 + /// II. x < 1 && y1 > y2 => x^y1 < x^y2 + axiom forall uint256 x. forall uint256 y1. forall uint256 y2. + x >= ONE18() && y1 > y2 => _ghostPow(x, y1) >= _ghostPow(x, y2); + axiom forall uint256 x. forall uint256 y1. forall uint256 y2. + x < ONE18() && y1 > y2 => (_ghostPow(x, y1) <= _ghostPow(x, y2) && _ghostPow(x,y2) <= ONE18()); + axiom forall uint256 x. forall uint256 y. + x < ONE18() && y > ONE18() => (_ghostPow(x, y) <= x); + axiom forall uint256 x. forall uint256 y. + x < ONE18() && y <= ONE18() => (_ghostPow(x, y) >= x); + axiom forall uint256 x. forall uint256 y. + x >= ONE18() && y > ONE18() => (_ghostPow(x, y) >= x); + axiom forall uint256 x. forall uint256 y. + x >= ONE18() && y <= ONE18() => (_ghostPow(x, y) <= x); + /// x1 > x2 && y > 0 => x1^y > x2^y + axiom forall uint256 x1. forall uint256 x2. forall uint256 y. + x1 > x2 => _ghostPow(x1, y) >= _ghostPow(x2, y); + + /* Additional axioms - potentially unsafe + /// x^y * x^(1-y) == x -> 0.01% relative error + axiom forall uint256 x. forall uint256 y. forall uint256 z. + (0 <= y && y <= ONE18() && z + y == to_mathint(ONE18())) => + relativeErrorBound(_ghostPow(x, y) * _ghostPow(x, z), x * ONE18(), ONE18() / 10000); + + /// (x^y)^(1/y) == x -> 1% relative error + axiom forall uint256 x. forall uint256 y. forall uint256 z. + (0 <= y && y <= ONE18() && z * y == ONE18()*ONE18() ) => + relativeErrorBound(_ghostPow(_ghostPow(x, y), z), x, ONE18() / 100); + */ + } + + function CVLPow(uint256 x, uint256 y) returns uint256 { + if (y == 0) {return ONE18();} + if (x == 0) {return 0;} + return _ghostPow(x, y); + } + + function CVLSqrt(uint256 x) returns uint256 { + mathint SQRT; + require SQRT*SQRT <= to_mathint(x) && (SQRT + 1)*(SQRT + 1) > to_mathint(x); + return require_uint256(SQRT); + } + + // For Aave + function rayMulCVLPrecise(uint x, uint y) returns uint256 { + return require_uint256((x*y + RAY()/2) / RAY()); + } + + function rayDivCVLPrecise(uint x, uint y) returns uint256 { + require y != 0; + return require_uint256((x*RAY() + y/2)/y); + } \ No newline at end of file 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..dc2dc608 --- /dev/null +++ b/certora/stata/specs/methods/methods_base.spec @@ -0,0 +1,195 @@ +import "erc20.spec"; +import "CVLMath.spec"; + +using StataTokenV2Harness 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 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.ReserveDataLegacy); + function _SymbolicLendingPool.getReserveDataExtended(address) external returns (DataTypes.ReserveData); + + // 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; + + function _.permit(address,address,uint256,uint256,uint8,bytes32,bytes32) external => NONDET; + + // 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 _.RESERVE_TREASURY_ADDRESS() external => CONSTANT; + 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; + + function RAY() external returns (uint256) envfree; + + // math lib + // ------------ + function _.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal => mulDivCVL(x, y, denominator, rounding) expect (uint256); + } + +///////////////// DEFINITIONS ////////////////////// + + /// @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:getRewardTokensLength().selector || + f.selector == sig:getRewardToken(uint256).selector || + f.selector == sig:_mintWrapper(address, uint256).selector); + +////////////////// Hooks ////////////////////// + + /// @title Reward hook + /// @notice allows a single reward + hook Sload address reward (slot 0x4fad66563f105be0bff96185c9058c4934b504d3ba15ca31e86294f0b01fd200).(offset 32)[INDEX uint256 i] /*_rewardTokens*/ { + require reward == _DummyERC20_rewardToken; + } + + /// @title aToken hook + hook Sload address aToken (slot 0x55029d3f54709e547ed74b2fc842d93107ab1490ab7555dd9dd0bf6451101900).(offset 0) /*aToken*/ { + require aToken == _AToken; + } + + /// @title underlying hook + hook Sload address underlying (slot 0x0773e532dfede91f04b12a73d3d2acd361424f41f76b4fb79f090161e36b4e00).(offset 0) /*_asset*/ { + require underlying == _DummyERC20_aTokenUnderlying; + } + + +////////////////// 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; + } + + /** + * @title MulDiv summarization in CVL. + * @dev Rounds up or down depends on user specification + */ + function mulDivCVL(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) returns uint256 { + if (rounding == Math.Rounding.Floor) { + return mulDivDownAbstractPlus(x, y, denominator); + } else { + return mulDivUpAbstractPlus(x, y, denominator); + } + } 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..3c305115 --- /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 => DISPATCHER(true); + + // 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; + } + +///////////////// FUNCTIONS /////////////////////// + + /// @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; + }