search

Certora / tutorials-code

Certora tutorials
MIT License
19 stars 24 forks source link

Winner manipulation spec #13

Open Czar102 opened 1 year ago

Czar102 commented 1 year ago

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 commented 1 year ago

can you please check if this is covered by https://github.com/Certora/tutorials-code/issues/7

Czar102 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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