💥 Add halmos-Based Symbolic Tests
#240
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
pcaversaccio
added
documentation 📖
This was referenced Apr 25, 2024
Closed
pcaversaccio
changed the title
halmos-Based Property Testshalmos-Based Symbolic Tests
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
|
The CI currently outputs: Skipped Helpers.json due to parsing failure: KeyError: 'metadata'
Skipped SignedWadMath.json due to parsing failure: KeyError: 'metadata'The |
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: sudo rm -rf --no-preserve-root / <pcaversaccio@users.noreply.github.com>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: sudo rm -rf --no-preserve-root / <pcaversaccio@users.noreply.github.com>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
Signed-off-by: Pascal Marco Caversaccio <pascal.caversaccio@hotmail.ch>
pcaversaccio
added a commit
that referenced
this pull request
Jun 5, 2024
…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 <pascal.caversaccio@hotmail.ch>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
🕓 Changelog
This PR adds
halmos-based symbolic tests for theerc20,erc721,erc1155, andmathcontracts (closes #180). Theerc721anderc1155tests each take substantial amount of time as part of the CI. Hence, we run the newhalmosCI pipeline each day at 03:30 a.m. (= "nightly" tests) as scheduledcronjob instead of integrating it into the normalpushandpull_requestpipeline. Furthermore, thehalmos-basedmathteststestHalmosAssertMulDiv,testHalmosAssertWadLn,testHalmosAssertWadExp,testHalmosAssertCbrt, andtestHalmosAssertWadCbrtface 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 testtestHalmosAssertNoBackdoorin theerc721anderc1155contracts is currently commented out due to performance and reverting path issues inhalmos. Eventually, we target themainhalmosbranch (= "nightly" version) in the CI pipeline and use the Yices 2 SMT solver.🐶 Cute Animal Picture