diff --git a/Makefile b/Makefile
index a9cdf29..7478b43 100644
--- a/Makefile
+++ b/Makefile
@@ -27,14 +27,30 @@ MX_TESTING_OUTPUT_DIR ::= .build/mx/output
MX_TESTING_INPUTS ::= $(wildcard $(MX_TESTING_INPUT_DIR)/**/*.mx)
MX_TESTING_OUTPUTS ::= $(patsubst $(MX_TESTING_INPUT_DIR)/%,$(MX_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_TESTING_INPUTS))
-.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test
+MX_RUST_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+MX_RUST_KOMPILED ::= .build/mx-rust-kompiled
+MX_RUST_TIMESTAMP ::= $(MX_RUST_KOMPILED)/timestamp
+
+MX_RUST_TESTING_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+MX_RUST_TESTING_KOMPILED ::= .build/mx-rust-testing-kompiled
+MX_RUST_TESTING_TIMESTAMP ::= $(MX_RUST_TESTING_KOMPILED)/timestamp
+MX_RUST_TESTING_INPUT_DIR ::= tests/mx-rust
+MX_RUST_TESTING_OUTPUT_DIR ::= .build/mx-rust/output
+MX_RUST_TESTING_INPUTS ::= $(wildcard $(MX_RUST_TESTING_INPUT_DIR)/*.run)
+MX_RUST_TESTING_OUTPUTS ::= $(patsubst $(MX_RUST_TESTING_INPUT_DIR)/%,$(MX_RUST_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_RUST_TESTING_INPUTS))
+
+.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test
clean:
rm -r .build
-build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP) $(MX_TESTING_TIMESTAMP)
+build: $(RUST_PREPROCESSING_TIMESTAMP) \
+ $(RUST_EXECUTION_TIMESTAMP) \
+ $(MX_TESTING_TIMESTAMP) \
+ $(MX_RUST_TIMESTAMP) \
+ $(MX_RUST_TESTING_TIMESTAMP)
-test: syntax-test preprocessing-test execution-test mx-test
+test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test
syntax-test: $(SYNTAX_OUTPUTS)
@@ -44,6 +60,8 @@ execution-test: $(EXECUTION_OUTPUTS)
mx-test: $(MX_TESTING_OUTPUTS)
+mx-rust-test: $(MX_RUST_TESTING_OUTPUTS)
+
$(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
# Workaround for https://github.com/runtimeverification/k/issues/4141
-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -59,6 +77,22 @@ $(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES)
-rm -r $(MX_TESTING_KOMPILED)
$$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug
+$(MX_RUST_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
+ # Workaround for https://github.com/runtimeverification/k/issues/4141
+ -rm -r $(MX_RUST_KOMPILED)
+ $$(which kompile) mx-rust-semantics/targets/blockchain/mx-rust.md \
+ -o $(MX_RUST_KOMPILED) \
+ -I . \
+ --debug
+
+$(MX_RUST_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
+ # Workaround for https://github.com/runtimeverification/k/issues/4141
+ -rm -r $(MX_RUST_TESTING_KOMPILED)
+ $$(which kompile) mx-rust-semantics/targets/testing/mx-rust.md \
+ -o $(MX_RUST_TESTING_KOMPILED) \
+ -I . \
+ --debug
+
$(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
mkdir -p $(RUST_SYNTAX_OUTPUT_DIR)
kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@
@@ -75,7 +109,11 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%
# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
# as a dependency
-$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST_EXECUTION_TIMESTAMP)
+$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: \
+ $(EXECUTION_INPUT_DIR)/%.run \
+ $(RUST_EXECUTION_TIMESTAMP) \
+ parse-rust.sh \
+ parse-test.sh
mkdir -p $(EXECUTION_OUTPUT_DIR)
krun \
"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
@@ -97,3 +135,22 @@ $(MX_TESTING_OUTPUT_DIR)/%.mx.executed.kore: $(MX_TESTING_INPUT_DIR)/%.mx $(MX_T
--output-file $@.tmp
cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
mv -f $@.tmp $@
+
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
+# as a dependency
+$(MX_RUST_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+ $(MX_RUST_TESTING_INPUT_DIR)/%.run \
+ $(MX_RUST_TESTING_TIMESTAMP) \
+ parse-mx-rust.sh \
+ parse-mx-rust-test.sh
+ mkdir -p $(MX_RUST_TESTING_OUTPUT_DIR)
+ krun \
+ "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
+ --definition $(MX_RUST_TESTING_KOMPILED) \
+ --parser $(CURDIR)/parse-mx-rust.sh \
+ --output kore \
+ --output-file $@.tmp \
+ -cTEST='$(shell cat $<)' \
+ -pTEST=$(CURDIR)/parse-mx-rust-test.sh
+ cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+ mv -f $@.tmp $@
diff --git a/mx-rust-semantics/main/configuration.md b/mx-rust-semantics/main/configuration.md
new file mode 100644
index 0000000..b7de223
--- /dev/null
+++ b/mx-rust-semantics/main/configuration.md
@@ -0,0 +1,17 @@
+```k
+
+requires "mx-semantics/main/configuration.md"
+requires "rust-semantics/config.md"
+
+module MX-RUST-COMMON-CONFIGURATION
+ imports MX-COMMON-CONFIGURATION
+ imports RUST-CONFIGURATION
+
+ configuration
+
+
+
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/expression.md b/mx-rust-semantics/main/expression.md
new file mode 100644
index 0000000..1e6a692
--- /dev/null
+++ b/mx-rust-semantics/main/expression.md
@@ -0,0 +1,9 @@
+```k
+
+requires "expression/strings.md"
+
+module MX-RUST-EXPRESSION
+ imports private MX-RUST-EXPRESSION-STRINGS
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-rust-semantics/main/expression/strings.md b/mx-rust-semantics/main/expression/strings.md
new file mode 100644
index 0000000..5edf1a0
--- /dev/null
+++ b/mx-rust-semantics/main/expression/strings.md
@@ -0,0 +1,34 @@
+```k
+
+module MX-RUST-EXPRESSION-STRINGS
+ imports private BOOL
+ imports private INT
+ imports private MX-RUST-REPRESENTATION
+ imports private RUST-VALUE-SYNTAX
+ imports private STRING
+
+ rule concatString(ptrValue(_, S1:String), ptrValue(_, S2:String))
+ => ptrValue(null, S1 +String S2)
+
+ rule toString(ptrValue(_, i32(Value:MInt{32})))
+ => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4))
+ rule toString(ptrValue(_, u32(Value:MInt{32})))
+ => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4))
+ rule toString(ptrValue(_, i64(Value:MInt{64})))
+ => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4))
+ rule toString(ptrValue(_, u64(Value:MInt{64})))
+ => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4))
+ rule toString(ptrValue(_, u128(Value:MInt{128})))
+ => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 128 divInt 4))
+ rule toString(ptrValue(null, Value:String)) => ptrValue(null, Value)
+ // TODO: convert all Value entries to string
+
+ syntax String ::= padLeftString(value:String, padding:String, count:Int) [function, total]
+ rule padLeftString(...value:S, padding:P, count:C) => S
+ requires C <=Int lengthString(S) orBool lengthString(P) =/=Int 1
+ rule padLeftString(S:String => P +String S, P:String, _Count:Int)
+ [owise]
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/glue.md b/mx-rust-semantics/main/glue.md
new file mode 100644
index 0000000..9b9162d
--- /dev/null
+++ b/mx-rust-semantics/main/glue.md
@@ -0,0 +1,50 @@
+```k
+
+module MX-RUST-GLUE
+ imports private COMMON-K-CELL
+ imports private MX-COMMON-SYNTAX
+ imports private RUST-EXECUTION-CONFIGURATION
+ imports private RUST-VALUE-SYNTAX
+ imports private MX-RUST-REPRESENTATION
+
+ rule
+
+ storeHostValue
+ (... destination: rustDestination(ValueId, _:MxRustType)
+ , value: wrappedRust(V:Value)
+ )
+ => .K
+ ...
+
+ Values:Map => Values[ValueId <- V]
+ requires ValueId >=Int 0
+
+ rule
+ (.K => mxRustEmptyValue(T))
+ ~> storeHostValue
+ (... destination: rustDestination(_, T:MxRustType)
+ , value: mxWrappedEmpty
+ )
+ rule
+ (ptrValue(_, V:Value) => .K)
+ ~> storeHostValue
+ (... value: mxWrappedEmpty => wrappedRust(V)
+ )
+
+ rule
+
+ mxRustLoadPtr(P:Int) => ptrValue(ptr(P), V)
+ ...
+
+ P |-> V:Value ...
+
+ rule
+ mxRustNewValue(V:Value) => ptrValue(ptr(NextId), V) ...
+ NextId:Int => NextId +Int 1
+ Values:Map => Values[NextId <- V]
+
+ rule mxIntValue(I:Int) ~> mxValueToRust(T:Type)
+ => mxRustNewValue(integerToValue(I, T))
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/modules.md b/mx-rust-semantics/main/modules.md
new file mode 100644
index 0000000..c9aa757
--- /dev/null
+++ b/mx-rust-semantics/main/modules.md
@@ -0,0 +1,11 @@
+```k
+
+requires "modules/biguint.md"
+requires "modules/storage.md"
+
+module MX-RUST-MODULES
+ imports private MX-RUST-MODULES-BIGUINT
+ imports private MX-RUST-MODULES-STORAGE
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/modules/biguint.md b/mx-rust-semantics/main/modules/biguint.md
new file mode 100644
index 0000000..1e4e363
--- /dev/null
+++ b/mx-rust-semantics/main/modules/biguint.md
@@ -0,0 +1,48 @@
+```k
+
+module MX-RUST-MODULES-BIGUINT
+ imports private COMMON-K-CELL
+ imports private MX-COMMON-SYNTAX
+ imports private MX-RUST-REPRESENTATION
+ imports private RUST-EXECUTION-CONFIGURATION
+ imports private RUST-REPRESENTATION
+ imports private RUST-SHARED-SYNTAX
+
+ rule
+
+ normalizedMethodCall
+ ( #token("BigUint", "Identifier"):Identifier
+ , #token("from", "Identifier"):Identifier
+ , ( ptr(ValueId:Int)
+ , .NormalizedCallParams
+ )
+ )
+ // TODO: Should check that V >= 0
+ => mxRustBigIntNew(valueToInteger(V))
+ ...
+
+ ValueId |-> V:Value ...
+
+ // --------------------------------------
+
+ syntax MxRustInstruction ::= mxRustBigIntNew(IntOrError)
+ | "mxRustCreateBigUint"
+
+ rule mxRustBigIntNew(V:Int)
+ => MX#bigIntNew(mxIntValue(V))
+ ~> mxValueToRust(i32)
+ ~> mxRustCreateBigUint
+
+ rule ptrValue(ptr(BigUintId:Int), _) ~> mxRustCreateBigUint
+ => mxRustNewValue
+ ( struct
+ ( #token("BigUint", "Identifier"):Identifier
+ , #token("mx_biguint_id", "Identifier"):Identifier |-> BigUintId
+ )
+ )
+
+ rule mxRustEmptyValue(BigUint) => mxRustBigIntNew(0)
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/modules/storage.md b/mx-rust-semantics/main/modules/storage.md
new file mode 100644
index 0000000..582f64b
--- /dev/null
+++ b/mx-rust-semantics/main/modules/storage.md
@@ -0,0 +1,113 @@
+```k
+
+module MX-RUST-MODULES-STORAGE
+ imports private COMMON-K-CELL
+ imports private MX-COMMON-SYNTAX
+ imports private MX-RUST-REPRESENTATION
+ imports private RUST-EXECUTION-CONFIGURATION
+ imports private RUST-REPRESENTATION
+ imports private RUST-SHARED-SYNTAX
+
+ rule
+ normalizedMethodCall
+ ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+ , #token("new", "Identifier"):Identifier
+ , ( ptr(KeyId:Int)
+ , ptr(ResultTypeId:Int)
+ , .NormalizedCallParams
+ )
+ )
+ => mxRustNewValue
+ ( struct
+ ( Type
+ , #token("storage_key", "Identifier"):Identifier |-> KeyId
+ #token("result_type", "Identifier"):Identifier |-> ResultTypeId
+ )
+ )
+
+ rule
+
+ normalizedMethodCall
+ ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+ , #token("set", "Identifier"):Identifier
+ , ( ptr(SelfId:Int)
+ , ptr(ValueId:Int)
+ , .NormalizedCallParams
+ )
+ )
+ => MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
+ ...
+
+
+ SelfId |-> struct
+ ( Type
+ , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
+ _:Map
+ )
+ StorageKeyId |-> StorageKey:String
+ ValueId |-> V:Value
+ ...
+
+
+ rule
+
+ normalizedMethodCall
+ ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+ , #token("set_if_empty", "Identifier"):Identifier
+ , ( ptr(SelfId:Int)
+ , ptr(ValueId:Int)
+ , .NormalizedCallParams
+ )
+ )
+ => MX#storageLoad(mxStringValue(StorageKey), rustDestination(-1, noType))
+ ~> setIfEmpty
+ ~> MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
+ ...
+
+
+ SelfId |-> struct
+ ( Type
+ , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
+ _:Map
+ )
+ StorageKeyId |-> StorageKey:String
+ ValueId |-> V:Value
+ ...
+
+
+ rule mxRustEmptyValue(noType) ~> storeHostValue(...) ~> setIfEmpty
+ => .K
+ rule storeHostValue(... value: wrappedRust(_))
+ ~> setIfEmpty ~> MX#storageStore(_)
+ => .K
+
+ rule
+
+ normalizedMethodCall
+ ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+ , #token("get", "Identifier"):Identifier
+ , ( ptr(SelfId:Int)
+ , .NormalizedCallParams
+ )
+ )
+ => MX#storageLoad(mxStringValue(StorageKey), rustDestination(NextId, ResultType))
+ ~> mxRustLoadPtr(NextId)
+ ...
+
+
+ SelfId |-> struct
+ ( Type
+ , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
+ #token("result_type", "Identifier"):Identifier |-> ResultTypeId:Int
+ _:Map
+ )
+ StorageKeyId |-> StorageKey:String
+ ResultTypeId |-> ResultType:MxRustType
+ ...
+
+ NextId:Int => NextId +Int 1
+
+ syntax MxRustInstruction ::= "setIfEmpty"
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/mx-rust-common.md b/mx-rust-semantics/main/mx-rust-common.md
new file mode 100644
index 0000000..1758966
--- /dev/null
+++ b/mx-rust-semantics/main/mx-rust-common.md
@@ -0,0 +1,17 @@
+```k
+
+requires "expression.md"
+requires "glue.md"
+requires "modules.md"
+requires "preprocessing.md"
+requires "representation.md"
+
+module MX-RUST-COMMON
+ imports private MX-RUST-EXPRESSION
+ imports private MX-RUST-GLUE
+ imports private MX-RUST-MODULES
+ imports private MX-RUST-PREPROCESSING
+ imports private MX-RUST-REPRESENTATION
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/preprocessing.md b/mx-rust-semantics/main/preprocessing.md
new file mode 100644
index 0000000..812d0c0
--- /dev/null
+++ b/mx-rust-semantics/main/preprocessing.md
@@ -0,0 +1,11 @@
+```k
+
+requires "preprocessing/methods.md"
+requires "preprocessing/traits.md"
+
+module MX-RUST-PREPROCESSING
+ imports private MX-RUST-PREPROCESSING-METHODS
+ imports private MX-RUST-PREPROCESSING-TRAITS
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md
new file mode 100644
index 0000000..5d4d3f9
--- /dev/null
+++ b/mx-rust-semantics/main/preprocessing/methods.md
@@ -0,0 +1,124 @@
+```k
+
+module MX-RUST-PREPROCESSING-METHODS
+ imports private COMMON-K-CELL
+ imports private K-EQUAL-SYNTAX
+ imports private LIST
+ imports private MX-RUST-REPRESENTATION
+ imports private RUST-PREPROCESSING-CONFIGURATION
+ imports private RUST-REPRESENTATION
+ imports private RUST-SHARED-SYNTAX
+ imports private STRING
+
+ syntax Identifier ::= "storage_mapper" [token]
+
+ syntax MxRustInstruction ::= mxRustPreprocessMethods(trait: TypePath, methodNames: List)
+ | mxRustPreprocessMethod(trait: TypePath, methodName: Identifier)
+ | addStorageMethodBody
+ ( trait: TypePath
+ , methodName: Identifier
+ , storageName:String
+ , mapperValueType:MxRustTypeOrError
+ )
+
+ rule
+ mxRustPreprocessMethods(T:TypePath)
+ => mxRustPreprocessMethods(T, MethodNames)
+ ...
+
+ T
+ MethodNames:List
+
+ rule mxRustPreprocessMethods(_:TypePath, .List) => .K
+ rule mxRustPreprocessMethods(T:TypePath, ListItem(MethodName:Identifier) Names:List)
+ => mxRustPreprocessMethod(T, MethodName) ~> mxRustPreprocessMethods(T, Names)
+
+ rule
+
+ mxRustPreprocessMethod(Trait:TypePath, Method:Identifier)
+ => addStorageMethodBody
+ (... trait: Trait, methodName: Method
+ , storageName: getStorageName(Atts)
+ , mapperValueType: getMapperValueType(MapperValue)
+ )
+ ...
+
+ Trait
+ Method
+ empty
+ Atts:OuterAttributes
+
+ #token("SingleValueMapper", "Identifier") < MapperValue:GenericArg , .GenericArgList >
+
+ requires getStorageName(Atts) =/=K ""
+ [priority(50)]
+ rule mxRustPreprocessMethod(_Trait:TypePath, _Method:Identifier) => .K
+ [priority(100)]
+
+ rule
+
+ addStorageMethodBody
+ (... trait: Trait:TypePath, methodName: Method:Identifier
+ , storageName: StorageName:String
+ , mapperValueType: MapperValueType:MxRustType) => .K
+ ...
+
+ Trait
+ Method
+ Params:NormalizedFunctionParameterList
+
+ empty => block(buildStorageMethodBody(Params, StorageName, MapperValueType))
+
+
+ syntax String ::= getStorageName(atts:OuterAttributes) [function, total]
+ rule getStorageName() => ""
+ rule getStorageName(.NonEmptyOuterAttributes) => ""
+ rule getStorageName
+ ( (#[ #token("storage_mapper", "Identifier") :: .SimplePathList
+ ( Name:String, .CallParamsList )
+ ])
+ _:NonEmptyOuterAttributes
+ ) => Name
+ rule getStorageName
+ ( (#[ #token("view", "Identifier") :: .SimplePathList
+ ( _Name:PathExprSegments, .CallParamsList )
+ ])
+ Atts:NonEmptyOuterAttributes
+ )
+ => getStorageName(Atts)
+
+ syntax BlockExpression ::= buildStorageMethodBody
+ ( params: NormalizedFunctionParameterList
+ , storageName: String
+ , mapperValueType: MxRustType
+ ) [function, total]
+ rule buildStorageMethodBody
+ (... params: (_S:SelfSort : _), Params:NormalizedFunctionParameterList
+ , storageName: StorageName:String
+ , mapperValueType: ValueType:MxRustType
+ )
+ => { .InnerAttributes
+ #token("SingleValueMapper", "Identifier"):Identifier
+ :: #token("new", "Identifier"):PathIdentSegment
+ ( concatString(StorageName, buildParamsConcat(Params))
+ , ptrValue(null, ValueType)
+ , .CallParamsList
+ )
+ }
+
+ syntax Expression ::= buildParamsConcat(params: NormalizedFunctionParameterList) [function , total]
+ rule buildParamsConcat(.NormalizedFunctionParameterList) => ""
+ rule buildParamsConcat(Param:NormalizedFunctionParameter , L:NormalizedFunctionParameterList)
+ => concatString(paramToString(Param), buildParamsConcat(L))
+
+ syntax Expression ::= paramToString(NormalizedFunctionParameter) [function, total]
+ rule paramToString(I:Identifier : _:Type) => toString(I)
+ rule paramToString(S:SelfSort : _:Type) => toString(S)
+
+ syntax MxRustTypeOrError ::= getMapperValueType(GenericArg) [function, total]
+ rule getMapperValueType(Type:GenericArg) => error("unknown Mx-Rust type", Type)
+ [owise]
+ rule getMapperValueType(#token("BigUint", "Identifier")) => BigUint
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/preprocessing/traits.md b/mx-rust-semantics/main/preprocessing/traits.md
new file mode 100644
index 0000000..e37339e
--- /dev/null
+++ b/mx-rust-semantics/main/preprocessing/traits.md
@@ -0,0 +1,27 @@
+```k
+
+module MX-RUST-PREPROCESSING-TRAITS
+ imports private COMMON-K-CELL
+ imports private LIST
+ imports private MX-RUST-REPRESENTATION
+ imports private RUST-PREPROCESSING-CONFIGURATION
+ imports private RUST-SHARED-SYNTAX
+
+ syntax MxRustInstruction ::= mxRustPreprocessTraits(List)
+ | mxRustPreprocessTrait(TypePath)
+
+ rule
+
+ mxRustPreprocessTraits => mxRustPreprocessTraits(Traits)
+ ...
+
+ Traits:List
+
+ rule mxRustPreprocessTraits(.List) => .K
+ rule mxRustPreprocessTraits(ListItem(Trait:TypePath) Traits:List)
+ => mxRustPreprocessTrait(Trait) ~> mxRustPreprocessTraits(Traits)
+
+ rule mxRustPreprocessTrait(Trait:TypePath) => mxRustPreprocessMethods(Trait)
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md
new file mode 100644
index 0000000..a17f947
--- /dev/null
+++ b/mx-rust-semantics/main/representation.md
@@ -0,0 +1,28 @@
+```k
+
+module MX-RUST-REPRESENTATION
+ imports RUST-REPRESENTATION
+ imports RUST-SHARED-SYNTAX
+
+ syntax MxRustInstruction ::= "mxRustPreprocessTraits"
+ | mxRustPreprocessMethods(TypePath)
+ | mxRustNewValue(ValueOrError)
+ | mxRustEmptyValue(MxRustType)
+ | mxValueToRust(Type)
+ | mxRustLoadPtr(Int)
+
+ syntax MxRustType ::= "noType" | "BigUint"
+ syntax MxRustTypeOrError ::= MxRustType | SemanticsError
+ syntax Value ::= MxRustType
+
+ syntax SemanticsError ::= unknownMxRustType(GenericArg)
+
+ syntax MxWrappedValue ::= wrappedRust(Value)
+
+ syntax Expression ::= concatString(Expression, Expression) [seqstrict]
+ | toString(Expression) [strict]
+
+ syntax MxValue ::= rustDestination(Int, MxRustType)
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/blockchain/configuration.md b/mx-rust-semantics/targets/blockchain/configuration.md
new file mode 100644
index 0000000..8a1526a
--- /dev/null
+++ b/mx-rust-semantics/targets/blockchain/configuration.md
@@ -0,0 +1,21 @@
+```k
+
+requires "../../main/configuration.md"
+
+module COMMON-K-CELL
+ configuration
+ .K
+endmodule
+
+module MX-RUST-CONFIGURATION
+ imports COMMON-K-CELL
+ imports MX-RUST-COMMON-CONFIGURATION
+
+ configuration
+
+
+
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/blockchain/mx-rust.md b/mx-rust-semantics/targets/blockchain/mx-rust.md
new file mode 100644
index 0000000..f12e9e3
--- /dev/null
+++ b/mx-rust-semantics/targets/blockchain/mx-rust.md
@@ -0,0 +1,21 @@
+```k
+
+requires "configuration.md"
+requires "mx-semantics/main/mx-common.md"
+requires "mx-semantics/main/syntax.md"
+requires "rust-semantics/rust-common.md"
+requires "rust-semantics/rust-common-syntax.md"
+requires "../../main/mx-rust-common.md"
+
+module MX-RUST-SYNTAX
+ imports RUST-COMMON-SYNTAX
+endmodule
+
+module MX-RUST
+ imports private MX-COMMON
+ imports private MX-RUST-COMMON
+ imports private MX-RUST-CONFIGURATION
+ imports private RUST-COMMON
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/testing/configuration.md b/mx-rust-semantics/targets/testing/configuration.md
new file mode 100644
index 0000000..724e3ec
--- /dev/null
+++ b/mx-rust-semantics/targets/testing/configuration.md
@@ -0,0 +1,30 @@
+```k
+
+requires "../../main/configuration.md"
+requires "../../test/configuration.md"
+
+module COMMON-K-CELL
+ imports MX-RUST-REPRESENTATION
+ imports RUST-PREPROCESSING-SYNTAX
+ imports RUST-SHARED-SYNTAX
+
+ syntax MxRustTest
+
+ configuration
+ crateParser($PGM:Crate) ~> mxRustPreprocessTraits ~> ($TEST:MxRustTest):KItem
+endmodule
+
+module MX-RUST-CONFIGURATION
+ imports COMMON-K-CELL
+ imports MX-RUST-COMMON-CONFIGURATION
+ imports MX-RUST-EXECUTION-TEST-CONFIGURATION
+
+ configuration
+
+
+
+
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/testing/mx-rust.md b/mx-rust-semantics/targets/testing/mx-rust.md
new file mode 100644
index 0000000..3acfae8
--- /dev/null
+++ b/mx-rust-semantics/targets/testing/mx-rust.md
@@ -0,0 +1,31 @@
+```k
+
+requires "configuration.md"
+requires "mx-semantics/main/mx-common.md"
+requires "mx-semantics/main/syntax.md"
+requires "mx-semantics/test/configuration.md"
+requires "mx-semantics/test/execution.md"
+requires "rust-semantics/rust-common.md"
+requires "rust-semantics/rust-common-syntax.md"
+requires "rust-semantics/test/configuration.md"
+requires "rust-semantics/test/execution.md"
+requires "../../main/mx-rust-common.md"
+requires "../../main/representation.md"
+requires "../../test/execution.md"
+
+module MX-RUST-SYNTAX
+ imports RUST-COMMON-SYNTAX
+ imports MX-RUST-TESTING-PARSING-SYNTAX
+endmodule
+
+module MX-RUST
+ imports private MX-COMMON
+ imports private MX-RUST-TEST
+ imports private MX-RUST-CONFIGURATION
+ imports private MX-RUST-COMMON
+ imports private MX-TEST-EXECUTION
+ imports private RUST-COMMON
+ imports private RUST-EXECUTION-TEST
+endmodule
+
+```
diff --git a/mx-rust-semantics/test/configuration.md b/mx-rust-semantics/test/configuration.md
new file mode 100644
index 0000000..0701dcb
--- /dev/null
+++ b/mx-rust-semantics/test/configuration.md
@@ -0,0 +1,15 @@
+```k
+
+module MX-RUST-EXECUTION-TEST-CONFIGURATION
+ imports MX-TEST-CONFIGURATION
+ imports RUST-EXECUTION-TEST-CONFIGURATION
+
+ configuration
+
+
+
+ .Map
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/test/execution.md b/mx-rust-semantics/test/execution.md
new file mode 100644
index 0000000..267e32f
--- /dev/null
+++ b/mx-rust-semantics/test/execution.md
@@ -0,0 +1,54 @@
+```k
+
+module MX-RUST-TESTING-PARSING-SYNTAX
+ imports INT-SYNTAX
+ imports MX-TEST-EXECUTION-PARSING-SYNTAX
+ imports RUST-EXECUTION-TEST-PARSING-SYNTAX
+ imports RUST-SHARED-SYNTAX
+ imports RUST-VALUE-SYNTAX
+ imports STRING-SYNTAX
+
+ syntax MxRustTest ::= ExecutionTest
+ syntax ExecutionItem ::= "set_named" String
+ | "push_named" String
+ | "get_bigint_from_struct"
+ | "check_eq" Int
+ | TestInstruction
+
+endmodule
+
+module MX-RUST-TEST
+ imports private COMMON-K-CELL
+ imports private MX-RUST-EXECUTION-TEST-CONFIGURATION
+ imports private MX-RUST-TESTING-PARSING-SYNTAX
+ imports private RUST-EXECUTION-CONFIGURATION
+
+ rule
+ set_named Name:String => .K ...
+ ListItem(Value) => .List ...
+ M:Map => M[Name <- Value]
+
+ rule
+ push_named Name:String => .K ...
+ .List => ListItem(Value) ...
+ Name |-> Value ...
+
+ rule
+
+ ptrValue
+ ( _
+ , struct
+ ( #token("BigUint", "Identifier")
+ , #token("mx_biguint_id", "Identifier"):Identifier |-> BigUintIdId _:Map
+ )
+ )
+ ~> get_bigint_from_struct ; Test:ExecutionTest
+ => push mxIntValue(MInt2Unsigned(BigUintId))
+ ~> get_big_int
+ ~> Test
+ ...
+
+ BigUintIdId |-> i32(BigUintId:MInt{32}) ...
+endmodule
+
+```
diff --git a/mx-semantics/targets/testing/configuration.md b/mx-semantics/targets/testing/configuration.md
index 3f6e4b5..9e0155c 100644
--- a/mx-semantics/targets/testing/configuration.md
+++ b/mx-semantics/targets/testing/configuration.md
@@ -17,9 +17,9 @@ module MX-CONFIGURATION
configuration
-
+
endmodule
diff --git a/mx-semantics/test/execution.md b/mx-semantics/test/execution.md
index 2386f63..23a3d5c 100644
--- a/mx-semantics/test/execution.md
+++ b/mx-semantics/test/execution.md
@@ -18,7 +18,7 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX
| setCallee(String)
| addAccount(String)
| setBalance(account:String, token:String, nonce:Int, value:Int)
- | setStorage(account:String, key:String, value:MxValue)
+ | setStorage(account:String, key:String, value:MxWrappedValue)
| setBlockTimestamp(Int)
| setMockCode(String, MxValue)
@@ -238,7 +238,7 @@ module MX-ACCOUNTS-TEST
setStorage
(... account: Account:String
, key: Key:String
- , value: Value:MxValue
+ , value: Value:MxWrappedValue
) => .K
...
@@ -251,7 +251,7 @@ module MX-ACCOUNTS-TEST
setStorage
(... account: Account:String
, key: Key:String
- , value: Value:MxValue
+ , value: Value:MxWrappedValue
) => .K
...
@@ -260,7 +260,7 @@ module MX-ACCOUNTS-TEST
.Bag =>
Key
- wrappedMx(Value)
+ Value
[priority(100)]
diff --git a/parse-mx-rust-test.sh b/parse-mx-rust-test.sh
new file mode 100755
index 0000000..abb0296
--- /dev/null
+++ b/parse-mx-rust-test.sh
@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+ --output kore \
+ --definition .build/mx-rust-testing-kompiled \
+ --module MX-RUST-SYNTAX \
+ --sort MxRustTest \
+ $1
diff --git a/parse-mx-rust.sh b/parse-mx-rust.sh
new file mode 100755
index 0000000..c20b2ec
--- /dev/null
+++ b/parse-mx-rust.sh
@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+ --output kore \
+ --definition .build/mx-rust-testing-kompiled \
+ --module RUST-COMMON-SYNTAX \
+ --sort Crate \
+ $1
diff --git a/rust-semantics/config.md b/rust-semantics/config.md
index 2f7f00f..155771d 100644
--- a/rust-semantics/config.md
+++ b/rust-semantics/config.md
@@ -6,8 +6,8 @@ module RUST-CONFIGURATION
configuration
-
+
endmodule
diff --git a/rust-semantics/expression/calls.md b/rust-semantics/expression/calls.md
index 32abd98..3c2d535 100644
--- a/rust-semantics/expression/calls.md
+++ b/rust-semantics/expression/calls.md
@@ -14,6 +14,16 @@ module RUST-EXPRESSION-CALLS
, params: CallParamsList
, reversedNormalizedParams: NormalizedCallParams
)
+ syntax Instruction ::= staticMethodCall
+ ( traitName: TypePath
+ , method: Identifier
+ , params: CallParamsList
+ , reversedNormalizedParams: NormalizedCallParams
+ )
+ syntax Instruction ::= reverseNormalizeParams
+ ( params: CallParamsList
+ , reversedNormalizedParams: NormalizedCallParams
+ )
syntax NormalizedCallParams ::= reverse(NormalizedCallParams, NormalizedCallParams) [function, total]
rule reverse(.NormalizedCallParams, R:NormalizedCallParams) => R
@@ -28,35 +38,50 @@ module RUST-EXPRESSION-CALLS
rule
- methodCall
- (... self: ptrValue(ptr(A) #as P, _)
- , method: MethodName:Identifier
- , params: Args:CallParamsList
- )
- => methodCall
- (... traitName: TraitName
- , method: MethodName
- , params: Args
- , reversedNormalizedParams: P, .NormalizedCallParams
- )
+ ( .K
+ => reverseNormalizeParams
+ (... params: Args
+ , reversedNormalizedParams: P, .NormalizedCallParams
+ )
+ ~> TraitName
+ )
+ ~> methodCall
+ (... self: ptrValue(ptr(A) #as P, _)
+ , method: _MethodName:Identifier
+ , params: Args:CallParamsList
+ )
...
A |-> struct(TraitName:TypePath, _) ...
requires isValueWithPtr(Args)
- rule methodCall
- (... traitName: _TraitName:TypePath
- , method: _MethodName:Identifier
- , params: (ptrValue(ptr(_) #as P:Ptr, _:Value) , Cps:CallParamsList) => Cps
+ rule
+ ( reverseNormalizeParams
+ (... params: .CallParamsList
+ , reversedNormalizedParams: Args:NormalizedCallParams
+ )
+ ~> TraitName:TypePath
+ ~> methodCall
+ (... self: _
+ , method: MethodName:Identifier
+ , params: _:CallParamsList
+ )
+ )
+ => normalizedMethodCall
+ ( TraitName
+ , MethodName
+ , reverse(Args, .NormalizedCallParams)
+ )
+
+ rule reverseNormalizeParams
+ (... params: (ptrValue(ptr(_) #as P:Ptr, _:Value) , Cps:CallParamsList) => Cps
, reversedNormalizedParams: Args:NormalizedCallParams
=> P, Args
)
rule
- methodCall
- (... traitName: _TraitName:TypePath
- , method: _MethodName:Identifier
- , params: (ptrValue(null, V:Value) , Cps:CallParamsList) => Cps
+ reverseNormalizeParams
+ (... params: (ptrValue(null, V:Value) , Cps:CallParamsList) => Cps
, reversedNormalizedParams: Args:NormalizedCallParams
=> ptr(NextId), Args
)
@@ -64,13 +89,41 @@ module RUST-EXPRESSION-CALLS
NextId:Int => NextId +Int 1
Values:Map => Values[NextId <- V]
+
+ rule TraitName:Identifier :: MethodName:Identifier :: .PathExprSegments ( )
+ => staticMethodCall(... trait: TraitName, method: MethodName, params: .CallParamsList)
+ rule TraitName:Identifier :: MethodName:Identifier :: .PathExprSegments
+ ( Args:CallParamsList )
+ => staticMethodCall(... trait: TraitName, method: MethodName, params: Args)
+ rule TraitName:Identifier :: MethodName:Identifier :: .PathExprSegments
+ ( Args:CallParamsList , )
+ => staticMethodCall(... trait: TraitName, method: MethodName, params: Args)
+
rule
- methodCall
- (... traitName: TraitName:TypePath
- , method: MethodName:Identifier
- , params: .CallParamsList
- , reversedNormalizedParams: Args:NormalizedCallParams
- )
+ ( .K
+ => reverseNormalizeParams
+ (... params: Args
+ , reversedNormalizedParams: .NormalizedCallParams
+ )
+ )
+ ~> staticMethodCall
+ (... trait: _TraitName:TypePath
+ , method: _MethodName:Identifier
+ , params: Args:CallParamsList
+ )
+ requires isValueWithPtr(Args)
+
+ rule
+ ( reverseNormalizeParams
+ (... params: .CallParamsList
+ , reversedNormalizedParams: Args:NormalizedCallParams
+ )
+ ~> staticMethodCall
+ (... trait: TraitName:TypePath
+ , method: MethodName:Identifier
+ , params: _:CallParamsList
+ )
+ )
=> normalizedMethodCall
( TraitName
, MethodName
diff --git a/rust-semantics/expression/casts.md b/rust-semantics/expression/casts.md
index c7988eb..9138421 100644
--- a/rust-semantics/expression/casts.md
+++ b/rust-semantics/expression/casts.md
@@ -39,6 +39,7 @@ module RUST-CASTS
rule implicitCast(V:Bool, bool) => V
rule implicitCast(struct(T, _) #as V, T) => V
+ rule implicitCast(struct(T, _) #as V, T < _ >) => V
// Rewrites
diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md
index 437ab2e..c47e0d0 100644
--- a/rust-semantics/expression/literals.md
+++ b/rust-semantics/expression/literals.md
@@ -18,6 +18,7 @@ module RUST-EXPRESSION-INTEGER-LITERALS
rule I:IntegerLiteral => wrapPtrValueOrError(null, parseInteger(I))
rule B:Bool:LiteralExpression => ptrValue(null, B:Bool:Value)
+ rule S:String => ptrValue(null, S)
syntax ValueOrError ::= parseInteger(IntegerLiteral) [function, total]
| parseInteger(String) [function, total]
@@ -60,7 +61,6 @@ module RUST-EXPRESSION-INTEGER-LITERALS
[owise]
- syntax ValueOrError ::= integerToValue(Int, Type) [function, total]
rule integerToValue(I:Int, i32) => i32(Int2MInt(I))
requires sminMInt(32) <=Int I andBool I <=Int smaxMInt(32)
rule integerToValue(I:Int, u32) => u32(Int2MInt(I))
@@ -74,6 +74,13 @@ module RUST-EXPRESSION-INTEGER-LITERALS
=> error("integerToValue: unimplemented", ListItem(I:Int:KItem) ListItem(T:Type:KItem))
[owise]
+ rule valueToInteger(V:Value) => error("cannot convert to integer", ListItem(V)) [owise]
+ rule valueToInteger(i32(V:MInt{32})) => MInt2Signed(V)
+ rule valueToInteger(u32(V:MInt{32})) => MInt2Unsigned(V)
+ rule valueToInteger(i64(V:MInt{64})) => MInt2Signed(V)
+ rule valueToInteger(u64(V:MInt{64})) => MInt2Unsigned(V)
+ rule valueToInteger(u128(V:MInt{128})) => MInt2Unsigned(V)
+
syntax Bool ::= endsWith(containing:String, contained:String) [function, total]
rule endsWith(Containing:String, Contained:String)
=> substrString
diff --git a/rust-semantics/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md
index 01d33f6..fc3a6fd 100644
--- a/rust-semantics/preprocessing/configuration.md
+++ b/rust-semantics/preprocessing/configuration.md
@@ -14,6 +14,7 @@ module RUST-PREPROCESSING-CONFIGURATION
tuple(.ValueList)
+ .List // List of TypePath
my_identifier:TypePath
diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md
index 83e0ad1..4828b65 100644
--- a/rust-semantics/preprocessing/initialization.md
+++ b/rust-semantics/preprocessing/initialization.md
@@ -10,6 +10,7 @@ module INITIALIZATION
traitInitializer(Name:TypePath) => .K
...
+ .List => ListItem(Name) ...
...
.Bag
diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
index e3f2506..0ff511e 100644
--- a/rust-semantics/representation.md
+++ b/rust-semantics/representation.md
@@ -24,6 +24,7 @@ module RUST-VALUE-SYNTAX
| tuple(ValueList)
| struct(TypePath, Map) // Map from field name (Identifier) to value ID (Int)
| Bool
+ | String
syntax ValueList ::= List{Value, ","}
syntax ValueOrError ::= Value | SemanticsError
@@ -66,6 +67,12 @@ module RUST-REPRESENTATION
, params: CallParamsList
)
[seqstrict(1, 3), result(ValueWithPtr)]
+ | staticMethodCall
+ ( trait: TypePath
+ , method: Identifier
+ , params: CallParamsList
+ )
+ [strict(3), result(ValueWithPtr)]
syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError
@@ -85,6 +92,10 @@ module RUST-REPRESENTATION
syntax Bool ::= isLocalVariable(ValueName) [function, total]
syntax Bool ::= isValueWithPtr(K) [function, total, symbol(isValueWithPtr)]
+ syntax IntOrError ::= Int | SemanticsError
+ syntax IntOrError ::= valueToInteger(Value) [function, total]
+ syntax ValueOrError ::= integerToValue(Int, Type) [function, total]
+
endmodule
```
diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md
index e9de99b..c3747ab 100644
--- a/rust-semantics/rust-common-syntax.md
+++ b/rust-semantics/rust-common-syntax.md
@@ -324,7 +324,6 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
| BreakExpression
| UnderscoreExpression
- | CallExpression
| ErrorPropagationExpression
| TypeCastExpression
// TODO: Removed because it causes ambiguities.
@@ -340,7 +339,11 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
> Expression "." Identifier // FieldExpression
- // > CallExpression
+ // https://doc.rust-lang.org/reference/expressions/call-expr.html
+ // TODO: Not implemented properly to avoid ambiguities
+ > PathExpression "(" ")"
+ > PathExpression "(" CallParams ")"
+
| Expression "[" Expression "]"
// > ErrorPropagationExpression
@@ -527,9 +530,6 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
```k
- // TODO: Not implemented properly to avoid ambiguities
- syntax CallExpression ::= PathExpression "(" MaybeCallParams ")"
- syntax MaybeCallParams ::= "" | CallParams
syntax CallParams ::= CallParamsList | CallParamsList ","
syntax CallParamsList ::= NeList{Expression, ","}
@@ -582,6 +582,7 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
syntax MacroInvocation ::= SimplePath "!" DelimTokenTree
// TODO: Not implemented properly
syntax DelimTokenTree ::= "(" MaybeCallParams ")"
+ syntax MaybeCallParams ::= "" | CallParams
// TODO: Not implemented properly
syntax MacroInvocationSemi ::= MacroInvocation ";"
diff --git a/rust-semantics/targets/execution/configuration.md b/rust-semantics/targets/execution/configuration.md
index c035ed0..bb59e86 100644
--- a/rust-semantics/targets/execution/configuration.md
+++ b/rust-semantics/targets/execution/configuration.md
@@ -15,9 +15,9 @@ module RUST-RUNNING-CONFIGURATION
configuration
-
-
+
+
endmodule
diff --git a/rust-semantics/targets/preprocessing/configuration.md b/rust-semantics/targets/preprocessing/configuration.md
index d122260..014bdc4 100644
--- a/rust-semantics/targets/preprocessing/configuration.md
+++ b/rust-semantics/targets/preprocessing/configuration.md
@@ -14,10 +14,10 @@ module RUST-RUNNING-CONFIGURATION
configuration
-
+
endmodule
diff --git a/tests/mx-rust/storage.1.run b/tests/mx-rust/storage.1.run
new file mode 100644
index 0000000..911768f
--- /dev/null
+++ b/tests/mx-rust/storage.1.run
@@ -0,0 +1,12 @@
+
+addAccount("Owner");
+setCallee("Owner");
+new Storage;
+set_named "self";
+push_named "self";
+push 10u64;
+call Storage.set_no_arg;
+push_named "self";
+call Storage.get_no_arg;
+get_bigint_from_struct;
+check_eq mxIntValue(10)
diff --git a/tests/mx-rust/storage.2.run b/tests/mx-rust/storage.2.run
new file mode 100644
index 0000000..bdefa78
--- /dev/null
+++ b/tests/mx-rust/storage.2.run
@@ -0,0 +1,9 @@
+
+addAccount("Owner");
+setCallee("Owner");
+new Storage;
+set_named "self";
+push_named "self";
+call Storage.get_no_arg;
+get_bigint_from_struct;
+check_eq mxIntValue(0)
diff --git a/tests/mx-rust/storage.3.run b/tests/mx-rust/storage.3.run
new file mode 100644
index 0000000..7881110
--- /dev/null
+++ b/tests/mx-rust/storage.3.run
@@ -0,0 +1,20 @@
+addAccount("Owner");
+setCallee("Owner");
+new Storage;
+set_named "self";
+
+push_named "self";
+push 10u64;
+call Storage.set_no_arg_if_empty;
+push_named "self";
+call Storage.get_no_arg;
+get_bigint_from_struct;
+check_eq mxIntValue(10);
+
+push_named "self";
+push 20u64;
+call Storage.set_no_arg_if_empty;
+push_named "self";
+call Storage.get_no_arg;
+get_bigint_from_struct;
+check_eq mxIntValue(10)
diff --git a/tests/mx-rust/storage.rs b/tests/mx-rust/storage.rs
new file mode 100644
index 0000000..0b16596
--- /dev/null
+++ b/tests/mx-rust/storage.rs
@@ -0,0 +1,33 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use multiversx_sc::imports::*;
+
+#[multiversx_sc::contract]
+pub trait Storage {
+ #[view(noArg)]
+ #[storage_mapper("no_arg")]
+ fn no_arg_storage(&self) -> SingleValueMapper;
+
+ #[view(getName)]
+ #[storage_mapper("name")]
+ fn one_arg_storage(&self, key: u64) -> SingleValueMapper;
+
+ #[init]
+ fn init(&self) {}
+
+ #[upgrade]
+ fn upgrade(&self) {}
+
+ fn set_no_arg(&self, value: u64) {
+ self.no_arg_storage().set(BigUint::from(value))
+ }
+
+ fn get_no_arg(&self) -> BigUint {
+ self.no_arg_storage().get()
+ }
+
+ fn set_no_arg_if_empty(&self, value: u64) {
+ self.no_arg_storage().set_if_empty(BigUint::from(value))
+ }
+}
diff --git a/tests/mx/storage/get-existing-storage.mx b/tests/mx/storage/get-existing-storage.mx
index 0ebcd78..23a3457 100644
--- a/tests/mx/storage/get-existing-storage.mx
+++ b/tests/mx/storage/get-existing-storage.mx
@@ -1,6 +1,6 @@
addAccount("Owner");
setCallee("Owner");
-setStorage("Owner", "MyKey", mxStringValue("Hello"));
+setStorage("Owner", "MyKey", wrappedMx(mxStringValue("Hello")));
push mxIntValue(12);
push mxStringValue("MyKey");
diff --git a/tests/mx/storage/set-existing-storage.mx b/tests/mx/storage/set-existing-storage.mx
index 094fc9b..58be307 100644
--- a/tests/mx/storage/set-existing-storage.mx
+++ b/tests/mx/storage/set-existing-storage.mx
@@ -1,6 +1,6 @@
addAccount("Owner");
setCallee("Owner");
-setStorage("Owner", "MyKey", mxStringValue("Hello"));
+setStorage("Owner", "MyKey", wrappedMx(mxStringValue("Hello")));
push wrappedMx(mxStringValue("World"));
push mxStringValue("MyKey");