mirror of
https://github.com/hanzoai/papers.git
synced 2026-10-29 07:34:31 +00:00
29 lines
1.1 KiB
TeX
29 lines
1.1 KiB
TeX
\section{Proof Engineering}
|
|
|
|
\label{sec:engineering}
|
|
% ============================================================================
|
|
|
|
\subsection{Lean 4 Proof Architecture}
|
|
|
|
The proof suite is organized into five Lean 4 packages, one per system, with
|
|
a shared foundation package containing common definitions (permission lattice,
|
|
cryptographic primitives, state machine framework).
|
|
|
|
\subsection{Automation}
|
|
|
|
Approximately 60\% of proof steps are automated using Lean 4 tactics:
|
|
\begin{itemize}[leftmargin=1.1em]
|
|
\item \texttt{simp}: Simplification for algebraic properties.
|
|
\item \texttt{omega}: Linear arithmetic over integers and naturals.
|
|
\item \texttt{decide}: Decidable propositions over finite types.
|
|
\item Custom tactics for state machine reachability and permission
|
|
lattice reasoning.
|
|
\end{itemize}
|
|
|
|
\subsection{Verification Time}
|
|
|
|
Full verification (type-checking all 12,000 lines) completes in 47 seconds on
|
|
a 16-core machine. This runs in CI on every commit to the proof repository.
|
|
|
|
% ============================================================================
|