mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-02 11:39:52 +00:00
zeekay
f4ee7a0525
Bylines, paper authorship, correspondence addresses and the founder blurb under each post named an individual. They name the organisation that published the work instead: the brand on posts and pages, the research byline on papers, and research@ in place of a personal address. Both are what these repositories already used elsewhere — nothing new was coined. Co-authors are untouched. Where a paper named someone else alongside, they stay named; only the one byline changed. Bibliography entries, running heads, PDF metadata and affiliations move with it, so a citation still resolves to whoever the cited paper names. Sample and fixture data uses the placeholder name these tests already use elsewhere, so no assertion changed meaning.
85 lines
2.7 KiB
TeX
85 lines
2.7 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}
|
|
\input{../shared/lstlang}
|
|
\usepackage{xcolor}
|
|
\usepackage{enumitem}
|
|
\usepackage{float}
|
|
\usepackage{algorithm}
|
|
\usepackage{algpseudocode}
|
|
|
|
\newtheorem{theorem}{Theorem}
|
|
\newtheorem{lemma}[theorem]{Lemma}
|
|
\newtheorem{definition}{Definition}
|
|
\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}
|
|
}
|
|
|
|
\hypersetup{
|
|
colorlinks=true,
|
|
linkcolor=blue,
|
|
citecolor=blue,
|
|
urlcolor=blue
|
|
}
|
|
|
|
\title{Symbolic Execution for Smart Contract Verification}
|
|
\author{
|
|
Lux Research \\
|
|
Lux Industries, Inc.\thanks{Corresponding author: [email protected]}\\
|
|
\texttt{[email protected]}
|
|
}
|
|
\date{2025}
|
|
|
|
\begin{document}
|
|
|
|
\luxcoverpage
|
|
|
|
\begin{abstract}
|
|
Symbolic execution replaces concrete inputs with symbolic variables and reasons about all
|
|
possible execution paths simultaneously. Applied to smart contracts, it can prove that a
|
|
property holds for every possible input---or find a concrete counterexample that violates
|
|
it. This paper teaches symbolic execution from first principles, then demonstrates its
|
|
application through Halmos, a symbolic testing tool for EVM bytecode. We present 9
|
|
Halmos proofs deployed in Lux Network's smart contract verification pipeline: AMM constant
|
|
product invariant, bridge deposit/withdrawal balance, yield vault solvency, token supply
|
|
conservation, access control completeness, reentrancy absence, flash loan safety, oracle
|
|
staleness bounds, and fee accounting correctness. Each proof is presented as a Solidity
|
|
test that the reader can run with \texttt{halmos --function check\_}. We cover the
|
|
theory (path constraints, SMT solvers, loop unrolling), the practice (writing symbolic
|
|
tests, interpreting counterexamples, handling path explosion), and the limits (undecidability,
|
|
hash collision assumptions, external call modeling).
|
|
\end{abstract}
|
|
|
|
\tableofcontents
|
|
\newpage
|
|
|
|
%% ============================================================
|
|
|
|
\input{sections/01-what-is-symbolic-execution}
|
|
\input{sections/02-how-halmos-works}
|
|
\input{sections/03-writing-symbolic-tests}
|
|
\input{sections/04-our-9-halmos-proofs}
|
|
\input{sections/05-understanding-counterexamples}
|
|
\input{sections/06-smt-solvers-the-engine-under-the-hood}
|
|
\input{sections/07-halmos-vs-fuzzing-vs-formal-verification}
|
|
\input{sections/08-integrating-halmos-into-ci}
|
|
\input{sections/09-limitations-and-honest-assessment}
|
|
\input{sections/99-conclusion}
|
|
|
|
\end{document}
|