mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-02 11:22:13 +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.
16 lines
564 B
TeX
16 lines
564 B
TeX
\section{Phase 4: Symbolic Execution with Halmos}
|
|
|
|
|
|
Symbolic execution (covered in depth in our companion paper) proves properties for
|
|
\emph{all} inputs. In the audit context, we write Halmos tests for the most critical
|
|
invariants:
|
|
|
|
\begin{itemize}[nosep]
|
|
\item Token supply conservation.
|
|
\item Bridge balance invariant (locked = minted on destination).
|
|
\item Access control completeness (all admin functions revert for non-admins).
|
|
\item Vault share/asset ratio monotonicity.
|
|
\end{itemize}
|
|
|
|
%% ============================================================
|