		Search-engine friendly clone of the ACL2 documentation.

Transitions-certify

Certify-next

New system state resulting from a certify event.

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

The cert and dests parameters of this function are the corresponding components of the certify event.

If the validator is correct, the proposal is removed from the map of pending proposals, and the certificate is added to the DAG.

Whether the validator is correct or faulty, a message with the certificate is added to the network, for each of the destinations indicated in the event.

Definitions and Theorems

Function: certify-next

(defun certify-next (cert dests systate)
 (declare (xargs :guard (and (certificatep cert)
                             (address-setp dests)
                             (system-statep systate))))
 (declare (xargs :guard (certify-possiblep cert dests systate)))
 (let ((__function__ 'certify-next))
   (declare (ignorable __function__))
   (b*
     (((certificate cert) cert)
      ((proposal prop) cert.proposal)
      (network (get-network-state systate))
      (new-msgs (make-certificate-messages cert dests))
      (new-network (union new-msgs network))
      (systate (update-network-state new-network systate))
      ((when (not (in prop.author
                      (correct-addresses systate))))
       systate)
      ((validator-state vstate)
       (get-validator-state prop.author systate))
      (new-proposed (omap::delete prop vstate.proposed))
      (new-dag (insert (certificate-fix cert)
                       vstate.dag))
      (new-vstate (change-validator-state vstate
                                          :proposed new-proposed
                                          :dag new-dag))
      (systate
           (update-validator-state prop.author new-vstate systate)))
     systate)))

Theorem: system-statep-of-certify-next

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

Theorem: correct-addresses-of-certify-next

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

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

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

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

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

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

(defthm validator-state->proposed-of-certify-next
 (b* ((?new-systate (certify-next cert dests systate)))
  (equal
   (validator-state->proposed (get-validator-state val new-systate))
   (if
    (and (equal (address-fix val)
                (certificate->author cert))
         (in (address-fix val)
             (correct-addresses systate)))
    (omap::delete
      (certificate->proposal cert)
      (validator-state->proposed (get-validator-state val systate)))
    (validator-state->proposed
         (get-validator-state val systate))))))

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

(defthm validator-state->endorsed-of-certify-next
 (b* ((?new-systate (certify-next cert dests systate)))
  (equal
   (validator-state->endorsed (get-validator-state val new-systate))
   (validator-state->endorsed (get-validator-state val systate)))))

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

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

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

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

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

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

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

(defthm get-network-state-of-certify-next
  (b* ((?new-systate (certify-next cert dests systate)))
    (equal (get-network-state new-systate)
           (union (make-certificate-messages cert dests)
                  (get-network-state systate)))))

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

(defthm certify-next-of-certificate-fix-cert
  (equal (certify-next (certificate-fix cert)
                       dests systate)
         (certify-next cert dests systate)))

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

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

Theorem: certify-next-of-address-set-fix-dests

(defthm certify-next-of-address-set-fix-dests
  (equal (certify-next cert (address-set-fix dests)
                       systate)
         (certify-next cert dests systate)))

Theorem: certify-next-address-set-equiv-congruence-on-dests

(defthm certify-next-address-set-equiv-congruence-on-dests
  (implies (address-set-equiv dests dests-equiv)
           (equal (certify-next cert dests systate)
                  (certify-next cert dests-equiv systate)))
  :rule-classes :congruence)

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

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

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

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