		Search-engine friendly clone of the ACL2 documentation.

Elections

Tally-leader-stake-votes

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

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

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 whose authors are members of the committee active at the immediately following odd round: these are all the possible voters for the leader. The commtt input to this function is the active committee at the odd round just after the even round of 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 check whether the leader address is among the refernced previous certificates or not, counting its stake as part of the `yes' or `no' vote stakes. We return both voting stakes.

Definitions and Theorems

Function: tally-leader-stake-votes

(defun tally-leader-stake-votes (leader voters commtt)
 (declare (xargs :guard (and (addressp leader)
                             (certificate-setp voters)
                             (committeep commtt))))
 (declare (xargs :guard (subset (certificate-set->author-set voters)
                                (committee-members commtt))))
 (let ((__function__ 'tally-leader-stake-votes))
  (declare (ignorable __function__))
  (b*
   (((when (or (not (mbt (certificate-setp voters)))
               (emptyp voters)))
     (mv 0 0))
    (voter (head voters))
    (voter-stake (committee-member-stake (certificate->author voter)
                                         commtt))
    ((mv yes-stake-rest no-stake-rest)
     (tally-leader-stake-votes leader (tail voters)
                               commtt)))
   (if (in (address-fix leader)
           (certificate->previous voter))
       (mv (+ voter-stake yes-stake-rest)
           no-stake-rest)
     (mv yes-stake-rest
         (+ voter-stake no-stake-rest))))))

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

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

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

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

Theorem: tally-leader-stake-votes-of-address-fix-leader

(defthm tally-leader-stake-votes-of-address-fix-leader
  (equal (tally-leader-stake-votes (address-fix leader)
                                   voters commtt)
         (tally-leader-stake-votes leader voters commtt)))

Theorem: tally-leader-stake-votes-address-equiv-congruence-on-leader

(defthm tally-leader-stake-votes-address-equiv-congruence-on-leader
 (implies
      (address-equiv leader leader-equiv)
      (equal (tally-leader-stake-votes leader voters commtt)
             (tally-leader-stake-votes leader-equiv voters commtt)))
 :rule-classes :congruence)

Theorem: tally-leader-stake-votes-of-certificate-set-fix-voters

(defthm tally-leader-stake-votes-of-certificate-set-fix-voters
  (equal
       (tally-leader-stake-votes leader (certificate-set-fix voters)
                                 commtt)
       (tally-leader-stake-votes leader voters commtt)))

Theorem: tally-leader-stake-votes-certificate-set-equiv-congruence-on-voters

(defthm
 tally-leader-stake-votes-certificate-set-equiv-congruence-on-voters
 (implies
      (certificate-set-equiv voters voters-equiv)
      (equal (tally-leader-stake-votes leader voters commtt)
             (tally-leader-stake-votes leader voters-equiv commtt)))
 :rule-classes :congruence)

Theorem: tally-leader-stake-votes-of-committee-fix-commtt

(defthm tally-leader-stake-votes-of-committee-fix-commtt
 (equal
     (tally-leader-stake-votes leader voters (committee-fix commtt))
     (tally-leader-stake-votes leader voters commtt)))

Theorem: tally-leader-stake-votes-committee-equiv-congruence-on-commtt

(defthm
      tally-leader-stake-votes-committee-equiv-congruence-on-commtt
 (implies
      (committee-equiv commtt commtt-equiv)
      (equal (tally-leader-stake-votes leader voters commtt)
             (tally-leader-stake-votes leader voters commtt-equiv)))
 :rule-classes :congruence)