Update Lesson 1 to CVL2 and config files

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }
 

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }
 

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }
 

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }
 

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }
 

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }
 

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }
 

.gitignore

@@ -25,6 +25,11 @@ cache/
 .certora*
 .last_confs
 certora_*
+.zip-output-url.txt
 
 # mac
 .DS_Store
+
+# vim
+.*.swp
+.*.swo

01.Lesson_GettingStarted/ERC20Lesson1/ERC20.spec

@@ -1,43 +1,45 @@
-/***
+/**
  * # ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is an example specification for a generic ERC20 contract. It contains several
+ * simple rules verifying the integrity of the transfer function.
+ * To run, execute the following command in terminal:
+ * 
+ * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ * 
+ * One of the rules here is badly phrased, and results in an erroneous fail.
+ * Understand the counter example provided by the Prover and then run the fixed
+ * spec:
  *
- * certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
- *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
+ // Operations on mathints can never overflow nor underflow
  assert balance_sender_after == balance_sender_before - amount,
  "transfer must decrease sender's balance by amount";
 
@@ -46,33 +48,39 @@ rule transferSpec {
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/ERC20Fixed.spec

@@ -1,81 +1,86 @@
-/***
- * # ERC20 Example
+/**
+ * # Fixed ERC20 Example
  *
- * This is an example specification for a generic ERC20 contract.
- * To run, execute the following command in terminal/cmd:
+ * This is the fixed version of ERC20.spec. Note the changes in rule `transferSpec`.
+ * Run using:
  *
- *certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
+ *certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
  *
- * A simple rule that checks the integrity of the transfer function. 
- *
- * Understand the counter example and then rerun:
- *
- * certoraRun ERC20.sol: --verify ERC20:ERC20Fixed.spec --solc solc8.0
+ * There should be no errors.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
-//// ## Part 1: Basic rules ////////////////////////////////////////////////////
 
-/// Transfer must move `amount` tokens from the caller's account to `recipient`
-rule transferSpec {
- address recip; uint256 amount;
+/// @title Transfer must move `amount` tokens from the caller's account to `recipient`
+rule transferSpec(address recipient, uint amount) {
 
  env e;
-address sender = e.msg.sender;
- // mathinttype that represents an integer of any size;
- mathint balance_sender_before = balanceOf(sender);
- mathint balance_recip_before = balanceOf(recip);
+
+ // `mathint` is a type that represents an integer of any size
+ mathint balance_sender_before = balanceOf(e.msg.sender);
+ mathint balance_recip_before = balanceOf(recipient);
 
- transfer(e, recip, amount);
+ transfer(e, recipient, amount);
 
- mathint balance_sender_after = balanceOf(sender);
- mathint balance_recip_after = balanceOf(recip);
+ mathint balance_sender_after = balanceOf(e.msg.sender);
+ mathint balance_recip_after = balanceOf(recipient);
 
- // operations on mathints can never overflow or underflow. 
- assert recip != sender => balance_sender_after == balance_sender_before - amount,
+ 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";
 
- assert recip != sender => balance_recip_after == balance_recip_before + amount,
+ assert recipient != sender => balance_recip_after == balance_recip_before + amount,
  "transfer must increase recipient's balance by amount";
 
- assert recip == sender => balance_sender_after == balance_sender_before,
+ assert recipient == sender => balance_sender_after == balance_sender_before,
  "transfer must not change sender's balancer when transferring to self";
 }
 
 
-/// Transfer must revert if the sender's balance is too small
-rule transferReverts {
- env e; address recip; uint amount;
+/// @title Transfer must revert if the sender's balance is too small
+rule transferReverts(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) < amount;
 
- transfer@withrevert(e, recip, amount);
+ transfer@withrevert(e, recipient, amount);
 
  assert lastReverted,
- "transfer(recip,amount) must revert if sender's balance is less than `amount`";
+ "transfer(recipient,amount) must revert if sender's balance is less than `amount`";
 }
 
 
-/// Transfer must not revert unless
-/// the sender doesn't have enough funds,
-/// or the message value is nonzero,
-/// or the recipient's balance would overflow,
-/// or the message sender is 0,
-/// or the recipient is 0
-///
-/// @title Transfer doesn't revert
-rule transferDoesntRevert {
- env e; address recipient; uint amount;
+/** @title Transfer must not revert unless
+ * - the sender doesn't have enough funds,
+ * - or the message value is nonzero,
+ * - or the recipient's balance would overflow,
+ * - or the message sender is 0,
+ * - or the recipient is 0
+ */
+rule transferDoesntRevert(address recipient, uint amount) {
+ env e;
 
  require balanceOf(e.msg.sender) > amount;
- require e.msg.value == 0;
- require balanceOf(recipient) + amount < max_uint;
+ require e.msg.value == 0; // No payment
+
+ // This requirement prevents overflow of recipient's balance.
+ // We convert `max_uint` to type `mathint` since:
+ // 1. a sum always returns type `mathint`, hence the left hand side is `mathint`,
+ // 2. `mathint` can only be compared to another `mathint`
+ require balanceOf(recipient) + amount < to_mathint(max_uint);
+
+ // Recall that `address(0)` is a special address that in general should not be used
  require e.msg.sender != 0;
  require recipient != 0;
 

01.Lesson_GettingStarted/ERC20Lesson1/Parametric.spec

@@ -1,41 +1,53 @@
-/***
- * # ERC20 Example
+/**
+ * # ERC20 Parametric Example
  *
- * This is an example specification for a generic ERC20 contract.
- * 
- * To simulate the execution of all functions in the main contract, 
- * you can define a method argument in the rule and use it in a statement.
- * Run:
- * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "parametric rule"
+ * Another example specification for an ERC20 contract. This one using a parametric rule,
+ * which is a rule that encompasses all the methods in the current contract. It is called
+ * parametric since one of the rule's parameters is the current contract method.
+ * To run enter:
  * 
+ * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
+ *
+ * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
+ * results and understand the counter example - which discovers a weakness in the
+ * current contract.
  */
 
-methods {
- // When a function is not using the environment (e.g., msg.sender), it can be declared as envfree 
- balanceOf(address) returns(uint) envfree
- allowance(address,address) returns(uint) envfree
- totalSupply() returns(uint) envfree
+// The methods block below gives various declarations regarding solidity methods.
+methods
+{
+ // When a function is not using the environment (e.g., `msg.sender`), it can be
+ // declared as `envfree`
+ function balanceOf(address) external returns (uint) envfree;
+ function allowance(address,address) external returns(uint) envfree;
+ function totalSupply() external returns (uint) envfree;
 }
 
 
-//// ## Part 2: parametric rules ///////////////////////////////////////////////
-
-/// If `approve` changes a holder's allowance, then it was called by the holder
-rule onlyHolderCanChangeAllowance {
- address holder; address spender;
+/// @title If `approve` changes a holder's allowance, then it was called by the holder
+rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {
 
+ // The allowance before the method was called
  mathint allowance_before = allowance(holder, spender);
 
- method f; env e; calldataarg args; 
+ env e;
+ calldataarg args; // Arguments for the method f
  f(e, args); 
 
+ // The allowance after the method was called
  mathint allowance_after = allowance(holder, spender);
 
  assert allowance_after > allowance_before => e.msg.sender == holder,
- "approve must only change the sender's allowance";
-
- assert allowance_after > allowance_before =>
- (f.selector == approve(address,uint).selector || f.selector == increaseAllowance(address,uint).selector),
- "only approve and increaseAllowance can increase allowances";
+ "only the sender can change its own allowance";
+
+ // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
+ assert (
+ allowance_after > allowance_before =>
+ (
+ f.selector == sig:approve(address, uint).selector ||
+ f.selector == sig:increaseAllowance(address, uint).selector
+ )
+ ),
+ "only approve and increaseAllowance can increase allowances";
 }