karmacoma

Support vyper jumptables

3

**Is your feature request related to a problem? Please describe.** Newer versions of vyper use jumptable-based dispatchers. We don't currently handle them very gracefully because of the mod operation. For...

we actually do have an option that can help: ``` Solver options: --smt-exp-by-const N interpret constant power up to N (default: 2) ```

as is the case in this test: ```solidity function test_expRefinement(uint256 x) external { vm.assume(x != 0); unchecked { assert(x ** 4 != 0); } } ```

Support for missing EVM opcodes

4

Opcodes to support: - [x] CREATE (#21) - [x] CREATE2 (#163) - [x] DELEGATECALL (#159) - [x] CALLCODE (#159) - [x] EXTCODECOPY - [x] MSIZE (#38) - [x] ADDMOD (#101)...

TypeError: object of type 'BitVecRef' has no len() in padded_slice

1

Repro with: ```solidity // SPDX-License-Identifier: MIT pragma solidity ^0.8.15; import "forge-std/Test.sol"; import {SymTest} from "halmos-cheatcodes/SymTest.sol"; import {console2} from "forge-std/console2.sol"; contract WithImmutable { address immutable target; constructor(address _target) { target =...

Support configuration via halmos.toml

1

## Problem Currently, halmos only supports configuration via command line arguments. There are problems with this: - the number of arguments is growing quite a bit, and likely to continue...

## Problem If you're a halmos user, how hard is it to integrate in your CI? ## Solution Maybe having a nicely packaged halmos GitHub Action would help? Real question,...

Parse symbols from build to print readable traces

1

**Is your feature request related to a problem? Please describe.** Traces currently display only EVM-level raw hex values (for logs, calldata, deployed contracts, etc). **Describe the solution you'd like** It...

# Problem Non-linear arithmetic on bitvectors is very expensive for SMT solvers. Simple queries take a very long time to complete, for instance: ```py from z3 import * x =...

# Problem The behavior of assertions in StdAssertions.sol in [forge-std v1.8.0](https://github.com/foundry-rs/forge-std/releases/tag/v1.8.0) is changing. The old behavior is a "soft assert" in solidity, it logs a message and calls `fail()` to...