delegationToZeroAlwaysPossible - aave token v3/certora

gistfile1.txt

rule delegationToZeroAlwaysPossible() {
    env e;
    require e.msg.value == 0;
    require validDelegationState(e.msg.sender); // _balances[e.msg.sender].delegationState < 4

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

    delegate@withrevert(e, 0);
    assert !lastReverted;
}