papers/lux-formal-verification-lean4/sections/09-common-patterns.tex

\section{Common Patterns}


\subsection{Pattern: State Machine Invariant}

Most blockchain proofs follow this pattern: define a state machine, state an invariant,
prove it holds initially and is preserved by every transition.

\begin{lstlisting}[language=Lean,caption={State machine invariant pattern}]
-- Define state and transitions
structure State where
  round : Nat
  locked : Option Block
  decided : Option Block

inductive Transition : State -> State -> Prop where
  | propose : ... -> Transition s s'
  | vote : ... -> Transition s s'
  | commit : ... -> Transition s s'

-- Define invariant
def SafetyInvariant (s : State) : Prop :=
  ∀ b1 b2, s.decided = some b1 -> s.decided = some b2 -> b1 = b2

-- Prove base case
theorem safety_init : SafetyInvariant initialState := by
  intro b1 b2 h1 h2
  simp [initialState] at h1

-- Prove inductive case
theorem safety_preserved (s s' : State)
    (h_inv : SafetyInvariant s)
    (h_trans : Transition s s') :
    SafetyInvariant s' := by
  cases h_trans with
  | propose ... => ...
  | vote ... => ...
  | commit ... => ...
\end{lstlisting}

\subsection{Pattern: Well-Founded Induction for Liveness}

Liveness proofs require showing that some measure decreases. Lean~4's well-founded
recursion handles this naturally:

\begin{lstlisting}[language=Lean,caption={Well-founded liveness argument}]
-- Rounds strictly increase
theorem round_progress (s : State)
    (h_sync : Synchronous s)
    (h_honest_proposer : HonestProposer s s.round) :
    ∃ s', Transition s s' ∧ s'.round > s.round := by
  -- Honest proposer in synchronous period
  -- guarantees round advancement
  obtain ⟨s', htrans, _⟩ := honest_propose_succeeds h_sync h_honest_proposer
  exact ⟨s', htrans, round_increases htrans⟩
\end{lstlisting}

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