4.2. Basic exercises

ERC20

ERC20.sol contains an ERC20 implementation. Write an invariant for ERC20 verifying that address(0) always has zero balance. Run the invariant on ERC20.sol and discover the violation in the contract.

Important

Remember to use the optimistic_loop option, see Important: Optimistic loop.

Hints

CVL types

You can use balanceOf(0) in CVL without casting it to address.

Solution

A solution is available in zero.spec.

English auction basic exercise

In EnglishAuction.sol, you will find the implementation of a simple English Auction for selling an NFT. The auction process and additional features are described in the solidity file. Here is a summary of the main details:

1. The seller of the NFT deploys the contract and sets the NFT and the token to be used.

2. A participant can bid a certain amount to become the new highest bidder.

3. Once the bid has ended the highest bidder gets the NFT, and the seller receives the highest bidder’s tokens.

Exercises

Write a spec for EnglishAuction.sol containing the following two invariants.

1. The highestBid is higher than or equal to any other bid.

2. The bid of the highestBidder equals the highestBid. You may assume that address(0) cannot place a bid.

Hints

Methods block hint

You will need to define the getters as envfree.

Highest bidder hint

What is the initial value of the highest bidder?

Solution

A full solution is available in EnglishAuction.spec.