openzeppelin-contracts/certora/specs/GovernorBase.spec

//////////////////////////////////////////////////////////////////////////////
///////////////////// Governor.sol base definitions //////////////////////////
//////////////////////////////////////////////////////////////////////////////

methods {
    proposalSnapshot(uint256) returns uint256 envfree // matches proposalVoteStart
    proposalDeadline(uint256) returns uint256 envfree
    hashProposal(address[],uint256[],bytes[],bytes32) returns uint256 envfree
    isExecuted(uint256) returns bool envfree
    isCanceled(uint256) returns bool envfree
    execute(address[], uint256[], bytes[], bytes32) returns uint256
    // initialized(uint256) returns bool envfree

    hasVoted(uint256, address) returns bool

    castVote(uint256, uint8) returns uint256

    // internal functions made public in harness:
    _quorumReached(uint256) returns bool envfree
    _voteSucceeded(uint256) returns bool envfree

}

/*
 //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 ///////////////////////////////////////////////////// State Diagram //////////////////////////////////////////////////////////
 //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 //                                                                                                                          //
 //                                                                castVote(s)()                                             //
 //  -------------  propose()  ----------------------  time pass  ---------------       time passes         -----------      //
 // | No Proposal | --------> | Before Start (Delay) | --------> | Voting Period | ----------------------> | execute() |     //
 //  -------------             ----------------------             --------------- -> Executed/Canceled      -----------      //
 //  ------------------------------------------------------------|---------------|-------------------------|-------------->  //
 // t                                                          start            end                     timelock             //
 //                                                                                                                          //
 //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
*/



///////////////////////////////////////////////////////////////////////////////////////
///////////////////////////////// Global Valid States /////////////////////////////////
///////////////////////////////////////////////////////////////////////////////////////

    // not complete
    /*
     * If any of the properties are non zero, the rest has to be non zero 
     */
     // start   !0  !0  !0
     // end =   !0  !0  !0
     // exe = 0  0  1   1
     // can = 0  1  0   1
    invariant proposalInitiated(uint256 pId)
            (proposalSnapshot(pId) != 0 <=> proposalDeadline(pId) != 0) &&
            (isCanceled(pId) => proposalSnapshot(pId) != 0) &&
            (isExecuted(pId) => proposalSnapshot(pId) != 0)

    // pass
    /*
     * A proposal cannot end unless it started.
     */
    invariant voteStartBeforeVoteEnd(uint256 pId)
        (proposalSnapshot(pId) > 0 =>  proposalSnapshot(pId) < proposalDeadline(pId))
             && (proposalSnapshot(pId) == 0 => proposalDeadline(pId) == 0)


    // pass
    /*
     * A proposal cannot be both executed and canceled.
     */
    invariant noBothExecutedAndCanceled(uint256 pId) 
            !isExecuted(pId) || !isCanceled(pId)



///////////////////////////////////////////////////////////////////////////////////////
////////////////////////////////// In-State Rules /////////////////////////////////////
///////////////////////////////////////////////////////////////////////////////////////

//==========================================
//------------- Voting Period --------------
//==========================================

    // pass
    /*
     * A user cannot vote twice
     */
    rule doubleVoting(uint256 pId, uint8 sup) {
        env e;
        address user = e.msg.sender;

        bool votedCheck = hasVoted(e, pId, user);
        require votedCheck == true;

        castVote@withrevert(e, pId, sup);
        bool reverted = lastReverted;

        assert votedCheck => reverted, "double voting accured";
    }


///////////////////////////////////////////////////////////////////////////////////////
//////////////////////////// State Transitions Rules //////////////////////////////////
///////////////////////////////////////////////////////////////////////////////////////

//===========================================
//-------- Propose() --> End of Time --------
//===========================================

    // pass
    /*
     * The voting must start not before the proposal’s creation time
     */
    rule noStartBeforeCreation(uint256 pId) {
        uint256 previousStart = proposalSnapshot(pId);
        require previousStart == 0;
        env e;
        calldataarg arg;
        propose(e, arg);

        uint newStart = proposalSnapshot(pId);
        // if created, start is after current block number (creation block)
        assert(newStart != previousStart => newStart >= e.block.number);
    }


    // pass
    /*
     * Once a proposal is created, voteStart and voteEnd are immutable
     */
    rule immutableFieldsAfterProposalCreation(uint256 pId, method f) {
        uint _voteStart = proposalSnapshot(pId);
        uint _voteEnd = proposalDeadline(pId);
        require _voteStart > 0; // proposal was created - relation proved in noStartBeforeCreation

        env e;
        calldataarg arg;
        f(e, arg);

        uint voteStart_ = proposalSnapshot(pId);
        uint voteEnd_ = proposalDeadline(pId);
        assert _voteStart == voteStart_;
        assert _voteEnd == voteEnd_;
    }

    // pass
    /*
     * A proposal cannot be neither executed nor canceled before it starts
     */
    rule noExecuteOrCancelBeforeStarting(uint256 pId, method f){
        env e;

        require !isExecuted(pId) && !isCanceled(pId);

        calldataarg arg;
        f(e, arg);

        assert e.block.number < proposalSnapshot(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before start";
    }

//============================================
//--- End of Voting Period --> End of Time ---
//============================================

    // pass
    /*
     * A proposal cannot be neither executed nor canceled before proposal's deadline
     */
    rule noExecuteOrCancelBeforeDeadline(uint256 pId, method f){
        env e;

        requireInvariant voteStartBeforeVoteEnd(pId);
        require !isExecuted(pId) && !isCanceled(pId);

        calldataarg arg;
        f(e, arg);

        assert e.block.number < proposalDeadline(pId) => (!isExecuted(pId) && !isCanceled(pId)), "executed/cancelled before deadline";
    }

////////////////////////////////////////////////////////////////////////////////
////////////////////// Integrity Of Functions (Unit Tests) /////////////////////
////////////////////////////////////////////////////////////////////////////////

/**
 * Check hashProposal hashing is reliable (different inputs lead to different buffers hashed)
 */
/*
rule checkHashProposal {
    address[] t1;
    address[] t2;
    uint256[] v1;
    uint256[] v2;
    bytes[] c1;
    bytes[] c2;
    bytes32 d1;
    bytes32 d2;

    uint256 h1 = hashProposal(t1,v1,c1,d1);
    uint256 h2 = hashProposal(t2,v2,c2,d2);
    bool equalHashes = h1 == h2;
    assert equalHashes => t1.length == t2.length;
    assert equalHashes => v1.length == v2.length;
    assert equalHashes => c1.length == c2.length;
    assert equalHashes => d1 == d2;
}
*/

////////////////////////////////////////////////////////////////////////////////
//////////////////////////////// High Level Rules //////////////////////////////
////////////////////////////////////////////////////////////////////////////////

    // not passing
    /*
     * all non-view functions should revert if proposal is executed
     */
    rule allFunctionsRevertIfExecuted(uint256 pId, method f) filtered { f -> !f.isView } {
        env e; calldataarg args;
        require(isExecuted(pId));
        f@withrevert(e,args);
        assert(lastReverted == true, "Function was not reverted");
    }

    // not passing
    /*
     * all non-view functions should revert if proposal is canceled
     */
    rule allFunctionsRevertIfCanceled(method f) filtered { f -> !f.isView } {
        env e; calldataarg args;
        uint256 pId = e.msg.value;
        require(isCanceled(pId));
        requireInvariant noBothExecutedAndCanceled(pId);
        f@withrevert(e,args);
        assert(lastReverted == true, "Function was not reverted");
    }