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
+        <k> ukmDecodePreprocessedCell(B:Bytes) => .K ... </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
+        <k>
+            ukmEncodePreprocessedCell
+            => ukmEncodedPreprocessedCell(encodeUkmFullPreprocessedCell(Cell))
+            ...
+        </k>
+        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