		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Trim-blocks-for-round

Trim a blockchain to what is needed to calculate the (bonded) committee at a given round.

Signature
(trim-blocks-for-round round blocks) → trimmed-blocks
Arguments: round — Guard (posp round).; blocks — Guard (block-listp blocks).
Returns: trimmed-blocks — Type (block-listp trimmed-blocks).

Based on the definition of bonded-committee-at-round, the calculation of the bonded committee at a round only depends on the blocks before that round. It does not depend on the blocks after that round, or on the block (if any) at that round.

This function removes from a list of blocks all the ones whose round is less than or equal to a given round. More precisely, it does that when the blocks are ordered (i.e. when they satisfy blocks-orderedp). But we do not require the ordering here, and just remove blocks until we find one whose round is below the given round.

Definitions and Theorems

Function: trim-blocks-for-round

(defun trim-blocks-for-round (round blocks)
  (declare (xargs :guard (and (posp round)
                              (block-listp blocks))))
  (let ((__function__ 'trim-blocks-for-round))
    (declare (ignorable __function__))
    (b* (((when (endp blocks)) nil)
         ((when (> (pos-fix round)
                   (block->round (car blocks))))
          (block-list-fix blocks)))
      (trim-blocks-for-round round (cdr blocks)))))

Theorem: block-listp-of-trim-blocks-for-round

(defthm block-listp-of-trim-blocks-for-round
  (b* ((trimmed-blocks (trim-blocks-for-round round blocks)))
    (block-listp trimmed-blocks))
  :rule-classes :rewrite)

Theorem: trim-blocks-for-round-of-pos-fix-round

(defthm trim-blocks-for-round-of-pos-fix-round
  (equal (trim-blocks-for-round (pos-fix round)
                                blocks)
         (trim-blocks-for-round round blocks)))

Theorem: trim-blocks-for-round-pos-equiv-congruence-on-round

(defthm trim-blocks-for-round-pos-equiv-congruence-on-round
  (implies (acl2::pos-equiv round round-equiv)
           (equal (trim-blocks-for-round round blocks)
                  (trim-blocks-for-round round-equiv blocks)))
  :rule-classes :congruence)

Theorem: trim-blocks-for-round-of-block-list-fix-blocks

(defthm trim-blocks-for-round-of-block-list-fix-blocks
  (equal (trim-blocks-for-round round (block-list-fix blocks))
         (trim-blocks-for-round round blocks)))

Theorem: trim-blocks-for-round-block-list-equiv-congruence-on-blocks

(defthm trim-blocks-for-round-block-list-equiv-congruence-on-blocks
  (implies (block-list-equiv blocks blocks-equiv)
           (equal (trim-blocks-for-round round blocks)
                  (trim-blocks-for-round round blocks-equiv)))
  :rule-classes :congruence)