		Search-engine friendly clone of the ACL2 documentation.

Quorum-intersection

Quorum-intersection-has-correct-validator

A quorum intersection has at least one correct validator if the committee is non-empty and fault-tolerant.

This is the main property of quorum intersection. Given a non-empty fault-tolerant committee, and two quora of validators in the committee, the function pick-common-correct-validator returns a validator that is in both quora and is correct.

First we prove that the function returns a correct validator in the intersection, from which it easily follows that it returns a correct validator in both quora.

Definitions and Theorems

Theorem: quorum-intersection-has-correct-validator

(defthm quorum-intersection-has-correct-validator
 (implies
     (and (address-setp vals1)
          (address-setp vals2)
          (committee-nonemptyp commtt)
          (committee-fault-tolerant-p commtt systate)
          (subset vals1 (committee-members commtt))
          (subset vals2 (committee-members commtt))
          (>= (committee-members-stake vals1 commtt)
              (committee-quorum-stake commtt))
          (>= (committee-members-stake vals2 commtt)
              (committee-quorum-stake commtt)))
     (b* ((val (pick-common-correct-validator vals1 vals2 systate)))
       (and (in val vals1)
            (in val vals2)
            (in val (correct-addresses systate))))))