		Search-engine friendly clone of the ACL2 documentation.

Dags

Dag-in-committees-p

Check if the author of every certificate in a DAG is a member of the committee active at the round of the certificate.

The guard ensures that the committee can be in fact calculated.

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

We prove a theorem saying that, under this predicate, if all the certificates in a set have a given round then those certificates' authors are all members of the active committee for that round. We phrase the round hypothesis as subset instead of equality, so that includes the case of the empty set, in which case the round is irrelevant. Showing that the committees is not nil requires a few hints: we need to exhibit a witness certificate to use dag-in-committees-p-necc: the witness certificate is the first one in certs-with-round.

We prove a theorem saying that, under this predicate, the authors of all the certificates in any given round are members of the committee at that round.

We prove a theorem saying that, under this predicate, given a certificate in the DAG, the committee at that round is not empty. The reason is that the author of that certificate must be in the committee.

Definitions and Theorems

Theorem: dag-in-committees-p-necc

(defthm dag-in-committees-p-necc
 (implies
  (dag-in-committees-p dag blockchain)
  (implies
       (in cert dag)
       (in (certificate->author cert)
           (committee-members
                (active-committee-at-round (certificate->round cert)
                                           blockchain))))))

Theorem: booleanp-of-dag-in-committees-p

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

Theorem: dag-in-committees-p-necc-bind-dag

(defthm dag-in-committees-p-necc-bind-dag
  (implies
       (and (in cert dag)
            (dag-in-committees-p dag blockchain))
       (in (certificate->author cert)
           (committee-members
                (active-committee-at-round (certificate->round cert)
                                           blockchain)))))

Theorem: dag-in-committees-p-of-empty-dag

(defthm dag-in-committees-p-of-empty-dag
  (dag-in-committees-p nil blockchain))

Theorem: dag-in-committees-p-of-insert

(defthm dag-in-committees-p-of-insert
 (equal
  (dag-in-committees-p (insert cert dag)
                       blockchain)
  (and (dag-in-committees-p dag blockchain)
       (in (certificate->author cert)
           (committee-members
                (active-committee-at-round (certificate->round cert)
                                           blockchain))))))

Theorem: authors-at-same-round-in-committee-when-dag-in-committees-p

(defthm authors-at-same-round-in-committee-when-dag-in-committees-p
  (implies
       (and (dag-in-committees-p dag blockchain)
            (certificate-setp certs)
            (subset certs dag)
            (subset (certificate-set->round-set certs)
                    (insert round nil)))
       (subset (certificate-set->author-set certs)
               (committee-members
                    (active-committee-at-round round blockchain)))))

Theorem: round-in-committee-when-dag-in-committees-p

(defthm round-in-committee-when-dag-in-committees-p
 (implies
  (and (certificate-setp dag)
       (dag-in-committees-p dag blockchain)
       (posp round))
  (subset (certificate-set->author-set (certs-with-round round dag))
          (committee-members
               (active-committee-at-round round blockchain)))))

Theorem: committee-nonemptyp-when-dag-in-committees-p

(defthm committee-nonemptyp-when-dag-in-committees-p
  (implies (and (dag-in-committees-p dag blockchain)
                (in cert dag))
           (committee-nonemptyp
                (active-committee-at-round (certificate->round cert)
                                           blockchain))))