Pi-Squared-Inc · virgil-serbanuta · Sep 25, 2024 · Sep 13, 2024
diff --git 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 > [email protected] && mv -f [email protected] $@
@@ -196,3 +214,31 @@ $(MX_RUST_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 		-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/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
 
-```
+```
diff --git a/mx-rust-semantics/main/expression/raw-value.md 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
@@ -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
@@ -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
+        <k>
+            normalizedMethodCall
+                ( #token("MxRust#Hooks", "Identifier"):Identifier
+                , #token("MxRust#loadMxReturnValue", "Identifier"):Identifier
+                ,   ( ptr(ReturnTypeId:Int)
+                    , .PtrList
+                    )
+                )
+            => MX#popLastReturnValue(.MxValueList) ~> mxToRustTyped(T)
+            ...
+        </k>
+        <values>
+            ReturnTypeId |-> rustType(T)
+            ...
+        </values>
+
+endmodule
+
+```
diff --git 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
             ...
         </values>
 
+    rule
+        <k>
+            normalizedMethodCall
+                ( #token("MxRust#Proxy", "Identifier"):Identifier
+                    => ProxyType
+                , MethodName:Identifier
+                , (ptr(SelfId:Int) , _Params:PtrList)
+                )
+            ...
+        </k>
+        <values>
+            SelfId |-> struct
+                    ( _
+                    , #token("proxy_type", "Identifier"):Identifier |-> ProxyTypeId:Int
+                      _:Map
+                    )
+            ProxyTypeId |-> rustType(ProxyType:TypePath)
+            ...
+        </values>
+        <trait-path> ProxyType </trait-path>
+        <method-name> MethodName </method-name>
+
     syntax MxOrRustValueOrInstruction ::= MxOrRustValue | MxRustInstruction
 
     syntax RustMxInstruction ::= rustMxManagedExecuteOnDestContext

diff --git 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
@@ -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
         <mx-rust-preprocessed>
             <mx-rust-contract-trait/>
             <mx-rust-endpoint-to-function/>
+            <mx-rust-proxies/>
         </mx-rust-preprocessed>
 endmodule
 
@@ -18,6 +20,18 @@ module MX-RUST-PREPROCESSED-CONTRACT-TRAIT-CONFIGURATION
         <mx-rust-contract-trait> (#token("no#path", "Identifier"):Identifier):TypePath </mx-rust-contract-trait>  // String to Identifier
 endmodule
 
+module MX-RUST-PREPROCESSED-PROXIES-CONFIGURATION
+    imports RUST-SHARED-SYNTAX
+
+    configuration
+        <mx-rust-proxies>
+            <mx-rust-proxy multiplicity="*" type="Map">
+                <mx-rust-proxy-module> (#token("no#path", "Identifier"):Identifier):TypePath </mx-rust-proxy-module>
+                <mx-rust-proxy-trait> #token("no#path", "Identifier"):Identifier:TypePath </mx-rust-proxy-trait>
+            </mx-rust-proxy>
+        </mx-rust-proxies>
+endmodule
+
 module MX-RUST-PREPROCESSED-ENDPOINTS-CONFIGURATION
     imports MAP