		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificates-ordered-even-p

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

Signature
(certificates-ordered-even-p certs) → yes/no
Arguments: certs — Guard (certificate-listp certs).
Returns: yes/no — Type (booleanp 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 strictly increasing, even round numbers is that the collected lists of anchors also have strictly increasing, even round numbers.

Definitions and Theorems

Function: certificates-ordered-even-p

(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: booleanp-of-certificates-ordered-even-p

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

Theorem: certificates-ordered-even-p-of-certificate-list-fix-certs

(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: certificates-ordered-even-p-certificate-list-equiv-congruence-on-certs

(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)