		Search-engine friendly clone of the ACL2 documentation.

Dags

Dag-has-committees-p

Check if the active committee at the round of every certificate in a DAG can be calculated from a given blockchain.

The intent is that the DAG and blockchain are the ones of a validator. This is an invariant of the DAGs of validators, as proved elsewhere.

Besides the auto-generated dag-has-committees-p-necc, we also introduce a variant that helps bind the free variable dag when there is a hypothesis saying that a certificate cert is in it.

Definitions and Theorems

Theorem: dag-has-committees-p-necc

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

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

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

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

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

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

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

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

(defthm dag-has-committees-p-of-insert
  (iff (dag-has-committees-p (insert cert dag)
                             blockchain)
       (and (dag-has-committees-p dag blockchain)
            (active-committee-at-round (certificate->round cert)
                                       blockchain))))