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’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

💥 Add halmos-Based Symbolic Tests #240

Merged
merged 74 commits into from
May 22, 2024
Merged

💥 Add halmos-Based Symbolic Tests #240

merged 74 commits into from
May 22, 2024

Conversation

pcaversaccio
Copy link
Owner

@pcaversaccio pcaversaccio commented Apr 25, 2024 •
edited
Loading

🕓 Changelog

This PR adds 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.

🐶 Cute Animal Picture

image

@pcaversaccio
♻️ Started refactoring
310ad65 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ FML
b056c36 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ temporary fix and I hate it
4c36d4a 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ fix type issue
ed1d220 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
💥 Add halmos-Based Property Tests
d606d3c 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio pcaversaccio self-assigned this Apr 25, 2024
@pcaversaccio pcaversaccio added documentation 📖 Improvements or additions to documentation feature 💥 New feature or request dependencies 🔁 Pull requests that update a dependency file ci/cd 👷‍♂️ CI/CD configurations refactor/cleanup ♻️ Code refactorings and cleanups labels Apr 25, 2024
@pcaversaccio pcaversaccio added this to the 0.1.0 milestone Apr 25, 2024
This was referenced Apr 25, 2024
Merged
Closed
@pcaversaccio pcaversaccio changed the title 💥 Add halmos-Based Property Tests 💥 Add halmos-Based Symbolic Tests Apr 25, 2024
@pcaversaccio pcaversaccio linked an issue Apr 25, 2024 that may be closed by this pull request
💥 Integrate 🐍 snekmate Contracts With Halmos #180
Closed
@pcaversaccio
♻️ Rebasing
7e3b55e 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Rebasing
7d2be5c 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Rebasing
806e151 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Rebasing
40219af 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Small fix
a07133d 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
Copy link
Owner Author

pcaversaccio commented Apr 25, 2024 •
edited
Loading

The CI currently outputs:

Skipped Helpers.json due to parsing failure: KeyError: 'metadata'
Skipped SignedWadMath.json due to parsing failure: KeyError: 'metadata'

The Helpers contract is found here: lib/prb-test/src/Helpers.sol and the SignedWadMath contract here: lib/solmate/src/utils/SignedWadMath.sol. I reported the bug here: a16z/halmos#281.

pcaversaccio and others added 27 commits May 13, 2024 19:51
@pcaversaccio
Merge branch 'modules' into feat/halmos
2daa0d3 
Signed-off-by: sudo rm -rf --no-preserve-root / <[email protected]>
@pcaversaccio
👷 Add setuptools
d59caa0 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Speedup Fixes
d5e709e 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
Merge branch 'modules' into feat/halmos
96cbf3b
@pcaversaccio
Merge branch 'modules' into feat/halmos
ba1eb9f 
Signed-off-by: sudo rm -rf --no-preserve-root / <[email protected]>
@pcaversaccio
♻️ Fix echidna tests
377dfe1 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Fix cancun issue
0f8feda 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ I hate my life
e79b501 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
Merge branch 'modules' into feat/halmos
287ec43
@pcaversaccio
♻️ Prettify toml Files
3624359 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
👷 Move Halmos Tests to Separate CI Pipeline
c3fb817 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
👷 CI File Formatting
7abc917 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Refactor ERC20 Halmos Test
4f3e71b 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Set cron job time
b077a9c 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Wording
fd2636d 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Refactor ERC721 Halmos Test
ac9ef70 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ temporary debugging
1ff31c6 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ temporary debugging
e0be3d5 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ fix ERC1155 Test
069ccf5 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ fix ERC1155 Test
170b0c5 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ not testing the others now
1185197 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ fix test
9ea1b33 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ fix test
cd28e28 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ This must work
2d43bb7 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Full test
e3418b3 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Comment out testHalmosAssertNoBackdoor in ERC721
802cdab 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio
♻️ Cleanup
fc1712b 
Signed-off-by: Pascal Marco Caversaccio <[email protected]>
@pcaversaccio pcaversaccio merged commit 459ec3f into modules May 22, 2024
13 checks passed
@pcaversaccio pcaversaccio deleted the feat/halmos branch May 22, 2024 09:29
pcaversaccio added a commit that referenced this pull request Jun 5, 2024
@pcaversaccio
🔁 Upgrade to Vyper Version 0.4.0 and Make All 🐍 snekmate Contract…
4cb87bf 
…s Module-Friendly (#207)

██╗░░░██╗██╗░░░██╗██████╗░███████╗██████╗░
██║░░░██║╚██╗░██╔╝██╔══██╗██╔════╝██╔══██╗
╚██╗░██╔╝░╚████╔╝░██████╔╝█████╗░░██████╔╝
░╚████╔╝░░░╚██╔╝░░██╔═══╝░██╔══╝░░██╔══██╗
░░╚██╔╝░░░░░██║░░░██║░░░░░███████╗██║░░██║
░░░╚═╝░░░░░░╚═╝░░░╚═╝░░░░░╚══════╝╚═╝░░╚═╝

⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢀⣀⣤⣴⢶⣾⣞⠒⠶⢤⣀⡀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢰⡟⢩⣇⠀⢛⣿⡟⠀⠀⠀⠙⢿⡲⢤⣀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠘⣿⡒⡳⠒⠚⠙⠒⠂⠀⠀⠰⡄⢹⡄⢟⢷⣄⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠈⠉⢹⡿⠶⣶⣤⡤⠤⠤⠖⢿⠁⣹⣺⡾⠈⢷⡀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠈⡇⠀⠀⠘⣗⡒⠒⠒⢺⡏⣹⣽⡇⢰⠀⢳⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢸⠇⠀⠀⡄⢿⣉⠑⠒⢚⣏⣹⠉⡟⡞⢀⡎⡇⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⣼⠀⠀⠀⢧⣾⣮⣉⠒⢺⠋⡟⢺⣷⠛⣟⡼⣿⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢠⡏⠀⠀⣇⣼⣾⠃⠈⠁⡏⢸⠷⣇⣼⠚⠋⠀⡟⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢀⣿⠀⣠⢀⣟⣡⡏⠀⠀⣸⠁⣿⣟⣩⡄⢀⠀⣸⠇⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢸⣿⣠⠿⣼⢛⡟⠀⠀⢠⠃⢸⣟⡽⣥⠷⡜⣶⡟⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢸⡇⢹⣶⢯⢯⣉⠒⠶⡞⣠⣿⢯⡴⢧⢼⣿⠏⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠘⣷⣾⣸⠻⢤⣈⠉⣻⠉⢠⣇⣾⣷⣿⠟⠁⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠘⣿⠃⠀⠀⠀⣰⠃⢀⡿⣻⣿⠟⠁⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢀⣼⠋⠀⠀⠀⢠⠇⢀⣾⠟⠋⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⣼⠃⠀⠀⠀⠀⠀⢀⣾⠏⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢰⡏⠀⠀⠀⠀⠀⢀⣿⠏⢠⡿⣄⠀⠀⠀⠀⠀⠀⠀⠀⣀⣠⠴⠶⠶⠶⠤⣄⣀⠀⠀⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢠⣿⠀⠀⠀⠀⠀⢀⣾⡏⠀⠀⠻⣝⠷⣄⣀⣀⣀⣤⠶⠛⠁⠀⠀⠀⠀⠀⠀⠈⢻⡙⢶⣄⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⣀⣀⣀⣀⣀⣀⠀⢸⡇⡀⠘⢦⣰⢃⣸⣿⠀⠀⠀⠀⠙⢷⣄⣀⣩⣥⡤⠤⠦⠦⠤⢤⣤⣤⣤⣴⡶⠏⠀⠀⠙⡆⠀⠀⠀⠀⠀
⠀⠀⠀⣠⡴⠞⠛⠉⢀⡠⠆⠀⠉⠙⢻⡇⠙⠢⣄⣿⣁⣼⣿⣤⠤⠤⠶⠛⠛⠉⠁⠀⣀⣀⣠⡤⠤⠤⠴⢶⠤⠴⠦⠤⣤⣀⣀⣴⡇⠀⠀⠀⠀⠀
⠀⢀⡞⠁⠀⠀⠀⢠⡎⠀⠀⠀⠀⠀⢸⡇⠲⣄⡀⠙⣇⣼⣿⠀⠀⠀⠀⣀⣤⠶⠚⠛⠉⠀⠀⠀⠀⠀⠀⠈⠙⠓⢦⡀⠀⠀⠙⠛⠦⣤⡀⠀⠀⠀
⢠⡟⠀⠀⠀⠀⠀⢸⣄⣤⣤⢤⣤⣀⣸⡇⠀⠀⠉⣋⣯⣸⣿⣤⡤⠞⠋⠁⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢹⡄⠀⠀⠀⠀⠀⠙⢧⡀⠀
⢸⡇⠀⠀⠀⠀⠀⠘⢿⣉⠀⠀⠀⠉⠛⣿⠤⢤⣀⠈⠙⣤⡿⣧⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⣀⣀⣀⣤⣤⣤⣀⣸⣿⡄⠀⠀⠀⠀⠀⠘⣷⠀
⠸⣧⠀⠀⠀⠀⠀⠀⠀⠙⠛⠒⠒⠚⠛⢻⡆⠠⣄⣉⣉⣹⡼⢻⣧⠀⠀⠀⠀⠀⣀⣠⣤⠶⠟⠛⠋⠉⠀⠀⠀⠀⠀⠀⣹⡇⠀⠀⠀⠀⠀⠀⣹⠀
⠀⠘⢷⣄⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢻⣄⠀⠀⠀⠀⠹⣍⠈⠳⣦⣴⡾⠿⠛⠉⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⣠⡼⠋⠀⠀⠀⠀⠀⠀⢰⡿⡀
⠀⠀⠀⠙⠷⣤⣀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠻⣄⠀⠀⠀⠀⠈⠳⡄⠀⠉⠛⠲⠤⠤⣤⣀⣀⣤⠤⠤⠤⠔⠚⠋⠁⠀⠀⠀⠀⠀⠀⠀⢠⣿⠃⠀
⠀⠀⠀⠀⠀⠈⠙⠛⠶⠤⣤⣤⣤⣤⣤⣤⣴⠶⠿⢧⣄⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢀⣴⡿⠁⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠉⠳⢦⣀⡀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⣀⣤⣶⠟⠋⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠈⠙⠒⠲⠤⠤⢤⣄⣀⣀⣀⣀⣀⣀⣠⣤⣤⣤⡤⠶⠶⠛⠛⠉⠀⠀⠀⠀⠀⠀⠀
⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⢀⣀⣀⠀⠀⠀⠀⠀⠀⠈⠉⠈⠁⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀⠀

### 🕓 Changelog

We bump the Vyper version to the latest breaking release `0.4.0`
(technically, since Vyper `0.4.0` has not been released yet, we use the
latest release candidate
`0.4.0rc6` (https://github.com/vyperlang/vyper/releases/tag/v0.4.0rc6)
instead), which implements _stateless_ (see
vyperlang/vyper@c6f457a)
and _stateful_ modules (see
vyperlang/vyper@8ccacb3).
Furthermore, all existing `🐍 snekmate` contracts have been refactored to
be module-friendly (closes #221):

- [x] Authentication
  - [x] `ownable` (#218)
  - [x] `ownable_2step` (#219)
  - [x] `access_control` (#216)
- [x] Extensions
  - [x] `erc2981` (#233)
  - [x] `erc4626` (#236)
- [x] Governance
  - [x] `timelock_controller` (#220)
- [x] Tokens
  - [x] `erc20` (#234)
  - [x] `erc721` (#237)
  - [x] `erc1155` (#238)
- [x] Utility Functions
  - [x] `base64` (#222)
  - [x] `batch_distributor` (#223)
  - [x] `create_address` (#224)
  - [x] `create2_address` (#225)
  - [x] `ecdsa` (#227)
  - [x] `message_hash_utils` (#227)
  - [x] `signature_checker` (#228)
  - [x] `eip712_domain_separator` (#229)
  - [x] `math` (#230)
  - [x] `merkle_proof_verification` (#231)
  - [x] `multicall` (#232)

Furthermore, this PR closes the following issues:
- [x] Closes #175 (#243),
- [x] Closes #184 (#239),
- [x] Closes #180 (#240).

Eventually, the following changes are implemented:
- [x] Use `snake_case` notation for module and mock contracts. (#242)
- [x] The mathematical utility functions `_log_2`, `_log_10`, and
`_log_256` are renamed to `_log2`, `_log10`, and `_log256`. (#242)
- [x] Add documentation on how to use 🐍 snekmate contracts as modules.
(#247)

---------

Signed-off-by: Pascal Marco Caversaccio <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@pcaversaccio pcaversaccio

Labels
ci/cd 👷‍♂️ CI/CD configurations dependencies 🔁 Pull requests that update a dependency file documentation 📖 Improvements or additions to documentation feature 💥 New feature or request refactor/cleanup ♻️ Code refactorings and cleanups
Projects
None yet
Milestone
0.1.0
Development

Successfully merging this pull request may close these issues.

💥 Integrate 🐍 snekmate Contracts With Halmos
1 participant
@pcaversaccio