mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
75 lines
2.4 KiB
TeX
75 lines
2.4 KiB
TeX
\section{BFT Threshold Proofs}
|
|
|
|
|
|
BFT protocols depend on precise arithmetic relationships between $n$ (total validators),
|
|
$f$ (maximum Byzantine), and $q$ (quorum size). Getting these off by one breaks
|
|
everything.
|
|
|
|
\subsection{The $3f + 1$ Bound}
|
|
|
|
\begin{theorem}
|
|
BFT consensus requires $n \geq 3f + 1$ validators.
|
|
\end{theorem}
|
|
|
|
\begin{proof}
|
|
Safety requires two quorums to overlap in at least one honest validator. A quorum has
|
|
size $q = \lceil (n + f + 1) / 2 \rceil$. Two quorums overlap in at least $2q - n$
|
|
validators. For this overlap to contain an honest validator: $2q - n > f$, i.e.,
|
|
$2 \cdot \lceil (n + f + 1) / 2 \rceil - n > f$, which simplifies to $n > 3f$, i.e.,
|
|
$n \geq 3f + 1$.
|
|
\end{proof}
|
|
|
|
\begin{lstlisting}[language=Lean,caption={$3f + 1$ bound in Lean~4}]
|
|
-- n validators, f Byzantine, need safety
|
|
theorem bft_minimum_validators
|
|
(n f : Nat)
|
|
(quorum_size : Nat := (n + f + 1) / 2 + 1)
|
|
(h_overlap_honest : 2 * quorum_size - n > f)
|
|
: n >= 3 * f + 1 := by
|
|
omega
|
|
|
|
-- Converse: if n < 3f + 1, no safe quorum exists
|
|
theorem bft_impossibility
|
|
(n f : Nat) (h : n < 3 * f + 1)
|
|
: ¬∃ q, q <= n ∧ 2 * q - n > f := by
|
|
intro ⟨q, hq_le, hq_overlap⟩
|
|
omega
|
|
\end{lstlisting}
|
|
|
|
The \texttt{omega} tactic decides linear arithmetic---it automatically verifies
|
|
inequalities over natural numbers and integers. For BFT threshold proofs, it is the
|
|
workhorse.
|
|
|
|
\subsection{Quorum Size Calculations}
|
|
|
|
\begin{lstlisting}[language=Lean,caption={Quorum properties}]
|
|
def quorumSize (n : Nat) : Nat := 2 * n / 3 + 1
|
|
|
|
-- A quorum is always a majority
|
|
theorem quorum_is_majority (n : Nat) (hn : n >= 1) :
|
|
quorumSize n > n / 2 := by
|
|
unfold quorumSize; omega
|
|
|
|
-- Two quorums always overlap
|
|
theorem two_quorums_overlap (n : Nat) (hn : n >= 4)
|
|
(Q1 Q2 : Finset (Fin n))
|
|
(h1 : Q1.card >= quorumSize n)
|
|
(h2 : Q2.card >= quorumSize n) :
|
|
(Q1 ∩ Q2).Nonempty := by
|
|
have : Q1.card + Q2.card > n := by
|
|
unfold quorumSize at h1 h2; omega
|
|
exact Finset.inter_nonempty_of_card_lt_card_add Q1 Q2 (by omega)
|
|
|
|
-- Quorum minus Byzantine still nonempty
|
|
theorem quorum_honest_nonempty
|
|
(n f : Nat) (hn : n >= 3 * f + 1)
|
|
(Q : Finset (Fin n)) (F : Finset (Fin n))
|
|
(hQ : Q.card >= quorumSize n) (hF : F.card <= f) :
|
|
(Q \ F).Nonempty := by
|
|
have : Q.card - F.card >= 1 := by
|
|
unfold quorumSize at hQ; omega
|
|
exact Finset.nonempty_of_card_pos (by omega)
|
|
\end{lstlisting}
|
|
|
|
%% ============================================================
|