		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate-list-orderedp

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

Signature
(certificate-list-orderedp certs) → yes/no
Arguments: certs — Guard (certificate-listp certs).
Returns: yes/no — Type (booleanp yes/no).

This is analogous to blocks-orderedp, 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.

Definitions and Theorems

Function: certificate-list-orderedp

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

Theorem: booleanp-of-certificate-list-orderedp

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

Theorem: certificate-list-orderedp-of-certificate-list-fix-certs

(defthm certificate-list-orderedp-of-certificate-list-fix-certs
  (equal (certificate-list-orderedp (certificate-list-fix certs))
         (certificate-list-orderedp certs)))

Theorem: certificate-list-orderedp-certificate-list-equiv-congruence-on-certs

(defthm
 certificate-list-orderedp-certificate-list-equiv-congruence-on-certs
 (implies (certificate-list-equiv certs certs-equiv)
          (equal (certificate-list-orderedp certs)
                 (certificate-list-orderedp certs-equiv)))
 :rule-classes :congruence)