		Search-engine friendly clone of the ACL2 documentation.

Operations-leaders

Leader-at-round

Address of the leader validator at a given non-zero even round.

Signature
(leader-at-round round vals) → leader
Arguments: round — Guard (posp round).; vals — Guard (address-setp vals).
Returns: leader — Type (addressp leader).

We pass the set of electable validators to this function. We retrieve the natural number for the round from the under-specified function for the leader index. We reduce the natural number modulo the number of validators, and use the index to pick the leader address.

The set of validators must be non-empty, otherwise there is no validator to pick.

Definitions and Theorems

Function: leader-at-round

(defun leader-at-round (round vals)
  (declare (xargs :guard (and (posp round) (address-setp vals))))
  (declare (xargs :guard (and (evenp round)
                              (not (emptyp vals)))))
  (let ((__function__ 'leader-at-round))
    (declare (ignorable __function__))
    (b* ((index (leader-index round))
         (index (mod index (cardinality vals))))
      (nth-address index vals))))

Theorem: addressp-of-leader-at-round

(defthm addressp-of-leader-at-round
  (b* ((leader (leader-at-round round vals)))
    (addressp leader))
  :rule-classes :rewrite)