karmacoma
Halmos systematically explores as many paths as possible, we should add some option to produce coverage reports. Some unordered thoughts: - we operate at the bytecode level, should we print...
## Problem sometimes symbolic state can cause forks during the execution of `setUp()` in surprising ways. For instance: ```sol // in a contract not meant to be deployed to a...
we don't have a very nice way to deal with empty byte sequences in general (for things like calldata, returndata, code). They get sometimes represented as `bytes()`, sometimes as `[]`,...
Validate the legality of jump destination targets Previously, you could jump anywhere in bytecode (inluding non-jumpdests or the middle of a PUSH), we did not validate that the bytecode jumped...
**Is your feature request related to a problem? Please describe.** Currently, you can jump anywhere in bytecode (inluding non-jumpdests or the middle of a PUSH), we do not validate that...
**Is your feature request related to a problem? Please describe.** We currently use only z3 to solve both path conditions and assertions. Some solvers like cvc5, bitwuzla or boolector, etc....
```solidity // SPDX-License-Identifier: MIT pragma solidity ^0.8.15; import "forge-std/Test.sol"; contract Test49 is Test { function test_concreteKeccak_up() external { bytes32 hash = keccak256(abi.encodePacked(uint256(3))); uint256 bit = uint256(hash) & 1; if (uint256(hash)...
``` // SPDX-License-Identifier: UNLICENSED pragma solidity ^0.8.19; import {SymTest} from "halmos-cheatcodes/SymTest.sol"; import {Test, console2} from "forge-std/Test.sol"; import {WETH9} from "../src/WETH9.sol"; contract WETHSymTest is SymTest, Test { WETH9 weth; function setUp()...
**Describe the bug** The huff deployer from foundry-huff does a lot of things under the hood and we don't support it atm. **To Reproduce** - install foundry-huff - use the...
``` /// @custom:halmos --array-lengths m=5 function test_dynamic_bytes(bytes memory m) { console.log(m.length); } ``` I would have expected m.length to be 5, but it was 0x41 in my test. The alternative...