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.
45 lines
1.2 KiB
TeX
45 lines
1.2 KiB
TeX
\section{Halmos Symbolic Testing}
|
|
|
|
|
|
Where fuzzing samples the input space randomly, Halmos explores it exhaustively (within
|
|
loop bounds). We use Halmos for the strongest properties where fuzzing alone is
|
|
insufficient:
|
|
|
|
\begin{lstlisting}[language=Solidity,caption={Halmos symbolic test for access control}]
|
|
function check_onlyOwnerCanSetFee(
|
|
address caller,
|
|
uint256 newFee
|
|
) public {
|
|
vm.assume(caller != owner);
|
|
vm.prank(caller);
|
|
|
|
// Must revert for non-owner
|
|
try pool.setFee(newFee) {
|
|
assert(false); // Should not reach here
|
|
} catch {
|
|
// Expected: revert
|
|
}
|
|
}
|
|
\end{lstlisting}
|
|
|
|
\subsection{Complementary Techniques}
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}llll@{}}
|
|
\toprule
|
|
\textbf{Property Type} & \textbf{Foundry Fuzz} & \textbf{Foundry Invariant} & \textbf{Halmos} \\
|
|
\midrule
|
|
Single-tx invariant & Good & N/A & Best \\
|
|
Multi-tx invariant & N/A & Good & N/A \\
|
|
Edge case detection & Good & Good & Best \\
|
|
Sequence-dependent & N/A & Best & N/A \\
|
|
Proof guarantee & No & No & Yes \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{When to use each technique.}
|
|
\end{table}
|
|
|
|
%% ============================================================
|