Merge branch 'main' into rename-ncp

Pi-Squared-Inc · Sep 23, 2024 · 0c665cc · 0c665cc
2 parents 00e6489 + 067c58f
commit 0c665cc
Show file tree

Hide file tree

Showing 38 changed files with 270 additions and 99 deletions.
diff --git a/Makefile b/Makefile
@@ -132,17 +132,18 @@ $(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
+			$(wildcard parsers/inc-*.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,17 +162,18 @@ $(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
+			$(wildcard parsers/inc-*.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 $@
 
@@ -181,18 +183,20 @@ $(MX_RUST_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 $(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
+			$(wildcard parsers/inc-*.sh) \
+			parsers/args-mx-rust-contract.sh \
+			parsers/contract-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 $@
diff --git a/mx-rust-semantics/main/calls/configuration.md b/mx-rust-semantics/main/calls/configuration.md
@@ -7,10 +7,6 @@ module MX-RUST-CALLS-CONFIGURATION
     configuration
         <mx-rust-calls>
             <rust-execution-state-stack> .List </rust-execution-state-stack>
-            <mx-rust-endpoint-to-function> .Map </mx-rust-endpoint-to-function>  // String to Identifier
-
-            // Valid only while a contract call is being prepared
-            <mx-rust-last-trait-name> (#token("no#path", "Identifier"):Identifier):TypePath </mx-rust-last-trait-name>
         </mx-rust-calls>
 endmodule
 

diff --git a/mx-rust-semantics/main/calls/implementation.md b/mx-rust-semantics/main/calls/implementation.md
@@ -5,6 +5,8 @@ module MX-RUST-CALLS-IMPLEMENTATION
     imports private MX-CALL-CONFIGURATION
     imports private MX-COMMON-SYNTAX
     imports private MX-RUST-CALLS-CONFIGURATION
+    imports private MX-RUST-PREPROCESSED-ENDPOINTS-CONFIGURATION
+    imports private MX-RUST-PREPROCESSED-CONFIGURATION
     imports private MX-RUST-REPRESENTATION
     imports private RUST-EXECUTION-CONFIGURATION
     imports private RUST-PREPROCESSING-CONFIGURATION
@@ -45,16 +47,14 @@ module MX-RUST-CALLS-IMPLEMENTATION
         <k>
             host.newEnvironment
                 ( rustCode
-                    ( EndpointToFunction:Map
-                    , TraitName:TypePath
+                    ( MxRustPreprocessed:MxRustPreprocessedCell
                     , Preprocessed:PreprocessedCell
                     )
                 )
             => .K
             ...
         </k>
-        <mx-rust-last-trait-name> _ => TraitName </mx-rust-last-trait-name>
-        <mx-rust-endpoint-to-function> _ => EndpointToFunction </mx-rust-endpoint-to-function>
+        (_:MxRustPreprocessedCell => MxRustPreprocessed)
         (_:PreprocessedCell => Preprocessed)
 
     rule
@@ -68,10 +68,7 @@ module MX-RUST-CALLS-IMPLEMENTATION
         <mx-rust-endpoint-to-function>
             FunctionName |-> Endpoint:Identifier ...
         </mx-rust-endpoint-to-function>
-        <mx-rust-last-trait-name>
-            TraitName:TypePath
-            => (#token("no#path", "Identifier"):Identifier):TypePath
-        </mx-rust-last-trait-name>
+        <mx-rust-contract-trait> TraitName:TypePath </mx-rust-contract-trait>
         <mx-call-args> Args:MxValueList </mx-call-args>
         <trait-path> TraitName </trait-path>
         <method-name> Endpoint </method-name>

diff --git a/mx-rust-semantics/main/configuration.md b/mx-rust-semantics/main/configuration.md
@@ -2,18 +2,21 @@
 
 requires "calls/configuration.md"
 requires "mx-semantics/main/configuration.md"
+requires "preprocessing/configuration.md"
 requires "rust-semantics/config.md"
 
 module MX-RUST-COMMON-CONFIGURATION
     imports MX-COMMON-CONFIGURATION
     imports MX-RUST-CALLS-CONFIGURATION
+    imports MX-RUST-PREPROCESSED-CONFIGURATION
     imports RUST-CONFIGURATION
 
     configuration
         <mx-rust>
+            <mx-rust-calls/>
+            <mx-rust-preprocessed/>
             <mx-common/>
             <rust/>
-            <mx-rust-calls/>
         </mx-rust>
 endmodule
 

diff --git a/mx-rust-semantics/main/preprocessing/configuration.md b/mx-rust-semantics/main/preprocessing/configuration.md
@@ -0,0 +1,27 @@
+```k
+
+module MX-RUST-PREPROCESSED-CONFIGURATION
+    imports MX-RUST-PREPROCESSED-CONTRACT-TRAIT-CONFIGURATION
+    imports MX-RUST-PREPROCESSED-ENDPOINTS-CONFIGURATION
+
+    configuration
+        <mx-rust-preprocessed>
+            <mx-rust-contract-trait/>
+            <mx-rust-endpoint-to-function/>
+        </mx-rust-preprocessed>
+endmodule
+
+module MX-RUST-PREPROCESSED-CONTRACT-TRAIT-CONFIGURATION
+    imports RUST-SHARED-SYNTAX
+
+    configuration
+        <mx-rust-contract-trait> (#token("no#path", "Identifier"):Identifier):TypePath </mx-rust-contract-trait>  // String to Identifier
+endmodule
+
+module MX-RUST-PREPROCESSED-ENDPOINTS-CONFIGURATION
+    imports MAP
+
+    configuration
+        <mx-rust-endpoint-to-function> .Map </mx-rust-endpoint-to-function>  // String to Identifier
+endmodule
+```
diff --git a/mx-rust-semantics/main/preprocessing/methods.md b/mx-rust-semantics/main/preprocessing/methods.md
@@ -5,6 +5,7 @@ module MX-RUST-PREPROCESSING-METHODS
     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-REPRESENTATION
     imports private RUST-PREPROCESSING-CONFIGURATION
     imports private RUST-REPRESENTATION

diff --git a/mx-rust-semantics/main/preprocessing/traits.md b/mx-rust-semantics/main/preprocessing/traits.md
@@ -3,20 +3,43 @@
 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-REPRESENTATION
     imports private RUST-PREPROCESSING-CONFIGURATION
     imports private RUST-SHARED-SYNTAX
 
-    syntax MxRustInstruction  ::= mxRustPreprocessTraits(List)
+    syntax MxRustInstruction  ::= mxRustPreprocessAddTraits(List)
+                                | mxRustPreprocessAddTrait(TypePath)
+                                | mxRustPreprocessTraits(List)
                                 | mxRustPreprocessTrait(TypePath)
 
     rule
         <k>
-            mxRustPreprocessTraits => mxRustPreprocessTraits(Traits)
+            mxRustPreprocessTraits
+            => mxRustPreprocessAddTraits(Traits) ~> mxRustPreprocessTraits(Traits)
             ...
         </k>
         <trait-list> Traits:List </trait-list>
 
+    rule mxRustPreprocessAddTraits(.List) => .K
+    rule mxRustPreprocessAddTraits(ListItem(Trait:TypePath) Traits:List)
+        => mxRustPreprocessAddTrait(Trait) ~> mxRustPreprocessAddTraits(Traits)
+
+    rule
+        <k>
+            mxRustPreprocessAddTrait(Trait:TypePath) => .K
+            ...
+        </k>
+        <trait-path> Trait </trait-path>
+        <trait-attributes>
+            #[ #token("multiversx_sc", "Identifier")
+                :: #token("contract", "Identifier")
+                :: .SimplePathList
+            ]
+            .NonEmptyOuterAttributes
+        </trait-attributes>
+        <mx-rust-contract-trait> _ => Trait </mx-rust-contract-trait>
+
     rule mxRustPreprocessTraits(.List) => .K
     rule mxRustPreprocessTraits(ListItem(Trait:TypePath) Traits:List)
         => mxRustPreprocessTrait(Trait) ~> mxRustPreprocessTraits(Traits)

diff --git a/mx-rust-semantics/main/representation.md b/mx-rust-semantics/main/representation.md
@@ -33,8 +33,9 @@ module MX-RUST-REPRESENTATION
 
     syntax MxValue ::= rustDestination(Int, MxRustType)
 
+    syntax MxRustPreprocessedCell
     syntax PreprocessedCell
-    syntax ContractCode ::= rustCode(endpointToFunction: Map, type: TypePath, preprocessed: PreprocessedCell)
+    syntax ContractCode ::= rustCode(MxRustPreprocessedCell,  PreprocessedCell)
 endmodule
 
 ```
diff --git a/mx-rust-semantics/setup/mx.md b/mx-rust-semantics/setup/mx.md
@@ -3,7 +3,7 @@
 module MX-RUST-SETUP-MX
     imports private COMMON-K-CELL
     imports private MX-COMMON-SYNTAX
-    imports private MX-RUST-CALLS-CONFIGURATION
+    imports private MX-RUST-PREPROCESSED-CONFIGURATION
     imports private MX-RUST-REPRESENTATION
     imports private MX-SETUP-SYNTAX
     imports private RUST-PREPROCESSING-CONFIGURATION
@@ -16,7 +16,7 @@ module MX-RUST-SETUP-MX
                                       "," gasLimit: Int
                                       "," args: MxValueList
                                       ")"
-    syntax MXRustInstruction  ::= "MxRust#addAccountWithPreprocessedCode" "(" String "," TypePath ")"
+    syntax MXRustInstruction  ::= "MxRust#addAccountWithPreprocessedCode" "(" String ")"
                                 | "MxRust#clearMxReturnValue"
 
     rule mxRustCreateAccount(Address:String) => MXSetup#add_account(Address)
@@ -59,7 +59,7 @@ module MX-RUST-SETUP-MX
                 , gasLimit: GasLimit:Int
                 , args: Args:MxValueList
                 )
-            => MxRust#addAccountWithPreprocessedCode(Contract, TraitName)
+            => MxRust#addAccountWithPreprocessedCode(Contract)
               ~> callContract
                   ( "#init"
                   , prepareIndirectContractCallInput
@@ -75,20 +75,19 @@ module MX-RUST-SETUP-MX
               ~> MxRust#clearMxReturnValue
             ...
         </k>
-        <preprocessed> ... <trait-list> ListItem(TraitName:TypePath) </trait-list>  </preprocessed>
 
     rule
         <k>
-            MxRust#addAccountWithPreprocessedCode(Contract, TraitName)
+            MxRust#addAccountWithPreprocessedCode(Contract)
             => MxRust#clearPreprocessed
                 ~> MXSetup#add_account_with_code
                     ( Contract
-                    , rustCode(EndpointToFunction, TraitName, Preprocessed)
+                    , rustCode(MxRustPreprocessed, Preprocessed)
                     )
             ...
         </k>
         Preprocessed:PreprocessedCell
-        <mx-rust-endpoint-to-function> EndpointToFunction:Map </mx-rust-endpoint-to-function>
+        MxRustPreprocessed:MxRustPreprocessedCell
 
     syntax MXRustInstruction ::= "MxRust#clearPreprocessed"
     rule
@@ -99,7 +98,12 @@ module MX-RUST-SETUP-MX
         (_:PreprocessedCell
         => <preprocessed> ... <trait-list> .List </trait-list>  </preprocessed>
         )
-        <mx-rust-endpoint-to-function> _ => .Map </mx-rust-endpoint-to-function>
+        (_:MxRustPreprocessedCell
+        =>  <mx-rust-preprocessed>
+                <mx-rust-endpoint-to-function> .Map </mx-rust-endpoint-to-function>
+                ...
+            </mx-rust-preprocessed>
+        )
 
     rule _V:MxValue ~> MxRust#clearMxReturnValue => .K
 

diff --git a/parse-mx-rust-contract-args.sh b/parse-mx-rust-contract-args.sh
diff --git a/parse-mx-rust-contract-test.sh b/parse-mx-rust-contract-test.sh
diff --git a/parse-mx-rust-contract.sh b/parse-mx-rust-contract.sh
diff --git a/parse-mx-rust-test.sh b/parse-mx-rust-test.sh
diff --git a/parse-mx-rust.sh b/parse-mx-rust.sh
diff --git a/parse-rust.sh b/parse-rust.sh
diff --git a/parsers/args-mx-rust-contract.sh 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/contract-mx-rust-contract.sh 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.sh 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
@@ -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
@@ -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
@@ -0,0 +1,8 @@
+function parse_endpoint_args() {
+    kast \
+        --output kore \
+        --definition $1 \
+        --module MX-RUST-SYNTAX \
+        --sort MxValueList \
+        $2
+}