diff --git a/deps/blockchain-k-plugin_release b/deps/blockchain-k-plugin_release index fdd690bc92..8fd1ef7508 100644 --- a/deps/blockchain-k-plugin_release +++ b/deps/blockchain-k-plugin_release @@ -1 +1 @@ -c095983f3aec21c52f00b2d433202052ad7db104 +b42e6ede9f6b72cedabc519810416e2994caad45 diff --git a/deps/k_release b/deps/k_release index 452ca39512..d974b1f71e 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.0.87 +6.0.133 diff --git a/deps/pyk_release b/deps/pyk_release index b2762b40d3..e9c898b343 100644 --- a/deps/pyk_release +++ b/deps/pyk_release @@ -1 +1 @@ -v0.1.448 +v0.1.461 diff --git a/flake.lock b/flake.lock index a69ba17653..374fd9ad7f 100644 --- a/flake.lock +++ b/flake.lock @@ -67,17 +67,17 @@ "xbyak": "xbyak" }, "locked": { - "lastModified": 1696084865, - "narHash": "sha256-0db01iMbkwUgOHI+ZiR1GiwLkL2turGOPH3oSkp4Eq0=", + "lastModified": 1696357247, + "narHash": "sha256-cCsH/uM1lfuCxfgflVwtg61Il6WjdZ/mDNwijIaRiRo=", "owner": "runtimeverification", "repo": "blockchain-k-plugin", - "rev": "c095983f3aec21c52f00b2d433202052ad7db104", + "rev": "b42e6ede9f6b72cedabc519810416e2994caad45", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "blockchain-k-plugin", - "rev": "c095983f3aec21c52f00b2d433202052ad7db104", + "rev": "b42e6ede9f6b72cedabc519810416e2994caad45", "type": "github" } }, @@ -98,17 +98,17 @@ ] }, "locked": { - "lastModified": 1693573175, - "narHash": "sha256-G6lV2a+oO3SJfvO+kKzcXeFQNXbhvF1T5SiZ9g3XME8=", + "lastModified": 1695839205, + "narHash": "sha256-9USUlWcL4YOseMJdQ1h4XvihR4/FG5zykykI7eY/13A=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "c2b639109b5c84c3f2c8abf9a826e50ab9525314", + "rev": "6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "c2b639109b5c84c3f2c8abf9a826e50ab9525314", + "rev": "6c2f5ab988e2c5f98b1cdeb04b8a5787d8a7c566", "type": "github" } }, @@ -366,11 +366,11 @@ "flake-compat_4": { "flake": false, "locked": { - "lastModified": 1673956053, - "narHash": "sha256-4gtG9iQuiKITOjNQQeQIpoIB6b16fm+504Ch3sNKLd8=", + "lastModified": 1696267196, + "narHash": "sha256-AAQ/2sD+0D18bb8hKuEEVpHUYD1GmO2Uh/taFamn6XQ=", "owner": "edolstra", "repo": "flake-compat", - "rev": "35bb57c0c8d8b62bbfd284272c928ceb64ddbde9", + "rev": "4f910c9827911b1ec2bf26b5a062cd09f8d89f85", "type": "github" }, "original": { @@ -448,11 +448,11 @@ "systems": "systems" }, "locked": { - "lastModified": 1692799911, - "narHash": "sha256-3eihraek4qL744EvQXsK1Ha6C3CR7nnT8X2qWap4RNk=", + "lastModified": 1694529238, + "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", "owner": "numtide", "repo": "flake-utils", - "rev": "f9e7cf818399d17d347f847525c5a5a8032e4e44", + "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", "type": "github" }, "original": { @@ -533,11 +533,11 @@ "nixpkgs": "nixpkgs" }, "locked": { - "lastModified": 1691140388, - "narHash": "sha256-AH3fx2VFGPRSOjnuakab4T4AdUstwTnFTbnkoU4df8Q=", + "lastModified": 1696410815, + "narHash": "sha256-uku47D/L+VzO3sVoZbnexPQPGeQtMwMFBesyaA1vKtE=", "owner": "shazow", "repo": "foundry.nix", - "rev": "6089aad0ef615ac8c7b0c948d6052fa848c99523", + "rev": "a56126a754d73f85d904768fed569a9e250388d9", "type": "github" }, "original": { @@ -627,17 +627,17 @@ "z3-src": "z3-src" }, "locked": { - "lastModified": 1692867782, - "narHash": "sha256-qPqg7hpCvRWOrG8k7jwbbTqThb0NFWQHZhZSeEqYI/g=", + "lastModified": 1695129967, + "narHash": "sha256-wLMrn/a10zH3Zvl+ln2Z37b8n4c013i+udkKfFf61Eg=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "1da6c43b8bb74a231b58978b1964a45d7ca753e4", + "rev": "63397c713d21322434d572281c1407d929a1189e", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "1da6c43b8bb74a231b58978b1964a45d7ca753e4", + "rev": "85b5d086840a0f1e89499f086b50d7258598fc8b", "type": "github" } }, @@ -654,17 +654,17 @@ "z3-src": "z3-src_2" }, "locked": { - "lastModified": 1692867782, - "narHash": "sha256-qPqg7hpCvRWOrG8k7jwbbTqThb0NFWQHZhZSeEqYI/g=", + "lastModified": 1695129967, + "narHash": "sha256-wLMrn/a10zH3Zvl+ln2Z37b8n4c013i+udkKfFf61Eg=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "1da6c43b8bb74a231b58978b1964a45d7ca753e4", + "rev": "63397c713d21322434d572281c1407d929a1189e", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "1da6c43b8bb74a231b58978b1964a45d7ca753e4", + "rev": "63397c713d21322434d572281c1407d929a1189e", "type": "github" } }, @@ -977,16 +977,16 @@ "rv-utils": "rv-utils" }, "locked": { - "lastModified": 1693947872, - "narHash": "sha256-pKiHZz+koADXQ3MdfzE39ADKSVnUIvmVbfkyZqNmXGQ=", + "lastModified": 1696460597, + "narHash": "sha256-5DDKlhQcnZvMKByOScNx7kRn2bEB7RHUAKeu/0nEq9U=", "owner": "runtimeverification", "repo": "k", - "rev": "3997d65c227fde4e67cedfca83a8a2d2436229e6", + "rev": "cf6252fa9bfc9867e956fe3a20868722e62effd5", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v6.0.87", + "ref": "v6.0.133", "repo": "k", "type": "github" } @@ -1023,11 +1023,11 @@ "utils": "utils_2" }, "locked": { - "lastModified": 1692976793, - "narHash": "sha256-ytl8wuFYYx9NAaIBLjil/UgZcK9fBgXDspDE1y+gNHM=", + "lastModified": 1696257790, + "narHash": "sha256-2iNcK72D4V9l+sjHBvv0ZAXXdSYf0YVX4MuaMvSxgb8=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "f3e29231a9a8bc4373fbbc74866f96df454cbc7e", + "rev": "0952940a242d8909da60d3ebde6059b47579f530", "type": "github" }, "original": { @@ -1604,16 +1604,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1695658775, - "narHash": "sha256-o3DRBtLwa7+mSU1FeGs2mDBelpQ4yuDx1AmMEWkSy6o=", + "lastModified": 1696491819, + "narHash": "sha256-WjolGOqS/liz609TlGOXI5RjnQQo9NIh4jK5MXZ5B1k=", "owner": "runtimeverification", "repo": "pyk", - "rev": "ca97bb1caf81ddbb70c87d9aa7be1a4b5385fb2b", + "rev": "79c45d9f1ae355b591cbd2e8b77c6205ab170835", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.448", + "ref": "v0.1.461", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index d807d917ba..bd6d9fb4ee 100644 --- a/flake.nix +++ b/flake.nix @@ -3,13 +3,13 @@ inputs = { nixpkgs.url = "github:NixOS/nixpkgs/b01f185e4866de7c5b5a82f833ca9ea3c3f72fc4"; - k-framework.url = "github:runtimeverification/k/v6.0.87"; + k-framework.url = "github:runtimeverification/k/v6.0.133"; k-framework.inputs.nixpkgs.follows = "nixpkgs"; #nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.url = "github:runtimeverification/rv-nix-tools"; poetry2nix.follows = "pyk/poetry2nix"; - blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/c095983f3aec21c52f00b2d433202052ad7db104"; + blockchain-k-plugin.url = "github:runtimeverification/blockchain-k-plugin/b42e6ede9f6b72cedabc519810416e2994caad45"; blockchain-k-plugin.inputs.flake-utils.follows = "k-framework/flake-utils"; blockchain-k-plugin.inputs.nixpkgs.follows = "k-framework/nixpkgs"; ethereum-tests.url = "github:ethereum/tests/6401889dec4eee58e808fd178fb2c7f628a3e039"; @@ -17,7 +17,7 @@ ethereum-legacytests.url = "github:ethereum/legacytests/d7abc42a7b352a7b44b1f66b58aca54e4af6a9d7"; ethereum-legacytests.flake = false; haskell-backend.follows = "k-framework/haskell-backend"; - pyk.url = "github:runtimeverification/pyk/v0.1.448"; + pyk.url = "github:runtimeverification/pyk/v0.1.461"; pyk.inputs.flake-utils.follows = "k-framework/flake-utils"; pyk.inputs.nixpkgs.follows = "k-framework/nixpkgs"; foundry.url = "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 8eca4ee11a..0c8a46d57f 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -156,63 +156,63 @@ cron = ["capturer (>=2.4)"] [[package]] name = "coverage" -version = "7.3.1" +version = "7.3.2" description = "Code coverage measurement for Python" optional = false python-versions = ">=3.8" files = [ - {file = "coverage-7.3.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:cd0f7429ecfd1ff597389907045ff209c8fdb5b013d38cfa7c60728cb484b6e3"}, - {file = "coverage-7.3.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:966f10df9b2b2115da87f50f6a248e313c72a668248be1b9060ce935c871f276"}, - {file = "coverage-7.3.1-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:0575c37e207bb9b98b6cf72fdaaa18ac909fb3d153083400c2d48e2e6d28bd8e"}, - {file = "coverage-7.3.1-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:245c5a99254e83875c7fed8b8b2536f040997a9b76ac4c1da5bff398c06e860f"}, - {file = "coverage-7.3.1-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4c96dd7798d83b960afc6c1feb9e5af537fc4908852ef025600374ff1a017392"}, - {file = "coverage-7.3.1-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:de30c1aa80f30af0f6b2058a91505ea6e36d6535d437520067f525f7df123887"}, - {file = "coverage-7.3.1-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:50dd1e2dd13dbbd856ffef69196781edff26c800a74f070d3b3e3389cab2600d"}, - {file = "coverage-7.3.1-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:b9c0c19f70d30219113b18fe07e372b244fb2a773d4afde29d5a2f7930765136"}, - {file = "coverage-7.3.1-cp310-cp310-win32.whl", hash = "sha256:770f143980cc16eb601ccfd571846e89a5fe4c03b4193f2e485268f224ab602f"}, - {file = "coverage-7.3.1-cp310-cp310-win_amd64.whl", hash = "sha256:cdd088c00c39a27cfa5329349cc763a48761fdc785879220d54eb785c8a38520"}, - {file = "coverage-7.3.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:74bb470399dc1989b535cb41f5ca7ab2af561e40def22d7e188e0a445e7639e3"}, - {file = "coverage-7.3.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:025ded371f1ca280c035d91b43252adbb04d2aea4c7105252d3cbc227f03b375"}, - {file = "coverage-7.3.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a6191b3a6ad3e09b6cfd75b45c6aeeffe7e3b0ad46b268345d159b8df8d835f9"}, - {file = "coverage-7.3.1-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:7eb0b188f30e41ddd659a529e385470aa6782f3b412f860ce22b2491c89b8593"}, - {file = "coverage-7.3.1-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:75c8f0df9dfd8ff745bccff75867d63ef336e57cc22b2908ee725cc552689ec8"}, - {file = "coverage-7.3.1-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:7eb3cd48d54b9bd0e73026dedce44773214064be93611deab0b6a43158c3d5a0"}, - {file = "coverage-7.3.1-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:ac3c5b7e75acac31e490b7851595212ed951889918d398b7afa12736c85e13ce"}, - {file = "coverage-7.3.1-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:5b4ee7080878077af0afa7238df1b967f00dc10763f6e1b66f5cced4abebb0a3"}, - {file = "coverage-7.3.1-cp311-cp311-win32.whl", hash = "sha256:229c0dd2ccf956bf5aeede7e3131ca48b65beacde2029f0361b54bf93d36f45a"}, - {file = "coverage-7.3.1-cp311-cp311-win_amd64.whl", hash = "sha256:c6f55d38818ca9596dc9019eae19a47410d5322408140d9a0076001a3dcb938c"}, - {file = "coverage-7.3.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:5289490dd1c3bb86de4730a92261ae66ea8d44b79ed3cc26464f4c2cde581fbc"}, - {file = "coverage-7.3.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:ca833941ec701fda15414be400c3259479bfde7ae6d806b69e63b3dc423b1832"}, - {file = "coverage-7.3.1-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:cd694e19c031733e446c8024dedd12a00cda87e1c10bd7b8539a87963685e969"}, - {file = "coverage-7.3.1-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:aab8e9464c00da5cb9c536150b7fbcd8850d376d1151741dd0d16dfe1ba4fd26"}, - {file = "coverage-7.3.1-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:87d38444efffd5b056fcc026c1e8d862191881143c3aa80bb11fcf9dca9ae204"}, - {file = "coverage-7.3.1-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:8a07b692129b8a14ad7a37941a3029c291254feb7a4237f245cfae2de78de037"}, - {file = "coverage-7.3.1-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:2829c65c8faaf55b868ed7af3c7477b76b1c6ebeee99a28f59a2cb5907a45760"}, - {file = "coverage-7.3.1-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:1f111a7d85658ea52ffad7084088277135ec5f368457275fc57f11cebb15607f"}, - {file = "coverage-7.3.1-cp312-cp312-win32.whl", hash = "sha256:c397c70cd20f6df7d2a52283857af622d5f23300c4ca8e5bd8c7a543825baa5a"}, - {file = "coverage-7.3.1-cp312-cp312-win_amd64.whl", hash = "sha256:5ae4c6da8b3d123500f9525b50bf0168023313963e0e2e814badf9000dd6ef92"}, - {file = "coverage-7.3.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:ca70466ca3a17460e8fc9cea7123c8cbef5ada4be3140a1ef8f7b63f2f37108f"}, - {file = "coverage-7.3.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:f2781fd3cabc28278dc982a352f50c81c09a1a500cc2086dc4249853ea96b981"}, - {file = "coverage-7.3.1-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6407424621f40205bbe6325686417e5e552f6b2dba3535dd1f90afc88a61d465"}, - {file = "coverage-7.3.1-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:04312b036580ec505f2b77cbbdfb15137d5efdfade09156961f5277149f5e344"}, - {file = "coverage-7.3.1-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ac9ad38204887349853d7c313f53a7b1c210ce138c73859e925bc4e5d8fc18e7"}, - {file = "coverage-7.3.1-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:53669b79f3d599da95a0afbef039ac0fadbb236532feb042c534fbb81b1a4e40"}, - {file = "coverage-7.3.1-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:614f1f98b84eb256e4f35e726bfe5ca82349f8dfa576faabf8a49ca09e630086"}, - {file = "coverage-7.3.1-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:f1a317fdf5c122ad642db8a97964733ab7c3cf6009e1a8ae8821089993f175ff"}, - {file = "coverage-7.3.1-cp38-cp38-win32.whl", hash = "sha256:defbbb51121189722420a208957e26e49809feafca6afeef325df66c39c4fdb3"}, - {file = "coverage-7.3.1-cp38-cp38-win_amd64.whl", hash = "sha256:f4f456590eefb6e1b3c9ea6328c1e9fa0f1006e7481179d749b3376fc793478e"}, - {file = "coverage-7.3.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:f12d8b11a54f32688b165fd1a788c408f927b0960984b899be7e4c190ae758f1"}, - {file = "coverage-7.3.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:f09195dda68d94a53123883de75bb97b0e35f5f6f9f3aa5bf6e496da718f0cb6"}, - {file = "coverage-7.3.1-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c6601a60318f9c3945be6ea0f2a80571f4299b6801716f8a6e4846892737ebe4"}, - {file = "coverage-7.3.1-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:07d156269718670d00a3b06db2288b48527fc5f36859425ff7cec07c6b367745"}, - {file = "coverage-7.3.1-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:636a8ac0b044cfeccae76a36f3b18264edcc810a76a49884b96dd744613ec0b7"}, - {file = "coverage-7.3.1-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:5d991e13ad2ed3aced177f524e4d670f304c8233edad3210e02c465351f785a0"}, - {file = "coverage-7.3.1-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:586649ada7cf139445da386ab6f8ef00e6172f11a939fc3b2b7e7c9082052fa0"}, - {file = "coverage-7.3.1-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:4aba512a15a3e1e4fdbfed2f5392ec221434a614cc68100ca99dcad7af29f3f8"}, - {file = "coverage-7.3.1-cp39-cp39-win32.whl", hash = "sha256:6bc6f3f4692d806831c136c5acad5ccedd0262aa44c087c46b7101c77e139140"}, - {file = "coverage-7.3.1-cp39-cp39-win_amd64.whl", hash = "sha256:553d7094cb27db58ea91332e8b5681bac107e7242c23f7629ab1316ee73c4981"}, - {file = "coverage-7.3.1-pp38.pp39.pp310-none-any.whl", hash = "sha256:220eb51f5fb38dfdb7e5d54284ca4d0cd70ddac047d750111a68ab1798945194"}, - {file = "coverage-7.3.1.tar.gz", hash = "sha256:6cb7fe1581deb67b782c153136541e20901aa312ceedaf1467dcb35255787952"}, + {file = "coverage-7.3.2-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:d872145f3a3231a5f20fd48500274d7df222e291d90baa2026cc5152b7ce86bf"}, + {file = "coverage-7.3.2-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:310b3bb9c91ea66d59c53fa4989f57d2436e08f18fb2f421a1b0b6b8cc7fffda"}, + {file = "coverage-7.3.2-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f47d39359e2c3779c5331fc740cf4bce6d9d680a7b4b4ead97056a0ae07cb49a"}, + {file = "coverage-7.3.2-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:aa72dbaf2c2068404b9870d93436e6d23addd8bbe9295f49cbca83f6e278179c"}, + {file = "coverage-7.3.2-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:beaa5c1b4777f03fc63dfd2a6bd820f73f036bfb10e925fce067b00a340d0f3f"}, + {file = "coverage-7.3.2-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:dbc1b46b92186cc8074fee9d9fbb97a9dd06c6cbbef391c2f59d80eabdf0faa6"}, + {file = "coverage-7.3.2-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:315a989e861031334d7bee1f9113c8770472db2ac484e5b8c3173428360a9148"}, + {file = "coverage-7.3.2-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:d1bc430677773397f64a5c88cb522ea43175ff16f8bfcc89d467d974cb2274f9"}, + {file = "coverage-7.3.2-cp310-cp310-win32.whl", hash = "sha256:a889ae02f43aa45032afe364c8ae84ad3c54828c2faa44f3bfcafecb5c96b02f"}, + {file = "coverage-7.3.2-cp310-cp310-win_amd64.whl", hash = "sha256:c0ba320de3fb8c6ec16e0be17ee1d3d69adcda99406c43c0409cb5c41788a611"}, + {file = "coverage-7.3.2-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:ac8c802fa29843a72d32ec56d0ca792ad15a302b28ca6203389afe21f8fa062c"}, + {file = "coverage-7.3.2-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:89a937174104339e3a3ffcf9f446c00e3a806c28b1841c63edb2b369310fd074"}, + {file = "coverage-7.3.2-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e267e9e2b574a176ddb983399dec325a80dbe161f1a32715c780b5d14b5f583a"}, + {file = "coverage-7.3.2-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:2443cbda35df0d35dcfb9bf8f3c02c57c1d6111169e3c85fc1fcc05e0c9f39a3"}, + {file = "coverage-7.3.2-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:4175e10cc8dda0265653e8714b3174430b07c1dca8957f4966cbd6c2b1b8065a"}, + {file = "coverage-7.3.2-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:0cbf38419fb1a347aaf63481c00f0bdc86889d9fbf3f25109cf96c26b403fda1"}, + {file = "coverage-7.3.2-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:5c913b556a116b8d5f6ef834038ba983834d887d82187c8f73dec21049abd65c"}, + {file = "coverage-7.3.2-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:1981f785239e4e39e6444c63a98da3a1db8e971cb9ceb50a945ba6296b43f312"}, + {file = "coverage-7.3.2-cp311-cp311-win32.whl", hash = "sha256:43668cabd5ca8258f5954f27a3aaf78757e6acf13c17604d89648ecc0cc66640"}, + {file = "coverage-7.3.2-cp311-cp311-win_amd64.whl", hash = "sha256:e10c39c0452bf6e694511c901426d6b5ac005acc0f78ff265dbe36bf81f808a2"}, + {file = "coverage-7.3.2-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:4cbae1051ab791debecc4a5dcc4a1ff45fc27b91b9aee165c8a27514dd160836"}, + {file = "coverage-7.3.2-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:12d15ab5833a997716d76f2ac1e4b4d536814fc213c85ca72756c19e5a6b3d63"}, + {file = "coverage-7.3.2-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3c7bba973ebee5e56fe9251300c00f1579652587a9f4a5ed8404b15a0471f216"}, + {file = "coverage-7.3.2-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:fe494faa90ce6381770746077243231e0b83ff3f17069d748f645617cefe19d4"}, + {file = "coverage-7.3.2-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f6e9589bd04d0461a417562649522575d8752904d35c12907d8c9dfeba588faf"}, + {file = "coverage-7.3.2-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:d51ac2a26f71da1b57f2dc81d0e108b6ab177e7d30e774db90675467c847bbdf"}, + {file = "coverage-7.3.2-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:99b89d9f76070237975b315b3d5f4d6956ae354a4c92ac2388a5695516e47c84"}, + {file = "coverage-7.3.2-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:fa28e909776dc69efb6ed975a63691bc8172b64ff357e663a1bb06ff3c9b589a"}, + {file = "coverage-7.3.2-cp312-cp312-win32.whl", hash = "sha256:289fe43bf45a575e3ab10b26d7b6f2ddb9ee2dba447499f5401cfb5ecb8196bb"}, + {file = "coverage-7.3.2-cp312-cp312-win_amd64.whl", hash = "sha256:7dbc3ed60e8659bc59b6b304b43ff9c3ed858da2839c78b804973f613d3e92ed"}, + {file = "coverage-7.3.2-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:f94b734214ea6a36fe16e96a70d941af80ff3bfd716c141300d95ebc85339738"}, + {file = "coverage-7.3.2-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:af3d828d2c1cbae52d34bdbb22fcd94d1ce715d95f1a012354a75e5913f1bda2"}, + {file = "coverage-7.3.2-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:630b13e3036e13c7adc480ca42fa7afc2a5d938081d28e20903cf7fd687872e2"}, + {file = "coverage-7.3.2-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:c9eacf273e885b02a0273bb3a2170f30e2d53a6d53b72dbe02d6701b5296101c"}, + {file = "coverage-7.3.2-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d8f17966e861ff97305e0801134e69db33b143bbfb36436efb9cfff6ec7b2fd9"}, + {file = "coverage-7.3.2-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:b4275802d16882cf9c8b3d057a0839acb07ee9379fa2749eca54efbce1535b82"}, + {file = "coverage-7.3.2-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:72c0cfa5250f483181e677ebc97133ea1ab3eb68645e494775deb6a7f6f83901"}, + {file = "coverage-7.3.2-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:cb536f0dcd14149425996821a168f6e269d7dcd2c273a8bff8201e79f5104e76"}, + {file = "coverage-7.3.2-cp38-cp38-win32.whl", hash = "sha256:307adb8bd3abe389a471e649038a71b4eb13bfd6b7dd9a129fa856f5c695cf92"}, + {file = "coverage-7.3.2-cp38-cp38-win_amd64.whl", hash = "sha256:88ed2c30a49ea81ea3b7f172e0269c182a44c236eb394718f976239892c0a27a"}, + {file = "coverage-7.3.2-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:b631c92dfe601adf8f5ebc7fc13ced6bb6e9609b19d9a8cd59fa47c4186ad1ce"}, + {file = "coverage-7.3.2-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:d3d9df4051c4a7d13036524b66ecf7a7537d14c18a384043f30a303b146164e9"}, + {file = "coverage-7.3.2-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:5f7363d3b6a1119ef05015959ca24a9afc0ea8a02c687fe7e2d557705375c01f"}, + {file = "coverage-7.3.2-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:2f11cc3c967a09d3695d2a6f03fb3e6236622b93be7a4b5dc09166a861be6d25"}, + {file = "coverage-7.3.2-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:149de1d2401ae4655c436a3dced6dd153f4c3309f599c3d4bd97ab172eaf02d9"}, + {file = "coverage-7.3.2-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:3a4006916aa6fee7cd38db3bfc95aa9c54ebb4ffbfc47c677c8bba949ceba0a6"}, + {file = "coverage-7.3.2-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:9028a3871280110d6e1aa2df1afd5ef003bab5fb1ef421d6dc748ae1c8ef2ebc"}, + {file = "coverage-7.3.2-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:9f805d62aec8eb92bab5b61c0f07329275b6f41c97d80e847b03eb894f38d083"}, + {file = "coverage-7.3.2-cp39-cp39-win32.whl", hash = "sha256:d1c88ec1a7ff4ebca0219f5b1ef863451d828cccf889c173e1253aa84b1e07ce"}, + {file = "coverage-7.3.2-cp39-cp39-win_amd64.whl", hash = "sha256:b4767da59464bb593c07afceaddea61b154136300881844768037fd5e859353f"}, + {file = "coverage-7.3.2-pp38.pp39.pp310-none-any.whl", hash = "sha256:ae97af89f0fbf373400970c0a21eef5aa941ffeed90aee43650b81f7d7f47637"}, + {file = "coverage-7.3.2.tar.gz", hash = "sha256:be32ad29341b0170e795ca590e1c07e81fc061cb5b10c74ce7203491484404ef"}, ] [package.dependencies] @@ -342,13 +342,13 @@ flake8 = "*" [[package]] name = "flake8-type-checking" -version = "2.4.1" +version = "2.4.2" description = "A flake8 plugin for managing type-checking imports & forward references" optional = false python-versions = ">=3.8" files = [ - {file = "flake8_type_checking-2.4.1-py3-none-any.whl", hash = "sha256:fe75cfe668e3bf6914dd2ba36579bbe6c82f3795127774e7584ecc8c9f7379e5"}, - {file = "flake8_type_checking-2.4.1.tar.gz", hash = "sha256:f3c7023114dee2ec2e8282a9080206ffd8fdd61205626593aa5c801bc2f8035d"}, + {file = "flake8_type_checking-2.4.2-py3-none-any.whl", hash = "sha256:921efdcb2bfcd6d6cd3bb411419e9dcbd506bd8893ad749030d9cce032129f28"}, + {file = "flake8_type_checking-2.4.2.tar.gz", hash = "sha256:468a7c91ca6ebe58c4af6836dda3bfeba7bfb7c0b5f724baf5024ad5fda0504c"}, ] [package.dependencies] @@ -606,13 +606,13 @@ files = [ [[package]] name = "packaging" -version = "23.1" +version = "23.2" description = "Core utilities for Python packages" optional = false python-versions = ">=3.7" files = [ - {file = "packaging-23.1-py3-none-any.whl", hash = "sha256:994793af429502c4ea2ebf6bf664629d07c1a9fe974af92966e4b8d2df7edc61"}, - {file = "packaging-23.1.tar.gz", hash = "sha256:a392980d2b6cffa644431898be54b0045151319d1e7ec34f0cfed48767dd334f"}, + {file = "packaging-23.2-py3-none-any.whl", hash = "sha256:8c491190033a9af7e1d931d0b5dacc2ef47509b34dd0de67ed209b5203fc88c7"}, + {file = "packaging-23.2.tar.gz", hash = "sha256:048fb0e9405036518eaaf48a55953c750c11e1a1b68e0dd1a9d62ed0c092cfc5"}, ] [[package]] @@ -659,13 +659,13 @@ flake8 = ">=5.0.0" [[package]] name = "platformdirs" -version = "3.10.0" +version = "3.11.0" description = "A small Python package for determining appropriate platform-specific dirs, e.g. a \"user data dir\"." optional = false python-versions = ">=3.7" files = [ - {file = "platformdirs-3.10.0-py3-none-any.whl", hash = "sha256:d7c24979f292f916dc9cbf8648319032f551ea8c49a4c9bf2fb556a02070ec1d"}, - {file = "platformdirs-3.10.0.tar.gz", hash = "sha256:b45696dab2d7cc691a3226759c0d3b00c47c8b6e293d96f6436f733303f77f6d"}, + {file = "platformdirs-3.11.0-py3-none-any.whl", hash = "sha256:e9d171d00af68be50e9202731309c4e658fd8bc76f55c11c7dd760d023bda68e"}, + {file = "platformdirs-3.11.0.tar.gz", hash = "sha256:cf8ee52a3afdb965072dcc652433e0c7e3e40cf5ea1477cd4b3b1d2eb75495b3"}, ] [package.extras] @@ -790,7 +790,7 @@ plugins = ["importlib-metadata"] [[package]] name = "pyk" -version = "0.1.448" +version = "0.1.461" description = "" optional = false python-versions = "^3.10" @@ -810,8 +810,8 @@ tomli = "^2.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.448" -resolved_reference = "ca97bb1caf81ddbb70c87d9aa7be1a4b5385fb2b" +reference = "v0.1.461" +resolved_reference = "79c45d9f1ae355b591cbd2e8b77c6205ab170835" [[package]] name = "pyperclip" @@ -893,13 +893,13 @@ dev = ["pre-commit", "pytest-asyncio", "tox"] [[package]] name = "pytest-timeout" -version = "2.1.0" +version = "2.2.0" description = "pytest plugin to abort hanging tests" optional = false -python-versions = ">=3.6" +python-versions = ">=3.7" files = [ - {file = "pytest-timeout-2.1.0.tar.gz", hash = "sha256:c07ca07404c612f8abbe22294b23c368e2e5104b521c1790195561f37e1ac3d9"}, - {file = "pytest_timeout-2.1.0-py3-none-any.whl", hash = "sha256:f6f50101443ce70ad325ceb4473c4255e9d74e3c7cd0ef827309dfa4c0d975c6"}, + {file = "pytest-timeout-2.2.0.tar.gz", hash = "sha256:3b0b95dabf3cb50bac9ef5ca912fa0cfc286526af17afc806824df20c2f72c90"}, + {file = "pytest_timeout-2.2.0-py3-none-any.whl", hash = "sha256:bde531e096466f49398a59f2dde76fa78429a09a12411466f88a07213e220de2"}, ] [package.dependencies] @@ -927,13 +927,13 @@ testing = ["filelock"] [[package]] name = "pyupgrade" -version = "3.13.0" +version = "3.15.0" description = "A tool to automatically upgrade syntax for newer versions." optional = false python-versions = ">=3.8.1" files = [ - {file = "pyupgrade-3.13.0-py2.py3-none-any.whl", hash = "sha256:8add43ca1fea6eaeb6815b0b987d1f6ff49ec48085169b2a32e9a797e2d2f8fd"}, - {file = "pyupgrade-3.13.0.tar.gz", hash = "sha256:92220ef0408ff5898bce8ce7845c33bf7bb79c8ff852c5a1dc4305e6333cd60b"}, + {file = "pyupgrade-3.15.0-py2.py3-none-any.whl", hash = "sha256:8dc8ebfaed43566e2c65994162795017c7db11f531558a74bc8aa077907bc305"}, + {file = "pyupgrade-3.15.0.tar.gz", hash = "sha256:a7fde381060d7c224f55aef7a30fae5ac93bbc428367d27e70a603bc2acd4f00"}, ] [package.dependencies] @@ -1075,4 +1075,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "0989e521a276d5702a2cb5da02927f97d6ca77864edcf175f0ffc9cdaffffcaa" +content-hash = "3d97eb00a8b24672a738cee1c8ca57e90235482562134c38abf342383dc0a0e3" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 88a4c15ced..b0f8926226 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.314" +version = "1.0.315" description = "" authors = [ "Runtime Verification, Inc. ", @@ -17,7 +17,7 @@ packages = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.448" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.461" } tomlkit = "^0.11.6" xdg-base-dirs = "^6.0.0" diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 2e92eddbaa..af8df6f2ff 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.314' +VERSION: Final = '1.0.315' diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md index afc975f115..5993e751c8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md @@ -17,73 +17,75 @@ Some important numbers that are referred to often during execution. These can be used for pattern-matching on the LHS of rules as well (`alias` attribute expands all occurances of these in rules). ```k - syntax Int ::= "pow256" [alias] /* 2 ^Int 256 */ + syntax Int ::= "pow5" [macro] /* 2 ^Int 5 */ + | "pow8" [macro] /* 2 ^Int 8 */ + | "pow16" [alias] /* 2 ^Int 16 */ + | "pow24" [alias] /* 2 ^Int 24 */ + | "pow32" [alias] /* 2 ^Int 32 */ + | "pow40" [alias] /* 2 ^Int 40 */ + | "pow48" [alias] /* 2 ^Int 48 */ + | "pow56" [alias] /* 2 ^Int 56 */ + | "pow64" [alias] /* 2 ^Int 64 */ + | "pow72" [alias] /* 2 ^Int 72 */ + | "pow80" [alias] /* 2 ^Int 80 */ + | "pow88" [alias] /* 2 ^Int 88 */ + | "pow96" [alias] /* 2 ^Int 96 */ + | "pow104" [alias] /* 2 ^Int 104 */ + | "pow112" [alias] /* 2 ^Int 112 */ + | "pow120" [alias] /* 2 ^Int 120 */ + | "pow128" [alias] /* 2 ^Int 128 */ + | "pow136" [alias] /* 2 ^Int 136 */ + | "pow144" [alias] /* 2 ^Int 144 */ + | "pow152" [alias] /* 2 ^Int 152 */ + | "pow160" [alias] /* 2 ^Int 160 */ + | "pow168" [alias] /* 2 ^Int 168 */ + | "pow176" [alias] /* 2 ^Int 176 */ + | "pow184" [alias] /* 2 ^Int 184 */ + | "pow192" [alias] /* 2 ^Int 192 */ + | "pow200" [alias] /* 2 ^Int 200 */ + | "pow208" [alias] /* 2 ^Int 208 */ + | "pow216" [alias] /* 2 ^Int 216 */ + | "pow224" [alias] /* 2 ^Int 224 */ + | "pow232" [alias] /* 2 ^Int 232 */ + | "pow240" [alias] /* 2 ^Int 240 */ + | "pow248" [alias] /* 2 ^Int 248 */ | "pow255" [alias] /* 2 ^Int 255 */ - | "pow248" [alias] /* 2 ^Int 248" */ - | "pow240" [alias] /* 2 ^Int 240" */ - | "pow232" [alias] /* 2 ^Int 232" */ - | "pow224" [alias] /* 2 ^Int 224" */ - | "pow216" [alias] /* 2 ^Int 216" */ - | "pow208" [alias] /* 2 ^Int 208" */ - | "pow200" [alias] /* 2 ^Int 200" */ - | "pow192" [alias] /* 2 ^Int 192" */ - | "pow184" [alias] /* 2 ^Int 184" */ - | "pow176" [alias] /* 2 ^Int 176" */ - | "pow168" [alias] /* 2 ^Int 168" */ - | "pow160" [alias] /* 2 ^Int 160" */ - | "pow152" [alias] /* 2 ^Int 152" */ - | "pow144" [alias] /* 2 ^Int 144" */ - | "pow136" [alias] /* 2 ^Int 136" */ - | "pow128" [alias] /* 2 ^Int 128" */ - | "pow120" [alias] /* 2 ^Int 120" */ - | "pow112" [alias] /* 2 ^Int 112" */ - | "pow104" [alias] /* 2 ^Int 104" */ - | "pow96" [alias] /* 2 ^Int 96" */ - | "pow88" [alias] /* 2 ^Int 88" */ - | "pow80" [alias] /* 2 ^Int 80" */ - | "pow72" [alias] /* 2 ^Int 72" */ - | "pow64" [alias] /* 2 ^Int 64" */ - | "pow56" [alias] /* 2 ^Int 56" */ - | "pow48" [alias] /* 2 ^Int 48" */ - | "pow40" [alias] /* 2 ^Int 40" */ - | "pow32" [alias] /* 2 ^Int 32" */ - | "pow24" [alias] /* 2 ^Int 24" */ - | "pow16" [alias] /* 2 ^Int 16" */ - | "pow8" [macro] /* 2 ^Int 8" */ + | "pow256" [alias] /* 2 ^Int 256 */ // ------------------------------------------------ - rule pow256 => 115792089237316195423570985008687907853269984665640564039457584007913129639936 - rule pow255 => 57896044618658097711785492504343953926634992332820282019728792003956564819968 - rule pow248 => 452312848583266388373324160190187140051835877600158453279131187530910662656 - rule pow240 => 1766847064778384329583297500742918515827483896875618958121606201292619776 - rule pow232 => 6901746346790563787434755862277025452451108972170386555162524223799296 - rule pow224 => 26959946667150639794667015087019630673637144422540572481103610249216 - rule pow216 => 105312291668557186697918027683670432318895095400549111254310977536 - rule pow208 => 411376139330301510538742295639337626245683966408394965837152256 - rule pow200 => 1606938044258990275541962092341162602522202993782792835301376 - rule pow192 => 6277101735386680763835789423207666416102355444464034512896 - rule pow184 => 24519928653854221733733552434404946937899825954937634816 - rule pow176 => 95780971304118053647396689196894323976171195136475136 - rule pow168 => 374144419156711147060143317175368453031918731001856 - rule pow160 => 1461501637330902918203684832716283019655932542976 - rule pow152 => 5708990770823839524233143877797980545530986496 - rule pow144 => 22300745198530623141535718272648361505980416 - rule pow136 => 87112285931760246646623899502532662132736 - rule pow128 => 340282366920938463463374607431768211456 - rule pow120 => 1329227995784915872903807060280344576 - rule pow112 => 5192296858534827628530496329220096 - rule pow104 => 20282409603651670423947251286016 - rule pow96 => 79228162514264337593543950336 - rule pow88 => 309485009821345068724781056 - rule pow80 => 1208925819614629174706176 - rule pow72 => 4722366482869645213696 - rule pow64 => 18446744073709551616 - rule pow56 => 72057594037927936 - rule pow48 => 281474976710656 - rule pow40 => 1099511627776 - rule pow32 => 4294967296 - rule pow24 => 16777216 - rule pow16 => 65536 + rule pow5 => 32 rule pow8 => 256 + rule pow16 => 65536 + rule pow24 => 16777216 + rule pow32 => 4294967296 + rule pow40 => 1099511627776 + rule pow48 => 281474976710656 + rule pow56 => 72057594037927936 + rule pow64 => 18446744073709551616 + rule pow72 => 4722366482869645213696 + rule pow80 => 1208925819614629174706176 + rule pow88 => 309485009821345068724781056 + rule pow96 => 79228162514264337593543950336 + rule pow104 => 20282409603651670423947251286016 + rule pow112 => 5192296858534827628530496329220096 + rule pow120 => 1329227995784915872903807060280344576 + rule pow128 => 340282366920938463463374607431768211456 + rule pow136 => 87112285931760246646623899502532662132736 + rule pow144 => 22300745198530623141535718272648361505980416 + rule pow152 => 5708990770823839524233143877797980545530986496 + rule pow160 => 1461501637330902918203684832716283019655932542976 + rule pow168 => 374144419156711147060143317175368453031918731001856 + rule pow176 => 95780971304118053647396689196894323976171195136475136 + rule pow184 => 24519928653854221733733552434404946937899825954937634816 + rule pow192 => 6277101735386680763835789423207666416102355444464034512896 + rule pow200 => 1606938044258990275541962092341162602522202993782792835301376 + rule pow208 => 411376139330301510538742295639337626245683966408394965837152256 + rule pow216 => 105312291668557186697918027683670432318895095400549111254310977536 + rule pow224 => 26959946667150639794667015087019630673637144422540572481103610249216 + rule pow232 => 6901746346790563787434755862277025452451108972170386555162524223799296 + rule pow240 => 1766847064778384329583297500742918515827483896875618958121606201292619776 + rule pow248 => 452312848583266388373324160190187140051835877600158453279131187530910662656 + rule pow255 => 57896044618658097711785492504343953926634992332820282019728792003956564819968 + rule pow256 => 115792089237316195423570985008687907853269984665640564039457584007913129639936 ``` Maximums and minimums @@ -188,6 +190,8 @@ The maximum and minimum values of each type are defined below. | "minSInt256" [alias] | "minSInt256Word" [alias] | "maxSInt256" [alias] + | "minUInt5" [macro] + | "maxUInt5" [alias] | "minUInt8" [macro] | "maxUInt8" [alias] | "minUInt16" [macro] @@ -357,6 +361,8 @@ The maximum and minimum values of each type are defined below. rule minSFixed128x10 => -1701411834604692317316873037158841057280000000000 /* (-2^487 ) * 10^10 */ rule maxSFixed128x10 => 1701411834604692317316873037158841057270000000000 /* ( 2^487 - 1) * 10^10 */ + rule minUInt5 => 0 + rule maxUInt5 => 31 /* 2^5 - 1 */ rule minUInt8 => 0 rule maxUInt8 => 255 /* 2^8 - 1 */ rule minUInt16 => 0 @@ -510,6 +516,7 @@ Range of types rule #rangeSInt ( 248 , X ) => #range ( minSInt248 <= X <= maxSInt248 ) rule #rangeSInt ( 256 , X ) => #range ( minSInt256 <= X <= maxSInt256 ) + rule #rangeUInt ( 5 , X ) => #range ( minUInt5 <= X < pow5 ) rule #rangeUInt ( 8 , X ) => #range ( minUInt8 <= X < pow8 ) rule #rangeUInt ( 16 , X ) => #range ( minUInt16 <= X < pow16 ) rule #rangeUInt ( 24 , X ) => #range ( minUInt24 <= X < pow24 ) diff --git a/kevm-pyk/src/kevm_pyk/kproj/plugin b/kevm-pyk/src/kevm_pyk/kproj/plugin index da834be67f..b42e6ede9f 160000 --- a/kevm-pyk/src/kevm_pyk/kproj/plugin +++ b/kevm-pyk/src/kevm_pyk/kproj/plugin @@ -1 +1 @@ -Subproject commit da834be67f6c0aff11140ddfc0b04561494c14b8 +Subproject commit b42e6ede9f6b72cedabc519810416e2994caad45 diff --git a/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected b/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected index 5018138626..45333622f2 100644 --- a/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected +++ b/kevm-pyk/src/tests/integration/test-data/gas-abstraction.expected @@ -19,66 +19,8 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (344 steps) +│ (445 steps) ├─ 5 -│ k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K -│ pc: 420 -│ callDepth: 0 -│ statusCode: STATUSCODE:StatusCode -│ -┊ constraint: true -┊ subst: { - CONTINUATION <- CONTINUATION:K - EXITCODE_CELL <- EXITCODE_CELL:Int - STATUSCODE <- STATUSCODE:StatusCode - TOUCHEDACCOUNTS_CELL <- TOUCHEDACCOUNTS_CELL:Set - CALLER_ID <- CALLER_ID:Int - ?_VGAS <- ?_VGAS:Int - ?_VCALLGAS <- ?_VCALLGAS:Int - VGAS_2285f3e8 <- ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -157 ) - SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set - REFUND_CELL <- REFUND_CELL:Int - GASPRICE_CELL <- GASPRICE_CELL:Int - ORIGIN_ID <- ORIGIN_ID:Int - BLOCKHASHES_CELL <- BLOCKHASHES_CELL:List - PREVIOUSHASH_CELL <- PREVIOUSHASH_CELL:Int - OMMERSHASH_CELL <- OMMERSHASH_CELL:Int - COINBASE_CELL <- COINBASE_CELL:Int - STATEROOT_CELL <- STATEROOT_CELL:Int - TRANSACTIONSROOT_CELL <- TRANSACTIONSROOT_CELL:Int - RECEIPTSROOT_CELL <- RECEIPTSROOT_CELL:Int - LOGSBLOOM_CELL <- LOGSBLOOM_CELL:Bytes - DIFFICULTY_CELL <- DIFFICULTY_CELL:Int - NUMBER_CELL <- NUMBER_CELL:Int - GASLIMIT_CELL <- GASLIMIT_CELL:Int - GASUSED_CELL <- GASUSED_CELL:Gas - TIMESTAMP_CELL <- TIMESTAMP_CELL:Int - EXTRADATA_CELL <- EXTRADATA_CELL:Bytes - MIXHASH_CELL <- MIXHASH_CELL:Int - BLOCKNONCE_CELL <- BLOCKNONCE_CELL:Int - BASEFEE_CELL <- BASEFEE_CELL:Int - WITHDRAWALSROOT_CELL <- WITHDRAWALSROOT_CELL:Int - OMMERBLOCKHEADERS_CELL <- OMMERBLOCKHEADERS_CELL:JSON - CHAINID_CELL <- CHAINID_CELL:Int - TXORDER_CELL <- TXORDER_CELL:List - TXPENDING_CELL <- TXPENDING_CELL:List - MESSAGES_CELL <- MESSAGES_CELL:MessageCellMap - DEPTH_CELL <- DEPTH_CELL:Int - EXPECTEDREASON_CELL <- EXPECTEDREASON_CELL:Bytes - EXPECTEDDEPTH_CELL <- EXPECTEDDEPTH_CELL:Int - CHECKEDTOPICS_CELL <- CHECKEDTOPICS_CELL:List - CHECKEDDATA_CELL <- CHECKEDDATA_CELL:Bool - EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account - GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int -} -├─ 6 -│ k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K -│ pc: 420 -│ callDepth: 0 -│ statusCode: STATUSCODE:StatusCode -│ -│ (101 steps) -├─ 7 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K │ pc: 808 │ callDepth: 0 @@ -93,7 +35,7 @@ CALLER_ID <- CALLER_ID:Int ?_VGAS <- ?_VGAS:Int ?_VCALLGAS <- ?_VCALLGAS:Int - VGAS_d38c7e07 <- ( VGAS_2285f3e8:Int +Int -45 ) + VGAS_1675167e <- ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -202 ) SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set REFUND_CELL <- REFUND_CELL:Int GASPRICE_CELL <- GASPRICE_CELL:Int @@ -129,21 +71,21 @@ EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int } -├─ 8 +├─ 6 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K │ pc: 808 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) -├─ 9 +├─ 7 │ k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K │ pc: 808 │ callDepth: 0 │ statusCode: EVMC_REVERT │ │ (2 steps) -└─ 10 (leaf, terminal) +└─ 8 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 808 callDepth: 0 @@ -157,7 +99,7 @@ │ statusCode: STATUSCODE_FINAL -Node 10: +Node 8: ( @@ -895,7 +837,8 @@ Node 10: ( #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xed\x9fsS" false ~> #return 128 0 - ~> #pc [ CALL ] => #pc [ JUMPI ] ) + ~> #pc [ CALL ] => #end EVMC_REVERT + ~> #pc [ REVERT ] ) ~> #execute ~> _CONTINUATION @@ -908,7 +851,7 @@ Node 10: - ( _OUTPUT_CELL => b"" ) + ( _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\x01" ) .List @@ -932,10 +875,10 @@ Node 10: 0 - ( ( 132 => ( ( ??_VGAS +Int ??_VCALLGAS ) +Int -127 ) ) : ( ( selector ( "infiniteGas()" ) => 583 ) : ( ( 645326474426547203313410069153905908525362434349 => 928 ) : ( ( 167 => 345 ) : ( ( selector ( "testInfiniteGas()" ) => ( ( ??_VGAS +Int ??_VCALLGAS ) +Int -36 ) ) : ( .WordStack => ( 167 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) + ( ( 132 => 428 ) : ( ( selector ( "infiniteGas()" ) => ( ( ??_VGAS +Int ??_VCALLGAS ) +Int -127 ) ) : ( ( 645326474426547203313410069153905908525362434349 => 583 ) : ( ( 167 => 928 ) : ( ( selector ( "testInfiniteGas()" ) => 345 ) : ( .WordStack => ( ( ( ??_VGAS +Int ??_VCALLGAS ) +Int -36 ) : ( 167 : ( selector ( "testInfiniteGas()" ) : .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\xed\x9fsS\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" + ( 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\xed\x9fsS\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => 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\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\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\xed\x9fsS\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) ... ... @@ -1100,214 +1043,6 @@ Node 10: [label(BASIC-BLOCK-4-TO-5)] rule [BASIC-BLOCK-6-TO-7]: - - - ( #pc [ JUMPI ] => #end EVMC_REVERT - ~> #pc [ REVERT ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - ( 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" ) - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"c\xfe\xc36" - - - 0 - - - ( ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -127 ) => 428 ) : ( ( 583 => ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -127 ) ) : ( ( 928 => 583 ) : ( ( 345 => 928 ) : ( ( ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -36 ) => 345 ) : ( ( 167 => ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) +Int -36 ) ) : ( ( selector ( "testInfiniteGas()" ) => 167 ) : ( .WordStack => ( selector ( "testInfiniteGas()" ) : .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\xed\x9fsS\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => 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\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\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\xed\x9fsS\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) - - ... - ... - - 5 - - - #gas ( ?_VCALLGAS:Int ) - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( CALLER_ID:Int ( #end EVMC_REVERT => #halt ) @@ -1516,9 +1251,9 @@ Node 10: andBool ( NUMBER_CELL:Int <=Int maxSInt256 andBool ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) + rule [BASIC-BLOCK-7-TO-8]: #halt @@ -1727,14 +1462,14 @@ Node 10: andBool ( NUMBER_CELL:Int <=Int maxSInt256 andBool ( ( ?_VGAS:Int +Int ?_VCALLGAS:Int ) #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K - │ pc: 1539 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (12 steps) - ├─ 11 - │ k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ... - │ pc: 1569 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (5 steps) - ├─ 13 - │ k: #execute ~> CONTINUATION:K - │ pc: 1571 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (2 steps) - ├─ 14 - │ k: #execute ~> CONTINUATION:K - │ pc: 1572 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (9 steps) - ├─ 15 - │ k: #access [ POP , POP 0 ] ~> POP 0 ~> #pc [ POP ] ~> #execute ~> CONTINUATION:K - │ pc: 1572 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (12 steps) - ├─ 16 - │ k: #access [ POP , POP 0 ] ~> POP 0 ~> #pc [ POP ] ~> #execute ~> CONTINUATION:K - │ pc: 1573 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (12 steps) - ├─ 17 - │ k: #access [ JUMP , JUMP 334 ] ~> JUMP 334 ~> #pc [ JUMP ] ~> #execute ~> CONTINUAT ... - │ pc: 1574 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (13 steps) - ├─ 18 - │ k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ... - │ pc: 334 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (5 steps) - ├─ 19 - │ k: #execute ~> CONTINUATION:K - │ pc: 337 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (12 steps) - ├─ 20 - │ k: #access [ MLOAD , MLOAD 64 ] ~> MLOAD 64 ~> #pc [ MLOAD ] ~> #execute ~> CONTINU ... - │ pc: 337 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (6 steps) - ├─ 21 - │ k: #execute ~> CONTINUATION:K - │ pc: 339 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (2 steps) - ├─ 22 - │ k: #execute ~> CONTINUATION:K - │ pc: 340 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (12 steps) - ├─ 23 - │ k: #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int + ... - │ pc: 340 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (5 steps) - ├─ 24 - │ k: #execute ~> CONTINUATION:K - │ pc: 343 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (2 steps) - ├─ 25 - │ k: #execute ~> CONTINUATION:K - │ pc: 344 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (9 steps) - ├─ 26 - │ k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ... - │ pc: 344 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (5 steps) - ├─ 27 - │ k: #execute ~> CONTINUATION:K - │ pc: 347 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (12 steps) - ├─ 28 - │ k: #access [ MLOAD , MLOAD 64 ] ~> MLOAD 64 ~> #pc [ MLOAD ] ~> #execute ~> CONTINU ... - │ pc: 347 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (6 steps) - ├─ 29 - │ k: #execute ~> CONTINUATION:K - │ pc: 349 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (2 steps) - ├─ 30 - │ k: #execute ~> CONTINUATION:K - │ pc: 350 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (2 steps) - ├─ 31 - │ k: #execute ~> CONTINUATION:K - │ pc: 351 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (2 steps) - ├─ 32 - │ k: #execute ~> CONTINUATION:K - │ pc: 352 - │ callDepth: 0 - │ statusCode: STATUSCODE:StatusCode - │ - │ (14 steps) - ├─ 33 │ k: #end EVMC_SUCCESS ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K │ pc: 352 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) - ├─ 34 + ├─ 11 │ k: #halt ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K │ pc: 352 │ callDepth: 0 │ statusCode: EVMC_SUCCESS │ │ (2 steps) - ├─ 35 (terminal) + ├─ 13 (terminal) │ k: #halt ~> CONTINUATION:K │ pc: 352 │ callDepth: 0 @@ -1116,8 +962,9 @@ rule [BASIC-BLOCK-7-TO-9]: - ( JUMPI 1569 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) => JUMP 1569 ) - ~> #pc [ JUMPI ] + ( JUMPI 1569 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) + ~> #pc [ JUMPI ] => #end EVMC_SUCCESS + ~> #pc [ RETURN ] ) ~> #execute ~> _CONTINUATION @@ -1130,7 +977,7 @@ - b"" + ( b"" => #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) ) .List @@ -1154,10 +1001,10 @@ 0 - ( ( 0 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( 0 : ( ( VV0_n_114b9705:Int => 0 ) : ( 334 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) + ( ( 0 => selector ( "sum_N(uint256)" ) ) : ( ( 0 : ( VV0_n_114b9705:Int : ( 334 : ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + ( 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\x00Lc\xe5b" => 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" ) +Bytes ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) => #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) ) ... ... @@ -1324,10 +1171,31 @@ )))))))))) ensures ( VV0_n_114b9705:Int =/=K 0 andBool ( 0 @@ -1544,10 +1412,8 @@ rule [BASIC-BLOCK-9-TO-11]: - ( JUMP 1569 - ~> #pc [ JUMPI ] => #access [ JUMPDEST , JUMPDEST ] - ~> JUMPDEST - ~> #pc [ JUMPDEST ] ) + ( #end EVMC_SUCCESS => #halt ) + ~> #pc [ RETURN ] ~> #execute ~> _CONTINUATION @@ -1560,8 +1426,11 @@ - b"" + #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) + + ( _STATUSCODE => EVMC_SUCCESS ) + .List @@ -1584,10 +1453,10 @@ 0 - ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( 0 : ( 0 : ( 334 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) + ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) ... ... @@ -1751,12 +1620,32 @@ andBool ( ORIGIN_ID:Int @@ -1973,10 +1862,9 @@ rule [BASIC-BLOCK-11-TO-13]: - ( #access [ JUMPDEST , JUMPDEST ] - ~> JUMPDEST - ~> #pc [ JUMPDEST ] => .K ) - ~> #execute + #halt + ~> ( #pc [ RETURN ] + ~> #execute => .K ) ~> _CONTINUATION @@ -1988,8 +1876,11 @@ - b"" + #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) + + EVMC_SUCCESS + .List @@ -2012,10 +1903,10 @@ 0 - ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 334 ) : ( 0 : ( 0 : ( ( 334 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) ) + ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) + 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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) ... ... @@ -2179,5046 +2070,33 @@ andBool ( ORIGIN_ID:Int - - - #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 334 => 0 ) : ( 0 : ( ( 0 => 334 ) : ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( .K => #access [ POP , POP 0 ] - ~> POP 0 - ~> #pc [ POP ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( 0 : ( ( 0 => 334 ) : ( ( 334 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - #access [ POP , POP 0 ] - ~> POP 0 - ~> #pc [ POP ] - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 0 => 334 ) : ( ( 334 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #access [ POP , POP 0 ] - ~> POP 0 - ~> #pc [ POP ] => #access [ JUMP , JUMP 334 ] - ~> JUMP 334 - ~> #pc [ JUMP ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 334 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #access [ JUMP , JUMP 334 ] - ~> JUMP 334 - ~> #pc [ JUMP ] => #access [ JUMPDEST , JUMPDEST ] - ~> JUMPDEST - ~> #pc [ JUMPDEST ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #access [ JUMPDEST , JUMPDEST ] - ~> JUMPDEST - ~> #pc [ JUMPDEST ] => .K ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 64 ) : ( ( selector ( "sum_N(uint256)" ) => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( .WordStack => ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( .K => #access [ MLOAD , MLOAD 64 ] - ~> MLOAD 64 - ~> #pc [ MLOAD ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 64 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #access [ MLOAD , MLOAD 64 ] - ~> MLOAD 64 - ~> #pc [ MLOAD ] => .K ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 128 ) : ( ( 128 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( .K => #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ] - ~> MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) - ~> #pc [ MSTORE ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( 128 : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( 128 : ( selector ( "sum_N(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\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ] - ~> MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) - ~> #pc [ MSTORE ] => .K ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 128 => 32 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(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\x00Lc\xe5b" => 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" ) +Bytes ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) => #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 32 => 160 ) : ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(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\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( .K => #access [ JUMPDEST , JUMPDEST ] - ~> JUMPDEST - ~> #pc [ JUMPDEST ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( 160 : ( selector ( "sum_N(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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #access [ JUMPDEST , JUMPDEST ] - ~> JUMPDEST - ~> #pc [ JUMPDEST ] => .K ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 160 => 64 ) : ( ( selector ( "sum_N(uint256)" ) => 160 ) : ( .WordStack => ( selector ( "sum_N(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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( .K => #access [ MLOAD , MLOAD 64 ] - ~> MLOAD 64 - ~> #pc [ MLOAD ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 64 => 160 ) : ( ( 160 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(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\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #access [ MLOAD , MLOAD 64 ] - ~> MLOAD 64 - ~> #pc [ MLOAD ] => .K ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 160 => 128 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( 160 : ( selector ( "sum_N(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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 128 => 160 ) : ( 128 : ( ( 160 => 128 ) : ( selector ( "sum_N(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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 160 => 32 ) : ( 128 : ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(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\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 32 => 128 ) : ( ( 128 => 32 ) : ( selector ( "sum_N(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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( .K => #end EVMC_SUCCESS - ~> #pc [ RETURN ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - ( b"" => #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) ) - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( 32 : ( selector ( "sum_N(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\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - ( #end EVMC_SUCCESS => #halt ) - ~> #pc [ RETURN ] - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) - - - ( _STATUSCODE => EVMC_SUCCESS ) - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( selector ( "sum_N(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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 - - - #halt - ~> ( #pc [ RETURN ] - ~> #execute => .K ) - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - - - #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) - - - EVMC_SUCCESS - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int ) - - - 0 - - - ( selector ( "sum_N(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" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes #range ( #buf ( 32 , bool2Word ( VV0_n_114b9705:Int <=Int 51816696836262767 ) ) , 28 , 4 ) - - ... - ... - - 6 - - - 9079256848778916870 - - - false - - - 0 - - - - - .List - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( VV0_n_114b9705:Int =/=K 0 - andBool ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0