		Search-engine friendly clone of the ACL2 documentation.

Certificates

Cert-with-author+round

Retrieve, from a set of certificates, a certificate with a given author and round.

Signature
(cert-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.

Definitions and Theorems

Function: cert-with-author+round

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

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

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

Theorem: cert-with-author+round-of-address-fix-author

(defthm cert-with-author+round-of-address-fix-author
  (equal (cert-with-author+round (address-fix author)
                                 round certs)
         (cert-with-author+round author round certs)))

Theorem: cert-with-author+round-address-equiv-congruence-on-author

(defthm cert-with-author+round-address-equiv-congruence-on-author
 (implies (address-equiv author author-equiv)
          (equal (cert-with-author+round author round certs)
                 (cert-with-author+round author-equiv round certs)))
 :rule-classes :congruence)

Theorem: cert-with-author+round-of-pos-fix-round

(defthm cert-with-author+round-of-pos-fix-round
  (equal (cert-with-author+round author (pos-fix round)
                                 certs)
         (cert-with-author+round author round certs)))

Theorem: cert-with-author+round-pos-equiv-congruence-on-round

(defthm cert-with-author+round-pos-equiv-congruence-on-round
 (implies (acl2::pos-equiv round round-equiv)
          (equal (cert-with-author+round author round certs)
                 (cert-with-author+round author round-equiv certs)))
 :rule-classes :congruence)

Theorem: cert-with-author+round-of-certificate-set-fix-certs

(defthm cert-with-author+round-of-certificate-set-fix-certs
  (equal (cert-with-author+round author
                                 round (certificate-set-fix certs))
         (cert-with-author+round author round certs)))

Theorem: cert-with-author+round-certificate-set-equiv-congruence-on-certs

(defthm
   cert-with-author+round-certificate-set-equiv-congruence-on-certs
 (implies (certificate-set-equiv certs certs-equiv)
          (equal (cert-with-author+round author round certs)
                 (cert-with-author+round author round certs-equiv)))
 :rule-classes :congruence)

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

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

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

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

Theorem: cert-with-author+round-element

(defthm cert-with-author+round-element
  (implies (cert-with-author+round author round certs)
           (in (cert-with-author+round author round certs)
               certs)))

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

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

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

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

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

(defthm cert-with-author+round-of-insert-iff
 (implies
      (and (certificatep cert)
           (certificate-setp certs))
      (iff (cert-with-author+round author round (insert cert certs))
           (or (and (equal (certificate->author cert)
                           (address-fix author))
                    (equal (certificate->round cert)
                           (pos-fix round)))
               (cert-with-author+round author round certs)))))

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

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

Theorem: cert-with-author+round-when-delete

(defthm cert-with-author+round-when-delete
 (implies
      (and (cert-with-author+round author round (delete cert certs))
           (certificate-setp certs))
      (cert-with-author+round author round certs)))

Theorem: cert-with-author+round-of-delete

(defthm cert-with-author+round-of-delete
  (implies
       (and (certificate-setp certs)
            (cert-with-author+round author round certs)
            (or (not (equal (certificate->author cert)
                            (address-fix author)))
                (not (equal (certificate->round cert)
                            (pos-fix round)))))
       (cert-with-author+round author round (delete cert certs))))