		Search-engine friendly clone of the ACL2 documentation.

Previous-quorum-def-and-init-and-next

Validator-previous-quorum-p

Check if either a certificate has round 1 and it has no references to previous certificates, or the round is not 1 and the certificate's references to previous certificates are in the committee for the round just before the certificate round and form a non-zero quorum in that committee, where the committee is calculated by a validator (represented by its state).

Signature
(validator-previous-quorum-p cert vstate) → yes/no
Arguments: cert — Guard (certificatep cert).; vstate — Guard (validator-statep vstate).
Returns: yes/no — Type (booleanp yes/no).

This is used by previous-quorum-p to define our invariant. The validator whose state is vstate is the one that has the certificate in the DAG. The guard ensures that the validator can calculate the committee.

To check the non-zeroness of the quorum, we equivalently check the non-emptiness of the previous references.

We prove a theorem about the predecessors of cert, which we use to prove dag-predecessor-quorum-p from previous-quorum-p later. The theorem says that, under the invariant, for certificates after round 1, the stake of the authors of the predecessor certificates is at least the quorum stake for the committee at the previous round. This is the case under the backward closure hypothesis (which is an already proved invariant): the authors of the predecessors are exactly the previous certificate references (addresses) in the certificate. Without the backward closure hypothesis, the authors of the predecessors are the intersection of the previous reference authors and the authors of the certificates actually present in the previous round; the closure tells us the the former is a subset of the latter, which simplifies the intersection.

Definitions and Theorems

Function: validator-previous-quorum-p

(defun validator-previous-quorum-p (cert vstate)
 (declare (xargs :guard (and (certificatep cert)
                             (validator-statep vstate))))
 (declare
     (xargs :guard (or (equal (certificate->round cert) 1)
                       (active-committee-at-round
                            (1- (certificate->round cert))
                            (validator-state->blockchain vstate)))))
 (let ((__function__ 'validator-previous-quorum-p))
   (declare (ignorable __function__))
   (b* (((validator-state vstate) vstate)
        ((certificate cert) cert))
     (if (= cert.round 1)
         (emptyp cert.previous)
       (b* ((commtt (active-committee-at-round (1- cert.round)
                                               vstate.blockchain)))
         (and (not (emptyp cert.previous))
              (subset cert.previous
                      (committee-members commtt))
              (>= (committee-members-stake cert.previous commtt)
                  (committee-quorum-stake commtt))))))))

Theorem: booleanp-of-validator-previous-quorum-p

(defthm booleanp-of-validator-previous-quorum-p
  (b* ((yes/no (validator-previous-quorum-p cert vstate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: predecessor-quorum-when-validator-previous-quorum-p

(defthm predecessor-quorum-when-validator-previous-quorum-p
 (implies
  (and (validator-previous-quorum-p cert vstate)
       (certificate-previous-in-dag-p
            cert (validator-state->dag vstate))
       (not (equal (certificate->round cert) 1)))
  (b*
   ((commtt (active-committee-at-round
                 (1- (certificate->round cert))
                 (validator-state->blockchain vstate)))
    (stake
        (committee-members-stake
             (certificate-set->author-set
                  (predecessors cert (validator-state->dag vstate)))
             commtt)))
   (and (> stake 0)
        (>= stake
            (committee-quorum-stake commtt))))))

Theorem: validator-previous-quorum-p-of-certificate-fix-cert

(defthm validator-previous-quorum-p-of-certificate-fix-cert
  (equal (validator-previous-quorum-p (certificate-fix cert)
                                      vstate)
         (validator-previous-quorum-p cert vstate)))

Theorem: validator-previous-quorum-p-certificate-equiv-congruence-on-cert

(defthm
   validator-previous-quorum-p-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (validator-previous-quorum-p cert vstate)
                  (validator-previous-quorum-p cert-equiv vstate)))
  :rule-classes :congruence)

Theorem: validator-previous-quorum-p-of-validator-state-fix-vstate

(defthm validator-previous-quorum-p-of-validator-state-fix-vstate
 (equal
     (validator-previous-quorum-p cert (validator-state-fix vstate))
     (validator-previous-quorum-p cert vstate)))

Theorem: validator-previous-quorum-p-validator-state-equiv-congruence-on-vstate

(defthm
 validator-previous-quorum-p-validator-state-equiv-congruence-on-vstate
 (implies (validator-state-equiv vstate vstate-equiv)
          (equal (validator-previous-quorum-p cert vstate)
                 (validator-previous-quorum-p cert vstate-equiv)))
 :rule-classes :congruence)