		Search-engine friendly clone of the ACL2 documentation.

Last-anchor-def-and-init

Last-anchor

Last committed anchor in a validator state.

Signature
(last-anchor vstate all-vals) → anchor?
Arguments: vstate — Guard (validator-statep vstate).; all-vals — Guard (address-setp all-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. The validator must be able to calculate the active committee for the last committed round, 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 all-vals)
 (declare (xargs :guard (and (validator-statep vstate)
                             (address-setp all-vals))))
 (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 all-vals))
       ((unless commtt) nil)
       (leader (leader-at-round vstate.last commtt)))
    (certificate-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 all-vals)))
    (certificate-optionp anchor?))
  :rule-classes :rewrite)

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

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

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

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

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

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

Theorem: last-anchor-in-dag

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

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

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

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

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

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 all-vals)
                  (last-anchor vstate-equiv all-vals)))
  :rule-classes :congruence)

Theorem: last-anchor-of-address-set-fix-all-vals

(defthm last-anchor-of-address-set-fix-all-vals
  (equal (last-anchor vstate (address-set-fix all-vals))
         (last-anchor vstate all-vals)))

Theorem: last-anchor-address-set-equiv-congruence-on-all-vals

(defthm last-anchor-address-set-equiv-congruence-on-all-vals
  (implies (address-set-equiv all-vals all-vals-equiv)
           (equal (last-anchor vstate all-vals)
                  (last-anchor vstate all-vals-equiv)))
  :rule-classes :congruence)