feat: execution traces (#199)

Introduces models for call contexts, messages and call outputs. Depending on the verbosity level, we now render a an execution trace for counterexample paths, setUp() + explored paths and test deployment (constructor) path.

This also introduces a number of semantic fixes related to context handling, such as:
- max call depth
- forbidden opcodes in static context
- reading returndata out of bounds reverts
 
Additionally we now have better handling of exceptions for control flow: we can halt the current context by raising a subclass of EvmException, or halt the current path by raising a subclass of HalmosException.

Co-authored-by: Daejun Park <[email protected]>

.git-blame-ignore-revs

@@ -1,2 +1,3 @@
 # Migrate code style to Black
 449404c7a2b318b8203dbccbeac11c87d20c422f
+00cc14c20659cbf717594451dfc7906b295dca98

examples/tokens/ERC20/remappings.txt

@@ -1 +1,2 @@
 openzeppelin/=../../../tests/lib/openzeppelin-contracts/contracts/
+ds-test/=../../../tests/lib/forge-std/lib/ds-test/src/

examples/tokens/ERC721/remappings.txt

@@ -1 +1,2 @@
 openzeppelin/=../../../tests/lib/openzeppelin-contracts/contracts/
+ds-test/=../../../tests/lib/forge-std/lib/ds-test/src/

pyproject.toml

@@ -34,3 +34,7 @@ halmos = "halmos.__main__:main"
 
 [tool.black]
 target-versions = ["py38", "py39", "py310", "py311"]
+
+[tool.pytest.ini_options]
+# TODO: re-add test_traces.py when we have a better way to support it in CI
+addopts = "--ignore=tests/lib/solady/ext/woke --ignore=tests/test_traces.py"