diff --git a/Makefile b/Makefile
index 5f60cfa6..586e06c0 100644
--- a/Makefile
+++ b/Makefile
@@ -69,9 +69,6 @@ ULM_SEMANTICS_FILES ::= $(shell find ulm-semantics/ -type f -a '(' -name '*.md'
 ULM_EXECUTION_KOMPILED ::= .build/ulm-execution-kompiled
 ULM_EXECUTION_TIMESTAMP ::= $(ULM_EXECUTION_KOMPILED)/timestamp
 
-ULM_PREPROCESSING_KOMPILED ::= .build/ulm-preprocessing-kompiled
-ULM_PREPROCESSING_TIMESTAMP ::= $(ULM_PREPROCESSING_KOMPILED)/timestamp
-
 ULM_TESTING_KOMPILED ::= .build/ulm-testing-kompiled
 ULM_TESTING_TIMESTAMP ::= $(ULM_TESTING_KOMPILED)/timestamp
 
@@ -96,11 +93,9 @@ clean:
 
 build: $(RUST_PREPROCESSING_TIMESTAMP) \
 				$(RUST_EXECUTION_TIMESTAMP) \
-				$(ULM_PREPROCESSING_TIMESTAMP) \
 				$(ULM_TESTING_TIMESTAMP)
 
 build-ulm: $(ULM_EXECUTION_TIMESTAMP) \
-				$(ULM_PREPROCESSING_TIMESTAMP) \
 				.build/emit-contract-bytes
 
 build-legacy: \
@@ -217,17 +212,6 @@ $(ULM_EXECUTION_TIMESTAMP): $(ULM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
 			-I ../evm-semantics/kevm-pyk/src/kevm_pyk/kproj/plugin \
 			-v
 
-$(ULM_PREPROCESSING_TIMESTAMP): $(ULM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) deps/blockchain-k-plugin/build/krypto/lib/krypto.a
-	# Workaround for https://github.com/runtimeverification/k/issues/4141
-	-rm -r $(ULM_PREPROCESSING_KOMPILED)
-	$$(which kompile) ulm-semantics/targets/preprocessing/ulm-target.md  \
-			--hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \
-			-ccopt -lsecp256k1 -ccopt -lssl -ccopt 'deps/blockchain-k-plugin/build/krypto/lib/krypto.a' \
-			--emit-json -o $(ULM_PREPROCESSING_KOMPILED) \
-			-I . \
-			-I deps/blockchain-k-plugin \
-			--debug
-
 $(ULM_TESTING_TIMESTAMP): $(ULM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) deps/blockchain-k-plugin/build/krypto/lib/krypto.a
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(ULM_TESTING_KOMPILED)
diff --git a/compilation/prepare-contract.sh b/compilation/prepare-contract.sh
index 2fd696b4..a3313c74 100755
--- a/compilation/prepare-contract.sh
+++ b/compilation/prepare-contract.sh
@@ -7,7 +7,7 @@ set -e
 set -x
 
 ULM_CONTRACTS_TESTING_INPUT_DIR=tests/ulm-contracts
-ULM_PREPROCESSING_KOMPILED=.build/ulm-preprocessing-kompiled
+ULM_EXECUTION_KOMPILED=.build/ulm-execution-kompiled
 COMPILATION_DIR=.build/compilation
 TEMP_DIR=$COMPILATION_DIR/tmp
 
@@ -15,21 +15,13 @@ mkdir -p $TEMP_DIR
 
 compilation/prepare-rust-bundle.sh $1 $TEMP_DIR/input.tmp
 
-krun \
+kparse \
   $TEMP_DIR/input.tmp \
-  --parser $(pwd)/parsers/crates-ulm-preprocessing-execution.sh \
-  --definition $ULM_PREPROCESSING_KOMPILED \
-  --output kore \
-  --output-file $TEMP_DIR/output.kore \
-
-poetry -C rust-lite install
-
-poetry -C rust-lite run python \
-  -m rust_lite.extract_preprocessed \
-  $TEMP_DIR/output.kore \
-  $TEMP_DIR/output.preprocessed.kore \
+  --sort WrappedCrateList \
+  --definition $ULM_EXECUTION_KOMPILED \
+  > $TEMP_DIR/output.kore
 
 WORKDIR=$(dirname $(pwd))
 export LD_LIBRARY_PATH=$WORKDIR/ulm/kllvm:$WORKDIR/rust-demo-semantics/.build/ulm-execution-kompiled
 
-.build/emit-contract-bytes $TEMP_DIR/output.preprocessed.kore > $2
+.build/emit-contract-bytes $TEMP_DIR/output.kore > $2
diff --git a/ulm-semantics/main/decoding.md b/ulm-semantics/main/decoding.md
index f8fc1305..ea84977f 100644
--- a/ulm-semantics/main/decoding.md
+++ b/ulm-semantics/main/decoding.md
@@ -1,10 +1,8 @@
 ```k
 
-requires "decoding/impl.md"
 requires "decoding/syntax.md"
 
 module ULM-DECODING
-    imports private ULM-DECODING-IMPL
 endmodule
 
 ```
diff --git a/ulm-semantics/main/decoding/impl.md b/ulm-semantics/main/decoding/impl.md
deleted file mode 100644
index 149c980a..00000000
--- a/ulm-semantics/main/decoding/impl.md
+++ /dev/null
@@ -1,16 +0,0 @@
-```k
-
-module ULM-DECODING-IMPL
-    imports private COMMON-K-CELL
-    imports private ULM-DECODING-SYNTAX
-    imports private ULM-FULL-PREPROCESSED-CONFIGURATION
-
-    syntax UlmFullPreprocessedCell  ::= decodeUlmFullPreprocessedCell(Bytes)
-                                        [function, hook(ULM.decode)]
-
-    rule
-        <k> ulmDecodePreprocessedCell(B:Bytes) => .K ... </k>
-        (_:UlmFullPreprocessedCell => decodeUlmFullPreprocessedCell(B))
-endmodule
-
-```
diff --git a/ulm-semantics/main/decoding/syntax.md b/ulm-semantics/main/decoding/syntax.md
index 44717c4c..f572bfb2 100644
--- a/ulm-semantics/main/decoding/syntax.md
+++ b/ulm-semantics/main/decoding/syntax.md
@@ -2,8 +2,10 @@
 
 module ULM-DECODING-SYNTAX
     imports BYTES-SYNTAX
+    imports RUST-CRATE-LIST-SYNTAX
 
-    syntax ULMInstruction ::= ulmDecodePreprocessedCell(Bytes)
+    syntax WrappedCrateList ::= ulmDecodeRustCrates(Bytes)
+                                [function, hook(ULM.decode)]
 
 endmodule
 
diff --git a/ulm-semantics/targets/execution/configuration.md b/ulm-semantics/targets/execution/configuration.md
index 47862f25..69076649 100644
--- a/ulm-semantics/targets/execution/configuration.md
+++ b/ulm-semantics/targets/execution/configuration.md
@@ -7,12 +7,15 @@ requires "rust-semantics/config.md"
 module COMMON-K-CELL
     imports private BYTES-SYNTAX
     imports private INT-SYNTAX
+    imports private RUST-PREPROCESSING-SYNTAX
     imports private ULM-DECODING-SYNTAX
     imports private ULM-EXECUTION-SYNTAX
+    imports private ULM-PREPROCESSING-SYNTAX
 
     configuration
         <k>
-            ulmDecodePreprocessedCell($PGM:Bytes)
+            cratesParser(ulmDecodeRustCrates($PGM:Bytes))
+            ~> ulmPreprocessCrates
             ~> ulmExecute($CREATE:Bool, $PGM:Bytes, $ACCTCODE:Int, $GAS:Int)
         </k>
 endmodule
diff --git a/ulm-semantics/targets/execution/ulm-target.md b/ulm-semantics/targets/execution/ulm-target.md
index 7e433e89..7b5e705f 100644
--- a/ulm-semantics/targets/execution/ulm-target.md
+++ b/ulm-semantics/targets/execution/ulm-target.md
@@ -5,22 +5,24 @@ requires "../../main/encoding.md"
 requires "../../main/execution.md"
 requires "../../main/preprocessing.md"
 requires "configuration.md"
+requires "rust-semantics/full-preprocessing.md"
 requires "rust-semantics/rust-common.md"
 requires "rust-semantics/rust-common-syntax.md"
 
 
 module ULM-TARGET-SYNTAX
+    imports RUST-CRATES-SYNTAX
 endmodule
 
 module ULM-TARGET
     imports private RUST-COMMON
+    imports private RUST-FULL-PREPROCESSING
     imports private ULM-DECODING
     imports private ULM-ENCODING
     imports private ULM-EXECUTION
     imports private ULM-PREPROCESSING
     imports private ULM-SEMANTICS-HOOKS-TO-ULM-FUNCTIONS
     imports private ULM-TARGET-CONFIGURATION
-
 endmodule
 
 ```
diff --git a/ulm-semantics/targets/preprocessing/configuration.md b/ulm-semantics/targets/preprocessing/configuration.md
deleted file mode 100644
index ccf73101..00000000
--- a/ulm-semantics/targets/preprocessing/configuration.md
+++ /dev/null
@@ -1,32 +0,0 @@
-```k
-
-requires "../../main/configuration.md"
-requires "../../main/preprocessed-configuration.md"
-requires "rust-semantics/config.md"
-requires "rust-semantics/full-preprocessing.md"
-requires "rust-semantics/rust-common-syntax.md"
-
-module COMMON-K-CELL
-    imports private RUST-PREPROCESSING-SYNTAX
-    imports private ULM-ENCODING-SYNTAX
-    imports private ULM-PREPROCESSING-SYNTAX
-
-    configuration
-        <k>
-            cratesParser($PGM:WrappedCrateList)
-            ~> ulmPreprocessCrates
-        </k>
-endmodule
-
-module ULM-TARGET-CONFIGURATION
-    imports COMMON-K-CELL
-    imports ULM-FULL-PREPROCESSED-CONFIGURATION
-    imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION
-
-    configuration
-        <ulm-full-preprocessed/>
-        <ulm-preprocessing-ephemeral/>
-        <k/>
-endmodule
-
-```
diff --git a/ulm-semantics/targets/preprocessing/ulm-target.md b/ulm-semantics/targets/preprocessing/ulm-target.md
deleted file mode 100644
index a62d1fb5..00000000
--- a/ulm-semantics/targets/preprocessing/ulm-target.md
+++ /dev/null
@@ -1,17 +0,0 @@
-```k
-
-requires "../../main/encoding.md"
-requires "../../main/preprocessing.md"
-requires "configuration.md"
-
-module ULM-TARGET-SYNTAX
-endmodule
-
-module ULM-TARGET
-    imports private RUST-FULL-PREPROCESSING
-    imports private ULM-ENCODING
-    imports private ULM-PREPROCESSING
-    imports private ULM-TARGET-CONFIGURATION
-endmodule
-
-```