		Search-engine friendly clone of the ACL2 documentation.

Messages

Message-certs-with-dest

Extract, from a set of messages, the ones with a given destination, and return their certificates.

Signature
(message-certs-with-dest dest msgs) → certs
Arguments: dest — Guard (addressp dest).; msgs — Guard (message-setp msgs).
Returns: certs — Type (certificate-setp certs).

This can be used to obtain, from the network (which is a set of messages), the certificates addressed to a certain validator.

Definitions and Theorems

Function: message-certs-with-dest

(defun message-certs-with-dest (dest msgs)
  (declare (xargs :guard (and (addressp dest)
                              (message-setp msgs))))
  (let ((__function__ 'message-certs-with-dest))
    (declare (ignorable __function__))
    (b* (((when (emptyp msgs)) nil)
         (msg (head msgs)))
      (if (equal (message->destination msg)
                 (address-fix dest))
          (insert (message->certificate msg)
                  (message-certs-with-dest dest (tail msgs)))
        (message-certs-with-dest dest (tail msgs))))))

Theorem: certificate-setp-of-message-certs-with-dest

(defthm certificate-setp-of-message-certs-with-dest
  (b* ((certs (message-certs-with-dest dest msgs)))
    (certificate-setp certs))
  :rule-classes :rewrite)

Theorem: message-certs-with-dest-of-address-fix-dest

(defthm message-certs-with-dest-of-address-fix-dest
  (equal (message-certs-with-dest (address-fix dest)
                                  msgs)
         (message-certs-with-dest dest msgs)))

Theorem: message-certs-with-dest-address-equiv-congruence-on-dest

(defthm message-certs-with-dest-address-equiv-congruence-on-dest
  (implies (address-equiv dest dest-equiv)
           (equal (message-certs-with-dest dest msgs)
                  (message-certs-with-dest dest-equiv msgs)))
  :rule-classes :congruence)

Theorem: message-certs-with-dest-of-empty-msgs

(defthm message-certs-with-dest-of-empty-msgs
  (implies (emptyp msgs)
           (equal (message-certs-with-dest dest msgs)
                  nil)))

Theorem: in-of-message-certs-with-dest

(defthm in-of-message-certs-with-dest
  (implies (message-setp msgs)
           (equal (in cert
                      (message-certs-with-dest dest msgs))
                  (and (in (message cert dest) msgs)
                       (certificatep cert)))))

Theorem: message-certs-with-dest-of-insert

(defthm message-certs-with-dest-of-insert
  (implies (and (messagep msg) (message-setp msgs))
           (equal (message-certs-with-dest dest (insert msg msgs))
                  (if (equal (message->destination msg)
                             (address-fix dest))
                      (insert (message->certificate msg)
                              (message-certs-with-dest dest msgs))
                    (message-certs-with-dest dest msgs)))))

Theorem: message-certs-with-dest-of-union

(defthm message-certs-with-dest-of-union
  (implies (and (message-setp msgs1)
                (message-setp msgs2))
           (equal (message-certs-with-dest dest (union msgs1 msgs2))
                  (union (message-certs-with-dest dest msgs1)
                         (message-certs-with-dest dest msgs2)))))

Theorem: message-certs-with-dest-of-delete

(defthm message-certs-with-dest-of-delete
  (implies (message-setp msgs)
           (equal (message-certs-with-dest dest (delete msg msgs))
                  (if (and (in msg msgs)
                           (equal (message->destination msg)
                                  (address-fix dest)))
                      (delete (message->certificate msg)
                              (message-certs-with-dest dest msgs))
                    (message-certs-with-dest dest msgs)))))

Subtopics

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