		Search-engine friendly clone of the ACL2 documentation.

Elections

Leader-stake-votes

Count the stake votes for a leader.

Signature
(leader-stake-votes leader voters commtt) → yes-stake
Arguments: leader — Guard (addressp leader).; voters — Guard (certificate-setp voters).; commtt — Guard (committeep commtt).
Returns: yes-stake — Type (natp yes-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 should be 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.

We do not require, in the guard, that the voter certificates are all at the same round and that they are authored by members of the committee. This is for simplicity, and also because, when this function is used, we do not have, readily available, the condition that the voter certificate authors are members of the committee; that is an invariant that is proved elsewhere.

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. This is why we use committee-validator-stake instead of committee-member-stake.

We go through the voters, and check whether the leader address is among the referenced previous certificates or not, counting its stake as part of the resulting vote stake.

Definitions and Theorems

Function: leader-stake-votes

(defun leader-stake-votes (leader voters commtt)
  (declare (xargs :guard (and (addressp leader)
                              (certificate-setp voters)
                              (committeep commtt))))
  (let ((__function__ 'leader-stake-votes))
    (declare (ignorable __function__))
    (b* (((when (emptyp (certificate-set-fix voters)))
          0)
         (voter (head voters))
         (voter-stake
              (committee-validator-stake (certificate->author voter)
                                         commtt))
         (yes-stake (leader-stake-votes leader (tail voters)
                                        commtt)))
      (if (in (address-fix leader)
              (certificate->previous voter))
          (+ voter-stake yes-stake)
        yes-stake))))

Theorem: natp-of-leader-stake-votes

(defthm natp-of-leader-stake-votes
  (b* ((yes-stake (leader-stake-votes leader voters commtt)))
    (natp yes-stake))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

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

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

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

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