|
|
|---|
|
|
|
|---|
Check if a list of certificates has even and strictly increasing (right to left) round numbers.
(certificates-ordered-even-p certs) → yes/no
This is analogous to blocks-ordered-even-p, but for certificates instead of blocks. The reason for having this predicate on certificates is that blockchains are extended from sequences of anchors, which are lists of certificates; the reason why blocks have even and strictly increasing round numbers is that the collected lists of anchors also have strictly increasing, even round numbers.
Function:
(defun certificates-ordered-even-p (certs) (declare (xargs :guard (certificate-listp certs))) (let ((__function__ 'certificates-ordered-even-p)) (declare (ignorable __function__)) (b* (((when (endp certs)) t) (cert (car certs)) (round (certificate->round cert)) ((unless (evenp round)) nil) ((when (endp (cdr certs))) t) ((unless (> round (certificate->round (cadr certs)))) nil)) (certificates-ordered-even-p (cdr certs)))))
Theorem:
(defthm booleanp-of-certificates-ordered-even-p (b* ((yes/no (certificates-ordered-even-p certs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm certificates-ordered-even-p-of-certificate-list-fix-certs (equal (certificates-ordered-even-p (certificate-list-fix certs)) (certificates-ordered-even-p certs)))
Theorem:
(defthm certificates-ordered-even-p-certificate-list-equiv-congruence-on-certs (implies (certificate-list-equiv certs certs-equiv) (equal (certificates-ordered-even-p certs) (certificates-ordered-even-p certs-equiv))) :rule-classes :congruence)