Remove the preprocessing target

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)

compilation/prepare-contract.sh

@@ -7,29 +7,21 @@ 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
 
 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

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

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
 

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

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