Aave Dashboard

12

Contracts

119

Rules

109/119

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();

}

OptimismBridgeExecutor, ArbitrumBridgeExecutor, PolygonBridgeExecutor

Last update 10/07/2022
verified

Description

The _delay variable should always have a proper value, between the minimum and maximum delay state variables.

Pseudo formula

getMinimumDelay() <= getDelay() ∧ getDelay() <= getMaximumDelay()

CVL CODE

invariant properDelay()
	getMinimumDelay() <= getDelay() && getDelay() <= getMaximumDelay()

actionNotCanceledAndExecuted

Last update 10/07/2022
verified

Description

For any action set in the mapping _actionSets[], its ‘executed’ and ‘canceled’ attributes must never be true at the same time.

Pseudo formula

¬(_actionSets[id].executed ∧ _actionSets[id].canceled)

CVL CODE

invariant actionNotCanceledAndExecuted(uint256 setID)
	! (getActionsSetCanceled(setID) && getActionsSetExecuted(setID))

whoChangedStateVariables

Last update 10/07/2022
verified

Description

Only the contract address can change the state variables of the contract.

Pseudo formula

   {
        delay1 = getDelay();
        period1 = getGracePeriod();
        minDelay1 = getMinimumDelay();
        maxDelay1 = getMaximumDelay();
        guardian1 = getGuardian();
    }
	< call to any contract method f >
    {
        delay2 = getDelay();
        period2 = getGracePeriod();
        minDelay2 = getMinimumDelay();
        maxDelay2 = getMaximumDelay();
        guardian2 = getGuardian();
    
        ¬( delay1 == delay2 ∧
        period1 == period2 ∧
        minDelay1 == minDelay2 ∧
        maxDelay1 == maxDelay2 ∧
        guardian1 == guardian2) 
        =>
        msg.sender == currentContract
    }

CVL CODE

rule whoChangedStateVariables(method f)
{
	env e;
	calldataarg args;
	// State variables before
	uint256 delay1 = getDelay();
	uint256 period1 = getGracePeriod();
	uint256 minDelay1 = getMinimumDelay();
	uint256 maxDelay1 = getMaximumDelay();
	address guardian1 = getGuardian();
	// Call function
	f(e, args);
	// State variables after
	uint256 delay2 = getDelay();
	uint256 period2 = getGracePeriod();
	uint256 minDelay2 = getMinimumDelay();
	uint256 maxDelay2 = getMaximumDelay();
	address guardian2 = getGuardian();

	bool stateChanged = !( delay1 == delay2 &&
		 period1 == period2 &&
		 minDelay1 == minDelay2 &&
		 maxDelay1 == maxDelay2 &&
		 guardian1 == guardian2);

	assert stateChanged => e.msg.sender == currentContract,
		"Someone else changed state variables";
}

queueDoesntModifyStateVariables

Last update 10/07/2022
verified

Description

The queue function must not change the state variables of contract (except _actionsSetCounter).

Pseudo formula

   {
        delay1 = getDelay();
        period1 = getGracePeriod();
        minDelay1 = getMinimumDelay();
        maxDelay1 = getMaximumDelay();
        guardian1 = getGuardian();
    }
	queue(random arguments)
    {
        delay2 = getDelay();
        period2 = getGracePeriod();
        minDelay2 = getMinimumDelay();
        maxDelay2 = getMaximumDelay();
        guardian2 = getGuardian();
    
        delay1 == delay2 ∧
        period1 == period2 ∧
        minDelay1 == minDelay2 ∧
        maxDelay1 == maxDelay2 ∧
        guardian1 == guardian2 
    }

CVL CODE

rule queueDoesntModifyStateVariables()
{
	env e;
	calldataarg args;
	// State variables before
	uint256 delay1 = getDelay();
	uint256 period1 = getGracePeriod();
	uint256 minDelay1 = getMinimumDelay();
	uint256 maxDelay1 = getMaximumDelay();
	address guardian1 = getGuardian();

	// Call queue with one action in the set.
	queue2(e, args);

	// State variables after
	uint256 delay2 = getDelay();
	uint256 period2 = getGracePeriod();
	uint256 minDelay2 = getMinimumDelay();
	uint256 maxDelay2 = getMaximumDelay();
	address guardian2 = getGuardian();

	bool stateIntact =  delay1 == delay2 &&
		 period1 == period2 &&
		 minDelay1 == minDelay2 &&
		 maxDelay1 == maxDelay2 &&
		 guardian1 == guardian2;

	assert stateIntact,
		"_queue changed state variables unexpectedly";
}

queueCannotCancel

Last update 10/07/2022
verified

Description

A call to _queue cannot cancel any actions set.

Pseudo formula

    {
        environment e;
        getCurrentState(ID) at e ≠ canceled;
    }
    
        queue2(random arguments)
    
    {
        getCurrentState(ID) at e ≠ canceled;
    } 

CVL CODE

rule queueCannotCancel()
{
	env e;
	calldataarg args;
	uint256 actionsSetId;

	require getCurrentState(e, actionsSetId) != 2;
		queue(e, args);
	assert getCurrentState(e, actionsSetId) != 2;
}

executeCannotCancel

Last update 10/07/2022
verified

Description

A call to execute cannot cancel any actions set.

Pseudo formula

    {
        environment e
        getCurrentState(e, setCanceled) == 'queued'
        getGuardian() ≠ target contract address
    }
        execute(setCall) at e
    {
        getCurrentState(setCanceled) at e ≠ 'canceled'
    }

CVL CODE

rule executeCannotCancel()
{
	env e;
	calldataarg args;
	uint256 calledSet;
	uint256 canceledSet;

	require getCurrentState(e, canceledSet) != 2;
	require getGuardian() != _mock(e);
	
	execute(e, calledSet);

	assert getCurrentState(e, canceledSet) != 2;
}
Subtitle

We assume the guardian is not a target contract.

noIncarnations

Last update 17/07/2022
verified

Description

An action set ID is never queued twice, after being executed once.

Pseudo formula

{
    environment e 
    environment e2
    environment e3
    actionsSetId = getActionsSetCount()
}
    queue(random arguments) at e
    execute(actionsSetId) at e2
    queue@withrevert(random arguments) at e3
{
    getCurrentState(actionsSetId) at e3 ≠ 'queued'
}

CVL CODE

// First part:
// Prove that an actions set is marked as 'queued'
// After invoking queue2.
rule noIncarnations1()
{
	env e;
	calldataarg args;
	uint256 actionsSetId = getActionsSetCount();
	require actionsSetId < max_uint;
	requireInvariant notCanceledNotExecuted(actionsSetId);
	queue2(e, args);
	assert getCurrentState(e, actionsSetId) == 0
	&& actionsSetId < getActionsSetCount();
}

// Second part:
// Given the first part, after execute of that set,
// the same set cannot be marked as 'queued'.
rule noIncarnations2(uint256 actionsSetId)
{
	env e;
	execute(e, actionsSetId);
	assert getCurrentState(e, actionsSetId) != 0;
}

// Third part:
// Given the second part, while an action set is not marked
// as 'queued', calling queue2 with any arguments
// cannot set the same set to 'queued' again.
rule noIncarnations3(uint256 actionsSetId)
{
	env e;
	calldataarg args;
	require actionsSetId <= getActionsSetCount();
	require getCurrentState(e, actionsSetId) != 0;
	queue2(e, args);
	assert getCurrentState(e, actionsSetId) != 0;
}
Subtitle

Verified by dividing to three separate sequential rules. Rule #2 relies on the validity of rule #1 and rule #3 relies on the validity of rule #2.

executedForever

Last update 10/07/2022
verified

Description

Once executed, an actions set ID remains executed forever.

Pseudo formula

    {
        environment e
        environment e2
        getCurrentState(actionsSetId) at e == 'executed'
    }   
	< call to any contract method f>
    {
        getCurrentState(actionsSetId) at e2 == 'executed'
    }

CVL CODE

rule executedForever(method f, uint256 actionsSetId)
{
	env e; env e2;
	calldataarg args;
	require getCurrentState(e, actionsSetId) == 1;
		f(e, args);
	assert getCurrentState(e2, actionsSetId) == 1;
} 

canceledForever

Last update 10/07/2022
verified

Description

Once canceled, an actions set ID remains canceled forever.

Pseudo formula

    {
        environment e
        environment e2
        getCurrentState(actionsSetId) at e == 'canceled'
    }   
	< call to any contract method f>
    {
        getCurrentState(actionsSetId) at e2 == 'canceled'
    }

CVL CODE

rule canceledForever(method f, uint256 actionsSetId)
{
	env e; env e2;
	calldataarg args;
	require getCurrentState(e, actionsSetId) == 2;
		f(e, args);
	assert getCurrentState(e2, actionsSetId) == 2;
}

expiredForever

Last update 10/07/2022
verified

Description

Once expired, an actions set ID remains expired forever.

Pseudo formula

    {
        environment e
        environment e2
        getCurrentState(actionsSetId) at e == 'expired'
    }   
	< call to any contract method f>
    {
        getCurrentState(actionsSetId) at e2 == 'expired'
    }

CVL CODE

rule expiredForever(method f, uint256 actionsSetId)
{
	env e; env e2;
	calldataarg args;
	require getCurrentState(e, actionsSetId) == 3;
	require e.block.timestamp <= e2.block.timestamp;
	 
	if (f.selector == updateGracePeriod(uint256).selector) {
		uint256 oldPeriod = getGracePeriod();
		updateGracePeriod(e, args);
		uint256 newPeriod = getGracePeriod();
		assert newPeriod <= oldPeriod =>
		getCurrentState(e2, actionsSetId) == 3;
	}
	else {
		f(e, args);
		assert getCurrentState(e2, actionsSetId) == 3;
	}	
} 
Subtitle

Upon a call to updateGracePeriod(uint256), an actionSet becomes ‘queued’ again, but this is an expected behavior. For any other function call, an expired set remains so.

queuedStateConsistency

Last update 10/07/2022
verified

Description

After calling to queue, the new action set state must be ‘queued’.

Pseudo formula

{
    environment e
    ID = getActionsSetCount()
}
    queue(random arguments)
{
    getCurrentState(ID) at e == 'queued'
}

CVL CODE

rule queuedStateConsistency()
{
	env e;
	calldataarg args;
	uint256 id = getActionsSetCount();
	requireInvariant notCanceledNotExecuted(id);
	queue2(e, args);
	assert getCurrentState(e, id) == 0;
}

queuedChangedCounter

Last update 10/07/2022
verified

Description

Queue must increase action counter set by 1.

Pseudo formula

{
    count1 = getActionsSetCount() < uint256.max
}
    queue(random arguments)
{
    count2 = getActionsSetCount()
    count2 == count1+1
}

CVL CODE

rule queuedChangedCounter()
{
	env e;
	calldataarg args;
	uint256 count1 = getActionsSetCount();
		queue2(e, args);
	uint256 count2 = getActionsSetCount();

	assert count1 < max_uint => count2 == count1+1;
}
Subtitle

Assuming no overflow for actionsSetCount

onlyCancelCanCancel

Last update 10/07/2022
verified

Description

Only cancel(uint256) function can cancel a queued set.

Pseudo formula

{
    getCurrentState(actionsSetId) == 'queued'
    getGuardian() ≠ target contract address
}
    < call to any contract method f>
{
    getCurrentState(actionsSetId) == 'canceled' 
    =>
    f.selector == cancel(uint256)
}

CVL CODE

rule onlyCancelCanCancel(method f, uint actionsSetId)
{
	env e;
	calldataarg args;
	require getGuardian() != _mock(e);
	require getCurrentState(e, actionsSetId) != 2;

		f(e, args);

	assert getCurrentState(e, actionsSetId) == 2
			=> f.selector == cancel(uint256).selector;
}
Subtitle

We assume the guardian is not a target contract.

cancelExclusive

Last update 10/07/2022
verified

Description

cancel(uint256) only cancels one action set.

Pseudo formula

    {
	environment e;
	stateBefore = getCurrentState(actionsSetId2) at e
    }
    
        cancel(actionsSetId1) at e
    
    {
        stateAfter = getCurrentState(actionsSetId2) at e
	
        actionsSetId1 ≠ actionsSetId2 => stateBefore == stateAfter
    }

CVL CODE

rule cancelExclusive(uint actionsSetId1, uint actionsSetId2)
{
	env e;
	uint8 stateBefore = getCurrentState(e, actionsSetId2);
		cancel(e, actionsSetId1);
	uint8 stateAfter = getCurrentState(e, actionsSetId2);

	assert actionsSetId1 != actionsSetId2 => stateBefore == stateAfter;
}

holdYourHorses

Last update 10/07/2022
verified

Description

When a delay is defined, a queued action set cannot be executed immediately.

Pseudo formula

{
    environment e
    actionsSetId = getActionsSetCount()
    delay = getDelay()
}
    queue(random arguments) at e
    execute@withrevert(actionsSetId) at e
{
    delay > 0 => last reverted
}

CVL CODE

rule holdYourHorses()
{
	env e;
	calldataarg args;
	uint256 actionsSetId = getActionsSetCount();
	
	uint256 delay = getDelay();
	queue2(e, args);
	execute@withrevert(e, actionsSetId);
	assert delay > 0 => lastReverted;
}

executedValidTransition1

Last update 10/07/2022
verified

Description

An action set cannot transform from ‘queued’ to ‘executed’ by a function different than execute(uint256).

Pseudo formula

{
    environment e
    state1 = getCurrentState(actionsSetId) at e
}
    < call to any contract method f ≠ execute(uint256) > 
{
    state2 = getCurrentState(actionsSetId) at e
    
    ¬(state1 == 'queued' ∧ state2 == 'executed')
}

CVL CODE

rule executedValidTransition1(method f, uint256 actionsSetId)
filtered{f -> !f.isView}
{
	env e;
	calldataarg args;
	uint8 state1 = getCurrentState(e, actionsSetId);
		f(e, args);
	uint8 state2 = getCurrentState(e, actionsSetId);

	assert f.selector != execute(uint256).selector =>
	! (state1 == 0 && state2 == 1);
}

executedValidTransition2

Last update 10/07/2022
verified

Description

If an action set was executed, then this set (and only it) must change from ‘queued’ to ‘executed’.

Pseudo formula

{
    environment e
    state1 = getCurrentState(actionsSetId) at e
}
    execute(actionsSetId2) at e
{
    state2 = getCurrentState(actionsSetId) at e
    
    actionsSetId2 == actionsSetId <=> 
    state1 == 'queued' ∧ state2 == 'executed'
}

CVL CODE

rule executedValidTransition2(uint256 actionsSetId)
{
	env e;
	uint actionsSetId2;
	uint8 state1 = getCurrentState(e, actionsSetId);
		execute(e, actionsSetId2);
	uint8 state2 = getCurrentState(e, actionsSetId);

	assert actionsSetId2 == actionsSetId <=> state1 == 0 && state2 == 1;
}

independentQueuedActions

Last update 15/07/2022
failure

Description

Two action sets in different blocks should be queued successfully even if the actions are identical.

Pseudo formula

{
    environment e1
    environment e2
    enviornment e3
    e1.msg.sender == e3.msg.sender
    e1.block.timestamp < e3.block.timestamp
    queue(random arguments) at e3 doesn't revert
}
    queue(same random arguments) at e1
    < call to a state changing f method > at e2
    queue@withrevert(same random arguments) at e3
{
    ¬lastReverted
}

CVL CODE

rule independentQueuedActions(method f)
filtered{f -> stateVariableUpdate(f)}
{
	env e1; env e2; env e3;
	calldataarg args;
	calldataarg argsUpdate;
	
	// Assume different blocks (block3 later than block1)
	require e1.block.timestamp < e3.block.timestamp;
	require e1.msg.sender == e3.msg.sender;
	require e3.msg.value == 0;
	require e3.block.timestamp + getDelay() < max_uint;

        // Assume queue2 doesn't revert.
	storage initState = lastStorage; 
	queue2(e3, args);

	// queue first set, at storage of before last call to queue2.
	queue2(e1, args) at initState;
	// Call some state variable changing method.
		f(e2, argsUpdate);
	// Try to queue second set, with same arguments.
	queue2@withrevert(e3, args);

	assert !lastReverted;
}

executeRevertsBeforeDelay

Last update 10/07/2022
verified

Description

Cannot execute before delay period passed.

Pseudo formula

{
    environment e
    environment e2
    actionsSetId = getActionsSetCount()
    delay = getDelay()
}
    queue(random arguments) at e
    < call to some state changing function f> at e2
    execute@withrevert(actionsSetId) at e2
{
    e2.block.timestamp < e.block.timestamp + delay => lastReverted
}

CVL CODE

rule executeRevertsBeforeDelay(method f)
filtered{f -> stateVariableUpdate(f)}
{
	env e; 
	env e2;
	calldataarg args;
	calldataarg args2;
	uint256 actionsSetId = getActionsSetCount();
	uint256 delay = getDelay();
	queue2(e, args);

	uint256 execTime1 = getActionsSetExecutionTime(actionsSetId);
		f(e2, args2);
	uint256 execTime2 = getActionsSetExecutionTime(actionsSetId);

	execute@withrevert(e2, actionsSetId);

	assert 
		(e2.block.timestamp < e.block.timestamp + delay => lastReverted)
		&& (execTime2 == execTime1);
}

sameExecutionTimesReverts

Last update 10/07/2022
verified

Description

Two similar actions sets, cannot be queued together even in different blocks, when their execution time is equal.

Pseudo formula

{
    environment e1
    environment e2
    args = calldata random arguments
    t1 = e1.block.timestamp
    t2 = e2.block.timestamp
    t1 < t2
}
    queue(args) at e1
    delay1 = getDelay()
    updateDelay(delay) at e1
    delay2 = getDelay()
    queue@withrevert(args) at e2
{
    t1 + delay1 == t2 + delay2 => lastReverted
}

CVL CODE

rule sameExecutionTimesReverts()
{
	env e1; env e2;
	calldataarg args;
	uint256 delay;
	uint256 t1 = e1.block.timestamp;
	uint256 t2 = e2.block.timestamp;

	// Assume different blocks (block2 later than block1)
	require t1 < t2;

	// queue first set.
	queue2(e1, args);
	// Change the delay period.
	uint256 delay1 = getDelay();
		updateDelay(e1, delay);
	uint256 delay2 = getDelay();
	// Try to queue second set, with same arguments.
	queue2@withrevert(e2, args);

	assert t1 + delay1 == t2 + delay2 => lastReverted;
}
Subtitle

This rule is intended to demonstrate that a change to the delay period between two blocks leads to revert of a second queue() if the transactions are identical and the execution time turns out to be the same.

actionDuplicate

Last update 10/07/2022
verified

Description

queue cannot be called twice with the same arguments.

Pseudo formula

{
    environment e
    args = calldata random arguments
}
    queue(args) at e
    queue@withrevert(args) at e
{
    lastReverted
}

CVL CODE

rule actionDuplicate()
{
	env e; 
	calldataarg args;

	queue2(e, args);
	queue2@withrevert(e, args);
	assert lastReverted;
}

executeFailsIfExpired

Last update 10/07/2022
verified

Description

Execute must fail if the actions set state is expired.

Pseudo formula

{
    environment e
    stateBefore = getCurrentState(actionsSetId) at e
}
    execute@withrevert(actionsSetId) at e
{
    stateBefore == 'expired' => lastReverted
}

CVL CODE

rule executeFailsIfExpired(uint256 actionsSetId)
{
	env e;
	uint8 stateBefore = getCurrentState(e, actionsSetId);
	execute@withrevert(e, actionsSetId);
	bool executeReverted = lastReverted;
	assert stateBefore == 3 => executeReverted;
}

queuePriviliged

Last update 10/07/2022
verified

Description

queue() is a priviliged operation.

Pseudo formula

{
    environment e1
    environment e2
}
    queue(random arguments) at e1
    queue@withrevert(other random arguments) at e2
{
    e1.msg.sender ≠ e2.msg.sender => lastReverted
}

CVL CODE

rule queuePriviliged()
{
	env e1;
	env e2;
	calldataarg args1;
	calldataarg args2;
	queue2(e1, args1);
	queue2@withrevert(e2, args2);
	assert e1.msg.sender != e2.msg.sender => lastReverted;
}

cancelPriviliged

Last update 10/07/2022
verified

Description

cancel(uint256) is a priviliged operation

Pseudo formula

{
    environment e1
    environment e2
}
    cancel(random arguments) at e1
    cancel@withrevert(other random arguments) at e2
{
    e1.msg.sender ≠ e2.msg.sender => lastReverted
}

CVL CODE

rule cancelPriviliged()
{
	env e1;
	env e2;
	calldataarg args1;
	calldataarg args2;
	cancel(e1, args1);
	cancel@withrevert(e2, args2);
	assert e1.msg.sender != e2.msg.sender => lastReverted;
}
Last update 10/08/2022
verified

Description

burn operation is additive. This rule was contributed by parth-15 and 0xDatapunk

Pseudo formula

    burn(user, receiverOfUnderlying, amount1, index)
    burn(user, receiverOfUnderlying, amount2, index)
{
    balanceOfUnderlyingTokenAfterSeparate := UNDERLYING_ASSET.balanceOf(receiverOfUnderlying),
    balanceSeparate := balanceOf(user),
    totalSupplySeparate := totalSupply()
}
    ~
    burn(user, receiverOfUnderlying, amount1 + amount2, index)
{
    balanceOfUnderlyingTokenAfterSeparate == UNDERLYING_ASSET.balanceOf(receiverOfUnderlying),
    balanceSeparate == balanceOf(user),
    totalSupplySeparate == totalSupply()
}

CVL CODE

rule burnAdditive(
    address user,
    address receiverOfUnderlying,
    uint256 amount1,
    uint256 amount2,
    uint256 index
) {
    env e;
    storage initialStorage = lastStorage;
    burn(e, user, receiverOfUnderlying, amount1, index);
    burn(e, user, receiverOfUnderlying, amount2, index);
    mathint balanceOfUnderlyingTokenAfterSeparate = UNDERLYING_ASSET.balanceOf(receiverOfUnderlying);
    uint256 balanceSeparate = balanceOf(user);
    mathint totalSupplySeparate = totalSupply();
    burn(e, user, receiverOfUnderlying, amount1 + amount2, index) at initialStorage;
    mathint balanceOfUnderlyingTokenAfterCombined = UNDERLYING_ASSET.balanceOf(receiverOfUnderlying);
    uint256 balanceCombined = balanceOf(user);
    mathint totalSupplyCombined = totalSupply();
    assert balanceOfUnderlyingTokenAfterSeparate == balanceOfUnderlyingTokenAfterCombined;
    assert balanceSeparate == balanceCombined;
    assert totalSupplySeparate == totalSupplyCombined;
}

transferUnderlyingToAdditivity

Last update 10/08/2022
verified

Description

transferUnderlyingTo operation is additive This rule was contributed by 0xDatapunk

Pseudo formula

    transferUnderlyingTo(target, amount1)
    transferUnderlyingTo(target, amount2)

{
    _balance := UNDERLYING_ASSET.balanceOf(target)
}
    ~
    transferUnderlyingTo(target, amount1 + amount2)
{
    _balance == UNDERLYING_ASSET.balanceOf(target)
}

CVL CODE

rule transferUnderlyingToAdditivity(address target, uint256 amount1, uint256 amount2) {
    env e;
    storage init = lastStorage;
    transferUnderlyingTo(e, target, amount1);
    transferUnderlyingTo(e, target, amount2);
    uint256 _balance = UNDERLYING_ASSET.balanceOf(target);
    transferUnderlyingTo(e, target, amount1 + amount2) at init;
    uint256 balance_ = UNDERLYING_ASSET.balanceOf(target);
    assert _balance == balance_;
}
Last update 10/08/2022
verified

Description

mint operation is additive This rule was contributed by parth-15 and 0xDatapunk

Pseudo formula

    mint(user, amount1, index)
    mint(user, amount2, index)
{
    balanceOfUnderlyingTokenAfterSeparate := UNDERLYING_ASSET.balanceOf(receiverOfUnderlying),
    balanceSeparate := balanceOf(user),
    totalSupplySeparate := totalSupply()
}
    ~
    mint(user, amount1 + amount2, index)
{
    balanceOfUnderlyingTokenAfterSeparate == UNDERLYING_ASSET.balanceOf(receiverOfUnderlying),
    balanceSeparate == balanceOf(user),
    totalSupplySeparate == totalSupply()
}

CVL CODE

rule mintAdditive(
    address user,
    uint256 amount1,
    uint256 amount2,
    uint256 index
) {
    env e;
    storage initialState = lastStorage;
    mint(e, user, amount1, index);
    mint(e, user, amount2, index);
    mathint balanceOfUnderlyingTokenAfterSeparate = UNDERLYING_ASSET.balanceOf(user);
    uint256 balanceSeparate = balanceOf(user);
    mathint totalSupplySeparate = totalSupply();
    mint(e, user, amount1 + amount2, index) at initialState;
    mathint balanceOfUnderlyingTokenAfterCombined = UNDERLYING_ASSET.balanceOf(user);
    uint256 balanceCombined = balanceOf(user);
    mathint totalSupplyCombined = totalSupply();
    assert balanceOfUnderlyingTokenAfterSeparate == balanceOfUnderlyingTokenAfterCombined;
    assert balanceSeparate == balanceCombined;
    assert totalSupplySeparate == totalSupplyCombined;
}

mintPreservesUnderlyingAsset

Last update 10/08/2022
verified

Description

mint operation do not affect the totalSupply or UserBalanceOfUnderlyingAsset This rule was contributed by parth-15

Pseudo formula

{
    totalSupplyOfUnderlyingAssetBefore := UNDERLYING_ASSET.totalSupply(),
    balanceOfUnderlyingAssetBefore := UNDERLYING_ASSET.balanceOf(user)
}
   mint(user, amount, index)
{
    totalSupplyOfUnderlyingAssetBefore == UNDERLYING_ASSET.totalSupply(),
    balanceOfUnderlyingAssetBefore == UNDERLYING_ASSET.balanceOf(user)
}

CVL CODE

rule mintPreservesUnderlyingAsset(
    address user,
    uint256 amount,
    uint256 index
) {
    env e;
    mathint totalSupplyOfUnderlyingAssetBefore = UNDERLYING_ASSET.totalSupply();
    mathint balanceOfUnderlyingAssetBefore = UNDERLYING_ASSET.balanceOf(user);
    mint(e, user, amount, index);
    mathint totalSupplyOfUnderlyingAssetAfter = UNDERLYING_ASSET.totalSupply();
    mathint balanceOfUnderlyingAssetAfter = UNDERLYING_ASSET.balanceOf(user);
    assert totalSupplyOfUnderlyingAssetAfter == totalSupplyOfUnderlyingAssetBefore;
    assert balanceOfUnderlyingAssetBefore == balanceOfUnderlyingAssetAfter;
}

proportionalBalancesAndTotalSupplies

Last update 10/08/2022
verified

Description

scaledBalance / internalBalance should be always equal to scaledTotalSupply / internalTotalSupply, that is, internalBalance * scaledTotalSupply should be always equal to scaledBalance * internalTotalSupply. Similarly, scaledBalance * totalSupply should be always equal to balance * scaledTotalSupply, and internalBalance * totalSupply should be always equal to balance * internalTotalSuppl. This rule was contributed by fyang1024

Pseudo formula

{
    _ATokenInternalBalance * _ATokenScaledTotalSupply == _ATokenScaledBalance * _ATokenInternalTotalSupply,
    _ATokenScaledBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenScaledTotalSupply,
    _ATokenInternalBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenInternalTotalSupply
}
    
{
    ATokenInternalBalance_ * ATokenScaledTotalSupply_ == ATokenScaledBalance_ * ATokenInternalTotalSupply_,
    ATokenScaledBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenScaledTotalSupply_,
    ATokenInternalBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenInternalTotalSupply_
}

CVL CODE

rule proportionalBalancesAndTotalSupplies(address user) {
    mathint _ATokenInternalBalance = internalBalanceOf(user);
    mathint _ATokenScaledBalance = scaledBalanceOf(user);
    mathint _ATokenBalance = balanceOf(user);
    mathint _ATokenInternalTotalSupply = internalTotalSupply();
    mathint _ATokenScaledTotalSupply = scaledTotalSupply();
    mathint _ATokenTotalSupply = totalSupply();
    require _ATokenInternalBalance * _ATokenScaledTotalSupply == _ATokenScaledBalance * _ATokenInternalTotalSupply;
    require _ATokenScaledBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenScaledTotalSupply;
    require _ATokenInternalBalance * _ATokenTotalSupply == _ATokenBalance * _ATokenInternalTotalSupply;
    env e; calldataarg args; method f;
    f(e, args);
    mathint ATokenInternalBalance_ = internalBalanceOf(user);
    mathint ATokenScaledBalance_ = scaledBalanceOf(user);
    mathint ATokenBalance_ = balanceOf(user);
    mathint ATokenInternalTotalSupply_ = internalTotalSupply();
    mathint ATokenScaledTotalSupply_ = scaledTotalSupply();
    mathint ATokenTotalSupply_ = totalSupply();
    assert ATokenInternalBalance_ * ATokenScaledTotalSupply_ == ATokenScaledBalance_ * ATokenInternalTotalSupply_;
    assert ATokenScaledBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenScaledTotalSupply_;
    assert ATokenInternalBalance_ * ATokenTotalSupply_ == ATokenBalance_ * ATokenInternalTotalSupply_;
}

equivalenceOfMint

Last update 10/08/2022
verified

Description

Minting to RESERVE_TREASURY_ADDRESS and invoking mintToTreasury method should be equivalent. This rule was contributed by fyang1024

Pseudo formula

    mintToTreasury(amount, index) 
{ 
    _ATokenInternalBalance := internalBalanceOf(RESERVE_TREASURY_ADDRESS()),
    _ATokenScaledBalance := scaledBalanceOf(RESERVE_TREASURY_ADDRESS()),
    _ATokenBalance := balanceOf(RESERVE_TREASURY_ADDRESS()),
    _ATokenInternalTotalSupply := internalTotalSupply(),
    _ATokenScaledTotalSupply := scaledTotalSupply(),
    _ATokenTotalSupply := totalSupply()
}
    ~
    mint(RESERVE_TREASURY_ADDRESS(), amount, index)
{
    _ATokenInternalBalance == internalBalanceOf(RESERVE_TREASURY_ADDRESS()),
    _ATokenScaledBalance == scaledBalanceOf(RESERVE_TREASURY_ADDRESS()),
    _ATokenBalance == balanceOf(RESERVE_TREASURY_ADDRESS()),
    _ATokenInternalTotalSupply == internalTotalSupply(),
    _ATokenScaledTotalSupply == scaledTotalSupply(),
    _ATokenTotalSupply == totalSupply()
}

CVL CODE

rule equivalenceOfMint(uint256 amount, uint256 index) {
    env e;
    storage init = lastStorage;
    mintToTreasury(e, amount, index);
    mathint _ATokenInternalBalance = internalBalanceOf(RESERVE_TREASURY_ADDRESS());
    mathint _ATokenScaledBalance = scaledBalanceOf(RESERVE_TREASURY_ADDRESS());
    mathint _ATokenBalance = balanceOf(RESERVE_TREASURY_ADDRESS());
    mathint _ATokenInternalTotalSupply = internalTotalSupply();
    mathint _ATokenScaledTotalSupply = scaledTotalSupply();
    mathint _ATokenTotalSupply = totalSupply();
    mint(e, RESERVE_TREASURY_ADDRESS(), amount, index) at init;
    mathint ATokenInternalBalance_ = internalBalanceOf(RESERVE_TREASURY_ADDRESS());
    mathint ATokenScaledBalance_ = scaledBalanceOf(RESERVE_TREASURY_ADDRESS());
    mathint ATokenBalance_ = balanceOf(RESERVE_TREASURY_ADDRESS());
    mathint ATokenInternalTotalSupply_ = internalTotalSupply();
    mathint ATokenScaledTotalSupply_ = scaledTotalSupply();
    mathint ATokenTotalSupply_ = totalSupply();
    assert _ATokenInternalBalance == ATokenInternalBalance_ &&
            _ATokenScaledBalance == ATokenScaledBalance_ &&
            _ATokenBalance == ATokenBalance_ &&
            _ATokenInternalTotalSupply == ATokenInternalTotalSupply_ &&
            _ATokenScaledTotalSupply == ATokenScaledTotalSupply_ &&
            _ATokenTotalSupply == ATokenTotalSupply_;
}

burnNoInterferenece

Last update 10/08/2022
verified

Description

burn operation does not change other user’s balance. This rule was contributed by 0xDatapunk

Pseudo formula

{
    _balance := balanceOf(user2),
    _underlyingBalance := UNDERLYING_ASSET.balanceOf(receiverOfUnderlying2)

}
    burn(user1, receiverOfUnderlying, amount, index)
{
    _balance == balanceOf(user2),
    _underlyingBalance == UNDERLYING_ASSET.balanceOf(receiverOfUnderlying2)
}

CVL CODE

rule burnNoInterfernece(address user1, address user2, address receiverOfUnderlying, address receiverOfUnderlying2,
    uint256 amount, uint256 index, uint256 stEthRebasingIndex, uint256 aaveLiquidityIndex)
{
    env e;
    // for onlyLendingPool modifier
    require e.msg.sender == LENDING_POOL;
    uint256 _balance = balanceOf(user2);
    uint256 _underlyingBalance = UNDERLYING_ASSET.balanceOf(receiverOfUnderlying2);
    burn(e, user1, receiverOfUnderlying, amount, index);
    uint256 balance_ = balanceOf(user2);
    uint256 underlyingBalance_ = UNDERLYING_ASSET.balanceOf(receiverOfUnderlying2);

    assert user1!=user2 => _balance==balance_;
    assert receiverOfUnderlying!=receiverOfUnderlying2 && receiverOfUnderlying2!=currentContract =>  _underlyingBalance==underlyingBalance_;
}

integrityOfTransferOnLiquidation

Last update 10/08/2022
verified

Description

When invoking transferOnLiquidation() The balance of a receiver should increase and the balance of a sender should decrease This rule was contributed by fyang1024

Pseudo formula

{
    totalSupplyBefore := totalSupply(),
    balanceOfSenderBefore := balanceOf(sender),
    balanceOfReceiverBefore := balanceOf(receiver),

}
    transferOnLiquidation(sender, receiver, amount)
{
    assert e.msg.sender == LENDING_POOL,
    assert amount != 0 => balanceOfSenderAfter < balanceOfSenderBefore,
    assert amount != 0 => balanceOfReceiverAfter > balanceOfReceiverBefore,
    assert totalSupplyAfter == totalSupplyBefore
}

CVL CODE

rule integrityOfTransferOnLiquidation(address sender, address receiver, uint256 amount) {
    require sender != receiver;
    mathint totalSupplyBefore = totalSupply();
    mathint balanceOfSenderBefore = balanceOf(sender);
    mathint balanceOfReceiverBefore = balanceOf(receiver);
    env e;
    transferOnLiquidation(e, sender, receiver, amount);
    mathint totalSupplyAfter = totalSupply();
    mathint balanceOfSenderAfter = balanceOf(sender);
    mathint balanceOfReceiverAfter = balanceOf(receiver);
    assert e.msg.sender == LENDING_POOL;
    assert amount != 0 => balanceOfSenderAfter < balanceOfSenderBefore;
    assert amount != 0 => balanceOfReceiverAfter > balanceOfReceiverBefore;
    assert totalSupplyAfter == totalSupplyBefore;
}

integrityOfTransferUnderlyingTo

Last update 10/08/2022
verified

Description

The balance of a reciver in TransferUnderlyingTo() should increase by amount and the balance of a sender in TransferUnderlyingTo() should decrease by amount.

Pseudo formula

{
    user != currentContract,
    userBalanceBefore := UNDERLYING_ASSET.balanceOf(user),
    totalSupplyBefore :=  UNDERLYING_ASSET.balanceOf(currentContract)
}
    amountTransfered := transferUnderlyingTo(user, amount)
{
    UNDERLYING_ASSET.balanceOf(user) = userBalanceBefore + amountTransfered,
    UNDERLYING_ASSET.balanceOf(currentContract) = totalSupplyBefore - amountTransfered
}

CVL CODE

rule integrityOfTransferUnderlyingTo(address user, uint256 amount) {
    env e;
    require user != currentContract;
    mathint totalSupplyBefore = UNDERLYING_ASSET.balanceOf(currentContract);
    mathint userBalanceBefore = UNDERLYING_ASSET.balanceOf(user);
    uint256 amountTransfered = transferUnderlyingTo(e, user, amount);
    mathint totalSupplyAfter = UNDERLYING_ASSET.balanceOf(currentContract);
    mathint userBalanceAfter = UNDERLYING_ASSET.balanceOf(user);
    assert userBalanceAfter == userBalanceBefore + amountTransfered;
    assert totalSupplyAfter == totalSupplyBefore - amountTransfered;
}

monotonicityOfMint

Last update 10/08/2022
verified

Description

Minting AStETH must increase the AStETH totalSupply and user’s balance

Pseudo formula

{
    ATokenInternalBalanceBefore := internalBalanceOf(user),
    ATokenScaledBalanceBefore := scaledBalanceOf(user),
    ATokenBalanceBefore := balanceOf(user),
    ATokenInternalTotalSupplyBefore := internalTotalSupply(),
    ATokenScaledTotalSupplyBefore := scaledTotalSupply(),
    ATokenTotalSupplyBefore := totalSupply()
}   
    mint(user, amount, index)
{
    ATokenInternalBalanceBefore < internalBalanceOf(user),
    ATokenScaledBalanceBefore < scaledBalanceOf(user),
    ATokenBalanceBefore < balanceOf(user),
    ATokenInternalTotalSupplyBefore < internalTotalSupply(),
    ATokenScaledTotalSupplyBefore < scaledTotalSupply(),
    ATokenTotalSupplyBefore < totalSupply()
}

CVL CODE

rule monotonicityOfMint(address user, uint256 amount, uint256 index) {
	env e;
    mathint _ATokenInternalBalance = internalBalanceOf(user);
    mathint _ATokenScaledBalance = scaledBalanceOf(user);
    mathint _ATokenBalance = balanceOf(user);
    mathint _ATokenInternalTotalSupply = internalTotalSupply();
    mathint _ATokenScaledTotalSupply = scaledTotalSupply();
    mathint _ATokenTotalSupply = totalSupply();
    
    mint(e, user, amount, index);
    
    mathint ATokenInternalBalance_ = internalBalanceOf(user);
    mathint ATokenScaledBalance_ = scaledBalanceOf(user);
    mathint ATokenBalance_ = balanceOf(user);
    mathint ATokenInternalTotalSupply_ = internalTotalSupply();
    mathint ATokenScaledTotalSupply_ = scaledTotalSupply();
    mathint ATokenTotalSupply_ = totalSupply();
    
    assert _ATokenInternalBalance < ATokenInternalBalance_;
    assert _ATokenScaledBalance < ATokenScaledBalance_;
    assert _ATokenBalance < ATokenBalance_;
    assert _ATokenInternalTotalSupply < ATokenInternalTotalSupply_;
    assert _ATokenScaledTotalSupply < ATokenScaledTotalSupply_;
    assert _ATokenTotalSupply < ATokenTotalSupply_;
}

monotonicityOfBurn

Last update 10/08/2022
verified

Description

Burning AStETH must decrease the AStETH totalSupply and user’s balance. It should also not decrease reciver’s underlying asset.

Pseudo formula

{
    ATokenInternalBalanceBefore := internalBalanceOf(user),
    ATokenScaledBalanceBefore := scaledBalanceOf(user),
    ATokenBalanceBefore := balanceOf(user),
    ATokenInternalTotalSupplyBefore := internalTotalSupply(),
    ATokenScaledTotalSupplyBefore := scaledTotalSupply(),
    ATokenTotalSupplyBefore := totalSupply(),
    underlyingReciverBalance := UNDERLYING_ASSET.balanceOf(reciver)
}   
    burn(user, reciver, amount, index) 
{
    ATokenInternalBalanceBefore > internalBalanceOf(user),
    ATokenScaledBalanceBefore > scaledBalanceOf(user),
    ATokenBalanceBefore > balanceOf(user),
    ATokenInternalTotalSupplyBefore > internalTotalSupply(),
    ATokenScaledTotalSupplyBefore > scaledTotalSupply(),
    ATokenTotalSupplyBefore > totalSupply(),
    underlyingReciverBalanceBefore <= UNDERLYING_ASSET.balanceOf(reciver)
}

CVL CODE

rule monotonicityOfBurn(address user, address reciver, uint256 amount, uint256 index) {
	env e;
    mathint _ATokenInternalBalance = internalBalanceOf(user);
    mathint _ATokenScaledBalance = scaledBalanceOf(user);
    mathint _ATokenBalance = balanceOf(user);
    mathint _ATokenInternalTotalSupply = internalTotalSupply();
    mathint _ATokenScaledTotalSupply = scaledTotalSupply();
    mathint _ATokenTotalSupply = totalSupply();
    mathint _underlyingReciverBalance = UNDERLYING_ASSET.balanceOf(reciver);
    
    burn(e, user, reciver, amount, index);
    
    mathint ATokenInternalBalance_ = internalBalanceOf(user);
    mathint ATokenScaledBalance_ = scaledBalanceOf(user);
    mathint ATokenBalance_ = balanceOf(user);
    mathint ATokenInternalTotalSupply_ = internalTotalSupply();
    mathint ATokenScaledTotalSupply_ = scaledTotalSupply();
    mathint ATokenTotalSupply_ = totalSupply();
    mathint underlyingReciverBalance_ = UNDERLYING_ASSET.balanceOf(reciver);
    
    
    assert _ATokenInternalBalance > ATokenInternalBalance_;
    assert _ATokenScaledBalance > ATokenScaledBalance_;
    assert _ATokenBalance > ATokenBalance_;
    assert _ATokenInternalTotalSupply > ATokenInternalTotalSupply_;
    assert _ATokenScaledTotalSupply > ATokenScaledTotalSupply_;
    assert _ATokenTotalSupply > ATokenTotalSupply_;
    
    assert _underlyingReciverBalance <= underlyingReciverBalance_;
}

mintBurnInvertability

Last update 10/08/2022
verified

Description

Minting and then burning has no effect within the AStETH context.

Pseudo formula

{
    ATokenInternalBalanceBefore := internalBalanceOf(user),
    ATokenScaledBalanceBefore := scaledBalanceOf(user),
    ATokenBalanceBefore := balanceOf(user),
    ATokenInternalTotalSupplyBefore := internalTotalSupply(),
    ATokenScaledTotalSupplyBefore := scaledTotalSupply(),
    ATokenTotalSupplyBefore := totalSupply()

}                                                                      
    mint(user, amount, index)
    burn(user, reciver, amount, index)
{
    ATokenInternalBalanceBefore = internalBalanceOf(user),
    ATokenScaledBalanceBefore = scaledBalanceOf(user),
    ATokenBalanceBefore = balanceOf(user),
    ATokenInternalTotalSupplyBefore = internalTotalSupply(),
    ATokenScaledTotalSupplyBefore = scaledTotalSupply(),
    ATokenTotalSupplyBefore = totalSupply()
}

CVL CODE

rule mintBurnInvertability(address user, uint256 amount, uint256 index, address reciver){
    env e;
    
    mathint _ATokenInternalBalance = internalBalanceOf(user);
    mathint _ATokenScaledBalance = scaledBalanceOf(user);
    mathint _ATokenBalance = balanceOf(user);
    mathint _ATokenInternalTotalSupply = internalTotalSupply();
    mathint _ATokenScaledTotalSupply = scaledTotalSupply();
    mathint _ATokenTotalSupply = totalSupply();
    
    mint(e, user, amount, index);
    burn(e, user, reciver, amount, index);
    
    mathint ATokenInternalBalance_ = internalBalanceOf(user);
    mathint ATokenScaledBalance_ = scaledBalanceOf(user);
    mathint ATokenBalance_ = balanceOf(user);
    mathint ATokenInternalTotalSupply_ = internalTotalSupply();
    mathint ATokenScaledTotalSupply_ = scaledTotalSupply();
    mathint ATokenTotalSupply_ = totalSupply();
    
    assert _ATokenInternalBalance == ATokenInternalBalance_;
    assert _ATokenScaledBalance == ATokenScaledBalance_;
    assert _ATokenBalance == ATokenBalance_;
    assert _ATokenInternalTotalSupply == ATokenInternalTotalSupply_;
    assert _ATokenScaledTotalSupply == ATokenScaledTotalSupply_;
    assert _ATokenTotalSupply == ATokenTotalSupply_;
}

aTokenCantAffectUnderlying

Last update 10/08/2022
verified

Description

AStETH cannot change the totalSupply of the underlying asset

Pseudo formula

{
    underlyingTotalSupply := UNDERLYING_ASSET.totalSupply()
}
    
{
    UNDERLYING_ASSET.totalSupply() = underlyingTotalSupply
}

CVL CODE

rule aTokenCantAffectUnderlying(){
    env e; calldataarg args; method f;
    mathint _underlyingTotalSupply = UNDERLYING_ASSET.totalSupply();
    f(e, args);
    mathint underlyingTotalSupply_ = UNDERLYING_ASSET.totalSupply();
    assert _underlyingTotalSupply == underlyingTotalSupply_;
}

operationAffectMaxTwo

Last update 10/08/2022
verified

Description

Check that each possible operation changes the balance of at most two users

Pseudo formula

{
    ATokenInternalBalance1 := internalBalanceOf(user1),               
    ATokenInternalBalance2 := internalBalanceOf(user2),
    ATokenInternalBalance3 := internalBalanceOf(user3),
    ATokenScaledBalance1 := scaledBalanceOf(user1),
    ATokenScaledBalance2 := scaledBalanceOf(user2),
    ATokenScaledBalance3 := scaledBalanceOf(user3),
    ATokenBalance1 := balanceOf(user1),
    ATokenBalance2 := balanceOf(user2),
    ATokenBalance3 := balanceOf(user3)
}
    
{
    ATokenInternalBalance1 = internalBalanceOf(user1) ∨ ATokenInternalBalance2 = internalBalanceOf(user2) ∨ ATokenInternalBalance3 = internalBalanceOf(user3),
    ATokenScaledBalance1 = scaledBalanceOf(user1) ∨ ATokenScaledBalance2 = scaledBalanceOf(user2) ∨ ATokenScaledBalance3 = scaledBalanceOf(user3),
    ATokenBalance1 = balanceOf(user1) ∨ ATokenBalance2 = balanceOf(user2) ∨ ATokenBalance3 = balanceOf(user3)
}

CVL CODE

rule operationAffectMaxTwo(address user1, address user2, address user3)
{
	env e; calldataarg arg; method f;
	require user1!=user2 && user1!=user3 && user2!=user3;
    mathint _ATokenInternalBalance1 = internalBalanceOf(user1);
    mathint _ATokenInternalBalance2 = internalBalanceOf(user2);
    mathint _ATokenInternalBalance3 = internalBalanceOf(user3);
    mathint _ATokenScaledBalance1 = scaledBalanceOf(user1);
    mathint _ATokenScaledBalance2 = scaledBalanceOf(user2);
    mathint _ATokenScaledBalance3 = scaledBalanceOf(user3);
    mathint _ATokenBalance1 = balanceOf(user1);
    mathint _ATokenBalance2 = balanceOf(user2);
    mathint _ATokenBalance3 = balanceOf(user3);
	
    f(e, arg);
    mathint ATokenInternalBalance1_ = internalBalanceOf(user1);
    mathint ATokenInternalBalance2_ = internalBalanceOf(user2);
    mathint ATokenInternalBalance3_ = internalBalanceOf(user3);
    mathint ATokenScaledBalance1_ = scaledBalanceOf(user1);
    mathint ATokenScaledBalance2_ = scaledBalanceOf(user2);
    mathint ATokenScaledBalance3_ = scaledBalanceOf(user3);
    mathint ATokenBalance1_ = balanceOf(user1);
    mathint ATokenBalance2_ = balanceOf(user2);
    mathint ATokenBalance3_ = balanceOf(user3);
	assert (_ATokenInternalBalance1 == ATokenInternalBalance1_ || _ATokenInternalBalance2 == ATokenInternalBalance2_ || _ATokenInternalBalance3 == ATokenInternalBalance3_);
	assert (_ATokenScaledBalance1 == ATokenScaledBalance1_ || _ATokenScaledBalance2 == ATokenScaledBalance2_ || _ATokenScaledBalance3 == ATokenScaledBalance3_);
	assert (_ATokenBalance1 == ATokenBalance1_ || _ATokenBalance2 == ATokenBalance2_ || _ATokenBalance3 == ATokenBalance3_);
}

integrityBalanceOfTotalSupply

Last update 10/08/2022
verified

Description

Check that the changes to total supply are coherent with the changes to balance

Pseudo formula

{
    ATokenInternalBalance1 := internalBalanceOf(user1),               
    ATokenInternalBalance2 := internalBalanceOf(user2),
    ATokenScaledBalance1 := scaledBalanceOf(user1),
    ATokenScaledBalance2 := scaledBalanceOf(user2),
    ATokenBalance1 := balanceOf(user1),
    ATokenBalance2 := balanceOf(user2),
    ATokenInternalTotalSupply = internalTotalSupply(),
    ATokenScaledTotalSupply = scaledTotalSupply(),
    ATokenTotalSupply = totalSupply()
}
    
{
    ATokenInternalBalance1 ≠ internalBalanceOf(user1) ∧ ATokenInternalBalance2 ≠ internalBalanceOf(user2) ⇒ (internalBalanceOf(user1) - ATokenInternalBalance1) + (internalBalanceOf(user2) - ATokenInternalBalance2) = (internalTotalSupply() - ATokenInternalTotalSupply),
    ATokenScaledBalance1 ≠ scaledBalanceOf(user1) ∧ ATokenScaledBalance2 ≠ scaledBalanceOf(user2) ⇒ (scaledBalanceOf(user1) - ATokenScaledBalance1) + (scaledBalanceOf(user2) - ATokenScaledBalance2) = (scaledTotalSupply() - ATokenScaledTotalSupply),
    ATokenBalance1 ≠ balanceOf(user1) ∧ ATokenBalance2 ≠ balanceOf(user2) ⇒ (ATokenBalance1 - balanceOf(user1)) + (ATokenBalance2 - balanceOf(user2)) = (totalSupply() - ATokenTotalSupply)

}

CVL CODE

rule integrityBalanceOfTotalSupply(address user1, address user2){
	env e; calldataarg arg; method f;
    require user1 != user2;
	
    mathint _ATokenInternalBalance1 = internalBalanceOf(user1);
    mathint _ATokenInternalBalance2 = internalBalanceOf(user2);
    mathint _ATokenScaledBalance1 = scaledBalanceOf(user1);
    mathint _ATokenScaledBalance2 = scaledBalanceOf(user2);
    mathint _ATokenBalance1 = balanceOf(user1);
    mathint _ATokenBalance2 = balanceOf(user2);
    mathint _ATokenInternalTotalSupply = internalTotalSupply();
    mathint _ATokenScaledTotalSupply = scaledTotalSupply();
    mathint _ATokenTotalSupply = totalSupply();
	 
	f(e, arg); 
    mathint ATokenInternalBalance1_ = internalBalanceOf(user1);
    mathint ATokenInternalBalance2_ = internalBalanceOf(user2);
    mathint ATokenScaledBalance1_ = scaledBalanceOf(user1);
    mathint ATokenScaledBalance2_ = scaledBalanceOf(user2);
    mathint ATokenBalance1_ = balanceOf(user1);
    mathint ATokenBalance2_ = balanceOf(user2);
    mathint ATokenInternalTotalSupply_ = internalTotalSupply();
    mathint ATokenScaledTotalSupply_ = scaledTotalSupply();
    mathint ATokenTotalSupply_ = totalSupply();
    assert ((ATokenInternalBalance1_ != _ATokenInternalBalance1) && (ATokenInternalBalance2_ != _ATokenInternalBalance2)) =>
            (ATokenInternalBalance1_ - _ATokenInternalBalance1) + (ATokenInternalBalance2_ - _ATokenInternalBalance2)  == (ATokenInternalTotalSupply_ - _ATokenInternalTotalSupply);
    assert ((ATokenScaledBalance1_ != _ATokenScaledBalance1) && (ATokenScaledBalance2_ != _ATokenScaledBalance2)) =>
            (ATokenScaledBalance1_ - _ATokenScaledBalance1) + (ATokenScaledBalance2_ - _ATokenScaledBalance2)  == (ATokenScaledTotalSupply_ - _ATokenScaledTotalSupply);
    assert ((ATokenBalance1_ != _ATokenBalance1) && (ATokenBalance2_ != _ATokenBalance2)) =>
            (ATokenBalance1_ - _ATokenBalance1) + (ATokenBalance2_ - _ATokenBalance2)  == (ATokenTotalSupply_ - ATokenTotalSupply_);
}

atokenPeggedToUnderlying

Last update 10/08/2022
verified

Description

Checks that the totalSupply of AStETH must be backed by underlying asset in the contract when deposit or withdraw is called

Pseudo formula

{
    _underlyingBalance >= _aTokenTotalSupply
}
    LENDING_POOL.deposit(UNDERLYING_ASSET, amount, user, referralCode);
                                OR
    LENDING_POOL.withdraw(e, UNDERLYING_ASSET, amount, user);
{
    msg.sender ≠ currentContract => underlyingBalance_ >= aTokenTotalSupply_
}

CVL CODE

rule atokenPeggedToUnderlying(env e, uint256 amount, address user, uint16 referralCode){
    uint8 case;
    mathint _underlyingBalance = UNDERLYING_ASSET.balanceOf(currentContract);
    mathint _aTokenTotalSupply = internalTotalSupply();
    require _underlyingBalance >= _aTokenTotalSupply;
    require LENDING_POOL.aToken() == currentContract;
    
    if (case == 0){
        LENDING_POOL.deposit(e, UNDERLYING_ASSET, amount, user, referralCode);
    }
    else if (case == 1){
        LENDING_POOL.withdraw(e, UNDERLYING_ASSET, amount, user);
    }
    
    mathint underlyingBalance_ = UNDERLYING_ASSET.balanceOf(currentContract);
    mathint aTokenTotalSupply_ = internalTotalSupply();
    assert e.msg.sender != currentContract => underlyingBalance_ >= aTokenTotalSupply_;
}

totalSupplyIsSumOfBalances

Last update 10/08/2022
verified

Description

The AStETH totalSupply, tracked by the contract, is the sum of AStETH balances across all users.

Pseudo formula

totalsGhost() == internalTotalSupply()

CVL CODE

invariant totalSupplyIsSumOfBalances()
    totalsGhost() == internalTotalSupply()

totalSupplyGESingleUserBalance

Last update 10/08/2022
verified

Description

The AStETH balance of a single user is less or equal to the total supply Note: for every function that transfers funds between 2 users within the system, we required that the initial sum of balances of the users is less than or equal to totalSupply.

Pseudo formula

totalsGhost() >= internalBalanceOf(user)

CVL CODE

invariant totalSupplyGESingleUserBalance(address user, env e)
    totalsGhost() >= internalBalanceOf(user)
    {
        preserved transferFrom(address spender, address reciever, uint256 amount) with (env e2) {
            require internalBalanceOf(user) + internalBalanceOf(spender) <= totalsGhost();
        }
        preserved transfer(address reciever, uint256 amount) with (env e3) {
            require e3.msg.sender == e.msg.sender;
            require internalBalanceOf(user) + internalBalanceOf(e3.msg.sender) <= totalsGhost();
        }
        preserved transferOnLiquidation(address from, address to, uint256 amount) with (env e4) {
            require internalBalanceOf(user) + internalBalanceOf(from) <= totalsGhost(); 
        }
        preserved burn(address owner, address recieverUnderlying, uint256 amount, uint256 index)  with (env e5) {
            require internalBalanceOf(user) + internalBalanceOf(owner) <= totalsGhost(); 
        }
    }

permitIntegrity

Last update 26/09/2022
verified

Description

Integrity of permit function - successful permit function increases the nonce of owner by 1 and also changes the allowance of owner to spender. Contributed by https://github.com/parth-15

Pseudo formula

    {
        nonceBefore = getNonce(owner)
    }
    <
        permit(owner, spender, value, deadline, v, r, s)
    >
    {
        allowance(owner, spender) == value && getNonce(owner) == nonceBefore + 1
    }

CVL CODE

rule permitIntegrity() {
    env e;
    address owner;
    address spender;
    uint256 value;
    uint256 deadline;
    uint8 v;
    bytes32 r;
    bytes32 s;

    uint256 allowanceBefore = allowance(owner, spender);
    mathint nonceBefore = getNonce(owner);

    //checking this because function is using unchecked math and such a high nonce is unrealistic
    require nonceBefore < max_uint;

    permit(e, owner, spender, value, deadline, v, r, s);

    uint256 allowanceAfter = allowance(owner, spender);
    mathint nonceAfter = getNonce(owner);

    assert allowanceAfter == value, "permit increases allowance of owner to spender on success";
    assert nonceAfter == nonceBefore + 1, "successful call to permit function increases nonce of owner by 1";
}

addressZeroNoPower

Last update 26/09/2022
verified

Description

Address 0 has no voting or proposition power. Contributed by https://github.com/JayP11

Pseudo formula

{
        getPowerCurrent(0, VOTING_POWER) == 0 && getPowerCurrent(0, PROPOSITION_POWER) == && balanceOf(0) == 0
    }

CVL CODE

invariant addressZeroNoPower()
  getPowerCurrent(0, VOTING_POWER()) == 0 && getPowerCurrent(0, PROPOSITION_POWER()) == 0 && balanceOf(0) == 0

metaDelegateByTypeOnlyCallableWithProperlySignedArguments

Last update 26/09/2022
verified

Description

Verify that metaDelegateByType can only be called with a signed request. Contributed by https://github.com/kustosz

Pseudo formula

{
        ecrecover(v,r,s) != delegator
    }
    <
        metaDelegateByType@withrevert(delegator, delegatee, delegationType, deadline, v, r, s)
    >
    {
        lastReverted == true
    }

CVL CODE

rule metaDelegateByTypeOnlyCallableWithProperlySignedArguments(env e, address delegator, address delegatee, uint8 delegationType, uint256 deadline, uint8 v, bytes32 r, bytes32 s) {
    require ecrecoverWrapper(computeMetaDelegateByTypeHash(delegator, delegatee, delegationType, deadline, _nonces(delegator)), v, r, s) != delegator;
    metaDelegateByType@withrevert(e, delegator, delegatee, delegationType, deadline, v, r, s);
    assert lastReverted;
}

metaDelegateNonRepeatable

Last update 26/09/2022
verified

Description

Verify that it’s impossible to use the same arguments to call metaDalegate twice. Contributed by https://github.com/kustosz

Pseudo formula

{
        hash1 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce)
        hash2 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce + 1)
        ecrecover(hash1, v, r, s) == delegator
    }
    <
        metaDelegate(e1, delegator, delegatee, v, r, s)
        metaDelegate@withrevert(e2, delegator, delegatee, delegationType, deadline, v, r, s)
    >
    {
        lastReverted == true
    }

CVL CODE

rule metaDelegateNonRepeatable(env e1, env e2, address delegator, address delegatee, uint256 deadline, uint8 v, bytes32 r, bytes32 s) {
    uint256 nonce = _nonces(delegator);
    bytes32 hash1 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce);
    bytes32 hash2 = computeMetaDelegateHash(delegator, delegatee, deadline, nonce+1);
    // assume no hash collisions
    require hash1 != hash2;
    // assume first call is properly signed
    require ecrecoverWrapper(hash1, v, r, s) == delegator;
    // assume ecrecover is sane: cannot sign two different messages with the same (v,r,s)
    require ecrecoverWrapper(hash2, v, r, s) != ecrecoverWrapper(hash1, v, r, s);
    metaDelegate(e1, delegator, delegatee, deadline, v, r, s);
    metaDelegate@withrevert(e2, delegator, delegatee, deadline, v, r, s);
    assert lastReverted;
}

delegatingToAnotherUserRemovesPowerFromOldDelegatee

Last update 26/09/2022
verified

Description

Power of the previous delegate is removed when the delegatee delegates to another delegate. Contributed by https://github.com/priyankabhanderi

Pseudo formula

{
        _votingBalance = getDelegatedVotingBalance(alice)
    }
    <
        delegateByType(alice, VOTING_POWER)
        delegateByType(bob, VOTING_POWER)
    >
    {
        alice != bob => getDelegatedVotingBalance(alice) == _votingBalance
    }

CVL CODE

rule delegatingToAnotherUserRemovesPowerFromOldDelegatee(env e, address alice, address bob) {

    require e.msg.sender != ZERO_ADDRESS(); 
    require e.msg.sender != alice && e.msg.sender != bob;
    require alice != ZERO_ADDRESS() && bob != ZERO_ADDRESS();

    require getVotingDelegate(e.msg.sender) != alice;

    uint72 _votingBalance = getDelegatedVotingBalance(alice);

    delegateByType(e, alice, VOTING_POWER());

    assert getVotingDelegate(e.msg.sender) == alice;

    delegateByType(e, bob, VOTING_POWER());

    assert getVotingDelegate(e.msg.sender) == bob;
    uint72 votingBalance_ = getDelegatedVotingBalance(alice);
    assert alice != bob => votingBalance_ == _votingBalance;
}
Last update 26/09/2022
verified

Description

Voting and proposition power change only as a result of specific functions. Contributed by https://github.com/top-sekret

Pseudo formula

{
        powerBefore = getPowerCurrent(alice, type)
    }
    <
        f(e, args)
    >
    {
       powerAfter = getPowerCurrent(alice, type)
       powerAfter != powerBefore =>
        f.selector == delegate(address).selector ||
        f.selector == delegateByType(address, uint8).selector ||
        f.selector == metaDelegate(address, address, uint256, uint8, bytes32, bytes32).selector ||
        f.selector == metaDelegateByType(address, address, uint8, uint256, uint8, bytes32, bytes32).selector ||
        f.selector == transfer(address, uint256).selector ||
        f.selector == transferFrom(address, address, uint256).selector
    }

CVL CODE

rule powerChanges(address alice, method f) {
    env e;
    calldataarg args;

    uint8 type;
    require type <= 1;
    uint256 powerBefore = getPowerCurrent(alice, type);

    f(e, args);

    uint256 powerAfter = getPowerCurrent(alice, type);

    assert powerBefore != powerAfter =>
        f.selector == delegate(address).selector ||
        f.selector == delegateByType(address, uint8).selector ||
        f.selector == metaDelegate(address, address, uint256, uint8, bytes32, bytes32).selector ||
        f.selector == metaDelegateByType(address, address, uint8, uint256, uint8, bytes32, bytes32).selector ||
        f.selector == transfer(address, uint256).selector ||
        f.selector == transferFrom(address, address, uint256).selector;
}

delegateIndependence

Last update 26/09/2022
verified

Description

Changing a delegate of one type doesn't influence the delegate of the other type. Written by https://github.com/top-sekret

Pseudo formula

{
        delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender)
    }
    <
        delegateByType(e, delegatee, 1 - type)
    >
    {
       delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender)
       delegateBefore == delegateAfter
    }

CVL CODE

rule delegateIndependence(method f) {
    env e;

    uint8 type;
    require type <= 1;

    address delegateBefore = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender);

    delegateByType(e, _, 1 - type);

    address delegateAfter = type == 1 ? getPropositionDelegate(e.msg.sender) : getVotingDelegate(e.msg.sender);

    assert delegateBefore == delegateAfter;
}

votingPowerChangesWhileNotBeingADelegatee

Last update 26/09/2022
verified

Description

Verifying voting power increases/decreases while not being a voting delegatee yourself.\ Contributed by https://github.com/Zarfsec

Pseudo formula

{
        votingPowerBefore = getPowerCurrent(a, VOTING_POWER)
        balanceBefore = balanceOf(a)
        isVotingDelegatorBefore = getDelegatingVoting(a)
        isVotingDelegateeBefore = getDelegatedVotingBalance(a) != 0
    }
    <
        f(e, args)
    >
    {
        votingPowerAfter = getPowerCurrent(a, VOTING_POWER()
        balanceAfter = getBalance(a)
        isVotingDelegatorAfter = getDelegatingVoting(a);
        isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0

        votingPowerBefore < votingPowerAfter <=> 
        (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) ||
        (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0))
        &&
        votingPowerBefore > votingPowerAfter <=> 
        (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) ||
        (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0))
    }

CVL CODE

rule votingPowerChangesWhileNotBeingADelegatee(address a) {
    require a != 0;

    uint256 votingPowerBefore = getPowerCurrent(a, VOTING_POWER());
    uint256 balanceBefore = getBalance(a);
    bool isVotingDelegatorBefore = getDelegatingVoting(a);
    bool isVotingDelegateeBefore = getDelegatedVotingBalance(a) != 0;

    method f;
    env e;
    calldataarg args;
    f(e, args);

    uint256 votingPowerAfter = getPowerCurrent(a, VOTING_POWER());
    uint256 balanceAfter = getBalance(a);
    bool isVotingDelegatorAfter = getDelegatingVoting(a);
    bool isVotingDelegateeAfter = getDelegatedVotingBalance(a) != 0;

    require !isVotingDelegateeBefore && !isVotingDelegateeAfter;

    /* 
    If you're not a delegatee, your voting power only increases when
        1. You're not delegating and your balance increases
        2. You're delegating and stop delegating and your balanceBefore != 0
    */
    assert votingPowerBefore < votingPowerAfter <=> 
        (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore < balanceAfter)) ||
        (isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore != 0));

    /*
    If you're not a delegatee, your voting power only decreases when
        1. You're not delegating and your balance decreases
        2. You're not delegating and start delegating and your balanceBefore != 0
    */
    assert votingPowerBefore > votingPowerAfter <=> 
        (!isVotingDelegatorBefore && !isVotingDelegatorAfter && (balanceBefore > balanceAfter)) ||
        (!isVotingDelegatorBefore && isVotingDelegatorAfter && (balanceBefore != 0));
}

propositionPowerChangesWhileNotBeingADelegatee

Last update 26/09/2022
verified

Description

Verify that proposition power increases/decreases while not being a voting delegatee yourself. Contributed by https://github.com/Zarfsec

Pseudo formula

    {
        propositionPowerBefore = getPowerCurrent(a, PROPOSITION_POWER)
        balanceBefore = balanceOf(a)
        isPropositionDelegatorBefore = getDelegatingProposition(a)
        isPropositionDelegateeBefore = getDelegatedPropositionBalance(a) != 0
    }
    <
        f(e, args)
    >
    {
        propositionPowerAfter = getPowerCurrent(a, PROPOSITION_POWER()
        balanceAfter = getBalance(a)
        isPropositionDelegatorAfter = getDelegatingProposition(a);
        isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0

        propositionPowerBefore < propositionPowerAfter <=> 
        (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) ||
        (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0))
        &&
        propositionPowerBefore > propositionPowerAfter <=> 
        (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore > balanceAfter)) ||
        (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0))
    }

CVL CODE

rule propositionPowerChangesWhileNotBeingADelegatee(address a) {
    require a != 0;

    uint256 propositionPowerBefore = getPowerCurrent(a, PROPOSITION_POWER());
    uint256 balanceBefore = getBalance(a);
    bool isPropositionDelegatorBefore = getDelegatingProposition(a);
    bool isPropositionDelegateeBefore = getDelegatedPropositionBalance(a) != 0;

    method f;
    env e;
    calldataarg args;
    f(e, args);

    uint256 propositionPowerAfter = getPowerCurrent(a, PROPOSITION_POWER());
    uint256 balanceAfter = getBalance(a);
    bool isPropositionDelegatorAfter = getDelegatingProposition(a);
    bool isPropositionDelegateeAfter = getDelegatedPropositionBalance(a) != 0;

    require !isPropositionDelegateeBefore && !isPropositionDelegateeAfter;

    /*
    If you're not a delegatee, your proposition power only increases when
        1. You're not delegating and your balance increases
        2. You're delegating and stop delegating and your balanceBefore != 0
    */
    assert propositionPowerBefore < propositionPowerAfter <=> 
        (!isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore < balanceAfter)) ||
        (isPropositionDelegatorBefore && !isPropositionDelegatorAfter && (balanceBefore != 0));
    
    /*
    If you're not a delegatee, your proposition power only decreases when
        1. You're not delegating and your balance decreases
        2. You're not delegating and start delegating and your balanceBefore != 0
    */
    assert propositionPowerBefore > propositionPowerAfter <=> 
        (!isPropositionDelegatorBefore && !isPropositionDelegatorBefore && (balanceBefore > balanceAfter)) ||
        (!isPropositionDelegatorBefore && isPropositionDelegatorAfter && (balanceBefore != 0));
}

allowanceStateChange

Last update 26/09/2022
verified

Description

Allowance only changes as a result of specific subset of functions. Contributed by https://github.com/oracleorb

Pseudo formula

    {
        allowanceBefore = allowance(owner, spender)
    }
    <
        f(e, args)
    >
    {
       allowance(owner, spender) != allowanceBefore =>f.selector==approve(address,uint256).selector 
            || f.selector==increaseAllowance(address,uint256).selector
            || f.selector==decreaseAllowance(address,uint256).selector
            || f.selector==transferFrom(address,address,uint256).selector
            || f.selector==permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector

    }

CVL CODE

rule allowanceStateChange(env e){
    address owner;
    address user;
    method f;
    calldataarg args;

    uint256 allowanceBefore=getAllowance(owner,user);
    f(e, args);
    uint256 allowanceAfter=getAllowance(owner,user);

    assert allowanceBefore!=allowanceAfter => f.selector==approve(address,uint256).selector 
    || f.selector==increaseAllowance(address,uint256).selector
    || f.selector==decreaseAllowance(address,uint256).selector
    || f.selector==transferFrom(address,address,uint256).selector
    || f.selector==permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector;
}

delegateCorrectness

Last update 26/09/2022
verified

Description

User’s delegation flag is switched on iff user is delegating to an address other than his own own or 0.

Pseudo formula

    {
        (getVotingDelegate(account) == account || getVotingDelegate(account) == 0) <=> !getDelegatingVoting(account)
        &&
        (getPropositionDelegate(account) == account || getPropositionDelegate(account) == 0) <=> !getDelegatingProposition(account)
    }

CVL CODE

invariant delegateCorrectness(address user)
    ((getVotingDelegate(user) == user || getVotingDelegate(user) == 0) <=> !getDelegatingVoting(user))
    &&
    ((getPropositionDelegate(user) == user || getPropositionDelegate(user) == 0) <=> !getDelegatingProposition(user))
    {
        preserved {
            requireInvariant delegationStateValid(user);
        }
    }

sumOfVBalancesCorrectness

Last update 26/09/2022
verified

Description

Sum of delegated voting balances and undelegated voting balances is equal to total supply

Pseudo formula

  {
        sumDelegatedVotingBalances + sumUndelegatedVotingBalances == totalSupply()
    }

CVL CODE

invariant sumOfVBalancesCorrectness() sumDelegatedBalancesV + sumUndelegatedBalancesV == totalSupply()

sumOfPBalancesCorrectness

Last update 26/09/2022
verified

Description

Sum of delegated proposition balances and undelegated proposition balances is equal to total supply.

Pseudo formula

    {
        sumDelegatedPropositionBalances + sumUndelegatedPropositionBalances == totalSupply()
    }

CVL CODE

invariant sumOfPBalancesCorrectness() sumDelegatedBalancesP + sumUndelegatedBalancesP == totalSupply()

powerWhenNotDelegating

Last update 26/09/2022
verified

Description

If an account is not receiving delegation of power (one type) from anybody, and that account is not delegating that power to anybody, the power of that account must be equal to its token balance.

Pseudo formula

    {
        dvb = _balances[account].delegatedVotingBalance
        votingPower = getPowerCurrent(account, VOTING_POWER)
        (dvb == 0 && !isDelegatingVoting(account)) => votingPower == balanceOf(account)
    }

CVL CODE

rule powerWhenNotDelegating(address account) {
    uint256 balance = balanceOf(account);
    bool isDelegatingVoting = getDelegatingVoting(account);
    bool isDelegatingProposition = getDelegatingProposition(account);
    uint72 dvb = getDelegatedVotingBalance(account);
    uint72 dpb = getDelegatedPropositionBalance(account);

    uint256 votingPower = getPowerCurrent(account, VOTING_POWER());
    uint256 propositionPower = getPowerCurrent(account, PROPOSITION_POWER());

    assert dvb == 0 && !isDelegatingVoting => votingPower == balance;
    assert dpb == 0 && !isDelegatingProposition => propositionPower == balance;
}

vpTransferWhenBothNotDelegating

Last update 26/09/2022
verified

Description

When both accounts are not delegating: On transfer of z amount of tokens from account1 to account2, voting power holds the following properties:

Pseudo formula

   {
       !isDelegatingVoting(account1) && !isDelegatingVoting(account2)
       account1PowerBefore = getPowerCurrent(account1, VOTING_POWER)
       account2PowerBefore = getPowerCurrent(account2, VOTING_POWER)
       account3PowerBefore = getPowerCurrent(account3, VOTING_POWER)
   }
   <
       transferFrom(account1, account2, z)
   >
   {
       getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore - z
       getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore + z
       getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore
   }

CVL CODE

rule vpTransferWhenBothNotDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingVoting = getDelegatingVoting(alice);
    bool isBobDelegatingVoting = getDelegatingVoting(bob);

    // both accounts are not delegating
    require !isAliceDelegatingVoting && !isBobDelegatingVoting;

    uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER());

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER());

    assert alicePowerAfter == alicePowerBefore - amount;
    assert bobPowerAfter == bobPowerBefore + amount;
    assert charliePowerAfter == charliePowerBefore;
}

ppTransferWhenBothNotDelegating

Last update 26/09/2022
verified

Description

When both account1 and account2 are not delegating: On transfer of z amount of tokens from account1 to account2, proposition power holds the following properties:

Pseudo formula

   {
       !isDelegatingProposition(account1) && !isDelegatingProposition(account2)
       account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER)
       account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER)
       account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER)
   }
   <
       transferFrom(account1, account2, z)
   >
   {
       getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore - z
       getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore + z
       getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore
   }

CVL CODE

rule ppTransferWhenBothNotDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingProposition = getDelegatingProposition(alice);
    bool isBobDelegatingProposition = getDelegatingProposition(bob);

    require !isAliceDelegatingProposition && !isBobDelegatingProposition;

    uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER());

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER());

    assert alicePowerAfter == alicePowerBefore - amount;
    assert bobPowerAfter == bobPowerBefore + amount;
    assert charliePowerAfter == charliePowerBefore;
}

vpDelegateWhenBothNotDelegating

Last update 26/09/2022
verified

Description

When both account1 and account2 are not delegating: After account1 will delegate his voting power to account2, the following properties hold:

Pseudo formula

    {
        account1 = e.msg.sender
        !isDelegatingVoting(account1) && !isDelegatingVoting(account2)
        account1PowerBefore = getPowerCurrent(account1, VOTING_POWER)
        account2PowerBefore = getPowerCurrent(account2, VOTING_POWER)
        account3PowerBefore = getPowerCurrent(account3, VOTING_POWER)
    }
    <
        delegate(account2)
    >
    {
        getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore - balanceOf(account1)
        getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore
    }

CVL CODE

rule vpDelegateWhenBothNotDelegating(address alice, address bob, address charlie) {
    env e;
    require alice == e.msg.sender;
    require alice != 0 && bob != 0 && charlie != 0;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingVoting = getDelegatingVoting(alice);
    bool isBobDelegatingVoting = getDelegatingVoting(bob);

    require !isAliceDelegatingVoting && !isBobDelegatingVoting;

    uint256 aliceBalance = balanceOf(alice);
    uint256 bobBalance = balanceOf(bob);

    uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER());

    delegate(e, bob);

    uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER());

    assert alicePowerAfter == alicePowerBefore - aliceBalance;
    assert bobPowerAfter == bobPowerBefore + (aliceBalance / DELEGATED_POWER_DIVIDER()) * DELEGATED_POWER_DIVIDER();
    assert getVotingDelegate(alice) == bob;
    assert charliePowerAfter == charliePowerBefore;
}

ppDelegateWhenBothNotDelegating

Last update 26/09/2022
verified

Description

When both account1 and account2 are not delegating: After account1 will delegate his proposition power to account2, the following properties hold:

Pseudo formula

    {
        account1 = e.msg.sender
        !isDelegatingProposition(account1) && !isDelegatingProposition(account2)
        account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER)
        account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER)
        account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER)
    }
    <
        delegate(account2)
    >
    {
        getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore - balanceOf(account1)
        getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore
    }

CVL CODE

rule ppDelegateWhenBothNotDelegating(address alice, address bob, address charlie) {
    env e;
    require alice == e.msg.sender;
    require alice != 0 && bob != 0 && charlie != 0;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingProposition = getDelegatingProposition(alice);
    bool isBobDelegatingProposition = getDelegatingProposition(bob);

    require !isAliceDelegatingProposition && !isBobDelegatingProposition;

    uint256 aliceBalance = balanceOf(alice);
    uint256 bobBalance = balanceOf(bob);

    uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER());

    delegate(e, bob);

    uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER());

    assert alicePowerAfter == alicePowerBefore - aliceBalance;
    assert bobPowerAfter == bobPowerBefore + (aliceBalance / DELEGATED_POWER_DIVIDER()) * DELEGATED_POWER_DIVIDER();
    assert getPropositionDelegate(alice) == bob;
    assert charliePowerAfter == charliePowerBefore;
}

vpTransferWhenOnlyOneIsDelegating

Last update 26/09/2022
verified

Description

When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: On transfer of z amount of tokens from account1 to account2, the following properties hold

Pseudo formula

    {
        isDelegatingVoting(account1) && !isDelegatingVoting(account2)
        account1PowerBefore = getPowerCurrent(account1, VOTING_POWER)
        account2PowerBefore = getPowerCurrent(account2, VOTING_POWER)
        account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) 
        delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER)
        balanceAccount1Before = balanceOf(account1)
    }
    <
        transferFrom(account1, account2, z)
    >
    {
        getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore == 0
        getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore + z
        getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore
    }

CVL CODE

rule vpTransferWhenOnlyOneIsDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingVoting = getDelegatingVoting(alice);
    bool isBobDelegatingVoting = getDelegatingVoting(bob);
    address aliceDelegate = getVotingDelegate(alice);
    require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != charlie;

    require isAliceDelegatingVoting && !isBobDelegatingVoting;

    uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER());
    // no delegation of anyone to Alice
    require alicePowerBefore == 0;

    uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER());
    uint256 aliceBalanceBefore = balanceOf(alice);

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER());
    uint256 aliceBalanceAfter = balanceOf(alice);

    assert alicePowerBefore == alicePowerAfter;
    assert aliceDelegatePowerAfter == 
        aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + normalize(aliceBalanceAfter);
    assert bobPowerAfter == bobPowerBefore + amount;
    assert charliePowerBefore == charliePowerAfter;
}

ppTransferWhenOnlyOneIsDelegating

Last update 26/09/2022
verified

Description

When account1 is delegating proposition power to delegatee1 and account2 is not delegating proposition power: On transfer of z amount of tokens from account1 to account2, the following properties hold

Pseudo formula

    {
        isDelegatingProposition(account1) && !isDelegatingProposition(account2)
        account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER)
        account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER)
        account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) 
        delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER)
        balanceAccount1Before = balanceOf(account1)
    }
    <
        transferFrom(account1, account2, z)
    >
    {
        getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore == 0
        getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore + z
        getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore
    }

CVL CODE

rule ppTransferWhenOnlyOneIsDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingProposition = getDelegatingProposition(alice);
    bool isBobDelegatingProposition = getDelegatingProposition(bob);
    address aliceDelegate = getPropositionDelegate(alice);
    require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != charlie;

    require isAliceDelegatingProposition && !isBobDelegatingProposition;

    uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER());
    // no delegation of anyone to Alice
    require alicePowerBefore == 0;

    uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());
    uint256 aliceBalanceBefore = balanceOf(alice);

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());
    uint256 aliceBalanceAfter = balanceOf(alice);

    // still zero
    assert alicePowerBefore == alicePowerAfter;
    assert aliceDelegatePowerAfter == 
        aliceDelegatePowerBefore - normalize(aliceBalanceBefore) + normalize(aliceBalanceAfter);
    assert bobPowerAfter == bobPowerBefore + amount;
    assert charliePowerBefore == charliePowerAfter;
}

vpStopDelegatingWhenOnlyOneIsDelegating

Last update 26/09/2022
verified

Description

When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: After account will stop delegating voting power to delegatee1, the following properties hold

Pseudo formula

    {
        account1 == msg.sender && isDelegatingVoting(account1)
        account1PowerBefore = getPowerCurrent(account1, VOTING_POWER)
        account2PowerBefore = getPowerCurrent(account2, VOTING_POWER)
        account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) 
        delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER)
        balanceAccount1Before = balanceOf(account1) 
    }
    <
        delegate(0)    
    >
    {
        getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore + balanceOfAccount1Before
        getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10
        getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore
    }

CVL CODE

rule vpStopDelegatingWhenOnlyOneIsDelegating(address alice, address charlie) {
    env e;
    require alice != charlie;
    require alice == e.msg.sender;

    bool isAliceDelegatingVoting = getDelegatingVoting(alice);
    address aliceDelegate = getVotingDelegate(alice);

    require isAliceDelegatingVoting && aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != charlie;

    uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER());

    delegate(e, 0);

    uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER());

    assert alicePowerAfter == alicePowerBefore + balanceOf(alice);
    assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice));
    assert charliePowerAfter == charliePowerBefore;
}

ppStopDelegatingWhenOnlyOneIsDelegating

Last update 26/09/2022
verified

Description

When account1 is delegating proposition power to delegatee1 and account2 is not delegating proposition power: After account will stop delegating proposition power to delegatee1, the following properties hold

Pseudo formula

    {
        account1 == msg.sender && isDelegatingProposition(account1)
        account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER)
        account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER)
        account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) 
        delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER)
        balanceAccount1Before = balanceOf(account1) 
    }
    <
        delegate(0)    
    >
    {
        getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore + balanceOfAccount1Before
        getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - balanceAccount1Before / 10^10 * 10^10
        getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore
    }

CVL CODE

rule ppStopDelegatingWhenOnlyOneIsDelegating(address alice, address charlie) {
    env e;
    require alice != charlie;
    require alice == e.msg.sender;

    bool isAliceDelegatingProposition = getDelegatingProposition(alice);
    address aliceDelegate = getPropositionDelegate(alice);

    require isAliceDelegatingProposition && aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != charlie;

    uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());

    delegate(e, 0);

    uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());

    assert alicePowerAfter == alicePowerBefore + balanceOf(alice);
    assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice));
    assert charliePowerAfter == charliePowerBefore;
}

vpChangeDelegateWhenOnlyOneIsDelegating

Last update 26/09/2022
verified

Description

When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: After account1 will delegate power to delegatee2, the following properties hold:

Pseudo formula

    {
        account1 == msg.sender && isDelegatingVoting(account1)
        account1PowerBefore = getPowerCurrent(account1, VOTING_POWER)
        account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) 
        delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER)
        delegatee2PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER)
        
    }
    <
        delegate(delegatee2)
    >
    {
        getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore == 0
        getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(delegatee2, VOTING_POWER) == delegatee2PowerBefore + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore
    }

CVL CODE

rule vpChangeDelegateWhenOnlyOneIsDelegating(address alice, address delegate2, address charlie) {
    env e;
    require alice != charlie && alice != delegate2 && charlie != delegate2;
    require alice == e.msg.sender;

    bool isAliceDelegatingVoting = getDelegatingVoting(alice);
    address aliceDelegate = getVotingDelegate(alice);
    require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != delegate2 && 
        delegate2 != 0 && delegate2 != charlie && aliceDelegate != charlie;

    require isAliceDelegatingVoting;

    uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER());
    uint256 delegate2PowerBefore = getPowerCurrent(delegate2, VOTING_POWER());

    delegate(e, delegate2);

    uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER());
    uint256 delegate2PowerAfter = getPowerCurrent(delegate2, VOTING_POWER());
    address aliceDelegateAfter = getVotingDelegate(alice);

    assert alicePowerBefore == alicePowerAfter;
    assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice));
    assert delegate2PowerAfter == delegate2PowerBefore + normalize(balanceOf(alice));
    assert aliceDelegateAfter == delegate2;
    assert charliePowerAfter == charliePowerBefore;
}

ppChangeDelegateWhenOnlyOneIsDelegating

Last update 26/09/2022
verified

Description

When account1 is delegating voting power to delegatee1 and account2 is not delegating voting power: After account1 will delegate power to delegatee2, the following properties hold:

Pseudo formula

    {
        account1 == msg.sender && isDelegatingProposition(account1)
        account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER)
        account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) 
        delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER)
        delegatee2PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER)
        
    }
    <
        delegate(delegatee2)
    >
    {
        getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore == 0
        getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(delegatee2, PROPOSITION_POWER) == delegatee2PowerBefore + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore
    }

CVL CODE

rule ppChangeDelegateWhenOnlyOneIsDelegating(address alice, address delegate2, address charlie) {
    env e;
    require alice != charlie && alice != delegate2 && charlie != delegate2;
    require alice == e.msg.sender;

    bool isAliceDelegatingVoting = getDelegatingProposition(alice);
    address aliceDelegate = getPropositionDelegate(alice);
    require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != delegate2 && 
        delegate2 != 0 && delegate2 != charlie && aliceDelegate != charlie;

    require isAliceDelegatingVoting;

    uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());
    uint256 delegate2PowerBefore = getPowerCurrent(delegate2, PROPOSITION_POWER());

    delegate(e, delegate2);

    uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());
    uint256 delegate2PowerAfter = getPowerCurrent(delegate2, PROPOSITION_POWER());
    address aliceDelegateAfter = getPropositionDelegate(alice);

    assert alicePowerBefore == alicePowerAfter;
    assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(balanceOf(alice));
    assert delegate2PowerAfter == delegate2PowerBefore + normalize(balanceOf(alice));
    assert aliceDelegateAfter == delegate2;
    assert charliePowerAfter == charliePowerBefore;
}

vpOnlyAccount2IsDelegating

Last update 26/09/2022
verified

Description

Account1 not delegating voting power to anybody, account2 is delegating voting power to delegatee2: On transfer of z tokens from account1 to account 2, the following properties hold:

Pseudo formula

    {
        isDelegatingVoting(account1) && isDelegatingVoting(account2)
        delegatee2 == getVotingDelegate(account2)
        account1PowerBefore = getPowerCurrent(account1, VOTING_POWER)
        account3PowerBefore = getPowerCurrent(account3, VOTING_POWER) 
        delegatee2PowerBefore = getPowerCurrent(delegatee2, VOTING_POWER)
        account2BalanceBefore == balanceOf(account2)
    } 
    <
        transferFrom(account1, account2, z)
    >
    {
        getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore - z
        getPowerCurrent(account2, VOTING_POWER) == 0
        getPowerCurrent(delegatee2, VOTING_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 *10^10 + balanceOf(account2) / 10^10 * 10^10
        getPowerCurrent(account3, VOTING_POWER) == account3PowerBefore
    }

CVL CODE

rule vpOnlyAccount2IsDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingVoting = getDelegatingVoting(alice);
    bool isBobDelegatingVoting = getDelegatingVoting(bob);
    address bobDelegate = getVotingDelegate(bob);
    require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie;

    require !isAliceDelegatingVoting && isBobDelegatingVoting;

    uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER());
    require bobPowerBefore == 0;
    uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER());
    uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, VOTING_POWER());
    uint256 bobBalanceBefore = balanceOf(bob);

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER());
    uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, VOTING_POWER());
    uint256 bobBalanceAfter = balanceOf(bob);

    assert alicePowerAfter == alicePowerBefore - amount;
    assert bobPowerAfter == 0;
    assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalize(bobBalanceBefore) + normalize(bobBalanceAfter);

    assert charliePowerAfter == charliePowerBefore;
}

ppOnlyAccount2IsDelegating

Last update 26/09/2022
verified

Description

Account1 not delegating proposition power to anybody, account2 is delegating proposition power to delegatee2: On transfer of z tokens from account1 to account 2, the following properties hold:

Pseudo formula

    {
        isDelegatingProposition(account1) && isDelegatingProposition(account2)
        account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER)
        account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER) 
        delegatee2PowerBefore = getPowerCurrent(delegatee2, PROPOSITION_POWER)
        account2BalanceBefore == balanceOf(account2)
    } 
    <
        transferFrom(account1, account2, z)
    >
    {
        getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore - z
        getPowerCurrent(account2, PROPOSITION_POWER) == 0
        getPowerCurrent(delegatee2, PROPOSITION_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 *10^10 + balanceOf(account2) / 10^10 * 10^10
        getPowerCurrent(account3, PROPOSITION_POWER) == account3PowerBefore
    }

CVL CODE

rule ppOnlyAccount2IsDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegating = getDelegatingProposition(alice);
    bool isBobDelegating = getDelegatingProposition(bob);
    address bobDelegate = getPropositionDelegate(bob);
    require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie;

    require !isAliceDelegating && isBobDelegating;

    uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
    require bobPowerBefore == 0;
    uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, PROPOSITION_POWER());
    uint256 bobBalanceBefore = balanceOf(bob);

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, PROPOSITION_POWER());
    uint256 bobBalanceAfter = balanceOf(bob);

    assert alicePowerAfter == alicePowerBefore - amount;
    assert bobPowerAfter == 0;
    assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalize(bobBalanceBefore) + normalize(bobBalanceAfter);

    assert charliePowerAfter == charliePowerBefore;
}

vpTransferWhenBothAreDelegating

Last update 26/09/2022
verified

Description

Account1 is delegating voting power to delegatee1, account2 is delegating voting power to delegatee2: On transfer of z tokens from account1 to account2, the following properties hold:

Pseudo formula

    {
        isDelegatingVoting(account1) && isDelegatingVoting(account2)
        account1PowerBefore = getPowerCurrent(account1, VOTING_POWER)
        account2PowerBefore = getPowerCurrent(account2, VOTING_POWER)
        account3PowerBefore = getPowerCurrent(account3, VOTING_POWER)
        delegatee1PowerBefore = getPowerCurrent(delegatee1, VOTING_POWER)
        delegatee2PowerBefore = getPowerCurrent(delegatee2, VOTING_POWER)
        account1BalanceBefore = balanceOf(account1)
        account2BalanceBefore = balanceOf(account2)
    }
    <
        transferFrom(account1, account2, z)
    >
    {
        getPowerCurrent(account1, VOTING_POWER) == account1PowerBefore == 0
        getPowerCurrent(account2, VOTING_POWER) == account2PowerBefore == 0
        getPowerCurrent(delegatee1, VOTING_POWER) == delegatee1PowerBefore - account1BalanceBefore / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(delegatee2, VOTING_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 * 10^10 + balanceOf(account2) / 10^10 * 10^10
    }

CVL CODE

rule vpTransferWhenBothAreDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegatingVoting = getDelegatingVoting(alice);
    bool isBobDelegatingVoting = getDelegatingVoting(bob);
    require isAliceDelegatingVoting && isBobDelegatingVoting;
    address aliceDelegate = getVotingDelegate(alice);
    address bobDelegate = getVotingDelegate(bob);
    require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != charlie;
    require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie;
    require aliceDelegate != bobDelegate;

    uint256 alicePowerBefore = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, VOTING_POWER());
    uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, VOTING_POWER());
    uint256 aliceBalanceBefore = balanceOf(alice);
    uint256 bobBalanceBefore = balanceOf(bob);

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, VOTING_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, VOTING_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, VOTING_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, VOTING_POWER());
    uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, VOTING_POWER());
    uint256 aliceBalanceAfter = balanceOf(alice);
    uint256 bobBalanceAfter = balanceOf(bob);

    assert alicePowerAfter == alicePowerBefore;
    assert bobPowerAfter == bobPowerBefore;
    assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(aliceBalanceBefore) 
        + normalize(aliceBalanceAfter);

    uint256 normalizedBalanceBefore = normalize(bobBalanceBefore);
    uint256 normalizedBalanceAfter = normalize(bobBalanceAfter);
    assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalizedBalanceBefore + normalizedBalanceAfter;
}

ppTransferWhenBothAreDelegating

Last update 26/09/2022
verified

Description

Account1 is delegating proposition power to delegatee1, account2 is delegating proposition power to delegatee2: On transfer of z tokens from account1 to account2, the following holds

Pseudo formula

    {
        isDelegatingProposition(account1) && isDelegatingProposition(account2)
        account1PowerBefore = getPowerCurrent(account1, PROPOSITION_POWER)
        account2PowerBefore = getPowerCurrent(account2, PROPOSITION_POWER)
        account3PowerBefore = getPowerCurrent(account3, PROPOSITION_POWER)
        delegatee1PowerBefore = getPowerCurrent(delegatee1, PROPOSITION_POWER)
        delegatee2PowerBefore = getPowerCurrent(delegatee2, PROPOSITION_POWER)
        account1BalanceBefore = balanceOf(account1)
        account2BalanceBefore = balanceOf(account2)
    }
    <
        transferFrom(account1, account2, z)
    >
    {
        getPowerCurrent(account1, PROPOSITION_POWER) == account1PowerBefore == 0
        getPowerCurrent(account2, PROPOSITION_POWER) == account2PowerBefore == 0
        getPowerCurrent(delegatee1, PROPOSITION_POWER) == delegatee1PowerBefore - account1BalanceBefore / 10^10 * 10^10 + balanceOf(account1) / 10^10 * 10^10
        getPowerCurrent(delegatee2, PROPOSITION_POWER) == delegatee2PowerBefore - account2BalanceBefore / 10^10 * 10^10 + balanceOf(account2) / 10^10 * 10^10
    }

CVL CODE

rule ppTransferWhenBothAreDelegating(address alice, address bob, address charlie, uint256 amount) {
    env e;
    require alice != bob && bob != charlie && alice != charlie;

    bool isAliceDelegating = getDelegatingProposition(alice);
    bool isBobDelegating = getDelegatingProposition(bob);
    require isAliceDelegating && isBobDelegating;
    address aliceDelegate = getPropositionDelegate(alice);
    address bobDelegate = getPropositionDelegate(bob);
    require aliceDelegate != alice && aliceDelegate != 0 && aliceDelegate != bob && aliceDelegate != charlie;
    require bobDelegate != bob && bobDelegate != 0 && bobDelegate != alice && bobDelegate != charlie;
    require aliceDelegate != bobDelegate;

    uint256 alicePowerBefore = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerBefore = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerBefore = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());
    uint256 bobDelegatePowerBefore = getPowerCurrent(bobDelegate, PROPOSITION_POWER());
    uint256 aliceBalanceBefore = balanceOf(alice);
    uint256 bobBalanceBefore = balanceOf(bob);

    transferFrom(e, alice, bob, amount);

    uint256 alicePowerAfter = getPowerCurrent(alice, PROPOSITION_POWER());
    uint256 bobPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER());
    uint256 charliePowerAfter = getPowerCurrent(charlie, PROPOSITION_POWER());
    uint256 aliceDelegatePowerAfter = getPowerCurrent(aliceDelegate, PROPOSITION_POWER());
    uint256 bobDelegatePowerAfter = getPowerCurrent(bobDelegate, PROPOSITION_POWER());
    uint256 aliceBalanceAfter = balanceOf(alice);
    uint256 bobBalanceAfter = balanceOf(bob);

    assert alicePowerAfter == alicePowerBefore;
    assert bobPowerAfter == bobPowerBefore;
    assert aliceDelegatePowerAfter == aliceDelegatePowerBefore - normalize(aliceBalanceBefore) 
        + normalize(aliceBalanceAfter);

    uint256 normalizedBalanceBefore = normalize(bobBalanceBefore);
    uint256 normalizedBalanceAfter = normalize(bobBalanceAfter);
    assert bobDelegatePowerAfter == bobDelegatePowerBefore - normalizedBalanceBefore + normalizedBalanceAfter;
}

delegationTypeIndependence

Last update 26/09/2022
verified

Description

Only delegate() and metaDelegate() may change both voting and proposition delegates of an account at once.

Pseudo formula

    {
        delegateVBefore = getVotingDelegate(account)
        delegatePBefore = getPropositionDelegate(account)
    }
    <
        f(e, args)
    >
    {
        delegateVAfter = getVotingDelegate(account)
        delegatePAfter = getPropositionDelegate(account)
        (delegateVBefore == delegateVAfter || delegatePBefore == delegatePAfter) || (f.selector == delegate(address).selector || f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector)
    }

CVL CODE

rule votingDelegateChanges(address alice, method f) {
    env e;
    calldataarg args;

    address aliceVotingDelegateBefore = getVotingDelegate(alice);
    address alicePropDelegateBefore = getPropositionDelegate(alice);

    f(e, args);

    address aliceVotingDelegateAfter = getVotingDelegate(alice);
    address alicePropDelegateAfter = getPropositionDelegate(alice);

    // only these four function may change the delegate of an address
    assert aliceVotingDelegateAfter != aliceVotingDelegateBefore || alicePropDelegateBefore != alicePropDelegateAfter =>
        f.selector == delegate(address).selector || 
        f.selector == delegateByType(address,uint8).selector ||
        f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector ||
        f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector;
}

cantDelegateTwice

Last update 26/09/2022
verified

Description

Delegating twice to the same delegate _delegate changes the delegate’s voting power only once.

Pseudo formula

    {
        votingPowerBefore = getPowerCurrent(_delegate, VOTING_POWER)
        propositionPowerBefore = getPowerCurrent(_delegate, PROPOSITION_POWER)
    }
    <
        delegate(_delegate)
        votingPowerAfter = getPowerCurrent(_delegate, VOTING_POWER)
        propositionPowerAfter = getPowerCurrent(_delegate, PROPOSITION_POWER)
        delegate(_delegate)
    >
    {
        getPowerCurrent(_delegate, VOTING_POWER) == votingPowerAfter
        getPowerCurrent(_delegate, PROPOSITION_POWER) == propositionPowerAfter 
    }

CVL CODE

rule cantDelegateTwice(address _delegate) {
    env e;

    address delegateBeforeV = getVotingDelegate(e.msg.sender);
    address delegateBeforeP = getPropositionDelegate(e.msg.sender);
    require delegateBeforeV != _delegate && delegateBeforeV != e.msg.sender && delegateBeforeV != 0;
    require delegateBeforeP != _delegate && delegateBeforeP != e.msg.sender && delegateBeforeP != 0;
    require _delegate != e.msg.sender && _delegate != 0 && e.msg.sender != 0;
    require getDelegationState(e.msg.sender) == FULL_POWER_DELEGATED();

    uint256 votingPowerBefore = getPowerCurrent(_delegate, VOTING_POWER());
    uint256 propPowerBefore = getPowerCurrent(_delegate, PROPOSITION_POWER());
    
    delegate(e, _delegate);
    
    uint256 votingPowerAfter = getPowerCurrent(_delegate, VOTING_POWER());
    uint256 propPowerAfter = getPowerCurrent(_delegate, PROPOSITION_POWER());

    delegate(e, _delegate);

    uint256 votingPowerAfter2 = getPowerCurrent(_delegate, VOTING_POWER());
    uint256 propPowerAfter2 = getPowerCurrent(_delegate, PROPOSITION_POWER());

    assert votingPowerAfter == votingPowerBefore + normalize(balanceOf(e.msg.sender));
    assert propPowerAfter == propPowerBefore + normalize(balanceOf(e.msg.sender));
    assert votingPowerAfter2 == votingPowerAfter && propPowerAfter2 == propPowerAfter;
}

transferCorrect

Last update 26/09/2022
verified

Description

Token transfer works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0.

Pseudo formula

    {
        balanceFromBefore = balanceOf(msg.sender)
        balanceToBefore = balanceOf(to)
    }
    <
        transfer(to, amount)
    >
    {
        lastReverted => to = 0 || amount > balanceOf(msg.sender)
        !lastReverted => balanceOf(to) = balanceToBefore + amount &&
                        balanceOf(msg.sender) = balanceFromBefore - amount
    }

CVL CODE

rule transferCorrect(address to, uint256 amount) {
    env e;
    require e.msg.value == 0 && e.msg.sender != 0;
    uint256 fromBalanceBefore = balanceOf(e.msg.sender);
    uint256 toBalanceBefore = balanceOf(to);
    require fromBalanceBefore + toBalanceBefore < AAVE_MAX_SUPPLY() / 100;
    
    // proven elsewhere
    address v_delegateTo = getVotingDelegate(to);
    mathint dvbTo = getDelegatedVotingBalance(v_delegateTo);
    require dvbTo >= balanceOf(to) / DELEGATED_POWER_DIVIDER() && 
        dvbTo < SCALED_MAX_SUPPLY() - amount / DELEGATED_POWER_DIVIDER();
    address p_delegateTo = getPropositionDelegate(to);
    mathint pvbTo = getDelegatedPropositionBalance(p_delegateTo);
    require pvbTo >= balanceOf(to) / DELEGATED_POWER_DIVIDER() && 
        pvbTo < SCALED_MAX_SUPPLY() - amount / DELEGATED_POWER_DIVIDER();

    // proven elsewhere
    address v_delegateFrom = getVotingDelegate(e.msg.sender);
    address p_delegateFrom = getPropositionDelegate(e.msg.sender);
    mathint dvbFrom = getDelegatedVotingBalance(v_delegateFrom);
    mathint pvbFrom = getDelegatedPropositionBalance(p_delegateFrom);
    require dvbFrom >= balanceOf(e.msg.sender) / DELEGATED_POWER_DIVIDER();
    require pvbFrom >= balanceOf(e.msg.sender) / DELEGATED_POWER_DIVIDER();

    require validDelegationState(e.msg.sender) && validDelegationState(to);
    require ! ( (getDelegatingVoting(to) && v_delegateTo == to) ||
                (getDelegatingProposition(to) && p_delegateTo == to));
    
    // to not overcomplicate the constraints on dvbTo and dvbFrom
    require v_delegateFrom != v_delegateTo && p_delegateFrom != p_delegateTo;

    transfer@withrevert(e, to, amount);
    bool reverted = lastReverted;
    if (!reverted) {
        if (e.msg.sender == to) {
            assert balanceOf(e.msg.sender) == fromBalanceBefore;
        } else {
            assert balanceOf(e.msg.sender) == fromBalanceBefore - amount;
            assert balanceOf(to) == toBalanceBefore + amount;
        }
    } else {
        assert amount > fromBalanceBefore || to == 0;
    }
}

transferFromCorrect

Last update 26/09/2022
verified

Description

Token transferFrom function works correctly. Balances are updated if not reverted. If reverted then the transfer amount was too high, or the recipient is 0, or the allowance was not sufficient

Pseudo formula

    {
        balanceFromBefore = balanceOf(from)
        balanceToBefore = balanceOf(to)
    }
    <
        transferFrom(from, to, amount)
    >
    {
        lastreverted => to = 0 || amount > balanceOf(from)
        !lastreverted => balanceOf(to) = balanceToBefore + amount &&
                        balanceOf(from) = balanceFromBefore - amount
    }

CVL CODE

rule transferFromCorrect(address from, address to, uint256 amount) {
    env e;
    require e.msg.value == 0;
    uint256 fromBalanceBefore = balanceOf(from);
    uint256 toBalanceBefore = balanceOf(to);
    uint256 allowanceBefore = allowance(from, e.msg.sender);
    require fromBalanceBefore + toBalanceBefore < AAVE_MAX_SUPPLY();

    transferFrom(e, from, to, amount);

    assert from != to =>
        balanceOf(from) == fromBalanceBefore - amount &&
        balanceOf(to) == toBalanceBefore + amount &&
        (allowance(from, e.msg.sender) == allowanceBefore - amount ||
         allowance(from, e.msg.sender) == max_uint256);
}

zeroAddressNoBalance

Last update 26/09/2022
verified

Description

Balance of address 0 is always 0

Pseudo formula

{ balanceOf(0) = 0 }

CVL CODE

invariant ZeroAddressNoBalance()
    balanceOf(0) == 0

NoChangeTotalSupply

Last update 26/09/2022
verified

Description

Contract calls don’t change token total supply.

Pseudo formula

    {
        supplyBefore = totalSupply()
    }
    < f(e, args)>
    {
        supplyAfter = totalSupply()
        supplyBefore == supplyAfter
    }

CVL CODE

rule NoChangeTotalSupply(method f) {
    // require f.selector != burn(uint256).selector && f.selector != mint(address, uint256).selector;
    uint256 totalSupplyBefore = totalSupply();
    env e;
    calldataarg args;
    f(e, args);
    assert totalSupply() == totalSupplyBefore;
}

ChangingAllowance

Last update 26/09/2022
verified

Description

Allowance changes correctly as a result of calls to approve, transfer, increaseAllowance, decreaseAllowance

Pseudo formula

    {
        allowanceBefore = allowance(from, spender)
    }
    <
        f(e, args)
    >
    {
        f.selector = approve(spender, amount) => allowance(from, spender) = amount
        f.selector = transferFrom(from, spender, amount) => allowance(from, spender) = allowanceBefore - amount
        f.selector = decreaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore - delta
        f.selector = increaseAllowance(spender, delta) => allowance(from, spender) = allowanceBefore + delta
        generic f.selector => allowance(from, spender) == allowanceBefore
    }

CVL CODE

rule ChangingAllowance(method f, address from, address spender) {
    uint256 allowanceBefore = allowance(from, spender);
    env e;
    if (f.selector == approve(address, uint256).selector) {
        address spender_;
        uint256 amount;
        approve(e, spender_, amount);
        if (from == e.msg.sender && spender == spender_) {
            assert allowance(from, spender) == amount;
        } else {
            assert allowance(from, spender) == allowanceBefore;
        }
    } else if (f.selector == transferFrom(address,address,uint256).selector) {
        address from_;
        address to;
        address amount;
        transferFrom(e, from_, to, amount);
        uint256 allowanceAfter = allowance(from, spender);
        if (from == from_ && spender == e.msg.sender) {
            assert from == to || allowanceBefore == max_uint256 || allowanceAfter == allowanceBefore - amount;
        } else {
            assert allowance(from, spender) == allowanceBefore;
        }
    } else if (f.selector == decreaseAllowance(address, uint256).selector) {
        address spender_;
        uint256 amount;
        require amount <= allowanceBefore;
        decreaseAllowance(e, spender_, amount);
        if (from == e.msg.sender && spender == spender_) {
            assert allowance(from, spender) == allowanceBefore - amount;
        } else {
            assert allowance(from, spender) == allowanceBefore;
        }
    } else if (f.selector == increaseAllowance(address, uint256).selector) {
        address spender_;
        uint256 amount;
        require amount + allowanceBefore < max_uint256;
        increaseAllowance(e, spender_, amount);
        if (from == e.msg.sender && spender == spender_) {
            assert allowance(from, spender) == allowanceBefore + amount;
        } else {
            assert allowance(from, spender) == allowanceBefore;
        }
    } 
    else
    {
        calldataarg args;
        f(e, args);
        assert allowance(from, spender) == allowanceBefore ||
            f.selector == permit(address,address,uint256,uint256,uint8,bytes32,bytes32).selector;
    }
}

TransferSumOfFromAndToBalancesStaySame

Last update 26/09/2022
verified

Description

Transfer from msg.sender to b doesn’t change the sum of their balances

Pseudo formula

    {
        balancesBefore = balanceOf(msg.sender) + balanceOf(b)
    }
    <
        transfer(b, amount)
    >
    {
        balancesBefore == balanceOf(msg.sender) + balanceOf(b)
    }

CVL CODE

rule TransferSumOfFromAndToBalancesStaySame(address to, uint256 amount) {
    env e;
    mathint sum = balanceOf(e.msg.sender) + balanceOf(to);
    require sum < max_uint256;
    transfer(e, to, amount); 
    assert balanceOf(e.msg.sender) + balanceOf(to) == sum;
}

TransferFromSumOfFromAndToBalancesStaySame

Last update 26/09/2022
verified

Description

transferFrom from a to b doesn’t change the sum of their balances

Pseudo formula

    {
        balancesBefore = balanceOf(a) + balanceOf(b)
    }
    <
        transferFrom(a, b)
    >
    {
        balancesBefore == balanceOf(a) + balanceOf(b)
    }

CVL CODE

rule TransferFromSumOfFromAndToBalancesStaySame(address from, address to, uint256 amount) {
    env e;
    mathint sum = balanceOf(from) + balanceOf(to);
    require sum < max_uint256;
    transferFrom(e, from, to, amount); 
    assert balanceOf(from) + balanceOf(to) == sum;
}

TransferDoesntChangeOtherBalance

Last update 26/09/2022
verified

Description

Transfer from msg.sender to alice doesn’t change the balance of other addresses

Pseudo formula

    {
        balanceBefore = balanceOf(charlie)
    }
    <
        transfer(alice, amount)
    >
    {
        balanceOf(charlie) == balanceBefore
    }

CVL CODE

rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) {
    env e;
    require other != e.msg.sender;
    require other != to && other != currentContract;
    uint256 balanceBefore = balanceOf(other);
    transfer(e, to, amount); 
    assert balanceBefore == balanceOf(other);
}

TransferFromDoesntChangeOtherBalance

Last update 26/09/2022
verified

Description

transferFrom of tokens from alice to bob doesn’t change the balance of other addresses

Pseudo formula

    {
        balanceBefore = balanceOf(charlie)
    }
    <
        transferFrom(alice, bob, amount)
    >
    {
        balanceOf(charlie) = balanceBefore
    }

CVL CODE

rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) {
    env e;
    require other != from;
    require other != to;
    uint256 balanceBefore = balanceOf(other);
    transferFrom(e, from, to, amount); 
    assert balanceBefore == balanceOf(other);
}

OtherBalanceOnlyGoesUp

Last update 26/09/2022
verified

Description

Balance of an address, who is not a sender or a recipient in transfer functions, doesn’t decrease as a result of contract calls

Pseudo formula

   {
        balanceBefore = balanceOf(charlie)
    }
    <
        f(e, args)
    >
    {
        f.selector != transfer && f.selector != transferFrom => balanceOf(charlie) == balanceBefore
    }

CVL CODE

rule OtherBalanceOnlyGoesUp(address other, method f) {
    env e;
    require other != currentContract;
    uint256 balanceBefore = balanceOf(other);

    if (f.selector == transferFrom(address, address, uint256).selector) {
        address from;
        address to;
        uint256 amount;
        require(other != from);
        require balanceOf(from) + balanceBefore < max_uint256;
        transferFrom(e, from, to, amount);
    } else if (f.selector == transfer(address, uint256).selector) {
        require other != e.msg.sender;
        require balanceOf(e.msg.sender) + balanceBefore < max_uint256;
        calldataarg args;
        f(e, args);
    } else {
        require other != e.msg.sender;
        calldataarg args;
        f(e, args);
    }

    assert balanceOf(other) >= balanceBefore;
}

Aave Governance Level 2 Requirement Update

Last update 20/09/2022
verified

Description

The execution delay is always bounded by the minimum and maximum values.

Pseudo formula

MINIMUM_DELAY() <= getDelay() ∧ getDelay() <= MAXIMUM_DELAY()

CVL CODE

invariant properDelay()
    MINIMUM_DELAY() <= getDelay() && getDelay() <= MAXIMUM_DELAY()
Subtitle

In the verification of this invariant, we filtered the call to the function `executeTransaction()`, since in our tool modeling, the low-level call can result in arbitrary changes to the contract states variables.

nonZeroGracePeriod

Last update 20/09/2022
failure

Description

The grace period is always larger than zero.

Pseudo formula

GRACE_PERIOD() > 0

CVL CODE

invariant nonZeroGracePeriod()
    GRACE_PERIOD() > 0
Subtitle

In the verification of this invariant, we filtered the call to the function `executeTransaction()`, since in our tool modeling, the low-level call can result in arbitrary changes to the contract states variables.

nonZeroVotingDuration

Last update 20/09/2022
verified

Description

The voting duration is always larger than zero.

Pseudo formula

VOTING_DURATION() > 0

CVL CODE

invariant nonZeroVotingDuration()
    VOTING_DURATION() > 0
Subtitle

In the verification of this invariant, we filtered the call to the function `executeTransaction()`, since in our tool modeling, the low-level call can result in arbitrary changes to the contract states variables.

nonZeroPropositionalThreshold

Last update 20/09/2022
failure

Description

The proposition threshold is always larger than zero.

Pseudo formula

PROPOSITION_THRESHOLD() > 0

CVL CODE

invariant nonZeroPropositionThreshold()
    PROPOSITION_THRESHOLD() > 0
Subtitle

In the verification of this invariant, we filtered the call to the function `executeTransaction()`, since in our tool modeling, the low-level call can result in arbitrary changes to the contract states variables.

nonZeroMinimumQuorum

Last update 20/09/2022
failure

Description

The minimum quorum is always larger than zero.

Pseudo formula

MINIMUM_QUORUM() > 0

CVL CODE

invariant nonZeroMinimumQuorum()
    MINIMUM_QUORUM() > 0
Subtitle

In the verification of this invariant, we filtered the call to the function `executeTransaction()`, since in our tool modeling, the low-level call can result in arbitrary changes to the contract states variables.

thresholdLessThan100

Last update 20/09/2022
failure

Description

The proposition threshold is always smaller than 100%.

Pseudo formula

PROPOSITION_THRESHOLD() < ONE_HUNDRED_WITH_PRECISION()

CVL CODE

invariant thresholdLessThan100()
    PROPOSITION_THRESHOLD() < ONE_HUNDRED_WITH_PRECISION()
Subtitle

In the verification of this invariant, we filtered the call to the function `executeTransaction()`, since in our tool modeling, the low-level call can result in arbitrary changes to the contract states variables.

differentialLessThan100

Last update 20/09/2022
failure

Description

The voting differential is always smaller than 100%.

Pseudo formula

VOTE_DIFFERENTIAL() < ONE_HUNDRED_WITH_PRECISION()

CVL CODE

invariant differentialLessThan100()
    VOTE_DIFFERENTIAL() < ONE_HUNDRED_WITH_PRECISION()
Subtitle

In the verification of this invariant, we filtered the call to the function `executeTransaction()`, since in our tool modeling, the low-level call can result in arbitrary changes to the contract states variables.

onlyAdminChangesAdmin

Last update 20/09/2022
verified

Description

Only the admin (or pending admin) can change the admin.

Pseudo formula

{
    _admin = getAdmin() ∧
    _pendingAdmin = getPendingAdmin()
}
    < call to any function f >
{
    admin_ = getAdmin() 
    ∧ (f == acceptAdmin() => admin_ == _pendingAdmin && msg.sender == _pendingAdmin)
    ∧ (f ≠ acceptAdmin() => _admin != admin_ => msg.sender == _admin)
}

CVL CODE

rule onlyAdminChangesAdmin(method f)
{
    env e;
    calldataarg args;

    address _admin = getAdmin();
    address _pendingAdmin = getPendingAdmin();
    f(e, args);
    address admin_ = getAdmin();
    if (f.selector == acceptAdmin().selector){
        assert admin_ == _pendingAdmin;
        assert e.msg.sender == _pendingAdmin;
    }
    else{
        assert _admin != admin_ => e.msg.sender == _admin;
    }
}

Aave-StarkNet L1-L2 Bridge

Static To Dynamic Amount Is Inversible

Last update 05/10/2022
verified

Description

For every asset, lending pool, and amount, transforming amount from static to dynamic and back must result in the initial amount.

Pseudo formula

_dynamicToStaticAmount(_staticToDynamicAmount(amount, asset, lendingPool), asset, lendingPool) == amount

CVL CODE

rule dynamicToStaticInversible1(uint256 amount)
{
    address asset;
    requireRayIndex(asset);
    uint256 dynm = _staticToDynamicAmount_Wrapper(amount, asset, LENDINGPOOL_L1);
    uint256 stat = _dynamicToStaticAmount_Wrapper(dynm, asset, LENDINGPOOL_L1);
    assert amount == stat;
}
Subtitle

We assume both indexes (L1, L2) are represented in Ray (1e27).

Dynamic To Static Amount Is Inversible

Last update 05/10/2022
failure

Description

For every asset, lending pool, and amount, transforming amount from dynamic to static and back must result in the initial amount.

Pseudo formula

_staticToDynamicAmount(_dynamicToStaticAmount(amount, asset, lendingPool), asset, lendingPool) == amount

CVL CODE

rule dynamicToStaticInversible2(uint256 amount)
{
    address asset;
    requireRayIndex(asset);
    uint256 indexL1 = LENDINGPOOL_L1.liquidityIndexByAsset(asset);
    uint256 stat = _dynamicToStaticAmount_Wrapper(amount, asset, LENDINGPOOL_L1);
    uint256 dynm = _staticToDynamicAmount_Wrapper(stat, asset, LENDINGPOOL_L1);
     assert dynm == amount;
Subtitle

We assume both indexes (L1, L2) are represented in Ray (1e27).

Dynamic To Static Amount Is Inversible Within An Error Bound

Last update 05/10/2022
verified

Description

For every asset, lending pool, and amount, transforming amount from dynamic to static and back must result an amount within a certain error bar from the initial amount.

Pseudo formula

stat = _dynamicToStaticAmount(amount, asset, lendingPool)
dynm = _staticToDynamicAmount(stat, asset, lendingPool)

dynm - amount <= (indexL1/RAY() + 1)/2

CVL CODE

rule dynamicToStaticInversible3(uint256 amount)
{
    address asset;
    requireRayIndex(asset);
    uint256 indexL1 = LENDINGPOOL_L1.liquidityIndexByAsset(asset);
    uint256 stat = _dynamicToStaticAmount_Wrapper(amount, asset, LENDINGPOOL_L1);
    uint256 dynm = _staticToDynamicAmount_Wrapper(stat, asset, LENDINGPOOL_L1);
    assert dynm - amount <= (indexL1/RAY() + 1)/2; // Pass
}
Subtitle

We assume both indexes (L1, L2) are represented in Ray (1e27).

Integrity Of Withdraw

Last update 05/10/2022
verified

Description

After a successful call to withdraw, the token balances must change correctly.

Pseudo formula

{
    setupTokens(underlying, AToken, static)
    recipient ≠ AToken
    recipient ≠ Bridge
    
        underlyingBalanceBefore = tokenBalanceOf(underlying, recipient)
        ATokenBalanceBefore = tokenBalanceOf(AToken, recipient)
        rewardTokenBalanceBefore = tokenBalanceOf(_rewardToken, recipient)
}
    
    initiateWithdraw_L2(AToken, staticAmount, recipient, toUnderlyingAsset)

{
         underlyingBalanceAfter = tokenBalanceOf(underlying, recipient)
         ATokenBalanceAfter = tokenBalanceOf(AToken, recipient)
         rewardTokenBalanceAfter = tokenBalanceOf(_rewardToken, recipient)
  
    toUnderlyingAsset =>
    (underlyingBalanceAfter >= underlyingBalanceBefore) ∧
    (ATokenBalanceAfter == ATokenBalanceBefore)

    ¬toUnderlyingAsset =>
    (ATokenBalanceAfter >= ATokenBalanceBefore) ∧
    (underlyingBalanceAfter == underlyingBalanceBefore)

     rewardTokenBalanceAfter >= rewardTokenBalanceBefore;
}

CVL CODE

rule integrityOfWithdraw(address recipient){
    bool toUnderlyingAsset;
    uint256 staticAmount; 
    env e; calldataarg args;
    address underlying;
    address static;
    address aToken;
    uint256 l2RewardsIndex = BRIDGE_L2.l2RewardsIndex();
    
    setupTokens(underlying, aToken, static);
    setupUser(e.msg.sender);
    require recipient != aToken;
    require recipient != currentContract;

    uint256 underlyingBalanceBefore = tokenBalanceOf(e, underlying, recipient);
    uint256 aTokenBalanceBefore = tokenBalanceOf(e, aToken, recipient);
    uint256 rewardTokenBalanceBefore = tokenBalanceOf(e, REWARD_TOKEN, recipient);

    initiateWithdraw_L2(e, aToken, staticAmount, recipient, toUnderlyingAsset);

    uint256 underlyingBalanceAfter = tokenBalanceOf(e, underlying, recipient);
    uint256 aTokenBalanceAfter = tokenBalanceOf(e, aToken, recipient);
    uint256 rewardTokenBalanceAfter = tokenBalanceOf(e, REWARD_TOKEN, recipient);

    if (toUnderlyingAsset){
        assert 
        (underlyingBalanceAfter >= underlyingBalanceBefore) &&
        (aTokenBalanceAfter == aTokenBalanceBefore);
    }
    else {
        assert 
        (aTokenBalanceAfter >= aTokenBalanceBefore) &&
        (underlyingBalanceAfter == underlyingBalanceBefore);

    }
    assert rewardTokenBalanceAfter >= rewardTokenBalanceBefore;
}

Deposit Withdraw Reversed

Last update 05/10/2022
verified

Description

A call to deposit and a subsequent call to withdraw with the same amount of staticATokens received must yield the same original balance for the user.

Pseudo formula

{
    l2Recipient = address2uint256(eF.msg.sender)
    setupTokens(asset, Atoken, static)
    setupUser(eB.msg.sender)
    
    balanceU1 = tokenBalanceOf(asset, eB.msg.sender) 
    balanceA1 = tokenBalanceOf(Atoken, eB.msg.sender)
    balanceS1 = tokenBalanceOf(static, eB.msg.sender)
}
    
    staticAmount = deposit(Atoken, l2Recipient, amount, referralCode, fromUA) @ env eB
        
    initiateWithdraw_L2(Atoken, staticAmount, eB.msg.sender, toUA) @ env eF
{
     balanceU2 = tokenBalanceOf(asset, eB.msg.sender)
     balanceA2 = tokenBalanceOf(Atoken, eB.msg.sender)
     balanceS2 = tokenBalanceOf(static, eB.msg.sender)
     
     balanceS1 == balanceS2 
         ∧
     fromUA == toUA => balanceU2 - balanceU1 <= (indexL1/RAY()+1)/2 
         ∧
     fromUA == toUA => balanceA2 == balanceA1
}

CVL CODE

rule depositWithdrawReversed(uint256 amount)
{
    env eB; env eF;
    address Atoken; // AAVE Token
    address asset;  // underlying asset
    address static; // staticAToken
    uint256 l2Recipient = BRIDGE_L2.address2uint256(eF.msg.sender);
    uint16 referralCode;
    bool fromUA; // (deposit) from underlying asset
    bool toUA; // (withdraw) to underlying asset

    setupTokens(asset, Atoken, static);
    setupUser(eB.msg.sender);
    uint256 indexL1 = LENDINGPOOL_L1.liquidityIndexByAsset(asset);
    require indexL1 >= RAY() && indexL1 <= 2*RAY();

    uint256 balanceU1 = tokenBalanceOf(eB, asset, eB.msg.sender);
    uint256 balanceA1 = tokenBalanceOf(eB, Atoken, eB.msg.sender);
    uint256 balanceS1 = tokenBalanceOf(eB, static, eB.msg.sender);
        uint256 staticAmount = deposit(eB, Atoken, l2Recipient, amount, referralCode, fromUA);

        initiateWithdraw_L2(eF, Atoken, staticAmount, eB.msg.sender, toUA);
    uint256 balanceU3 = tokenBalanceOf(eF, asset, eB.msg.sender);
    uint256 balanceA3 = tokenBalanceOf(eF, Atoken, eB.msg.sender);
    uint256 balanceS3 = tokenBalanceOf(eF, static, eB.msg.sender);
    
    assert balanceS1 == balanceS3;
    assert fromUA == toUA => balanceU3 - balanceU1 <= (indexL1/RAY()+1)/2;
    assert fromUA == toUA => balanceA3 == balanceA1;
}
Subtitle

Since rule #2 is violated, the underlying asset balance is not conserved in the process, but the difference is bounded by the liquidity index. The third assertion statement was proven for specific values of the liquidity index. The other two for every value. address2uint256 represents a classic one-to-one conversion between an address variable to a uint256 variable.

Initialize Integrity

Last update 05/10/2022
verified

Description

After a call to initialize, a pair of underlying asset and AToken addresses must be registered correctly.

Pseudo formula

{
     AToken._underlyingAsset == 0
     lendingPool.underlyingAssetToAToken_L1[asset] == 0
}
    
    initialize()  

{
     asset ≠ 0 ∧ AToken ≠ 0 =>
      
     AToken._underlyingAsset == asset
     <=>
     lendingPool.underlyingAssetToAToken_L1[asset] == AToken
}

CVL CODE

rule initializeIntegrity(address AToken, address asset)
{
    env e;
    calldataarg args;

    // Post-constructor conditions
    require getUnderlyingAssetHelper(AToken) == 0;
    require getATokenOfUnderlyingAsset(LENDINGPOOL_L1, asset) == 0;
    
    initialize(e, args);

    assert (asset !=0 && AToken !=0) => (
        getUnderlyingAssetHelper(AToken) == asset 
        <=>
        getATokenOfUnderlyingAsset(LENDINGPOOL_L1, asset) == AToken);
}

AToken Asset Pair

Last update 05/10/2022
verified

Description

Once initialize has been called, asset being registered as the underlying token of AToken, and AToken being connected to asset in the lending pool must always hold.

Pseudo formula

asset ≠ 0 ∧ AToken ≠ 0 =>
      
AToken._underlyingAsset == asset
     <=>
lendingPool.underlyingAssetToAToken_L1[asset] == AToken

CVL CODE

definition excludeInitialize(method f) returns bool =
    f.selector != 
    initialize(uint256, address, address, address[], uint256[], uint256[]).selector; 

definition messageSentFilter(method f) returns bool = 
    f.selector != receiveRewards(uint256, address, uint256).selector
    &&
    f.selector != withdraw(address, uint256, address, uint256, uint256, bool).selector;

invariant ATokenAssetPair(address asset, address AToken)
    (asset !=0 <=> AToken !=0) 
    =>
    (getUnderlyingAssetHelper(AToken) == asset 
    <=>
    getATokenOfUnderlyingAsset(LENDINGPOOL_L1, asset) == AToken)
    filtered{f -> excludeInitialize(f)  && messageSentFilter(f)}
Subtitle

In the verification of this invariant, we exclude calling to `initialize()` since we assume it was already called.

Cancel After Deposit Gives Back Exact Amount

Last update 05/10/2022
failure

Description

Cancelling a deposit successfully by requesting the staticAmount minted after deposit, must return the user’s balance to the original state.

Pseudo formula

{
    user == e1.msg.sender
    user == e2.msg.sender
    user == e3.msg.sender

    setupTokens(asset, AToken, static)
   
    e1.block.timestamp <= e2.block.timestamp
    e2.block.timestamp < e3.block.timestamp

    ATokenBalance1 = tokenBalanceOf(AToken, user);
    assetBalance1 = tokenBalanceOf(asset, user)
}
    staticAmount = deposit(AToken, recipient, amount, code, fromUA) @ env e1
    startDepositCancellation(AToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce) @ env e2
    cancelDeposit(AToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce) @ env e3
{
    ATokenBalance2 = tokenBalanceOf(AToken, user)
    assetBalance2 = tokenBalanceOf(asset, user)

    fromUA =>
         assetBalance1 == assetBalance2 + amount 
         ∧
         ATokenBalance2 == ATokenBalance1 + amount 

    !fromUA =>
        assetBalance1 == assetBalance2
        ∧
        ATokenBalance1 == ATokenBalance2  
}

CVL CODE

rule cancelAfterDepositGivesBackExactAmount(uint256 amount) {
    env e1;
    env e2;
    env e3;
    address user = e1.msg.sender;
    address asset ;
    address aToken;
    address static ;
    address recipient;
    bool fromUA;
    uint256 rewardsIndex;
    uint256 blockNumber;
    uint256 nonce;
    uint16 code;

    setupTokens(asset, aToken, static);
    requireValidUser(user);
    requireRayIndex(asset);
    require e1.msg.sender == e2.msg.sender;
    require e2.msg.sender == e3.msg.sender;
    require e1.block.timestamp <= e2.block.timestamp;
    require e2.block.timestamp < e3.block.timestamp;

    uint256 ATokenBalance1 = tokenBalanceOf(e1, aToken, user);
    uint256 assetBalance1 = tokenBalanceOf(e1, asset, user);
        uint256 staticAmount = deposit(e1, aToken, recipient, amount, code, fromUA);
        startDepositCancellation(e2, aToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce);
        cancelDeposit(e3, aToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce);
    uint256 ATokenBalance2 = tokenBalanceOf(e3, aToken, user);
    uint256 assetBalance2 = tokenBalanceOf(e3, asset, user);

    if(fromUA){
        assert assetBalance1 == assetBalance2 + amount;
        assert ATokenBalance2 == ATokenBalance1 + amount;  
    }
    else {
        assert assetBalance1 == assetBalance2;
        assert ATokenBalance1 == ATokenBalance2;
    }
}
Subtitle

The violation of this rule emerged from the same violation of the rule 'Dynamic To Static Amount Is Inversible'.

Cannot Cancel Deposit And Gain Both Deposit And Refund

Last update 05/10/2022
failure

Description

Once a deposit has been cancelled, the user cannot keep the minted staticATokens.

Pseudo formula

{
    user == e1.msg.sender
    user == e2.msg.sender
    user == e3.msg.sender
    setupTokens(asset, AToken, static)
    
    ATokenBalance1 = tokenBalanceOf(AToken, user)
    staticBalance1 = tokenBalanceOf(static, user)
}
    staticAmount = deposit(AToken, recipient, amount, code, fromUA) @ env e1
{
    ATokenBalance2 = tokenBalanceOf(AToken, user)
    staticBalance2 = tokenBalanceOf(static, user) 
}
    startDepositCancellation(AToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce) @ env e2
    cancelDeposit(AToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce) @ env e3 
     
{
    ATokenBalance3 = tokenBalanceOf(AToken, user)
    staticBalance3 = tokenBalanceOf(static, user)
     
    staticBalance2 > staticBalance1 => ATokenBalance3 == ATokenBalance2
}

CVL CODE

rule cannotCancelDepositAndGainBothTokens(address user, uint256 amount) {
    env e1; env e2; env e3;
    calldataarg args1;
    address asset;
    address aToken;
    address static;
    uint256 recipient = BRIDGE_L2.address2uint256(user);
    uint16 code;
    bool fromUA;
    uint256 rewardsIndex;
    uint256 blockNumber;
    uint256 nonce;

    setupTokens(asset, aToken, static);
    setupUser(user);
    require user == e1.msg.sender;
    require user == e2.msg.sender;
    require user == e3.msg.sender;
    
    uint256 ATokenBalance1 = tokenBalanceOf(e1, aToken, user);
    uint256 staticBalance1 = tokenBalanceOf(e1, static, user);

    uint256 staticAmount = deposit(e1, aToken, recipient, amount, code, fromUA);
    
    uint256 ATokenBalance2 = tokenBalanceOf(e1, aToken, user);
    uint256 staticBalance2 = tokenBalanceOf(e1, static, user);

    startDepositCancellation(e2, aToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce);
    cancelDeposit(e3, aToken, staticAmount, recipient, rewardsIndex, blockNumber, nonce);
    
    uint256 ATokenBalance3 = tokenBalanceOf(e3, aToken, user);
    uint256 staticBalance3 = tokenBalanceOf(e3, static, user);

    // If static tokens were minted, no deposit cancellation should succeed.
    assert staticBalance2 > staticBalance1 => ATokenBalance3 == ATokenBalance2;
}

Integrity Of Approved Tokens And Token Data

Last update 05/10/2022
verified

Description

Integrity of _approvedL1Tokens array length: totalApprovedTokens counts the number of times a memory write was done to the mapping _aTokenData.

Pseudo formula

totalApprovedTokens == _approvedL1Tokens.length

CVL CODE

//Total of l2TokenAddresses
ghost mathint totalApprovedTokens {
    init_state axiom totalApprovedTokens == 0;
}

// Updates the ghost when change l2TokenAddress
hook Sstore _aTokenData[KEY address token].l2TokenAddress uint256 new_tokenAddress
    (uint256 old_tokenAddress) STORAGE {
        totalApprovedTokens = totalApprovedTokens + 1;
}

// Check integrity of _approvedL1Tokens array lenght and totalApprovedTokens change
// excluding initialize
invariant integrityApprovedTokensAndTokenData()
    totalApprovedTokens == getApprovedL1TokensLength()
    { preserved { 
        // Avoiding overflow
        require getApprovedL1TokensLength() < MAX_ARRAY_LENGTH(); 
    } }
Subtitle

Contributed by Jonatascm.

Initialize Tokens Revert Cases

Last update 05/10/2022
failure

Description

Verifies if initialize checks for invalid arrays of l1Tokens and l2Tokens. If the L2 tokens array contains duplicates of addresses, initialize must revert.

Pseudo formula

{
    _aTokenData[l1TokenA].l2TokenAddress() == 0 
        ∧
    _aTokenData[l1TokenB].l2TokenAddress() == 0 
}
    initialize@canrevert(l2Bridge, messagingContract,
    incentivesController, [l1TokenA, l1TokenB],
    [l2Token, l2Token])  
{
    last call reverted
}

CVL CODE

rule shouldRevertInitializeTokens(address AToken, address asset){
    env e;
    uint256 l2Bridge;
    address msg;
    address controller;
    address l1TokenA;
    address l1TokenB;
    uint256 l2Token;
    uint256 ceil1;
    uint256 ceil2;
    // Post-constructor conditions
    require getUnderlyingAssetHelper(AToken) == 0;
    require getATokenOfUnderlyingAsset(LENDINGPOOL_L1, asset) == 0;
    require getL2TokenOfAToken(l1TokenA) == 0 
        && getL2TokenOfAToken(l1TokenB) == 0;
    // In this case, both l1Tokens point to same l2Token :
    // L1TokenA => L2Token
    // L1TokenB => L2Token
    initialize@withrevert(e, l2Bridge, msg, controller,
     [l1TokenA, l1TokenB], [l2Token,l2Token], [ceil1, ceil2]);
    assert lastReverted;
}
Subtitle

Contributed by Jonatascm.

Integrity Of Deposit Expanded

Last update 05/10/2022
verified

Description

Verifies the correctness of balances after a successful deposit.

Pseudo formula

{
    setupTokens(underlyingAsset, AToken, staticAToken)
    
    recipientUnderlyingAssetBalanceBefore = tokenBalanceOf(
        underlyingAsset, recipient)
    recipientATokenBalanceBefore = tokenBalanceOf(
        AToken, recipient)
    recipientStaticATokenBalanceBefore = tokenBalanceOf(
        staticAToken, recipient)
    recipientRewardTokenBalanceBefore = tokenBalanceOf(
        _rewardToken, recipient)
    
    senderUnderlyingAssetBalanceBefore = tokenBalanceOf(
        underlyingAsset, e.msg.sender)
    senderATokenBalanceBefore = tokenBalanceOf(
        AToken, e.msg.sender)
    senderStaticATokenBalanceBefore = tokenBalanceOf(
        staticAToken, e.msg.sender)
    senderRewardTokenBalanceBefore = tokenBalanceOf(
        _rewardToken, e.msg.sender)

}
      
     staticAmount = deposit(AToken, l2Recipient, amount, referralCode, fromUnderlyingAsset) @ env e
     
{
    recipientUnderlyingAssetBalanceAfter = tokenBalanceOf(underlyingAsset, recipient)
    recipientATokenBalanceAfter = tokenBalanceOf(AToken, recipient);
    recipientStaticATokenBalanceAfter = tokenBalanceOf(staticAToken, recipient)
    recipientRewardTokenBalanceAfter = tokenBalanceOf(_rewardToken, recipient)
    
    senderUnderlyingAssetBalanceAfter = tokenBalanceOf(underlyingAsset, e.msg.sender)
    senderATokenBalanceAfter = tokenBalanceOf(AToken, e.msg.sender)
    senderStaticATokenBalanceAfter = tokenBalanceOf(staticAToken, e.msg.sender)
    senderRewardTokenBalanceAfter = tokenBalanceOf(_rewardToken, e.msg.sender)
           
    fromUnderlyingAsset =>
        senderUnderlyingAssetBalanceAfter == senderUnderlyingAssetBalanceBefore - amount ∧
        senderATokenBalanceAfter == senderATokenBalanceBefore ∧
        recipientStaticATokenBalanceAfter == recipientStaticATokenBalanceBefore + staticAmount
    
    !fromUnderlyingAsset => 
         
        senderUnderlyingAssetBalanceAfter == senderUnderlyingAssetBalanceBefore ∧
        senderATokenBalanceBefore - senderATokenBalanceAfter - amount <= (indexL1/RAY() + 1)/2 ∧
        recipientStaticATokenBalanceAfter == recipientStaticATokenBalanceBefore + staticAmount
        
    e.msg.sender ≠ recipient => 
    
        senderStaticATokenBalanceAfter == senderStaticATokenBalanceBefore ∧
        recipientUnderlyingAssetBalanceAfter == recipientUnderlyingAssetBalanceBefore ∧
        recipientATokenBalanceAfter == recipientATokenBalanceBefore
    
    senderRewardTokenBalanceAfter == senderRewardTokenBalanceBefore 
    
    recipientRewardTokenBalanceAfter == recipientRewardTokenBalanceBefore
}

CVL CODE

rule integrityOfDepositExpanded(){
    env e; 
    address recipient;
    uint256 amount;
    address aToken;
    address underlyingAsset; 
    address staticAToken;
    uint256 l2Recipient = BRIDGE_L2.address2uint256(recipient);
    uint16 referralCode;
    bool fromUnderlyingAsset; 
    uint256 indexL1 = LENDINGPOOL_L1.liquidityIndexByAsset(underlyingAsset);
    
    setupTokens(underlyingAsset, aToken, staticAToken);
    setupUser(e.msg.sender);
    setupUser(recipient);
    requireRayIndex(underlyingAsset);
    // Recipient balances before
    uint256 recipientUnderlyingAssetBalanceBefore = tokenBalanceOf(e, underlyingAsset, recipient);
    uint256 recipientATokenBalanceBefore = tokenBalanceOf(e, aToken, recipient);
    uint256 recipientStaticATokenBalanceBefore = tokenBalanceOf(e, staticAToken, recipient);
    uint256 recipientRewardTokenBalanceBefore = tokenBalanceOf(e, REWARD_TOKEN, recipient);
    // Sender balances before
    uint256 senderUnderlyingAssetBalanceBefore = tokenBalanceOf(e, underlyingAsset, e.msg.sender);
    uint256 senderATokenBalanceBefore = tokenBalanceOf(e, aToken, e.msg.sender);
    uint256 senderStaticATokenBalanceBefore = tokenBalanceOf(e, staticAToken, e.msg.sender);
    uint256 senderRewardTokenBalanceBefore = tokenBalanceOf(e, REWARD_TOKEN, e.msg.sender); 
    uint256 staticAmount = deposit(e, aToken, l2Recipient, amount, referralCode, fromUnderlyingAsset);
    // Recipient balances after
    uint256 recipientUnderlyingAssetBalanceAfter = tokenBalanceOf(e, underlyingAsset, recipient);
    uint256 recipientATokenBalanceAfter = tokenBalanceOf(e, aToken, recipient);
    uint256 recipientStaticATokenBalanceAfter = tokenBalanceOf(e, staticAToken, recipient);
    uint256 recipientRewardTokenBalanceAfter = tokenBalanceOf(e, REWARD_TOKEN, recipient);
    // Sender balances after
    uint256 senderUnderlyingAssetBalanceAfter = tokenBalanceOf(e, underlyingAsset, e.msg.sender);
    uint256 senderATokenBalanceAfter = tokenBalanceOf(e, aToken, e.msg.sender);
    uint256 senderStaticATokenBalanceAfter = tokenBalanceOf(e, staticAToken, e.msg.sender);
    uint256 senderRewardTokenBalanceAfter = tokenBalanceOf(e, REWARD_TOKEN, e.msg.sender); 
           
    if (fromUnderlyingAsset){
        assert 
        (senderUnderlyingAssetBalanceAfter == senderUnderlyingAssetBalanceBefore - amount) &&
        (senderATokenBalanceAfter == senderATokenBalanceBefore) &&
        (recipientStaticATokenBalanceAfter == recipientStaticATokenBalanceBefore + staticAmount);
    }
    else {
        assert 
        (senderUnderlyingAssetBalanceAfter == senderUnderlyingAssetBalanceBefore) &&
        (senderATokenBalanceAfter - senderATokenBalanceBefore + amount <= (indexL1/RAY() + 1)/2) &&
        (recipientStaticATokenBalanceAfter == recipientStaticATokenBalanceBefore + staticAmount);
    }
    if (e.msg.sender != recipient) {
        assert 
        (senderStaticATokenBalanceAfter == senderStaticATokenBalanceBefore) &&
        (recipientUnderlyingAssetBalanceAfter == recipientUnderlyingAssetBalanceBefore) &&
        (recipientATokenBalanceAfter == recipientATokenBalanceBefore);
    }
    assert senderRewardTokenBalanceAfter == senderRewardTokenBalanceBefore &&
           recipientRewardTokenBalanceAfter == recipientRewardTokenBalanceBefore;
}
Subtitle

Contributed by Jessicapointing. We assume the recipient is not a contract. When fromUnderlyingAsset=false we verified the rule for specific values of the liquidity index, otherwise for an arbitrary value of the index.