tmp

Dockerfile

@@ -8,8 +8,7 @@ FROM runtimeverificationinc/kframework-k:ubuntu-noble-${K_COMMIT}
 RUN    apt-get update              \
     && apt-get upgrade --yes       \
     && apt-get install --yes       \
-                       curl \
-                       libcrypto++-dev
+                       curl
 
 ARG USER_ID=1001
 ARG GROUP_ID=1001

ukm-semantics/test/execution.md

@@ -5,8 +5,6 @@ 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
@@ -29,8 +27,6 @@ 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
@@ -39,10 +35,6 @@ 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