		Search-engine friendly clone of the ACL2 documentation.

Messages

Make-certificate-messages

Create messages for a certificate with given destinations.

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

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

These are the messages broadcasted to the network when a certificate is created.

Definitions and Theorems

Function: make-certificate-messages

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

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

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

Theorem: make-certificate-messages-of-certificate-fix-cert

(defthm make-certificate-messages-of-certificate-fix-cert
  (equal (make-certificate-messages (certificate-fix cert)
                                    dests)
         (make-certificate-messages cert dests)))

Theorem: make-certificate-messages-certificate-equiv-congruence-on-cert

(defthm
     make-certificate-messages-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (make-certificate-messages cert dests)
                  (make-certificate-messages cert-equiv dests)))
  :rule-classes :congruence)

Theorem: in-of-make-certificate-messages

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

Theorem: message-set->certificate-set-of-make-certificate-messages

(defthm message-set->certificate-set-of-make-certificate-messages
  (equal (message-set->certificate-set
              (make-certificate-messages cert dests))
         (if (emptyp dests)
             nil
           (insert (certificate-fix cert) nil))))

Subtopics

Message-certs-with-dest-of-make-certificate-messages: Relation between message extraction and message creation.