		Search-engine friendly clone of the ACL2 documentation.

Elections

Leader-at-round

Leader at a round, given a committee active at that round.

We introduce a constrained function that, given a round number and a non-empty committee, returns an address in the committee. This is the chosen leader at that round.

In AleoBFT, this calculation is deterministic, given the round number and committee, but the details are unimportant to our model. Thus, the use of constrained function is appropriate.

Definitions and Theorems

Theorem: addressp-of-leader-at-round

(defthm addressp-of-leader-at-round
  (addressp (leader-at-round round commtt)))

Theorem: leader-in-committee

(defthm leader-in-committee
  (implies (committee-nonemptyp commtt)
           (in (leader-at-round round commtt)
               (committee-members commtt))))

Theorem: leader-at-round-of-pos-fix

(defthm leader-at-round-of-pos-fix
  (equal (leader-at-round (pos-fix round) commtt)
         (leader-at-round round commtt)))

Theorem: leader-at-round-of-committee-fix

(defthm leader-at-round-of-committee-fix
  (equal (leader-at-round round (committee-fix commtt))
         (leader-at-round round commtt)))