karmacoma
Halmos is an EVM-level tool, which means that in principle we can target any bytecode, regardless of the source language used (Solidity, Vyper, Huff, ...) However at the moment at...
The issue is described here: https://github.com/Uniswap/v3-periphery/issues/52 can halmos find the problem and produce a counterexample? If it does, we should consider it for inclusion under tests/
Currently: - tests with no counterexamples return 0 and a green `[PASS]` - tests with counterexamples, or `unknown` results return non-0 and a red `[FAIL]` This makes running the test...
**Is your feature request related to a problem? Please describe.** Using `makeAddr("name")` (from forge-std) in a test results in the following error: ``` Warning: setUp() execution encountered an issue at...
## Problem When you run `forge test -vvv`, you get these nice traces:  This is great devex because it helps the developer make sense of how the error...
## Problem We currently only ever invoke Z3 to solve both path queries and assertion queries. This works well in general, but there is evidence in the literature that different...
## Problem We don't have a way to specify what version of the EVM we support. So for instance when support for PUSH0 was added, it means that we now...
`jumpi_id()` keeps showing up when I profile tests, because it causes us to eagerly compute `valid_jump_destinations()` Fundamentally, `valid_jump_destinations()` does a linear scan of the whole code for a contract. Even...
Take these tests: ```solidity function to_address(uint256 x) public pure returns (address) { return address(uint160(uint256(keccak256(abi.encode(x))))); } function test_uint256_collision(uint256 x, uint256 y) public { vm.assume(x != y); assertNotEq(keccak256(abi.encode(x)), keccak256(abi.encode(y))); } function test_uint160_collision(uint256...
**Describe the bug** As reported by https://t.me/c/1815219512/2277 and easily reproducible. We get the following warnings during the execution of `setUp()`: ``` WARNING:halmos:path.append(false) (see https://github.com/a16z/halmos/wiki/warnings#internal-error) WARNING:halmos:path.append(false) (see https://github.com/a16z/halmos/wiki/warnings#internal-error) ``` With some...