Max-faulty-for-total
Maximum number of units of stake associated to faulty validators,
out of a total, for the protocol to be fault-tolerant.
- Signature
(max-faulty-for-total total) → max
- Arguments
- total — Guard (natp total).
- Returns
- max — Type (natp max).
The classic BFT condition for fault tolerance is that
the number of faulty participants is (strictly) less than
one third of the total number of participants:
f < n/3, using the common symbols
f and n for the two numbers.
This relation works for every positive n,
whether it is a multiple of 3 or not.
Multiplying both sides by 3, we get 3f < n,
and taking f as the maximum value that satisfies the inequality
(as opposed to potentially smaller values than the maximum),
we get to the sometimes stated condition n = 3f + 1,
although this condition is less general for n,
because it forces n to be one more than a multiple of 3.
The other possibilities are n = 3f + 2 and n = 3f + 3.
In AleoBFT, the participants are not fixed,
because they are the members of the changing committee;
so n and f vary with the committee.
Furthermore, AleoBFT uses not numbers of validators,
but units of stake associated to the validators;
thus n is the sum of the units of stake
of all the validators in the committee,
and f is the maximim sum of the units of stake
of the faulty validators in the committee.
The distinction between the maximum f
and possibly smaller values of f
is worth emphasizing,
because recent BFT literature
does not always state things clearly in this respect.
The stake associated to the faulty validators in a committee
is not something that validators know,
because validators do not know which validators are faulty.
In contrast, the stake n associated to
all the validators in a committee is known,
because the committee is known (calculated from the blockchain).
Thus the maximum f satisfying f < n/3
can be calculated from n.
So when a validator needs to use f in some computation,
it is the maximum such f, calculable from n,
not the (unknowable to the validator)
stake of the faulty validators in the committee.
Some BFT literature uses phrases like
``up to f < n/3 faulty validators'',
implying that f is another parameter of the system, besides n.
But when validators need to use f as part of their computation,
as is the case for AleoBFT,
it makes more sense for f to be the maximum value
that satisfies the inequality,
because it allows for the maximum possible stake faulty validators.
So in our model f is always that maximum,
and it is calculable from n.
This ACL2 function performs this calculation.
The input total is n,
and the output is the maximum f such that f < n/3.
We define the function to return 0 if n = 0,
although n = 0 does not correspond to a practical situation.
So consider the normal case n > 0.
If n is a multiple of 3,
f is one less than the integer n/3;
if n is not a multiple of 3,
f is the floor of n/3.
We can put the two cases together by noting that
the ceiling of an integer is the integer (i.e. a no-op)
and that the floor of a non-integer is
one less than the ceiling of the non-integer.
So we define f as
one less than the ceiling of n/3,
or equivalently as the floor of (n-1)/3.
We prove the two equivalent, in fact.
We also prove that this function returns something below n/3,
and that one more than that is not below n/3:
that is, we prove that it returns the maximum.
We could have alternatively defined this function in terms of maximum,
via a recursion to find it, or even in a non-executable way,
but instead we pick the definition with ceiling,
and prove it equivalent to the other two possible definitions.
We also prove that n \geq 3f + 1 when n \neq 0,
that n \geq f even if n = 0,
that n > f when n \neq 0,
and that f < n - f when n \neq 0;
in the latter, the significance of n - f is that
it is the quorum, corresponding to f,
necessary for fault tolerance conditions.
If n is 1 or 2 or 3, no failures are tolerated:
f must be 0.
The case n = 1 is a degenerate one,
but the protocol could probably still work in a degenerate way.
The cases n = 2 and n = 3 could make sense,
but since they tolerate no failures,
they are not used in practice.
If n is 4 or more, we can tolerate
an increasing amount of faulty validators,
any amount whose stake is less than or equal to $f$,
so that is usually the practical minimum for n.
Definitions and Theorems
Function: max-faulty-for-total
(defun max-faulty-for-total (total)
(declare (xargs :guard (natp total)))
(let ((__function__ 'max-faulty-for-total))
(declare (ignorable __function__))
(if (zp total)
0
(1- (ceiling total 3)))))
Theorem: natp-of-max-faulty-for-total
(defthm natp-of-max-faulty-for-total
(b* ((max (max-faulty-for-total total)))
(natp max))
:rule-classes (:rewrite :type-prescription))
Theorem: max-faulty-for-total-of-nfix-total
(defthm max-faulty-for-total-of-nfix-total
(equal (max-faulty-for-total (nfix total))
(max-faulty-for-total total)))
Theorem: max-faulty-for-total-nat-equiv-congruence-on-total
(defthm max-faulty-for-total-nat-equiv-congruence-on-total
(implies (acl2::nat-equiv total total-equiv)
(equal (max-faulty-for-total total)
(max-faulty-for-total total-equiv)))
:rule-classes :congruence)
Theorem: max-faulty-for-total-alt-def
(defthm max-faulty-for-total-alt-def
(equal (max-faulty-for-total total)
(if (zp total) 0 (floor (1- total) 3))))
Theorem: max-faulty-for-total-upper-bound
(defthm max-faulty-for-total-upper-bound
(implies (not (zp total))
(b* ((common-lisp::?max (max-faulty-for-total total)))
(< max (/ total 3))))
:rule-classes
((:linear :trigger-terms ((max-faulty-for-total total)))))
Theorem: max-faulty-for-total-upper-bound-tight
(defthm max-faulty-for-total-upper-bound-tight
(implies (not (zp total))
(b* ((common-lisp::?max (max-faulty-for-total total)))
(>= (1+ max) (/ total 3))))
:rule-classes
((:linear :trigger-terms ((1+ (max-faulty-for-total total))))))
Theorem: total-lower-bound-wrt-max-faulty
(defthm total-lower-bound-wrt-max-faulty
(implies (not (zp total))
(>= total
(1+ (* 3 (max-faulty-for-total total)))))
:rule-classes
((:linear :trigger-terms ((max-faulty-for-total total)))))
Theorem: max-faulty-for-total-leq-total
(defthm max-faulty-for-total-leq-total
(implies (natp total)
(b* ((common-lisp::?max (max-faulty-for-total total)))
(<= max total)))
:rule-classes
((:linear :trigger-terms ((max-faulty-for-total total)))))
Theorem: max-faulty-for-total-lt-total
(defthm max-faulty-for-total-lt-total
(implies (posp total)
(b* ((common-lisp::?max (max-faulty-for-total total)))
(< max total)))
:rule-classes
((:linear :trigger-terms ((max-faulty-for-total total)))))
Theorem: max-faulty-for-total-lt-quorum
(defthm max-faulty-for-total-lt-quorum
(implies (posp total)
(b* ((common-lisp::?max (max-faulty-for-total total)))
(< max (- total max))))
:rule-classes :linear)