Skip to content

Commit

Permalink
before munging the new storage. Currently it's NOT compiling
Browse files Browse the repository at this point in the history
  • Loading branch information
nisnislevi committed Aug 27, 2024
1 parent ea9d815 commit 843f6e4
Show file tree
Hide file tree
Showing 7 changed files with 184 additions and 22 deletions.
28 changes: 20 additions & 8 deletions certora/stata/conf/verifyERC4626.conf
Original file line number Diff line number Diff line change
@@ -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",
Expand All @@ -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,
Expand Down
10 changes: 10 additions & 0 deletions certora/stata/harness/ERC20AaveLMStorage_Harness.sol
Original file line number Diff line number Diff line change
@@ -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;
}
6 changes: 6 additions & 0 deletions certora/stata/harness/ERC4626StataTokenStorage_Harness.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
import {SafeERC20, IERC20} from 'openzeppelin-contracts/contracts/token/ERC20/utils/SafeERC20.sol';


contract ERC4626StataTokenStorage_Harness {
IERC20 _aToken;
}
9 changes: 9 additions & 0 deletions certora/stata/harness/ERC4626Storage_Harness.sol
Original file line number Diff line number Diff line change
@@ -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;
}
109 changes: 109 additions & 0 deletions certora/stata/harness/StataTokenV2Harness.sol
Original file line number Diff line number Diff line change
@@ -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;
}
*/
}
2 changes: 1 addition & 1 deletion certora/stata/scripts/run-all.sh
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#CMN="--compilation_steps_only"
CMN="--compilation_steps_only"



Expand Down
42 changes: 29 additions & 13 deletions certora/stata/specs/methods/methods_base.spec
Original file line number Diff line number Diff line change
@@ -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 ////////////////////////
Expand All @@ -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
// -----
Expand Down Expand Up @@ -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 =
Expand All @@ -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 //////////////////////

Expand All @@ -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
Expand All @@ -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;
Expand Down

0 comments on commit 843f6e4

Please sign in to comment.