		Search-engine friendly clone of the ACL2 documentation.

Dag-committees

Dag-committees-p

Definition of the invariant: for every certificate in the DAG of a validator, the validator can calculate the active committee at the round of the certificate, and the certificate's author is a member of the that committee.

This is expressed via two predicates on DAGs.

Definitions and Theorems

Theorem: dag-committees-p-necc

(defthm dag-committees-p-necc
 (implies
  (dag-committees-p systate)
  (implies
      (in val (correct-addresses systate))
      (b* (((validator-state vstate)
            (get-validator-state val systate)))
        (and (dag-has-committees-p vstate.dag vstate.blockchain)
             (dag-in-committees-p vstate.dag vstate.blockchain))))))

Theorem: booleanp-of-dag-committees-p

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

Theorem: dag-committees-p-of-system-state-fix-systate

(defthm dag-committees-p-of-system-state-fix-systate
  (equal (dag-committees-p (system-state-fix systate))
         (dag-committees-p systate)))

Theorem: dag-committees-p-system-state-equiv-congruence-on-systate

(defthm dag-committees-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (dag-committees-p systate)
                  (dag-committees-p systate-equiv)))
  :rule-classes :congruence)