From 5783250721c734fe0e8684fe38db5ad274397fdc Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 11 Sep 2024 18:45:22 +0300 Subject: [PATCH] Contract initialization without args and simple calls --- Makefile | 46 +++++++- mx-rust-semantics/main/calls.md | 9 ++ mx-rust-semantics/main/calls/configuration.md | 17 +++ .../main/calls/implementation.md | 92 +++++++++++++++ mx-rust-semantics/main/configuration.md | 3 + mx-rust-semantics/main/glue.md | 84 ++++++++------ mx-rust-semantics/main/modules/biguint.md | 30 ++++- mx-rust-semantics/main/modules/storage.md | 10 +- mx-rust-semantics/main/mx-rust-common.md | 2 + .../main/preprocessing/methods.md | 85 ++++++++++++-- mx-rust-semantics/main/representation.md | 14 ++- mx-rust-semantics/setup/mx.md | 107 ++++++++++++++++++ .../targets/contract-testing/configuration.md | 38 +++++++ .../targets/contract-testing/mx-rust.md | 35 ++++++ mx-rust-semantics/targets/testing/mx-rust.md | 2 + mx-rust-semantics/test/execution.md | 24 ++-- mx-semantics/main/accounts/configuration.md | 2 +- mx-semantics/main/accounts/storage-hooks.md | 2 +- mx-semantics/main/accounts/storage-tools.md | 8 +- mx-semantics/main/biguint/tools.md | 4 + mx-semantics/main/calls/tools.md | 26 ++--- mx-semantics/main/syntax.md | 19 +++- mx-semantics/main/tools.md | 3 + mx-semantics/setup/setup.md | 54 +++++++++ mx-semantics/targets/testing/mx.md | 2 + mx-semantics/test/execution.md | 48 ++++---- parse-mx-rust-contract-test.sh | 8 ++ parse-mx-rust-contract.sh | 8 ++ rust-semantics/expression.md | 2 + rust-semantics/expression/struct.md | 15 +++ rust-semantics/representation.md | 3 + rust-semantics/targets/preprocessing/rust.md | 4 + rust-semantics/test/execution.md | 22 ++-- tests/mx-rust-contracts/contract-setup.1.run | 14 +++ tests/mx-rust-contracts/contract-setup.rs | 24 ++++ tests/mx-rust/storage.rs | 6 +- tests/mx/biguint/add.mx | 2 + tests/mx/biguint/div.mx | 2 + tests/mx/biguint/eq.mx | 2 + tests/mx/biguint/gt.mx | 2 + tests/mx/biguint/lt.mx | 2 + tests/mx/biguint/mul.mx | 2 + tests/mx/biguint/sub.mx | 2 + tests/mx/storage/get-empty-storage.mx | 2 +- tests/mx/storage/get-existing-storage.mx | 4 +- tests/mx/storage/set-empty-storage.mx | 4 +- tests/mx/storage/set-existing-storage.mx | 6 +- 47 files changed, 762 insertions(+), 140 deletions(-) create mode 100644 mx-rust-semantics/main/calls.md create mode 100644 mx-rust-semantics/main/calls/configuration.md create mode 100644 mx-rust-semantics/main/calls/implementation.md create mode 100644 mx-rust-semantics/setup/mx.md create mode 100644 mx-rust-semantics/targets/contract-testing/configuration.md create mode 100644 mx-rust-semantics/targets/contract-testing/mx-rust.md create mode 100644 mx-semantics/setup/setup.md create mode 100755 parse-mx-rust-contract-test.sh create mode 100755 parse-mx-rust-contract.sh create mode 100644 rust-semantics/expression/struct.md create mode 100644 tests/mx-rust-contracts/contract-setup.1.run create mode 100644 tests/mx-rust-contracts/contract-setup.rs 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")