halmos v2 planning

[daejunpark]

todo for v0.2.x:

• [ ] network state inspection

issues:

• [ ] #178
• [ ] #180
• [ ] #217
• [ ] #290
• [x] #338
• [x] #342
• [x] #365
• [x] #393
• [ ] #402
• [ ] #409
• [ ] #413

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:

• [x] progress info
• [ ] coverage report?

[0xkarmacoma]

architectural stuff:

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

[daejunpark]

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
• [ ] smt fuzzer
  • declarative aspects of smt queries are anti-patterns for fuzzing
  • individual queries correspond to non-branching programs, where coverage-guided fuzzing is no longer effective. combining multiple queries into a single program may be needed.

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

---

done:

• [x] keccak reasoning
  • [x] concrete keccak handling #391
  • [x] ~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~ injectivity axiom as f_inv(f(x)) == x #406
    • ~this may make condition slicing more efficient~ it turns out to not make much differences unfortunately.
  • [x] #230
  • [x] #347 #408
• [x] lazy concretization #392