diff --git a/.github/workflows/update-expected-output.yml b/.github/workflows/update-expected-output.yml
index fb97845d5..69f16eb3c 100644
--- a/.github/workflows/update-expected-output.yml
+++ b/.github/workflows/update-expected-output.yml
@@ -28,11 +28,12 @@ jobs:
docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
- name: 'Run integration tests'
run: |
- docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS='--numprocesses=6 --update-expected-output -vv -k "not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)"'
- docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS='--numprocesses=6 --update-expected-output -vv -k "test_kontrol_cse or test_foundry_minimize_proof"'
+ TEST_ARGS="--maxfail=1000 --numprocesses=6 --update-expected-output --force-sequential -vv"
+ docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)\"' || true"
+ docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} bash -c "make cov-integration TEST_ARGS='${TEST_ARGS} -k \"test_kontrol_cse or test_foundry_minimize_proof\"' || true"
- name: 'Copy updated files to host'
run: |
- docker cp kontrol-ci-integration-${GITHUB_SHA}:/home/user/src/tests/integration/test-data/show ./src/tests/integration/test-data/show
+ docker cp kontrol-ci-integration-${GITHUB_SHA}:/home/github-user/workspace/src/tests/integration/test-data/show ./src/tests/integration/test-data/
- name: 'Configure GitHub user'
run: |
git config user.name devops
diff --git a/deps/k_release b/deps/k_release
index d5d966726..0fc5d288c 100644
--- a/deps/k_release
+++ b/deps/k_release
@@ -1 +1 @@
-7.1.131
+7.1.145
diff --git a/deps/kevm_release b/deps/kevm_release
index 8760327c7..6afafdddf 100644
--- a/deps/kevm_release
+++ b/deps/kevm_release
@@ -1 +1 @@
-1.0.709
+1.0.727
diff --git a/flake.lock b/flake.lock
index c1513c84e..cc6b32833 100644
--- a/flake.lock
+++ b/flake.lock
@@ -49,17 +49,17 @@
"xbyak": "xbyak"
},
"locked": {
- "lastModified": 1725480100,
- "narHash": "sha256-2gTqoktcvJUAmH4ES0B+r0BNt0PLPEYnCbZQxcIuJUA=",
+ "lastModified": 1726502502,
+ "narHash": "sha256-J9IJiXHyCh42z65mEHYj/gnSLxOxbOF0riX8SLlQ3l8=",
"owner": "runtimeverification",
"repo": "blockchain-k-plugin",
- "rev": "a18c1d424957f794a1254d7e560712749c2aeb10",
+ "rev": "f1f7edb7cb7286906fe42aa37d2106036cef849f",
"type": "github"
},
"original": {
"owner": "runtimeverification",
"repo": "blockchain-k-plugin",
- "rev": "a18c1d424957f794a1254d7e560712749c2aeb10",
+ "rev": "f1f7edb7cb7286906fe42aa37d2106036cef849f",
"type": "github"
}
},
@@ -134,11 +134,11 @@
"systems": "systems_2"
},
"locked": {
- "lastModified": 1694529238,
- "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
+ "lastModified": 1710146030,
+ "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
"owner": "numtide",
"repo": "flake-utils",
- "rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
+ "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
"type": "github"
},
"original": {
@@ -152,11 +152,11 @@
"systems": "systems_5"
},
"locked": {
- "lastModified": 1694529238,
- "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
+ "lastModified": 1710146030,
+ "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
"owner": "numtide",
"repo": "flake-utils",
- "rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
+ "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
"type": "github"
},
"original": {
@@ -351,16 +351,16 @@
]
},
"locked": {
- "lastModified": 1725395202,
- "narHash": "sha256-UCMS6H8zIjFzN4xAXdCNcW7UChAp9knpRnscTg5z+jA=",
+ "lastModified": 1726170219,
+ "narHash": "sha256-pQG1D9oDG24h7I/ekTI96IGZ7ikWrip0m4o1uDFIBZc=",
"owner": "runtimeverification",
"repo": "k",
- "rev": "42e03545c319847e7df84e6fbc196b2f51c148a0",
+ "rev": "6e23a83e5380f9eae45a73e3956776f2e666da35",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v7.1.131",
+ "ref": "v7.1.142",
"repo": "k",
"type": "github"
}
@@ -390,16 +390,16 @@
]
},
"locked": {
- "lastModified": 1725395202,
- "narHash": "sha256-UCMS6H8zIjFzN4xAXdCNcW7UChAp9knpRnscTg5z+jA=",
+ "lastModified": 1726685098,
+ "narHash": "sha256-FVCrOS4IAlA08ZiYlmaSdrLoYFmSd7UFiJem/Zg2C8o=",
"owner": "runtimeverification",
"repo": "k",
- "rev": "42e03545c319847e7df84e6fbc196b2f51c148a0",
+ "rev": "c418935015dba62f29b9ada1a55b710126385ab6",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v7.1.131",
+ "ref": "v7.1.145",
"repo": "k",
"type": "github"
}
@@ -435,16 +435,16 @@
]
},
"locked": {
- "lastModified": 1725553368,
- "narHash": "sha256-u/KXzfzcAOTYRB/QN5XRS08x0VKx8t0maRalhZ72BMw=",
+ "lastModified": 1726723597,
+ "narHash": "sha256-2+Q0LXkbvuwV9PxQIDqHsscY/Ksj7Y3dVXuOgRTEhHU=",
"owner": "runtimeverification",
"repo": "evm-semantics",
- "rev": "5c533d3c8a8fc78c63c1cf11656cb2e1c65e52f0",
+ "rev": "2e0cae45e73e50c8e0a114f748dcf4d11234d107",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v1.0.709",
+ "ref": "v1.0.727",
"repo": "evm-semantics",
"type": "github"
}
@@ -485,16 +485,16 @@
"utils": "utils"
},
"locked": {
- "lastModified": 1724355360,
- "narHash": "sha256-wy+g2rVUn2dYoZ/JSA8x0cWNWYDxnxLpAzaucjUBciQ=",
+ "lastModified": 1726098480,
+ "narHash": "sha256-BOCKGOKzJLlYHSOCd2QOERS/sE038domlBc1h6nvM5s=",
"owner": "runtimeverification",
"repo": "llvm-backend",
- "rev": "b9d2a6da360e2b14a60a22928d625f43fb71ae02",
+ "rev": "344d1335c0fb8d146b0fa2954b0194afbe11dae6",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v0.1.84",
+ "ref": "v0.1.88",
"repo": "llvm-backend",
"type": "github"
}
@@ -517,16 +517,16 @@
"utils": "utils_2"
},
"locked": {
- "lastModified": 1724355360,
- "narHash": "sha256-wy+g2rVUn2dYoZ/JSA8x0cWNWYDxnxLpAzaucjUBciQ=",
+ "lastModified": 1726098480,
+ "narHash": "sha256-BOCKGOKzJLlYHSOCd2QOERS/sE038domlBc1h6nvM5s=",
"owner": "runtimeverification",
"repo": "llvm-backend",
- "rev": "b9d2a6da360e2b14a60a22928d625f43fb71ae02",
+ "rev": "344d1335c0fb8d146b0fa2954b0194afbe11dae6",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v0.1.84",
+ "ref": "v0.1.88",
"repo": "llvm-backend",
"type": "github"
}
@@ -542,11 +542,11 @@
]
},
"locked": {
- "lastModified": 1693660503,
- "narHash": "sha256-B/g2V4v6gjirFmy+I5mwB2bCYc0l3j5scVfwgl6WOl8=",
+ "lastModified": 1703863825,
+ "narHash": "sha256-rXwqjtwiGKJheXB43ybM8NwWB8rO2dSRrEqes0S7F5Y=",
"owner": "nix-community",
"repo": "nix-github-actions",
- "rev": "bd5bdbb52350e145c526108f4ef192eb8e554fa0",
+ "rev": "5163432afc817cf8bd1f031418d1869e4c9d5547",
"type": "github"
},
"original": {
@@ -565,11 +565,11 @@
]
},
"locked": {
- "lastModified": 1693660503,
- "narHash": "sha256-B/g2V4v6gjirFmy+I5mwB2bCYc0l3j5scVfwgl6WOl8=",
+ "lastModified": 1703863825,
+ "narHash": "sha256-rXwqjtwiGKJheXB43ybM8NwWB8rO2dSRrEqes0S7F5Y=",
"owner": "nix-community",
"repo": "nix-github-actions",
- "rev": "bd5bdbb52350e145c526108f4ef192eb8e554fa0",
+ "rev": "5163432afc817cf8bd1f031418d1869e4c9d5547",
"type": "github"
},
"original": {
@@ -963,11 +963,11 @@
]
},
"locked": {
- "lastModified": 1697388351,
- "narHash": "sha256-63N2eBpKaziIy4R44vjpUu8Nz5fCJY7okKrkixvDQmY=",
+ "lastModified": 1719749022,
+ "narHash": "sha256-ddPKHcqaKCIFSFc/cvxS14goUhCOAwsM1PbMr0ZtHMg=",
"owner": "numtide",
"repo": "treefmt-nix",
- "rev": "aae39f64f5ecbe89792d05eacea5cb241891292a",
+ "rev": "8df5ff62195d4e67e2264df0b7f5e8c9995fd0bd",
"type": "github"
},
"original": {
@@ -986,11 +986,11 @@
]
},
"locked": {
- "lastModified": 1697388351,
- "narHash": "sha256-63N2eBpKaziIy4R44vjpUu8Nz5fCJY7okKrkixvDQmY=",
+ "lastModified": 1719749022,
+ "narHash": "sha256-ddPKHcqaKCIFSFc/cvxS14goUhCOAwsM1PbMr0ZtHMg=",
"owner": "numtide",
"repo": "treefmt-nix",
- "rev": "aae39f64f5ecbe89792d05eacea5cb241891292a",
+ "rev": "8df5ff62195d4e67e2264df0b7f5e8c9995fd0bd",
"type": "github"
},
"original": {
diff --git a/flake.nix b/flake.nix
index 08d4a2a38..2751a9a4f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -2,7 +2,7 @@
description = "Kontrol";
inputs = {
- kevm.url = "github:runtimeverification/evm-semantics/v1.0.709";
+ kevm.url = "github:runtimeverification/evm-semantics/v1.0.727";
nixpkgs.follows = "kevm/nixpkgs";
k-framework.follows = "kevm/k-framework";
flake-utils.follows = "kevm/flake-utils";
diff --git a/poetry.lock b/poetry.lock
index 68a7e6151..6283c34c5 100644
--- a/poetry.lock
+++ b/poetry.lock
@@ -465,19 +465,19 @@ testing = ["hatch", "pre-commit", "pytest", "tox"]
[[package]]
name = "filelock"
-version = "3.15.4"
+version = "3.16.1"
description = "A platform independent file lock."
optional = false
python-versions = ">=3.8"
files = [
- {file = "filelock-3.15.4-py3-none-any.whl", hash = "sha256:6ca1fffae96225dab4c6eaf1c4f4f28cd2568d3ec2a44e15a08520504de468e7"},
- {file = "filelock-3.15.4.tar.gz", hash = "sha256:2207938cbc1844345cb01a5a95524dae30f0ce089eba5b00378295a17e3e90cb"},
+ {file = "filelock-3.16.1-py3-none-any.whl", hash = "sha256:2082e5703d51fbf98ea75855d9d5527e33d8ff23099bec374a134febee6946b0"},
+ {file = "filelock-3.16.1.tar.gz", hash = "sha256:c249fbfcd5db47e5e2d6d62198e565475ee65e4831e2561c8e313fa7eb961435"},
]
[package.extras]
-docs = ["furo (>=2023.9.10)", "sphinx (>=7.2.6)", "sphinx-autodoc-typehints (>=1.25.2)"]
-testing = ["covdefaults (>=2.3)", "coverage (>=7.3.2)", "diff-cover (>=8.0.1)", "pytest (>=7.4.3)", "pytest-asyncio (>=0.21)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)", "pytest-timeout (>=2.2)", "virtualenv (>=20.26.2)"]
-typing = ["typing-extensions (>=4.8)"]
+docs = ["furo (>=2024.8.6)", "sphinx (>=8.0.2)", "sphinx-autodoc-typehints (>=2.4.1)"]
+testing = ["covdefaults (>=2.3)", "coverage (>=7.6.1)", "diff-cover (>=9.2)", "pytest (>=8.3.3)", "pytest-asyncio (>=0.24)", "pytest-cov (>=5)", "pytest-mock (>=3.14)", "pytest-timeout (>=2.3.1)", "virtualenv (>=20.26.4)"]
+typing = ["typing-extensions (>=4.12.2)"]
[[package]]
name = "flake8"
@@ -556,6 +556,17 @@ files = [
classify-imports = "*"
flake8 = "*"
+[[package]]
+name = "future"
+version = "1.0.0"
+description = "Clean single-source support for Python 3 and 2"
+optional = false
+python-versions = ">=2.6, !=3.0.*, !=3.1.*, !=3.2.*"
+files = [
+ {file = "future-1.0.0-py3-none-any.whl", hash = "sha256:929292d34f5872e70396626ef385ec22355a1fae8ad29e1a734c3e43f9fbc216"},
+ {file = "future-1.0.0.tar.gz", hash = "sha256:bd2968309307861edae1458a4f8a4f3598c03be43b97521076aebf5d94c07b05"},
+]
+
[[package]]
name = "graphviz"
version = "0.20.3"
@@ -588,13 +599,13 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve
[[package]]
name = "hypothesis"
-version = "6.111.2"
+version = "6.112.1"
description = "A library for property-based testing"
optional = false
python-versions = ">=3.8"
files = [
- {file = "hypothesis-6.111.2-py3-none-any.whl", hash = "sha256:055e8228958e22178d6077e455fd86a72044d02dac130dbf9c8b31e161b9809c"},
- {file = "hypothesis-6.111.2.tar.gz", hash = "sha256:0496ad28c7240ee9ba89fcc7fb1dc74e89f3e40fbcbbb5f73c0091558dec8e6e"},
+ {file = "hypothesis-6.112.1-py3-none-any.whl", hash = "sha256:93631b1498b20d2c205ed304cbd41d50e9c069d78a9c773c1324ca094c5e30ce"},
+ {file = "hypothesis-6.112.1.tar.gz", hash = "sha256:b070d7a1bb9bd84706c31885c9aeddc138e2b36a9c112a91984f49501c567856"},
]
[package.dependencies]
@@ -621,22 +632,26 @@ zoneinfo = ["backports.zoneinfo (>=0.2.1)", "tzdata (>=2024.1)"]
[[package]]
name = "importlib-metadata"
-version = "8.4.0"
+version = "8.5.0"
description = "Read metadata from Python packages"
optional = false
python-versions = ">=3.8"
files = [
- {file = "importlib_metadata-8.4.0-py3-none-any.whl", hash = "sha256:66f342cc6ac9818fc6ff340576acd24d65ba0b3efabb2b4ac08b598965a4a2f1"},
- {file = "importlib_metadata-8.4.0.tar.gz", hash = "sha256:9a547d3bc3608b025f93d403fdd1aae741c24fbb8314df4b155675742ce303c5"},
+ {file = "importlib_metadata-8.5.0-py3-none-any.whl", hash = "sha256:45e54197d28b7a7f1559e60b95e7c567032b602131fbd588f1497f47880aa68b"},
+ {file = "importlib_metadata-8.5.0.tar.gz", hash = "sha256:71522656f0abace1d072b9e5481a48f07c138e00f079c38c8f883823f9c26bd7"},
]
[package.dependencies]
-zipp = ">=0.5"
+zipp = ">=3.20"
[package.extras]
+check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)"]
+cover = ["pytest-cov"]
doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"]
+enabler = ["pytest-enabler (>=2.2)"]
perf = ["ipython"]
-test = ["flufl.flake8", "importlib-resources (>=1.3)", "jaraco.test (>=5.4)", "packaging", "pyfakefs", "pytest (>=6,!=8.1.*)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-mypy", "pytest-perf (>=0.9.2)", "pytest-ruff (>=0.2.1)"]
+test = ["flufl.flake8", "importlib-resources (>=1.3)", "jaraco.test (>=5.4)", "packaging", "pyfakefs", "pytest (>=6,!=8.1.*)", "pytest-perf (>=0.9.2)"]
+type = ["pytest-mypy"]
[[package]]
name = "iniconfig"
@@ -665,7 +680,7 @@ colors = ["colorama (>=0.4.6)"]
[[package]]
name = "kevm-pyk"
-version = "1.0.709"
+version = "1.0.727"
description = ""
optional = false
python-versions = "^3.10"
@@ -673,26 +688,26 @@ files = []
develop = false
[package.dependencies]
-kframework = "7.1.131"
+kframework = "7.1.145"
pathos = "*"
tomlkit = "^0.11.6"
[package.source]
type = "git"
url = "https://github.com/runtimeverification/evm-semantics.git"
-reference = "v1.0.709"
-resolved_reference = "5c533d3c8a8fc78c63c1cf11656cb2e1c65e52f0"
+reference = "v1.0.727"
+resolved_reference = "2e0cae45e73e50c8e0a114f748dcf4d11234d107"
subdirectory = "kevm-pyk"
[[package]]
name = "kframework"
-version = "7.1.131"
+version = "7.1.145"
description = ""
optional = false
python-versions = "<4.0,>=3.10"
files = [
- {file = "kframework-7.1.131-py3-none-any.whl", hash = "sha256:b16de689e8b4c70f6484b5b399b09a9dbe35ffbc847fce719d7c17de53d2ee9f"},
- {file = "kframework-7.1.131.tar.gz", hash = "sha256:2052038a3c8627f3127a3efb5de41d8fce462c3119f91d47a958d2c8e8687553"},
+ {file = "kframework-7.1.145-py3-none-any.whl", hash = "sha256:a9107a75d25906200db2510ccb931358b8b50eb5bbd0f60680d50ace994baa19"},
+ {file = "kframework-7.1.145.tar.gz", hash = "sha256:2e6254450247ab79227fef430d3824076a377a8ec2a7648b8274c2e403d91938"},
]
[package.dependencies]
@@ -767,13 +782,13 @@ files = [
[[package]]
name = "mdit-py-plugins"
-version = "0.4.1"
+version = "0.4.2"
description = "Collection of plugins for markdown-it-py"
optional = false
python-versions = ">=3.8"
files = [
- {file = "mdit_py_plugins-0.4.1-py3-none-any.whl", hash = "sha256:1020dfe4e6bfc2c79fb49ae4e3f5b297f5ccd20f010187acc52af2921e27dc6a"},
- {file = "mdit_py_plugins-0.4.1.tar.gz", hash = "sha256:834b8ac23d1cd60cec703646ffd22ae97b7955a6d596eb1d304be1e251ae499c"},
+ {file = "mdit_py_plugins-0.4.2-py3-none-any.whl", hash = "sha256:0c673c3f889399a33b95e88d2f0d111b4447bdfea7f237dab2d488f459835636"},
+ {file = "mdit_py_plugins-0.4.2.tar.gz", hash = "sha256:5f2cd1fdb606ddf152d37ec30e46101a60512bc0e5fa1a7002c36647b09e26b5"},
]
[package.dependencies]
@@ -932,19 +947,19 @@ flake8 = ">=5.0.0"
[[package]]
name = "platformdirs"
-version = "4.2.2"
+version = "4.3.6"
description = "A small Python package for determining appropriate platform-specific dirs, e.g. a `user data dir`."
optional = false
python-versions = ">=3.8"
files = [
- {file = "platformdirs-4.2.2-py3-none-any.whl", hash = "sha256:2d7a1657e36a80ea911db832a8a6ece5ee53d8de21edd5cc5879af6530b1bfee"},
- {file = "platformdirs-4.2.2.tar.gz", hash = "sha256:38b7b51f512eed9e84a22788b4bce1de17c0adb134d6becb09836e37d8654cd3"},
+ {file = "platformdirs-4.3.6-py3-none-any.whl", hash = "sha256:73e575e1408ab8103900836b97580d5307456908a03e92031bab39e4554cc3fb"},
+ {file = "platformdirs-4.3.6.tar.gz", hash = "sha256:357fb2acbc885b0419afd3ce3ed34564c13c9b95c89360cd9563f73aa5e2b907"},
]
[package.extras]
-docs = ["furo (>=2023.9.10)", "proselint (>=0.13)", "sphinx (>=7.2.6)", "sphinx-autodoc-typehints (>=1.25.2)"]
-test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=7.4.3)", "pytest-cov (>=4.1)", "pytest-mock (>=3.12)"]
-type = ["mypy (>=1.8)"]
+docs = ["furo (>=2024.8.6)", "proselint (>=0.14)", "sphinx (>=8.0.2)", "sphinx-autodoc-typehints (>=2.4)"]
+test = ["appdirs (==1.4.4)", "covdefaults (>=2.3)", "pytest (>=8.3.2)", "pytest-cov (>=5)", "pytest-mock (>=3.14)"]
+type = ["mypy (>=1.11.2)"]
[[package]]
name = "pluggy"
@@ -1016,17 +1031,17 @@ test = ["enum34", "ipaddress", "mock", "pywin32", "wmi"]
[[package]]
name = "pybind11"
-version = "2.13.5"
+version = "2.13.6"
description = "Seamless operability between C++11 and Python"
optional = false
python-versions = ">=3.7"
files = [
- {file = "pybind11-2.13.5-py3-none-any.whl", hash = "sha256:dc35a98b61a0d23ee8599b317664f5be7e259fdc369a3b810b1ebbc3f5674d27"},
- {file = "pybind11-2.13.5.tar.gz", hash = "sha256:ae33f635322f9d9741abde0c5f348bf9373f6c22298883395e586cb43c55574e"},
+ {file = "pybind11-2.13.6-py3-none-any.whl", hash = "sha256:237c41e29157b962835d356b370ededd57594a26d5894a795960f0047cb5caf5"},
+ {file = "pybind11-2.13.6.tar.gz", hash = "sha256:ba6af10348c12b24e92fa086b39cfba0eff619b61ac77c406167d813b096d39a"},
]
[package.extras]
-global = ["pybind11-global (==2.13.5)"]
+global = ["pybind11-global (==2.13.6)"]
[[package]]
name = "pycodestyle"
@@ -1080,6 +1095,24 @@ files = [
{file = "pycryptodome-3.20.0.tar.gz", hash = "sha256:09609209ed7de61c2b560cc5c8c4fbf892f8b15b1faf7e4cbffac97db1fffda7"},
]
+[[package]]
+name = "pyevmasm"
+version = "0.2.3"
+description = "Ethereum Virtual Machine (EVM) assembler and disassembler"
+optional = false
+python-versions = ">2.7"
+files = [
+ {file = "pyevmasm-0.2.3-py2-none-any.whl", hash = "sha256:6dbc96f7251a5287cc2af868c96c760c2343c882afe99d01996f8133a5769355"},
+ {file = "pyevmasm-0.2.3-py3-none-any.whl", hash = "sha256:57eeb2b8482a56b215402780e97c175ba11b34584d2ad0914deab146b37be540"},
+ {file = "pyevmasm-0.2.3.tar.gz", hash = "sha256:1b3334e2d25bfbc4fac5e14a5d7b814999256c12dbc4c34796b9982dad73fcf6"},
+]
+
+[package.dependencies]
+future = "*"
+
+[package.extras]
+dev = ["coverage", "flake8", "nose"]
+
[[package]]
name = "pyflakes"
version = "3.2.0"
@@ -1117,15 +1150,18 @@ files = [
[[package]]
name = "pyreadline3"
-version = "3.4.1"
+version = "3.5.4"
description = "A python implementation of GNU readline."
optional = false
-python-versions = "*"
+python-versions = ">=3.8"
files = [
- {file = "pyreadline3-3.4.1-py3-none-any.whl", hash = "sha256:b0efb6516fd4fb07b45949053826a62fa4cb353db5be2bbb4a7aa1fdd1e345fb"},
- {file = "pyreadline3-3.4.1.tar.gz", hash = "sha256:6f3d1f7b8a31ba32b73917cefc1f28cc660562f39aea8646d30bd6eff21f7bae"},
+ {file = "pyreadline3-3.5.4-py3-none-any.whl", hash = "sha256:eaf8e6cc3c49bcccf145fc6067ba8643d1df34d604a1ec0eccbf7a18e6d3fae6"},
+ {file = "pyreadline3-3.5.4.tar.gz", hash = "sha256:8d57d53039a1c75adba8e50dd3d992b28143480816187ea5efbd5c78e6c885b7"},
]
+[package.extras]
+dev = ["build", "flake8", "mypy", "pytest", "twine"]
+
[[package]]
name = "pytest"
version = "7.4.4"
@@ -1233,13 +1269,13 @@ tokenize-rt = ">=5.2.0"
[[package]]
name = "rich"
-version = "13.8.0"
+version = "13.8.1"
description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal"
optional = false
python-versions = ">=3.7.0"
files = [
- {file = "rich-13.8.0-py3-none-any.whl", hash = "sha256:2e85306a063b9492dffc86278197a60cbece75bcb766022f3436f567cae11bdc"},
- {file = "rich-13.8.0.tar.gz", hash = "sha256:a5ac1f1cd448ade0d59cc3356f7db7a7ccda2c8cbae9c7a90c28ff463d3e91f4"},
+ {file = "rich-13.8.1-py3-none-any.whl", hash = "sha256:1760a3c0848469b97b558fc61c85233e3dafb69c7a071b4d60c38099d3cd4c06"},
+ {file = "rich-13.8.1.tar.gz", hash = "sha256:8260cda28e3db6bf04d2d1ef4dbc03ba80a824c88b0e7668a0f23126a424844a"},
]
[package.dependencies]
@@ -1251,18 +1287,18 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"]
[[package]]
name = "setuptools"
-version = "74.1.2"
+version = "75.1.0"
description = "Easily download, build, install, upgrade, and uninstall Python packages"
optional = false
python-versions = ">=3.8"
files = [
- {file = "setuptools-74.1.2-py3-none-any.whl", hash = "sha256:5f4c08aa4d3ebcb57a50c33b1b07e94315d7fc7230f7115e47fc99776c8ce308"},
- {file = "setuptools-74.1.2.tar.gz", hash = "sha256:95b40ed940a1c67eb70fc099094bd6e99c6ee7c23aa2306f4d2697ba7916f9c6"},
+ {file = "setuptools-75.1.0-py3-none-any.whl", hash = "sha256:35ab7fd3bcd95e6b7fd704e4a1539513edad446c097797f2985e0e4b960772f2"},
+ {file = "setuptools-75.1.0.tar.gz", hash = "sha256:d59a21b17a275fb872a9c3dae73963160ae079f1049ed956880cd7c09b120538"},
]
[package.extras]
check = ["pytest-checkdocs (>=2.4)", "pytest-ruff (>=0.2.1)", "ruff (>=0.5.2)"]
-core = ["importlib-metadata (>=6)", "importlib-resources (>=5.10.2)", "jaraco.text (>=3.7)", "more-itertools (>=8.8)", "packaging (>=24)", "platformdirs (>=2.6.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"]
+core = ["importlib-metadata (>=6)", "importlib-resources (>=5.10.2)", "jaraco.collections", "jaraco.functools", "jaraco.text (>=3.7)", "more-itertools", "more-itertools (>=8.8)", "packaging", "packaging (>=24)", "platformdirs (>=2.6.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"]
cover = ["pytest-cov"]
doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "pyproject-hooks (!=1.1)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier", "towncrier (<24.7)"]
enabler = ["pytest-enabler (>=2.2)"]
@@ -1393,13 +1429,13 @@ files = [
[[package]]
name = "zipp"
-version = "3.20.1"
+version = "3.20.2"
description = "Backport of pathlib-compatible object wrapper for zip files"
optional = false
python-versions = ">=3.8"
files = [
- {file = "zipp-3.20.1-py3-none-any.whl", hash = "sha256:9960cd8967c8f85a56f920d5d507274e74f9ff813a0ab8889a5b5be2daf44064"},
- {file = "zipp-3.20.1.tar.gz", hash = "sha256:c22b14cc4763c5a5b04134207736c107db42e9d3ef2d9779d465f5f1bcba572b"},
+ {file = "zipp-3.20.2-py3-none-any.whl", hash = "sha256:a817ac80d6cf4b23bf7f2828b7cabf326f15a001bea8b1f9b49631780ba28350"},
+ {file = "zipp-3.20.2.tar.gz", hash = "sha256:bc9eb26f4506fda01b81bcde0ca78103b6e62f991b381fec825435c836edbc29"},
]
[package.extras]
@@ -1413,4 +1449,4 @@ type = ["pytest-mypy"]
[metadata]
lock-version = "2.0"
python-versions = "^3.10"
-content-hash = "861d3e7a0ca2f436563148b916980d1a93a4c3e88db597645cdd2c6c19f51a5e"
+content-hash = "007fe7af0702634f18b3dc804b5441add4d9b2ad5a4cd558862151cc2122dc97"
diff --git a/pyproject.toml b/pyproject.toml
index 3293c88e5..f2913bb84 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -12,9 +12,10 @@ authors = [
[tool.poetry.dependencies]
python = "^3.10"
-kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.709", subdirectory = "kevm-pyk" }
+kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.727", subdirectory = "kevm-pyk" }
eth-utils = "^4.1.1"
pycryptodome = "^3.20.0"
+pyevmasm = "^0.2.3"
[tool.poetry.group.dev.dependencies]
autoflake = "*"
diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py
index 5979bca6d..8eb5dd23c 100644
--- a/src/kontrol/__main__.py
+++ b/src/kontrol/__main__.py
@@ -40,6 +40,7 @@
from .hevm import Hevm
from .kompile import foundry_kompile
from .prove import foundry_prove
+from .solc import CompilationUnit
from .solc_to_k import solc_compile, solc_to_k
from .utils import _LOG_FORMAT, _rv_blue, _rv_yellow, check_k_version, config_file_path, console, loglevel
@@ -311,11 +312,13 @@ def exec_view_kcfg(options: ViewKcfgOptions) -> None:
contract_name, _ = test_id.split('.')
proof = foundry.get_apr_proof(test_id)
+ compilation_unit = CompilationUnit.load_build_info(options.foundry_root)
+
def _short_info(cterm: CTerm) -> Iterable[str]:
return foundry.short_info_for_contract(contract_name, cterm)
def _custom_view(elem: KCFGElem) -> Iterable[str]:
- return foundry.custom_view(contract_name, elem)
+ return foundry.custom_view(contract_name, elem, compilation_unit)
node_printer = foundry_node_printer(foundry, contract_name, proof)
viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view)
diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py
index 57ec7356e..6a90586a6 100644
--- a/src/kontrol/foundry.py
+++ b/src/kontrol/foundry.py
@@ -45,6 +45,7 @@
from pyk.utils import ensure_dir_path, hash_str, run_process_2, single, unique
from . import VERSION
+from .solc import CompilationUnit
from .solc_to_k import Contract, _contract_name_from_bytecode
from .state_record import RecreateState, StateDiffEntry, StateDumpEntry
from .utils import (
@@ -86,7 +87,6 @@
UnrefuteNodeOptions,
)
-
_LOGGER: Final = logging.getLogger(__name__)
@@ -347,6 +347,13 @@ def srcmap_data(self, contract_name: str, pc: int) -> tuple[Path, int, int] | No
_, start, end = byte_offset_to_lines(src_contract_text.split('\n'), s, l)
return (src_contract_path, start, end)
+ def solidity_src_print(self, path: Path, start: int, end: int) -> Iterable[str]:
+ lines = path.read_text().split('\n')
+ prefix_lines = [f' {l}' for l in lines[:start]]
+ actual_lines = [f' | {l}' for l in lines[start:end]]
+ suffix_lines = [f' {l}' for l in lines[end:]]
+ return prefix_lines + actual_lines + suffix_lines
+
def solidity_src(self, contract_name: str, pc: int) -> Iterable[str]:
srcmap_data = self.srcmap_data(contract_name, pc)
if srcmap_data is None:
@@ -354,11 +361,7 @@ def solidity_src(self, contract_name: str, pc: int) -> Iterable[str]:
contract_path, start, end = srcmap_data
if not (contract_path.exists() and contract_path.is_file()):
return [f'No file at path for contract {contract_name}: {contract_path}']
- lines = contract_path.read_text().split('\n')
- prefix_lines = [f' {l}' for l in lines[:start]]
- actual_lines = [f' | {l}' for l in lines[start:end]]
- suffix_lines = [f' {l}' for l in lines[end:]]
- return prefix_lines + actual_lines + suffix_lines
+ return self.solidity_src_print(contract_path, start, end)
def short_info_for_contract(self, contract_name: str, cterm: CTerm) -> list[str]:
ret_strs = self.kevm.short_info(cterm)
@@ -370,11 +373,21 @@ def short_info_for_contract(self, contract_name: str, cterm: CTerm) -> list[str]
ret_strs.append(f'src: {str(path)}:{start}:{end}')
return ret_strs
- def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]:
+ def custom_view(self, contract_name: str, element: KCFGElem, compilation_unit: CompilationUnit) -> Iterable[str]:
if type(element) is KCFG.Node:
pc_cell = element.cterm.try_cell('PC_CELL')
+ program_cell = element.cterm.try_cell('PROGRAM_CELL')
if type(pc_cell) is KToken and pc_cell.sort == INT:
- return self.solidity_src(contract_name, int(pc_cell.token))
+ if type(program_cell) is KToken:
+ try:
+ bytecode = ast.literal_eval(program_cell.token)
+ instruction = compilation_unit.get_instruction(bytecode, int(pc_cell.token))
+ node = instruction.node()
+ start_line, _, end_line, _ = node.source_range()
+ return self.solidity_src_print(Path(node.source.name), start_line - 1, end_line)
+ except Exception:
+ return [f'No sourcemap data for contract at pc {contract_name}: {int(pc_cell.token)}']
+ return ['NO DATA']
elif type(element) is KCFG.Edge:
return list(element.rules)
elif type(element) is KCFG.NDBranch:
@@ -382,11 +395,22 @@ def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]:
return ['NO DATA']
def build(self, no_metadata: bool) -> None:
- forge_build_args = ['forge', 'build', '--build-info', '--root', str(self._root)] + (
- ['--no-metadata'] if no_metadata else []
- )
+ forge_build_args = [
+ 'forge',
+ 'build',
+ '--build-info',
+ '--extra-output',
+ 'storageLayout',
+ 'evm.bytecode.generatedSources',
+ 'evm.deployedBytecode.generatedSources',
+ '--root',
+ str(self._root),
+ ] + (['--no-metadata'] if no_metadata else [])
try:
- run_process_2(forge_build_args, logger=_LOGGER)
+ run_process_2(
+ forge_build_args,
+ logger=_LOGGER,
+ )
except FileNotFoundError as err:
raise RuntimeError(
"Error: 'forge' command not found. Please ensure that 'forge' is installed and added to your PATH."
@@ -1351,24 +1375,32 @@ class FoundryNodePrinter(KEVMNodePrinter):
foundry: Foundry
contract_name: str
omit_unstable_output: bool
+ compilation_unit: CompilationUnit
def __init__(self, foundry: Foundry, contract_name: str, omit_unstable_output: bool = False):
KEVMNodePrinter.__init__(self, foundry.kevm)
self.foundry = foundry
self.contract_name = contract_name
self.omit_unstable_output = omit_unstable_output
+ self.compilation_unit = CompilationUnit.load_build_info(foundry._root)
def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
ret_strs = super().print_node(kcfg, node)
_pc = node.cterm.try_cell('PC_CELL')
+ program_cell = node.cterm.try_cell('PROGRAM_CELL')
+
if type(_pc) is KToken and _pc.sort == INT:
- srcmap_data = self.foundry.srcmap_data(self.contract_name, int(_pc.token))
- if not self.omit_unstable_output and srcmap_data is not None:
- path, start, end = srcmap_data
- ret_strs.append(f'src: {str(path)}:{start}:{end}')
+ if type(program_cell) is KToken:
+ try:
+ bytecode = ast.literal_eval(program_cell.token)
+ instruction = self.compilation_unit.get_instruction(bytecode, int(_pc.token))
+ ast_node = instruction.node()
+ start_line, _, end_line, _ = ast_node.source_range()
+ ret_strs.append(f'src: {str(Path(ast_node.source.name))}:{start_line}:{end_line}')
+ except Exception:
+ pass
calldata_cell = node.cterm.try_cell('CALLDATA_CELL')
- program_cell = node.cterm.try_cell('PROGRAM_CELL')
if type(program_cell) is KToken:
selector_bytes = None
diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md
index 455933b4a..40e33181b 100644
--- a/src/kontrol/kdist/cheatcodes.md
+++ b/src/kontrol/kdist/cheatcodes.md
@@ -328,15 +328,17 @@ This rule then takes from the function call data the account using `#asWord(#ran
```
function symbolicStorage(address) external;
+function setArbitraryStorage(address) external;
```
-`cheatcode.call.symbolicStorage` will match when the `symbolicStorage` cheat code function is called.
+`cheatcode.call.symbolicStorage` will match when either of the `symbolicStorage` or `setArbitraryStorage` cheat code functions are called.
This rule then takes the address using `#asWord(#range(ARGS, 0, 32))` and makes its storage completely symbolic.
```k
rule [cheatcode.call.symbolicStorage]:
#cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #setSymbolicStorage #asWord(ARGS) ...
requires SELECTOR ==Int selector ( "symbolicStorage(address)" )
+ orBool SELECTOR ==Int selector ( "setArbitraryStorage(address)")
```
#### `copyStorage` - Copies the storage of one account into another.
@@ -1585,6 +1587,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa
rule ( selector ( "expectEmit(bool,bool,bool,bool,address)" ) => 2176505587 )
rule ( selector ( "sign(uint256,bytes32)" ) => 3812747940 )
rule ( selector ( "symbolicStorage(address)" ) => 769677742 )
+ rule ( selector ( "setArbitraryStorage(address)" ) => 3781367863 )
rule ( selector ( "freshUInt(uint8)" ) => 625253732 )
rule ( selector ( "freshBool()" ) => 2935720297 )
rule ( selector ( "freshBytes(uint256)" ) => 1389402351 )
diff --git a/src/kontrol/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md
index d3c5d1a7b..51f02cf4e 100644
--- a/src/kontrol/kdist/kontrol_lemmas.md
+++ b/src/kontrol/kdist/kontrol_lemmas.md
@@ -33,16 +33,6 @@ module KONTROL-AUX-LEMMAS
rule ethUpperBound => 2 ^Int ethMaxWidth
// ----------------------------------------
- // chop and +Int
- rule [chop-plus]: chop (A +Int B) ==Int 0 => A ==Int (-1) *Int B
- requires #rangeUInt(256, A) andBool #rangeUInt(256, (-1) *Int B)
- [concrete(B), simplification, comm]
-
- // chop and -Int
- rule [chop-zero-minus]: chop (0 -Int A) ==Int B => A ==Int (pow256 -Int B) modInt pow256
- requires #rangeUInt(256, A) andBool #rangeUInt(256, B)
- [concrete(B), simplification, comm, preserves-definedness]
-
// ==Int
rule [int-eq-refl]: X ==Int X => true [simplification]
@@ -85,18 +75,6 @@ module KONTROL-AUX-LEMMAS
// modInt
rule (X *Int Y) modInt Z => 0 requires X modInt Z ==Int 0 [simplification, concrete(X, Z), preserves-definedness]
- // Further generalization of: maxUIntXXX &Int #asWord ( BA )
- rule X &Int #asWord ( BA ) => #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) )
- requires #rangeUInt(256, X)
- andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
- andBool log2Int (X +Int 1) modInt 8 ==Int 0
- andBool (log2Int (X +Int 1)) /Int 8 <=Int lengthBytes(BA) andBool lengthBytes(BA) <=Int 32
- [simplification, concrete(X), preserves-definedness]
-
- rule #asWord( BA ) >>Int N => #asWord( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) )
- requires 0 <=Int N andBool N modInt 8 ==Int 0
- [simplification, concrete(N), preserves-definedness]
-
// >>Int
rule [shift-to-div]: X >>Int N => X /Int (2 ^Int N)
requires 0 <=Int X andBool 0 <=Int N [simplification(60), concrete(N)]
@@ -105,24 +83,6 @@ module KONTROL-AUX-LEMMAS
rule B ==K false => notBool B [simplification(30), comm]
rule B ==K true => B [simplification(30), comm]
- // bool2Word
- rule bool2Word(X) ==Int 0 => notBool X [simplification(30), comm]
- rule bool2Word(X) =/=Int 0 => X [simplification(30), comm]
- rule bool2Word(X) ==Int 1 => X [simplification(30), comm]
- rule bool2Word(X) =/=Int 1 => notBool X [simplification(30), comm]
-
- rule [bool2Word-lt-true]: bool2Word(_:Bool) true requires 1 notBool B [simplification(30)]
- rule [bool2Word-gt-zero]: 0 B [simplification(30)]
- rule [bool2Word-gt-false]: X:Int false requires 1 true [simplification, smt-lemma]
- rule bool2Word(X) <=Int 1 => true [simplification, smt-lemma]
-
- rule bool2Word ( X ) xorInt bool2Word ( Y ) => bool2Word ( (X andBool notBool Y) orBool (notBool X andBool Y) ) [simplification]
- rule 1 xorInt bool2Word ( X ) => 1 -Int bool2Word ( X ) [simplification, comm]
- rule 0 xorInt bool2Word ( X ) => bool2Word ( X ) [simplification, comm]
-
//
// .Bytes
//
@@ -177,48 +137,6 @@ module KONTROL-AUX-LEMMAS
//
// Specific simplifications
//
- rule X &Int #asWord ( BA ) ==Int Y:Int => true
- requires 0 <=Int X andBool X false
- requires 0 <=Int X andBool X true
- requires 0 <=Int X andBool X false
- requires 0 <=Int X andBool X true
- requires 0 <=Int X andBool X false
- requires 0 <=Int X andBool X 0
requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z
andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
@@ -226,21 +144,6 @@ module KONTROL-AUX-LEMMAS
andBool log2Int(X +Int 1) <=Int log2Int(Y)
[simplification, concrete(X, Y), preserves-definedness]
- rule chop ( X *Int Y ) => X *Int Y
- requires 0 <=Int X andBool X X *Int Y { true #Equals X *Int Y (A /Int 10) *Int B <=Int (C /Int 10) *Int D
requires 0 <=Int A andBool 0 <=Int C andBool A modInt 10 ==Int 0 andBool C modInt 10 ==Int 0
@@ -262,12 +165,6 @@ module KONTROL-AUX-LEMMAS
rule X true requires X <=Int 0 andBool 0 <=Int A andBool 0 true requires X <=Int 0 andBool 0 X +Int Y X +Int Y X *Int Y X *Int Y X /Int Y X -Int Y
- requires #rangeUInt(256, X)
- andBool #rangeUInt(256, Y)
- andBool Y <=Int X
- [simplification]
-
rule X -Int Y <=Int Z => true
requires X <=Int Z
andBool 0 <=Int Y
@@ -316,13 +207,6 @@ module KONTROL-AUX-LEMMAS
requires 0 <=Int N andBool N notBool B orBool (B andBool C <=Int A)
- requires 0 <=Int A
- [simplification]
-
- rule bool2Word(X) *Int Y ==Int Z => (X andBool (Y ==Int Z)) orBool ((notBool X) andBool Z ==Int 0)
- [simplification]
-
rule X *Int Y <=Int Z => Y dict[str, Callable]:
| EVMChainOptions.get_argument_type()
| {
'match-test': list_of(parse_test_version_tuple),
- 'init-node-from': file_path,
+ 'init-node-from-diff': file_path,
+ 'init-node-from-dump': file_path,
'include-summary': list_of(parse_test_version_tuple),
}
)
diff --git a/src/kontrol/solc.py b/src/kontrol/solc.py
new file mode 100644
index 000000000..a13f5626b
--- /dev/null
+++ b/src/kontrol/solc.py
@@ -0,0 +1,595 @@
+from __future__ import annotations
+
+import hashlib
+import json
+import logging
+import os
+from collections import deque
+from functools import cache, cached_property
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+ from collections.abc import Iterator
+ from pathlib import Path
+
+import pyevmasm # type: ignore
+
+if TYPE_CHECKING:
+ from typing import Any
+
+ Json = dict[str, Any]
+
+ """
+ An AstNodeSourceMapEntry is triple (s,l,f) where
+ s denotes the start offset in bytes
+ l denotes the length in bytes
+ f denotes the identifier of the source unit
+ See: https://docs.soliditylang.org/en/latest/internals/source_mappings.html
+ """
+ AstNodeSourceMapEntry = tuple[int, int, int]
+
+ """
+ A ContractSourceMapEntry is a tuple (s,l,f,j,m) where
+ s denotes the start offset in bytes
+ l denotes the length in bytes
+ f denotes the identifier of the source unit
+ j denotes the jump type 'i', 'o', or '-'
+ m denotes the modifier depth
+ See: https://docs.soliditylang.org/en/latest/internals/source_mappings.html
+ """
+ ContractSourceMapEntry = tuple[int, int, int, str, int]
+
+ """
+ A contract source map is a map from instruction offsets to source map entries.
+ See: https://docs.soliditylang.org/en/latest/internals/source_mappings.html
+ """
+ ContractSourceMap = dict[int, ContractSourceMapEntry]
+
+ """
+ A line,column pair
+ """
+ LineColumn = tuple[int, int]
+
+ """
+ A source range is a tuple (start_line, start_column, end_line, end_column)
+ """
+ SourceRange = tuple[int, int, int, int]
+
+
+_LOGGER = logging.getLogger(__name__)
+
+
+class Instruction:
+
+ data: pyevmasm.Instruction
+ compilation_unit: CompilationUnit
+ contract: ContractSource
+ source_map_entry: ContractSourceMapEntry
+ offset: int
+
+ def __init__(
+ self,
+ data: pyevmasm.Instruction,
+ compilation_unit: CompilationUnit,
+ contract: ContractSource,
+ source_map_entry: ContractSourceMapEntry,
+ offset: int,
+ ):
+ self.data = data
+ self.compilation_unit = compilation_unit
+ self.contract = contract
+ self.source_map_entry = source_map_entry
+ self.offset = offset
+
+ @property
+ def pc(self) -> int:
+ return self.data.pc
+
+ @property
+ def operand_size(self) -> int:
+ return self.data.operand_size
+
+ def __str__(self) -> str:
+ return f'{self.data}'
+
+ def source_range(self) -> SourceRange:
+ try:
+ (s, l, f, *_) = self.source_map_entry
+ try:
+ source = self.compilation_unit.get_source_by_id(f)
+ except KeyError:
+ try:
+ source = self.contract.generated_sources[f]
+ except KeyError:
+ return (1, 1, 1, 1)
+ start_line, start_column = source.offset_to_position(s)
+ end_line, end_column = source.offset_to_position(s + l - 1)
+ return (start_line, start_column, end_line, end_column)
+ except Exception:
+ return (1, 1, 1, 1)
+
+ def node(self) -> AstNode:
+ try:
+ s, l, f, j, m = self.source_map_entry
+ try:
+ source = self.compilation_unit.get_source_by_id(f)
+ except KeyError:
+ source = self.contract.generated_sources[f]
+ node = source.ast.find_by_range(s, s + l)
+ assert node is not None
+ return node
+ except Exception as error:
+ raise Exception('Node not found.') from error
+
+
+class AstNode:
+ json: Json
+ parent: AstNode | None
+ source: Source
+
+ def __init__(self, dct: Json, source: Source, parent: AstNode | None = None):
+ self.json = dct
+ self.source = source
+ self.parent = parent
+
+ def __hash__(self) -> int:
+ result = self.json.get('id')
+ if isinstance(result, int):
+ return result
+ result = self.json.get('src')
+ if isinstance(result, str):
+ return hash(result)
+ raise TypeError('AstNode.id is not an int.')
+
+ def __eq__(self, other: Any) -> bool:
+ if not isinstance(other, AstNode):
+ return False
+ return self.json.get('src') == other.json.get('src')
+
+ ###########################################################################
+ # Traveral Methods
+
+ def _children(self) -> Iterator[AstNode]:
+ """Iterate all direct children."""
+ values = self.json.values()
+ for value in values:
+ if AstNode.is_solidity_node_like(value):
+ yield AstNode(value, self.source, self)
+ elif isinstance(value, list):
+ for child in value:
+ if AstNode.is_solidity_node_like(child):
+ yield AstNode(child, self.source, self)
+ return
+
+ @cache # noqa: B019
+ def children(self) -> list[AstNode]:
+ return list(self._children())
+
+ @cache # noqa: B019
+ def sourcemap(self) -> AstNodeSourceMapEntry:
+ """Return the source map associated with this node.
+
+ The first component is the start offset in unicode points.
+ The second compnent is the length in unicode points.
+ The third compnent is the identifier of the source unit.
+ """
+ parts = self.json['src'].split(':')
+ start, length, source_id = (int(part) for part in parts)
+ return (start, length, source_id)
+
+ def find_by_range(self, range_start: int, range_end: int) -> AstNode | None:
+ """Find the inner-most AstNode surrounding the given source range"""
+ start, l, source_id = self.sourcemap() # noqa: E741
+ end = start + l
+ if not (start <= range_start and range_end <= end):
+ return None
+ closest = self
+ queue = deque(self.children())
+ while len(queue) > 0:
+ current = queue.popleft()
+ start, l, source_id = current.sourcemap() # noqa: E741
+ end = start + l
+ if start <= range_start and range_end <= end:
+ queue = deque(current.children())
+ closest = current
+ return closest
+
+ def source_range(self) -> SourceRange:
+ start, l, _ = self.sourcemap()
+ range = self.source.offset_to_position(start) + self.source.offset_to_position(start + l - 1)
+ return range
+
+ def get(self, name: str, default: Any) -> Any:
+ if name in self.json:
+ return self.json[name]
+ else:
+ return default
+
+ ###########################################################################
+ # Type Checking
+
+ @staticmethod
+ def is_node_like(node: Any) -> bool:
+ return isinstance(node, dict) and 'nodeType' in node and isinstance(node['nodeType'], str)
+
+ @staticmethod
+ def is_solidity_node_like(node: Any) -> bool:
+ return AstNode.is_node_like(node) and not node['nodeType'].startswith('Yul')
+
+
+class Source:
+ """
+ Represents a source unit used during compilation.
+ """
+
+ _uuid: int
+
+ """
+ Virtual name of the source. This looks like a file path,
+ but it might be a generated pseudo name.
+ """
+ _name: str
+
+ """
+ The output standard Json, i.e. output.sources.$name
+ """
+ _json: Json
+
+ """
+ The original source text.
+ """
+ _source_text: str
+
+ """
+ A flag indicating that this source was generated by the compiler.
+ """
+ _generated: bool
+
+ """
+ A map of byte offsets to (line, column)-pairs.
+ """
+ _positions: dict[int, LineColumn]
+
+ """
+ A map of (line, column)-pairs to byte offsets.
+ """
+ _offsets: dict[LineColumn, int]
+
+ def __init__(self, uuid: int, name: str, json: Json, source_text: str, generated: bool = False):
+ self._uuid = uuid
+ self._name = name
+ self._json = json
+ self._source_text = source_text
+ self._generated = generated
+ self._positions = {}
+ self._offsets = {}
+ self._cache_source_map()
+
+ @property
+ def uuid(self) -> int:
+ """
+ A universal unique identifier for the source unit.
+ Use id to get a local relative to the compilation unit.
+ """
+ return self._uuid
+
+ @property
+ def id(self) -> int:
+ """
+ The local id of the source unit relative to the compilation unit.
+ Use uuid to get a univeral id.
+ """
+ result = self._json.get('id')
+ if isinstance(result, int):
+ return result
+ raise TypeError('Source.json.id is not an int.')
+
+ @property
+ def ast(self) -> AstNode:
+ dct = self._json.get('ast')
+ if isinstance(dct, dict):
+ return AstNode(dct, self)
+ raise TypeError('Source.json.ast is not a dict.')
+
+ def offset_to_position(self, offset: int) -> LineColumn:
+ """Return the (line, column)-pair for a given byte-offset.
+
+ lines and columns start at 1.
+ """
+ return self._positions[offset]
+
+ def position_to_offset(self, position: LineColumn) -> int:
+ """Return the byte-offset of a given (line, column)-pair
+
+ lines and columns start at 1.
+ """
+ return self._offsets[position]
+
+ @property
+ def source_text(self) -> str:
+ return self._source_text
+
+ def _cache_source_map(self) -> None:
+ line, column = (1, 1)
+ for offset in range(len(self.source_text)):
+ self._positions[offset] = (line, column)
+ self._offsets[(line, column)] = offset
+ char = self.source_text[offset]
+ if char == '\n':
+ line, column = (line + 1, 1)
+ else:
+ column = column + len(char.encode('utf-8'))
+
+ @property
+ def offsets(self) -> dict[LineColumn, int]:
+ """Map from (line, column)-pairs to byte offsets."""
+ return self._offsets
+
+ @property
+ def name(self) -> str:
+ return self._name
+
+ def is_generated(self) -> bool:
+ return self._generated
+
+
+class ContractSource:
+ _uuid: int
+ _file_path: str
+ _contract_name: str
+ _json: Any
+ _compilation_unit: CompilationUnit
+
+ _source_map: ContractSourceMap
+ _init_source_map: ContractSourceMap
+ _storage_layout: list[dict[str, Any]]
+
+ def __init__(
+ self, id: int, file_path: str, contract_name: str, json: Any, compilation_unit: CompilationUnit
+ ) -> None:
+ self._uuid = id
+ self._file_path = file_path
+ self._contract_name = contract_name
+ self._json = json
+ self._compilation_unit = compilation_unit
+ self._source_map = {}
+ self._init_source_map = {}
+ self._cache_source_map()
+ self._cache_init_source_map()
+ self._storage_layout = []
+
+ @property
+ def uuid(self) -> int:
+ """
+ A unique identifier for the contract.
+ """
+ return self._uuid
+
+ @cached_property
+ def generated_sources(self) -> dict[int, Source]:
+ """
+ Return a map of all associated generated sources.
+
+ The key is the local source id (not the uuid) of the source.
+ """
+ sources: dict[int, Source] = {}
+ generated_sources = self._json.get('evm', {}).get('bytecode', {}).get('generatedSources', [])
+ generated_sources += self._json.get('evm', {}).get('deployedBytecode', {}).get('generatedSources', [])
+ for generated_source in generated_sources:
+ source_id = generated_source['id']
+ source_uuid = to_uuid(f'{self.uuid}:{source_id}')
+ name = generated_source.get('name')
+ contents = generated_source.get('contents', '')
+ source = Source(source_uuid, name, generated_source, contents, True)
+ sources[source.id] = source
+ return sources
+
+ @cached_property
+ def instructions(self) -> list[Instruction]:
+ def map(offset: int, instruction: pyevmasm.Instruction) -> Instruction:
+ source_map_entry = self._source_map.get(offset, (-1, -1, -1, '-', 0))
+ return Instruction(instruction, self._compilation_unit, self, source_map_entry, offset)
+
+ return [
+ map(offset, instruction)
+ for offset, instruction in enumerate(pyevmasm.disassemble_all(self.get_deployed_bytecode))
+ ]
+
+ @cached_property
+ def init_instructions(self) -> list[Instruction]:
+ def map(offset: int, instruction: pyevmasm.Instruction) -> Instruction:
+ source_map_entry = self._init_source_map.get(offset, (-1, -1, -1, '-', 0))
+ return Instruction(instruction, self._compilation_unit, self, source_map_entry, offset)
+
+ return [
+ map(offset, instruction)
+ for offset, instruction in enumerate(pyevmasm.disassemble_all(self.get_init_bytecode))
+ ]
+
+ @cached_property
+ def pc_to_instruction_offsets(self) -> dict[int, int]:
+ result = {}
+ for i, instr in enumerate(self.instructions):
+ pc_start = instr.pc
+ pc_end = instr.pc + instr.operand_size + 1
+ for pc in range(pc_start, pc_end):
+ result[pc] = i
+ return result
+
+ @cached_property
+ def init_pc_to_instruction_offsets(self) -> dict[int, int]:
+ result = {}
+ for i, instr in enumerate(self.init_instructions):
+ pc_start = instr.pc
+ pc_end = instr.pc + instr.operand_size + 1
+ for pc in range(pc_start, pc_end):
+ result[pc] = i
+ return result
+
+ def instruction_by_pc(self, pc: int) -> Instruction:
+ offset = self.pc_to_instruction_offsets[pc]
+ return self.instructions[offset]
+
+ def init_instruction_by_pc(self, pc: int) -> Instruction:
+ offset = self.init_pc_to_instruction_offsets[pc]
+ return self.init_instructions[offset]
+
+ @cached_property
+ def get_deployed_bytecode(self) -> bytes:
+ ref = self._json.get('evm') if 'evm' in self._json else self._json
+ raw = ref.get('deployedBytecode').get('object').removeprefix('0x')
+ return bytes.fromhex(raw)
+
+ @cached_property
+ def get_init_bytecode(self) -> bytes:
+ ref = self._json.get('evm') if 'evm' in self._json else self._json
+ raw = ref.get('bytecode').get('object').removeprefix('0x')
+ return bytes.fromhex(raw)
+
+ def _cache_source_map(self) -> None:
+ ref = self._json.get('evm') if 'evm' in self._json else self._json
+ raw = ref.get('deployedBytecode', {}).get('sourceMap', '')
+ instrs_srcmap = raw.split(';')
+ s, l, f, j, m = (0, 0, 0, '', 0) # noqa: E741
+ for i, instr_srcmap in enumerate(instrs_srcmap):
+ fields = instr_srcmap.split(':')
+ s = int(fields[0]) if len(fields) > 0 and fields[0] else s
+ l = int(fields[1]) if len(fields) > 1 and fields[1] else l # noqa: E741
+ f = int(fields[2]) if len(fields) > 2 and fields[2] else f
+ j = fields[3] if len(fields) > 3 and fields[3] else j
+ m = int(fields[4]) if len(fields) > 4 and fields[4] else m
+ self._source_map[i] = (s, l, f, j, m)
+
+ def _cache_init_source_map(self) -> None:
+ ref = self._json.get('evm') if 'evm' in self._json else self._json
+ raw = ref.get('bytecode', {}).get('sourceMap', '')
+ instrs_srcmap = raw.split(';')
+ s, l, f, j, m = (0, 0, 0, '', 0) # noqa: E741
+ for i, instr_srcmap in enumerate(instrs_srcmap):
+ fields = instr_srcmap.split(':')
+ s = int(fields[0]) if len(fields) > 0 and fields[0] else s
+ l = int(fields[1]) if len(fields) > 1 and fields[1] else l # noqa: E741
+ f = int(fields[2]) if len(fields) > 2 and fields[2] else f
+ j = fields[3] if len(fields) > 3 and fields[3] else j
+ m = int(fields[4]) if len(fields) > 4 and fields[4] else m
+ self._init_source_map[i] = (s, l, f, j, m)
+
+
+class CompilationUnit:
+ """Easy access to Solidity standard json"""
+
+ _id: int
+ _sources: dict[int, Source] # Source UUID => Source
+ _contracts: dict[bytes, ContractSource]
+
+ def __init__(self, id: int, sources: dict[int, Source], contracts: dict[bytes, ContractSource]):
+ self._id = id
+ self._sources = sources
+ self._contracts = contracts
+
+ @property
+ def uuid(self) -> int:
+ """
+ A unique identifier for the compilation unit.
+ """
+ return self._id
+
+ @staticmethod
+ def load_build_info(foundry_root: Path) -> CompilationUnit:
+ build_info_files = (foundry_root / 'out' / 'build-info').glob('*.json')
+ build_info = json.loads(max(build_info_files, key=os.path.getmtime).read_text())
+ sources: dict[int, Source] = {} # Source id => Source
+ contracts: dict[bytes, ContractSource] = {} # CBOR metadata => contract
+ compilation_unit_uuid = to_uuid(build_info['id'])
+ compilation_unit = CompilationUnit(compilation_unit_uuid, sources, contracts)
+ try:
+ for source_name, source_json in build_info.get('output', {}).get('sources', {}).items():
+ absolute_path = source_json.get('ast').get('absolutePath')
+ source_uuid = to_uuid(f'{compilation_unit_uuid}:{source_name}')
+ source_text = build_info.get('input', {}).get('sources', {}).get(source_name, {}).get('content', '')
+ source = Source(source_uuid, source_name, source_json, source_text)
+ sources[source_uuid] = source
+ contracts_json = build_info.get('output', {}).get('contracts', {}).get(source_name, {})
+ for contract_name, contract_json in contracts_json.items():
+ contract_uuid = to_uuid(f'{source_uuid}:{contract_name}')
+ contract = ContractSource(
+ contract_uuid, absolute_path, contract_name, contract_json, compilation_unit
+ )
+ contract_bytecode = contract.get_deployed_bytecode
+ cbor_data = CompilationUnit.get_cbor_data(contract_bytecode)
+ contracts[cbor_data] = contract
+
+ # Add all generated sources
+ for generated_source in contract.generated_sources.values():
+ sources[generated_source.uuid] = generated_source
+
+ except (KeyError, IndexError):
+ _LOGGER.error(
+ '.output.contracts.$contract_name.evm.deployedBytecode.generatedSources not found in build-info file.'
+ )
+ except FileNotFoundError:
+ _LOGGER.error('No build-info file found in build-info directory.')
+
+ return compilation_unit
+
+ def get_instruction(self, contract_bytecode: bytes, pc: int) -> Instruction:
+ # First try to match init bytecode 1-to-1
+ try:
+ contract_source = self.get_contract_by_initcode(contract_bytecode)
+ return contract_source.init_instruction_by_pc(pc)
+ except Exception:
+ pass
+
+ # We cannot identify the contract by the full deployed bytecode.
+
+ # The deployed bytecode on-chain can be different from the
+ # deployed bytecode given in the standard json.
+ # This can for example be the case, when a library is linked at deployment time
+ # or when an immutable varirable is initialized at deployment time.
+ # Hence, to identify the contract, we only look at the CBOR-encoded metadata
+ # at the end of the bytecode. This metadata should not change between deployments.
+
+ # We don't actually need to decode it, we just need to know the length of the metadata.
+ cbor_data = CompilationUnit.get_cbor_data(contract_bytecode)
+ contract = self._contracts.get(cbor_data, None)
+ if contract is not None:
+ return contract.instruction_by_pc(pc)
+
+ # The former method can fail to detect the contract, if the CBOR_DATA
+ # is not at the end of the bytecode. In this case we use this slower
+ # method to find the contract. Notice, that it is possible to trick
+ # the method into return the wrong contract by copying the CBOR_DATA
+ # of another contract into the malicuous contract's bytecode.
+ for cbor_data, contract in self._contracts.items():
+ if cbor_data in contract_bytecode:
+ return contract.instruction_by_pc(pc)
+ raise Exception('Contract not found.')
+
+ def get_contract_by_initcode(self, bytecode: bytes) -> ContractSource:
+ for contract in self._contracts.values():
+ if contract.get_init_bytecode == bytecode:
+ return contract
+ raise Exception('Contract initialization code not found.')
+
+ @staticmethod
+ def get_cbor_data(contract_bytecode: bytes) -> bytes:
+ # Notice, that the CBOR_DATA is not necessarily at the end of the bytecode.
+ # Hence this method can return incorrect data.
+ cbor_length = contract_bytecode[-2:] # last two bytes
+ cbor_length = int.from_bytes(cbor_length, byteorder='big') # type: ignore
+ cbor_data = contract_bytecode[-cbor_length - 2 : -2] # type: ignore
+ return cbor_data
+
+ def get_source_by_id(self, source_id: int) -> Source:
+ for source in self._sources.values():
+ if source.id == source_id:
+ return source
+ raise KeyError('Source not found.')
+
+
+def to_uuid(s: str) -> int:
+ # Compute the SHA-256 hash of the input string
+ sha256_hash = hashlib.sha256(s.encode('utf-8')).hexdigest()
+ # Convert the hexadecimal hash to an integer
+ hash_int = int(sha256_hash, 16) % (2**31)
+ return hash_int
diff --git a/src/kontrol/utils.py b/src/kontrol/utils.py
index 138d2b5d5..fd92fe31f 100644
--- a/src/kontrol/utils.py
+++ b/src/kontrol/utils.py
@@ -248,6 +248,12 @@ def foundry_toml_extra_contents() -> str:
"""
+def foundry_toml_cancun_schedule() -> str:
+ return """
+evm_version = "cancun"
+"""
+
+
def _rv_yellow() -> str:
return '#ffcc07'
diff --git a/src/tests/integration/test-data/cse-lemmas.k b/src/tests/integration/test-data/cse-lemmas.k
index f64b3e75a..aefb4e126 100644
--- a/src/tests/integration/test-data/cse-lemmas.k
+++ b/src/tests/integration/test-data/cse-lemmas.k
@@ -14,11 +14,6 @@ module CSE-LEMMAS
requires #rangeUInt ( 256 , X )
[simplification]
- // for-loop chop
- rule chop ( ( X:Int +Int Y:Int ) ) ==Int 0 => X ==Int pow256 -Int (Y modInt pow256)
- requires #rangeUInt(256, X) andBool 0 <=Int Y
- [simplification, concrete(Y)]
-
// Set equality needed for discharging `#Not ( #Exists ( ... )` on `` unification
rule { S1:Set #Equals S2:Set |Set SetItem ( X ) } =>
{ X in S1 } #And
@@ -55,12 +50,9 @@ module CSE-LEMMAS
andBool X +Int 1 <=Int A
[concrete(X), simplification, preserves-definedness]
- rule { #asWord ( X ) #Equals #asWord ( Y ) } => { X #Equals Y }
- requires lengthBytes(X) ==Int lengthBytes(Y) andBool lengthBytes(X) <=Int 32
- [simplification]
-
- rule #asWord ( B ) <=Int X => true requires X >=Int ( 2 ^Int (8 *Int minInt(32, lengthBytes(B))) -Int 1 ) [simplification]
- rule #asWord ( B ) true requires X >=Int 2 ^Int (8 *Int minInt(32, lengthBytes(B))) [simplification]
+ rule [powByteLen-compute]:
+ #powByteLen(SIZE) => 2 ^Int (8 *Int SIZE)
+ [simplification, concrete(SIZE)]
endmodule
diff --git a/src/tests/integration/test-data/end-to-end-prove-all b/src/tests/integration/test-data/end-to-end-prove-all
index 642fd998f..4e4c53ec1 100644
--- a/src/tests/integration/test-data/end-to-end-prove-all
+++ b/src/tests/integration/test-data/end-to-end-prove-all
@@ -1,4 +1,5 @@
CounterTest.test_Increment()
+TransientStorageTest.testTransientStoreLoad(uint256,uint256)
UnitTest.test_assertEq_address_err()
UnitTest.test_assertEq_bool_err()
UnitTest.test_assertEq_bytes32_err()
diff --git a/src/tests/integration/test-data/pausability-lemmas.k b/src/tests/integration/test-data/pausability-lemmas.k
index becea1aa0..c6497bfbe 100644
--- a/src/tests/integration/test-data/pausability-lemmas.k
+++ b/src/tests/integration/test-data/pausability-lemmas.k
@@ -50,7 +50,7 @@ module PAUSABILITY-LEMMAS [symbolic]
// Cancellativity #6
rule (A -Int B) -Int (C -Int B) => A -Int C [simplification]
-
+
// Upper bound on (pow256 - 32) &Int lengthBytes(X)
rule notMaxUInt5 &Int Y <=Int Y => true
requires 0 <=Int Y
@@ -67,26 +67,9 @@ module PAUSABILITY-LEMMAS [symbolic]
rule notMaxUInt5 &Int X +Int 31 true requires 0 <=Int X [simplification]
//
- // #asWord
+ // #asInteger
//
- // Move to function parameters
- rule { #asWord ( X ) #Equals #asWord ( Y ) } => #Top
- requires X ==K Y
- [simplification]
-
- // #asWord ignores leading zeros
- rule #asWord ( BA1 +Bytes BA2 ) => #asWord ( BA2 )
- requires #asInteger(BA1) ==Int 0
- [simplification, concrete(BA1)]
-
-
- // Equality and #range
- rule #asWord ( #range ( #buf ( 32 , _X:Int ) , S:Int , W:Int ) ) ==Int Y:Int => false
- requires S +Int W <=Int 32
- andBool (2 ^Int (8 *Int W)) <=Int Y
- [concrete(S, W, Y), simplification]
-
// Conversion from bytes always yields a non-negative integer
rule 0 <=Int #asInteger ( _ ) => true [simplification]
diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
index df89c5b56..a80ce47c6 100644
--- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
+++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AccountParamsTest.testDealConcrete()
│
│ (898 steps)
@@ -15,7 +16,7 @@
│ method: test%AccountParamsTest.testDealConcrete()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
index 08d0b3e0b..70204a886 100644
--- a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%AddConst.applyOp(uint256)
┃
┃ (branch)
-┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
┃ │
┃ ├─ 8
┃ │ k: #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%cse%AddConst.applyOp(uint256)
┃ │
┃ │ (446 steps)
@@ -22,23 +26,30 @@
┃ │ pc: 87
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%cse%AddConst.applyOp(uint256)
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool
+ C_ADDCONST_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) CONTINUATION:K
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%AddConst.applyOp(uint256)
│
│ (371 steps)
@@ -47,10 +58,14 @@
│ pc: 179
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_REVERT
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%AddConst.applyOp(uint256)
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool
+ C_ADDCONST_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected
index 2f30bcca1..64ac0971a 100644
--- a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected
+++ b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AddrTest.test_addr_true()
│
│ (1258 steps)
@@ -12,10 +13,11 @@
│ pc: 333
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AddrTest.test_addr_true()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
index b18f0d9e3..761ba63a7 100644
--- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ArithmeticCallTest.setUp()
│
│ (1024 steps)
@@ -12,16 +13,20 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add(uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: 1
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%ArithmeticContract.add(uint256,uint256)
┃ │
┃ │ (73 steps)
@@ -32,7 +37,8 @@
┃ statusCode: EVMC_REVERT
┃ method: test%ArithmeticCallTest.test_double_add(uint256,uint256)
┃
-┣━━┓ constraints:
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
┃ ┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ ┃ ( maxUInt256 -Int VV1_y_114b9705:Int ) CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraints:
+┗━━┓ subst: .Subst
+ ┃ constraint:
┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) +Int VV1_y_114b9705:Int ) <=Int VV0_x_114b9705:Int
@@ -89,6 +100,7 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add(uint256,uint256)
│
│ (745 steps)
diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected
index b0912bf92..1b2cecdf3 100644
--- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ArithmeticCallTest.setUp()
│
│ (1045 steps)
@@ -12,16 +13,20 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add(uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: 1
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%ArithmeticContract.add(uint256,uint256)
┃ │
┃ │ (73 steps)
@@ -32,7 +37,8 @@
┃ statusCode: EVMC_REVERT
┃ method: test%ArithmeticCallTest.test_double_add_double_sub(uint256,uint256)
┃
-┣━━┓ constraints:
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
┃ ┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ ┃ ( maxUInt256 -Int VV1_y_114b9705:Int ) CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraints:
+┗━━┓ subst: .Subst
+ ┃ constraint:
┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int
@@ -134,6 +149,7 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add(uint256,uint256)
│
│ (1579 steps)
diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected
index 2aef1fa31..9e9b902fa 100644
--- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ArithmeticCallTest.setUp()
│
│ (1077 steps)
@@ -12,10 +13,12 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraints:
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
┃ ┃ ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: 1
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256)
┃ │
┃ │ (73 steps)
@@ -49,9 +57,11 @@
┃ pc: 1584
┃ callDepth: 0
┃ statusCode: EVMC_REVERT
+┃ src: lib/forge-std/lib/ds-test/src/test.sol:48:48
┃ method: test%ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256)
┃
-┣━━┓ constraints:
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
┃ ┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ ┃ VV2_z_114b9705:Int <=Int ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int )
┃ ┃ ( ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) -Int VV2_z_114b9705:Int ) +Int VV1_y_114b9705:Int ) CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraints:
+┗━━┓ subst: .Subst
+ ┃ constraint:
┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ VV2_z_114b9705:Int <=Int ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int )
┃ ( ( VV0_x_114b9705:Int +Int VV1_y_114b9705:Int ) -Int VV2_z_114b9705:Int ) <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
@@ -134,6 +153,7 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256)
│
│ (762 steps)
diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected
index 6cd5b621d..c7ce9bf0a 100644
--- a/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ArithmeticContract.add(uint256,uint256).cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add(uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int VV1_y_114b9705:Int )
┃ │
┃ ├─ 8
┃ │ k: #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%ArithmeticContract.add(uint256,uint256)
┃ │
┃ │ (470 steps)
@@ -22,23 +26,30 @@
┃ │ pc: 128
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%ArithmeticContract.add(uint256,uint256)
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool
+ C_ARITHMETICCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: ( maxUInt256 -Int VV1_y_114b9705:Int ) CONTINUATION:K
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add(uint256,uint256)
│
│ (407 steps)
@@ -47,10 +58,14 @@
│ pc: 550
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_REVERT
+ │ src: lib/forge-std/src/StdInvariant.sol:90:90
│ method: src%ArithmeticContract.add(uint256,uint256)
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool
+ C_ARITHMETICCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected
index c8ae7e2a1..dbd6ca087 100644
--- a/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ArithmeticContract.add_sub_external(uint256,uint256,uint256).cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: 1024 <=Int CALLDEPTH_CELL:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ 1024 <=Int CALLDEPTH_CELL:Int
┃ │
┃ ├─ 17
┃ │ k: #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256)
┃ │
┃ │ (539 steps)
@@ -22,17 +26,22 @@
┃ │ pc: 295
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_REVERT
+┃ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:63
┃ │ method: src%ArithmeticContract.add_sub_external(uint256,uint256,uint256)
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool
+ C_ARITHMETICCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┣━━┓ constraints:
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
┃ ┃ CALLDEPTH_CELL:Int
+ C_ARITHMETICCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┣━━┓ constraints:
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
┃ ┃ CALLDEPTH_CELL:Int
+ C_ARITHMETICCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraints:
+┗━━┓ subst: .Subst
+ ┃ constraint:
┃ CALLDEPTH_CELL:Int
+ C_ARITHMETICCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected
index 283cbe78a..1a2da4b40 100644
--- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected
+++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (182 steps)
@@ -12,6 +13,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.checkFail_assert_false()
│
│ (307 steps)
@@ -47,7 +50,7 @@
│ method: test%AssertTest.checkFail_assert_false()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 7 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
index ae0dc65c3..3c28d7a55 100644
--- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
+++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (182 steps)
@@ -12,6 +13,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.testFail_assert_true()
│
│ (200 steps)
@@ -28,6 +31,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.testFail_assert_true()
│
│ (1 step)
@@ -36,6 +40,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.testFail_assert_true()
│
│ (2 steps)
@@ -44,6 +49,7 @@
pc: 328
callDepth: 0
statusCode: EVMC_SUCCESS
+ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
method: test%AssertTest.testFail_assert_true()
diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
index d0f1c4c14..8e19ecb0f 100644
--- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
+++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (182 steps)
@@ -12,6 +13,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.testFail_expect_revert()
│
│ (417 steps)
@@ -28,6 +31,7 @@
│ pc: 811
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:78:78
│ method: test%AssertTest.testFail_expect_revert()
│
│ (1 step)
@@ -36,6 +40,7 @@
│ pc: 811
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:78:78
│ method: test%AssertTest.testFail_expect_revert()
│
│ (230 steps)
@@ -44,6 +49,7 @@
│ pc: 892
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:78:78
│ method: test%AssertTest.testFail_expect_revert()
│
│ (1 step)
@@ -52,6 +58,7 @@
│ pc: 892
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:78:78
│ method: test%AssertTest.testFail_expect_revert()
│
│ (18 steps)
@@ -60,6 +67,7 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.call_assert_false()
│
│ (1 step)
@@ -68,6 +76,7 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.call_assert_false()
│
│ (319 steps)
@@ -108,6 +117,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.testFail_expect_revert()
│
│ (1 step)
@@ -116,6 +126,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.testFail_expect_revert()
│
│ (2 steps)
@@ -124,6 +135,7 @@
pc: 328
callDepth: 0
statusCode: EVMC_SUCCESS
+ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
method: test%AssertTest.testFail_expect_revert()
diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected
index cca11727d..d13b54270 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (182 steps)
@@ -12,6 +13,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.test_assert_false()
│
│ (307 steps)
diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected
index d96bf404a..25dcb5145 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (182 steps)
@@ -12,6 +13,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.test_assert_true()
│
│ (263 steps)
@@ -28,6 +31,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.test_assert_true()
│
│ (1 step)
@@ -36,6 +40,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.test_assert_true()
│
│ (2 steps)
@@ -44,10 +49,11 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.test_assert_true()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 7 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected
index 3a39c4dc2..f70ced65f 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (182 steps)
@@ -12,6 +13,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.test_failing_branch(uint256)
│
│ (360 steps)
@@ -28,16 +31,20 @@
│ pc: 1116
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:74:74
│ method: test%AssertTest.test_failing_branch(uint256)
┃
┃ (branch)
-┣━━┓ constraint: 100 <=Int VV0_x_114b9705:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ 100 <=Int VV0_x_114b9705:Int
┃ │
┃ ├─ 9
┃ │ k: JUMPI 1124 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execu ...
┃ │ pc: 1116
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74
┃ │ method: test%AssertTest.test_failing_branch(uint256)
┃ │
┃ │ (39 steps)
@@ -46,6 +53,7 @@
┃ │ pc: 328
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
┃ │ method: test%AssertTest.test_failing_branch(uint256)
┃ │
┃ │ (1 step)
@@ -54,6 +62,7 @@
┃ │ pc: 328
┃ │ callDepth: 0
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
┃ │ method: test%AssertTest.test_failing_branch(uint256)
┃ │
┃ │ (2 steps)
@@ -62,23 +71,27 @@
┃ │ pc: 328
┃ │ callDepth: 0
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
┃ │ method: test%AssertTest.test_failing_branch(uint256)
┃ │
┃ ┊ constraint: true
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ subst: ...
┃ └─ 7 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: VV0_x_114b9705:Int #pc [ JUMPI ] ~> #execu ...
│ pc: 1116
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:74:74
│ method: test%AssertTest.test_failing_branch(uint256)
│
│ (63 steps)
diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected
index f065f2ab5..35eb78ae1 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (182 steps)
@@ -12,6 +13,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.test_revert_branch(uint256,uint256)
│
│ (366 steps)
@@ -28,16 +31,20 @@
│ pc: 1590
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/lib/ds-test/src/test.sol:48:62
│ method: test%AssertTest.test_revert_branch(uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int
┃ │
┃ ├─ 9
┃ │ k: JUMPI 1594 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ...
┃ │ pc: 1590
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62
┃ │ method: test%AssertTest.test_revert_branch(uint256,uint256)
┃ │
┃ │ (72 steps)
@@ -64,13 +71,16 @@
┃ statusCode: EVMC_REVERT
┃ method: test%AssertTest.test_revert_branch(uint256,uint256)
┃
-┗━━┓ constraint: VV0_x_114b9705:Int #pc [ JU ...
│ pc: 1590
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62
│ method: test%AssertTest.test_revert_branch(uint256,uint256)
│
│ (37 steps)
@@ -79,6 +89,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.test_revert_branch(uint256,uint256)
│
│ (1 step)
@@ -87,6 +98,7 @@
│ pc: 328
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
│ method: test%AssertTest.test_revert_branch(uint256,uint256)
│
│ (2 steps)
@@ -95,6 +107,7 @@
pc: 328
callDepth: 0
statusCode: EVMC_SUCCESS
+ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
method: test%AssertTest.test_revert_branch(uint256,uint256)
diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
index 571b474ec..e0cb6f154 100644
--- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssumeTest.testFail_assume_false(uint256,uint256)
│
│ (561 steps)
@@ -28,6 +29,7 @@
│ pc: 281
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%AssumeTest.testFail_assume_false(uint256,uint256)
│
│ (1 step)
@@ -36,6 +38,7 @@
│ pc: 281
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%AssumeTest.testFail_assume_false(uint256,uint256)
│
│ (2 steps)
@@ -44,6 +47,7 @@
pc: 281
callDepth: 0
statusCode: EVMC_SUCCESS
+ src: lib/forge-std/src/StdInvariant.sol:61:63
method: test%AssumeTest.testFail_assume_false(uint256,uint256)
diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
index 39dd2fc1c..efc4bc42a 100644
--- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssumeTest.testFail_assume_true(uint256,uint256)
│
│ (547 steps)
@@ -52,6 +53,7 @@
│ pc: 281
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%AssumeTest.testFail_assume_true(uint256,uint256)
│
│ (1 step)
@@ -60,6 +62,7 @@
│ pc: 281
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%AssumeTest.testFail_assume_true(uint256,uint256)
│
│ (2 steps)
@@ -68,10 +71,11 @@
│ pc: 281
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%AssumeTest.testFail_assume_true(uint256,uint256)
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
index 12bc06a1c..e1bed70c0 100644
--- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssumeTest.test_assume_false(uint256,uint256)
│
│ (571 steps)
@@ -52,6 +53,7 @@
│ pc: 281
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%AssumeTest.test_assume_false(uint256,uint256)
│
│ (1 step)
@@ -60,6 +62,7 @@
│ pc: 281
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%AssumeTest.test_assume_false(uint256,uint256)
│
│ (2 steps)
@@ -68,6 +71,7 @@
pc: 281
callDepth: 0
statusCode: EVMC_SUCCESS
+ src: lib/forge-std/src/StdInvariant.sol:61:63
method: test%AssumeTest.test_assume_false(uint256,uint256)
diff --git a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected
index b5a8c8e92..12634558e 100644
--- a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected
+++ b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%BlockParamsTest.testWarp(uint256)
│
│ (965 steps)
@@ -12,10 +13,11 @@
│ pc: 281
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:61:63
│ method: test%BlockParamsTest.testWarp(uint256)
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
index f4306dfc4..3e235f4c4 100644
--- a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%CSETest.setUp()
│
│ (1550 steps)
@@ -12,16 +13,20 @@
│ pc: 669
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:82:82
│ method: test%CSETest.test_add_const(uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: pow64 <=Int VV0_x_114b9705:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ pow64 <=Int VV0_x_114b9705:Int
┃ │
┃ ├─ 10
┃ │ k: JUMPI 678 bool2Word ( pow64 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #exec ...
┃ │ pc: 669
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/forge-std/src/StdInvariant.sol:82:82
┃ │ method: test%CSETest.test_add_const(uint256,uint256)
┃ │
┃ │ (193 steps)
@@ -30,15 +35,19 @@
┃ pc: 737
┃ callDepth: 0
┃ statusCode: STATUSCODE:StatusCode
+┃ src: lib/forge-std/src/StdInvariant.sol:78:78
┃ method: test%CSETest.test_add_const(uint256,uint256)
┃
-┗━━┓ constraint: VV0_x_114b9705:Int #pc [ JUMPI ] ~> #exec ...
│ pc: 669
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:82:82
│ method: test%CSETest.test_add_const(uint256,uint256)
│
│ (1123 steps)
@@ -47,10 +56,11 @@
│ pc: 221
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/src/StdInvariant.sol:89:91
│ method: test%CSETest.test_add_const(uint256,uint256)
│
┊ constraint: true
- ┊ subst: OMITTED SUBST
+ ┊ subst: ...
└─ 8 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
index a8b070eb2..1dce23e3f 100644
--- a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%CSETest.setUp()
│
│ (1556 steps)
@@ -15,7 +16,9 @@
│ method: test%CSETest.test_identity(uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: pow64 <=Int VV0_x_114b9705:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ pow64 <=Int VV0_x_114b9705:Int
┃ │
┃ ├─ 10
┃ │ k: JUMPI 2519 bool2Word ( pow64 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #exe ...
@@ -32,7 +35,9 @@
┃ statusCode: STATUSCODE:StatusCode
┃ method: test%CSETest.test_identity(uint256,uint256)
┃
-┗━━┓ constraint: VV0_x_114b9705:Int #pc [ JUMPI ] ~> #exe ...
@@ -47,10 +52,11 @@
│ pc: 221
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/src/StdInvariant.sol:89:91
│ method: test%CSETest.test_identity(uint256,uint256)
│
┊ constraint: true
- ┊ subst: OMITTED SUBST
+ ┊ subst: ...
└─ 8 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected
index 8d586a872..8cecd0b0e 100644
--- a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected
+++ b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%CallableStorageContract.str()
┃
┃ (branch)
-┣━━┓ constraint: C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ==Int 0
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ==Int 0
┃ │
┃ ├─ 8
┃ │ k: #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%CallableStorageContract.str()
┃ │
┃ │ (867 steps)
@@ -22,23 +26,31 @@
┃ │ pc: 86
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%CallableStorageContract.str()
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool 1 in_keys ( C_CALLABLESTORAGECONTRACT_STORAGE:Map ) )
+┃ ┊ ( notBool
+ C_CALLABLESTORAGECONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: ( notBool C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ==Int 0 )
+┗━━┓ subst: .Subst
+ ┃ constraint:
+ ┃ ( notBool C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ==Int 0 )
│
├─ 9
│ k: #execute ~> CONTINUATION:K
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%CallableStorageContract.str()
│
│ (1033 steps)
@@ -47,10 +59,15 @@
│ pc: 86
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%CallableStorageContract.str()
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool 1 in_keys ( C_CALLABLESTORAGECONTRACT_STORAGE:Map ) )
+ ┊ ( notBool
+ C_CALLABLESTORAGECONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected b/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected
index 81f84a667..bbdae0801 100644
--- a/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected
+++ b/src/tests/integration/test-data/show/CallableStorageTest.test_str().cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%CallableStorageTest.setUp()
│
│ (3775 steps)
@@ -12,10 +13,11 @@
│ pc: 240
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:77:79
│ method: test%CallableStorageTest.test_str()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 6 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected
index 3e8739ecc..f92e7b41c 100644
--- a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected
+++ b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│
│ (1161 steps)
├─ 5 (terminal)
@@ -11,9 +12,10 @@
│ pc: 253
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:73:75
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected
index 780074e0e..5aedc2472 100644
--- a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected
+++ b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ConstructorTest.test_contract_call()
│
│ (2233 steps)
@@ -12,10 +13,11 @@
│ pc: 278
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:85:87
│ method: test%ConstructorTest.test_contract_call()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
index 9c95ac21b..53f659d2f 100644
--- a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
+++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ContractFieldTest.setUp()
│
│ (2231 steps)
@@ -12,10 +13,11 @@
│ pc: 194
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:69:71
│ method: test%ContractFieldTest.testEscrowToken()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 7 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected
index 9336b8952..ffb7bd215 100644
--- a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected
+++ b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%Enum.enum_argument_range(uint8)
│
│ (514 steps)
@@ -12,10 +13,19 @@
│ pc: 68
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%Enum.enum_argument_range(uint8)
│
-┊ constraint: OMITTED CONSTRAINT
-┊ subst: OMITTED SUBST
+┊ constraint:
+┊ ( notBool 0 in_keys ( C_ENUM_STORAGE:Map ) )
+┊ ( notBool
+ C_ENUM_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┊ ( notBool
+ C_ENUM_MEMBER_CONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┊ ( notBool C_ENUM_ID:Int ==Int C_ENUM_MEMBER_CONTRACT_ID:Int )
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected
index 3ebeae948..c0f1689d8 100644
--- a/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected
+++ b/src/tests/integration/test-data/show/Enum.enum_storage_range().cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%Enum.enum_storage_range()
┃
┃ (branch)
-┣━━┓ constraint: CALLDEPTH_CELL:Int CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%Enum.enum_storage_range()
┃ │
┃ │ (1242 steps)
@@ -22,23 +26,35 @@
┃ │ pc: 68
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%Enum.enum_storage_range()
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool 0 in_keys ( C_ENUM_STORAGE:Map ) )
+┃ ┊ ( notBool
+ C_ENUM_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool
+ C_ENUM_MEMBER_CONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool C_ENUM_ID:Int ==Int C_ENUM_MEMBER_CONTRACT_ID:Int )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: 1024 <=Int CALLDEPTH_CELL:Int
+┗━━┓ subst: .Subst
+ ┃ constraint:
+ ┃ 1024 <=Int CALLDEPTH_CELL:Int
│
├─ 9
│ k: #execute ~> CONTINUATION:K
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%Enum.enum_storage_range()
│
│ (348 steps)
@@ -47,10 +63,19 @@
│ pc: 161
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_REVERT
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%Enum.enum_storage_range()
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool 0 in_keys ( C_ENUM_STORAGE:Map ) )
+ ┊ ( notBool
+ C_ENUM_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ ( notBool
+ C_ENUM_MEMBER_CONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ ( notBool C_ENUM_ID:Int ==Int C_ENUM_MEMBER_CONTRACT_ID:Int )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/Enum.init.cse.expected b/src/tests/integration/test-data/show/Enum.init.cse.expected
index 976ceb99a..ce74733ad 100644
--- a/src/tests/integration/test-data/show/Enum.init.cse.expected
+++ b/src/tests/integration/test-data/show/Enum.init.cse.expected
@@ -12,8 +12,11 @@
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
│
-┊ constraint: OMITTED CONSTRAINT
-┊ subst: OMITTED SUBST
+┊ constraint:
+┊ ( notBool
+ C_ENUM_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected
index 9d99d6fca..301980237 100644
--- a/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/Identity.applyOp(uint256).cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%Identity.applyOp(uint256)
┃
┃ (branch)
-┣━━┓ constraint: CALLDEPTH_CELL:Int CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%cse%Identity.applyOp(uint256)
┃ │
┃ │ (712 steps)
@@ -22,23 +26,30 @@
┃ │ pc: 87
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: src%cse%Identity.applyOp(uint256)
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool
+ C_IDENTITY_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: 1024 <=Int CALLDEPTH_CELL:Int
+┗━━┓ subst: .Subst
+ ┃ constraint:
+ ┃ 1024 <=Int CALLDEPTH_CELL:Int
│
├─ 9
│ k: #execute ~> CONTINUATION:K
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%Identity.applyOp(uint256)
│
│ (443 steps)
@@ -47,10 +58,14 @@
│ pc: 163
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_REVERT
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%Identity.applyOp(uint256)
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool
+ C_IDENTITY_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected b/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected
index 89719958f..ec55d661a 100644
--- a/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/Identity.identity(uint256).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%Identity.identity(uint256)
│
│ (331 steps)
@@ -12,10 +13,14 @@
│ pc: 87
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%cse%Identity.identity(uint256)
│
-┊ constraint: OMITTED CONSTRAINT
-┊ subst: OMITTED SUBST
+┊ constraint:
+┊ ( notBool
+ C_IDENTITY_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
index 21cd80b30..1f8228cac 100644
--- a/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.add(uint256).cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ImportedContract.add(uint256)
┃
┃ (branch)
-┣━━┓ constraint: #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 ) <=Int ( maxUInt256 -Int VV0_x_114b9705:Int )
┃ │
┃ ├─ 8
┃ │ k: #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%ImportedContract.add(uint256)
┃ │
┃ │ (379 steps)
@@ -22,23 +26,30 @@
┃ │ pc: 107
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%ImportedContract.add(uint256)
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool
+ C_IMPORTEDCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: ( maxUInt256 -Int VV0_x_114b9705:Int ) CONTINUATION:K
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ImportedContract.add(uint256)
│
│ (349 steps)
@@ -47,10 +58,14 @@
│ pc: 226
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_REVERT
+ │ src: lib/forge-std/src/StdInvariant.sol:81:83
│ method: test%ImportedContract.add(uint256)
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool
+ C_IMPORTEDCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
index 3a51e465a..9dba4c635 100644
--- a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ImportedContract.count()
│
│ (206 steps)
@@ -12,10 +13,14 @@
│ pc: 90
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ImportedContract.count()
│
-┊ constraint: OMITTED CONSTRAINT
-┊ subst: OMITTED SUBST
+┊ constraint:
+┊ ( notBool
+ C_IMPORTEDCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
index 8fc6bb944..9a281653b 100644
--- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│
│ (48 steps)
├─ 3 (terminal)
@@ -11,9 +12,13 @@
│ pc: 21
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
+│ src: test/nested/SimpleNested.t.sol:7:11
│
-┊ constraint: OMITTED CONSTRAINT
-┊ subst: OMITTED SUBST
+┊ constraint:
+┊ ( notBool
+ C_IMPORTEDCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
index 93c6d4963..ae3e29fad 100644
--- a/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ImportedContract.set(uint256).cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ImportedContract.set(uint256)
┃
┃ (branch)
-┣━━┓ constraint: 3 <=Int #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 )
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ 3 <=Int #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 )
┃ │
┃ ├─ 8
┃ │ k: #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%ImportedContract.set(uint256)
┃ │
┃ │ (373 steps)
@@ -22,23 +26,30 @@
┃ │ pc: 107
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%ImportedContract.set(uint256)
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool
+ C_IMPORTEDCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 ) CONTINUATION:K
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ImportedContract.set(uint256)
│
│ (362 steps)
@@ -47,10 +58,14 @@
│ pc: 107
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%ImportedContract.set(uint256)
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool
+ C_IMPORTEDCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected
index cc6707a3a..f9008a595 100644
--- a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected
+++ b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%InterfaceTagTest.setUp()
│
│ (1795 steps)
@@ -12,10 +13,11 @@
│ pc: 194
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:69:71
│ method: test%InterfaceTagTest.testInterface()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 7 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected
index 497d75085..9c4a614b5 100644
--- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected
+++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%SetUpDeployTest.setUp()
│
│ (876 steps)
@@ -12,6 +13,7 @@
│ pc: 194
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:69:71
│ method: test%SetUpDeployTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%SetUpDeployTest.test_extcodesize()
│
│ (348 steps)
@@ -28,6 +31,7 @@
│ pc: 194
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:69:71
│ method: test%SetUpDeployTest.test_extcodesize()
│
│ (1 step)
@@ -36,6 +40,7 @@
│ pc: 194
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:69:71
│ method: test%SetUpDeployTest.test_extcodesize()
│
│ (2 steps)
@@ -44,10 +49,11 @@
│ pc: 194
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/src/StdInvariant.sol:69:71
│ method: test%SetUpDeployTest.test_extcodesize()
│
┊ constraint: true
-┊ subst: OMITTED SUBST
+┊ subst: ...
└─ 10 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected b/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected
index 60b93ef74..fd52f3384 100644
--- a/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/StaticCallContract.set(uint256).cse.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%StaticCallContract.set(uint256)
│
│ (274 steps)
@@ -12,10 +13,14 @@
│ pc: 62
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: EVMC_SUCCESS
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%StaticCallContract.set(uint256)
│
-┊ constraint: OMITTED CONSTRAINT
-┊ subst: OMITTED SUBST
+┊ constraint:
+┊ ( notBool
+ C_STATICCALLCONTRACT_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected
index d3e02f65c..e853fcdd7 100644
--- a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected
+++ b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected
@@ -4,16 +4,20 @@
│ pc: 0
│ callDepth: CALLDEPTH_CELL:Int
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%TGovernance.getEscrowTokenTotalSupply()
┃
┃ (branch)
-┣━━┓ constraint: 1024 <=Int CALLDEPTH_CELL:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ 1024 <=Int CALLDEPTH_CELL:Int
┃ │
┃ ├─ 13
┃ │ k: #execute ~> CONTINUATION:K
┃ │ pc: 0
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%TGovernance.getEscrowTokenTotalSupply()
┃ │
┃ │ (376 steps)
@@ -22,17 +26,33 @@
┃ │ pc: 153
┃ │ callDepth: CALLDEPTH_CELL:Int
┃ │ statusCode: EVMC_REVERT
+┃ │ src: test/nested/SimpleNested.t.sol:7:11
┃ │ method: test%TGovernance.getEscrowTokenTotalSupply()
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( notBool 0 in_keys ( C_TGOVERNANCE_ESCROW_STORAGE:Map ) )
+┃ ┊ ( notBool 0 in_keys ( C_TGOVERNANCE_STORAGE:Map ) )
+┃ ┊ ( notBool
+ C_TGOVERNANCE_ESCROW_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool
+ C_TGOVERNANCE_ESCROW_TOKEN_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool
+ C_TGOVERNANCE_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool C_TGOVERNANCE_ESCROW_ID:Int ==Int C_TGOVERNANCE_ESCROW_TOKEN_ID:Int )
+┃ ┊ ( notBool C_TGOVERNANCE_ESCROW_ID:Int ==Int C_TGOVERNANCE_ID:Int )
+┃ ┊ ( notBool C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ==Int C_TGOVERNANCE_ID:Int )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┣━━┓ constraints:
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
┃ ┃ CALLDEPTH_CELL:Int
+ C_TGOVERNANCE_ESCROW_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool
+ C_TGOVERNANCE_ESCROW_TOKEN_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool
+ C_TGOVERNANCE_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+┃ ┊ ( notBool C_TGOVERNANCE_ESCROW_ID:Int ==Int C_TGOVERNANCE_ESCROW_TOKEN_ID:Int )
+┃ ┊ ( notBool C_TGOVERNANCE_ESCROW_ID:Int ==Int C_TGOVERNANCE_ID:Int )
+┃ ┊ ( notBool C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ==Int C_TGOVERNANCE_ID:Int )
+┃ ┊ subst: ...
┃ └─ 2 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraints:
+┗━━┓ subst: .Subst
+ ┃ constraint:
┃ CALLDEPTH_CELL:Int
+ C_TGOVERNANCE_ESCROW_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ ( notBool
+ C_TGOVERNANCE_ESCROW_TOKEN_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ ( notBool
+ C_TGOVERNANCE_ID:Int
+ in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ ┊ ( notBool C_TGOVERNANCE_ESCROW_ID:Int ==Int C_TGOVERNANCE_ESCROW_TOKEN_ID:Int )
+ ┊ ( notBool C_TGOVERNANCE_ESCROW_ID:Int ==Int C_TGOVERNANCE_ID:Int )
+ ┊ ( notBool C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ==Int C_TGOVERNANCE_ID:Int )
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/gas-abstraction.expected b/src/tests/integration/test-data/show/gas-abstraction.expected
index 9a918854c..1ae5640b1 100644
--- a/src/tests/integration/test-data/show/gas-abstraction.expected
+++ b/src/tests/integration/test-data/show/gas-abstraction.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%GasTest.testInfiniteGas()
│
│ (683 steps)
@@ -15,59 +16,8 @@
│ method: test%GasTest.testInfiniteGas()
│
┊ constraint: true
-┊ subst: {
- CONTINUATION <- CONTINUATION:K
- EXITCODE_CELL <- EXITCODE_CELL:Int
- STATUSCODE <- STATUSCODE:StatusCode
- CALLER_ID <- CALLER_ID:Int
- VGAS <- VGAS:Int
- VGAS_4b7cee1f <- ( VGAS:Int +Int -373 )
- CALLGAS_CELL <- CALLGAS_CELL:Gas
- SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set
- REFUND_CELL <- REFUND_CELL:Int
- GASPRICE_CELL <- GASPRICE_CELL:Int
- ORIGIN_ID <- ORIGIN_ID:Int
- BLOCKHASHES_CELL <- BLOCKHASHES_CELL:List
- PREVIOUSHASH_CELL <- PREVIOUSHASH_CELL:Int
- OMMERSHASH_CELL <- OMMERSHASH_CELL:Int
- COINBASE_CELL <- COINBASE_CELL:Int
- STATEROOT_CELL <- STATEROOT_CELL:Int
- TRANSACTIONSROOT_CELL <- TRANSACTIONSROOT_CELL:Int
- RECEIPTSROOT_CELL <- RECEIPTSROOT_CELL:Int
- LOGSBLOOM_CELL <- LOGSBLOOM_CELL:Bytes
- DIFFICULTY_CELL <- DIFFICULTY_CELL:Int
- NUMBER_CELL <- NUMBER_CELL:Int
- GASLIMIT_CELL <- GASLIMIT_CELL:Int
- GASUSED_CELL <- GASUSED_CELL:Gas
- TIMESTAMP_CELL <- TIMESTAMP_CELL:Int
- EXTRADATA_CELL <- EXTRADATA_CELL:Bytes
- MIXHASH_CELL <- MIXHASH_CELL:Int
- BLOCKNONCE_CELL <- BLOCKNONCE_CELL:Int
- BASEFEE_CELL <- BASEFEE_CELL:Int
- WITHDRAWALSROOT_CELL <- WITHDRAWALSROOT_CELL:Int
- BLOBGASUSED_CELL <- BLOBGASUSED_CELL:Int
- EXCESSBLOBGAS_CELL <- EXCESSBLOBGAS_CELL:Int
- BEACONROOT_CELL <- BEACONROOT_CELL:Int
- OMMERBLOCKHEADERS_CELL <- OMMERBLOCKHEADERS_CELL:JSON
- TXORDER_CELL <- TXORDER_CELL:List
- TXPENDING_CELL <- TXPENDING_CELL:List
- MESSAGES_CELL <- MESSAGES_CELL:MessageCellMap
- PREVCALLER_CELL <- PREVCALLER_CELL:Account
- PREVORIGIN_CELL <- PREVORIGIN_CELL:Account
- NEWCALLER_CELL <- NEWCALLER_CELL:Account
- NEWORIGIN_CELL <- NEWORIGIN_CELL:Account
- DEPTH_CELL <- DEPTH_CELL:Int
- EXPECTEDREASON_CELL <- EXPECTEDREASON_CELL:Bytes
- EXPECTEDDEPTH_CELL <- EXPECTEDDEPTH_CELL:Int
- EXPECTEDADDRESS_CELL <- EXPECTEDADDRESS_CELL:Account
- EXPECTEDVALUE_CELL <- EXPECTEDVALUE_CELL:Int
- EXPECTEDDATA_CELL <- EXPECTEDDATA_CELL:Bytes
- OPCODETYPE_CELL <- OPCODETYPE_CELL:OpcodeType
- CHECKEDTOPICS_CELL <- CHECKEDTOPICS_CELL:List
- CHECKEDDATA_CELL <- CHECKEDDATA_CELL:Bool
- EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account
- GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int
-}
+┊ subst:
+┊ VGAS_4b7cee1f <- ( VGAS:Int +Int -373 )
├─ 4
│ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
│ pc: 2698
diff --git a/src/tests/integration/test-data/show/merge-loop-heads.expected b/src/tests/integration/test-data/show/merge-loop-heads.expected
index a92c4c7c0..cf64e6988 100644
--- a/src/tests/integration/test-data/show/merge-loop-heads.expected
+++ b/src/tests/integration/test-data/show/merge-loop-heads.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%BMCLoopsTest.test_bmc(uint256)
│
│ (350 steps)
@@ -12,25 +13,31 @@
│ pc: 1449
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:62:62
│ method: test%BMCLoopsTest.test_bmc(uint256)
┃
┃ (branch)
-┣━━┓ constraint: VV0_n_114b9705:Int <=Int 0
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ VV0_n_114b9705:Int <=Int 0
┃ │
┃ ├─ 4
┃ │ k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int 0 ) ~> #pc [ JUMPI ] ~> #execute ...
┃ │ pc: 1449
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/forge-std/src/StdInvariant.sol:62:62
┃ │ method: test%BMCLoopsTest.test_bmc(uint256)
┃ │
-┃ ┊ constraint: OMITTED CONSTRAINT
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ constraint:
+┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <=Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 0 andBool ( pow24 #pc [ JUMPI ...
┃ │ pc: 1449
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/forge-std/src/StdInvariant.sol:62:62
┃ │ method: test%BMCLoopsTest.test_bmc(uint256)
┃ │
┃ │ (135 steps)
@@ -39,15 +46,19 @@
┃ pc: 350
┃ callDepth: 0
┃ statusCode: STATUSCODE:StatusCode
+┃ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
┃ method: test%BMCLoopsTest.test_bmc(uint256)
┃
-┗━━┓ constraint: 0 #pc [ JUMPI ] ~> #execute ...
│ pc: 1449
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:62:62
│ method: test%BMCLoopsTest.test_bmc(uint256)
│
│ (224 steps)
@@ -56,35 +67,44 @@
│ pc: 1449
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:62:62
│ method: test%BMCLoopsTest.test_bmc(uint256)
┃
┃ (branch)
- ┣━━┓ constraint: VV0_n_114b9705:Int <=Int 1
+ ┣━━┓ subst: .Subst
+ ┃ ┃ constraint:
+ ┃ ┃ VV0_n_114b9705:Int <=Int 1
┃ │
┃ ├─ 9
┃ │ k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int 1 ) ~> #pc [ JUMPI ] ~> #execute ...
┃ │ pc: 1449
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+ ┃ │ src: lib/forge-std/src/StdInvariant.sol:62:62
┃ │ method: test%BMCLoopsTest.test_bmc(uint256)
┃ │
- ┃ ┊ constraint: OMITTED CONSTRAINT
- ┃ ┊ subst: OMITTED SUBST
+ ┃ ┊ constraint:
+ ┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 #pc [ JUMPI ...
┃ pc: 1449
┃ callDepth: 0
┃ statusCode: STATUSCODE:StatusCode
+ ┃ src: lib/forge-std/src/StdInvariant.sol:62:62
┃ method: test%BMCLoopsTest.test_bmc(uint256)
┃ (continues as previously)
┃
- ┗━━┓ constraint: 1 #pc [ JUMPI ] ~> #execute ...
│ pc: 1449
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:62:62
│ method: test%BMCLoopsTest.test_bmc(uint256)
│
│ (224 steps)
@@ -93,35 +113,44 @@
│ pc: 1449
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:62:62
│ method: test%BMCLoopsTest.test_bmc(uint256)
┃
┃ (branch)
- ┣━━┓ constraint: VV0_n_114b9705:Int <=Int 2
+ ┣━━┓ subst: .Subst
+ ┃ ┃ constraint:
+ ┃ ┃ VV0_n_114b9705:Int <=Int 2
┃ │
┃ ├─ 15
┃ │ k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int 2 ) ~> #pc [ JUMPI ] ~> #execute ...
┃ │ pc: 1449
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+ ┃ │ src: lib/forge-std/src/StdInvariant.sol:62:62
┃ │ method: test%BMCLoopsTest.test_bmc(uint256)
┃ │
- ┃ ┊ constraint: OMITTED CONSTRAINT
- ┃ ┊ subst: OMITTED SUBST
+ ┃ ┊ constraint:
+ ┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 #pc [ JUMPI ...
┃ pc: 1449
┃ callDepth: 0
┃ statusCode: STATUSCODE:StatusCode
+ ┃ src: lib/forge-std/src/StdInvariant.sol:62:62
┃ method: test%BMCLoopsTest.test_bmc(uint256)
┃ (continues as previously)
┃
- ┗━━┓ constraint: 2 #pc [ JUMPI ] ~> #execute ...
│ pc: 1449
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:62:62
│ method: test%BMCLoopsTest.test_bmc(uint256)
│
│ (224 steps)
@@ -130,25 +159,32 @@
│ pc: 1449
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:62:62
│ method: test%BMCLoopsTest.test_bmc(uint256)
┃
┃ (branch)
- ┣━━┓ constraint: VV0_n_114b9705:Int <=Int 3
+ ┣━━┓ subst: .Subst
+ ┃ ┃ constraint:
+ ┃ ┃ VV0_n_114b9705:Int <=Int 3
┃ │
┃ └─ 21 (leaf, pending)
┃ k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int 3 ) ~> #pc [ JUMPI ] ~> #execute ...
┃ pc: 1449
┃ callDepth: 0
┃ statusCode: STATUSCODE:StatusCode
+ ┃ src: lib/forge-std/src/StdInvariant.sol:62:62
┃ method: test%BMCLoopsTest.test_bmc(uint256)
┃
- ┗━━┓ constraint: 3 #pc [ JUMPI ] ~> #execute ...
pc: 1449
callDepth: 0
statusCode: STATUSCODE:StatusCode
+ src: lib/forge-std/src/StdInvariant.sol:62:62
method: test%BMCLoopsTest.test_bmc(uint256)
diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected
index 522b22760..3c95ee8d5 100644
--- a/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected
+++ b/src/tests/integration/test-data/show/minimized/AssertTest.testFail_expect_revert().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (1272 steps)
@@ -12,6 +13,7 @@
pc: 328
callDepth: 0
statusCode: EVMC_SUCCESS
+ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
method: test%AssertTest.testFail_expect_revert()
diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected
index 6b8150ff8..243bc04a1 100644
--- a/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected
+++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_assert_false().expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (493 steps)
diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected
index 1354e0166..0e7f2c536 100644
--- a/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected
+++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_failing_branch(uint256).expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (543 steps)
@@ -12,16 +13,20 @@
│ pc: 1116
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:74:74
│ method: test%AssertTest.test_failing_branch(uint256)
┃
┃ (branch)
-┣━━┓ constraint: 100 <=Int VV0_x_114b9705:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ 100 <=Int VV0_x_114b9705:Int
┃ │
┃ ├─ 9
┃ │ k: JUMPI 1124 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execu ...
┃ │ pc: 1116
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/forge-std/src/StdInvariant.sol:74:74
┃ │ method: test%AssertTest.test_failing_branch(uint256)
┃ │
┃ │ (42 steps)
@@ -30,23 +35,27 @@
┃ │ pc: 328
┃ │ callDepth: 0
┃ │ statusCode: EVMC_SUCCESS
+┃ │ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
┃ │ method: test%AssertTest.test_failing_branch(uint256)
┃ │
┃ ┊ constraint: true
-┃ ┊ subst: OMITTED SUBST
+┃ ┊ subst: ...
┃ └─ 7 (leaf, target, terminal)
┃ k: #halt ~> CONTINUATION:K
┃ pc: PC_CELL_5d410f2a:Int
┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int
┃ statusCode: STATUSCODE_FINAL:StatusCode
┃
-┗━━┓ constraint: VV0_x_114b9705:Int #pc [ JUMPI ] ~> #execu ...
│ pc: 1116
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:74:74
│ method: test%AssertTest.test_failing_branch(uint256)
│
│ (66 steps)
diff --git a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected
index 131f025b0..efb378b48 100644
--- a/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected
+++ b/src/tests/integration/test-data/show/minimized/AssertTest.test_revert_branch(uint256,uint256).expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%AssertTest.setUp()
│
│ (549 steps)
@@ -12,16 +13,20 @@
│ pc: 1590
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/lib/ds-test/src/test.sol:48:62
│ method: test%AssertTest.test_revert_branch(uint256,uint256)
┃
┃ (branch)
-┣━━┓ constraint: VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int
┃ │
┃ ├─ 9
┃ │ k: JUMPI 1594 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ...
┃ │ pc: 1590
┃ │ callDepth: 0
┃ │ statusCode: STATUSCODE:StatusCode
+┃ │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62
┃ │ method: test%AssertTest.test_revert_branch(uint256,uint256)
┃ │
┃ │ (75 steps)
@@ -32,13 +37,16 @@
┃ statusCode: EVMC_REVERT
┃ method: test%AssertTest.test_revert_branch(uint256,uint256)
┃
-┗━━┓ constraint: VV0_x_114b9705:Int #pc [ JU ...
│ pc: 1590
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/lib/ds-test/src/test.sol:48:62
│ method: test%AssertTest.test_revert_branch(uint256,uint256)
│
│ (40 steps)
@@ -47,6 +55,7 @@
pc: 328
callDepth: 0
statusCode: EVMC_SUCCESS
+ src: lib/kontrol-cheatcodes/src/KontrolCheats.sol:8:8
method: test%AssertTest.test_revert_branch(uint256,uint256)
diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected
index a5a82dbea..9d114eafd 100644
--- a/src/tests/integration/test-data/show/node-refutation.expected
+++ b/src/tests/integration/test-data/show/node-refutation.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%MergeTest.test_branch_merge(uint256)
│
│ (324 steps)
@@ -12,25 +13,32 @@
│ pc: 525
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: lib/forge-std/src/StdInvariant.sol:90:90
│ method: test%MergeTest.test_branch_merge(uint256)
┃
┃ (branch)
-┣━━┓ constraint: 10 <=Int VV0_x_114b9705:Int
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ 10 <=Int VV0_x_114b9705:Int
┃ │
┃ └─ 4 (leaf, refuted)
┃ k: JUMPI 535 bool2Word ( 10 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execute ...
┃ pc: 525
┃ callDepth: 0
┃ statusCode: STATUSCODE:StatusCode
+┃ src: lib/forge-std/src/StdInvariant.sol:90:90
┃ method: test%MergeTest.test_branch_merge(uint256)
┃
-┗━━┓ constraint: VV0_x_114b9705:Int #pc [ JUMPI ] ~> #execute ...
│ pc: 525
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:90:90
│ method: test%MergeTest.test_branch_merge(uint256)
│
│ (90 steps)
@@ -39,6 +47,7 @@
│ pc: 235
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+ │ src: lib/forge-std/src/StdInvariant.sol:77:79
│ method: test%MergeTest.test_branch_merge(uint256)
│
│ (1 step)
@@ -47,6 +56,7 @@
│ pc: 235
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/src/StdInvariant.sol:77:79
│ method: test%MergeTest.test_branch_merge(uint256)
│
│ (2 steps)
@@ -55,10 +65,11 @@
│ pc: 235
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/src/StdInvariant.sol:77:79
│ method: test%MergeTest.test_branch_merge(uint256)
│
┊ constraint: true
- ┊ subst: OMITTED SUBST
+ ┊ subst: ...
└─ 2 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/show/split-node.expected b/src/tests/integration/test-data/show/split-node.expected
index 7611c16aa..b12252bd5 100644
--- a/src/tests/integration/test-data/show/split-node.expected
+++ b/src/tests/integration/test-data/show/split-node.expected
@@ -4,6 +4,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%PrankTest.setUp()
│
│ (601 steps)
@@ -12,6 +13,7 @@
│ pc: 292
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+│ src: lib/forge-std/lib/ds-test/src/test.sol:47:63
│ method: test%PrankTest.setUp()
│
│ (1 step)
@@ -20,6 +22,7 @@
│ pc: 0
│ callDepth: 0
│ statusCode: STATUSCODE:StatusCode
+│ src: test/nested/SimpleNested.t.sol:7:11
│ method: test%PrankTest.testSymbolicStartPrank(address)
│
│ (585 steps)
@@ -39,7 +42,9 @@
│ method: test%PrankTest.testSymbolicStartPrank(address)
┃
┃ (branch)
-┣━━┓ constraint: VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263
+┣━━┓ subst: .Subst
+┃ ┃ constraint:
+┃ ┃ VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263
┃ │
┃ └─ 70 (leaf, refuted)
┃ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -48,7 +53,9 @@
┃ statusCode: STATUSCODE:StatusCode
┃ method: test%PrankTest.testSymbolicStartPrank(address)
┃
-┗━━┓ constraint: ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263 )
+┗━━┓ subst: .Subst
+ ┃ constraint:
+ ┃ ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263 )
│
├─ 71 (split)
│ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -58,7 +65,9 @@
│ method: test%PrankTest.testSymbolicStartPrank(address)
┃
┃ (branch)
- ┣━━┓ constraint: VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349
+ ┣━━┓ subst: .Subst
+ ┃ ┃ constraint:
+ ┃ ┃ VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349
┃ │
┃ └─ 72 (leaf, refuted)
┃ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -67,7 +76,9 @@
┃ statusCode: STATUSCODE:StatusCode
┃ method: test%PrankTest.testSymbolicStartPrank(address)
┃
- ┗━━┓ constraint: ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349 )
+ ┗━━┓ subst: .Subst
+ ┃ constraint:
+ ┃ ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349 )
│
├─ 73 (split)
│ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -77,7 +88,9 @@
│ method: test%PrankTest.testSymbolicStartPrank(address)
┃
┃ (branch)
- ┣━━┓ constraint: VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518
+ ┣━━┓ subst: .Subst
+ ┃ ┃ constraint:
+ ┃ ┃ VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518
┃ │
┃ └─ 74 (leaf, refuted)
┃ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -86,7 +99,9 @@
┃ statusCode: STATUSCODE:StatusCode
┃ method: test%PrankTest.testSymbolicStartPrank(address)
┃
- ┗━━┓ constraint: ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518 )
+ ┗━━┓ subst: .Subst
+ ┃ constraint:
+ ┃ ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518 )
│
├─ 75
│ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
@@ -117,6 +132,7 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%Prank.msgSender()
│
│ (1 step)
@@ -125,6 +141,7 @@
│ pc: 0
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%Prank.msgSender()
│
│ (320 steps)
@@ -133,6 +150,7 @@
│ pc: 130
│ callDepth: 1
│ statusCode: STATUSCODE:StatusCode
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%Prank.msgSender()
│
│ (1 step)
@@ -141,6 +159,7 @@
│ pc: 130
│ callDepth: 1
│ statusCode: EVMC_SUCCESS
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%Prank.msgSender()
│
│ (2 steps)
@@ -149,6 +168,7 @@
│ pc: 130
│ callDepth: 1
│ statusCode: EVMC_SUCCESS
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%Prank.msgSender()
│
│ (1 step)
@@ -157,6 +177,7 @@
│ pc: 130
│ callDepth: 1
│ statusCode: EVMC_SUCCESS
+ │ src: test/nested/SimpleNested.t.sol:7:11
│ method: src%Prank.msgSender()
│
│ (549 steps)
@@ -165,6 +186,7 @@
│ pc: 1578
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:47
│ method: test%PrankTest.testSymbolicStartPrank(address)
│
│ (1 step)
@@ -173,6 +195,7 @@
│ pc: 1578
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:47
│ method: test%PrankTest.testSymbolicStartPrank(address)
│
│ (102 steps)
@@ -181,6 +204,7 @@
│ pc: 292
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:63
│ method: test%PrankTest.testSymbolicStartPrank(address)
│
│ (1 step)
@@ -189,6 +213,7 @@
│ pc: 292
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:63
│ method: test%PrankTest.testSymbolicStartPrank(address)
│
│ (2 steps)
@@ -197,10 +222,14 @@
│ pc: 292
│ callDepth: 0
│ statusCode: EVMC_SUCCESS
+ │ src: lib/forge-std/lib/ds-test/src/test.sol:47:63
│ method: test%PrankTest.testSymbolicStartPrank(address)
│
- ┊ constraint: OMITTED CONSTRAINT
- ┊ subst: OMITTED SUBST
+ ┊ constraint:
+ ┊ ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263 )
+ ┊ ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349 )
+ ┊ ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518 )
+ ┊ subst: ...
└─ 10 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
pc: PC_CELL_5d410f2a:Int
diff --git a/src/tests/integration/test-data/src/TransientStorage.t.sol b/src/tests/integration/test-data/src/TransientStorage.t.sol
new file mode 100644
index 000000000..c4006f525
--- /dev/null
+++ b/src/tests/integration/test-data/src/TransientStorage.t.sol
@@ -0,0 +1,22 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.25;
+
+import "forge-std/Test.sol";
+
+contract TransientStorageTest is Test {
+ function testTransientStoreLoad(uint256 key, uint256 value) public {
+ // Store `value` at `key` in transient storage
+ assembly {
+ tstore(key, value)
+ }
+
+ uint256 loadedValue;
+
+ // Load `value` from `key` in transient storage
+ assembly {
+ loadedValue := tload(key)
+ }
+
+ assertEq(loadedValue, value, "TLOAD did not return the correct value");
+ }
+}
\ No newline at end of file
diff --git a/src/tests/integration/test-data/symbolic-bytes-lemmas.k b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
index abc913dfa..76376da0c 100644
--- a/src/tests/integration/test-data/symbolic-bytes-lemmas.k
+++ b/src/tests/integration/test-data/symbolic-bytes-lemmas.k
@@ -62,13 +62,6 @@ module SYMBOLIC-BYTES-LEMMAS
andBool 0 <=Int X andBool 0 { #buf ( 32, X ) #Equals B }
- requires #rangeUInt(256, X) andBool lengthBytes( B ) ==Int 32
- [simplification, concrete(X), preserves-definedness]
-
//
// String-related manipulation
//
diff --git a/src/tests/integration/test_kontrol.py b/src/tests/integration/test_kontrol.py
index a9e81669e..ef4917a60 100644
--- a/src/tests/integration/test_kontrol.py
+++ b/src/tests/integration/test_kontrol.py
@@ -13,6 +13,7 @@
from kontrol.kompile import foundry_kompile
from kontrol.options import BuildOptions, ProveOptions
from kontrol.prove import foundry_prove
+from kontrol.utils import append_to_file, foundry_toml_cancun_schedule
from .utils import TEST_DATA_DIR, assert_pass
@@ -59,6 +60,7 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath
if not foundry_root.is_dir():
init_project(project_root=foundry_root, skip_forge=False)
copy_tree(str(TEST_DATA_DIR / 'src'), str(foundry_root / 'test'))
+ append_to_file(foundry_root / 'foundry.toml', foundry_toml_cancun_schedule())
foundry_kompile(
BuildOptions(
@@ -112,6 +114,7 @@ def test_kontrol_end_to_end(
'usegas': False,
'port': server_end_to_end.port,
'force_sequential': force_sequential,
+ 'schedule': 'CANCUN',
}
),
)