papers/lux-symbolic-execution-halmos/sections/03-writing-symbolic-tests.tex

\section{Writing Symbolic Tests}


A Halmos symbolic test looks like a normal Foundry test, except:
\begin{itemize}[nosep]
  \item Function name starts with \texttt{check\_} (not \texttt{test\_}).
  \item Parameters are symbolic---Halmos provides all possible values.
  \item \texttt{assert} statements define the property to verify.
  \item \texttt{vm.assume} constrains symbolic inputs to valid ranges.
\end{itemize}

\subsection{Example: Token Transfer Conservation}

\begin{lstlisting}[language=Solidity,caption={Symbolic test: total supply is conserved by transfers}]
function check_transfer_conserves_supply(
    address from,
    address to,
    uint256 amount
) public {
    // Preconditions
    vm.assume(from != to);
    vm.assume(from != address(0));
    vm.assume(to != address(0));

    // Record state before
    uint256 supplyBefore = token.totalSupply();
    uint256 fromBefore = token.balanceOf(from);
    uint256 toBefore = token.balanceOf(to);

    // Assume from has enough balance
    vm.assume(fromBefore >= amount);

    // Execute
    vm.prank(from);
    token.transfer(to, amount);

    // Verify conservation
    uint256 supplyAfter = token.totalSupply();
    assert(supplyAfter == supplyBefore);
    assert(token.balanceOf(from) == fromBefore - amount);
    assert(token.balanceOf(to) == toBefore + amount);
}
\end{lstlisting}

Halmos will symbolically execute this for \emph{all} values of \texttt{from},
\texttt{to}, and \texttt{amount} simultaneously. If any combination violates an
assertion, Halmos produces concrete values that trigger the violation.

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