Encode and decode contracts in tests

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
 
 ```

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
+
+```

ukm-semantics/main/encoding.md

@@ -4,7 +4,8 @@ requires "encoding/syntax.md"
 requires "encoding/encoder.md"
 
 module UKM-ENCODING
-    imports UKM-CALLDATA-ENCODER
+    imports private UKM-CALLDATA-ENCODER
+    imports private UKM-ENCODING-IMPL
 endmodule
 
 ```

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
+
+```

ukm-semantics/main/encoding/syntax.md

@@ -6,6 +6,7 @@ module UKM-ENCODING-SYNTAX
     imports RUST-REPRESENTATION
 
     syntax UKMInstruction ::= "ukmEncodePreprocessedCell"
+                            | ukmEncodedPreprocessedCell(Bytes)
 
     syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list
                    | encodeFunctionSignature (String, List) [function]