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.
26 lines
1.1 KiB
TeX
26 lines
1.1 KiB
TeX
\section{Lean 4 Development}
|
|
|
|
\label{sec:lean}
|
|
%% ============================================================================
|
|
|
|
The full development is in \texttt{lux/formal/lean/Consensus/}:
|
|
|
|
\begin{itemize}
|
|
\item \texttt{DAGEVM.lean} — DAG-EVM safety, commutativity, topological
|
|
order invariance, no-double-spend, serialisability.
|
|
\item \texttt{DAGZChain.lean} — DAG-Z-Chain nullifier-disjointness,
|
|
proofs-commute, parallel-verify soundness, FHE linearity.
|
|
\item \texttt{PQZParallel.lean} — cross-chain non-interference: running
|
|
C/X/Z/Q/D/A/O/R/S DAGs concurrently preserves per-chain safety;
|
|
Quasar stamps are independently verifiable; validator signing across
|
|
$k$ chains scales linearly.
|
|
\item \texttt{Safety.lean}, \texttt{Liveness.lean}, \texttt{BFT.lean} —
|
|
Pre-existing per-chain consensus safety (not modified).
|
|
\item \texttt{Quasar.lean} — PQ certificate unforgeability (not
|
|
modified); supplies the finality assumption for DAG antichains.
|
|
\end{itemize}
|
|
|
|
Build: \texttt{cd lux/formal/lean \&\& lake build}.
|
|
|
|
%% ============================================================================
|