diff --git a/.github/workflows/docker-push.yml b/.github/workflows/kontrol-push-fixed-deps.yml similarity index 95% rename from .github/workflows/docker-push.yml rename to .github/workflows/kontrol-push-fixed-deps.yml index 909a6da4d..032f04bcc 100644 --- a/.github/workflows/docker-push.yml +++ b/.github/workflows/kontrol-push-fixed-deps.yml @@ -1,5 +1,5 @@ --- -name: 'Push Docker Image' +name: 'Push Kontrol w/ FIXED Dependencies' on: workflow_dispatch: @@ -29,7 +29,7 @@ jobs: echo "CONTAINER_NAME=kontrol-ci-docker-${GITHUB_SHA}" >> ${GITHUB_ENV} BRANCH_NAME="${{ github.event.inputs.kontrol_branch }}" SANITIZED_BRANCH_NAME=$(echo "${BRANCH_NAME}" | tr '/' '-' | tr -cd '[:alnum:]-_.') - GHCR_TAG=ghcr.io/runtimeverification/kontrol/kontrol:ubuntu-jammy-${SANITIZED_BRANCH_NAME} + GHCR_TAG=ghcr.io/runtimeverification/kontrol/kontrol-custom:ubuntu-jammy-${SANITIZED_BRANCH_NAME} echo "GHCR_TAG=${GHCR_TAG}" >> ${GITHUB_ENV} echo "DOCKER_USER=user" >> ${GITHUB_ENV} echo "DOCKER_GROUP=user" >> ${GITHUB_ENV} diff --git a/.github/workflows/kontrol-push-unfixed-deps.yml b/.github/workflows/kontrol-push-unfixed-deps.yml new file mode 100644 index 000000000..d4855da09 --- /dev/null +++ b/.github/workflows/kontrol-push-unfixed-deps.yml @@ -0,0 +1,74 @@ +--- +name: 'Push Kontrol w/ Dependencies' +on: + workflow_dispatch: + inputs: + kontrol-version: + description: 'Branch/Tag to use for Kontrol' + required: false + default: '' + kevm-version: + description: 'SHA to use for KEVM' + required: false + default: '' + k-version: + description: 'SHA to use for K' + required: false + default: '' + llvm-version: + description: 'SHA to use for LLVM Backend' + required: false + default: '' + haskell-version: + description: 'SHA to use for Haskell Backend' + required: false + default: '' +permissions: + packages: write + +jobs: + build-kontrol: + runs-on: [self-hosted, normal] + steps: + - name: 'Login to GitHub Container Registry' + uses: docker/login-action@v2 + with: + registry: ghcr.io + username: ${{ github.actor }} + password: ${{ secrets.GITHUB_TOKEN }} + - name: 'Build Kontrol' + shell: bash + run: | + set -o pipefail + docker run --env GH_TOKEN=${{ secrets.GITHUB_TOKEN }} --rm -it --detach --name kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kup:latest + if [ -n "${{ inputs.kontrol-version }}" ]; then + KONTROL_OVERRIDE="--version ${{ inputs.kontrol-version }}" + fi + if [ -n "${{ inputs.kevm-version }}" ]; then + KEVM_OVERRIDE="--override kevm ${{ inputs.kevm-version }}" + fi + if [ -n "${{ inputs.k-version }}" ]; then + K_OVERRIDE="--override kevm/k-framework ${{ inputs.k-version }}" + fi + if [ -n "${{ inputs.llvm-version }}" ]; then + LLVM_OVERRIDE="--override kevm/k-framework/llvm-backend ${{ inputs.llvm-version }}" + fi + if [ -n "${{ inputs.haskell-version }}" ]; then + HASKELL_OVERRIDE="--override kevm/k-framework/haskell-backend ${{ inputs.haskell-version }}" + fi + docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash -c "kup install kontrol ${KONTROL_OVERRIDE} ${KEVM_OVERRIDE} ${K_OVERRIDE} ${LLVM_OVERRIDE} ${HASKELL_OVERRIDE}" + docker exec kontrol-build-with-kup-${{ github.run_id }} /bin/bash -c "kup list kontrol --inputs" >> versions.out + docker commit kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }} + docker push ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }} + - name: 'Publish Versions to Artifacts' + uses: actions/upload-artifact@v3 + with: + name: Versions + path: versions.out + - name: 'Publish Image Name to Workflow Summary' + run: | + echo "Image Name: ghcr.io/runtimeverification/kontrol-custom:${{ github.run_id }}" >> $GITHUB_STEP_SUMMARY + - name: 'Tear down Docker' + if: always() + run: | + docker stop --time=0 kontrol-build-with-kup-${{ github.run_id }} diff --git a/README.md b/README.md index 1e42ba748..e264c04f6 100644 --- a/README.md +++ b/README.md @@ -71,7 +71,82 @@ To update the expected output of the tests, use the `--update-expected-output` f make cov-integration TEST_ARGS="--numprocesses=8 --update-expected-output" ``` -For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter. +### Build Development Kontrol Image with Fixed Upstream Dependencies +-------------------------------- +Relevant to this workflow [kontrol-push-fixed-deps.yml](.github/workflows/kontrol-push-fixed-deps.yml) +>This is relevant for internal development to publish development images of Kontrol with modified Kontrol changes and retain fixed upstream dependencies. +The use case for this workflow is intended to facilitate testing changes to Kontrol needed for use in testing CI or in other downstream workflows without needing to publish changes or PRs first. + +The intent is to reduce the friction of needing custom builds and avoiding lengthy upstream changes and PRs. + +### Build Kontrol with Kup and Specific Dependency Overrides +-------------------------------- +Relevant to this workflow [kup-build-kontrol.yml](.github/workflows/kontrol-push-unfixed-deps.yml) +> This is relevant for internal development to publish development images of Kontrol for use in KaaS or a dockerized test environment. +Use the workflow [Kup Build Kontrol](.github/workflows/kup-build-kontrol.yml) to publish a custom version of Kontrol for use in CI and [KaaS](https://kaas.runtimeverification.com/). +[See KUP docs for more information](https://github.com/runtimeverification/kup/blob/master/src/kup/install-help.md#kup-install----override) + +#### Using Kup +------------- +Relevant dependency options are shown below and can be listed using `kup list kontrol --inputs` +For example: +``` +Inputs: +├── k-framework - follows kevm/k-framework +├── kevm - github:runtimeverification/evm-semantics (6c2526b) +│ ├── blockchain-k-plugin - github:runtimeverification/blockchain-k-plugin (c9264b2) +│ │ ├── k-framework - github:runtimeverification/k (5d1ccd5) +│ │ │ ├── haskell-backend - github:runtimeverification/haskell-backend (d933d5c) +│ │ │ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils +│ │ │ ├── llvm-backend - github:runtimeverification/llvm-backend (37b1dd9) +│ │ │ │ ├── immer-src - github:runtimeverification/immer (4b0914f) +│ │ │ │ └── rv-utils - github:runtimeverification/rv-nix-tools (a650588) +│ │ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/llvm-backend/rv-utils +│ │ └── rv-utils - follows kevm/blockchain-k-plugin/k-framework/rv-utils +│ ├── haskell-backend - follows kevm/k-framework/haskell-backend +│ ├── k-framework - github:runtimeverification/k (81bcc24) +│ │ ├── haskell-backend - github:runtimeverification/haskell-backend (786c780) +│ │ │ └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils +│ │ ├── llvm-backend - github:runtimeverification/llvm-backend (d5eab4b) +│ │ │ ├── immer-src - github:runtimeverification/immer (4b0914f) +│ │ │ └── rv-utils - github:runtimeverification/rv-nix-tools (a650588) +│ │ └── rv-utils - follows kevm/k-framework/llvm-backend/rv-utils +│ └── rv-utils - follows kevm/k-framework/rv-utils +└── rv-utils - follows kevm/rv-utils +``` +> **Notice**: the 'follows' in the 'kup list' output. This shows the links to the important dependencies and which are affected when you set the overrides. + +Now run a build using kup and specific dependency overrides: + +`kup install kontrol --override kevm/k-framework/haskell-backend "hash/branch_name" --override kevm/k-framework/haskell-backend "hash"` + +> **Note**: It's important that you use the short-rev hash or the long for specific revisions of the dependencies to modify. + +#### Using the workflow to publish to ghcr.io/runtimeverification +-------------------------------- + +#### Running the workflow +- Go to repo [Kontrol Actions Page](https://github.com/runtimeverification/kontrol/actions) +- Click on "Push Kontrol w/ Dependencies" from the left hand list +- Click on "Run Workflow" on the top right corner of the list of workflow runs is an option "Run Workflow". +- Use the 'master' branch unless you're doing something special. +- Input the override hash strings for specific dependencies to override in kontrol. See below on how to find the hash for the dependency. +- Then click "Run Workflow" and a job will start. +- The workflow summary shows the name of the image that was built and pushed e.g. ghcr.io/runtimeverification/kontrol-custom:tag + +> **Note**: The tag will be a randomly generated string. + +[The workflow](.github/workflows/kontrol-push-unfixed-deps.yml) takes multiple inputs to override the various components of kontrol. Those overrides are listed above in the example output of 'kup list kontrol --inputs' + +To set the desired revisions of the dependencies. Find the associated hash on the branch and commit made to be used for the dependnecy override. +If an input is left blank, the workflow will workout the default hash to use based on kontrols latest release. + +Example to fetch the desired hash to insert a different dependency version into the kontrol build. +Substitude the k-framework revision used to build kontrol. +``` +K_TAG=$(curl -s https://raw.githubusercontent.com/runtimeverification/kontrol/master/deps/k_release) +git ls-remote https://github.com/runtimeverification/k.git refs/tags/v${K_TAG} | awk '{print $1}' +``` ## Resources diff --git a/deps/k_release b/deps/k_release index 9aa8cae8e..5f759ce58 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.205 +7.1.207 diff --git a/deps/kevm_release b/deps/kevm_release index 3a8abe45d..4f91bbee6 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.779 +1.0.783 diff --git a/flake.lock b/flake.lock index bf742f54e..4501bf4f4 100644 --- a/flake.lock +++ b/flake.lock @@ -390,16 +390,16 @@ ] }, "locked": { - "lastModified": 1737403363, - "narHash": "sha256-W+qMyPgbgoeFugC9vQKOoHUHdbLqvS2X7ObhcMEQxOU=", + "lastModified": 1737656969, + "narHash": "sha256-rgt44+Zt9NLeYtBfbxSCKmuS+/YrCPKOoq1s5ggv7wQ=", "owner": "runtimeverification", "repo": "k", - "rev": "ab00be0b289ac0fe59c845ffb82c8c4a107f50ff", + "rev": "53ae31ec1518a054776e8ba7b31a4c369f8af023", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.205", + "ref": "v7.1.207", "repo": "k", "type": "github" } @@ -435,16 +435,16 @@ ] }, "locked": { - "lastModified": 1737531698, - "narHash": "sha256-l3p1qZtmCYGUsuL9aXVSBk5B2BKBk7lafK+ONjedAZ8=", + "lastModified": 1737702704, + "narHash": "sha256-2yw41KmDf0DvdBOaPfWcEKh0nrTghMdKUBbQ6w5Lplw=", "owner": "runtimeverification", "repo": "evm-semantics", - "rev": "69256070065dad12ce46dedfbf1d45b3084d335d", + "rev": "439ff0f33a7e8e1a70a387d56f75291912a5d973", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v1.0.779", + "ref": "v1.0.783", "repo": "evm-semantics", "type": "github" } diff --git a/flake.nix b/flake.nix index a17fea0c4..29271fc5f 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Kontrol"; inputs = { - kevm.url = "github:runtimeverification/evm-semantics/v1.0.779"; + kevm.url = "github:runtimeverification/evm-semantics/v1.0.783"; 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 c452c5761..eb4acbcb5 100644 --- a/poetry.lock +++ b/poetry.lock @@ -2,14 +2,14 @@ [[package]] name = "attrs" -version = "24.3.0" +version = "25.1.0" description = "Classes Without Boilerplate" optional = false python-versions = ">=3.8" groups = ["main", "dev"] files = [ - {file = "attrs-24.3.0-py3-none-any.whl", hash = "sha256:ac96cd038792094f438ad1f6ff80837353805ac950cd2aa0e0625ef19850c308"}, - {file = "attrs-24.3.0.tar.gz", hash = "sha256:8f5c07333d543103541ba7be0e2ce16eeee8130cb0b3f9238ab904ce1e85baff"}, + {file = "attrs-25.1.0-py3-none-any.whl", hash = "sha256:c75a69e28a550a7e93789579c22aa26b0f5b83b75dc4e08fe092980051e1090a"}, + {file = "attrs-25.1.0.tar.gz", hash = "sha256:1c97078a80c814273a76b2a298a932eb681c87415c11dee0a6921de7f1b02c3e"}, ] [package.extras] @@ -112,14 +112,14 @@ colorama = {version = "*", markers = "platform_system == \"Windows\""} [[package]] name = "cmd2" -version = "2.5.9" +version = "2.5.11" description = "cmd2 - quickly build feature-rich and user-friendly interactive command line applications in Python" optional = false python-versions = ">=3.8" groups = ["main"] files = [ - {file = "cmd2-2.5.9-py3-none-any.whl", hash = "sha256:b2621661fe48a5a94343bd0f3285c18ca51ed9edda61406b6898895be0eb99ad"}, - {file = "cmd2-2.5.9.tar.gz", hash = "sha256:09bb13637832bc818aad5577ccdf5dbeb0c9fbe5b9412ff78d5084f7846f83ab"}, + {file = "cmd2-2.5.11-py3-none-any.whl", hash = "sha256:cbc79525e423dc2085ef7922cdc5586d1fedaecb768cdfb05e5482ee0740b755"}, + {file = "cmd2-2.5.11.tar.gz", hash = "sha256:30a0d385021fbe4a4116672845e5695bbe56eb682f9096066776394f954a7429"}, ] [package.dependencies] @@ -649,14 +649,14 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "hypothesis" -version = "6.124.2" +version = "6.124.7" description = "A library for property-based testing" optional = false python-versions = ">=3.9" groups = ["main"] files = [ - {file = "hypothesis-6.124.2-py3-none-any.whl", hash = "sha256:fef7709a404929a9cd3e785f60a6e026089aab986e288b1fdced13091574d474"}, - {file = "hypothesis-6.124.2.tar.gz", hash = "sha256:c98823fc1323f23399e5f2251982fd1f38259f84cf627aaaea1b3f0a0d4d2b03"}, + {file = "hypothesis-6.124.7-py3-none-any.whl", hash = "sha256:a6e1f66de84de3152d57f595a187a123ce3ecdea9dc8ef51ff8dcaa069137085"}, + {file = "hypothesis-6.124.7.tar.gz", hash = "sha256:8ed6c6ae47e7d26d869c1dc3dee04e8fc50c95240715bb9915ded88d6d920f0e"}, ] [package.dependencies] @@ -734,7 +734,7 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kevm-pyk" -version = "1.0.779" +version = "1.0.783" description = "" optional = false python-versions = "^3.10" @@ -743,27 +743,27 @@ files = [] develop = false [package.dependencies] -kframework = "7.1.205" +kframework = "7.1.207" pathos = "*" tomlkit = "^0.11.6" [package.source] type = "git" url = "https://github.com/runtimeverification/evm-semantics.git" -reference = "v1.0.779" -resolved_reference = "69256070065dad12ce46dedfbf1d45b3084d335d" +reference = "v1.0.783" +resolved_reference = "439ff0f33a7e8e1a70a387d56f75291912a5d973" subdirectory = "kevm-pyk" [[package]] name = "kframework" -version = "7.1.205" +version = "7.1.207" description = "" optional = false python-versions = "<4.0,>=3.10" groups = ["main"] files = [ - {file = "kframework-7.1.205-py3-none-any.whl", hash = "sha256:4e09f6b86b0431dcb76efe0f364ecb4da3bf8a52e7d4c8d6422f85412c944c3a"}, - {file = "kframework-7.1.205.tar.gz", hash = "sha256:d9d6b8fa39fc0271d475bb404e6e4bab1f56d33ff1111d667c56f9b1205b7d09"}, + {file = "kframework-7.1.207-py3-none-any.whl", hash = "sha256:aef7de704bcd404899def82460cb14beccd57a95d29b106e7cf379c7daaa3aca"}, + {file = "kframework-7.1.207.tar.gz", hash = "sha256:1acb6aa7b9bac5e170420015d6e5246f924e480287e68e4fa9fc20eb9874b228"}, ] [package.dependencies] @@ -1599,4 +1599,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.1" python-versions = "^3.10" -content-hash = "ff49535579af0b71ea04f78292bc68341370ce55d5fcdd2e1f501ff7f6067739" +content-hash = "3c74d397c72333756fb2c617bd3fb46a948d88aba912b0eaeff48acd02873bf8" diff --git a/pyproject.toml b/pyproject.toml index c877e0b4c..710f31406 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.779", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.783", subdirectory = "kevm-pyk" } eth-utils = "^4.1.1" pycryptodome = "^3.20.0" pyevmasm = "^0.2.3" diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index cbd6f7c4e..0a5dfbd08 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -26,6 +26,7 @@ collect, extract_lhs, flatten_label, + free_vars, minimize_term, set_cell, top_down, @@ -34,9 +35,10 @@ from pyk.kcfg import KCFG from pyk.kcfg.kcfg import Step from pyk.kcfg.minimize import KCFGMinimizer +from pyk.kdist import kdist from pyk.prelude.bytes import bytesToken from pyk.prelude.collections import map_empty -from pyk.prelude.k import DOTS +from pyk.prelude.k import DOTS, GENERATED_TOP_CELL from pyk.prelude.kbool import notBool from pyk.prelude.kint import INT, intToken from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue @@ -103,7 +105,7 @@ def cut_point_rules( break_on_basic_blocks: bool, break_on_load_program: bool, ) -> list[str]: - return ['FOUNDRY-CHEAT-CODES.rename'] + KEVMSemantics.cut_point_rules( + return ['FOUNDRY-CHEAT-CODES.rename', 'FOUNDRY-ACCOUNTS.forget'] + KEVMSemantics.cut_point_rules( break_on_jumpi, break_on_jump, break_on_calls, @@ -153,14 +155,145 @@ def _exec_rename_custom_step(self, cterm: CTerm) -> KCFGExtendResult | None: _LOGGER.info(f'Renaming {target_var.name} to {name}') return Step(CTerm(new_cterm.config, constraints), 1, (), ['foundry_rename'], cut=True) - def custom_step(self, cterm: CTerm, _cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None: + def _check_forget_pattern(self, cterm: CTerm) -> bool: + """Given a CTerm, check if the rule 'FOUNDRY-ACCOUNTS.forget' is at the top of the K_CELL. + This method checks if the 'FOUNDRY-ACCOUNTS.forget' rule is at the top of the `K_CELL` in the given `cterm`. + If the rule matches, the resulting substitution is cached in `_cached_subst` for later use in `custom_step` + :param cterm: The CTerm representing the current state of the proof node. + :return: `True` if the pattern matches and a custom step can be made; `False` otherwise. + """ + abstract_pattern = KSequence( + [ + KApply('cheatcode_forget', [KVariable('###TERM1'), KVariable('###OPERATOR'), KVariable('###TERM2')]), + KVariable('###CONTINUATION'), + ] + ) + self._cached_subst = abstract_pattern.match(cterm.cell('K_CELL')) + return self._cached_subst is not None + + def _exec_forget_custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None: + """Remove the constraint at the top of K_CELL of a given CTerm from its path constraints, + as part of the 'FOUNDRY-ACCOUNTS.forget' cut-rule. + :param cterm: CTerm representing a proof node + :param cterm_symbolic: CTermSymbolic instance + :return: A Step of depth 1 carrying a new configuration in which the constraint is consumed from the top + of the K cell and is removed from the initial path constraints if it existed, together with + information that the `cheatcode_forget` rule has been applied. + """ + + def _find_constraints_to_keep(cterm: CTerm, constraint_vars: frozenset[str]) -> set[KInner]: + range_patterns: list[KInner] = [ + mlEqualsTrue(KApply('_ set[KInner]: + for constraint_variant in constraints_to_remove: + simplification_cterm = initial_cterm.add_constraint(constraint_variant) + result_cterm, _ = cterm_symbolic.simplify(simplification_cterm) + # Extract constraints that appear after simplification but are not in the 'to keep' set + result_constraints = set(result_cterm.constraints).difference(constraints_to_keep) + + if len(result_constraints) == 1: + target_constraint = single(result_constraints) + if target_constraint in constraints: + _LOGGER.info(f'forgetBranch: removing constraint: {target_constraint}') + constraints.remove(target_constraint) + break + else: + _LOGGER.info(f'forgetBranch: constraint: {target_constraint} not found in current constraints') + else: + # If no constraints or multiple constraints appear, log this scenario. + if len(result_constraints) == 0: + _LOGGER.info(f'forgetBranch: constraint {constraint_variant} entailed by remaining constraints') + result_cterm, _ = cterm_symbolic.simplify(CTerm(empty_config.config, [constraint_variant])) + if len(result_cterm.constraints) == 1: + to_remove = single(result_cterm.constraints) + if to_remove in constraints: + _LOGGER.info(f'forgetBranch: removing constraint: {to_remove}') + constraints.remove(to_remove) + else: + _LOGGER.info( + f'forgetBranch: more than one constraint found after simplification and removal:\n{result_constraints}' + ) + return constraints + + _operators = ['_==Int_', '_=/=Int_', '_<=Int_', '_=Int_', '_>Int_'] + subst = self._cached_subst + assert subst is not None + # Extract the terms and operator from the substitution + fst_term = subst['###TERM1'] + snd_term = subst['###TERM2'] + operator = subst['###OPERATOR'] + assert isinstance(operator, KToken) + # Construct the positive and negative constraints + pos_constraint = mlEqualsTrue(KApply(_operators[int(operator.token)], fst_term, snd_term)) + neg_constraint = mlEqualsTrue(notBool(KApply(_operators[int(operator.token)], fst_term, snd_term))) + # To be able to better simplify, we maintain range constraints on the variables present in the constraint + constraint_vars: frozenset[str] = free_vars(fst_term).union(free_vars(snd_term)) + constraints_to_keep: set[KInner] = _find_constraints_to_keep(cterm, constraint_vars) + + # Set up initial configuration for constraint simplification, and simplify it to get all + # of the kept constraints in the form in which they will appear after constraint simplification + kevm = KEVM(kdist.get('kontrol.foundry')) + empty_config: CTerm = CTerm.from_kast(kevm.definition.empty_config(GENERATED_TOP_CELL)) + initial_cterm, _ = cterm_symbolic.simplify(CTerm(empty_config.config, constraints_to_keep)) + constraints_to_keep = set(initial_cterm.constraints) + + # Simplify in the presence of constraints to keep, then remove the constraints to keep to + # reveal simplified constraint, then remove if present in original constraints + new_constraints: set[KInner] = _filter_constraints_by_simplification( + cterm_symbolic=cterm_symbolic, + initial_cterm=initial_cterm, + constraints_to_remove=[pos_constraint, neg_constraint], + constraints_to_keep=constraints_to_keep, + constraints=set(cterm.constraints), + empty_config=empty_config, + ) + + # Update the K_CELL with the continuation + new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION']))) + return Step(CTerm(new_cterm.config, new_constraints), 1, (), ['cheatcode_forget'], cut=True) + + def custom_step(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None: if self._check_rename_pattern(cterm): return self._exec_rename_custom_step(cterm) + elif self._check_forget_pattern(cterm): + return self._exec_forget_custom_step(cterm, cterm_symbolic) else: - return super().custom_step(cterm, _cterm_symbolic) + return super().custom_step(cterm, cterm_symbolic) def can_make_custom_step(self, cterm: CTerm) -> bool: - return self._check_rename_pattern(cterm) or super().can_make_custom_step(cterm) + return any( + [self._check_rename_pattern(cterm), self._check_forget_pattern(cterm), super().can_make_custom_step(cterm)] + ) class FoundryKEVM(KEVM): diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index c7c4ffcc9..15da6c2a9 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -1142,6 +1142,26 @@ Mock functions [priority(30)] ``` + +Abstraction functions +--------------------- + +#### `forgetBranch` - removes a given path constraint. + +``` + function forgetBranch(uint256 op1, ComparisonOperator op, uint256 op2) external; +``` + +```k + rule [cheatcode.call.abstract]: + #cheatcode_call SELECTOR ARGS + => #forget ( #asWord(#range(ARGS,0,32)), #asWord(#range(ARGS,32,32)), #asWord(#range(ARGS,64,32))) + ... + + requires SELECTOR ==Int selector ( "forgetBranch(uint256,uint8,uint256)" ) + +``` + Utils ----- @@ -1751,6 +1771,7 @@ Selectors for **implemented** cheat code functions. rule ( selector ( "mockCall(address,bytes,bytes)" ) => 3110212580 ) rule ( selector ( "mockFunction(address,address,bytes)" ) => 2918731041 ) rule ( selector ( "copyStorage(address,address)" ) => 540912653 ) + rule ( selector ( "forgetBranch(uint256,uint8,uint256)" ) => 1720990067 ) ``` Selectors for **unimplemented** cheat code functions. diff --git a/src/kontrol/kdist/foundry.md b/src/kontrol/kdist/foundry.md index 2ac8861a7..871f0dd18 100644 --- a/src/kontrol/kdist/foundry.md +++ b/src/kontrol/kdist/foundry.md @@ -78,6 +78,10 @@ Then, we define helpers in K which can: STORAGE => STORAGE [ #loc(FoundryCheat . Failed) <- 1 ] ... + + syntax KItem ::= #forget ( Int , Int , Int ) [symbol(cheatcode_forget)] + // ----------------------------------------------------------------------- + rule [forget]: #forget(_C1,_OP,_C2) => .K ... ``` #### Structure of execution 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 6a2bc826c..749effdd8 100644 --- a/src/tests/integration/test-data/end-to-end-prove-all +++ b/src/tests/integration/test-data/end-to-end-prove-all @@ -1,14 +1,25 @@ CounterTest.test_Increment() +ForgetBranchTest.test_forgetBranch(uint256) RandomVarTest.test_custom_names() -RandomVarTest.test_randomBool() RandomVarTest.test_randomAddress() -RandomVarTest.test_randomUint() -RandomVarTest.test_randomUint_192() -RandomVarTest.test_randomUint_Range(uint256,uint256) +RandomVarTest.test_randomBool() RandomVarTest.test_randomBytes_length(uint256) RandomVarTest.test_randomBytes4_length() RandomVarTest.test_randomBytes8_length() +RandomVarTest.test_randomUint_192() +RandomVarTest.test_randomUint_Range(uint256,uint256) +RandomVarTest.test_randomUint() TransientStorageTest.testTransientStoreLoad(uint256,uint256) +UnitTest.test_assert_eq_address_darray(address[]) +UnitTest.test_assert_eq_bool_darray(bool[]) +UnitTest.test_assert_eq_bytes32_darray(bytes32[]) +UnitTest.test_assert_eq_int256_darray(int256[]) +UnitTest.test_assert_eq_uint256_darray(uint256[]) +UnitTest.test_assertApproxEqAbs_int_same_sign(uint256,uint256,uint256) +UnitTest.test_assertApproxEqAbs_uint(uint256,uint256,uint256) +UnitTest.test_assertApproxEqRel_int_same_sign_unit() +UnitTest.test_assertApproxEqRel_int_zero_cases_unit() +UnitTest.test_assertApproxEqRel_uint_unit() UnitTest.test_assertEq_address_err() UnitTest.test_assertEq_bool_err() UnitTest.test_assertEq_bytes32_err() @@ -39,13 +50,3 @@ UnitTest.test_assertNotEq(bytes32,bytes32) UnitTest.test_assertNotEq(int256,int256) UnitTest.test_assertTrue_err() UnitTest.test_assertTrue(bool) -UnitTest.test_assertApproxEqAbs_uint(uint256,uint256,uint256) -UnitTest.test_assertApproxEqAbs_int_same_sign(uint256,uint256,uint256) -UnitTest.test_assertApproxEqRel_uint_unit() -UnitTest.test_assertApproxEqRel_int_same_sign_unit() -UnitTest.test_assertApproxEqRel_int_zero_cases_unit() -UnitTest.test_assert_eq_bytes32_darray(bytes32[]) -UnitTest.test_assert_eq_bool_darray(bool[]) -UnitTest.test_assert_eq_int256_darray(int256[]) -UnitTest.test_assert_eq_uint256_darray(uint256[]) -UnitTest.test_assert_eq_address_darray(address[]) diff --git a/src/tests/integration/test-data/end-to-end-prove-show b/src/tests/integration/test-data/end-to-end-prove-show index 028eb6cd8..067333b96 100644 --- a/src/tests/integration/test-data/end-to-end-prove-show +++ b/src/tests/integration/test-data/end-to-end-prove-show @@ -1 +1,2 @@ +ForgetBranchTest.test_forgetBranch(uint256) RandomVarTest.test_custom_names() diff --git a/src/tests/integration/test-data/end-to-end-prove-skip b/src/tests/integration/test-data/end-to-end-prove-skip index 903580e0c..2668de8ef 100644 --- a/src/tests/integration/test-data/end-to-end-prove-skip +++ b/src/tests/integration/test-data/end-to-end-prove-skip @@ -1,3 +1,19 @@ +UnitTest.test_assert_eq_address_darray_err() +UnitTest.test_assert_eq_bool_darray_err() +UnitTest.test_assert_eq_bytes32_darray_err() +UnitTest.test_assert_eq_int256_darray_err() +UnitTest.test_assert_eq_uint256_darray_err() +UnitTest.test_assertApproxEqAbs_int_opp_sign_err() +UnitTest.test_assertApproxEqAbs_int_opp_sign(uint256,uint256,uint256) +UnitTest.test_assertApproxEqAbs_int_same_sign_err() +UnitTest.test_assertApproxEqAbs_int_zero_cases_err() +UnitTest.test_assertApproxEqAbs_int_zero_cases(uint256,uint256) +UnitTest.test_assertApproxEqAbs_uint_err() +UnitTest.test_assertApproxEqRel_int_opp_sign_err() +UnitTest.test_assertApproxEqRel_int_opp_sign_unit() +UnitTest.test_assertApproxEqRel_int_same_sign_err() +UnitTest.test_assertApproxEqRel_int_zero_cases_err() +UnitTest.test_assertApproxEqRel_uint_err() UnitTest.test_assertEq_address_err() UnitTest.test_assertEq_bool_err() UnitTest.test_assertEq_bytes32_err() @@ -13,20 +29,4 @@ UnitTest.test_assertNotEq_bool_err() UnitTest.test_assertNotEq_bytes32_err() UnitTest.test_assertNotEq_err() UnitTest.test_assertNotEq_int256_err() -UnitTest.test_assertTrue_err() -UnitTest.test_assertApproxEqAbs_uint_err() -UnitTest.test_assertApproxEqAbs_int_same_sign_err() -UnitTest.test_assertApproxEqAbs_int_opp_sign(uint256,uint256,uint256) -UnitTest.test_assertApproxEqAbs_int_opp_sign_err() -UnitTest.test_assertApproxEqAbs_int_zero_cases(uint256,uint256) -UnitTest.test_assertApproxEqAbs_int_zero_cases_err() -UnitTest.test_assertApproxEqRel_uint_err() -UnitTest.test_assertApproxEqRel_int_same_sign_err() -UnitTest.test_assertApproxEqRel_int_opp_sign_unit() -UnitTest.test_assertApproxEqRel_int_opp_sign_err() -UnitTest.test_assertApproxEqRel_int_zero_cases_err() -UnitTest.test_assert_eq_bytes32_darray_err() -UnitTest.test_assert_eq_bool_darray_err() -UnitTest.test_assert_eq_int256_darray_err() -UnitTest.test_assert_eq_address_darray_err() -UnitTest.test_assert_eq_uint256_darray_err() \ No newline at end of file +UnitTest.test_assertTrue_err() \ No newline at end of file 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 30ef0fb59..8ce6adf4e 100644 --- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected +++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected @@ -33,7 +33,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -50,7 +50,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -304,7 +304,7 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 - ( _OUTPUT_CELL => #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -261,7 +261,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -275,10 +275,10 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0 - ( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) + ( _OUTPUT_CELL:Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) 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 3509a9af7..224231d75 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 @@ -34,7 +34,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -264,7 +264,7 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 andBool ( TIMESTAMP_CELL:Int #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -141,7 +141,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -515,7 +515,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ~> ( .K => #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -540,16 +540,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 CALLER_ID:Int - b"\xdf\xb7\xfe\xd0" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) + b"\xdf\xb7\xfe\xd0" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) 0 - ( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y : ( ?KV0_x : ( 247 : ( selector ( "test_double_add(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) + ( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 247 : ( selector ( "test_double_add(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) - b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) 0 @@ -665,7 +665,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 @@ -910,10 +910,10 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - ensures ( 0 <=Int ?KV0_x - andBool ( 0 <=Int ?KV1_y - andBool ( ?KV0_x #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -941,7 +941,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -1317,7 +1317,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1334,7 +1334,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -1711,7 +1711,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1728,7 +1728,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( 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 6199594f2..c626a4c93 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 @@ -173,7 +173,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -190,7 +190,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -564,7 +564,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> ( .K => #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -589,16 +589,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 CALLER_ID:Int - b"\xe1\xc3j\x8c" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) + b"\xe1\xc3j\x8c" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) 0 - ( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y : ( ?KV0_x : ( 247 : ( selector ( "test_double_add_double_sub(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) + ( 196 : ( selector ( "add(uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 247 : ( selector ( "test_double_add_double_sub(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) - b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) 0 @@ -714,7 +714,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"w\x16\x02\xf7" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 @@ -959,10 +959,10 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - ensures ( 0 <=Int ?KV0_x - andBool ( 0 <=Int ?KV1_y - andBool ( ?KV0_x #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -990,7 +990,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -1366,7 +1366,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1383,7 +1383,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -1760,7 +1760,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1777,7 +1777,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -2158,7 +2158,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2175,7 +2175,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -2558,7 +2558,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2575,7 +2575,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( 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 4d632dbd9..e46057596 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 @@ -177,7 +177,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -194,7 +194,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -570,7 +570,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -587,7 +587,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -964,7 +964,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> ( .K => #return 128 32 ~> #pc [ STATICCALL ] ~> #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -989,16 +989,16 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT CALLER_ID:Int - b"\x922\xed\x8c" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + b"\x922\xed\x8c" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 - ( 228 : ( selector ( "add_sub_external(uint256,uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 247 : ( selector ( "test_double_add_sub_external(uint256,uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) + ( 228 : ( selector ( "add_sub_external(uint256,uint256,uint256)" ) : ( 491460923342184218035706888008750043977755113263 : ( 0 : ( ?KV2_z:Int : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 247 : ( selector ( "test_double_add_sub_external(uint256,uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) - b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 @@ -1114,7 +1114,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( b"\n\x92T\xe4" => b"\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) ) + ( b"\n\x92T\xe4" => b"\x9c&\xe07" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) ) 0 @@ -1359,12 +1359,12 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - ensures ( 0 <=Int ?KV0_x - andBool ( 0 <=Int ?KV1_y - andBool ( 0 <=Int ?KV2_z - andBool ( ?KV0_x #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1392,7 +1392,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -1773,7 +1773,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1790,7 +1790,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( @@ -2172,7 +2172,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2189,7 +2189,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -2572,7 +2572,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2589,7 +2589,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( ListItem ( 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 2907a5dc0..a197790ee 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 @@ -82,7 +82,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 - ( _OUTPUT_CELL => #buf ( 32 , ( KV0_x:Int +Int KV1_y:Int ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , ( KV0_x:Int +Int KV1_y:Int ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -260,7 +260,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -274,10 +274,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0 - ( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) + ( _OUTPUT_CELL:Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) 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 f615ee2fe..c43cfb883 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 @@ -151,7 +151,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -165,10 +165,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) @@ -337,7 +337,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -351,10 +351,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) + ( _OUTPUT_CELL:Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ARITHMETICCONTRACT_ID:Int ) ) @@ -527,7 +527,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -541,10 +541,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _OUTPUT_CELL => #buf ( 32 , ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ARITHMETICCONTRACT_ID:Int ) ) @@ -718,7 +718,7 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -732,10 +732,10 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256): - ( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) + ( _OUTPUT_CELL:Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ARITHMETICCONTRACT_ID: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 0f4005130..b26bc102c 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 @@ -67,7 +67,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -84,7 +84,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -297,7 +297,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -326,7 +326,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -541,7 +541,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 andBool ( ORIGIN_ID:Int #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -793,7 +793,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -810,7 +810,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -1036,7 +1036,7 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 cad3904ce..65ed17e16 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 @@ -313,7 +313,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -330,7 +330,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -543,7 +543,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -572,7 +572,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -787,7 +787,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 andBool ( ORIGIN_ID:Int #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1039,7 +1039,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1056,7 +1056,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1282,7 +1282,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 c059452a2..0a01fc323 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 @@ -404,7 +404,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -421,7 +421,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -634,7 +634,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -663,7 +663,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -878,7 +878,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 andBool ( ORIGIN_ID:Int CALL 0 645326474426547203313410069153905908525362434349 0 128 4 128 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1133,7 +1133,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #return 128 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1379,7 +1379,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1540,10 +1540,10 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( false => true ) - ( _EXPECTEDREASON_CELL => b"" ) + ( _EXPECTEDREASON_CELL:Bytes => b"" ) - ( _EXPECTEDDEPTH_CELL => 0 ) + ( _EXPECTEDDEPTH_CELL:Int => 0 ) @@ -1629,7 +1629,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1880,7 +1880,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2225,7 +2225,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2571,7 +2571,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2917,7 +2917,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2934,7 +2934,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ListItem ( @@ -3266,7 +3266,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3618,7 +3618,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #checkRevert ~> #updateRevertOutput 128 0 ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3970,7 +3970,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ~> #updateRevertOutput 128 0 => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4314,7 +4314,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4562,7 +4562,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 e1d963a32..5b1b2aa09 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 @@ -310,7 +310,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -327,7 +327,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -540,7 +540,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -569,7 +569,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -784,7 +784,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 andBool ( ORIGIN_ID:Int #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1036,7 +1036,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1053,7 +1053,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -1279,7 +1279,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 60c34dd20..87272be20 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 @@ -70,7 +70,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -87,7 +87,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -300,7 +300,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -329,7 +329,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -544,7 +544,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 andBool ( ORIGIN_ID:Int #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -796,7 +796,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -813,7 +813,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1039,7 +1039,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 91b8973a1..840b6226b 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 @@ -376,7 +376,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -393,7 +393,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -606,7 +606,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -635,7 +635,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -654,7 +654,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x ) ) + ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x:Int ) ) 0 @@ -850,12 +850,12 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 andBool ( ORIGIN_ID:Int JUMPI 1124 bool2Word ( 100 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1108,7 +1108,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1352,7 +1352,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1595,7 +1595,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1612,7 +1612,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1841,7 +1841,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1858,7 +1858,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -2087,7 +2087,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2333,7 +2333,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 6b41bfd24..501b0437f 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 @@ -627,7 +627,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -644,7 +644,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -857,7 +857,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -886,7 +886,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -905,7 +905,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 @@ -1101,14 +1101,14 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 andBool ( ORIGIN_ID:Int JUMPI 1594 bool2Word ( KV1_y:Int <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1363,7 +1363,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1609,7 +1609,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ~> #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1854,7 +1854,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( #end EVMC_REVERT => #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1871,7 +1871,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -2102,7 +2102,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2119,7 +2119,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -2350,7 +2350,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 #halt ~> ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2598,7 +2598,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 4e7c3f7ae..280fa7784 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 @@ -317,7 +317,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 ( .K => STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -546,7 +546,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #return 128 0 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -798,7 +798,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #pc [ STATICCALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1047,7 +1047,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1077,7 +1077,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1282,7 +1282,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 - requires ( _KV0_a ==Int KV1_b:Int + requires ( _KV0_a:Int ==Int KV1_b:Int andBool ( 0 <=Int KV1_b:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -1295,7 +1295,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1529,7 +1529,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 - requires ( _KV0_a ==Int KV1_b:Int + requires ( _KV0_a:Int ==Int KV1_b:Int andBool ( 0 <=Int KV1_b:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -1542,7 +1542,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -323,7 +323,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #return 128 0 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -575,7 +575,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 128 0 ~> #pc [ STATICCALL ] => .K ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -823,7 +823,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1070,7 +1070,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 388 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1319,7 +1319,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1569,7 +1569,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1598,7 +1598,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1818,7 +1818,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2067,7 +2067,7 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 andBool ( KV1_b:Int STATICCALL 0 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -572,7 +572,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #return 128 0 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -824,7 +824,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 128 0 ~> #pc [ STATICCALL ] => .K ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1072,7 +1072,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int CALL 0 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1319,7 +1319,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #return 388 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1568,7 +1568,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1818,7 +1818,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1847,7 +1847,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -2067,7 +2067,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2316,7 +2316,7 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 andBool ( KV1_b:Int - ( .K => JUMPI 508 bool2Word ( ??WORD <=Int 0 ) + ( .K => JUMPI 508 bool2Word ( ??WORD:Int <=Int 0 ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -254,7 +254,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 - ( b"" => #buf ( 32 , ??WORD ) ) + ( b"" => #buf ( 32 , ??WORD:Int ) ) .List @@ -279,10 +279,10 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 0 - ( .WordStack => ( 0 : ( ??WORD : ( 220 : ( selector ( "setUp()" ) : .WordStack ) ) ) ) ) + ( .WordStack => ( 0 : ( ??WORD:Int : ( 220 : ( selector ( "setUp()" ) : .WordStack ) ) ) ) ) - ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ??WORD ) +Bytes b"\x00\x00\x00 " ) + ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xa0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ??WORD:Int ) +Bytes b"\x00\x00\x00 " ) 0 @@ -467,14 +467,14 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -501,7 +501,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -719,7 +719,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -748,7 +748,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -967,7 +967,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -996,7 +996,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1216,7 +1216,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1245,7 +1245,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #buf ( 32 , ?WORD:Int ) => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1466,7 +1466,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int 4 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1713,7 +1713,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1740,7 +1740,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -1958,7 +1958,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1985,7 +1985,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -2204,7 +2204,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2231,7 +2231,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -2451,7 +2451,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2478,7 +2478,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -2699,7 +2699,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 andBool ( ?WORD:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2726,7 +2726,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -2953,7 +2953,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2970,7 +2970,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -3198,7 +3198,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3215,7 +3215,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -3444,7 +3444,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3461,7 +3461,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List 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 cb918e8fe..1d41c4f6a 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 @@ -34,7 +34,7 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -265,7 +265,7 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 andBool ( TIMESTAMP_CELL:Int #cheatcode_return 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -393,7 +393,7 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 ( JUMPI 678 bool2Word ( pow64 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -410,7 +410,7 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -708,10 +708,10 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 rule [BASIC-BLOCK-1-TO-9]: - ( .K => JUMPI 678 bool2Word ( pow64 <=Int ?KV0_x ) + ( .K => JUMPI 678 bool2Word ( pow64 <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -744,13 +744,13 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\x0f\xee)\xd1" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\x0f\xee)\xd1" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 - ( .WordStack => ( bool2Word ( ?KV0_x ( bool2Word ( ?KV0_x:Int ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" ) @@ -1031,10 +1031,10 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - ensures ( 0 <=Int ?KV0_x - andBool ( 0 <=Int ?KV1_y - andBool ( ?KV0_x #cheatcode_return 128 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -389,7 +389,7 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 ( JUMPI 2519 bool2Word ( pow64 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -406,7 +406,7 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -702,10 +702,10 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 rule [BASIC-BLOCK-1-TO-9]: - ( .K => JUMPI 2519 bool2Word ( pow64 <=Int ?KV0_x ) + ( .K => JUMPI 2519 bool2Word ( pow64 <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -738,13 +738,13 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\xc0\xbd\x83$" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\xc0\xbd\x83$" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 - ( .WordStack => ( bool2Word ( ?KV0_x ( bool2Word ( ?KV0_x:Int ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" ) @@ -1025,10 +1025,10 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))) - ensures ( 0 <=Int ?KV0_x - andBool ( 0 <=Int ?KV1_y - andBool ( ?KV0_x ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -98,10 +98,10 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 - ( _OUTPUT_CELL => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + ( _OUTPUT_CELL:Bytes => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -266,7 +266,7 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -280,10 +280,10 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0 - ( _OUTPUT_CELL => #range ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes #buf ( 32 , C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Bytes #range ( C_CALLABLESTORAGECONTRACT_STR_S_CONTENTS:Bytes , 0 , ( ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Int -32 ) ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int -32 ) , chop ( ( ( chop ( ( ( ( notMaxUInt5 &Int ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) ) +Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int 224 ) ) -Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int -160 ) ) ) ) + ( _OUTPUT_CELL:Bytes => #range ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes #buf ( 32 , C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Bytes #range ( C_CALLABLESTORAGECONTRACT_STR_S_CONTENTS:Bytes , 0 , ( ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int ) +Int -32 ) ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" , ( ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) +Int -32 ) , chop ( ( ( chop ( ( ( ( notMaxUInt5 &Int ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) ) +Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int 224 ) ) -Int ( 32 *Int ( ( C_CALLABLESTORAGECONTRACT_STR_S_LENGTH:Int +Int maxUInt5 ) /Int 32 ) ) ) +Int -160 ) ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) 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 f919fac25..da90bd342 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 @@ -34,7 +34,7 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -305,13 +305,13 @@ module SUMMARY-TEST%CALLABLESTORAGETEST.TEST-STR():0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -49,7 +49,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.INIT:0 ( b"" => b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x00\xeaW`\x005`\xe0\x1c\x80c\x92\xdfO\xbd\x11a\x00\x8cW\x80c\xe0\x18\x0b\x0b\x11a\x00fW\x80c\xe0\x18\x0b\x0b\x14a\x01\x81W\x80c\xe2\f\x9fq\x14a\x01\x89W\x80c\xe9\x9bk1\x14a\x01\x81W\x80c\xfav&\xd4\x14a\x01\x91W`\x00\x80\xfd[\x80c\x92\xdfO\xbd\x14a\x01YW\x80c\xb5P\x8a\xa9\x14a\x01aW\x80c\xbaAO\xa6\x14a\x01iW`\x00\x80\xfd[\x80c?r\x86\xf4\x11a\x00\xc8W\x80c?r\x86\xf4\x14a\x01\x1fW\x80cf\xd9\xa9\xa0\x14a\x01'W\x80c\x85\"l\x81\x14a\x01^<#\x14a\x01\x17W[`\x00\x80\xfd[a\x00\xf7a\x01\x9eV[`@Qa\x01\x04\x91\x90a\fvV[`@Q\x80\x91\x03\x90\xf3[a\x01\x15a\x02\x00V[\x00[a\x00\xf7a\x04IV[a\x00\xf7a\x04\xa9V[a\x01/a\x05\tV[`@Qa\x01\x04\x91\x90a\f\xc3V[a\x01Da\x05\xf8V[`@Qa\x01\x04\x91\x90a\r\xa6V[a\x01/a\x06\xc8V[a\x01\x15a\x07\xaeV[a\x01Da\x07\xc3V[a\x01qa\x08\x93V[`@Q\x90\x15\x15\x81R` \x01a\x01\x04V[a\x01\x15a\t\xc0V[a\x00\xf7a\t\xd2V[`\x07Ta\x01q\x90`\xff\x16\x81V[```\x14\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90[\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8W[PPPPP\x90P\x90V[`\x1bT`\xff\x16a\x02\x12Wa\x02\x12a\x0e V[`\x00`@Qa\x02 \x90a\fiV[`@Q\x80\x91\x03\x90`\x00\xf0\x80\x15\x80\x15a\x02=`\x00\xfd[P`@Qc`\xfeG\xb1`\xe0\x1b\x81Ra\x158`\x04\x82\x01R\x90\x91P`\x01`\x01`\xa0\x1b\x03\x82\x16\x90c`\xfeG\xb1\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x02\x83W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02\x97W=`\x00\x80>=`\x00\xfd[PP`\x1bT`@Qc\x08\x01\xf1i`\xe1\x1b\x81R`\x03`\x04\x82\x01Ra\x01\x00\x90\x91\x04`\x01`\x01`\xa0\x1b\x03\x16\x92Pc\x10\x03\xe2\xd2\x91P`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x02\xe5W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x02\xf9W=`\x00\x80>=`\x00\xfd[PPPPa\x03\x7f`\x1b`\x01\x90T\x90a\x01\x00\n\x90\x04`\x01`\x01`\xa0\x1b\x03\x16`\x01`\x01`\xa0\x1b\x03\x16c\x06f\x1a\xbd`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x03SW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x03w\x91\x90a\x0e6V[a\x10\xe4a\n2V[`@Qc\x08\x01\xf1i`\xe1\x1b\x81R`\x05`\x04\x82\x01R`\x01`\x01`\xa0\x1b\x03\x82\x16\x90c\x10\x03\xe2\xd2\x90`$\x01`\x00`@Q\x80\x83\x03\x81`\x00\x87\x80;\x15\x80\x15a\x03\xc1W`\x00\x80\xfd[PZ\xf1\x15\x80\x15a\x03\xd5W=`\x00\x80>=`\x00\xfd[PPPPa\x04F\x81`\x01`\x01`\xa0\x1b\x03\x16c\x06f\x1a\xbd`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x04\x1aW=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x04>\x91\x90a\x0e6V[a\x15=a\n2V[PV[```\x16\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8WPPPPP\x90P\x90V[```\x15\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8WPPPPP\x90P\x90V[```\x19\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW`\x00\x84\x81R` \x90\x81\x90 `@\x80Q\x80\x82\x01\x82R`\x02\x86\x02\x90\x92\x01\x80T`\x01`\x01`\xa0\x1b\x03\x16\x83R`\x01\x81\x01\x80T\x83Q\x81\x87\x02\x81\x01\x87\x01\x90\x94R\x80\x84R\x93\x94\x91\x93\x85\x83\x01\x93\x92\x83\x01\x82\x82\x80\x15a\x05\xd7W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90`\x00\x90[\x82\x82\x90T\x90a\x01\x00\n\x90\x04`\xe0\x1b`\x01`\x01`\xe0\x1b\x03\x19\x16\x81R` \x01\x90`\x04\x01\x90` \x82`\x03\x01\x04\x92\x83\x01\x92`\x01\x03\x82\x02\x91P\x80\x84\x11a\x05\x99W\x90P[PPPPP\x81RPP\x81R` \x01\x90`\x01\x01\x90a\x05-V[PPPP\x90P\x90V[```\x18\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW\x83\x82\x90`\x00R` `\x00 \x01\x80Ta\x06;\x90a\x0eOV[\x80`\x1f\x01` \x80\x91\x04\x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80Ta\x06g\x90a\x0eOV[\x80\x15a\x06\xb4W\x80`\x1f\x10a\x06\x89Wa\x01\x00\x80\x83T\x04\x02\x83R\x91` \x01\x91a\x06\xb4V[\x82\x01\x91\x90`\x00R` `\x00 \x90[\x81T\x81R\x90`\x01\x01\x90` \x01\x80\x83\x11a\x06\x97W\x82\x90\x03`\x1f\x16\x82\x01\x91[PPPPP\x81R` \x01\x90`\x01\x01\x90a\x06\x1cV[```\x1a\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW`\x00\x84\x81R` \x90\x81\x90 `@\x80Q\x80\x82\x01\x82R`\x02\x86\x02\x90\x92\x01\x80T`\x01`\x01`\xa0\x1b\x03\x16\x83R`\x01\x81\x01\x80T\x83Q\x81\x87\x02\x81\x01\x87\x01\x90\x94R\x80\x84R\x93\x94\x91\x93\x85\x83\x01\x93\x92\x83\x01\x82\x82\x80\x15a\x07\x96W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90`\x00\x90[\x82\x82\x90T\x90a\x01\x00\n\x90\x04`\xe0\x1b`\x01`\x01`\xe0\x1b\x03\x19\x16\x81R` \x01\x90`\x04\x01\x90` \x82`\x03\x01\x04\x92\x83\x01\x92`\x01\x03\x82\x02\x91P\x80\x84\x11a\x07XW\x90P[PPPPP\x81RPP\x81R` \x01\x90`\x01\x01\x90a\x06\xecV[`\x1bT`\xff\x16\x15a\x07\xc1Wa\x07\xc1a\x0e V[V[```\x17\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01`\x00\x90[\x82\x82\x10\x15a\x05\xefW\x83\x82\x90`\x00R` `\x00 \x01\x80Ta\x08\x06\x90a\x0eOV[\x80`\x1f\x01` \x80\x91\x04\x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80Ta\x082\x90a\x0eOV[\x80\x15a\x08\x7fW\x80`\x1f\x10a\x08TWa\x01\x00\x80\x83T\x04\x02\x83R\x91` \x01\x91a\x08\x7fV[\x82\x01\x91\x90`\x00R` `\x00 \x90[\x81T\x81R\x90`\x01\x01\x90` \x01\x80\x83\x11a\x08bW\x82\x90\x03`\x1f\x16\x82\x01\x91[PPPPP\x81R` \x01\x90`\x01\x01\x90a\x07\xe7V[`\x07T`\x00\x90a\x01\x00\x90\x04`\xff\x16\x15a\x08\xb5WP`\x07Ta\x01\x00\x90\x04`\xff\x16\x90V[`\x00sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\t\xbbW`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x82\x84\x01R\x82Q\x80\x83\x03\x84\x01\x81R``\x83\x01\x90\x93R`\x00\x92\x90\x91a\tC\x91\x7ff\x7f\x9dp\xcaA\x1dp\xea\xd5\r\x8d\\\"\x07\r\xaf\xc3j\xd7_=\xcf^r7\xb2*\xde\x9a\xec\xc4\x91`\x80\x01a\x0e\x89V[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\t]\x91a\x0e\xbaV[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\t\x9aW`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\t\x9fV[``\x91P[P\x91PP\x80\x80` \x01\x90Q\x81\x01\x90a\t\xb7\x91\x90a\x0e\xd6V[\x91PP[\x91\x90PV[`\x1bT`\xff\x16a\x07\xc1Wa\x07\xc1a\x0e V[```\x13\x80T\x80` \x02` \x01`@Q\x90\x81\x01`@R\x80\x92\x91\x90\x81\x81R` \x01\x82\x80T\x80\x15a\x01\xf6W` \x02\x82\x01\x91\x90`\x00R` `\x00 \x90\x81T`\x01`\x01`\xa0\x1b\x03\x16\x81R`\x01\x90\x91\x01\x90` \x01\x80\x83\x11a\x01\xd8WPPPPP\x90P\x90V[\x80\x82\x14a\x0bYW\x7fA0O\xac\xd92=u\xb1\x1b\xcd\xd6\t\xcb8\xef\xff\xfd\xb0W\x10\xf7\xca\xf0\xe9\xb1lm\x9dp\x9fP`@Qa\n\xa3\x90` \x80\x82R`\"\x90\x82\x01R\x7fError: a == b not satisfied [uin`@\x82\x01Rat]`\xf0\x1b``\x82\x01R`\x80\x01\x90V[`@Q\x80\x91\x03\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x08\x08\x08\x08\x13\x19Y\x9d`\xb2\x1b``\x82\x01R` \x81\x01\x84\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1`@\x80Q\x81\x81R`\n\x81\x83\x01Ri\x08\x08\x08\x08\x08\x14\x9aY\xda\x1d`\xb2\x1b``\x82\x01R` \x81\x01\x83\x90R\x90Q\x7f\xb2\xde/\xbe\x80\x1a\r\xf6\xc0\xcb\xdd\xfdD\x8b\xa3\xc4\x1dH\xa0@\xca5\xc5l\x81\x96\xef\x0f\xca\xe7!\xa8\x91\x81\x90\x03`\x80\x01\x90\xa1a\x0bYa\x0b]V[PPV[sq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-;\x15a\fXW`@\x80Qsq\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-` \x82\x01\x81\x90Re\x19\x98Z[\x19Y`\xd2\x1b\x92\x82\x01\x92\x90\x92R`\x01``\x82\x01R`\x00\x91\x90\x7fp\xca\x10\xbb\xd0\xdb\xfd\x90 \xa9\xf4\xb14\x02\xc1l\xb1 p^\r\x1c\n\xea\xb1\x0f\xa3S\xaeXo\xc4\x90`\x80\x01`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\x0b\xf7\x92\x91` \x01a\x0e\x89V[`@\x80Q`\x1f\x19\x81\x84\x03\x01\x81R\x90\x82\x90Ra\f\x11\x91a\x0e\xbaV[`\x00`@Q\x80\x83\x03\x81`\x00\x86Z\xf1\x91PP=\x80`\x00\x81\x14a\fNW`@Q\x91P`\x1f\x19`?=\x01\x16\x82\x01`@R=\x82R=`\x00` \x84\x01>a\fSV[``\x91P[PPPP[`\x07\x80Ta\xff\x00\x19\x16a\x01\x00\x17\x90UV[a\x01\f\x80a\x0f\x00\x839\x01\x90V[` \x80\x82R\x82Q\x82\x82\x01\x81\x90R`\x00\x91\x90\x84\x82\x01\x90`@\x85\x01\x90\x84[\x81\x81\x10\x15a\f\xb7W\x83Q`\x01`\x01`\xa0\x1b\x03\x16\x83R\x92\x84\x01\x92\x91\x84\x01\x91`\x01\x01a\f\x92V[P\x90\x96\x95PPPPPPV[`\x00` \x80\x83\x01\x81\x84R\x80\x85Q\x80\x83R`@\x92P\x82\x86\x01\x91P\x82\x81`\x05\x1b\x87\x01\x01\x84\x88\x01`\x00\x80[\x84\x81\x10\x15a\rgW\x89\x84\x03`?\x19\x01\x86R\x82Q\x80Q`\x01`\x01`\xa0\x1b\x03\x16\x85R\x88\x01Q\x88\x85\x01\x88\x90R\x80Q\x88\x86\x01\x81\x90R\x90\x89\x01\x90\x83\x90``\x87\x01\x90[\x80\x83\x10\x15a\rRW\x83Q`\x01`\x01`\xe0\x1b\x03\x19\x16\x82R\x92\x8b\x01\x92`\x01\x92\x90\x92\x01\x91\x90\x8b\x01\x90a\r(V[P\x97\x8a\x01\x97\x95PPP\x91\x87\x01\x91`\x01\x01a\f\xebV[P\x91\x99\x98PPPPPPPPPV[`\x00[\x83\x81\x10\x15a\r\x91W\x81\x81\x01Q\x83\x82\x01R` \x01a\ryV[\x83\x81\x11\x15a\r\xa0W`\x00\x84\x84\x01R[PPPPV[`\x00` \x80\x83\x01\x81\x84R\x80\x85Q\x80\x83R`@\x86\x01\x91P`@\x81`\x05\x1b\x87\x01\x01\x92P\x83\x87\x01`\x00[\x82\x81\x10\x15a\x0e\x13W\x87\x85\x03`?\x19\x01\x84R\x81Q\x80Q\x80\x87Ra\r\xf4\x81\x89\x89\x01\x8a\x85\x01a\rvV[`\x1f\x01`\x1f\x19\x16\x95\x90\x95\x01\x86\x01\x94P\x92\x85\x01\x92\x90\x85\x01\x90`\x01\x01a\r\xcdV[P\x92\x97\x96PPPPPPPV[cNH{q`\xe0\x1b`\x00R`\x01`\x04R`$`\x00\xfd[`\x00` \x82\x84\x03\x12\x15a\x0eHW`\x00\x80\xfd[PQ\x91\x90PV[`\x01\x81\x81\x1c\x90\x82\x16\x80a\x0ecW`\x7f\x82\x16\x91P[` \x82\x10\x81\x03a\x0e\x83WcNH{q`\xe0\x1b`\x00R`\"`\x04R`$`\x00\xfd[P\x91\x90PV[`\x01`\x01`\xe0\x1b\x03\x19\x83\x16\x81R\x81Q`\x00\x90a\x0e\xac\x81`\x04\x85\x01` \x87\x01a\rvV[\x91\x90\x91\x01`\x04\x01\x93\x92PPPV[`\x00\x82Qa\x0e\xcc\x81\x84` \x87\x01a\rvV[\x91\x90\x91\x01\x92\x91PPV[`\x00` \x82\x84\x03\x12\x15a\x0e\xe8W`\x00\x80\xfd[\x81Q\x80\x15\x15\x81\x14a\x0e\xf8W`\x00\x80\xfd[\x93\x92PPPV\xfe`\x80`@R`\x05`\x00U`\xf5\x80a\x00\x17`\x009`\x00\xf3\xfe`\x80`@R`\x046\x10`0W`\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n\xa1dsolcC\x00\x08\r\x00\n" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -305,7 +305,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.INIT:0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List 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 eea594a44..c5f847603 100644 --- a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected +++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected @@ -34,7 +34,7 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List 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 dd61dfb39..457f40149 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 @@ -42,7 +42,7 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -56,10 +56,10 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) 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 f6de1631b..be30d1984 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 @@ -92,7 +92,7 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -106,10 +106,10 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_ENUM_ID:Int ) |Set SetItem ( C_ENUM_MEMBER_CONTRACT_ID:Int ) ) @@ -308,7 +308,7 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -322,10 +322,10 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) 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 3ef942a8f..f9d23f769 100644 --- a/src/tests/integration/test-data/show/Enum.init.cse.expected +++ b/src/tests/integration/test-data/show/Enum.init.cse.expected @@ -33,7 +33,7 @@ module SUMMARY-TEST%ENUM.INIT:0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -47,10 +47,10 @@ module SUMMARY-TEST%ENUM.INIT:0 - ( _OUTPUT_CELL => b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x006W`\x005`\xe0\x1c\x80cc6\xf6\x1e\x14a\x00;W\x80c\x84|7\xfb\x14a\x00EW[`\x00\x80\xfd[a\x00Ca\x00XV[\x00[a\x00Ca\x00S6`\x04a\x01\xd2V[a\x01~V[`\x00T`@\x80Qch\xaf7\xdf`\xe0\x1b\x81R\x90Q`\x05\x92`\x01`\x01`\xa0\x1b\x03\x16\x91ch\xaf7\xdf\x91`\x04\x80\x83\x01\x92` \x92\x91\x90\x82\x90\x03\x01\x81\x86Z\xfa\x15\x80\x15a\x00\xa2W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x00\xc6\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x00\xd7Wa\x00\xd7a\x02\x13V[\x11\x15a\x00\xe5Wa\x00\xe5a\x02)V[`\x00\x80`\x00\x90T\x90a\x01\x00\n\x90\x04`\x01`\x01`\xa0\x1b\x03\x16`\x01`\x01`\xa0\x1b\x03\x16ch\xaf7\xdf`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x019W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x01]\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x01nWa\x01na\x02\x13V[\x10\x15a\x01|Wa\x01|a\x02)V[V[`\x05\x81`\x05\x81\x11\x15a\x01\x92Wa\x01\x92a\x02\x13V[\x11\x15a\x01\xa0Wa\x01\xa0a\x02)V[`\x00\x81`\x05\x81\x11\x15a\x01\xb4Wa\x01\xb4a\x02\x13V[\x10\x15a\x01\xc2Wa\x01\xc2a\x02)V[PV[`\x06\x81\x10a\x01\xc2W`\x00\x80\xfd[`\x00` \x82\x84\x03\x12\x15a\x01\xe4W`\x00\x80\xfd[\x815a\x01\xef\x81a\x01\xc5V[\x93\x92PPPV[`\x00` \x82\x84\x03\x12\x15a\x02\x08W`\x00\x80\xfd[\x81Qa\x01\xef\x81a\x01\xc5V[cNH{q`\xe0\x1b`\x00R`!`\x04R`$`\x00\xfd[cNH{q`\xe0\x1b`\x00R`\x01`\x04R`$`\x00\xfd\xfe\xa1dsolcC\x00\x08\r\x00\n" ) + ( _OUTPUT_CELL:Bytes => b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\x046\x10a\x006W`\x005`\xe0\x1c\x80cc6\xf6\x1e\x14a\x00;W\x80c\x84|7\xfb\x14a\x00EW[`\x00\x80\xfd[a\x00Ca\x00XV[\x00[a\x00Ca\x00S6`\x04a\x01\xd2V[a\x01~V[`\x00T`@\x80Qch\xaf7\xdf`\xe0\x1b\x81R\x90Q`\x05\x92`\x01`\x01`\xa0\x1b\x03\x16\x91ch\xaf7\xdf\x91`\x04\x80\x83\x01\x92` \x92\x91\x90\x82\x90\x03\x01\x81\x86Z\xfa\x15\x80\x15a\x00\xa2W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x00\xc6\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x00\xd7Wa\x00\xd7a\x02\x13V[\x11\x15a\x00\xe5Wa\x00\xe5a\x02)V[`\x00\x80`\x00\x90T\x90a\x01\x00\n\x90\x04`\x01`\x01`\xa0\x1b\x03\x16`\x01`\x01`\xa0\x1b\x03\x16ch\xaf7\xdf`@Q\x81c\xff\xff\xff\xff\x16`\xe0\x1b\x81R`\x04\x01` `@Q\x80\x83\x03\x81\x86Z\xfa\x15\x80\x15a\x019W=`\x00\x80>=`\x00\xfd[PPPP`@Q=`\x1f\x19`\x1f\x82\x01\x16\x82\x01\x80`@RP\x81\x01\x90a\x01]\x91\x90a\x01\xf6V[`\x05\x81\x11\x15a\x01nWa\x01na\x02\x13V[\x10\x15a\x01|Wa\x01|a\x02)V[V[`\x05\x81`\x05\x81\x11\x15a\x01\x92Wa\x01\x92a\x02\x13V[\x11\x15a\x01\xa0Wa\x01\xa0a\x02)V[`\x00\x81`\x05\x81\x11\x15a\x01\xb4Wa\x01\xb4a\x02\x13V[\x10\x15a\x01\xc2Wa\x01\xc2a\x02)V[PV[`\x06\x81\x10a\x01\xc2W`\x00\x80\xfd[`\x00` \x82\x84\x03\x12\x15a\x01\xe4W`\x00\x80\xfd[\x815a\x01\xef\x81a\x01\xc5V[\x93\x92PPPV[`\x00` \x82\x84\x03\x12\x15a\x02\x08W`\x00\x80\xfd[\x81Qa\x01\xef\x81a\x01\xc5V[cNH{q`\xe0\x1b`\x00R`!`\x04R`$`\x00\xfd[cNH{q`\xe0\x1b`\x00R`\x01`\x04R`$`\x00\xfd\xfe\xa1dsolcC\x00\x08\r\x00\n" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) diff --git a/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected new file mode 100644 index 000000000..cc93e77bf --- /dev/null +++ b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected @@ -0,0 +1,1338 @@ + +┌─ 1 (root, init) +│ k: #execute ~> CONTINUATION:K +│ pc: 0 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/ForgetBranch.t.sol:8:21 +│ method: test%ForgetBranchTest.test_forgetBranch(uint256) +│ +│ (755 steps) +├─ 3 +│ k: #forget ( KV0_x:Int , 5 , 200 ) ~> #cheatcode_return 128 0 ~> #pc [ CALL ] ~> #e ... +│ pc: 1294 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/ForgetBranch.t.sol:14:14 +│ method: test%ForgetBranchTest.test_forgetBranch(uint256) +│ +│ (1 step) +├─ 4 +│ k: #cheatcode_return 128 0 ~> #pc [ CALL ] ~> #execute ~> CONTINUATION:K +│ pc: 1294 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/ForgetBranch.t.sol:14:14 +│ method: test%ForgetBranchTest.test_forgetBranch(uint256) +│ +│ (72 steps) +├─ 5 (split) +│ k: JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) ~> #pc [ JUMPI ] ~> #execute ~> CON ... +│ pc: 1322 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/ForgetBranch.t.sol:15:19 +│ method: test%ForgetBranchTest.test_forgetBranch(uint256) +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ KV0_x:Int <=Int 200 +┃ │ +┃ ├─ 6 +┃ │ k: JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) ~> #pc [ JUMPI ] ~> #execute ~> CON ... +┃ │ pc: 1322 +┃ │ callDepth: 0 +┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/ForgetBranch.t.sol:15:19 +┃ │ method: test%ForgetBranchTest.test_forgetBranch(uint256) +┃ │ +┃ │ (49 steps) +┃ ├─ 8 (terminal) +┃ │ k: #halt ~> CONTINUATION:K +┃ │ pc: 320 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: test/ForgetBranch.t.sol:10:20 +┃ │ method: test%ForgetBranchTest.test_forgetBranch(uint256) +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 2 (leaf, target, terminal) +┃ k: #halt ~> CONTINUATION:K +┃ pc: PC_CELL_5d410f2a:Int +┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int +┃ statusCode: STATUSCODE_FINAL:StatusCode +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ 200 #pc [ JUMPI ] ~> #execute ~> CON ... + │ pc: 1322 + │ callDepth: 0 + │ statusCode: STATUSCODE:StatusCode + │ src: test/ForgetBranch.t.sol:15:19 + │ method: test%ForgetBranchTest.test_forgetBranch(uint256) + │ + │ (40 steps) + ├─ 9 (terminal) + │ k: #halt ~> CONTINUATION:K + │ pc: 320 + │ callDepth: 0 + │ statusCode: EVMC_SUCCESS + │ src: test/ForgetBranch.t.sol:10:20 + │ method: test%ForgetBranchTest.test_forgetBranch(uint256) + │ + ┊ constraint: true + ┊ subst: ... + └─ 2 (leaf, target, terminal) + k: #halt ~> CONTINUATION:K + pc: PC_CELL_5d410f2a:Int + callDepth: CALLDEPTH_CELL_5d410f2a:Int + statusCode: STATUSCODE_FINAL:StatusCode + + + + +module SUMMARY-TEST%FORGETBRANCHTEST.TEST-FORGETBRANCH(UINT256):0 + + + rule [BASIC-BLOCK-1-TO-3]: + + + ( .K => #forget ( KV0_x:Int , 5 , 200 ) + ~> #cheatcode_return 128 0 + ~> #pc [ CALL ] ) + ~> #execute + ~> _CONTINUATION:K + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int ) + + + 0 + + + ( .WordStack => ( 228 : ( selector ( "forgetBranch(uint256,uint8,uint256)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) + + + ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" ) + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + + .Set + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int KV0_x:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( #forget ( KV0_x:Int , 5 , 200 ) ~> .K => .K ) + ~> #cheatcode_return 128 0 + ~> #pc [ CALL ] + ~> #execute + ~> _CONTINUATION:K + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int ) + + + 0 + + + ( 228 : ( selector ( "forgetBranch(uint256,uint8,uint256)" ) : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + + .Set + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int KV0_x:Int + andBool ( 200 + + + ( #cheatcode_return 128 0 + ~> #pc [ CALL ] => JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) + ~> #pc [ JUMPI ] ) + ~> #execute + ~> _CONTINUATION:K + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int ) + + + 0 + + + ( ( 228 => 0 ) : ( ( selector ( "forgetBranch(uint256,uint8,uint256)" ) => KV0_x:Int ) : ( ( 645326474426547203313410069153905908525362434349 => 319 ) : ( ( 0 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) => .WordStack ) ) ) ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + + .Set + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int KV0_x:Int + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) + ~> #pc [ JUMPI ] + ~> #execute => #halt ~> .K ) + ~> _CONTINUATION:K + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int ) + + + 0 + + + ( ( 0 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) => .WordStack ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + + .Set + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int KV0_x:Int + andBool ( KV0_x:Int <=Int 200 + andBool ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( JUMPI 1326 bool2Word ( KV0_x:Int <=Int 200 ) + ~> #pc [ JUMPI ] + ~> #execute => #halt ~> .K ) + ~> _CONTINUATION:K + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) + + + .List + + + .List + + + .Set + + + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"P#a\xd8" +Bytes #buf ( 32 , KV0_x:Int ) + + + 0 + + + ( ( 0 => selector ( "test_forgetBranch(uint256)" ) ) : ( ( KV0_x:Int : ( 319 : ( selector ( "test_forgetBranch(uint256)" ) : .WordStack ) ) ) => .WordStack ) ) + + + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00f\x949s" +Bytes #buf ( 32 , KV0_x:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" + + + 0 + + + 0 + + + false + + + 0 + + ... + + + + .List + + + 0 + + + SetItem ( 645326474426547203313410069153905908525362434349 ) + + + .Map + + + .Set + + ... + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + ) + + ... + + + ... + + + false + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int KV0_x:Int + andBool ( 200 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 - ( _OUTPUT_CELL => #buf ( 32 , KV0_x:Int ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , KV0_x:Int ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_IDENTITY_ID:Int ) ) @@ -267,7 +267,7 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -281,10 +281,10 @@ module SUMMARY-SRC%CSE%IDENTITY.APPLYOP(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) 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 b46893d41..e22911dcd 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 @@ -37,7 +37,7 @@ module SUMMARY-SRC%CSE%IDENTITY.IDENTITY(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,10 +51,10 @@ module SUMMARY-SRC%CSE%IDENTITY.IDENTITY(UINT256):0 - ( _OUTPUT_CELL => #buf ( 32 , KV0_x:Int ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , KV0_x:Int ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) 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 c510e14da..38800ad8e 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 @@ -82,7 +82,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -266,7 +266,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -280,10 +280,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.ADD(UINT256):0 - ( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) + ( _OUTPUT_CELL:Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) 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 f75a11a5a..5ff629d20 100644 --- a/src/tests/integration/test-data/show/ImportedContract.count().cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.count().cse.expected @@ -37,7 +37,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,10 +51,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.COUNT():0 - ( _OUTPUT_CELL => #buf ( 32 , #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , #lookup ( C_IMPORTEDCONTRACT_STORAGE:Map , 0 ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) 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 ed1f0e86c..33ba21ca1 100644 --- a/src/tests/integration/test-data/show/ImportedContract.init.cse.expected +++ b/src/tests/integration/test-data/show/ImportedContract.init.cse.expected @@ -35,7 +35,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -49,10 +49,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.INIT:0 - ( _OUTPUT_CELL => b"`\x80`@R`\x046\x10`0W`\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" ) + ( _OUTPUT_CELL:Bytes => b"`\x80`@R`\x046\x10`0W`\x005`\xe0\x1c\x80c\x06f\x1a\xbd\x14`5W\x80c\x10\x03\xe2\xd2\x14`[W\x80c`\xfeG\xb1\x14`lW[`\x00\x80\xfd[4\x80\x15`@W`\x00\x80\xfd[P`I`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`j`f6`\x04`\xabV[`\x87V[\x00[4\x80\x15`wW`\x00\x80\xfd[P`j`\x836`\x04`\xabV[`\x99V[\x80`\x00T`\x93\x91\x90`\xc3V[`\x00UPV[`\x03`\x00T\x10\x15`\xa6WPV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xbcW`\x00\x80\xfd[P5\x91\x90PV[`\x00\x82\x19\x82\x11\x15`\xe3WcNH{q`\xe0\x1b`\x00R`\x11`\x04R`$`\x00\xfd[P\x01\x90V\xfe\xa1dsolcC\x00\x08\r\x00\n" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) 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 a03695b29..b64266145 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 @@ -82,7 +82,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -96,10 +96,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) @@ -264,7 +264,7 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -278,10 +278,10 @@ module SUMMARY-TEST%IMPORTEDCONTRACT.SET(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) 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 3017ecff3..8acabefa5 100644 --- a/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected +++ b/src/tests/integration/test-data/show/InterfaceTagTest.testInterface().cse.expected @@ -34,7 +34,7 @@ module SUMMARY-TEST%INTERFACETAGTEST.TESTINTERFACE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,7 +51,7 @@ module SUMMARY-TEST%INTERFACETAGTEST.TESTINTERFACE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List diff --git a/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected b/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected index e5eb08823..5003ca484 100644 --- a/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected +++ b/src/tests/integration/test-data/show/RandomVarTest.test_custom_names().expected @@ -160,11 +160,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 rule [BASIC-BLOCK-1-TO-3]: - ( .K => #rename ( ??WORD , "BOOLEAN" ) + ( .K => #rename ( ??WORD:Int , "BOOLEAN" ) ~> #cheatcode_return 128 32 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -178,7 +178,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - ( b"" => #buf ( 32 , ??WORD ) ) + ( b"" => #buf ( 32 , ??WORD:Int ) ) .List @@ -391,14 +391,14 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( TIMESTAMP_CELL:Int #cheatcode_return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -423,7 +423,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?BOOLEAN ) ) + #buf ( 32 , ( ?WORD:Int => ?BOOLEAN:Int ) ) .List @@ -640,23 +640,23 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int - ( #cheatcode_return 128 32 ~> .K => #rename ( ??WORD , "BOOLEAN" ) + ( #cheatcode_return 128 32 ~> .K => #rename ( ??WORD:Int , "BOOLEAN" ) ~> #cheatcode_return 160 32 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -670,7 +670,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( BOOLEAN:Int => ??WORD ) ) + #buf ( 32 , ( BOOLEAN:Int => ??WORD:Int ) ) .List @@ -887,12 +887,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int #cheatcode_return 160 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -917,7 +917,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?BOOLEAN_0 ) ) + #buf ( 32 , ( ?WORD:Int => ?BOOLEAN_0:Int ) ) .List @@ -1136,12 +1136,12 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int #pc [ STATICCALL ] => .K ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1384,7 +1384,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int - ( .K => #rename ( ??WORD , "NEW_SLOT" ) + ( .K => #rename ( ??WORD:Int , "NEW_SLOT" ) ~> #cheatcode_return 256 32 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1414,7 +1414,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - ( b"" => #buf ( 32 , ??WORD ) ) + ( b"" => #buf ( 32 , ??WORD:Int ) ) .List @@ -1619,8 +1619,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #cheatcode_return 256 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1661,7 +1661,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?NEW_SLOT ) ) + #buf ( 32 , ( ?WORD:Int => ?NEW_SLOT:Int ) ) .List @@ -1866,8 +1866,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int ?WORD:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -1880,23 +1880,23 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ?WORD:Int - ( #cheatcode_return 256 32 ~> .K => #rename ( ??WORD , "NEW_ACCOUNT" ) + ( #cheatcode_return 256 32 ~> .K => #rename ( ??WORD:Int , "NEW_ACCOUNT" ) ~> #cheatcode_return 288 32 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1910,7 +1910,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( NEW_SLOT:Int => ??WORD ) ) + #buf ( 32 , ( NEW_SLOT:Int => ??WORD:Int ) ) .List @@ -2115,8 +2115,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -2129,14 +2129,14 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( NEW_SLOT:Int #cheatcode_return 288 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2161,7 +2161,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - #buf ( 32 , ( ?WORD:Int => ?NEW_ACCOUNT ) ) + #buf ( 32 , ( ?WORD:Int => ?NEW_ACCOUNT:Int ) ) .List @@ -2366,8 +2366,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int ?WORD:Int andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int @@ -2384,14 +2384,14 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ?WORD:Int =/=Int 728815563385977040452943777879061427756277306518 andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) - ensures ( 0 <=Int ?NEW_ACCOUNT - andBool ( ?NEW_ACCOUNT ( #cheatcode_return 288 32 - ~> #pc [ STATICCALL ] => #rename ( ??STORAGE , "NEW_ACCOUNT_STORAGE" ) + ~> #pc [ STATICCALL ] => #rename ( ??STORAGE:Map , "NEW_ACCOUNT_STORAGE" ) ~> #cheatcode_return 320 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2568,10 +2568,10 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 0 - ??STORAGE + ??STORAGE:Map - ??STORAGE + ??STORAGE:Map .Map @@ -2663,8 +2663,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -2681,7 +2681,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) @@ -2694,7 +2694,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ~> #cheatcode_return 320 0 ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2839,10 +2839,10 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 0 - ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE ) + ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE:Map ) - ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE ) + ( ?STORAGE:Map => ?NEW_ACCOUNT_STORAGE:Map ) .Map @@ -2934,8 +2934,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -2952,7 +2952,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) @@ -2962,11 +2962,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ( #cheatcode_return 320 0 - ~> #pc [ CALL ] => #rename ( ??BYTES , "NEW_BYTES" ) + ~> #pc [ CALL ] => #rename ( ??BYTES:Bytes , "NEW_BYTES" ) ~> #cheatcode_return 320 0 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2980,7 +2980,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes ??BYTES ) + ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes ??BYTES:Bytes ) .List @@ -3206,8 +3206,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -3224,11 +3224,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ))))))))))))))))))))) - ensures 32 ==Int lengthBytes ( ??BYTES ) + ensures 32 ==Int lengthBytes ( ??BYTES:Bytes ) [priority(20), label(BASIC-BLOCK-13-TO-14)] rule [BASIC-BLOCK-14-TO-15]: @@ -3238,7 +3238,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ~> #cheatcode_return 320 0 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3252,7 +3252,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes ( ?BYTES:Bytes => ?NEW_BYTES ) + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 " +Bytes ( ?BYTES:Bytes => ?NEW_BYTES:Bytes ) .List @@ -3478,8 +3478,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -3497,11 +3497,11 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))))))))))))) - ensures 32 ==Int lengthBytes ( ?NEW_BYTES ) + ensures 32 ==Int lengthBytes ( ?NEW_BYTES:Bytes ) [priority(20), label(BASIC-BLOCK-14-TO-15)] rule [BASIC-BLOCK-15-TO-16]: @@ -3511,7 +3511,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ~> #pc [ STATICCALL ] => POP 1 ~> #pc [ POP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3751,8 +3751,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -3770,7 +3770,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))))))))))))) @@ -3782,7 +3782,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 ( POP 1 ~> #pc [ POP ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3799,7 +3799,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -4025,8 +4025,8 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 - requires ( _BOOLEAN ==Int 1 - andBool ( _BOOLEAN_0 ==Int 0 + requires ( _BOOLEAN:Int ==Int 1 + andBool ( _BOOLEAN_0:Int ==Int 0 andBool ( 0 <=Int NEW_SLOT:Int andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int @@ -4044,7 +4044,7 @@ module SUMMARY-TEST%RANDOMVARTEST.TEST-CUSTOM-NAMES():0 andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( NEW_ACCOUNT:Int =/=Int 728815563385977040452943777879061427756277306518 - andBool ( _C_RANDOMVARTEST_ID =/=Int 645326474426547203313410069153905908525362434349 + andBool ( _C_RANDOMVARTEST_ID:Int =/=Int 645326474426547203313410069153905908525362434349 andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) )))))))))))))))))))))) 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 74e0c344d..31410769a 100644 --- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected +++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected @@ -70,7 +70,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -87,7 +87,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -341,7 +341,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -370,7 +370,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -606,7 +606,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 andBool ( ORIGIN_ID:Int #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -879,7 +879,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -896,7 +896,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -1143,7 +1143,7 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 ea7f161c6..74936941a 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 @@ -37,7 +37,7 @@ module SUMMARY-TEST%STATICCALLCONTRACT.SET(UINT256):0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -51,10 +51,10 @@ module SUMMARY-TEST%STATICCALLCONTRACT.SET(UINT256):0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) 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 a869046be..ebc024faa 100644 --- a/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected +++ b/src/tests/integration/test-data/show/TGovernance.getEscrowTokenTotalSupply().cse.expected @@ -149,7 +149,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -163,10 +163,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) @@ -393,7 +393,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -407,10 +407,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 - ( _OUTPUT_CELL => #buf ( 32 , ( #asWord ( #range ( #buf ( 32 , #lookup ( C_TGOVERNANCE_ESCROW_TOKEN_STORAGE:Map , 0 ) ) , 16 , 16 ) ) +Int 45 ) ) ) + ( _OUTPUT_CELL:Bytes => #buf ( 32 , ( #asWord ( #range ( #buf ( 32 , #lookup ( C_TGOVERNANCE_ESCROW_TOKEN_STORAGE:Map , 0 ) ) , 16 , 16 ) ) +Int 45 ) ) ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_TGOVERNANCE_ID:Int ) |Set SetItem ( C_TGOVERNANCE_ESCROW_ID:Int ) |Set SetItem ( C_TGOVERNANCE_ESCROW_TOKEN_ID:Int ) ) @@ -644,7 +644,7 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -658,10 +658,10 @@ module SUMMARY-TEST%TGOVERNANCE.GETESCROWTOKENTOTALSUPPLY():0 - ( _OUTPUT_CELL => b"" ) + ( _OUTPUT_CELL:Bytes => b"" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) ( TOUCHEDACCOUNTS_CELL:Set => TOUCHEDACCOUNTS_CELL:Set |Set SetItem ( C_TGOVERNANCE_ID:Int ) |Set SetItem ( C_TGOVERNANCE_ESCROW_ID:Int ) ) diff --git a/src/tests/integration/test-data/show/gas-abstraction.expected b/src/tests/integration/test-data/show/gas-abstraction.expected index 1822c744d..82e14cbe8 100644 --- a/src/tests/integration/test-data/show/gas-abstraction.expected +++ b/src/tests/integration/test-data/show/gas-abstraction.expected @@ -421,7 +421,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 ( .K => #end EVMC_REVERT ~> #pc [ REVERT ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -642,7 +642,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 andBool ( TIMESTAMP_CELL:Int #halt ) ~> #pc [ REVERT ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -673,7 +673,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -882,7 +882,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 andBool ( ORIGIN_ID:Int ( #pc [ REVERT ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1120,7 +1120,7 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 andBool ( ORIGIN_ID:Int JUMPI 1478 bool2Word ( KV0_n:Int <=Int 0 ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1191,7 +1191,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( TIMESTAMP_CELL:Int 1 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1438,7 +1438,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( KV0_n:Int 2 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1683,7 +1683,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( KV0_n:Int 3 ) ) ~> #pc [ JUMPI ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1929,7 +1929,7 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 andBool ( KV0_n:Int #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL 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 131248867..95193f315 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 @@ -282,7 +282,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -299,7 +299,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -446,10 +446,10 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 false - ( _EXPECTEDREASON_CELL => b"" ) + ( _EXPECTEDREASON_CELL:Bytes => b"" ) - ( _EXPECTEDDEPTH_CELL => 0 ) + ( _EXPECTEDDEPTH_CELL:Int => 0 ) @@ -517,7 +517,7 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 andBool ( TIMESTAMP_CELL:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -293,7 +293,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -506,7 +506,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 andBool ( TIMESTAMP_CELL:Int - ( .K => JUMPI 1124 bool2Word ( 100 <=Int ?KV0_x ) + ( .K => JUMPI 1124 bool2Word ( 100 <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -359,13 +359,13 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x ) ) + ( b"\n\x92T\xe4" => b"F\"\xb1U" +Bytes #buf ( 32 , ?KV0_x:Int ) ) 0 - ( .WordStack => ( ?KV0_x : ( 327 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) + ( .WordStack => ( ?KV0_x:Int : ( 327 : ( selector ( "test_failing_branch(uint256)" ) : .WordStack ) ) ) ) ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" ) @@ -553,14 +553,14 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -587,7 +587,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -816,7 +816,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( JUMPI 1124 bool2Word ( 100 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -833,7 +833,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List 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 d76f77f4e..3725f3ba5 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 @@ -574,10 +574,10 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 rule [BASIC-BLOCK-1-TO-8]: - ( .K => JUMPI 1594 bool2Word ( ?KV1_y <=Int ?KV0_x ) + ( .K => JUMPI 1594 bool2Word ( ?KV1_y:Int <=Int ?KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -610,13 +610,13 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) ) + ( b"\n\x92T\xe4" => b"\x8c\x0e\xdd\x8b" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) ) 0 - ( .WordStack => ( ?KV1_y : ( ?KV0_x : ( 327 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) + ( .WordStack => ( ?KV1_y:Int : ( ?KV0_x:Int : ( 327 : ( selector ( "test_revert_branch(uint256,uint256)" ) : .WordStack ) ) ) ) ) ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" ) @@ -804,16 +804,16 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -840,7 +840,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) - ( _STATUSCODE => EVMC_REVERT ) + ( _STATUSCODE:StatusCode => EVMC_REVERT ) .List @@ -1071,7 +1071,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 ( JUMPI 1594 bool2Word ( KV1_y:Int <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1088,7 +1088,7 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List diff --git a/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected b/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected index 07e47add6..2dc187d85 100644 --- a/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected +++ b/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected @@ -116,13 +116,13 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 rule [BASIC-BLOCK-1-TO-17]: - ( .K => JUMPI 99 bool2Word ( ?KV2_z ==Int 0 ) + ( .K => JUMPI 99 bool2Word ( ?KV2_z:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ~> #return 128 32 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -147,16 +147,16 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 CALLER_ID:Int - b"\x15T\xa2\xa4" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + b"\x15T\xa2\xa4" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 - ( 228 : ( selector ( "applyOp(uint256,uint256,bool)" ) : ( 491460923342184218035706888008750043977755113263 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 193 : ( selector ( "test_branch_merge(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) ) + ( 228 : ( selector ( "applyOp(uint256,uint256,bool)" ) : ( 491460923342184218035706888008750043977755113263 : ( ?KV2_z:Int : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 193 : ( selector ( "test_branch_merge(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) ) - b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) 0 @@ -270,13 +270,13 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 ( CALLER_ID:Int => 728815563385977040452943777879061427756277306518 ) - ( b"\n\x92T\xe4" => b"\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) ) + ( b"\n\x92T\xe4" => b"\xe0~\\\x97" +Bytes #buf ( 32 , ?KV0_x:Int ) +Bytes #buf ( 32 , ?KV1_y:Int ) +Bytes #buf ( 32 , ?KV2_z:Int ) ) 0 - ( .WordStack => ( 0 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 60 : ( selector ( "applyOp(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) + ( .WordStack => ( 0 : ( ?KV2_z:Int : ( ?KV1_y:Int : ( ?KV0_x:Int : ( 60 : ( selector ( "applyOp(uint256,uint256,bool)" ) : .WordStack ) ) ) ) ) ) ) ( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" ) @@ -507,19 +507,19 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 andBool ( TIMESTAMP_CELL:Int #return 128 32 ~> #pc [ CALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -549,7 +549,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -924,7 +924,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 ~> #return 128 32 ~> #pc [ CALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -941,7 +941,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( @@ -1317,7 +1317,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 ~> #return 128 32 ~> #pc [ CALL ] ~> #execute => #halt ~> .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1334,7 +1334,7 @@ module SUMMARY-TEST%MERGEKCFGTEST.TEST-BRANCH-MERGE(UINT256,UINT256,BOOL):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ( ListItem ( diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected index 5e67920d3..af5c290bc 100644 --- a/src/tests/integration/test-data/show/node-refutation.expected +++ b/src/tests/integration/test-data/show/node-refutation.expected @@ -88,7 +88,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 ( .K => JUMPI 535 bool2Word ( 10 <=Int KV0_x:Int ) ~> #pc [ JUMPI ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -316,7 +316,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( TIMESTAMP_CELL:Int #pc [ JUMPI ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -564,7 +564,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( KV0_x:Int #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -593,7 +593,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -811,7 +811,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( KV0_x:Int ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1058,7 +1058,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 andBool ( KV0_x:Int ( #execute => #halt ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -677,7 +677,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) .List @@ -931,7 +931,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 andBool ( TIMESTAMP_CELL:Int ( #halt => #execute ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -960,7 +960,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"" - ( EVMC_SUCCESS => ?_STATUSCODE ) + ( EVMC_SUCCESS => ?_STATUSCODE:StatusCode ) .List @@ -979,7 +979,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 CALLER_ID:Int - ( b"\n\x92T\xe4" => b"h\xc6\xc8\x93" +Bytes #buf ( 32 , ?KV0_addr ) ) + ( b"\n\x92T\xe4" => b"h\xc6\xc8\x93" +Bytes #buf ( 32 , ?KV0_addr:Int ) ) 0 @@ -1196,12 +1196,12 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 andBool ( ORIGIN_ID:Int CALL 0 645326474426547203313410069153905908525362434349 0 128 36 128 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1477,7 +1477,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -1745,7 +1745,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #cheatcode_return 128 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2014,7 +2014,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #pc [ CALL ] => STATICCALL 0 491460923342184218035706888008750043977755113263 128 4 128 32 ~> #pc [ STATICCALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2184,22 +2184,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _NEWCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -2268,7 +2268,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2467,22 +2467,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => 645326474426547203313410069153905908525362434349 ) + ( _NEWCALLER_CELL:Account => 645326474426547203313410069153905908525362434349 ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -2551,7 +2551,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -2750,22 +2750,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => 491460923342184218035706888008750043977755113263 ) + ( _NEWCALLER_CELL:Account => 491460923342184218035706888008750043977755113263 ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -2834,7 +2834,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3075,22 +3075,22 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - ( _PREVCALLER_CELL => 728815563385977040452943777879061427756277306518 ) + ( _PREVCALLER_CELL:Account => 728815563385977040452943777879061427756277306518 ) - ( _PREVORIGIN_CELL => ORIGIN_ID:Int ) + ( _PREVORIGIN_CELL:Account => ORIGIN_ID:Int ) - ( _NEWCALLER_CELL => KV0_addr:Int ) + ( _NEWCALLER_CELL:Account => KV0_addr:Int ) - ( _NEWORIGIN_CELL => .Account ) + ( _NEWORIGIN_CELL:Account => .Account ) ( false => true ) - ( _DEPTH_CELL => 0 ) + ( _DEPTH_CELL:Int => 0 ) false @@ -3191,7 +3191,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3445,7 +3445,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -3728,7 +3728,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4011,7 +4011,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4348,7 +4348,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -4719,7 +4719,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -5120,7 +5120,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -5521,7 +5521,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -5995,7 +5995,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -6366,7 +6366,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -6765,7 +6765,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -7164,7 +7164,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -7637,7 +7637,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -8008,7 +8008,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -8408,7 +8408,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -8808,7 +8808,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -9282,7 +9282,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -9299,7 +9299,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xa98[\xe1\x02\xac>\xac)t\x83\xddb3\xd6+>\x14\x96" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -9656,7 +9656,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -9702,7 +9702,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -10059,7 +10059,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -10105,7 +10105,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00V\x15\xde\xb7\x98\xbb>M\xfa\x019\xdf\xa1\xb3\xd43\xcc#\xb7/" - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -10462,7 +10462,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -10508,7 +10508,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 #buf ( 32 , KV0_addr:Int ) - ( _STATUSCODE => EVMC_SUCCESS ) + ( _STATUSCODE:StatusCode => EVMC_SUCCESS ) ListItem ( @@ -10939,7 +10939,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 128 32 ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -11313,7 +11313,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -11716,7 +11716,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -12119,7 +12119,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -12599,7 +12599,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #setLocalMem 128 32 b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xa98[\xe1\x02\xac>\xac)t\x83\xddb3\xd6+>\x14\x96" ) ~> #pc [ STATICCALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -12973,7 +12973,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -13379,7 +13379,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -13785,7 +13785,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ STATICCALL ] ~> #endPrank ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -14268,7 +14268,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #pc [ STATICCALL ] => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -14642,7 +14642,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #endPrank => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -15048,7 +15048,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #endPrank => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -15454,7 +15454,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #endPrank => CALL 0 645326474426547203313410069153905908525362434349 0 160 4 160 0 ~> #pc [ CALL ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -15934,7 +15934,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -16191,7 +16191,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -16476,7 +16476,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -16761,7 +16761,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #return 160 0 ) ~> #pc [ CALL ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17100,7 +17100,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ~> #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17357,7 +17357,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17643,7 +17643,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -17929,7 +17929,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #pc [ CALL ] => #end EVMC_SUCCESS ~> #pc [ STOP ] ) ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -18265,7 +18265,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 ( #end EVMC_SUCCESS => #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -18522,7 +18522,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -18804,7 +18804,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19086,7 +19086,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 #halt ) ~> #pc [ STOP ] ~> #execute - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19418,7 +19418,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 #halt ~> ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19675,7 +19675,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 728815563385977040452943777879061427756277306518 + requires ( _KV0_addr:Int ==Int 728815563385977040452943777879061427756277306518 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -19957,7 +19957,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 645326474426547203313410069153905908525362434349 + requires ( _KV0_addr:Int ==Int 645326474426547203313410069153905908525362434349 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL @@ -20239,7 +20239,7 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 - requires ( _KV0_addr ==Int 491460923342184218035706888008750043977755113263 + requires ( _KV0_addr:Int ==Int 491460923342184218035706888008750043977755113263 andBool ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( pow24 ( #pc [ STOP ] ~> #execute => .K ) - ~> _CONTINUATION + ~> _CONTINUATION:K NORMAL diff --git a/src/tests/integration/test-data/src/ForgetBranch.t.sol b/src/tests/integration/test-data/src/ForgetBranch.t.sol new file mode 100644 index 000000000..fe4064aa8 --- /dev/null +++ b/src/tests/integration/test-data/src/ForgetBranch.t.sol @@ -0,0 +1,21 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity >=0.8.13; + +import {Test, console} from "forge-std/Test.sol"; +import "kontrol-cheatcodes/KontrolCheats.sol"; + + +contract ForgetBranchTest is Test, KontrolCheats { + + function test_forgetBranch(uint256 x) public { + uint256 y; + + vm.assume(x > 200); + kevm.forgetBranch(x, KontrolCheatsBase.ComparisonOperator.GreaterThan, 200); + if(x > 200){ + y = 21; + } else { + y = 42; + } + } +} \ No newline at end of file