papers/lux-formal-verification-lean4/sections/08-practical-guide-writing-your-first-block.tex

\section{Practical Guide: Writing Your First Blockchain Proof}


\subsection{Environment Setup}

\begin{lstlisting}[language=bash,caption={Setting up a Lean~4 project}]
# Install elan (Lean version manager)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Create a new project
lake init my-proofs
cd my-proofs

# Add mathlib (the standard math library)
echo 'require mathlib from git
  "https://github.com/leanprover-community/mathlib4"' >> lakefile.lean

lake update
lake build
\end{lstlisting}

\subsection{Step-by-Step: Proving a Threshold Property}

Problem: prove that if $n \geq 3f + 1$ and we have $n - f$ honest validators, then
honest validators form a quorum of size $> 2n/3$.

\begin{lstlisting}[language=Lean,caption={Complete threshold proof, start to finish}]
import Mathlib.Tactic.Omega

-- Step 1: Define quorum size
def quorumSize (n : Nat) : Nat := 2 * n / 3 + 1

-- Step 2: State the theorem
theorem honest_form_quorum (n f : Nat)
    (h_bft : n >= 3 * f + 1)
    (h_honest_count : Nat := n - f) :
    h_honest_count >= quorumSize n := by
  -- Step 3: Unfold definitions
  unfold quorumSize
  -- Step 4: Let omega handle the arithmetic
  omega
\end{lstlisting}

That's it. Four lines of proof. The \texttt{omega} tactic handles all the linear
arithmetic. The key insight: most BFT threshold proofs reduce to linear arithmetic,
and \texttt{omega} automates linear arithmetic completely.

\subsection{When Omega Is Not Enough}

For non-linear properties (e.g., involving multiplication of variables), \texttt{omega}
fails. Then you need manual proof steps:

\begin{lstlisting}[language=Lean,caption={Non-linear threshold proof}]
-- Prove: quorum^2 > n * f (for security margin)
theorem quorum_security_margin (n f : Nat) (hn : n >= 3 * f + 1) :
    (quorumSize n) ^ 2 > n * f := by
  unfold quorumSize
  -- omega can't handle x^2, so we expand manually
  have h1 : 2 * n / 3 + 1 >= f + 1 := by omega
  have h2 : (2 * n / 3 + 1) * (2 * n / 3 + 1) > n * f := by
    nlinarith [sq_nonneg (n - 3 * f)]
  exact h2
\end{lstlisting}

The \texttt{nlinarith} tactic handles nonlinear arithmetic with hints.

%% ============================================================