(TOB) Non-exhaustive list of system properties

[anishnaik]

A non-exhaustive list of system properties that should not be violated. Can be used as a base for writing fuzz tests.

FranchiserFactory

recall

• votingToken.balanceOf(msg.sender) should increase by the sum of the votingToken balances of the delegatee subtree.
• Should only revert if called on a Franchiser that msg.sender did not deploy (pre-condition)
• Should not revert otherwise

fund

• votingToken.balanceOf(msg.sender) should decrease by _amount
• votingToken.balanceOf(franchiser) should increase by _amount
• franchiser.code.size > 0
• votingToken.getVotes(delegatee) should increase by _amount
• Should revert if votingToken.balanceOf(msg.sender) < _amount (pre-condition)
• Should revert if franchiser.delegatee != address(0)
• Should not revert otherwise

Franchiser

subDelegate

• franchiser.code.size > 0
• votingToken.balanceOf(franchiser) should increase by _amount
• votingToken.balanceOf(address(this)) should decrease by _amount
• votingToken.getVotes(subDelegatee) should increase by _amount
• votingToken.getVotes(delegatee) should decrease by _amount
• Should revert if _subDelegatees.length() > maximumSubDelegatees
• Should revert if votingToken.balanceOf(address(this)) < _amount (pre-condition)
• Should not revert otherwise

unSubDelegate

• votingToken.balanceOf(address(this)) should increase by the sum of the votingToken balances of the subDelegatee subtree.
• Should only revert if msg.sender != delegatee (pre-condition)
• Should not revert otherwise

recall

• votingToken.balanceOf(to) should increase by the sum of the votingToken balances of all sub-delegatee subtrees in the _subDelegatees EnumerableSet.
• Should only revert if msg.sender != owner (pre-condition)
• Should not revert otherwise