		Search-engine friendly clone of the ACL2 documentation.

Operations-author-round-pairs

Add-endorsed

Add an author-round pair to the set of endorsed pairs of all the correct validators in a given set of endorsers.

Signature
(add-endorsed endorsers author round systate) → new-systate
Arguments: endorsers — Guard (address-setp endorsers).; author — Guard (addressp author).; round — Guard (posp round).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

When a new certificate is created by a (correct or faulty) validator, it must have been signed by the validators whose addresses are in the endorsers component of the certificate. As discussed in signers-do-not-have-author+round-p, this signing must leave a record in the state of correct validators, in the form of an author-round pair added to the set of such pairs. This addition is described by this ACL2 function: we go through all the endorsers, and if correct, we add the pair to their set.

Definitions and Theorems

Function: add-endorsed

(defun add-endorsed (endorsers author round systate)
 (declare (xargs :guard (and (address-setp endorsers)
                             (addressp author)
                             (posp round)
                             (system-statep systate))))
 (declare (xargs :guard (subset endorsers (all-addresses systate))))
 (let ((__function__ 'add-endorsed))
  (declare (ignorable __function__))
  (b*
   (((when (emptyp endorsers))
     (system-state-fix systate))
    (endorser (head endorsers))
    (vstate (get-validator-state endorser systate))
    (systate
       (if vstate
           (b* ((new-vstate (add-endorsed-val author round vstate)))
             (update-validator-state endorser new-vstate systate))
         systate)))
   (add-endorsed (tail endorsers)
                 author round systate))))

Theorem: system-statep-of-add-endorsed

(defthm system-statep-of-add-endorsed
  (b* ((new-systate (add-endorsed endorsers author round systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: add-endorsed-of-system-state-fix-systate

(defthm add-endorsed-of-system-state-fix-systate
  (equal (add-endorsed endorsers
                       author round (system-state-fix systate))
         (add-endorsed endorsers author round systate)))

Theorem: add-endorsed-system-state-equiv-congruence-on-systate

(defthm add-endorsed-system-state-equiv-congruence-on-systate
  (implies
       (system-state-equiv systate systate-equiv)
       (equal (add-endorsed endorsers author round systate)
              (add-endorsed endorsers author round systate-equiv)))
  :rule-classes :congruence)

Theorem: get-network-state-of-add-endorsed

(defthm get-network-state-of-add-endorsed
  (b* ((?new-systate (add-endorsed endorsers author round systate)))
    (equal (get-network-state new-systate)
           (get-network-state systate))))

Theorem: all-addresses-of-add-endorsed

(defthm all-addresses-of-add-endorsed
 (implies
  (subset endorsers (all-addresses systate))
  (b* ((?new-systate (add-endorsed endorsers author round systate)))
    (equal (all-addresses new-systate)
           (all-addresses systate)))))

Theorem: correct-addresses-of-add-endorsed

(defthm correct-addresses-of-add-endorsed
 (implies
  (subset endorsers (all-addresses systate))
  (b* ((?new-systate (add-endorsed endorsers author round systate)))
    (equal (correct-addresses new-systate)
           (correct-addresses systate)))))

Theorem: validator-state->round-of-add-endorsed

(defthm validator-state->round-of-add-endorsed
 (equal (validator-state->round
             (get-validator-state
                  val
                  (add-endorsed endorsers author round systate)))
        (validator-state->round (get-validator-state val systate))))

Theorem: validator-state->dag-of-add-endorsed

(defthm validator-state->dag-of-add-endorsed
  (equal (validator-state->dag
              (get-validator-state
                   val
                   (add-endorsed endorsers author round systate)))
         (validator-state->dag (get-validator-state val systate))))

Theorem: validator-state->buffer-of-add-endorsed

(defthm validator-state->buffer-of-add-endorsed
  (equal
       (validator-state->buffer
            (get-validator-state
                 val
                 (add-endorsed endorsers author round systate)))
       (validator-state->buffer (get-validator-state val systate))))

Theorem: validator-state->endorsed-of-add-endorsed

(defthm validator-state->endorsed-of-add-endorsed
 (equal
  (validator-state->endorsed
       (get-validator-state
            val
            (add-endorsed endorsers author round systate)))
  (if
   (and (in val endorsers)
        (in val (correct-addresses systate)))
   (insert
      (address+pos author round)
      (validator-state->endorsed (get-validator-state val systate)))
   (validator-state->endorsed (get-validator-state val systate)))))

Theorem: validator-state->last-of-add-endorsed

(defthm validator-state->last-of-add-endorsed
 (implies
   (in val (correct-addresses systate))
   (equal
        (validator-state->last
             (get-validator-state
                  val
                  (add-endorsed endorsers author round systate)))
        (validator-state->last (get-validator-state val systate)))))

Theorem: validator-state->blockchain-of-add-endorsed

(defthm validator-state->blockchain-of-add-endorsed
 (implies
    (in val (correct-addresses systate))
    (equal (validator-state->blockchain
                (get-validator-state
                     val
                     (add-endorsed endorsers author round systate)))
           (validator-state->blockchain
                (get-validator-state val systate)))))

Theorem: validator-state->committed-of-add-endorsed

(defthm validator-state->committed-of-add-endorsed
 (implies
  (in val (correct-addresses systate))
  (equal
   (validator-state->committed
        (get-validator-state
             val
             (add-endorsed endorsers author round systate)))
   (validator-state->committed (get-validator-state val systate)))))