import "GovernorBase.spec"

using ERC20VotesHarness as erc20votes

methods {
    ghost_sum_vote_power_by_id(uint256) returns uint256 envfree
    // castVote(uint256, uint8) returns uint256
    // castVoteBySig(uint256,uint8,uint8,bytes32,bytes32) returns uint256

    quorum(uint256) returns uint256
    proposalVotes(uint256) returns (uint256, uint256, uint256) envfree

    quorumNumerator() returns uint256
    _executor() returns address

    erc20votes._getPastVotes(address, uint256) returns uint256

    getExecutor() returns address

    //0xe38335e5 => DISPATCHER(true)
}

//////////////////////////////////////////////////////////////////////////////
///////////////////////////////// GHOSTS /////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////

ghost hasVoteGhost(uint256) returns uint256 {
    init_state axiom forall uint256 pId. hasVoteGhost(pId) == 0;
}

hook Sstore _proposalVotes[KEY uint256 pId].hasVoted[KEY address user] bool current_voting_State (bool old_voting_state) STORAGE{
   havoc hasVoteGhost assuming forall uint256 p. ((p == pId && current_voting_State && !old_voting_state) ? (hasVoteGhost@new(p) == hasVoteGhost@old(p) + 1)  :
                                                 (hasVoteGhost@new(p) == hasVoteGhost@old(p)));
}

ghost sum_all_votes_power() returns uint256 {
	init_state axiom sum_all_votes_power() == 0;
}

hook Sstore ghost_sum_vote_power_by_id [KEY uint256 pId] uint256 current_power(uint256 old_power) STORAGE {
	havoc sum_all_votes_power assuming sum_all_votes_power@new() == sum_all_votes_power@old() - old_power + current_power;
}

ghost tracked_weight(uint256) returns uint256 {
	init_state axiom forall uint256 p. tracked_weight(p) == 0;
}
ghost sum_tracked_weight() returns uint256 {
	init_state axiom sum_tracked_weight() == 0;
}

ghost votesAgainst() returns uint256 {
    init_state axiom votesAgainst() == 0;
}

ghost votesFor() returns uint256 {
    init_state axiom votesFor() == 0;
}

ghost votesAbstain() returns uint256 {
    init_state axiom votesAbstain() == 0;
}

hook Sstore _proposalVotes [KEY uint256 pId].againstVotes uint256 votes(uint256 old_votes) STORAGE {
	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
    havoc votesAgainst assuming votesAgainst@new() == votesAgainst@old() - old_votes + votes;
}

hook Sstore _proposalVotes [KEY uint256 pId].forVotes uint256 votes(uint256 old_votes) STORAGE {
	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
    havoc votesFor assuming votesFor@new() == votesFor@old() - old_votes + votes;
}

hook Sstore _proposalVotes [KEY uint256 pId].abstainVotes uint256 votes(uint256 old_votes) STORAGE {
	havoc tracked_weight assuming forall uint256 p.(p == pId => tracked_weight@new(p) == tracked_weight@old(p) - old_votes + votes) &&
	                                            (p != pId => tracked_weight@new(p) == tracked_weight@old(p));
	havoc sum_tracked_weight assuming sum_tracked_weight@new() == sum_tracked_weight@old() - old_votes + votes;
    havoc votesAbstain assuming votesAbstain@new() == votesAbstain@old() - old_votes + votes;
}


ghost totalVotesPossible(uint256) returns uint256 {
	init_state axiom forall uint256 bn. totalVotesPossible(bn) == 0;
}

// Was done with _getVotes by mistake. Should check GovernorBasicHarness but _getVotes is from GovernorHarness
hook Sstore erc20votes._getPastVotes[KEY address uId][KEY uint256 blockNumber] uint256 voteWeight(uint256 old_voteWeight) STORAGE {
	havoc totalVotesPossible assuming forall uint256 bn.
	                                (bn == blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn) - old_voteWeight + voteWeight)
	                                && (bn != blockNumber => totalVotesPossible@new(bn) == totalVotesPossible@old(bn));
}

invariant checkGetVotesGhost(address uId, uint256 blockNumber, env e)
    erc20votes._getPastVotes(e, uId, blockNumber) == erc20votes.getPastVotes(e, uId, blockNumber)

rule whatCahnges(uint256 blockNumber, method f) {
    env e;
    calldataarg args;
    uint256 ghostBefore = totalVotesPossible(blockNumber);
    f(e,args);
    uint256 ghostAfter = totalVotesPossible(blockNumber);
    assert ghostAfter ==  ghostBefore, "ghost was changed";
}

//////////////////////////////////////////////////////////////////////////////
////////////////////////////// INVARIANTS ////////////////////////////////////
//////////////////////////////////////////////////////////////////////////////


/*
 * sum of all votes casted is equal to the sum of voting power of those who voted, per each proposal
 */
invariant SumOfVotesCastEqualSumOfPowerOfVotedPerProposal(uint256 pId) 
	tracked_weight(pId) == ghost_sum_vote_power_by_id(pId)
		
/*
 * sum of all votes casted is equal to the sum of voting power of those who voted
 */
invariant SumOfVotesCastEqualSumOfPowerOfVoted() 
	sum_tracked_weight() == sum_all_votes_power()
		
/*
* totalVoted >= vote(id)
*/
invariant OneIsNotMoreThanAll(uint256 pId) 
	sum_all_votes_power() >= tracked_weight(pId)


//NEED GHOST FIX	
/*
* totalVotesPossible >= votePower(id)
*/
invariant possibleTotalVotes(uint256 pId, env e) 
	tracked_weight(pId) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId))

invariant voteGettersCheck(uint256 pId, address acc, env e) 
	erc20votes.getPastVotes(e, acc, proposalSnapshot(pId)) <= erc20votes.getPastTotalSupply(e, proposalSnapshot(pId))

/*
* totalVotesPossible >= votePower(id)
*/
// invariant possibleTotalVotes(uint pId)
//invariant trackedVsTotal(uint256 pId) 
//	tracked_weight(pId) <= possibleMaxOfVoters(pId)


/*
rule someOtherRuleToRemoveLater(uint256 num){
    env e; calldataarg args; method f;
    uint256 x = hasVoteGhost(num);
    f(e, args);
    assert(false);
}
*/


/*
 * Checks that only one user is updated in the system when calling cast vote functions (assuming hasVoted is changing correctly, false->true, with every vote cast)
 */
rule oneUserVotesInCast(uint256 pId, uint8 sup, method f) filtered {f -> f.selector == castVote(uint256, uint8).selector || 
                                                                    f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector} {
    env e; calldataarg args;                                                            
    uint256 ghost_Before = hasVoteGhost(pId);                                           
    if (f.selector == castVote(uint256, uint8).selector)
    {
        castVote(e, pId, sup);
    } /*else if (f.selector == 0x7b3c71d3) {
        require(_pId_Harness() == proposalId);
        f(e,args);
    }*/ else if (f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector) {
        uint8 v; bytes32 r; bytes32 s;
        castVoteBySig(e, pId, sup, v, r, s);
    } else{
        f(e, args);
    }
    uint256 ghost_After = hasVoteGhost(pId);
    assert(ghost_After == ghost_Before + 1, "Raised by more than 1");
}


/*
 * Checks that in any call to cast vote functions only the sender's value is updated
 */
rule noVoteForSomeoneElse(uint256 pId, uint8 sup, method f) filtered {f -> f.selector == castVote(uint256, uint8).selector || 
                                                                          f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector} {
    env e; calldataarg args;
    address voter = e.msg.sender;
    address user;
    bool hasVotedBefore_Voter = hasVoted(e, pId, voter);
    bool hasVotedBefore_User = hasVoted(e, pId, user);
    require(!hasVotedBefore_Voter);
    if (f.selector == castVote(uint256, uint8).selector)
    {
        castVote(e, pId, sup);
    } /*else if (f.selector == 0x7b3c71d3) {
        require(_pId_Harness() == proposalId);
        f(e,args);
    }*/ else if (f.selector == castVoteBySig(uint256, uint8, uint8, bytes32, bytes32).selector) {
        uint8 v; bytes32 r; bytes32 s;
        castVoteBySig(e, pId, sup, v, r, s);
    } else{
        f(e, args);
    }
    bool hasVotedAfter_Voter = hasVoted(e, pId, voter);
    bool hasVotedAfter_User = hasVoted(e, pId, user);
    assert hasVotedBefore_Voter != hasVotedAfter_Voter => (user != voter => hasVotedBefore_User == hasVotedAfter_User);
}


rule votingWeightMonotonicity(method f){
    uint256 votingWeightBefore = sum_tracked_weight();

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

    uint256 votingWeightAfter = sum_tracked_weight();

    assert votingWeightBefore <= votingWeightAfter, "Voting weight was decreased somehow";
}


function callFunctionWithParams(method f, uint256 proposalId, env e) {
    address[] targets;
    uint256[] values;
    bytes[] calldatas;
    bytes32 descriptionHash;
    uint8 support;
    uint8 v; bytes32 r; bytes32 s;
	if (f.selector == callPropose(address[], uint256[], bytes[]).selector) {
		uint256 result = callPropose(e, targets, values, calldatas);
        require result == proposalId;
	} else if (f.selector == execute(address[], uint256[], bytes[], bytes32).selector) {
        uint256 result = execute(e, targets, values, calldatas, descriptionHash);
        require result == proposalId;
	} else if (f.selector == castVote(uint256, uint8).selector) {
		castVote(e, proposalId, support);
	//} else if  (f.selector == castVoteWithReason(uint256, uint8, string).selector) {
	//	castVoteWithReason(e, proposalId, support, reason);
	} else if (f.selector == castVoteBySig(uint256, uint8,uint8, bytes32, bytes32).selector) {
		castVoteBySig(e, proposalId, support, v, r, s);
	} else {
		calldataarg args;
		f(e,args);
	}
}

// run on ALex's branch to avoid tiomeouts: --staging alex/external-timeout-for-solvers
// --staging shelly/forSasha
rule hasVotedCorrelation(uint256 pId, method f, env e, uint256 bn) filtered {f -> f.selector != 0x7d5e81e2}{
    uint256 againstBefore = votesAgainst();
    uint256 forBefore = votesFor();
    uint256 abstainBefore = votesAbstain();
    //againstBefore, forBefore, abstainBefore = proposalVotes(pId);

    address acc = e.msg.sender;

    bool hasVotedBefore = hasVoted(e, pId, acc);
    uint256 votesBefore = getVotes(e, acc, bn);
    require votesBefore > 0;

    //calldataarg args;
    //f(e, args);
    callFunctionWithParams(f, pId, e);

    uint256 againstAfter = votesAgainst();
    uint256 forAfter = votesFor();
    uint256 abstainAfter = votesAbstain();
    //againstAfter, forAfter, abstainAfter = proposalVotes(pId);

    uint256 votesAfter = getVotes(e, acc, bn);
    bool hasVotedAfter = hasVoted(e, pId, acc);

    assert hasVotedBefore != hasVotedAfter => againstBefore <= againstAfter || forBefore <= forAfter || abstainBefore <= abstainAfter, "no correlation";
}


/*
* Check privileged operations
*/
rule privilegedOnly(method f, uint256 newQuorumNumerator){
    env e;
    calldataarg arg;
    uint256 quorumNumBefore = quorumNumerator(e);
    //require e.msg.sender == currentContract;

    f(e, arg);

    //updateQuorumNumerator(e, newQuorumNumerator);

    uint256 quorumNumAfter = quorumNumerator(e);

    address executorCheck = getExecutor(e);
    // address executorCheck = _executor(e);

    assert quorumNumBefore != quorumNumAfter => e.msg.sender == executorCheck, "non priveleged user changed quorum numerator";
}