From e925c83ac355abe0f20bca81186bc81a292b957d Mon Sep 17 00:00:00 2001 From: ACassimiro Date: Fri, 24 Jan 2025 14:38:49 -0300 Subject: [PATCH] Update to match master branch (#945) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Implement kevm.forgetBranch cheatcode (#899) * draft FOUNDRYSemantics * forgetBranch * add mlEqualsTrue * minor corrections * add simplification step * formatting * add back not equal * rename FOUNDRYSemantics to KontrolSemantics * checking for negation as well * correcting indentation * expanding functionality * heuristic simplifications * further refinement * refactoring _exec_forget_custom_step * add show test * fix test * update expected output --------- Co-authored-by: Petar Maksimovic Co-authored-by: Palina Co-authored-by: Petar Maksimović * Update dependency: deps/kevm_release (#940) * deps/kevm_release: Set Version 1.0.780 * Sync Poetry files: kevm-pyk version 1.0.780 * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: devops * Build Custom Kontrol Versions using a workflow (#941) * new file: .github/workflows/kup-build-kontrol.yml - Adding a new feature to build kontrol images using kup and --overrides * Update .github/workflows/kup-build-kontrol.yml Co-authored-by: Everett Hildenbrandt * modified: .github/workflows/docker-push.yml modified: .github/workflows/kup-build-kontrol.yml - Standardizing the naming between these two workflows to know which is for which - Docker-push builds a custom version of kontrol with fixed dependencies already published and built with kontrol - kup-build-kontrol.yml will build the existing kontrol code with a single new dependency modified: README.md - Adding some readme instructions. * renamed: .github/workflows/docker-push.yml -> .github/workflows/kontrol-push-fixed-deps.yml renamed: .github/workflows/kup-build-kontrol.yml -> .github/workflows/kontrol-push-unfixed-deps.yml modified: README.md - Add some background between the two kontrol build workflows * modified: README.md -- Adding content to explain the two custom kontrol build workflows * Update README.md Co-authored-by: Anton Savienko * Filling in the 'get' placeholder with functionality to fetch appropriate defaults when nothing is provided * modified: README.md - Adding instructions to fetch hash and use the wrofklow with multiple dep options now available * Update spelling and gramar * modified: .github/workflows/kontrol-push-unfixed-deps.yml - Fixing reporting of final versions used to build kontrol. - Removing dfining override for undefined inputs to the workflow --------- Co-authored-by: Everett Hildenbrandt Co-authored-by: Anton Savienko --------- Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: Petar Maksimovic Co-authored-by: Palina Co-authored-by: Petar Maksimović Co-authored-by: rv-jenkins Co-authored-by: devops Co-authored-by: Freeman <105403280+F-WRunTime@users.noreply.github.com> Co-authored-by: Everett Hildenbrandt Co-authored-by: Anton Savienko --- ...r-push.yml => kontrol-push-fixed-deps.yml} | 4 +- .../workflows/kontrol-push-unfixed-deps.yml | 65 + README.md | 77 +- deps/kevm_release | 2 +- flake.lock | 8 +- flake.nix | 2 +- poetry.lock | 8 +- pyproject.toml | 2 +- src/kontrol/foundry.py | 143 +- src/kontrol/kdist/cheatcodes.md | 21 + src/kontrol/kdist/foundry.md | 4 + .../test-data/end-to-end-prove-all | 29 +- .../test-data/end-to-end-prove-show | 1 + .../test-data/end-to-end-prove-skip | 34 +- ...chTest.test_forgetBranch(uint256).expected | 1338 +++++++++++++++++ .../test-data/src/ForgetBranch.t.sol | 21 + 16 files changed, 1709 insertions(+), 50 deletions(-) rename .github/workflows/{docker-push.yml => kontrol-push-fixed-deps.yml} (95%) create mode 100644 .github/workflows/kontrol-push-unfixed-deps.yml create mode 100644 src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected create mode 100644 src/tests/integration/test-data/src/ForgetBranch.t.sol 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..8f62f301c --- /dev/null +++ b/.github/workflows/kontrol-push-unfixed-deps.yml @@ -0,0 +1,65 @@ +--- +name: 'Push Kontrol w/ Dependencies' +on: + workflow_dispatch: + inputs: + kevm-version: + description: 'Branch/Tag to use for KEVM' + required: false + default: '' + k-version: + description: 'Branch/Tag to use for K' + required: false + default: '' + llvm-version: + description: 'Branch/Tag to use for LLVM Backend' + required: false + default: '' + haskell-version: + description: 'Branch/Tag to use for Haskell Backend' + required: false + default: '' + +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 --rm -it --detach --name kontrol-build-with-kup-${{ github.run_id }} ghcr.io/runtimeverification/kup:latest + 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 ${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/kevm_release b/deps/kevm_release index 3a8abe45d..efbcd8ea6 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.779 +1.0.780 diff --git a/flake.lock b/flake.lock index bf742f54e..531e74096 100644 --- a/flake.lock +++ b/flake.lock @@ -435,16 +435,16 @@ ] }, "locked": { - "lastModified": 1737531698, - "narHash": "sha256-l3p1qZtmCYGUsuL9aXVSBk5B2BKBk7lafK+ONjedAZ8=", + "lastModified": 1737638869, + "narHash": "sha256-FMy3opWscIAYlq3KnoLiB4mLnLAPnhHwKphHkSDF7jk=", "owner": "runtimeverification", "repo": "evm-semantics", - "rev": "69256070065dad12ce46dedfbf1d45b3084d335d", + "rev": "8868e817eba64fa6615a73f14e33b5845193c94a", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v1.0.779", + "ref": "v1.0.780", "repo": "evm-semantics", "type": "github" } diff --git a/flake.nix b/flake.nix index a17fea0c4..e809697d7 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.780"; 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..2e5533fef 100644 --- a/poetry.lock +++ b/poetry.lock @@ -734,7 +734,7 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kevm-pyk" -version = "1.0.779" +version = "1.0.780" description = "" optional = false python-versions = "^3.10" @@ -750,8 +750,8 @@ 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.780" +resolved_reference = "8868e817eba64fa6615a73f14e33b5845193c94a" subdirectory = "kevm-pyk" [[package]] @@ -1599,4 +1599,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.1" python-versions = "^3.10" -content-hash = "ff49535579af0b71ea04f78292bc68341370ce55d5fcdd2e1f501ff7f6067739" +content-hash = "f9da75ffbfc5e3c99ca0d51f7b7d05a936394f9483071c1ea6071bf74595913d" diff --git a/pyproject.toml b/pyproject.toml index c877e0b4c..bc1e3d3aa 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.780", 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 8bdbd9c5f..cc38d73e4 100644 --- a/src/kontrol/kdist/foundry.md +++ b/src/kontrol/kdist/foundry.md @@ -80,6 +80,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/ForgetBranchTest.test_forgetBranch(uint256).expected b/src/tests/integration/test-data/show/ForgetBranchTest.test_forgetBranch(uint256).expected new file mode 100644 index 000000000..aec40fd4a --- /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 + + + 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 + + + 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 + + + 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 + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + ( _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 + + + NORMAL + + + CANCUN + + + false + + + + + b"" + + + ( _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 =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