		Search-engine friendly clone of the ACL2 documentation.

Fault-tolerance

Committee-correct-members

Addresses of the correct validators in a committee.

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

Whether a validator is correct or not depends on whether the map in the system state includes the validator's address as a key. Thus, we need the system state, besides the committee, to calculate this set of addresses of correct validators in the committee, which we do by intersecting the committee's addresses with the addressess of all the correct validators in the system.

Since, as proved in the definition of the system state transitions, the correctness vs. faultiness of validators never changes (expressed as the preservation of correct-addresses), it follows that, given a committee, the result of this ACL2 function does not change as the system state evolves, which we prove here.

Definitions and Theorems

Function: committee-correct-members

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

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

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

Theorem: committee-correct-members-subset-committee-members

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

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

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

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

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

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

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

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

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

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

(defthm committee-correct-members-of-event-next
  (implies (event-possiblep event systate)
           (b* ((?new-systate (event-next event systate)))
             (equal (committee-correct-members commtt new-systate)
                    (committee-correct-members commtt systate)))))

Theorem: committee-correct-members-of-committee-fix-commtt

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

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

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

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

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

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

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