		Search-engine friendly clone of the ACL2 documentation.

Messages

Message-certificates-with-destination

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

Signature
(message-certificates-with-destination 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-certificates-with-destination

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

Theorem: certificate-setp-of-message-certificates-with-destination

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

Theorem: message-certificates-with-destination-of-address-fix-dest

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

Theorem: message-certificates-with-destination-address-equiv-congruence-on-dest

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

Theorem: in-of-message-certificates-with-destination

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

Theorem: message-certificates-with-destination-when-emptyp

(defthm message-certificates-with-destination-when-emptyp
  (implies (emptyp msgs)
           (equal (message-certificates-with-destination dest msgs)
                  nil)))

Theorem: message-certificates-with-destination-of-insert

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

Theorem: message-certificates-with-destination-of-union

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

Theorem: message-certificates-with-destination-of-delete

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

Subtopics

Message-certificates-with-destination-of-make-certificate-messages: Relation between message extraction and message creation.