		Search-engine friendly clone of the ACL2 documentation.

Transitions-create-certificate

Create-certificate-next

New state resulting from a create-certificate event.

Signature
(create-certificate-next cert systate) → new-systate
Arguments: cert — Guard (certificatep cert).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

If the author of the new certificate is a correct validator, the certificate is added to the DAG of the validator. If instead the author of the new certificate is a faulty validator, there is no change to the state of the validator, which is always the indication of faulty validator.

Either way, regardless of the correctness or faultiness of the author, the certificate is reliably broadcasted to all the correct validators, by adding messages to the network consisting of the certificate and the address of all correct validators other than the author if correct; note that the removal of the author's address from the correct-addresses set has no effect if the author is a faulty validator. If the author is a correct validator, the reason for broadcasting to all the other correct validators should be obvious, since the validator follows the protocol. If the author is a faulty validator, the reason has to do with the nature of reliable broadcast, which in our model is assumed to be provided by the underlying layers: in reliable broadcast, if a correct validator receives the message, then every other correct validator must eventually receive the message. This is the case even if the faulty validator sends the message only to some of the validators, because reliable broadcast guarantees that there are enough correct validators to propagate the message to all the correct validators. So, either way, the message goes to all correct validators (except the author if correct, since it does not need it) by virtue of reliable broadcast.

There is no need to generate or even consider messages for faulty validators. They are free to behave arbitrarily anyhow (within the restrictions of reliable broadcast), and so it does not matter which messages they receive or not.

We also extend the states of the correct endorsers to record that they signed a certificate with the given author and pair.

We prove that, after this event, the set of certificates of each validator is the old set plus the new certificate. This is the case whether the certificate author is correct or faulty. If the author is correct, the certificate is added to its DAG, and messages with the certificate are sent for all the other correct validators. If the author is faulty, messages with that certificate are sent to all correct validators; this is the reliable broadcast assumption underlying the model. The addition of the new certificate affects all correct validators, not just the author (if correct). This is the only event that adds a certificate to the set of certificates for (each correct) validator.

Definitions and Theorems

Function: create-certificate-next-val

(defun create-certificate-next-val (cert vstate)
  (declare (xargs :guard (and (certificatep cert)
                              (validator-statep vstate))))
  (let ((__function__ 'create-certificate-next-val))
    (declare (ignorable __function__))
    (b* ((dag (validator-state->dag vstate))
         (new-dag (insert cert dag)))
      (change-validator-state vstate
                              :dag new-dag))))

Theorem: validator-statep-of-create-certificate-next-val

(defthm validator-statep-of-create-certificate-next-val
  (b* ((new-vstate (create-certificate-next-val cert vstate)))
    (validator-statep new-vstate))
  :rule-classes :rewrite)

Function: create-certificate-next

(defun create-certificate-next (cert systate)
 (declare (xargs :guard (and (certificatep cert)
                             (system-statep systate))))
 (declare
      (xargs :guard (create-certificate-possiblep cert systate)))
 (let ((__function__ 'create-certificate-next))
  (declare (ignorable __function__))
  (b*
   (((certificate cert) cert)
    (systate
      (if
        (in cert.author (correct-addresses systate))
        (b* ((vstate (get-validator-state cert.author systate))
             (new-vstate (create-certificate-next-val cert vstate)))
          (update-validator-state cert.author new-vstate systate))
        systate))
    (systate (add-endorsed cert.endorsers
                           cert.author cert.round systate))
    (network (get-network-state systate))
    (new-messages (messages-for-certificate
                       cert
                       (delete cert.author
                               (correct-addresses systate))))
    (new-network (union new-messages network)))
   (update-network-state new-network systate))))

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

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

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

(defthm create-certificate-next-of-system-state-fix-systate
  (equal (create-certificate-next cert (system-state-fix systate))
         (create-certificate-next cert systate)))

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

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

Theorem: validator-state->round-of-create-certificate-next

(defthm validator-state->round-of-create-certificate-next
 (implies
  (and (certificatep cert)
       (in val (correct-addresses systate)))
  (equal
   (validator-state->round
       (get-validator-state val
                            (create-certificate-next cert systate)))
   (validator-state->round (get-validator-state val systate)))))

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

(defthm validator-state->dag-of-create-certificate-next
 (implies
  (and (certificatep cert)
       (in val (correct-addresses systate)))
  (equal
   (validator-state->dag
       (get-validator-state val
                            (create-certificate-next cert systate)))
   (if
     (equal val (certificate->author cert))
     (insert
          cert
          (validator-state->dag (get-validator-state val systate)))
     (validator-state->dag (get-validator-state val systate))))))

Theorem: validator-state->dag-subset-create-certificate-next

(defthm validator-state->dag-subset-create-certificate-next
 (implies
  (and (in val (correct-addresses systate))
       (certificatep cert)
       (create-certificate-possiblep cert systate))
  (subset
   (validator-state->dag (get-validator-state val systate))
   (validator-state->dag
    (get-validator-state val
                         (create-certificate-next cert systate))))))

Theorem: validator-state->dag-of-create-certificate-next-same

(defthm validator-state->dag-of-create-certificate-next-same
 (implies
  (and (certificatep cert)
       (in val (correct-addresses systate))
       (not (equal val (certificate->author cert))))
  (equal
   (validator-state->dag
       (get-validator-state val
                            (create-certificate-next cert systate)))
   (validator-state->dag (get-validator-state val systate)))))

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

(defthm validator-state->buffer-of-create-certificate-next
 (implies
  (and (certificatep cert)
       (in val (correct-addresses systate)))
  (equal
   (validator-state->buffer
       (get-validator-state val
                            (create-certificate-next cert systate)))
   (validator-state->buffer (get-validator-state val systate)))))

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

(defthm validator-state->last-of-create-certificate-next
 (implies
  (in val (correct-addresses systate))
  (equal
   (validator-state->last
       (get-validator-state val
                            (create-certificate-next cert systate)))
   (validator-state->last (get-validator-state val systate)))))

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

(defthm validator-state->blockchain-of-create-certificate-next
 (implies
  (in val (correct-addresses systate))
  (equal
   (validator-state->blockchain
       (get-validator-state val
                            (create-certificate-next cert systate)))
   (validator-state->blockchain
        (get-validator-state val systate)))))

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

(defthm validator-state->committed-of-create-certificate-next
 (implies
  (in val (correct-addresses systate))
  (equal
   (validator-state->committed
       (get-validator-state val
                            (create-certificate-next cert systate)))
   (validator-state->committed (get-validator-state val systate)))))

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

(defthm get-network-state-of-create-certificate-next
 (implies
   (subset (certificate->endorsers cert)
           (all-addresses systate))
   (equal (get-network-state (create-certificate-next cert systate))
          (union (get-network-state systate)
                 (messages-for-certificate
                      cert
                      (delete (certificate->author cert)
                              (correct-addresses systate)))))))