diff --git a/Dockerfile b/Dockerfile
index 305329a..5c59231 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -8,7 +8,8 @@ FROM runtimeverificationinc/kframework-k:ubuntu-noble-${K_COMMIT}
RUN apt-get update \
&& apt-get upgrade --yes \
&& apt-get install --yes \
- curl
+ curl \
+ libcrypto++-dev
ARG USER_ID=1001
ARG GROUP_ID=1001
diff --git a/ukm-semantics/main/decoding.md b/ukm-semantics/main/decoding.md
index 3561da2..8d41757 100644
--- a/ukm-semantics/main/decoding.md
+++ b/ukm-semantics/main/decoding.md
@@ -1,8 +1,10 @@
```k
+requires "decoding/impl.md"
requires "decoding/syntax.md"
module UKM-DECODING
+ imports private UKM-DECODING-IMPL
endmodule
```
diff --git a/ukm-semantics/main/decoding/impl.md b/ukm-semantics/main/decoding/impl.md
new file mode 100644
index 0000000..631bbe6
--- /dev/null
+++ b/ukm-semantics/main/decoding/impl.md
@@ -0,0 +1,16 @@
+```k
+
+module UKM-DECODING-IMPL
+ imports private COMMON-K-CELL
+ imports private UKM-DECODING-SYNTAX
+ imports private UKM-FULL-PREPROCESSED-CONFIGURATION
+
+ syntax UkmFullPreprocessedCell ::= decodeUkmFullPreprocessedCell(Bytes)
+ [function, hook(ULM.decode)]
+
+ rule
+ ukmDecodePreprocessedCell(B:Bytes) => .K ...
+ (_:UkmFullPreprocessedCell => decodeUkmFullPreprocessedCell(B))
+endmodule
+
+```
diff --git a/ukm-semantics/main/encoding.md b/ukm-semantics/main/encoding.md
index 9f08445..eeb1cdf 100644
--- a/ukm-semantics/main/encoding.md
+++ b/ukm-semantics/main/encoding.md
@@ -1,8 +1,10 @@
```k
+requires "encoding/impl.md"
requires "encoding/syntax.md"
module UKM-ENCODING
+ imports private UKM-ENCODING-IMPL
endmodule
```
diff --git a/ukm-semantics/main/encoding/impl.md b/ukm-semantics/main/encoding/impl.md
new file mode 100644
index 0000000..d0f10b0
--- /dev/null
+++ b/ukm-semantics/main/encoding/impl.md
@@ -0,0 +1,22 @@
+```k
+
+module UKM-ENCODING-IMPL
+ imports private COMMON-K-CELL
+ imports private BYTES-SYNTAX
+ imports private UKM-ENCODING-SYNTAX
+ imports private UKM-FULL-PREPROCESSED-CONFIGURATION
+
+ syntax Bytes ::= encodeUkmFullPreprocessedCell(UkmFullPreprocessedCell)
+ [function, hook(ULM.encode)]
+
+ rule
+
+ ukmEncodePreprocessedCell
+ => ukmEncodedPreprocessedCell(encodeUkmFullPreprocessedCell(Cell))
+ ...
+
+ Cell:UkmFullPreprocessedCell
+
+endmodule
+
+```
diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md
index d303075..bd0dab4 100644
--- a/ukm-semantics/main/encoding/syntax.md
+++ b/ukm-semantics/main/encoding/syntax.md
@@ -4,6 +4,7 @@ module UKM-ENCODING-SYNTAX
imports BYTES-SYNTAX
syntax UKMInstruction ::= "ukmEncodePreprocessedCell"
+ | ukmEncodedPreprocessedCell(Bytes)
endmodule
diff --git a/ukm-semantics/targets/testing/configuration.md b/ukm-semantics/targets/testing/configuration.md
index 37cc2ab..e4842ad 100644
--- a/ukm-semantics/targets/testing/configuration.md
+++ b/ukm-semantics/targets/testing/configuration.md
@@ -9,7 +9,9 @@ requires "rust-semantics/test/configuration.md"
module COMMON-K-CELL
imports private RUST-EXECUTION-TEST-PARSING-SYNTAX
imports private RUST-PREPROCESSING-SYNTAX
+ imports private UKM-ENCODING-SYNTAX
imports private UKM-PREPROCESSING-SYNTAX
+ imports private UKM-TEST-SYNTAX
configuration
diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md
index 1321ddc..bfd9566 100644
--- a/ukm-semantics/targets/testing/ukm-target.md
+++ b/ukm-semantics/targets/testing/ukm-target.md
@@ -1,5 +1,7 @@
```k
+requires "../../main/decoding.md"
+requires "../../main/encoding.md"
requires "../../main/execution.md"
requires "../../main/preprocessing.md"
requires "../../test/execution.md"
@@ -18,6 +20,8 @@ module UKM-TARGET
imports private RUST-COMMON
imports private RUST-FULL-PREPROCESSING
imports private RUST-EXECUTION-TEST
+ imports private UKM-DECODING
+ imports private UKM-ENCODING
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 77956e4..b1611f9 100644
--- a/ukm-semantics/test/execution.md
+++ b/ukm-semantics/test/execution.md
@@ -5,6 +5,8 @@ module UKM-TEST-SYNTAX
imports RUST-EXECUTION-TEST-PARSING-SYNTAX
imports UKM-HOOKS-UKM-SYNTAX
+ syntax UkmInstruction ::= "ukmDecodePreprocessedCell"
+
syntax ExecutionItem ::= "mock" "CallData"
| "mock" "Caller"
| "mock" UkmHook UkmHookResult
@@ -27,6 +29,8 @@ endmodule
module UKM-TEST-EXECUTION
imports private COMMON-K-CELL
imports private RUST-EXECUTION-TEST-CONFIGURATION
+ imports private UKM-DECODING-SYNTAX
+ imports private UKM-ENCODING-SYNTAX
imports private UKM-EXECUTION-SYNTAX
imports private UKM-HOOKS-BYTES-CONFIGURATION
imports private UKM-HOOKS-BYTES-SYNTAX
@@ -35,6 +39,10 @@ module UKM-TEST-EXECUTION
imports private UKM-HOOKS-UKM-SYNTAX
imports private UKM-TEST-SYNTAX
+ // Patching the encoding result to decoding for test purposes
+ rule ukmEncodedPreprocessedCell(B:Bytes) ~> ukmDecodePreprocessedCell
+ => ukmDecodePreprocessedCell(B)
+
syntax Mockable ::= UkmHook
rule