mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +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.
35 lines
1.2 KiB
TeX
35 lines
1.2 KiB
TeX
\section{Understanding Counterexamples}
|
|
|
|
|
|
When Halmos finds a violation, it produces a concrete counterexample. Reading these
|
|
correctly is critical.
|
|
|
|
\subsection{Anatomy of a Counterexample}
|
|
|
|
\begin{lstlisting}[language=bash,caption={Halmos counterexample output}]
|
|
$ halmos --function check_transfer_conserves_supply
|
|
Counterexample:
|
|
p_from_address = 0x1234...
|
|
p_to_address = 0x1234...
|
|
p_amount_uint256 = 1000
|
|
|
|
Violation: assert(supplyAfter == supplyBefore) at line 18
|
|
\end{lstlisting}
|
|
|
|
This tells us: when \texttt{from == to}, the transfer implementation double-counts.
|
|
The fix: add \texttt{vm.assume(from != to)} or fix the contract.
|
|
|
|
\subsection{False Positives}
|
|
|
|
Halmos may report violations that cannot occur in practice because:
|
|
\begin{itemize}[nosep]
|
|
\item \textbf{Missing assumptions}: The test does not constrain inputs enough. Fix: add
|
|
\texttt{vm.assume}.
|
|
\item \textbf{Abstracted storage}: Halmos starts with arbitrary storage unless you set
|
|
it up explicitly.
|
|
\item \textbf{Hash collisions}: Halmos treats \texttt{keccak256} as an uninterpreted
|
|
function. It may find ``collisions'' that cannot occur with the real hash function.
|
|
\end{itemize}
|
|
|
|
%% ============================================================
|