		Search-engine friendly clone of the ACL2 documentation.

Committees

Committee-after-blocks

Calculate the committee after a list of blocks.

Signature
(committee-after-blocks blocks all-vals) → commtt
Arguments: blocks — Guard (block-listp blocks).; all-vals — Guard (address-setp all-vals).
Returns: commtt — Type (committeep commtt).

The list of blocks is the blockchain (of a validator), or a prefix of that blockchain (more on this later). We calculate the committee that results from updating the genesis committee with all the transactions in the blocks. Since, as explained in validator-state, the blockchain goes from right to left (i.e. the leftmost block is the newest and the rightmost block is the oldest), we update the genesis committee from right to left to arrive at the resulting committee.

The role of the all-vals input is explained in update-committee-with-transaction.

We show that the committee's members are in all-vals, so long as the genesis committee's members are.

Definitions and Theorems

Function: committee-after-blocks

(defun committee-after-blocks (blocks all-vals)
  (declare (xargs :guard (and (block-listp blocks)
                              (address-setp all-vals))))
  (let ((__function__ 'committee-after-blocks))
    (declare (ignorable __function__))
    (b* (((when (endp blocks))
          (genesis-committee))
         (commtt (committee-after-blocks (cdr blocks)
                                         all-vals)))
      (update-committee-with-transaction-list
           (block->transactions (car blocks))
           commtt all-vals))))

Theorem: committeep-of-committee-after-blocks

(defthm committeep-of-committee-after-blocks
  (b* ((commtt (committee-after-blocks blocks all-vals)))
    (committeep commtt))
  :rule-classes :rewrite)

Theorem: committee-after-blocks-subset-all-vals

(defthm committee-after-blocks-subset-all-vals
  (implies (and (address-setp all-vals)
                (subset (committee-members (genesis-committee))
                        all-vals))
           (b* ((?commtt (committee-after-blocks blocks all-vals)))
             (subset (committee-members commtt)
                     all-vals))))

Theorem: committee-after-blocks-of-block-list-fix-blocks

(defthm committee-after-blocks-of-block-list-fix-blocks
  (equal (committee-after-blocks (block-list-fix blocks)
                                 all-vals)
         (committee-after-blocks blocks all-vals)))

Theorem: committee-after-blocks-block-list-equiv-congruence-on-blocks

(defthm committee-after-blocks-block-list-equiv-congruence-on-blocks
  (implies (block-list-equiv blocks blocks-equiv)
           (equal (committee-after-blocks blocks all-vals)
                  (committee-after-blocks blocks-equiv all-vals)))
  :rule-classes :congruence)

Theorem: committee-after-blocks-of-address-set-fix-all-vals

(defthm committee-after-blocks-of-address-set-fix-all-vals
  (equal (committee-after-blocks blocks (address-set-fix all-vals))
         (committee-after-blocks blocks all-vals)))

Theorem: committee-after-blocks-address-set-equiv-congruence-on-all-vals

(defthm
    committee-after-blocks-address-set-equiv-congruence-on-all-vals
  (implies (address-set-equiv all-vals all-vals-equiv)
           (equal (committee-after-blocks blocks all-vals)
                  (committee-after-blocks blocks all-vals-equiv)))
  :rule-classes :congruence)