From e961491526b72bab85a054c1dea1b48d07fa7b01 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 1 May 2024 11:38:35 +1000 Subject: [PATCH 1/3] Never abstract KTokens (domain values), use subsort for code cell abstraction * The cell abstraction mechanism serves to reduce AST _depth_, so it should not be necessary to abstract cells containing `KToken` instances. * In case of the `` cell, this allows us to use the `ModuleDecl` sort instead of the supersort `Code` (which caused unnecessary branching) --- kmxwasm/src/kmxwasm/ast/mx.py | 1 + kmxwasm/src/kmxwasm/property_testing/cell_abstracter.py | 8 ++++++-- kmxwasm/src/kmxwasm/property_testing/running.py | 4 ++-- 3 files changed, 9 insertions(+), 4 deletions(-) diff --git a/kmxwasm/src/kmxwasm/ast/mx.py b/kmxwasm/src/kmxwasm/ast/mx.py index 3bec5040..64ca8d18 100644 --- a/kmxwasm/src/kmxwasm/ast/mx.py +++ b/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. diff --git a/kmxwasm/src/kmxwasm/property_testing/cell_abstracter.py b/kmxwasm/src/kmxwasm/property_testing/cell_abstracter.py index 027fae24..4e6b0be4 100644 --- a/kmxwasm/src/kmxwasm/property_testing/cell_abstracter.py +++ b/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) diff --git a/kmxwasm/src/kmxwasm/property_testing/running.py b/kmxwasm/src/kmxwasm/property_testing/running.py index eabe70e7..4ebd365f 100644 --- a/kmxwasm/src/kmxwasm/property_testing/running.py +++ b/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='', variable_root='AbstractCode', - variable_sort=CODE, + variable_sort=MODULE_DECL, destination=target_node_id, ), CODE_CUT_POINT_RULES, From 308b10d07ee7339941f2927530a0b35e5116f5a6 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 1 May 2024 01:43:51 +0000 Subject: [PATCH 2/3] Set Version: 0.1.21 --- kmxwasm/pyproject.toml | 2 +- package/version | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kmxwasm/pyproject.toml b/kmxwasm/pyproject.toml index c1c557dc..6cdb66f3 100644 --- a/kmxwasm/pyproject.toml +++ b/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. ", diff --git a/package/version b/package/version index baa98378..79062996 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.20 +0.1.21 From 539a2187d05576348cf07b9e160625459b1fae49 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 30 Apr 2024 11:06:05 +1000 Subject: [PATCH 3/3] add updateMap rules to mx-lemmas.md --- .../kmxwasm/kdist/mxwasm-semantics/mx-lemmas.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/mx-lemmas.md b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/mx-lemmas.md index 6f986635..6fed3cee 100644 --- a/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/mx-lemmas.md +++ b/kmxwasm/src/kmxwasm/kdist/mxwasm-semantics/mx-lemmas.md @@ -12,6 +12,21 @@ 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 @@ -19,6 +34,7 @@ module MX-LEMMAS [symbolic] 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