Skip to content

Commit

Permalink
fix: revert certora changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@sakulstra
sakulstra committed Aug 11, 2023
1 parent b07130c commit 9154fb6
Show file tree
Hide file tree
Showing 5 changed files with 305 additions and 371 deletions.
213 changes: 96 additions & 117 deletions certora/harness/.AaveTokenV3Harness.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,129 +8,108 @@

pragma solidity ^0.8.0;


import {StakedAaveV3} from '../munged/src/contracts/StakedAaveV3.sol';
import {IERC20} from 'openzeppelin-contracts/contracts/token/ERC20/IERC20.sol';

import {DelegationMode} from 'aave-token-v3/DelegationAwareBalance.sol';
import {BaseDelegation} from 'aave-token-v3/BaseDelegation.sol';

contract AaveTokenV3Harness is StakedAaveV3 {
constructor(
IERC20 stakedToken,
IERC20 rewardToken,
uint256 unstakeWindow,
address rewardsVault,
address emissionManager,
uint128 distributionDuration
)
StakedAaveV3(
stakedToken,
rewardToken,
unstakeWindow,
rewardsVault,
emissionManager,
distributionDuration
)
{}

// Returns amount of the cooldown initiated by the user.
function cooldownAmount(address user) public view returns (uint216) {
return stakersCooldowns[user].amount;
}

// Returns timestamp of the cooldown initiated by the user.
function cooldownTimestamp(address user) public view returns (uint40) {
return stakersCooldowns[user].timestamp;
}

// Returns the asset's emission per second from the sturct
function getAssetEmissionPerSecond(
address token
) public view returns (uint128) {
return assets[token].emissionPerSecond;
}

// Returns the asset's last updated timestamp from the sturct
function getAssetLastUpdateTimestamp(
address token
) public view returns (uint128) {
return assets[token].lastUpdateTimestamp;
}

// Returns the asset's global index from the sturct
function getAssetGlobalIndex(address token) public view returns (uint256) {
return assets[token].index;
}

// Returns the user's personal index for the specific asset
function getUserPersonalIndex(
address token,
address user
) public view returns (uint256) {
return assets[token].users[user];
}

function _getExchangeRateWrapper(
uint256 totalAssets,
uint256 totalShares
) public pure returns (uint216) {
return _getExchangeRate(totalAssets, totalShares);
}

// returns user's token balance, used in some community rules
function getBalance(address user) public view returns (uint104) {
return _balances[user].balance;
}

// returns user's delegated proposition balance
function getDelegatedPropositionBalance(
address user
) public view returns (uint72) {
return _balances[user].delegatedPropositionBalance;
}

// returns user's delegated voting balance
function getDelegatedVotingBalance(
address user
) public view returns (uint72) {
return _balances[user].delegatedVotingBalance;
}

//returns user's delegating proposition status
function getDelegatingProposition(address user) public view returns (bool) {
return
_balances[user].delegationMode == DelegationMode.PROPOSITION_DELEGATED ||
_balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
}

// returns user's delegating voting status
function getDelegatingVoting(address user) public view returns (bool) {
return
_balances[user].delegationMode == DelegationMode.VOTING_DELEGATED ||
_balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
}

// returns user's voting delegate
function getVotingDelegate(address user) public view returns (address) {
return _votingDelegatee[user];
}

// returns user's proposition delegate
function getPropositionDelegate(address user) public view returns (address) {
return _propositionDelegatee[user];
}

// returns user's delegation state
function getDelegationMode(
address user
) public view returns (DelegationMode) {
return _balances[user].delegationMode;
}

function __getPowerCurrent(
address user,
GovernancePowerType delegationType
) public view virtual returns (uint256) {
return BaseDelegation.getPowerCurrent(user, delegationType);
constructor(IERC20 stakedToken, IERC20 rewardToken, uint256 unstakeWindow, address rewardsVault,
address emissionManager, uint128 distributionDuration)
StakedAaveV3(stakedToken, rewardToken, unstakeWindow, rewardsVault,
emissionManager, distributionDuration) {}

// Returns amount of the cooldown initiated by the user.
function cooldownAmount(address user) public view returns (uint216) {
return stakersCooldowns[user].amount;
}

// Returns timestamp of the cooldown initiated by the user.
function cooldownTimestamp(address user) public view returns (uint40) {
return stakersCooldowns[user].timestamp;
}

// Returns the asset's emission per second from the sturct
function getAssetEmissionPerSecond(address token) public view returns (uint128) {
return assets[token].emissionPerSecond;
}

// Returns the asset's last updated timestamp from the sturct
function getAssetLastUpdateTimestamp(address token) public view returns (uint128) {
return assets[token].lastUpdateTimestamp;
}

// Returns the asset's global index from the sturct
function getAssetGlobalIndex(address token) public view returns (uint256) {
return assets[token].index;
}

// Returns the user's personal index for the specific asset
function getUserPersonalIndex(address token, address user) public view returns (uint256) {
return assets[token].users[user];
}

function _getExchangeRateWrapper(uint256 totalAssets, uint256 totalShares) public pure returns (uint216) {
return _getExchangeRate(totalAssets, totalShares);
}






// returns user's token balance, used in some community rules
function getBalance(address user) public view returns (uint104) {
return _balances[user].balance;
}

// returns user's delegated proposition balance
function getDelegatedPropositionBalance(address user) public view returns (uint72) {
return _balances[user].delegatedPropositionBalance;
}

// returns user's delegated voting balance
function getDelegatedVotingBalance(address user) public view returns (uint72) {
return _balances[user].delegatedVotingBalance;
}

//returns user's delegating proposition status
function getDelegatingProposition(address user) public view returns (bool) {
return
_balances[user].delegationMode == DelegationMode.PROPOSITION_DELEGATED ||
_balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
}

// returns user's delegating voting status
function getDelegatingVoting(address user) public view returns (bool) {
return
_balances[user].delegationMode == DelegationMode.VOTING_DELEGATED ||
_balances[user].delegationMode == DelegationMode.FULL_POWER_DELEGATED;
}

// returns user's voting delegate
function getVotingDelegate(address user) public view returns (address) {
return _votingDelegatee[user];
}

// returns user's proposition delegate
function getPropositionDelegate(address user) public view returns (address) {
return _propositionDelegatee[user];
}

// returns user's delegation state
function getDelegationMode(address user) public view returns (DelegationMode) {
return _balances[user].delegationMode;
}

function __getPowerCurrent(address user, GovernancePowerType delegationType)
public
view
virtual
returns (uint256)
{
return BaseDelegation.getPowerCurrent(user,delegationType);
}
}
127 changes: 58 additions & 69 deletions certora/harness/DummyERC20Impl.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,84 +8,73 @@ pragma solidity 0.8.19;
import {IERC20} from 'openzeppelin-contracts/contracts/token/ERC20/IERC20.sol';

contract DummyERC20Impl is IERC20 {
address internal _owner;

constructor(address owner_) {
_owner = owner_;
}

modifier onlyOwner() {
require(msg.sender == _owner, 'only owner can access');
_;
}
address internal _owner;

function owner() public view returns (address) {
return _owner;
}
constructor(address owner_){
_owner = owner_;
}

uint256 t;
mapping(address => uint256) b;
mapping(address => mapping(address => uint256)) a;
modifier onlyOwner()
{
require (msg.sender == _owner, "only owner can access");
_;
}

string public name;
string public symbol;
uint public decimals;
function owner() public view returns (address) {
return _owner;
}

function myAddress() public returns (address) {
return address(this);
}
uint256 t;
mapping (address => uint256) b;
mapping (address => mapping (address => uint256)) a;

function add(uint a, uint b) internal pure returns (uint256) {
uint c = a + b;
require(c >= a);
return c;
}
string public name;
string public symbol;
uint public decimals;

function sub(uint a, uint b) internal pure returns (uint256) {
require(a >= b);
return a - b;
}
function myAddress() public returns (address) {
return address(this);
}

function totalSupply() public view override returns (uint256) {
return t;
}
function add(uint a, uint b) internal pure returns (uint256) {
uint c = a +b;
require (c >= a);
return c;
}
function sub(uint a, uint b) internal pure returns (uint256) {
require (a>=b);
return a-b;
}

function balanceOf(address account) public view override returns (uint256) {
return b[account];
}
function totalSupply() public override view returns (uint256) {
return t;
}
function balanceOf(address account) public view override returns (uint256) {
return b[account];
}
function transfer(address recipient, uint256 amount) external override returns (bool) {
b[msg.sender] = sub(b[msg.sender], amount);
b[recipient] = add(b[recipient], amount);
return true;
}
function allowance(address owner, address spender) external override view returns (uint256) {
return a[owner][spender];
}
function approve(address spender, uint256 amount) external override returns (bool) {
a[msg.sender][spender] = amount;
return true;
}

function transfer(
address recipient,
uint256 amount
) external override returns (bool) {
b[msg.sender] = sub(b[msg.sender], amount);
b[recipient] = add(b[recipient], amount);
return true;
}

function allowance(
address owner,
address spender
) external view override returns (uint256) {
return a[owner][spender];
}

function approve(
address spender,
uint256 amount
) external override returns (bool) {
a[msg.sender][spender] = amount;
return true;
}

function transferFrom(
address sender,
address recipient,
uint256 amount
) external override returns (bool) {
b[sender] = sub(b[sender], amount);
b[recipient] = add(b[recipient], amount);
a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
return true;
}
function transferFrom(
address sender,
address recipient,
uint256 amount
) external override returns (bool) {
b[sender] = sub(b[sender], amount);
b[recipient] = add(b[recipient], amount);
a[sender][msg.sender] = sub(a[sender][msg.sender], amount);
return true;
}
}
3 changes: 2 additions & 1 deletion certora/harness/RewardVault.sol
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
// SPDX-License-Identifier: agpl-3.0
pragma solidity 0.8.19;

contract RewardVault {}
contract RewardVault {
}
Loading

0 comments on commit 9154fb6

Please sign in to comment.