diff --git a/Makefile b/Makefile
index 21d8493..3a1416b 100644
--- a/Makefile
+++ b/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 $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())"
mv -f $@.tmp $@
+
+
+# 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 "<(<" > $@.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 "::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/parsers/crates-ukm-testing-execution.sh b/parsers/crates-ukm-testing-execution.sh
new file mode 100755
index 0000000..5c0d00e
--- /dev/null
+++ b/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
diff --git a/parsers/test-ukm-testing-execution.sh b/parsers/test-ukm-testing-execution.sh
new file mode 100755
index 0000000..4107757
--- /dev/null
+++ b/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
diff --git a/rust-semantics/expression/expression-list.md b/rust-semantics/expression/expression-list.md
index 453f04e..5ab2c71 100644
--- a/rust-semantics/expression/expression-list.md
+++ b/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)
diff --git a/rust-semantics/expression/tuple.md b/rust-semantics/expression/tuple.md
index 8195137..a097e40 100644
--- a/rust-semantics/expression/tuple.md
+++ b/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))
diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md
index d6d2dc8..884de7d 100644
--- a/rust-semantics/helpers.md
+++ b/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
```
diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
index 63479d9..f4489b1 100644
--- a/rust-semantics/representation.md
+++ b/rust-semantics/representation.md
@@ -89,6 +89,7 @@ module RUST-REPRESENTATION
, reversedNormalizedParams: PtrList
)
| "clearValue"
+ | tupleExpression(TupleElementsNoEndComma)
syntax PtrList ::= reverse(PtrList, PtrList) [function, total]
diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md
index f5e192e..e81ab94 100644
--- a/rust-semantics/test/execution.md
+++ b/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
(V:PtrValue ~> return_value) => .K ...
.List => ListItem(V) ...
+ rule (V:PtrValue ~> return_value_to_arg) => push V
+
rule
check_eq ptrValue(_, V:Value) => .K ...
ListItem(ptrValue(_, V)) => .List ...
diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs
new file mode 100644
index 0000000..34d7fff
--- /dev/null
+++ b/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);
+}
diff --git a/tests/ukm-no-contract/test_bytes_hooks.append32.run b/tests/ukm-no-contract/test_bytes_hooks.append32.run
new file mode 100644
index 0000000..124d4c5
--- /dev/null
+++ b/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
diff --git a/tests/ukm-no-contract/test_bytes_hooks.append64.run b/tests/ukm-no-contract/test_bytes_hooks.append64.run
new file mode 100644
index 0000000..b02a99a
--- /dev/null
+++ b/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
diff --git a/tests/ukm-no-contract/test_bytes_hooks.appenddecode32.run b/tests/ukm-no-contract/test_bytes_hooks.appenddecode32.run
new file mode 100644
index 0000000..63ac827
--- /dev/null
+++ b/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
diff --git a/tests/ukm-no-contract/test_bytes_hooks.appenddecode64.run b/tests/ukm-no-contract/test_bytes_hooks.appenddecode64.run
new file mode 100644
index 0000000..02c92d4
--- /dev/null
+++ b/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
diff --git a/tests/ukm-no-contract/test_bytes_hooks.appenddecodestr.run b/tests/ukm-no-contract/test_bytes_hooks.appenddecodestr.run
new file mode 100644
index 0000000..1bf0409
--- /dev/null
+++ b/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
diff --git a/tests/ukm-no-contract/test_bytes_hooks.appendstr.run b/tests/ukm-no-contract/test_bytes_hooks.appendstr.run
new file mode 100644
index 0000000..400b52c
--- /dev/null
+++ b/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
diff --git a/tests/ukm-no-contract/test_bytes_hooks.empty.run b/tests/ukm-no-contract/test_bytes_hooks.empty.run
new file mode 100644
index 0000000..0a9455e
--- /dev/null
+++ b/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
diff --git a/tests/ukm-no-contract/test_bytes_hooks.rs b/tests/ukm-no-contract/test_bytes_hooks.rs
new file mode 100644
index 0000000..097b812
--- /dev/null
+++ b/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)
+}
diff --git a/ukm-semantics/main/configuration.md b/ukm-semantics/main/configuration.md
index c48c3c5..73fefae 100644
--- a/ukm-semantics/main/configuration.md
+++ b/ukm-semantics/main/configuration.md
@@ -1,8 +1,13 @@
```k
+requires "hooks/bytes.md"
+
module UKM-CONFIGURATION
+ imports UKM-HOOKS-BYTES-CONFIGURATION
configuration
- .K
+
+
+
endmodule
```
\ No newline at end of file
diff --git a/ukm-semantics/main/execution.md b/ukm-semantics/main/execution.md
index 8ea891e..057de65 100644
--- a/ukm-semantics/main/execution.md
+++ b/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
-```
\ No newline at end of file
+```
diff --git a/ukm-semantics/main/hooks.md b/ukm-semantics/main/hooks.md
new file mode 100644
index 0000000..3c55c44
--- /dev/null
+++ b/ukm-semantics/main/hooks.md
@@ -0,0 +1,9 @@
+```k
+
+requires "hooks/bytes.md"
+
+module UKM-HOOKS
+ imports private UKM-HOOKS-BYTES
+endmodule
+
+```
diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md
new file mode 100644
index 0000000..bd202c8
--- /dev/null
+++ b/ukm-semantics/main/hooks/bytes.md
@@ -0,0 +1,258 @@
+```k
+
+module UKM-HOOKS-BYTES-CONFIGURATION
+ imports INT-SYNTAX
+ imports MAP
+
+ configuration
+
+
+ .Map // Int to Bytes
+
+
+ 0
+
+
+endmodule
+
+module UKM-HOOKS-BYTES
+ imports private BYTES
+ imports private COMMON-K-CELL
+ imports private RUST-HELPERS
+ imports private RUST-REPRESENTATION
+ imports private UKM-HOOKS-BYTES-CONFIGURATION
+
+ syntax Identifier ::= "bytes_hooks" [token]
+ | "empty" [token]
+ | "length" [token]
+ | "append_u128" [token]
+ | "append_u64" [token]
+ | "append_u32" [token]
+ | "append_u16" [token]
+ | "append_u8" [token]
+ | "append_str" [token]
+ | "decode_u128" [token]
+ | "decode_u64" [token]
+ | "decode_u32" [token]
+ | "decode_u16" [token]
+ | "decode_u8" [token]
+ | "decode_str" [token]
+
+ syntax UkmBytesValue ::= ukmBytesValue(Bytes)
+ syntax UkmExpression ::= ukmBytesId(MInt{64})
+ | UkmBytesValue
+ syntax KResult ::= UkmBytesValue
+
+ rule
+
+ normalizedFunctionCall
+ ( :: bytes_hooks :: empty :: .PathExprSegments
+ , .PtrList
+ )
+ => ptrValue(null, u64(Int2MInt(NextId)))
+ ...
+
+
+ M => M[NextId <- b""]
+
+
+ NextId:Int => NextId +Int 1
+
+ requires notBool uoverflowMInt(64, NextId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: length :: .PathExprSegments
+ , BufferIdId:Ptr, .PtrList
+ )
+ => ukmBytesLength(BufferIdId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: append_u128 :: .PathExprSegments
+ , BufferIdId:Ptr, IntId:Ptr, .PtrList
+ )
+ => ukmBytesAppendInt(BufferIdId, IntId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: append_u64 :: .PathExprSegments
+ , BufferIdId:Ptr, IntId:Ptr, .PtrList
+ )
+ => ukmBytesAppendInt(BufferIdId, IntId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: append_u32 :: .PathExprSegments
+ , BufferIdId:Ptr, IntId:Ptr, .PtrList
+ )
+ => ukmBytesAppendInt(BufferIdId, IntId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: append_u16 :: .PathExprSegments
+ , BufferIdId:Ptr, IntId:Ptr, .PtrList
+ )
+ => ukmBytesAppendInt(BufferIdId, IntId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: append_u8 :: .PathExprSegments
+ , BufferIdId:Ptr, IntId:Ptr, .PtrList
+ )
+ => ukmBytesAppendInt(BufferIdId, IntId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: append_str :: .PathExprSegments
+ , BufferIdId:Ptr, StrId:Ptr, .PtrList
+ )
+ => ukmBytesAppendStr(BufferIdId, StrId)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: decode_u128 :: .PathExprSegments
+ , BufferIdId:Ptr, .PtrList
+ )
+ => ukmBytesDecode(BufferIdId, u32)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: decode_u64 :: .PathExprSegments
+ , BufferIdId:Ptr, .PtrList
+ )
+ => ukmBytesDecode(BufferIdId, u64)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: decode_u32 :: .PathExprSegments
+ , BufferIdId:Ptr, .PtrList
+ )
+ => ukmBytesDecode(BufferIdId, u32)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: decode_u16 :: .PathExprSegments
+ , BufferIdId:Ptr, .PtrList
+ )
+ => ukmBytesDecode(BufferIdId, u16)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: decode_u8 :: .PathExprSegments
+ , BufferIdId:Ptr, .PtrList
+ )
+ => ukmBytesDecode(BufferIdId, u8)
+
+ rule
+ normalizedFunctionCall
+ ( :: bytes_hooks :: decode_str :: .PathExprSegments
+ , BufferIdId:Ptr, .PtrList
+ )
+ => ukmBytesDecode(BufferIdId, str)
+
+ // ---------------------------------------
+
+ rule
+
+ ukmBytesId(BytesId) => ukmBytesValue(Value)
+ ...
+
+
+ MInt2Unsigned(BytesId) |-> Value:Bytes
+ ...
+
+
+ syntax UKMInstruction ::= ukmBytesLength(Expression) [strict(1)]
+ | ukmBytesLength(UkmExpression) [strict(1)]
+ | ukmBytesAppendInt(Expression, Expression) [seqstrict]
+ | ukmBytesAppendInt(UkmExpression, Int) [strict(1)]
+ | ukmBytesAppendStr(Expression, Expression) [seqstrict]
+ | ukmBytesAppendBytes(UkmExpression, Bytes) [strict(1)]
+ | ukmBytesAppendLenAndBytes(Bytes, Bytes)
+ | ukmBytesDecode(Expression, Type) [strict(1)]
+ | ukmBytesDecode(UkmExpression, Type) [strict(1)]
+ | ukmBytesDecode(Int, Bytes, Type)
+ | ukmBytesDecodeInt(Int, Bytes, Type)
+ | ukmBytesDecode(ValueOrError, Bytes)
+ syntax Expression ::= ukmBytesNew(Bytes)
+
+ rule
+
+ ukmBytesNew(B:Bytes)
+ => ptrValue(null, u64(Int2MInt(NextId)))
+ ...
+
+
+ M => M[NextId <- B]
+
+
+ NextId:Int => NextId +Int 1
+
+ requires notBool uoverflowMInt(64, NextId)
+
+ rule ukmBytesLength(ptrValue(_, u64(BytesId))) => ukmBytesLength(ukmBytesId(BytesId))
+ rule ukmBytesLength(ukmBytesValue(Value:Bytes))
+ => ptrValue(null, u32(Int2MInt(lengthBytes(Value))))
+ requires notBool uoverflowMInt(32, lengthBytes(Value))
+
+ rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u128(Value)))
+ => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value))
+ rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u64(Value)))
+ => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value))
+ rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u32(Value)))
+ => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value))
+ rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u16(Value)))
+ => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value))
+ rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u8(Value)))
+ => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value))
+
+ rule ukmBytesAppendInt(ukmBytesValue(B:Bytes), Value:Int)
+ => ukmBytesAppendLenAndBytes(B, Int2Bytes(Value, BE, Unsigned))
+
+ rule ukmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String))
+ => ukmBytesAppendBytes(ukmBytesId(BytesId), String2Bytes(Value))
+
+ rule ukmBytesAppendBytes(ukmBytesValue(B:Bytes), Value:Bytes)
+ => ukmBytesAppendLenAndBytes(B, Value)
+
+ rule ukmBytesAppendLenAndBytes(First:Bytes, Second:Bytes)
+ => ukmBytesNew(First +Bytes Int2Bytes(2, lengthBytes(Second), BE) +Bytes Second)
+ requires lengthBytes(Second) ukmBytesDecode(ukmBytesId(BytesId), T:Type)
+ rule ukmBytesDecode(ukmBytesValue(B:Bytes), T:Type)
+ => ukmBytesDecode
+ ( Bytes2Int(substrBytes(B, 0, 2), BE, Unsigned)
+ , substrBytes(B, 2, lengthBytes(B))
+ , T:Type
+ )
+ requires 2 <=Int lengthBytes(B)
+ rule ukmBytesDecode(Len:Int, B:Bytes, T:Type)
+ => ukmBytesDecodeInt
+ ( Bytes2Int(substrBytes(B, 0, Len), BE, Unsigned)
+ , substrBytes(B, Len, lengthBytes(B))
+ , T:Type
+ )
+ requires Len <=Int lengthBytes(B) andBool isUnsignedInt(T)
+ rule ukmBytesDecode(Len:Int, B:Bytes, T:Type)
+ => ukmBytesDecodeInt
+ ( Bytes2Int(substrBytes(B, 0, Len), BE, Signed)
+ , substrBytes(B, Len, lengthBytes(B))
+ , T:Type
+ )
+ requires Len <=Int lengthBytes(B) andBool isSignedInt(T)
+ rule ukmBytesDecode(Len:Int, B:Bytes, str)
+ => ukmBytesDecode
+ ( Bytes2String(substrBytes(B, 0, Len))
+ , substrBytes(B, Len, lengthBytes(B))
+ )
+ requires Len <=Int lengthBytes(B)
+ rule ukmBytesDecodeInt(Value:Int, B:Bytes, T:Type)
+ => ukmBytesDecode(integerToValue(Value, T), B)
+ rule ukmBytesDecode(Value:Value, B:Bytes)
+ => tupleExpression(ukmBytesNew(B) , ptrValue(null, Value) , .TupleElementsNoEndComma)
+endmodule
+
+```
diff --git a/ukm-semantics/targets/testing/configuration.md b/ukm-semantics/targets/testing/configuration.md
index 5efece1..84c1fc9 100644
--- a/ukm-semantics/targets/testing/configuration.md
+++ b/ukm-semantics/targets/testing/configuration.md
@@ -20,6 +20,7 @@ endmodule
module UKM-TARGET-CONFIGURATION
imports COMMON-K-CELL
imports RUST-EXECUTION-CONFIGURATION
+ imports RUST-EXECUTION-TEST-CONFIGURATION
imports UKM-CONFIGURATION
imports UKM-FULL-PREPROCESSED-CONFIGURATION
imports UKM-TEST-CONFIGURATION
@@ -29,6 +30,7 @@ module UKM-TARGET-CONFIGURATION
+
diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md
index ef9bef4..1321ddc 100644
--- a/ukm-semantics/targets/testing/ukm-target.md
+++ b/ukm-semantics/targets/testing/ukm-target.md
@@ -10,11 +10,14 @@ requires "rust-semantics/full-preprocessing.md"
requires "rust-semantics/test/execution.md"
module UKM-TARGET-SYNTAX
+ imports RUST-COMMON-SYNTAX
+ imports UKM-TEST-SYNTAX
endmodule
module UKM-TARGET
imports private RUST-COMMON
imports private RUST-FULL-PREPROCESSING
+ imports private RUST-EXECUTION-TEST
imports private UKM-EXECUTION
imports private UKM-PREPROCESSING
imports private UKM-TARGET-CONFIGURATION
diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md
index 67a390a..e3bc92e 100644
--- a/ukm-semantics/test/execution.md
+++ b/ukm-semantics/test/execution.md
@@ -1,6 +1,7 @@
```k
module UKM-TEST-SYNTAX
+ imports RUST-EXECUTION-TEST-PARSING-SYNTAX
endmodule
module UKM-TEST-EXECUTION