papers/lux-symbolic-execution-halmos/sections/02-how-halmos-works.tex

\section{How Halmos Works}


Halmos is a symbolic testing tool for EVM smart contracts, developed by a16z. It
integrates with Foundry's testing framework: you write Solidity tests with symbolic inputs,
and Halmos explores all paths through the EVM bytecode.

\subsection{Architecture}

\begin{enumerate}
  \item \textbf{Compilation}: Halmos uses Foundry to compile Solidity to EVM bytecode.
  \item \textbf{Symbolic EVM}: Halmos implements a complete EVM interpreter that operates
    on symbolic values (bitvectors of width 256).
  \item \textbf{Path exploration}: At each conditional jump (\texttt{JUMPI}), Halmos forks
    execution into two paths: one where the condition is true, one where it is false.
  \item \textbf{Property checking}: At the end of each path, Halmos checks whether any
    \texttt{assert} statement was violated. If so, it queries the SMT solver for a
    satisfying assignment to the path constraints, producing a concrete counterexample.
  \item \textbf{Result}: Either all paths satisfy all assertions (proof), or a
    counterexample is found (bug).
\end{enumerate}

\subsection{Symbolic Values in the EVM}

The EVM operates on 256-bit words. Halmos represents each word as either a concrete
\texttt{uint256} or a symbolic bitvector expression. EVM operations become SMT operations:

\begin{table}[H]
\centering
\small
\begin{tabular}{@{}lll@{}}
\toprule
\textbf{EVM Opcode} & \textbf{Concrete} & \textbf{Symbolic} \\
\midrule
\texttt{ADD} & $a + b$ & \texttt{bvadd(a, b)} \\
\texttt{MUL} & $a \times b$ & \texttt{bvmul(a, b)} \\
\texttt{DIV} & $a / b$ & \texttt{bvudiv(a, b)} \\
\texttt{LT} & $a < b$ & \texttt{bvult(a, b)} \\
\texttt{SSTORE} & \texttt{storage[k] = v} & \texttt{store(mem, k, v)} \\
\texttt{SLOAD} & \texttt{storage[k]} & \texttt{select(mem, k)} \\
\bottomrule
\end{tabular}
\caption{EVM opcodes as SMT bitvector operations.}
\end{table}

\subsection{Path Explosion and Loop Unrolling}

The number of paths grows exponentially with the number of branches. A function with
$k$ independent \texttt{if} statements has $2^k$ paths. Loops are worse: a \texttt{for}
loop iterating $n$ times with a branch inside generates $2^n$ paths.

Halmos handles this with \emph{loop unrolling}: loops are unrolled up to a configurable
bound (default: 2). This means Halmos proves properties for all inputs \emph{assuming
loops execute at most $k$ times}. For many contracts this is sufficient, but the user
must understand this limitation.

\begin{lstlisting}[language=bash,caption={Running Halmos with loop bounds}]
# Default: unroll loops 2 times
halmos --function check_invariant

# Increase for thorough checking (slower)
halmos --function check_invariant --loop 10

# Set solver timeout
halmos --function check_invariant --solver-timeout-assertion 60000
\end{lstlisting}

%% ============================================================