Adds certora spec for Ownable2Step

[spalladino]

Adds a certora spec for formally verifying Ownable2Step. Includes the rules:

• transferOwnershipSetsPendingOwner
• onlyCurrentOwnerCanCallOnlyOwner: verifies that transfer, renounce, and user functions decorated with onlyOwner can indeed only be called by the current owner
• onlyPendingOwnerCanAccept
• renounceDoesNotRequireTwoSteps

[Amxx]

What about a rule like

    oldOwner = owner();
    oldPendingOwner = pendingOwner();
    
    env e;
    method f;
    calldataarg args;
    f(e, args);
    
    assert (
        owner() != oldOwner ||
        pendingOwner() != oldPendingOwner
    ) => (
        msg.sender == oldOwner || 
        msg.sender == oldPendingOwner
    );
    
    assert owner() != oldOwner => pendingOwner() == address(0);

[spalladino]

@Amxx added!

[frangio]

Superceded by https://github.com/OpenZeppelin/openzeppelin-contracts/pull/4094.