		Search-engine friendly clone of the ACL2 documentation.

Operations-anchors

Committed-anchors

Sequence of anchors committed by a validator.

Signature
(committed-anchors vstate vals) → anchors
Arguments: vstate — Guard (validator-statep vstate).; vals — Guard (address-setp vals).
Returns: anchors — Type (certificate-listp anchors).

If the last committed round is 0 (i.e. there is no last committed round), no anchors have been committed, and we return nil. Otherwise, we obtain the last committed anchor, and we use collect-all-anchors starting from that one. Thus, this function gives us the list of all anchors committed so far, in reverse chronological order (i.e. the last one come first in the list).

Definitions and Theorems

Function: committed-anchors

(defun committed-anchors (vstate vals)
 (declare (xargs :guard (and (validator-statep vstate)
                             (address-setp vals))))
 (declare
     (xargs :guard (and (not (emptyp vals))
                        (evenp (validator-state->last vstate))
                        (or (equal (validator-state->last vstate) 0)
                            (last-anchor vstate vals)))))
 (let ((__function__ 'committed-anchors))
   (declare (ignorable __function__))
   (b* (((validator-state vstate) vstate)
        ((when (equal vstate.last 0)) nil)
        (last-anchor (last-anchor vstate vals)))
     (collect-all-anchors last-anchor vstate.dag vals))))

Theorem: certificate-listp-of-committed-anchors

(defthm certificate-listp-of-committed-anchors
  (b* ((anchors (committed-anchors vstate vals)))
    (certificate-listp anchors))
  :rule-classes :rewrite)

Theorem: committed-anchors-when-last-is-0

(defthm committed-anchors-when-last-is-0
  (implies (equal (validator-state->last vstate) 0)
           (equal (committed-anchors vstate vals)
                  nil)))

Theorem: consp-of-committed-anchors-when-last-not-0

(defthm consp-of-committed-anchors-when-last-not-0
  (implies (not (equal (validator-state->last vstate)
                       0))
           (consp (committed-anchors vstate vals)))
  :rule-classes :type-prescription)

Theorem: car-of-committed-anchors

(defthm car-of-committed-anchors
  (implies (and (not (equal (validator-state->last vstate)
                            0))
                (last-anchor vstate vals))
           (equal (car (committed-anchors vstate vals))
                  (last-anchor vstate vals))))