halmos v2 planning

[daejunpark]

todo for v0.2.x:

• network state inspection

issues:

• Create a test that demonstrates the payable multicall vulnerability #178
• Halmos throws Counterexample: unknown warning on solc versions < 0.8.17 #180
• Halmos is not able to generate paths for contracts deployed with CREATE3 #217
• Add cancun support #290
• WARNING:halmos:path.append(false) in Damn Vulnerable Defi - NaiveReceiver.t.sol #338
• Messages for unknown calls #342
• feat: add support for new symbolic-friendly vm cheatcodes #365
• support for Uniswap v2 testing workflow #393
• Halmos fails with Z3Exception: b'parser error' in MODEXP #402
• support expectRevert and expectEmit cheatcodes #409
• halmos should not generate private keys that correspond to deployed contract addresses #413

external tests:

• update farcaster tests test: simplify symbolic tests using new halmos cheatcode farcasterxyz/contracts#431
• update morpho tests test: update halmos tests for new halmos version morpho-org/morpho-data-structures#143
• address openzeppelin test failures: Add Halmos support OpenZeppelin/openzeppelin-contracts#5034

investigate:

• progress info
• coverage report?

[0xkarmacoma]

architectural stuff:

• release jsi
• bake jsi into solvers image
• test jsi integration in halmos
• remove --test-parallel
• 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:

• keccak reasoning
  • concrete keccak handling feat: handle concrete keccaks concretely (WIP) #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 injectivity axiom as f_inv(f(x)) == x perf: improve hash injectivity constraints #406
    • this may make condition slicing more efficient it turns out to not make much differences unfortunately.
  • improve hash reasoning and performance #230
  • handle truncated hashes #347 feat: injectivity for truncated hashes #408
• lazy concretization feat: lazy concretization #392