		Search-engine friendly clone of the ACL2 documentation.

Certificates

Certificate->signers

Signers of a certificate.

Signature
(certificate->signers cert) → signers
Arguments: cert — Guard (certificatep cert).
Returns: signers — Type (address-setp signers).

These are the author and the endorsers, i.e. all the validators who signed the certificate.

Definitions and Theorems

Function: certificate->signers

(defun certificate->signers (cert)
  (declare (xargs :guard (certificatep cert)))
  (let ((__function__ 'certificate->signers))
    (declare (ignorable __function__))
    (b* (((certificate cert) cert))
      (insert cert.author cert.endorsers))))

Theorem: address-setp-of-certificate->signers

(defthm address-setp-of-certificate->signers
  (b* ((signers (certificate->signers cert)))
    (address-setp signers))
  :rule-classes :rewrite)

Theorem: not-emptyp-of-certificate->signers

(defthm not-emptyp-of-certificate->signers
  (b* ((?signers (certificate->signers cert)))
    (not (emptyp signers))))

Theorem: certificate->signers-of-certificate-fix-cert

(defthm certificate->signers-of-certificate-fix-cert
  (equal (certificate->signers (certificate-fix cert))
         (certificate->signers cert)))

Theorem: certificate->signers-certificate-equiv-congruence-on-cert

(defthm certificate->signers-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (certificate->signers cert)
                  (certificate->signers cert-equiv)))
  :rule-classes :congruence)