New correct endorser state
resulting from a
(create-endorser-next cert vstate) → new-vstate
The input
The author-round pair of the certificate is added to the set of endorsed author-round pairs.
Function:
(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 cert.author :pos cert.round) endorsed))) (change-validator-state vstate :endorsed new-endorsed))))
Theorem:
(defthm validator-statep-of-create-endorser-next (b* ((new-vstate (create-endorser-next cert vstate))) (validator-statep new-vstate)) :rule-classes :rewrite)
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(defthm create-endorser-next-of-certificate-fix-cert (equal (create-endorser-next (certificate-fix cert) vstate) (create-endorser-next cert vstate)))
Theorem:
(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:
(defthm create-endorser-next-of-validator-state-fix-vstate (equal (create-endorser-next cert (validator-state-fix vstate)) (create-endorser-next cert vstate)))
Theorem:
(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)