		Search-engine friendly clone of the ACL2 documentation.

Blocks

Blocks-ordered-even-p

Check if a list of blocks has strictly increasing (right to left), even round numbers.

Signature
(blocks-ordered-even-p blocks) → yes/no
Arguments: blocks — Guard (block-listp blocks).
Returns: yes/no — Type (booleanp yes/no).

The state of each (correct) validator includes a list of blocks that models the blockchain (as seen by the validator): see validator-state. As explained there, blocks go from right to left, i.e. the car is the newest block.

Blocks are committed at even rounds, using increasingly higher round numbers, at most one block per (even) round. So the blocks will have round numbers in stricly increasing order, and they will all be even. This predicate fomalizes these constraints on round numbers.

Definitions and Theorems

Function: blocks-ordered-even-p

(defun blocks-ordered-even-p (blocks)
  (declare (xargs :guard (block-listp blocks)))
  (let ((__function__ 'blocks-ordered-even-p))
    (declare (ignorable __function__))
    (b* (((when (endp blocks)) t)
         (block (car blocks))
         (round (block->round block))
         ((unless (evenp round)) nil)
         ((when (endp (cdr blocks))) t)
         ((unless (> round (block->round (cadr blocks))))
          nil))
      (blocks-ordered-even-p (cdr blocks)))))

Theorem: booleanp-of-blocks-ordered-even-p

(defthm booleanp-of-blocks-ordered-even-p
  (b* ((yes/no (blocks-ordered-even-p blocks)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: blocks-ordered-even-p-of-cdr

(defthm blocks-ordered-even-p-of-cdr
  (implies (blocks-ordered-even-p blocks)
           (blocks-ordered-even-p (cdr blocks))))

Theorem: newest-geq-oldest-when-blocks-ordered-even-p

(defthm newest-geq-oldest-when-blocks-ordered-even-p
  (implies (and (blocks-ordered-even-p blocks)
                (consp blocks))
           (>= (block->round (car blocks))
               (block->round (car (last blocks)))))
  :rule-classes :linear)

Theorem: evenp-of-car-when-blocks-ordered-even-p

(defthm evenp-of-car-when-blocks-ordered-even-p
  (implies (and (blocks-ordered-even-p blocks)
                (consp blocks))
           (evenp (block->round (car blocks)))))

Theorem: evenp-of-car-of-last-when-blocks-ordered-even-p

(defthm evenp-of-car-of-last-when-blocks-ordered-even-p
  (implies (and (blocks-ordered-even-p blocks)
                (consp blocks))
           (evenp (block->round (car (last blocks))))))

Theorem: evenp-of-nth-when-blocks-ordered-even-p

(defthm evenp-of-nth-when-blocks-ordered-even-p
  (implies (and (blocks-ordered-even-p blocks)
                (< (nfix i) (len blocks)))
           (evenp (block->round (nth i blocks)))))

Theorem: blocks-ordered-even-p-of-append

(defthm blocks-ordered-even-p-of-append
  (equal (blocks-ordered-even-p (append blocks1 blocks2))
         (and (blocks-ordered-even-p blocks1)
              (blocks-ordered-even-p blocks2)
              (or (endp blocks1)
                  (endp blocks2)
                  (>= (block->round (car (last blocks1)))
                      (+ 2 (block->round (car blocks2))))))))

Theorem: blocks-ordered-even-p-of-block-list-fix-blocks

(defthm blocks-ordered-even-p-of-block-list-fix-blocks
  (equal (blocks-ordered-even-p (block-list-fix blocks))
         (blocks-ordered-even-p blocks)))

Theorem: blocks-ordered-even-p-block-list-equiv-congruence-on-blocks

(defthm blocks-ordered-even-p-block-list-equiv-congruence-on-blocks
  (implies (block-list-equiv blocks blocks-equiv)
           (equal (blocks-ordered-even-p blocks)
                  (blocks-ordered-even-p blocks-equiv)))
  :rule-classes :congruence)