a16z
The toy tests are missing with the new halmos version
Describe the bug
Toy tests are missing check_ keyword so there is nothing to test
whitehat@fb6550204d45:~/halmos/examples/toy$ halmos
[⠊] Compiling...
[⠢] Compiling 2 files with 0.8.21
[⠆] Solc 0.8.21 finished in 90.13ms
Compiler run successful!
Error: No tests with the prefix `check_`
To Reproduce
git clone https://github.com/a16z/halmos/
cd halmos/examples/toy
halmos
Environment:
- OS: Ubuntu 22:04
- Python version: 3.9
- Halmos and other dependency versions: [e.g.,
pip list]
whitehat@fb6550204d45:~/halmos/examples/toy$ pip list
Package Version
------------------------- -------------
abch-tree-sitter 1.1.1
abch-tree-sitter-solidity 1.2.1
aiofiles 0.8.0
aiohttp 3.8.5
aiosignal 1.3.1
asttokens 2.0.5
async-timeout 4.0.3
attrs 23.1.0
backcall 0.2.0
bitarray 2.8.1
blinker 1.4
charset-normalizer 3.2.0
click 8.1.6
cryptography 3.4.8
cytoolz 0.12.2
dbus-python 1.2.18
decorator 5.1.1
distro 1.7.0
eth-abi 4.1.0
eth-account 0.8.0
eth-hash 0.5.2
eth-keyfile 0.6.1
eth-keys 0.4.0
eth-rlp 0.3.0
eth-typing 3.4.0
eth-utils 2.2.0
exceptiongroup 1.1.3
executing 1.2.0
frozenlist 1.4.0
graphviz 0.19.2
hexbytes 0.3.1
httplib2 0.20.2
idna 3.4
importlib-metadata 4.6.4
iniconfig 2.0.0
intervaltree 3.1.0
ipdb 0.13.13
ipython 8.14.0
jedi 0.19.0
jeepney 0.7.1
keyring 23.5.0
launchpadlib 1.10.16
lazr.restfulclient 0.14.4
lazr.uri 1.0.6
markdown-it-py 3.0.0
matplotlib-inline 0.1.6
mdurl 0.1.2
more-itertools 8.10.0
multidict 6.0.4
networkx 2.8.8
oauthlib 3.2.0
packaging 23.1
parsimonious 0.9.0
parso 0.8.3
pathvalidate 2.5.2
pexpect 4.8.0
pickleshare 0.7.5
pip 22.0.2
pluggy 1.2.0
prompt-toolkit 3.0.39
ptyprocess 0.7.0
pure-eval 0.2.2
pycryptodome 3.18.0
pydantic 1.10.12
Pygments 2.16.1
PyGObject 3.42.1
PyJWT 2.3.0
pyparsing 2.4.7
pytest 7.4.0
python-apt 2.4.0+ubuntu2
regex 2023.8.8
rich 13.5.2
rich-click 1.6.1
rlp 3.0.0
SecretStorage 3.3.1
setuptools 59.6.0
six 1.16.0
sortedcontainers 2.4.0
stack-data 0.6.2
tblib 1.7.0
tomli 2.0.1
toolz 0.12.0
traitlets 5.9.0
typing_extensions 4.7.1
unicorn 1.0.2
wadllib 1.3.6
watchdog 2.2.1
wcwidth 0.2.6
websocket-client 1.6.1
wheel 0.37.1
woke 3.5.0
yarl 1.9.2
z3-solver 4.12.2.0
zipp 1.0.0
Additional context I was performing some tests to check that halmos was well configured at the auditor-toolbox docker image and notice the toy version is old.
Recommendation: Add the check_ keyword to all the toy tests
Keeping the test prefix makes it easy in this case to run the forge fuzzer:
$ forge test
[PASS] testTotalPriceBuggy(uint96,uint32) (runs: 256, μ: 462, ~: 466)
I suppose though it would be cool to add /// @custom:halmos --function test to the Example.t.sol so that halmos knows how to process these out of the box.
We can update the toy examples as suggested by Karma, once #184 is fixed.
Closing this, the instructions in https://github.com/a16z/halmos/tree/main/examples/simple#simple-examples have the right command: halmos --function test