3.2. Borda count election

This example of a Borda count election is found in the Borda folder. In the IBorda.sol file, you will find a description of the system and the interface that should be implemented by the contracts.

Read Borda.sol and Borda.spec to understand the system and the properties. You might encounter new features of CVL which later lessons address. The goal in this lesson is to practice understanding violations.

Tip

The bugs are relatively simple and can easily be found manually. Avoid looking for bugs manually before running the Prover. Instead, follow the Prover’s counter-examples to locate the bugs. Counter-examples may vary from one run to the other, we provide links and hints to a run which may differ from your own run.

Look at the following links (or run the provided conf files) of four faulty implementations and understand the violation.

  1. Results of verification Borda Bug1 Report , run with BordaBug1.conf

  2. Results of verification Borda Bug2 Report , run with BordaBug2.conf

  3. Results of verification Borda Bug3 Report , run with BordaBug3.conf

  4. Results of verification Borda Bug4 Report , run with BordaBug4.conf

Tip

Use the file tree view (third icon on the left panel) to view the files in this verification run to check your conclusions.

Hints for Borda

Hint for BordaBug1.sol

Start with the failing assert of integrityPoints, find the term that is false:

../_images/BordaBug1Step1.png

Next, look at the values before the call to vote() either in the Global State of the initial state the rule started with, or follow the return values from the calls to points() before the call to vote().

../_images/BordaBug1Step2.jpg

Have you noticed the values of s and f? Use the variables value view at the right hand side.

Hint for BordaBug2.sol

Multiple rules fail on this version of the code. Take a look at noEffect, a parametric rule, which has an entry for each checked method. The rule fails on vote(). Notice the unexpected change to points. You can drill into the execution of vote(). See store and load operations as well as internal function calls. Does anything look unexpected from a correct implementation of vote()?

../_images/BordaBug2Step1.jpg
Hint for BordaBug3.sol

Understanding reverting condition might be tricky, as some of them are compiler-generated. The Prover provides as much information as possible. Here it is clear.

../_images/BordaBug3.jpg
Hint for BordaBug4.sol

One of the nice features of the Certora Prover is that parametric rules and invariants are checked against all external functions. A newly added function is checked without any modification of the spec.

The best way to understand the coverage of the spec is via bug injection. Our CertoraMutate and Gambit tools help performing this task. According to the Borda mutation report the coverage is 100%, which means that all mutants were caught by at least one rule. However, the type of mutants Gambit generates is limited and there might be an injected bug that will point at a missing rule.