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.
64 lines
2.0 KiB
TeX
64 lines
2.0 KiB
TeX
\section{Induction on Chain Height}
|
||
|
||
|
||
Many blockchain properties require induction on the height (length) of the chain.
|
||
|
||
\subsection{Chain Validity}
|
||
|
||
A valid chain is one where every block's parent hash matches the hash of the preceding
|
||
block, and every block contains a valid quorum certificate.
|
||
|
||
\begin{lstlisting}[language=Lean,caption={Chain validity by induction on height}]
|
||
inductive ValidChain : List Block -> Prop where
|
||
| genesis : ValidChain [genesisBlock]
|
||
| extend :
|
||
ValidChain chain ->
|
||
block.parentHash = hash (chain.head!) ->
|
||
ValidCertificate block.cert (validatorSetAt chain.length) ->
|
||
ValidChain (block :: chain)
|
||
|
||
-- Property: all blocks in a valid chain have valid certificates
|
||
theorem all_certs_valid :
|
||
ValidChain chain ->
|
||
∀ b ∈ chain, ValidCertificate b.cert (validatorSetAt b.height) := by
|
||
intro hvc
|
||
induction hvc with
|
||
| genesis =>
|
||
intro b hb
|
||
simp at hb; subst hb
|
||
exact genesis_cert_valid
|
||
| extend hvc hparent hcert ih =>
|
||
intro b hb
|
||
cases hb with
|
||
| head => exact hcert
|
||
| tail _ hb' => exact ih b hb'
|
||
\end{lstlisting}
|
||
|
||
\subsection{Fork-Free Property}
|
||
|
||
\begin{theorem}[No Forks]
|
||
If the consensus protocol satisfies safety, then for any two valid chains sharing the
|
||
same genesis, one is a prefix of the other.
|
||
\end{theorem}
|
||
|
||
\begin{lstlisting}[language=Lean,caption={Fork-freedom from safety}]
|
||
theorem no_forks
|
||
(c1 c2 : List Block)
|
||
(hv1 : ValidChain c1) (hv2 : ValidChain c2)
|
||
(hgen : c1.getLast? = c2.getLast?)
|
||
(safety : ConsensusSafety)
|
||
: IsPrefix c1 c2 ∨ IsPrefix c2 c1 := by
|
||
-- Induction on the shorter chain
|
||
wlog h : c1.length <= c2.length
|
||
· exact Or.symm (this c2 c1 hv2 hv1 hgen.symm safety (le_of_not_le h))
|
||
-- At each height, safety ensures same block
|
||
induction c1 with
|
||
| nil => exact Or.inl (nil_prefix c2)
|
||
| cons b1 rest ih =>
|
||
have h_eq := safety b1.height
|
||
-- Block at each height is unique by safety
|
||
exact prefix_cons_of_same_block h_eq (ih ...)
|
||
\end{lstlisting}
|
||
|
||
%% ============================================================
|