		Search-engine friendly clone of the ACL2 documentation.

Operations-message-creation

Messages-for-certificate

Create messages for a certificate with given destinations.

Signature
(messages-for-certificate cert dests) → msgs
Arguments: cert — Guard (certificatep cert).; dests — Guard (address-setp dests).
Returns: msgs — Type (message-setp msgs).

For each address, we create a message with the certificate and the address as destination.

This is used to model the broadcasting of a certificate in create-certificate-next.

Definitions and Theorems

Function: messages-for-certificate

(defun messages-for-certificate (cert dests)
 (declare (xargs :guard (and (certificatep cert)
                             (address-setp dests))))
 (let ((__function__ 'messages-for-certificate))
  (declare (ignorable __function__))
  (cond ((emptyp dests) nil)
        (t (insert (make-message :certificate cert
                                 :destination (head dests))
                   (messages-for-certificate cert (tail dests)))))))

Theorem: message-setp-of-messages-for-certificate

(defthm message-setp-of-messages-for-certificate
  (b* ((msgs (messages-for-certificate cert dests)))
    (message-setp msgs))
  :rule-classes :rewrite)

Theorem: message->certificate-when-in-messages-for-certificate

(defthm message->certificate-when-in-messages-for-certificate
  (implies (and (certificatep cert)
                (in msg
                    (messages-for-certificate cert dests)))
           (equal (message->certificate msg)
                  cert)))

Theorem: in-of-messages-for-certificate

(defthm in-of-messages-for-certificate
  (implies (address-setp dests)
           (equal (in msg
                      (messages-for-certificate cert dests))
                  (and (messagep msg)
                       (equal (message->certificate msg)
                              (certificate-fix cert))
                       (in (message->destination msg)
                           dests)))))