diff --git a/Makefile b/Makefile
index 47af25d..2d304dd 100644
--- a/Makefile
+++ b/Makefile
@@ -31,7 +31,6 @@ 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
@@ -39,15 +38,21 @@ 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 > $@.tmp && mv -f $@.tmp $@
@@ -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 $@.tmp \
 		-cTEST="$(shell cat $<)" \
-		-pTEST=$(CURDIR)/parse-test.sh
+		-pTEST=$(CURDIR)/parsers/test-rust.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
 
@@ -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 $@.tmp \
 		-cTEST='$(shell cat $<)' \
-		-pTEST=$(CURDIR)/parse-mx-rust-test.sh
+		-pTEST=$(CURDIR)/parsers/test-mx-rust.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
+			$(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 $@.tmp \
 		-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 $@.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/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md
index bf0676e..9aff04f 100644
--- 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
index e37339e..8248105 100644
--- 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
index 5de8bc8..f66d0d3 100644
--- 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)
 
diff --git a/mx-rust-semantics/setup/mx.md b/mx-rust-semantics/setup/mx.md
index 75f243b..514ff9e 100644
--- a/mx-rust-semantics/setup/mx.md
+++ b/mx-rust-semantics/setup/mx.md
@@ -16,6 +16,7 @@ module MX-RUST-SETUP-MX
                                       "," gasLimit: Int
                                       "," args: MxValueList
                                       ")"
+    syntax MXRustInstruction  ::= "MxRust#addAccountWithPreprocessedCode" "(" String ")"
     syntax MXRustInstruction  ::= "MxRust#addAccountWithPreprocessedCode" "(" String "," TypePath ")"
                                 | "MxRust#clearMxReturnValue"
 
@@ -59,7 +60,8 @@ module MX-RUST-SETUP-MX
                 , gasLimit: GasLimit:Int
                 , args: Args:MxValueList
                 )
-            => MxRust#addAccountWithPreprocessedCode(Contract, TraitName)
+            => findContractName(Traits)
+              ~> MxRust#addAccountWithPreprocessedCode(Contract)
               ~> callContract
                   ( "#init"
                   , prepareIndirectContractCallInput
@@ -75,7 +77,10 @@ module MX-RUST-SETUP-MX
               ~> MxRust#clearMxReturnValue
             ...
         </k>
-        <preprocessed> ... <trait-list> ListItem(TraitName:TypePath) </trait-list>  </preprocessed>
+        <preprocessed> ... <trait-list> Traits:List </trait-list>  </preprocessed>
+
+    rule TraitName:TypePath ~> MxRust#addAccountWithPreprocessedCode(Contract)
+        => MxRust#addAccountWithPreprocessedCode(Contract, TraitName)
 
     rule
         <k>
diff --git a/mx-rust-semantics/targets/blockchain/mx-rust.md b/mx-rust-semantics/targets/blockchain/mx-rust.md
index f12e9e3..825bce4 100644
--- a/mx-rust-semantics/targets/blockchain/mx-rust.md
+++ b/mx-rust-semantics/targets/blockchain/mx-rust.md
@@ -1,21 +1,15 @@
 ```k
 
 requires "configuration.md"
-requires "mx-semantics/main/mx-common.md"
-requires "mx-semantics/main/syntax.md"
-requires "rust-semantics/rust-common.md"
-requires "rust-semantics/rust-common-syntax.md"
-requires "../../main/mx-rust-common.md"
+requires "../common/mx-rust.md"
 
 module MX-RUST-SYNTAX
-    imports RUST-COMMON-SYNTAX
+    imports MX-RUST-COMMON-TARGET-SYNTAX
 endmodule
 
 module MX-RUST
-    imports private MX-COMMON
-    imports private MX-RUST-COMMON
-    imports private MX-RUST-CONFIGURATION
-    imports private RUST-COMMON
+    imports private COMMON-K-CELL
+    imports private MX-RUST-COMMON-TARGET
 endmodule
 
 ```
diff --git a/mx-rust-semantics/targets/common/configuration-testing.md b/mx-rust-semantics/targets/common/configuration-testing.md
new file mode 100644
index 0000000..bba2649
--- /dev/null
+++ b/mx-rust-semantics/targets/common/configuration-testing.md
@@ -0,0 +1,19 @@
+```k
+
+requires "../../main/configuration.md"
+requires "../../test/configuration.md"
+
+module MX-RUST-CONFIGURATION
+    imports COMMON-K-CELL
+    imports MX-RUST-COMMON-CONFIGURATION
+    imports MX-RUST-EXECUTION-TEST-CONFIGURATION
+
+    configuration
+        <mx-rust-cfg>
+            <mx-rust-test/>
+            <mx-rust/>
+            <k/>
+        </mx-rust-cfg>
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/common/mx-rust-testing.md b/mx-rust-semantics/targets/common/mx-rust-testing.md
new file mode 100644
index 0000000..2b0abd1
--- /dev/null
+++ b/mx-rust-semantics/targets/common/mx-rust-testing.md
@@ -0,0 +1,33 @@
+```k
+
+requires "configuration-testing.md"
+requires "mx-rust.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-COMMON-TEST-SYNTAX
+    imports RUST-COMMON-SYNTAX
+    imports MX-RUST-TESTING-PARSING-SYNTAX
+endmodule
+
+module MX-RUST-COMMON-TEST
+    imports private MX-RUST-COMMON-TARGET
+    imports private MX-RUST-TEST
+    imports private MX-RUST-SETUP-MX
+    imports private MX-SETUP
+    imports private MX-TEST-EXECUTION
+    imports private RUST-EXECUTION-TEST
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/common/mx-rust.md b/mx-rust-semantics/targets/common/mx-rust.md
new file mode 100644
index 0000000..45480c3
--- /dev/null
+++ b/mx-rust-semantics/targets/common/mx-rust.md
@@ -0,0 +1,20 @@
+```k
+
+requires "mx-semantics/main/mx-common.md"
+requires "mx-semantics/main/syntax.md"
+requires "rust-semantics/rust-common.md"
+requires "rust-semantics/rust-common-syntax.md"
+requires "../../main/mx-rust-common.md"
+
+module MX-RUST-COMMON-TARGET-SYNTAX
+    imports RUST-COMMON-SYNTAX
+endmodule
+
+module MX-RUST-COMMON-TARGET
+    imports private MX-COMMON
+    imports private MX-RUST-COMMON
+    imports private MX-RUST-CONFIGURATION
+    imports private RUST-COMMON
+endmodule
+
+```
diff --git a/mx-rust-semantics/targets/contract-testing/configuration.md b/mx-rust-semantics/targets/contract-testing/configuration.md
index 1771cfa..0ecdc3b 100644
--- a/mx-rust-semantics/targets/contract-testing/configuration.md
+++ b/mx-rust-semantics/targets/contract-testing/configuration.md
@@ -1,8 +1,5 @@
 ```k
 
-requires "../../main/configuration.md"
-requires "../../test/configuration.md"
-
 module COMMON-K-CELL
     imports MX-RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
@@ -23,17 +20,4 @@ module COMMON-K-CELL
         </k>
 endmodule
 
-module MX-RUST-CONFIGURATION
-    imports COMMON-K-CELL
-    imports MX-RUST-COMMON-CONFIGURATION
-    imports MX-RUST-EXECUTION-TEST-CONFIGURATION
-
-    configuration
-        <mx-rust-cfg>
-            <mx-rust-test/>
-            <mx-rust/>
-            <k/>
-        </mx-rust-cfg>
-endmodule
-
 ```
diff --git a/mx-rust-semantics/targets/contract-testing/mx-rust.md b/mx-rust-semantics/targets/contract-testing/mx-rust.md
index 15d6188..23117e4 100644
--- a/mx-rust-semantics/targets/contract-testing/mx-rust.md
+++ b/mx-rust-semantics/targets/contract-testing/mx-rust.md
@@ -1,35 +1,15 @@
 ```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"
+requires "../common/mx-rust-testing.md"
 
 module MX-RUST-SYNTAX
-    imports RUST-COMMON-SYNTAX
-    imports MX-RUST-TESTING-PARSING-SYNTAX
+    imports MX-RUST-COMMON-TEST-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
+    imports private COMMON-K-CELL
+    imports private MX-RUST-COMMON-TEST
 endmodule
 
 ```
diff --git a/mx-rust-semantics/targets/testing/configuration.md b/mx-rust-semantics/targets/testing/configuration.md
index 724e3ec..aced1a8 100644
--- a/mx-rust-semantics/targets/testing/configuration.md
+++ b/mx-rust-semantics/targets/testing/configuration.md
@@ -1,8 +1,5 @@
 ```k
 
-requires "../../main/configuration.md"
-requires "../../test/configuration.md"
-
 module COMMON-K-CELL
     imports MX-RUST-REPRESENTATION
     imports RUST-PREPROCESSING-SYNTAX
@@ -14,17 +11,4 @@ module COMMON-K-CELL
         <k> crateParser($PGM:Crate) ~> mxRustPreprocessTraits ~> ($TEST:MxRustTest):KItem </k>
 endmodule
 
-module MX-RUST-CONFIGURATION
-    imports COMMON-K-CELL
-    imports MX-RUST-COMMON-CONFIGURATION
-    imports MX-RUST-EXECUTION-TEST-CONFIGURATION
-
-    configuration
-        <mx-rust-cfg>
-            <mx-rust-test/>
-            <mx-rust/>
-            <k/>
-        </mx-rust-cfg>
-endmodule
-
 ```
diff --git a/mx-rust-semantics/targets/testing/mx-rust.md b/mx-rust-semantics/targets/testing/mx-rust.md
index 7fd019d..23117e4 100644
--- a/mx-rust-semantics/targets/testing/mx-rust.md
+++ b/mx-rust-semantics/targets/testing/mx-rust.md
@@ -1,33 +1,15 @@
 ```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 "../../test/execution.md"
+requires "../common/mx-rust-testing.md"
 
 module MX-RUST-SYNTAX
-    imports RUST-COMMON-SYNTAX
-    imports MX-RUST-TESTING-PARSING-SYNTAX
+    imports MX-RUST-COMMON-TEST-SYNTAX
 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
-    imports private MX-TEST-EXECUTION
-    imports private RUST-COMMON
-    imports private RUST-EXECUTION-TEST
+    imports private COMMON-K-CELL
+    imports private MX-RUST-COMMON-TEST
 endmodule
 
 ```
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
+        <k>
+            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
+        </k>
+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/parse-mx-rust-contract-args.sh b/parse-mx-rust-contract-args.sh
deleted file mode 100755
index 4dfd2d1..0000000
--- a/parse-mx-rust-contract-args.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#! /bin/bash
-
-kast \
-    --output kore \
-    --definition .build/mx-rust-contract-testing-kompiled \
-    --module MX-RUST-SYNTAX \
-    --sort MxValueList \
-    $1
diff --git a/parse-mx-rust-contract-test.sh b/parse-mx-rust-contract-test.sh
deleted file mode 100755
index 56499eb..0000000
--- a/parse-mx-rust-contract-test.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#! /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
deleted file mode 100755
index 4ec1a73..0000000
--- a/parse-mx-rust-contract.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#! /bin/bash
-
-kast \
-    --output kore \
-    --definition .build/mx-rust-contract-testing-kompiled \
-    --module RUST-COMMON-SYNTAX \
-    --sort Crate \
-    $1
diff --git a/parse-mx-rust-test.sh b/parse-mx-rust-test.sh
deleted file mode 100755
index abb0296..0000000
--- a/parse-mx-rust-test.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#! /bin/bash
-
-kast \
-    --output kore \
-    --definition .build/mx-rust-testing-kompiled \
-    --module MX-RUST-SYNTAX \
-    --sort MxRustTest \
-    $1
diff --git a/parse-mx-rust.sh b/parse-mx-rust.sh
deleted file mode 100755
index c20b2ec..0000000
--- a/parse-mx-rust.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#! /bin/bash
-
-kast \
-    --output kore \
-    --definition .build/mx-rust-testing-kompiled \
-    --module RUST-COMMON-SYNTAX \
-    --sort Crate \
-    $1
diff --git a/parse-rust.sh b/parse-rust.sh
deleted file mode 100755
index 1833265..0000000
--- a/parse-rust.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-#! /bin/bash
-
-kast \
-    --output kore \
-    --definition .build/rust-execution-kompiled \
-    --module RUST-COMMON-SYNTAX \
-    --sort Crate \
-    $1
diff --git a/parsers/args-mx-rust-contract.sh b/parsers/args-mx-rust-contract.sh
new file mode 100755
index 0000000..6480a66
--- /dev/null
+++ b/parsers/args-mx-rust-contract.sh
@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-endpoint-args-file.sh
+
+parse_endpoint_args .build/mx-rust-contract-testing-kompiled $1
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-contract.sh b/parsers/contract-mx-rust-contract.sh
new file mode 100755
index 0000000..741bbc1
--- /dev/null
+++ b/parsers/contract-mx-rust-contract.sh
@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-contract-file.sh
+
+parse_rust .build/mx-rust-contract-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/contract-mx-rust.sh b/parsers/contract-mx-rust.sh
new file mode 100755
index 0000000..0fc9f71
--- /dev/null
+++ b/parsers/contract-mx-rust.sh
@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-contract-file.sh
+
+parse_rust .build/mx-rust-testing-kompiled $1
diff --git a/parsers/contract-rust.sh b/parsers/contract-rust.sh
new file mode 100755
index 0000000..82a59b8
--- /dev/null
+++ b/parsers/contract-rust.sh
@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-contract-file.sh
+
+parse_rust .build/rust-execution-kompiled $1
diff --git a/parsers/inc-contract-file.sh b/parsers/inc-contract-file.sh
new file mode 100644
index 0000000..08bc0dd
--- /dev/null
+++ b/parsers/inc-contract-file.sh
@@ -0,0 +1,8 @@
+function parse_rust() {
+    kast \
+        --output kore \
+        --definition $1 \
+        --module RUST-COMMON-SYNTAX \
+        --sort Crate \
+        $2
+}
diff --git a/parsers/inc-endpoint-args-file.sh b/parsers/inc-endpoint-args-file.sh
new file mode 100644
index 0000000..d1dded6
--- /dev/null
+++ b/parsers/inc-endpoint-args-file.sh
@@ -0,0 +1,8 @@
+function parse_endpoint_args() {
+    kast \
+        --output kore \
+        --definition $1 \
+        --module MX-RUST-SYNTAX \
+        --sort MxValueList \
+        $2
+}
diff --git a/parsers/inc-test-mx-rust-file.sh b/parsers/inc-test-mx-rust-file.sh
new file mode 100644
index 0000000..256ebae
--- /dev/null
+++ b/parsers/inc-test-mx-rust-file.sh
@@ -0,0 +1,8 @@
+function parse_test() {
+    kast \
+        --output kore \
+        --definition $1 \
+        --module MX-RUST-SYNTAX \
+        --sort MxRustTest \
+        $2
+}
diff --git a/parsers/test-mx-rust-contract.sh b/parsers/test-mx-rust-contract.sh
new file mode 100755
index 0000000..70857d1
--- /dev/null
+++ b/parsers/test-mx-rust-contract.sh
@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-test-mx-rust-file.sh
+
+parse_test .build/mx-rust-contract-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/parsers/test-mx-rust.sh b/parsers/test-mx-rust.sh
new file mode 100755
index 0000000..34a1338
--- /dev/null
+++ b/parsers/test-mx-rust.sh
@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-test-mx-rust-file.sh
+
+parse_test .build/mx-rust-testing-kompiled $1
diff --git a/parse-test.sh b/parsers/test-rust.sh
similarity index 100%
rename from parse-test.sh
rename to parsers/test-rust.sh
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/configuration.md b/rust-semantics/preprocessing/configuration.md
index fc3a6fd..314415a 100644
--- a/rust-semantics/preprocessing/configuration.md
+++ b/rust-semantics/preprocessing/configuration.md
@@ -18,6 +18,7 @@ module RUST-PREPROCESSING-CONFIGURATION
             <traits>
                 <trait multiplicity="*" type="Map">
                     <trait-path> my_identifier:TypePath </trait-path>
+                    <trait-attributes> `emptyOuterAttributes`(.KList):OuterAttributes </trait-attributes>
                     <method-list> .List </method-list>  // List of Identifier
                     <methods>
                         <method multiplicity="*" type="Map">
diff --git a/rust-semantics/preprocessing/crate.md b/rust-semantics/preprocessing/crate.md
index 099a3e6..017e932 100644
--- a/rust-semantics/preprocessing/crate.md
+++ b/rust-semantics/preprocessing/crate.md
@@ -12,10 +12,15 @@ 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))
+        (.K => traitParser(T, .TypePath, ItemAtts))
         ~> crateParser
-          ( (_Atts:InnerAttributes (_ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate
+          ( (_Atts:InnerAttributes (ItemAtts:OuterAttributes _V:MaybeVisibility T:Trait):Item Is:Items):Crate
             => (.InnerAttributes Is):Crate
           )
     rule (.K => CI:ConstantItem:KItem)
diff --git a/rust-semantics/preprocessing/initialization.md b/rust-semantics/preprocessing/initialization.md
index 4828b65..e77c750 100644
--- a/rust-semantics/preprocessing/initialization.md
+++ b/rust-semantics/preprocessing/initialization.md
@@ -7,7 +7,7 @@ module INITIALIZATION
     imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
 
     rule
-        <k> traitInitializer(Name:TypePath) => .K
+        <k> traitInitializer(Name:TypePath, Atts:OuterAttributes) => .K
             ...
         </k>
         <trait-list> .List => ListItem(Name) ...</trait-list>
@@ -16,6 +16,7 @@ module INITIALIZATION
             .Bag
             =>  <trait>
                     <trait-path> Name </trait-path>
+                    <trait-attributes> Atts </trait-attributes>
                     ...
                 </trait>
         </traits>
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 e848d55..7de2da7 100644
--- a/rust-semantics/preprocessing/syntax.md
+++ b/rust-semantics/preprocessing/syntax.md
@@ -12,11 +12,17 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX
     imports RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
 
-    syntax Initializer  ::= traitParser(Trait)
-                          | traitMethodsParser(AssociatedItems, traitName:Identifier)
+    syntax MaybeTypePath ::= ".TypePath" | TypePath
+
+    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(
@@ -28,6 +34,7 @@ module RUST-PREPROCESSING-PRIVATE-SYNTAX
                                 OuterAttributes
                             )
 
+    syntax TypePath ::= append(MaybeTypePath, Identifier)  [function, total]
 endmodule
 
 ```
diff --git a/rust-semantics/preprocessing/tools.md b/rust-semantics/preprocessing/tools.md
index 2896052..7fede8e 100644
--- a/rust-semantics/preprocessing/tools.md
+++ b/rust-semantics/preprocessing/tools.md
@@ -2,6 +2,7 @@
 
 module RUST-PREPROCESSING-TOOLS
     imports private BOOL
+    imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
     imports private RUST-REPRESENTATION
     imports private RUST-SHARED-SYNTAX
     imports private RUST-VALUE-SYNTAX
@@ -13,6 +14,16 @@ module RUST-PREPROCESSING-TOOLS
 
     rule reverse(.CallParamsList, L:CallParamsList) => L
     rule reverse((P , Ps:CallParamsList => Ps), (L:CallParamsList => P, L))
+
+    rule append(.TypePath, Name:Identifier) => Name
+    rule append(:: T:TypePathSegments, Name:Identifier) => :: appendSegments(T, Name)
+    rule append(T:TypePathSegments, Name:Identifier) => appendSegments(T, Name)
+
+    rule appendSegments(S:TypePathSegment, Name:Identifier) => S :: Name
+    rule appendSegments(S:TypePathSegment :: T:TypePathSegments, Name:Identifier)
+        => S :: appendSegments(T, Name)
+
+    syntax TypePathSegments ::= appendSegments(TypePathSegments, Identifier)  [function, total]
 endmodule
 
 ```
\ No newline at end of file
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 0fc23aa..3f3fb51 100644
--- a/rust-semantics/preprocessing/trait.md
+++ b/rust-semantics/preprocessing/trait.md
@@ -3,9 +3,13 @@
 module TRAIT
     imports private RUST-PREPROCESSING-PRIVATE-SYNTAX
 
-    rule traitParser(trait Name:Identifier { .InnerAttributes Functions:AssociatedItems })
-        => traitInitializer(Name)
-          ~> traitMethodsParser(Functions, Name)
+    rule traitParser
+            ( 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 d7636ff..26c354e 100644
--- a/rust-semantics/rust-common-syntax.md
+++ b/rust-semantics/rust-common-syntax.md
@@ -497,7 +497,8 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
 ```k
 
   syntax TupleExpression ::= "(" MaybeTupleElements ")"
-  syntax MaybeTupleElements ::= "" | TupleElements
+  syntax MaybeTupleElements ::= ""  [symbol(noTupleElements)]
+                              | TupleElements
   syntax TupleElements  ::= Expression ","
                           | Expression "," TupleElementsNoEndComma
                           | Expression "," TupleElementsNoEndComma ","