		Search-engine friendly clone of the ACL2 documentation.

Blocks

Blocks-orderedp

Check if a list of blocks is ordered, i.e. it has strictly increasing round numbers from right to left.

Signature
(blocks-orderedp 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. Blocks go from right to left, i.e. the car is the newest block.

Blocks are committed at increasingly higher round numbers, at most one block per round. So the blocks have round numbers in stricly increasing order. This predicate fomalizes this constraint on round numbers of blocks.

The fact that the round numbers are even is captured in block.

Definitions and Theorems

Function: blocks-orderedp

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

Theorem: booleanp-of-blocks-orderedp

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

Theorem: blocks-orderedp-of-cdr

(defthm blocks-orderedp-of-cdr
  (implies (blocks-orderedp blocks)
           (blocks-orderedp (cdr blocks))))

Theorem: newest-geq-oldest-when-blocks-orderedp

(defthm newest-geq-oldest-when-blocks-orderedp
  (implies (and (blocks-orderedp blocks)
                (consp blocks))
           (>= (block->round (car blocks))
               (block->round (car (last blocks)))))
  :rule-classes
  ((:linear :trigger-terms ((block->round (car blocks))
                            (block->round (car (last blocks)))))))

Theorem: blocks-orderedp-of-append

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

Theorem: blocks-orderedp-of-block-list-fix-blocks

(defthm blocks-orderedp-of-block-list-fix-blocks
  (equal (blocks-orderedp (block-list-fix blocks))
         (blocks-orderedp blocks)))

Theorem: blocks-orderedp-block-list-equiv-congruence-on-blocks

(defthm blocks-orderedp-block-list-equiv-congruence-on-blocks
  (implies (block-list-equiv blocks blocks-equiv)
           (equal (blocks-orderedp blocks)
                  (blocks-orderedp blocks-equiv)))
  :rule-classes :congruence)