		Search-engine friendly clone of the ACL2 documentation.

Transitions-create

Create-author-next

New correct author state resulting from a create event.

Signature
(create-author-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 the certificate's author. See the (indirect) callers of this function.

The certificate is added to the DAG.

Definitions and Theorems

Function: create-author-next

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

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

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

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

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

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

(defthm validator-state->dag-of-create-author-next
  (b* ((?new-vstate (create-author-next cert vstate)))
    (equal (validator-state->dag new-vstate)
           (insert (certificate-fix cert)
                   (validator-state->dag vstate)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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