diff --git a/certora/stata/conf/verifyERC4626.conf b/certora/stata/conf/verifyERC4626.conf index 1583b01a..cecf005c 100644 --- a/certora/stata/conf/verifyERC4626.conf +++ b/certora/stata/conf/verifyERC4626.conf @@ -1,6 +1,9 @@ { "files": [ - "certora/stata/harness/StaticATokenLMHarness.sol", + "certora/stata/harness/StataTokenV2Harness.sol", + "certora/stata/harness/ERC4626StataTokenStorage_Harness.sol", + "certora/stata/harness/ERC4626Storage_Harness.sol", +// "certora/stata/harness/ERC20AaveLMStorage_Harness.sol", "certora/stata/harness/pool/SymbolicLendingPool.sol", "certora/stata/harness/rewards/RewardsControllerHarness.sol", "certora/stata/harness/rewards/TransferStrategyHarness.sol", @@ -16,19 +19,28 @@ "ATokenInstance:POOL=SymbolicLendingPool", "ATokenInstance:_incentivesController=RewardsControllerHarness", "ATokenInstance:_underlyingAsset=DummyERC20_aTokenUnderlying", - "StaticATokenLMHarness:INCENTIVES_CONTROLLER=RewardsControllerHarness", - "StaticATokenLMHarness:POOL=SymbolicLendingPool", - "StaticATokenLMHarness:_aToken=ATokenInstance", - "StaticATokenLMHarness:_aTokenUnderlying=DummyERC20_aTokenUnderlying", - "StaticATokenLMHarness:_reward_A=DummyERC20_rewardToken" + "StataTokenV2Harness:INCENTIVES_CONTROLLER=RewardsControllerHarness", + "StataTokenV2Harness:POOL=SymbolicLendingPool", + "ERC4626StataTokenStorage_Harness:_aToken=ATokenInstance", + "ERC4626Storage_Harness:_asset=DummyERC20_aTokenUnderlying", +// "ERC4626Storage_Harness:the_storage._asset=DummyERC20_aTokenUnderlying", + "StataTokenV2Harness:_reward_A=DummyERC20_rewardToken" ], "packages": [ "aave-v3-core/=src/core", "aave-v3-periphery/=src/periphery", "solidity-utils/=lib/solidity-utils/src", "forge-std/=lib/forge-std/src", - ], - "verify":"StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626.spec", + "openzeppelin-contracts-upgradeable/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable", + "openzeppelin-contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts", + "@openzeppelin/contracts/=lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts", + +//lib/solidity-utils/lib/openzeppelin-contracts-upgradeable/lib/ +//@openzeppelin/contracts/=lib/openzeppelin-contracts/contracts/ + +], +// "verify":"StaticATokenLMHarness:certora/stata/specs/erc4626/erc4626.spec", + "verify":"StataTokenV2Harness:certora/stata/specs/erc4626/erc4626.spec", "solc": "solc8.20", "msg": "ERC4626 properties", "optimistic_loop": true, diff --git a/certora/stata/harness/ERC20AaveLMStorage_Harness.sol b/certora/stata/harness/ERC20AaveLMStorage_Harness.sol new file mode 100644 index 00000000..0cf0ce06 --- /dev/null +++ b/certora/stata/harness/ERC20AaveLMStorage_Harness.sol @@ -0,0 +1,10 @@ +import {SafeERC20, IERC20} from 'openzeppelin-contracts/contracts/token/ERC20/utils/SafeERC20.sol'; +import {RewardIndexCache, UserRewardsData} from 'aave-v3-periphery/contracts/static-a-token/interfaces/IERC20AaveLM.sol'; + + +contract ERC20AaveLMStorage_Harness { + address _referenceAsset; // a/v token to track rewards on INCENTIVES_CONTROLLER + address[] _rewardTokens; + mapping(address user => IERC20AaveLM.RewardIndexCache cache) _startIndex; + mapping(address user => mapping(address reward => IERC20AaveLM.UserRewardsData cache)) _userRewardsData; +} diff --git a/certora/stata/harness/ERC4626StataTokenStorage_Harness.sol b/certora/stata/harness/ERC4626StataTokenStorage_Harness.sol new file mode 100644 index 00000000..156e34bb --- /dev/null +++ b/certora/stata/harness/ERC4626StataTokenStorage_Harness.sol @@ -0,0 +1,6 @@ +import {SafeERC20, IERC20} from 'openzeppelin-contracts/contracts/token/ERC20/utils/SafeERC20.sol'; + + +contract ERC4626StataTokenStorage_Harness { + IERC20 _aToken; +} diff --git a/certora/stata/harness/ERC4626Storage_Harness.sol b/certora/stata/harness/ERC4626Storage_Harness.sol new file mode 100644 index 00000000..77c375b3 --- /dev/null +++ b/certora/stata/harness/ERC4626Storage_Harness.sol @@ -0,0 +1,9 @@ +import {SafeERC20, IERC20} from 'openzeppelin-contracts/contracts/token/ERC20/utils/SafeERC20.sol'; +import {ERC4626Upgradeable} from 'openzeppelin-contracts-upgradeable/contracts/token/ERC20/extensions/ERC4626Upgradeable.sol'; + +contract ERC4626Storage_Harness { + IERC20 _asset; + uint8 _underlyingDecimals; + + ERC4626Upgradeable.ERC4626Storage the_storage; +} diff --git a/certora/stata/harness/StataTokenV2Harness.sol b/certora/stata/harness/StataTokenV2Harness.sol new file mode 100644 index 00000000..126f1fec --- /dev/null +++ b/certora/stata/harness/StataTokenV2Harness.sol @@ -0,0 +1,109 @@ +// 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; + address internal _reward_B; + + ERC4626Storage the_storage; + + function get_the_storage() public view returns (ERC4626Storage storage ret) { + ret = the_storage; + } + + + constructor( + IPool pool, + IRewardsController rewardsController + ) StataTokenV2(pool, rewardsController) {} + + function rate() external view returns (uint256) { + return _rate(); + } + + /* + // returns the address of the underlying asset of the static aToken + function getStaticATokenUnderlying() public view returns (address) { + //return _aTokenUnderlying; + return asset(); + } + + // 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); + } + /* + function getUserRewardsData(address user, address reward) + external view + returns (uint128) { + UserRewardsData memory currentUserRewardsData = _userRewardsData[user][ + reward + ]; + return currentUserRewardsData.rewardsIndexOnLastInteraction; + } + */ +} diff --git a/certora/stata/scripts/run-all.sh b/certora/stata/scripts/run-all.sh index cf5e50e9..653a66d2 100644 --- a/certora/stata/scripts/run-all.sh +++ b/certora/stata/scripts/run-all.sh @@ -1,4 +1,4 @@ -#CMN="--compilation_steps_only" +CMN="--compilation_steps_only" diff --git a/certora/stata/specs/methods/methods_base.spec b/certora/stata/specs/methods/methods_base.spec index 1678f706..872e1166 100644 --- a/certora/stata/specs/methods/methods_base.spec +++ b/certora/stata/specs/methods/methods_base.spec @@ -1,12 +1,13 @@ import "erc20.spec"; -using StaticATokenLMHarness as _StaticATokenLM; +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; +using ERC4626Storage_Harness as _ERC4626_storage; /////////////////// Methods //////////////////////// @@ -29,10 +30,10 @@ methods { // static aToken harness // --------------------- - function getStaticATokenUnderlying() external returns (address) envfree; - function getRewardsIndexOnLastInteraction(address, address) external returns (uint128) envfree; - function getRewardTokensLength() external returns (uint256) envfree; - function getRewardToken(uint256) external returns (address) envfree; + // function getStaticATokenUnderlying() external returns (address) envfree; + //function getRewardsIndexOnLastInteraction(address, address) external returns (uint128) envfree; + //function getRewardTokensLength() external returns (uint256) envfree; + //function getRewardToken(uint256) external returns (address) envfree; // erc20 // ----- @@ -91,11 +92,26 @@ methods { function _DummyERC20_rewardToken.totalSupply() external returns (uint256) envfree; function _.UNDERLYING_ASSET_ADDRESS() external => CONSTANT UNRESOLVED; + + function RAY() external returns (uint256) envfree; + function get_the_storage() external returns (ERC4626Upgradeable.ERC4626Storage storage) envfree; + function ERC4626Upgradeable._getERC4626Storage() internal returns (ERC4626Upgradeable.ERC4626Storage storage) => + get_the_storage(); +} + +function _getERC4626StorageCVL() returns ERC4626Upgradeable.ERC4626Storage { + return get_the_storage(); +} + + +function getStaticATokenUnderlying() returns address { + return _ERC4626_storage._asset; } + ///////////////// DEFINITIONS ////////////////////// - definition RAY() returns uint256 = 10^27; +// definition RAY() returns uint256 = 10^27; /// @notice Claim rewards methods definition claimFunctions(method f) returns bool = @@ -106,18 +122,18 @@ methods { definition collectAndUpdateFunction(method f) returns bool = f.selector == sig:collectAndUpdateRewards(address).selector; - definition harnessOnlyMethods(method f) returns bool = +/* definition harnessOnlyMethods(method f) returns bool = (harnessMethodsMinusHarnessClaimMethods(f) || f.selector == sig:claimSingleRewardOnBehalf(address, address, address).selector || - f.selector == sig:claimDoubleRewardOnBehalfSame(address, address, address).selector); + f.selector == sig:claimDoubleRewardOnBehalfSame(address, address, address).selector);*/ - definition harnessMethodsMinusHarnessClaimMethods(method f) returns bool = +/* definition harnessMethodsMinusHarnessClaimMethods(method f) returns bool = (f.selector == sig:getStaticATokenUnderlying().selector || f.selector == sig:getRewardTokensLength().selector || f.selector == sig:getRewardToken(uint256).selector || f.selector == sig:getRewardsIndexOnLastInteraction(address, address).selector || f.selector == sig:getUserRewardsData(address, address).selector || - f.selector == sig:_mintWrapper(address, uint256).selector); + f.selector == sig:_mintWrapper(address, uint256).selector);*/ ////////////////// FUNCTIONS ////////////////////// @@ -126,10 +142,10 @@ methods { * Setup the `StaticATokenLM`'s rewards so they contain a single reward token * which is` _DummyERC20_rewardToken`. */ - function single_RewardToken_setup() { +/* function single_RewardToken_setup() { require getRewardTokensLength() == 1; require getRewardToken(0) == _DummyERC20_rewardToken; - } + }*/ /** * @title Single reward setup in RewardsController @@ -144,7 +160,7 @@ methods { /// @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 getRewardTokensLength() > 0;*/ require _RewardsController.getAvailableRewardsCount(_AToken) > 0; require _RewardsController.getRewardsByAsset(_AToken, 0) == _DummyERC20_rewardToken; require currentContract != e.msg.sender;