dapphub / dapphub/dapptools

hevm: expand symbolic tests

Open
#468 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
Haskell
Stars
2.1k
Forks
320
PR merge metrics
No merged PRs in 30d

Description

This is a tracking issue containing ideas for expanding the test coverage of the symbolic execution modes of hevm.

- [ ] integrate the solc semanticTests (see [here](https://github.com/dapphub/dapptools/pull/467#issuecomment-668019856)).
- [ ] generate a set of negative tests for hevm equivalence by manually modifying the yul optimizer tests
- [ ] integrate hevm symbolic into the test suite [here](https://github.com/dddejan/solidity-semantics-tests)
- [ ] explore the contracts in the [solc-verify test suite](https://github.com/SRI-CSL/solidity/tree/boogie/test/solc-verify) and compare the results
- [ ] explore the contracts in the [verisol test suite](https://github.com/microsoft/verisol/tree/master/Test/regressions) and compare the results
- [ ] run `hevm equivalence` against optimized and unoptimized versions of all of the above contracts
- [ ] confirm the verification results in [`k-dss`](https://github.com/dapphub/k-dss) and [`k-uniswap-v2`](https://github.com/dapp-org/k-uniswap-v2) using `hevm symbolic` (requires integration with `act`)

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.