		Search-engine friendly clone of the ACL2 documentation.

Transitions-create

Create-next

New system state resulting from a create event.

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

The input cert of this function is the certificate in the create event; see event.

If the author is correct, its state is updated using create-author-next.

The states of the correct endorsers are updated using create-endorsers-next; this only affects correct endorsers, since we only explicitly model the state of correct validators.

The certificate is broadcast to all the correct validators, except for the author if correct. This is realized by adding to the network one message for each correct validator as destination (except the author if correct), all containing the certificate. The deletion (via delete) of the certificate's author from the set of all correct validators has no effect if the certtificate's author is faulty, as appropriate.

It may seems strange that the messages are sent only to correct validators, since a validator does not know which validators are correct or faulty. An AleoBFT implementation would send them to all validators, but faulty validators behave arbitrarily regardless of which messages they receive. Thus, in our model of AleoBFT, we ignore messages sent to faulty validators by only adding to the network messages sent to correct validators. After all, recall again that our system model only explicitly includes correct, not faulty, validators.

It may also seem strange that the messages are sent to all the (correct) validators in the system, and not just the ones in the committee. An AleoBFT implementation would only send them to the committee. However, as explained in system-states, our model of AleoBFT implicitly models syncing by including all possible validators in the system, and by having all of them update their internal states based on certificates generated by the active committee. This is way our model adds to the network messages to all validators: in this modeling approach, it is in fact critical that the certificate is broadcast not just to the committees, but to all the validators.

In our model, adding a message to the network implies that the message can always be eventually delivered, i.e. it is never lost. This matches the typical assumption, in the BFT literature, of eventually reliable, and authenticated, network connections. The authentication comes from the fact that the certificate in the message includes the author, which is also the sender. There is no event, in our model, to drop or modify messages in the network. They can only be added, and removed when delivered to validators. In an implementation, this kind of network behavior can be realized via encryption and re-transmissions on top of TCP/IP; the extent to which this actually realizes the network assumptions should be subjected to more rigorous study, but for now we accept this assumption as realistic, which is customary in the BFT literature.

If a certificate is authored by a faulty validator, the validator may not send the certificate to any validator, but in this case it is as if no certificate creation takes place: we do not model the internal state of faulty validators; we are only concerned with the effects that faulty validator's messages can have on correct validators.

If a faulty validator authors a certificate, the validator may only send it to some validators, not all of them. If it only sends it to faulty validators, then again it is as if the certificate creation never happened. If it sends it to at least one correct validator, the correct validator will be able to send it to other correct validators, and eventually all correct validators should have it: this is the underlying reliable broadcast assumption, which in our model is represented simply by the way we model the network and how messages are added and removed.

Definitions and Theorems

Function: create-next

(defun create-next (cert systate)
 (declare (xargs :guard (and (certificatep cert)
                             (system-statep systate))))
 (declare (xargs :guard (create-possiblep cert systate)))
 (let ((__function__ 'create-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-author-next cert vstate)))
            (update-validator-state cert.author new-vstate systate))
        systate))
    (systate (create-endorsers-next cert systate))
    (network (get-network-state systate))
    (msgs (make-certificate-messages
               cert
               (delete cert.author
                       (correct-addresses systate))))
    (new-network (union msgs network))
    (systate (update-network-state new-network systate)))
   systate)))

Theorem: system-statep-of-create-next

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

Theorem: correct-addresses-of-create-next

(defthm correct-addresses-of-create-next
  (b* ((?new-systate (create-next cert systate)))
    (equal (correct-addresses new-systate)
           (correct-addresses systate))))

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

(defthm validator-state->round-of-create-next
 (b* ((?new-systate (create-next cert systate)))
  (equal
      (validator-state->round (get-validator-state val new-systate))
      (validator-state->round (get-validator-state val systate)))))

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

(defthm validator-state->dag-of-create-next
 (implies
  (in val (correct-addresses systate))
  (b* ((?new-systate (create-next cert systate)))
   (equal
     (validator-state->dag (get-validator-state val new-systate))
     (if
      (equal val (certificate->author cert))
      (insert
           (certificate-fix cert)
           (validator-state->dag (get-validator-state val systate)))
      (validator-state->dag (get-validator-state val systate)))))))

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

(defthm validator-state->endorsed-of-create-next
 (implies
  (in val (correct-addresses systate))
  (b* ((?new-systate (create-next cert systate)))
   (equal
    (validator-state->endorsed
         (get-validator-state val new-systate))
    (if
     (in val (certificate->endorsers cert))
     (insert
      (make-address+pos :address (certificate->author cert)
                        :pos (certificate->round cert))
      (validator-state->endorsed (get-validator-state val systate)))
     (validator-state->endorsed
          (get-validator-state val systate)))))))

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

(defthm validator-state->last-of-create-next
 (b* ((?new-systate (create-next cert systate)))
  (equal
       (validator-state->last (get-validator-state val new-systate))
       (validator-state->last (get-validator-state val systate)))))

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

(defthm validator-state->blockchain-of-create-next
  (b* ((?new-systate (create-next cert systate)))
    (equal (validator-state->blockchain
                (get-validator-state val new-systate))
           (validator-state->blockchain
                (get-validator-state val systate)))))

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

(defthm validator-state->committed-of-create-next
 (b* ((?new-systate (create-next cert systate)))
  (equal
   (validator-state->committed
        (get-validator-state val new-systate))
   (validator-state->committed (get-validator-state val systate)))))

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

(defthm get-network-state-of-create-next
  (b* ((?new-systate (create-next cert systate)))
    (equal (get-network-state new-systate)
           (union (get-network-state systate)
                  (make-certificate-messages
                       cert
                       (delete (certificate->author cert)
                               (correct-addresses systate)))))))

Theorem: create-next-of-certificate-fix-cert

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

Theorem: create-next-certificate-equiv-congruence-on-cert

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

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

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

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

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