methods {
    PROPOSER_ROLE() returns(bytes32) envfree

    _DONE_TIMESTAMP() returns(uint256) envfree
    _minDelay() returns(uint256) envfree
    _checkRole(bytes32) => DISPATCHER(true)

    isOperation(bytes32) returns(bool) envfree
    isOperationPending(bytes32) returns(bool) envfree
    isOperationReady(bytes32) returns(bool)
    isOperationDone(bytes32) returns(bool) envfree
    getTimestamp(bytes32) returns(uint256) envfree
    getMinDelay() returns(uint256) envfree

    hashOperation(address, uint256, bytes, bytes32, bytes32) returns(bytes32) envfree
    hashOperationBatch(address[], uint256[], bytes[], bytes32, bytes32) returns(bytes32) envfree

    schedule(address, uint256, bytes, bytes32, bytes32, uint256)
    scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256)
    execute(address, uint256, bytes, bytes32, bytes32)
    executeBatch(address[], uint256[], bytes[], bytes32, bytes32)
    cancel(bytes32)
}


////////////////////////////////////////////////////////////////////////////
//                         Functions                                      //
////////////////////////////////////////////////////////////////////////////


function hashIdCorrelation(bytes32 id, address target, uint256 value, bytes data, bytes32 predecessor, bytes32 salt){
    require data.length < 32;
    require hashOperation(target, value, data, predecessor, salt) == id;
}


////////////////////////////////////////////////////////////////////////////
//                         Invariants                                     //
////////////////////////////////////////////////////////////////////////////


// STATUS - verified
// `isOperation()` correctness check
invariant operationCheck(bytes32 id)
    getTimestamp(id) > 0 <=> isOperation(id)
filtered { f -> !f.isView }

// STATUS - verified
// `isOperationPending()` correctness check
invariant pendingCheck(bytes32 id)
    getTimestamp(id) > _DONE_TIMESTAMP() <=> isOperationPending(id)
filtered { f -> !f.isView }

// STATUS - verified
// `isOperationReady()` correctness check
invariant readyCheck(env e, bytes32 id)
    (e.block.timestamp >= getTimestamp(id) && getTimestamp(id) > 1) <=> isOperationReady(e, id)
filtered { f -> !f.isView }

// STATUS - verified
// `isOperationDone()` correctness check
invariant doneCheck(bytes32 id)
    getTimestamp(id) == _DONE_TIMESTAMP() <=> isOperationDone(id)
filtered { f -> !f.isView }


////////////////////////////////////////////////////////////////////////////
//                            Rules                                       //
////////////////////////////////////////////////////////////////////////////


/////////////////////////////////////////////////////////////
// STATE TRANSITIONS
/////////////////////////////////////////////////////////////


// STATUS - verified
// Possible transitions: form `!isOperation()` to `!isOperation()` or `isOperationPending()` only
rule unsetPendingTransitionGeneral(method f, env e){
    bytes32 id;

    require !isOperation(id);
    require e.block.timestamp > 1;

    calldataarg args;
    f(e, args);

    assert isOperationPending(id) || !isOperation(id);
}


// STATUS - verified
// Possible transitions: form `!isOperation()` to `isOperationPending()` via `schedule()` and `scheduleBatch()` only
rule unsetPendingTransitionMethods(method f, env e){
    bytes32 id;

    require !isOperation(id);

    calldataarg args;
    f(e, args);

    assert isOperationPending(id) => (f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector
                                || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector), "Why do we need to follow the schedule?";
}


// STATUS - verified
// Possible transitions: form `ready()` to `isOperationDone()` via `execute()` and `executeBatch()` only
rule readyDoneTransition(method f, env e){
    bytes32 id;

    require isOperationReady(e, id);

    calldataarg args;
    f(e, args);

    assert isOperationDone(id) => f.selector == execute(address, uint256, bytes, bytes32, bytes32).selector
                                || f.selector == executeBatch(address[], uint256[], bytes[], bytes32, bytes32).selector , "It's not isOperationDone yet!";
}


// STATUS - verified
// isOperationPending() -> cancelled() via cancel() only
rule pendingCancelledTransition(method f, env e){
    bytes32 id;

    require isOperationPending(id);

    calldataarg args;
    f(e, args);

    assert !isOperation(id) => f.selector == cancel(bytes32).selector, "How you dare to cancel me?";
}


// STATUS - verified
// isOperationDone() -> nowhere
rule doneToNothingTransition(method f, env e){
    bytes32 id;

    require isOperationDone(id);

    calldataarg args;
    f(e, args);

    assert isOperationDone(id), "Did you find a way to escape? There is no way! HA-HA-HA";
}



/////////////////////////////////////////////////////////////
// THE REST
/////////////////////////////////////////////////////////////


// STATUS - verified
// only TimelockController contract can change minDelay
rule minDelayOnlyChange(method f, env e){
    uint256 delayBefore = _minDelay();

    calldataarg args;
    f(e, args);

    uint256 delayAfter = _minDelay();

    assert delayBefore != delayAfter => e.msg.sender == currentContract, "You cannot change your destiny! Only I can!";
}


// STATUS - verified
// scheduled operation timestamp == block.timestamp + delay (kind of unit test)
rule scheduleCheck(method f, env e){
    bytes32 id;

    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;

    hashIdCorrelation(id, target, value, data, predecessor, salt);

    schedule(e, target, value, data, predecessor, salt, delay);

    assert getTimestamp(id) == to_uint256(e.block.timestamp + delay), "Time doesn't obey to mortal souls";
}


// STATUS - verified
// Cannot call `execute()` on a isOperationPending (not ready) operation
rule cannotCallExecute(method f, env e){
    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
    bytes32 id;

    hashIdCorrelation(id, target, value, data, predecessor, salt);
    require isOperationPending(id) && !isOperationReady(e, id);

    execute@withrevert(e, target, value, data, predecessor, salt);

    assert lastReverted, "you go against execution nature";
}


// STATUS - verified
// Cannot call `execute()` on a !isOperation operation
rule executeRevertsFromUnset(method f, env e, env e2){
    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
    bytes32 id;

    hashIdCorrelation(id, target, value, data, predecessor, salt);
    require !isOperation(id);

    execute@withrevert(e, target, value, data, predecessor, salt);

    assert lastReverted, "you go against execution nature";
}


// STATUS - verified
// Execute reverts => state returns to isOperationPending
rule executeRevertsEffectCheck(method f, env e){
    address target; uint256 value; bytes data; bytes32 predecessor; bytes32 salt;
    bytes32 id;

    hashIdCorrelation(id, target, value, data, predecessor, salt);
    require isOperationPending(id) && !isOperationReady(e, id);

    execute@withrevert(e, target, value, data, predecessor, salt);
    bool reverted = lastReverted;

    assert lastReverted => isOperationPending(id) && !isOperationReady(e, id), "you go against execution nature";
}


// STATUS - verified
// Canceled operations cannot be executed → can’t move from canceled to isOperationDone
rule cancelledNotExecuted(method f, env e){
    bytes32 id;

    require !isOperation(id);
    require e.block.timestamp > 1;

    calldataarg args;
    f(e, args);

    assert !isOperationDone(id), "The ship is not a creature of the air";
}


// STATUS - verified
// Only proposers can schedule
rule onlyProposer(method f, env e) filtered { f -> f.selector == schedule(address, uint256, bytes, bytes32, bytes32, uint256).selector
                                                    || f.selector == scheduleBatch(address[], uint256[], bytes[], bytes32, bytes32, uint256).selector } {
    bytes32 id;
    bytes32 role;
    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;

    _checkRole@withrevert(e, PROPOSER_ROLE());

    bool isCheckRoleReverted = lastReverted;

    calldataarg args;
    f@withrevert(e, args);

    bool isScheduleReverted = lastReverted;

    assert isCheckRoleReverted => isScheduleReverted, "Enemy was detected";
}


// STATUS - verified
// if `ready` then has waited minimum period after isOperationPending()
rule cooldown(method f, env e, env e2){
    bytes32 id;
    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;
    uint256 minDelay = getMinDelay();

    hashIdCorrelation(id, target, value, data, predecessor, salt);

    schedule(e, target, value, data, predecessor, salt, delay);

    calldataarg args;
    f(e, args);

    assert isOperationReady(e2, id) => (e2.block.timestamp - e.block.timestamp >= minDelay), "No rush! When I'm ready, I'm ready";
}


// STATUS - verified
// `schedule()` should change only one id's timestamp
rule scheduleChange(env e){
    bytes32 id;  bytes32 otherId;
    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt; uint256 delay;

    uint256 otherIdTimestampBefore = getTimestamp(otherId);

    hashIdCorrelation(id, target, value, data, predecessor, salt);

    schedule(e, target, value, data, predecessor, salt, delay);

    assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
}


// STATUS - verified
// `execute()` should change only one id's timestamp
rule executeChange(env e){
    bytes32 id;  bytes32 otherId;
    address target; uint256 value; bytes data ;bytes32 predecessor; bytes32 salt;
    uint256 otherIdTimestampBefore = getTimestamp(otherId);

    hashIdCorrelation(id, target, value, data, predecessor, salt);

    execute(e, target, value, data, predecessor, salt);

    assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
}


// STATUS - verified
// `cancel()` should change only one id's timestamp
rule cancelChange(env e){
    bytes32 id;  bytes32 otherId;

    uint256 otherIdTimestampBefore = getTimestamp(otherId);

    cancel(e, id);

    assert id != otherId => otherIdTimestampBefore == getTimestamp(otherId), "Master of puppets, I'm pulling your strings";
}