Display foundry-style traces

[0xkarmacoma]

Problem

When you run forge test -vvv, you get these nice traces:

This is great devex because it helps the developer make sense of how the error happens and the path to get there.

The thing is, halmos deals with not just one but many paths and it would be super helpful to visualize the explored paths in this way.

Solution

At the right level of verbosity, we should display not just the counterexample but also the path that got there.

At the right debug level, we could also display all explored paths like this (1 path = 1 trace), to make sure the path exploration phase is hitting the right areas.

Bonus points for displaying:

• [ ] nice contract names
• [ ] nice function names
• [ ] pretty printed calldata
• [ ] logs