Bytes hooks

Makefile

@@ -64,7 +64,7 @@ DEMOS_TESTING_OUTPUT_DIR ::= .build/demos/output
 DEMOS_TESTING_INPUTS ::= $(wildcard $(DEMOS_TESTING_INPUT_DIR)/*.run)
 DEMOS_TESTING_OUTPUTS ::= $(patsubst $(DEMOS_TESTING_INPUT_DIR)/%,$(DEMOS_TESTING_OUTPUT_DIR)/%.executed.kore,$(DEMOS_TESTING_INPUTS))
 
-UKM_SEMANTICS_FILES ::= $(shell find mx-rust-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
+UKM_SEMANTICS_FILES ::= $(shell find ukm-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')')
 
 UKM_EXECUTION_KOMPILED ::= .build/ukm-execution-kompiled
 UKM_EXECUTION_TIMESTAMP ::= $(UKM_EXECUTION_KOMPILED)/timestamp
@@ -75,7 +75,14 @@ UKM_PREPROCESSING_TIMESTAMP ::= $(UKM_PREPROCESSING_KOMPILED)/timestamp
 UKM_TESTING_KOMPILED ::= .build/ukm-testing-kompiled
 UKM_TESTING_TIMESTAMP ::= $(UKM_TESTING_KOMPILED)/timestamp
 
-.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_CONTRACTS_TESTING_INPUT_DIR ::= tests/ukm-contracts
+
+UKM_NO_CONTRACT_TESTING_INPUT_DIR ::= tests/ukm-no-contract
+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))
+
+.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
 
@@ -96,7 +103,7 @@ build-legacy: \
 		$(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP)
 
 
-test: build syntax-test preprocessing-test execution-test crates-test
+test: build syntax-test preprocessing-test execution-test crates-test ukm-no-contracts-test
 
 test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test
 
@@ -118,6 +125,8 @@ mx-rust-two-contracts-test: $(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUTS)
 
 demos-test: $(DEMOS_TESTING_OUTPUTS)
 
+ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS)
+
 $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -373,3 +382,45 @@ $(CRATES_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 		-pTEST=$(CURDIR)/parsers/test-rust.sh
 	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
 	mv -f [email protected] $@
+
+
+# TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs
+# as a dependency
+$(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
+			$(UKM_NO_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_NO_CONTRACT_TESTING_OUTPUT_DIR)
+
+	echo "<(<" > [email protected]
+	echo "::bytes_hooks" >> [email protected]
+	echo "<|>" >> [email protected]
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> [email protected]
+	echo ">)>" >> [email protected]
+
+	# echo "<(<" > [email protected]
+	# echo "::ukm" >> [email protected]
+	# echo "<|>" >> [email protected]
+	# cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs >> [email protected]
+	# echo ">)>" >> [email protected]
+
+	echo "<(<" >> [email protected]
+	echo "$<" | sed 's%^.*/%%' | sed 's/\..*//' | sed 's/^/::/' >> [email protected]
+	echo "<|>" >> [email protected]
+	cat "$(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs" >> [email protected]
+	echo ">)>" >> [email protected]
+
+	krun \
+		[email protected] \
+		--parser $(CURDIR)/parsers/crates-ukm-testing-execution.sh \
+		--definition $(UKM_TESTING_KOMPILED) \
+		--output kore \
+		--output-file [email protected] \
+		-cTEST='$(shell cat $<)' \
+		-pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh
+	cat [email protected] | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
+	mv -f [email protected] $@

parsers/crates-ukm-testing-execution.sh

@@ -0,0 +1,5 @@
+#! /bin/bash
+
+source ${BASH_SOURCE%/*}/inc-crates.sh
+
+parse_crates .build/ukm-testing-kompiled $1

parsers/test-ukm-testing-execution.sh

@@ -0,0 +1,8 @@
+#! /bin/bash
+
+kast \
+    --output kore \
+    --definition .build/ukm-testing-kompiled \
+    --module UKM-TARGET-SYNTAX \
+    --sort ExecutionTest \
+    $1

rust-semantics/expression/expression-list.md

@@ -6,6 +6,7 @@ module RUST-EXPRESSION-EXPRESSION-LIST
     imports private RUST-VALUE-SYNTAX
 
     rule evaluate(L:ExpressionList) => evaluate(expressionListToValueList(L))
+        requires isValueWithPtr(L)
 
     rule isValueWithPtr(.ExpressionList) => true
     rule isValueWithPtr(E:Expression , T:ExpressionList)

rust-semantics/expression/tuple.md

@@ -12,8 +12,6 @@ module RUST-EXPRESSION-TUPLE
     rule (E:Expression , T:TupleElementsNoEndComma,):TupleExpression
         => tupleExpression(E , T)
 
-    syntax Instruction ::= tupleExpression(TupleElementsNoEndComma)
-
     rule (.K => evaluate(tupleElementsToExpressionList(Es)))
         ~> tupleExpression(Es:TupleElementsNoEndComma)
     rule (evaluate(L:ValueList) ~> tupleExpression(_:TupleElementsNoEndComma))

rust-semantics/helpers.md

@@ -20,8 +20,27 @@ module RUST-HELPERS
     rule isSameType(u16(_), u16) => true
     rule isSameType(i8(_), i8) => true
     rule isSameType(u8(_), u8) => true
+    rule isSameType(_:String, str) => true
     rule isSameType(struct(T, _), T:TypePath) => true
     rule isSameType(struct(T, _), T:Identifier _:GenericArgs ) => true
 
+    syntax Bool ::= isUnsignedInt(Type)  [function, total]
+    rule isUnsignedInt(_) => false [owise]
+    rule isUnsignedInt(u8) => true
+    rule isUnsignedInt(u16) => true
+    rule isUnsignedInt(u32) => true
+    rule isUnsignedInt(u64) => true
+    rule isUnsignedInt(u128) => true
+    rule isUnsignedInt(&T => T)
+
+    syntax Bool ::= isSignedInt(Type)  [function, total]
+    rule isSignedInt(_) => false [owise]
+    rule isSignedInt(u8) => true
+    rule isSignedInt(u16) => true
+    rule isSignedInt(u32) => true
+    rule isSignedInt(u64) => true
+    rule isSignedInt(u128) => true
+    rule isSignedInt(&T => T)
+
 endmodule
 ```

rust-semantics/representation.md

@@ -89,6 +89,7 @@ module RUST-REPRESENTATION
                               , reversedNormalizedParams: PtrList
                               )
                           | "clearValue"
+                          | tupleExpression(TupleElementsNoEndComma)
 
     syntax PtrList ::= reverse(PtrList, PtrList) [function, total]
 

rust-semantics/test/execution.md

@@ -10,6 +10,7 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "call" TypePath "." Identifier
                             | "call" PathInExpression
                             | "return_value"
+                            | "return_value_to_arg"
                             | "check_eq" Expression  [strict]
                             | "push" Expression [strict]
 endmodule
@@ -79,6 +80,8 @@ module RUST-EXECUTION-TEST
         <k> (V:PtrValue ~> return_value) => .K ... </k>
         <test-stack> .List => ListItem(V) ... </test-stack>
 
+    rule (V:PtrValue ~> return_value_to_arg) => push V
+
     rule
         <k> check_eq ptrValue(_, V:Value) => .K ... </k>
         <test-stack> ListItem(ptrValue(_, V)) => .List ... </test-stack>

tests/ukm-contracts/bytes_hooks.rs

@@ -0,0 +1,18 @@
+extern "C" {
+  fn empty() -> u64;
+  fn length(bytes_id: u64) -> u32;
+
+  fn append_u128(bytes_id: u64, value: u128) -> u64;
+  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_str(bytes_id: u64, value: &str) -> u64;
+
+  fn decode_u128(bytes_id: u64) -> (u64, u128);
+  fn decode_u64(bytes_id: u64) -> (u64, u64);
+  fn decode_u32(bytes_id: u64) -> (u64, u32);
+  fn decode_u16(bytes_id: u64) -> (u64, u16);
+  fn decode_u8(bytes_id: u64) -> (u64, u8);
+  fn decode_str(bytes_id: u64) -> (u64, str);
+}

tests/ukm-no-contract/test_bytes_hooks.append32.run

@@ -0,0 +1,13 @@
+push 10_u32;
+call :: test_bytes_hooks :: append_u32;
+return_value_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 3_u32;
+
+push 1000_u32;
+call :: test_bytes_hooks :: append_u32;
+return_value_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 4_u32

tests/ukm-no-contract/test_bytes_hooks.append64.run

@@ -0,0 +1,13 @@
+push 10_u64;
+call :: test_bytes_hooks :: append_u64;
+return_value_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 3_u32;
+
+push 1000_u64;
+call :: test_bytes_hooks :: append_u64;
+return_value_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 4_u32

tests/ukm-no-contract/test_bytes_hooks.appenddecode32.run

@@ -0,0 +1,9 @@
+push 10_u32;
+call :: test_bytes_hooks :: append_decode_u32;
+return_value;
+check_eq(2_u64, 10_u32);
+
+push 2_u64;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 0_u32

tests/ukm-no-contract/test_bytes_hooks.appenddecode64.run

@@ -0,0 +1,9 @@
+push 10_u64;
+call :: test_bytes_hooks :: append_decode_u64;
+return_value;
+check_eq(2_u64, 10_u32);
+
+push 2_u64;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 0_u32

tests/ukm-no-contract/test_bytes_hooks.appenddecodestr.run

@@ -0,0 +1,9 @@
+push "Hello";
+call :: test_bytes_hooks :: append_decode_str;
+return_value;
+check_eq(2_u64, "Hello");
+
+push 2_u64;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 0_u32

tests/ukm-no-contract/test_bytes_hooks.appendstr.run

@@ -0,0 +1,13 @@
+push "Hello";
+call :: test_bytes_hooks :: append_str;
+return_value_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 7_u32;
+
+push "Everyone";
+call :: test_bytes_hooks :: append_str;
+return_value_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 10_u32

tests/ukm-no-contract/test_bytes_hooks.empty.run

@@ -0,0 +1,5 @@
+call :: test_bytes_hooks :: empty;
+return_value_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+check_eq 0_u32

tests/ukm-no-contract/test_bytes_hooks.rs

@@ -0,0 +1,46 @@
+#![no_std]
+
+fn empty() -> u64 {
+    ::bytes_hooks::empty()
+}
+
+fn append_u64(v:u64) -> u64 {
+    let id = ::bytes_hooks::empty();
+    ::bytes_hooks::append_u64(id, v)
+}
+
+fn append_decode_u64(v:u64) -> (u64, u32) {
+    let id = ::bytes_hooks::empty();
+    let id = ::bytes_hooks::append_u64(id, v);
+    ::bytes_hooks::decode_u32(id)
+}
+
+fn append_u32(v:u32) -> u64 {
+    let id = ::bytes_hooks::empty();
+    ::bytes_hooks::append_u32(id, v)
+}
+
+fn append_decode_u32(v:u32) -> (u64, u32) {
+    let id = ::bytes_hooks::empty();
+    let id = ::bytes_hooks::append_u32(id, v);
+    ::bytes_hooks::decode_u32(id)
+}
+
+fn append_str(v:&str) -> u64 {
+    let id = ::bytes_hooks::empty();
+    ::bytes_hooks::append_str(id, v)
+}
+
+fn append_decode_str(v:&str) -> (u64, str) {
+    let id = ::bytes_hooks::empty();
+    let id = ::bytes_hooks::append_str(id, v);
+    ::bytes_hooks::decode_str(id)
+}
+
+fn append_decode_multi_1(v1:u32, v2:str) -> (u64, u32, str) {
+    let id = ::bytes_hooks::empty();
+    let id = ::bytes_hooks::append_u32(id, v);
+    let (id, v32) = ::bytes_hooks::decode_u32(id);
+    let (id, vstr) = ::bytes_hooks::decode_str(id);
+    (id, v32, vstr)
+}

ukm-semantics/main/configuration.md

@@ -1,8 +1,13 @@
 ```k
 
+requires "hooks/bytes.md"
+
 module UKM-CONFIGURATION
+    imports UKM-HOOKS-BYTES-CONFIGURATION
     configuration
-        <ukm> .K </ukm>
+        <ukm>
+            <ukm-bytes/>
+        </ukm>
 endmodule
 
 ```

ukm-semantics/main/execution.md

@@ -1,8 +1,10 @@
 ```k
 
 requires "execution/syntax.md"
+requires "hooks.md"
 
 module UKM-EXECUTION
+    imports private UKM-HOOKS
 endmodule
 
-```
+```

ukm-semantics/main/hooks.md

@@ -0,0 +1,9 @@
+```k
+
+requires "hooks/bytes.md"
+
+module UKM-HOOKS
+    imports private UKM-HOOKS-BYTES
+endmodule
+
+```