mirror of
https://github.com/lux-apps/papers.git
synced 2026-11-03 05:07:46 +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.
28 lines
842 B
TeX
28 lines
842 B
TeX
\section{Integrating Halmos into CI}
|
|
|
|
|
|
\begin{lstlisting}[language=YAML,caption={CI configuration for Halmos symbolic tests}]
|
|
symbolic-verification:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: actions/checkout@v4
|
|
- name: Install Foundry
|
|
uses: foundry-rs/foundry-toolchain@v1
|
|
- name: Install Halmos
|
|
run: pip install halmos
|
|
- name: Build contracts
|
|
run: forge build
|
|
- name: Run symbolic tests
|
|
run: |
|
|
halmos --function check_ \
|
|
--loop 5 \
|
|
--solver-timeout-assertion 120000 \
|
|
--solver-threads 4
|
|
\end{lstlisting}
|
|
|
|
Every pull request must pass all \texttt{check\_} tests before merge. Timeouts are
|
|
treated as failures: if the solver cannot decide, the test must be simplified or the
|
|
contract refactored.
|
|
|
|
%% ============================================================
|