		Search-engine friendly clone of the ACL2 documentation.

Transitions-create

Create-endorser-next

New correct endorser state resulting from a create event.

Signature
(create-endorser-next cert vstate) → new-vstate
Arguments: cert — Guard (certificatep cert).; vstate — Guard (validator-statep vstate).
Returns: new-vstate — Type (validator-statep new-vstate).

The input cert of this function is the certificate in the create event; see event. The input vstate is the state of the validator whose address is endorser. See the (indirect) callers of this function.

The author-round pair of the certificate is added to the set of endorsed author-round pairs.

Definitions and Theorems

Function: create-endorser-next

(defun create-endorser-next (cert vstate)
 (declare (xargs :guard (and (certificatep cert)
                             (validator-statep vstate))))
 (let ((__function__ 'create-endorser-next))
  (declare (ignorable __function__))
  (b*
   (((certificate cert) cert)
    (endorsed (validator-state->endorsed vstate))
    (new-endorsed
       (insert (make-address+pos :address (certificate->author cert)
                                 :pos (certificate->round cert))
               endorsed)))
   (change-validator-state vstate
                           :endorsed new-endorsed))))

Theorem: validator-statep-of-create-endorser-next

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

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

(defthm validator-state->round-of-create-endorser-next
  (b* ((?new-vstate (create-endorser-next cert vstate)))
    (equal (validator-state->round new-vstate)
           (validator-state->round vstate))))

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

(defthm validator-state->dag-of-create-endorser-next
  (b* ((?new-vstate (create-endorser-next cert vstate)))
    (equal (validator-state->dag new-vstate)
           (validator-state->dag vstate))))

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

(defthm validator-state->endorsed-of-create-endorser-next
 (b* ((?new-vstate (create-endorser-next cert vstate)))
  (equal
       (validator-state->endorsed new-vstate)
       (insert (make-address+pos :address (certificate->author cert)
                                 :pos (certificate->round cert))
               (validator-state->endorsed vstate)))))

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

(defthm validator-state->last-of-create-endorser-next
  (b* ((?new-vstate (create-endorser-next cert vstate)))
    (equal (validator-state->last new-vstate)
           (validator-state->last vstate))))

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

(defthm validator-state->blockchain-of-create-endorser-next
  (b* ((?new-vstate (create-endorser-next cert vstate)))
    (equal (validator-state->blockchain new-vstate)
           (validator-state->blockchain vstate))))

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

(defthm validator-state->committed-of-create-endorser-next
  (b* ((?new-vstate (create-endorser-next cert vstate)))
    (equal (validator-state->committed new-vstate)
           (validator-state->committed vstate))))

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

(defthm create-endorser-next-of-certificate-fix-cert
  (equal (create-endorser-next (certificate-fix cert)
                               vstate)
         (create-endorser-next cert vstate)))

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

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

Theorem: create-endorser-next-of-validator-state-fix-vstate

(defthm create-endorser-next-of-validator-state-fix-vstate
  (equal (create-endorser-next cert (validator-state-fix vstate))
         (create-endorser-next cert vstate)))

Theorem: create-endorser-next-validator-state-equiv-congruence-on-vstate

(defthm
    create-endorser-next-validator-state-equiv-congruence-on-vstate
  (implies (validator-state-equiv vstate vstate-equiv)
           (equal (create-endorser-next cert vstate)
                  (create-endorser-next cert vstate-equiv)))
  :rule-classes :congruence)