Certora / tutorials-code

Certora tutorials
MIT License
19 stars 24 forks source link

Constructor ghost corruption #21

Open Czar102 opened 1 year ago

Czar102 commented 1 year ago

pr: #20

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: included in the above verification, see votedFunctionIsVotedMapping, preferLastVotedHigh, onlyVotingCanChangeTheWinner and viewNeverRevert.

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

Really hope this one is interesting. Definitely check out the description in the pr!