diff --git a/Makefile b/Makefile index 954bdd4..b61e3e1 100644 --- a/Makefile +++ b/Makefile @@ -45,7 +45,14 @@ MX_RUST_CONTRACT_TESTING_OUTPUT_DIR ::= .build/mx-rust-contracts/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 +MX_RUST_TWO_CONTRACTS_TESTING_KOMPILED ::= .build/mx-rust-two-contracts-testing-kompiled +MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP ::= $(MX_RUST_TWO_CONTRACTS_TESTING_KOMPILED)/timestamp +MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR ::= tests/mx-rust-two-contracts +MX_RUST_TWO_CONTRACTS_TESTING_OUTPUT_DIR ::= .build/mx-rust-two-contracts/output +MX_RUST_TWO_CONTRACTS_TESTING_INPUTS ::= $(wildcard $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/*.run) +MX_RUST_TWO_CONTRACTS_TESTING_OUTPUTS ::= $(patsubst $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/%,$(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_RUST_TWO_CONTRACTS_TESTING_INPUTS)) + +.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test clean: rm -r .build @@ -55,9 +62,10 @@ build: $(RUST_PREPROCESSING_TIMESTAMP) \ $(MX_TESTING_TIMESTAMP) \ $(MX_RUST_TIMESTAMP) \ $(MX_RUST_TESTING_TIMESTAMP) \ - $(MX_RUST_CONTRACT_TESTING_TIMESTAMP) + $(MX_RUST_CONTRACT_TESTING_TIMESTAMP) \ + $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP) -test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test +test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test syntax-test: $(SYNTAX_OUTPUTS) @@ -71,6 +79,8 @@ mx-rust-test: $(MX_RUST_TESTING_OUTPUTS) mx-rust-contract-test: $(MX_RUST_CONTRACT_TESTING_OUTPUTS) +mx-rust-two-contracts-test: $(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUTS) + $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(RUST_PREPROCESSING_KOMPILED) @@ -110,6 +120,14 @@ $(MX_RUST_CONTRACT_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FI -I . \ --debug +$(MX_RUST_TWO_CONTRACTS_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_TWO_CONTRACTS_TESTING_KOMPILED) + $$(which kompile) mx-rust-semantics/targets/two-contracts-testing/mx-rust.md \ + -o $(MX_RUST_TWO_CONTRACTS_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 $@ @@ -196,3 +214,31 @@ $(MX_RUST_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ -pARGS=$(CURDIR)/parsers/args-mx-rust-contract.sh cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" mv -f $@.tmp $@ + +$(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ + $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/%.run \ + $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/%.1.rs \ + $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/%.1.args \ + $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/%.2.rs \ + $(MX_RUST_TWO_CONTRACTS_TESTING_INPUT_DIR)/%.2.args \ + $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP) \ + parsers/contract-mx-rust-two-contracts.sh \ + parsers/args-mx-rust-two-contracts.sh \ + parsers/test-mx-rust-two-contracts.sh + mkdir -p $(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUT_DIR) + krun \ + --definition $(MX_RUST_TWO_CONTRACTS_TESTING_KOMPILED) \ + --output kore \ + --output-file $@.tmp \ + -cPGM1='$(shell cat $(patsubst %.run,%.1.rs,$<))' \ + -pPGM1=$(CURDIR)/parsers/contract-mx-rust-two-contracts.sh \ + -cPGM2='$(shell cat $(patsubst %.run,%.2.rs,$<))' \ + -pPGM2=$(CURDIR)/parsers/contract-mx-rust-two-contracts.sh \ + -cTEST='$(shell cat $<)' \ + -pTEST=$(CURDIR)/parsers/test-mx-rust-two-contracts.sh \ + -cARGS1='$(shell cat $(patsubst %.run,%.1.args,$<))' \ + -pARGS1=$(CURDIR)/parsers/args-mx-rust-two-contracts.sh \ + -cARGS2='$(shell cat $(patsubst %.run,%.2.args,$<))' \ + -pARGS2=$(CURDIR)/parsers/args-mx-rust-two-contracts.sh + cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" + mv -f $@.tmp $@ diff --git a/mx-rust-semantics/main/expression.md b/mx-rust-semantics/main/expression.md index 08301ed..c1fe286 100644 --- a/mx-rust-semantics/main/expression.md +++ b/mx-rust-semantics/main/expression.md @@ -1,15 +1,17 @@ ```k requires "expression/mx-to-rust.md" +requires "expression/raw-value.md" requires "expression/rust-to-mx.md" requires "expression/strings.md" requires "expression/struct.md" module MX-RUST-EXPRESSION imports private MX-RUST-EXPRESSION-MX-TO-RUST + imports private MX-RUST-EXPRESSION-RAW-VALUE imports private MX-RUST-EXPRESSION-RUST-TO-MX imports private MX-RUST-EXPRESSION-STRINGS imports private MX-RUST-EXPRESSION-STRUCT endmodule -``` \ No newline at end of file +``` diff --git a/mx-rust-semantics/main/expression/raw-value.md b/mx-rust-semantics/main/expression/raw-value.md new file mode 100644 index 0000000..0f5a52d --- /dev/null +++ b/mx-rust-semantics/main/expression/raw-value.md @@ -0,0 +1,10 @@ +```k + +module MX-RUST-EXPRESSION-RAW-VALUE + imports private MX-RUST-REPRESENTATION + + rule rawValue(V:Value) => mxRustNewValue(V) + +endmodule + +``` diff --git a/mx-rust-semantics/main/modules.md b/mx-rust-semantics/main/modules.md index fa8e6d6..386d74b 100644 --- a/mx-rust-semantics/main/modules.md +++ b/mx-rust-semantics/main/modules.md @@ -2,12 +2,14 @@ requires "modules/address.md" requires "modules/biguint.md" -requires "modules/storage.md" +requires "modules/hooks.md" requires "modules/proxy.md" +requires "modules/storage.md" module MX-RUST-MODULES imports private MX-RUST-MODULES-ADDRESS imports private MX-RUST-MODULES-BIGUINT + imports private MX-RUST-MODULES-HOOKS imports private MX-RUST-MODULES-PROXY imports private MX-RUST-MODULES-STORAGE endmodule diff --git a/mx-rust-semantics/main/modules/hooks.md b/mx-rust-semantics/main/modules/hooks.md new file mode 100644 index 0000000..2a2da4d --- /dev/null +++ b/mx-rust-semantics/main/modules/hooks.md @@ -0,0 +1,30 @@ +```k + +module MX-RUST-MODULES-HOOKS + imports private COMMON-K-CELL + imports private MX-COMMON-SYNTAX + imports private MX-RUST-REPRESENTATION + imports private RUST-EXECUTION-CONFIGURATION + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + + rule + + normalizedMethodCall + ( #token("MxRust#Hooks", "Identifier"):Identifier + , #token("MxRust#loadMxReturnValue", "Identifier"):Identifier + , ( ptr(ReturnTypeId:Int) + , .PtrList + ) + ) + => MX#popLastReturnValue(.MxValueList) ~> mxToRustTyped(T) + ... + + + ReturnTypeId |-> rustType(T) + ... + + +endmodule + +``` diff --git a/mx-rust-semantics/main/modules/proxy.md b/mx-rust-semantics/main/modules/proxy.md index 2530c8f..d048867 100644 --- a/mx-rust-semantics/main/modules/proxy.md +++ b/mx-rust-semantics/main/modules/proxy.md @@ -66,6 +66,28 @@ module MX-RUST-MODULES-PROXY ... + rule + + normalizedMethodCall + ( #token("MxRust#Proxy", "Identifier"):Identifier + => ProxyType + , MethodName:Identifier + , (ptr(SelfId:Int) , _Params:PtrList) + ) + ... + + + SelfId |-> struct + ( _ + , #token("proxy_type", "Identifier"):Identifier |-> ProxyTypeId:Int + _:Map + ) + ProxyTypeId |-> rustType(ProxyType:TypePath) + ... + + ProxyType + MethodName + syntax MxOrRustValueOrInstruction ::= MxOrRustValue | MxRustInstruction syntax RustMxInstruction ::= rustMxManagedExecuteOnDestContext diff --git a/mx-rust-semantics/main/preprocessing.md b/mx-rust-semantics/main/preprocessing.md index 812d0c0..53598b5 100644 --- a/mx-rust-semantics/main/preprocessing.md +++ b/mx-rust-semantics/main/preprocessing.md @@ -1,10 +1,12 @@ ```k requires "preprocessing/methods.md" +requires "preprocessing/proxy.md" requires "preprocessing/traits.md" module MX-RUST-PREPROCESSING imports private MX-RUST-PREPROCESSING-METHODS + imports private MX-RUST-PREPROCESSING-PROXY imports private MX-RUST-PREPROCESSING-TRAITS endmodule diff --git a/mx-rust-semantics/main/preprocessing/configuration.md b/mx-rust-semantics/main/preprocessing/configuration.md index 1027410..5d66a39 100644 --- a/mx-rust-semantics/main/preprocessing/configuration.md +++ b/mx-rust-semantics/main/preprocessing/configuration.md @@ -3,11 +3,13 @@ module MX-RUST-PREPROCESSED-CONFIGURATION imports MX-RUST-PREPROCESSED-CONTRACT-TRAIT-CONFIGURATION imports MX-RUST-PREPROCESSED-ENDPOINTS-CONFIGURATION + imports MX-RUST-PREPROCESSED-PROXIES-CONFIGURATION configuration + endmodule @@ -18,6 +20,18 @@ module MX-RUST-PREPROCESSED-CONTRACT-TRAIT-CONFIGURATION (#token("no#path", "Identifier"):Identifier):TypePath // String to Identifier endmodule +module MX-RUST-PREPROCESSED-PROXIES-CONFIGURATION + imports RUST-SHARED-SYNTAX + + configuration + + + (#token("no#path", "Identifier"):Identifier):TypePath + #token("no#path", "Identifier"):Identifier:TypePath + + +endmodule + module MX-RUST-PREPROCESSED-ENDPOINTS-CONFIGURATION imports MAP diff --git a/mx-rust-semantics/main/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md index b606643..e3beff1 100644 --- a/mx-rust-semantics/main/preprocessing/methods.md +++ b/mx-rust-semantics/main/preprocessing/methods.md @@ -4,8 +4,8 @@ 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-PREPROCESSED-ENDPOINTS-CONFIGURATION + imports private MX-RUST-PREPROCESSED-PROXIES-CONFIGURATION imports private MX-RUST-REPRESENTATION imports private RUST-PREPROCESSING-CONFIGURATION imports private RUST-REPRESENTATION @@ -14,16 +14,42 @@ module MX-RUST-PREPROCESSING-METHODS syntax Identifier ::= "storage_mapper" [token] - syntax MxRustInstruction ::= mxRustPreprocessMethods(trait: TypePath, methodNames: List) - | mxRustPreprocessMethod(trait: TypePath, methodName: Identifier) - | mxRustPreprocessStorage(trait: TypePath, methodName: Identifier) - | mxRustPreprocessEndpoint(trait: TypePath, methodName: Identifier) + syntax MxRustInstruction ::= mxRustPreprocessMethods + ( trait: TypePath + , traitType: TraitType + , methodNames: List + ) + | mxRustPreprocessMethod + ( trait: TypePath + , traitType: TraitType + , methodName: Identifier + ) + | mxRustPreprocessStorage + ( trait: TypePath + , traitType: TraitType + , methodName: Identifier + ) + | mxRustPreprocessEndpoint + ( trait: TypePath + , traitType: TraitType + , methodName: Identifier + ) + | mxRustPreprocessProxyMethod + ( trait: TypePath + , traitType: TraitType + , methodName: Identifier + ) | addStorageMethodBody ( trait: TypePath , methodName: Identifier , storageName:String , mapperValueType:MxRustTypeOrError ) + | addProxyMethodBody + ( trait: TypePath + , methodName: Identifier + , proxyModule: TypePathOrError + ) | mxRustAddEndpointMapping ( trait: TypePath , methodName: Identifier @@ -31,24 +57,30 @@ module MX-RUST-PREPROCESSING-METHODS ) rule - mxRustPreprocessMethods(T:TypePath) - => mxRustPreprocessMethods(T, MethodNames) + mxRustPreprocessMethods(T:TypePath, TType:TraitType) + => mxRustPreprocessMethods(T, TType, MethodNames) ... T MethodNames:List - rule mxRustPreprocessMethods(_:TypePath, .List) => .K - rule mxRustPreprocessMethods(T:TypePath, ListItem(MethodName:Identifier) Names:List) - => mxRustPreprocessMethod(T, MethodName) ~> mxRustPreprocessMethods(T, Names) + rule mxRustPreprocessMethods(_:TypePath, contract, .List) => .K + rule mxRustPreprocessMethods(Trait:TypePath, proxy, .List) => rustMxAddProxyMethods(Trait) + + rule mxRustPreprocessMethods + (T:TypePath, TType:TraitType, ListItem(MethodName:Identifier) Names:List) + => mxRustPreprocessMethod(T, TType, MethodName) + ~> mxRustPreprocessMethods(T, TType, Names) - rule mxRustPreprocessMethod(Trait:TypePath, Method:Identifier) - => mxRustPreprocessStorage(Trait, Method) - ~> mxRustPreprocessEndpoint(Trait, Method) + rule mxRustPreprocessMethod(Trait:TypePath, TType:TraitType, Method:Identifier) + => mxRustPreprocessStorage(Trait, TType, Method) + ~> mxRustPreprocessEndpoint(Trait, TType, Method) + ~> mxRustPreprocessProxyMethod(Trait, TType, Method) + rule mxRustPreprocessStorage(_Trait:TypePath, proxy, _Method:Identifier) => .K rule - mxRustPreprocessStorage(Trait:TypePath, Method:Identifier) + mxRustPreprocessStorage(Trait:TypePath, contract, Method:Identifier) => addStorageMethodBody (... trait: Trait, methodName: Method , storageName: getStorageName(Atts) @@ -65,12 +97,29 @@ module MX-RUST-PREPROCESSING-METHODS requires getStorageName(Atts) =/=K "" [priority(50)] - rule mxRustPreprocessStorage(_Trait:TypePath, _Method:Identifier) => .K + rule mxRustPreprocessStorage(_Trait:TypePath, contract, _Method:Identifier) => .K [priority(100)] rule - mxRustPreprocessEndpoint(Trait:TypePath, Method:Identifier) + mxRustPreprocessEndpoint(Trait:TypePath, proxy, Method:Identifier) + => .K + ... + + Trait + Method + + empty + => block(buildProxyEndpointMethod(Params, getEndpointName(Atts, Method), rustType(ReturnType))) + + Atts:OuterAttributes + Params:NormalizedFunctionParameterList + ReturnType => #token("MxRust#Proxy", "Identifier") + requires getEndpointName(Atts, Method) =/=K "" + [priority(50)] + rule + + mxRustPreprocessEndpoint(Trait:TypePath, contract, Method:Identifier) => mxRustAddEndpointMapping (... trait: Trait, methodName: Method , endpointName: getEndpointName(Atts, Method) @@ -82,9 +131,36 @@ module MX-RUST-PREPROCESSING-METHODS Atts:OuterAttributes requires getEndpointName(Atts, Method) =/=K "" [priority(50)] - rule mxRustPreprocessEndpoint(_Trait:TypePath, _Method:Identifier) => .K + rule mxRustPreprocessEndpoint(_Trait:TypePath, contract, _Method:Identifier) => .K [priority(100)] + rule mxRustPreprocessProxyMethod(_Trait:TypePath, proxy, _Method:Identifier) => .K + rule + + mxRustPreprocessProxyMethod(Trait:TypePath, contract, Method:Identifier) + => addProxyMethodBody + (... trait: Trait, methodName: Method + , proxyModule: parentTypePath(ReturnType) + ) + ... + + Trait + Method + empty + Atts:OuterAttributes + ReturnType:TypePath + requires isProxyMethod(Atts) + rule + + mxRustPreprocessProxyMethod(Trait:TypePath, contract, Method:Identifier) + => .K + ... + + Trait + Method + Atts:OuterAttributes + requires notBool isProxyMethod(Atts) + rule mxRustAddEndpointMapping @@ -112,6 +188,27 @@ module MX-RUST-PREPROCESSING-METHODS empty => block(buildStorageMethodBody(Params, StorageName, MapperValueType)) + rule + + addProxyMethodBody + (... trait: Trait:TypePath, methodName: Method:Identifier + , proxyModule: ProxyModule:TypePath + ) => .K + ... + + Trait + Method + + SelfName:SelfSort : _ + , AddressName:Identifier : #token("ManagedAddress", "Identifier") + , .NormalizedFunctionParameterList + + + empty => block(buildProxyMethodBody(SelfName, AddressName, ProxyTrait)) + + ProxyModule + ProxyTrait:TypePath + syntax String ::= getStorageName(atts:OuterAttributes) [function, total] rule getStorageName() => "" rule getStorageName(.NonEmptyOuterAttributes) => "" @@ -151,6 +248,61 @@ module MX-RUST-PREPROCESSING-METHODS => getEndpointName(Atts, Default) [owise] + syntax Bool ::= isProxyMethod(atts:OuterAttributes) [function, total] + rule isProxyMethod() => false + rule isProxyMethod(.NonEmptyOuterAttributes) => false + rule isProxyMethod + ( (#[ #token("proxy", "Identifier") :: .SimplePathList]) + _:NonEmptyOuterAttributes + ) => true + rule isProxyMethod(_:OuterAttribute Atts:NonEmptyOuterAttributes) + => isProxyMethod(Atts) + [owise] + + syntax BlockExpression ::= buildProxyEndpointMethod + ( params: NormalizedFunctionParameterList + , endpointName: String + , returnType: MxRustType + ) [function] + rule buildProxyEndpointMethod + (... params: S:SelfSort : _ , Params:NormalizedFunctionParameterList + , endpointName: Name + , returnType: ReturnType + ) + => { .InnerAttributes + S . #token("endpoint_name", "Identifier") = Name; + S . #token("args", "Identifier") = + (paramsToMaybeTupleElements(Params)):TupleExpression; + S . #token("return_type", "Identifier") = ptrValue(null, ReturnType); + S + } + + // TODO: Move this to the Rust semantics + syntax MaybeTupleElements ::= paramsToMaybeTupleElements(NormalizedFunctionParameterList) + [function, total] + rule paramsToMaybeTupleElements(.NormalizedFunctionParameterList) => `noTupleElements`(.KList) + rule paramsToMaybeTupleElements(Name:Identifier : _ , .NormalizedFunctionParameterList) + => Name , + rule paramsToMaybeTupleElements + ( Name:Identifier : _ + , N:NormalizedFunctionParameter + , Ns:NormalizedFunctionParameterList + ) + => Name , paramsToTupleElementsNoEndComma(N , Ns) + rule paramsToMaybeTupleElements(P , Ps:NormalizedFunctionParameterList) + => error("Unexpected param in paramsToMaybeTupleElements", ListItem(P) ListItem(Ps)) , + [owise] + + syntax TupleElementsNoEndComma ::= paramsToTupleElementsNoEndComma(NormalizedFunctionParameterList) + [function, total] + rule paramsToTupleElementsNoEndComma(.NormalizedFunctionParameterList) + => .TupleElementsNoEndComma + rule paramsToTupleElementsNoEndComma(Name:Identifier : _ , Ps:NormalizedFunctionParameterList) + => Name , paramsToTupleElementsNoEndComma(Ps) + rule paramsToTupleElementsNoEndComma(P , Ps:NormalizedFunctionParameterList) + => error("Unexpected param in paramsToTupleElementsNoEndComma", ListItem(P)) + , paramsToTupleElementsNoEndComma(Ps) + syntax BlockExpression ::= buildStorageMethodBody ( params: NormalizedFunctionParameterList , storageName: String @@ -184,6 +336,26 @@ module MX-RUST-PREPROCESSING-METHODS [owise] rule getMapperValueType(#token("BigUint", "Identifier") #as T:Type) => rustType(T) + + syntax BlockExpression ::= buildProxyMethodBody + ( selfName: SelfSort + , addressName: Identifier + , proxyTrait: TypePath + ) [function] + rule buildProxyMethodBody + (... selfName: _SelfName:SelfSort + , addressName: AddressName:Identifier + , proxyTrait: ProxyTrait:TypePath + ) + => { .InnerAttributes + #token("MxRust#Proxy", "Identifier"):Identifier + :: #token("new", "Identifier"):PathIdentSegment + ( AddressName + , rawValue(rustType(ProxyTrait)) + , .CallParamsList + ) + } + endmodule ``` diff --git a/mx-rust-semantics/main/preprocessing/proxy.md b/mx-rust-semantics/main/preprocessing/proxy.md new file mode 100644 index 0000000..b738c64 --- /dev/null +++ b/mx-rust-semantics/main/preprocessing/proxy.md @@ -0,0 +1,61 @@ +```k + +module MX-RUST-PREPROCESSING-PROXY + imports COMMON-K-CELL + imports MX-RUST-REPRESENTATION + imports RUST-PREPROCESSING-CONFIGURATION + + rule + + rustMxAddProxyMethods(Trait:TypePath) + => error + ( "execute_on_dest_context already exists for trait" + , ListItem(Trait) + ) + ... + + Trait + #token("execute_on_dest_context", "Identifier") + [priority(50)] + + rule + + rustMxAddProxyMethods(Trait:TypePath) + => .K + ... + + Trait + ( .Bag + => + #token("execute_on_dest_context", "Identifier") + self : $selftype , .NormalizedFunctionParameterList + #token("MxRust#CallReturnType", "Identifier") + + block({ + .InnerAttributes + ( + ( + ( #token("MxRust#Proxy", "Identifier") + :: (#token("MxRust#execute_on_dest_context", "Identifier"):PathExprSegment) + :: .PathExprSegments + ) + ( self, .CallParamsList ) + ):Expression; + ( + ( #token("MxRust#Hooks", "Identifier") + :: (#token("MxRust#loadMxReturnValue", "Identifier"):PathExprSegment) + :: .PathExprSegments + ) + ( self . #token("return_type", "Identifier"), .CallParamsList ) + ):Expression + ):Statements + }) + + `emptyOuterAttributes`(.KList):OuterAttributes + + ) + [priority(100)] + +endmodule + +``` diff --git a/mx-rust-semantics/main/preprocessing/traits.md b/mx-rust-semantics/main/preprocessing/traits.md index 7c561da..9babce8 100644 --- a/mx-rust-semantics/main/preprocessing/traits.md +++ b/mx-rust-semantics/main/preprocessing/traits.md @@ -4,14 +4,17 @@ module MX-RUST-PREPROCESSING-TRAITS imports private COMMON-K-CELL imports private LIST imports private MX-RUST-PREPROCESSED-CONTRACT-TRAIT-CONFIGURATION + imports private MX-RUST-PREPROCESSED-PROXIES-CONFIGURATION imports private MX-RUST-REPRESENTATION imports private RUST-PREPROCESSING-CONFIGURATION + imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX syntax MxRustInstruction ::= mxRustPreprocessAddTraits(List) | mxRustPreprocessAddTrait(TypePath) | mxRustPreprocessTraits(List) | mxRustPreprocessTrait(TypePath) + | mxRustPreprocessAddProxy(TypePathOrError, TypePath) rule @@ -25,6 +28,10 @@ module MX-RUST-PREPROCESSING-TRAITS rule mxRustPreprocessAddTraits(ListItem(Trait:TypePath) Traits:List) => mxRustPreprocessAddTrait(Trait) ~> mxRustPreprocessAddTraits(Traits) + rule mxRustPreprocessTraits(.List) => .K + rule mxRustPreprocessTraits(ListItem(Trait:TypePath) Traits:List) + => mxRustPreprocessTrait(Trait) ~> mxRustPreprocessTraits(Traits) + rule mxRustPreprocessAddTrait(Trait:TypePath) => .K @@ -39,12 +46,64 @@ module MX-RUST-PREPROCESSING-TRAITS .NonEmptyOuterAttributes _ => Trait + rule + + mxRustPreprocessAddTrait(Trait:TypePath) + => mxRustPreprocessAddProxy(parentTypePath(Trait), Trait) + ... + + Trait + + #[ #token("multiversx_sc", "Identifier") + :: #token("proxy", "Identifier") + :: .SimplePathList + ] + .NonEmptyOuterAttributes + - rule mxRustPreprocessTraits(.List) => .K - rule mxRustPreprocessTraits(ListItem(Trait:TypePath) Traits:List) - => mxRustPreprocessTrait(Trait) ~> mxRustPreprocessTraits(Traits) + rule + + mxRustPreprocessTrait(Trait:TypePath) + => mxRustPreprocessMethods(Trait, contract) + ... + + Trait + + #[ #token("multiversx_sc", "Identifier") + :: #token("contract", "Identifier") + :: .SimplePathList + ] + .NonEmptyOuterAttributes + + rule + + mxRustPreprocessTrait(Trait:TypePath) + => mxRustPreprocessMethods(Trait, proxy) + ... + + Trait + + #[ #token("multiversx_sc", "Identifier") + :: #token("proxy", "Identifier") + :: .SimplePathList + ] + .NonEmptyOuterAttributes + - rule mxRustPreprocessTrait(Trait:TypePath) => mxRustPreprocessMethods(Trait) + rule + + mxRustPreprocessAddProxy(Module:TypePath, Trait:TypePath) + => .K + ... + + + .Bag + => + Module + Trait + + ... + endmodule ``` diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md index 130f363..c28c7a1 100644 --- a/mx-rust-semantics/main/representation.md +++ b/mx-rust-semantics/main/representation.md @@ -1,13 +1,15 @@ ```k module MX-RUST-REPRESENTATION + imports MX-RUST-REPRESENTATION-CONVERSIONS imports MX-COMMON-SYNTAX imports MX-RUST-REPRESENTATION-CONVERSIONS imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX syntax MxRustInstruction ::= "mxRustPreprocessTraits" - | mxRustPreprocessMethods(TypePath) + | mxRustPreprocessMethods(TypePath, TraitType) + | rustMxAddProxyMethods(TypePath) | mxRustCreateAccount(String) | mxRustCreateContract ( owner: String @@ -23,17 +25,19 @@ module MX-RUST-REPRESENTATION | rustValuesToMx(ValueList, MxValueList) | mxRustLoadPtr(Int) | mxRustGetBigIntFromStruct(Value) + | mxRustGetStringFromId(Int) | mxRustNewStruct(MxRustStructType, CallParamsList) [strict(2), result(ValueWithPtr)] + syntax TraitType ::= "contract" | "proxy" syntax MxRustType ::= "noType" | rustType(Type) syntax MxRustTypeOrError ::= MxRustType | SemanticsError syntax Value ::= MxRustType - syntax SemanticsError ::= unknownMxRustType(GenericArg) - syntax Expression ::= concatString(Expression, Expression) [seqstrict] | toString(Expression) [strict] + | rawValue(Value) + | SemanticsError // TODO: Remove. syntax MxValue ::= rustDestination(Int, MxRustType) diff --git a/mx-rust-semantics/setup/mx.md b/mx-rust-semantics/setup/mx.md index 478e988..401a3ee 100644 --- a/mx-rust-semantics/setup/mx.md +++ b/mx-rust-semantics/setup/mx.md @@ -27,7 +27,8 @@ module MX-RUST-SETUP-MX , code: Code:Crate , args: Args:MxValueList ) - => crateParser(Code) + => MxRust#clearPreprocessed + ~> crateParser(Code) ~> mxRustPreprocessTraits ~> MxRust#addAccountWithPreprocessedCode (... owner: Owner diff --git a/mx-rust-semantics/targets/two-contracts-testing/configuration.md b/mx-rust-semantics/targets/two-contracts-testing/configuration.md new file mode 100644 index 0000000..bbed2a2 --- /dev/null +++ b/mx-rust-semantics/targets/two-contracts-testing/configuration.md @@ -0,0 +1,29 @@ +```k + +module COMMON-K-CELL + imports MX-RUST-REPRESENTATION + imports RUST-SHARED-SYNTAX + imports STRING + + syntax MxRustTest + + configuration + + mxRustCreateAccount("Owner") + ~> mxRustCreateContract + (... owner: "Owner" + , contractAccount: "TestContract1" + , code: $PGM1:Crate + , args: $ARGS1:MxValueList + ) + ~> mxRustCreateContract + (... owner: "Owner" + , contractAccount: "TestContract2" + , code: $PGM2:Crate + , args: $ARGS2:MxValueList + ) + ~> ($TEST:MxRustTest):KItem + +endmodule + +``` diff --git a/mx-rust-semantics/targets/two-contracts-testing/mx-rust.md b/mx-rust-semantics/targets/two-contracts-testing/mx-rust.md new file mode 100644 index 0000000..23117e4 --- /dev/null +++ b/mx-rust-semantics/targets/two-contracts-testing/mx-rust.md @@ -0,0 +1,15 @@ +```k + +requires "configuration.md" +requires "../common/mx-rust-testing.md" + +module MX-RUST-SYNTAX + imports MX-RUST-COMMON-TEST-SYNTAX +endmodule + +module MX-RUST + imports private COMMON-K-CELL + imports private MX-RUST-COMMON-TEST +endmodule + +``` diff --git a/mx-semantics/main/calls/hooks.md b/mx-semantics/main/calls/hooks.md index de8c109..8f7e048 100644 --- a/mx-semantics/main/calls/hooks.md +++ b/mx-semantics/main/calls/hooks.md @@ -4,6 +4,7 @@ module MX-CALLS-HOOKS imports private COMMON-K-CELL imports private INT imports private MX-CALL-CONFIGURATION + imports private MX-CALL-RETURN-VALUE-CONFIGURATION imports private MX-CALL-TOOLS-SYNTAX imports private MX-COMMON-SYNTAX imports private STRING @@ -12,6 +13,10 @@ module MX-CALLS-HOOKS MX#getCaller ( .MxValueList ) => mxStringValue(Caller) ... Caller:String + rule + MX#popLastReturnValue ( .MxValueList ) => V ... + (V:MxValue , L:MxValueList) => L + rule MX#managedMultiTransferESDTNFTExecute diff --git a/parsers/args-mx-rust-two-contracts.sh b/parsers/args-mx-rust-two-contracts.sh new file mode 100755 index 0000000..03cc235 --- /dev/null +++ b/parsers/args-mx-rust-two-contracts.sh @@ -0,0 +1,5 @@ +#! /bin/bash + +source ${BASH_SOURCE%/*}/inc-endpoint-args-file.sh + +parse_endpoint_args .build/mx-rust-two-contracts-testing-kompiled $1 diff --git a/parsers/contract-mx-rust-two-contracts.sh b/parsers/contract-mx-rust-two-contracts.sh new file mode 100755 index 0000000..98dfb1f --- /dev/null +++ b/parsers/contract-mx-rust-two-contracts.sh @@ -0,0 +1,5 @@ +#! /bin/bash + +source ${BASH_SOURCE%/*}/inc-contract-file.sh + +parse_rust .build/mx-rust-two-contracts-testing-kompiled $1 diff --git a/parsers/test-mx-rust-two-contracts.sh b/parsers/test-mx-rust-two-contracts.sh new file mode 100755 index 0000000..8bfdbf4 --- /dev/null +++ b/parsers/test-mx-rust-two-contracts.sh @@ -0,0 +1,5 @@ +#! /bin/bash + +source ${BASH_SOURCE%/*}/inc-test-mx-rust-file.sh + +parse_test .build/mx-rust-two-contracts-testing-kompiled $1 diff --git a/rust-semantics/preprocessing.md b/rust-semantics/preprocessing.md index f12e1f0..4a47388 100644 --- a/rust-semantics/preprocessing.md +++ b/rust-semantics/preprocessing.md @@ -5,6 +5,7 @@ requires "preprocessing/crate.md" requires "preprocessing/configuration.md" requires "preprocessing/helpers.md" requires "preprocessing/initialization.md" +requires "preprocessing/module.md" requires "preprocessing/syntax.md" requires "preprocessing/tools.md" requires "preprocessing/trait.md" @@ -14,6 +15,7 @@ module RUST-PREPROCESSING imports private CRATE imports private INITIALIZATION imports private RUST-CONSTANTS + imports private RUST-MODULE imports private RUST-PREPROCESSING-TOOLS imports private TRAIT imports private TRAIT-METHODS diff --git a/rust-semantics/preprocessing/crate.md b/rust-semantics/preprocessing/crate.md index 7a7e817..017e932 100644 --- a/rust-semantics/preprocessing/crate.md +++ b/rust-semantics/preprocessing/crate.md @@ -12,8 +12,13 @@ module CRATE ( (_Atts:InnerAttributes (_A:OuterAttributes _U:UseDeclaration):Item Is:Items):Crate => (.InnerAttributes Is):Crate ) + rule (.K => moduleParser(M)) + ~> crateParser + ( (_Atts:InnerAttributes (_ItemAtts:OuterAttributes _V:MaybeVisibility M:Module):Item Is:Items):Crate + => (.InnerAttributes Is):Crate + ) rule - (.K => traitParser(T, ItemAtts)) + (.K => traitParser(T, .TypePath, ItemAtts)) ~> crateParser ( (_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate => (.InnerAttributes Is):Crate diff --git a/rust-semantics/preprocessing/module.md b/rust-semantics/preprocessing/module.md new file mode 100644 index 0000000..536b394 --- /dev/null +++ b/rust-semantics/preprocessing/module.md @@ -0,0 +1,25 @@ +```k + +module RUST-MODULE + imports private RUST-PREPROCESSING-PRIVATE-SYNTAX + + rule moduleParser(mod Name:Identifier { _:InnerAttributes Contents:Items }) + => moduleItemsParser(Contents, Name) + + rule moduleItemsParser(.Items, _Name) => .K + rule + (.K => traitParser(T, Name, ItemAtts)) + ~> moduleItemsParser + ( (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items + => Is + , Name + ) + rule + moduleItemsParser + ( (_OuterAttributes _:MacroItem):Item Is:Items + => Is + , _Name + ) +endmodule + +``` diff --git a/rust-semantics/preprocessing/syntax.md b/rust-semantics/preprocessing/syntax.md index 056f403..7de2da7 100644 --- a/rust-semantics/preprocessing/syntax.md +++ b/rust-semantics/preprocessing/syntax.md @@ -14,12 +14,15 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX syntax MaybeTypePath ::= ".TypePath" | TypePath - syntax Initializer ::= traitParser(Trait, OuterAttributes) - | traitMethodsParser(AssociatedItems, traitName:Identifier) + syntax Initializer ::= traitParser(Trait, MaybeTypePath, OuterAttributes) + | traitMethodsParser(AssociatedItems, traitName:TypePath) | traitInitializer ( traitName: TypePath , atts: OuterAttributes ) + syntax Initializer ::= moduleParser(Module) + | moduleItemsParser(Items, TypePath) + syntax Initializer ::= addMethod(traitName : TypePath, function: Function, atts:OuterAttributes) | #addMethod( diff --git a/rust-semantics/preprocessing/trait-methods.md b/rust-semantics/preprocessing/trait-methods.md index 79bb0f7..b5ec681 100644 --- a/rust-semantics/preprocessing/trait-methods.md +++ b/rust-semantics/preprocessing/trait-methods.md @@ -4,12 +4,12 @@ module TRAIT-METHODS imports private RUST-PREPROCESSING-PRIVATE-HELPERS imports private RUST-PREPROCESSING-PRIVATE-SYNTAX - rule traitMethodsParser(.AssociatedItems, _Name:Identifier) + rule traitMethodsParser(.AssociatedItems, _Name:TypePath) => .K rule (.K => addMethod(TraitName, F, A)) ~> traitMethodsParser( (A:OuterAttributes F:Function) AIs:AssociatedItems => AIs, - TraitName:Identifier + TraitName:TypePath ) endmodule diff --git a/rust-semantics/preprocessing/trait.md b/rust-semantics/preprocessing/trait.md index 3a1c360..3f3fb51 100644 --- a/rust-semantics/preprocessing/trait.md +++ b/rust-semantics/preprocessing/trait.md @@ -4,11 +4,12 @@ module TRAIT imports private RUST-PREPROCESSING-PRIVATE-SYNTAX rule traitParser - ( trait Name:Identifier { .InnerAttributes Functions:AssociatedItems } - , ItemAtts:OuterAttributes - ) - => traitInitializer(Name, ItemAtts) - ~> traitMethodsParser(Functions, Name) + ( trait Name:Identifier { .InnerAttributes Functions:AssociatedItems } + , Path:MaybeTypePath + , ItemAtts:OuterAttributes + ) + => traitInitializer(append(Path, Name), ItemAtts) + ~> traitMethodsParser(Functions, append(Path, Name)) endmodule ``` diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md index 0d49a30..5ee3ab7 100644 --- a/rust-semantics/rust-common-syntax.md +++ b/rust-semantics/rust-common-syntax.md @@ -394,7 +394,9 @@ https://doc.rust-lang.org/reference/items/extern-crates.html > Expression ".." Expression [seqstrict] > right: - Expression "=" Expression + // The Rust reference says that assignments are evaluated + // in reverse order. + Expression "=" Expression [seqstrict(2, 1)] | Expression "+=" Expression | Expression "-=" Expression | Expression "*=" Expression diff --git a/tests/mx-rust-two-contracts/proxy.1.args b/tests/mx-rust-two-contracts/proxy.1.args new file mode 100644 index 0000000..e69de29 diff --git a/tests/mx-rust-two-contracts/proxy.1.rs b/tests/mx-rust-two-contracts/proxy.1.rs new file mode 100644 index 0000000..b4fd8cf --- /dev/null +++ b/tests/mx-rust-two-contracts/proxy.1.rs @@ -0,0 +1,43 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +mod my_proxy { + multiversx_sc::imports!(); + + #[multiversx_sc::proxy] + pub trait Storage { + #[endpoint(getMyStorage)] + fn get_my_storage(&self) -> BigUint; + + #[endpoint(setMyStorage)] + fn set_my_storage(&self, value: &BigUint); + } +} + +#[multiversx_sc::contract] +pub trait Caller { + #[init] + fn init(&self) {} + + #[upgrade] + fn upgrade(&self) {} + + #[endpoint(getStorage)] + fn get_storage(&self, address: ManagedAddress) -> BigUint { + self.storage_proxy(address) + .get_my_storage() + .execute_on_dest_context() + } + + #[endpoint(setStorage)] + fn set_my_storage(&self, address: ManagedAddress, value: BigUint) { + self.storage_proxy(address) + .set_my_storage(value) + .execute_on_dest_context() + } + + #[proxy] + fn storage_proxy(&self, sc_address: ManagedAddress) -> my_proxy::Proxy; +} diff --git a/tests/mx-rust-two-contracts/proxy.2.args b/tests/mx-rust-two-contracts/proxy.2.args new file mode 100644 index 0000000..e69de29 diff --git a/tests/mx-rust-two-contracts/proxy.2.rs b/tests/mx-rust-two-contracts/proxy.2.rs new file mode 100644 index 0000000..adb93c5 --- /dev/null +++ b/tests/mx-rust-two-contracts/proxy.2.rs @@ -0,0 +1,27 @@ +#![no_std] + +#[allow(unused_imports)] +use multiversx_sc::imports::*; + +#[multiversx_sc::contract] +pub trait Storage { + #[view(noArg)] + #[storage_mapper("my_value")] + fn my_storage(&self) -> SingleValueMapper; + + #[init] + fn init(&self) {} + + #[upgrade] + fn upgrade(&self) {} + + #[endpoint(getMyStorage)] + fn get_my_storage(&self) -> BigUint { + self.my_storage().get() + } + + #[endpoint(setMyStorage)] + fn set_my_storage(&self, value: &BigUint) { + self.my_storage().set(value) + } +} diff --git a/tests/mx-rust-two-contracts/proxy.run b/tests/mx-rust-two-contracts/proxy.run new file mode 100644 index 0000000..c69576f --- /dev/null +++ b/tests/mx-rust-two-contracts/proxy.run @@ -0,0 +1,34 @@ +setCallee("Owner"); + +push mxListValue(mxStringValue("TestContract2")); +push mxStringValue("getStorage"); +push mxIntValue(0); +push mxTransfersValue(); +push mxIntValue(0); +push mxStringValue("TestContract1"); +call 6 MX#managedExecuteOnDestContext; +check_eq mxIntValue(0); + +push_return_value; +check_eq mxIntValue(0); + +push mxListValue(mxStringValue("TestContract2"), mxIntValue(8)); +push mxStringValue("setStorage"); +push mxIntValue(0); +push mxTransfersValue(); +push mxIntValue(0); +push mxStringValue("TestContract1"); +call 6 MX#managedExecuteOnDestContext; +check_eq mxIntValue(0); + +push mxListValue(mxStringValue("TestContract2")); +push mxStringValue("getStorage"); +push mxIntValue(0); +push mxTransfersValue(); +push mxIntValue(0); +push mxStringValue("TestContract1"); +call 6 MX#managedExecuteOnDestContext; +check_eq mxIntValue(0); + +push_return_value; +check_eq mxIntValue(8)