		Search-engine friendly clone of the ACL2 documentation.

Transitions-endorse

Endorse-next

New system state resulting from an endorse event.

Signature
(endorse-next prop endor systate) → new-systate
Arguments: prop — Guard (proposalp prop).; endor — Guard (addressp endor).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

The prop and endor parameters of this function are the corresponding components of the endorse event.

The proposal message is removed from the network, and an endorsement message is added to the network. Additionally, if the endorser is correct, its state is updated to record that it has endorsed the proposal.

Definitions and Theorems

Function: endorse-next

(defun endorse-next (prop endor systate)
 (declare (xargs :guard (and (proposalp prop)
                             (addressp endor)
                             (system-statep systate))))
 (declare (xargs :guard (endorse-possiblep prop endor systate)))
 (let ((__function__ 'endorse-next))
   (declare (ignorable __function__))
   (b* (((proposal prop) prop)
        (network (get-network-state systate))
        (old-msg (make-message-proposal :proposal prop
                                        :destination endor))
        (new-msg (make-message-endorsement :proposal prop
                                           :endorser endor))
        (new-network (insert new-msg (delete old-msg network)))
        (systate (update-network-state new-network systate))
        ((unless (in (address-fix endor)
                     (correct-addresses systate)))
         systate)
        ((validator-state vstate)
         (get-validator-state endor systate))
        (new-endorsed (insert (proposal-fix prop)
                              vstate.endorsed))
        (new-vstate (change-validator-state vstate
                                            :endorsed new-endorsed))
        (systate (update-validator-state endor new-vstate systate)))
     systate)))

Theorem: system-statep-of-endorse-next

(defthm system-statep-of-endorse-next
  (b* ((new-systate (endorse-next prop endor systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: correct-addresses-of-endorse-next

(defthm correct-addresses-of-endorse-next
  (b* ((?new-systate (endorse-next prop endor systate)))
    (equal (correct-addresses new-systate)
           (correct-addresses systate))))

Theorem: validator-state->round-of-endorse-next

(defthm validator-state->round-of-endorse-next
 (b* ((?new-systate (endorse-next prop endor systate)))
  (equal
      (validator-state->round (get-validator-state val new-systate))
      (validator-state->round (get-validator-state val systate)))))

Theorem: validator-state->dag-of-endorse-next

(defthm validator-state->dag-of-endorse-next
 (b* ((?new-systate (endorse-next prop endor systate)))
   (equal
        (validator-state->dag (get-validator-state val new-systate))
        (validator-state->dag (get-validator-state val systate)))))

Theorem: validator-state->proposed-of-endorse-next

(defthm validator-state->proposed-of-endorse-next
 (b* ((?new-systate (endorse-next prop endor systate)))
  (equal
   (validator-state->proposed (get-validator-state val new-systate))
   (validator-state->proposed (get-validator-state val systate)))))

Theorem: validator-state->endorsed-of-endorse-next

(defthm validator-state->endorsed-of-endorse-next
 (b* ((?new-systate (endorse-next prop endor systate)))
  (equal
   (validator-state->endorsed (get-validator-state val new-systate))
   (if
    (and (equal (address-fix val)
                (address-fix endor))
         (in (address-fix val)
             (correct-addresses systate)))
    (insert
      (proposal-fix prop)
      (validator-state->endorsed (get-validator-state val systate)))
    (validator-state->endorsed
         (get-validator-state val systate))))))

Theorem: validator-state->last-of-endorse-next

(defthm validator-state->last-of-endorse-next
 (b* ((?new-systate (endorse-next prop endor systate)))
  (equal
       (validator-state->last (get-validator-state val new-systate))
       (validator-state->last (get-validator-state val systate)))))

Theorem: validator-state->blockchain-of-endorse-next

(defthm validator-state->blockchain-of-endorse-next
  (b* ((?new-systate (endorse-next prop endor systate)))
    (equal (validator-state->blockchain
                (get-validator-state val new-systate))
           (validator-state->blockchain
                (get-validator-state val systate)))))

Theorem: validator-state->committed-of-endorse-next

(defthm validator-state->committed-of-endorse-next
 (b* ((?new-systate (endorse-next prop endor systate)))
  (equal
   (validator-state->committed
        (get-validator-state val new-systate))
   (validator-state->committed (get-validator-state val systate)))))

Theorem: get-network-state-of-endorse-next

(defthm get-network-state-of-endorse-next
  (b* ((?new-systate (endorse-next prop endor systate)))
    (equal (get-network-state new-systate)
           (insert (message-endorsement prop endor)
                   (delete (message-proposal prop endor)
                           (get-network-state systate))))))

Theorem: endorse-next-of-proposal-fix-prop

(defthm endorse-next-of-proposal-fix-prop
  (equal (endorse-next (proposal-fix prop)
                       endor systate)
         (endorse-next prop endor systate)))

Theorem: endorse-next-proposal-equiv-congruence-on-prop

(defthm endorse-next-proposal-equiv-congruence-on-prop
  (implies (proposal-equiv prop prop-equiv)
           (equal (endorse-next prop endor systate)
                  (endorse-next prop-equiv endor systate)))
  :rule-classes :congruence)

Theorem: endorse-next-of-address-fix-endor

(defthm endorse-next-of-address-fix-endor
  (equal (endorse-next prop (address-fix endor)
                       systate)
         (endorse-next prop endor systate)))

Theorem: endorse-next-address-equiv-congruence-on-endor

(defthm endorse-next-address-equiv-congruence-on-endor
  (implies (address-equiv endor endor-equiv)
           (equal (endorse-next prop endor systate)
                  (endorse-next prop endor-equiv systate)))
  :rule-classes :congruence)

Theorem: endorse-next-of-system-state-fix-systate

(defthm endorse-next-of-system-state-fix-systate
  (equal (endorse-next prop endor (system-state-fix systate))
         (endorse-next prop endor systate)))

Theorem: endorse-next-system-state-equiv-congruence-on-systate

(defthm endorse-next-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (endorse-next prop endor systate)
                  (endorse-next prop endor systate-equiv)))
  :rule-classes :congruence)