		Search-engine friendly clone of the ACL2 documentation.

Last-anchor-present

Last-anchor-present-p

Definition of the invariant: for each correct validator, if the last committed round is not 0, there is an anchor at that round.

This predicate implicitly requires that the validator can calculate the active committee at the last committed round (if not 0), because otherwise last-anchor returns nil.

Definitions and Theorems

Theorem: last-anchor-present-p-necc

(defthm last-anchor-present-p-necc
 (implies
      (last-anchor-present-p systate)
      (implies (in val (correct-addresses systate))
               (b* ((vstate (get-validator-state val systate)))
                 (implies (not (equal (validator-state->last vstate)
                                      0))
                          (last-anchor vstate))))))

Theorem: booleanp-of-last-anchor-present-p

(defthm booleanp-of-last-anchor-present-p
  (b* ((yes/no (last-anchor-present-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: last-anchor-present-p-of-system-state-fix-systate

(defthm last-anchor-present-p-of-system-state-fix-systate
  (equal (last-anchor-present-p (system-state-fix systate))
         (last-anchor-present-p systate)))

Theorem: last-anchor-present-p-system-state-equiv-congruence-on-systate

(defthm
     last-anchor-present-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (last-anchor-present-p systate)
                  (last-anchor-present-p systate-equiv)))
  :rule-classes :congruence)