		Search-engine friendly clone of the ACL2 documentation.

Operations-certificate-retrieval

Certificate-with-author+round

Retrieve the certificate from a set with a given author and round.

Signature
(certificate-with-author+round author round certs) → cert?
Arguments: author — Guard (addressp author).; round — Guard (posp round).; certs — Guard (certificate-setp certs).
Returns: cert? — Type (certificate-optionp cert?).

If there is no certificate with the given author and round, nil is returned, for no certificate.

If there is a certificate with the given author and round, the first one found is returned, according to the total ordering of the set. However, this function will be used in sets where certificates have unique combinations of author and round, which justifies the use of `the' above in `Retrieve the certificate...'.

Definitions and Theorems

Function: certificate-with-author+round

(defun certificate-with-author+round (author round certs)
  (declare (xargs :guard (and (addressp author)
                              (posp round)
                              (certificate-setp certs))))
  (let ((__function__ 'certificate-with-author+round))
    (declare (ignorable __function__))
    (b* (((when (emptyp certs)) nil)
         ((certificate cert) (head certs))
         ((when (and (equal author cert.author)
                     (equal round cert.round)))
          (certificate-fix cert)))
      (certificate-with-author+round author round (tail certs)))))

Theorem: certificate-optionp-of-certificate-with-author+round

(defthm certificate-optionp-of-certificate-with-author+round
  (b* ((cert? (certificate-with-author+round author round certs)))
    (certificate-optionp cert?))
  :rule-classes :rewrite)

Theorem: certificate->author-of-certificate-with-author+round

(defthm certificate->author-of-certificate-with-author+round
  (b* ((?cert? (certificate-with-author+round author round certs)))
    (implies cert?
             (equal (certificate->author cert?)
                    (address-fix author)))))

Theorem: certificate->round-of-certificate-with-author+round

(defthm certificate->round-of-certificate-with-author+round
  (b* ((?cert? (certificate-with-author+round author round certs)))
    (implies cert?
             (equal (certificate->round cert?)
                    (pos-fix round)))))

Theorem: certificate-with-author+round-element

(defthm certificate-with-author+round-element
  (implies (and (certificate-setp certs)
                (certificate-with-author+round author round certs))
           (in (certificate-with-author+round author round certs)
               certs)))

Theorem: certificate-with-author+round-when-element

(defthm certificate-with-author+round-when-element
  (implies (and (in cert certs)
                (equal (certificate->author cert)
                       author)
                (equal (certificate->round cert) round))
           (certificate-with-author+round author round certs)))

Theorem: certificate-with-author+round-when-subset

(defthm certificate-with-author+round-when-subset
  (implies (and (certificate-with-author+round author round certs0)
                (subset certs0 certs))
           (certificate-with-author+round author round certs)))

Theorem: certificate-with-author+round-of-insert-iff

(defthm certificate-with-author+round-of-insert-iff
 (iff
    (certificate-with-author+round author round (insert cert certs))
    (or (and (equal (certificate->author cert)
                    author)
             (equal (certificate->round cert) round))
        (certificate-with-author+round author round certs))))

Theorem: certificate-with-author+round-of-union-iff

(defthm certificate-with-author+round-of-union-iff
 (implies
    (and (certificate-setp certs1)
         (certificate-setp certs2)
         (addressp author)
         (posp round))
    (iff (certificate-with-author+round
              author round (union certs1 certs2))
         (or (certificate-with-author+round author round certs1)
             (certificate-with-author+round author round certs2)))))