halmos v2 planning - Githubissues

a16z / halmos

A symbolic testing tool for EVM smart contracts

GNU Affero General Public License v3.0

813 stars 67 forks source link

halmos v2 planning #346

Open daejunpark opened 2 months ago

daejunpark commented 2 months ago

todo for v0.2.x:

[ ] keccak reasoning
- [x] concrete keccak handling #391
- [ ] local injectivity of hash, using inclusion set: if x and y in inclusion set, then hash(x) == hash(y) => x == y; and t is in inclusion set for all t used as input of hash
- [ ] #347 #230
- [ ] this may make condition slicing more efficient
[ ] smt fuzzer
[x] lazy concretization #392
[ ] network state inspection

external tests:

[x] update farcaster tests https://github.com/farcasterxyz/contracts/pull/431
[x] update morpho tests https://github.com/morpho-org/morpho-data-structures/pull/143
[ ] address openzeppelin test failures: https://github.com/OpenZeppelin/openzeppelin-contracts/pull/5034

investigate:

[ ] progress info
[ ] coverage report?

karmacoma-eth commented 1 month ago

architectural stuff:

[ ] release jsi
[ ] bake jsi into solvers image
[ ] test jsi integration in halmos
[ ] remove --test-parallel
[ ] fix --early-exit

daejunpark commented 1 month ago

backlog:

further discussion needed:

[ ] ignore when assertion solving timeout, default = 1m (or 100s for generic storage)
[ ] path condition slicing:
- tradeoff between overhead of maintaining dependencies and performance improvement is unclear

optional:

[ ] smt encoding using overflow predicates
[ ] preprocess and summarize function/contract paths, grouped by storage updates (a single merged path condition for all reverting paths)
[ ] path merging
[ ] hybrid dfs+bfs