		Search-engine friendly clone of the ACL2 documentation.

Last-anchor-voters-def-and-init-and-next

Validator-last-anchor-voters-p

Check if a validator state satisfies the invariant.

Signature
(validator-last-anchor-voters-p vstate) → yes/no
Arguments: vstate — Guard (validator-statep vstate).
Returns: yes/no — Type (booleanp yes/no).

Either the last committed round is 0, or the committee at the next round can be calculated and the total stake of the successors of the last anchor is more than f, where f is the maximum stake of faulty validators in the committee.

The fact that the last anchor is present is in the guard, but in last-anchor-voters-p it is established from the previously proved invariant last-anchor-present-p. The guard also includes conditions ensuring that the validator can calculate committees at all rounds with certificates (and in particular the comittee at the round just after the last committed, if the anchor has any successors), and that the authors of all the certificates in a round are members of the committee at that round (and in particular the successors of the anchor, if any, are members of the committee at their round); these guard conditions are established, in last-anchor-voters-p, via previously proved invariants used as guards there.

Definitions and Theorems

Function: validator-last-anchor-voters-p

(defun validator-last-anchor-voters-p (vstate)
 (declare (xargs :guard (validator-statep vstate)))
 (declare
  (xargs
   :guard
   (and
       (or (equal (validator-state->last vstate) 0)
           (last-anchor vstate))
       (dag-has-committees-p (validator-state->dag vstate)
                             (validator-state->blockchain vstate))
       (dag-in-committees-p (validator-state->dag vstate)
                            (validator-state->blockchain vstate)))))
 (let ((__function__ 'validator-last-anchor-voters-p))
  (declare (ignorable __function__))
  (b* (((validator-state vstate) vstate)
       ((when (equal vstate.last 0)) t)
       (commtt (active-committee-at-round (1+ vstate.last)
                                          vstate.blockchain)))
   (and
      commtt
      (> (committee-members-stake
              (cert-set->author-set (successors (last-anchor vstate)
                                                vstate.dag))
              commtt)
         (committee-max-faulty-stake commtt))))))

Theorem: booleanp-of-validator-last-anchor-voters-p

(defthm booleanp-of-validator-last-anchor-voters-p
  (b* ((yes/no (validator-last-anchor-voters-p vstate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

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

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

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