		Search-engine friendly clone of the ACL2 documentation.

Fault-tolerance

Validator-committees-fault-tolerant-p

Check if the active committees calculated by a validator are all fault-tolerant.

Each validator calculates its own active committee at each round, based on its own copy of the blockchain. This predicate checks whether a validator (represented by its state) calculates committees that are fault-tolerant, for all the rounds for which it can calculate a committee, given the validator's current blockchain.

For each state transition, if this predicate holds on a validator's state after the transition, then it also holds on the validator's state before the transition. This is because the committees that a validator can calculate before the transition are a subset of the ones that the validator can calculate after the transition. They are in fact the same for all transitions except commit, because the other transitions do not change any blockchains. For a commit transition, only the blockchain of the target validator changes, but in a way that does not affect the calculation of committees at earlier rounds. The key rule for this is active-committee-at-round-of-extend-blockchain-no-change, along with other rules to relieve hypotheses, as done in other proofs that involve similar reasoning. But we need to assume two already proved invariants.

First we prove four lemmas involving just the systate argument of the predicate, which follow directly from the preservation of committee-fault-tolerant-p proved earlier. The lemmas are then used to prove four theorems involving both arguments of the predicate.

Definitions and Theorems

Theorem: validator-committees-fault-tolerant-p-necc

(defthm validator-committees-fault-tolerant-p-necc
 (implies
    (validator-committees-fault-tolerant-p vstate systate)
    (implies
         (posp round)
         (b* ((commtt (active-committee-at-round
                           round
                           (validator-state->blockchain vstate))))
           (implies commtt
                    (committee-fault-tolerant-p commtt systate))))))

Theorem: booleanp-of-validator-committees-fault-tolerant-p

(defthm booleanp-of-validator-committees-fault-tolerant-p
  (b*
   ((yes/no (validator-committees-fault-tolerant-p vstate systate)))
   (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: validator-committees-fault-tolerant-p-of-validator-state-fix-vstate

(defthm
 validator-committees-fault-tolerant-p-of-validator-state-fix-vstate
 (equal (validator-committees-fault-tolerant-p
             (validator-state-fix vstate)
             systate)
        (validator-committees-fault-tolerant-p vstate systate)))

Theorem: validator-committees-fault-tolerant-p-validator-state-equiv-congruence-on-vstate

(defthm
 validator-committees-fault-tolerant-p-validator-state-equiv-congruence-on-vstate
 (implies
  (validator-state-equiv vstate vstate-equiv)
  (equal
      (validator-committees-fault-tolerant-p vstate systate)
      (validator-committees-fault-tolerant-p vstate-equiv systate)))
 :rule-classes :congruence)

Theorem: validator-committees-fault-tolerant-p-of-system-state-fix-systate

(defthm
  validator-committees-fault-tolerant-p-of-system-state-fix-systate
  (equal (validator-committees-fault-tolerant-p
              vstate (system-state-fix systate))
         (validator-committees-fault-tolerant-p vstate systate)))

Theorem: validator-committees-fault-tolerant-p-system-state-equiv-congruence-on-systate

(defthm
 validator-committees-fault-tolerant-p-system-state-equiv-congruence-on-systate
 (implies
  (system-state-equiv systate systate-equiv)
  (equal
      (validator-committees-fault-tolerant-p vstate systate)
      (validator-committees-fault-tolerant-p vstate systate-equiv)))
 :rule-classes :congruence)

Theorem: validator-committees-fault-tolerant-p-of-create-next-lemma

(defthm validator-committees-fault-tolerant-p-of-create-next-lemma
  (b* ((?new-systate (create-next cert systate)))
    (implies
         (validator-committees-fault-tolerant-p vstate new-systate)
         (validator-committees-fault-tolerant-p vstate systate))))

Theorem: validator-committees-fault-tolerant-p-of-accept-next-lemma

(defthm validator-committees-fault-tolerant-p-of-accept-next-lemma
 (implies
   (accept-possiblep msg systate)
   (b* ((?new-systate (accept-next msg systate)))
     (implies
          (validator-committees-fault-tolerant-p vstate new-systate)
          (validator-committees-fault-tolerant-p vstate systate)))))

Theorem: validator-committees-fault-tolerant-p-of-advance-next-lemma

(defthm validator-committees-fault-tolerant-p-of-advance-next-lemma
 (implies
   (advance-possiblep val systate)
   (b* ((?new-systate (advance-next val systate)))
     (implies
          (validator-committees-fault-tolerant-p vstate new-systate)
          (validator-committees-fault-tolerant-p vstate systate)))))

Theorem: validator-committees-fault-tolerant-p-of-commit-next-lemma

(defthm validator-committees-fault-tolerant-p-of-commit-next-lemma
 (implies
   (commit-possiblep val systate)
   (b* ((?new-systate (commit-next val systate)))
     (implies
          (validator-committees-fault-tolerant-p vstate new-systate)
          (validator-committees-fault-tolerant-p vstate systate)))))

Theorem: validator-committees-fault-tolerant-p-of-create-next

(defthm validator-committees-fault-tolerant-p-of-create-next
  (b* ((?new-systate (create-next cert systate)))
    (implies (validator-committees-fault-tolerant-p
                  (get-validator-state val new-systate)
                  new-systate)
             (validator-committees-fault-tolerant-p
                  (get-validator-state val systate)
                  systate))))

Theorem: validator-committees-fault-tolerant-p-of-accept-next

(defthm validator-committees-fault-tolerant-p-of-accept-next
  (implies (accept-possiblep msg systate)
           (b* ((?new-systate (accept-next msg systate)))
             (implies (validator-committees-fault-tolerant-p
                           (get-validator-state val new-systate)
                           new-systate)
                      (validator-committees-fault-tolerant-p
                           (get-validator-state val systate)
                           systate)))))

Theorem: validator-committees-fault-tolerant-p-of-advance-next

(defthm validator-committees-fault-tolerant-p-of-advance-next
  (implies (advance-possiblep val systate)
           (b* ((?new-systate (advance-next val systate)))
             (implies (validator-committees-fault-tolerant-p
                           (get-validator-state val1 new-systate)
                           new-systate)
                      (validator-committees-fault-tolerant-p
                           (get-validator-state val1 systate)
                           systate)))))

Theorem: validator-committees-fault-tolerant-p-of-commit-next

(defthm validator-committees-fault-tolerant-p-of-commit-next
  (implies (and (commit-possiblep val systate)
                (in val1 (correct-addresses systate))
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate))
           (b* ((?new-systate (commit-next val systate)))
             (implies (validator-committees-fault-tolerant-p
                           (get-validator-state val1 new-systate)
                           new-systate)
                      (validator-committees-fault-tolerant-p
                           (get-validator-state val1 systate)
                           systate)))))

Theorem: validator-committees-fault-tolerant-p-of-event-next

(defthm validator-committees-fault-tolerant-p-of-event-next
  (implies (and (event-possiblep event systate)
                (in val (correct-addresses systate))
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate))
           (b* ((?new-systate (event-next event systate)))
             (implies (validator-committees-fault-tolerant-p
                           (get-validator-state val new-systate)
                           new-systate)
                      (validator-committees-fault-tolerant-p
                           (get-validator-state val systate)
                           systate)))))