		Search-engine friendly clone of the ACL2 documentation.

Operations-anchors

Last-anchor

Last committed anchor in a validator state.

Signature
(last-anchor vstate vals) → anchor?
Arguments: vstate — Guard (validator-statep vstate).; vals — Guard (address-setp vals).
Returns: anchor? — Type (certificate-optionp anchor?).

A validator state includes a component with the latest committed round number (or 0 if no rounds have been committed yet). We return the certificate at that round authored by the leader of that round, if such a certificate is in the DAG; if the certificate is absent, we return nil. If no round has been committed yet, we also return nil.

Definitions and Theorems

Function: last-anchor

(defun last-anchor (vstate vals)
  (declare (xargs :guard (and (validator-statep vstate)
                              (address-setp vals))))
  (declare
       (xargs :guard (and (not (emptyp vals))
                          (evenp (validator-state->last vstate)))))
  (let ((__function__ 'last-anchor))
    (declare (ignorable __function__))
    (b* (((validator-state vstate) vstate)
         ((when (equal vstate.last 0)) nil)
         (leader (leader-at-round vstate.last vals)))
      (cert-with-author+round leader vstate.last vstate.dag))))

Theorem: certificate-optionp-of-last-anchor

(defthm certificate-optionp-of-last-anchor
  (b* ((anchor? (last-anchor vstate vals)))
    (certificate-optionp anchor?))
  :rule-classes :rewrite)

Theorem: certificate->author-of-last-anchor

(defthm certificate->author-of-last-anchor
  (implies (last-anchor vstate vals)
           (equal (certificate->author (last-anchor vstate vals))
                  (leader-at-round (validator-state->last vstate)
                                   vals))))

Theorem: certificate->round-of-last-anchor

(defthm certificate->round-of-last-anchor
  (implies (last-anchor vstate vals)
           (equal (certificate->round (last-anchor vstate vals))
                  (validator-state->last vstate))))

Theorem: last-anchor-in-dag

(defthm last-anchor-in-dag
  (implies (last-anchor vstate vals)
           (in (last-anchor vstate vals)
               (validator-state->dag vstate))))