8000 render known addresses in counterexamples · Issue #447 · a16z/halmos · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

render known addresses in counterexamples #447

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 < 8FD2 a class="Link--inTextBlock" href="https://docs.github.com/terms" target="_blank">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
Open
0xkarmacoma opened this issue Jan 27, 2025 · 0 comments
Open

render known addresses in counterexamples #447

0xkarmacoma opened this issue Jan 27, 2025 · 0 comments
Labels
enhancement New feature or request

Comments

@0xkarmacoma
Copy link
Collaborator

In this test:

https://github.com/0xAurelou/faucet-solidity/

Without the vm.deal(user, 0), one of the counterexamples reads like this:

Counterexample: 
    halmos_allowedAmount_uint256_f02bd9a_01 = 0x0000000000000000000000000000000000000000000000040000000001c00000
    halmos_owner_address_4e9e28c_03 = 0x0000000000000000010000000000000000000000
    halmos_waitTime_uint256_f81d8e0_02 = 0x0000000000000000000000000000000000000000000000000000000000000000
    p_user_address_39ff443_00 = 0x00000000000000000000000000000000000000000000000000000000aaaa0002

Most of these are arbitrary values, the key is p_user_address_39ff443_00 = ...aaaa0002, which is the address of the faucet. The counter
example immediately makes sense once you figure that out, but it's tricky without logging the addresses after deployment.

If instead we could show:

p_user_address_39ff443_00 = ETHFaucet_deploy_1

or

// would work if the tests included vm.label(faucet, "faucet")
p_user_address_39ff443_00 = faucet
@0xkarmacoma 0xkarmacoma added the enhancement New feature or request label Jan 27, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@0xkarmacoma
0