certora / tutorials-code Goto Github PK

Certora tutorials

License: MIT License

Solidity 57.69% Ruby 37.50% Python 4.81%

tutorials-code's Introduction

Tutorials code

This repository contains the code examples for the Certora Prover Tutorials. The Certora Prover is a formal verification tool for smart contract. The tutorials are part of the Certora Prover Documentation.

tutorials-code's People

Contributors

Stargazers

Watchers

tutorials-code's Issues

Bug Coverage

Overview:

Set winner and Pause voting.

PR : https://github.com/Certora/tutorials-code/pull/6
BordaMissingRule.spec

A run of the new BordaMissingRule.spec on the original Borda.sol ->> https://prover.certora.com/output/547/9c7f0d95bde54d29b8d69e0ec27cfc51?anonymousKey=32f03dcc32835daf5c901e9306805db81ed9903c

A run of the new BordaMissingRule.spec on the BordaNewBug.sol ->> https://prover.certora.com/output/547/2160830e2fd74ebc8d40a8e3659aac42?anonymousKey=46ff60261303d503578de0fa3964c3eeafa9c512

A run of the new Borda.spec on the BordaNewBug.sol ->>
https://prover.certora.com/output/547/499585e8e92c4538980b7f0d48b528cd?anonymousKey=0730884c87d843db86f6027ce846e67062a93da2

Solution for the prover challenge

Hi!
I submitted a PR #4 with a solution to the challenge. Ran so fast that misplaced where should I put the prover reports and put them in the PR. Pasting them also here:

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: none

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

It was really fun, learned a bunch on CVL grammar and invariant thinking. Thanks a lot :)

Constructor doesn't change state

pr: #22

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 and onlyVotingCanChangeTheWinner.

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

Thanks!

Winner manipulation spec

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!

Forbid view function reverts

Hi, displaying info below:

pr: #16

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

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

Thanks for the challenge yet again!

Constructor ghost corruption

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

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!

Solution to Borda

Hi team here is my solution
https://github.com/peritoflores/tutorials-code

Missing spec

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