mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-03 05:07:46 +00:00
48 lines
2.0 KiB
TeX
48 lines
2.0 KiB
TeX
\section{Our Proof Corpus: 384 Theorems, 0 Sorry}
|
|
|
|
|
|
The \texttt{luxfi/formal} repository contains 384 machine-checked theorems organized
|
|
into the following modules:
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}llr@{}}
|
|
\toprule
|
|
\textbf{Module} & \textbf{Domain} & \textbf{Theorems} \\
|
|
\midrule
|
|
\texttt{Consensus.Safety} & Quasar consensus safety & 47 \\
|
|
\texttt{Consensus.Liveness} & Quasar consensus liveness & 38 \\
|
|
\texttt{Consensus.Threshold} & BFT threshold arithmetic & 52 \\
|
|
\texttt{Crypto.BLS} & BLS12-381 signature properties & 31 \\
|
|
\texttt{Crypto.Aggregate} & Signature aggregation & 28 \\
|
|
\texttt{Crypto.Pulsar} & Post-quantum threshold scheme & 44 \\
|
|
\texttt{Crypto.NTT} & NTT correctness & 23 \\
|
|
\texttt{Bridge.Safety} & Teleport bridge invariants & 36 \\
|
|
\texttt{Bridge.Liveness} & Cross-chain message delivery & 29 \\
|
|
\texttt{Chain.Validity} & Chain structure properties & 31 \\
|
|
\texttt{Chain.Finality} & Finality and fork-freedom & 25 \\
|
|
\bottomrule
|
|
\textbf{Total} & & \textbf{384} \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{Proof corpus by module. Every theorem compiles with \texttt{lake build}. Zero \texttt{sorry}.}
|
|
\end{table}
|
|
|
|
\subsection{Zero Sorry Policy}
|
|
|
|
\texttt{sorry} is Lean~4's escape hatch---it axiomatically asserts any proposition as true.
|
|
A proof containing \texttt{sorry} is not a proof; it is a claim. Our CI pipeline
|
|
(\texttt{lake build} followed by \texttt{grep -r sorry}) rejects any commit containing
|
|
\texttt{sorry} in a theorem statement. Lemmas may use \texttt{sorry} during development
|
|
on feature branches, but merges to \texttt{main} require zero \texttt{sorry}.
|
|
|
|
\subsection{Proof Maintenance}
|
|
|
|
Proofs break when the model changes. We maintain proofs alongside the Go implementation:
|
|
when the consensus protocol changes, the Lean model must be updated first and all proofs
|
|
must re-compile before the Go code is modified. This is enforced by CI: the Lean build
|
|
gate blocks the Go build gate.
|
|
|
|
%% ============================================================
|