Remove typed maps (#155)

* Remove MapInt2Int

* Remove MapIntToBytes

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Jost Berthold <[email protected]>
Co-authored-by: Bruce Collie <[email protected]>

deps/mx-semantics_release

@@ -1 +1 @@
-0.1.88
+0.1.92

flake.nix

@@ -6,7 +6,7 @@
     pyk.url = "github:runtimeverification/k/v7.1.30?dir=pyk";
     nixpkgs-pyk.follows = "pyk/nixpkgs";
     poetry2nix.follows = "pyk/poetry2nix";
-    mx-semantics.url = "github:runtimeverification/mx-semantics/v0.1.88";
+    mx-semantics.url = "github:runtimeverification/mx-semantics/v0.1.92";
     nixpkgs.follows = "k-framework/nixpkgs";
     flake-utils.follows = "k-framework/flake-utils";
     rv-utils.url = "github:runtimeverification/rv-nix-tools";

kmxwasm/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmxwasm"
-version = "0.1.72"
+version = "0.1.73"
 description = "Symbolic execution for the MultiversX blockchain with the Wasm semantics, using pyk."
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -22,7 +22,7 @@ pytest-kmxwasm = "kmxwasm.testing.fixtures"
 
 [tool.poetry.dependencies]
 python = "^3.10"
-kmultiversx = { git = "https://github.com/runtimeverification/mx-semantics.git", tag = "v0.1.88", subdirectory = "kmultiversx" }
+kmultiversx = { git = "https://github.com/runtimeverification/mx-semantics.git", tag = "v0.1.92", subdirectory = "kmultiversx" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

kmxwasm/src/kmxwasm/ast/mx.py

@@ -3,7 +3,7 @@
 
 from pyk.kast.inner import KApply, KInner, KSequence, KSort, KToken, collect
 
-from .collections import cell_map, full_list, k_map, simple_list
+from .collections import cell_map, full_list, simple_list
 from .generic import (
     find_with_path,
     get_with_path,
@@ -73,16 +73,6 @@ def listBytes(items: Iterable[KInner]) -> KInner:  # noqa: N802
     return full_list(concat_label='_ListBytes_', item_label='ListBytesItem', empty_label='.ListBytes', items=items)
 
 
-def mapIntToBytes(int_to_bytes: dict[KInner, KInner]) -> KInner:  # noqa: N802
-    return k_map(
-        concat_label='_MapIntToBytes_', item_label='_Int2Bytes|->_', empty_label='.MapIntToBytes', items=int_to_bytes
-    )
-
-
-def mapIntToInt(int_to_int: dict[KInner, KInner]) -> KInner:  # noqa: N802
-    return k_map(concat_label='_MapIntToInt_', item_label='_Int2Int|->_', empty_label='.MapIntToInt', items=int_to_int)
-
-
 def bytesStack(items: Iterable[KInner]) -> KInner:  # noqa: N802
     return simple_list(concat_label='bytesStackList', empty_label='.List{"bytesStackList"}', items=items)
 

kmxwasm/src/kmxwasm/proofs.py

@@ -17,6 +17,7 @@
 from pyk.ktool.kprint import KPrint
 from pyk.ktool.krun import KRunOutput, _krun
 from pyk.prelude.bytes import BYTES, bytesToken_from_str
+from pyk.prelude.collections import MAP
 from pyk.prelude.k import K
 from pyk.prelude.kbool import TRUE, andBool, notBool
 from pyk.prelude.kint import INT, intToken, leInt, ltInt
@@ -60,7 +61,6 @@
 SUMMARIES_DIR = DATA_DIR / 'summaries'
 
 GENERATED_RULE_PRIORITY = 20
-MAP = KSort('Map')
 
 # Setting this disables compilation.
 DEBUG_ID = ''  #'ca3493ec081b72857fe96a8b6d3b3f969505e6bc09d91d16eaff9995f2c551ad'
@@ -661,8 +661,8 @@ def run_for_input(
         ('<funcIds>', 'MyFuncIds', MAP),
         # Real symbolic inputs
         # <elrond>
-        ('<bufferHeap>', 'MyBuffers', KSort('MapIntToBytes')),
-        ('<bigIntHeap>', 'MyInts', KSort('MapIntToInt')),
+        ('<bufferHeap>', 'MyBuffers', MAP),
+        ('<bigIntHeap>', 'MyInts', MAP),
         # <elrond>/<node>/<callState>
         ('<callArgs>', 'MyCallArgs', KSort('ListBytes')),
         ('<caller>', 'MyCaller', BYTES),

kmxwasm/src/kmxwasm/property_testing/wasm_krun_initializer.py

@@ -10,8 +10,6 @@
     get_contract_mod_idx_cell,
     get_wasm_cell,
     listBytes,
-    mapIntToBytes,
-    mapIntToInt,
     replace_contract_mod_idx_cell,
     replace_wasm_cell,
     set_accounts_cell_content,
@@ -83,8 +81,8 @@ def __prepare_krun_cell(self, start_cell: KInner, first: KInner) -> KInner:
         krun_cell = set_logging_cell_content(krun_cell, token(''))
         krun_cell = set_generated_counter_cell_content(krun_cell, token(0))
         krun_cell = set_call_args_cell_content(krun_cell, listBytes([]))
-        krun_cell = set_big_int_heap_cell_content(krun_cell, mapIntToInt({}))
-        krun_cell = set_buffer_heap_cell_content(krun_cell, mapIntToBytes({}))
+        krun_cell = set_big_int_heap_cell_content(krun_cell, map_empty())
+        krun_cell = set_buffer_heap_cell_content(krun_cell, map_empty())
         krun_cell = set_exit_code_cell_content(krun_cell, token(0))
         krun_cell = set_cur_block_timestamp_cell_content(krun_cell, token(0))
         krun_cell = set_cur_block_nonce_cell_content(krun_cell, token(0))

kmxwasm/src/tests/integration/test_claims.py

@@ -11,7 +11,7 @@
 from pyk.prelude.string import stringToken
 
 from kmxwasm.ast.configuration import wrap_with_generated_top_if_needed
-from kmxwasm.ast.mx import accountCellMap, bytesStack, directCall, listAsyncCall, listBytes, mapIntToBytes, mapIntToInt
+from kmxwasm.ast.mx import accountCellMap, bytesStack, directCall, listAsyncCall, listBytes
 from kmxwasm.ast.wasm import (
     elemInstCellMap,
     funcDefCellMap,
@@ -80,8 +80,8 @@ def callStateCell() -> KInner:  # noqa: N802
                 ),
             ),
             wasmCell(),
-            KApply('<bigIntHeap>', mapIntToInt({})),
-            KApply('<bufferHeap>', mapIntToBytes({})),
+            KApply('<bigIntHeap>', map_empty()),
+            KApply('<bufferHeap>', map_empty()),
             KApply('<bytesStack>', bytesStack([])),
             KApply('<contractModIdx>', optionalInt_empty()),
             KApply('<asyncCalls>', listAsyncCall([])),

package/version

@@ -1 +1 @@
-0.1.72
+0.1.73