Machine-checked Reasoning About Complex Voting Schemes Using Higher-order Logic

No Author Given

No Institute Given

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 IMP. 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 → SPECHOL.

1 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 votecounting 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 [?]. 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 [?]. 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, transportedwithout-tampering and that all electronic ballots are included in the final tally 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 methods for extending them to STV are in their infancy [?].

We describe a methodology for formally reasoning about complex vote-counting schemes. Specifically, we describe how we first formally encoded the Englishlanguage 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 IMP 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 → SPECHOL.

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 Prêt à Voter. 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).

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.

2 Hare-Clark Single Transferable Voting

Farrell and McAllister [?] provide a definitive study of preferential electoral systems in Australia. Wen [?] 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.

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. 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.

The Hare-Clark Scheme. 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 [?,?]. A slightly different version has also been used to elect members of the Legislative Assembly in the Australian Capital Territory (ACT) since 1995 [?]. Handcounting 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. We already have a formal specification of Hare-Clark ACT [?], 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.

3 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 [?].

Hill et al [?] 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 [?] 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 [?].

Kiniry et al [?] 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 “this level of coverage (100% statement and condition coverage) does not prove that the system is error-free. … 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” [?].

Cochran conducted a comprehensive study of verifying STV counting using light-weight (automatic) methods [?,?] by attempting to formally verify a Java program for the Irish proportional representation single-transferable voting scheme against its English natural language description using the ESC/Java tool. Most proofs were completed automatically, but in some, “ESC/Java2 could neither verify the loop invariants nor the post-condition” [?, p 46]. 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 “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.” [?, page 63].

Recent attempts by Beckert et al [?] show that even state-of-the-art lightweight 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 (higherorder) logic is apparent in the work of DeYoung and Schurmann [?]. 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.

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 et al [?] 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:

Formal specifications: the specification is encoded as a formula of higherorder 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;

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;

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 → SPECHOL which can be exported and checked by others using their own favourite theorem prover.

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;

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 12.2. 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 [?], the CakeML [?] 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!

4 Existing e-Voting and e-Counting Systems

Many e-voting systems provide trustworthiness whilst maintaining ballot anonymity using cryptographic zero-knowledge proofs: Scantegrity, PunchScan and Prêt à 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 [?] 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êt à Voter caled vVote [?]. 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. 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 [?]. In Germany [?], 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 et al found “no hot exploits” but found “some vulnerabilities and bad software engineering practices” and concluded that it was a “fragile system with a large trusted computing base” [?]. Three bugs have been found in this software by members of the Logic and Computation Group at the Australian National University [?]. 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. The approach discussed next is aimed at producing fully formally verified vote-counting programs that can handle the complexity of PR voting systems.

5 Higher-order Logic and the HOL4 Theorem Prover

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 [?]. 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.

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 (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:

SPECHOL: a hand-encoding of the English-language description of the vote-counting

process into higher-order logic; IMP: an implementation in SML of a vote-counting program based upon SPECHOL; IMPHOL: a hand-translation of IMP into higher-order logic; 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.

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 [?]). 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.

The specification (in this case the translation of the legislation into HOL4’s logic) is performed 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.

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. Programming directly in HOL4’s formal logic also helps to ensure that the nonfunctional features of SML are avoided.

The astute reader may notice there are certain gaps in this methodology that cannot be filled: there is no proof that the SML program (IMP) is the same as the HOL4 translation (IMPHOL), and there is no proof that the HOL4 encoding of the legislation (SPECHOL) is logically the same as the legislation itself.

6 Translating Legislation into Higher-order Logic

The following list of HOL4 syntax may be helpful.

HOL4 x y. A   T     F   ~t t_{1} \/ t_{2} t_{1} /\ t_{2} t_{1} ==> t_{2} t_{1} = t_{2} !x.t ?x.t
Logic λxy. A verum falsum ¬t t_{1} ∨ t_{2} t_{1} ∧ t_{2} t_{1} → t_{2} t_{1} = t_{2} ∀x.t ∃x.t

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 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 “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 are three different ways of interpreting which candidate should be excluded:

(a) the candidate who has the lowest count at the last count or transfer at which all of the candidates concerned had pairwise unequal counts;

(b) 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;

(c) 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.).

Option (a) 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 (b) causes deferral to counts more recent than option (a), 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 (c) 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 (c).

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 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.

6.1 Assumptions About the Implementation

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.

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 COUNT_HCT, so we have the following function definition to work with:

COUNT_HCT: num -> 'a list -> 'a list list -> 'a list

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.

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 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:

(time, seats, quota, elected, excluded, rem, surps, groups)

where…

time is a parameter representing temporality (the level of recursion). It increases

by one with each recursion. seats is the number of seats to be filled. Note that this value is not intended

to change over the course of the count. 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. 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. excluded is the list of excluded candidates. Excluding a candidate is interpreted

as placing a candidate in this list. 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 tuple

   (name, total, transfers) where:

name is the identifier of the candidate (this can be any equality type).

total is the total value of votes assigned to the candidate.

transfers is a list of transfers assigned to the candidate and is of the form

      (value, ballots, clause) where

value is the transfer value associated with the transfer and is a tuple of

          the form (numerator, denominator).

ballots is the list of ballots associated with the transfer.

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.

surps is a list of pending transfers of surplus votes from elected candidate. groups is a list of transfers pending from the exclusion of a candidate. Each

member of both surps and groups is of the form (value, ballots) where value is the transfer value of the ballots and is a tuple of the form (numerator,

      denominator).

ballots is the list of ballots awaiting transfer.

Assuming the function performing the recursion on the state tuple is called FINAL_STAGE, we have the following function type definition:

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

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 6.4. An example function and statements that are used by the clauses are given in Section 6.2 below. Sanity checks are given in section 6.3. 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.

6.2 Example Definitions

The function shown in Listing 1.1 is used to simplify the clauses in Section 6.4. 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.

Listing 1.1: Executable function definitions.

 1 (*  Returns  list of  ballots  whose  first  preference  is cand *)
 2 val  FIRSTS_FOR_DEF = Define  `
 3  FIRSTS_FOR  cand  ballots =
 4  FILTER  (($= cand) o HD) ballots`;
 5 (* Sums  the  number  of  ballots  with a first  preference  for
 6  each of the  running  candidates.   This is  needed  simply
 7  because  the  legislation  specifies  that  this is how  the
 8  quota  should  be  calculated. *)
 9 val  SUM_FIRSTS_DEF = Define  `
10  (SUM_FIRSTS  []        ballots = 0)
11 /\ (SUM_FIRSTS (c::cs) ballots =
12  LENGTH (FIRSTS_FOR c ballots)
13  + SUM_FIRSTS  cs  ballots)`;

6.3 Sanity Checks

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 below.

Listing 1.2 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.

Listing 1.2: Candidates cannot be introduced partway through the count.

 1 !seats  cands  ballots  state  state'.
 2  (COUNT_HCT  seats  cands  ballots = FINAL_STAGE  state)
 3  /\ (COUNT_HCT  seats  cands  ballots = FINAL_STAGE  state')
 4  /\  TIME_VAR  state' > TIME_VAR  state
 5  ==> !cand. IS_REM_CAND  state' cand
 6  ==>  IS_REM_CAND  state  cand

6.4 Example of a Clause in Higher-order Logic

Each of the 14 clauses in the Tasmanian Hare-Clark legislation was thus handtranslated into higher-order logic. We give just one example below.

Clause 2: First preference votes to be counted

The number of first preferences recorded for each candidate, on ballot papers which are not informal ballot papers, is to be counted.

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 1.3 below.

Listing 1.3: Clause 2

 1 !seats  cands  ballots  cand  rem_cands  quota.
 2 (COUNT_HCT  seats  cands  ballots =
 3  FINAL_STAGE (t0,seats,quota,[],[],rem_cands,[]))
 4 /\ (MEM  cand  cands =
 5  MEM (cand,
 6  LENGTH (FIRSTS_FOR  cand  ballots),
 7  [((1,1),  FIRSTS_FOR  cand  ballots, clause2)])
 8  rem_cands)

Note that the “count” of the first preferences is given by LENGTH (FIRSTS FOR cand ballots). The function LENGTH is a predefined function in HOL4, and FIRSTS FOR is defined in Listing 1.1.

7 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).

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 (c) on page 8). 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.

7.1 Testing the SML Implementation for Efficiency

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 (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.^{1} 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: [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:

TAS = (surplus / total votes in prev. transfer) = 2 / 4 = 1/2 ACT = (surplus / total unexhaust. votes in prev. transfer) = 2 / 2 = 1

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:

TAS: 1 for C, 1 for B so B eliminated as C had more votes in previous round; ACT: 1 for C, 2 for B so C eliminated.

The programs confirmed that this example leads to a different results.

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. Note that every example took less than 80 seconds to count, and consumed less than 10 GiB of memory.

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) [?]. 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) [?]. 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

1 If a large number of ballots are generated naïvely, 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.

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.

8 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 termrewriting. 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 P of the function. By instantiating this property in various ways, we can prove interesting properties of the function as illustrated next.

8.1 Properties of the function MERGE

Definition 1 (MERGE def). The function MERGE (used to define MERGE_SORT) is

    (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))

where [] is the empty list, x::xs is a list with head x and tail xs and R is a function that returns true if its first argument is “less than” its second.

Theorem 1. The MERGE function terminates for all inputs

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.

HOL4 generates, automatically, an induction principle (lemma) called MERGE ind for proving properties P of the result of the MERGE function:

Lemma 1 (MERGE ind). For all properties P, if the following conditions hold

1. P R left right holds whenever left or right is empty

 2. P R (l::ls) (r::rs) holds whenever ~ R l r and P R (l::ls) rs hold
 3. P R (l::ls) (r::rs) holds whenever R l r and P R ls (r::rs) hold

then P v v1 v2 holds for all values of v, v1 and v2:

 !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

Note how HOL4 has reformulated the definition to avoid overlapping cases

where MERGE ind has v4::v5 instead of left.

As an example of a proof by induction using MERGE ind, we to prove that the result of MERGE, viewed as a set, is the union of the lists l and r, viewed as sets.

Theorem 2. !v v1 v2. set (MERGE v v1 v2) = (set v1) UNION (set v2)

Proof. We instantiate P of the theorem MERGE ind to

         \c l r. set (MERGE c l r) = set l UNION set r

HOL4 then sets out the framework for a proof by induction, where the inductive steps and their assumptions match the structure of MERGE def (Definition 1). The essence of the proof is that each step in the definition of MERGE preserves the desired property.

8.2 Termination of MERGE SORT

Definition 2 (MERGE SORT def). The definition of MERGE_SORT is

(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)

where:

TAKE n list returns a list consisting of the first n members of list; DROP n list returns a list consisting of all but the first n members of list.

Intuitively, 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 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: there exists a well-founded relation < such that, if a call to MERGE SORT R L generates a call to MERGE SORT R' L', then (R′, L′) < (R, L).

Once that is proved, details omitted, we obtain:

Theorem 3. MERGE_SORT terminates for all inputs.

HOL4 generates, automatically, a correct induction principle MERGE SORT ind for proving an arbitrary property P about MERGE SORT. Again, if you instantiate P to “the definition of MERGE SORT above, terminates with these arguments” then the theorem MERGE SORT ind says that the definition of MERGE SORT terminates in all cases.

If we want to prove that

!v v1. set (MERGE_SORT v v1) = set v1

we instantiate P in MERGE SORT ind to

\c l. set (MERGE_SORT c l) = set l

to get a lemma whose conclusion is that the property set (MERGE SORT v v1) = set v1 always holds, and whose assumptions essentially say that each step in the definition of MERGE SORT preserves that property.

9 Raj has token for what follows this!

10 Raj has token for what follows this!

10.1 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 NEXT1 STAGE returns the next state (1 step) from a given state. Then we defined FINAL STAGE in terms of NEXT1 STAGE

Definition 3 (FINAL STAGE def). The function FINAL STAGE, which given a state of the count, returns the final state obtained from the given state

   |- !state.
     FINAL_STAGE state =
     case STAGE_RESULT state of
       NONE => FINAL_STAGE (NEXT1_STAGE state)
     | SOME result => result

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 mk thm, which creates a ”fake” theorem, without proving it.

This gives an induction theorem:

Lemma 2 (FINAL STAGE ind).
   |- !P.
     (!state.
        ((STAGE_RESULT state = NONE) ==> P (NEXT1_STAGE state)) ==>
        P state) ==>
     !v. P v

This theorem is clearly true if and only if repeated calls applying NEXT1 STAGE to a state eventually reaches a state where STAGE RESULT state is not NONE.

As an alternative approach we defined, as an inductively defined relation, the concept of one state being a future state of another one.

Definition 4 (IS FUTURE rule). A state s is a future state of init, that is, IS FUTURE init s is true, if either

 – s = init, or

– s is the next state of a state state (s = NEXT1 STAGE state) which is itself a future state of init

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)` ;

In this sort of definition, 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 IS FUTURE ind

Lemma 3 (IS FUTURE ind).
    |- !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

This says that for a given property, if

– the property is preserved from one state to the next (NEXT1 STAGE state), provided the first state does not have the finalised election result (STAGE RESULT

   state = NONE), and

– the property holds of the initial state then the property holds of all states in the future of the initial state.

In this automatically generated theorem, the property is named 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 IS FUTURE, above, derives new cases of init and state, such that IS FUTURE init state holds, by working forwards from state. Equally you can work backwards from the future state final, as in the following definition:

Definition 5 (IS FUTURE alt rule). A state final is a future state of init, that is, IS FUTURE init final is true, if either

 – init = final, or

– final is a future state of the next state NEXT1 STAGE init of init

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)` ;

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.

Lemma 4. 1. IS FUTURE obeys the introduction rule for IS FUTURE alt

      |- IS_FUTURE (NEXT1_STAGE s') fst ==>
      (STAGE_RESULT s' = NONE) ==>
      IS_FUTURE s' fst

2. IS FUTURE alt obeys the introduction rule for IS FUTURE

   |- IS_FUTURE_alt init fst ==>
      (STAGE_RESULT fst = NONE) ==>
         IS_FUTURE_alt init (NEXT1_STAGE fst)
 3. IS FUTURE alt is equivalent to IS FUTURE

Proof. 1. proved by induction on IS FUTURE

2. proved by induction on IS FUTURE alt

3. proved from the previous parts using further inductions on both IS FUTURE

   and IS FUTURE alt

We had also defined ALL STAGES, which gives the set of successive states in the counting process. ALL STAGES def; Definition 6 (ALL STAGES def). Given a non-empty list state::states' of state, ALL STAGES (state::states') is the list of states consisting of these states and all future states from state.

   |- !states' state.
     ALL_STAGES (state::states') =
     case STAGE_RESULT state of
       NONE => ALL_STAGES (NEXT1_STAGE state::state::states')
     | SOME v => state::states'

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 [init], the initial state.

As usual, its definition generates an induction principle

Lemma 5 (ALL STAGES ind).
   |- !P.
     (!state states'.
        ((STAGE_RESULT state = NONE) ==>
         P (NEXT1_STAGE state::state::states')) ==>
        P (state::states')) /\ P [] ==>
     !v. P v

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:

IS\_FUTURE init state = MEM state (ALL\_STAGES [init])

We can prove

Lemma 6 (MEM AS IF). If state fst is a member of the list ALL STAGES (s::ss), then either it is a future state of s or it is in ss

|- MEM fst (ALL_STAGES (s::ss)) ==> IS_FUTURE_alt s fst \/ MEM fst ss

Proof. This is proved by induction on ALL STAGES, ie, using ALL STAGES ind, where the condition P on v is that if v is non-empty say v = s::ss, then this equality holds. Note that this is straightforward using the introduction clauses

of IS FUTURE alt, not those of IS FUTURE.

Then setting ss to be [], we get MEM AS1 IF

   |- MEM state (ALL_STAGES [init]) ==> IS_FUTURE_alt init state

(but note that we cannot prove MEM AS1 IF by induction directly, as the inductive step needs to use, and can prove, the stronger condition MEM AS IF.

Then we prove

Lemma 7 (IS FUTURE alt in AS).
   |- IS_FUTURE_alt init state ==> !ss. MEM state (ALL_STAGES (init::ss))

Proof. by induction on IS FUTURE alt

Again, we only want the case where ss = [], but the inductive step needs to use, and can prove, the stronger result

11 Some Sanity Check Conditions

11.1 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 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:

Lemma 8. If lists l1 and l2 are permutations of each other, then

– their member sets of the same, and

– if the members of one are all distinct, then so are the members of the other

|- !l1 l2. PERM l1 l2 ==> (set l1 = set l2)
|- !l1 l2. PERM l1 l2 ==> (ALL_DISTINCT l1 =ALL_DISTINCT l2)

The definition of 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.

Definition 7. ALL CANDS state is a list of all the candidates, that is, the concatenation of lists of elected, excluded and remaining candidates.

ALL_CANDS (time,seats,quota,elected,excluded,rem,surps,groups) =
     elected ++ excluded ++ MAP FST rem

Then the required result is

   PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)

However we need the following condition to hold:

Definition 8. rem (the remaining candidates component of a state) satisfies rem3ne if each remaining candidate entry has at least one group of votes.

This is required by the code for 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).

Lemma 9 (state rem3ne). In each state of a count, the entries for remaining candidates satisfy rem3ne.

   |- !seats cands ballots state.
        IS_FUTURE (INIT_STATE seats cands ballots) state ==>
     rem3ne (REM_CANDS_VAR state)

Lemma 10 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

EXTRACT SURPS which returns a pair, of which the first (FST) component is the

remaining candidates after deleting those elected with a surplus DROP EXACT which returns the remaining candidates after deleting those elected

with just enough votes (no surplus) EXTRACT ELECTED which returns the candidates elected (its argument acc just

accumulates previous results)

These functions rely on their input list 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.

Lemma 10 (PERM elected rem). If a list rem of remaining candidates is sorted by total votes, then the list in it of elected candidate (extracted by EXTRACT ELECTED, concatenated with the list of those not elected, as determined by EXTRACT SURPS and then DROP EXACT, is a permutation of the list rem.

   |- !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)

Note that entries for remaining candidates consist of the candidate, total votes, and groups of votes, whereas EXTRACT ELECTED returns a list of just candidates. Hence the occurrences of MAP FST in the code above. Also, the EXTRACT ELECTED is tail-recursive, with accumulator 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:

Lemma 11 (MERGE SORT PERM). If a list is sorted, the result is a permutation of the original list.

   |- !v v1. PERM (MERGE_SORT v v1) v1

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:

   |- PERM (ee ++ el ++ nl::ex ++ mfde) (el ++ ex ++ mfr)
      PERM (ee ++ nl::mfde) mfr

Finally this gave us the theorem PERM NEXT1 CANDS, that candidates are preserved:

Theorem 4. If s and s′ are two consecutive states in the count, ALL CANDS s is a permutation of ALL CANDS s′.

   |- rem3ne rem ==>
   (state = (time,seats,quota,elected,excluded,rem,surps,groups)) ==>
   PERM (ALL_CANDS (NEXT1_STAGE state)) (ALL_CANDS state)

Together with Lemma 9, this gives us that the list of all candidates is unchanged, up to pernutation, throughout the count.

12 Difficulties in the proofs

12.1 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.

Termination of the main algorithm This relies on the fact that in each iteration of the algorithm (ie, in each call to 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

– group of votes is distributed, or

– a remaining candidate is excluded

So we need to look at when new groups of votes are created, ready to be distributed. This occurs when

– a remaining candidate is elected

– a remaining candidate is excluded

So this requires constructing a measure on the state, involving

– the number of elected or “remaining” candidates

– the number of remaining candidates

– the number of groups of votes remaining to be distributed

and showing that this measure decreases at each iteration.

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.

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 NEXT1 STAGE).

12.2 Errors discovered

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.

taking the n’th member of a shorter list The condition that the list of remaining candidates are distinct:

    !entry1 entry2 x y. (EL x (REM_CANDS_VAR state) = entry1)
              /\ (EL y (REM_CANDS_VAR state) = entry2)
          ==> ((FST entry1 = FST entry2) ==> (x = y))

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 EL n list, which returns the n’th member of list, is undefined where list is too short to have an n’th member.

In fact we reformulated the condition to use the predicate ALL DISTINCT, provided in HOL, which has the supplied theorem EL ALL DISTINCT EL EQ, which illustrates the need for a condition that the index is within the length of the list.

    |- !l.  ALL_DISTINCT l =
      !n1 n2.  n1 < LENGTH l /\ n2 < LENGTH l ==>
        ((EL n1 l = EL n2 l) = (n1 = n2))

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.

characterization of states of the count Although we describe the functions ALL STAGES and IS FUTURE above, the specification of the program does not use these. They are used only to prove things about the program.

Initially the notion of a state which occurs during the count was given by

   (COUNT HCT seats cands ballots = FINAL STAGE state)

where COUNT HCT expresses the entire process: it calculates the initial state, and then applies 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

   IS FUTURE (INIT STATE seats cands ballots) state