diff --git a/Makefile b/Makefile
index 7478b43..803b7da 100644
--- a/Makefile
+++ b/Makefile
@@ -39,7 +39,15 @@ 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
+MX_RUST_CONTRACT_TESTING_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+MX_RUST_CONTRACT_TESTING_KOMPILED ::= .build/mx-rust-contract-testing-kompiled
+MX_RUST_CONTRACT_TESTING_TIMESTAMP ::= $(MX_RUST_CONTRACT_TESTING_KOMPILED)/timestamp
+MX_RUST_CONTRACT_TESTING_INPUT_DIR ::= tests/mx-rust-contracts
+MX_RUST_CONTRACT_TESTING_OUTPUT_DIR ::= .build/mx-rust-contarcts/output
+MX_RUST_CONTRACT_TESTING_INPUTS ::= $(wildcard $(MX_RUST_CONTRACT_TESTING_INPUT_DIR)/*.run)
+MX_RUST_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(MX_RUST_CONTRACT_TESTING_INPUT_DIR)/%,$(MX_RUST_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_RUST_CONTRACT_TESTING_INPUTS))
+
+.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test
clean:
rm -r .build
@@ -48,9 +56,10 @@ build: $(RUST_PREPROCESSING_TIMESTAMP) \
$(RUST_EXECUTION_TIMESTAMP) \
$(MX_TESTING_TIMESTAMP) \
$(MX_RUST_TIMESTAMP) \
- $(MX_RUST_TESTING_TIMESTAMP)
+ $(MX_RUST_TESTING_TIMESTAMP) \
+ $(MX_RUST_CONTRACT_TESTING_TIMESTAMP)
-test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test
+test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test
syntax-test: $(SYNTAX_OUTPUTS)
@@ -62,6 +71,8 @@ mx-test: $(MX_TESTING_OUTPUTS)
mx-rust-test: $(MX_RUST_TESTING_OUTPUTS)
+mx-rust-contract-test: $(MX_RUST_CONTRACT_TESTING_OUTPUTS)
+
$(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
# Workaround for https://github.com/runtimeverification/k/issues/4141
-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -93,6 +104,15 @@ $(MX_RUST_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX
-I . \
--debug
+
+$(MX_RUST_CONTRACT_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_CONTRACT_TESTING_KOMPILED)
+ $$(which kompile) mx-rust-semantics/targets/contract-testing/mx-rust.md \
+ -o $(MX_RUST_CONTRACT_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 $@
@@ -154,3 +174,23 @@ $(MX_RUST_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
-pTEST=$(CURDIR)/parse-mx-rust-test.sh
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_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+ $(MX_RUST_CONTRACT_TESTING_INPUT_DIR)/%.run \
+ $(MX_RUST_CONTRACT_TESTING_TIMESTAMP) \
+ parse-mx-rust-contract.sh \
+ parse-mx-rust-contract-test.sh
+ mkdir -p $(MX_RUST_CONTRACT_TESTING_OUTPUT_DIR)
+ krun \
+ "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
+ --definition $(MX_RUST_CONTRACT_TESTING_KOMPILED) \
+ --parser $(CURDIR)/parse-mx-rust-contract.sh \
+ --output kore \
+ --output-file $@.tmp \
+ -cTEST='$(shell cat $<)' \
+ -pTEST=$(CURDIR)/parse-mx-rust-contract-test.sh
+ cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+ mv -f $@.tmp $@
diff --git a/mx-rust-semantics/main/calls.md b/mx-rust-semantics/main/calls.md
new file mode 100644
index 0000000..f0b6c1c
--- /dev/null
+++ b/mx-rust-semantics/main/calls.md
@@ -0,0 +1,9 @@
+```k
+
+requires "calls/implementation.md"
+
+module MX-RUST-CALLS
+ imports private MX-RUST-CALLS-IMPLEMENTATION
+endmodule
+
+```
\ No newline at end of file
diff --git a/mx-rust-semantics/main/calls/configuration.md b/mx-rust-semantics/main/calls/configuration.md
new file mode 100644
index 0000000..3cab8a3
--- /dev/null
+++ b/mx-rust-semantics/main/calls/configuration.md
@@ -0,0 +1,17 @@
+```k
+
+module MX-RUST-CALLS-CONFIGURATION
+ imports LIST
+ imports RUST-SHARED-SYNTAX
+
+ configuration
+
+ .List
+ .Map // String to Identifier
+
+ // Valid only while a contract call is being prepared
+ (#token("no#path", "Identifier"):Identifier):TypePath
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/calls/implementation.md b/mx-rust-semantics/main/calls/implementation.md
new file mode 100644
index 0000000..f3119ce
--- /dev/null
+++ b/mx-rust-semantics/main/calls/implementation.md
@@ -0,0 +1,92 @@
+```k
+
+module MX-RUST-CALLS-IMPLEMENTATION
+ imports private COMMON-K-CELL
+ imports private MX-CALL-CONFIGURATION
+ imports private MX-COMMON-SYNTAX
+ imports private MX-RUST-CALLS-CONFIGURATION
+ imports private MX-RUST-REPRESENTATION
+ imports private RUST-EXECUTION-CONFIGURATION
+ imports private RUST-PREPROCESSING-CONFIGURATION
+ imports private RUST-REPRESENTATION
+ imports private RUST-SHARED-SYNTAX
+
+ rule (.K => rustValueToMx(V))
+ ~> rustValuesToMx((V:Value , L:ValueList => L), _:MxValueList)
+ rule (V:MxValue => .K)
+ ~> rustValuesToMx(_:ValueList, (L:MxValueList => V , L))
+ rule rustValuesToMx(.ValueList, ReversedArgs:MxValueList) ~> Hook:MxHookName
+ => Hook(reverse(ReversedArgs, .MxValueList))
+
+ rule
+
+ host.pushCallState => .K
+ ...
+
+ Execution:ExecutionCell
+ .List => ListItem(Execution) ...
+
+ rule
+
+ host.popCallState => .K
+ ...
+
+ (_:ExecutionCell => Execution)
+ ListItem(Execution:ExecutionCell) => .List ...
+
+ rule
+
+ host.resetCallState => .K
+ ...
+
+ (_:ExecutionCell => ... .Map )
+
+ rule
+
+ host.newEnvironment
+ ( rustCode
+ ( EndpointToFunction:Map
+ , TraitName:TypePath
+ , Preprocessed:PreprocessedCell
+ )
+ )
+ => .K
+ ...
+
+ _ => TraitName
+ _ => EndpointToFunction
+ (_:PreprocessedCell => Preprocessed)
+
+ rule
+
+ host.mkCall(FunctionName:String)
+ => MxRust#newContractObject(TraitName)
+ ~> MxRust#partialMethodCall(Endpoint, mxArgsToRustArgs(Args))
+ ...
+
+
+ FunctionName |-> Endpoint:Identifier ...
+
+
+ TraitName:TypePath
+ => (#token("no#path", "Identifier"):Identifier):TypePath
+
+ Args:MxValueList
+
+ rule ptrValue(...) #as SelfValue:Expression
+ ~> MxRust#partialMethodCall(Method:Identifier, Params:CallParamsList)
+ => methodCall(... self: SelfValue, method: Method, params: Params)
+
+ syntax MxRustInstruction ::= "MxRust#newContractObject" "(" TypePath ")"
+ rule MxRust#newContractObject(P:TypePath) => Rust#newStruct(P, .Map)
+
+ syntax MxRustInstruction ::= "MxRust#partialMethodCall" "(" Identifier "," CallParamsList ")"
+
+ syntax CallParamsList ::= mxArgsToRustArgs(MxValueList) [function, total]
+ rule mxArgsToRustArgs(.MxValueList) => .CallParamsList
+
+ rule (ptrValue(_, V:Value) => rustValueToMx(V)) ~> endCall
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/configuration.md b/mx-rust-semantics/main/configuration.md
index b7de223..d0fab20 100644
--- a/mx-rust-semantics/main/configuration.md
+++ b/mx-rust-semantics/main/configuration.md
@@ -1,16 +1,19 @@
```k
+requires "calls/configuration.md"
requires "mx-semantics/main/configuration.md"
requires "rust-semantics/config.md"
module MX-RUST-COMMON-CONFIGURATION
imports MX-COMMON-CONFIGURATION
+ imports MX-RUST-CALLS-CONFIGURATION
imports RUST-CONFIGURATION
configuration
+
endmodule
diff --git a/mx-rust-semantics/main/glue.md b/mx-rust-semantics/main/glue.md
index 9b9162d..137b0d0 100644
--- a/mx-rust-semantics/main/glue.md
+++ b/mx-rust-semantics/main/glue.md
@@ -1,50 +1,60 @@
```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 ...
+ imports private COMMON-K-CELL
+ imports private K-EQUAL-SYNTAX
+ imports private MX-COMMON-SYNTAX
+ imports private MX-RUST-REPRESENTATION
+ imports private RUST-EXECUTION-CONFIGURATION
+ imports private RUST-VALUE-SYNTAX
+
+ rule (.K => mxValueToRust(T, V))
+ ~> storeHostValue
+ (... destination: rustDestination(_ValueId, rustType(T):MxRustType)
+ , value: V:MxValue
+ )
+ requires notBool isMxEmptyValue(V)
+ rule
+
+ ptrValue(_, V:Value)
+ ~> storeHostValue
+ (... destination: rustDestination(ValueId, _:MxRustType)
+ , value: _:MxValue
+ )
+ => .K
+ ...
+
+ Values:Map => Values[ValueId <- V]
+ requires ValueId >=Int 0
+
+ rule
+ (.K => mxRustEmptyValue(T))
+ ~> storeHostValue
+ (... destination: rustDestination(_, T:MxRustType)
+ , value: mxEmptyValue
+ )
+
+ 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)
+ rule V:MxValue ~> mxValueToRust(T:Type)
+ => mxValueToRust(T, V)
+
+ rule mxValueToRust(T:Type, mxIntValue(I:Int))
=> mxRustNewValue(integerToValue(I, T))
+ requires
+ (T ==K i32 orBool T ==K u32)
+ orBool (T ==K i64 orBool T ==K u64)
+
endmodule
```
diff --git a/mx-rust-semantics/main/modules/biguint.md b/mx-rust-semantics/main/modules/biguint.md
index 1e4e363..9c333d0 100644
--- a/mx-rust-semantics/main/modules/biguint.md
+++ b/mx-rust-semantics/main/modules/biguint.md
@@ -41,8 +41,36 @@ module MX-RUST-MODULES-BIGUINT
)
)
- rule mxRustEmptyValue(BigUint) => mxRustBigIntNew(0)
+ rule mxRustEmptyValue(rustType(#token("BigUint", "Identifier")))
+ => mxRustBigIntNew(0)
+ rule mxValueToRust(#token("BigUint", "Identifier"), mxIntValue(I:Int))
+ => mxRustBigIntNew(I)
+
+ rule rustValueToMx
+ ( struct
+ ( #token("BigUint", "Identifier"):Identifier
+ , _:Map
+ ) #as S:Value
+ )
+ => mxRustGetBigIntFromStruct(S)
+
+ rule
+
+ mxRustGetBigIntFromStruct
+ ( struct
+ ( #token("BigUint", "Identifier"):Identifier
+ , #token("mx_biguint_id", "Identifier"):Identifier |-> BigUintIdId:Int
+ _:Map
+ )
+ )
+ => mxGetBigInt(MInt2Unsigned(BigUintId))
+ ...
+
+
+ BigUintIdId |-> i32(BigUintId:MInt{32})
+ ...
+
endmodule
```
diff --git a/mx-rust-semantics/main/modules/storage.md b/mx-rust-semantics/main/modules/storage.md
index 582f64b..e72ad16 100644
--- a/mx-rust-semantics/main/modules/storage.md
+++ b/mx-rust-semantics/main/modules/storage.md
@@ -35,7 +35,7 @@ module MX-RUST-MODULES-STORAGE
, .NormalizedCallParams
)
)
- => MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
+ => rustValuesToMx((V, .ValueList), (mxStringValue(StorageKey), .MxValueList)) ~> MX#storageStore
...
@@ -61,7 +61,8 @@ module MX-RUST-MODULES-STORAGE
)
=> MX#storageLoad(mxStringValue(StorageKey), rustDestination(-1, noType))
~> setIfEmpty
- ~> MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
+ ~> rustValuesToMx((V, .ValueList), (mxStringValue(StorageKey), .MxValueList))
+ ~> MX#storageStore
...
@@ -77,9 +78,10 @@ module MX-RUST-MODULES-STORAGE
rule mxRustEmptyValue(noType) ~> storeHostValue(...) ~> setIfEmpty
=> .K
- rule storeHostValue(... value: wrappedRust(_))
- ~> setIfEmpty ~> MX#storageStore(_)
+ rule storeHostValue(... value: V:MxValue)
+ ~> setIfEmpty ~> _:KItem ~> MX#storageStore
=> .K
+ requires notBool isMxEmptyValue(V)
rule
diff --git a/mx-rust-semantics/main/mx-rust-common.md b/mx-rust-semantics/main/mx-rust-common.md
index 1758966..ddd52cd 100644
--- a/mx-rust-semantics/main/mx-rust-common.md
+++ b/mx-rust-semantics/main/mx-rust-common.md
@@ -1,5 +1,6 @@
```k
+requires "calls.md"
requires "expression.md"
requires "glue.md"
requires "modules.md"
@@ -7,6 +8,7 @@ requires "preprocessing.md"
requires "representation.md"
module MX-RUST-COMMON
+ imports private MX-RUST-CALLS
imports private MX-RUST-EXPRESSION
imports private MX-RUST-GLUE
imports private MX-RUST-MODULES
diff --git a/mx-rust-semantics/main/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md
index 5d4d3f9..bf0676e 100644
--- a/mx-rust-semantics/main/preprocessing/methods.md
+++ b/mx-rust-semantics/main/preprocessing/methods.md
@@ -4,6 +4,7 @@ module MX-RUST-PREPROCESSING-METHODS
imports private COMMON-K-CELL
imports private K-EQUAL-SYNTAX
imports private LIST
+ imports private MX-RUST-CALLS-CONFIGURATION
imports private MX-RUST-REPRESENTATION
imports private RUST-PREPROCESSING-CONFIGURATION
imports private RUST-REPRESENTATION
@@ -14,12 +15,19 @@ module MX-RUST-PREPROCESSING-METHODS
syntax MxRustInstruction ::= mxRustPreprocessMethods(trait: TypePath, methodNames: List)
| mxRustPreprocessMethod(trait: TypePath, methodName: Identifier)
+ | mxRustPreprocessStorage(trait: TypePath, methodName: Identifier)
+ | mxRustPreprocessEndpoint(trait: TypePath, methodName: Identifier)
| addStorageMethodBody
( trait: TypePath
, methodName: Identifier
, storageName:String
, mapperValueType:MxRustTypeOrError
)
+ | mxRustAddEndpointMapping
+ ( trait: TypePath
+ , methodName: Identifier
+ , endpointName:String
+ )
rule
mxRustPreprocessMethods(T:TypePath)
@@ -33,9 +41,13 @@ module MX-RUST-PREPROCESSING-METHODS
rule mxRustPreprocessMethods(T:TypePath, ListItem(MethodName:Identifier) Names:List)
=> mxRustPreprocessMethod(T, MethodName) ~> mxRustPreprocessMethods(T, Names)
+ rule mxRustPreprocessMethod(Trait:TypePath, Method:Identifier)
+ => mxRustPreprocessStorage(Trait, Method)
+ ~> mxRustPreprocessEndpoint(Trait, Method)
+
rule
- mxRustPreprocessMethod(Trait:TypePath, Method:Identifier)
+ mxRustPreprocessStorage(Trait:TypePath, Method:Identifier)
=> addStorageMethodBody
(... trait: Trait, methodName: Method
, storageName: getStorageName(Atts)
@@ -52,9 +64,38 @@ module MX-RUST-PREPROCESSING-METHODS
requires getStorageName(Atts) =/=K ""
[priority(50)]
- rule mxRustPreprocessMethod(_Trait:TypePath, _Method:Identifier) => .K
+ rule mxRustPreprocessStorage(_Trait:TypePath, _Method:Identifier) => .K
+ [priority(100)]
+
+ rule
+
+ mxRustPreprocessEndpoint(Trait:TypePath, Method:Identifier)
+ => mxRustAddEndpointMapping
+ (... trait: Trait, methodName: Method
+ , endpointName: getEndpointName(Atts, Method)
+ )
+ ...
+
+ Trait
+ Method
+ Atts:OuterAttributes
+ requires getEndpointName(Atts, Method) =/=K ""
+ [priority(50)]
+ rule mxRustPreprocessEndpoint(_Trait:TypePath, _Method:Identifier) => .K
[priority(100)]
+ rule
+
+ mxRustAddEndpointMapping
+ (... trait: _Trait:TypePath, methodName: Method:Identifier
+ , endpointName: EndpointName:String
+ )
+ => .K
+ ...
+
+ M:Map => M[EndpointName <- Method]
+ requires notBool EndpointName in_keys(M)
+
rule
addStorageMethodBody
@@ -79,19 +120,41 @@ module MX-RUST-PREPROCESSING-METHODS
])
_:NonEmptyOuterAttributes
) => Name
- rule getStorageName
- ( (#[ #token("view", "Identifier") :: .SimplePathList
- ( _Name:PathExprSegments, .CallParamsList )
- ])
- Atts:NonEmptyOuterAttributes
- )
+ rule getStorageName(_:OuterAttribute Atts:NonEmptyOuterAttributes)
=> getStorageName(Atts)
+ [owise]
+
+ syntax String ::= getEndpointName(atts:OuterAttributes, default:Identifier) [function, total]
+ rule getEndpointName(, _:Identifier) => ""
+ rule getEndpointName(.NonEmptyOuterAttributes, _:Identifier) => ""
+ rule getEndpointName
+ ( (#[ #token("init", "Identifier") :: .SimplePathList
+ ])
+ _:NonEmptyOuterAttributes
+ , _:Identifier
+ ) => "#init"
+ rule getEndpointName
+ ( (#[ #token("upgrade", "Identifier") :: .SimplePathList
+ ])
+ _:NonEmptyOuterAttributes
+ , _:Identifier
+ ) => "#upgrade"
+ rule getEndpointName
+ ( (#[ #token("endpoint", "Identifier") :: .SimplePathList
+ ( Name:Identifier :: .PathExprSegments, .CallParamsList )
+ ])
+ _:NonEmptyOuterAttributes
+ , _:Identifier
+ ) => IdentifierToString(Name)
+ rule getEndpointName(_:OuterAttribute Atts:NonEmptyOuterAttributes, Default:Identifier)
+ => getEndpointName(Atts, Default)
+ [owise]
syntax BlockExpression ::= buildStorageMethodBody
( params: NormalizedFunctionParameterList
, storageName: String
, mapperValueType: MxRustType
- ) [function, total]
+ ) [function]
rule buildStorageMethodBody
(... params: (_S:SelfSort : _), Params:NormalizedFunctionParameterList
, storageName: StorageName:String
@@ -111,6 +174,7 @@ module MX-RUST-PREPROCESSING-METHODS
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)
@@ -118,7 +182,8 @@ module MX-RUST-PREPROCESSING-METHODS
syntax MxRustTypeOrError ::= getMapperValueType(GenericArg) [function, total]
rule getMapperValueType(Type:GenericArg) => error("unknown Mx-Rust type", Type)
[owise]
- rule getMapperValueType(#token("BigUint", "Identifier")) => BigUint
+ rule getMapperValueType(#token("BigUint", "Identifier") #as T:Type)
+ => rustType(T)
endmodule
```
diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md
index a17f947..0ff2ce9 100644
--- a/mx-rust-semantics/main/representation.md
+++ b/mx-rust-semantics/main/representation.md
@@ -1,28 +1,36 @@
```k
module MX-RUST-REPRESENTATION
+ imports MX-COMMON-SYNTAX
imports RUST-REPRESENTATION
imports RUST-SHARED-SYNTAX
syntax MxRustInstruction ::= "mxRustPreprocessTraits"
| mxRustPreprocessMethods(TypePath)
+ | mxRustCreateAccount(String)
+ | mxRustCreateContract(owner: String, contractAccount: String, code: Crate)
| mxRustNewValue(ValueOrError)
| mxRustEmptyValue(MxRustType)
| mxValueToRust(Type)
+ | mxValueToRust(Type, MxValue)
+ | rustValueToMx(Value)
+ | rustValuesToMx(ValueList, MxValueList)
| mxRustLoadPtr(Int)
+ | mxRustGetBigIntFromStruct(Value)
- syntax MxRustType ::= "noType" | "BigUint"
+ syntax MxRustType ::= "noType" | rustType(Type)
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)
+
+ syntax PreprocessedCell
+ syntax ContractCode ::= rustCode(endpointToFunction: Map, type: TypePath, preprocessed: PreprocessedCell)
endmodule
```
diff --git a/mx-rust-semantics/setup/mx.md b/mx-rust-semantics/setup/mx.md
new file mode 100644
index 0000000..1e7c311
--- /dev/null
+++ b/mx-rust-semantics/setup/mx.md
@@ -0,0 +1,107 @@
+```k
+
+module MX-RUST-SETUP-MX
+ imports private COMMON-K-CELL
+ imports private MX-COMMON-SYNTAX
+ imports private MX-RUST-CALLS-CONFIGURATION
+ imports private MX-RUST-REPRESENTATION
+ imports private MX-SETUP-SYNTAX
+ imports private RUST-PREPROCESSING-CONFIGURATION
+ imports private RUST-PREPROCESSING-SYNTAX
+
+ syntax MXRustInstruction ::= "MxRust#addAccountWithPreprocessedCode"
+ "(" owner: String
+ "," newAddress: String
+ "," egldValue: Int
+ "," gasLimit: Int
+ "," args: MxValueList
+ ")"
+ syntax MXRustInstruction ::= "MxRust#addAccountWithPreprocessedCode" "(" String "," TypePath ")"
+ | "MxRust#clearMxReturnValue"
+
+ rule mxRustCreateAccount(Address:String) => MXSetup#add_account(Address)
+
+ rule mxRustCreateContract
+ (... owner: Owner:String
+ , contractAccount: Contract:String
+ , code: Code:Crate
+ )
+ => crateParser(Code)
+ ~> mxRustPreprocessTraits
+ ~> MxRust#addAccountWithPreprocessedCode
+ (... owner: Owner
+ , newAddress: Contract
+ , egldValue: 0
+ , gasLimit: 0
+ , args: .MxValueList
+ )
+
+ // Trying to put the following three rules in one causes this kind of error:
+ //
+ // [Error] Internal: Uncaught exception thrown of type ClassCastException
+ // (ClassCastException: class org.kframework.kore.ADT$KAs cannot be cast to class
+ // org.kframework.kore.KRewrite (org.kframework.kore.ADT$KAs and
+ // org.kframework.kore.KRewrite are in unnamed module of loader 'app'))
+ //
+ // most likely, this happes because we need this:
+ //
+ // ... ListItem(TraitName:TypePath)
+ // #as Preprocessed:PreprocessedCell
+ //
+ // https://github.com/runtimeverification/k/issues/4638
+ rule
+
+ MxRust#addAccountWithPreprocessedCode
+ (...owner: Owner:String
+ , newAddress: Contract:String
+ , egldValue: EgldValue:Int
+ , gasLimit: GasLimit:Int
+ , args: Args:MxValueList
+ )
+ => MxRust#addAccountWithPreprocessedCode(Contract, TraitName)
+ ~> callContract
+ ( "#init"
+ , prepareIndirectContractCallInput
+ (... caller: Owner
+ , callee: Contract
+ , egldValue: EgldValue
+ , esdtTransfers: .MxEsdtTransferList
+ , gasLimit: GasLimit
+ , args:Args
+ )
+ )
+ ~> finishExecuteOnDestContext
+ ~> MxRust#clearMxReturnValue
+ ...
+
+ ... ListItem(TraitName:TypePath)
+
+ rule
+
+ MxRust#addAccountWithPreprocessedCode(Contract, TraitName)
+ => MxRust#clearPreprocessed
+ ~> MXSetup#add_account_with_code
+ ( Contract
+ , rustCode(EndpointToFunction, TraitName, Preprocessed)
+ )
+ ...
+
+ Preprocessed:PreprocessedCell
+ EndpointToFunction:Map
+
+ syntax MXRustInstruction ::= "MxRust#clearPreprocessed"
+ rule
+
+ MxRust#clearPreprocessed => .K
+ ...
+
+ (_:PreprocessedCell
+ => ... .List
+ )
+ _ => .Map
+
+ rule _V:MxValue ~> MxRust#clearMxReturnValue => .K
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/contract-testing/configuration.md b/mx-rust-semantics/targets/contract-testing/configuration.md
new file mode 100644
index 0000000..4a66aed
--- /dev/null
+++ b/mx-rust-semantics/targets/contract-testing/configuration.md
@@ -0,0 +1,38 @@
+```k
+
+requires "../../main/configuration.md"
+requires "../../test/configuration.md"
+
+module COMMON-K-CELL
+ imports MX-RUST-REPRESENTATION
+ imports RUST-SHARED-SYNTAX
+ imports STRING
+
+ syntax MxRustTest
+
+ configuration
+
+ mxRustCreateAccount("Owner")
+ ~> mxRustCreateContract
+ (... owner: "Owner"
+ , contractAccount: "TestContract"
+ , code: $PGM:Crate
+ )
+ ~> ($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/contract-testing/mx-rust.md b/mx-rust-semantics/targets/contract-testing/mx-rust.md
new file mode 100644
index 0000000..15d6188
--- /dev/null
+++ b/mx-rust-semantics/targets/contract-testing/mx-rust.md
@@ -0,0 +1,35 @@
+```k
+
+requires "configuration.md"
+requires "mx-semantics/main/mx-common.md"
+requires "mx-semantics/main/syntax.md"
+requires "mx-semantics/setup/setup.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 "../../setup/mx.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-RUST-SETUP-MX
+ imports private MX-SETUP
+ imports private MX-TEST-EXECUTION
+ imports private RUST-COMMON
+ imports private RUST-EXECUTION-TEST
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/testing/mx-rust.md b/mx-rust-semantics/targets/testing/mx-rust.md
index 3acfae8..7fd019d 100644
--- a/mx-rust-semantics/targets/testing/mx-rust.md
+++ b/mx-rust-semantics/targets/testing/mx-rust.md
@@ -3,6 +3,7 @@
requires "configuration.md"
requires "mx-semantics/main/mx-common.md"
requires "mx-semantics/main/syntax.md"
+requires "mx-semantics/setup/setup.md"
requires "mx-semantics/test/configuration.md"
requires "mx-semantics/test/execution.md"
requires "rust-semantics/rust-common.md"
@@ -20,6 +21,7 @@ endmodule
module MX-RUST
imports private MX-COMMON
+ imports private MX-SETUP
imports private MX-RUST-TEST
imports private MX-RUST-CONFIGURATION
imports private MX-RUST-COMMON
diff --git a/mx-rust-semantics/test/execution.md b/mx-rust-semantics/test/execution.md
index 267e32f..4837597 100644
--- a/mx-rust-semantics/test/execution.md
+++ b/mx-rust-semantics/test/execution.md
@@ -34,21 +34,15 @@ module MX-RUST-TEST
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}) ...
+ ptrValue
+ ( _
+ , struct
+ ( #token("BigUint", "Identifier")
+ , _:Map
+ ) #as S:Value
+ )
+ ~> get_bigint_from_struct
+ => mxRustGetBigIntFromStruct(S)
endmodule
```
diff --git a/mx-semantics/main/accounts/configuration.md b/mx-semantics/main/accounts/configuration.md
index a5b66c4..995a3e9 100644
--- a/mx-semantics/main/accounts/configuration.md
+++ b/mx-semantics/main/accounts/configuration.md
@@ -57,7 +57,7 @@ module MX-STORAGE-CONFIGURATION
""
- mxWrappedEmpty
+ mxEmptyValue:MxValue
endmodule
diff --git a/mx-semantics/main/accounts/storage-hooks.md b/mx-semantics/main/accounts/storage-hooks.md
index 06a8518..260493f 100644
--- a/mx-semantics/main/accounts/storage-hooks.md
+++ b/mx-semantics/main/accounts/storage-hooks.md
@@ -7,7 +7,7 @@ module MX-STORAGE-HOOKS
rule MX#storageLoad(mxStringValue(Key:String), Destination:MxValue )
=> storageLoad(getCallee(), Key, Destination)
- rule MX#storageStore(mxStringValue(Key:String), Value:MxWrappedValue)
+ rule MX#storageStore(mxStringValue(Key:String), Value:MxValue)
=> storageStore(getCallee(), Key, Value)
endmodule
diff --git a/mx-semantics/main/accounts/storage-tools.md b/mx-semantics/main/accounts/storage-tools.md
index 835630f..b18b706 100644
--- a/mx-semantics/main/accounts/storage-tools.md
+++ b/mx-semantics/main/accounts/storage-tools.md
@@ -5,7 +5,7 @@ module MX-STORAGE-TOOLS-SYNTAX
imports STRING-SYNTAX
syntax MxInstructions ::= storageLoad(address: String, key: String, destination: MxValue)
- | storageStore(address: String, key: String, value: MxWrappedValue)
+ | storageStore(address: String, key: String, value: MxValue)
endmodule
module MX-STORAGE-TOOLS
@@ -29,7 +29,7 @@ module MX-STORAGE-TOOLS
rule
storageLoad(... address: Address:String, key: _Key:String, destination: Destination:MxValue)
- => storeHostValue(Destination, mxWrappedEmpty)
+ => storeHostValue(Destination, mxEmptyValue)
...
Address
@@ -37,7 +37,7 @@ module MX-STORAGE-TOOLS
rule
- storageStore(... address: Address:String, key: Key:String, value: Value:MxWrappedValue)
+ storageStore(... address: Address:String, key: Key:String, value: Value:MxValue)
=> .K
...
@@ -48,7 +48,7 @@ module MX-STORAGE-TOOLS
rule
- storageStore(... address: Address:String, key: Key:String, value: Value:MxWrappedValue)
+ storageStore(... address: Address:String, key: Key:String, value: Value:MxValue)
=> .K
...
diff --git a/mx-semantics/main/biguint/tools.md b/mx-semantics/main/biguint/tools.md
index a880c91..1648d40 100644
--- a/mx-semantics/main/biguint/tools.md
+++ b/mx-semantics/main/biguint/tools.md
@@ -9,6 +9,10 @@ module MX-BIGUINT-TOOLS
clearBigInts => .K ...
_ => .Map
_ => 0
+
+ rule
+ mxGetBigInt(IntId:Int) => mxIntValue(V) ...
+ IntId |-> V:Int ...
endmodule
```
diff --git a/mx-semantics/main/calls/tools.md b/mx-semantics/main/calls/tools.md
index 22691b2..7a045d0 100644
--- a/mx-semantics/main/calls/tools.md
+++ b/mx-semantics/main/calls/tools.md
@@ -14,15 +14,6 @@ module MX-CALL-TOOLS-SYNTAX
args:MxValueList
)
- syntax MxCallDataCell ::= prepareIndirectContractCallInput(
- caller: String,
- callee: String,
- egldValue: Int,
- esdtTransfers: MxEsdtTransferList,
- gasLimit: Int,
- args: MxValueList
- ) [function, total]
-
endmodule
module MX-CALLS-TOOLS
@@ -43,12 +34,9 @@ module MX-CALLS-TOOLS
, input: MxCallDataCell
)
[symbol(callContractAux)]
- | callContract(function: String, input: MxCallDataCell )
- [symbol(callContractString)]
- | "finishExecuteOnDestContext" [symbol(finishExecuteOnDestContext)]
- | "endCall" [symbol(endCall)]
| "asyncExecute" [symbol(asyncExecute)]
| "setVMOutput" [symbol(setVMOutput)]
+ | "clearMxReturnValues"
| mkCall(function: String, callData: MxCallDataCell)
// -----------------------------------------------------------------------------------
@@ -83,6 +71,10 @@ module MX-CALLS-TOOLS
#as MxCallData
)
=> pushWorldState
+ // TODO: clearMxReturnValues is not part of the actual MX semantics,
+ // but it makes it easier to identify endpoints that do not
+ // return anything (see setVMOutput-no-retv).
+ ~> clearMxReturnValues
~> pushCallState
~> resetCallState
~> transferFunds(Caller, Callee, EgldValue)
@@ -314,6 +306,10 @@ module MX-CALLS-TOOLS
[owise]
// -----------------------------------------------------------------------
+ rule
+ (V:MxValue => .K) ~> endCall ...
+ .MxValueList => V, .MxValueList
+
rule [endCall]:
endCall
=> asyncExecute
@@ -365,6 +361,10 @@ module MX-CALLS-TOOLS
rule [[getCallee() => Callee]]
Callee:String
+ rule
+ clearMxReturnValues => .K ...
+ _ => .MxValueList
+
endmodule
```
diff --git a/mx-semantics/main/syntax.md b/mx-semantics/main/syntax.md
index 474abd8..60407ff 100644
--- a/mx-semantics/main/syntax.md
+++ b/mx-semantics/main/syntax.md
@@ -14,12 +14,13 @@ module MX-COMMON-SYNTAX
| MxEsdtTransfer
| mxTransfersValue(MxEsdtTransferList)
| mxUnitValue()
- | MxWrappedValue
- syntax MxWrappedValue ::= "mxWrappedEmpty"
+ | MxEmptyValue
+ syntax MxEmptyValue ::= "mxEmptyValue"
syntax MxHookName ::= r"MX#[a-zA-Z][a-zA-Z0-9]*" [token]
syntax MxValueList ::= List{MxValue, ","}
syntax HookCall ::= MxHookName "(" MxValueList ")"
+ syntax MxValueList ::= reverse(MxValueList, MxValueList) [function, total]
syntax Int ::= lengthValueList(MxValueList) [function, total]
syntax String ::= getMxString(MxValue) [function, total]
@@ -41,12 +42,17 @@ module MX-COMMON-SYNTAX
| "pushWorldState" [symbol(pushWorldState)]
| "dropWorldState" [symbol(dropWorldState)]
| "clearBigInts" [symbol(clearBigInts)]
+ | "endCall" [symbol(endCall)]
+ | "finishExecuteOnDestContext" [symbol(finishExecuteOnDestContext)]
| processBuiltinFunction(BuiltinFunction, String, String, MxCallDataCell)
[symbol(processBuiltinFunction)]
| newExecutionEnvironment(contractAddress:String)
| checkBool(Bool, String) [symbol(checkBool)]
| storeHostValue(destination: MxValue, value: MxValue)
| returnCallData(MxValue) [symbol(returnCallData)]
+ | mxGetBigInt(Int) [symbol(mxGetBigInt)]
+ | callContract(function: String, input: MxCallDataCell )
+ [symbol(callContractString)]
syntax MxHostInstructions ::= "host" "." "newEnvironment" "(" ContractCode ")"
| "host" "." "mkCall" "(" functionName:String ")"
@@ -79,6 +85,15 @@ module MX-COMMON-SYNTAX
| "SimulateFailed" [symbol(SimulateFailed)]
syntax String ::= getCallee() [function, total]
+
+ syntax MxCallDataCell ::= prepareIndirectContractCallInput(
+ caller: String,
+ callee: String,
+ egldValue: Int,
+ esdtTransfers: MxEsdtTransferList,
+ gasLimit: Int,
+ args: MxValueList
+ ) [function, total]
endmodule
```
diff --git a/mx-semantics/main/tools.md b/mx-semantics/main/tools.md
index 3e12a8d..aeafb80 100644
--- a/mx-semantics/main/tools.md
+++ b/mx-semantics/main/tools.md
@@ -23,6 +23,9 @@ module MX-TOOLS
// Fix for https://github.com/runtimeverification/k/issues/4587
rule lengthValueList(_) => 0 [owise]
+ rule reverse(.MxValueList, L:MxValueList) => L
+ rule reverse((E:MxValue , L1:MxValueList => L1), (L2:MxValueList => E , L2))
+
endmodule
```
\ No newline at end of file
diff --git a/mx-semantics/setup/setup.md b/mx-semantics/setup/setup.md
new file mode 100644
index 0000000..04d9994
--- /dev/null
+++ b/mx-semantics/setup/setup.md
@@ -0,0 +1,54 @@
+```k
+
+module MX-SETUP-SYNTAX
+ imports MX-COMMON-SYNTAX
+ imports STRING
+ syntax MxInstruction ::= "MXSetup#add_account" "(" String ")"
+ | "MXSetup#add_account_with_code" "(" String "," ContractCode ")"
+endmodule
+
+module MX-SETUP
+ imports private COMMON-K-CELL
+ imports private MX-ACCOUNTS-CONFIGURATION
+ imports private MX-SETUP-SYNTAX
+
+ syntax MxInstruction ::= "MXSetup#error"
+
+ rule
+ (.K => MXSetup#error) ~> MXSetup#add_account(S:String) ...
+ S
+ [priority(50)]
+ rule
+ MXSetup#add_account(S:String) => .K ...
+
+ .Bag
+ =>
+ S
+ // .Bag
+ // .Bag
+ ...
+
+ ...
+
+ [priority(100)]
+
+ rule
+ (.K => MXSetup#error) ~> MXSetup#add_account_with_code(S:String, _) ...
+ S
+ [priority(50)]
+ rule
+ MXSetup#add_account_with_code(S:String, Code:ContractCode) => .K ...
+
+ .Bag
+ =>
+ S
+ Code
+ ...
+
+ ...
+
+ [priority(100)]
+
+endmodule
+
+```
diff --git a/mx-semantics/targets/testing/mx.md b/mx-semantics/targets/testing/mx.md
index 548d0f8..ab8b3dd 100644
--- a/mx-semantics/targets/testing/mx.md
+++ b/mx-semantics/targets/testing/mx.md
@@ -4,6 +4,7 @@ requires "configuration.md"
requires "../../main/mx-common.md"
requires "../../main/communication-mocks.md"
requires "../../main/syntax.md"
+requires "../../setup/setup.md"
requires "../../test/execution.md"
module MX-SYNTAX
@@ -15,6 +16,7 @@ module MX
imports private MX-COMMON
imports private MX-COMMUNICATION-MOCKS
imports private MX-CONFIGURATION
+ imports private MX-SETUP
imports private MX-TEST-EXECUTION
endmodule
diff --git a/mx-semantics/test/execution.md b/mx-semantics/test/execution.md
index 23a3d5c..b4f2a59 100644
--- a/mx-semantics/test/execution.md
+++ b/mx-semantics/test/execution.md
@@ -6,6 +6,7 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX
imports STRING-SYNTAX
syntax TestInstruction ::= "error"
+ | "push"
| "push" MxValue
| "call" argcount:Int MxHookName
| "get_big_int"
@@ -18,7 +19,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:MxWrappedValue)
+ | setStorage(account:String, key:String, value:MxValue)
| setBlockTimestamp(Int)
| setMockCode(String, MxValue)
@@ -26,7 +27,6 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX
syntax MxValueStack ::= List{MxValue, ","}
- syntax MxWrappedValue ::= wrappedMx(MxValue)
endmodule
module MX-TEST-INTERNAL-SYNTAX
@@ -46,8 +46,13 @@ module MX-TEST-EXECUTION
imports private MX-TEST-CONFIGURATION
imports private MX-TEST-EXECUTION-PARSING-SYNTAX
- rule I:TestInstruction ; Is:MxTest => I ~> Is
- rule .MxTest => .K
+ rule Is:MxTest => mxChainTest(Is)
+
+ syntax K ::= mxChainTest(MxTest) [function, total]
+ rule mxChainTest(.MxTest) => .K
+ rule mxChainTest(I:TestInstruction ; Is:MxTest) => I ~> mxChainTest(Is)
+
+ rule V:MxValue ~> push => push V
rule
push V:MxValue => .K ...
@@ -57,9 +62,10 @@ module MX-TEST-EXECUTION
call N:Int Hook:MxHookName => Hook(takeArgs(N, L)) ...
L:MxValueStack => drop(N, L)
- rule
- V:MxValue => .K ...
- L:MxValueStack => V , L
+ rule V:MxValue ~> check_eq V => .K
+
+
+ rule mxIntValue(IntId) ~> get_big_int => testGetBigInt(IntId)
rule
get_big_int => testGetBigInt(IntId) ...
@@ -67,8 +73,8 @@ module MX-TEST-EXECUTION
rule
storeHostValue (... destination: Destination:MxValue, value: Value:MxValue)
- ~> push_store_data ; Is
- => Is
+ ~> push_store_data
+ => .K
...
L:MxValueStack => Destination, Value, L
@@ -172,25 +178,10 @@ endmodule
module MX-ACCOUNTS-TEST
imports private COMMON-K-CELL
imports private MX-ACCOUNTS-CONFIGURATION
+ imports private MX-SETUP-SYNTAX
imports private MX-TEST-EXECUTION-PARSING-SYNTAX
- rule
- (.K => error) ~> addAccount(S:String) ...
- S
- [priority(50)]
- rule
- addAccount(S:String) => .K ...
-
- .Bag
- =>
- S
- .Bag
- .Bag
- ...
-
- ...
-
- [priority(100)]
+ rule addAccount(S:String) => MXSetup#add_account(S)
rule
setBalance
@@ -238,7 +229,7 @@ module MX-ACCOUNTS-TEST
setStorage
(... account: Account:String
, key: Key:String
- , value: Value:MxWrappedValue
+ , value: Value:MxValue
) => .K
...
@@ -251,7 +242,7 @@ module MX-ACCOUNTS-TEST
setStorage
(... account: Account:String
, key: Key:String
- , value: Value:MxWrappedValue
+ , value: Value:MxValue
) => .K
...
@@ -262,6 +253,7 @@ module MX-ACCOUNTS-TEST
Key
Value
+ ...
[priority(100)]
diff --git a/parse-mx-rust-contract-test.sh b/parse-mx-rust-contract-test.sh
new file mode 100755
index 0000000..56499eb
--- /dev/null
+++ b/parse-mx-rust-contract-test.sh
@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+ --output kore \
+ --definition .build/mx-rust-contract-testing-kompiled \
+ --module MX-RUST-SYNTAX \
+ --sort MxRustTest \
+ $1
diff --git a/parse-mx-rust-contract.sh b/parse-mx-rust-contract.sh
new file mode 100755
index 0000000..4ec1a73
--- /dev/null
+++ b/parse-mx-rust-contract.sh
@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+ --output kore \
+ --definition .build/mx-rust-contract-testing-kompiled \
+ --module RUST-COMMON-SYNTAX \
+ --sort Crate \
+ $1
diff --git a/rust-semantics/expression.md b/rust-semantics/expression.md
index 7502c3f..0f59644 100644
--- a/rust-semantics/expression.md
+++ b/rust-semantics/expression.md
@@ -6,6 +6,7 @@ requires "expression/constants.md"
requires "expression/casts.md"
requires "expression/literals.md"
requires "expression/references.md"
+requires "expression/struct.md"
requires "expression/tools.md"
requires "expression/variables.md"
@@ -15,6 +16,7 @@ module RUST-EXPRESSION
imports private RUST-EXPRESSION-CONSTANTS
imports private RUST-EXPRESSION-LITERALS
imports private RUST-EXPRESSION-REFERENCES
+ imports private RUST-EXPRESSION-STRUCT
imports private RUST-EXPRESSION-TOOLS
imports private RUST-EXPRESSION-VARIABLES
imports private RUST-INTEGER-OPERATIONS
diff --git a/rust-semantics/expression/struct.md b/rust-semantics/expression/struct.md
new file mode 100644
index 0000000..1e3925b
--- /dev/null
+++ b/rust-semantics/expression/struct.md
@@ -0,0 +1,15 @@
+```k
+
+module RUST-EXPRESSION-STRUCT
+ imports COMMON-K-CELL
+ imports RUST-EXECUTION-CONFIGURATION
+ imports RUST-REPRESENTATION
+
+ rule
+ Rust#newStruct(P:TypePath, Fields:Map) => ptrValue(ptr(NVI), struct(P, Fields)) ...
+ VALUES:Map => VALUES[NVI <- struct(P, Fields)]
+ NVI:Int => NVI +Int 1
+
+endmodule
+
+```
diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
index 0ff511e..87c5b7f 100644
--- a/rust-semantics/representation.md
+++ b/rust-semantics/representation.md
@@ -73,6 +73,7 @@ module RUST-REPRESENTATION
, params: CallParamsList
)
[strict(3), result(ValueWithPtr)]
+ | "Rust#newStruct" "(" type:TypePath "," fields:Map ")"
syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError
@@ -96,6 +97,8 @@ module RUST-REPRESENTATION
syntax IntOrError ::= valueToInteger(Value) [function, total]
syntax ValueOrError ::= integerToValue(Int, Type) [function, total]
+ syntax String ::= IdentifierToString(Identifier) [function, total, hook(STRING.token2string)]
+
endmodule
```
diff --git a/rust-semantics/targets/preprocessing/rust.md b/rust-semantics/targets/preprocessing/rust.md
index 730f28d..d17c2f9 100644
--- a/rust-semantics/targets/preprocessing/rust.md
+++ b/rust-semantics/targets/preprocessing/rust.md
@@ -20,7 +20,11 @@ module RUST
imports private RUST-BOOL-OPERATIONS
imports private RUST-EXPRESSION-CONSTANTS
imports private RUST-PREPROCESSING
+ imports private RUST-REPRESENTATION
imports private RUST-RUNNING-CONFIGURATION
+
+ // Making a warning go away
+ rule isLocalVariable(_) => false
endmodule
```
diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
index ee6f3e8..0076655 100644
--- a/rust-semantics/test/execution.md
+++ b/rust-semantics/test/execution.md
@@ -23,15 +23,23 @@ module RUST-EXECUTION-TEST
imports private RUST-PREPROCESSING-CONFIGURATION
imports private RUST-REPRESENTATION
- rule E:ExecutionItem ; Es:ExecutionTest => E ~> Es
- rule .ExecutionTest => .K
+ rule Es:ExecutionTest => rustChainTest(Es)
+
+ syntax K ::= rustChainTest(ExecutionTest) [function, total]
+ rule rustChainTest(.ExecutionTest) => .K
+ rule rustChainTest(I:ExecutionItem ; Is:ExecutionTest) => I ~> rustChainTest(Is)
rule
- new P:TypePath => .K ...
- .List => ListItem(ptr(NVI)) ...
+
+ (.K => Rust#newStruct(P, .Map))
+ ~> new P:TypePath
+ ...
+
P
- VALUES:Map => VALUES[NVI <- struct(P, .Map)]
- NVI:Int => NVI +Int 1
+
+ rule
+ ptrValue(P:Ptr, _:Value) ~> new _:TypePath => .K ...
+ .List => ListItem(P) ...
rule
@@ -67,7 +75,7 @@ module RUST-EXECUTION-TEST
) => normalizedMethodCall(TraitName, MethodName, Args)
rule
- (V:PtrValue ~> return_value ; Es:ExecutionTest) => Es ...
+ (V:PtrValue ~> return_value) => .K ...
.List => ListItem(V) ...
rule
diff --git a/tests/mx-rust-contracts/contract-setup.1.run b/tests/mx-rust-contracts/contract-setup.1.run
new file mode 100644
index 0000000..95a03d8
--- /dev/null
+++ b/tests/mx-rust-contracts/contract-setup.1.run
@@ -0,0 +1,14 @@
+setCallee("Owner");
+
+push mxListValue();
+push mxStringValue("getMyStorage");
+push mxIntValue(0);
+push mxTransfersValue();
+push mxIntValue(0);
+push mxStringValue("TestContract");
+call 6 MX#managedExecuteOnDestContext;
+check_eq mxIntValue(0);
+
+push_return_value;
+check_eq mxIntValue(10)
+
diff --git a/tests/mx-rust-contracts/contract-setup.rs b/tests/mx-rust-contracts/contract-setup.rs
new file mode 100644
index 0000000..5483974
--- /dev/null
+++ b/tests/mx-rust-contracts/contract-setup.rs
@@ -0,0 +1,24 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use multiversx_sc::imports::*;
+
+#[multiversx_sc::contract]
+pub trait Storage {
+ #[view(noArg)]
+ #[storage_mapper("no_arg")]
+ fn my_storage(&self) -> SingleValueMapper;
+
+ #[init]
+ fn init(&self) {
+ self.my_storage().set_if_empty(BigUint::from(10))
+ }
+
+ #[upgrade]
+ fn upgrade(&self) {}
+
+ #[endpoint(getMyStorage)]
+ fn get_my_storage(&self) -> BigUint {
+ self.my_storage().get()
+ }
+}
diff --git a/tests/mx-rust/storage.rs b/tests/mx-rust/storage.rs
index 0b16596..f8ff529 100644
--- a/tests/mx-rust/storage.rs
+++ b/tests/mx-rust/storage.rs
@@ -24,10 +24,10 @@ pub trait Storage {
}
fn get_no_arg(&self) -> BigUint {
- self.no_arg_storage().get()
+ self.no_arg_storage().get()
}
fn set_no_arg_if_empty(&self, value: u64) {
- self.no_arg_storage().set_if_empty(BigUint::from(value))
- }
+ self.no_arg_storage().set_if_empty(BigUint::from(value))
+ }
}
diff --git a/tests/mx/biguint/add.mx b/tests/mx/biguint/add.mx
index 548c1ba..cd86d46 100644
--- a/tests/mx/biguint/add.mx
+++ b/tests/mx/biguint/add.mx
@@ -1,7 +1,9 @@
push mxIntValue(10);
call 1 MX#bigIntNew;
+push;
push mxIntValue(20);
call 1 MX#bigIntNew;
+push;
call 2 MX#bigIntAdd;
get_big_int;
check_eq mxIntValue(30)
diff --git a/tests/mx/biguint/div.mx b/tests/mx/biguint/div.mx
index 50c61eb..5c33b47 100644
--- a/tests/mx/biguint/div.mx
+++ b/tests/mx/biguint/div.mx
@@ -1,7 +1,9 @@
push mxIntValue(40);
call 1 MX#bigIntNew;
+push;
push mxIntValue(500);
call 1 MX#bigIntNew;
+push;
call 2 MX#bigIntDiv;
get_big_int;
check_eq mxIntValue(12)
diff --git a/tests/mx/biguint/eq.mx b/tests/mx/biguint/eq.mx
index c811ec1..79800c7 100644
--- a/tests/mx/biguint/eq.mx
+++ b/tests/mx/biguint/eq.mx
@@ -1,6 +1,8 @@
push mxIntValue(20);
call 1 MX#bigIntNew;
+push;
push mxIntValue(20);
call 1 MX#bigIntNew;
+push;
call 2 MX#bigIntCmp;
check_eq mxIntValue(0)
diff --git a/tests/mx/biguint/gt.mx b/tests/mx/biguint/gt.mx
index a18aff7..24fe5e8 100644
--- a/tests/mx/biguint/gt.mx
+++ b/tests/mx/biguint/gt.mx
@@ -1,6 +1,8 @@
push mxIntValue(10);
call 1 MX#bigIntNew;
+push;
push mxIntValue(20);
call 1 MX#bigIntNew;
+push;
call 2 MX#bigIntCmp;
check_eq mxIntValue(1)
diff --git a/tests/mx/biguint/lt.mx b/tests/mx/biguint/lt.mx
index ca2859b..284b1b0 100644
--- a/tests/mx/biguint/lt.mx
+++ b/tests/mx/biguint/lt.mx
@@ -1,6 +1,8 @@
push mxIntValue(20);
call 1 MX#bigIntNew;
+push;
push mxIntValue(10);
call 1 MX#bigIntNew;
+push;
call 2 MX#bigIntCmp;
check_eq mxIntValue(-1)
diff --git a/tests/mx/biguint/mul.mx b/tests/mx/biguint/mul.mx
index f65ece6..7e999aa 100644
--- a/tests/mx/biguint/mul.mx
+++ b/tests/mx/biguint/mul.mx
@@ -1,7 +1,9 @@
push mxIntValue(40);
call 1 MX#bigIntNew;
+push;
push mxIntValue(50);
call 1 MX#bigIntNew;
+push;
call 2 MX#bigIntMul;
get_big_int;
check_eq mxIntValue(2000)
diff --git a/tests/mx/biguint/sub.mx b/tests/mx/biguint/sub.mx
index 3365431..63df829 100644
--- a/tests/mx/biguint/sub.mx
+++ b/tests/mx/biguint/sub.mx
@@ -1,7 +1,9 @@
push mxIntValue(40);
call 1 MX#bigIntNew;
+push;
push mxIntValue(50);
call 1 MX#bigIntNew;
+push;
call 2 MX#bigIntSub;
get_big_int;
check_eq mxIntValue(10)
diff --git a/tests/mx/storage/get-empty-storage.mx b/tests/mx/storage/get-empty-storage.mx
index d008fe2..d2c210d 100644
--- a/tests/mx/storage/get-empty-storage.mx
+++ b/tests/mx/storage/get-empty-storage.mx
@@ -6,4 +6,4 @@ push mxStringValue("MyKey");
call 2 MX#storageLoad;
push_store_data;
check_eq mxIntValue(12);
-check_eq mxWrappedEmpty
+check_eq mxEmptyValue
diff --git a/tests/mx/storage/get-existing-storage.mx b/tests/mx/storage/get-existing-storage.mx
index 23a3457..baa66c0 100644
--- a/tests/mx/storage/get-existing-storage.mx
+++ b/tests/mx/storage/get-existing-storage.mx
@@ -1,10 +1,10 @@
addAccount("Owner");
setCallee("Owner");
-setStorage("Owner", "MyKey", wrappedMx(mxStringValue("Hello")));
+setStorage("Owner", "MyKey", mxStringValue("Hello"));
push mxIntValue(12);
push mxStringValue("MyKey");
call 2 MX#storageLoad;
push_store_data;
check_eq mxIntValue(12);
-check_eq wrappedMx(mxStringValue("Hello"))
+check_eq mxStringValue("Hello")
diff --git a/tests/mx/storage/set-empty-storage.mx b/tests/mx/storage/set-empty-storage.mx
index be6ff6f..fb51a20 100644
--- a/tests/mx/storage/set-empty-storage.mx
+++ b/tests/mx/storage/set-empty-storage.mx
@@ -1,7 +1,7 @@
addAccount("Owner");
setCallee("Owner");
-push wrappedMx(mxStringValue("Hello"));
+push mxStringValue("Hello");
push mxStringValue("MyKey");
call 2 MX#storageStore;
@@ -10,4 +10,4 @@ push mxStringValue("MyKey");
call 2 MX#storageLoad;
push_store_data;
check_eq mxIntValue(12);
-check_eq wrappedMx(mxStringValue("Hello"))
+check_eq mxStringValue("Hello")
diff --git a/tests/mx/storage/set-existing-storage.mx b/tests/mx/storage/set-existing-storage.mx
index 58be307..7025490 100644
--- a/tests/mx/storage/set-existing-storage.mx
+++ b/tests/mx/storage/set-existing-storage.mx
@@ -1,8 +1,8 @@
addAccount("Owner");
setCallee("Owner");
-setStorage("Owner", "MyKey", wrappedMx(mxStringValue("Hello")));
+setStorage("Owner", "MyKey", mxStringValue("Hello"));
-push wrappedMx(mxStringValue("World"));
+push mxStringValue("World");
push mxStringValue("MyKey");
call 2 MX#storageStore;
@@ -11,4 +11,4 @@ push mxStringValue("MyKey");
call 2 MX#storageLoad;
push_store_data;
check_eq mxIntValue(12);
-check_eq wrappedMx(mxStringValue("World"))
+check_eq mxStringValue("World")