		Search-engine friendly clone of the ACL2 documentation.

Fault-tolerance

Committee-faulty-members

Addresses of the faulty validators in a committee.

Signature
(committee-faulty-members commtt systate) → addresses
Arguments: commtt — Guard (committeep commtt).; systate — Guard (system-statep systate).
Returns: addresses — Type (address-setp addresses).

This is the difference between all the validators in the committee and the correct ones.

Definitions and Theorems

Function: committee-faulty-members

(defun committee-faulty-members (commtt systate)
  (declare (xargs :guard (and (committeep commtt)
                              (system-statep systate))))
  (let ((__function__ 'committee-faulty-members))
    (declare (ignorable __function__))
    (difference (committee-members commtt)
                (correct-addresses systate))))

Theorem: address-setp-of-committee-faulty-members

(defthm address-setp-of-committee-faulty-members
  (b* ((addresses (committee-faulty-members commtt systate)))
    (address-setp addresses))
  :rule-classes :rewrite)

Theorem: committee-faulty-members-subset-committee-members

(defthm committee-faulty-members-subset-committee-members
  (subset (committee-faulty-members commtt systate)
          (committee-members commtt)))

Theorem: committee-faulty-members-of-create-next

(defthm committee-faulty-members-of-create-next
  (b* ((?new-systate (create-next cert systate)))
    (equal (committee-faulty-members commtt new-systate)
           (committee-faulty-members commtt systate))))

Theorem: committee-faulty-members-of-accept-next

(defthm committee-faulty-members-of-accept-next
  (implies (accept-possiblep msg systate)
           (b* ((?new-systate (accept-next msg systate)))
             (equal (committee-faulty-members commtt new-systate)
                    (committee-faulty-members commtt systate)))))

Theorem: committee-faulty-members-of-advance-next

(defthm committee-faulty-members-of-advance-next
  (implies (advance-possiblep val systate)
           (b* ((?new-systate (advance-next val systate)))
             (equal (committee-faulty-members commtt new-systate)
                    (committee-faulty-members commtt systate)))))

Theorem: committee-faulty-members-of-commit-next

(defthm committee-faulty-members-of-commit-next
  (implies (commit-possiblep val systate)
           (b* ((?new-systate (commit-next val systate)))
             (equal (committee-faulty-members commtt new-systate)
                    (committee-faulty-members commtt systate)))))

Theorem: committee-faulty-members-of-event-next

(defthm committee-faulty-members-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-faulty-members-of-committee-fix-commtt

(defthm committee-faulty-members-of-committee-fix-commtt
  (equal (committee-faulty-members (committee-fix commtt)
                                   systate)
         (committee-faulty-members commtt systate)))

Theorem: committee-faulty-members-committee-equiv-congruence-on-commtt

(defthm
      committee-faulty-members-committee-equiv-congruence-on-commtt
  (implies (committee-equiv commtt commtt-equiv)
           (equal (committee-faulty-members commtt systate)
                  (committee-faulty-members commtt-equiv systate)))
  :rule-classes :congruence)

Theorem: committee-faulty-members-of-system-state-fix-systate

(defthm committee-faulty-members-of-system-state-fix-systate
 (equal (committee-faulty-members commtt (system-state-fix systate))
        (committee-faulty-members commtt systate)))

Theorem: committee-faulty-members-system-state-equiv-congruence-on-systate

(defthm
  committee-faulty-members-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (committee-faulty-members commtt systate)
                  (committee-faulty-members commtt systate-equiv)))
  :rule-classes :congruence)