Aave Dashboard

1

Contracts

17

Rules

17/17

Verified

Aave_Ecosystem_Reserve_V2

remainingBalance_LE_deposit

Last update 29/04/2022
verified

Description

Stream's remaining balance is always equal or less than the stream deposit

Pseudo formula

{
    stream.remainingBalance <= stream.deposit
}

CVL CODE

invariant remainingBalance_LE_deposit(uint256 streamId)
    getStreamExists(streamId) => getStreamRemainingBalance(streamId) <= getStreamDeposit(streamId)

balanceOf_LE_deposit

Last update 29/04/2022
verified

Description

stream's balanceOf() returns a value equal or less than stream's deposit

Pseudo formula

{
    balanceOf(stream, alice) <= stream.deposit
}

CVL CODE

invariant balanceOf_LE_deposit(env e, uint256 streamId)
    getStreamExists(streamId) => balanceOf(e, streamId, getStreamRecipient(streamId)) <= getStreamDeposit(streamId)

ratePerSecond_GE_1

Last update 29/04/2022
verified

Description

Stream's rate per second is always equal or greater than 1

Pseudo formula

{
    stream.ratePerSecond >= 1
}

CVL CODE

invariant ratePerSecond_GE_1(uint256 streamId)
    getStreamExists(streamId) => getStreamRPS(streamId) >= 1

cantWithdrawTooEarly

Last update 29/04/2022
verified

Description

Recipient cannot withdraw before start time

Pseudo formula

{
    stream.startTime >= block.timestamp => balanceOf(stream, recipient) == 0
}

CVL CODE

invariant cantWithdrawTooEarly(env e, uint256 streamId)
    getStreamExists(streamId) && e.block.timestamp <= getStreamStartTime(streamId) =>
        balanceOf(e, streamId, getStreamRecipient(streamId)) == 0

streamHasSenderAndRecipient

Last update 29/04/2022
verified

Description

Every stream has a sender and a recipient

Pseudo formula

{
    stream.isEntity => stream.sender != 0 && stream.recipient != 0
}

CVL CODE

invariant streamHasSenderAndRecipient(uint256 streamId)
    getStreamExists(streamId) => getStreamRecipient(streamId) != 0 && getStreamSender(streamId) != 0

withdrawalsSolvent

Last update 29/04/2022
verified

Description

Sum of all withdrawals from a stream is equal or less than the original stream deposit

Pseudo formula

{
    Σ(stream withdrawals) <= stream.deposit
}

CVL CODE

invariant withdrawalsSolvent(uint256 streamId)
    to_mathint(getStreamRemainingBalance(streamId)) == 
        (to_mathint(getStreamDeposit(streamId)) - sumWithdrawalsPerStream[streamId])
    // filter out createStream because it resets the deposit value
    filtered { f-> f.selector != createStream(address, uint256, address, uint256, uint256).selector }

_nextStreamIdCorrectness

Last update 29/04/2022
verified

Description

Next Stream ID only goes up

Pseudo formula

{
            nextIdBefore = _nextStreamId()
}
<
            f(e, args)
>
{
            _nextStreamId() >= nextIdBefore
}

CVL CODE

rule _nextStreamIdCorrectness(method f)
filtered { f-> f.selector != initialize(address).selector} 
{
    env e;
    calldataarg args;
    uint256 _nextStreamIdBefore = _nextStreamId();
    f(e, args);
    uint256 _nextStreamIdAfter = _nextStreamId();
    assert _nextStreamIdAfter >= _nextStreamIdBefore;
}

streamRemainingBalanceMonotonicity

Last update 29/04/2022
verified

Description

Existing stream's remaining balance can only decrease

Pseudo formula

{
            remainingBalancebefore = stream.remainingBalance
}
<
            f(e, args)
>
{
            stream.remainingBalance <= remainingBalanceBefore
}

CVL CODE

rule streamRemainingBalanceMonotonicity(method f, uint256 streamId) {
    env e;
    calldataarg args;
    
    require getStreamExists(streamId);
    // without this prover creates a new stream with the same id as the current one
    require _nextStreamId() > streamId;
    uint256 remainingBalanceBefore = getStreamRemainingBalance(streamId);
    f(e, args);
    uint256 remainingBalanceAfter = getStreamRemainingBalance(streamId);
    assert remainingBalanceAfter <= remainingBalanceBefore;
}

integrityOfWithdraw

Last update 29/04/2022
verified

Description

Recipient cannot withdraw more than the current balance

Pseudo formula

{
            amount > balanceOf(stream, msg.sender)
}
<
            withdrawFromStream(stream, amount)
>
{
            lastReverted
}

CVL CODE

rule integrityOfWithdraw(uint256 streamId, uint256 amount) {
    env e;
    address recipient = getStreamRecipient(streamId);
    require e.msg.sender == recipient;
    uint256 balanceBefore = balanceOf(e, streamId, recipient);
    require amount > balanceBefore;
    withdrawFromStream@withrevert(e, streamId, amount);
    bool reverted = lastReverted;
    assert reverted;
}

fullWithdrawPossible

Last update 29/04/2022
verified

Description

Withdrawing full balance is always possible if treasury has sufficient token balance

Pseudo formula

{
            balance = balanceOf(stream, msg.sender)
}
<
            withdrawFromStream(stream, balance)
>
{
            !lastReverted
}

CVL CODE

rule fullWithdrawPossible(uint256 streamId) {
    env e;
    require getStreamExists(streamId);
    address recipient = getStreamRecipient(streamId);
    require e.msg.sender == recipient;
    require e.msg.sender != currentContract;
    uint256 balance = balanceOf(e, streamId, recipient);
    require balance > 0 && balance <= getStreamRemainingBalance(streamId);
    require _asset.balanceOf(currentContract) >= balance;
    require to_mathint(_asset.balanceOf(e.msg.sender)) + to_mathint(balance) < max_uint256;
    withdrawFromStream@withrevert(e, streamId, balance);
    assert !lastReverted;    
}

deltaOfCorrectness

Last update 29/04/2022
verified

Description

deltaOf() returns a correct value

Pseudo formula

 {
            stream.stopTime > stream.startTime
            stream.isEntity
 }
 <
            delta = deltaOf(stream)
 >
 {
            start >= block.timestamp => delta == 0
            block.timestamp > start && stop >= block.timestamp => delta == block.timestamp - start
            block.timestamp > stop => delta == stop - start
 }

CVL CODE

rule deltaOfCorrectness(uint256 streamId) {
    env e;
    require e.msg.value == 0;
    uint256 start = getStreamStartTime(streamId);
    uint256 stop = getStreamStopTime(streamId);
    require stop > start;
    uint256 delta = deltaOf@withrevert(e, streamId);
    assert lastReverted => !getStreamExists(streamId);
    assert start >= e.block.timestamp => delta == 0;
    assert e.block.timestamp > start && stop >= e.block.timestamp => delta == e.block.timestamp - start;
    assert e.block.timestamp > stop => delta == stop - start;
}

createStreamCorrectness

Last update 29/04/2022
verified

Description

createStream() succeeds if parameters are valid

Pseudo formula

{
            createStreamParamCheck(params) == true
}
<
            createStream(params)
>
{
            !lastReverted
}

CVL CODE

rule createStreamCorrectness(address recipient, uint256 deposit, address tokenAddress, 
    uint256 startTime, uint256 stopTime) {
    env e;
    require e.msg.value == 0;
    bool paramCheck = createStreamParamCheck(recipient, startTime, stopTime, deposit, e.msg.sender, e.block.timestamp);
    createStream@withrevert(e, recipient, deposit, tokenAddress, startTime, stopTime);
    assert lastReverted <=> !paramCheck;
}

noStreamAfterCancel

Last update 29/04/2022
verified

Description

after cancelStream() is called, stream is deleted

Pseudo formula

{
            stream.isEntity == true
}
<
            cancelStream(stream)
>
{
            stream.isEntity == false
}

CVL CODE

rule noStreamAfterCancel(uint256 streamId) {
    env e;
    require getStreamExists(streamId);
    cancelStream(e, streamId);
    assert !getStreamExists(streamId);
}

zeroRemainingBalanceDeleted

Last update 29/04/2022
verified

Description

Stream's remaining balance after any operation

Pseudo formula

{
    getStreamRemainingBalance(streamId) > 0
}
<
    f(e, args)
>
{
    getStreamRemainingBalance(streamId) > 0
}

CVL CODE

rule zeroRemainingBalanceDeleted(method f, uint256 streamId) {
    env e;
    calldataarg args;

    uint256 balanceBefore = getStreamRemainingBalance(streamId);
    require balanceBefore > 0;

    f(e, args);

    uint256 balanceAfter = getStreamRemainingBalance(streamId);
    assert balanceAfter > 0;

}

withdrawAvailable

Last update 29/04/2022
verified

Description

If withdraw is available for one stream, it's also available for another stream, provided treasury balance is sufficient. This is a way to check that withdrawal is available.

Pseudo formula

{
            amount1 <= balanceOf(stream1, msg.sender)
            amount2 <= balanceOf(stream2, msg.sender)
            tokenBalance = token.balanceOf(currentContract)
}
<
            withdrawFromStream(stream1, amount1) without revert
            withdrawFromStream(stream2, amount2) at init
>
{
            lastReverted => tokenBalance < amount2
}

CVL CODE

rule withdrawAvailable(uint256 stream1, uint256 stream2, uint256 amount1, uint256 amount2 ) {
    env e1;
    env e2;
    storage init = lastStorage;
    uint256 tokenBalance = _asset.balanceOf(currentContract);
    require currentContract != e1.msg.sender && currentContract != e2.msg.sender;
    withdrawFromStream(e1, stream1, amount1);
    require getStreamExists(stream2);
    require e2.msg.sender == getStreamRecipient(stream2) && e2.msg.sender != 0;
    uint256 balanceRecipient2 = balanceOf(e2, stream2, e2.msg.sender);
    require balanceRecipient2 <= getStreamDeposit(stream2);
    require amount2 <= balanceRecipient2 && amount2 > 0;
    require to_mathint(amount2) + to_mathint(_asset.balanceOf(e2.msg.sender)) < max_uint256;
    withdrawFromStream@withrevert(e2, stream2, amount2) at init;
    uint256 tokenBalanceAfter2 = _asset.balanceOf(currentContract);
    assert lastReverted => tokenBalance < amount2;
}

treasuryBalanceCorrectness

Last update 29/04/2022
verified

Description

Treasury balance can decrease appropriately only on withdrawFromStream and cancelStream()

Pseudo formula

{
            treasuryBalanceBefore = token.balanceOf(currentContract)
            recipientBalance = balanceOf(stream, msg.sender)
            amount <= recipientBalance
}
<
            withdrawFromStream(stream, amount) or cancelStream(stream)
>
{
           token.balanceOf(currentContract) - treasuryBalanceBefore <= recipientBalance
}

CVL CODE

rule treasuryBalanceCorrectness(method f, uint256 streamId) {
    env e;

    streamingTreasuryFunctions(f);
    require getStreamRecipient(streamId) == e.msg.sender;
    uint256 treasuryBalanceBefore = _asset.balanceOf(currentContract);
    uint256 recipientBalanceBefore = balanceOf(e, streamId, e.msg.sender);

    if (f.selector == withdrawFromStream(uint256, uint256).selector) {
        uint256 amount;
        withdrawFromStream(e, streamId, amount);
    } else if (f.selector == cancelStream(uint256).selector) {
        cancelStream(e, streamId);
    } else {

        calldataarg args;
        f(e, args);
    }

    uint256 treasuryBalanceAfter = _asset.balanceOf(currentContract);

    assert treasuryBalanceBefore - treasuryBalanceAfter <= recipientBalanceBefore;
}

onlyFundAdminCanCreate

Last update 29/04/2022
verified

Description

Only fundAdmin may call createStream() successfully

Pseudo formula

<
    createStream(e, args)
>
{
    reverted = lastReverted
    !reverted => e.msg.sender == getFundsAdmin()
}

CVL CODE

rule onlyFundAdminCanCreate(address recipient, uint256 deposit, address token, uint256 start, uint256 end) {
    env e;

    createStream@withrevert(e, recipient, deposit, token, start, end);
    bool reverted = lastReverted;
    assert !reverted => e.msg.sender == getFundsAdmin();

}