		Search-engine friendly clone of the ACL2 documentation.

Elections

Tally-leader-votes

Count the `yes' and `no' votes for a leader.

Signature
(tally-leader-votes leader voters) → (mv yes-count no-count)
Arguments: leader — Guard (addressp leader).; voters — Guard (certificate-setp voters).
Returns: yes-count — Type (natp yes-count).; no-count — Type (natp no-count).

The leader input to this function is the address of the leader at some even round, as returned by leader-at-round. The voters input to this function is the set of all the certificates in the DAG who are members of the committee active at the immediately following odd round: these are all the voters for the leader. Note that the active committee may have changed between the even and odd round, if it changed between the two rounds exactly at the lookback distance. This possible change of committee is unproblematic for the purpose of the correctness of the protocol, as we ensure by way of formal proofs.

We go through the voters, and for each voter check whether the given leader authored one of the certificates referenced in the voter certificate, counting `yes' or `no' votes, respectively. We return both counts.

Definitions and Theorems

Function: tally-leader-votes

(defun tally-leader-votes (leader voters)
  (declare (xargs :guard (and (addressp leader)
                              (certificate-setp voters))))
  (let ((__function__ 'tally-leader-votes))
    (declare (ignorable __function__))
    (b* (((when (emptyp voters)) (mv 0 0))
         (voter (head voters))
         ((mv yes-count no-count)
          (tally-leader-votes leader (tail voters))))
      (if (in leader (certificate->previous voter))
          (mv (1+ yes-count) no-count)
        (mv yes-count (1+ no-count))))))

Theorem: natp-of-tally-leader-votes.yes-count

(defthm natp-of-tally-leader-votes.yes-count
  (b* (((mv ?yes-count ?no-count)
        (tally-leader-votes leader voters)))
    (natp yes-count))
  :rule-classes :rewrite)

Theorem: natp-of-tally-leader-votes.no-count

(defthm natp-of-tally-leader-votes.no-count
  (b* (((mv ?yes-count ?no-count)
        (tally-leader-votes leader voters)))
    (natp no-count))
  :rule-classes :rewrite)