		Search-engine friendly clone of the ACL2 documentation.

Fault-tolerance

Committee-fault-tolerant-p

Check if a committee is fault-tolerant.

Signature
(committee-fault-tolerant-p commtt systate) → yes/no
Arguments: commtt — Guard (committeep commtt).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

This is the case when the total stake of faulty members in the committee does not exceed the maximum tolerated stake of faulty validators in the committee. Or, equivalently, when the total stake of the correct members in the committee is at least the quorum stake of the committee; we prove this equivalent definition as a theorem.

The fault tolerance of a committee does not change as the system transitions from one state to the next, because the dependency on the system state is only on the addresses of correct vs. faulty validators, which do not change as the system evolves.

Definitions and Theorems

Function: committee-fault-tolerant-p

(defun committee-fault-tolerant-p (commtt systate)
  (declare (xargs :guard (and (committeep commtt)
                              (system-statep systate))))
  (let ((__function__ 'committee-fault-tolerant-p))
    (declare (ignorable __function__))
    (<= (committee-members-stake
             (committee-faulty-members commtt systate)
             commtt)
        (committee-max-faulty-stake commtt))))

Theorem: booleanp-of-committee-fault-tolerant-p

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

Theorem: committee-fault-tolerant-p-alt-def

(defthm committee-fault-tolerant-p-alt-def
  (equal (committee-fault-tolerant-p commtt systate)
         (>= (committee-members-stake
                  (committee-correct-members commtt systate)
                  commtt)
             (committee-quorum-stake commtt))))

Theorem: committee-fault-tolerant-p-of-create-next

(defthm committee-fault-tolerant-p-of-create-next
  (b* ((?new-systate (create-next cert systate)))
    (equal (committee-fault-tolerant-p commtt new-systate)
           (committee-fault-tolerant-p commtt systate))))

Theorem: committee-fault-tolerant-p-of-accept-next

(defthm committee-fault-tolerant-p-of-accept-next
  (implies (accept-possiblep msg systate)
           (b* ((?new-systate (accept-next msg systate)))
             (equal (committee-fault-tolerant-p commtt new-systate)
                    (committee-fault-tolerant-p commtt systate)))))

Theorem: committee-fault-tolerant-p-of-advance-next

(defthm committee-fault-tolerant-p-of-advance-next
  (implies (advance-possiblep val systate)
           (b* ((?new-systate (advance-next val systate)))
             (equal (committee-fault-tolerant-p commtt new-systate)
                    (committee-fault-tolerant-p commtt systate)))))

Theorem: committee-fault-tolerant-p-of-commit-next

(defthm committee-fault-tolerant-p-of-commit-next
  (implies (commit-possiblep val systate)
           (b* ((?new-systate (commit-next val systate)))
             (equal (committee-fault-tolerant-p commtt new-systate)
                    (committee-fault-tolerant-p commtt systate)))))

Theorem: committee-fault-tolerant-p-of-event-next

(defthm committee-fault-tolerant-p-of-event-next
  (implies (event-possiblep event systate)
           (b* ((?new-systate (event-next event systate)))
             (equal (committee-faulty-members commtt new-systate)
                    (committee-faulty-members commtt systate)))))

Theorem: committee-fault-tolerant-p-of-committee-fix-commtt

(defthm committee-fault-tolerant-p-of-committee-fix-commtt
  (equal (committee-fault-tolerant-p (committee-fix commtt)
                                     systate)
         (committee-fault-tolerant-p commtt systate)))

Theorem: committee-fault-tolerant-p-committee-equiv-congruence-on-commtt

(defthm
    committee-fault-tolerant-p-committee-equiv-congruence-on-commtt
 (implies (committee-equiv commtt commtt-equiv)
          (equal (committee-fault-tolerant-p commtt systate)
                 (committee-fault-tolerant-p commtt-equiv systate)))
 :rule-classes :congruence)

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

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

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

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