Mx-rust framework and storage implementation

Makefile

@@ -27,14 +27,30 @@ MX_TESTING_OUTPUT_DIR ::= .build/mx/output
 MX_TESTING_INPUTS ::= $(wildcard $(MX_TESTING_INPUT_DIR)/**/*.mx)
 MX_TESTING_OUTPUTS ::= $(patsubst $(MX_TESTING_INPUT_DIR)/%,$(MX_TESTING_OUTPUT_DIR)/%.executed.kore,$(MX_TESTING_INPUTS))
 
-.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test
+MX_RUST_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+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))
+
+.PHONY: clean build test syntax-test preprocessing-test execution-test mx-test mx-rust-test
 
 clean:
 	rm -r .build
 
-build: $(RUST_PREPROCESSING_TIMESTAMP) $(RUST_EXECUTION_TIMESTAMP) $(MX_TESTING_TIMESTAMP)
+build: $(RUST_PREPROCESSING_TIMESTAMP) \
+				$(RUST_EXECUTION_TIMESTAMP) \
+				$(MX_TESTING_TIMESTAMP) \
+				$(MX_RUST_TIMESTAMP) \
+				$(MX_RUST_TESTING_TIMESTAMP)
 
-test: syntax-test preprocessing-test execution-test mx-test
+test: build syntax-test preprocessing-test execution-test mx-test mx-rust-test
 
 syntax-test: $(SYNTAX_OUTPUTS)
 
@@ -44,6 +60,8 @@ execution-test: $(EXECUTION_OUTPUTS)
 
 mx-test: $(MX_TESTING_OUTPUTS)
 
+mx-rust-test: $(MX_RUST_TESTING_OUTPUTS)
+
 $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -59,6 +77,22 @@ $(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES)
 	-rm -r $(MX_TESTING_KOMPILED)
 	$$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug
 
+$(MX_RUST_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
+	# Workaround for https://github.com/runtimeverification/k/issues/4141
+	-rm -r $(MX_RUST_KOMPILED)
+	$$(which kompile) mx-rust-semantics/targets/blockchain/mx-rust.md \
+			-o $(MX_RUST_KOMPILED) \
+			-I . \
+			--debug
+
+$(MX_RUST_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_TESTING_KOMPILED)
+	$$(which kompile) mx-rust-semantics/targets/testing/mx-rust.md \
+			-o $(MX_RUST_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 $@
@@ -75,7 +109,11 @@ $(PREPROCESSING_OUTPUT_DIR)/%.rs.preprocessed.kore: $(PREPROCESSING_INPUT_DIR)/%
 
 # TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
 # as a dependency
-$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: $(EXECUTION_INPUT_DIR)/%.run $(RUST_EXECUTION_TIMESTAMP)
+$(EXECUTION_OUTPUT_DIR)/%.run.executed.kore: \
+			$(EXECUTION_INPUT_DIR)/%.run \
+			$(RUST_EXECUTION_TIMESTAMP) \
+			parse-rust.sh \
+			parse-test.sh
 	mkdir -p $(EXECUTION_OUTPUT_DIR)
 	krun \
 		"$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" \
@@ -97,3 +135,22 @@ $(MX_TESTING_OUTPUT_DIR)/%.mx.executed.kore: $(MX_TESTING_INPUT_DIR)/%.mx $(MX_T
 		--output-file $@.tmp
 	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_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
+	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 \
+		--output kore \
+		--output-file $@.tmp \
+		-cTEST='$(shell cat $<)' \
+		-pTEST=$(CURDIR)/parse-mx-rust-test.sh
+	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f $@.tmp $@

mx-rust-semantics/main/configuration.md

@@ -0,0 +1,17 @@
+```k
+
+requires "mx-semantics/main/configuration.md"
+requires "rust-semantics/config.md"
+
+module MX-RUST-COMMON-CONFIGURATION
+    imports MX-COMMON-CONFIGURATION
+    imports RUST-CONFIGURATION
+
+    configuration
+        <mx-rust>
+            <mx-common/>
+            <rust/>
+        </mx-rust>
+endmodule
+
+```

mx-rust-semantics/main/expression.md

@@ -0,0 +1,9 @@
+```k
+
+requires "expression/strings.md"
+
+module MX-RUST-EXPRESSION
+    imports private MX-RUST-EXPRESSION-STRINGS
+endmodule
+
+```

mx-rust-semantics/main/expression/strings.md

@@ -0,0 +1,34 @@
+```k
+
+module MX-RUST-EXPRESSION-STRINGS
+    imports private BOOL
+    imports private INT
+    imports private MX-RUST-REPRESENTATION
+    imports private RUST-VALUE-SYNTAX
+    imports private STRING
+
+    rule concatString(ptrValue(_, S1:String), ptrValue(_, S2:String))
+          => ptrValue(null, S1 +String S2)
+
+    rule toString(ptrValue(_, i32(Value:MInt{32})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4))
+    rule toString(ptrValue(_, u32(Value:MInt{32})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 32 divInt 4))
+    rule toString(ptrValue(_, i64(Value:MInt{64})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4))
+    rule toString(ptrValue(_, u64(Value:MInt{64})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 64 divInt 4))
+    rule toString(ptrValue(_, u128(Value:MInt{128})))
+        => ptrValue(null, padLeftString(Base2String(MInt2Unsigned(Value), 16), "0", 128 divInt 4))
+    rule toString(ptrValue(null, Value:String)) => ptrValue(null, Value)
+    // TODO: convert all Value entries to string
+
+    syntax String ::= padLeftString(value:String, padding:String, count:Int)  [function, total]
+    rule padLeftString(...value:S, padding:P, count:C) => S
+        requires C <=Int lengthString(S) orBool lengthString(P) =/=Int 1
+    rule padLeftString(S:String => P +String S, P:String, _Count:Int)
+        [owise]
+
+endmodule
+
+```

mx-rust-semantics/main/glue.md

@@ -0,0 +1,50 @@
+```k
+
+module MX-RUST-GLUE
+  imports private COMMON-K-CELL
+  imports private MX-COMMON-SYNTAX
+  imports private RUST-EXECUTION-CONFIGURATION
+  imports private RUST-VALUE-SYNTAX
+  imports private MX-RUST-REPRESENTATION
+
+  rule
+      <k>
+          storeHostValue
+              (... destination: rustDestination(ValueId, _:MxRustType)
+              , value: wrappedRust(V:Value)
+              )
+          => .K
+          ...
+      </k>
+      <values> Values:Map => Values[ValueId <- V] </values>
+      requires ValueId >=Int 0
+
+  rule
+      (.K => mxRustEmptyValue(T))
+      ~>  storeHostValue
+              (... destination: rustDestination(_, T:MxRustType)
+              , value: mxWrappedEmpty
+              )
+  rule
+      (ptrValue(_, V:Value) => .K)
+      ~>   storeHostValue
+              (... value: mxWrappedEmpty => wrappedRust(V)
+              )
+
+  rule
+      <k>
+          mxRustLoadPtr(P:Int) => ptrValue(ptr(P), V)
+          ...
+      </k>
+      <values> P |-> V:Value ... </values>
+
+    rule
+        <k> mxRustNewValue(V:Value) => ptrValue(ptr(NextId), V) ... </k>
+        <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
+        <values> Values:Map => Values[NextId <- V] </values>
+
+    rule mxIntValue(I:Int) ~> mxValueToRust(T:Type)
+        => mxRustNewValue(integerToValue(I, T))
+endmodule
+
+```

mx-rust-semantics/main/modules.md

@@ -0,0 +1,11 @@
+```k
+
+requires "modules/biguint.md"
+requires "modules/storage.md"
+
+module MX-RUST-MODULES
+    imports private MX-RUST-MODULES-BIGUINT
+    imports private MX-RUST-MODULES-STORAGE
+endmodule
+
+```

mx-rust-semantics/main/modules/biguint.md

@@ -0,0 +1,48 @@
+```k
+
+module MX-RUST-MODULES-BIGUINT
+    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("BigUint", "Identifier"):Identifier
+                , #token("from", "Identifier"):Identifier
+                ,   ( ptr(ValueId:Int)
+                    , .NormalizedCallParams
+                    )
+                )
+            // TODO: Should check that V >= 0
+            => mxRustBigIntNew(valueToInteger(V))
+            ...
+        </k>
+        <values> ValueId |-> V:Value ... </values>
+
+  // --------------------------------------
+
+    syntax MxRustInstruction  ::= mxRustBigIntNew(IntOrError)
+                                | "mxRustCreateBigUint"
+
+    rule mxRustBigIntNew(V:Int)
+        => MX#bigIntNew(mxIntValue(V))
+            ~> mxValueToRust(i32)
+            ~> mxRustCreateBigUint
+
+    rule ptrValue(ptr(BigUintId:Int), _) ~> mxRustCreateBigUint
+        => mxRustNewValue
+            ( struct
+                ( #token("BigUint", "Identifier"):Identifier
+                , #token("mx_biguint_id", "Identifier"):Identifier |-> BigUintId
+                )
+            )
+
+    rule mxRustEmptyValue(BigUint) => mxRustBigIntNew(0)
+
+endmodule
+
+```

mx-rust-semantics/main/modules/storage.md

@@ -0,0 +1,113 @@
+```k
+
+module MX-RUST-MODULES-STORAGE
+    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("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+            , #token("new", "Identifier"):Identifier
+            ,   ( ptr(KeyId:Int)
+                , ptr(ResultTypeId:Int)
+                , .NormalizedCallParams
+                )
+            )
+        => mxRustNewValue
+            ( struct
+                ( Type
+                , #token("storage_key", "Identifier"):Identifier |-> KeyId
+                    #token("result_type", "Identifier"):Identifier |-> ResultTypeId
+                )
+            )
+
+    rule
+        <k>
+            normalizedMethodCall
+                ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+                , #token("set", "Identifier"):Identifier
+                ,   ( ptr(SelfId:Int)
+                    , ptr(ValueId:Int)
+                    , .NormalizedCallParams
+                    )
+                )
+            => MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
+            ...
+        </k>
+        <values>
+            SelfId |-> struct
+                        ( Type
+                        , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
+                            _:Map
+                        )
+            StorageKeyId |-> StorageKey:String
+            ValueId |-> V:Value
+            ...
+        </values>
+
+    rule
+        <k>
+            normalizedMethodCall
+                ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+                , #token("set_if_empty", "Identifier"):Identifier
+                ,   ( ptr(SelfId:Int)
+                    , ptr(ValueId:Int)
+                    , .NormalizedCallParams
+                    )
+                )
+            => MX#storageLoad(mxStringValue(StorageKey), rustDestination(-1, noType))
+                ~> setIfEmpty
+                ~> MX#storageStore(mxStringValue(StorageKey), wrappedRust(V))
+            ...
+        </k>
+        <values>
+            SelfId |-> struct
+                        ( Type
+                        , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
+                            _:Map
+                        )
+            StorageKeyId |-> StorageKey:String
+            ValueId |-> V:Value
+            ...
+        </values>
+
+    rule mxRustEmptyValue(noType) ~> storeHostValue(...) ~> setIfEmpty
+        => .K
+    rule storeHostValue(... value: wrappedRust(_))
+          ~> setIfEmpty ~> MX#storageStore(_)
+        => .K
+
+    rule
+        <k>
+            normalizedMethodCall
+                ( #token("SingleValueMapper", "Identifier"):Identifier #as Type:Identifier
+                , #token("get", "Identifier"):Identifier
+                ,   ( ptr(SelfId:Int)
+                    , .NormalizedCallParams
+                    )
+                )
+            => MX#storageLoad(mxStringValue(StorageKey), rustDestination(NextId, ResultType))
+                ~> mxRustLoadPtr(NextId)
+            ...
+        </k>
+        <values>
+            SelfId |-> struct
+                        ( Type
+                        , #token("storage_key", "Identifier"):Identifier |-> StorageKeyId:Int
+                            #token("result_type", "Identifier"):Identifier |-> ResultTypeId:Int
+                            _:Map
+                        )
+            StorageKeyId |-> StorageKey:String
+            ResultTypeId |-> ResultType:MxRustType
+            ...
+        </values>
+        <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
+
+    syntax MxRustInstruction ::= "setIfEmpty"
+endmodule
+
+```