		Search-engine friendly clone of the ACL2 documentation.

Transitions-receive-certificate

Receive-certificate-next

New system state resulting from a receive-certificate event.

Signature
(receive-certificate-next msg systate) → new-systate
Arguments: msg — Guard (messagep msg).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

The certificate is added to the buffer of the destination validator. Recall that receive-certificate-possiblep requires the destination address to be of a correct validator.

The message is removed from the network.

Furthermore, if the validator has previously endorsed that certificate, the author-round pair is removed from the set of pairs, because the certificate is now in the buffer. The set deletion has no effect if the set does not have the pair, so we remove the element unconditionally.

Definitions and Theorems

Function: receive-certificate-next

(defun receive-certificate-next (msg systate)
 (declare (xargs :guard (and (messagep msg)
                             (system-statep systate))))
 (declare
      (xargs :guard (receive-certificate-possiblep msg systate)))
 (let ((__function__ 'receive-certificate-next))
   (declare (ignorable __function__))
   (b* (((certificate cert)
         (message->certificate msg))
        (dest (message->destination msg))
        ((validator-state vstate)
         (get-validator-state dest systate))
        (new-buffer (insert cert vstate.buffer))
        (new-endorsed (delete (make-address+pos :address cert.author
                                                :pos cert.round)
                              vstate.endorsed))
        (new-vstate (change-validator-state vstate
                                            :buffer new-buffer
                                            :endorsed new-endorsed))
        (systate (update-validator-state dest new-vstate systate))
        (network (get-network-state systate))
        (new-network (delete (message-fix msg) network))
        (systate (update-network-state new-network systate)))
     systate)))

Theorem: system-statep-of-receive-certificate-next

(defthm system-statep-of-receive-certificate-next
  (b* ((new-systate (receive-certificate-next msg systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: all-addresses-of-receive-certificate-next

(defthm all-addresses-of-receive-certificate-next
  (implies
       (receive-certificate-possiblep msg systate)
       (b* ((?new-systate (receive-certificate-next msg systate)))
         (equal (all-addresses new-systate)
                (all-addresses systate)))))

Theorem: correct-addresses-of-receive-certificate-next

(defthm correct-addresses-of-receive-certificate-next
  (implies
       (receive-certificate-possiblep msg systate)
       (b* ((?new-systate (receive-certificate-next msg systate)))
         (equal (correct-addresses new-systate)
                (correct-addresses systate)))))

Theorem: faulty-addresses-of-receive-certificate-next

(defthm faulty-addresses-of-receive-certificate-next
  (implies
       (receive-certificate-possiblep msg systate)
       (b* ((?new-systate (receive-certificate-next msg systate)))
         (equal (faulty-addresses new-systate)
                (faulty-addresses systate)))))

Theorem: validator-state->dag-of-receive-certificate-next

(defthm validator-state->dag-of-receive-certificate-next
 (implies
  (receive-certificate-possiblep msg systate)
  (b* ((?new-systate (receive-certificate-next msg systate)))
   (equal
        (validator-state->dag (get-validator-state val new-systate))
        (validator-state->dag (get-validator-state val systate))))))

Theorem: validator-state->buffer-of-receive-certificate-next

(defthm validator-state->buffer-of-receive-certificate-next
 (implies
  (and (in val (correct-addresses systate))
       (receive-certificate-possiblep msg systate))
  (b* ((?new-systate (receive-certificate-next msg systate)))
   (equal
    (validator-state->buffer (get-validator-state val new-systate))
    (if
     (equal val (message->destination msg))
     (insert
        (message->certificate msg)
        (validator-state->buffer (get-validator-state val systate)))
     (validator-state->buffer
          (get-validator-state val systate)))))))

Theorem: validator-state->endorsed-of-receive-certificate-next

(defthm validator-state->endorsed-of-receive-certificate-next
 (implies
  (receive-certificate-possiblep msg systate)
  (b* ((?new-systate (receive-certificate-next msg systate)))
   (equal
    (validator-state->endorsed
         (get-validator-state val new-systate))
    (if
     (equal (address-fix val)
            (message->destination msg))
     (delete
      (make-address+pos
           :address (certificate->author (message->certificate msg))
           :pos (certificate->round (message->certificate msg)))
      (validator-state->endorsed (get-validator-state val systate)))
     (validator-state->endorsed
          (get-validator-state val systate)))))))

Theorem: validator-state->last-of-receive-certificate-next

(defthm validator-state->last-of-receive-certificate-next
 (implies
  (receive-certificate-possiblep msg systate)
  (b* ((?new-systate (receive-certificate-next msg systate)))
   (equal
       (validator-state->last (get-validator-state val new-systate))
       (validator-state->last (get-validator-state val systate))))))

Theorem: validator-state->blockchain-of-receive-certificate-next

(defthm validator-state->blockchain-of-receive-certificate-next
  (implies
       (receive-certificate-possiblep msg systate)
       (b* ((?new-systate (receive-certificate-next msg systate)))
         (equal (validator-state->blockchain
                     (get-validator-state val new-systate))
                (validator-state->blockchain
                     (get-validator-state val systate))))))

Theorem: validator-state->committed-of-receive-certificate-next

(defthm validator-state->committed-of-receive-certificate-next
  (implies
       (receive-certificate-possiblep msg systate)
       (b* ((?new-systate (receive-certificate-next msg systate)))
         (equal (validator-state->committed
                     (get-validator-state val new-systate))
                (validator-state->committed
                     (get-validator-state val systate))))))

Theorem: get-network-state-of-receive-certificate-next

(defthm get-network-state-of-receive-certificate-next
  (b* ((?new-systate (receive-certificate-next msg systate)))
    (equal (get-network-state new-systate)
           (delete (message-fix msg)
                   (get-network-state systate)))))

Theorem: receive-certificate-next-of-message-fix-msg

(defthm receive-certificate-next-of-message-fix-msg
  (equal (receive-certificate-next (message-fix msg)
                                   systate)
         (receive-certificate-next msg systate)))

Theorem: receive-certificate-next-message-equiv-congruence-on-msg

(defthm receive-certificate-next-message-equiv-congruence-on-msg
  (implies (message-equiv msg msg-equiv)
           (equal (receive-certificate-next msg systate)
                  (receive-certificate-next msg-equiv systate)))
  :rule-classes :congruence)

Theorem: receive-certificate-next-of-system-state-fix-systate

(defthm receive-certificate-next-of-system-state-fix-systate
  (equal (receive-certificate-next msg (system-state-fix systate))
         (receive-certificate-next msg systate)))

Theorem: receive-certificate-next-system-state-equiv-congruence-on-systate

(defthm
  receive-certificate-next-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (receive-certificate-next msg systate)
                  (receive-certificate-next msg systate-equiv)))
  :rule-classes :congruence)