• Top

• Last-anchor-def-and-init

Last-anchor

Last committed anchor in a validator state.

Signature

(last-anchor vstate) → anchor?

Arguments

vstate — Guard (validator-statep vstate).

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. The validator must be able to calculate the active committee for the last committed round, and the committee must be non-empty, in order to calculate the leader; we return nil if the validator cannot calculate that committee.

Definitions and Theorems

Function: last-anchor

(defun last-anchor (vstate)
 (declare (xargs :guard (validator-statep vstate)))
 (let ((__function__ 'last-anchor))
   (declare (ignorable __function__))
   (b*
    (((validator-state vstate) vstate)
     ((when (equal vstate.last 0)) nil)
     (commtt
          (active-committee-at-round vstate.last vstate.blockchain))
     ((unless commtt) nil)
     ((unless (committee-nonemptyp commtt))
      nil)
     (leader (leader-at-round vstate.last commtt)))
    (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)))
    (certificate-optionp anchor?))
  :rule-classes :rewrite)

Theorem: last-not-0-when-last-anchor

(defthm last-not-0-when-last-anchor
  (implies (last-anchor vstate)
           (not (equal (validator-state->last vstate)
                       0))))

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

(defthm certificate->author-of-last-anchor
 (implies
    (last-anchor vstate)
    (equal (certificate->author (last-anchor vstate))
           (b* ((commtt (active-committee-at-round
                             (validator-state->last vstate)
                             (validator-state->blockchain vstate))))
             (leader-at-round (validator-state->last vstate)
                              commtt)))))

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

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

Theorem: last-anchor-in-dag

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

Theorem: active-committee-at-round-when-last-anchor

(defthm active-committee-at-round-when-last-anchor
 (implies
  (last-anchor vstate)
  (active-committee-at-round (validator-state->last vstate)
                             (validator-state->blockchain vstate))))

Theorem: last-anchor-of-validator-state-fix-vstate

(defthm last-anchor-of-validator-state-fix-vstate
  (equal (last-anchor (validator-state-fix vstate))
         (last-anchor vstate)))

Theorem: last-anchor-validator-state-equiv-congruence-on-vstate

(defthm last-anchor-validator-state-equiv-congruence-on-vstate
  (implies (validator-state-equiv vstate vstate-equiv)
           (equal (last-anchor vstate)
                  (last-anchor vstate-equiv)))
  :rule-classes :congruence)