		Search-engine friendly clone of the ACL2 documentation.

Committed-anchors-sequences

Committed-anchors

Sequence of anchors committed by a validator.

Signature
(committed-anchors vstate) → anchors
Arguments: vstate — Guard (validator-statep vstate).
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 latest one is the car of the list).

Definitions and Theorems

Function: committed-anchors

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

Theorem: certificate-listp-of-committed-anchors

(defthm certificate-listp-of-committed-anchors
  (b* ((anchors (committed-anchors vstate)))
    (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) 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)))
  :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))
           (equal (car (committed-anchors vstate))
                  (last-anchor vstate))))

Theorem: certificates-dag-paths-p-of-committed-anchors

(defthm certificates-dag-paths-p-of-committed-anchors
  (implies
       (or (equal (validator-state->last vstate) 0)
           (in (last-anchor vstate)
               (validator-state->dag vstate)))
       (b* ((?anchors (committed-anchors vstate)))
         (certificates-dag-paths-p anchors
                                   (validator-state->dag vstate)))))

Theorem: committed-anchors-of-validator-state-fix-vstate

(defthm committed-anchors-of-validator-state-fix-vstate
  (equal (committed-anchors (validator-state-fix vstate))
         (committed-anchors vstate)))

Theorem: committed-anchors-validator-state-equiv-congruence-on-vstate

(defthm committed-anchors-validator-state-equiv-congruence-on-vstate
  (implies (validator-state-equiv vstate vstate-equiv)
           (equal (committed-anchors vstate)
                  (committed-anchors vstate-equiv)))
  :rule-classes :congruence)