• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
      • Aleobft-static
      • Aleobft-dynamic
      • Aleobft-stake2
        • Definition
          • Initialization
          • Transitions
            • Transitions-accept
            • Transitions-create
            • Dags
            • Elections
              • Leader-stake-votes
              • Leader-at-round
            • Event-next
            • Transitions-commit
            • Event-possiblep
            • Events-possiblep
            • Events-next
            • Transitions-advance
            • Blockchains
            • Anchors
          • States
          • Events
      • Aleobft-stake
      • Library-extensions
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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 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 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))))
 (declare (xargs :guard (subset (certificate-set->author-set voters)
                                (committee-members commtt))))
 (let ((__function__ 'leader-stake-votes))
  (declare (ignorable __function__))
  (b*
   (((when (or (not (mbt (certificate-setp voters)))
               (emptyp voters)))
     0)
    (voter (head voters))
    (voter-stake (committee-member-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)