		Search-engine friendly clone of the ACL2 documentation.

Quorum-intersection

Stake-of-quorum-intersection

Stake of a quorum intersection.

We show that the intersection of two quora that are both subsets of a non-empty committee of total stake n have more than f stake. Refer to max-faulty-for-total for a description of f and n.

The non-emptiness of the committee is a critical assumption. If the committee is empty, we have n = f = 0, and the intersection does not have a non-zero stake.

Let A and B be the two sets of (addresses of) validators whose total stakes are S(A) and S(B). Since they each form a quorum, their stakes are at least n - f:

S(A) \geq n - f

S(B) \geq n - f

Furthermore, since both A and B are subsets of the committee, their union is also a subset of the committe, and thus the stake of the union is bounded by the committee's total stake, i.e.

S(A \cup B) \leq n

This fact is proved as a local lemma, which fires as a rewrite rule in the proof of the main theorem.

We start from the previously proved (in committee-members-stake) fact that

S(A \cup B) = S(A) + S(B) - S(A \cap B)

from which we get

S(A \cap B) = S(A) + S(B) - S(A \cup B)

If we use the quorum inequalities of A and B (see above), we obtain

S(A \cap B) \geq 2n - 2f - S(A \cup B)

But as mentioned earlier we have

S(A \cup B) \leq n

that is

- S(A \cup B) \geq -n

and if we use that in the inequality above we get

S(A \cap B) \geq 2n - 2f - n

Since f < n/3, we have n > 3f, which we substitute above obtaining

S(A \cap B) \geq 2n - 2f - n = n - 2f > 3f - 2f = f

So we get

S(A \cap B) > f

Note that committees are defined to be non-empty, so we have n > 0, which is necessary here, otherwise f = n = 0 and f = n/3 (not f < n/3).

ACL2's built-in arithmetic, plus perhaps some other arithmetic rules that happen to be available, takes care of the reasoning detailed above, but we need to help things with a few hints. We expand various definition so to expose max-faulty-for-total, for which the linear rule total-lower-bound-wrt-max-faulty fires in the proof, corresponding to n > 3f above; that rule says n \geq 3f + 1, which is equivalent. We also need to expand the cardinality of the intersection, and disable the rule that expands the cardinality of the union. We also need a lemma, as mentioned earlier.

Definitions and Theorems

Theorem: stake-of-quorum-intersection

(defthm stake-of-quorum-intersection
  (implies (and (address-setp vals1)
                (address-setp vals2)
                (committee-nonemptyp commtt)
                (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)))
           (> (committee-members-stake (intersect vals1 vals2)
                                       commtt)
              (committee-max-faulty-stake commtt)))
  :rule-classes :linear)