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

@@ -1,8 +1,10 @@
 ```k
 
+requires "encoding/impl.md"
 requires "encoding/syntax.md"
 
 module UKM-ENCODING
+    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

@@ -4,6 +4,7 @@ module UKM-ENCODING-SYNTAX
     imports BYTES-SYNTAX
 
     syntax UKMInstruction ::= "ukmEncodePreprocessedCell"
+                            | ukmEncodedPreprocessedCell(Bytes)
 
 endmodule
 

ukm-semantics/targets/testing/configuration.md

@@ -9,12 +9,16 @@ 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
         <k>
             cratesParser($PGM:WrappedCrateList)
             ~> ukmPreprocessCrates
+            ~> ukmEncodePreprocessedCell
+            ~> ukmDecodePreprocessedCell
             ~> $TEST:ExecutionTest
         </k>
 endmodule

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

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
@@ -19,6 +21,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
@@ -27,6 +31,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