From 9183c270e0b7bc1ab40f3d1be0260a13d1a8dfcf Mon Sep 17 00:00:00 2001 From: Shebin John Date: Fri, 24 Nov 2023 14:34:37 +0530 Subject: [PATCH 1/4] Renamed sample_conf -> ERC20 --- lesson2_started/erc20/{sample_conf.conf => ERC20.conf} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename lesson2_started/erc20/{sample_conf.conf => ERC20.conf} (78%) diff --git a/lesson2_started/erc20/sample_conf.conf b/lesson2_started/erc20/ERC20.conf similarity index 78% rename from lesson2_started/erc20/sample_conf.conf rename to lesson2_started/erc20/ERC20.conf index 32fb364..24af8ef 100644 --- a/lesson2_started/erc20/sample_conf.conf +++ b/lesson2_started/erc20/ERC20.conf @@ -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" } From e76f48f9c171918a654db038f0932bddc7979181 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Fri, 24 Nov 2023 14:35:08 +0530 Subject: [PATCH 2/4] Created ERC20Fixed conf file --- lesson2_started/erc20/ERC20Fixed.conf | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 lesson2_started/erc20/ERC20Fixed.conf diff --git a/lesson2_started/erc20/ERC20Fixed.conf b/lesson2_started/erc20/ERC20Fixed.conf new file mode 100644 index 0000000..6173100 --- /dev/null +++ b/lesson2_started/erc20/ERC20Fixed.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "ERC20.sol" + ], + "verify": "ERC20:ERC20Fixed.spec", + "wait_for_results": "all", + "rule_sanity": "basic", + "msg": "ERC20Fixed run using .conf file" +} From 7eb6c00eec08c90fd79ba2fac87f7ffea7bd71f3 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Fri, 24 Nov 2023 14:35:41 +0530 Subject: [PATCH 3/4] Refactored ERC20Fixed specs --- lesson2_started/erc20/ERC20Fixed.spec | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/lesson2_started/erc20/ERC20Fixed.spec b/lesson2_started/erc20/ERC20Fixed.spec index ab987fc..52a65f2 100644 --- a/lesson2_started/erc20/ERC20Fixed.spec +++ b/lesson2_started/erc20/ERC20Fixed.spec @@ -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"; From 7bf826c7ca6953d5b96d276dcb500543557f5c50 Mon Sep 17 00:00:00 2001 From: Shebin John Date: Fri, 24 Nov 2023 15:14:00 +0530 Subject: [PATCH 4/4] solc expects one argument --- lesson2_started/erc20/TotalGreaterThanUser.spec | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lesson2_started/erc20/TotalGreaterThanUser.spec b/lesson2_started/erc20/TotalGreaterThanUser.spec index c0749d7..d71b004 100644 --- a/lesson2_started/erc20/TotalGreaterThanUser.spec +++ b/lesson2_started/erc20/TotalGreaterThanUser.spec @@ -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? */