Open zapaz opened 1 year ago
Missing specs ensures that we can have more than one voter Buggy contract enforce only one voter, the cheater that can vote for himself Existing oneCanVote did not catch this bug
Missing spec : #18
A run of the new BordaMissingRule.spec on the original Borda.sol that is verified https://prover.certora.com/output/88083/ee33b030b2f346968a6e75a7ebd389bc/?anonymousKey=832264b21688ea4c31b2c6bcd26e20011b251bb4
A run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug https://prover.certora.com/output/88083/1d302e93e9ea43ba8fe8366f86984e71/?anonymousKey=ce8882019f6167ff1ff0243fcd6708ca9654e889
A run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug https://prover.certora.com/output/88083/6ee308b0f0c14987aaf5c215e10874e2/?anonymousKey=0f97fbf396b84bd42090d0ad47b2144c341c1d80
Missing specs ensures that we can have more than one voter Buggy contract enforce only one voter, the cheater that can vote for himself Existing oneCanVote did not catch this bug
Missing spec : #18
A run of the new BordaMissingRule.spec on the original Borda.sol that is verified https://prover.certora.com/output/88083/ee33b030b2f346968a6e75a7ebd389bc/?anonymousKey=832264b21688ea4c31b2c6bcd26e20011b251bb4
A run of Borda.spec on BordaNewBug.sol showing the existing spec misses the bug https://prover.certora.com/output/88083/1d302e93e9ea43ba8fe8366f86984e71/?anonymousKey=ce8882019f6167ff1ff0243fcd6708ca9654e889
A run of BordaMissingRule.spec on BordaNewBug.sol showing your rule catches the bug https://prover.certora.com/output/88083/6ee308b0f0c14987aaf5c215e10874e2/?anonymousKey=0f97fbf396b84bd42090d0ad47b2144c341c1d80