		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificates-with-signer

Retrieve, from a set of certificates, the subset of certificates whose signers include a given address.

Signature
(certificates-with-signer signer certs) → certs-with-signer
Arguments: signer — Guard (addressp signer).; certs — Guard (certificate-setp certs).
Returns: certs-with-signer — Type (certificate-setp certs-with-signer).

Definitions and Theorems

Function: certificates-with-signer

(defun certificates-with-signer (signer certs)
  (declare (xargs :guard (and (addressp signer)
                              (certificate-setp certs))))
  (let ((__function__ 'certificates-with-signer))
    (declare (ignorable __function__))
    (b* (((when (emptyp certs)) nil)
         (cert (head certs)))
      (if (in (address-fix signer)
              (certificate->signers cert))
          (insert (certificate-fix cert)
                  (certificates-with-signer signer (tail certs)))
        (certificates-with-signer signer (tail certs))))))

Theorem: certificate-setp-of-certificates-with-signer

(defthm certificate-setp-of-certificates-with-signer
  (b* ((certs-with-signer (certificates-with-signer signer certs)))
    (certificate-setp certs-with-signer))
  :rule-classes :rewrite)

Theorem: certificates-with-signer-of-address-fix-signer

(defthm certificates-with-signer-of-address-fix-signer
  (equal (certificates-with-signer (address-fix signer)
                                   certs)
         (certificates-with-signer signer certs)))

Theorem: certificates-with-signer-address-equiv-congruence-on-signer

(defthm certificates-with-signer-address-equiv-congruence-on-signer
  (implies (address-equiv signer signer-equiv)
           (equal (certificates-with-signer signer certs)
                  (certificates-with-signer signer-equiv certs)))
  :rule-classes :congruence)

Theorem: in-of-certificates-with-signer

(defthm in-of-certificates-with-signer
  (implies (certificate-setp certs)
           (equal (in cert
                      (certificates-with-signer signer certs))
                  (and (in cert certs)
                       (in (address-fix signer)
                           (certificate->signers cert))))))

Theorem: certificates-with-signer-when-emptyp

(defthm certificates-with-signer-when-emptyp
  (implies (emptyp certs)
           (equal (certificates-with-signer signer certs)
                  nil)))

Theorem: certificates-with-signer-of-insert

(defthm certificates-with-signer-of-insert
  (implies
       (and (certificatep cert)
            (certificate-setp certs))
       (equal (certificates-with-signer signer (insert cert certs))
              (if (in (address-fix signer)
                      (certificate->signers cert))
                  (insert cert
                          (certificates-with-signer signer certs))
                (certificates-with-signer signer certs)))))