Add an author-pair to the set of endorsed pairs in the state of a correct validator.
(add-endorsed-val author round vstate) → new-vstate
This is used in add-endorsed. See the documentation of that function.
Function:
(defun add-endorsed-val (author round vstate) (declare (xargs :guard (and (addressp author) (posp round) (validator-statep vstate)))) (let ((__function__ 'add-endorsed-val)) (declare (ignorable __function__)) (b* ((endorsed (validator-state->endorsed vstate)) (new-endorsed (insert (make-address+pos :address author :pos round) endorsed))) (change-validator-state vstate :endorsed new-endorsed))))
Theorem:
(defthm validator-statep-of-add-endorsed-val (b* ((new-vstate (add-endorsed-val author round vstate))) (validator-statep new-vstate)) :rule-classes :rewrite)