4.5. Ghost exercises¶

Simple voting contract¶

This exercise refers to the simple Voting contract.

Use a ghost and an invariant to prove that if _hasVoted changed then the vote method was called.
Use a ghost and an invariant to prove that the values of _hasVoted can only change from false to true.
Write a complete spec for the Voting contract, using ghosts, invariants and rules.
Check that your spec passes without violations on Voting and also catches the bugs in the five buggy implementations:
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¶

Using Gambit to test your spec¶

Gambit is a Certora tool that automatically generates random 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¶

To run the Prover on all mutations we need a Prover configuration file (see Using config files) with a mutations object.
Voting.conf includes a simple mutations object. It simply specifies the file to be mutated as Voting.sol.
From the lesson4_invariants/simple_voting/ folder run the following command:
```
certoraMutate Voting.conf
```
This will run the Voting.spec on all mutations (asynchronously), sending jobs to the server.
After all the verification jobs have been sent to the cloud, you can follow the progress of your test at the Mutation Tests Dashboard.

Mutation tests dashboard¶
View the report on the provided link once the test is completed. Below is an example of a mutation test report.

Mutation test 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.

Use a ghost and a hook to indicate that someone placed some bid.
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¶

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.