Encode and decode contracts in tests

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "deps/ulm"]
+	path = deps/ulm
+	url = [email protected]:Pi-Squared-Inc/ulm

Dockerfile

@@ -12,7 +12,8 @@ COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
 RUN    apt-get update              \
     && apt-get upgrade --yes       \
     && apt-get install --yes       \
-                       curl
+                       curl \
+                       libcrypto++-dev
 #                        cmake       \
 #                        pandoc      \
 #                        python3     \

Makefile

@@ -87,6 +87,23 @@ UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-with-contract/output
 UKM_WITH_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/*.run)
 UKM_WITH_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_WITH_CONTRACT_TESTING_INPUTS))
 
+UKM_FLAGS ::= -I deps/ulm/kllvm \
+        -ccopt -Ldeps/ulm/kllvm \
+				-ccopt -lulmkllvm
+
+# TODO: Use a plugin directory that is accessible from the current project
+CRYPTO_FLAGS ::= -I ../evm-semantics/kevm-pyk/src/kevm_pyk/kproj/plugin \
+				-ccopt -lssl \
+				-ccopt -lcrypto \
+				-ccopt -lsecp256k1 \
+        -ccopt $KRYPTO_DIR/evm-semantics/plugin/krypto.a  \
+
+# PLUGIN_FLAGS ::= --hook-namespaces 'ULM KRYPTO'
+PLUGIN_FLAGS ::= --hook-namespaces 'ULM' \
+								-ccopt -std=c++17 \
+								${UKM_FLAGS} \
+								# ${CRYPTO_FLAGS}
+
 .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
@@ -134,6 +151,10 @@ ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS)
 
 ukm-with-contracts-test: $(UKM_WITH_CONTRACT_TESTING_OUTPUTS)
 
+ulm-plugin:
+	make -C deps/ulm/kllvm/ libulmkllvm.so
+.PHONY: ulm-plugin
+
 $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(RUST_PREPROCESSING_KOMPILED)
@@ -197,10 +218,11 @@ $(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
 			-I . \
 			--debug
 
-$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
+$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) ulm-plugin
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(UKM_TESTING_KOMPILED)
 	$$(which kompile) ukm-semantics/targets/testing/ukm-target.md \
+			${PLUGIN_FLAGS} \
 			--emit-json -o $(UKM_TESTING_KOMPILED) \
 			-I . \
 			--debug

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