Voting process

Basic voting process

This archetype defines a basic voting process. The chairman is responsible for registering voters. The use of the mutable extension gives the chairman the extra right to modify the voting agenda, in Created state only.

The result of the vote is computed with the bury action: winners are ballots with the highest number of votes.

voting_process.arl
archetype voting_process
variable[%transferable%] chairperson : role = @tz1chairperson
(* vote start *)
variable[%mutable chairperson (instate (Created))%] startDate : date = 2019-11-12T00:00:00
(* vote deadline *)
variable[%mutable chairperson (instate (Created))%] deadline : date = 2020-11-12T00:00:00
asset voter identified by addr {
addr : role;
hasVoted : bool
}
asset ballot identified by value {
value : string;
nbvotes : int;
}
asset winner {
winvalue : string
}
(* state machine *)
states =
| Created initial with { s1 : winner.isempty(); }
| Voting with { s2 : winner.isempty(); }
| Buried
action register (v : role) {
called by chairperson
require {
c1 : state = Created;
}
effect {
voter.add({ addr = v; hasVoted = false })
}
}
transition start () from Created {
to Voting when { now > startDate }
}
action vote (val : pkey of ballot) {
require {
c2 : voter.contains(caller);
c3 : state = Voting;
c4 : voter.get(caller).hasVoted = false;
}
effect {
voter.update (caller, { hasVoted = true });
if ballot.contains(val) then
ballot.update(val,{ nbvotes += 1})
else
ballot.add({ value = val; nbvotes = 1})
}
}
transition bury () from Voting {
require {
c5 : now > deadline;
}
to Buried
with effect {
let nbvotesMax = ballot.max(the.nbvotes) in
for b in ballot do
if (b.nbvotes = nbvotesMax)
then winner.add({ winvalue = b.value })
done
}
}
specification {
contract invariant s3 {
startDate < deadline
}
contract invariant s4 {
(voter.select(the.hasVoted = true)).count() = ballot.sum(the.nbvotes)
}
contract invariant s5 {
forall w in winner,
forall b in ballot,
let some wb = ballot.get(w.winvalue) in
b.nbvotes <= wb.nbvotes
otherwise false
}
}