		Search-engine friendly clone of the ACL2 documentation.

Messages

Make-endorsement-messages

Create messages for an endorsement from given endorsers.

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

For each given address, we create an endorsement message with the proposal and with the address as endorser.

These are the messages consumed from the network when a faulty validator creates a certificate: see transitions-certify.

Definitions and Theorems

Function: make-endorsement-messages

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

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

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

Theorem: in-of-make-endorsement-messages

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

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

(defthm make-endorsement-messages-of-proposal-fix-prop
  (equal (make-endorsement-messages (proposal-fix prop)
                                    endors)
         (make-endorsement-messages prop endors)))

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

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

Theorem: make-endorsement-messages-of-address-set-fix-endors

(defthm make-endorsement-messages-of-address-set-fix-endors
  (equal (make-endorsement-messages prop (address-set-fix endors))
         (make-endorsement-messages prop endors)))

Theorem: make-endorsement-messages-address-set-equiv-congruence-on-endors

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