		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: see transitions-certify.

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 (address-set-fix dests)) nil)
     (t (insert (make-message-certificate :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: in-of-make-certificate-messages

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

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: make-certificate-messages-of-address-set-fix-dests

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

Theorem: make-certificate-messages-address-set-equiv-congruence-on-dests

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