		Search-engine friendly clone of the ACL2 documentation.

Dags

Dag-predecessor-quorum-p

Check if the total stake of the precedessor certificates of each certificate in a DAG at a round later than 1 is non-zero and at least the quorum of the active committee at the previous round.

The guard ensures that, for every certificate of the DAG, the active committee for the round can be calculated and the author is a member of that committee. Thus, for every certificate, all the authors of the predecessor certificates are members of the active committee for the certificate's previous round.

This is an invariant of the DAGs of validators, as proved elsewhere.

The fact that the stake is non-zero implies that there is at least one predecessor.

Definitions and Theorems

Theorem: dag-predecessor-quorum-p-necc

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

Theorem: booleanp-of-dag-predecessor-quorum-p

(defthm booleanp-of-dag-predecessor-quorum-p
  (b* ((yes/no (dag-predecessor-quorum-p dag blockchain)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: not-emptyp-predecessors-when-dag-predecessor-quorum-p

(defthm not-emptyp-predecessors-when-dag-predecessor-quorum-p
  (implies (and (dag-predecessor-quorum-p dag blockchain)
                (in cert dag)
                (not (equal (certificate->round cert) 1)))
           (not (emptyp (predecessors cert dag)))))