mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-03 05:07:46 +00:00
zeekay
dd93cb41f7
Sweep across the non-Tier-1 paper catalogue (Tier-1 owned by parallel
agent and excluded). All 113 processed papers already had luxcover
wired up; this commit fixes 14 build breakers and produces fresh
PDFs across the catalogue.
Fixes:
- lux-blockchain-scaling-laws: em-dash inside lstlisting -> --
- lux-corona-pq: stale \input pointing at 03-the-corona-scheme renamed
to 03-the-corona-scheme (file already renamed on disk)
- lux-lattice-cryptography-primer: same Corona->Corona rename
- lux-formal-verification-lean4: Lean source uses unicode (×, ∀, ∃, ∈,
∧, ∨, ∩, ≠, ⟨, ⟩, ·, ¬) inside lstlistings. Added a literate map
so listings render the math glyphs without UTF-8 fault.
- lux-id-did-specification: ✓/✗ in tabular replaced with \ding{51}
/ \ding{55} (pifont). Added pifont package.
- lux-ntt-simd-implementation: middle-dot in Go assembly listings;
added literate {·}{\textperiodcentered}.
- lux-ntt-transform: μ, ×, –, — in regular text (no T1 fontenc).
Replaced with $\mu$/$\times$/--/--- via unicode->latex sweep.
- lux-perpetuals-derivatives, lux-quantum-consensus,
lux-quasar-consensus, lux-tee-computing-mesh: same unicode->latex
sweep across body text. Also fixed broken math segment
`$L_{avg} = 10$\times$$` -> `$L_{avg} = 10\times$`.
- lux-zchain: emoji glyphs in roadmap table replaced with
parenthetical text.
- lux-triple-proof-consensus: dropped duplicate \usepackage{geometry}
that clashed with luxcover (geometry option clash).
- pq: defined missing \Rq macro.
PDFs rebuilt for the full Tier-2/3 set.
Excluded (Tier-1, parallel agent): lp-073-pulsar, lp-stricte2epq,
dag-evm-formal, lp-010-quasar-stm-{3,4}, lp-020-quasar-consensus,
lux-institutional-custody, lux-nist-mptc-submission, pqsafe-il5,
pq-rns, plus shared/ and lps/.
111 lines
3.4 KiB
TeX
111 lines
3.4 KiB
TeX
\documentclass[11pt,a4paper]{article}
|
||
\usepackage{../shared/luxcover}
|
||
\usepackage[utf8]{inputenc}
|
||
\usepackage[T1]{fontenc}
|
||
\usepackage{amsmath,amssymb,amsfonts,amsthm}
|
||
\usepackage{graphicx}
|
||
\usepackage{hyperref}
|
||
\usepackage{booktabs}
|
||
\usepackage{listings}
|
||
\usepackage{listingsutf8}
|
||
\input{../shared/lstlang}
|
||
\usepackage{xcolor}
|
||
\usepackage{enumitem}
|
||
\usepackage{float}
|
||
|
||
\newtheorem{theorem}{Theorem}
|
||
\newtheorem{lemma}[theorem]{Lemma}
|
||
\newtheorem{proposition}[theorem]{Proposition}
|
||
\newtheorem{definition}{Definition}
|
||
\newtheorem{corollary}[theorem]{Corollary}
|
||
\newtheorem{remark}{Remark}
|
||
|
||
\lstset{
|
||
basicstyle=\small\ttfamily,
|
||
keywordstyle=\color{blue}\bfseries,
|
||
commentstyle=\color{gray},
|
||
stringstyle=\color{red},
|
||
breaklines=true,
|
||
frame=single,
|
||
numbers=left,
|
||
numberstyle=\tiny\color{gray},
|
||
extendedchars=true,
|
||
inputencoding=utf8,
|
||
literate=%
|
||
{×}{{$\times$}}1
|
||
{→}{{$\to$}}1
|
||
{←}{{$\leftarrow$}}1
|
||
{≥}{{$\geq$}}1
|
||
{≤}{{$\leq$}}1
|
||
{μ}{{$\mu$}}1
|
||
{►}{{\ensuremath{\blacktriangleright}}}1
|
||
{✓}{{\ensuremath{\checkmark}}}1
|
||
{✅}{{\ensuremath{\checkmark}}}1
|
||
{—}{{--}}1
|
||
{–}{{-}}1
|
||
{¬}{{\ensuremath{\neg}}}1
|
||
{·}{{\ensuremath{\cdot}}}1
|
||
{∀}{{\ensuremath{\forall}}}1
|
||
{∃}{{\ensuremath{\exists}}}1
|
||
{∈}{{\ensuremath{\in}}}1
|
||
{∉}{{\ensuremath{\notin}}}1
|
||
{∧}{{\ensuremath{\wedge}}}1
|
||
{∨}{{\ensuremath{\vee}}}1
|
||
{∩}{{\ensuremath{\cap}}}1
|
||
{≠}{{\ensuremath{\neq}}}1
|
||
{⟨}{{\ensuremath{\langle}}}1
|
||
{⟩}{{\ensuremath{\rangle}}}1
|
||
}
|
||
|
||
\hypersetup{
|
||
colorlinks=true,
|
||
linkcolor=blue,
|
||
citecolor=blue,
|
||
urlcolor=blue
|
||
}
|
||
|
||
\title{Formal Verification with Lean~4 for Blockchain Systems}
|
||
\author{
|
||
Zach Kelling \\
|
||
Lux Industries, Inc.\thanks{Corresponding author: [email protected]}\\
|
||
\texttt{[email protected]}
|
||
}
|
||
\date{2025}
|
||
|
||
\begin{document}
|
||
|
||
\luxcoverpage
|
||
|
||
\begin{abstract}
|
||
Formal verification provides mathematical certainty that software satisfies its specification.
|
||
This paper teaches formal verification from first principles using Lean~4, a dependently typed
|
||
proof assistant and programming language developed at Microsoft Research. We cover the
|
||
foundations---propositions as types, tactics, induction---then apply them to blockchain-specific
|
||
problems: consensus safety and liveness, BFT threshold arithmetic, and cryptographic
|
||
primitive correctness. We present 384 machine-checked theorems with zero uses of
|
||
\texttt{sorry} (Lean's axiom-of-trust escape hatch), covering Lux Network's Quasar
|
||
consensus, BLS signature aggregation, and post-quantum threshold schemes. Every proof
|
||
compiles with \texttt{lake build} and is maintained in \texttt{luxfi/formal}. This is a
|
||
builder's guide: each concept is followed by working Lean~4 code that the reader can type,
|
||
compile, and modify.
|
||
\end{abstract}
|
||
|
||
\tableofcontents
|
||
\newpage
|
||
|
||
%% ============================================================
|
||
|
||
\input{sections/01-why-formal-verification}
|
||
\input{sections/02-lean-4-fundamentals}
|
||
\input{sections/03-modeling-consensus-in-lean-4}
|
||
\input{sections/04-induction-on-chain-height}
|
||
\input{sections/05-bft-threshold-proofs}
|
||
\input{sections/06-cryptographic-primitive-verification}
|
||
\input{sections/07-our-proof-corpus-384-theorems-0-sorry}
|
||
\input{sections/08-practical-guide-writing-your-first-block}
|
||
\input{sections/09-common-patterns}
|
||
\input{sections/10-lessons-learned}
|
||
\input{sections/99-conclusion}
|
||
|
||
\end{document}
|