Pi-Squared-Inc · virgil-serbanuta · Sep 13, 2024 · Sep 13, 2024 · Sep 13, 2024
diff --git a/Makefile b/Makefile
@@ -31,23 +31,28 @@ MX_RUST_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name
 MX_RUST_KOMPILED ::= .build/mx-rust-kompiled
 MX_RUST_TIMESTAMP ::= $(MX_RUST_KOMPILED)/timestamp
 
-MX_RUST_TESTING_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
 MX_RUST_TESTING_KOMPILED ::= .build/mx-rust-testing-kompiled
 MX_RUST_TESTING_TIMESTAMP ::= $(MX_RUST_TESTING_KOMPILED)/timestamp
 MX_RUST_TESTING_INPUT_DIR ::= tests/mx-rust
 MX_RUST_TESTING_OUTPUT_DIR ::= .build/mx-rust/output
 MX_RUST_TESTING_INPUTS ::= $(wildcard $(MX_RUST_TESTING_INPUT_DIR)/*.run)
 MX_RUST_TESTING_OUTPUTS ::= $(patsubst $(MX_RUST_TESTING_INPUT_DIR)/%,$(MX_RUST_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_RUST_TESTING_INPUTS))
 
-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_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
@@ -57,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)
 
@@ -73,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)
@@ -104,7 +112,6 @@ $(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)
@@ -113,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 > [email protected] && mv -f [email protected] $@
@@ -132,17 +147,17 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%
 $(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: \
 			$(EXECUTION_INPUT_DIR)/%.run \
 			$(RUST_EXECUTION_TIMESTAMP) \
-			parse-rust.sh \
-			parse-test.sh
+			parsers/contract-rust.sh \
+			parsers/test-rust.sh
 	mkdir -p $(EXECUTION_OUTPUT_DIR)
 	krun \
 		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
 		--definition $(RUST_EXECUTION_KOMPILED) \
-		--parser $(CURDIR)/parse-rust.sh \
+		--parser $(CURDIR)/parsers/contract-rust.sh \
 		--output kore \
 		--output-file [email protected] \
 		-cTEST="$(shell cat $<)" \
-		-pTEST=$(CURDIR)/parse-test.sh
+		-pTEST=$(CURDIR)/parsers/test-rust.sh
 	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f [email protected] $@
 
@@ -161,38 +176,67 @@ $(MX_TESTING_OUTPUT_DIR)/%.mx.executed.kore: $(MX_TESTING_INPUT_DIR)/%.mx $(MX_T
 $(MX_RUST_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 			$(MX_RUST_TESTING_INPUT_DIR)/%.run \
 			$(MX_RUST_TESTING_TIMESTAMP) \
-			parse-mx-rust.sh \
-			parse-mx-rust-test.sh
+			parsers/contract-mx-rust.sh \
+			parsers/test-mx-rust.sh
 	mkdir -p $(MX_RUST_TESTING_OUTPUT_DIR)
 	krun \
 		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
 		--definition $(MX_RUST_TESTING_KOMPILED) \
-		--parser $(CURDIR)/parse-mx-rust.sh \
+		--parser $(CURDIR)/parsers/contract-mx-rust.sh \
 		--output kore \
 		--output-file [email protected] \
 		-cTEST='$(shell cat $<)' \
-		-pTEST=$(CURDIR)/parse-mx-rust-test.sh
+		-pTEST=$(CURDIR)/parsers/test-mx-rust.sh
 	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f [email protected] $@
 
-
 # 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
+			$(MX_RUST_CONTRACT_TESTING_INPUT_DIR)/$(patsubst %.run,%.args,$<) \
+			parsers/contract-mx-rust-contract.sh \
+			parsers/args-mx-rust-contract.sh \
+			parsers/test-mx-rust-contract.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 \
+		--parser $(CURDIR)/parsers/contract-mx-rust-contract.sh \
 		--output kore \
 		--output-file [email protected] \
 		-cTEST='$(shell cat $<)' \
-		-pTEST=$(CURDIR)/parse-mx-rust-contract-test.sh \
+		-pTEST=$(CURDIR)/parsers/test-mx-rust-contract.sh \
 		-cARGS='$(shell cat $(patsubst %.run,%.args,$<))' \
-		-pARGS=$(CURDIR)/parse-mx-rust-contract-args.sh
+		-pARGS=$(CURDIR)/parsers/args-mx-rust-contract.sh
+	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f [email protected] $@
+
+$(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 [email protected] \
+		-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 [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f [email protected] $@
diff --git a/mx-rust-semantics/main/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md
@@ -13,10 +13,26 @@ 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
+                                    )
                                 | addStorageMethodBody
                                     ( trait: TypePath
                                     , methodName: Identifier
@@ -30,24 +46,27 @@ module MX-RUST-PREPROCESSING-METHODS
                                     )
 
     rule
-        <k> mxRustPreprocessMethods(T:TypePath)
-            => mxRustPreprocessMethods(T, MethodNames)
+        <k> mxRustPreprocessMethods(T:TypePath, TType:TraitType)
+            => mxRustPreprocessMethods(T, TType, MethodNames)
             ...
         </k>
         <trait-path> T </trait-path>
         <method-list> MethodNames:List </method-list>
 
-    rule mxRustPreprocessMethods(_:TypePath, .List) => .K
-    rule mxRustPreprocessMethods(T:TypePath, ListItem(MethodName:Identifier) Names:List)
-        => mxRustPreprocessMethod(T, MethodName) ~> mxRustPreprocessMethods(T, Names)
+    rule mxRustPreprocessMethods(_:TypePath, _:TraitType, .List) => .K
+    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)
 
+    rule mxRustPreprocessStorage(_Trait:TypePath, proxy, _Method:Identifier) => .K
     rule
         <k>
-            mxRustPreprocessStorage(Trait:TypePath, Method:Identifier)
+            mxRustPreprocessStorage(Trait:TypePath, contract, Method:Identifier)
             => addStorageMethodBody
                 (... trait: Trait, methodName: Method
                 , storageName: getStorageName(Atts)
@@ -64,12 +83,28 @@ module MX-RUST-PREPROCESSING-METHODS
         </method-return-type>
         requires getStorageName(Atts) =/=K ""
         [priority(50)]
-    rule mxRustPreprocessStorage(_Trait:TypePath, _Method:Identifier) => .K
+    rule mxRustPreprocessStorage(_Trait:TypePath, contract, _Method:Identifier) => .K
         [priority(100)]
 
     rule
         <k>
-            mxRustPreprocessEndpoint(Trait:TypePath, Method:Identifier)
+            mxRustPreprocessEndpoint(Trait:TypePath, proxy, Method:Identifier)
+            => .K
+            ...
+        </k>
+        <trait-path> Trait </trait-path>
+        <method-name> Method </method-name>
+        <method-implementation>
+            empty
+            => block(buildProxyEndpointMethod(Params, getEndpointName(Atts, Method)))
+        </method-implementation>
+        <method-outer-attributes> Atts:OuterAttributes </method-outer-attributes>
+        <method-params> Params:NormalizedFunctionParameterList </method-params>
+        requires getEndpointName(Atts, Method) =/=K ""
+        [priority(50)]
+    rule
+        <k>
+            mxRustPreprocessEndpoint(Trait:TypePath, contract, Method:Identifier)
             => mxRustAddEndpointMapping
                 (... trait: Trait, methodName: Method
                 , endpointName: getEndpointName(Atts, Method)
@@ -81,7 +116,7 @@ module MX-RUST-PREPROCESSING-METHODS
         <method-outer-attributes> Atts:OuterAttributes </method-outer-attributes>
         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
@@ -150,6 +185,42 @@ module MX-RUST-PREPROCESSING-METHODS
         => getEndpointName(Atts, Default)
         [owise]
 
+    syntax BlockExpression ::= buildProxyEndpointMethod
+                                  ( params: NormalizedFunctionParameterList
+                                  , endpointName: String
+                                  )  [function]
+    rule buildProxyEndpointMethod
+            (... params: S:SelfSort : _ , Params:NormalizedFunctionParameterList
+            , endpointName: Name
+            )
+        => { .InnerAttributes
+              S . #token("endpoint_name", "Identifier") = Name;
+              S . #token("args", "Identifier") =
+                  (paramsToMaybeTupleElements(Params)):TupleExpression;
+              S
+            }
+    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)) , 
+
+    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

diff --git a/mx-rust-semantics/main/preprocessing/traits.md b/mx-rust-semantics/main/preprocessing/traits.md
@@ -21,7 +21,32 @@ module MX-RUST-PREPROCESSING-TRAITS
     rule mxRustPreprocessTraits(ListItem(Trait:TypePath) Traits:List)
         => mxRustPreprocessTrait(Trait) ~> mxRustPreprocessTraits(Traits)
 
-    rule mxRustPreprocessTrait(Trait:TypePath) => mxRustPreprocessMethods(Trait)
+    rule
+        <k>
+            mxRustPreprocessTrait(Trait:TypePath) => mxRustPreprocessMethods(Trait, contract)
+            ...
+        </k>
+        <trait-path> Trait </trait-path>
+        <trait-attributes>
+            #[ #token("multiversx_sc", "Identifier")
+                :: #token("contract", "Identifier")
+                :: .SimplePathList
+            ]
+            .NonEmptyOuterAttributes
+        </trait-attributes>
+    rule
+        <k>
+            mxRustPreprocessTrait(Trait:TypePath) => mxRustPreprocessMethods(Trait, proxy)
+            ...
+        </k>
+        <trait-path> Trait </trait-path>
+        <trait-attributes>
+            #[ #token("multiversx_sc", "Identifier")
+                :: #token("proxy", "Identifier")
+                :: .SimplePathList
+            ]
+            .NonEmptyOuterAttributes
+        </trait-attributes>
 endmodule
 
 ```
diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md
@@ -6,7 +6,7 @@ module MX-RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
 
     syntax MxRustInstruction  ::= "mxRustPreprocessTraits"
-                                | mxRustPreprocessMethods(TypePath)
+                                | mxRustPreprocessMethods(TypePath, TraitType)
                                 | mxRustCreateAccount(String)
                                 | mxRustCreateContract
                                     ( owner: String
@@ -22,6 +22,7 @@ module MX-RUST-REPRESENTATION
                                 | mxRustLoadPtr(Int)
                                 | mxRustGetBigIntFromStruct(Value)
 
+    syntax TraitType ::= "contract" | "proxy"
     syntax MxRustType ::= "noType" | rustType(Type)
     syntax MxRustTypeOrError ::= MxRustType | SemanticsError
     syntax Value ::= MxRustType
@@ -30,6 +31,7 @@ module MX-RUST-REPRESENTATION
 
     syntax Expression ::= concatString(Expression, Expression)  [seqstrict]
                         | toString(Expression)  [strict]
+                        | error(String, KItem)
 
     syntax MxValue ::= rustDestination(Int, MxRustType)