Skip to content

Refactored Tutorial Lesson 2 #27

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Refactored Tutorial Lesson 2 #27

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9183c27
Renamed sample_conf -> ERC20
remedcu Nov 24, 2023
e76f48f
Created ERC20Fixed conf file
remedcu Nov 24, 2023
7eb6c00
Refactored ERC20Fixed specs
remedcu Nov 24, 2023
7bf826c
solc expects one argument
remedcu Nov 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion lesson2_started/erc20/sample_conf.conf → lesson2_started/erc20/ERC20.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,5 +6,5 @@
"wait_for_results": "all",
"rule_sanity": "basic",
// Note: json5 supports comments!
"msg": "First run using .conf file"
"msg": "ERC20 initial run using .conf file"
}
9 changes: 9 additions & 0 deletions lesson2_started/erc20/ERC20Fixed.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
{
"files": [
"ERC20.sol"
],
"verify": "ERC20:ERC20Fixed.spec",
"wait_for_results": "all",
"rule_sanity": "basic",
"msg": "ERC20Fixed run using .conf file"
}
7 changes: 3 additions & 4 deletions lesson2_started/erc20/ERC20Fixed.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,18 +24,17 @@ methods
rule transferSpec(address recipient, uint amount) {

env e;
address sender = e.msg.sender; // A convenient alias

// `mathint` is a type that represents an integer of any size
mathint balance_sender_before = balanceOf(e.msg.sender);
mathint balance_sender_before = balanceOf(sender);
mathint balance_recip_before = balanceOf(recipient);

transfer(e, recipient, amount);

mathint balance_sender_after = balanceOf(e.msg.sender);
mathint balance_sender_after = balanceOf(sender);
mathint balance_recip_after = balanceOf(recipient);

address sender = e.msg.sender; // A convenient alias

// Operations on mathints can never overflow or underflow.
assert recipient != sender => balance_sender_after == balance_sender_before - amount,
"transfer must decrease sender's balance by amount";
Expand Down
4 changes: 2 additions & 2 deletions lesson2_started/erc20/TotalGreaterThanUser.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,12 +7,12 @@
*
* First run only the rule `totalSupplyAfterMint`:
*
* certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc --rule totalSupplyAfterMint
* certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc solc8.0 --rule totalSupplyAfterMint
*
* This rule will fail due to the Prover's tendency to over-approximate the states.
* Now run the fixed rule `totalSupplyAfterMintWithPrecondition`:
*
* certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc --rule totalSupplyAfterMintWithPrecondition
* certoraRun ERC20.sol --verify ERC20:TotalGreaterThanUser.spec --solc solc8.0 --rule totalSupplyAfterMintWithPrecondition
*
* Do you understand why the second rule passed?
*/
Expand Down