4.5. Ghost exercises#

Simple voting contract#

This exercise refers to the simple Voting contract.

  1. Use a ghost and an invariant to prove that if _hasVoted changed then the vote method was called.

  2. Use a ghost and an invariant to prove that the values of _hasVoted can only change from false to true.

  3. Write a complete spec for the Voting contract, using ghosts, invariants and rules.

  4. Check that your spec passes without violations on Voting and also catches the bugs in the five buggy implementations:

  5. Check that your spec catches all mutations generated by Gambit (see Using Gambit to test your spec below, which provides an example using Gambit).

Hints#

Solution

The full solution is at Voting_solution.spec.

Using Gambit to test your spec#

Gambit is a Certora tool that automatically generates mutations (bugs) in the code. This is useful for testing the coverage of your spec. See the Mutant generation page for Gambit installation instructions.

Gambit can be used with the Certora Prover to automatically run your spec on all generated mutations. This is explained in detail in Using Gambit with the Prover. Here, we provide an example that runs Voting.spec on all mutations.

Gambit example#

  1. To run the Prover on all mutations we need a mutation configuration file and a Prover configuration file (see Using config files).

    1. A basic mutation configuration file for this is found at mutate.conf. This file simply specifies the file to be mutated as Voting.sol.

    2. We’ll use the Prover configuration file found at Voting.conf.

  2. From the lesson4_invariants/simple_voting/ folder run the following command:

    certoraMutate --prover_conf Voting.conf --mutation_conf mutate.mconf
    

    This will run the Voting.spec on all mutations (asynchronously), sending jobs to the server.

  3. The script will notify you how to view the results once all jobs are completed. Most likely you will be notified that:

    You will receive an email notification when this process is completed.
    

    This email will contain a link to the report.

  4. View the report on the provided link. Below is an example of a mutation testing report.

Mutation testing report example

Mutation testing report example#

English auction#

This exercise is about the EnglishAuction.sol contract. We’ve met this contract before in the English auction basic exercise. To make it harder, we abandon the assumption that address(0) cannot place a bid.

  1. Use a ghost and a hook to indicate that someone placed some bid.

  2. Prove that highestBid is strictly greater than all other bids, provided someone has placed a bid.

Setup note#

The EnglishAuction contract calls other contracts. For example, it calls ERC721Mock.transferFrom. If the Prover is not certain what code is called, it will over-approximate by assuming anything can happen. In particular, this can cause ghost variables to have arbitrary values. We will learn more about this in the next lesson.

For now, to avoid such issues, ensure you config file contains the following lines:

{
    "files": [
	// Declare all three contracts
        "lesson4_invariants/auction/EnglishAuction.sol:EnglishAuction",
        "lesson4_invariants/auction/EnglishAuction.sol:ERC721Mock",
        "lesson4_invariants/auction/EnglishAuction.sol:ERC20Mock"
    ],
    "link": [
	// Link EnglishAuction storage variables to contracts
        "EnglishAuction:nft=ERC721Mock",
	"EnglishAuction:token=ERC20Mock"
    ],

These lines will tell the Prover to always associate the EnglishAuction variables nft and token with the contracts ERC721Mock and ERC20Mock respectively.

Hints#

Solution

The full solution is at EnglishAuction_strict.spec.

Funds managers#

This exercise is for the Manager.sol contract, which we’ve met in Funds managers exercise. The exercise now is to prove that every active manager manages a fund. Use a ghost when writing the invariants and verify them using the Certora Prover.

Hints#

Solution

The full solution is at Manager_ghost.spec.