		Search-engine friendly clone of the ACL2 documentation.

Same-committees-def-and-implied

Same-committees-p

Definition of the invariant: for any two correct validators in the system, if they both calculate an active committee at a round, compute the same active committee at that round.

Note that no requirement applies if only one validator can calculate the committee but not the other. A validator may be ahead of another one.

Definitions and Theorems

Theorem: same-committees-p-necc

(defthm same-committees-p-necc
 (implies
  (same-committees-p systate)
  (implies
   (and (in val1 (correct-addresses systate))
        (in val2 (correct-addresses systate)))
   (same-active-committees-p
    (validator-state->blockchain (get-validator-state val1 systate))
    (validator-state->blockchain
         (get-validator-state val2 systate))))))

Theorem: booleanp-of-same-committees-p

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

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

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

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

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