		Search-engine friendly clone of the ACL2 documentation.

Committees

Active-committee-at-round

Active committee at a given round.

Signature
(active-committee-at-round round blocks) → commtt?
Arguments: round — Guard (posp round).; blocks — Guard (block-listp blocks).
Returns: commtt? — Type (committee-optionp commtt?).

As explained in lookback, the active committee for a given round, i.e. the one in charge of the round, is the one bonded at the earlier round whose distance is B from the round of interest, or the genesis committee if such earlier round does not exist (i.e. it would be 0 or negative, before round 1). This ACL2 function formalizes this notion of active committee.

Note that there is no guarantee that there is a bonded committee at round R - B, where R is the round of interest. Thus, this function returns an optional committee, nil if no committee is available.

We prove some properties of active committees analogous to certain properties of bonded committees, using in fact those previously proved theorems in the proofs. We also prove some specializations of the theorem that says that if a round has an active committee then every round before that round does as well; the specializations are for the 1, 2, and 3 rounds before.

Definitions and Theorems

Function: active-committee-at-round

(defun active-committee-at-round (round blocks)
  (declare (xargs :guard (and (posp round)
                              (block-listp blocks))))
  (let ((__function__ 'active-committee-at-round))
    (declare (ignorable __function__))
    (if (> (pos-fix round) (lookback))
        (bonded-committee-at-round (- (pos-fix round) (lookback))
                                   blocks)
      (genesis-committee))))

Theorem: committee-optionp-of-active-committee-at-round

(defthm committee-optionp-of-active-committee-at-round
  (b* ((commtt? (active-committee-at-round round blocks)))
    (committee-optionp commtt?))
  :rule-classes :rewrite)

Theorem: active-committee-at-round-when-no-blocks

(defthm active-committee-at-round-when-no-blocks
  (implies (endp blocks)
           (b* ((commtt (active-committee-at-round round blocks)))
             (implies commtt
                      (equal commtt (genesis-committee))))))

Theorem: active-committee-at-round-of-round-leq-2+lookback

(defthm active-committee-at-round-of-round-leq-2+lookback
  (implies (and (blocks-ordered-even-p blocks)
                (<= (pos-fix round) (+ 2 (lookback))))
           (equal (active-committee-at-round round blocks)
                  (genesis-committee))))

Theorem: active-committee-at-round-of-append-no-change

(defthm active-committee-at-round-of-append-no-change
 (implies
    (and (blocks-ordered-even-p (append blocks1 blocks))
         (active-committee-at-round round blocks))
    (equal (active-committee-at-round round (append blocks1 blocks))
           (active-committee-at-round round blocks))))

Theorem: active-committee-at-earlier-round-when-at-later-round

(defthm active-committee-at-earlier-round-when-at-later-round
  (implies (and (active-committee-at-round later blocks)
                (< (pos-fix earlier) (pos-fix later)))
           (active-committee-at-round earlier blocks)))

Theorem: active-committee-at-previous-round-when-at-round

(defthm active-committee-at-previous-round-when-at-round
  (implies (and (active-committee-at-round round blocks)
                (> (pos-fix round) 1))
           (active-committee-at-round (1- round)
                                      blocks)))

Theorem: active-committee-at-previous2-round-when-at-round

(defthm active-committee-at-previous2-round-when-at-round
  (implies (and (active-committee-at-round round blocks)
                (> (pos-fix round) 2))
           (active-committee-at-round (- round 2)
                                      blocks)))

Theorem: active-committee-at-previous3-round-when-at-round

(defthm active-committee-at-previous3-round-when-at-round
  (implies (and (active-committee-at-round round blocks)
                (> (pos-fix round) 3))
           (active-committee-at-round (- round 3)
                                      blocks)))

Theorem: active-committee-at-round-iff-round-upper-bound

(defthm active-committee-at-round-iff-round-upper-bound
  (iff (active-committee-at-round round blocks)
       (<= (nfix (- (pos-fix round) (lookback)))
           (+ 2 (blocks-last-round blocks)))))

Theorem: active-committee-at-round-of-pos-fix-round

(defthm active-committee-at-round-of-pos-fix-round
  (equal (active-committee-at-round (pos-fix round)
                                    blocks)
         (active-committee-at-round round blocks)))

Theorem: active-committee-at-round-pos-equiv-congruence-on-round

(defthm active-committee-at-round-pos-equiv-congruence-on-round
  (implies (acl2::pos-equiv round round-equiv)
           (equal (active-committee-at-round round blocks)
                  (active-committee-at-round round-equiv blocks)))
  :rule-classes :congruence)

Theorem: active-committee-at-round-of-block-list-fix-blocks

(defthm active-committee-at-round-of-block-list-fix-blocks
  (equal (active-committee-at-round round (block-list-fix blocks))
         (active-committee-at-round round blocks)))

Theorem: active-committee-at-round-block-list-equiv-congruence-on-blocks

(defthm
    active-committee-at-round-block-list-equiv-congruence-on-blocks
  (implies (block-list-equiv blocks blocks-equiv)
           (equal (active-committee-at-round round blocks)
                  (active-committee-at-round round blocks-equiv)))
  :rule-classes :congruence)