diff --git a/.gitignore b/.gitignore index bccb8eddfb..859f6eae87 100644 --- a/.gitignore +++ b/.gitignore @@ -20,3 +20,4 @@ /tests/vm/*.out .DS_Store .idea/ +.vscode/ diff --git a/deps/blockchain-k-plugin_release b/deps/blockchain-k-plugin_release index 5a9e45b5d3..02e3cbf46a 100644 --- a/deps/blockchain-k-plugin_release +++ b/deps/blockchain-k-plugin_release @@ -1 +1 @@ -f1f7edb7cb7286906fe42aa37d2106036cef849f +3492f6deff69f11b64e700cdb6305024fc0fac84 diff --git a/deps/k_release b/deps/k_release index 67639f4f28..f1dc680537 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.142 +7.1.156 diff --git a/flake.lock b/flake.lock index 8a990aa489..283ddc981a 100644 --- a/flake.lock +++ b/flake.lock @@ -45,17 +45,17 @@ "xbyak": "xbyak" }, "locked": { - "lastModified": 1726502502, - "narHash": "sha256-J9IJiXHyCh42z65mEHYj/gnSLxOxbOF0riX8SLlQ3l8=", + "lastModified": 1727733679, + "narHash": "sha256-bk4pBo1mIjze8QOwCMRH6uiUCi2zY5F4Ep3aYCT01Mg=", "owner": "runtimeverification", "repo": "blockchain-k-plugin", - "rev": "f1f7edb7cb7286906fe42aa37d2106036cef849f", + "rev": "3492f6deff69f11b64e700cdb6305024fc0fac84", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "blockchain-k-plugin", - "rev": "f1f7edb7cb7286906fe42aa37d2106036cef849f", + "rev": "3492f6deff69f11b64e700cdb6305024fc0fac84", "type": "github" } }, @@ -316,16 +316,16 @@ ] }, "locked": { - "lastModified": 1726170219, - "narHash": "sha256-pQG1D9oDG24h7I/ekTI96IGZ7ikWrip0m4o1uDFIBZc=", + "lastModified": 1727294569, + "narHash": "sha256-0acBhM4McFJ93BO0pamzHr6ekLWgiH4gvw2428JX7wY=", "owner": "runtimeverification", "repo": "k", - "rev": "6e23a83e5380f9eae45a73e3956776f2e666da35", + "rev": "d0d2553f1254991600a830b108d98fe9febc1f5a", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.142", + "ref": "v7.1.151", "repo": "k", "type": "github" } @@ -352,16 +352,16 @@ ] }, "locked": { - "lastModified": 1726170219, - "narHash": "sha256-pQG1D9oDG24h7I/ekTI96IGZ7ikWrip0m4o1uDFIBZc=", + "lastModified": 1728459307, + "narHash": "sha256-OgaFqZODgQyG1ufJH+xEVmEKD6eyrO7JPJb9UQfbI8M=", "owner": "runtimeverification", "repo": "k", - "rev": "6e23a83e5380f9eae45a73e3956776f2e666da35", + "rev": "76c534f16df17febd4560e9b492cfa024d82e9b0", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.142", + "ref": "v7.1.156", "repo": "k", "type": "github" } @@ -401,16 +401,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1726098480, - "narHash": "sha256-BOCKGOKzJLlYHSOCd2QOERS/sE038domlBc1h6nvM5s=", + "lastModified": 1727116141, + "narHash": "sha256-htGQy05VRhuAWdMkUzCf67gkKRGSHfJUeXU5bc2Z27Q=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "344d1335c0fb8d146b0fa2954b0194afbe11dae6", + "rev": "b830daaa6392ff256e62970cab89deeaaf7aab95", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.88", + "ref": "v0.1.95", "repo": "llvm-backend", "type": "github" } @@ -432,16 +432,16 @@ "utils": "utils_2" }, "locked": { - "lastModified": 1726098480, - "narHash": "sha256-BOCKGOKzJLlYHSOCd2QOERS/sE038domlBc1h6nvM5s=", + "lastModified": 1727813652, + "narHash": "sha256-x29OdXQARnaith+dz88R3O056tlJcC4VqFbFzlbqLEc=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "344d1335c0fb8d146b0fa2954b0194afbe11dae6", + "rev": "812ea2ad00c91b7b5d144bd2624c7293802db45f", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.88", + "ref": "v0.1.98", "repo": "llvm-backend", "type": "github" } diff --git a/flake.nix b/flake.nix index 556b138283..4a6a37bd72 100644 --- a/flake.nix +++ b/flake.nix @@ -2,14 +2,14 @@ description = "A flake for the KEVM Semantics"; inputs = { - k-framework.url = "github:runtimeverification/k/v7.1.142"; + k-framework.url = "github:runtimeverification/k/v7.1.156"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; poetry2nix.follows = "k-framework/poetry2nix"; blockchain-k-plugin = { url = - "github:runtimeverification/blockchain-k-plugin/f1f7edb7cb7286906fe42aa37d2106036cef849f"; + "github:runtimeverification/blockchain-k-plugin/3492f6deff69f11b64e700cdb6305024fc0fac84"; inputs.flake-utils.follows = "k-framework/flake-utils"; inputs.nixpkgs.follows = "k-framework/nixpkgs"; }; diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index bcb11ec4a6..f1778cf1a2 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -36,33 +36,33 @@ tomli = {version = ">=2.0.1", markers = "python_version < \"3.11\""} [[package]] name = "black" -version = "24.8.0" +version = "24.10.0" description = "The uncompromising code formatter." optional = false -python-versions = ">=3.8" +python-versions = ">=3.9" files = [ - {file = "black-24.8.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:09cdeb74d494ec023ded657f7092ba518e8cf78fa8386155e4a03fdcc44679e6"}, - {file = "black-24.8.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:81c6742da39f33b08e791da38410f32e27d632260e599df7245cccee2064afeb"}, - {file = "black-24.8.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:707a1ca89221bc8a1a64fb5e15ef39cd755633daa672a9db7498d1c19de66a42"}, - {file = "black-24.8.0-cp310-cp310-win_amd64.whl", hash = "sha256:d6417535d99c37cee4091a2f24eb2b6d5ec42b144d50f1f2e436d9fe1916fe1a"}, - {file = "black-24.8.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:fb6e2c0b86bbd43dee042e48059c9ad7830abd5c94b0bc518c0eeec57c3eddc1"}, - {file = "black-24.8.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:837fd281f1908d0076844bc2b801ad2d369c78c45cf800cad7b61686051041af"}, - {file = "black-24.8.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:62e8730977f0b77998029da7971fa896ceefa2c4c4933fcd593fa599ecbf97a4"}, - {file = "black-24.8.0-cp311-cp311-win_amd64.whl", hash = "sha256:72901b4913cbac8972ad911dc4098d5753704d1f3c56e44ae8dce99eecb0e3af"}, - {file = "black-24.8.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:7c046c1d1eeb7aea9335da62472481d3bbf3fd986e093cffd35f4385c94ae368"}, - {file = "black-24.8.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:649f6d84ccbae73ab767e206772cc2d7a393a001070a4c814a546afd0d423aed"}, - {file = "black-24.8.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:2b59b250fdba5f9a9cd9d0ece6e6d993d91ce877d121d161e4698af3eb9c1018"}, - {file = "black-24.8.0-cp312-cp312-win_amd64.whl", hash = "sha256:6e55d30d44bed36593c3163b9bc63bf58b3b30e4611e4d88a0c3c239930ed5b2"}, - {file = "black-24.8.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:505289f17ceda596658ae81b61ebbe2d9b25aa78067035184ed0a9d855d18afd"}, - {file = "black-24.8.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:b19c9ad992c7883ad84c9b22aaa73562a16b819c1d8db7a1a1a49fb7ec13c7d2"}, - {file = "black-24.8.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:1f13f7f386f86f8121d76599114bb8c17b69d962137fc70efe56137727c7047e"}, - {file = "black-24.8.0-cp38-cp38-win_amd64.whl", hash = "sha256:f490dbd59680d809ca31efdae20e634f3fae27fba3ce0ba3208333b713bc3920"}, - {file = "black-24.8.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:eab4dd44ce80dea27dc69db40dab62d4ca96112f87996bca68cd75639aeb2e4c"}, - {file = "black-24.8.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:3c4285573d4897a7610054af5a890bde7c65cb466040c5f0c8b732812d7f0e5e"}, - {file = "black-24.8.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:9e84e33b37be070ba135176c123ae52a51f82306def9f7d063ee302ecab2cf47"}, - {file = "black-24.8.0-cp39-cp39-win_amd64.whl", hash = "sha256:73bbf84ed136e45d451a260c6b73ed674652f90a2b3211d6a35e78054563a9bb"}, - {file = "black-24.8.0-py3-none-any.whl", hash = "sha256:972085c618ee94f402da1af548a4f218c754ea7e5dc70acb168bfaca4c2542ed"}, - {file = "black-24.8.0.tar.gz", hash = "sha256:2500945420b6784c38b9ee885af039f5e7471ef284ab03fa35ecdde4688cd83f"}, + {file = "black-24.10.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:e6668650ea4b685440857138e5fe40cde4d652633b1bdffc62933d0db4ed9812"}, + {file = "black-24.10.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:1c536fcf674217e87b8cc3657b81809d3c085d7bf3ef262ead700da345bfa6ea"}, + {file = "black-24.10.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:649fff99a20bd06c6f727d2a27f401331dc0cc861fb69cde910fe95b01b5928f"}, + {file = "black-24.10.0-cp310-cp310-win_amd64.whl", hash = "sha256:fe4d6476887de70546212c99ac9bd803d90b42fc4767f058a0baa895013fbb3e"}, + {file = "black-24.10.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:5a2221696a8224e335c28816a9d331a6c2ae15a2ee34ec857dcf3e45dbfa99ad"}, + {file = "black-24.10.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:f9da3333530dbcecc1be13e69c250ed8dfa67f43c4005fb537bb426e19200d50"}, + {file = "black-24.10.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:4007b1393d902b48b36958a216c20c4482f601569d19ed1df294a496eb366392"}, + {file = "black-24.10.0-cp311-cp311-win_amd64.whl", hash = "sha256:394d4ddc64782e51153eadcaaca95144ac4c35e27ef9b0a42e121ae7e57a9175"}, + {file = "black-24.10.0-cp312-cp312-macosx_10_13_x86_64.whl", hash = "sha256:b5e39e0fae001df40f95bd8cc36b9165c5e2ea88900167bddf258bacef9bbdc3"}, + {file = "black-24.10.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:d37d422772111794b26757c5b55a3eade028aa3fde43121ab7b673d050949d65"}, + {file = "black-24.10.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:14b3502784f09ce2443830e3133dacf2c0110d45191ed470ecb04d0f5f6fcb0f"}, + {file = "black-24.10.0-cp312-cp312-win_amd64.whl", hash = "sha256:30d2c30dc5139211dda799758559d1b049f7f14c580c409d6ad925b74a4208a8"}, + {file = "black-24.10.0-cp313-cp313-macosx_10_13_x86_64.whl", hash = "sha256:1cbacacb19e922a1d75ef2b6ccaefcd6e93a2c05ede32f06a21386a04cedb981"}, + {file = "black-24.10.0-cp313-cp313-macosx_11_0_arm64.whl", hash = "sha256:1f93102e0c5bb3907451063e08b9876dbeac810e7da5a8bfb7aeb5a9ef89066b"}, + {file = "black-24.10.0-cp313-cp313-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ddacb691cdcdf77b96f549cf9591701d8db36b2f19519373d60d31746068dbf2"}, + {file = "black-24.10.0-cp313-cp313-win_amd64.whl", hash = "sha256:680359d932801c76d2e9c9068d05c6b107f2584b2a5b88831c83962eb9984c1b"}, + {file = "black-24.10.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:17374989640fbca88b6a448129cd1745c5eb8d9547b464f281b251dd00155ccd"}, + {file = "black-24.10.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:63f626344343083322233f175aaf372d326de8436f5928c042639a4afbbf1d3f"}, + {file = "black-24.10.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ccfa1d0cb6200857f1923b602f978386a3a2758a65b52e0950299ea014be6800"}, + {file = "black-24.10.0-cp39-cp39-win_amd64.whl", hash = "sha256:2cd9c95431d94adc56600710f8813ee27eea544dd118d45896bb734e9d7a0dc7"}, + {file = "black-24.10.0-py3-none-any.whl", hash = "sha256:3bb2b7a1f7b685f85b11fed1ef10f8a9148bceb49853e47a294a3dd963c1dd7d"}, + {file = "black-24.10.0.tar.gz", hash = "sha256:846ea64c97afe3bc677b761787993be4991810ecc7a4a937816dd6bddedc4875"}, ] [package.dependencies] @@ -76,7 +76,7 @@ typing-extensions = {version = ">=4.0.1", markers = "python_version < \"3.11\""} [package.extras] colorama = ["colorama (>=0.4.3)"] -d = ["aiohttp (>=3.7.4)", "aiohttp (>=3.7.4,!=3.9.0)"] +d = ["aiohttp (>=3.10)"] jupyter = ["ipython (>=7.8.0)", "tokenize-rt (>=3.2.0)"] uvloop = ["uvloop (>=0.15.2)"] @@ -244,13 +244,13 @@ toml = ["tomli"] [[package]] name = "dill" -version = "0.3.8" +version = "0.3.9" description = "serialize all of Python" optional = false python-versions = ">=3.8" files = [ - {file = "dill-0.3.8-py3-none-any.whl", hash = "sha256:c36ca9ffb54365bdd2f8eb3eff7d2a21237f8452b57ace88b1ac615b7e815bd7"}, - {file = "dill-0.3.8.tar.gz", hash = "sha256:3ebe3c479ad625c4553aca177444d89b486b1d84982eeacded644afc0cf797ca"}, + {file = "dill-0.3.9-py3-none-any.whl", hash = "sha256:468dff3b89520b474c0397703366b7b95eebe6303f108adf9b19da1f702be87a"}, + {file = "dill-0.3.9.tar.gz", hash = "sha256:81aa267dddf68cbfe8029c42ca9ec6a4ab3b22371d1c450abc54422577b4512c"}, ] [package.extras] @@ -287,18 +287,18 @@ testing = ["hatch", "pre-commit", "pytest", "tox"] [[package]] name = "filelock" -version = "3.16.0" +version = "3.16.1" description = "A platform independent file lock." optional = false python-versions = ">=3.8" files = [ - {file = "filelock-3.16.0-py3-none-any.whl", hash = "sha256:f6ed4c963184f4c84dd5557ce8fece759a3724b37b80c6c4f20a2f63a4dc6609"}, - {file = "filelock-3.16.0.tar.gz", hash = "sha256:81de9eb8453c769b63369f87f11131a7ab04e367f8d97ad39dc230daa07e3bec"}, + {file = "filelock-3.16.1-py3-none-any.whl", hash = "sha256:2082e5703d51fbf98ea75855d9d5527e33d8ff23099bec374a134febee6946b0"}, + {file = "filelock-3.16.1.tar.gz", hash = "sha256:c249fbfcd5db47e5e2d6d62198e565475ee65e4831e2561c8e313fa7eb961435"}, ] [package.extras] -docs = ["furo (>=2024.8.6)", "sphinx (>=8.0.2)", "sphinx-autodoc-typehints (>=2.4)"] -testing = ["covdefaults (>=2.3)", "coverage (>=7.6.1)", "diff-cover (>=9.1.1)", "pytest (>=8.3.2)", "pytest-asyncio (>=0.24)", "pytest-cov (>=5)", "pytest-mock (>=3.14)", "pytest-timeout (>=2.3.1)", "virtualenv (>=20.26.3)"] +docs = ["furo (>=2024.8.6)", "sphinx (>=8.0.2)", "sphinx-autodoc-typehints (>=2.4.1)"] +testing = ["covdefaults (>=2.3)", "coverage (>=7.6.1)", "diff-cover (>=9.2)", "pytest (>=8.3.3)", "pytest-asyncio (>=0.24)", "pytest-cov (>=5)", "pytest-mock (>=3.14)", "pytest-timeout (>=2.3.1)", "virtualenv (>=20.26.4)"] typing = ["typing-extensions (>=4.12.2)"] [[package]] @@ -410,13 +410,13 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "hypothesis" -version = "6.112.1" +version = "6.113.0" description = "A library for property-based testing" optional = false python-versions = ">=3.8" files = [ - {file = "hypothesis-6.112.1-py3-none-any.whl", hash = "sha256:93631b1498b20d2c205ed304cbd41d50e9c069d78a9c773c1324ca094c5e30ce"}, - {file = "hypothesis-6.112.1.tar.gz", hash = "sha256:b070d7a1bb9bd84706c31885c9aeddc138e2b36a9c112a91984f49501c567856"}, + {file = "hypothesis-6.113.0-py3-none-any.whl", hash = "sha256:d539180eb2bb71ed28a23dfe94e67c851f9b09f3ccc4125afad43f17e32e2bad"}, + {file = "hypothesis-6.113.0.tar.gz", hash = "sha256:5556ac66fdf72a4ccd5d237810f7cf6bdcd00534a4485015ef881af26e20f7c7"}, ] [package.dependencies] @@ -425,10 +425,10 @@ exceptiongroup = {version = ">=1.0.0", markers = "python_version < \"3.11\""} sortedcontainers = ">=2.1.0,<3.0.0" [package.extras] -all = ["backports.zoneinfo (>=0.2.1)", "black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.70)", "django (>=3.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.13)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.17.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.1)"] +all = ["backports.zoneinfo (>=0.2.1)", "black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.73)", "django (>=3.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.14)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.17.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.2)"] cli = ["black (>=19.10b0)", "click (>=7.0)", "rich (>=9.0.0)"] codemods = ["libcst (>=0.3.16)"] -crosshair = ["crosshair-tool (>=0.0.70)", "hypothesis-crosshair (>=0.0.13)"] +crosshair = ["crosshair-tool (>=0.0.73)", "hypothesis-crosshair (>=0.0.14)"] dateutil = ["python-dateutil (>=1.4)"] django = ["django (>=3.2)"] dpcontracts = ["dpcontracts (>=0.4)"] @@ -439,7 +439,7 @@ pandas = ["pandas (>=1.1)"] pytest = ["pytest (>=4.6)"] pytz = ["pytz (>=2014.1)"] redis = ["redis (>=3.0.0)"] -zoneinfo = ["backports.zoneinfo (>=0.2.1)", "tzdata (>=2024.1)"] +zoneinfo = ["backports.zoneinfo (>=0.2.1)", "tzdata (>=2024.2)"] [[package]] name = "importlib-metadata" @@ -505,13 +505,13 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kframework" -version = "7.1.142" +version = "7.1.156" description = "" optional = false python-versions = "<4.0,>=3.10" files = [ - {file = "kframework-7.1.142-py3-none-any.whl", hash = "sha256:41dc2f26ea3acff1d79fd6e87519cedba94f3a9de8e313066a7fbb7654710c4c"}, - {file = "kframework-7.1.142.tar.gz", hash = "sha256:e55b516f8c5ecf0b1d166b89f3845b4207f07b86fa5843d8f0aab4cb9a9888ef"}, + {file = "kframework-7.1.156-py3-none-any.whl", hash = "sha256:3dfd7f4c27cf36f9ee07e1ff3163b436776739dd190a6a060125ed35a7671149"}, + {file = "kframework-7.1.156.tar.gz", hash = "sha256:1cec1caf7e9e1ba5837937436e961079013de355229e0d8da955db0dea65fc50"}, ] [package.dependencies] @@ -616,27 +616,31 @@ files = [ [[package]] name = "multiprocess" -version = "0.70.16" +version = "0.70.17" description = "better multiprocessing and multithreading in Python" optional = false python-versions = ">=3.8" files = [ - {file = "multiprocess-0.70.16-pp310-pypy310_pp73-macosx_10_13_x86_64.whl", hash = "sha256:476887be10e2f59ff183c006af746cb6f1fd0eadcfd4ef49e605cbe2659920ee"}, - {file = "multiprocess-0.70.16-pp310-pypy310_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:d951bed82c8f73929ac82c61f01a7b5ce8f3e5ef40f5b52553b4f547ce2b08ec"}, - {file = "multiprocess-0.70.16-pp38-pypy38_pp73-macosx_10_9_x86_64.whl", hash = "sha256:37b55f71c07e2d741374998c043b9520b626a8dddc8b3129222ca4f1a06ef67a"}, - {file = "multiprocess-0.70.16-pp38-pypy38_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:ba8c31889abf4511c7308a8c52bb4a30b9d590e7f58523302ba00237702ca054"}, - {file = "multiprocess-0.70.16-pp39-pypy39_pp73-macosx_10_13_x86_64.whl", hash = "sha256:0dfd078c306e08d46d7a8d06fb120313d87aa43af60d66da43ffff40b44d2f41"}, - {file = "multiprocess-0.70.16-pp39-pypy39_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:e7b9d0f307cd9bd50851afaac0dba2cb6c44449efff697df7c7645f7d3f2be3a"}, - {file = "multiprocess-0.70.16-py310-none-any.whl", hash = "sha256:c4a9944c67bd49f823687463660a2d6daae94c289adff97e0f9d696ba6371d02"}, - {file = "multiprocess-0.70.16-py311-none-any.whl", hash = "sha256:af4cabb0dac72abfb1e794fa7855c325fd2b55a10a44628a3c1ad3311c04127a"}, - {file = "multiprocess-0.70.16-py312-none-any.whl", hash = "sha256:fc0544c531920dde3b00c29863377f87e1632601092ea2daca74e4beb40faa2e"}, - {file = "multiprocess-0.70.16-py38-none-any.whl", hash = "sha256:a71d82033454891091a226dfc319d0cfa8019a4e888ef9ca910372a446de4435"}, - {file = "multiprocess-0.70.16-py39-none-any.whl", hash = "sha256:a0bafd3ae1b732eac64be2e72038231c1ba97724b60b09400d68f229fcc2fbf3"}, - {file = "multiprocess-0.70.16.tar.gz", hash = "sha256:161af703d4652a0e1410be6abccecde4a7ddffd19341be0a7011b94aeb171ac1"}, + {file = "multiprocess-0.70.17-pp310-pypy310_pp73-macosx_10_15_x86_64.whl", hash = "sha256:7ddb24e5bcdb64e90ec5543a1f05a39463068b6d3b804aa3f2a4e16ec28562d6"}, + {file = "multiprocess-0.70.17-pp310-pypy310_pp73-macosx_11_0_arm64.whl", hash = "sha256:d729f55198a3579f6879766a6d9b72b42d4b320c0dcb7844afb774d75b573c62"}, + {file = "multiprocess-0.70.17-pp310-pypy310_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:c2c82d0375baed8d8dd0d8c38eb87c5ae9c471f8e384ad203a36f095ee860f67"}, + {file = "multiprocess-0.70.17-pp38-pypy38_pp73-macosx_10_9_arm64.whl", hash = "sha256:a22a6b1a482b80eab53078418bb0f7025e4f7d93cc8e1f36481477a023884861"}, + {file = "multiprocess-0.70.17-pp38-pypy38_pp73-macosx_10_9_x86_64.whl", hash = "sha256:349525099a0c9ac5936f0488b5ee73199098dac3ac899d81d326d238f9fd3ccd"}, + {file = "multiprocess-0.70.17-pp38-pypy38_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:27b8409c02b5dd89d336107c101dfbd1530a2cd4fd425fc27dcb7adb6e0b47bf"}, + {file = "multiprocess-0.70.17-pp39-pypy39_pp73-macosx_10_13_arm64.whl", hash = "sha256:2ea0939b0f4760a16a548942c65c76ff5afd81fbf1083c56ae75e21faf92e426"}, + {file = "multiprocess-0.70.17-pp39-pypy39_pp73-macosx_10_13_x86_64.whl", hash = "sha256:2b12e081df87ab755190e227341b2c3b17ee6587e9c82fecddcbe6aa812cd7f7"}, + {file = "multiprocess-0.70.17-pp39-pypy39_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:a0f01cd9d079af7a8296f521dc03859d1a414d14c1e2b6e676ef789333421c95"}, + {file = "multiprocess-0.70.17-py310-none-any.whl", hash = "sha256:38357ca266b51a2e22841b755d9a91e4bb7b937979a54d411677111716c32744"}, + {file = "multiprocess-0.70.17-py311-none-any.whl", hash = "sha256:2884701445d0177aec5bd5f6ee0df296773e4fb65b11903b94c613fb46cfb7d1"}, + {file = "multiprocess-0.70.17-py312-none-any.whl", hash = "sha256:2818af14c52446b9617d1b0755fa70ca2f77c28b25ed97bdaa2c69a22c47b46c"}, + {file = "multiprocess-0.70.17-py313-none-any.whl", hash = "sha256:20c28ca19079a6c879258103a6d60b94d4ffe2d9da07dda93fb1c8bc6243f522"}, + {file = "multiprocess-0.70.17-py38-none-any.whl", hash = "sha256:1d52f068357acd1e5bbc670b273ef8f81d57863235d9fbf9314751886e141968"}, + {file = "multiprocess-0.70.17-py39-none-any.whl", hash = "sha256:c3feb874ba574fbccfb335980020c1ac631fbf2a3f7bee4e2042ede62558a021"}, + {file = "multiprocess-0.70.17.tar.gz", hash = "sha256:4ae2f11a3416809ebc9a48abfc8b14ecce0652a0944731a1493a3c1ba44ff57a"}, ] [package.dependencies] -dill = ">=0.3.8" +dill = ">=0.3.9" [[package]] name = "mypy" @@ -721,20 +725,20 @@ files = [ [[package]] name = "pathos" -version = "0.3.2" +version = "0.3.3" description = "parallel graph management and execution in heterogeneous computing" optional = false python-versions = ">=3.8" files = [ - {file = "pathos-0.3.2-py3-none-any.whl", hash = "sha256:d669275e6eb4b3fbcd2846d7a6d1bba315fe23add0c614445ba1408d8b38bafe"}, - {file = "pathos-0.3.2.tar.gz", hash = "sha256:4f2a42bc1e10ccf0fe71961e7145fc1437018b6b21bd93b2446abc3983e49a7a"}, + {file = "pathos-0.3.3-py3-none-any.whl", hash = "sha256:e04616c6448608ad1f809360be22e3f2078d949a36a81e6991da6c2dd1f82513"}, + {file = "pathos-0.3.3.tar.gz", hash = "sha256:dcb2a5f321aa34ca541c1c1861011ea49df357bb908379c21dd5741f666e0a58"}, ] [package.dependencies] -dill = ">=0.3.8" -multiprocess = ">=0.70.16" -pox = ">=0.3.4" -ppft = ">=1.7.6.8" +dill = ">=0.3.9" +multiprocess = ">=0.70.17" +pox = ">=0.3.5" +ppft = ">=1.7.6.9" [[package]] name = "pathspec" @@ -763,13 +767,13 @@ flake8 = ">=5.0.0" [[package]] name = "platformdirs" -version = "4.3.3" +version = "4.3.6" description = "A small Python package for determining appropriate platform-specific dirs, e.g. a `user data dir`." optional = false python-versions = ">=3.8" files = [ - {file = "platformdirs-4.3.3-py3-none-any.whl", hash = "sha256:50a5450e2e84f44539718293cbb1da0a0885c9d14adf21b77bae4e66fc99d9b5"}, - {file = "platformdirs-4.3.3.tar.gz", hash = "sha256:d4e0b7d8ec176b341fb03cb11ca12d0276faa8c485f9cd218f613840463fc2c0"}, + {file = "platformdirs-4.3.6-py3-none-any.whl", hash = "sha256:73e575e1408ab8103900836b97580d5307456908a03e92031bab39e4554cc3fb"}, + {file = "platformdirs-4.3.6.tar.gz", hash = "sha256:357fb2acbc885b0419afd3ce3ed34564c13c9b95c89360cd9563f73aa5e2b907"}, ] [package.extras] @@ -794,28 +798,28 @@ testing = ["pytest", "pytest-benchmark"] [[package]] name = "pox" -version = "0.3.4" +version = "0.3.5" description = "utilities for filesystem exploration and automated builds" optional = false python-versions = ">=3.8" files = [ - {file = "pox-0.3.4-py3-none-any.whl", hash = "sha256:651b8ae8a7b341b7bfd267f67f63106daeb9805f1ac11f323d5280d2da93fdb6"}, - {file = "pox-0.3.4.tar.gz", hash = "sha256:16e6eca84f1bec3828210b06b052adf04cf2ab20c22fd6fbef5f78320c9a6fed"}, + {file = "pox-0.3.5-py3-none-any.whl", hash = "sha256:9e82bcc9e578b43e80a99cad80f0d8f44f4d424f0ee4ee8d4db27260a6aa365a"}, + {file = "pox-0.3.5.tar.gz", hash = "sha256:8120ee4c94e950e6e0483e050a4f0e56076e590ba0a9add19524c254bd23c2d1"}, ] [[package]] name = "ppft" -version = "1.7.6.8" +version = "1.7.6.9" description = "distributed and parallel Python" optional = false python-versions = ">=3.8" files = [ - {file = "ppft-1.7.6.8-py3-none-any.whl", hash = "sha256:de2dd4b1b080923dd9627fbdea52649fd741c752fce4f3cf37e26f785df23d9b"}, - {file = "ppft-1.7.6.8.tar.gz", hash = "sha256:76a429a7d7b74c4d743f6dba8351e58d62b6432ed65df9fe204790160dab996d"}, + {file = "ppft-1.7.6.9-py3-none-any.whl", hash = "sha256:dab36548db5ca3055067fbe6b1a17db5fee29f3c366c579a9a27cebb52ed96f0"}, + {file = "ppft-1.7.6.9.tar.gz", hash = "sha256:73161c67474ea9d81d04bcdad166d399cff3f084d5d2dc21ebdd46c075bbc265"}, ] [package.extras] -dill = ["dill (>=0.3.8)"] +dill = ["dill (>=0.3.9)"] [[package]] name = "psutil" @@ -907,17 +911,17 @@ files = [ [[package]] name = "pyreadline3" -version = "3.5.2" +version = "3.5.4" description = "A python implementation of GNU readline." optional = false python-versions = ">=3.8" files = [ - {file = "pyreadline3-3.5.2-py3-none-any.whl", hash = "sha256:a87d56791e2965b2b187e2ea33dcf664600842c997c0623c95cf8ef07db83de9"}, - {file = "pyreadline3-3.5.2.tar.gz", hash = "sha256:ba82292e52c5a3bb256b291af0c40b457c1e8699cac9a873abbcaac8aef3a1bb"}, + {file = "pyreadline3-3.5.4-py3-none-any.whl", hash = "sha256:eaf8e6cc3c49bcccf145fc6067ba8643d1df34d604a1ec0eccbf7a18e6d3fae6"}, + {file = "pyreadline3-3.5.4.tar.gz", hash = "sha256:8d57d53039a1c75adba8e50dd3d992b28143480816187ea5efbd5c78e6c885b7"}, ] [package.extras] -dev = ["build", "flake8", "pytest", "twine"] +dev = ["build", "flake8", "mypy", "pytest", "twine"] [[package]] name = "pytest" @@ -1026,18 +1030,19 @@ tokenize-rt = ">=5.2.0" [[package]] name = "rich" -version = "13.8.1" +version = "13.9.2" description = "Render rich text, tables, progress bars, syntax highlighting, markdown and more to the terminal" optional = false -python-versions = ">=3.7.0" +python-versions = ">=3.8.0" files = [ - {file = "rich-13.8.1-py3-none-any.whl", hash = "sha256:1760a3c0848469b97b558fc61c85233e3dafb69c7a071b4d60c38099d3cd4c06"}, - {file = "rich-13.8.1.tar.gz", hash = "sha256:8260cda28e3db6bf04d2d1ef4dbc03ba80a824c88b0e7668a0f23126a424844a"}, + {file = "rich-13.9.2-py3-none-any.whl", hash = "sha256:8c82a3d3f8dcfe9e734771313e606b39d8247bb6b826e196f4914b333b743cf1"}, + {file = "rich-13.9.2.tar.gz", hash = "sha256:51a2c62057461aaf7152b4d611168f93a9fc73068f8ded2790f29fe2b5366d0c"}, ] [package.dependencies] markdown-it-py = ">=2.2.0" pygments = ">=2.13.0,<3.0.0" +typing-extensions = {version = ">=4.0.0,<5.0", markers = "python_version < \"3.11\""} [package.extras] jupyter = ["ipywidgets (>=7.5.1,<9)"] @@ -1106,13 +1111,13 @@ files = [ [[package]] name = "tomli" -version = "2.0.1" +version = "2.0.2" description = "A lil' TOML parser" optional = false -python-versions = ">=3.7" +python-versions = ">=3.8" files = [ - {file = "tomli-2.0.1-py3-none-any.whl", hash = "sha256:939de3e7a6161af0c887ef91b7d41a53e7c5a1ca976325f429cb46ea9bc30ecc"}, - {file = "tomli-2.0.1.tar.gz", hash = "sha256:de526c12914f0c550d15924c62d72abc48d6fe7364aa87328337a31007fe8a4f"}, + {file = "tomli-2.0.2-py3-none-any.whl", hash = "sha256:2ebe24485c53d303f690b0ec092806a085f07af5a5aa1464f3931eec36caaa38"}, + {file = "tomli-2.0.2.tar.gz", hash = "sha256:d46d457a85337051c36524bc5349dd91b1877838e2979ac5ced3e710ed8a60ed"}, ] [[package]] @@ -1195,4 +1200,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "ae0b3f26c5c017db2751c3dc30b4f6b8c4e7ebcf739bff5cb0c322bfaf1fd90a" +content-hash = "6f42bfcdf4432727960d94c3922f2da4074da8969675afd756a0949171d08e22" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 4c16c4ed25..6ed7e6d320 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -kframework = "7.1.142" +kframework = "7.1.156" tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 89473a4d6d..ee4f4617e1 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -838,7 +838,6 @@ def kprove_args(self) -> ArgumentParser: args.add_argument( '--maintenance-rate', dest='maintenance_rate', - default=1, type=int, help='The number of proof iterations performed between two writes to disk and status bar updates. Note that setting to >1 may result in work being discarded if proof is interrupted.', ) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 84ec965406..bf74746c3f 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -20,13 +20,12 @@ from pyk.kast.manip import abstract_term_safely, flatten_label, set_cell from pyk.kast.pretty import paren from pyk.kcfg.kcfg import Step -from pyk.kcfg.semantics import KCFGSemantics +from pyk.kcfg.semantics import DefaultSemantics from pyk.kcfg.show import NodePrinter from pyk.ktool.kprove import KProve from pyk.ktool.krun import KRun from pyk.prelude.bytes import BYTES, pretty_bytes -from pyk.prelude.kbool import notBool -from pyk.prelude.kint import INT, eqInt, gtInt, intToken, ltInt +from pyk.prelude.kint import INT, gtInt, intToken, ltInt from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue from pyk.prelude.string import stringToken from pyk.prelude.utils import token @@ -50,7 +49,7 @@ # KEVM class -class KEVMSemantics(KCFGSemantics): +class KEVMSemantics(DefaultSemantics): auto_abstract_gas: bool allow_symbolic_program: bool _cached_subst: Subst | None @@ -98,6 +97,12 @@ def is_terminal(self, cterm: CTerm) -> bool: return False + def is_loop(self, cterm: CTerm) -> bool: + jumpi_pattern = KEVM.jumpi_applied(KVariable('###PCOUNT'), KVariable('###COND')) + pc_next_pattern = KEVM.pc_applied(KEVM.jumpi()) + branch_pattern = KSequence([jumpi_pattern, pc_next_pattern, KEVM.sharp_execute(), KVariable('###CONTINUATION')]) + return branch_pattern.match(cterm.cell('K_CELL')) is not None + def same_loop(self, cterm1: CTerm, cterm2: CTerm) -> bool: # In the same program, at the same calldepth, at the same program counter for cell in ['PC_CELL', 'CALLDEPTH_CELL', 'PROGRAM_CELL']: @@ -116,20 +121,6 @@ def same_loop(self, cterm1: CTerm, cterm2: CTerm) -> bool: return True return False - def extract_branches(self, cterm: CTerm) -> list[KInner]: - k_cell = cterm.cell('K_CELL') - jumpi_pattern = KEVM.jumpi_applied(KVariable('###PCOUNT'), KVariable('###COND')) - pc_next_pattern = KEVM.pc_applied(KEVM.jumpi()) - branch_pattern = KSequence([jumpi_pattern, pc_next_pattern, KEVM.sharp_execute(), KVariable('###CONTINUATION')]) - if subst := branch_pattern.match(k_cell): - cond = subst['###COND'] - if cond_subst := KEVM.bool_2_word(KVariable('###BOOL_2_WORD')).match(cond): - cond = cond_subst['###BOOL_2_WORD'] - else: - cond = eqInt(cond, intToken(0)) - return [mlEqualsTrue(cond), mlEqualsTrue(notBool(cond))] - return [] - def abstract_node(self, cterm: CTerm) -> CTerm: if not self.auto_abstract_gas: return cterm @@ -225,6 +216,29 @@ def can_make_custom_step(self, cterm: CTerm) -> bool: self._cached_subst = load_pattern.match(cterm.cell('K_CELL')) return self._cached_subst is not None + def is_mergeable(self, ct1: CTerm, ct2: CTerm) -> bool: + """Given two CTerms of Edges' targets, check if they are mergeable. + + Two CTerms are mergeable if their `STATUSCODE_CELL` and `PROGRAM_CELL` are the same. + If mergeable, the two corresponding Edges are merged into one. + + :param ct1: CTerm of one Edge's target. + :param ct2: CTerm of another Edge's target. + :return: `True` if the two CTerms are mergeable; `False` otherwise. + """ + status_code_1 = ct1.cell('STATUSCODE_CELL') + status_code_2 = ct2.cell('STATUSCODE_CELL') + program_1 = ct1.cell('PROGRAM_CELL') + program_2 = ct2.cell('PROGRAM_CELL') + if ( + type(status_code_1) is KApply + and type(status_code_2) is KApply + and type(program_1) is KToken + and type(program_2) is KToken + ): + return status_code_1 == status_code_2 and program_1 == program_2 + raise ValueError(f'Attempted to merge nodes with non-concrete or : {(ct1, ct2)}') + class KEVM(KProve, KRun): _use_hex: bool diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 99f8b4d449..56f673a5cc 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1818,9 +1818,14 @@ Precompiled Contracts ``` - `ECREC` performs ECDSA public key recovery. -- `SHA256` performs the SHA2-257 hash function. +- `SHA256` performs the SHA2-256 hash function. - `RIP160` performs the RIPEMD-160 hash function. - `ID` is the identity function (copies input to output). +- `MODEXP` performs arbitrary-precision modular exponentiation. +- `ECADD` performs point addition on the elliptic curve alt_bn128. +- `ECMUL` performs scalar multiplication on the elliptic curve alt_bn128. +- `ECPAIRING` performs an optimal ate pairing check on the elliptic curve alt_bn128. +- `BLAKE2F` performs the compression function F used in the BLAKE2 hashing algorithm. ```k syntax PrecompiledOp ::= "ECREC" diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k index 49d6ec9ee3..0bf1c666b9 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k @@ -13,7 +13,7 @@ module BITWISE-SIMPLIFICATION [symbolic] rule A |Int 0 => A [simplification] rule A |Int A => A [simplification] - rule A |Int B => B |Int A [simplification(40), concrete(B), symbolic(A)] + rule A |Int B => B |Int A [simplification(30), symbolic(A), concrete(B)] rule X |Int _ ==Int 0 => false requires 0 true [simplification, smt-lemma] @@ -22,7 +22,7 @@ module BITWISE-SIMPLIFICATION [symbolic] // bit-and // ########################################################################### - rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification] + rule A &Int B => B &Int A [simplification(30), symbolic(A), concrete(B)] rule 0 &Int _ => 0 [simplification] rule _ &Int 0 => 0 [simplification] @@ -34,24 +34,26 @@ module BITWISE-SIMPLIFICATION [symbolic] rule [bitwise-or-lt-zero]: (X |Int Y) false requires 0 <=Int X andBool 0 <=Int Y andBool Z <=Int 0 [concrete(Z), simplification] rule [bitwise-and-lt-zero]: (X &Int Y) false requires 0 <=Int X andBool 0 <=Int Y andBool Z <=Int 0 [concrete(Z), simplification] - rule [bitwise-and-lt]: (X &Int Y) true requires 0 <=Int X andBool 0 <=Int Y andBool (X true requires 0 <=Int X andBool 0 <=Int Y andBool X true requires 0 <=Int X andBool 0 <=Int Y andBool (X true + requires 0 <=Int X andBool 0 <=Int Y andBool X Y requires #rangeUInt(XXX, Y) rule [bitwise-and-maxUInt-identity]: X &Int Y => Y - requires 0 <=Int X - andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1) + requires 0 <=Int X andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1) andBool 0 <=Int Y andBool Y 0 requires #rangeUInt(XXX, Y) + // Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(256 -Int XXX, Y) rule [bitwise-and-notMaxUInt-zero]: X &Int Y => 0 - requires #rangeUInt(256, X) - andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) ) + requires #rangeUInt(256, X) andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) ) andBool 0 <=Int Y andBool Y chop ( ( notMaxUInt5 &Int X ) +Int ( notMaxUInt5 &Int Y ) ) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k index 5d2f2f8cfd..00ad215864 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k @@ -72,30 +72,6 @@ module BYTES-SIMPLIFICATION [symbolic] andBool #asWord(B) X - requires 0 <=Int WB andBool 0 <=Int X andBool - ( ( WB <=Int 32 andBool X Int 32 andBool X X - requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR - andBool S +Int WR ==Int WB - andBool X #asWord ( B ) - requires #asInteger ( BZ ) ==Int 0 - [simplification, concrete(BZ)] - - rule [asWord-trim-overflowing-zeros]: - #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) ) - requires 32 #buf(W1 +Int W2, 0) requires 0 <=Int W1 andBool 0 <=Int W2 @@ -244,24 +220,6 @@ module BYTES-SIMPLIFICATION [symbolic] #range(#padRightToWidth(_, BUF), 0, WIDTH) => BUF requires lengthBytes(BUF) ==Int WIDTH [simplification] - rule [range-eq-check]: - BZ +Bytes #range ( B, S, W ) ==K B => true - requires 0 <=Int S andBool 0 <=Int W - andBool lengthBytes( B ) ==Int S +Int W - andBool #asInteger( BZ ) ==Int 0 - andBool lengthBytes( BZ ) ==Int S - andBool #asWord ( B ) #Top - requires 0 <=Int S andBool 0 <=Int W - andBool lengthBytes( B ) ==Int S +Int W - andBool #asInteger( BZ ) ==Int 0 - andBool lengthBytes( BZ ) ==Int S - andBool #asWord ( B ) - #range(B1, 0, S) +Bytes B2 +Bytes #range (B1 , S +Int lengthBytes(B2), lengthBytes(B1) -Int (S +Int lengthBytes(B2))) - requires 0 <=Int S andBool S +Int lengthBytes(B2) (B1 [ S := B ]) +Bytes B2 + requires 0 <=Int S andBool S +Int lengthBytes(B) #range(B1, 0, S) +Bytes B2 - requires 0 <=Int S andBool lengthBytes(B1) <=Int S +Int lengthBytes(B2) - [simplification(60)] + rule [memUpdate-concat-in-right]: (B1 +Bytes B2) [ S := B ] => B1 +Bytes (B2 [ S -Int lengthBytes(B1) := B ]) + requires lengthBytes(B1) <=Int S + [simplification(40)] rule [memUpdate-reorder]: - B:Bytes [ S1:Int := B1:Bytes] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ] [ S1 := B1 ] + B:Bytes [ S1:Int := B1:Bytes ] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ] [ S1 := B1 ] requires 0 <=Int S2 andBool S2 B [ S2 := B2 ] + B:Bytes [ S1:Int := B1:Bytes ] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ] requires 0 <=Int S2 andBool S2 <=Int S1 andBool S1 +Int lengthBytes(B1) <=Int S2 +Int lengthBytes(B2) [simplification] + rule [memUpdate-as-concat-inside]: + B1:Bytes [ S:Int := B2:Bytes ] => + #range(B1, 0, S) +Bytes B2 +Bytes #range(B1 , S +Int lengthBytes(B2), lengthBytes(B1) -Int (S +Int lengthBytes(B2))) + requires 0 <=Int S andBool S +Int lengthBytes(B2) #range(B1, 0, S) +Bytes B2 + requires 0 <=Int S andBool lengthBytes(B1) <=Int S +Int lengthBytes(B2) + [simplification(60)] + // lengthBytes rule [lengthBytes-geq-zero]: 0 <=Int lengthBytes ( _ ) => true [simplification, smt-lemma] @@ -301,15 +267,7 @@ module BYTES-SIMPLIFICATION [symbolic] rule [lengthBytes-leq-zero]: lengthBytes(B:Bytes) <=Int 0 => B ==K .Bytes [simplification] - // #asWord - - rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) )) - requires 0 <=Int M andBool M modInt 8 ==Int 0 - [simplification, preserves-definedness] - - // This simplification needs to be generalised properly - rule notMaxUInt224 &Int #asWord(#padRightToWidth(32, BUF)) => #asWord(#padRightToWidth(32, BUF)) - requires lengthBytes(BUF) <=Int 4 [simplification] + // #padToWidth rule #padToWidth(32, #asByteStack(V)) => #buf(32, V) requires #rangeUInt(256, V) [simplification] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k index a4c168fbb2..3a16df7834 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k @@ -1,17 +1,10 @@ requires "evm-types.md" module EVM-INT-SIMPLIFICATION - imports EVM-INT-SIMPLIFICATION-HASKELL -endmodule - -module EVM-INT-SIMPLIFICATION-HASKELL [symbolic] - imports EVM-INT-SIMPLIFICATION-COMMON -endmodule - -module EVM-INT-SIMPLIFICATION-COMMON - imports INT imports BOOL + imports BUF imports EVM-TYPES + imports INT imports WORD // ########################################################################### @@ -57,31 +50,92 @@ module EVM-INT-SIMPLIFICATION-COMMON // #asWord // ########################################################################### - rule [asWord-lb]: 0 <=Int #asWord(_WS) => true [simplification, smt-lemma] - rule [asWord-ub]: #asWord(_WS) true [simplification, smt-lemma] - - rule [asWord-lt]: - #asWord ( BA ) true - requires 2 ^Int ( 8 *Int lengthBytes(BA) ) <=Int X - [concrete(X), simplification] - - rule [asWord-lt-concat]: - #asWord ( BA1 +Bytes BA2 ) #asWord ( BA1 ) true - requires 0 <=Int S andBool 0 <=Int W - andBool 2 ^Int ( 8 *Int W ) <=Int X - [simplification, concrete(S, W, X), preserves-definedness] - - rule [lt-asWord-range]: - X X #buf ( 32 -Int lengthBytes(B1), 0 ) +Bytes B1 ==K #buf ( 32 -Int lengthBytes(B2), 0 ) +Bytes B2 + requires lengthBytes(B1) <=Int 32 andBool lengthBytes(B2) <=Int 32 + [simplification, preserves-definedness] + + // Unification: two `#asWord`s + rule [asWord-eq-asWord-ml]: + { #asWord ( B1 ) #Equals #asWord ( B2 ) } => { true #Equals #asWord ( B1 ) ==Int #asWord ( B2 ) } + requires lengthBytes(B1) <=Int 32 andBool lengthBytes(B2) <=Int 32 + [simplification, preserves-definedness] + + // Unification: `#asWord` and concrete number + rule [asWord-eq-num]: + #asWord ( B:Bytes ) ==Int X:Int => + 0 <=Int X andBool X { true #Equals #asWord ( B:Bytes ) ==K X:Int } requires lengthBytes(B) <=Int 32 [simplification, concrete(X), preserves-definedness] + rule [asWord-eq-num-ml-r]: { X:Int #Equals #asWord ( B:Bytes ) } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } requires lengthBytes(B) <=Int 32 [simplification, concrete(X), preserves-definedness] + + // Reduction: we can always remove leading zeros + rule [asWord-trim-leading-zeros]: + #asWord ( BZ +Bytes B ) => #asWord ( B ) + requires #asInteger ( BZ ) ==Int 0 + [simplification(40), concrete(BZ), preserves-definedness] + + // Reduction: we can always ignore content beyond 32 bytes + rule [asWord-trim-overflowing]: + #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) ) + requires 32 #asWord ( B ) requires 0 <=Int S andBool 0 <=Int W + andBool lengthBytes(B) <=Int 32 andBool lengthBytes(B) ==Int S +Int W andBool #asWord ( B ) X + requires 0 <=Int WB andBool 0 <=Int X andBool X >Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) ) + requires 0 <=Int N andBool N modInt 8 ==Int 0 + [simplification, concrete(N), preserves-definedness] + + // Reduction: division in terms of `#range` + rule [asWord-div]: + #asWord( BA ) /Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( log2Int( N ) /Int 8 ) ) ) + requires 0 true [simplification, smt-lemma] + rule [asWord-ub]: #asWord( _ ) true [simplification, smt-lemma] + + // Comparison: `#asWord(B)` is certainly less than something that does not fit into `lengthBytes(B)` bytes + rule [asWord-lt]: #asWord ( B ) true requires 2 ^Int (8 *Int minInt(32, lengthBytes(B))) <=Int X [simplification, preserves-definedness] + // Comparison: `#asWord(B)` is certainly less than or equal to something that is not less than the max number fitting into `lengthBytes(B)` bytes + rule [asWord-le]: #asWord ( B ) <=Int X:Int => true requires ( 2 ^Int (8 *Int minInt(32, lengthBytes(B))) -Int 1 ) <=Int X [simplification, preserves-definedness] + + // Comparison: `#asWord` of `+Bytes` when lower bytes match, with ` #asWord ( BA1 ) #asWord ( BA1 ) <=Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) ) + requires #asWord ( BA2 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) ) + andBool lengthBytes ( BA1 +Bytes BA2 ) <=Int 32 + [simplification, concrete(BA2, X), preserves-definedness] // ########################################################################### // chop diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 0969d2574a..661fa1c143 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -194,14 +194,6 @@ module LEMMAS-HASKELL [symbolic] imports EVM imports BUF - // ######################## - // Word Reasoning - // ######################## - - rule #asWord(BUF) /Int D => #asWord(#range(BUF, 0, lengthBytes(BUF) -Int log256Int(D))) - requires 0 ', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + ], + True, + False, + ), + ( + 'mergeable_not_care_others', + [ + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + KApply('', token(b'\x00')), + ) + ), + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + KApply('', token(b'\x01')), + ) + ), + ], + True, + False, + ), + ( + 'not_mergeable', + [ + CTerm( + KApply( + '', + KApply('', KApply('EVMC_SUCCESS')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + CTerm( + KApply( + '', + KApply('', KApply('EVMC_REVERT')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + ], + False, + True, + ), + ( + 'raise_error', + [ + CTerm( + KApply( + '', + KApply('', KToken('EVMC_SUCCESS', 'StatusCode')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + CTerm( + KApply( + '', + KApply('', KToken('EVMC_SUCCESS', 'StatusCode')), + KApply('', token(b'\xcc\xff\xff\xfac\x60\xf5')), + ) + ), + ], + False, + True, + ), +] + + +@pytest.mark.parametrize( + 'test_id,input,expected,raise_error', + IS_MERGEABLE_DATA, + ids=[test_id for test_id, *_ in IS_MERGEABLE_DATA], +) +def test_is_mergeable(test_id: str, input: list[CTerm], expected: KInner, raise_error: bool) -> None: + # When + try: + result = KEVMSemantics().is_mergeable(input[0], input[1]) + except ValueError: + assert raise_error + return + # Then + assert result == expected diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k index 373f0a195e..dff254eb89 100644 --- a/tests/specs/benchmarks/verification.k +++ b/tests/specs/benchmarks/verification.k @@ -17,8 +17,6 @@ module VERIFICATION-COMMON rule #asWord(#ecrec(HASH, SIGV, SIGR, SIGS)) => 0 requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification] rule 0 true requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification] - rule 0 <=Int #asWord(#ecrec(_ , _ , _ , _ )) => true [simplification] - rule #asWord(#ecrec(_ , _ , _ , _ )) true [simplification] rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification] diff --git a/tests/specs/examples/storage-spec.md b/tests/specs/examples/storage-spec.md index d27e067870..7950c5135e 100644 --- a/tests/specs/examples/storage-spec.md +++ b/tests/specs/examples/storage-spec.md @@ -26,7 +26,7 @@ requires "storage-bin-runtime.k" module VERIFICATION imports EDSL - imports LEMMAS + imports LEMMAS-WITHOUT-SLOT-UPDATES imports EVM-OPTIMIZATIONS imports STORAGE-VERIFICATION diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k index 0f9cd2517a..58f2fb0983 100644 --- a/tests/specs/functional/lemmas-spec.k +++ b/tests/specs/functional/lemmas-spec.k @@ -149,7 +149,7 @@ module LEMMAS-SPEC requires X =/=K Y - // Buffer write simplifications + // Memory update simplifications // ---------------------------- // claim runLemma ( M [ L := .Bytes ] [ N := WS:Bytes ] ) => doneLemma ( M [ N := WS ] ) ... requires L <=Int N @@ -164,9 +164,14 @@ module LEMMAS-SPEC claim runLemma( M:Bytes [ 32 := BA1 ] [ 32 := BA2 ] ) => doneLemma(M [ 32 := BA2 ] ) ... requires lengthBytes(BA1) <=Int lengthBytes(BA2) claim runLemma( M:Bytes [ 32 := BA1 ] [ 32 := #padToWidth(32, #asByteStack(#hashedLocation("Solidity", 2, OWNER))) ] ) => doneLemma(M [ 32 := #padToWidth(32, #asByteStack(#hashedLocation("Solidity", 2, OWNER))) ] ) ... requires lengthBytes(BA1) ==Int 32 andBool #rangeUInt(256, OWNER) - // Memory write past the end of the buffer - claim [write-past-end]: runLemma ( #buf(160, A) [ 160 := #buf(32, B) ] [ 192 := #buf(32, C) ] [ 224 := #buf(32, D) ] [ 256 := #buf(32, E) ] ) - => doneLemma ( #buf(160, A) +Bytes #buf(32, B) +Bytes #buf(32, C) +Bytes #buf(32, D) +Bytes #buf(32, E) ) ... + claim [memUpdate-past-end]: runLemma ( #buf(160, A) [ 160 := #buf(32, B) ] [ 192 := #buf(32, C) ] [ 224 := #buf(32, D) ] [ 256 := #buf(32, E) ] ) + => doneLemma ( #buf(160, A) +Bytes #buf(32, B) +Bytes #buf(32, C) +Bytes #buf(32, D) +Bytes #buf(32, E) ) ... + + claim [memUpdate-pinpoint]: runLemma ( ( B1 +Bytes B2 +Bytes B3 +Bytes B4 ) [ 70 := #buf(16, X:Int) ] ) + => doneLemma ( ( B1 +Bytes B2 +Bytes ( B3 [ 10 := #buf(16, X:Int) ] ) +Bytes B4 ) ) ... + requires lengthBytes(B1) ==Int 20 + andBool lengthBytes(B2) ==Int 40 + andBool lengthBytes(B3) ==Int 60 // #lookup simplifications // ----------------------- @@ -356,6 +361,11 @@ module LEMMAS-SPEC runLemma( #range (#buf(8, X:Int), -3, _:Int) ) => doneLemma( .Bytes ) ... requires 0 <=Int X andBool X runLemma( b"\xaa" ==K #range ( ( BYTES:Bytes +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) [ ( lengthBytes ( BYTES:Bytes ) /Int 2 ) := b"\xaa" ] , ( lengthBytes ( BYTES:Bytes ) /Int 2 ) , 1 ) ) + => doneLemma(true) ... + requires lengthBytes ( BYTES:Bytes ) runLemma ( #asWord ( ( #range( #buf ( 32 , X ), 0, 28 ) ):Bytes ) ) => doneLemma ( 0 ) ... requires #rangeUInt(32, X) @@ -557,18 +567,18 @@ module LEMMAS-SPEC claim [bit-240-m-or-nm]: runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int T ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 240 , X ) andBool #rangeUInt(256, T) claim [bit-248-m-or-nm]: runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int T ) ) ) => doneLemma( X ) ... requires #rangeUInt ( 248 , X ) andBool #rangeUInt(256, T) - // claim [bit-008-nm-or-m]: runLemma ( notMaxUInt8 &Int ( X |Int ( maxUInt8 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 248 , X ) andBool #rangeUInt(256, T) - // claim [bit-016-nm-or-m]: runLemma ( notMaxUInt16 &Int ( X |Int ( maxUInt16 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 240 , X ) andBool #rangeUInt(256, T) - // claim [bit-032-nm-or-m]: runLemma ( notMaxUInt32 &Int ( X |Int ( maxUInt32 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 224 , X ) andBool #rangeUInt(256, T) - // claim [bit-064-nm-or-m]: runLemma ( notMaxUInt64 &Int ( X |Int ( maxUInt64 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 192 , X ) andBool #rangeUInt(256, T) - // claim [bit-096-nm-or-m]: runLemma ( notMaxUInt96 &Int ( X |Int ( maxUInt96 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 160 , X ) andBool #rangeUInt(256, T) - // claim [bit-128-nm-or-m]: runLemma ( notMaxUInt128 &Int ( X |Int ( maxUInt128 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 128 , X ) andBool #rangeUInt(256, T) - // claim [bit-160-nm-or-m]: runLemma ( notMaxUInt160 &Int ( X |Int ( maxUInt160 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 96 , X ) andBool #rangeUInt(256, T) - // claim [bit-192-nm-or-m]: runLemma ( notMaxUInt192 &Int ( X |Int ( maxUInt192 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 64 , X ) andBool #rangeUInt(256, T) - // claim [bit-208-nm-or-m]: runLemma ( notMaxUInt208 &Int ( X |Int ( maxUInt208 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 48 , X ) andBool #rangeUInt(256, T) - // claim [bit-224-nm-or-m]: runLemma ( notMaxUInt224 &Int ( X |Int ( maxUInt224 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 32 , X ) andBool #rangeUInt(256, T) - // claim [bit-240-nm-or-m]: runLemma ( notMaxUInt240 &Int ( X |Int ( maxUInt240 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 16 , X ) andBool #rangeUInt(256, T) - // claim [bit-248-nm-or-m]: runLemma ( notMaxUInt248 &Int ( X |Int ( maxUInt248 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 8 , X ) andBool #rangeUInt(256, T) + claim [bit-008-nm-or-m]: runLemma ( notMaxUInt8 &Int ( X |Int ( maxUInt8 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 8 , X ) andBool #rangeUInt(256, T) + claim [bit-016-nm-or-m]: runLemma ( notMaxUInt16 &Int ( X |Int ( maxUInt16 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 16 , X ) andBool #rangeUInt(256, T) + claim [bit-032-nm-or-m]: runLemma ( notMaxUInt32 &Int ( X |Int ( maxUInt32 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 32 , X ) andBool #rangeUInt(256, T) + claim [bit-064-nm-or-m]: runLemma ( notMaxUInt64 &Int ( X |Int ( maxUInt64 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 64 , X ) andBool #rangeUInt(256, T) + claim [bit-096-nm-or-m]: runLemma ( notMaxUInt96 &Int ( X |Int ( maxUInt96 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 96 , X ) andBool #rangeUInt(256, T) + claim [bit-128-nm-or-m]: runLemma ( notMaxUInt128 &Int ( X |Int ( maxUInt128 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 128 , X ) andBool #rangeUInt(256, T) + claim [bit-160-nm-or-m]: runLemma ( notMaxUInt160 &Int ( X |Int ( maxUInt160 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 160 , X ) andBool #rangeUInt(256, T) + claim [bit-192-nm-or-m]: runLemma ( notMaxUInt192 &Int ( X |Int ( maxUInt192 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 192 , X ) andBool #rangeUInt(256, T) + claim [bit-208-nm-or-m]: runLemma ( notMaxUInt208 &Int ( X |Int ( maxUInt208 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 208 , X ) andBool #rangeUInt(256, T) + claim [bit-224-nm-or-m]: runLemma ( notMaxUInt224 &Int ( X |Int ( maxUInt224 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 224 , X ) andBool #rangeUInt(256, T) + claim [bit-240-nm-or-m]: runLemma ( notMaxUInt240 &Int ( X |Int ( maxUInt240 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 240 , X ) andBool #rangeUInt(256, T) + claim [bit-248-nm-or-m]: runLemma ( notMaxUInt248 &Int ( X |Int ( maxUInt248 &Int T ) ) ) => doneLemma( 0 ) ... requires #rangeUInt ( 248 , X ) andBool #rangeUInt(256, T) claim [bit-008-m-aW]: runLemma ( maxUInt8 &Int #asWord ( BA ) ) => doneLemma ( #asWord ( #range(BA, 31, 1) ) ) ... requires lengthBytes(BA) ==Int 32 claim [bit-016-m-aW]: runLemma ( maxUInt16 &Int #asWord ( BA ) ) => doneLemma ( #asWord ( #range(BA, 30, 2) ) ) ... requires lengthBytes(BA) ==Int 32 @@ -668,6 +678,84 @@ module LEMMAS-SPEC ) ... requires lengthBytes ( VV0_data_114b9705:Bytes ) <=Int 1073741824 + claim [asWord-unif-01]: // two `#asWord`s, both under 32 bytes + runLemma( + #asWord ( B1 +Bytes B2 ) ==Int #asWord ( B3 ) + ) => doneLemma( + #buf(22, 0) +Bytes B1 +Bytes B2 ==K #buf(16, 0) +Bytes B3 + ) ... + requires lengthBytes(B1) ==Int 4 andBool lengthBytes(B2) ==Int 6 + andBool lengthBytes(B3) ==Int 16 + + claim [asWord-unif-02]: // two `#asWord`s, left over 32 bytes + runLemma( + #asWord ( B1 +Bytes B2 ) ==Int #asWord ( B3 +Bytes B4 ) + ) => doneLemma( + #range ( B1, 7, 5 ) +Bytes B2 ==K #buf(7, 0) +Bytes B3 +Bytes B4 + ) ... + requires lengthBytes(B1) ==Int 12 andBool lengthBytes(B2) ==Int 27 + andBool lengthBytes(B3) ==Int 10 andBool lengthBytes(B4) ==Int 15 + + claim [asWord-unif-03]: // `#asWord` and constant out of range, buffer length <=Int 32 + runLemma( + #asWord ( B ) ==Int -15 orBool 2 ^Int 160 ==Int #asWord ( B ) + ) => doneLemma( + false + ) ... + requires lengthBytes(B) ==Int 16 + + claim [asWord-unif-04]: // `#asWord` and constant out of range, buffer length >Int 32 + runLemma( + #asWord ( B ) ==Int -15 orBool 2 ^Int 324 ==Int #asWord ( B ) + ) => doneLemma( + false + ) ... + requires lengthBytes(B) ==Int 36 + + claim [asWord-unif-05]: // `#asWord` and constant, buffer length <=Int 32 + runLemma( + #asWord ( B1 +Bytes B2 ) ==Int 9518572911576893851958972884578457483927345 + ) => doneLemma( + B1 +Bytes B2 ==K #buf(27, 9518572911576893851958972884578457483927345) + ) ... + requires lengthBytes(B1) ==Int 15 andBool lengthBytes(B2) ==Int 12 + + claim [asWord-unif-06]: // `#asWord` and constant, buffer length >Int 32 + runLemma( + #asWord ( B1 +Bytes B2 ) ==Int 294572972648782479679175618975648679836 + ) => doneLemma( + #range(B1, 3, 17) +Bytes B2 ==K #buf(32, 294572972648782479679175618975648679836) + ) ... + requires lengthBytes(B1) ==Int 20 andBool lengthBytes(B2) ==Int 15 + + claim [asWord-chop-overflow-div]: + runLemma( + #asWord( BA1 +Bytes BA2 ) /Int N + ) => doneLemma( + // #asWord ( BA2 ) /Int N + #asWord ( #range ( BA2, 0, lengthBytes( BA2 ) -Int ( log2Int( N ) /Int 8 ) ) ) + ) ... + requires 0 runLemma( + #asWord ( BA1 +Bytes BA2 +Bytes BA3 ) doneLemma( + #asWord ( BA2 +Bytes BA3 ) + requires #asWord ( BA3 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA3 ) ) ) + andBool 0 runLemma( + #asWord ( BA1 +Bytes BA2 +Bytes BA3 ) <=Int X:Int + ) => doneLemma( + #asWord ( BA2 +Bytes BA3 ) <=Int X + ) ... + requires #asWord ( BA3 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA3 ) ) ) + andBool 0 runLemma ( X &Int #asWord ( BA ) ==Int Y:Int ) => doneLemma ( true ) ... + requires 0 <=Int X andBool X runLemma ( X &Int #asWord ( BA ) ==Int Y:Int ) => doneLemma ( false ) ... + requires 0 <=Int X andBool X runLemma ( X &Int #asWord ( BA ) doneLemma ( true ) ... + requires 0 <=Int X andBool X runLemma ( X &Int #asWord ( BA ) doneLemma ( false ) ... + requires 0 <=Int X andBool X runLemma ( X &Int #asWord ( BA ) <=Int Y:Int ) => doneLemma ( true ) ... + requires 0 <=Int X andBool X runLemma ( X &Int #asWord ( BA ) <=Int Y:Int ) => doneLemma ( false ) ... + requires 0 <=Int X andBool X