# 4.1. Simple invariants examples#

Here are two simple examples of invariants. The second example Ball Game also highlights a subtle point of using invariants.

## A simple example#

In the folder simple_voting is a simple voting contract Voting.sol, shown below.

```
contract Voting {
mapping(address => bool) internal _hasVoted;
uint256 public votesInFavor;
uint256 public votesAgainst;
uint256 public totalVotes;
function vote(bool isInFavor) public {
require(!_hasVoted[msg.sender]);
_hasVoted[msg.sender] = true;
totalVotes += 1;
if (isInFavor) {
votesInFavor += 1;
} else {
votesAgainst += 1;
}
}
function hasVoted(address voter) public view returns (bool) {
return _hasVoted[voter];
}
}
```

A simple invariant of this contract is:
`votesInFavor + votesAgainst == totalVotes`

, which we express as an
invariant in Voting.spec.
The spec also contains two translations of the invariant to a rule, one correct and the
other wrong:

```
invariant sumResultsEqualsTotalVotes()
votesInFavor() + votesAgainst() == to_mathint(totalVotes());
```

```
rule sumResultsEqualsTotalVotesAsRule(method f) {
// Precondition
require votesInFavor() + votesAgainst() == to_mathint(totalVotes());
env e;
calldataarg args;
f(e, args);
assert (
votesInFavor() + votesAgainst() == to_mathint(totalVotes()),
"Sum of votes should equal total votes"
);
}
```

```
rule sumResultsEqualsTotalVotesWrong() {
assert (
votesInFavor() + votesAgainst() == to_mathint(totalVotes()),
"Sum of votes should equal total votes"
);
}
```

Running the Certora Prover verifies the invariant, and also the rule
`sumResultsEqualsTotalVotesAsRule`

(which is the translation of the invariant’s
induction step translation to a rule).
While the naive translation to a rule in `sumResultsEqualsTotalVotesWrong`

fails,
since it doesn’t have the necessary precondition.

Note

The invariant has another advantage over the rule besides its brevity – it also verifies the invariant holds after the constructor. In contrast, a parametric rule will not checked for the case where the parametric method is the constructor.