Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

馃挜 Integrate 馃悕 snekmate Contracts With Halmos #180

Closed
pcaversaccio opened this issue Nov 8, 2023 · 0 comments 路 Fixed by #207 or #240
Closed

馃挜 Integrate 馃悕 snekmate Contracts With Halmos #180

pcaversaccio opened this issue Nov 8, 2023 · 0 comments 路 Fixed by #207 or #240
Assignees
@pcaversaccio
Labels
feature 馃挜 New feature or request help wanted 馃啒 Extra attention is needed
Milestone
0.1.0

Comments

@pcaversaccio
Copy link
Owner

Halmos is a symbolic testing tool for EVM smart contracts. Solidity is currently offered by default, but Vyper support is added incrementally. Since we write all tests in Solidity (and is fully open-source), it integrates well with our test framework. Thus, we should use Halmos to formally verify 馃悕 snekmate contracts.

References
@pcaversaccio pcaversaccio self-assigned this Nov 8, 2023
@pcaversaccio pcaversaccio added feature 馃挜 New feature or request help wanted 馃啒 Extra attention is needed labels Nov 8, 2023
@pcaversaccio pcaversaccio added this to the 0.0.5 milestone Nov 8, 2023
@pcaversaccio pcaversaccio modified the milestones: 0.0.5, 0.1.0 Mar 7, 2024
@pcaversaccio pcaversaccio mentioned this issue Apr 2, 2024
Closed
32 tasks
This was referenced Apr 25, 2024
Merged
Merged
@pcaversaccio pcaversaccio linked a pull request Apr 25, 2024 that will close this issue
馃挜 Add halmos-Based Symbolic Tests #240
Merged
pcaversaccio added a commit that referenced this issue May 22, 2024
@pcaversaccio
馃挜 Add halmos-Based Symbolic Tests (#240)
459ec3f 
### 馃晸 Changelog

This PR adds [`halmos`](https://github.com/a16z/halmos)-based symbolic
tests for the `erc20`, `erc721`, `erc1155`, and `math` contracts (closes
#180). The `erc721` and `erc1155` tests each take substantial amount of
time as part of the CI. Hence, we run the new `halmos` CI pipeline each
day at 03:30 a.m. (= "nightly" tests) as scheduled `cron` job instead of
integrating it into the normal `push` and `pull_request` pipeline.
Furthermore, the `halmos`-based `math` tests `testHalmosAssertMulDiv`,
`testHalmosAssertWadLn`, `testHalmosAssertWadExp`,
`testHalmosAssertCbrt`, and `testHalmosAssertWadCbrt` face out of memory
issues as the timeout for the Z3 solver does not work for the queries of
these tests. Thus, these tests are currently commented out.
Additionally, the test `testHalmosAssertNoBackdoor` in the `erc721` and
`erc1155` contracts is currently commented out due to performance and
reverting path issues in `halmos`. Eventually, we target the `main`
`halmos` branch (= "nightly" version) in the CI pipeline and use the
[Yices 2 SMT solver](https://github.com/SRI-CSL/yices2).

---------

Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
@pcaversaccio pcaversaccio changed the title 馃挜 Integrate 馃悕 snekmate Contracts with Halmos 馃挜 Integrate 馃悕 snekmate Contracts With Halmos Jun 3, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@pcaversaccio pcaversaccio

Labels
feature 馃挜 New feature or request help wanted 馃啒 Extra attention is needed
Projects
None yet
Milestone
0.1.0
1 participant
@pcaversaccio