AAVE Token V3

.gitignore

@@ -4,3 +4,4 @@ out/
 .certora_config/
 .last_confs/
 .certora_*
+certora/resource_errors.json

certora/scripts/setup.sh

@@ -9,5 +9,5 @@ certoraRun certora/harness/AaveTokenV3Harness.sol:AaveTokenV3 \
     --solc solc8.13 \
     --optimistic_loop \
     --send_only \
-    --staging \
+    --cloud \
     --msg "AaveTokenV3:setup.spec $1"

certora/specs/setup.spec

@@ -135,4 +135,380 @@ hook Sstore _balances[KEY address user].balance uint104 balance
 
 */
 invariant totalSupplyEqualsBalances()
-    sumBalances == totalSupply()
+    sumBalances == totalSupply()
+
+
+/**
+    --------------------------------------------------------
+    --------------------------------------------------------
+                   Below are the new rules
+    --------------------------------------------------------
+    --------------------------------------------------------
+*/
+
+/**
+
+    Verify that only delegate functions can change someone's delegate.
+
+*/
+
+rule votingDelegateChanges_updated(address alice, method f) {
+    env e;
+    calldataarg args;
+
+    address aliceVotingDelegateBefore = getVotingDelegate(alice);
+    address alicePropositionDelegateBefore = getPropositionDelegate(alice);
+
+    f(e, args);
+
+    address aliceVotingDelegateAfter = getVotingDelegate(alice);
+    address alicePropositionDelegateAfter = getPropositionDelegate(alice);
+
+    // only these four function may change the delegate of an address
+    assert (aliceVotingDelegateAfter != aliceVotingDelegateBefore) ||  (alicePropositionDelegateBefore != alicePropositionDelegateAfter) =>
+        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;
+}
+
+/**
+
+    Integrity of delegate():
+        - Adds delegator balance to delegatee voting & proposing power
+        - Updates voting delegate
+
+
+*/
+
+rule integrityOfDdelegate(address bob, method f) filtered {
+        f -> 
+        f.selector == delegate(address).selector || 
+        f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector
+}{
+    env e;
+    calldataarg args;
+
+    address delegator;
+    uint256 deadline;
+    uint8 v;
+    bytes32 r;
+    bytes32 s;
+
+    // delegate not to self or to zero
+    require bob != e.msg.sender && bob != delegator && bob != 0;
+
+    // avoid unrealistic delegated balance
+    require(getDelegatedVotingBalance(bob) < MAX_DELEGATED_BALANCE());
+    require(getDelegatedPropositionBalance(bob) < MAX_DELEGATED_BALANCE());
+
+    uint256 bobVotingPowerBefore = getPowerCurrent(bob, VOTING_POWER());
+    uint256 bobPropositionPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
+
+    // Var declaration with initial value
+    uint256 delegatorBalance = 0;
+    address delegatorAddress = 0x0;
+
+    if (f.selector == delegate(address).selector){
+        delegatorAddress = e.msg.sender;
+    } else if (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector){
+        delegatorAddress = delegator;
+    }
+
+    bool votingDelegateWasNotBob = getVotingDelegate(delegatorAddress) != bob;
+    bool propositionDelegateWasNotBob = getPropositionDelegate(delegatorAddress) != bob;
+    delegatorBalance = balanceOf(delegatorAddress);        
+
+    if (f.selector == delegate(address).selector) {
+        delegate(e, bob);
+    } else if (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector) {
+        metaDelegate(e, delegator, bob, deadline, v, r, s);
+    } 
+    // Have to leave else branch otherwise there will be a error
+    else {
+        f(e, args);
+    }
+
+    // test the delegate indeed is now bob
+    assert bob == getVotingDelegate(delegatorAddress);
+    assert bob == getPropositionDelegate(delegatorAddress);  
+
+    // test the delegate's new voting power
+    uint256 bobVotingPowerAfter = getPowerCurrent(bob, VOTING_POWER());
+    assert votingDelegateWasNotBob => bobVotingPowerAfter == bobVotingPowerBefore + normalize(delegatorBalance);
+
+    // test the delegate's new proposition power
+    uint256 bobPropositionPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER());
+    assert propositionDelegateWasNotBob => bobPropositionPowerAfter == bobPropositionPowerBefore + normalize(delegatorBalance);
+}
+
+/**
+
+    Integrity of delegateByType():
+        - Invalid governance type will not change voting, proposition power and delegate
+        - Adds delegator balance to delegatee voting or proposing power
+        - It shall not influence the other power
+
+*/
+
+rule integrityOfDdelegateByType(address bob, method f) filtered {
+        f -> 
+        f.selector == delegateByType(address,uint8).selector ||
+        f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector
+}{
+    env e;
+    calldataarg args;
+    uint8 governanceType;
+
+    address delegator;
+    uint256 deadline;
+    uint8 v;
+    bytes32 r;
+    bytes32 s;
+
+    // delegate not to self or to zero
+    require bob != e.msg.sender && bob != delegator && bob != 0;
+
+    // avoid unrealistic delegated balance
+    require(getDelegatedVotingBalance(bob) < MAX_DELEGATED_BALANCE());
+    require(getDelegatedPropositionBalance(bob) < MAX_DELEGATED_BALANCE());
+
+    uint256 bobVotingPowerBefore = getPowerCurrent(bob, VOTING_POWER());
+    uint256 bobPropositionPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
+
+    // Var declaration with initial value
+    uint256 delegatorBalance = 0;
+    address delegatorAddress = 0x0;
+
+    if (f.selector == delegateByType(address,uint8).selector){
+        delegatorAddress = e.msg.sender;
+    } else if (f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector){
+        delegatorAddress = delegator;
+    }
+
+    address votingDelegateBefore = getVotingDelegate(delegatorAddress);
+    address propositionDelegateBefore = getPropositionDelegate(delegatorAddress);
+
+    bool votingDelegateWasNotBob = votingDelegateBefore != bob;
+    bool propositionDelegateWasNotBob = propositionDelegateBefore != bob;
+    delegatorBalance = balanceOf(delegatorAddress);        
+
+    if (f.selector == delegateByType(address,uint8).selector) {
+        delegateByType(e, bob, governanceType);
+    } else if (f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector) {
+        metaDelegateByType(e, delegator, bob, governanceType, deadline, v, r, s);
+    } 
+    // Have to leave else branch otherwise there will be a error
+    else {
+        f(e, args);
+    }
+
+
+    uint256 bobVotingPowerAfter = getPowerCurrent(bob, VOTING_POWER());
+    uint256 bobPropositionPowerAfter = getPowerCurrent(bob, PROPOSITION_POWER());
+
+    // Invalid governance type will not change voting, proposition power and delegate
+    assert governanceType != VOTING_POWER() && governanceType != PROPOSITION_POWER() =>
+        bobVotingPowerAfter == bobVotingPowerBefore && bobPropositionPowerAfter == bobPropositionPowerBefore &&
+        votingDelegateBefore == getVotingDelegate(delegatorAddress) && propositionDelegateBefore == getPropositionDelegate(delegatorAddress);
+
+    // test the delegate indeed is now bob and did not change other voting type delegate
+    assert governanceType == VOTING_POWER() => bob == getVotingDelegate(delegatorAddress);
+    assert governanceType == PROPOSITION_POWER() => bob == getPropositionDelegate(delegatorAddress);
+
+    // test the delegate's new voting power and proposition power
+    assert votingDelegateWasNotBob && governanceType == VOTING_POWER() => (bobVotingPowerAfter == bobVotingPowerBefore + normalize(delegatorBalance)) && 
+        bobPropositionPowerAfter == bobPropositionPowerBefore;
+
+    // test the delegate's new proposition power and voting power
+    assert propositionDelegateWasNotBob && governanceType == PROPOSITION_POWER() => (bobPropositionPowerAfter == bobPropositionPowerBefore + normalize(delegatorBalance)) && 
+        bobVotingPowerAfter == bobVotingPowerBefore;
+}
+
+/**
+
+    Testing correctness of delegating voting power
+
+*/
+
+rule delegateCorrectness_updated(address bob, method f) filtered {
+        f -> 
+        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
+}{
+    env e;
+    calldataarg args;
+
+    address delegator;
+    uint256 deadline;
+    uint8 v;
+    bytes32 r;
+    bytes32 s;
+
+    // delegate not to self or to zero
+    require bob != e.msg.sender && bob != delegator && bob != 0;
+
+    uint256 bobDelegatedBalance = getDelegatedVotingBalance(bob);
+    // avoid unrealistic delegated balance
+    require(bobDelegatedBalance < MAX_DELEGATED_BALANCE());
+
+    uint256 bobVotingPowerBefore = getPowerCurrent(bob, VOTING_POWER());
+    uint256 bobPropositionPowerBefore = getPowerCurrent(bob, PROPOSITION_POWER());
+
+    // Var declaration with initial value
+    uint256 delegatorBalance = 0;
+    address delegatorAddress = 0x0;
+
+    if (f.selector == delegate(address).selector || 
+        f.selector == delegateByType(address,uint8).selector) {
+
+        delegatorAddress = e.msg.sender;
+    } else if (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || 
+               f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector) {
+
+        delegatorAddress = delegator;
+    }
+
+    // filter that the delegator doesn't already delegate to bob
+    require getVotingDelegate(delegatorAddress) != bob;
+    delegatorBalance = balanceOf(delegatorAddress);        
+
+    if (f.selector == delegate(address).selector || 
+        f.selector == delegateByType(address,uint8).selector) {
+
+        if (f.selector == delegate(address).selector) {
+            delegate(e, bob);
+        } else {
+            delegateByType(e, bob, VOTING_POWER());
+        }
+
+    } else if (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector || 
+               f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector) {
+
+        if (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector) {
+            metaDelegate(e, delegator, bob, deadline, v, r, s);
+        } else { 
+            metaDelegateByType(e, delegator, bob, VOTING_POWER(), deadline, v, r, s);
+        }
+    } 
+    // Have to leave else branch otherwise there will be a error
+    else {
+        f(e, args);
+    }
+
+    // test the delegate indeed is now bob
+    assert bob == getVotingDelegate(delegatorAddress); 
+
+    // test the delegate's new voting power
+    uint256 bobVotingPowerAfter = getPowerCurrent(bob, VOTING_POWER());
+    //assert bobVotingPowerAfter == bobVotingPowerBefore + normalize(msgSenderBalance);
+    assert bobVotingPowerAfter == bobVotingPowerBefore + normalize(delegatorBalance);
+
+}
+
+
+
+
+/**
+
+    State transition from not having a voting power to having a voting power
+        One has voting power when:
+            balanceOf(user) > 0
+            User has been delegated power
+
+    sh certora/scripts/setup.sh stateTransitionToVotingPower withTransferFromAndDelegate
+*/
+
+rule stateTransitionToVotingPower(address bob, method f){
+    // We are not testing _governancePowerTransferByType() because function is public only in Harness contract 
+    //     and AaveTokenV3 has function defined as a internal.
+    require(f.selector != _governancePowerTransferByType(uint104,uint104,address,uint8).selector);
+
+    env e;
+    calldataarg args;
+    address to;
+    address from;
+    uint256 amount;
+    uint8 governanceType;
+
+    uint256 deadline;
+    uint8 v;
+    bytes32 r;
+    bytes32 s;
+
+    uint256 bobVotingPowerBefore = getPowerCurrent(bob, VOTING_POWER());
+    uint256 bobBalanceBefore = balanceOf(bob);
+
+    if (f.selector == transfer(address,uint256).selector){
+        transfer(e,to,amount);
+    } else if (f.selector == transferFrom(address,address,uint256).selector){
+        transferFrom(e,from,to,amount);
+    } else if (f.selector == delegateByType(address,uint8).selector) {
+        delegateByType(e, bob, governanceType);
+    } else if (f.selector == metaDelegate(address,address,uint256,uint8,bytes32,bytes32).selector) {
+        metaDelegate(e, from, bob, deadline, v, r, s);
+    } else if (f.selector == metaDelegateByType(address,address,uint8,uint256,uint8,bytes32,bytes32).selector) {
+        metaDelegateByType(e, to, bob, governanceType, deadline, v, r, s);
+    } else {
+        f(e, args);
+    }
+
+    uint256 bobVotingPowerAfter = getPowerCurrent(bob, VOTING_POWER());
+    uint256 bobBalanceAfter = balanceOf(bob);
+
+    bool hasVotingPowerBefore = bobVotingPowerBefore > 0;
+    bool hasVotingPowerAfter = bobVotingPowerAfter > 0;
+
+    assert !hasVotingPowerBefore && hasVotingPowerAfter => (
+        (bobBalanceBefore == 0 && bobBalanceAfter > 0) || 
+        (bobBalanceBefore > 0 && from == bob) || 
+        (e.msg.sender == bob && bobBalanceBefore > 0) || 
+        (getVotingDelegate(to) == bob || to == bob && balanceOf(to) > 0) || 
+        (getVotingDelegate(e.msg.sender) == bob && balanceOf(e.msg.sender) > 0) ||
+        (getVotingDelegate(from) == bob && balanceOf(from) > 0));
+}
+
+
+
+/**
+
+    State transition
+        One stops having voting power when:
+            They delegate to another account and they have not been delegated-to
+            They weren't delegating and transferred all their funds
+
+*/
+
+/*
+did not yet finish
+rule stateTransitionStopsHavingVotingPower(address bob, method f){
+    // We are not testing _governancePowerTransferByType() because function is public only in Harness contract 
+    //     and AaveTokenV3 has it as a internal function.
+    require(f.selector != _governancePowerTransferByType(uint104,uint104,address,uint8).selector);
+
+    uint256 bobVotingPowerBefore = getPowerCurrent(bob, VOTING_POWER());
+    uint256 bobBalanceBefore = balanceOf(bob);
+    address bobVotingDelegateBefore = getVotingDelegate(bob);
+
+    // Require that Bob had voting power
+    require(bobVotingPowerBefore > 0);
+
+    env e;
+    calldataarg args;
+    address to;
+    address from;
+    uint256 amount;
+
+    if (f.selector == transfer(address,uint256).selector){
+        transfer(e,to,amount);
+    } 
+
+    uint256 bobVotingPowerAfter = getPowerCurrent(bob, VOTING_POWER());
+    bool hasVotingPowerAfter = bobVotingPowerAfter > 0;
+
+    assert !hasVotingPowerAfter;
+}
+*/
+