		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) → commtt
Arguments: blocks — Guard (block-listp blocks).
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.

Definitions and Theorems

Function: committee-after-blocks

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

Theorem: committeep-of-committee-after-blocks

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

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))
         (committee-after-blocks blocks)))

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)
                  (committee-after-blocks blocks-equiv)))
  :rule-classes :congruence)