Signers of a certificate.
(certificate->signers cert) → signers
These are the author and the endorsers.
Function:
(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:
(defthm address-setp-of-certificate->signers (b* ((signers (certificate->signers cert))) (address-setp signers)) :rule-classes :rewrite)