diff --git a/README.md b/README.md index 2100ec6523..02966e28e6 100644 --- a/README.md +++ b/README.md @@ -281,7 +281,7 @@ Files produced by test runs, e.g. kompiled definition and logs, can be found in For Developers -------------- -If built from the source, the `kevm-pyk` executable will be installed in a virtual environemtn handled by Poetry. +If built from the source, the `kevm-pyk` executable will be installed in a virtual environment handled by Poetry. You can call `kevm-pyk --help` to get a quick summary of how to use the script. Run the file `tests/ethereum-tests/BlockchainTests/GeneralStateTests/VMTests/vmArithmeticTest/add0.json`: diff --git a/deps/k_release b/deps/k_release index 45158c60d1..92d74b933f 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.0.106 +7.0.114 diff --git a/flake.lock b/flake.lock index e7446b8122..8cf8f8a4f1 100644 --- a/flake.lock +++ b/flake.lock @@ -164,17 +164,17 @@ "z3": "z3" }, "locked": { - "lastModified": 1717048155, - "narHash": "sha256-HHrXt2UoG1RbKmAGmOroQJjUbyiE+6c1dJxqoIfp3H0=", + "lastModified": 1717504162, + "narHash": "sha256-muZL1MfImaMimk+f/SwPj4xrlRvDnSpovDhAx/WqdCw=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "b6ab7a9054ae900c97c48e61027fd602dbd2acb8", + "rev": "abceb59fcbc47d1bc537ff797f806c8bb8649626", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "b6ab7a9054ae900c97c48e61027fd602dbd2acb8", + "rev": "abceb59fcbc47d1bc537ff797f806c8bb8649626", "type": "github" } }, @@ -208,16 +208,16 @@ "rv-utils": "rv-utils_3" }, "locked": { - "lastModified": 1717398151, - "narHash": "sha256-6xKGH3t5ePt7CZPYACGpwx0VOxOQ6L8Wk2Vlcafui88=", + "lastModified": 1717603356, + "narHash": "sha256-+XD9c8XcKI5x3XZCVXpFQbtBHn2Kiply1wZ7NHWENUs=", "owner": "runtimeverification", "repo": "k", - "rev": "9100689e357a7e5820362869a73684468ef9c91b", + "rev": "9629a8dfd046db68e27efc7b1c9accd783000004", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.0.106", + "ref": "v7.0.114", "repo": "k", "type": "github" } @@ -259,16 +259,16 @@ ] }, "locked": { - "lastModified": 1716543761, - "narHash": "sha256-YQIrz7KjDiwLtHMzRYxzt1+rcCUdeGDmBQl+zWOq5us=", + "lastModified": 1717532732, + "narHash": "sha256-0VTqGrolstZlxtd6DRmoWnJsYO+BB8i+PniGKenB34I=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "0b0bdaeaf5acfed9034c40bec68b285dc5fac4dc", + "rev": "caca83fbec616482760697fbf7620c45e9b560b7", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.31", + "ref": "v0.1.42", "repo": "llvm-backend", "type": "github" } @@ -413,17 +413,17 @@ }, "locked": { "dir": "pyk", - "lastModified": 1717398151, - "narHash": "sha256-6xKGH3t5ePt7CZPYACGpwx0VOxOQ6L8Wk2Vlcafui88=", + "lastModified": 1717603356, + "narHash": "sha256-+XD9c8XcKI5x3XZCVXpFQbtBHn2Kiply1wZ7NHWENUs=", "owner": "runtimeverification", "repo": "k", - "rev": "9100689e357a7e5820362869a73684468ef9c91b", + "rev": "9629a8dfd046db68e27efc7b1c9accd783000004", "type": "github" }, "original": { "dir": "pyk", "owner": "runtimeverification", - "ref": "v7.0.106", + "ref": "v7.0.114", "repo": "k", "type": "github" } diff --git a/flake.nix b/flake.nix index a2c235b5fa..350a5bc0e3 100644 --- a/flake.nix +++ b/flake.nix @@ -2,11 +2,11 @@ description = "A flake for the KEVM Semantics"; inputs = { - k-framework.url = "github:runtimeverification/k/v7.0.106"; + k-framework.url = "github:runtimeverification/k/v7.0.114"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; - pyk.url = "github:runtimeverification/k/v7.0.106?dir=pyk"; + pyk.url = "github:runtimeverification/k/v7.0.114?dir=pyk"; nixpkgs-pyk.follows = "pyk/nixpkgs"; poetry2nix.follows = "pyk/poetry2nix"; blockchain-k-plugin = { diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 5a4fe3e01c..b75df1f06e 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -814,7 +814,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "7.0.106" +version = "7.0.114" description = "" optional = false python-versions = "^3.10" @@ -835,8 +835,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/k.git" -reference = "v7.0.106" -resolved_reference = "9100689e357a7e5820362869a73684468ef9c91b" +reference = "v7.0.114" +resolved_reference = "9629a8dfd046db68e27efc7b1c9accd783000004" subdirectory = "pyk" [[package]] @@ -1100,20 +1100,20 @@ files = [ [[package]] name = "zipp" -version = "3.19.1" +version = "3.19.2" description = "Backport of pathlib-compatible object wrapper for zip files" optional = false python-versions = ">=3.8" files = [ - {file = "zipp-3.19.1-py3-none-any.whl", hash = "sha256:2828e64edb5386ea6a52e7ba7cdb17bb30a73a858f5eb6eb93d8d36f5ea26091"}, - {file = "zipp-3.19.1.tar.gz", hash = "sha256:35427f6d5594f4acf82d25541438348c26736fa9b3afa2754bcd63cdb99d8e8f"}, + {file = "zipp-3.19.2-py3-none-any.whl", hash = "sha256:f091755f667055f2d02b32c53771a7a6c8b47e1fdbc4b72a8b9072b3eef8015c"}, + {file = "zipp-3.19.2.tar.gz", hash = "sha256:bf1dcf6450f873a13e952a29504887c89e6de7506209e5b1bcc3460135d4de19"}, ] [package.extras] doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-lint"] -test = ["big-O", "jaraco.functools", "jaraco.itertools", "jaraco.test", "more-itertools", "pytest (>=6,!=8.1.*)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-ignore-flaky", "pytest-mypy", "pytest-ruff (>=0.2.1)"] +test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", "jaraco.test", "more-itertools", "pytest (>=6,!=8.1.*)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-ignore-flaky", "pytest-mypy", "pytest-ruff (>=0.2.1)"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "45437d8fea0996c09f97bef3f34aec2504c39e0a5e5aa22a1481b76687e02ffd" +content-hash = "2ad0313020cff78b809d5e32b09839482ae10979baad535ce9d79ca0d21d38d6" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index c165464421..6ebb73007b 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.583" +version = "1.0.590" description = "" authors = [ "Runtime Verification, Inc. ", @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/k.git", tag="v7.0.106", subdirectory = "pyk" } +pyk = { git = "https://github.com/runtimeverification/k.git", tag="v7.0.114", subdirectory = "pyk" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 494c52bfd2..df47a5f1b6 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '1.0.583' +VERSION: Final = '1.0.590' diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index b362e4af4c..0d7120b04c 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -157,7 +157,7 @@ def _create_argument_parser() -> ArgumentParser: kevm_kompile_spec_args.add_argument('--target', type=KompileTarget, help='[haskell|maude]') kevm_kompile_spec_args.add_argument( - '--debug-build', dest='debug_build', default=None, help='Enable debug symbols in LLVM builds.' + '--debug-build', dest='debug_build', help='Enable debug symbols in LLVM builds.' ) prove_args = command_parser.add_parser( @@ -267,12 +267,14 @@ def _create_argument_parser() -> ArgumentParser: run_args.add_argument( '--no-expand-macros', dest='expand_macros', + default=None, action='store_false', help='Do not expand macros on the input term before execution.', ) run_args.add_argument( '--debugger', dest='debugger', + default=None, action='store_true', help='Run GDB debugger for execution.', ) @@ -489,7 +491,7 @@ def default() -> dict[str, Any]: 'schedule': 'SHANGHAI', 'chainid': 1, 'mode': 'NORMAL', - 'use_gas': True, + 'usegas': True, } @staticmethod @@ -877,7 +879,7 @@ def target_args(self) -> ArgumentParser: @cached_property def k_args(self) -> ArgumentParser: args = super().definition_args - args.add_argument('--depth', default=None, type=int, help='Maximum depth to execute to.') + args.add_argument('--depth', type=int, help='Maximum depth to execute to.') return args @cached_property @@ -886,26 +888,26 @@ def kprove_args(self) -> ArgumentParser: args.add_argument( '--debug-equations', type=list_of(str, delim=','), - default=[], help='Comma-separate list of equations to debug.', ) args.add_argument( '--always-check-subsumption', dest='always_check_subsumption', - default=True, + default=None, action='store_true', help='Check subsumption even on non-terminal nodes (default, experimental).', ) args.add_argument( '--no-always-check-subsumption', dest='always_check_subsumption', + default=None, action='store_false', help='Do not check subsumption on non-terminal nodes (experimental).', ) args.add_argument( '--fast-check-subsumption', dest='fast_check_subsumption', - default=False, + default=None, action='store_true', help='Use fast-check on k-cell to determine subsumption (experimental).', ) @@ -916,21 +918,20 @@ def kprove_legacy_args(self) -> ArgumentParser: args = ArgumentParser(add_help=False) args.add_argument( '--bug-report', - default=False, + default=None, action='store_true', help='Generate a haskell-backend bug report for the execution.', ) args.add_argument( '--debugger', dest='debugger', - default=False, + default=None, action='store_true', help='Launch proof in an interactive debugger.', ) args.add_argument( '--max-depth', dest='max_depth', - default=None, type=int, help='The maximum number of computational steps to prove.', ) @@ -938,20 +939,17 @@ def kprove_legacy_args(self) -> ArgumentParser: '--max-counterexamples', type=int, dest='max_counterexamples', - default=None, help='Maximum number of counterexamples reported before a forcible stop.', ) args.add_argument( '--branching-allowed', type=int, dest='branching_allowed', - default=None, help='Number of branching events allowed before a forcible stop.', ) args.add_argument( '--haskell-backend-arg', dest='haskell_backend_args', - default=[], action='append', help='Arguments passed to the Haskell backend execution engine.', ) @@ -980,18 +978,16 @@ def evm_chain_args(self) -> ArgumentParser: args.add_argument( '--schedule', choices=schedules, - default='SHANGHAI', help=f"schedule to use for execution [{'|'.join(schedules)}].", ) - args.add_argument('--chainid', type=int, default=1, help='chain ID to use for execution.') + args.add_argument('--chainid', type=int, help='chain ID to use for execution.') args.add_argument( '--mode', choices=modes, - default='NORMAL', help="execution mode to use [{'|'.join(modes)}].", ) args.add_argument( - '--no-gas', action='store_false', dest='usegas', default=True, help='omit gas cost computations.' + '--no-gas', default=None, action='store_false', dest='usegas', help='omit gas cost computations.' ) return args @@ -1001,7 +997,7 @@ def display_args(self) -> ArgumentParser: args.add_argument( '--sort-collections', dest='sort_collections', - default=False, + default=None, action='store_true', help='Sort collections before outputting term.', ) @@ -1013,7 +1009,7 @@ def rpc_args(self) -> ArgumentParser: args.add_argument( '--trace-rewrites', dest='trace_rewrites', - default=False, + default=None, action='store_true', help='Log traces of all simplification and rewrite rule applications.', ) @@ -1021,13 +1017,12 @@ def rpc_args(self) -> ArgumentParser: '--kore-rpc-command', dest='kore_rpc_command', type=str, - default=None, help='Custom command to start RPC server.', ) args.add_argument( '--use-booster', dest='use_booster', - default=False, + default=None, action='store_true', help='Use the booster RPC server instead of kore-rpc.', ) @@ -1040,13 +1035,14 @@ def rpc_args(self) -> ArgumentParser: args.add_argument( '--post-exec-simplify', dest='post_exec_simplify', - default=True, + default=None, action='store_true', help='Always simplify states with kore backend after booster execution, only usable with --use-booster.', ) args.add_argument( '--no-post-exec-simplify', dest='post_exec_simplify', + default=None, action='store_false', help='Do not simplify states with kore backend after booster execution, only usable with --use-booster.', ) @@ -1060,14 +1056,12 @@ def rpc_args(self) -> ArgumentParser: '--port', dest='port', type=int, - default=None, help='Use existing RPC server on named port.', ) args.add_argument( '--maude-port', dest='maude_port', type=int, - default=None, help='Use existing Maude RPC server on named port.', ) return args @@ -1078,101 +1072,103 @@ def explore_args(self) -> ArgumentParser: args.add_argument( '--break-every-step', dest='break_every_step', - default=False, + default=None, action='store_true', help='Store a node for every EVM opcode step (expensive).', ) args.add_argument( '--break-on-jumpi', dest='break_on_jumpi', - default=False, + default=None, action='store_true', help='Store a node for every EVM jump opcode.', ) args.add_argument( '--break-on-calls', dest='break_on_calls', - default=False, + default=None, action='store_true', help='Store a node for every EVM call made.', ) args.add_argument( '--no-break-on-calls', dest='break_on_calls', - default=True, + default=None, action='store_false', help='Do not store a node for every EVM call made (default).', ) args.add_argument( '--break-on-storage', dest='break_on_storage', - default=False, + default=None, action='store_true', help='Store a node for every EVM SSTORE/SLOAD made.', ) args.add_argument( '--break-on-basic-blocks', dest='break_on_basic_blocks', - default=False, + default=None, action='store_true', help='Store a node for every EVM basic block (implies --break-on-calls).', ) args.add_argument( '--max-depth', dest='max_depth', - default=1000, type=int, help='Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.', ) args.add_argument( '--max-iterations', dest='max_iterations', - default=None, type=int, help='Number of times to expand the next pending node in the CFG.', ) args.add_argument( '--failure-information', dest='failure_info', - default=True, + default=None, action='store_true', help='Show failure summary for all failing tests (default).', ) args.add_argument( '--no-failure-information', dest='failure_info', + default=None, action='store_false', help='Do not show failure summary for failing tests.', ) args.add_argument( '--auto-abstract-gas', dest='auto_abstract_gas', + default=None, action='store_true', help='Automatically extract gas cell when infinite gas is enabled.', ) args.add_argument( '--counterexample-information', dest='counterexample_info', - default=True, + default=None, action='store_true', help='Show models for failing nodes (default).', ) args.add_argument( '--no-counterexample-information', dest='counterexample_info', + default=None, action='store_false', help='Do not show models for failing nodes.', ) args.add_argument( '--fail-fast', dest='fail_fast', - default=True, + default=None, action='store_true', help='Stop execution on other branches if a failing node is detected (default).', ) args.add_argument( '--no-fail-fast', dest='fail_fast', + default=None, action='store_false', help='Continue execution on other branches if a failing node is detected.', ) @@ -1184,14 +1180,12 @@ def k_gen_args(self) -> ArgumentParser: args.add_argument( '--require', dest='requires', - default=[], action='append', help='Extra K requires to include in generated output.', ) args.add_argument( '--module-import', dest='imports', - default=[], action='append', help='Extra modules to import into generated main module.', ) @@ -1204,7 +1198,6 @@ def kcfg_show_args(self) -> ArgumentParser: '--node', type=node_id_like, dest='nodes', - default=[], action='append', help='List of nodes to display as well.', ) @@ -1212,36 +1205,36 @@ def kcfg_show_args(self) -> ArgumentParser: '--node-delta', type=arg_pair_of(node_id_like, node_id_like), dest='node_deltas', - default=[], action='append', help='List of nodes to display delta for.', ) args.add_argument( '--failure-information', dest='failure_info', - default=False, + default=None, action='store_true', help='Show failure summary for cfg.', ) args.add_argument( '--no-failure-information', dest='failure_info', + default=None, action='store_false', help='Do not show failure summary for cfg.', ) args.add_argument( - '--to-module', dest='to_module', default=False, action='store_true', help='Output edges as a K module.' + '--to-module', dest='to_module', default=None, action='store_true', help='Output edges as a K module.' ) args.add_argument( - '--pending', dest='pending', default=False, action='store_true', help='Also display pending nodes.' + '--pending', dest='pending', default=None, action='store_true', help='Also display pending nodes.' ) args.add_argument( - '--failing', dest='failing', default=False, action='store_true', help='Also display failing nodes.' + '--failing', dest='failing', default=None, action='store_true', help='Also display failing nodes.' ) args.add_argument( '--counterexample-information', dest='counterexample_info', - default=False, + default=None, action='store_true', help="Show models for failing nodes. Should be called with the '--failure-information' flag.", ) diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 6c62d02abb..2732d98519 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -389,11 +389,11 @@ def to_hex(kast: KInner) -> KInner: @staticmethod def halt() -> KApply: - return KApply('#halt_EVM_KItem') + return KApply('halt') @staticmethod def sharp_execute() -> KApply: - return KApply('#execute_EVM_KItem') + return KApply('execute') @staticmethod def jumpi() -> KApply: @@ -413,7 +413,7 @@ def jump_applied(pc: KInner) -> KApply: @staticmethod def pc_applied(op: KInner) -> KApply: - return KApply('#pc[_]_EVM_InternalOp_OpCode', [op]) + return KApply('pc', [op]) @staticmethod def pow128() -> KApply: @@ -425,35 +425,35 @@ def pow256() -> KApply: @staticmethod def range_uint(width: int, i: KInner) -> KApply: - return KApply('#rangeUInt(_,_)_WORD_Bool_Int_Int', [intToken(width), i]) + return KApply('rangeUInt', [intToken(width), i]) @staticmethod def range_sint(width: int, i: KInner) -> KApply: - return KApply('#rangeSInt(_,_)_WORD_Bool_Int_Int', [intToken(width), i]) + return KApply('rangeSInt', [intToken(width), i]) @staticmethod def range_address(i: KInner) -> KApply: - return KApply('#rangeAddress(_)_WORD_Bool_Int', [i]) + return KApply('rangeAddress', [i]) @staticmethod def range_bool(i: KInner) -> KApply: - return KApply('#rangeBool(_)_WORD_Bool_Int', [i]) + return KApply('rangeBool', [i]) @staticmethod def range_bytes(width: KInner, ba: KInner) -> KApply: - return KApply('#rangeBytes(_,_)_WORD_Bool_Int_Int', [width, ba]) + return KApply('rangeBytes', [width, ba]) @staticmethod def range_nonce(i: KInner) -> KApply: - return KApply('#rangeNonce(_)_WORD_Bool_Int', [i]) + return KApply('rangeNonce', [i]) @staticmethod def range_blocknum(ba: KInner) -> KApply: - return KApply('#rangeBlockNum(_)_WORD_Bool_Int', [ba]) + return KApply('rangeBlockNum', [ba]) @staticmethod def bool_2_word(cond: KInner) -> KApply: - return KApply('bool2Word(_)_EVM-TYPES_Int_Bool', [cond]) + return KApply('bool2Word', [cond]) @staticmethod def size_bytes(ba: KInner) -> KApply: @@ -465,7 +465,7 @@ def inf_gas(g: KInner) -> KApply: @staticmethod def compute_valid_jumpdests(p: KInner) -> KApply: - return KApply('#computeValidJumpDests(_)_EVM_Set_Bytes', [p]) + return KApply('computeValidJumpDests', [p]) @staticmethod def bin_runtime(c: KInner) -> KApply: @@ -477,13 +477,11 @@ def init_bytecode(c: KInner) -> KApply: @staticmethod def is_precompiled_account(i: KInner, s: KInner) -> KApply: - return KApply('#isPrecompiledAccount(_,_)_EVM_Bool_Int_Schedule', [i, s]) + return KApply('isPrecompiledAccount', [i, s]) @staticmethod def hashed_location(compiler: str, base: KInner, offset: KInner, member_offset: int = 0) -> KApply: - location = KApply( - '#hashedLocation(_,_,_)_HASHED-LOCATIONS_Int_String_Int_IntList', [stringToken(compiler), base, offset] - ) + location = KApply('hashLoc', [stringToken(compiler), base, offset]) if member_offset > 0: location = KApply('_+Int_', [location, intToken(member_offset)]) return location @@ -494,11 +492,11 @@ def loc(accessor: KInner) -> KApply: @staticmethod def lookup(map: KInner, key: KInner) -> KApply: - return KApply('#lookup(_,_)_EVM-TYPES_Int_Map_Int', [map, key]) + return KApply('lookup', [map, key]) @staticmethod def abi_calldata(name: str, args: list[KInner]) -> KApply: - return KApply('#abiCallData(_,_)_EVM-ABI_Bytes_String_TypedArgs', [stringToken(name), KEVM.typed_args(args)]) + return KApply('abiCallData', [stringToken(name), KEVM.typed_args(args)]) @staticmethod def abi_selector(name: str) -> KApply: @@ -506,11 +504,11 @@ def abi_selector(name: str) -> KApply: @staticmethod def abi_address(a: KInner) -> KApply: - return KApply('#address(_)_EVM-ABI_TypedArg_Int', [a]) + return KApply('abi_type_address', [a]) @staticmethod def abi_bool(b: KInner) -> KApply: - return KApply('#bool(_)_EVM-ABI_TypedArg_Int', [b]) + return KApply('abi_type_bool', [b]) @staticmethod def abi_type(type: str, value: KInner) -> KApply: @@ -526,7 +524,7 @@ def abi_array(elem_type: KInner, length: KInner, elems: list[KInner]) -> KApply: @staticmethod def as_word(b: KInner) -> KApply: - return KApply('#asWord(_)_EVM-TYPES_Int_Bytes', [b]) + return KApply('asWord', [b]) @staticmethod def empty_typedargs() -> KApply: @@ -562,7 +560,7 @@ def wordstack_len(wordstack: KInner) -> int: @staticmethod def parse_bytestack(s: KInner) -> KApply: - return KApply('#parseByteStack(_)_SERIALIZATION_Bytes_String', [s]) + return KApply('parseByteStack', [s]) @staticmethod def bytes_empty() -> KApply: @@ -570,7 +568,7 @@ def bytes_empty() -> KApply: @staticmethod def buf(width: KInner, v: KInner) -> KApply: - return KApply('#buf(_,_)_BUF-SYNTAX_Bytes_Int_Int', [width, v]) + return KApply('buf', [width, v]) @staticmethod def intlist(ints: list[KInner]) -> KApply: @@ -677,7 +675,7 @@ def compute_jumpdests(sections: list[KInner]) -> KInner: offset = 0 jumpdests = [] for s in sections: - if type(s) is KApply and s.label == KLabel('#buf(_,_)_BUF-SYNTAX_Bytes_Int_Int'): + if type(s) is KApply and s.label == KLabel('buf'): width_token = s.args[0] assert type(width_token) is KToken offset += int(width_token.token) @@ -692,7 +690,7 @@ def compute_jumpdests(sections: list[KInner]) -> KInner: def _process_jumpdests(bytecode: bytes, offset: int) -> list[KToken]: - """Computes the location of JUMPDEST opcodes from a given bytecode. + """Computes the location of JUMPDEST opcodes from a given bytecode while avoiding bytes from within the PUSH opcodes. :param bytecode: The bytecode of the contract as bytes. :type bytecode: bytes @@ -701,4 +699,16 @@ def _process_jumpdests(bytecode: bytes, offset: int) -> list[KToken]: :return: A list of intToken instances representing the positions of all found jump destinations in the bytecode adjusted by the offset. :rtype: list[KToken] """ - return [intToken(offset + i) for i, byte in enumerate(bytecode) if byte == 0x5B] + push1 = 0x60 + push32 = 0x7F + jumpdest = 0x5B + i = 0 + jumpdests: list[KToken] = [] + while i < len(bytecode): + if push1 <= bytecode[i] <= push32: + i += bytecode[i] - push1 + 2 + else: + if bytecode[i] == jumpdest: + jumpdests.append(intToken(offset + i)) + i += 1 + return jumpdests diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md index 9db573e05b..3d548876b6 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md @@ -31,123 +31,123 @@ which denotes (indeed, is translated to) the following byte array: where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of `2835717307`, the first four bytes of the hash value of the `transfer` function signature, `keccak256("transfer(address,unit256)")`, and `T1 : ... : T32` and `V1 : ... : V32` are the byte-array representations of `TO` and `VALUE` respectively. ```k - syntax TypedArg ::= #address ( Int ) [klabel(abi_type_address), symbol] - | #uint256 ( Int ) [klabel(abi_type_uint256), symbol] - | #uint248 ( Int ) [klabel(abi_type_uint248), symbol] - | #uint240 ( Int ) [klabel(abi_type_uint240), symbol] - | #uint232 ( Int ) [klabel(abi_type_uint232), symbol] - | #uint224 ( Int ) [klabel(abi_type_uint224), symbol] - | #uint216 ( Int ) [klabel(abi_type_uint216), symbol] - | #uint208 ( Int ) [klabel(abi_type_uint208), symbol] - | #uint200 ( Int ) [klabel(abi_type_uint200), symbol] - | #uint192 ( Int ) [klabel(abi_type_uint192), symbol] - | #uint184 ( Int ) [klabel(abi_type_uint184), symbol] - | #uint176 ( Int ) [klabel(abi_type_uint176), symbol] - | #uint168 ( Int ) [klabel(abi_type_uint168), symbol] - | #uint160 ( Int ) [klabel(abi_type_uint160), symbol] - | #uint152 ( Int ) [klabel(abi_type_uint152), symbol] - | #uint144 ( Int ) [klabel(abi_type_uint144), symbol] - | #uint136 ( Int ) [klabel(abi_type_uint136), symbol] - | #uint128 ( Int ) [klabel(abi_type_uint128), symbol] - | #uint120 ( Int ) [klabel(abi_type_uint120), symbol] - | #uint112 ( Int ) [klabel(abi_type_uint112), symbol] - | #uint104 ( Int ) [klabel(abi_type_uint104), symbol] - | #uint96 ( Int ) [klabel(abi_type_uint96), symbol] - | #uint88 ( Int ) [klabel(abi_type_uint88), symbol] - | #uint80 ( Int ) [klabel(abi_type_uint80), symbol] - | #uint72 ( Int ) [klabel(abi_type_uint72), symbol] - | #uint64 ( Int ) [klabel(abi_type_uint64), symbol] - | #uint56 ( Int ) [klabel(abi_type_uint56), symbol] - | #uint48 ( Int ) [klabel(abi_type_uint48), symbol] - | #uint40 ( Int ) [klabel(abi_type_uint40), symbol] - | #uint32 ( Int ) [klabel(abi_type_uint32), symbol] - | #uint24 ( Int ) [klabel(abi_type_uint24), symbol] - | #uint16 ( Int ) [klabel(abi_type_uint16), symbol] - | #uint8 ( Int ) [klabel(abi_type_uint8), symbol] - | #int256 ( Int ) [klabel(abi_type_int256), symbol] - | #int248 ( Int ) [klabel(abi_type_int248), symbol] - | #int240 ( Int ) [klabel(abi_type_int240), symbol] - | #int232 ( Int ) [klabel(abi_type_int232), symbol] - | #int224 ( Int ) [klabel(abi_type_int224), symbol] - | #int216 ( Int ) [klabel(abi_type_int216), symbol] - | #int208 ( Int ) [klabel(abi_type_int208), symbol] - | #int200 ( Int ) [klabel(abi_type_int200), symbol] - | #int192 ( Int ) [klabel(abi_type_int192), symbol] - | #int184 ( Int ) [klabel(abi_type_int184), symbol] - | #int176 ( Int ) [klabel(abi_type_int176), symbol] - | #int168 ( Int ) [klabel(abi_type_int168), symbol] - | #int160 ( Int ) [klabel(abi_type_int160), symbol] - | #int152 ( Int ) [klabel(abi_type_int152), symbol] - | #int144 ( Int ) [klabel(abi_type_int144), symbol] - | #int136 ( Int ) [klabel(abi_type_int136), symbol] - | #int128 ( Int ) [klabel(abi_type_int128), symbol] - | #int120 ( Int ) [klabel(abi_type_int120), symbol] - | #int112 ( Int ) [klabel(abi_type_int112), symbol] - | #int104 ( Int ) [klabel(abi_type_int104), symbol] - | #int96 ( Int ) [klabel(abi_type_int96), symbol] - | #int88 ( Int ) [klabel(abi_type_int88), symbol] - | #int80 ( Int ) [klabel(abi_type_int80), symbol] - | #int72 ( Int ) [klabel(abi_type_int72), symbol] - | #int64 ( Int ) [klabel(abi_type_int64), symbol] - | #int56 ( Int ) [klabel(abi_type_int56), symbol] - | #int48 ( Int ) [klabel(abi_type_int48), symbol] - | #int40 ( Int ) [klabel(abi_type_int40), symbol] - | #int32 ( Int ) [klabel(abi_type_int32), symbol] - | #int24 ( Int ) [klabel(abi_type_int24), symbol] - | #int16 ( Int ) [klabel(abi_type_int16), symbol] - | #int8 ( Int ) [klabel(abi_type_int8), symbol] - | #bytes1 ( Int ) [klabel(abi_type_bytes1), symbol] - | #bytes2 ( Int ) [klabel(abi_type_bytes2), symbol] - | #bytes3 ( Int ) [klabel(abi_type_bytes3), symbol] - | #bytes4 ( Int ) [klabel(abi_type_bytes4), symbol] - | #bytes5 ( Int ) [klabel(abi_type_bytes5), symbol] - | #bytes6 ( Int ) [klabel(abi_type_bytes6), symbol] - | #bytes7 ( Int ) [klabel(abi_type_bytes7), symbol] - | #bytes8 ( Int ) [klabel(abi_type_bytes8), symbol] - | #bytes9 ( Int ) [klabel(abi_type_bytes9), symbol] - | #bytes10 ( Int ) [klabel(abi_type_bytes10), symbol] - | #bytes11 ( Int ) [klabel(abi_type_bytes11), symbol] - | #bytes12 ( Int ) [klabel(abi_type_bytes12), symbol] - | #bytes13 ( Int ) [klabel(abi_type_bytes13), symbol] - | #bytes14 ( Int ) [klabel(abi_type_bytes14), symbol] - | #bytes15 ( Int ) [klabel(abi_type_bytes15), symbol] - | #bytes16 ( Int ) [klabel(abi_type_bytes16), symbol] - | #bytes17 ( Int ) [klabel(abi_type_bytes17), symbol] - | #bytes18 ( Int ) [klabel(abi_type_bytes18), symbol] - | #bytes19 ( Int ) [klabel(abi_type_bytes19), symbol] - | #bytes20 ( Int ) [klabel(abi_type_bytes20), symbol] - | #bytes21 ( Int ) [klabel(abi_type_bytes21), symbol] - | #bytes22 ( Int ) [klabel(abi_type_bytes22), symbol] - | #bytes23 ( Int ) [klabel(abi_type_bytes23), symbol] - | #bytes24 ( Int ) [klabel(abi_type_bytes24), symbol] - | #bytes25 ( Int ) [klabel(abi_type_bytes25), symbol] - | #bytes26 ( Int ) [klabel(abi_type_bytes26), symbol] - | #bytes27 ( Int ) [klabel(abi_type_bytes27), symbol] - | #bytes28 ( Int ) [klabel(abi_type_bytes28), symbol] - | #bytes29 ( Int ) [klabel(abi_type_bytes29), symbol] - | #bytes30 ( Int ) [klabel(abi_type_bytes30), symbol] - | #bytes31 ( Int ) [klabel(abi_type_bytes31), symbol] - | #bytes32 ( Int ) [klabel(abi_type_bytes32), symbol] - | #bool ( Int ) [klabel(abi_type_bool), symbol] - | #bytes ( Bytes ) [klabel(abi_type_bytes), symbol] - | #string ( String ) [klabel(abi_type_string), symbol] - | #array ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array), symbol] - | #tuple ( TypedArgs ) [klabel(abi_type_tuple), symbol] - // ---------------------------------------------------------------------------------------------- + syntax TypedArg ::= #address ( Int ) [symbol(abi_type_address)] + | #uint256 ( Int ) [symbol(abi_type_uint256)] + | #uint248 ( Int ) [symbol(abi_type_uint248)] + | #uint240 ( Int ) [symbol(abi_type_uint240)] + | #uint232 ( Int ) [symbol(abi_type_uint232)] + | #uint224 ( Int ) [symbol(abi_type_uint224)] + | #uint216 ( Int ) [symbol(abi_type_uint216)] + | #uint208 ( Int ) [symbol(abi_type_uint208)] + | #uint200 ( Int ) [symbol(abi_type_uint200)] + | #uint192 ( Int ) [symbol(abi_type_uint192)] + | #uint184 ( Int ) [symbol(abi_type_uint184)] + | #uint176 ( Int ) [symbol(abi_type_uint176)] + | #uint168 ( Int ) [symbol(abi_type_uint168)] + | #uint160 ( Int ) [symbol(abi_type_uint160)] + | #uint152 ( Int ) [symbol(abi_type_uint152)] + | #uint144 ( Int ) [symbol(abi_type_uint144)] + | #uint136 ( Int ) [symbol(abi_type_uint136)] + | #uint128 ( Int ) [symbol(abi_type_uint128)] + | #uint120 ( Int ) [symbol(abi_type_uint120)] + | #uint112 ( Int ) [symbol(abi_type_uint112)] + | #uint104 ( Int ) [symbol(abi_type_uint104)] + | #uint96 ( Int ) [symbol(abi_type_uint96) ] + | #uint88 ( Int ) [symbol(abi_type_uint88) ] + | #uint80 ( Int ) [symbol(abi_type_uint80) ] + | #uint72 ( Int ) [symbol(abi_type_uint72) ] + | #uint64 ( Int ) [symbol(abi_type_uint64) ] + | #uint56 ( Int ) [symbol(abi_type_uint56) ] + | #uint48 ( Int ) [symbol(abi_type_uint48) ] + | #uint40 ( Int ) [symbol(abi_type_uint40) ] + | #uint32 ( Int ) [symbol(abi_type_uint32) ] + | #uint24 ( Int ) [symbol(abi_type_uint24) ] + | #uint16 ( Int ) [symbol(abi_type_uint16) ] + | #uint8 ( Int ) [symbol(abi_type_uint8) ] + | #int256 ( Int ) [symbol(abi_type_int256) ] + | #int248 ( Int ) [symbol(abi_type_int248) ] + | #int240 ( Int ) [symbol(abi_type_int240) ] + | #int232 ( Int ) [symbol(abi_type_int232) ] + | #int224 ( Int ) [symbol(abi_type_int224) ] + | #int216 ( Int ) [symbol(abi_type_int216) ] + | #int208 ( Int ) [symbol(abi_type_int208) ] + | #int200 ( Int ) [symbol(abi_type_int200) ] + | #int192 ( Int ) [symbol(abi_type_int192) ] + | #int184 ( Int ) [symbol(abi_type_int184) ] + | #int176 ( Int ) [symbol(abi_type_int176) ] + | #int168 ( Int ) [symbol(abi_type_int168) ] + | #int160 ( Int ) [symbol(abi_type_int160) ] + | #int152 ( Int ) [symbol(abi_type_int152) ] + | #int144 ( Int ) [symbol(abi_type_int144) ] + | #int136 ( Int ) [symbol(abi_type_int136) ] + | #int128 ( Int ) [symbol(abi_type_int128) ] + | #int120 ( Int ) [symbol(abi_type_int120) ] + | #int112 ( Int ) [symbol(abi_type_int112) ] + | #int104 ( Int ) [symbol(abi_type_int104) ] + | #int96 ( Int ) [symbol(abi_type_int96) ] + | #int88 ( Int ) [symbol(abi_type_int88) ] + | #int80 ( Int ) [symbol(abi_type_int80) ] + | #int72 ( Int ) [symbol(abi_type_int72) ] + | #int64 ( Int ) [symbol(abi_type_int64) ] + | #int56 ( Int ) [symbol(abi_type_int56) ] + | #int48 ( Int ) [symbol(abi_type_int48) ] + | #int40 ( Int ) [symbol(abi_type_int40) ] + | #int32 ( Int ) [symbol(abi_type_int32) ] + | #int24 ( Int ) [symbol(abi_type_int24) ] + | #int16 ( Int ) [symbol(abi_type_int16) ] + | #int8 ( Int ) [symbol(abi_type_int8) ] + | #bytes1 ( Int ) [symbol(abi_type_bytes1) ] + | #bytes2 ( Int ) [symbol(abi_type_bytes2) ] + | #bytes3 ( Int ) [symbol(abi_type_bytes3) ] + | #bytes4 ( Int ) [symbol(abi_type_bytes4) ] + | #bytes5 ( Int ) [symbol(abi_type_bytes5) ] + | #bytes6 ( Int ) [symbol(abi_type_bytes6) ] + | #bytes7 ( Int ) [symbol(abi_type_bytes7) ] + | #bytes8 ( Int ) [symbol(abi_type_bytes8) ] + | #bytes9 ( Int ) [symbol(abi_type_bytes9) ] + | #bytes10 ( Int ) [symbol(abi_type_bytes10)] + | #bytes11 ( Int ) [symbol(abi_type_bytes11)] + | #bytes12 ( Int ) [symbol(abi_type_bytes12)] + | #bytes13 ( Int ) [symbol(abi_type_bytes13)] + | #bytes14 ( Int ) [symbol(abi_type_bytes14)] + | #bytes15 ( Int ) [symbol(abi_type_bytes15)] + | #bytes16 ( Int ) [symbol(abi_type_bytes16)] + | #bytes17 ( Int ) [symbol(abi_type_bytes17)] + | #bytes18 ( Int ) [symbol(abi_type_bytes18)] + | #bytes19 ( Int ) [symbol(abi_type_bytes19)] + | #bytes20 ( Int ) [symbol(abi_type_bytes20)] + | #bytes21 ( Int ) [symbol(abi_type_bytes21)] + | #bytes22 ( Int ) [symbol(abi_type_bytes22)] + | #bytes23 ( Int ) [symbol(abi_type_bytes23)] + | #bytes24 ( Int ) [symbol(abi_type_bytes24)] + | #bytes25 ( Int ) [symbol(abi_type_bytes25)] + | #bytes26 ( Int ) [symbol(abi_type_bytes26)] + | #bytes27 ( Int ) [symbol(abi_type_bytes27)] + | #bytes28 ( Int ) [symbol(abi_type_bytes28)] + | #bytes29 ( Int ) [symbol(abi_type_bytes29)] + | #bytes30 ( Int ) [symbol(abi_type_bytes30)] + | #bytes31 ( Int ) [symbol(abi_type_bytes31)] + | #bytes32 ( Int ) [symbol(abi_type_bytes32)] + | #bool ( Int ) [symbol(abi_type_bool) ] + | #bytes ( Bytes ) [symbol(abi_type_bytes) ] + | #string ( String ) [symbol(abi_type_string) ] + | #array ( TypedArg , Int , TypedArgs ) [symbol(abi_type_array) ] + | #tuple ( TypedArgs ) [symbol(abi_type_tuple) ] + // -------------------------------------------------------------------------------------- syntax TypedArgs ::= List{TypedArg, ","} [symbol(typedArgs)] // ------------------------------------------------------------ - syntax Bytes ::= #abiCallData ( String , TypedArgs ) [klabel(#abiCallData), function] - // ------------------------------------------------------------------------------------- + syntax Bytes ::= #abiCallData ( String , TypedArgs ) [symbol(abiCallData), function] + // ------------------------------------------------------------------------------------ rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) +Bytes #encodeArgs(ARGS) - syntax Bytes ::= #signatureCallData ( String, TypedArgs ) [klabel(#signatureCallData), function] - // ------------------------------------------------------------------------------------------------ + syntax Bytes ::= #signatureCallData ( String, TypedArgs ) [symbol(signatureCallData), function] + // ----------------------------------------------------------------------------------------------- rule #signatureCallData( FNAME , ARGS ) => #parseByteStack(substrString(Keccak256(String2Bytes(#generateSignature(FNAME, ARGS))), 0, 8)) - syntax String ::= #generateSignature ( String, TypedArgs ) [klabel(#generateSignature), function, total] - | #generateSignatureArgs ( TypedArgs ) [klabel(#generateSignatureArgs),function, total] + syntax String ::= #generateSignature ( String, TypedArgs ) [symbol(generateSignature), function, total] + | #generateSignatureArgs ( TypedArgs ) [symbol(generateSignatureArgs),function, total] // -------------------------------------------------------------------------------------------------------------- rule #generateSignature( FNAME , ARGS ) => FNAME +String "(" +String #generateSignatureArgs(ARGS) +String ")" @@ -155,8 +155,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #generateSignatureArgs(TARGA:TypedArg, .TypedArgs) => #typeName(TARGA) rule #generateSignatureArgs(TARGA:TypedArg, TARGB:TypedArg, TARGS) => #typeName(TARGA) +String "," +String #generateSignatureArgs(TARGB, TARGS) - syntax String ::= #typeName ( TypedArg ) [klabel(#typeName), function, total] - // ----------------------------------------------------------------------------- + syntax String ::= #typeName ( TypedArg ) [symbol(typeName), function, total] + // ---------------------------------------------------------------------------- rule #typeName( #address( _ )) => "address" rule #typeName( #uint256( _ )) => "uint256" @@ -268,9 +268,9 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of rule #typeName( #tuple(ARGS)) => "(" +String #generateSignatureArgs(ARGS) +String ")" - syntax Bytes ::= #encodeArgs ( TypedArgs ) [klabel(#encodeArgs), function] - syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [klabel(#encodeArgsAux), function] - // ------------------------------------------------------------------------------------------------------ + syntax Bytes ::= #encodeArgs ( TypedArgs ) [symbol(encodeArgs), function] + syntax Bytes ::= #encodeArgsAux ( TypedArgs , Int , Bytes , Bytes ) [symbol(encodeArgsAux), function] + // ----------------------------------------------------------------------------------------------------- rule #encodeArgs(ARGS) => #encodeArgsAux(ARGS, #lenOfHeads(ARGS), .Bytes, .Bytes) rule #encodeArgsAux(.TypedArgs, _:Int, HEADS, TAILS) => HEADS +Bytes TAILS @@ -288,13 +288,13 @@ The `#lenOfHeads` is a recursive function used to calculate the space required f For most types, this is a fixed 32 bytes, except for static tuples, for which the length is the cumulative length of their contents. ```k - syntax Int ::= #lenOfHeads ( TypedArgs ) [klabel(#lenOfHeads), function, total] - // ------------------------------------------------------------------------------- + syntax Int ::= #lenOfHeads ( TypedArgs ) [symbol(lenOfHeads), function, total] + // ------------------------------------------------------------------------------ rule #lenOfHeads(.TypedArgs) => 0 rule #lenOfHeads(ARG, ARGS) => #lenOfHead(ARG) +Int #lenOfHeads(ARGS) - syntax Int ::= #lenOfHead ( TypedArg ) [klabel(#lenOfHead), function, total] - // ---------------------------------------------------------------------------- + syntax Int ::= #lenOfHead ( TypedArg ) [symbol(lenOfHead), function, total] + // --------------------------------------------------------------------------- rule #lenOfHead( #tuple( ARGS )) => #lenOfHeads(ARGS) requires #isStaticType(#tuple(ARGS)) rule #lenOfHead( _) => 32 [owise] ``` @@ -302,16 +302,16 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th `#isStaticType` checks if a given `TypedArg` is a static type in order to determine if it has a fixed size. ```k - syntax Bool ::= #isStaticType ( TypedArg ) [klabel(#isStaticType), function, total] - // ----------------------------------------------------------------------------------- + syntax Bool ::= #isStaticType ( TypedArg ) [symbol(isStaticType), function, total] + // ---------------------------------------------------------------------------------- rule #isStaticType( #bytes( _ )) => false rule #isStaticType( #string( _ )) => false rule #isStaticType(#array(_, _, _)) => false rule #isStaticType( #tuple( ARGS )) => notBool #hasDynamicType(ARGS) rule #isStaticType( _) => true [owise] - syntax Bool ::= #hasDynamicType(TypedArgs) [klabel(#hasDynamicType), function, total] - // ------------------------------------------------------------------------------------- + syntax Bool ::= #hasDynamicType(TypedArgs) [symbol(hasDynamicType), function, total] + // ------------------------------------------------------------------------------------ rule #hasDynamicType(.TypedArgs) => false rule #hasDynamicType(T, TS) => #hasDynamicType(TS) requires #isStaticType(T) rule #hasDynamicType(T, _) => true requires notBool #isStaticType(T) @@ -321,22 +321,22 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th - for `#bytes(BS)` and `#string(BS)`, the size is 32 bytes for the length prefix plus the size of the actual byte sequence, rounded up to the nearest multiple of 32. - for `#tuple(ARGS)`, the size is 32 bytes for the length prefix plus the cumulative size of its elements. - for `#array(T, N, _)` that has elements of a static `TypedArg` `T`, the size is `32 * (1 + N)`,which accounts for 32 bytes for the length prefix and 32 bytes for each element. - - for dynamic type arrays `#array(T, N, ELEMS)`, the size is `32 * (1 + N + #sizeOfDynamicTypeList(ELEMS))`. + - for dynamic type arrays `#array(T, N, ELEMS)`, the size is `32 * (1 + N) + #sizeOfDynamicTypeList(ELEMS)`. ```k - syntax Int ::= #sizeOfDynamicType ( TypedArg ) [klabel(#sizeOfDynamicType), function] - // ------------------------------------------------------------------------------------- + syntax Int ::= #sizeOfDynamicType ( TypedArg ) [symbol(sizeOfDynamicType), function] + // ------------------------------------------------------------------------------------ rule #sizeOfDynamicType( #bytes(BS)) => 32 +Int #ceil32(lengthBytes(BS)) rule #sizeOfDynamicType( #string(BS)) => 32 +Int #ceil32(lengthBytes(String2Bytes(BS))) rule #sizeOfDynamicType( #tuple(ARGS)) => 32 +Int #sizeOfDynamicTypeList(ARGS) rule #sizeOfDynamicType(#array(T, N, _)) => 32 *Int (1 +Int N) requires #isStaticType(T) - rule #sizeOfDynamicType(#array(T, N, ELEMS)) => 32 *Int (1 +Int N +Int #sizeOfDynamicTypeList(ELEMS)) + rule #sizeOfDynamicType(#array(T, N, ELEMS)) => (32 *Int (1 +Int N)) +Int #sizeOfDynamicTypeList(ELEMS) requires notBool #isStaticType(T) - syntax Int ::= #sizeOfDynamicTypeList ( TypedArgs ) [klabel(#sizeOfDynamicTypeList), function, total] - // ----------------------------------------------------------------------------------------------------- + syntax Int ::= #sizeOfDynamicTypeList ( TypedArgs ) [symbol(sizeOfDynamicTypeList), function, total] + // ---------------------------------------------------------------------------------------------------- rule #sizeOfDynamicTypeList(TARG, TARGS) => #sizeOfDynamicType(TARG) +Int #sizeOfDynamicTypeList(TARGS) requires notBool #isStaticType(TARG) @@ -345,8 +345,8 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th rule #sizeOfDynamicTypeList(.TypedArgs) => 0 - syntax Bytes ::= #enc ( TypedArg ) [klabel(#enc), function] - // ----------------------------------------------------------- + syntax Bytes ::= #enc ( TypedArg ) [symbol(enc), function] + // ---------------------------------------------------------- // static Type rule #enc(#address( DATA )) => #bufStrict(32, #getValue(#address( DATA ))) @@ -458,14 +458,14 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th rule #enc(#array(_, N, DATA)) => #enc(#uint256(N)) +Bytes #encodeArgs(DATA) rule #enc( #tuple( DATA )) => #encodeArgs(DATA) - syntax Bytes ::= #encBytes ( Int , Bytes ) [klabel(#encBytes), function] - // ------------------------------------------------------------------------ + syntax Bytes ::= #encBytes ( Int , Bytes ) [symbol(encBytes), function] + // ----------------------------------------------------------------------- rule #encBytes(N, BS) => #enc(#uint256(N)) +Bytes BS +Bytes #bufStrict(#ceil32(N) -Int N, 0) ``` ```k - syntax Int ::= #getValue ( TypedArg ) [klabel(#getValue), function] - // ------------------------------------------------------------------- + syntax Int ::= #getValue ( TypedArg ) [symbol(getValue), function] + // ------------------------------------------------------------------ rule #getValue( #bool( X )) => X requires #rangeBool(X) rule #getValue(#address( X )) => X requires #rangeAddress(X) @@ -602,37 +602,37 @@ where `1003892871367861763272476045097431689001461395759728643661426852242313133 ```k syntax EventArg ::= TypedArg - | #indexed ( TypedArg ) [klabel(#indexed)] - // ------------------------------------------------------------ + | #indexed ( TypedArg ) [symbol(indexed)] + // ----------------------------------------------------------- syntax EventArgs ::= List{EventArg, ","} [symbol(eventArgs)] // ------------------------------------------------------------ - syntax SubstateLogEntry ::= #abiEventLog ( Int , String , EventArgs ) [klabel(#abiEventLog), function] - // ------------------------------------------------------------------------------------------------------ + syntax SubstateLogEntry ::= #abiEventLog ( Int , String , EventArgs ) [symbol(abiEventLog), function] + // ----------------------------------------------------------------------------------------------------- rule #abiEventLog(ACCT_ID, EVENT_NAME, EVENT_ARGS) => { ACCT_ID | #getEventTopics(EVENT_NAME, EVENT_ARGS) | #encodeArgs(#getNonIndexedArgs(EVENT_ARGS)) } - syntax List ::= #getEventTopics ( String , EventArgs ) [klabel(#getEventTopics), function] - // ------------------------------------------------------------------------------------------ + syntax List ::= #getEventTopics ( String , EventArgs ) [symbol(getEventTopics), function] + // ----------------------------------------------------------------------------------------- rule #getEventTopics(ENAME, EARGS) => ListItem(#parseHexWord(Keccak256(String2Bytes(#generateSignature(ENAME, #getTypedArgs(EARGS)))))) #getIndexedArgs(EARGS) - syntax TypedArgs ::= #getTypedArgs ( EventArgs ) [klabel(#getTypedArgs), function] - // ---------------------------------------------------------------------------------- + syntax TypedArgs ::= #getTypedArgs ( EventArgs ) [symbol(getTypedArgs), function] + // --------------------------------------------------------------------------------- rule #getTypedArgs(#indexed(E), ES) => E, #getTypedArgs(ES) rule #getTypedArgs(E:TypedArg, ES) => E, #getTypedArgs(ES) rule #getTypedArgs(.EventArgs) => .TypedArgs - syntax List ::= #getIndexedArgs ( EventArgs ) [klabel(#getIndexedArgs), function] - // --------------------------------------------------------------------------------- + syntax List ::= #getIndexedArgs ( EventArgs ) [symbol(getIndexedArgs), function] + // -------------------------------------------------------------------------------- rule #getIndexedArgs(#indexed(E), ES) => ListItem(#getValue(E)) #getIndexedArgs(ES) rule #getIndexedArgs(_:TypedArg, ES) => #getIndexedArgs(ES) rule #getIndexedArgs(.EventArgs) => .List - syntax TypedArgs ::= #getNonIndexedArgs ( EventArgs ) [klabel(#getNonIndexedArgs), function] - // -------------------------------------------------------------------------------------------- + syntax TypedArgs ::= #getNonIndexedArgs ( EventArgs ) [symbol(getNonIndexedArgs), function] + // ------------------------------------------------------------------------------------------- rule #getNonIndexedArgs(#indexed(_), ES) => #getNonIndexedArgs(ES) rule #getNonIndexedArgs(E:TypedArg, ES) => E, #getNonIndexedArgs(ES) rule #getNonIndexedArgs(.EventArgs) => .TypedArgs @@ -641,8 +641,8 @@ where `1003892871367861763272476045097431689001461395759728643661426852242313133 ### Function selectors ```k - syntax Int ::= selector ( String ) [alias, klabel(abi_selector), symbol, function, no-evaluators] - // ------------------------------------------------------------------------------------------------- + syntax Int ::= selector ( String ) [alias, symbol(abi_selector), function, no-evaluators] + // ----------------------------------------------------------------------------------------- ``` ```k diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md index 01ac1f7509..5a57db23a9 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/buf.md @@ -23,7 +23,7 @@ Claims should always use `#bufStrict` in LHS and `#buf` in RHS. ```k syntax Bytes ::= #bufStrict ( Int , Int ) [klabel(#bufStrict), function] - syntax Bytes ::= #buf ( Int , Int ) [klabel(#buf), function, total, smtlib(buf)] + syntax Bytes ::= #buf ( Int , Int ) [symbol(buf), function, total, smtlib(buf)] syntax Int ::= #ceil32 ( Int ) [klabel(#ceil32), macro] // ------------------------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md index 676d5f70d2..fca29562ba 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md @@ -27,9 +27,9 @@ module BIN-RUNTIME imports EVM-ABI syntax Contract - syntax Bytes ::= #binRuntime ( Contract ) [alias, klabel(binRuntime), symbol, function, no-evaluators] - | #initBytecode ( Contract ) [alias, klabel(initBytecode), symbol, function, no-evaluators] - // ------------------------------------------------------------------------------------------------------ + syntax Bytes ::= #binRuntime ( Contract ) [alias, symbol(binRuntime) , function, no-evaluators] + | #initBytecode ( Contract ) [alias, symbol(initBytecode), function, no-evaluators] + // -------------------------------------------------------------------------------------------------- endmodule ``` diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index 8255fe104f..c4f46f6172 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -27,7 +27,7 @@ Primitives provide the basic conversion from K's sorts `Int` and `Bool` to EVM's - `word2Bool` interprets a `Int` as a `Bool`. ```k - syntax Int ::= bool2Word ( Bool ) [klabel(bool2Word), function, total, smtlib(bool2Word)] + syntax Int ::= bool2Word ( Bool ) [symbol(bool2Word), function, total, smtlib(bool2Word)] // ----------------------------------------------------------------------------------------- rule bool2Word( true ) => 1 rule bool2Word( false ) => 0 @@ -342,8 +342,8 @@ Bytes helper functions - `#padToWidth(N, WS)` and `#padRightToWidth` make sure that a `Bytes` is the correct size. ```k - syntax Int ::= #asWord ( Bytes ) [klabel(#asWord), function, total, smtlib(asWord)] - // ----------------------------------------------------------------------------------- + syntax Int ::= #asWord ( Bytes ) [symbol(asWord), function, total, smtlib(asWord)] + // ---------------------------------------------------------------------------------- rule #asWord(WS) => chop(Bytes2Int(WS, BE, Unsigned)) [concrete] syntax Int ::= #asInteger ( Bytes ) [klabel(#asInteger), function, total] @@ -407,9 +407,9 @@ Storage/Memory Lookup `#lookup*` looks up a key in a map and returns 0 if the key doesn't exist, otherwise returning its value. ```k - syntax Int ::= #lookup ( Map , Int ) [klabel(#lookup), function, total, smtlib(lookup)] - | #lookupMemory ( Map , Int ) [klabel(#lookupMemory), function, total, smtlib(lookupMemory)] - // ---------------------------------------------------------------------------------------------------------- + syntax Int ::= #lookup ( Map , Int ) [symbol(lookup), function, total, smtlib(lookup)] + | #lookupMemory ( Map , Int ) [symbol(lookupMemory), function, total, smtlib(lookupMemory)] + // --------------------------------------------------------------------------------------------------------- rule [#lookup.some]: #lookup( (KEY |-> VAL:Int) _M, KEY ) => VAL modInt pow256 rule [#lookup.none]: #lookup( M, KEY ) => 0 requires notBool KEY in_keys(M) //Impossible case, for completeness 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 73f258c234..74a33200f1 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -183,9 +183,9 @@ Our semantics is modal, with the initial mode being set on the command line via - `VMTESTS` skips `CALL*` and `CREATE` operations. ```k - syntax Mode ::= "NORMAL" [klabel(NORMAL), symbol] - | "VMTESTS" [klabel(VMTESTS), symbol] - // --------------------------------------------------- + syntax Mode ::= "NORMAL" [symbol(NORMAL) ] + | "VMTESTS" [symbol(VMTESTS)] + // ------------------------------------------- ``` State Stacks @@ -259,8 +259,9 @@ Control Flow - `#end_` sets the `statusCode` and the program counter of the last executed opcode, then halts execution. ```k - syntax KItem ::= "#halt" | "#end" StatusCode - // -------------------------------------------- + syntax KItem ::= "#halt" [symbol(halt)] + | "#end" StatusCode [symbol(end) ] + // ------------------------------------------------- rule [end]: #end SC => #halt ... _ => SC @@ -289,8 +290,8 @@ OpCode Execution - `#execute` loads the next opcode. ```k - syntax KItem ::= "#execute" - // --------------------------- + syntax KItem ::= "#execute" [symbol(execute)] + // --------------------------------------------- rule [halt]: #halt ~> (#execute => .K) ... @@ -509,8 +510,8 @@ The arguments to `PUSH` must be skipped over (as they are inline), and the opcod - `#pc` calculates the next program counter of the given operator. ```k - syntax InternalOp ::= "#pc" "[" OpCode "]" - // ------------------------------------------ + syntax InternalOp ::= "#pc" "[" OpCode "]" [symbol(pc)] + // ------------------------------------------------------- rule #pc [ OP ] => .K ... PCOUNT => PCOUNT +Int #widthOp(OP) @@ -1049,7 +1050,7 @@ The `JUMP*` family of operations affect the current program counter. syntax BinStackOp ::= "JUMPI" // ----------------------------- - rule [jumpi.false]: JUMPI _DEST I => .K ... requires I ==Int 0 + rule [jumpi.false]: JUMPI _DEST I => .K ... requires I ==Int 0 rule [jumpi.true]: JUMPI DEST I => JUMP DEST ... requires I =/=Int 0 syntax InternalOp ::= "#endBasicBlock" @@ -1335,8 +1336,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d rule [precompile.true]: #precompiled?(ACCTCODE, SCHED) => #next [ #precompiled(ACCTCODE) ] ... requires #isPrecompiledAccount(ACCTCODE, SCHED) [preserves-definedness] rule [precompile.false]: #precompiled?(ACCTCODE, SCHED) => .K ... requires notBool #isPrecompiledAccount(ACCTCODE, SCHED) - syntax Bool ::= #isPrecompiledAccount ( Int , Schedule ) [klabel(#isPrecompiledAccount), function, total, smtlib(isPrecompiledAccount)] - // --------------------------------------------------------------------------------------------------------------------------------------- + syntax Bool ::= #isPrecompiledAccount ( Int , Schedule ) [symbol(isPrecompiledAccount), function, total, smtlib(isPrecompiledAccount)] + // -------------------------------------------------------------------------------------------------------------------------------------- rule [isPrecompiledAccount]: #isPrecompiledAccount(ACCTCODE, SCHED) => 0 #accessAccounts ADDRSET:Set => .K ... TOUCHED_ACCOUNTS => TOUCHED_ACCOUNTS |Set ADDRSET - syntax Set ::= #computeValidJumpDests(Bytes) [klabel(#computeValidJumpDests), function, memo, total] - | #computeValidJumpDests(Bytes, Int, List) [klabel(#computeValidJumpDestsAux), function ] - // ------------------------------------------------------------------------------------------------------------------ + syntax Set ::= #computeValidJumpDests(Bytes) [symbol(computeValidJumpDests), function, memo, total] + | #computeValidJumpDests(Bytes, Int, List) [symbol(computeValidJumpDests), function ] + // ----------------------------------------------------------------------------------------------------------------- rule #computeValidJumpDests(_PGM) => .Set rule #computeValidJumpDests(_PGM, _I, _RESULT) => .Set diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md index 5b6653e7f9..085f29445f 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -57,7 +57,8 @@ In particular, this means that `#gas(_) false`, and `#gas(_) <=G module INFINITE-GAS imports GAS - syntax Gas ::= #gas(Int) [klabel(infGas), symbol, smtlib(infGas)] + syntax Gas ::= #gas(Int) [symbol(infGas), smtlib(infGas)] + // --------------------------------------------------------- rule #gas(G) +Gas G' => #gas(G +Int G') rule #gas(G) -Gas G' => #gas(G -Int G') @@ -207,8 +208,8 @@ module GAS-FEES rule [Cinitcode.new]: Cinitcode(SCHED, INITCODELEN) => Ginitcodewordcost < SCHED > *Int ( INITCODELEN up/Int 32 ) requires Ghasmaxinitcodesize << SCHED >> [concrete] rule [Cinitcode.old]: Cinitcode(SCHED, _) => 0 requires notBool Ghasmaxinitcodesize << SCHED >> [concrete] - syntax Bool ::= #accountEmpty ( AccountCode , Int , Int ) [function, total, klabel(accountEmpty), symbol] - // --------------------------------------------------------------------------------------------------------- + syntax Bool ::= #accountEmpty ( AccountCode , Int , Int ) [function, total, symbol(accountEmpty)] + // ------------------------------------------------------------------------------------------------- rule #accountEmpty(CODE, NONCE, BAL) => CODE ==K .Bytes andBool NONCE ==Int 0 andBool BAL ==Int 0 syntax Gas ::= #allBut64th ( Gas ) [symbol(#allBut64th_Gas), overload(#allBut64th), function, total, smtlib(gas_allBut64th_Gas)] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md index 51977f681e..af784ca907 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md @@ -54,7 +54,7 @@ More information about how storage locations are defined in Solidity can be foun Specifically, `#hashedLocation` is defined as follows, capturing the storage layout schemes of Solidity and Vyper. ```k - syntax Int ::= #hashedLocation( String , Int , IntList ) [klabel(hashLoc), function, smtlib(hashLoc)] + syntax Int ::= #hashedLocation( String , Int , IntList ) [symbol(hashLoc), function, smtlib(hashLoc)] // ----------------------------------------------------------------------------------------------------- rule #hashedLocation(_LANG, BASE, .IntList ) => BASE rule #hashedLocation( LANG, BASE, OFFSET OFFSETS) => #hashedLocation(LANG, #hashedLocation(LANG, BASE, OFFSET .IntList), OFFSETS) requires OFFSETS =/=K .IntList @@ -78,17 +78,17 @@ module SOLIDITY-FIELDS syntax Contract syntax Field syntax ContractAccess ::= Contract - | ContractAccess "." Field [klabel(contract_access_field), symbol] - | ContractAccess "[" Int "]" [klabel(contract_access_index), symbol] - // -------------------------------------------------------------------------------------------- + | ContractAccess "." Field [symbol(contract_access_field)] + | ContractAccess "[" Int "]" [symbol(contract_access_index)] + // ------------------------------------------------------------------------------------ - syntax Int ::= #loc ( ContractAccess ) [klabel(contract_access_loc), function, symbol] - // -------------------------------------------------------------------------------------- + syntax Int ::= #loc ( ContractAccess ) [symbol(contract_access_loc), function] + // ------------------------------------------------------------------------------ rule #loc(_:Contract) => 0 rule #loc(C [ I ]) => #hash(#loc(C), I) - syntax Int ::= #hash ( Int , Int ) [klabel(contract_access_hash), function, symbol] - // ----------------------------------------------------------------------------------- + syntax Int ::= #hash ( Int , Int ) [symbol(contract_access_hash), function] + // --------------------------------------------------------------------------- rule #hash(I1, I2) => keccak(#bufStrict(32, I2) +Bytes #bufStrict(32, I1)) endmodule diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md index 78491f535c..94ec093152 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/json-rpc.md @@ -95,8 +95,8 @@ module JSON-RPC .List - syntax JSON ::= "undef" [klabel(JSON-RPCundef), symbol] - // ------------------------------------------------------- + syntax JSON ::= "undef" [symbol(JSON-RPCundef)] + // ----------------------------------------------- syntax Bool ::= isProperJson ( JSON ) [klabel(isProperJson), function] | isProperJsonList ( JSONs ) [klabel(isProperJsonList), function] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index d46be3575d..8dd7628f1b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -54,8 +54,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Default Schedule ```k - syntax Schedule ::= "DEFAULT" [klabel(DEFAULT_EVM), symbol, smtlib(schedule_DEFAULT)] - // ------------------------------------------------------------------------------------- + syntax Schedule ::= "DEFAULT" [symbol(DEFAULT_EVM), smtlib(schedule_DEFAULT)] + // ----------------------------------------------------------------------------- rule Gzero < DEFAULT > => 0 rule Gbase < DEFAULT > => 2 rule Gverylow < DEFAULT > => 3 @@ -150,8 +150,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Frontier Schedule ```k - syntax Schedule ::= "FRONTIER" [klabel(FRONTIER_EVM), symbol, smtlib(schedule_FRONTIER)] - // ---------------------------------------------------------------------------------------- + syntax Schedule ::= "FRONTIER" [symbol(FRONTIER_EVM), smtlib(schedule_FRONTIER)] + // -------------------------------------------------------------------------------- rule Gtxcreate < FRONTIER > => 21000 rule SCHEDCONST < FRONTIER > => SCHEDCONST < DEFAULT > requires SCHEDCONST =/=K Gtxcreate @@ -161,8 +161,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Homestead Schedule ```k - syntax Schedule ::= "HOMESTEAD" [klabel(HOMESTEAD_EVM), symbol, smtlib(schedule_HOMESTEAD)] - // ------------------------------------------------------------------------------------------- + syntax Schedule ::= "HOMESTEAD" [symbol(HOMESTEAD_EVM), smtlib(schedule_HOMESTEAD)] + // ----------------------------------------------------------------------------------- rule SCHEDCONST < HOMESTEAD > => SCHEDCONST < DEFAULT > rule SCHEDFLAG << HOMESTEAD >> => SCHEDFLAG << DEFAULT >> @@ -171,8 +171,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Tangerine Whistle Schedule ```k - syntax Schedule ::= "TANGERINE_WHISTLE" [klabel(TANGERINE_WHISTLE_EVM), symbol, smtlib(schedule_TANGERINE_WHISTLE)] - // ------------------------------------------------------------------------------------------------------------------- + syntax Schedule ::= "TANGERINE_WHISTLE" [symbol(TANGERINE_WHISTLE_EVM), smtlib(schedule_TANGERINE_WHISTLE)] + // ----------------------------------------------------------------------------------------------------------- rule Gbalance < TANGERINE_WHISTLE > => 400 rule Gsload < TANGERINE_WHISTLE > => 200 rule Gcall < TANGERINE_WHISTLE > => 700 @@ -194,8 +194,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Spurious Dragon Schedule ```k - syntax Schedule ::= "SPURIOUS_DRAGON" [klabel(SPURIOUS_DRAGON_EVM), symbol, smtlib(schedule_SPURIOUS_DRAGON)] - // ------------------------------------------------------------------------------------------------------------- + syntax Schedule ::= "SPURIOUS_DRAGON" [symbol(SPURIOUS_DRAGON_EVM), smtlib(schedule_SPURIOUS_DRAGON)] + // ----------------------------------------------------------------------------------------------------- rule Gexpbyte < SPURIOUS_DRAGON > => 50 rule maxCodeSize < SPURIOUS_DRAGON > => 24576 @@ -210,8 +210,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Byzantium Schedule ```k - syntax Schedule ::= "BYZANTIUM" [klabel(BYZANTIUM_EVM), symbol, smtlib(schedule_BYZANTIUM)] - // ------------------------------------------------------------------------------------------- + syntax Schedule ::= "BYZANTIUM" [symbol(BYZANTIUM_EVM), smtlib(schedule_BYZANTIUM)] + // ----------------------------------------------------------------------------------- rule Rb < BYZANTIUM > => 3 *Int eth rule SCHEDCONST < BYZANTIUM > => SCHEDCONST < SPURIOUS_DRAGON > requires notBool ( SCHEDCONST ==K Rb ) @@ -226,8 +226,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Constantinople Schedule ```k - syntax Schedule ::= "CONSTANTINOPLE" [klabel(CONSTANTINOPLE_EVM), symbol, smtlib(schedule_CONSTANTINOPLE)] - // ---------------------------------------------------------------------------------------------------------- + syntax Schedule ::= "CONSTANTINOPLE" [symbol(CONSTANTINOPLE_EVM), smtlib(schedule_CONSTANTINOPLE)] + // -------------------------------------------------------------------------------------------------- rule Rb < CONSTANTINOPLE > => 2 *Int eth rule SCHEDCONST < CONSTANTINOPLE > => SCHEDCONST < BYZANTIUM > requires notBool ( SCHEDCONST ==K Rb ) @@ -243,8 +243,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Petersburg Schedule ```k - syntax Schedule ::= "PETERSBURG" [klabel(PETERSBURG_EVM), symbol, smtlib(schedule_PETERSBURG)] - // ---------------------------------------------------------------------------------------------- + syntax Schedule ::= "PETERSBURG" [symbol(PETERSBURG_EVM), smtlib(schedule_PETERSBURG)] + // -------------------------------------------------------------------------------------- rule SCHEDCONST < PETERSBURG > => SCHEDCONST < CONSTANTINOPLE > rule Ghasdirtysstore << PETERSBURG >> => false @@ -255,8 +255,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Istanbul Schedule ```k - syntax Schedule ::= "ISTANBUL" [klabel(ISTANBUL_EVM), symbol, smtlib(schedule_ISTANBUL)] - // ---------------------------------------------------------------------------------------- + syntax Schedule ::= "ISTANBUL" [symbol(ISTANBUL_EVM), smtlib(schedule_ISTANBUL)] + // -------------------------------------------------------------------------------- rule Gecadd < ISTANBUL > => 150 rule Gecmul < ISTANBUL > => 6000 rule Gecpairconst < ISTANBUL > => 45000 @@ -289,8 +289,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Berlin Schedule ```k - syntax Schedule ::= "BERLIN" [klabel(BERLIN_EVM), symbol, smtlib(schedule_BERLIN)] - // ---------------------------------------------------------------------------------- + syntax Schedule ::= "BERLIN" [symbol(BERLIN_EVM), smtlib(schedule_BERLIN)] + // -------------------------------------------------------------------------- rule Gcoldsload < BERLIN > => 2100 rule Gcoldaccountaccess < BERLIN > => 2600 rule Gwarmstorageread < BERLIN > => 100 @@ -319,8 +319,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### London Schedule ```k - syntax Schedule ::= "LONDON" [klabel(LONDON_EVM), symbol, smtlib(schedule_LONDON)] - // ---------------------------------------------------------------------------------- + syntax Schedule ::= "LONDON" [symbol(LONDON_EVM), smtlib(schedule_LONDON)] + // -------------------------------------------------------------------------- rule Rselfdestruct < LONDON > => 0 rule Rsstoreclear < LONDON > => Gsstorereset < LONDON > +Int Gaccessliststoragekey < LONDON > rule Rmaxquotient < LONDON > => 5 @@ -341,8 +341,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Merge Schedule ```k - syntax Schedule ::= "MERGE" [klabel(MERGE_EVM), symbol, smtlib(schedule_MERGE)] - // ------------------------------------------------------------------------------- + syntax Schedule ::= "MERGE" [symbol(MERGE_EVM), smtlib(schedule_MERGE)] + // ----------------------------------------------------------------------- rule Rb < MERGE > => 0 rule SCHEDCONST < MERGE > => SCHEDCONST < LONDON > requires notBool SCHEDCONST ==K Rb @@ -355,8 +355,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. ### Shanghai Schedule ```k - syntax Schedule ::= "SHANGHAI" [klabel(SHANGHAI_EVM), symbol, smtlib(schedule_SHANGHAI)] - // ---------------------------------------------------------------------------------------- + syntax Schedule ::= "SHANGHAI" [symbol(SHANGHAI_EVM), smtlib(schedule_SHANGHAI)] + // -------------------------------------------------------------------------------- rule maxInitCodeSize < SHANGHAI > => 2 *Int maxCodeSize < SHANGHAI > rule Ginitcodewordcost < SHANGHAI > => 2 rule SCHEDCONST < SHANGHAI > => SCHEDCONST < MERGE > diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index 69f1ce8c67..3fd8c34359 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -61,13 +61,13 @@ Address/Hash Helpers - `#blockHeaderHash` computes the hash of a block header given all the block data. ```k - syntax Int ::= #blockHeaderHash( Int , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int , Int , Bytes , Int , Int ) [function, klabel(blockHeaderHash), symbol] - | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, klabel(#blockHashHeaderBytes), symbol] - | #blockHeaderHash( Int , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int , Int , Bytes , Int , Int , Int) [function, klabel(blockHeaderHashBaseFee), symbol] - | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, klabel(#blockHashHeaderBaseFeeBytes), symbol] - | #blockHeaderHash( Int , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int , Int , Bytes , Int , Int , Int , Int) [function, klabel(blockHeaderHashWithdrawals), symbol] - | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, klabel(#blockHashHeaderWithdrawalsBytes), symbol] - // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- + syntax Int ::= #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int ) [function, symbol(blockHeaderHash) ] + | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(#blockHashHeaderBytes) ] + | #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int ) [function, symbol(blockHeaderHashBaseFee) ] + | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes ) [function, symbol(#blockHashHeaderBaseFeeBytes) ] + | #blockHeaderHash(Int , Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int , Int , Bytes, Int , Int , Int , Int ) [function, symbol(blockHeaderHashWithdrawals) ] + | #blockHeaderHash(Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes, Bytes) [function, symbol(#blockHashHeaderWithdrawalsBytes)] + // ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- rule #blockHeaderHash(HP:Bytes, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN) => #parseHexWord( Keccak256( #rlpEncode( [ HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN ] ) ) ) @@ -113,8 +113,8 @@ Address/Hash Helpers - `#hashSignedTx` Takes transaction data. Returns the hash of the rlp-encoded transaction with R S and V. ```k - syntax Bytes ::= #hashSignedTx( Int , Int , Int , Account , Int , Bytes , Int , Bytes , Bytes ) [klabel(#hashSignedTx), function] - | #hashTxData ( TxData ) [klabel(#hashTxData), function] + syntax Bytes ::= #hashTxData ( TxData ) [klabel(#hashTxData), function] + | #hashSignedTx( Int , Int , Int , Account , Int , Bytes , Int , Bytes , Bytes ) [klabel(#hashSignedTx), function] // --------------------------------------------------------------------------------------------------------------------------------- rule #hashSignedTx(TN, TP, TG, TT, TV, TD, TW, TR, TS) => Keccak256raw( #rlpEncode([ TN, TP, TG, #addrBytes(TT), TV, TD, TW, TR, TS ]) ) @@ -142,8 +142,8 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s - `#parseAccessListStorageKeys` interprets a JSON list object as a Set, casting each string element as a `Word`. ```k - syntax Int ::= #parseHexWord ( String ) [klabel(#parseHexWord), function] - | #parseWord ( String ) [klabel(#parseWord), function] + syntax Int ::= #parseWord ( String ) [klabel(#parseWord), function] + | #parseHexWord ( String ) [klabel(#parseHexWord), function] // ------------------------------------------------------------------------- rule #parseHexWord("") => 0 rule #parseHexWord("0x") => 0 @@ -158,16 +158,15 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s rule #alignHexString(S) => S requires lengthString(S) modInt 2 ==Int 0 rule #alignHexString(S) => "0" +String S requires notBool lengthString(S) modInt 2 ==Int 0 - syntax Bytes ::= #parseHexBytes ( String ) [klabel(#parseHexBytes), function] - | #parseHexBytesAux ( String ) [klabel(#parseHexBytesAux), function] - | #parseByteStack ( String ) [klabel(#parseByteStack), function, memo] - // --------------------------------------------------------- + syntax Bytes ::= #parseHexBytes ( String ) [symbol(parseHexBytes), function] + | #parseHexBytesAux ( String ) [symbol(parseHexBytesAux), function] + | #parseByteStack ( String ) [symbol(parseByteStack), function, memo] + // --------------------------------------------------------------------------------------- rule #parseByteStack(S) => #parseHexBytes(replaceAll(S, "0x", "")) - rule #parseHexBytes(S) => #parseHexBytesAux(#alignHexString(S)) + rule #parseHexBytesAux("") => .Bytes - rule #parseHexBytesAux(S) => Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE) - requires lengthString(S) >=Int 2 + rule #parseHexBytesAux(S) => Int2Bytes(lengthString(S) /Int 2, String2Base(S, 16), BE) requires lengthString(S) >=Int 2 syntax Map ::= #parseMap ( JSON ) [klabel(#parseMap), function] // --------------------------------------------------------------- @@ -183,7 +182,7 @@ These parsers can interperet hex-encoded strings as `Int`s, `Bytes`s, and `Map`s | #parseAccessListStorageKeys ( JSONs , List ) [klabel(#parseAccessListStorageKeysAux), function] // -------------------------------------------------------------------------------------------------------------- rule #parseAccessListStorageKeys( J ) => #parseAccessListStorageKeys(J, .List) - rule #parseAccessListStorageKeys([S:Bytes, REST], RESULT:List) => #parseAccessListStorageKeys([REST], ListItem(#asWord(S)) RESULT ) + rule #parseAccessListStorageKeys([S:Bytes, REST ], RESULT:List) => #parseAccessListStorageKeys([REST], ListItem(#asWord(S)) RESULT ) rule #parseAccessListStorageKeys([ .JSONs ], RESULT:List) => RESULT ``` @@ -192,16 +191,16 @@ Unparsing - `#padByte` ensures that the `String` interperetation of a `Int` is wide enough. ```k - syntax String ::= #padByte( String ) [klabel(#padByte), function] - // ----------------------------------------------------------------- + syntax String ::= #padByte ( String ) [klabel(#padByte), function] + // ------------------------------------------------------------------ rule #padByte( S ) => S requires lengthString(S) ==K 2 rule #padByte( S ) => "0" +String S requires lengthString(S) ==K 1 - syntax String ::= #unparseQuantity( Int ) [klabel(#unparseQuantity), function] - // ------------------------------------------------------------------------------ + syntax String ::= #unparseQuantity ( Int ) [klabel(#unparseQuantity), function] + // ------------------------------------------------------------------------------- rule #unparseQuantity( I ) => "0x" +String Base2String(I, 16) - syntax String ::= #unparseData ( Int, Int ) [klabel(#unparseData), function] + syntax String ::= #unparseData ( Int, Int ) [klabel(#unparseData ), function] | #unparseDataBytes ( Bytes ) [klabel(#unparseDataBytes), function] // --------------------------------------------------------------------------------------- rule #unparseData( DATA, LENGTH ) => #unparseDataBytes(#padToWidth(LENGTH,#asByteStack(DATA))) @@ -213,9 +212,9 @@ Unparsing - `#wordBytes` Takes an Int and represents it as a 32-byte wide Bytes ```k - syntax Bytes ::= #addrBytes( Account ) [klabel(#addrBytes), function] - | #wordBytes( Int ) [klabel(#wordBytes), function] - // --------------------------------------------------------------------- + syntax Bytes ::= #addrBytes ( Account ) [klabel(#addrBytes), function] + | #wordBytes ( Int ) [klabel(#wordBytes), function] + // ---------------------------------------------------------------------- rule #addrBytes(.Account) => .Bytes rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT) rule #wordBytes(WORD) => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD) @@ -239,12 +238,12 @@ Encoding example: `#rlpEncode( [ 0, 1, 1, "", #parseByteStack("0xef880") ] )` ```k - syntax Bytes ::= #rlpEncodeInt ( Int ) [klabel(#rlpEncodeInt), function] - | #rlpEncodeWord ( Int ) [klabel(#rlpEncodeWord), function] + syntax Bytes ::= #rlpEncodeInt ( Int ) [klabel(#rlpEncodeInt ), function] + | #rlpEncodeWord ( Int ) [klabel(#rlpEncodeWord ), function] | #rlpEncodeAddress ( Account ) [klabel(#rlpEncodeAddress), function] - | #rlpEncodeString ( String ) [klabel(#rlpEncodeString), function] - | #rlpEncodeBytes ( Bytes ) [klabel(#rlpEncodeBytes), function] - | #rlpEncode ( JSON ) [klabel(#rlpEncode), function] + | #rlpEncodeString ( String ) [klabel(#rlpEncodeString ), function] + | #rlpEncodeBytes ( Bytes ) [klabel(#rlpEncodeBytes ), function] + | #rlpEncode ( JSON ) [klabel(#rlpEncode ), function] | #rlpEncode ( JSONs, StringBuffer ) [klabel(#rlpEncodeJsonAux), function] // ----------------------------------------------------------------------------------------- rule #rlpEncodeInt(0) => b"\x80" @@ -277,8 +276,8 @@ Encoding rule #rlpEncodeLength(BYTES, OFFSET) => #rlpEncodeLength(BYTES, OFFSET, #asByteStack(lengthBytes(BYTES))) requires notBool ( lengthBytes(BYTES) #asByteStack(lengthBytes(BL) +Int OFFSET +Int 55) +Bytes BL +Bytes BYTES - syntax Bytes ::= #rlpEncodeFullAccount( Int, Int, Map, Bytes ) [klabel(#rlpEncodeFullAccount), function] - // -------------------------------------------------------------------------------------------------------- + syntax Bytes ::= #rlpEncodeFullAccount ( Int , Int , Map , Bytes ) [klabel(#rlpEncodeFullAccount), function] + // ------------------------------------------------------------------------------------------------------------ rule [rlpAcct]: #rlpEncodeFullAccount( NONCE, BAL, STORAGE, CODE ) => #rlpEncodeLength( #rlpEncodeInt(NONCE) +Bytes #rlpEncodeInt(BAL) @@ -287,10 +286,10 @@ Encoding , 192 ) - syntax Bytes ::= #rlpEncodeReceipt ( Int , Int , Bytes , List ) [klabel(#rlpEncodeReceipt), function] - | #rlpEncodeLogs ( List ) [klabel(#rlpEncodeLogs), function] - | #rlpEncodeLogsAux ( List, StringBuffer ) [klabel(#rlpEncodeLogsAux), function] - | #rlpEncodeTopics ( List, StringBuffer ) [klabel(#rlpEncodeTopics), function] + syntax Bytes ::= #rlpEncodeTopics ( List , StringBuffer ) [klabel(#rlpEncodeTopics ), function] + | #rlpEncodeReceipt ( Int , Int , Bytes , List ) [klabel(#rlpEncodeReceipt), function] + | #rlpEncodeLogs ( List ) [klabel(#rlpEncodeLogs ), function] + | #rlpEncodeLogsAux ( List , StringBuffer ) [klabel(#rlpEncodeLogsAux), function] // ----------------------------------------------------------------------------------------------------- rule [rlpReceipt]: #rlpEncodeReceipt(RS, RG, RB, RL) => #rlpEncodeLength( #rlpEncodeInt(RS) @@ -318,8 +317,8 @@ Encoding , ( OUT => OUT +String Bytes2String( #rlpEncodeWord(X) ) ) ) - syntax Bytes ::= #rlpEncodeTxData( TxData ) [klabel(#rlpEncodeTxData), function] - // -------------------------------------------------------------------------------- + syntax Bytes ::= #rlpEncodeTxData ( TxData ) [klabel(#rlpEncodeTxData), function] + // --------------------------------------------------------------------------------- rule #rlpEncodeTxData( LegacyTxData( TN, TP, TG, TT, TV, TD ) ) => #rlpEncode( [ TN, TP, TG, #addrBytes(TT), TV, TD ] ) @@ -361,12 +360,12 @@ Encoding , 192 ) - syntax Bytes ::= MerkleMapRLP( Map, Int ) [klabel(MerkleMapRLP), function] - // -------------------------------------------------------------------------- + syntax Bytes ::= MerkleMapRLP ( Map , Int ) [klabel(MerkleMapRLP), function] + // ---------------------------------------------------------------------------- rule MerkleMapRLP(M, I) => #rlpMerkleH( #rlpEncodeMerkleTree( { M[I] orDefault .MerkleTree }:>MerkleTree ) ) - syntax Bytes ::= #rlpMerkleH ( Bytes ) [function,klabel(MerkleRLPAux)] - // ---------------------------------------------------------------------- + syntax Bytes ::= #rlpMerkleH ( Bytes ) [function, klabel(MerkleRLPAux)] + // ----------------------------------------------------------------------- rule #rlpMerkleH ( X ) => #rlpEncodeBytes( #parseByteStack( Keccak256( X ) ) ) requires lengthBytes(X) >=Int 32 @@ -381,16 +380,16 @@ Decoding - `#rlpDecodeList` RLP decodes a single `Bytes` into a `JSONs`, interpereting the input as the RLP encoding of a list. ```k - syntax JSON ::= #rlpDecode(Bytes) [klabel(#rlpDecode), function] - | #rlpDecode(Bytes, LengthPrefix) [klabel(#rlpDecodeAux), function] - // --------------------------------------------------------------------------------- + syntax JSON ::= #rlpDecode ( Bytes ) [klabel(#rlpDecode ), function] + | #rlpDecode ( Bytes , LengthPrefix) [klabel(#rlpDecodeAux), function] + // ------------------------------------------------------------------------------------ rule #rlpDecode(BYTES) => #rlpDecode(BYTES, #decodeLengthPrefix(BYTES, 0)) rule #rlpDecode(BYTES, #str( LEN, POS)) => substrBytes(BYTES, POS, POS +Int LEN) rule #rlpDecode(BYTES, #list(_LEN, POS)) => [#rlpDecodeList(BYTES, POS)] - syntax JSONs ::= #rlpDecodeList(Bytes, Int) [klabel(#rlpDecodeList), function] - | #rlpDecodeList(Bytes, Int, LengthPrefix) [klabel(#rlpDecodeListAux), function] - // ----------------------------------------------------------------------------------------------- + syntax JSONs ::= #rlpDecodeList (Bytes , Int ) [klabel(#rlpDecodeList ), function] + | #rlpDecodeList (Bytes , Int , LengthPrefix) [klabel(#rlpDecodeListAux), function] + // -------------------------------------------------------------------------------------------------- rule #rlpDecodeList(BYTES, POS) => #rlpDecodeList(BYTES, POS, #decodeLengthPrefix(BYTES, POS)) requires POS .JSONs [owise] rule #rlpDecodeList(BYTES, POS, _:LengthPrefixType(L, P)) => #rlpDecode(substrBytes(BYTES, POS, L +Int P)) , #rlpDecodeList(BYTES, L +Int P) @@ -414,8 +413,8 @@ Decoding rule #decodeLengthPrefixLength(#list, BYTES, START, B0) => #decodeLengthPrefixLength(#list, START, B0 -Int 192 -Int 56 +Int 1, #asWord(substrBytes(BYTES, START +Int 1, START +Int 1 +Int (B0 -Int 192 -Int 56 +Int 1)))) rule #decodeLengthPrefixLength(TYPE, START, LL, L) => TYPE(L, START +Int 1 +Int LL) - syntax JSONs ::= #rlpDecodeTransaction(Bytes) [klabel(#rlpDecodeTransaction), function] - // --------------------------------------------------------------------------------------- + syntax JSONs ::= #rlpDecodeTransaction ( Bytes ) [klabel(#rlpDecodeTransaction), function] + // ------------------------------------------------------------------------------------------ rule #rlpDecodeTransaction(T) => #range(T, 0, 1), #rlpDecode(#range(T, 1, lengthBytes(T) -Int 1)) ``` @@ -429,25 +428,23 @@ Merkle Patricia Tree syntax KItem ::= Int | MerkleTree // For testing purposes syntax MerkleTree ::= ".MerkleTree" - | MerkleBranch ( Map, String ) [klabel(MerkleBranch)] + | MerkleBranch ( Map, String ) [klabel(MerkleBranch )] | MerkleExtension ( Bytes, MerkleTree ) [klabel(MerkleExtension)] - | MerkleLeaf ( Bytes, String ) [klabel(MerkleLeaf)] + | MerkleLeaf ( Bytes, String ) [klabel(MerkleLeaf )] // ------------------------------------------------------------------------------------- - syntax MerkleTree ::= MerkleUpdate ( MerkleTree, String, String ) [klabel(MerkleUpdate), function] + syntax MerkleTree ::= MerkleUpdate ( MerkleTree, String, String ) [klabel(MerkleUpdate ), function] | MerkleUpdate ( MerkleTree, Bytes, String ) [klabel(MerkleUpdateAux), function] - | MerklePut ( MerkleTree, Bytes, String ) [klabel(MerklePut), function] - | MerkleDelete ( MerkleTree, Bytes ) [klabel(MerkleDelete), function] + | MerklePut ( MerkleTree, Bytes, String ) [klabel(MerklePut ), function] + | MerkleDelete ( MerkleTree, Bytes ) [klabel(MerkleDelete ), function] // ----------------------------------------------------------------------------------------------------- rule MerkleUpdate ( TREE, S:String, VALUE ) => MerkleUpdate ( TREE, #nibbleize ( String2Bytes( S ) ), VALUE ) rule MerkleUpdate ( TREE, PATH:Bytes, VALUE ) => MerklePut ( TREE, PATH, VALUE ) requires VALUE =/=String "" rule MerkleUpdate ( TREE, PATH:Bytes, "" ) => MerkleDelete ( TREE, PATH ) - rule MerklePut ( .MerkleTree, PATH:Bytes, VALUE ) => MerkleLeaf ( PATH, VALUE ) - - rule MerklePut ( MerkleLeaf ( LEAFPATH, _ ), PATH, VALUE ) - => MerkleLeaf( LEAFPATH, VALUE ) + rule MerklePut ( .MerkleTree, PATH, VALUE ) => MerkleLeaf( PATH, VALUE ) + rule MerklePut ( MerkleLeaf ( LEAFPATH, _ ), PATH, VALUE ) => MerkleLeaf( LEAFPATH, VALUE ) requires LEAFPATH ==K PATH rule MerklePut ( MerkleLeaf ( LEAFPATH, LEAFVALUE ), PATH, VALUE ) @@ -535,7 +532,7 @@ Merkle Tree Aux Functions ```k syntax Bytes ::= #nibbleize ( Bytes ) [klabel(#nibbleize), function] - | #byteify ( Bytes ) [klabel(#byteify), function] + | #byteify ( Bytes ) [klabel(#byteify ), function] // -------------------------------------------------------------------- rule #nibbleize ( B ) => ( #range( #asByteStack ( B [ 0 ] /Int 16 ), 0, 1 ) +Bytes ( #range( #asByteStack ( B [ 0 ] %Int 16 ), 0, 1 ) ) @@ -564,8 +561,8 @@ Merkle Tree Aux Functions rule HPEncodeAux ( X ) => 2 requires notBool X ==Int 0 syntax Map ::= #cleanBranchMap ( Map ) [klabel(#cleanBranchMap), function] - | #cleanBranchMapAux ( Map, List, Set ) [klabel(#cleanBranchMapAux), function] - // ------------------------------------------------------------------------------------------- + | #cleanBranchMapAux ( Map , List, Set ) [klabel(#cleanBranchMapAux), function] + // -------------------------------------------------------------------------------------------- rule #cleanBranchMap( M ) => #cleanBranchMapAux( M, keys_list(M), .Set ) rule #cleanBranchMapAux( M, .List, S ) => removeAll( M, S ) @@ -676,7 +673,7 @@ Tree Root Helper Functions rule #precompiledAccountsMapAux( (ListItem( ACCT ) => .List) _, M => M[#parseByteStack ( #unparseData( ACCT, 20 ) ) <- #emptyContractRLP] ) syntax Bytes ::= "#emptyContractRLP" [function] - // ------------------------------------------------ + // ----------------------------------------------- rule #emptyContractRLP => #rlpEncodeLength( #rlpEncodeInt(0) +Bytes #rlpEncodeInt(0) +Bytes #rlpEncodeBytes( #parseByteStack( Keccak256(b"\x80") ) ) 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 a108d39f0d..7b6cba66b8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md @@ -470,17 +470,17 @@ Range of types -------------- ```k - syntax Bool ::= #rangeBool ( Int ) [klabel(#rangeBool), alias] - | #rangeSInt ( Int , Int ) [klabel(#rangeSInt), alias] - | #rangeUInt ( Int , Int ) [klabel(#rangeUInt), alias] - | #rangeSFixed ( Int , Int , Int ) [klabel(#rangeSFixed), alias] - | #rangeUFixed ( Int , Int , Int ) [klabel(#rangeUFixed), alias] - | #rangeAddress ( Int ) [klabel(#rangeAddress), alias] - | #rangeBytes ( Int , Int ) [klabel(#rangeBytes), alias] - | #rangeNonce ( Int ) [klabel(#rangeNonce), alias] - | #rangeSmall ( Int ) [klabel(#rangeSmall), alias] - | #rangeBlockNum ( Int ) [klabel(#rangeBlockNum), alias] - // ---------------------------------------------------------------------------------- + syntax Bool ::= #rangeBool ( Int ) [symbol(rangeBool) , alias] + | #rangeSInt ( Int , Int ) [symbol(rangeSInt) , alias] + | #rangeUInt ( Int , Int ) [symbol(rangeUInt) , alias] + | #rangeSFixed ( Int , Int , Int ) [symbol(rangeSFixed) , alias] + | #rangeUFixed ( Int , Int , Int ) [symbol(rangeUFixed) , alias] + | #rangeAddress ( Int ) [symbol(rangeAddress) , alias] + | #rangeBytes ( Int , Int ) [symbol(rangeBytes) , alias] + | #rangeNonce ( Int ) [symbol(rangeNonce) , alias] + | #rangeSmall ( Int ) [symbol(rangeSmall) , alias] + | #rangeBlockNum ( Int ) [symbol(rangeBlockNum), alias] + // --------------------------------------------------------------------------------- rule #rangeBool ( X ) => X ==Int 0 orBool X ==Int 1 rule #rangeSInt ( 8 , X ) => #range ( minSInt8 <= X <= maxSInt8 ) diff --git a/kevm-pyk/src/tests/unit/test_kevm.py b/kevm-pyk/src/tests/unit/test_kevm.py index 39e4389c1e..4dc2a2a02b 100644 --- a/kevm-pyk/src/tests/unit/test_kevm.py +++ b/kevm-pyk/src/tests/unit/test_kevm.py @@ -106,6 +106,7 @@ def test_kinner_to_hex(test_id: str, input: KInner, result: KInner) -> None: ], set_of([token(68), token(104), token(105), token(106), token(108)]), ), + ('jump_to_push', [token(bytes.fromhex('6001600055600A56605B5B'))], set_of([token(10)])), ] diff --git a/package/version b/package/version index 2fbb265a00..67a3b03096 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.583 +1.0.590 diff --git a/tests/specs/functional/abi-spec.k b/tests/specs/functional/abi-spec.k index 4b4d84bd5c..0d27b80096 100644 --- a/tests/specs/functional/abi-spec.k +++ b/tests/specs/functional/abi-spec.k @@ -39,4 +39,26 @@ module ABI-SPEC ... + claim [sizeOfDynamicType-2455]: + runLemma( + #sizeOfDynamicType( + #array( + #bytes(b"\x00"), + 3, + #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc") + ) + ) + ==Int + lengthBytes(#enc( + #array( + #bytes(b"\x00"), + 3, + #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc") + ) + )) + ) + => doneLemma(true) + ... + + endmodule diff --git a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k index b470162431..998ff13da0 100644 --- a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k @@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k index a7fd833423..3dd65adb3a 100644 --- a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k @@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k index 97a1f9b956..e76c5c2f5a 100644 --- a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k @@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k index ea22345d83..31fdc65a90 100644 --- a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k +++ b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k @@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) @@ -487,7 +487,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\xdd\x80a\x00\x1f`\x009`\x00\xf3\xfe`\x80`@R4\x80\x15`\x0fW`\x00\x80\xfd[P`\x046\x10`FW`\x005`\xe0\x1c\x80c\x15\xe6z\xa6\x14`KW\x80c03A;\x14`]W\x80c]3\xa2\x7f\x14`wW\x80cak\x8d\x05\x14`\x7fW[`\x00\x80\xfd[`[`V6`\x04`\x8fV[`\x01UV[\x00[`e`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`e`\x01T\x81V[`[`\x8a6`\x04`\x8fV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xa0W`\x00\x80\xfd[P5\x91\x90PV\xfe\xa2dipfsX\"\x12 k\xdd\x86\x85\x7f\xfc\x83n#6Y\x8de\xd5'\xc1*\x92U3\x1e\xbcVQ\x12,\xdc\x15\x7fVH\xf5dsolcC\x00\x08\r\x003" - ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ( 491460923342184218035706888008750043977755113263 => 263400868551549723330807389252719309078400616203 ) diff --git a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k index 68007c03a5..36f71fe482 100644 --- a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k +++ b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k @@ -143,7 +143,7 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC ( SetItem ( 1019 ) ( SetItem ( 102 ) ( SetItem ( 1028 ) ( SetItem ( 1040 ) ( SetItem ( 1068 ) ( SetItem ( 1155 ) ( SetItem ( 1175 ) ( SetItem ( 1249 ) ( SetItem ( 1269 ) ( SetItem ( 1359 ) ( SetItem ( 1395 ) ( SetItem ( 140 ) ( SetItem ( 1401 ) ( SetItem ( 1404 ) ( SetItem ( 1440 ) ( SetItem ( 1471 ) ( SetItem ( 1515 ) ( SetItem ( 1549 ) ( SetItem ( 1563 ) ( SetItem ( 1592 ) ( SetItem ( 16 ) ( SetItem ( 1612 ) ( SetItem ( 1648 ) ( SetItem ( 1756 ) ( SetItem ( 1818 ) ( SetItem ( 1842 ) ( SetItem ( 1878 ) ( SetItem ( 1909 ) ( SetItem ( 1953 ) ( SetItem ( 1987 ) ( SetItem ( 200 ) ( SetItem ( 2001 ) ( SetItem ( 2030 ) ( SetItem ( 2050 ) ( SetItem ( 2062 ) ( SetItem ( 2090 ) ( SetItem ( 2177 ) ( SetItem ( 2197 ) ( SetItem ( 2281 ) ( SetItem ( 2301 ) ( SetItem ( 234 ) ( SetItem ( 239 ) ( SetItem ( 2391 ) ( SetItem ( 2427 ) ( SetItem ( 2434 ) ( SetItem ( 2436 ) ( SetItem ( 247 ) ( SetItem ( 2470 ) ( SetItem ( 260 ) ( SetItem ( 2612 ) ( SetItem ( 2638 ) ( SetItem ( 269 ) ( SetItem ( 2699 ) ( SetItem ( 2704 ) ( SetItem ( 2728 ) ( SetItem ( 2732 ) ( SetItem ( 2737 ) ( SetItem ( 277 ) ( SetItem ( 2833 ) ( SetItem ( 285 ) ( SetItem ( 2946 ) ( SetItem ( 304 ) ( SetItem ( 3128 ) ( SetItem ( 3132 ) ( SetItem ( 328 ) ( SetItem ( 3286 ) ( SetItem ( 3312 ) ( SetItem ( 336 ) ( SetItem ( 3373 ) ( SetItem ( 3378 ) ( SetItem ( 3383 ) ( SetItem ( 3400 ) ( SetItem ( 3413 ) ( SetItem ( 3441 ) ( SetItem ( 3478 ) ( SetItem ( 349 ) ( SetItem ( 3490 ) ( SetItem ( 3530 ) ( SetItem ( 3591 ) ( SetItem ( 363 ) ( SetItem ( 3633 ) ( SetItem ( 3654 ) ( SetItem ( 3669 ) ( SetItem ( 368 ) ( SetItem ( 3687 ) ( SetItem ( 3694 ) ( SetItem ( 3697 ) ( SetItem ( 370 ) ( SetItem ( 3721 ) ( SetItem ( 3736 ) ( SetItem ( 3742 ) ( SetItem ( 378 ) ( SetItem ( 3781 ) ( SetItem ( 3820 ) ( SetItem ( 3851 ) ( SetItem ( 3864 ) ( SetItem ( 3882 ) ( SetItem ( 3889 ) ( SetItem ( 3909 ) ( SetItem ( 391 ) ( SetItem ( 3941 ) ( SetItem ( 3947 ) ( SetItem ( 3982 ) ( SetItem ( 399 ) ( SetItem ( 3996 ) ( SetItem ( 4014 ) ( SetItem ( 4024 ) ( SetItem ( 4042 ) ( SetItem ( 4058 ) ( SetItem ( 407 ) ( SetItem ( 4082 ) ( SetItem ( 4112 ) ( SetItem ( 415 ) ( SetItem ( 4157 ) ( SetItem ( 4162 ) ( SetItem ( 4173 ) ( SetItem ( 4178 ) ( SetItem ( 4180 ) ( SetItem ( 4188 ) ( SetItem ( 4206 ) ( SetItem ( 4221 ) ( SetItem ( 4228 ) ( SetItem ( 423 ) ( SetItem ( 4245 ) ( SetItem ( 4252 ) ( SetItem ( 4283 ) ( SetItem ( 439 ) ( SetItem ( 478 ) ( SetItem ( 486 ) ( SetItem ( 499 ) ( SetItem ( 557 ) ( SetItem ( 587 ) ( SetItem ( 597 ) ( SetItem ( 693 ) ( SetItem ( 789 ) ( SetItem ( 825 ) ( SetItem ( 933 ) SetItem ( 995 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 96 ) ( SetItem ( 91 ) ( SetItem ( 217 ) ( SetItem ( 116 ) ( SetItem ( 114 ) ( SetItem ( 112 ) ( SetItem ( 107 ) ( SetItem ( 179 ) ( SetItem ( 162 ) ( SetItem ( 122 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 140 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 96 ) ( SetItem ( 91 ) ( SetItem ( 217 ) ( SetItem ( 114 ) ( SetItem ( 112 ) ( SetItem ( 107 ) ( SetItem ( 179 ) ( SetItem ( 162 ) ( SetItem ( 122 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 140 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) @@ -781,7 +781,7 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC ( SetItem ( 3490 ) ( SetItem ( 2434 ) ( SetItem ( 2050 ) ( SetItem ( 4162 ) ( SetItem ( 2946 ) ( SetItem ( 1155 ) ( SetItem ( 995 ) ( SetItem ( 1987 ) ( SetItem ( 1440 ) ( SetItem ( 2177 ) ( SetItem ( 1249 ) ( SetItem ( 1953 ) ( SetItem ( 2470 ) ( SetItem ( 486 ) ( SetItem ( 102 ) ( SetItem ( 3654 ) ( SetItem ( 423 ) ( SetItem ( 391 ) ( SetItem ( 3591 ) ( SetItem ( 3687 ) ( SetItem ( 260 ) ( SetItem ( 2436 ) ( SetItem ( 1028 ) ( SetItem ( 4228 ) ( SetItem ( 3941 ) ( SetItem ( 3909 ) ( SetItem ( 933 ) ( SetItem ( 3781 ) ( SetItem ( 3530 ) ( SetItem ( 2090 ) ( SetItem ( 234 ) ( SetItem ( 3882 ) ( SetItem ( 4042 ) ( SetItem ( 363 ) ( SetItem ( 1515 ) ( SetItem ( 3851 ) ( SetItem ( 3947 ) ( SetItem ( 587 ) ( SetItem ( 2699 ) ( SetItem ( 328 ) ( SetItem ( 3400 ) ( SetItem ( 200 ) ( SetItem ( 2728 ) ( SetItem ( 2281 ) ( SetItem ( 3721 ) ( SetItem ( 2062 ) ( SetItem ( 4206 ) ( SetItem ( 4014 ) ( SetItem ( 3982 ) ( SetItem ( 2030 ) ( SetItem ( 3694 ) ( SetItem ( 2638 ) ( SetItem ( 1359 ) ( SetItem ( 399 ) ( SetItem ( 239 ) ( SetItem ( 1068 ) ( SetItem ( 140 ) ( SetItem ( 1612 ) ( SetItem ( 2732 ) ( SetItem ( 3820 ) ( SetItem ( 3373 ) ( SetItem ( 269 ) ( SetItem ( 4173 ) ( SetItem ( 557 ) ( SetItem ( 1549 ) ( SetItem ( 3378 ) ( SetItem ( 370 ) ( SetItem ( 4178 ) ( SetItem ( 1842 ) ( SetItem ( 4082 ) ( SetItem ( 1395 ) ( SetItem ( 499 ) ( SetItem ( 304 ) ( SetItem ( 368 ) ( SetItem ( 336 ) ( SetItem ( 4112 ) ( SetItem ( 16 ) ( SetItem ( 1040 ) ( SetItem ( 3312 ) ( SetItem ( 1648 ) ( SetItem ( 2704 ) ( SetItem ( 3441 ) ( SetItem ( 3889 ) ( SetItem ( 2833 ) ( SetItem ( 2001 ) ( SetItem ( 3633 ) ( SetItem ( 3697 ) ( SetItem ( 2737 ) ( SetItem ( 3478 ) ( SetItem ( 3286 ) ( SetItem ( 1878 ) ( SetItem ( 3383 ) ( SetItem ( 2391 ) ( SetItem ( 439 ) ( SetItem ( 407 ) ( SetItem ( 1175 ) ( SetItem ( 247 ) ( SetItem ( 4180 ) ( SetItem ( 2612 ) ( SetItem ( 277 ) ( SetItem ( 3413 ) ( SetItem ( 4245 ) ( SetItem ( 2197 ) ( SetItem ( 1269 ) ( SetItem ( 789 ) ( SetItem ( 1909 ) ( SetItem ( 597 ) ( SetItem ( 3669 ) ( SetItem ( 693 ) ( SetItem ( 378 ) ( SetItem ( 1818 ) ( SetItem ( 4058 ) ( SetItem ( 2427 ) ( SetItem ( 4283 ) ( SetItem ( 1019 ) ( SetItem ( 1563 ) ( SetItem ( 3128 ) ( SetItem ( 3864 ) ( SetItem ( 4024 ) ( SetItem ( 1592 ) ( SetItem ( 3736 ) ( SetItem ( 1401 ) ( SetItem ( 825 ) ( SetItem ( 478 ) ( SetItem ( 3742 ) ( SetItem ( 1471 ) ( SetItem ( 415 ) ( SetItem ( 1404 ) ( SetItem ( 3132 ) ( SetItem ( 4188 ) ( SetItem ( 4252 ) ( SetItem ( 3996 ) ( SetItem ( 1756 ) ( SetItem ( 285 ) ( SetItem ( 349 ) ( SetItem ( 4157 ) ( SetItem ( 4221 ) SetItem ( 2301 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 76 ) ( SetItem ( 65 ) ( SetItem ( 60 ) ( SetItem ( 15 ) ( SetItem ( 81 ) ( SetItem ( 83 ) ( SetItem ( 85 ) ( SetItem ( 91 ) ( SetItem ( 109 ) ( SetItem ( 131 ) ( SetItem ( 124 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 148 ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 76 ) ( SetItem ( 65 ) ( SetItem ( 60 ) ( SetItem ( 15 ) ( SetItem ( 81 ) ( SetItem ( 83 ) ( SetItem ( 91 ) ( SetItem ( 109 ) ( SetItem ( 131 ) ( SetItem ( 124 ) ( SetItem ( 186 ) ( SetItem ( 155 ) SetItem ( 148 ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k index 7d4c632962..edbdda5fb0 100644 --- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k @@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k index b509ad60fa..e0ce79b9c6 100644 --- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k @@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k index 1eb0948e74..2f08def8c8 100644 --- a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k @@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 16 ) ( SetItem ( 86 ) ( SetItem ( 48 ) ( SetItem ( 91 ) ( SetItem ( 343 ) ( SetItem ( 377 ) ( SetItem ( 361 ) ( SetItem ( 331 ) ( SetItem ( 384 ) ( SetItem ( 274 ) ( SetItem ( 224 ) ( SetItem ( 233 ) ( SetItem ( 116 ) ( SetItem ( 110 ) ( SetItem ( 105 ) ( SetItem ( 170 ) ( SetItem ( 172 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 151 ) ( SetItem ( 146 ) ( SetItem ( 401 ) ( SetItem ( 447 ) SetItem ( 429 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 86 ) ( SetItem ( 48 ) ( SetItem ( 91 ) ( SetItem ( 343 ) ( SetItem ( 377 ) ( SetItem ( 361 ) ( SetItem ( 331 ) ( SetItem ( 384 ) ( SetItem ( 274 ) ( SetItem ( 224 ) ( SetItem ( 233 ) ( SetItem ( 110 ) ( SetItem ( 105 ) ( SetItem ( 172 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 151 ) ( SetItem ( 146 ) ( SetItem ( 401 ) ( SetItem ( 447 ) SetItem ( 429 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k index d3631bb499..6e1813638e 100644 --- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k @@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k index 350d818327..d3469b1192 100644 --- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k @@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k index 8174547f28..4f1c87767d 100644 --- a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k +++ b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k @@ -143,7 +143,7 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC ( SetItem ( 10007 ) ( SetItem ( 10035 ) ( SetItem ( 10053 ) ( SetItem ( 1030 ) ( SetItem ( 1054 ) ( SetItem ( 1074 ) ( SetItem ( 1082 ) ( SetItem ( 113 ) ( SetItem ( 1150 ) ( SetItem ( 1159 ) ( SetItem ( 1217 ) ( SetItem ( 1247 ) ( SetItem ( 1257 ) ( SetItem ( 1271 ) ( SetItem ( 1299 ) ( SetItem ( 1378 ) ( SetItem ( 1398 ) ( SetItem ( 1459 ) ( SetItem ( 1479 ) ( SetItem ( 1486 ) ( SetItem ( 151 ) ( SetItem ( 1582 ) ( SetItem ( 16 ) ( SetItem ( 1678 ) ( SetItem ( 1692 ) ( SetItem ( 1720 ) ( SetItem ( 1807 ) ( SetItem ( 1827 ) ( SetItem ( 1898 ) ( SetItem ( 1922 ) ( SetItem ( 1981 ) ( SetItem ( 1998 ) ( SetItem ( 2023 ) ( SetItem ( 2059 ) ( SetItem ( 2167 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2253 ) ( SetItem ( 2262 ) ( SetItem ( 2338 ) ( SetItem ( 2358 ) ( SetItem ( 2370 ) ( SetItem ( 2372 ) ( SetItem ( 2386 ) ( SetItem ( 2414 ) ( SetItem ( 2493 ) ( SetItem ( 2513 ) ( SetItem ( 2579 ) ( SetItem ( 2615 ) ( SetItem ( 2619 ) ( SetItem ( 2655 ) ( SetItem ( 2686 ) ( SetItem ( 2730 ) ( SetItem ( 2764 ) ( SetItem ( 2778 ) ( SetItem ( 2807 ) ( SetItem ( 2827 ) ( SetItem ( 2841 ) ( SetItem ( 2869 ) ( SetItem ( 2948 ) ( SetItem ( 2968 ) ( SetItem ( 3034 ) ( SetItem ( 304 ) ( SetItem ( 3070 ) ( SetItem ( 3147 ) ( SetItem ( 3167 ) ( SetItem ( 3228 ) ( SetItem ( 3281 ) ( SetItem ( 3307 ) ( SetItem ( 3327 ) ( SetItem ( 3390 ) ( SetItem ( 3410 ) ( SetItem ( 3416 ) ( SetItem ( 3452 ) ( SetItem ( 3560 ) ( SetItem ( 3622 ) ( SetItem ( 3646 ) ( SetItem ( 3660 ) ( SetItem ( 3688 ) ( SetItem ( 371 ) ( SetItem ( 376 ) ( SetItem ( 3767 ) ( SetItem ( 3787 ) ( SetItem ( 3848 ) ( SetItem ( 3868 ) ( SetItem ( 3882 ) ( SetItem ( 390 ) ( SetItem ( 3910 ) ( SetItem ( 395 ) ( SetItem ( 397 ) ( SetItem ( 3989 ) ( SetItem ( 4025 ) ( SetItem ( 405 ) ( SetItem ( 4056 ) ( SetItem ( 4100 ) ( SetItem ( 413 ) ( SetItem ( 4134 ) ( SetItem ( 4148 ) ( SetItem ( 4177 ) ( SetItem ( 4197 ) ( SetItem ( 4231 ) ( SetItem ( 426 ) ( SetItem ( 435 ) ( SetItem ( 4373 ) ( SetItem ( 4399 ) ( SetItem ( 443 ) ( SetItem ( 4460 ) ( SetItem ( 4465 ) ( SetItem ( 4489 ) ( SetItem ( 4493 ) ( SetItem ( 4498 ) ( SetItem ( 451 ) ( SetItem ( 4512 ) ( SetItem ( 4540 ) ( SetItem ( 459 ) ( SetItem ( 4627 ) ( SetItem ( 4647 ) ( SetItem ( 467 ) ( SetItem ( 4721 ) ( SetItem ( 475 ) ( SetItem ( 4797 ) ( SetItem ( 4811 ) ( SetItem ( 483 ) ( SetItem ( 4839 ) ( SetItem ( 4935 ) ( SetItem ( 496 ) ( SetItem ( 4961 ) ( SetItem ( 4981 ) ( SetItem ( 504 ) ( SetItem ( 5064 ) ( SetItem ( 512 ) ( SetItem ( 5160 ) ( SetItem ( 5174 ) ( SetItem ( 520 ) ( SetItem ( 5202 ) ( SetItem ( 5304 ) ( SetItem ( 5324 ) ( SetItem ( 533 ) ( SetItem ( 5402 ) ( SetItem ( 541 ) ( SetItem ( 5442 ) ( SetItem ( 5469 ) ( SetItem ( 549 ) ( SetItem ( 5567 ) ( SetItem ( 557 ) ( SetItem ( 5587 ) ( SetItem ( 565 ) ( SetItem ( 5666 ) ( SetItem ( 5702 ) ( SetItem ( 5717 ) ( SetItem ( 5728 ) ( SetItem ( 573 ) ( SetItem ( 5762 ) ( SetItem ( 5772 ) ( SetItem ( 581 ) ( SetItem ( 5883 ) ( SetItem ( 589 ) ( SetItem ( 5938 ) ( SetItem ( 5993 ) ( SetItem ( 6009 ) ( SetItem ( 605 ) ( SetItem ( 6122 ) ( SetItem ( 613 ) ( SetItem ( 6177 ) ( SetItem ( 621 ) ( SetItem ( 6232 ) ( SetItem ( 6248 ) ( SetItem ( 6275 ) ( SetItem ( 629 ) ( SetItem ( 6314 ) ( SetItem ( 6339 ) ( SetItem ( 6349 ) ( SetItem ( 6357 ) ( SetItem ( 6363 ) ( SetItem ( 6367 ) ( SetItem ( 637 ) ( SetItem ( 6373 ) ( SetItem ( 645 ) ( SetItem ( 6527 ) ( SetItem ( 6553 ) ( SetItem ( 658 ) ( SetItem ( 6614 ) ( SetItem ( 6619 ) ( SetItem ( 6624 ) ( SetItem ( 6641 ) ( SetItem ( 6654 ) ( SetItem ( 6667 ) ( SetItem ( 6680 ) ( SetItem ( 6698 ) ( SetItem ( 672 ) ( SetItem ( 6721 ) ( SetItem ( 6728 ) ( SetItem ( 6756 ) ( SetItem ( 6793 ) ( SetItem ( 6805 ) ( SetItem ( 6845 ) ( SetItem ( 6906 ) ( SetItem ( 6948 ) ( SetItem ( 6969 ) ( SetItem ( 6984 ) ( SetItem ( 6987 ) ( SetItem ( 700 ) ( SetItem ( 7011 ) ( SetItem ( 7028 ) ( SetItem ( 7052 ) ( SetItem ( 7072 ) ( SetItem ( 7111 ) ( SetItem ( 7139 ) ( SetItem ( 7157 ) ( SetItem ( 7170 ) ( SetItem ( 7231 ) ( SetItem ( 7250 ) ( SetItem ( 7311 ) ( SetItem ( 7329 ) ( SetItem ( 7345 ) ( SetItem ( 7365 ) ( SetItem ( 7397 ) ( SetItem ( 7403 ) ( SetItem ( 7438 ) ( SetItem ( 7452 ) ( SetItem ( 7470 ) ( SetItem ( 7480 ) ( SetItem ( 7502 ) ( SetItem ( 7520 ) ( SetItem ( 7544 ) ( SetItem ( 7564 ) ( SetItem ( 7582 ) ( SetItem ( 7622 ) ( SetItem ( 7647 ) ( SetItem ( 7664 ) ( SetItem ( 7675 ) ( SetItem ( 7694 ) ( SetItem ( 7711 ) ( SetItem ( 7753 ) ( SetItem ( 7771 ) ( SetItem ( 7779 ) ( SetItem ( 7821 ) ( SetItem ( 7863 ) ( SetItem ( 7877 ) ( SetItem ( 789 ) ( SetItem ( 7919 ) ( SetItem ( 7941 ) ( SetItem ( 7973 ) ( SetItem ( 7997 ) ( SetItem ( 8029 ) ( SetItem ( 8089 ) ( SetItem ( 809 ) ( SetItem ( 8094 ) ( SetItem ( 8102 ) ( SetItem ( 8104 ) ( SetItem ( 8118 ) ( SetItem ( 8123 ) ( SetItem ( 8143 ) ( SetItem ( 8157 ) ( SetItem ( 8162 ) ( SetItem ( 8193 ) ( SetItem ( 8202 ) ( SetItem ( 8230 ) ( SetItem ( 8248 ) ( SetItem ( 8272 ) ( SetItem ( 8296 ) ( SetItem ( 8303 ) ( SetItem ( 8324 ) ( SetItem ( 8347 ) ( SetItem ( 8375 ) ( SetItem ( 8387 ) ( SetItem ( 8400 ) ( SetItem ( 8419 ) ( SetItem ( 8442 ) ( SetItem ( 8454 ) ( SetItem ( 8466 ) ( SetItem ( 8507 ) ( SetItem ( 8544 ) ( SetItem ( 8553 ) ( SetItem ( 8573 ) ( SetItem ( 8651 ) ( SetItem ( 8664 ) ( SetItem ( 867 ) ( SetItem ( 8692 ) ( SetItem ( 8730 ) ( SetItem ( 8743 ) ( SetItem ( 8772 ) ( SetItem ( 8797 ) ( SetItem ( 8802 ) ( SetItem ( 8808 ) ( SetItem ( 8810 ) ( SetItem ( 8873 ) ( SetItem ( 8892 ) ( SetItem ( 8968 ) ( SetItem ( 9000 ) ( SetItem ( 9060 ) ( SetItem ( 9065 ) ( SetItem ( 9073 ) ( SetItem ( 9075 ) ( SetItem ( 9089 ) ( SetItem ( 9094 ) ( SetItem ( 9114 ) ( SetItem ( 9128 ) ( SetItem ( 9133 ) ( SetItem ( 9164 ) ( SetItem ( 9173 ) ( SetItem ( 9201 ) ( SetItem ( 9219 ) ( SetItem ( 9243 ) ( SetItem ( 9267 ) ( SetItem ( 9274 ) ( SetItem ( 9295 ) ( SetItem ( 9318 ) ( SetItem ( 9346 ) ( SetItem ( 9358 ) ( SetItem ( 936 ) ( SetItem ( 9371 ) ( SetItem ( 9390 ) ( SetItem ( 9413 ) ( SetItem ( 9425 ) ( SetItem ( 9437 ) ( SetItem ( 9478 ) ( SetItem ( 9515 ) ( SetItem ( 9524 ) ( SetItem ( 9544 ) ( SetItem ( 962 ) ( SetItem ( 9622 ) ( SetItem ( 9654 ) ( SetItem ( 9692 ) ( SetItem ( 9697 ) ( SetItem ( 9711 ) ( SetItem ( 9716 ) ( SetItem ( 9729 ) ( SetItem ( 9738 ) ( SetItem ( 9752 ) ( SetItem ( 9757 ) ( SetItem ( 9778 ) ( SetItem ( 982 ) ( SetItem ( 9830 ) ( SetItem ( 9839 ) ( SetItem ( 9880 ) ( SetItem ( 9937 ) ( SetItem ( 9949 ) ( SetItem ( 9967 ) ( SetItem ( 9983 ) SetItem ( 9990 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 77 ) ( SetItem ( 16 ) ( SetItem ( 84 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 16 ) ( SetItem ( 48 ) ( SetItem ( 343 ) ( SetItem ( 366 ) ( SetItem ( 315 ) ( SetItem ( 322 ) ( SetItem ( 394 ) ( SetItem ( 291 ) ( SetItem ( 267 ) ( SetItem ( 249 ) ( SetItem ( 212 ) ( SetItem ( 221 ) ( SetItem ( 113 ) ( SetItem ( 108 ) ( SetItem ( 176 ) ( SetItem ( 162 ) ( SetItem ( 137 ) ( SetItem ( 123 ) ( SetItem ( 121 ) ( SetItem ( 181 ) ( SetItem ( 142 ) ( SetItem ( 592 ) ( SetItem ( 572 ) ( SetItem ( 563 ) ( SetItem ( 526 ) ( SetItem ( 461 ) ( SetItem ( 473 ) ( SetItem ( 406 ) ( SetItem ( 419 ) ( SetItem ( 438 ) SetItem ( 485 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k index a14f1fa11d..876f2ba817 100644 --- a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k +++ b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k @@ -143,7 +143,7 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC ( SetItem ( 102 ) ( SetItem ( 1075 ) ( SetItem ( 1095 ) ( SetItem ( 1101 ) ( SetItem ( 1137 ) ( SetItem ( 1245 ) ( SetItem ( 1307 ) ( SetItem ( 1331 ) ( SetItem ( 1340 ) ( SetItem ( 140 ) ( SetItem ( 1415 ) ( SetItem ( 1451 ) ( SetItem ( 1458 ) ( SetItem ( 1538 ) ( SetItem ( 1558 ) ( SetItem ( 16 ) ( SetItem ( 1648 ) ( SetItem ( 1684 ) ( SetItem ( 1691 ) ( SetItem ( 1693 ) ( SetItem ( 1729 ) ( SetItem ( 1760 ) ( SetItem ( 1804 ) ( SetItem ( 1838 ) ( SetItem ( 1852 ) ( SetItem ( 1881 ) ( SetItem ( 1901 ) ( SetItem ( 1937 ) ( SetItem ( 200 ) ( SetItem ( 2045 ) ( SetItem ( 2107 ) ( SetItem ( 2131 ) ( SetItem ( 2167 ) ( SetItem ( 2198 ) ( SetItem ( 2242 ) ( SetItem ( 2276 ) ( SetItem ( 2290 ) ( SetItem ( 2319 ) ( SetItem ( 2339 ) ( SetItem ( 234 ) ( SetItem ( 2373 ) ( SetItem ( 239 ) ( SetItem ( 247 ) ( SetItem ( 249 ) ( SetItem ( 2515 ) ( SetItem ( 2541 ) ( SetItem ( 257 ) ( SetItem ( 2602 ) ( SetItem ( 2607 ) ( SetItem ( 2631 ) ( SetItem ( 2635 ) ( SetItem ( 2640 ) ( SetItem ( 270 ) ( SetItem ( 2736 ) ( SetItem ( 279 ) ( SetItem ( 2792 ) ( SetItem ( 287 ) ( SetItem ( 2905 ) ( SetItem ( 295 ) ( SetItem ( 303 ) ( SetItem ( 3087 ) ( SetItem ( 3091 ) ( SetItem ( 311 ) ( SetItem ( 324 ) ( SetItem ( 3245 ) ( SetItem ( 3271 ) ( SetItem ( 332 ) ( SetItem ( 3332 ) ( SetItem ( 3337 ) ( SetItem ( 3342 ) ( SetItem ( 3359 ) ( SetItem ( 3372 ) ( SetItem ( 340 ) ( SetItem ( 3400 ) ( SetItem ( 3437 ) ( SetItem ( 3449 ) ( SetItem ( 3489 ) ( SetItem ( 353 ) ( SetItem ( 3550 ) ( SetItem ( 3592 ) ( SetItem ( 361 ) ( SetItem ( 3613 ) ( SetItem ( 3628 ) ( SetItem ( 3631 ) ( SetItem ( 3655 ) ( SetItem ( 3672 ) ( SetItem ( 369 ) ( SetItem ( 3711 ) ( SetItem ( 3750 ) ( SetItem ( 377 ) ( SetItem ( 3781 ) ( SetItem ( 3794 ) ( SetItem ( 3812 ) ( SetItem ( 3819 ) ( SetItem ( 3839 ) ( SetItem ( 3871 ) ( SetItem ( 3877 ) ( SetItem ( 3912 ) ( SetItem ( 3926 ) ( SetItem ( 393 ) ( SetItem ( 3944 ) ( SetItem ( 3954 ) ( SetItem ( 3972 ) ( SetItem ( 3988 ) ( SetItem ( 401 ) ( SetItem ( 4012 ) ( SetItem ( 4065 ) ( SetItem ( 4114 ) ( SetItem ( 4119 ) ( SetItem ( 4128 ) ( SetItem ( 4138 ) ( SetItem ( 414 ) ( SetItem ( 4147 ) ( SetItem ( 4186 ) ( SetItem ( 4210 ) ( SetItem ( 4218 ) ( SetItem ( 422 ) ( SetItem ( 4220 ) ( SetItem ( 4292 ) ( SetItem ( 4307 ) ( SetItem ( 4314 ) ( SetItem ( 434 ) ( SetItem ( 4346 ) ( SetItem ( 462 ) ( SetItem ( 497 ) ( SetItem ( 555 ) ( SetItem ( 585 ) ( SetItem ( 595 ) ( SetItem ( 691 ) ( SetItem ( 787 ) ( SetItem ( 869 ) ( SetItem ( 889 ) ( SetItem ( 945 ) ( SetItem ( 971 ) SetItem ( 991 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 69 ) ( SetItem ( 16 ) ( SetItem ( 350 ) ( SetItem ( 318 ) ( SetItem ( 311 ) ( SetItem ( 296 ) ( SetItem ( 214 ) ( SetItem ( 224 ) ( SetItem ( 222 ) ( SetItem ( 118 ) ( SetItem ( 101 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 190 ) ( SetItem ( 151 ) SetItem ( 142 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 69 ) ( SetItem ( 16 ) ( SetItem ( 350 ) ( SetItem ( 318 ) ( SetItem ( 311 ) ( SetItem ( 296 ) ( SetItem ( 214 ) ( SetItem ( 224 ) ( SetItem ( 222 ) ( SetItem ( 118 ) ( SetItem ( 132 ) ( SetItem ( 123 ) ( SetItem ( 190 ) ( SetItem ( 151 ) SetItem ( 142 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) @@ -471,7 +471,7 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC ( SetItem ( 102 ) ( SetItem ( 1075 ) ( SetItem ( 1095 ) ( SetItem ( 1101 ) ( SetItem ( 1137 ) ( SetItem ( 1245 ) ( SetItem ( 1307 ) ( SetItem ( 1331 ) ( SetItem ( 1340 ) ( SetItem ( 140 ) ( SetItem ( 1415 ) ( SetItem ( 1451 ) ( SetItem ( 1458 ) ( SetItem ( 1538 ) ( SetItem ( 1558 ) ( SetItem ( 16 ) ( SetItem ( 1648 ) ( SetItem ( 1684 ) ( SetItem ( 1691 ) ( SetItem ( 1693 ) ( SetItem ( 1729 ) ( SetItem ( 1760 ) ( SetItem ( 1804 ) ( SetItem ( 1838 ) ( SetItem ( 1852 ) ( SetItem ( 1881 ) ( SetItem ( 1901 ) ( SetItem ( 1937 ) ( SetItem ( 200 ) ( SetItem ( 2045 ) ( SetItem ( 2107 ) ( SetItem ( 2131 ) ( SetItem ( 2167 ) ( SetItem ( 2198 ) ( SetItem ( 2242 ) ( SetItem ( 2276 ) ( SetItem ( 2290 ) ( SetItem ( 2319 ) ( SetItem ( 2339 ) ( SetItem ( 234 ) ( SetItem ( 2373 ) ( SetItem ( 239 ) ( SetItem ( 247 ) ( SetItem ( 249 ) ( SetItem ( 2515 ) ( SetItem ( 2541 ) ( SetItem ( 257 ) ( SetItem ( 2602 ) ( SetItem ( 2607 ) ( SetItem ( 2631 ) ( SetItem ( 2635 ) ( SetItem ( 2640 ) ( SetItem ( 270 ) ( SetItem ( 2736 ) ( SetItem ( 279 ) ( SetItem ( 2792 ) ( SetItem ( 287 ) ( SetItem ( 2905 ) ( SetItem ( 295 ) ( SetItem ( 303 ) ( SetItem ( 3087 ) ( SetItem ( 3091 ) ( SetItem ( 311 ) ( SetItem ( 324 ) ( SetItem ( 3245 ) ( SetItem ( 3271 ) ( SetItem ( 332 ) ( SetItem ( 3332 ) ( SetItem ( 3337 ) ( SetItem ( 3342 ) ( SetItem ( 3359 ) ( SetItem ( 3372 ) ( SetItem ( 340 ) ( SetItem ( 3400 ) ( SetItem ( 3437 ) ( SetItem ( 3449 ) ( SetItem ( 3489 ) ( SetItem ( 353 ) ( SetItem ( 3550 ) ( SetItem ( 3592 ) ( SetItem ( 361 ) ( SetItem ( 3613 ) ( SetItem ( 3628 ) ( SetItem ( 3631 ) ( SetItem ( 3655 ) ( SetItem ( 3672 ) ( SetItem ( 369 ) ( SetItem ( 3711 ) ( SetItem ( 3750 ) ( SetItem ( 377 ) ( SetItem ( 3781 ) ( SetItem ( 3794 ) ( SetItem ( 3812 ) ( SetItem ( 3819 ) ( SetItem ( 3839 ) ( SetItem ( 3871 ) ( SetItem ( 3877 ) ( SetItem ( 3912 ) ( SetItem ( 3926 ) ( SetItem ( 393 ) ( SetItem ( 3944 ) ( SetItem ( 3954 ) ( SetItem ( 3972 ) ( SetItem ( 3988 ) ( SetItem ( 401 ) ( SetItem ( 4012 ) ( SetItem ( 4065 ) ( SetItem ( 4114 ) ( SetItem ( 4119 ) ( SetItem ( 4128 ) ( SetItem ( 4138 ) ( SetItem ( 414 ) ( SetItem ( 4147 ) ( SetItem ( 4186 ) ( SetItem ( 4210 ) ( SetItem ( 4218 ) ( SetItem ( 422 ) ( SetItem ( 4220 ) ( SetItem ( 4292 ) ( SetItem ( 4307 ) ( SetItem ( 4314 ) ( SetItem ( 434 ) ( SetItem ( 4346 ) ( SetItem ( 462 ) ( SetItem ( 497 ) ( SetItem ( 555 ) ( SetItem ( 585 ) ( SetItem ( 595 ) ( SetItem ( 691 ) ( SetItem ( 787 ) ( SetItem ( 869 ) ( SetItem ( 889 ) ( SetItem ( 945 ) ( SetItem ( 971 ) SetItem ( 991 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 258 ) ( SetItem ( 98 ) ( SetItem ( 65 ) ( SetItem ( 161 ) ( SetItem ( 70 ) ( SetItem ( 197 ) ( SetItem ( 171 ) ( SetItem ( 297 ) ( SetItem ( 265 ) ( SetItem ( 169 ) ( SetItem ( 137 ) ( SetItem ( 79 ) ( SetItem ( 243 ) ( SetItem ( 48 ) ( SetItem ( 16 ) ( SetItem ( 118 ) SetItem ( 89 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( SetItem ( 79 ) ( SetItem ( 70 ) ( SetItem ( 65 ) ( SetItem ( 16 ) ( SetItem ( 89 ) ( SetItem ( 98 ) ( SetItem ( 297 ) ( SetItem ( 265 ) ( SetItem ( 243 ) ( SetItem ( 258 ) ( SetItem ( 171 ) ( SetItem ( 169 ) ( SetItem ( 161 ) SetItem ( 137 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 ) diff --git a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k index 07b305f36d..3f9f590e36 100644 --- a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k +++ b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k @@ -143,7 +143,7 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC ( SetItem ( 1074 ) ( SetItem ( 1136 ) ( SetItem ( 1160 ) ( SetItem ( 1169 ) ( SetItem ( 1205 ) ( SetItem ( 1236 ) ( SetItem ( maxSInt8 ) ( SetItem ( 1280 ) ( SetItem ( 1314 ) ( SetItem ( 1328 ) ( SetItem ( 1357 ) ( SetItem ( 1377 ) ( SetItem ( 1413 ) ( SetItem ( 1521 ) ( SetItem ( 1583 ) ( SetItem ( 1607 ) ( SetItem ( 1643 ) ( SetItem ( 1674 ) ( SetItem ( 1718 ) ( SetItem ( 1752 ) ( SetItem ( 1766 ) ( SetItem ( 1795 ) ( SetItem ( 1815 ) ( SetItem ( 1849 ) ( SetItem ( 198 ) ( SetItem ( 1991 ) ( SetItem ( 2017 ) ( SetItem ( 205 ) ( SetItem ( 2078 ) ( SetItem ( 2083 ) ( SetItem ( 210 ) ( SetItem ( 2107 ) ( SetItem ( 2111 ) ( SetItem ( 2116 ) ( SetItem ( 2209 ) ( SetItem ( 222 ) ( SetItem ( 2229 ) ( SetItem ( 2300 ) ( SetItem ( 231 ) ( SetItem ( 233 ) ( SetItem ( 2370 ) ( SetItem ( 2390 ) ( SetItem ( 2420 ) ( SetItem ( 2426 ) ( SetItem ( 2431 ) ( SetItem ( 245 ) ( SetItem ( 2492 ) ( SetItem ( 254 ) ( SetItem ( 2562 ) ( SetItem ( 2582 ) ( SetItem ( 2611 ) ( SetItem ( 2615 ) ( SetItem ( 267 ) ( SetItem ( 2711 ) ( SetItem ( 276 ) ( SetItem ( 2824 ) ( SetItem ( 288 ) ( SetItem ( 297 ) ( SetItem ( 309 ) ( SetItem ( 3155 ) ( SetItem ( 318 ) ( SetItem ( 3181 ) ( SetItem ( 3242 ) ( SetItem ( 3247 ) ( SetItem ( 3252 ) ( SetItem ( 3269 ) ( SetItem ( 3281 ) ( SetItem ( 330 ) ( SetItem ( 3309 ) ( SetItem ( 3346 ) ( SetItem ( 3358 ) ( SetItem ( 339 ) ( SetItem ( 3398 ) ( SetItem ( 3459 ) ( SetItem ( 3501 ) ( SetItem ( 352 ) ( SetItem ( 3522 ) ( SetItem ( 3537 ) ( SetItem ( 3540 ) ( SetItem ( 3564 ) ( SetItem ( 3579 ) ( SetItem ( 3585 ) ( SetItem ( 3624 ) ( SetItem ( 364 ) ( SetItem ( 3663 ) ( SetItem ( 3694 ) ( SetItem ( 3707 ) ( SetItem ( 3725 ) ( SetItem ( 373 ) ( SetItem ( 3748 ) ( SetItem ( 3755 ) ( SetItem ( 3775 ) ( SetItem ( 3807 ) ( SetItem ( 3813 ) ( SetItem ( 3848 ) ( SetItem ( 386 ) ( SetItem ( 3862 ) ( SetItem ( 3880 ) ( SetItem ( 3890 ) ( SetItem ( 3908 ) ( SetItem ( 3924 ) ( SetItem ( 3957 ) ( SetItem ( 3978 ) ( SetItem ( 398 ) ( SetItem ( 4025 ) ( SetItem ( 4031 ) ( SetItem ( 4036 ) ( SetItem ( 4047 ) ( SetItem ( 4054 ) ( SetItem ( 4056 ) ( SetItem ( 407 ) ( SetItem ( 4099 ) ( SetItem ( 419 ) ( SetItem ( 428 ) ( SetItem ( 440 ) ( SetItem ( 449 ) ( SetItem ( 465 ) ( SetItem ( 477 ) ( SetItem ( 492 ) ( SetItem ( 497 ) ( SetItem ( 509 ) ( SetItem ( 518 ) ( SetItem ( 530 ) ( SetItem ( 539 ) ( SetItem ( 551 ) ( SetItem ( 565 ) ( SetItem ( 577 ) ( SetItem ( 605 ) ( SetItem ( 640 ) ( SetItem ( 698 ) ( SetItem ( 728 ) ( SetItem ( 738 ) ( SetItem ( 834 ) ( SetItem ( 89 ) ( SetItem ( 930 ) SetItem ( 966 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) => - ( SetItem ( 73 ) ( SetItem ( 68 ) ( SetItem ( 62 ) ( SetItem ( 15 ) ( SetItem ( 84 ) ( SetItem ( 93 ) ( SetItem ( 91 ) ( SetItem ( 136 ) SetItem ( 155 ) ) ) ) ) ) ) ) ) + ( SetItem ( 73 ) ( SetItem ( 68 ) ( SetItem ( 62 ) ( SetItem ( 15 ) ( SetItem ( 84 ) ( SetItem ( 93 ) ( SetItem ( 91 ) SetItem ( 136 ) ) ) ) ) ) ) ) ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )