|
|
|---|
|
|
|
|---|
Last round in a list of blocks, or 0 if there are no blocks.
(blocks-last-round blocks) → last
If blocks-orderedp holds, block rounds are in strictly increading order from right to left. This function returns the latest, i.e. highest, round. If there are no blocks, we totalize this function to return 0.
Although it may seem natural to add blocks-orderedp to this function's guard, we deliberately avoid that, for the following reason. Adding that guard here requires adding it to other operations, particularly active-committee-at-round. The latter is used to define system transistions, and is applied to blockchains of validators, which are just lists of blocks, not necessarily ordered. It is an invariant that they are in fact ordered, but that invariant is proved after defining the transitions, and so it is not available when defining the transitions.
Function:
(defun blocks-last-round (blocks) (declare (xargs :guard (block-listp blocks))) (let ((__function__ 'blocks-last-round)) (declare (ignorable __function__)) (if (consp blocks) (block->round (car blocks)) 0)))
Theorem:
(defthm natp-of-blocks-last-round (b* ((last (blocks-last-round blocks))) (natp last)) :rule-classes :rewrite)
Theorem:
(defthm evenp-of-blocks-last-round (evenp (blocks-last-round blocks)))
Theorem:
(defthm oldest-of-prefix-gt-newest-of-suffix-when-blocks-orderedp (implies (and (blocks-orderedp (append blocks1 blocks2)) (consp blocks1)) (> (block->round (car (last blocks1))) (blocks-last-round blocks2))) :rule-classes ((:linear :trigger-terms ((block->round (car (last blocks1))) (blocks-last-round blocks2)))))
Theorem:
(defthm blocks-last-round-of-block-list-fix-blocks (equal (blocks-last-round (block-list-fix blocks)) (blocks-last-round blocks)))
Theorem:
(defthm blocks-last-round-block-list-equiv-congruence-on-blocks (implies (block-list-equiv blocks blocks-equiv) (equal (blocks-last-round blocks) (blocks-last-round blocks-equiv))) :rule-classes :congruence)