From 0493bd4ad12a29499ca0e1ef553e7c20e522d9af Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Wed, 13 Nov 2024 11:27:55 +0800 Subject: [PATCH] `merge_node` Support (#829) * update copytree * introduce solidity code * add some comments * comment * replace copy_tree by copytree for py3.12 * fix * dirs_exist_ok=True * delete test * fix copytree * provide `merge` option for `minimize_proof` * provide `Branches` contract for merging node testing * add a test for merging node * add arguments to the parser * test configuration for merging node * make format/check * submit the expected * fix for kompile * fix kompile * fix `cse tests` * fix * fix * add endmodule * fix constracts.k.expected * fix * fix * Update help message for node merging Co-authored-by: JianHong Zhao --------- Co-authored-by: Palina --- src/kontrol/cli.py | 9 +- src/kontrol/foundry.py | 2 +- src/kontrol/options.py | 7 + src/tests/integration/conftest.py | 6 +- .../integration/test-data/foundry-minimize | 1 + .../test-data/foundry-minimize-merge | 1 + .../test-data/foundry/src/Branches.sol | 14 + .../foundry/test/MergeKCFGTest.t.sol | 29 + .../test-data/show/contracts.k.expected | 134 ++ .../test-data/show/foundry.k.expected | 16 + ...ranch_merge(uint256,uint256,bool).expected | 1690 +++++++++++++++++ src/tests/integration/test_foundry_prove.py | 5 +- src/tests/integration/test_kontrol.py | 6 +- src/tests/utils.py | 4 +- 14 files changed, 1913 insertions(+), 11 deletions(-) create mode 100644 src/tests/integration/test-data/foundry-minimize-merge create mode 100644 src/tests/integration/test-data/foundry/src/Branches.sol create mode 100644 src/tests/integration/test-data/foundry/test/MergeKCFGTest.t.sol create mode 100644 src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 35ed357a6..83a838621 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -692,7 +692,7 @@ def parse(s: str) -> list[T]: help='Print elements in hexadecimal encoding.', ) - command_parser.add_parser( + minimize_proof_args = command_parser.add_parser( 'minimize-proof', help='Minimize the KCFG of the proof for a given test.', parents=[ @@ -702,6 +702,13 @@ def parse(s: str) -> list[T]: config_args.config_args, ], ) + minimize_proof_args.add_argument( + '--merge', + dest='merge', + default=None, + action='store_true', + help='Merge the nodes of the KCFG into a successful branch and a revert branch.', + ) remove_node = command_parser.add_parser( 'remove-node', diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 3a765e061..12ecd5b12 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -1034,7 +1034,7 @@ def foundry_to_xml(foundry: Foundry, proofs: list[APRProof]) -> None: def foundry_minimize_proof(foundry: Foundry, options: MinimizeProofOptions) -> None: test_id = foundry.get_test_id(options.test, options.version) apr_proof = foundry.get_apr_proof(test_id) - apr_proof.minimize_kcfg() + apr_proof.minimize_kcfg(merge=options.merge) apr_proof.write_proof_data() diff --git a/src/kontrol/options.py b/src/kontrol/options.py index f6292ebf8..de3550c98 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -328,6 +328,13 @@ def get_argument_type() -> dict[str, Callable]: class MinimizeProofOptions(FoundryTestOptions, LoggingOptions, FoundryOptions): + merge: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'merge': False, + } @staticmethod def from_option_string() -> dict[str, str]: diff --git a/src/tests/integration/conftest.py b/src/tests/integration/conftest.py index fb1d63cee..060ef94c9 100644 --- a/src/tests/integration/conftest.py +++ b/src/tests/integration/conftest.py @@ -1,7 +1,7 @@ from __future__ import annotations -from distutils.dir_util import copy_tree from functools import partial +from shutil import copytree from typing import TYPE_CHECKING import pytest @@ -64,7 +64,7 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo foundry_root = root_tmp_dir / 'foundry' with FileLock(str(foundry_root) + '.lock'): if not foundry_root.is_dir(): - copy_tree(str(TEST_DATA_DIR / 'foundry'), str(foundry_root)) + copytree(str(TEST_DATA_DIR / 'foundry'), str(foundry_root), dirs_exist_ok=True) run_process_2(['forge', 'install', '--no-git', f'foundry-rs/forge-std@{FORGE_STD_REF}'], cwd=foundry_root) run_process_2( @@ -98,5 +98,5 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo ) session_foundry_root = tmp_path_factory.mktemp('foundry') - copy_tree(str(foundry_root), str(session_foundry_root)) + copytree(str(foundry_root), str(session_foundry_root), dirs_exist_ok=True) return Foundry(session_foundry_root, add_enum_constraints=True) diff --git a/src/tests/integration/test-data/foundry-minimize b/src/tests/integration/test-data/foundry-minimize index 35bf28fdc..d143d73f2 100644 --- a/src/tests/integration/test-data/foundry-minimize +++ b/src/tests/integration/test-data/foundry-minimize @@ -2,3 +2,4 @@ AssertTest.test_assert_false() AssertTest.testFail_expect_revert() AssertTest.test_failing_branch(uint256) AssertTest.test_revert_branch(uint256,uint256) +MergeKCFGTest.test_branch_merge(uint256,uint256,bool) diff --git a/src/tests/integration/test-data/foundry-minimize-merge b/src/tests/integration/test-data/foundry-minimize-merge new file mode 100644 index 000000000..4133bc2b5 --- /dev/null +++ b/src/tests/integration/test-data/foundry-minimize-merge @@ -0,0 +1 @@ +MergeKCFGTest.test_branch_merge(uint256,uint256,bool) \ No newline at end of file diff --git a/src/tests/integration/test-data/foundry/src/Branches.sol b/src/tests/integration/test-data/foundry/src/Branches.sol new file mode 100644 index 000000000..3b70094f2 --- /dev/null +++ b/src/tests/integration/test-data/foundry/src/Branches.sol @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + + +// CSE challenge: multiple branches that slow down the verification +contract Branches{ + function applyOp(uint256 x, uint256 y, bool z) public returns (uint256) { + if (z) { + return x + y; + } else { + return x * y; + } + } +} \ No newline at end of file diff --git a/src/tests/integration/test-data/foundry/test/MergeKCFGTest.t.sol b/src/tests/integration/test-data/foundry/test/MergeKCFGTest.t.sol new file mode 100644 index 000000000..2427d36ef --- /dev/null +++ b/src/tests/integration/test-data/foundry/test/MergeKCFGTest.t.sol @@ -0,0 +1,29 @@ +// SPDX-License-Identifier: UNLICENSED +pragma solidity =0.8.13; + +import "forge-std/Test.sol"; +import "src/Branches.sol"; + +contract MergeKCFGTest is Test { + Branches c; + + function setUp() external { + c = new Branches(); + } + + function test_branch_merge(uint256 x, uint256 y, bool z) external{ + vm.assume(x <= type(uint256).max - y); + try c.applyOp(x, y, z) returns (uint256 res) { + // This check will fail if the backend cannot recover the preds in the merged postcondition + // If so, assert res == x + y | res == x * y will pass + // If so, we should not always use merge_node, but provide both on need. + if (z) { + assert(res == x + y); + } else { + assert(res == x * y); + } + } catch { + assert(x != 0 && 2 ** 62 / x < y && !z); + } + } +} \ No newline at end of file diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected index ebd6ef69b..ff5c90bef 100644 --- a/src/tests/integration/test-data/show/contracts.k.expected +++ b/src/tests/integration/test-data/show/contracts.k.expected @@ -2212,6 +2212,29 @@ module S2KtestZModWarpTest-CONTRACT rule ( selector ( "test_warp_setup()" ) => 1375900050 ) +endmodule + +module S2KsrcZModBranches-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KsrcZModBranchesContract + + syntax S2KsrcZModBranchesContract ::= "S2KsrcZModBranches" [symbol("contract_src%Branches")] + + syntax Bytes ::= S2KsrcZModBranchesContract "." S2KsrcZModBranchesMethod [function, symbol("method_src%Branches")] + + syntax S2KsrcZModBranchesMethod ::= "S2KapplyOp" "(" Int ":" "uint256" "," Int ":" "uint256" "," Int ":" "bool" ")" [symbol("method_src%Branches_S2KapplyOp_uint256_uint256_bool")] + + rule ( S2KsrcZModBranches . S2KapplyOp ( KV0_x : uint256 , KV1_y : uint256 , KV2_z : bool ) => #abiCallData ( "applyOp" , ( #uint256 ( KV0_x ) , ( #uint256 ( KV1_y ) , ( #bool ( KV2_z ) , .TypedArgs ) ) ) ) ) + ensures ( #rangeUInt ( 256 , KV0_x ) + andBool ( #rangeUInt ( 256 , KV1_y ) + andBool ( #rangeBool ( KV2_z ) + ))) + + + rule ( selector ( "applyOp(uint256,uint256,bool)" ) => 3766377623 ) + + endmodule module S2KtestZModBroadcastTest-CONTRACT @@ -7652,6 +7675,117 @@ module S2KtestZModMergeTest-CONTRACT rule ( selector ( "test_branch_merge(uint256)" ) => 1000659212 ) +endmodule + +module S2KtestZModMergeKCFGTest-CONTRACT + imports public FOUNDRY + + syntax Contract ::= S2KtestZModMergeKCFGTestContract + + syntax S2KtestZModMergeKCFGTestContract ::= "S2KtestZModMergeKCFGTest" [symbol("contract_test%MergeKCFGTest")] + + syntax Bytes ::= S2KtestZModMergeKCFGTestContract "." S2KtestZModMergeKCFGTestMethod [function, symbol("method_test%MergeKCFGTest")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol("method_test%MergeKCFGTest_S2KISZUndTEST_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KexcludeArtifacts_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KexcludeContracts_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol("method_test%MergeKCFGTest_S2KexcludeSenders_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2Kfailed" "(" ")" [symbol("method_test%MergeKCFGTest_S2Kfailed_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KsetUp" "(" ")" [symbol("method_test%MergeKCFGTest_S2KsetUp_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetArtifactSelectors_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetArtifacts_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetContracts" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetContracts_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetSelectors_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtargetSenders" "(" ")" [symbol("method_test%MergeKCFGTest_S2KtargetSenders_")] + + syntax S2KtestZModMergeKCFGTestMethod ::= "S2KtestZUndbranchZUndmerge" "(" Int ":" "uint256" "," Int ":" "uint256" "," Int ":" "bool" ")" [symbol("method_test%MergeKCFGTest_S2KtestZUndbranchZUndmerge_uint256_uint256_bool")] + + rule ( S2KtestZModMergeKCFGTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KsetUp ( ) => #abiCallData ( "setUp" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) ) + + + rule ( S2KtestZModMergeKCFGTest . S2KtestZUndbranchZUndmerge ( KV0_x : uint256 , KV1_y : uint256 , KV2_z : bool ) => #abiCallData ( "test_branch_merge" , ( #uint256 ( KV0_x ) , ( #uint256 ( KV1_y ) , ( #bool ( KV2_z ) , .TypedArgs ) ) ) ) ) + ensures ( #rangeUInt ( 256 , KV0_x ) + andBool ( #rangeUInt ( 256 , KV1_y ) + andBool ( #rangeBool ( KV2_z ) + ))) + + + rule ( selector ( "IS_TEST()" ) => 4202047188 ) + + + rule ( selector ( "excludeArtifacts()" ) => 3041954473 ) + + + rule ( selector ( "excludeContracts()" ) => 3792478065 ) + + + rule ( selector ( "excludeSenders()" ) => 517440284 ) + + + rule ( selector ( "failed()" ) => 3124842406 ) + + + rule ( selector ( "setUp()" ) => 177362148 ) + + + rule ( selector ( "targetArtifactSelectors()" ) => 1725540768 ) + + + rule ( selector ( "targetArtifacts()" ) => 2233625729 ) + + + rule ( selector ( "targetContracts()" ) => 1064470260 ) + + + rule ( selector ( "targetSelectors()" ) => 2439649222 ) + + + rule ( selector ( "targetSenders()" ) => 1046363171 ) + + + rule ( selector ( "test_branch_merge(uint256,uint256,bool)" ) => 357868196 ) + + endmodule module S2KtestZModMethodDisambiguateTest-CONTRACT diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected index efa830fa6..3e917cda0 100644 --- a/src/tests/integration/test-data/show/foundry.k.expected +++ b/src/tests/integration/test-data/show/foundry.k.expected @@ -31,6 +31,7 @@ module FOUNDRY-MAIN imports public S2KtestZModFeeTest-VERIFICATION imports public S2KtestZModRollTest-VERIFICATION imports public S2KtestZModWarpTest-VERIFICATION + imports public S2KsrcZModBranches-VERIFICATION imports public S2KtestZModBroadcastTest-VERIFICATION imports public S2KtestZModCSETest-VERIFICATION imports public S2KtestZModStaticCallContract-VERIFICATION @@ -95,6 +96,7 @@ module FOUNDRY-MAIN imports public S2KsrcZModLoadStateDumpCode-VERIFICATION imports public S2KtestZModLoopsTest-VERIFICATION imports public S2KtestZModMergeTest-VERIFICATION + imports public S2KtestZModMergeKCFGTest-VERIFICATION imports public S2KtestZModMethodDisambiguateTest-VERIFICATION imports public S2KsrcZModMock-VERIFICATION imports public S2KsrcZModNestedMock-VERIFICATION @@ -343,6 +345,13 @@ module S2KtestZModWarpTest-VERIFICATION +endmodule + +module S2KsrcZModBranches-VERIFICATION + imports public S2KsrcZModBranches-CONTRACT + + + endmodule module S2KtestZModBroadcastTest-VERIFICATION @@ -794,6 +803,13 @@ module S2KtestZModMergeTest-VERIFICATION +endmodule + +module S2KtestZModMergeKCFGTest-VERIFICATION + imports public S2KtestZModMergeKCFGTest-CONTRACT + + + endmodule module S2KtestZModMethodDisambiguateTest-VERIFICATION 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 new file mode 100644 index 000000000..447471da6 --- /dev/null +++ b/src/tests/integration/test-data/show/minimized/MergeKCFGTest.test_branch_merge(uint256,uint256,bool).expected @@ -0,0 +1,1690 @@ + +┌─ 1 (root, init) +│ k: #execute ~> CONTINUATION:K +│ pc: 0 +│ callDepth: 0 +│ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 +│ method: test%MergeKCFGTest.setUp() +│ +│ (1925 steps) +├─ 17 (split) +│ k: JUMPI 99 bool2Word ( KV2_z:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ~> #return ... +│ pc: 85 +│ callDepth: 1 +│ statusCode: STATUSCODE:StatusCode +│ src: test/nested/SimpleNested.t.sol:7:11 +│ method: src%Branches.applyOp(uint256,uint256,bool) +┃ +┃ (branch) +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ ( notBool KV2_z:Int ==Int 0 ) +┃ │ +┃ ├─ 19 +┃ │ k: JUMPI 99 bool2Word ( KV2_z:Int ==Int 0 ) ~> #pc [ JUMPI ] ~> #execute ~> #return ... +┃ │ pc: 85 +┃ │ callDepth: 1 +┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: src%Branches.applyOp(uint256,uint256,bool) +┃ │ +┃ │ (668 steps) +┃ ├─ 39 (terminal) +┃ │ k: #halt ~> CONTINUATION:K +┃ │ pc: 194 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:69:71 +┃ │ method: test%MergeKCFGTest.test_branch_merge(uint256,uint256,bool) +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 10 (leaf, target, terminal) +┃ k: #halt ~> CONTINUATION:K +┃ pc: PC_CELL_5d410f2a:Int +┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int +┃ statusCode: STATUSCODE_FINAL:StatusCode +┃ +┣━━┓ subst: .Subst +┃ ┃ constraint: +┃ ┃ KV2_z:Int ==Int 0 +┃ ┃ ( notBool ( ( notBool KV0_x:Int ==Int 0 ) andBool maxUInt256 /Word KV0_x:Int #pc [ JUMPI ] ~> #execute ~> #return ... +┃ │ pc: 85 +┃ │ callDepth: 1 +┃ │ statusCode: STATUSCODE:StatusCode +┃ │ src: test/nested/SimpleNested.t.sol:7:11 +┃ │ method: src%Branches.applyOp(uint256,uint256,bool) +┃ │ +┃ │ (741 steps) +┃ ├─ 42 (terminal) +┃ │ k: #halt ~> CONTINUATION:K +┃ │ pc: 194 +┃ │ callDepth: 0 +┃ │ statusCode: EVMC_SUCCESS +┃ │ src: lib/forge-std/src/StdInvariant.sol:69:71 +┃ │ method: test%MergeKCFGTest.test_branch_merge(uint256,uint256,bool) +┃ │ +┃ ┊ constraint: true +┃ ┊ subst: ... +┃ └─ 10 (leaf, target, terminal) +┃ k: #halt ~> CONTINUATION:K +┃ pc: PC_CELL_5d410f2a:Int +┃ callDepth: CALLDEPTH_CELL_5d410f2a:Int +┃ statusCode: STATUSCODE_FINAL:StatusCode +┃ +┗━━┓ subst: .Subst + ┃ constraint: + ┃ KV2_z:Int ==Int 0 + ┃ ( notBool KV0_x:Int ==Int 0 ) + ┃ maxUInt256 /Word KV0_x:Int #pc [ JUMPI ] ~> #execute ~> #return ... + │ pc: 85 + │ callDepth: 1 + │ statusCode: STATUSCODE:StatusCode + │ src: test/nested/SimpleNested.t.sol:7:11 + │ method: src%Branches.applyOp(uint256,uint256,bool) + │ + │ (460 steps) + ├─ 43 (terminal) + │ k: #halt ~> CONTINUATION:K + │ pc: 194 + │ callDepth: 0 + │ statusCode: EVMC_SUCCESS + │ src: lib/forge-std/src/StdInvariant.sol:69:71 + │ method: test%MergeKCFGTest.test_branch_merge(uint256,uint256,bool) + │ + ┊ constraint: true + ┊ subst: ... + └─ 10 (leaf, target, terminal) + k: #halt ~> CONTINUATION:K + pc: PC_CELL_5d410f2a:Int + callDepth: CALLDEPTH_CELL_5d410f2a:Int + statusCode: STATUSCODE_FINAL:StatusCode + + + + +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 ) + ~> #pc [ JUMPI ] + ~> #execute + ~> #return 128 32 + ~> #pc [ CALL ] ) + ~> #execute + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + b"" + + + ( .List => ListItem ( + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + b"\x15T\xa2\xa4" +Bytes #buf ( 32 , ?KV0_x ) +Bytes #buf ( 32 , ?KV1_y ) +Bytes #buf ( 32 , ?KV2_z ) + + + 0 + + + ( 228 : ( selector ( "applyOp(uint256,uint256,bool)" ) : ( 491460923342184218035706888008750043977755113263 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 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 ) + + + 0 + + + 0 + + + false + + + 0 + + ... + ) ) + + + ( .List => ListItem ( { + ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) + | + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + } ) ) + + + ( .Set => ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) + + + + ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) + + + ( 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 ) ) + + + 0 + + + ( .WordStack => ( 0 : ( ?KV2_z : ( ?KV1_y : ( ?KV0_x : ( 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" ) + + + 0 + + + 0 + + + false + + + ( 0 => 1 ) + + ... + + + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( .Set => ( SetItem ( 491460923342184218035706888008750043977755113263 ) ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) ) + + + .Map + + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + ( 645326474426547203313410069153905908525362434349 => 491460923342184218035706888008750043977755113263 ) + + + 0 + + + .Map + + + .Map + + + .Map + + + ( 0 => 1 ) + + ... + + ( + + 728815563385977040452943777879061427756277306518 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + => ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) ) + + ... + + + ... + + + true + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( 0 <=Int CALLER_ID:Int + andBool ( 0 <=Int ORIGIN_ID:Int + andBool ( pow24 + + + ( JUMPI 99 bool2Word ( KV2_z:Int ==Int 0 ) + ~> #pc [ JUMPI ] + ~> #execute + ~> #return 128 32 + ~> #pc [ CALL ] + ~> #execute => #halt ~> .K ) + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + b"" + + + ( _STATUSCODE => EVMC_SUCCESS ) + + + ( ListItem ( + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + 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: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:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) + + + 0 + + + 0 + + + false + + + 0 + + ... + ) => .List ) + + + ( ListItem ( { + ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) + | + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + } ) => .List ) + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + + + + ( 491460923342184218035706888008750043977755113263 => 728815563385977040452943777879061427756277306518 ) + + + ( 728815563385977040452943777879061427756277306518 => CALLER_ID:Int ) + + + ( b"\xe0~\\\x97" => b"\x15T\xa2\xa4" ) +Bytes #buf ( 32 , KV0_x:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) + + + 0 + + + ( ( 0 => selector ( "test_branch_merge(uint256,uint256,bool)" ) ) : ( ( KV2_z:Int : ( KV1_y:Int : ( KV0_x:Int : ( 60 : ( selector ( "applyOp(uint256,uint256,bool)" ) : .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" => 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 , ( KV0_x:Int +Int KV1_y:Int ) ) +Bytes #range ( #buf ( 32 , KV0_x:Int ) , 28 , 4 ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) ) + + + 0 + + + 0 + + + false + + + ( 1 => 0 ) + + ... + + + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) + + + .Map + + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) + + ... + + + ... + + + true + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( KV2_z:Int =/=Int 0 + andBool ( KV2_z:Int + + + ( JUMPI 99 bool2Word ( KV2_z:Int ==Int 0 ) + ~> #pc [ JUMPI ] + ~> #execute + ~> #return 128 32 + ~> #pc [ CALL ] + ~> #execute => #halt ~> .K ) + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + b"" + + + ( _STATUSCODE => EVMC_SUCCESS ) + + + ( ListItem ( + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + 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: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:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) + + + 0 + + + 0 + + + false + + + 0 + + ... + ) => .List ) + + + ( ListItem ( { + ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) + | + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + } ) => .List ) + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + + + + ( 491460923342184218035706888008750043977755113263 => 728815563385977040452943777879061427756277306518 ) + + + ( 728815563385977040452943777879061427756277306518 => CALLER_ID:Int ) + + + ( b"\xe0~\\\x97" => b"\x15T\xa2\xa4" ) +Bytes #buf ( 32 , KV0_x:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes ( #buf ( 32 , KV2_z:Int ) => 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" ) + + + 0 + + + ( ( 0 => selector ( "test_branch_merge(uint256,uint256,bool)" ) ) : ( ( KV2_z:Int : ( KV1_y:Int : ( KV0_x:Int : ( 60 : ( selector ( "applyOp(uint256,uint256,bool)" ) : .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" => 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 , chop ( ( KV0_x:Int *Int KV1_y:Int ) ) ) +Bytes #range ( #buf ( 32 , KV0_x:Int ) , 28 , 4 ) +Bytes #buf ( 32 , KV1_y: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\x00" ) + + + 0 + + + 0 + + + false + + + ( 1 => 0 ) + + ... + + + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) + + + .Map + + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) + + ... + + + ... + + + true + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( KV2_z:Int ==Int 0 + andBool ( KV2_z:Int + + + ( JUMPI 99 bool2Word ( KV2_z:Int ==Int 0 ) + ~> #pc [ JUMPI ] + ~> #execute + ~> #return 128 32 + ~> #pc [ CALL ] + ~> #execute => #halt ~> .K ) + ~> _CONTINUATION + + + NORMAL + + + SHANGHAI + + + false + + + + + b"" + + + ( _STATUSCODE => EVMC_SUCCESS ) + + + ( ListItem ( + + 728815563385977040452943777879061427756277306518 + + + CALLER_ID:Int + + + 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: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:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes #buf ( 32 , KV2_z:Int ) + + + 0 + + + 0 + + + false + + + 0 + + ... + ) => .List ) + + + ( ListItem ( { + ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) + | + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 645326474426547203313410069153905908525362434349 ) ) + + + .Map + + } ) => .List ) + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + + + + ( 491460923342184218035706888008750043977755113263 => 728815563385977040452943777879061427756277306518 ) + + + ( 728815563385977040452943777879061427756277306518 => CALLER_ID:Int ) + + + ( b"\xe0~\\\x97" => b"\x15T\xa2\xa4" ) +Bytes #buf ( 32 , KV0_x:Int ) +Bytes #buf ( 32 , KV1_y:Int ) +Bytes ( #buf ( 32 , KV2_z:Int ) => 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" ) + + + 0 + + + ( ( 0 => selector ( "test_branch_merge(uint256,uint256,bool)" ) ) : ( ( KV2_z:Int : ( KV1_y:Int : ( KV0_x:Int : ( 60 : ( selector ( "applyOp(uint256,uint256,bool)" ) : .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" => 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\x00NH{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" +Bytes #range ( #buf ( 32 , KV0_x:Int ) , 28 , 4 ) +Bytes #buf ( 32 , KV1_y: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\x00" ) + + + 0 + + + 0 + + + false + + + ( 1 => 0 ) + + ... + + + + SELFDESTRUCT_CELL:Set + + + .List + + + 0 + + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) ( ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) => SetItem ( 645326474426547203313410069153905908525362434349 ) ) ) + + + .Map + + + + ORIGIN_ID:Int + + + + NUMBER_CELL:Int + + + TIMESTAMP_CELL:Int + + ... + + ... + + + + 1 + + + ( + + 491460923342184218035706888008750043977755113263 + + + 0 + + + .Map + + + .Map + + + .Map + + + 1 + + ... + + ( + + 645326474426547203313410069153905908525362434349 + + + 0 + + + .Map + + + .Map + + + .Map + + + 0 + + ... + + + + 728815563385977040452943777879061427756277306518 + + + 0 + + + ( 27 |-> 491460923342184218035706888008750043977755113263 ) + + + .Map + + + .Map + + + 2 + + ... + ) ) + + ... + + + ... + + + true + + + + + false + + + false + + ... + + + + false + + ... + + + + false + + ... + + + + false + + + false + + ... + + + + false + + + false + + + .List + + + .List + + + + .MockCallCellMap + + + .MockFunctionCellMap + + + + + false + + + false + + + false + + + false + + + false + + + .List + + + + requires ( KV2_z:Int ==Int 0 + andBool ( KV0_x:Int =/=Int 0 + andBool ( KV2_z:Int None: + merge = test_id in MINIMIZE_MERGE_TESTS + if no_use_booster: pytest.skip() @@ -363,7 +366,7 @@ def test_foundry_minimize_proof( # When foundry_prove(foundry=foundry, options=options) - foundry_minimize_proof(foundry, options=MinimizeProofOptions({'test': test_id})) + foundry_minimize_proof(foundry, options=MinimizeProofOptions({'test': test_id, 'merge': merge})) show_res = foundry_show( foundry=foundry, diff --git a/src/tests/integration/test_kontrol.py b/src/tests/integration/test_kontrol.py index 399f47945..cf77002ef 100644 --- a/src/tests/integration/test_kontrol.py +++ b/src/tests/integration/test_kontrol.py @@ -1,7 +1,7 @@ from __future__ import annotations import sys -from distutils.dir_util import copy_tree +from shutil import copytree from typing import TYPE_CHECKING import pytest @@ -59,7 +59,7 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath with FileLock(str(foundry_root) + '.lock'): if not foundry_root.is_dir(): init_project(project_root=foundry_root, skip_forge=False) - copy_tree(str(TEST_DATA_DIR / 'src'), str(foundry_root / 'test')) + copytree(str(TEST_DATA_DIR / 'src'), str(foundry_root / 'test'), dirs_exist_ok=True) append_to_file(foundry_root / 'foundry.toml', foundry_toml_cancun_schedule()) foundry_kompile( @@ -74,7 +74,7 @@ def foundry_end_to_end(foundry_root_dir: Path | None, tmp_path_factory: TempPath ) session_foundry_root = tmp_path_factory.mktemp('kontrol-test-project') - copy_tree(str(foundry_root), str(session_foundry_root)) + copytree(str(foundry_root), str(session_foundry_root), dirs_exist_ok=True) return Foundry(session_foundry_root) diff --git a/src/tests/utils.py b/src/tests/utils.py index 12c023b85..8803fc329 100644 --- a/src/tests/utils.py +++ b/src/tests/utils.py @@ -1,6 +1,6 @@ from __future__ import annotations -from distutils.dir_util import copy_tree +from shutil import copytree from typing import TYPE_CHECKING from pyk.utils import run_process_2 @@ -17,7 +17,7 @@ def forge_build(test_data_dir: Path, target_dir: Path) -> Foundry: - copy_tree(str(test_data_dir / 'foundry'), str(target_dir)) + copytree(str(test_data_dir / 'foundry'), str(target_dir), dirs_exist_ok=True) run_process_2(['forge', 'install', '--no-git', f'foundry-rs/forge-std@{FORGE_STD_REF}'], cwd=target_dir) run_process_2(['forge', 'build'], cwd=target_dir) return Foundry(foundry_root=target_dir)