Winner manipulation spec

[Czar102]

Hi, displaying info below:

pr: #12

A run of the new BordaMissingRule.spec on the original Borda.sol that is verified is here

A run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug is here

Reports of all previously acknowledged bounty specs on BordaNewBug.sol, these specs will be found in the bounty_specs folder: included in the previous verification, see votedFunctionIsVotedMapping

A run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug is here

Thanks for the challenge again!

[nd-certora]

can you please check if this is covered by
#7

[Czar102]

This is for sure partially covered by #7, I will check if I can produce an implementation that passes spec in #7 but fails this spec.

[Czar102]

The BordaNewBug.sol from the above verification in an example of a contract compliant with spec in #7, but where a vote manipulation is caught by this rule.
cc @imsrybr0

edit. demonstrated here

[nd-certora]

very interesting mutation, agree that it is not covered by the previous missing spec . Acknowledged as #3