Revert "TEST merging branches"

This reverts commit 011b056.

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, simple_list
+from .collections import cell_map, full_list, k_map, simple_list
 from .generic import (
     find_with_path,
     get_with_path,
@@ -73,6 +73,16 @@ 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,7 +17,6 @@
 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
@@ -61,6 +60,7 @@
 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', MAP),
-        ('<bigIntHeap>', 'MyInts', MAP),
+        ('<bufferHeap>', 'MyBuffers', KSort('MapIntToBytes')),
+        ('<bigIntHeap>', 'MyInts', KSort('MapIntToInt')),
         # <elrond>/<node>/<callState>
         ('<callArgs>', 'MyCallArgs', KSort('ListBytes')),
         ('<caller>', 'MyCaller', BYTES),

kmxwasm/src/kmxwasm/property_testing/wasm_krun_initializer.py

@@ -10,6 +10,8 @@
     get_contract_mod_idx_cell,
     get_wasm_cell,
     listBytes,
+    mapIntToBytes,
+    mapIntToInt,
     replace_contract_mod_idx_cell,
     replace_wasm_cell,
     set_accounts_cell_content,
@@ -81,8 +83,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, map_empty())
-        krun_cell = set_buffer_heap_cell_content(krun_cell, map_empty())
+        krun_cell = set_big_int_heap_cell_content(krun_cell, mapIntToInt({}))
+        krun_cell = set_buffer_heap_cell_content(krun_cell, mapIntToBytes({}))
         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
+from kmxwasm.ast.mx import accountCellMap, bytesStack, directCall, listAsyncCall, listBytes, mapIntToBytes, mapIntToInt
 from kmxwasm.ast.wasm import (
     elemInstCellMap,
     funcDefCellMap,
@@ -80,8 +80,8 @@ def callStateCell() -> KInner:  # noqa: N802
                 ),
             ),
             wasmCell(),
-            KApply('<bigIntHeap>', map_empty()),
-            KApply('<bufferHeap>', map_empty()),
+            KApply('<bigIntHeap>', mapIntToInt({})),
+            KApply('<bufferHeap>', mapIntToBytes({})),
             KApply('<bytesStack>', bytesStack([])),
             KApply('<contractModIdx>', optionalInt_empty()),
             KApply('<asyncCalls>', listAsyncCall([])),