		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certs-with-signer

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

Signature
(certs-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: certs-with-signer

(defun certs-with-signer (signer certs)
  (declare (xargs :guard (and (addressp signer)
                              (certificate-setp certs))))
  (let ((__function__ 'certs-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)
                  (certs-with-signer signer (tail certs)))
        (certs-with-signer signer (tail certs))))))

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

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

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

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

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

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

Theorem: in-of-certs-with-signer

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

Theorem: certs-with-signer-of-nil

(defthm certs-with-signer-of-nil
  (equal (certs-with-signer signer nil)
         nil))

Theorem: certs-with-signer-of-insert

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