		Search-engine friendly clone of the ACL2 documentation.

Dag-previous-quorum-def-and-init-and-next

Validator-dag-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-dag-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 dag-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 dag-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-dag-previous-quorum-p

(defun validator-dag-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-dag-previous-quorum-p))
  (declare (ignorable __function__))
  (b* (((validator-state vstate) vstate)
       ((certificate cert) cert))
   (if (= (certificate->round cert) 1)
       (emptyp (certificate->previous cert))
    (b*
     ((commtt
           (active-committee-at-round (1- (certificate->round cert))
                                      vstate.blockchain)))
     (and (not (emptyp (certificate->previous cert)))
          (subset (certificate->previous cert)
                  (committee-members commtt))
          (>= (committee-members-stake (certificate->previous cert)
                                       commtt)
              (committee-quorum-stake commtt))))))))

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

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

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

(defthm predecessor-quorum-when-validator-dag-previous-quorum-p
 (implies
  (and (validator-dag-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
             (cert-set->author-set
                  (predecessors cert (validator-state->dag vstate)))
             commtt)))
   (and (> stake 0)
        (>= stake
            (committee-quorum-stake commtt))))))

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

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

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

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

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

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

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

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