Voting process

Basic voting process

This archetype defines a basic voting process. The chairman is responsible for registering voters.

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

archetype voting_process
variable chairperson : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
variable chairperson_tmp : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
(* vote start *)
variable startDate : date = 2019-11-12T00:00:00
(* vote deadline *)
variable 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
entry 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 }
}
entry vote (val : pkey<ballot>) {
require {
c2 : voter.contains(caller);
c3 : state = Voting;
c4 : voter[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 () {
require {
c5 : now > deadline;
}
from Voting
to Buried
with effect {
var nbvotesMax : int = 0;
for b in ballot do
nbvotesMax := max(nbvotesMax, ballot[b].nbvotes)
done;
for b in ballot do
if (ballot[b].nbvotes = nbvotesMax)
then winner.add({ winvalue = ballot[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[w.winvalue] in
b.nbvotes <= wb.nbvotes
otherwise false
}
}
entry assign_new_chairperson (newrole : role) {
called by chairperson
effect {
chairperson_tmp := newrole;
}
}
entry confirm_chairperson () {
called by chairperson_tmp
effect {
chairperson := chairperson_tmp;
}
}
entry set_startDate (newstartDate : date) {
called by chairperson
require {
set_startDate_c1 : state = Created;
}
effect {
startDate := newstartDate
}
}
entry set_deadline (newdeadline : date) {
called by chairperson
require {
set_deadline_c1 : state = Created;
}
effect {
deadline := newdeadline
}
}
Edit on GitHub