		Search-engine friendly clone of the ACL2 documentation.

Fault-tolerance

System-committees-fault-tolerant-p

Check if a system state is fault-tolerant.

This is the case when every correct validator in the system calculates active committees that are all fault-tolerant.

As explained in fault-tolerance, fault tolerance is an assumption that must be made for every system state; it is not just an invariant property of the system given that it holds in the initial state, as would be the case with static committees in AleoBFT and other systems.

We show that if this predicate holds after a state transition, it also holds before the state transition. We use the similar theorems proved for validator-committees-fault-tolerant-p, to prove these theorems. We also extend it to sequences of events. These properties are conditional on two already proved invariants.

Definitions and Theorems

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

(defthm system-committees-fault-tolerant-p-necc
  (implies (system-committees-fault-tolerant-p systate)
           (implies (in val (correct-addresses systate))
                    (validator-committees-fault-tolerant-p
                         (get-validator-state val systate)
                         systate))))

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

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

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

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

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

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

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

(defthm system-committees-fault-tolerant-p-of-create-next
  (implies
       (create-possiblep cert systate)
       (b* ((?new-systate (create-next cert systate)))
         (implies (system-committees-fault-tolerant-p new-systate)
                  (system-committees-fault-tolerant-p systate)))))

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

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

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

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

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

(defthm system-committees-fault-tolerant-p-of-commit-next
  (implies
       (and (commit-possiblep val systate)
            (last-blockchain-round-p systate)
            (ordered-blockchain-p systate))
       (b* ((?new-systate (commit-next val systate)))
         (implies (system-committees-fault-tolerant-p new-systate)
                  (system-committees-fault-tolerant-p systate)))))

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

(defthm system-committees-fault-tolerant-p-of-event-next
  (implies
       (and (event-possiblep event systate)
            (last-blockchain-round-p systate)
            (ordered-blockchain-p systate))
       (b* ((?new-systate (event-next event systate)))
         (implies (system-committees-fault-tolerant-p new-systate)
                  (system-committees-fault-tolerant-p systate)))))

Theorem: system-committees-fault-tolerant-p-of-events-next

(defthm system-committees-fault-tolerant-p-of-events-next
  (implies
       (and (last-blockchain-round-p systate)
            (ordered-blockchain-p systate)
            (events-possiblep events systate))
       (b* ((new-systate (events-next events systate)))
         (implies (system-committees-fault-tolerant-p new-systate)
                  (system-committees-fault-tolerant-p systate)))))