\documentclass[10pt]{llncs}
%\usepackage{anuthesis}
%\usepackage{acmnew-xref}
%\usepackage{todonotes}
\usepackage{listings}
\usepackage{url}
\usepackage{subfig}
\usepackage{tikz}
\usepackage{varwidth}
\usepackage{mathtools}
\usepackage{color}
\usepackage{xcolor}
\usepackage{enumerate}
\usepackage[gen]{eurosym}
\pagestyle{plain}
\newcommand{\pavoter}{Pr\^et \`a Voter}
\newcommand{\impsml}{\texttt{IMP}}
\newcommand{\imphol}{\texttt{IMPHOL}}
\newcommand{\spechol}{\texttt{SPECHOL}}
%\definecolor{grey}{rgb}{0.5,0.5,0.5}
\definecolor{grey}{cmyk}{0.43, 0.35, 0.35,0.01}
\usetikzlibrary{shapes,positioning,arrows}
\tikzstyle{component}=
[rectangle,draw,text centered,rounded corners,minimum height=6em,minimum width=6em]
\lstset{language=ML,
basicstyle=\ttfamily\footnotesize,
numberfirstline=true,
firstnumber=1,
numbers=left,
numberstyle=\tiny\color{grey},
numbersep=10pt,
stepnumber=1,
breaklines=false,
showstringspaces=false,
showlines=true,
escapeinside={\%*},
captionpos=t,
frame=tl,
%framexleftmargin=1em,
%xleftmargin=1em,
xleftmargin=17pt,
framexleftmargin=4pt,
framexrightmargin=5pt,
framexbottommargin=4pt,
framextopmargin=4pt,
rulecolor=\color{grey},
frameshape={ynn}{y}{n}{ynn},
tabsize=4
}
\usepackage{caption}
\DeclareCaptionFont{white}{\color{white}}
\DeclareCaptionFormat{listing}{\colorbox[cmyk]{0.43, 0.35, 0.35,0.01}{\parbox{\textwidth}{\hspace{15pt}#1#2#3}}}
\captionsetup[lstlisting]{format=listing,labelfont=white,textfont=white, singlelinecheck=false, margin=0pt, font={bf,footnotesize}}
\title{Machine-checked Reasoning About Complex Voting Schemes Using
Higher-order Logic}
%\author{Jeremy E Dawson, Rajeev Gor\'{e}, Thomas Meumann}
%\institute{Research School of Computer Science, Australian National University}
\begin{document}
\maketitle
\begin{abstract}
We describe how we first formally encoded the English-language
Parliamentary Act for the Hare-Clark Single Transferable
Vote-counting scheme used in the Australian state of Tasmania into
higher-order logic, producing \spechol. Based on this logical
specification, we then encoded an SML program to count ballots
according to this specification inside the interactive theorem
prover HOL4, giving us \imphol. We then manually transliterated the
program as a real SML program \impsml{}. We are currently verifying
that the formalisation of the implementation implies the
formalisation of the specification: that is, we are using the HOL4
interactive theorem prover to prove the implication \imphol{} $\to$
\spechol.
%Here, we outline our current progress.
\end{abstract}
% \begin{quote}
% \bf Dear Reviewers,
% \bigskip
% We are also extremely grateful for the long list of detailed
% suggestions for improving our initial paper.
% \bigskip
% Given your kindness, we have tried to take every suggestion into
% account. As suggested: we have left out large sections describing
% the details of preferential voting such as the Droop quota, Gregory
% transfer method etc; we have left out material on end-to-end voter
% verifiable systems and cryptographic details; and we have brought in
% new material which describes the work we have completed since
% submission.
% \bigskip
% We believe that the paper is now significantly better. We would be
% willing to make any further changes that you regard as essential
% within a day or two of notification.
% \bigskip
% best wishes,
% \smallskip
% raj
% \end{quote}
\section{Introduction}
Two fundamental principles in tallying an election are the
transparency and trustworthiness of the process. Strict protocols are
enforced when dealing with the ballot boxes and interested parties are
provided with the opportunity to scrutinise the tally while it is
being undertaken. Thus traditional manual vote-counting methods are
designed to ensure trustworthiness via scrutiny.
Despite these measures, manually counting ballots is still
error-prone. During the 2013 Senate election, the Australian
Electoral Commission (AEC) was required to recount the Western
Australian (WA) ballots after a close result. During the recount,
approximately 1370 ballots were found to be missing. It is unclear
whether these ballots were present in the first count and then
mislaid, or whether the original tallies were wrong. The error had the
capacity to influence the outcome of the election, so the AEC was
forced to re-run the election for the WA seats in its entirety at a
cost of approximately AUD 20 million~\cite{sbs2014}. The electoral
commissioner of the AEC itself subsequently resigned.
Paper ballots and manual counting methods in modern elections are
therefore increasingly seen as archaic, especially as
cash-strapped electoral bodies seek cheaper alternatives. Indeed,
numerous electoral bodies are ploughing ahead with electronic
vote-casting and vote-counting of preferential votes using computers
and the most recent state election in New South Wales in Australia
even used an internet voting system which was shown to be vulnerable
to vote-tampering~\cite{teague-halderman-conversation}. Alarmingly,
many of these software systems are not open to scrutiny and some are
even officially deemed to be ``commercial in confidence'' and are
deliberately kept from researchers like us who wish to scrutinise the
code for correctness. Given the importance of the task of electing a
government, this state of affairs is totally unacceptable.
The ideal of course is to use some form of end-to-end verifiable
system which provides strong
evidence that electronic ballots are cast-as-intended,
transported-without-tampering and that all electronic ballots are
included in the final tally \emph{without having to blindly trust the
underlying computer code.}
Unfortunately, such systems do not guarantee that the electronic ballots
are counted correctly according to complex vote-counting schemes such
as single-transferable voting (STV) and
%proposals for extending counting
methods for extending them to STV are in
their infancy~\cite{teague2009}.
% In previous work [deliberately hidden], we showed that
% %~\cite{gore-meumann-evote14}, we showed that
% ``heavy-weight'' formal methods based upon higher-order logic are
% feasible for formally verifying the correctness of a simple
% first-past-the-post (FPTP) vote-counting algorithm. We also showed how our
% methodology allows us to prove desirable properties of FPTP such as
% the monotonicity criterion: if the ballots are changed so that the
% winning candidate is given more votes than previously then the same
% candidate wins again.
We describe a methodology for formally reasoning about complex
vote-counting schemes.
%such as STV scheme used for the election
%of multiple candidates in the Australian provinces of Tasmania and the
%Australian Capital Territory.
Specifically, we describe how we first formally encoded the
English-language Parliamentary Act for the Hare-Clark STV
vote-counting scheme used in the Australian state of Tasmania into
higher-order logic, giving a formula called \spechol. We then created
a more algorithmic version using the syntax of the
functional programming language Standard ML (SML) to give a formula
called \imphol. We manually transliterated this formula into an actual
SML program \impsml{} to count ballots. We are currently verifying
that the formalisation of the implementation logically implies the
formalisation of the specification: that is, we are using the HOL4
interactive theorem prover to machine-check the implication
\imphol~$\to$ \spechol.
%Here, we outline our current progress.
% In Section~\ref{sec:stv}, we describe the version of STV used in Tasmania
% and outline aspects which make hand-counting difficult and
% error-prone. In Section~\ref{sec:hare-clark-legislation}, we describe
% the English-language Hare-Clark Act of Parliament which defines the legislation
% which must be adhered to in counting votes in Tasmanian elections.
% In Section~\ref{sec:existing}, we describe existing electronic vote-counting
% software that is currently in use in Australia. In
% Section~\ref{sec:method}, we describe our methodology and explain why it
% is a highly trusted form of verification. In Section~\ref{sec:leginlog},
% we describe how we encoded the Tasmanian Hare-Clark Act into
% higher-order logic. In Section~\ref{sec:hol-reasoning}, we describe
% how we can formally prove algorithmic properties of this Act. In
% Section~\ref{sec:further}, we describe further work and conclude.
% Background and Need
%\input background
A note on nomenclature. We use the term ``voting scheme'' to mean a
traditional method that spells out how to cast a vote and how to count
such votes: for example single transferable voting scheme and first
past the post voting scheme. We use the term ``e-voting system'' to
mean an existing method for casting votes electronically: for example
\pavoter. We use the term ``e-voting software'' to mean a computer
program that allows voters to cast votes electronically: for example
eVACS. We use the term ``e-counting'' to mean the counting of ballots
by electronic means: for example the counting module inside eVACS or
homomorphic tallying. We use the term ``formal verification'' to mean
the process of guaranteeing that a ... We use the term
``machine-checked'' to mean ... We use the term ``light-weight
verification'' to mean the use of (usually automatic) computer tools
which are not guaranteed to be sound or complete: for example the JML
tool. We use the term ``heavy-weight'' verification to mean the use of
(usually interactive) computer tools which are trusted to be sound
(usually by having a small code base which has been heavily
scrutinised by many experts).
\paragraph{Acknowledgements:} We are extremely grateful to the
many suggestions for improvement from the reviewers of VoteID 2015. We
have tried to take every comment into account, and have even used some
of the suggested prose verbatim.
\section{Hare-Clark Single Transferable Voting}\label{sec:stv}
% We give a brief overview of proportional representation single
% transferable voting (PRSTV) to highlight the complexity of counting
% votes using such preferential schemes, particularly for electing
% multiple candidates.
Farrell and McAllister~\cite{farrel-mcallister-2006} provide a
definitive study of preferential electoral systems in
Australia. Wen~\cite{wen-phd} provides an engineering perspective of
preferential systems, legislation and verifiable cryptographic schemes
for preferential voting and counting. Here, we briefly describe STV
and Hare-Clark STV.
\paragraph{STV for Electing Multiple Candidates.} We assume that there
are more candidates than seats, as otherwise, there is no need for an
election. Voters order the candidates on the ballot paper in order of
preference, usually by placing a number next to each candidate's name.
To become elected, a candidate must reach a quota of votes, as opposed
to an absolute majority. This quota is set according to the number
of seats available. There are several ways of calculating a quota.
The votes are all initially allocated according to their first
preference. A candidate who reaches the quota is elected, or else, if
no candidate reaches the quota, then one ``weakest'' candidate is
eliminated. There are several ways to choose the ``weakest''
candidate.
% who are all equally weaker than the rest.
%
If a candidate is elected by reaching the quota, each surplus ballot
for that candidate is transferred to the next continuing (un-elected
and un-eliminated) candidate on that ballot. There are many different
ways to choose a surplus ballot, and many ways to choose its new,
possibly fractional, value.
%
If a candidate is eliminated, all of the ballots currently counted as
being for that candidate are transferred according to their next
(continuing) preference, again possibly with a fractional transfer
value.
%
The election is complete either when all seats are filled, or the
number of vacant seats equals the number of continuing candidates, in
which case all these candidates are elected.
The transfer of votes is key to ensuring that candidates with
particular political views are elected in proportion to their support
within the community, so the complexity resulting from surplus
calculations and transfers cannot be removed without seriously crippling
the system. As we shall see, there are many subtleties in the naive
description above.
\paragraph{The Hare-Clark Scheme.}\label{sec:hct}
Hare-Clark is an instance of the proportional representation scheme that
uses single transferable vote as described above and has been used to
elect members of Tasmania's House of Assembly since
1907~\cite{terry-newman-hare-clarke-guide,scott-bennett-hare-clarke-critical}.
A slightly different version has also been used to elect members of
the Legislative Assembly in the Australian Capital Territory (ACT)
since 1995~\cite{hare-clarke-guide-ecact}. Hand-counting according to
Hare-Clark is notoriously difficult and error-prone with some ballots
examined in excess of 50 times before a result is declared. Thus a
formally verified program for either version is likely to have
practical benefits almost immediately.
%
% Elections under this system in Tasmania typically take 2--4 weeks to
% count. Tasmania's population (300,000) is a relatively small political
% jurisdiction. The labour and time overhead involved in counting a
% Hare-Clark election is understandably prohibitive in some larger
% jurisdictions outside Tasmania, preventing it from becoming widely
% adopted. Often some ballots must be examined in excess of 50 times
% when ascertaining the result of a Hare-Clark election.
%
We already have a formal specification of Hare-Clark
ACT~\cite{abate-evacs-analysis}, so we decided to concentrate on
Hare-Clark Tasmania as this will allow us to compare and contrast the
properties of these two variants of Hare-Clark.
% \paragraph{Preferential Schemes Electing Multiple Candidates.}
% A variant of the scheme described above allows for the election of
% multiple candidates in each electorate according to the proportion of
% the votes that they get.
% As above, the ballots are transferred between the candidates at each
% stage of the count according to the voters' marked preferences.
% Candidates are eliminated in rounds, as in the
% preferential system described above, until a candidate reaches the
% quota and becomes elected. If the candidate's votes exceed the quota
% when this happens, then the surplus votes are transferred to the
% remaining candidates. Generally, if the total number of candidates
% remaining equals the number of remaining seats at any stage of a
% count, the remaining candidates are simply declared elected.
% The actual counting process is naturally more stringent and rigorous
% than this, but this analogy indicates the general principle. Some
% candidate may receive too many votes, and so the surplus votes could
% be considered ``wasted'' were they not to be transferred to the next
% most desirable candidate.
% There is usually a
% trade-off between efficiency and accuracy when calculating which votes
% should be transferred to whom. The process of calculating and
% transferring a surplus is usually the primary source of complexity in
% PR systems.
%
% \subsubsection{Quotas.}\label{sec:quotas}
% This section discusses two quotas used in PR systems: the Hare quota
% and the Droop quota. Other quotas do exist and are used in some
% jurisdictions, but space precludes us from including them all. They
% are typically smaller than the quotas explored below, and may in some
% cases elect more candidates than there are seats available.
% \paragraph{Hare Quota.}
% Early PR systems used the quota proposed by Thomas Hare~\cite{hare1857,comgenelect1909}, now
% known as the Hare quota. The Hare quota is calculated simply as the total
% number of votes divided by the total number of available seats:
% \[
% \frac{\text{votes}}{\text{seats}}
% \]
% This is a fairly na\"ive quota, and can be demonstrated so with a very
% simple example. Consider a situation in which there is only one seat
% available. Then the quota will be calculated as 100\% of the votes.
% Clearly a candidate should not need 100\% of the vote to be elected,
% but rather only more than 50\%.
% \paragraph{Droop Quota.}
% The Droop quota is much more commonly used, and is calculated as the number
% of valid votes divided by one more than the number of seats, rounded up to the
% nearest integer~\cite{comgenelect1909}:
% \[
% \left\lceil \frac{\text{votes}}{\text{seats} + 1} \right\rceil
% \]
% This quota represents the minimum number of votes possible whilst ensuring that
% it is impossible to elect more candidates than the number of seats available.
% Interestingly, candidates are guaranteed to be
% elected once they reach the Droop quota, even when using a larger quota such
% as the Hare quota.
% \subsubsection{Transfer Methods}\label{sec:transfermethods}
% What is the best way to select and/or
% transfer surplus votes from candidates that have already reached the quota? The
% options usually represent a compromise between efficiency and accuracy.
% \paragraph{Random Sampling.}
% The original system proposed by Hare provided for the random selection
% of surplus ballots from the pool of ballots allocated to a candidate.
% The nondeterministic nature of this decision is the main issue with
% this method. In some cases, it may influence the outcome of the
% election, and there can be obvious difficulties faced when attempting
% to confirm the results with a recount. As pointed out
% in~\cite{comgenelect1909}, this system is also unexpectedly
% labour-intensive to implement. Achieving a fair shuffling of physical
% ballot papers is impractical, especially when large numbers of ballot
% papers are involved. This is based on the observation that ballots
% with similar preferences tend to occur in groups during the count. In
% a computerised system, this would be less of an issue (but brings its
% own issues in terms of generating true random selections).
% \paragraph{Standard Gregory Fractional Transfer.}
% The Gregory fractional transfer method is an alternative transfer method
% aimed at removing the nondterminism of random sampling~\cite{comgenelect1909}.
% Instead of selecting ballots at random, all
% of the ballots in the transfer leading to the surplus must be re-examined, and
% then transferred at a fractional value. That is, transferred as fractional
% votes. This transfer value is calculated as the surplus
% divided by the number of ballots in the last transfer:
% \[
% \frac{\text{surplus}}{\text{size of original transfer}}
% \]
% This method removes the element of nondeterminism inherent in random sampling,
% thereby making the result reproducible. It is not clear, however, that a
% re-examination of the last transfer alone is representative enough. Certainly,
% the most recent transfer may produce a redistribution vastly different to the
% collective preferences of all of the votes attributed to the successful
% candidate. Farrell and McAlister~\cite{farrell2003} note that ``there is
% good reason to believe'' this issue
% influenced the outcome of the double dissolution election in 1974, in which
% Labor candidate Malcolm Colston narrowly missed out on achieving the final
% Queensland seat in the Senate. He may not have done so had the first-preference
% ballots of Neville Bonner (a successful Liberal candidate) been included in the
% transfer calculation.
% \paragraph{Inclusive Gregory Fractional Transfer.}
% The inclusive Gregory method is so named because it includes the entirety of
% the successful candidate's ballot pool in the re-examination and calculation of
% the transfer. This transfer method is more labour-intensive than the
% standard Gregory method, but can produce a more accurate representation of the
% voters' preferences.
% There actually exist two versions of the inclusive Gregory
% method: unweighted and weighted. The unweighted version does not take into
% account the existing fractional values of votes in the successful candidate's
% ballot pool when calculating the new transfer values for the subsequent transfer.
% In other words, when calculating the surplus from successful candidate $s$ to
% transfer to continuing candidates, votes obtained by candidate $s$ at low fractional
% values (say $\frac{1}{4}$ of the full value) will be treated when calculating
% the new transfer value as being full votes. The weighted system eliminates this
% issue by incorporating the existing value of a vote in the calculation of the
% new transfer value. The caveat is that it is more complex and thus more
% difficult to deal with reliably.
% In either case, using an inclusive Gregory transfer method means every single
% ballot which has been assigned to a candidate must be re-examined. This has
% real consequences in terms of the time it takes to ascertain the result of an
% election as well as the labour cost associated with the process. The weighted
% version also represents an increase in complexity.
% \subsection{Complexity is Necessary}
% It should be clear from the explanation above that PR systems are by far the
% most complex systems explored here. PR systems are also by far the fairest
% of the systems shown here.
% FPTP systems are simple but unfair whilst the much more representative PR systems
% exhibit a large step up in terms of complexity over both FPTP and preferential
% systems. Even within the spectrum of PR, systems can be separated in terms of
% fairness and complexity. Those that are fairer (using the weighted Gregory
% fractional transfer for instance) are more complex to count than less fair
% systems (such as those using random sampling).
% Complexity is necessary in electoral systems.
\section{Related Work}
Various authors have attempted to apply formal methods to algorithms
for STV counting, starting from early work using only ``pen and
paper'' proofs, and ending with more recent work using
``light-weight'' computer-based tools. We present them in order of the
amount of machine-checking that is involved in each. As far as we
know, the only other work on using ``heavy-weight'' verification is
our own previous work on reasoning about
the first-past-the-post voting scheme~\cite{DBLP:conf/ev/GoreM14}.
Hill {\it et al}~\cite{HillWichmannWoodall87} give a pen and paper
proof of various properties of an algorithm to count votes using the
Meek's method. It's correctness relies totally on these
pen and paper proofs, which presumably were checked by the
referees.
Poppleton~\cite{Poppleton97} takes a step towards machine-checked
proofs by writing a specification for STV vote-counting using the
logic-based specification language Z, but does machine-check an
implementation using tools based on Z~\cite{ztools}.
Kiniry {\it et al}~\cite{cochran-kiniry-tally-systems} formalised the
STV scheme used for proportional representation elections in Ireland
using the Alloy tool. They automatically generated test cases that
covered every possible scenario using breadth-first search. Finally,
they tested an implementation of the Irish vote-counting scheme, which
had been developed using light-weight formal methods, and found two
errors. They conclude that
{
\em
``this level of coverage (100\% statement and condition
coverage) does not prove that the system is error-free. \dots But
what it does do is (a) provide strong evidence, especially when
combined with a rigorous development method and formal verification,
that the system is correct, and (b) raise the state-of-the-art for
election tally system testing
enormously''
}~\cite{cochran-kiniry-tally-systems}.
Cochran conducted a comprehensive study of verifying STV counting
using light-weight (automatic) methods~\cite{KiniryMCOH06,cochran-phd}
by attempting to formally verify a Java program for the Irish
proportional representation single-transferable voting scheme against
its English natural language description
% . They manually translated this description
% into
% EBON~\cite{bon-modelling-language}, a formal English-like notation for
% specifying business rules and manually translated the EBON
% specification into the Java Modelling Language
% (JML)~\cite{leavens-baker-ruby-jml}. They manually annotated the JML
% specification
% code with pre- and post-conditions and invariants and
% tried to
% prove
% formally
% that it met them
using the ESC/Java tool. Most proofs were
completed automatically, but in some, ``\textit{ESC/Java2 could
neither verify the loop invariants nor the
post-condition}''~\cite[p~46]{cochran-phd}.
Moreover, lightweight formal methods, such as
ESC/Java, are not guaranteed to be sound or complete since their code
base is huge. Cochran concludes
with ``\textit{Despite the use of a verification-centric process, and
100\% statement coverage of the code, the following issues are
outstanding, representing a potential inconsistency in the JML
specifications.}''~\cite[page~63]{cochran-phd}.
Recent attempts by Beckert et al~\cite{verify14} show that even
state-of-the-art light-weight verification techniques such as bounded
model-checking do not scale to realistic elections for even simple
voting schemes such as first-past-the-post.
The move to using interactive theorem proving technology based upon
(higher-order) logic is apparent in the work of DeYoung and
Schurmann~\cite{DeYoungSchurmann12}. Rather than translating English
prose into higher-order logic, they express the vote-counting scheme
itself as a linear logic program. Read in a purely declarative manner,
this logic program specifies what the algorithm should do. It can also
be executed to count actual ballots, although tests showed that it did
not scale to real-world elections. The logical
framework they utilise is not able to capture formal reasoning about
the logic program itself: thus there is no correctness proof.
% That is, there is no explicit proof that the
% logic program meets its English-language specification.
The related work described above is mostly about the verification of
algorithms against specifications. Thus there is no ability to
formally compare and contrast two variants of the same voting scheme.
Light-weight methods allow us to specify two variants of an STV voting
scheme (say) and compare them by specifying different
post-conditions. But recall that such tools are not guaranteed to be
sound or complete. Recent work of Beckert {\it et
al}~\cite{DBLP:journals/istr/BeckertGSBW14} shows other
pen-and-paper methods for reasoning about voting schemes using
first-order and linear logic.
Our methodology goes one step beyond all of these efforts in the
following senses:
\begin{description}
\item[Formal specifications:] the specification is encoded as a
formula of higher-order logic inside the HOL4 theorem prover. Thus
it is type-checked and we can be sure that it actually is a
well-formed formula of higher-order logic;
\item[Formal termination:] the SML program is encoded into HOL4 as
$\imphol$ and HOL4 will only accept the program if we can create a
proof inside HOL4 that the program will terminate for all inputs;
\item[Proof Objects:] both the implementation and the specification
are encoded as formulae of higher-order logic inside the theorem
prover HOL4. Thus we can construct a proof that $\imphol \rightarrow
\spechol$ which can be exported and checked by others using their
own favourite theorem prover.
\item[Correctness:] the HOL4 theorem prover checks that all steps in
this proof are correct. That is, unlike all earlier work, we can be
certain that the proof is mathematically correct;
\end{description}
Our methodology has three inherent weaknesses. As with all formal
methods, there is no guarantee that $\spechol$ correctly captures the
English prose that makes up the Hare-Clark method of STV counting
since it is merely one person's interpretation of the English-language
prose of the relevant Parliamentary Act. We mitigated the risks of
errors in interpretation by using two people to complete the
formalisation: Meumann wrote the initial $\spechol$ and $\imphol$ but
Dawson carried out all the proofs. Thus, Dawson first had to check
whether both specifications accurately captured the Hare-Clark act and
Meumann's implementation. In so doing, Dawson found some errors, as
discussed in Section~\ref{sec:errors-in-spec}. Second, we have no
formal model of the programming language SML, so we cannot prove that
the final SML code meets its formal programming language semantics. As
we point out previously~\cite{DBLP:conf/ev/GoreM14}, the
CakeML~\cite{DBLP:conf/popl/KumarMNO14} project will allows us to
provide such proofs in the future. Finally, our approach is very
labour-intensive: it took Dawson at least six months of full-time work
to complete these proofs and he has over 20 years of experience in
using higher-order logic theorem provers!
\section{Existing e-Voting and e-Counting Systems}%
\label{sec:existing}
Many e-voting systems provide trustworthiness whilst maintaining
ballot anonymity using cryptographic zero-knowledge proofs:
Scantegrity, PunchScan and Pr\^et \`a Voter to name three. These
systems encrypt each voter's ballot before sending it electronically
to a central server to ensure that votes are received
tamper-free. Once received, there are two main methods for tallying
these encrypted votes: homomorphic tallying and mixnet tallying.
Homomorphic tallying does not require the votes to be decrypted since
it uses cryptographic methods to compute a simple sum over all the
encrypted ballots. They tend to be badly suited to preferential
systems (for both voting and counting) since they are primarily
designed to compute a simple (homomorphic) sum, rather than a complex
count in rounds as required by STV.
Mix-net methods require ballots to be decrypted and separated from the
voter's identity to maintain anonymity. The decrypted ballots can then
be counted either by hand or by using e-counting software (a computer
implementation of the relevant counting method). e-voting systems that
use mix-nets are usually better for preferential voting and counting
because their flexible ballot structure can handle complex ballot
structures such as those required by STV.
Note that neither homomorphic tallying nor mix-net-based tallying
alone can guarantee that STV votes are counted correctly because
homomorphic methods cannot handle STV ballots, and mix-net methods
usually rely on an unverified e-counting program or hand-counting to
count the ballots (in STV elections). Shufflesum~\cite{teague2009}
extends homomorphic tallying to simple STV ballots, but it has not
been implemented or used in any real elections.
The Australian state of Victoria recently allowed visually impaired
voters to cast an electronic vote using e-voting software based on
Pr\^et \`a Voter caled vVote~\cite{DBLP:journals/corr/CulnaneRST14}.
Voters could visually verify that their electronic ballot was
cast-as-intended but these electronic ballots were then printed and
inserted into the set of all paper ballots, which were counted
electronically using an in-house piece of software available for
scrutiny from the Victorian Electoral Commission web site.
% vVote produces zero-knowledge proofs to ensure that the electronic ballot is
% cast-as-intended.
The vote-counting software has not been verified in
any formal sense.
The Australian Electoral Commission (AEC) counts ballots using a form
of STV for federal Senate elections using in-house software called
EasyCount. It is also used by the AEC to provide ``for profit''
election services: for example, to count votes for the directorship of
a company. EasyCount is closed-source and Freedom of
Information (FoI) requests seeking access to EasyCount's source code
and documentation have been denied~\cite{foiref1}.
%citing that the source code and all documentation are
%``trade secrets''~\cite{foiref1}.
% Interestingly, the AEC contends
% that the algorithm as expressed in the code is a ``trade secret'' and
% that releasing the documentation to the public ``would allow the
% algorithm to be deduced''~\cite{foiref2}. In the case of the Senate
% elections, the algorithm should theoretically be that specified by the
% legislation pertaining to Senate counts, which is entirely public. It
% is worrying that the counting program uses an algorithm distinct from
% that specified in the legislation.
In Germany~\cite{dw2009}, legal
challenges against such ``black-box'' e-voting software have resulted
in their being outlawed. Clearly, it would be preferable to avoid that
situation in Australia.
The e-voting software eVACS, trademarked by Software Improvements Ltd,
is used by the Australian Capital Territory Electoral Commission
(ACTEC) to e-cast some of the votes and to e-count all of the votes in
Legislative Assembly elections. The software is written in unverified
C and some of the source code is freely available from the ACTEC
website. By analysing this code, Das {\it et al} found ``{\it no hot
exploits}'' but found ``{\it some vulnerabilities and bad software
engineering practices}'' and concluded that it was a ``{\em fragile system
with a large trusted computing base}''~\cite{das-niu-stegers-evacs}.
Three bugs have been found in this software by members of the Logic
and Computation Group at the Australian National
University~\cite{abate-evacs-analysis}. For each bug, it was possible
to design an example election whose outcome would have been incorrect.
These bugs were found precisely because the source code was available,
but other bugs could still be present. Using the raw ballots provided
by ACTEC, we have checked that these bugs did not affect the results
of the previous four elections for which eVACS was used.
EasyCount and eVACS both remove the human-error component in
complicated counting processes, but both of them have the potential to
introduce systemic counting errors.
% %
% One way of confirming the results of an election is to release the raw
% ballots to the public, allowing citizens to perform their own count.
%
% Unfortunately, releasing the actual ballots leaves open the potential
% for voter coercion and/or bribery~\cite{italian-attack,teague2009}.
% A coercer may
% attempt to coerce a particular vote from of an individual or group and
% is then able to check the released ballot list for the required
% occurence(s)\cite{italian-attack}.
% This issue is particularly evident in preferential and
% PR systems because the number of possible ballot permutations is
% enormous: generally much larger than the number of voters. As such,
% it is important that electronic systems be adequately trustworthy
% without having to provide access to the raw ballot data.
%
The approach discussed next is aimed at producing fully formally
verified vote-counting programs that can handle the complexity of PR
voting systems.
%Thus there will be no need for ballots to be released.
% Methodology
\section{Higher-order Logic and the HOL4 Theorem Prover}\label{sec:method}
The rigorousness of our approach stems from the use of HOL4 to
construct the proofs. HOL4 is an interactive theorem proving
assistant based upon Dana Scott's ``Logic for Computable Functions''
(LCF), a mathematically rigorous logic engine consisting of 8
primitive inference rules which have been proven to be mathematically
correct~\cite{gordon-melham-intro}. HOL4 implements this logic engine
using approximately 3000 lines of ML code and this code has been
scrutinised by experts in LCF to ensure that it correctly implements
the 8 inference rules. Any complex inference rules must be
constructed as a programmatic combination of the core primitive rules
only. Thus its code base is small and trusted.
%Thus the proofs produced in HOL4 are highly rigorous.
Our verification process falls under the rubric of ``heavy-weight
verification'' since it requires a person to direct the process in an
interactive fashion. As such, it is very labour intensive. It involves
producing a logical formalisation of both the program's requirements
and the program itself in the HOL4 theorem proving
assistant ({\url{http://hol.sourceforge.net/}}), then
constructing a formal proof showing that the program matches the
requirements. Producing the program using a strictly functional
programming style ensures the program can be readily represented in
higher order logic with minimal alterations. We
used Standard ML (SML), the same language in which HOL4 is
itself implemented.
When applied to electoral systems, the requirements are usually
informed by the relevant legislation. As we shall show,
translating complex legislation into rigorous
formal logic can be a non-trivial task.
Our methodology involves producing the following:
\begin{description}
\item[\rm\spechol{}:]\label{item:spec} a hand-encoding of the
English-language description of the vote-counting process into
higher-order logic;
\item[\rm\impsml{}:] an implementation in SML of a vote-counting
program based upon \spechol;
\item[\rm\imphol{}:]\label{item:trans} a hand-translation of \impsml{} into
higher-order logic;
\item[\rm Formal Proof:] A proof acceptable to the HOL4 theorem prover
that \imphol{} logically implies \spechol{}, which guarantees that
the \underline{translation} of the implementation meets the
\underline{translation} of the Parliamentary Act.
%(\ref{item:spec}) holds of the translation (\ref{item:trans}).
\end{description}
% Figure \ref{fig:initproc} gives a diagrammatical representation of these elements
% and how they relate to each other. From this point forth, the implementations
% in HOL4 and SML (\imphol and IMP respectively) will simply be referred to as
% the ``implementation,'' referring to the singular algorithm involved.
% \begin{figure}
% \begin{center}
% \begin{tikzpicture}[node distance = 10em, auto]
% % Components
% \node [component] (imp) {IMP};
% \node [component, anchor=west, shift={(3,0)}] (leg) at (imp.east) {Legislation};
% \node [component, anchor=south, shift={(0,3)}] (imphol) at (imp.north) {\imphol};
% \node [component, anchor=west, shift={(3,0)}] (spec) at (imphol.east) {SPEC};
% \path [draw] (imp) edge [<->,dotted] (leg);
% \path [draw] (imp) edge [-latex] (imphol);
% \path [draw] (imphol) edge [latex-latex] (spec);
% \path [draw] (leg) edge [-latex] (spec);
% % HOL4 box
% \node [shift={(-1,-1)}] (botleft) at (imphol.south west) {};
% \node [shift={(1,-1)}] (botright) at (spec.south east) {};
% \node [shift={(-1,1)}] (topleft) at (imphol.north west) {};
% \node [anchor=north east,shift={(1,1)}] (topright) at (spec.north east) {HOL4};
% \path [draw] (topright.north east) edge [dashed] (topleft.center) edge [dashed] (botright.center);
% \path [draw] (botleft.center) edge [dashed] (topleft.center) edge [dashed] (botright.center);
% \end{tikzpicture}
% \end{center}
% \normalsize
% \caption{Illustration of the components of the verification process.}
% \label{fig:initproc}
% \end{figure}
When applying this methodology to vote counting systems, the counting
program is represented in higher-order logic (as \imphol). It thus
becomes possible to prove various results about the program. We can
also verify the voting scheme itself (\spechol) with respect to various
desiderata. Our methodology is particularly suited to the
verification of new voting schemes against the presence of desired
properties or the avoidance of objectionable ones. For example it
would be possible to prove that the voting scheme in question adheres
to the independence of irrelevant alternatives (see~\cite{arrow1950}).
It is also possible to prove comparative results between different
voting schemes: for instance that voting scheme $A$ differs from
voting scheme $B$ in only $x$ specific situations.
% Large-Scale Case Study
%\section{The Hare-Clark STV Voting System}\label{sec:large}
% The Hare-Clark system is one of the most complex electoral systems in
% active use, and is therefore one of the most difficult electoral
% systems to verify. If the Hare-Clark verification can be shown to be
% feasible, then our methodology should be feasible for other simpler
% electoral systems.
The specification (in this case the translation of the legislation into
HOL4's logic) is performed \emph{prior} to the implementation of a counting
program. This is intended to ensure the specification remains as
independent of the implementation as possible. Thus ensuring any shortcuts
or misconceptions adopted during the implementation process are not carried through
to the specification.
%The updated ordering is shown in Figure \ref{fig:postsmallproc}.
Rather than producing an SML program and translating that to HOL4, the
program is produced first in HOL4's formal logic, then translated to
SML.
% This is intended to mirror the direction in which the CakeML translation
% would proceed if CakeML were to be used (CakeML is discussed in section
% \ref{sec:smalldiscussion}).
Programming directly in HOL4's formal logic
also helps to ensure that the non-functional features of SML are avoided.
% \begin{figure}
% \begin{center}
% \begin{tikzpicture}[node distance = 10em, auto]
% % Components
% \node [component] (imp) {IMP};
% \node [component, anchor=west, shift={(3,0)}] (leg) at (imp.east) {Legislation};
% \node [component, anchor=south, shift={(0,3)}] (imphol) at (imp.north) {\imphol};
% \node [component, anchor=west, shift={(3,0)}] (spec) at (imphol.east) {\spechol};
% \path [draw] (imp) edge [<->,dotted] (leg);
% \path [draw] (imphol) edge [-latex] (imp);
% \path [draw] (imphol) edge [latex-latex] (spec);
% \path [draw] (leg) edge [-latex] (spec);
% % HOL4 box
% \node [shift={(-1,-1)}] (botleft) at (imphol.south west) {};
% \node [shift={(1,-1)}] (botright) at (spec.south east) {};
% \node [shift={(-1,1)}] (topleft) at (imphol.north west) {};
% \node [anchor=north east,shift={(1,1)}] (topright) at (spec.north east) {HOL4};
% \path [draw] (topright.north east) edge [dashed] (topleft.center) edge [dashed] (botright.center);
% \path [draw] (botleft.center) edge [dashed] (topleft.center) edge [dashed] (botright.center);
% \end{tikzpicture}
% \end{center}
% \normalsize
% \caption{Updated verification procedure for the Hare-Clark case study.}
% \label{fig:postsmallproc}
% \end{figure}
The astute reader may notice there are certain gaps in this
methodology that cannot be filled: there is no \emph{proof} that the SML
program (\impsml) is the same as the HOL4 translation (\imphol), and there
is no \emph{proof} that the HOL4 encoding of the legislation (\spechol) is
logically the same as the legislation itself.
% These two issues are
% covered in Section~\ref{sec:small} and~\ref{sec:large} respectively.
\section{Translating Legislation into Higher-order Logic}\label{sec:leginlog}
The following list of HOL4 syntax may be helpful.
% \begin{center}
% \begin{tabular}{|c|c|}
% \hline
% HOL4 Syntax & Logic Syntax \\
% \hline & \\[-1.2em]\hline
% \texttt{T} & verum \\
% \hline
% \texttt{F} & falsum \\
% \hline
% \texttt{\~{}}$ t$ & $\lnot t$ \\
% \hline
% $t_1$ \texttt{\textbackslash/} $t_2$ & $t_1 \lor t_2$ \\
% \hline
% $t_1$ \texttt{/\textbackslash}$ t_2$ & $t_1 \land t_2$ \\
% \hline
% $t_1$ \texttt{==>} $t_2$ & $t_1 \Rightarrow t_2$ \\
% \hline
% $t_1$ \texttt{=} $t_2$ & $t_1 = t_2$ \\
% \hline
% $\mathtt{!} x \mathtt{.} t$ & $\forall x. t$ \\
% \hline
% $\mathtt{?} x \mathtt{.} t$ & $\exists x. t$ \\
% \hline
% \end{tabular}
% \end{center}
%
\begin{center}
\begin{tabular}{|c|@{\extracolsep{0.1em}}c|c|c|c|c|c|c|c|c|c|}
\hline
HOL4
& \texttt{\ x y. A}
& \texttt{T}
& \texttt{F}
& \texttt{\~{}}$ t$
& $t_1$ \verb!\/! $t_2$
& $t_1$ \verb!/\! $ t_2$
& $t_1$ \texttt{==>} $t_2$
& $t_1$ \texttt{=} $t_2$
& $\mathtt{!} x \mathtt{.} t$
& $\mathtt{?} x \mathtt{.} t$
\\ \hline
Logic
& $\lambda x y.\ A$
& verum
& falsum
& $\lnot t$
& $t_1 \lor t_2$
& $t_1 \land t_2$
& $t_1 \rightarrow t_2$
& $t_1 = t_2$
& $\forall x. t$
& $\exists x. t$
\\ \hline
\end{tabular}
\end{center}
% \section{The Hare-Clark System}\label{sec:hct}
% Widely viewed as one of the fairest electoral systems in use around the world,
% Hare-Clark is a proportional representation system that has been used to elect members of
% Tasmania's House of Assembly since
% 1907. It has also been used to elect members of the
% Legislative Assembly in the Australian Capital Territory (ACT) since 1995.
% The system uses the Droop quota and the standard Gregory fractional
% transfer method. Elections under this system in Tasmania typically take 2--4
% weeks to count. In terms of population, Tasmania is a relatively small
% political jurisdiction. The labour and time overhead involved in counting a
% Hare-Clark election is understandably prohibitive in some larger jurisdictions
% outside Tasmania,
% preventing it from becoming widely adopted. Often
% some ballots must be examined in excess of 50 times when ascertaining the result of
% a Hare-Clark election.
The translation of the Tasmanian House of Assembly vote counting legislation
is a non-trivial task. Theoretically, if there is only one way to
interpret the legislation logically, then higher-order logic is
expressive enough to capture the legislation's meaning.
When examined closely, however, the legislation contains various ambiguities and
contradictions that prevent a direct ``translation''. In many cases the
intended \emph{meaning} of the legislation must be encoded in HOL4 rather than a
direct logical translation of each predication.
For example, clause 12
deals with the case in which there is a tie amongst the weakest
candidates and one of them must be eliminated. The legislation
specifies that the tie is to be broken by deferring to \emph{``the last
count or transfer at which [the candidates involved in the tie] had an
unequal number of votes''}. When more than two candidates are
concerned,
%there is ambiguity surrounding which count should be
%deferred to.
there are three different ways of interpreting which
candidate should be excluded:
\begin{enumerate}[(a)]
\item\label{itm:pairwise} the candidate who has the lowest count at
the last count or transfer at which all of the candidates concerned
had pairwise unequal counts;
\item\label{itm:lowest} the candidate who has the lowest count at the
last count or transfer at which one candidate had a count less than
all of the other candidates concerned;
\item\label{itm:lex} the candidate who has the lowest count in a
lexicographical ordering of all of the previous counts for the
candidates concerned (with the most recent count being the first
element of the lexicographical combination and the next-most recent
count being the next element of the lexicographical combination etc.).
\end{enumerate}
Option (\ref{itm:pairwise}) appears to most closely mirror the wording of the legislation,
but causes deferral to counts older than the other two options. This one is the most
likely to defer all the way back to the initial count and result in a lot-based
elimination. Option (\ref{itm:lowest}) causes deferral to counts more recent than
option (\ref{itm:pairwise}), but may result in the exclusion of a candidate who
had a higher count than some or all of the other candidates concerned at a more
recent count. Option (\ref{itm:lex}) is the intuitively fairest option, but appears to
reflect the legislation least. The ACT has a similar issue with their
Hare-Clark legislation, in which the clauses regarding tie breaking are similarly
worded. The ACTEC interprets their legislation according to option (\ref{itm:lex}).
Ambiguities such as this increase the difficulty of the formalisation process.
Nevertheless, it is a testament to the rigorousness of our approach that it
results in ambiguities such as this being discovered and properly
questioned. This is a positive outcome if it results in a
tightening of the legislation.
Another issue encountered whilst formalising the legislation is that
the legislation is written in a procedural manner. In particular, the
legislation makes regular reference to various ``stages'' of the
count, and what should happen if certain conditions are met at various
stages. This implies a mutable representation of the count, where the
state changes over time (at each stage of the count) and is a
side-effect of the legislation specifying \emph{how} the votes should
be counted, not what the result of the count should be. This is in
direct contradiction with the ideal of functional programming, which
is to have a declarative representation of computation (effectively
stateless).
The procedural nature of the legislation forces the \spechol{} to make
statements about \imphol's ``state''. In lieu of an existing \imphol,
the \spechol{} must be built based on assumptions about \imphol's
structure. This results in a certain level of coupling between
\spechol{} and \imphol, but cannot be avoided when the legislation is
written in a procedural manner.
\subsection{Assumptions About the
Implementation}\label{sec:assumptions}
To have a concrete conceptualisation about which to build the logical
statements of the \spechol, some assumptions must be made about the
form of \imphol. The initial assumptions are explained below. Note
that some of the assumptions now need revision due to unforeseen
technical restrictions on \imphol. The revision process is yet to be
undertaken, but the intention is to combine it with a general review
of the \spechol{} to iron out any inconsistencies.
\subsubsection{Inputs and Outputs.}
The inputs and outputs of the counting procedure must be defined. This is
fairly straightforward. At a minimum, the procedure must take the set of
ballots and the set of running candidates as input. These are assumed to be provided
using lists: a mainstay of functional programming. The procedure is assumed to
take as input a list of candidates and a list of
ballots. Each ballot itself is assumed to be a list of candidates in order of
preference (the head of the list being the first preference). It is also
assumed the function takes as input the number of candidates to be elected since
the number of seats per electorate has changed multiple times in Tasmania.
The output of the function is assumed to be
a list of elected candidates. Let us call the function
\verb|COUNT_HCT|, so we have the following function definition to work with:
\begin{verbatim}
COUNT_HCT: num -> 'a list -> 'a list list -> 'a list
\end{verbatim}
where the first argument represents the number of available seats, the second
argument the list of running candidates and the third argument the list of
ballots.
\subsubsection{Stateful Representation.}
Some assumptions about the internal operation of the function are
needed to capture the stateful or procedural nature of the
legislation. It is necessary to assume that \verb|COUNT_HCT|
possesses some form of state, and that the state changes over time.
Moreover the state must take a particular
structure, so we can reason formally about its various components.
In a strictly functional programming language there is no implicit
concept of time or state. The closest thing to a state is the set of values of
all of the variables at a given level of recursion. In this conceptual
representation of state, the ``time'' is given by the level of recursion.
Naturally, a proper representation of time must be strictly monotonic. That is, with
each recursion the time must increase. In other words, backtracking back up the
recursion cannot be permitted until the final result is ascertained (and it
becomes possible to backtrack all the way to the surface tail-recursively).
Ultimately, within the Hare-Clark context, our concept of time need only capture
the temporal difference between the stages of the count, not the assignment of
individual variables or other small differences. Bundling the requisite
variables into a ``state'' represented
by a tuple allows us to recurse on the tuple and treat it as a close
approximation of a mutable state.
Based on the properties referred to by the legislation, it is assumed that the
state of the count is represented by a tuple of the following structure:
\begin{verbatim}
(time, seats, quota, elected, excluded, rem, surps, groups)
\end{verbatim}
%(time, seats, quota, elected, excluded, remaining, pending)
where\ldots
\begin{description}
\item[\texttt{time}] is a parameter representing temporality (the level of
recursion). It increases by one with each recursion.
\item[\texttt{seats}] is the number of seats to be filled. Note
that this value is not intended to change over the course of the count.
\item[\texttt{quota}] is the number of votes required by candidates in
order to be declared elected. It is calculated at the
beginning and remains unchanged throughout.
\item[\texttt{elected}] is a list of candidates who have been elected.
Declaring a candidate elected (as specified in the legislation)
means placing a candidate in this list.
\item[\texttt{excluded}] is the list of excluded candidates. Excluding a candidate is
interpreted as placing a candidate in this list.
\item[\texttt{rem}] is the list of continuing candidates, along with their
current vote counts and their transfer history. Each candidate in this list
is represented by the % following tuple
% \begin{verbatim}
% (name, total, transfers)
% \end{verbatim}
tuple \verb|(name, total, transfers)|
where:
\begin{description}
\item[\texttt{name}] is the identifier of the candidate (this can be any equality type).
\item[\texttt{total}] is the total value of votes assigned to the candidate.
\item[\texttt{transfers}] is a list of transfers assigned to the candidate and is of
the form
% \begin{verbatim}
% (value, ballots, clause)
% \end{verbatim}
\verb|(value, ballots, clause)|
where
\begin{description}
\item[\texttt{value}] is the transfer value associated with the transfer and is a tuple of
the form \texttt{(numerator, denominator)}.
\item[\texttt{ballots}] is the list of ballots associated with the transfer.
\item[\texttt{clause}] is intended to represent the clause responsible for the transfer
of the ballots to the candidate concerned. Note that this will likely be
removed when the specification is reviewed as the implementation does not use it.
\end{description}
\end{description}
% \item[\texttt{pending}] is a list of transfers pending from the
% exclusion of a candidate. Members of this list are of the form
\item[\texttt{surps}] is a list of pending transfers of surplus votes
from elected candidate.
\item[\texttt{groups}] is a list of transfers pending from the
exclusion of a candidate. Each member of both \texttt{surps} and
\texttt{groups} is of the form
% \begin{verbatim}
% (value, ballots)
% \end{verbatim}
\verb|(value, ballots)|
where
\begin{description}
\item[\texttt{value}] is the transfer value of the ballots and is a tuple of the
form \texttt{(numerator, denominator)}.
\item[\texttt{ballots}] is the list of ballots awaiting transfer.
\end{description}
\end{description}
Assuming the function performing the recursion on the state tuple is called
\verb|FINAL_STAGE|, we have the following function type definition:
\begin{verbatim}
FINAL_STAGE: num # num # num # 'a list # 'a list #
('a # num # ((num # num) # 'a list list # num) list) list #
((num # num) # 'a list list # num) list
-> 'a list
\end{verbatim}
It can be argued that these assumptions are not necessary: that the functions
can be quantified in each of the clauses. This would remove any dependency
on naming conventions, but the clauses will still need to make statements relying
on what form the functions take. This has the potential to blow out the complexity
of the individual clauses as each clause will need to cover many more possibilities
in terms of functional structure. Whether or not this would actually happen
is unclear. Potentially, more experience is needed to truly take advantage of
the expressibility of higher order logic.
With the assumptions in hand, it becomes possible to translate the
legislation into HOL4's formal syntax. The translation of one example
clause, is given in Section~\ref{sec:clauses}. An example function and
statements that are used by the clauses are given in
Section~\ref{sec:ncd} below. Sanity checks are given in section
\ref{sec:sanity}. Note that the definitions, sanity checks and
clausal statements will need to be revised to take into account the
final form of the implementation. They will also need to be reviewed
for their accuracy.
\lstset{language=ML,
basicstyle=\ttfamily\footnotesize,
numberfirstline=true,
firstnumber=1,
numbers=left,
numberstyle=\tiny\color{grey},
numbersep=10pt,
stepnumber=1,
breaklines=false,
showstringspaces=false,
showlines=true,
escapeinside={\%*},
captionpos=t,
frame=tl,
%framexleftmargin=1em,
%xleftmargin=1em,
xleftmargin=17pt,
framexleftmargin=4pt,
framexrightmargin=5pt,
framexbottommargin=4pt,
framextopmargin=4pt,
rulecolor=\color{grey},
frameshape={ynn}{y}{n}{ynn},
tabsize=4
}
\subsection{Example Definitions}\label{sec:ncd}
% The following are some definitions relating to the counting procedure and its
% stateful representation. These are aimed at making the clausal statements in
% section \ref{sec:clauses} more manageable. Note that none of these are
% proof obligations. Rather they are used in the construction of the proof
% obligations.
% The functions shown in Listing \ref{lst:statevars} are used in the clausal
% statements to access various parts of the tuple representing the state of the
% count.
% \begin{lstlisting}[caption={Variable isolation functions.}, label={lst:statevars}]
% (* The following isolate members of the state variable *)
% val TIME_VAR_DEF = Define `TIME_VAR (a,b,c,d,e,f,g,h) = a`;
% val SEATS_VAR = Define `SEATS_VAR (a,b,c,d,e,f,g,h) = b`;
% val QUOTA_VAR_DEF = Define `QUOTA_VAR (a,b,c,d,e,f,g,h) = c`;
% val ELECTED_VAR_DEF = Define `
% ELECTED_VAR (a,b,c,d,e,f,g,h) = d`;
% val EXCLUDED_VAR_DEF = Define `
% EXCLUDED_VAR (a,b,c,d,e,f,g,h) = e`;
% val REM_CANDS_VAR_DEF = Define `
% REM_CANDS_VAR (a,b,c,d,e,f,g,h) = f`;
% val EXCL_TRANS_VAR_DEF = Define `
% EXCL_TRANS_VAR (a,b,c,d,e,f,g,h) = g`;
% (* The following isolate parts of a continuing candidate *)
% val NAME_DEF = Define `
% NAME (a,b,c) = a`;
% val TOTAL_COUNT_DEF = Define `
% TOTAL_COUNT (a,b,c) = b`;
% val TRANSFERS_DEF = Define `
% TRANSFERS (a,b,c) = c`;
% (* The following isolates the transfer value from a transfer *)
% val TRANSFER_VALUE_DEF = Define `
% TRANSFER_VALUE (a,b) = a`;
% \end{lstlisting}
The function shown in Listing \ref{lst:genfuncts} is used to simplify
the clauses in Section~\ref{sec:clauses}. Such functions are
intended to be executable and translatable into SML so that they may
be used by the counting program should this be necessary.
\begin{lstlisting}[caption={Executable function definitions.}, label={lst:genfuncts}]
(* Returns list of ballots whose first preference is cand *)
val FIRSTS_FOR_DEF = Define `
FIRSTS_FOR cand ballots =
FILTER (($= cand) o HD) ballots`;
(* Sums the number of ballots with a first preference for
each of the running candidates. This is needed simply
because the legislation specifies that this is how the
quota should be calculated. *)
val SUM_FIRSTS_DEF = Define `
(SUM_FIRSTS [] ballots = 0)
/\ (SUM_FIRSTS (c::cs) ballots =
LENGTH (FIRSTS_FOR c ballots)
+ SUM_FIRSTS cs ballots)`;
\end{lstlisting}
%$
% \begin{lstlisting}[caption={Executable function definitions.}, label={lst:genfuncts}]
% (* Swap parameters of a function *)
% val SWAP_PARAMS_DEF = Define `SWAP_PARAMS f x y = f y x`;
% (* Transfer value greater than *)
% val TV_GT_DEF = Define `TV_GT (a,b) (x,y) = a * y > x * b`;
% (* Transfer value equal *)
% val TV_EQ_DEF = Define `TV_EQ (a,b) (x,y) = (a * y = x * b)`;
% (* Initial timestamps *)
% val T0_DEF = Define `t0 = 0`;
% val T1_DEF = Define `t1 = t0 + 1`;
% (* Clause stamps *)
% val CLAUSE_2_DEF = Define `clause2 = 2`;
% val CLAUSE_6_DEF = Define `clause6 = 6`;
% val CLAUSE_8_DEF = Define `clause8 = 8`;
% val CLAUSE_9_DEF = Define `clause9 = 9`;
% (* Gives the first preference of the supplied ballots. Note that we
% are assuming that only formal ballots are passed to the counting
% function. *)
% val FIRST_PREF_DEF = Define `
% (FIRST_PREF cands [] = NONE)
% /\ (FIRST_PREF cands (c::cs) = if MEM c cands then SOME c
% else NONE)`;
% (* Returns a list of ballots whose first preferences are for cand *)
% val FIRSTS_FOR_DEF = Define `
% FIRSTS_FOR cand ballots =
% FILTER (($= cand) o HD) ballots`;
% (* Sums the number of ballots with a first preference for each of the
% running candidates. This is needed simply because the legislation
% specifies that this is how the quota should be calculated. *)
% val SUM_FIRSTS_DEF = Define `
% (SUM_FIRSTS [] ballots = 0)
% /\ (SUM_FIRSTS (c::cs) ballots = LENGTH (FIRSTS_FOR c ballots)
% + SUM_FIRSTS cs ballots)`;
% (* Strip candidates till "next preference" *)
% val STRIP_BALLOT_DEF = Define `
% (STRIP_BALLOT excluded elected [] = [])
% /\ (STRIP_BALLOT excluded elected (c::cs) =
% if (MEM c excluded \/ MEM c elected)
% then STRIP_BALLOT excluded elected cs
% else (c::cs))`;
% \end{lstlisting}
% %$
% The functions listed in Listing \ref{lst:nonexecfuncts} show some more
% functions used to simplify the clausal statements in section
% \ref{sec:clauses}. These functions are not intended to be translatable
% to SML, and cannot necessarily be used by the counting program.
% \begin{lstlisting}[caption={Non-executable functions definitions.}, label={lst:nonexecfuncts}]
% (* Boolean test of whether cand_entry contains a surplus in state *)
% val HAS_SURPLUS_DEF = Define `
% HAS_SURPLUS state cand_entry =
% MEM cand_entry (REM_CANDS_VAR state)
% /\ TOTAL_COUNT cand_entry > QUOTA_VAR state`;
% (* Boolean test of whether cand has obtained a surplus in state *)
% val HAS_SURPLUS_GEN_DEF = Define `
% HAS_SURPLUS_GEN state cand = ?cand_entry. FST cand_entry = cand
% /\ MEM cand_entry (REM_CANDS_VAR state)
% /\ TOTAL_COUNT cand_entry > QUOTA_VAR state`;
% (* Boolean test: is cand one of the remaining candidates in state? *)
% val IS_REM_CAND_DEF = Define `
% IS_REM_CAND state cand =
% ?cand_entry. MEM cand_entry (REM_CANDS_VAR state)
% /\ FST cand_entry = cand`;
% (* Candidate removed from list of continuing candidates at time t *)
% val SURPLUS_TRANSFERRED_AT_DEF = Define `
% SURPLUS_TRANSFERRED_AT seats cands ballots t cand =
% ?state state'.
% (COUNT_HCT seats cands ballots = FINAL_STAGE state)
% /\ (COUNT_HCT seats cands ballots = FINAL_STAGE state')
% /\ (TIME_VAR state' = SUC (TIME_VAR state))
% /\ (TIME_VAR state = t)
% /\ IS_REM_CAND state cand /\ ~IS_REM_CAND state' cand`;
% (* The transfer group "group" is transferred at time t *)
% val GROUP_TRANSFERRED_AT_DEF = Define `
% GROUP_TRANSFERRED_AT seats cands ballots t group =
% ?pre_state post_state.
% (COUNT_HCT seats cands ballots = FINAL_STAGE pre_state)
% /\ (COUNT_HCT seats cands ballots = FINAL_STAGE post_state)
% /\ (TIME_VAR post_state = SUC t)
% /\ (TIME_VAR pre_state = t)
% /\ MEM group (EXCL_TRANS_VAR pre_state)
% /\ ~MEM group (EXCL_TRANS_VAR post_state)
% /\ !rcvr_pre. MEM rcvr_pre (REM_CANDS_VAR pre_state)
% ==> ?rcvr_post. (FST rcvr_post = FST rcvr_pre)
% /\ (TOTAL_COUNT rcvr_post
% = TOTAL_COUNT rcvr_pre + ((FST (FST group))
% * (LENGTH (FILTER (($= (FST rcvr_pre)) o HD
% o (UPDATE_BALLOT (EXCL_VAR pre_state)
% (ELECTED_VAR pre_state))) (SND group)))
% DIV (SND (FST group))))
% /\ (SND (SND rcvr_post)
% = (FST group
% , FILTER (($= (FST rcvr_pre)) o HD
% o (UPDATE_BALLOT (EXCL_VAR pre_state)
% (ELECTED_VAR pre_state))) (SND group)
% , clause9)
% ::(SND (SND rcvr_pre)))
% /\ MEM rcvr_post (REM_CANDS_VAR post_state)`;
% (* Returns the transfers in trans_list with transfer value tv *)
% val EXTRACT_TRANSFERS_DEF = Define `
% EXTRACT_TRANSFERS trans_list tv =
% FLAT (FST (UNZIP (SND (UNZIP
% (FILTER ((TV_EQ tv) o FST) trans_list)))))`;
% (* Candidates cand1 and cand2 have an equal count in state *)
% val COUNTS_EQUAL_DEF = Define `
% COUNTS_EQUAL cand1 cand2 state
% = ?cand_entry1 cand_entry2.
% (FST cand_entry1 = cand1)
% /\ (FST cand_entry2 = cand2)
% /\ MEM cand_entry1 (REM_CANDS_VAR state)
% /\ MEM cand_entry2 (REM_CANDS_VAR state)
% /\ (TOTAL_COUNT cand_entry1 = TOTAL_COUNT cand_entry2)`;
% (* Count of cand1 is less than count of cand2 in state *)
% val COUNT_LESS_THAN_DEF = Define `
% COUNT_LESS_THAN cand1 cand2 state
% = ?cand_entry1 cand_entry2.
% (FST cand_entry1 = cand1)
% /\ (FST cand_entry2 = cand2)
% /\ MEM cand_entry1 (REM_CANDS_VAR state)
% /\ MEM cand_entry2 (REM_CANDS_VAR state)
% /\ TOTAL_COUNT cand_entry1 < TOTAL_COUNT cand_entry2`;
% (* Count of cand1 is less than or equal to count of cand2 in state *)
% val COUNT_LESS_EQUAL_DEF = Define `
% COUNT_LESS_EQUAL cand1 cand2 state
% = ?cand_entry1 cand_entry2.
% (FST cand_entry1 = cand1)
% /\ (FST cand_entry2 = cand2)
% /\ MEM cand_entry1 (REM_CANDS_VAR state)
% /\ MEM cand_entry2 (REM_CANDS_VAR state)
% /\ TOTAL_COUNT cand_entry1 <= TOTAL_COUNT cand_entry2`;
% \end{lstlisting}
\subsection{Sanity Checks}\label{sec:sanity}
In addition to the clauses of the Tasmanian Hare-Clark legislation, some proof
obligations have been defined as sanity checks. These sanity checks can be
assumed in the clausal statements, reducing their complexity. One
such sanity checks is shown
%in Listings \ref{lst:remcandsdist}--\ref{lst:exclelectdisj}
below.
% Listing \ref{lst:remcandsdist} specifies that all of the candidates in the
% list of continuing candidates must be unique candidates. That is, a candidate
% cannot appear more than once in the list.
% \begin{lstlisting}[caption={Continuing candidates all distinct.},label={lst:remcandsdist}]
% !seats cands ballots state.
% (COUNT_HCT seats cands ballots = FINAL_STAGE state)
% ==> !entry1 entry2 x y. (EL x (REM_CANDS_VAR state) = entry1)
% /\ (EL y (REM_CANDS_VAR state) = entry1)
% ==> ((FST entry1 = FST entry2) ==> (x = y))
% \end{lstlisting}
% Listing \ref{lst:electdist} specifies that all of the candidates in the list
% of elected candidates must be unique.
% \begin{lstlisting}[caption={Elected candidates are all distinct.},label={lst:electdist}]
% !seats cands ballots state.
% (COUNT_HCT seats cands ballots = FINAL_STAGE state)
% ==> ALL_DISTINCT (ELECTED_VAR state)
% \end{lstlisting}
% Listing \ref{lst:excldist} specifies that all of the candidates in the list
% of excluded candidates must be unique.
% \begin{lstlisting}[caption={Excluded candidates are all distinct.},label={lst:excldist}]
% !seats cands ballots state.
% (COUNT_HCT seats cands ballots = FINAL_STAGE state)
% ==> ALL_DISTINCT (EXCL_VAR state)
% \end{lstlisting}
Listing \ref{lst:noreint} specifies that it must be impossible to
introduce candidates to the list of
continuing candidates after the count has begun. In other words, if a
candidate is in the list of continuing candidates, then that candidate must
have been in the list of candidates in all preceding states of the
count.
\begin{lstlisting}[caption={Candidates cannot be introduced partway through
the count.},label={lst:noreint}]
!seats cands ballots state state'.
(COUNT_HCT seats cands ballots = FINAL_STAGE state)
/\ (COUNT_HCT seats cands ballots = FINAL_STAGE state')
/\ TIME_VAR state' > TIME_VAR state
==> !cand. IS_REM_CAND state' cand
==> IS_REM_CAND state cand
\end{lstlisting}
% Listing \ref{lst:electedpersistent} specifies that once a candidate has
% been elected, that candidate remains elected for the remainder of the
% counting process. More specifically, a candidate cannot be \emph{removed} from
% the list of elected candidates at any stage of the counting.
% \begin{lstlisting}[caption={Elected persistent.},label={lst:electedpersistent}]
% !seats cands ballots state state' cand.
% (COUNT_HCT seats cands ballots = FINAL_STAGE state)
% /\ (COUNT_HCT seats cands ballots = FINAL_STAGE state')
% /\ TIME_VAR state' > TIME_VAR state
% /\ MEM cand (ELECTED_VAR state)
% ==> MEM cand (ELECTED_VAR state')
% \end{lstlisting}
% Listing \ref{lst:excludedpersistent} specifies that excluded candidates
% remain excluded for the duration of the remainder of the count. In the
% context of the program, no candidate can be removed from the list of
% excluded candidates once added.
% \begin{lstlisting}[caption={Excluded persistent.},label={lst:excludedpersistent}]
% !seats cands ballots state state' cand.
% (COUNT_HCT seats cands ballots = FINAL_STAGE state)
% /\ (COUNT_HCT seats cands ballots = FINAL_STAGE state')
% /\ TIME_VAR state' > TIME_VAR state
% /\ MEM cand (EXCL_VAR state)
% ==> MEM cand (EXCL_VAR state')
% \end{lstlisting}
% Listing \ref{lst:exclelectdisj} specifies that candidates cannot be both
% excluded and elected simultaneously. In other words, if a candidate is
% elected then that candidate cannot be excluded, and if a candidate is
% excluded, then that candidate cannot be elected. Coupled with the sanity
% checks in Listings \ref{lst:electedpersistent} and \ref{lst:excludedpersistent},
% this check ensures that if a candidate is excluded, that candidate cannot
% be declared elected at any stage of the count (and vice versa).
% \begin{lstlisting}[caption={Elected and excluded disjoint.},label={lst:exclelectdisj}]
% !seats cands ballots state cand.
% (COUNT_HCT seats cands ballots = FINAL_STAGE state)
% /\ (MEM cand (EXCL_VAR state) ==> ~MEM cand (ELECTED_VAR state))
% /\ (MEM cand (ELECTED_VAR state) ==> ~MEM cand (EXCL_VAR state))
% \end{lstlisting}
\subsection{Example of a Clause in Higher-order Logic }\label{sec:clauses}
Each of the 14 clauses in the Tasmanian Hare-Clark legislation was thus
hand-translated into higher-order logic. We give just one example below.
% \subsubsection{Clause 1: Interpretation}
% \begin{quote}
% \begin{enumerate}[(1)]
% \item In this Schedule, unless the contrary intention appears ---
% \begin{description}
% \item[quota] means the number of votes sufficient to elect a candidate at an election;
% \item[second preference recorded for a candidate] means the recording of the number ``2'' in the box next to the name of a candidate on a ballot paper;
% \item[surplus] means the number of votes which a candidate has obtained, at any stage of the counting of votes, in excess of the quota;
% \item[transfer value] means that portion of a vote which is transferred to the candidate next in the order of the elector's preference because it is unused by ---
% \begin{enumerate}[(a)]
% \item an elected candidate who has obtained a surplus; or
% \item a candidate excluded on account of his or her having the least number of votes.
% \end{enumerate}
% \end{description}
% \item For the purpose of the definition of ``transfer value'' in subclause (1), the transfer value of a vote is either one or a fraction of one.
% \end{enumerate}
% \end{quote}
% This clause is primarily definitional, and as such no proof obligation was
% derived.
% Instead, the following definition was made to reflect subclause (2).
% \begin{lstlisting}[caption={Valid transfer value.},label={lst:clause1}]
% val VALID_TRANS_VAL_DEF = Define `
% VALID_TRANS_VAL (n, d) = n <= d /\ n > 0`;
% \end{lstlisting}
% Under review, this clause will likely be turned into a proof obligation
% in its own right, ensuring that any transfer values that occur in the count
% are less than a fraction of 1.
\subsubsection{Clause 2: First preference votes to be counted}
\begin{quote}
The number of first preferences recorded for each candidate, on ballot papers
which are not informal ballot papers, is to be counted.
\end{quote}
This is somewhat abstract
in the context of our counting procedure and leaves little to specify concretely.
The proof obligation for this clause in HOL4 instead specifies how the counts
should be incorporated into the initial state tuple. See Listing \ref{lst:clause2}
below.
\begin{lstlisting}[caption={Clause 2},label={lst:clause2}]
!seats cands ballots cand rem_cands quota.
(COUNT_HCT seats cands ballots =
FINAL_STAGE (t0,seats,quota,[],[],rem_cands,[]))
/\ (MEM cand cands =
MEM (cand,
LENGTH (FIRSTS_FOR cand ballots),
[((1,1), FIRSTS_FOR cand ballots, clause2)])
rem_cands)
\end{lstlisting}
Note that the ``count'' of the first preferences is given by
\texttt{LENGTH (FIRSTS\_FOR cand ballots)}. The function \texttt{LENGTH}
is a predefined function in HOL4, and \texttt{FIRSTS\_FOR} is defined in
Listing~\ref{lst:genfuncts}.
% \subsection{Suggested Changes}
% There are several changes that will need to be made to the \spechol before it can
% be considered an accurate representation of the legislation.
% \begin{enumerate}
% \item The \spechol will need to be adjusted for the differences between the
% assumed functional structure from section \ref{sec:assumptions} and the final
% structure from section \ref{sec:hctcode}.
% The structure of the state tuple will need to be adjusted in \spechol to
% include the list of pending surplus transfers.
% \item The clauses can be strengthened by adding stipulations that any
% parts of the state tuple not involved in an update to the state must remain
% unchanged.
% \item Clauses 12 and 7(2) need to be updated to reflect the use of the
% lexicographical ordering method of breaking ties used in the implementation.
% Alternatively the implementation needs to be changed to reflect one of the
% clauses, and the other clause needs to be adapted accordingly.
% \item The assumptions upon which the clauses are based can be encoded as
% higher-order functions and type signatures. This will
% make the assumptions more rigorous and allow for associated proofs.
% \end{enumerate}
\section{From HOL4 to an SML Implementation}
The implementation is first written in HOL4, then translated into SML.
The translation is performed iteratively, ironing out any features used in
one language that are not available in the other. Since the implementation
is initially programmed in HOL4, the features that need removal are
primarily those available in HOL4 but not SML (a lambda calculus interpreter
for instance).
%As in the small-scale case study,
The semantic equivalence of these two implementations
is not rigorously guaranteed. A visual comparison is still convincing for this
larger case study, however, thanks to the strict functional nature of the implementations
and the restricted feature set they use.
The implementation breaks ties using the lexicographical ordering interpretation
(option (\ref{itm:lex}) on page \pageref{itm:lex}).
It does this by merge-sorting the list
of remaining candidates according to candidate counts at each stage of the
recursion. Merge sort is stable, allowing it to maintain the lexicographical
ordering discussed without further interference.
% \subsection{Code}\label{sec:hctcode}
% The code for the implementation
% is given in HOL4 syntax in Listing \ref{lst:hctimphol} and in SML syntax in Listing
% \ref{lst:hctimpsml}. Note that the implementations makes use of some of the
% definitions made in preparation for the specification from Listings \ref{lst:statevars}
% and \ref{lst:genfuncts}. The SML translations of these functions are included in
% the SML code listing (Listing \ref{lst:hctimpsml}).
% \begin{lstlisting}[caption={Hare-Clark Implementation in HOL4},label={lst:hctimphol}]
% (********************** Specialised Functions **********************)
% (* Combines function 'f' and relation 'r' to arguments 'a' and 'b' *)
% val COMBINE_DEF = Define `COMBINE f r a b = r (f a) (f b)`;
% (* Returns those candidates with a sufficient count to be elected. *)
% val EXTRACT_ELECTED_DEF = Define `
% (EXTRACT_ELECTED quota [] acc = acc)
% /\ (EXTRACT_ELECTED quota (c::cs) acc
% = if (TOTAL_COUNT c) >= quota
% then EXTRACT_ELECTED quota cs ((NAME c)::acc)
% else acc)`; (* Sorted, so we're done *)
% (* Extracts surpluses from the list of continuing candidates. *)
% (* Also returns a modified list of continuing candidates with *)
% (* those candidates who have a surplus removed. *)
% val EXTRACT_SURPS_DEF = Define `
% (EXTRACT_SURPS quota [] acc = ([], REVERSE acc))
% /\ (EXTRACT_SURPS quota ((name,total,[])::cs) acc
% = ((name,total,[])::cs, REVERSE acc))
% /\ (EXTRACT_SURPS quota ((name,total,(tv,bs,clause)::ts)::cs) acc
% = if total > quota
% then EXTRACT_SURPS quota cs
% (((total - quota, LENGTH bs) ,bs)::acc)
% else ((name,total,(tv,bs,clause)::ts)::cs, REVERSE acc))`;
% (* Sorted list, so we're done *)
% (* Removes candidates with an exact surplus from the list of *)
% (* continuing candidates. *)
% val DROP_EXACT_DEF = Define `
% (DROP_EXACT quota [] = [])
% /\ (DROP_EXACT quota (c::cs) = if (TOTAL_COUNT c) = quota
% then DROP_EXACT quota cs
% else (c::cs))`;
% (* Boolean test: is the head of the list equal to 'cand'? *)
% val HEAD_IS_DEF = Define `
% (HEAD_IS cand [] = F)
% /\ (HEAD_IS cand (h::t) = if h = cand then T else F)`;
% (* Handles transfer, returns updated list of continuing candidates *)
% val TRANSFER_BALLOTS_DEF = Define `
% (TRANSFER_BALLOTS clause excluded elected [] transfer acc = acc)
% /\ (TRANSFER_BALLOTS clause excluded elected
% ((name, count, transfers)::es) ((n,d), ballots) acc =
% let votes =
% FILTER ((HEAD_IS name) o (STRIP_BALLOT excluded elected))
% ballots in (* update_ballots *)
% let trans_size = ((LENGTH votes) * n) DIV d in
% TRANSFER_BALLOTS clause excluded elected es ((n,d), ballots)
% ((name, count + trans_size,
% ((n,d), votes, clause)::transfers)::acc))`;
% (* Takes a transfer and combines it with a transfer group with the *)
% (* same transfer value in the list provided. If there is no such *)
% (* group, a new one is created and appended. *)
% val COALESCE_DEF = Define `
% (COALESCE transfer [] = [transfer])
% /\ (COALESCE (tv, bs) ((gtv, gbs)::gs) =
% if TV_EQ tv gtv then ((gtv, bs ++ gbs)::gs)
% else ((gtv, gbs)::(COALESCE (tv, bs) gs)))`;
% (* Used by MERGE_SORT. *)
% val MERGE_DEF = Define `
% (MERGE R [] right = right)
% /\ (MERGE R left [] = left)
% /\ (MERGE R (l::ls) (r::rs) = if R l r
% then l::(MERGE R ls (r::rs))
% else r::(MERGE R (l::ls) rs))`;
% (* Standard merge sort. Needs valid proof of termination. *)
% val MERGE_SORT_DEF = tDefine "MERGE_SORT" `
% (MERGE_SORT R [] = [])
% /\ (MERGE_SORT R [h] = [h])
% /\ (MERGE_SORT R (h::t) =
% let middle = (LENGTH (h::t)) DIV 2 in
% let left = MERGE_SORT R (TAKE (middle) (h::t)) in
% let right = MERGE_SORT R (DROP (middle) (h::t)) in
% MERGE R left right)`
% (* Proof of termination here *);
% (* Groups transfers based on transfer value. *)
% val GROUP_DEF = Define `
% (GROUP [] acc = MERGE_SORT (COMBINE TRANSFER_VALUE TV_GT) acc)
% /\ (GROUP (t::ts) acc = GROUP ts (COALESCE t acc))`;
% (* Returns a double with the second member cons'd with surps *)
% val SND_CONS_DEF = Define `
% SND_CONS surps (a,b) = (a, surps ++ b)`;
% (* Returns the first two members of a triple as a double. *)
% val FIRST_TWO_DEF = Define `
% FIRST_TWO (a, b, c) = (a, b)`;
% (*************************** Main Logic ****************************)
% (* Contains most of the counting logic (ie. decisions about what *)
% (* actions need to be taken at each stage). Takes the state tuple *)
% (* as an argument, changes it depending on circumstances, then *)
% (* recurses on itself. Ultimately returns the list of elected *)
% (* candidates. Needs a proof of termination. *)
% (*******************************************************************)
% val FINAL_STAGE_DEF = tDefine "FINAL_STAGE"
% `FINAL_STAGE
% (time, seats, quota, elected, excluded, rem, surps, groups) =
% if (LENGTH elected) + (LENGTH rem) = seats
% then elected ++ (MAP NAME rem)
% else
% let rem_sorted = MERGE_SORT (COMBINE TOTAL_COUNT $>=) rem in
% let elected' = EXTRACT_ELECTED quota rem_sorted elected in
% let (cur_rem, surps')
% = SND_CONS surps (EXTRACT_SURPS quota rem_sorted []) in
% let cur_rem' = DROP_EXACT quota cur_rem in
% if ~(NULL groups)
% then (* transfer group *)
% let rem' = REVERSE
% (TRANSFER_BALLOTS
% clause9 excluded elected cur_rem' (HD groups) []) in
% FINAL_STAGE (time + 1, seats, quota, elected', excluded,
% rem', surps', TL groups)
% else if ~(NULL surps')
% then (* transfer surplus, clause here is dubious... *)
% let rem' = REVERSE
% (TRANSFER_BALLOTS
% clause8 excluded elected cur_rem' (HD surps') []) in
% FINAL_STAGE (time + 1, seats, quota, elected', excluded,
% rem', TL surps', groups)
% else (* eliminate candidate *)
% let groups' = GROUP
% ((MAP FIRST_TWO) (TRANSFERS (LAST cur_rem'))) [] in
% let excluded' = (NAME (LAST cur_rem')::excluded) in
% FINAL_STAGE (time + 1, seats, quota, elected', excluded',
% FRONT cur_rem', surps', groups')`
% (* Insert termination proof here *);
% (* Tail-recursively constructs the initial list of continuing *)
% (* candidates. *)
% val ALLOC_VOTES_DEF = Define `
% (ALLOC_VOTES [] ballots so_far = so_far)
% /\ (ALLOC_VOTES (c::cs) ballots so_far =
% let
% votes = FILTER (($= c) o HD) ballots
% in
% ALLOC_VOTES cs ballots
% ((c, LENGTH votes, [((1,1), votes, 2)])::so_far))`;
% (************************** Main Function **************************)
% (* *)
% (* Entry point to the count. Call this function to count a *)
% (* Tasmanian House of Assemlby election. *)
% (* *)
% (* Arguments: seats -- number of seats: int *)
% (* cands -- list of running candidates: 'a list *)
% (* ballots -- list of ballots: 'a list list *)
% (* *)
% (* Returns: List of candidates elected ('a list) *)
% (* *)
% (* When there is an unresolvable tie for elimination or surplus *)
% (* transfer, the candidate that is part of the tie and occurs *)
% (* latest in the argument 'cands' is selected for elimination. *)
% (* Therefore if random decisions are desired, the order of the *)
% (* argument 'cands' should be randomised. The results are *)
% (* reproducible by maintaining the order of the 'cands' argument *)
% (* in subsequent calls. *)
% (* *)
% (*******************************************************************)
% val COUNT_HCT_DEF = Define `
% (* Insert special cases here *)
% COUNT_HCT seats cands ballots =
% let
% rem_cands = ALLOC_VOTES cands ballots []
% in
% let
% state = (0, seats,
% ((LENGTH ballots) DIV (1 + seats)) + 1,
% [], [], rem_cands, [], [])
% in
% FINAL_STAGE state`;
% \end{lstlisting}
% \begin{lstlisting}[caption={Hare-Clark Implementation in SML},label={lst:hctimpsml}]
% (********************** Pre-Defined Functions **********************)
% (* These seven functions are pre-defined in HOL4, and have been *)
% (* translated here into SML to maintain consistency. *)
% (*******************************************************************)
% fun MEM x [] = false
% | MEM x (h::t) = (x = h) orelse MEM x t;
% fun FILTER P [] = []
% | FILTER P (h::t) = if P h then h::FILTER P t else FILTER P t;
% fun TAKE n [] = []
% | TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n - 1) xs;
% fun DROP n [] = []
% | DROP n (x::xs) = if n = 0 then x::xs else DROP (n - 1) xs;
% fun UNZIP [] = ([], [])
% | UNZIP ((a,b)::t) = (a::(#1 (UNZIP t)), b::(#2 (UNZIP t)));
% fun LAST (h::t) = if t = [] then h else LAST t;
% fun FRONT (h::t) = if t = [] then [] else h::FRONT t;
% (***************** Functions Translated from \spechol ******************)
% (* The following eleven functions were defined as part of the *)
% (* specification, but are useful for the implementation also, so *)
% (* have been reproduced in SML here. *)
% (*******************************************************************)
% (* For deconstructing entries of continuing candidates *)
% fun NAME (a,b,c) = a;
% fun TOTAL_COUNT (a,b,c) = b;
% fun TRANSFERS (a,b,c) = c;
% (* For extracting a transfer value from a transfer *)
% fun TRANSFER_VALUE (a,b) = a;
% (* Comparisons between transfer values... *)
% fun TV_GT (a,b) (x,y) = a * y > x * b;
% fun TV_EQ (a,b) (x,y) = (a * y = x * b);
% (* Clause stamps *)
% val clause2 = 2;
% val clause6 = 6;
% val clause8 = 8;
% val clause9 = 9;
% (* Strip candidates till "next preference" *)
% fun STRIP_BALLOT excluded elected [] = []
% | STRIP_BALLOT excluded elected (c::cs) =
% if MEM c excluded orelse MEM c elected
% then STRIP_BALLOT excluded elected cs
% else (c::cs);
% (************************ Counting Program *************************)
% (* Combines function 'f' and relation 'r' to arguments 'a' and 'b' *)
% fun COMBINE f r a b = r (f a) (f b);
% (* Returns those candidates with a sufficient count to be elected. *)
% fun EXTRACT_ELECTED quota [] acc = acc
% | EXTRACT_ELECTED quota (c::cs) acc
% = if (TOTAL_COUNT c) >= quota
% then EXTRACT_ELECTED quota cs ((NAME c)::acc)
% else acc; (* Sorted, so we're done *)
% (* Extracts surpluses from the list of continuing candidates. *)
% (* Also returns a modified list of continuing candidates with *)
% (* those candidates who have a surplus removed. *)
% fun EXTRACT_SURPS quota [] acc = ([], rev acc)
% | EXTRACT_SURPS quota ((name,total,[])::cs) acc
% = ((name,total,[])::cs, rev acc)
% | EXTRACT_SURPS quota ((name,total,(tv,bs,clause)::ts)::cs) acc
% = if total > quota
% then EXTRACT_SURPS quota cs
% (((total - quota, length bs) ,bs)::acc)
% else ((name,total,(tv,bs,clause)::ts)::cs, rev acc);
% (* Sorted list, so we're done *)
% (* Removes candidates with an exact surplus from the list of *)
% (* continuing candidates. *)
% fun DROP_EXACT quota [] = []
% | DROP_EXACT quota (c::cs) = if (TOTAL_COUNT c) = quota
% then DROP_EXACT quota cs
% else (c::cs);
% (* Boolean test: is the head of the list equal to 'cand'? *)
% fun HEAD_IS cand [] = false
% | HEAD_IS cand (h::t) = if h = cand then true else false;
% (* Handles transfer, returns updated list of continuing candidates *)
% fun TRANSFER_BALLOTS clause excluded elected [] transfer acc = acc
% | TRANSFER_BALLOTS clause excluded elected
% ((name, count, transfers)::es) ((n,d), ballots) acc =
% let val votes =
% FILTER ((HEAD_IS name) o (STRIP_BALLOT excluded elected))
% ballots in (* update_ballots *)
% let val trans_size = ((length votes) * n) div d in
% TRANSFER_BALLOTS clause excluded elected es ((n,d), ballots)
% ((name, count + trans_size,
% ((n,d), votes, clause)::transfers)::acc)
% end end;
% (* Takes a transfer and combines it with a transfer group with the *)
% (* same transfer value in the list provided. If there is no such *)
% (* group, a new one is created and appended. *)
% fun COALESCE transfer [] = [transfer]
% | COALESCE (tv, bs) ((gtv, gbs)::gs) =
% if TV_EQ tv gtv then ((gtv, bs @ gbs)::gs)
% else ((gtv, gbs)::(COALESCE (tv, bs) gs));
% (* Used by MERGE_SORT. *)
% fun MERGE R [] right = right
% | MERGE R left [] = left
% | MERGE R (l::ls) (r::rs) = if R l r
% then l::(MERGE R ls (r::rs))
% else r::(MERGE R (l::ls) rs);
% (* Standard merge sort. *)
% fun MERGE_SORT R [] = []
% | MERGE_SORT R [h] = [h]
% | MERGE_SORT R (h::t) =
% let val middle = (length (h::t)) div 2 in
% let val left = MERGE_SORT R (TAKE (middle) (h::t)) in
% let val right = MERGE_SORT R (DROP (middle) (h::t)) in
% MERGE R left right
% end end end;
% (* Groups transfers based on transfer value. *)
% fun GROUP [] acc = MERGE_SORT (COMBINE TRANSFER_VALUE TV_GT) acc
% | GROUP (t::ts) acc = GROUP ts (COALESCE t acc);
% (* Returns a double with the second member cons'd with surps *)
% fun SND_CONS surps (a,b) = (a, surps @ b);
% (* Returns the first two members of a triple as a double. *)
% fun FIRST_TWO (a, b, c) = (a, b);
% (*************************** Main Logic ****************************)
% (* Contains most of the counting logic (ie. decisions about what *)
% (* actions need to be taken at each stage). Takes the state tuple *)
% (* as an argument, changes it depending on circumstances, then *)
% (* recurses on itself. Ultimately returns the list of elected *)
% (* candidates. *)
% (*******************************************************************)
% fun FINAL_STAGE
% (time, seats, quota, elected, excluded, rem, surps, groups) =
% if (length elected) + (length rem) = seats
% then elected @ (map NAME rem)
% else
% let val rem_sorted
% = MERGE_SORT (COMBINE TOTAL_COUNT (curry op>=)) rem in
% let val elected'
% = EXTRACT_ELECTED quota rem_sorted elected in
% let val (cur_rem, surps')
% = SND_CONS surps (EXTRACT_SURPS quota rem_sorted []) in
% let val cur_rem' = DROP_EXACT quota cur_rem in
% if not (null groups)
% then (* transfer group *)
% let val rem' = rev
% (TRANSFER_BALLOTS
% clause9 excluded elected' cur_rem' (hd groups) []) in
% FINAL_STAGE (time + 1, seats, quota, elected', excluded,
% rem', surps', tl groups)
% end
% else if not (null surps')
% then (* transfer surplus, clause here is dubious... *)
% let val rem' = rev
% (TRANSFER_BALLOTS
% clause8 excluded elected' cur_rem' (hd surps') []) in
% print ("Transferring surplus...\n\n") ;
% FINAL_STAGE (time + 1, seats, quota, elected', excluded,
% rem', tl surps', groups)
% end
% else (* eliminate candidate *)
% let val groups' = GROUP
% ((map FIRST_TWO) (TRANSFERS (LAST cur_rem'))) [] in
% let val excluded' = ((NAME (LAST cur_rem'))::excluded) in
% FINAL_STAGE (time + 1, seats, quota, elected', excluded',
% FRONT cur_rem', surps', groups')
% end end
% end end end end;
% (* Tail-recursively constructs the initial list of continuing *)
% (* candidates. *)
% fun ALLOC_VOTES [] ballots so_far = so_far
% | ALLOC_VOTES (c::cs) ballots so_far =
% let
% val votes = FILTER (((curry op=) c) o hd) ballots
% in
% ALLOC_VOTES cs ballots
% ((c, length votes, [((1,1), votes, 2)])::so_far)
% end;
% (************************** Main Function **************************)
% (* *)
% (* Entry point to the count. Call this function to count a *)
% (* Tasmanian House of Assemlby election. *)
% (* *)
% (* Arguments: seats -- number of seats: int *)
% (* cands -- list of running candidates: 'a list *)
% (* ballots -- list of ballots: 'a list list *)
% (* *)
% (* Returns: List of candidates elected ('a list) *)
% (* *)
% (* When there is an unresolvable tie for elimination or surplus *)
% (* transfer, the candidate that is part of the tie and occurs *)
% (* latest in the argument 'cands' is selected for elimination. *)
% (* Therefore if random decisions are desired, the order of the *)
% (* argument 'cands' should be randomised. The results are *)
% (* reproducible by maintaining the order of the 'cands' argument *)
% (* in subsequent calls. *)
% (* *)
% (*******************************************************************)
% fun COUNT_HCT seats cands ballots =
% let
% val rem_cands = ALLOC_VOTES cands ballots []
% in
% let
% val state = (0, seats,
% ((length ballots) div (1 + seats)) + 1,
% [], [], rem_cands, [], [])
% in
% FINAL_STAGE state
% end
% end;
% \end{lstlisting}
\subsection{Testing the SML Implementation for Efficiency}\label{sec:largetests}
The implementation was tested both for preliminary correctness and to
ascertain whether it could handle the input sizes likely in real
public elections. All of the tests were conducted using PolyML
(\url{http://www.polyml.org/}) on GNU/Linux with an Intel Core
i7-3740QM processor and 16 GiB of RAM.
To test for bugs, we compared this implementation against an
implementation of the ACT's Hare-Clark system produced previously by
Dawson. Several randomly generated examples were produced with lists
of votes ranging from 50 thousand to 300 thousand in length and
between 10 and 40 candidates covering a range of possible
scenarios.\footnote{If a large number of ballots are generated
na\"ively, they become spread too evenly between the candidates.
This results in no candidate being elected until the final stages of
the count, which is unrealistic. The candidates were given random
popularity ratings to produce uneven distributions of ballots to
avoid this issue.} The two programs produced the same results for
each example, giving preliminary indications that the program is
correct.
However, there are differences between Hare-Clark ACT and Hare-Clark
Tasmania. The main difference that might lead to a
different outcome at an election is that the transfer value is
calculated differently. Tasmanian Hare-Clark calculates the transfer
value based on the total number of votes in the transfer leading to
the surplus whereas the ACT calculates it based on a subset of those:
the unexhausted ballots. The following small example which
illustrates the difference.
Imagine an election between 3 candidates (A, B and C), with two
available seats and a total of 5 votes. Let's say the votes were as
follows:
\texttt{
[A,B]
[A,B]
[A]
[A]
[C]
}
where the vote can be read from left to right in order of preference (so
the first vote has A as its first preference and B as its second).
%
In the first round, A will be elected with 4 votes and a surplus of 2
(the Droop quota is 2 votes). B and C remain unelected with counts of 0
and 1 respectively.
%
In the second round, 2 of A's votes will be counted towards B, but the
transfer value differs between the ACT and Tasmanian systems:
\begin{description}
\item[\rm TAS] = (surplus / total votes in prev.\ transfer)
= 2 / 4 = 1/2
\item[\rm ACT] = (surplus / total unexhaust. votes in
prev. transfer) = 2 / 2 = 1
\end{description}
Thus,the ACT would transfer the votes in
full, whereas in Tasmania they would transfer them as half votes.
So the result after round 2 would be:
\begin{description}
\item[\rm TAS:] 1 for C, 1 for B so B eliminated
as C had more votes in previous round;
\item[\rm ACT:] 1 for C, 2 for B so C eliminated.
\end{description}
% Strictly speaking,\marginpar{JED, did you extend the example to be a proper
% example?} this example doesn't adhere to Hare Clark formally
% (there aren't enough seats available in our scenario, or enough votes
% on the ballots to make them valid), but it was about as simple an
% example we could find.
The programs confirmed that this example leads
to a different results.
%The programs don't require a particular number
%of seats or a minimum number of preferences on the ballot.
% The example could be modified for a strict Hare Clark scenario, but
% unfortunately I don't have the time to do this. Besides, if you modify
% the scenario to strictly adhere to Hare Clark, the point would likely be
% lost amongst all the extra tallying and transferring that would have to
% occur.
The program was tested separately for its ability to handle large numbers
of ballots.
The tests ranged from 250 thousand votes with 10 candidates to 15 million
votes with 40 candidates.
% The time taken to count these examples is
% plotted in Figure \ref{fig:times} and the memory used is plotted in
% \ref{fig:memory}.\footnote{The values plotted in Figure
% \ref{fig:memory} were obtained by
% measuring the maximum resident size of the PolyML process, which was used to generate
% each example as well as count it. The process of generating the examples
% may have consumed more memory than counting them, so the values plotted give an
% upper bound on the memory usage only.}
Note that every example took less than 80 seconds to count, and consumed
less than 10 GiB of memory.
% \begin{figure}
% \input{times.tex}
% \caption{The time taken to count elections of varying size.}
% \label{fig:times}
% \end{figure}
% \begin{figure}
% \input{memory.tex}
% \caption{The memory usage of the counting program for elections of varying size.
% Note these values are upper bounds only.}
% \label{fig:memory}
% \end{figure}
There are 5 electorates in Tasmania used to elect the House of
Assembly using Hare-Clark, and these each have approximately 72
thousand enrolled voters (as at September 2013)~\cite{tec2013}. Our
implementation is more than adequately equipped to handle counts of
this size. The largest electorate used in any PR election in
Australia is New South Wales (NSW), with an enrolment of just under 5
million voters (as at August 2014)~\cite{nswec2014}. Once again, our
implementation is well able to handle counts of this size.
An initial analysis shows that our SML code has computational
complexity O(num\_candidates * num\_candidates * num\_votes), possibly
worse. We are confident that we can remove at least one of these
occurrences of num\_candidates by using SML arrays, and setting up a
HOL4 theory formalising the appropriate extra correctness properties.
An alternate view is that the verified code only has to be run once,
and it doesn't matter if it takes a week to run, even if the faster
unverified code has already produced a result which has been announced.
We are currently investigating whether it can handle hundreds of
candidates as occurred in the 2015 NSW State Election.
Incidentally, being functional, and moving bits of data all over the place, it depends crucially on real memory.
% \section{Discussion}
% As shown in Section~\ref{sec:largetests}, the implementation is efficient
% enough to handle very large real-world electorate sizes.
% Nevertheless, there are some issues that need to be discussed which
% have a bearing on the worth of the process as a whole.
% Producing the \spechol{} before the implementation was aimed at
% ensuring that \spechol{} remained untainted by errors in the
% implementation. Contrary to this goal, the specification has become
% highly coupled with the implementation. As mentioned in
% Section~\ref{sec:assumptions}, some assumptions about the
% implementation had to be made in order to have something concrete to
% reason about in the \spechol. This unfortunately resulted in the
% \spechol{} becoming dependent on the internal structure of the
% implementation.
% For example, the clauses of the
% \spechol regularly make reference to the way in which the representation
% of a continuing candidate changes under certain circumstances. If the structure
% of this
% representation must be changed in the implementation for practical reasons,
% the change must be carried through to the \spechol as well.
% Even if the implementation and \spechol are produced by separate parties,
% the parties would need to agree on the implementation's structure, potentially
% carrying bugs across the \spechol-\imphol gap.
% Regardless of the order in which the implementation and specification
% are produced, they must necessarily be coupled in this way. This is
% ultimately due to the procedural nature of the legislation (as
% mentioned in Section~\ref{sec:leginlog}). The legislation specifies
% \emph{how} to ascertain the result of an election, not \emph{what} the
% result should be. In other words, the legislation specifies what
% should be going on inside the implementation, not what results the
% implementation should produce. This is what forces the \spechol{} to
% make statements about the internal functioning of the counting
% program, producing the dependency.
% One potential way of sidestepping this issue is to commission a third
% party to produce their own independent version of the implementation.
% Assuming both implementations are correct, it should be possible to
% prove their equivalence. Thus the final implementation would be
% entirely separated from the form and structure shared between
% \spechol{} and \imphol.\footnote{Note that the second implementation
% would also need to be restricted to the intersection between HOL4's
% and SML's feature sets.} If the two implementations turn out to be
% structurally and algorithmically different, the proof of equivalence
% may be quite difficult but remains theoretically achievable.
% See Figure \ref{fig:postlargeproc}
% for a diagram showing the verification process with the proposed extra implementation
% included.
% \begin{figure}
% \begin{center}
% \begin{tikzpicture}[node distance = 10em, auto]
% % Components
% \node [component] (impv2) {IMPv2};
% \node [component, anchor=south, shift={(0,2.5)}] (impholv2) at (impv2.north) {\impholv2};
% \node [component, anchor=west, shift={(2.5,0)}] (imphol) at (impholv2.east) {\imphol};
% \node [component, anchor=west, shift={(2.5,0)}] (spec) at (imphol.east) {\spechol};
% \node [component, anchor=north, shift={(0,-2.5)}] (leg) at (spec.south) {Legislation};
% \path [draw] (imp) edge [<->,dotted] (leg);
% \path [draw] (impholv2) edge [-latex] (impv2);
% \path [draw] (imphol) edge [latex-latex] (spec);
% \path [draw] (leg) edge [->,dotted] (spec);
% \path [draw] (impholv2) edge [latex-latex] (imphol);
% % HOL4 box
% \node [shift={(-1,-1)}] (botleft) at (impholv2.south west) {};
% \node [shift={(1,-1)}] (botright) at (spec.south east) {};
% \node [shift={(-1,1)}] (topleft) at (impholv2.north west) {};
% \node [anchor=north east,shift={(1,1)}] (topright) at (spec.north east) {HOL4};
% \path [draw] (topright.north east) edge [dashed] (topleft.center) edge [dashed] (botright.center);
% \path [draw] (botleft.center) edge [dashed] (topleft.center) edge [dashed] (botright.center);
% \end{tikzpicture}
% \end{center}
% \normalsize
% \caption{Illustration of the final proposed verification process. The link between
% the legislation is dotted to indicate its tenuousness.}
% \label{fig:postlargeproc}
% \end{figure}
% One final issue needs to be discussed, and that is the complexity of
% the specification that has been produced. It is not clear that the
% specification actually meets the legislation. There is also no
% rigorous method of verifying that it does. In fact, it is likely
% harder for the average computer scientist to confirm that \spechol{}
% is faithful, than it would be for them to confirm that the
% implementation itself is faithful. This is partly due to the coupling
% between the implementation and specification mentioned above.
% The reader of \spechol{} must have a reasonable understanding of how
% the implementation works in order to have any hope of understanding
% whether the statements in \spechol{} actually represent what the
% legislation is trying to say. To put it bluntly, we may have simply
% replaced the legislation-implementation link (the link our process is
% intended to verify) with a legislation-specification link that is
% harder to follow. This is the single issue that is most likely to
% derail our approach's viability, and prevent it from being applied to
% real world PR systems: the translation step from legislation to
% specification is simply too loose and ill-defined.
% One way to avoid this issue is to produce more rigorous legislation
% that is more amenable to representation in HOL4's higher order logic.
% The legislation could be derived from a mathematical representation of
% the proposed electoral system, or the mathematical representation
% could be derived from custom legislation (produced with a strictly
% rigorous subset of the English language). In either case,
% legislatorial change would be necessary before any program produced in
% this way could be used for real elections.
%\section{JED to change}
% symbols to change ∃ ∧ ∀ ⇒ ∪
% :.,$s/∀/!/g
% :.,$s/∃/?/g
% :.,$s/⇒/==>/g
% :.,$s/∪/UNION/g
% :.,$s/¬/\~ /g
% :.,$s/λ/\\/g
% :.,$s/⊆/SUBSET/g
% :.,$s/∨/\\\//g
% :.,$s/∧/\/\\/g
\section{Proving Termination of Functions and
Properties of the Results of those Functions}
HOL4 requires function definitions to terminate, because the
underlying logic of computable functions requires that all functions
be total. So HOL4 does not actually allows us to state termination as
a formula of higher-order logic: rather the evidence of it is that HOL
accepts the definition of a function.
Once we input a function definition, HOL4 automatically attempts to
generate a proof of termination for it, using in-built strategies
based upon term-rewriting. If HOL4 cannot produce a termination proof
automatically, it outputs the statement of a lemma which would allow
it to complete the proof. If the user can prove the lemma
interactively, then HOL4 completes the proof of termination itself.
Once HOL4 accepts a function as terminating, it outputs,
automatically, an induction principle which can be used to prove an
arbitrary property \texttt{P} of the function. By instantiating this
property in various ways, we can prove interesting properties of the
function as illustrated next.
%\texttt{MERGE}.
% In most cases we use the \verb!typewriter! font accepted by HOL4
% according to the following table:
% \begin{center}
% \begin{tabular}[c]{|l|l|l|l|l|l|l|}
% \hline
% $\forall x y.\ A$
% & $\exists x y.\ A$
% & $\lambda x y.\ A$
% & $\lnot$
% & $\land$
% & $\lor$
% & $\Rightarrow$
% \\\hline
% \texttt{!x y.\ A}
% & \texttt{?x y.\ A}
% & \verb!\x y. A!
% & \verb!~!
% & \verb!/\!
% & \verb!\/!
% & \verb!==>!
% \\
% \hline
% \end{tabular}
% \end{center}
\subsection{Properties of the function \texttt{MERGE}}
\begin{definition}[\texttt{MERGE\_def}] \label{d-MERGE-def}
The function \verb!MERGE! (used to define \verb!MERGE_SORT!) is
\begin{verbatim}
(MERGE R [] right = right)
/\ (MERGE R left [] = left)
/\ (MERGE R (l::ls) (r::rs) = if R l r
then l::(MERGE R ls (r::rs))
else r::(MERGE R (l::ls) rs))
\end{verbatim}
where \verb![]! is the empty list, \verb|x::xs| is a list with head \verb|x| and
tail \verb|xs| and \verb|R| is a function
that returns \verb|true| if its first argument is ``less than'' its second.
\end{definition}
\begin{theorem}
The \texttt{MERGE} function terminates for all inputs
% \marginpar{What is the HOL4 way to express this ?}
\end{theorem}
\begin{proof}
HOL4 accepts this function, and can see for itself that it
terminates because one list argument gets smaller while the other
remains the same, in successive recursive calls.
\end{proof}
HOL4 generates, automatically, an induction principle (lemma) called
\texttt{MERGE\_ind} for proving properties \texttt{P} of the result of the
\texttt{MERGE} function:
\begin{lemma}[\texttt{MERGE\_ind}] \label{t-MERGE-ind}
For all properties \verb|P|,
if the following conditions hold
\begin{enumerate}
\item \verb|P R left right| holds whenever
\verb|left| or \verb|right| is empty
% \marginpar{There is as subtlety in the code in the need for v4 and v5?}
\item \verb|P R (l::ls) (r::rs)| holds whenever
\verb!~ R l r! and \verb|P R (l::ls) rs| hold
\item \verb|P R (l::ls) (r::rs)| holds whenever
\verb!R l r! and \verb|P R ls (r::rs)| hold
\end{enumerate}
then \verb|P v v1 v2| holds for all values of \verb|v|, \verb!v1! and \verb!v2!:
\begin{verbatim}
!P. (!R right. P R [] right) /\ (!R v4 v5. P R (v4::v5) [])
/\ (!R l ls r rs. ~ R l r /\ P R (l::ls) rs ==> P R (l::ls) (r::rs))
/\ (!R l ls r rs. R l r /\ P R ls (r::rs) ==> P R (l::ls) (r::rs))
==> !v v1 v2. P v v1 v2
\end{verbatim}
\end{lemma}
Note how HOL4 has reformulated the definition to avoid overlapping cases
where \texttt{MERGE\_ind} has \texttt{v4::v5} instead of \texttt{left}.
% Internally, in processing the definition, HOL4 uses the theorem
% \texttt{MERGE\_ind}. If we instantiate \texttt{P} to ``the definition
% of \texttt{MERGE}, above, terminates\marginpar{But we just said that
% we cannot express ``terminates'' in HOL?} with these arguments" then
% \texttt{MERGE\_ind} says that the definition of \texttt{MERGE} always
% terminates.
As an example of a proof by induction using \texttt{MERGE\_ind},
we to prove that the result of \texttt{MERGE}, viewed as a
set, is the union of the lists \texttt{l} and \texttt{r}, viewed as sets.
% \begin{verbatim}
% set (MERGE c l r) = set l UNION set r
% \end{verbatim}
%We proceed via the following lemma.
% \marginpar{Elide the lemma and turn into prose inside Proof ... }
\begin{theorem}
%For all \texttt{v}, \texttt{v1}, and \texttt{v2},
\begin{verbatim}
!v v1 v2. set (MERGE v v1 v2) = (set v1) UNION (set v2)
\end{verbatim}
\end{theorem}
\begin{proof}
We instantiate \texttt{P} of the theorem \texttt{MERGE\_ind} to
\begin{verbatim}
\c l r. set (MERGE c l r) = set l UNION set r
\end{verbatim}
HOL4 then sets out the framework for a proof by induction, where the
inductive steps and their assumptions match the structure of
\texttt{MERGE\_def} (Definition~\ref{d-MERGE-def}). The essence of
the proof is that each step in the definition of \texttt{MERGE}
preserves the desired property.
\end{proof}
% \begin{verbatim}
% (!R right. set (MERGE R [] right) = set right) /\
% (!R v4 v5. set (MERGE R (v4::v5) []) = v4 INSERT set v5) /\
% (!R l ls r rs.
% (~ R l r ==>
% (set (MERGE R (l::ls) rs) = (l INSERT set ls) UNION set rs)) /\
% (R l r ==>
% (set (MERGE R ls (r::rs)) = set ls UNION (r INSERT set rs))) ==>
% (set (MERGE R (l::ls) (r::rs)) =
% (l INSERT set ls) UNION (r INSERT set rs)))
% \end{verbatim}
\subsection{Termination of \texttt{MERGE\_SORT}}
\begin{definition}[\texttt{MERGE\_SORT\_def}] \label{d-MERGE-SORT-def}
The definition of \verb!MERGE_SORT! is
\begin{verbatim}
(MERGE_SORT R [] = []) /\
(MERGE_SORT R [h] = [h]) /\
(MERGE_SORT R (h::t) =
let middle = (LENGTH (h::t)) DIV 2 in
let left = MERGE_SORT R (TAKE (middle) (h::t)) in
let right = MERGE_SORT R (DROP (middle) (h::t)) in
MERGE R left right)
\end{verbatim}
where:
\begin{description}
\item[\texttt{TAKE n list}] returns a list consisting of the first $n$
members of \texttt{list};
\item[\texttt{DROP n list}] returns a list consisting of all but the
first $n$ members of \texttt{list}.
\end{description}
\end{definition}
Intuitively, \verb!MERGE_SORT! terminates because any recursive call
is applied to a shorter list, though to prove this fact requires some
tedious numerical work to show that \texttt{middle} is shorter than the length
of the original list, in cases where middle is used, thus HOL4 does not
prove this automatically.
%
However, HOL4 does present, automatically, the following condition
which the user must prove:
\begin{quote}
there exists a well-founded relation $<$ such that, if a call to
\texttt{MERGE\_SORT R L} generates a call to \texttt{MERGE\_SORT R'
L'}, then $(R',L') < (R,L)$.
\end{quote}
%
% HOL uses R' for the well-founded relation,\marginpar{Overloading of R'?}
% and uses \texttt{MERGE\_SORT\_tupled\_aux (R, L) = MERGE\_SORT R L}.
% So the goal for the user to prove is
%
% \begin{verbatim}
% ?R'.
% WF R' /\
% (!R v5 v4 h middle left.
% (middle = LENGTH (h::v4::v5) DIV 2) /\
% (left =
% MERGE_SORT_tupled_aux R' (R,TAKE middle (h::v4::v5))) ==>
% R' (R,DROP middle (h::v4::v5)) (R,h::v4::v5)) /\
% !R v5 v4 h middle.
% (middle = LENGTH (h::v4::v5) DIV 2) ==>
% R' (R,TAKE middle (h::v4::v5)) (R,h::v4::v5)
% \end{verbatim}
%
Once that is proved, details omitted, we obtain:
\begin{theorem}
\verb!MERGE_SORT! terminates for all inputs.
\end{theorem}
HOL4 generates, automatically, a correct induction principle
\texttt{MERGE\_SORT\_ind}
for proving an arbitrary property \texttt{P}
about \texttt{MERGE\_SORT}.
%
%the resulting theorem \texttt{MERGE\_SORT\_ind} is
%
% \begin{lemma}[\texttt{MERGE\_SORT\_ind}]
% ~
% \begin{verbatim}
% |- !P. (!R. P R [])
% /\ (!R h. P R [h])
% /\ (!R h v4 v5.
% (!middle left.
% (middle = LENGTH (h::v4::v5) DIV 2)
% /\ (left = MERGE_SORT R (TAKE middle (h::v4::v5)))
% ==> P R (DROP middle (h::v4::v5)))
% /\ (!middle. (middle = LENGTH (h::v4::v5) DIV 2)
% ==> P R (TAKE middle (h::v4::v5)))
% ==> P R (h::v4::v5))
% ==> !v v1. P v v1
% \end{verbatim}
% \end{lemma}
%
Again, if you instantiate P to
``the definition of \texttt{MERGE\_SORT} above, terminates with these arguments"
then the theorem \texttt{MERGE\_SORT\_ind} says that the definition of
\texttt{MERGE\_SORT} terminates in all cases.
If we want to prove that
\begin{verbatim}
!v v1. set (MERGE_SORT v v1) = set v1
\end{verbatim}
we instantiate P in \texttt{MERGE\_SORT\_ind} to
\begin{verbatim}
\c l. set (MERGE_SORT c l) = set l
\end{verbatim}
to get a lemma whose conclusion is
that the property \texttt{set (MERGE\_SORT v v1) = set v1} always holds,
% \begin{verbatim}
% !v v1. set (MERGE_SORT v v1) = set v1
% \end{verbatim}
and whose assumptions essentially say that
each step in the definition of \texttt{MERGE\_SORT} preserves that property.
% \texttt{set (MERGE\_SORT v v1) = set v1}.
\section{Raj has token for what follows this!}
\section{Raj has token for what follows this!}
\subsection{Future states OMITTED FROM FINAL VERSION}
The program involves a counting ``state", which records, in particular,
the candidates who are already elected or excluded, or otherwise ``remaining";
for these last, the parcels of votes which are (currently) to their credit are
recorded. The state also contains the parcels of votes, either arising from
the surplus for an elected candidate, or from an excluded candidate, which are
yet to be distributed.
The function \texttt{NEXT1\_STAGE} returns the next state (1 step)
from a given state.
Then we defined \texttt{FINAL\_STAGE} in terms of \texttt{NEXT1\_STAGE}
\begin{definition}[\texttt{FINAL\_STAGE\_def}]
The function \texttt{FINAL\_STAGE}, which given a state of the count,
returns the final state obtained from the given state
\begin{verbatim}
|- !state.
FINAL_STAGE state =
case STAGE_RESULT state of
NONE => FINAL_STAGE (NEXT1_STAGE state)
| SOME result => result
\end{verbatim}
\end{definition}
\texttt{STAGE\_RESULT state = NONE} means that state does not give the
(finished) election result.
We haven't yet proved the termination of this definition:
we used \texttt{mk\_thm}, which creates a "fake" theorem, without proving it.
This gives an induction theorem:
\begin{lemma}[\texttt{FINAL\_STAGE\_ind}]
\begin{verbatim}
|- !P.
(!state.
((STAGE_RESULT state = NONE) ==> P (NEXT1_STAGE state)) ==>
P state) ==>
!v. P v
\end{verbatim}
\end{lemma}
This theorem is clearly true if and only if repeated calls applying
\texttt{NEXT1\_STAGE} to a state eventually reaches a state where
\texttt{STAGE\_RESULT state}
is not \texttt{NONE}.
As an alternative approach we defined, as an inductively defined relation,
the concept of one state being a future state of another one.
\begin{definition}[\texttt{IS\_FUTURE\_rule}]
A state \texttt{s} is a future state of \texttt{init},
that is, \texttt{IS\_FUTURE init s} is true, if either
\begin{itemize}
\item \texttt{s} = \texttt{init}, or
\item \texttt{s} is the next state of a state \texttt{state}
(\texttt{s} = \texttt{NEXT1\_STAGE state})
which is itself a future state of \texttt{init}
\end{itemize}
\begin{verbatim}
val (IS_FUTURE_rule, IS_FUTURE_ind, IS_FUTURE_cases) = Hol_reln
`(!state. IS_FUTURE init state /\ (STAGE_RESULT state = NONE) ==>
IS_FUTURE init (NEXT1_STAGE state)) /\
(IS_FUTURE init init)` ;
\end{verbatim}
\end{definition}
In this sort of definition, \texttt{IS\_FUTURE init s}
holds whenever repeated application of instances
of the clauses given show it to be so, and not otherwise.
HOL automatically generates a theorem \texttt{IS\_FUTURE\_ind}
\begin{lemma}[\texttt{IS\_FUTURE\_ind}]
\begin{verbatim}
|- !init IS_FUTURE'.
(!state.
IS_FUTURE' state /\ (STAGE_RESULT state = NONE) ==>
IS_FUTURE' (NEXT1_STAGE state)) /\ IS_FUTURE' init ==>
!a0. IS_FUTURE init a0 ==> IS_FUTURE' a0
\end{verbatim}
\end{lemma}
This says that for a given property, if
\begin{itemize}
\item the property is preserved from one state to the next
(\texttt{NEXT1\_STAGE state}),
provided the first state does not have the finalised
election result (\texttt{STAGE\_RESULT state = NONE}),
and
\item the property holds of the initial state
\end{itemize}
then the property holds of all states in the future of the initial state.
In this automatically generated theorem,
the property is named \texttt{IS\_FUTURE'}, which is a variable.
This enables us to deal with sanity checks of properties
(like the distinctness of the remaining candidates) which are preserved from
one state to the next.
The definition of \texttt{IS\_FUTURE}, above,
derives new cases of \texttt{init} and \texttt{state},
such that \texttt{IS\_FUTURE init state} holds, by working forwards from state.
Equally you can work backwards from the future state \texttt{final},
as in the following definition:
\begin{definition}[\texttt{IS\_FUTURE\_alt\_rule}]
A state \texttt{final} is a future state of \texttt{init},
that is, \texttt{IS\_FUTURE init final} is true, if either
\begin{itemize}
\item \texttt{init} = \texttt{final}, or
\item \texttt{final} is a future state of
the next state \texttt{NEXT1\_STAGE init} of \texttt{init}
\end{itemize}
\end{definition}
\begin{verbatim}
val (IS_FUTURE_alt_rule, IS_FUTURE_alt_ind, IS_FUTURE_alt_cases) = Hol_reln
`(IS_FUTURE_alt (NEXT1_STAGE init) final /\
(STAGE_RESULT init = NONE) ==> IS_FUTURE_alt init final) /\
(IS_FUTURE_alt final final)` ;
\end{verbatim}
This gives a different definition, and, importantly, a different induction
theorem, which may or may not be easier to use, depending on exactly what it is
used for.
First we need to prove the equivalence of these two definitions.
\begin{lemma}
\begin{enumerate}
\item \texttt{IS\_FUTURE} obeys the introduction rule for
\texttt{IS\_FUTURE\_alt}
\begin{verbatim}
|- IS_FUTURE (NEXT1_STAGE s') fst ==>
(STAGE_RESULT s' = NONE) ==>
IS_FUTURE s' fst
\end{verbatim}
\item \texttt{IS\_FUTURE\_alt} obeys the introduction rule for
\texttt{IS\_FUTURE}
\begin{verbatim}
|- IS_FUTURE_alt init fst ==>
(STAGE_RESULT fst = NONE) ==>
IS_FUTURE_alt init (NEXT1_STAGE fst)
\end{verbatim}
\item \texttt{IS\_FUTURE\_alt} is equivalent to \texttt{IS\_FUTURE}
\end{enumerate}
\end{lemma}
\begin{proof}
\begin{enumerate}
\item proved by induction on \texttt{IS\_FUTURE}
\item proved by induction on \texttt{IS\_FUTURE\_alt}
\item proved from the previous parts using further inductions on
both \texttt{IS\_FUTURE} and \texttt{IS\_FUTURE\_alt}
\end{enumerate}
\end{proof}
We had also defined \texttt{ALL\_STAGES},
which gives the set of successive states in the counting process.
\texttt{ALL\_STAGES\_def};
\begin{definition}[\texttt{ALL\_STAGES\_def}]
Given a non-empty list \texttt{state::states'} of state,
\texttt{ALL\_STAGES (state::states')} is the list of states consisting of these
states and all future states from \texttt{state}.
\begin{verbatim}
|- !states' state.
ALL_STAGES (state::states') =
case STAGE_RESULT state of
NONE => ALL_STAGES (NEXT1_STAGE state::state::states')
| SOME v => state::states'
\end{verbatim}
\end{definition}
The argument is a list of states, which should be the list of states reached
so far, and returns the list of these and all subssequent states.
It will be used with a singleton argument \texttt{[init]}, the initial state.
As usual, its definition generates an induction principle
\begin{lemma}[\texttt{ALL\_STAGES\_ind}]
\begin{verbatim}
|- !P.
(!state states'.
((STAGE_RESULT state = NONE) ==>
P (NEXT1_STAGE state::state::states')) ==>
P (state::states')) /\ P [] ==>
!v. P v
\end{verbatim}
\end{lemma}
So we should be able to show that these two ways of characterising future
states starting from a given initial state are equivalent, that is:
\begin{verbatim}
IS\_FUTURE init state = MEM state (ALL\_STAGES [init])
\end{verbatim}
We can prove
\begin{lemma}[\texttt{MEM\_AS\_IF}]
If state \texttt{fst} is a member of the list \texttt{ALL\_STAGES (s::ss)},
then either it is a future state of \texttt{s} or it is in \texttt{ss}
\begin{verbatim}
|- MEM fst (ALL_STAGES (s::ss)) ==> IS_FUTURE_alt s fst \/ MEM fst ss
\end{verbatim}
\end{lemma}
\begin{proof}
This is proved by induction on \texttt{ALL\_STAGES},
ie, using \texttt{ALL\_STAGES\_ind},
where the condition \texttt{P} on \texttt{v} is that if \texttt{v} is non-empty
say \texttt{v} = \texttt{s::ss}, then this equality holds.
Note that this is straightforward using the introduction clauses of
\texttt{IS\_FUTURE\_alt}, \emph{not} those of \texttt{IS\_FUTURE}.
\end{proof}
Then setting \texttt{ss} to be \texttt{[]}, we get \texttt{MEM\_AS1\_IF}
\begin{verbatim}
|- MEM state (ALL_STAGES [init]) ==> IS_FUTURE_alt init state
\end{verbatim}
(but note that we \emph{cannot}
prove \texttt{MEM\_AS1\_IF} by induction directly,
as the inductive step needs to use, and can prove, the stronger condition
\texttt{MEM\_AS\_IF}.
Then we prove
\begin{lemma}[\texttt{IS\_FUTURE\_alt\_in\_AS}]
\begin{verbatim}
|- IS_FUTURE_alt init state ==> !ss. MEM state (ALL_STAGES (init::ss))
\end{verbatim}
\end{lemma}
\begin{proof}
by induction on \texttt{IS\_FUTURE\_alt}
\end{proof}
Again, we only want the case where \texttt{ss} = \texttt{[]}, but
the inductive step needs to use, and can prove, the stronger result
% This actually requires another lemma,
% \texttt{sub\_ALL\_STAGES}
% \begin{verbatim}
% |- set (s::ss) SUBSET set (ALL_STAGES (s::ss))
% \end{verbatim}
% which we also proved using \texttt{ALL\_STAGES\_ind}
%
% These give us the result
% \texttt{IS\_FUTURE\_ALL\_STAGES}
% \begin{verbatim}
% |- IS_FUTURE init state ⇔ MEM state (ALL_STAGES [init])
% \end{verbatim}
% which we get from \texttt{IS\_FUTURE\_alt\_in\_AS}
% and \texttt{IS\_FUTURE\_eqv}
\section{Some Sanity Check Conditions}
\subsection{That the list of candidates remains unchanged}
We showed that the list of elected, excluded and remaining candidates
is unchanged.
This needs to be formulated precisely,
since these lists are changed by moving candidates from one list to another,
and by re-ordering the remaining candidate list
according to the number of votes each candidate has.
One possible way is to turn each list into a set, and to take the union of the
sets, which literally should remain unchanged.
But this only shows the desired property if the lists contain members which are
all distinct.
In fact we want to show that these lists (jointly) contain all distinct
members, as another useful sanity check condition.
However if we use the built-in function \texttt{PERM},
which means that one list is a permutation of the other,
we can achieve both results at once, because HOL supplies the following
theorems:
\begin{lemma}
If lists \texttt{l1} and \texttt{l2} are permutations of each other, then
\begin{itemize}
\item their member sets of the same, and
\item if the members of one are all distinct,
then so are the members of the other
\end{itemize}
\end{lemma}
\begin{verbatim}
|- !l1 l2. PERM l1 l2 ==> (set l1 = set l2)
|- !l1 l2. PERM l1 l2 ==> (ALL_DISTINCT l1 = ALL_DISTINCT l2)
\end{verbatim}
The definition of \texttt{PERM} is provided by HOL,
along with these and numerous other useful lemmas.
So we want to show that at each iteration,
the concatenation of these lists is permuted.
\begin{definition}
\texttt{ALL\_CANDS state} is a list of all the candidates, that is,
the concatenation of lists of elected, excluded and remaining candidates.
\end{definition}
\begin{verbatim}
ALL_CANDS (time,seats,quota,elected,excluded,rem,surps,groups) =
elected ++ excluded ++ MAP FST rem
\end{verbatim}
Then the required result is
\begin{verbatim}
PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)
\end{verbatim}
However we need the following condition to hold:
\begin{definition}
\texttt{rem} (the remaining candidates component of a state)
satisfies \texttt{rem3ne} if each remaining candidate entry
has at least one group of votes.
\end{definition}
This is required by the code for \texttt{EXTRACT\_SURPS}
which gets the surplus votes for an elected candidate,
since the surplus votes are (at a reduced value)
the last parcel of votes credited to that candidate.
That this property holds is clear enough since each candidate
gets an initial parcel of votes,
and then can only accumulate more (until elected or excluded).
\begin{lemma}[\texttt{state\_rem3ne}] \label{l-state-rem3ne}
In each state of a count, the entries for remaining candidates
satisfy \texttt{rem3ne}.
\end{lemma}
\begin{verbatim}
|- !seats cands ballots state.
IS_FUTURE (INIT_STATE seats cands ballots) state ==>
rem3ne (REM_CANDS_VAR state)
\end{verbatim}
Lemma~\ref{l-PERM-elected-rem}
handles the phase of a counting step where
the list of remaining candidates is divided into those elected with a surplus,
those elected with exactly the right number of votes, and those continuing as
``remaining candidates".
This phase is handled by the three functions
\begin{description}
\item[\texttt{EXTRACT\_SURPS}] which returns a pair, of which the first
(\texttt{FST}) component is the remaining candidates after
deleting those elected with a surplus
\item[\texttt{DROP\_EXACT}] which returns the remaining candidates after
deleting those elected with just enough votes (no surplus)
\item[\texttt{EXTRACT\_ELECTED}] which returns the candidates elected
(its argument \texttt{acc} just accumulates previous results)
\end{description}
These functions rely on their input list \texttt{rem} being sorted by number of
votes, so their code need only look along the list from the start until
reaching the first candidate not satisfying the relevant criterion.
\begin{lemma}[\texttt{PERM\_elected\_rem}] \label{l-PERM-elected-rem}
If a list \texttt{rem} of remaining candidates is sorted by total votes,
then the list in it of elected candidate (extracted by
\texttt{EXTRACT\_ELECTED}, concatenated with the
list of those not elected, as determined by
\texttt{EXTRACT\_SURPS} and then \texttt{DROP\_EXACT},
is a permutation of the list \texttt{rem}.
\end{lemma}
\begin{verbatim}
|- !rem acc.
rem3ne rem ==>
SORTED (COMBINE TOTAL_COUNT $>=) rem ==>
PERM
(EXTRACT_ELECTED quota rem acc ++
MAP FST (DROP_EXACT quota (FST (EXTRACT_SURPS quota rem []))))
(acc ++ MAP FST rem)
\end{verbatim}
Note that entries for remaining candidates consist of the
candidate, total votes, and groups of votes,
whereas \texttt{EXTRACT\_ELECTED} returns a list of just candidates.
% (and, in other code examples, \texttt{elected} and \texttt{excluded})
Hence the occurrences of \texttt{MAP FST} in the code above.
Also, the \texttt{EXTRACT\_ELECTED} is tail-recursive, with accumulator
\texttt{acc} (not mentioned in the statement of the lemma).
Other parts of a counting step have relevant lemmas:
for example, since the remaining candidates are sorted by total votes,
we need the following:
\begin{lemma}[\texttt{MERGE\_SORT\_PERM}]
If a list is sorted, the result is a permutation of the original list.
\end{lemma}
\begin{verbatim}
|- !v v1. PERM (MERGE_SORT v v1) v1
\end{verbatim}
At several stages in the proof, to cope with the rearrangement of candidates
in the code (especially as some functions were written to be tail-recursive),
we needed lemmas such as:
\begin{verbatim}
|- PERM (ee ++ el ++ nl::ex ++ mfde) (el ++ ex ++ mfr) ⇔
PERM (ee ++ nl::mfde) mfr
\end{verbatim}
Finally this gave us the theorem \texttt{PERM\_NEXT1\_CANDS},
that candidates are preserved:
\begin{theorem}
If $s$ and $s'$ are two consecutive states in the count,
\texttt{ALL\_CANDS} $s$ is a permutation of \texttt{ALL\_CANDS} $s'$.
\end{theorem}
\begin{verbatim}
|- rem3ne rem ==>
(state = (time,seats,quota,elected,excluded,rem,surps,groups)) ==>
PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)
\end{verbatim}
Together with Lemma~\ref{l-state-rem3ne}, this gives us that the list of
all candidates is unchanged, up to pernutation, throughout the count.
\section{Difficulties in the proofs}
\subsection{Conditions which need to be proved}
These are examples of conditions which seem obvious, and are assumed by the
code (and, indeed, by the legislation), but proving that they hold requires
several steps of reasoning and tracing through the code.
Their proof is a lower priority since whenever they are not satisfied,
the code as written will not complete without error,
but for completeness, we intend to prove all such conditions.
\subsubsection{Termination of the main algorithm}
This relies on the fact that in each iteration of the algorithm
(ie, in each call to \texttt{NEXT1\_STAGE}),
the state gets closer to the termination condition, which is that
the number of elected and remaining candidates is less than or equal
to the number of candidates to be elected.
This relies on the fact that, at each iteration
\begin{itemize}
\item group of votes is distributed, or
\item a remaining candidate is excluded
\end{itemize}
So we need to look at when new groups of votes are created,
ready to be distributed.
This occurs when
\begin{itemize}
\item a remaining candidate is elected
\item a remaining candidate is excluded
\end{itemize}
So this requires constructing a measure on the state, involving
\begin{itemize}
\item the number of elected or ``remaining" candidates
\item the number of remaining candidates
\item the number of groups of votes remaining to be distributed
\end{itemize}
and showing that this measure decreases at each iteration.
\subsubsection{The condition that there be ``remaining'' candidates}
Since the counting program chooses the lowest ranking candidate to be
eliminated, this code depends on the fact that the list of ``remaining''
candidates be non-empty.
Since the code finishes the count whenever the number
of elected and remaining candidates is less than or equal to the number of
candidates to be elected, the problem can arise only when too many candidates
get elected. The mathematics defining the quota for election makes this
impossible, but to prove it requires that the total number of votes represented
by the state does not increase.
\subsubsection{That transfer values do not have denominator zero}
The code relies on the fact that the denominator of a transfer value
(which is a fraction) is not zero.
This in turn relies on the fact that the final parcel of votes which elects
a candidate is non-empty and that a candidate can get only one new parcel of
votes in each iteration of the algorithm (ie, in each call to
\texttt{NEXT1\_STAGE}).
\subsection{Errors discovered}\label{sec:errors-in-spec}
We found errors where conditions (expressed in HOL),
which we set out to prove, were in fact not provable.
We have not yet found cases where this was due to errors in the code
(that is, the specification, in HOL, of the program's behaviour).
Rather, the errors were all in the expression of the conditions
which were to be proved.
We surmise that this is because the ``program'' specification, in HOL,
was translated into Standard ML, and tested.
No doubt there were errors which were found in the course of this testing.
On the other hand, the correctness conditions were not tested in this way.
The errors found were as follows.
\subsubsection{taking the $n$'th member of a shorter list}
The condition that the list of remaining candidates are distinct:
\begin{verbatim}
!entry1 entry2 x y. (EL x (REM_CANDS_VAR state) = entry1)
/\ (EL y (REM_CANDS_VAR state) = entry2)
==> ((FST entry1 = FST entry2) ==> (x = y))
\end{verbatim}
\texttt{REM\_CANDS\_VAR} gives the list of entries for the remaining candidates,
where an entry consists of, firstly, the candidate name, and then
the votes currently credited to that candidate.
We want all the candidate names to be distinct.
This condition is erroneous in that \texttt{EL n list},
which returns the $n$'th member of \texttt{list}, is undefined
where \texttt{list} is too short to have an $n$'th member.
In fact we reformulated the condition to use the predicate
\texttt{ALL\_DISTINCT}, provided in HOL, which has the supplied theorem
\texttt{EL\_ALL\_DISTINCT\_EL\_EQ}, which illustrates the need for a condition
that the index is within the length of the list.
\begin{verbatim}
|- !l. ALL_DISTINCT l =
!n1 n2. n1 < LENGTH l /\ n2 < LENGTH l ==>
((EL n1 l = EL n2 l) = (n1 = n2))
\end{verbatim}
\subsubsection{need to assume candidates distinct initially}
To prove that the list of remaining candidates are distinct at any stage,
it is necessary to assume that the list of candidates provided initially is
distinct. This assumption was omitted.
\subsubsection{characterization of states of the count}
Although we describe the functions \texttt{ALL\_STAGES} and
\texttt{IS\_FUTURE} above, the specification of the program does not use these.
They are used only to prove things \emph{about} the program.
Initially the notion of a state which occurs during the count was given by
\texttt{(COUNT\_HCT seats cands ballots = FINAL\_STAGE state)}
where \texttt{COUNT\_HCT} expresses the entire process: it calculates the
initial state, and then applies \texttt{FINAL\_STAGE}, described above.
A state satisfies this condition if, by starting at that state, and completing
the count, you reach the same final state as the actual count.
While this condition is clearly satisfied by states in the actual count,
it is not clear that it cannot be satisfied by states which are not
states of the actual count.
So we replaced this condition by
\texttt{IS\_FUTURE (INIT\_STATE seats cands ballots) state}
\bibliographystyle{abbrv}
\bibliography{dawson-gore-meumann-voteid2015}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "dawson-gore-meumann-voteid2015"
%%% End: