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 <devops@runtimeverification.com>

Author: anvacaru

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. <contact@runtimeverification.com>",

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'

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,23 +490,23 @@ 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:
         return KApply('abi_selector', [stringToken(name)])
 
     @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,15 +558,15 @@ 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:
         return KApply('.Bytes_BYTES-HOOKED_Bytes')
 
     @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)