		Search-engine friendly clone of the ACL2 documentation.

Messages

Make-proposal-messages

Create messages for a proposal with given destinations.

Signature
(make-proposal-messages prop dests) → msgs
Arguments: prop — Guard (proposalp prop).; dests — Guard (address-setp dests).
Returns: msgs — Type (message-setp msgs).

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

These are the messages broadcasted to the network when a proposal is created: see transitions-propose.

Definitions and Theorems

Function: make-proposal-messages

(defun make-proposal-messages (prop dests)
 (declare (xargs :guard (and (proposalp prop)
                             (address-setp dests))))
 (let ((__function__ 'make-proposal-messages))
  (declare (ignorable __function__))
  (cond ((emptyp (address-set-fix dests)) nil)
        (t (insert (make-message-proposal :proposal prop
                                          :destination (head dests))
                   (make-proposal-messages prop (tail dests)))))))

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

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

Theorem: in-of-make-proposal-messages

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

Theorem: make-proposal-messages-of-proposal-fix-prop

(defthm make-proposal-messages-of-proposal-fix-prop
  (equal (make-proposal-messages (proposal-fix prop)
                                 dests)
         (make-proposal-messages prop dests)))

Theorem: make-proposal-messages-proposal-equiv-congruence-on-prop

(defthm make-proposal-messages-proposal-equiv-congruence-on-prop
  (implies (proposal-equiv prop prop-equiv)
           (equal (make-proposal-messages prop dests)
                  (make-proposal-messages prop-equiv dests)))
  :rule-classes :congruence)

Theorem: make-proposal-messages-of-address-set-fix-dests

(defthm make-proposal-messages-of-address-set-fix-dests
  (equal (make-proposal-messages prop (address-set-fix dests))
         (make-proposal-messages prop dests)))

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

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