From 3094eeeb8a7e8c60b1d261f370c55be821250c5e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andrei=20V=C4=83caru?= <16517508+anvacaru@users.noreply.github.com> Date: Tue, 4 Jun 2024 17:23:57 +0300 Subject: [PATCH] Eliminate complex KLabels from Python code (#2463) * abi.md: refactor klabel and symbol attributes * kevm.py: change klabels used in Python to symbols * Set Version: 1.0.586 * apply review suggestions * Set Version: 1.0.587 --------- Co-authored-by: devops --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/kevm.py | 46 ++- .../src/kevm_pyk/kproj/evm-semantics/abi.md | 292 +++++++++--------- .../src/kevm_pyk/kproj/evm-semantics/buf.md | 2 +- .../kevm_pyk/kproj/evm-semantics/evm-types.md | 12 +- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 25 +- .../kproj/evm-semantics/hashed-locations.md | 2 +- .../kproj/evm-semantics/serialization.md | 8 +- .../src/kevm_pyk/kproj/evm-semantics/word.md | 22 +- package/version | 2 +- 11 files changed, 207 insertions(+), 208 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index e2a5491000..00645b8653 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.586" +version = "1.0.587" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 342794dcb2..c5031d372a 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.586' +VERSION: Final = '1.0.587' diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 1cb9ca3b45..80d2bb7fc5 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -387,11 +387,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: @@ -411,7 +411,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: @@ -423,35 +423,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: @@ -463,7 +463,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: @@ -475,13 +475,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 @@ -492,11 +490,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: @@ -504,11 +502,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: @@ -524,7 +522,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: @@ -560,7 +558,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: @@ -568,7 +566,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: @@ -675,7 +673,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) 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 420cd0548a..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) @@ -324,8 +324,8 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th - 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) @@ -335,8 +335,8 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th 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/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 160e2a031e..07b21059b7 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -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(computeValidJumpDestsAux), function ] + // ----------------------------------------------------------------------------------------------------------------- rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, .List) syntax Set ::= #computeValidJumpDestsWithinBound(Bytes, Int, List) [klabel(#computeValidJumpDestsWithinBound), function] 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..7832f81be9 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 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..884b625a17 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -158,10 +158,10 @@ 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)) 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/package/version b/package/version index d38a0a2765..f449bb757c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.586 +1.0.587