Never abstract KTokens (domain values), use subsort for code cell

kmxwasm/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmxwasm"
-version = "0.1.20"
+version = "0.1.21"
 description = "Symbolic execution for the MultiversX blockchain with the Wasm semantics, using pyk."
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kmxwasm/src/kmxwasm/ast/mx.py

@@ -59,6 +59,7 @@
 FINISH_EXECUTE_ON_DEST_CONTEXT_LABEL = 'finishExecuteOnDestContext'
 
 CODE = KSort('Code')
+MODULE_DECL = KSort('ModuleDecl')
 
 
 # TODO: Move these to the elrond-semantics repository.

kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/mx-lemmas.md

@@ -12,13 +12,29 @@ module MX-LEMMAS-BASIC
 
 endmodule
 
+module MX-UPDATE-MAP
+  imports private BOOL
+  imports private MAP
+
+  // supply updateMap simplifications to avoid the MAP.updateAll hook error
+  // TODO upstream these equations to K:domains.md
+  rule updateMap(M, .Map) => M
+      [simplification]
+  rule updateMap(.Map, M) => M
+      [simplification]
+  rule updateMap(M1, K |-> V M2) => updateMap(M1[K <- V], M2)
+      requires notBool (K in_keys(M2))
+      [simplification, preserves-definedness]
+endmodule
+
 module MX-LEMMAS  [symbolic]
   imports private CEILS
   imports private ELROND
   imports private INT-INEQUALITIES-LEMMAS
   imports private INT-KORE
   imports private INT-NORMALIZATION-LEMMAS
   imports public MX-LEMMAS-BASIC
+  imports public MX-UPDATE-MAP
   imports private SET
   imports private SPARSE-BYTES-LEMMAS
   imports private WASM-TEXT

kmxwasm/src/kmxwasm/property_testing/cell_abstracter.py

@@ -1,7 +1,7 @@
 from collections.abc import Callable
 
 from pyk.cterm import CTerm
-from pyk.kast.inner import KApply, KInner, KSort, KVariable, bottom_up
+from pyk.kast.inner import KApply, KInner, KSort, KToken, KVariable, bottom_up
 from pyk.kcfg import KCFG
 from pyk.kcfg.kcfg import NodeIdLike
 
@@ -80,6 +80,8 @@ def replace(term: KInner) -> KInner:
                 return term
             if not term.arity == 1:
                 raise ValueError(f'Wrong arity for {cell_name}: {term.arity}')
+            if type(term.args[0]) is KToken:
+                return term
 
             variable = new_variable()
             variable_to_value[variable] = term.args[0]
@@ -135,8 +137,10 @@ def single_cell_abstracter(
     def replace_with_variable(
         config: KInner, variable_to_value: dict[KVariable, KInner], new_variable: Callable[[], KVariable]
     ) -> KInner:
-        variable = new_variable()
         original = get_single_argument_kapply_contents_path(config, cell_path)
+        if type(original) is KToken:
+            return config
+        variable = new_variable()
         variable_to_value[variable] = original
         return replace_contents_with_path(root=config, path=cell_path, replacement=variable)
 

kmxwasm/src/kmxwasm/property_testing/running.py

@@ -13,8 +13,8 @@
 from ..ast.mx import (
     ACCOUNTS_PATH,
     CALL_STACK_PATH,
-    CODE,
     INTERIM_STATES_PATH,
+    MODULE_DECL,
     cfg_changes_call_stack,
     cfg_changes_interim_states,
     cfg_touches_code,
@@ -99,7 +99,7 @@ def abstracters(
                 parent_path=ACCOUNTS_PATH,
                 cell_name='<code>',
                 variable_root='AbstractCode',
-                variable_sort=CODE,
+                variable_sort=MODULE_DECL,
                 destination=target_node_id,
             ),
             CODE_CUT_POINT_RULES,

package/version

@@ -1 +1 @@
-0.1.20
+0.1.21