Max-faulty-for-total
Maximum number of 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 validators is (strictly) less than
one third of the total number of validators:
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.
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 actual number of faulty validators
is not something that (correct) validators know.
In contrast, the total number n of validators is known,
and 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) number of faulty validators.
In the documentation of our model, for clarity,
we use f for the actual number of faulty validators,
and F for the maximum number of faulty validators.
This ACL2 function returns F.
We return F, i.e. the maximum f
that satisfies the relation for a given n.
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
(we could strengthen the guard of this function
to require a positive integer as input).
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.
If n is 1 or 2 or 3, no failures are tolerated:
F, and hence 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 number of faulty validators,
any number f \leq F,
so that is usually the practical minimum for n.
We prove below that the result of this function is less than n/3
(assuming positive n),
and that incrementing the result of this function by one
does not satisfy the condition:
that is, F is the maximum f satisfying f < n/3.
We also prove the equivalence of defining F
via ceiling or floor, as mentioned above.
We also prove that n \geq 3F + 1.
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)
Theorem: max-faulty-for-total-alt-def
(defthm max-faulty-for-total-alt-def
(b* nil
(equal (max-faulty-for-total n)
(if (zp n) 0 (floor (1- n) 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)
Theorem: max-faulty-for-total-upper-bound-tight
(defthm max-faulty-for-total-upper-bound-tight
(implies (natp total)
(b* ((common-lisp::?max (max-faulty-for-total total)))
(>= (1+ max) (/ total 3)))))
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)
