Pi-Squared-Inc · virgil-serbanuta · Oct 8, 2024
diff --git a/Makefile b/Makefile
@@ -82,6 +82,11 @@ UKM_NO_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-no-contract/output
 UKM_NO_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/*.run)
 UKM_NO_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_NO_CONTRACT_TESTING_INPUTS))
 
+UKM_WITH_CONTRACT_TESTING_INPUT_DIR ::= tests/ukm-with-contract
+UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-with-contract/output
+UKM_WITH_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/*.run)
+UKM_WITH_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_WITH_CONTRACT_TESTING_INPUTS))
+
 .PHONY: clean build build-legacy test test-legacy syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test ukm-no-contracts-test
 
 all: build test
@@ -127,6 +132,8 @@ demos-test: $(DEMOS_TESTING_OUTPUTS)
 
 ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS)
 
+ukm-with-contracts-test: $(UKM_WITH_CONTRACT_TESTING_OUTPUTS)
+
 $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -424,3 +431,51 @@ $(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 		-pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh
 	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f $@.tmp $@
+
+
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
+# as a dependency
+$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+			$(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%.run \
+			$(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs \
+			$(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs \
+			$(UKM_TESTING_TIMESTAMP) \
+			$(wildcard parsers/inc-*.sh) \
+			parsers/crates-ukm-testing-execution.sh \
+			parsers/test-ukm-testing-execution.sh
+	mkdir -p $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)
+
+	echo "<(<" > $@.in.tmp
+	echo "::bytes_hooks" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+
+	echo "<(<" >> $@.in.tmp
+	echo "::state_hooks" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/state_hooks.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+
+	echo "<(<" >> $@.in.tmp
+	echo "::ukm" >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+
+	echo "<(<" >> $@.in.tmp
+	echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/' >> $@.in.tmp
+	echo "<|>" >> $@.in.tmp
+	cat "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" >> $@.in.tmp
+	echo ">)>" >> $@.in.tmp
+
+	krun \
+		$@.in.tmp \
+		--parser $(CURDIR)/parsers/crates-ukm-testing-execution.sh \
+		--definition $(UKM_TESTING_KOMPILED) \
+		--output kore \
+		--output-file $@.tmp \
+		-cTEST='$(shell cat $<)' \
+		-pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh
+	cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f $@.tmp $@
diff --git a/mx-rust-semantics/main/preprocessing/configuration.md b/mx-rust-semantics/main/preprocessing/configuration.md
@@ -17,7 +17,7 @@ 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
+        <mx-rust-contract-trait> (#token("no#path", "Identifier"):Identifier):TypePath </mx-rust-contract-trait>
 endmodule
 
 module MX-RUST-PREPROCESSED-PROXIES-CONFIGURATION

diff --git a/rust-semantics/error.md b/rust-semantics/error.md
@@ -5,6 +5,8 @@ module RUST-ERROR-SYNTAX
 
     syntax ValueListOrError ::= concat(ValueOrError, ValueListOrError)  [function, total]
     syntax PtrListOrError ::= concat(Ptr, PtrListOrError)  [function, total]
+    syntax StringOrError ::= concat(StringOrError, StringOrError)  [function, total]
+    syntax NonEmptyStatementsOrError ::= concat(NonEmptyStatementsOrError, NonEmptyStatementsOrError)  [function, total]
     syntax PtrValueOrError ::= wrapPtrValueOrError(Ptr, ValueOrError)  [function, total]
     syntax TypePathOrError ::= doubleColonOrError(TypePathSegmentsOrError)  [function, total]
     syntax TypePathOrError ::= injectOrError(TypePathSegmentsOrError) [function, total]
@@ -22,10 +24,18 @@ module RUST-ERROR
     rule concat(V:Value, L:ValueList) => V , L
     rule concat(_:Value, E:SemanticsError) => E
     rule concat(E:SemanticsError, _:ValueListOrError) => E
-    rule concat(E:ValueOrError, L:ValueListOrError)
-        => error("unexpected branch (concat(ValueOrError, ValueListOrError))", ListItem(E) ListItem(L))
+
+    rule concat(S1:String:StringOrError, S2:String:StringOrError) => S1 +String S2
+    rule concat(_:String:StringOrError, E:SemanticsError:StringOrError) => E
+    rule concat(E:SemanticsError:StringOrError, _:StringOrError) => E
+    rule concat(S1:StringOrError, S2:StringOrError)
+        => error("concat(StringOrError, StringOrError): Unknown error", ListItem(S1) ListItem(S2))
         [owise]
 
+    rule concat(S1:NonEmptyStatements, S2:NonEmptyStatements) => concatNonEmptyStatements(S1, S2)
+    rule concat(_:NonEmptyStatements, E:SemanticsError) => E
+    rule concat(E:SemanticsError, _:NonEmptyStatementsOrError) => E
+
     rule wrapPtrValueOrError(P:Ptr, V:Value) => ptrValue(P, V)
     rule wrapPtrValueOrError(_:Ptr, E:SemanticsError) => E
 
@@ -38,9 +48,9 @@ module RUST-ERROR
     rule concat(_:TypePathSegment, E) => E
     rule concat(S:TypePathSegment, Ss:TypePathSegments) => S :: Ss
 
-    rule andOrError(_:ExpressionOrError, E:SemanticsError) => E
-    rule andOrError(E:SemanticsError, _:Expression) => E
-    rule andOrError(E1:Expression, E2:Expression) => E1 && E2
+    rule andOrError(_:ExpressionOrError, e(E:SemanticsError)) => e(E)
+    rule andOrError(e(E:SemanticsError), v(_:Expression)) => e(E)
+    rule andOrError(v(E1:Expression), v(E2:Expression)) => v(E1 && E2)
 
     rule tupleOrError(L:ValueList) => tuple(L)
     rule tupleOrError(E:SemanticsError) => E

diff --git a/rust-semantics/expression/comparisons.md b/rust-semantics/expression/comparisons.md
@@ -32,17 +32,17 @@ module RUST-EXPRESSION-STRUCT-COMPARISONS
     syntax ExpressionOrError ::= allPtrEquality(PtrListOrError, PtrListOrError)
                                   [function, total]
 
-    rule allPtrEquality(E:SemanticsError, _:PtrListOrError) => E
-    rule allPtrEquality(_:PtrList, E:SemanticsError) => E
+    rule allPtrEquality(E:SemanticsError, _:PtrListOrError) => e(E)
+    rule allPtrEquality(_:PtrList, E:SemanticsError) => e(E)
 
-    rule allPtrEquality(.PtrList, .PtrList) => true
+    rule allPtrEquality(.PtrList, .PtrList) => v(true)
     rule allPtrEquality((P:Ptr , Ps:PtrList), (Q:Ptr , Qs:PtrList))
-        => andOrError(P == Q , allPtrEquality(Ps, Qs))
+        => andOrError(v(P == Q) , allPtrEquality(Ps, Qs))
 
     rule allPtrEquality(.PtrList, (_:Ptr , _:PtrList) #as Ps:PtrList)
-        => error("allPtrEquality: Second list too long", ListItem(Ps))
+        => e(error("allPtrEquality: Second list too long", ListItem(Ps)))
     rule allPtrEquality((_:Ptr , _:PtrList) #as Ps:PtrList, .PtrList)
-        => error("zip(PtrList): First list too long", ListItem(Ps))
+        => e(error("zip(PtrList): First list too long", ListItem(Ps)))
 
 endmodule
 

diff --git a/rust-semantics/expression/struct.md b/rust-semantics/expression/struct.md
@@ -57,9 +57,9 @@ module RUST-EXPRESSION-STRUCT
     rule <k> 
             fromStructExpressionWithAssignmentsBuildFieldsMap(
                     Name:TypePath, 
-                    ((FieldName:Identifier : LE:Expression):StructExprField, RS):StructExprFields,
+                    ((FieldName:Identifier : Le:Expression):StructExprField, RS):StructExprFields,
                     FieldsMap:Map)
-                => LE ~> FieldName ~> fromStructExpressionWithAssignmentsBuildFieldsMap(Name, RS, FieldsMap)
+                => Le ~> FieldName ~> fromStructExpressionWithAssignmentsBuildFieldsMap(Name, RS, FieldsMap)
             ...
         </k>
 

diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md
@@ -42,5 +42,8 @@ module RUST-HELPERS
     rule isSignedInt(u128) => true
     rule isSignedInt(&T => T)
 
+    rule concatNonEmptyStatements(.NonEmptyStatements, S:NonEmptyStatements) => S
+    rule concatNonEmptyStatements(S:Statement Ss1:NonEmptyStatements, Ss2:NonEmptyStatements)
+        => S concatNonEmptyStatements(Ss1, Ss2)
 endmodule
 ```
diff --git a/rust-semantics/preprocessing/configuration.md b/rust-semantics/preprocessing/configuration.md
@@ -4,8 +4,6 @@ module RUST-PREPROCESSING-CONFIGURATION
     imports private RUST-REPRESENTATION
     imports private RUST-SHARED-SYNTAX
 
-    syntax Identifier ::= "my_identifier"  [token]
-
     configuration
         <preprocessed>
             <constants>
@@ -17,7 +15,7 @@ module RUST-PREPROCESSING-CONFIGURATION
             <struct-list> .List </struct-list>
             <structs>
                 <struct multiplicity="*" type="Map">
-                    <struct-path> my_identifier:TypePath </struct-path> 
+                    <struct-path> #token("not#initialized", "Identifier"):Identifier:TypePath </struct-path> 
                     <field-list> .List </field-list>  // List of Identifier
                     <fields>
                         <field multiplicity="*" type="Map">
@@ -30,14 +28,14 @@ module RUST-PREPROCESSING-CONFIGURATION
             <trait-list> .List </trait-list>  // List of TypePath
             <traits>
                 <trait multiplicity="*" type="Map">
-                    <trait-path> my_identifier:TypePath </trait-path>
+                    <trait-path> #token("not#initialized", "Identifier"):Identifier:TypePath </trait-path>
                     <trait-attributes> `emptyOuterAttributes`(.KList):OuterAttributes </trait-attributes>
                     <method-list> .List </method-list>  // List of Identifier
                 </trait>
             </traits>
             <methods>
                 <method multiplicity="*" type="Map">
-                    <method-name> my_identifier:PathInExpression </method-name>
+                    <method-name> #token("not#initialized", "Identifier"):Identifier:PathInExpression </method-name>
                     <method-params> .NormalizedFunctionParameterList </method-params>
                     <method-return-type> ():Type </method-return-type>
                     <method-implementation> empty:FunctionBodyRepresentation </method-implementation>

diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
@@ -98,7 +98,7 @@ module RUST-REPRESENTATION
     syntax MapOrError ::= Map | SemanticsError
 
     syntax Expression ::= Ptr
-    syntax ExpressionOrError ::= Expression | SemanticsError
+    syntax ExpressionOrError ::= v(Expression) | e(SemanticsError)
 
     syntax NormalizedFunctionParameterListOrError ::= NormalizedFunctionParameterList | SemanticsError
 
@@ -129,7 +129,10 @@ module RUST-REPRESENTATION
     syntax IntOrError ::= valueToInteger(Value)  [function, total]
     syntax ValueOrError ::= integerToValue(Int, Type)  [function, total]
 
+    syntax StringOrError ::= String | SemanticsError
+
     syntax String ::= IdentifierToString(Identifier)  [function, total, hook(STRING.token2string)]
+    syntax Identifier ::= StringToIdentifier(String)  [function, total, hook(STRING.string2token)]
 
     syntax CallParamsList ::= reverse(CallParamsList, CallParamsList)  [function, total]
 
@@ -175,6 +178,9 @@ module RUST-REPRESENTATION
 
     syntax TypePath ::= append(MaybeTypePath, Identifier)  [function, total]
 
+    syntax NonEmptyStatementsOrError ::= NonEmptyStatements | SemanticsError
+    syntax NonEmptyStatements ::= concatNonEmptyStatements(NonEmptyStatements, NonEmptyStatements)  [function, total]
+
 endmodule
 
 ```
diff --git a/rust-semantics/rust-common-syntax.md b/rust-semantics/rust-common-syntax.md
@@ -197,8 +197,8 @@ https://doc.rust-lang.org/reference/items/extern-crates.html
   syntax Struct ::= StructStruct | TupleStruct
   syntax TupleStruct ::= "TODO: not needed yet, not implementing"
   syntax StructStruct ::= "struct" Identifier MaybeGenericParams MaybeWhereClause "{" MaybeStructFields "}"
-  syntax MaybeStructFields ::= "" | StructFields
-  syntax StructFields ::= List{StructField, ","}
+  syntax MaybeStructFields ::= "" | StructFields | StructFields ","
+  syntax StructFields ::= NeList{StructField, ","}
   syntax StructField ::= OuterAttributes MaybeVisibility Identifier ":" Type //TODO: Outerfields and visibility for 
                                                                              //struct fields is not yet supported.
 

diff --git a/rust-semantics/test/configuration.md b/rust-semantics/test/configuration.md
@@ -6,6 +6,7 @@ module RUST-EXECUTION-TEST-CONFIGURATION
     configuration
         <rust-test>
             <test-stack> .List </test-stack>
+            <mocks> .Map </mocks>
         </rust-test>
 endmodule
 

diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
@@ -13,6 +13,7 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "return_value_to_arg"
                             | "check_eq" Expression  [strict]
                             | "push" Expression [strict]
+    syntax KItem ::= mock(KItem, K)
 endmodule
 
 module RUST-EXECUTION-TEST
@@ -92,6 +93,16 @@ module RUST-EXECUTION-TEST
         <values> VALUES:Map => VALUES[NVI <- V] </values>
         <next-value-id> NVI:Int => NVI +Int 1 </next-value-id>
 
+    syntax KItem ::= wrappedK(K)
+
+    rule
+        <k> mock(Mocked:KItem, Result:K) => .K ... </k>
+        <mocks> M:Map => M[Mocked <- wrappedK(Result)] </mocks>
+
+    rule
+        <k> (Mocked:KItem => Result) ...</k>
+        <mocks> Mocked |-> wrappedK(Result:K) ...</mocks>
+        [priority(10)]
 endmodule
 
 ```
diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs
@@ -6,7 +6,7 @@ extern "C" {
   fn append_u64(bytes_id: u64, value: u64) -> u64;
   fn append_u32(bytes_id: u64, value: u32) -> u64;
   fn append_u16(bytes_id: u64, value: u16) -> u64;
-  fn append_u7(bytes_id: u64, value: u8) -> u64;
+  fn append_u8(bytes_id: u64, value: u8) -> u64;
   fn append_str(bytes_id: u64, value: &str) -> u64;
 
   fn decode_u128(bytes_id: u64) -> (u64, u128);

diff --git a/tests/ukm-contracts/state_hooks.rs b/tests/ukm-contracts/state_hooks.rs
@@ -0,0 +1,4 @@
+extern "C" {
+  fn setStatus(status: u64);
+  fn setOutput(bytes_id: u64);
+}
diff --git a/tests/ukm-contracts/ukm.rs b/tests/ukm-contracts/ukm.rs
@@ -1,7 +1,7 @@
 #![no_std]
 
 // TODO: Support structs and figure out the content of MessageResult
-struct MessageResult { }
+struct MessageResult { gas: u64 }
 
 pub const EVMC_REJECTED: u64 = 0_u64;
 pub const EVMC_INTERNAL_ERROR: u64 = 1_u64;

diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run
@@ -0,0 +1,23 @@
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "myEndpoint(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 123_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: endpoints :: decode_single_u64;
+return_value;
+
+check_eq 126_u64
+
diff --git a/tests/ukm-with-contract/endpoints.rs b/tests/ukm-with-contract/endpoints.rs
@@ -0,0 +1,23 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use ukm::*;
+
+#[ukm::contract]
+pub trait Endpoints {
+    #[init]
+    fn init(&self) {}
+
+    #[endpoint(myEndpoint)]
+    fn endpoint(&self, value: u64) -> u64 {
+        value + 3_u64
+    }
+}
+
+fn decode_single_u64(bytes_id: u64) -> u64 {
+    let (remaining_id, value) = :: bytes_hooks :: decode_u64(bytes_id);
+    if :: bytes_hooks :: length(remaining_id) > 0_u32 {
+        fail();
+    };
+    value
+}
diff --git a/ukm-semantics/main/configuration.md b/ukm-semantics/main/configuration.md
@@ -1,12 +1,15 @@
 ```k
 
 requires "hooks/bytes.md"
+requires "hooks/state.md"
 
 module UKM-CONFIGURATION
     imports UKM-HOOKS-BYTES-CONFIGURATION
+    imports UKM-HOOKS-STATE-CONFIGURATION
     configuration
         <ukm>
             <ukm-bytes/>
+            <ukm-state/>
         </ukm>
 endmodule
 

diff --git a/ukm-semantics/main/execution.md b/ukm-semantics/main/execution.md
@@ -1,10 +1,14 @@
 ```k
 
+requires "execution/dispatch.md"
 requires "execution/syntax.md"
 requires "hooks.md"
+requires "representation.md"
 
 module UKM-EXECUTION
+    imports private UKM-EXECUTION-DISPATCH
     imports private UKM-HOOKS
+    imports private UKM-REPRESENTATION
 endmodule
 
 ```