		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).

If the validator is faulty, the endorsement messages are removed from the network, because they are consumed.

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 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))
     ((when (not (in prop.author
                     (correct-addresses systate))))
      (b*
       ((old-msgs (make-endorsement-messages prop cert.endorsers))
        (new-network (union new-msgs (difference network old-msgs)))
        (systate (update-network-state new-network 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))
     (new-network (union new-msgs network))
     (systate (update-network-state new-network 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)
      (if (in (certificate->author cert)
              (correct-addresses systate))
          (union (make-certificate-messages cert dests)
                 (get-network-state systate))
        (union (make-certificate-messages cert dests)
               (difference (get-network-state systate)
                           (make-endorsement-messages
                                (certificate->proposal cert)
                                (certificate->endorsers cert))))))))

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)