Preprocess contracts for ULM (#189)

* Preprocess contracts for ULM

* Compile the execution target for ulm execution

* Attempt to generate contract binary

* Prevent weird emit-contract-bytes crash

* Update the documentation

* Remove the preprocessing target

* Remove unneeded file

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,10 +93,11 @@ clean:
 
 build: $(RUST_PREPROCESSING_TIMESTAMP) \
 				$(RUST_EXECUTION_TIMESTAMP) \
-				$(ULM_EXECUTION_TIMESTAMP) \
-				$(ULM_PREPROCESSING_TIMESTAMP) \
 				$(ULM_TESTING_TIMESTAMP)
 
+build-ulm: $(ULM_EXECUTION_TIMESTAMP) \
+				.build/emit-contract-bytes
+
 build-legacy: \
 		$(MX_TESTING_TIMESTAMP) \
 		$(MX_RUST_TIMESTAMP) \
@@ -184,28 +182,35 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTI
 			-I . \
 			--debug
 
-$(ULM_EXECUTION_TIMESTAMP): $(ULM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) deps/blockchain-k-plugin/build/krypto/lib/krypto.a
+$(ULM_EXECUTION_TIMESTAMP): $(ULM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(ULM_EXECUTION_KOMPILED)
+	poetry -C ../evm-semantics/kevm-pyk run kdist build evm-semantics.plugin
+	make -C ../ulm/kllvm/ all
 	$$(which kompile) ulm-semantics/targets/execution/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_EXECUTION_KOMPILED) \
-			-I kllvm \
-			-I deps/blockchain-k-plugin \
+			--hook-namespaces 'KRYPTO ULM' \
+			-O2 \
+			-ccopt -g \
+			-ccopt -std=c++20 \
+			-ccopt -lcrypto \
+			-ccopt -lsecp256k1 \
+			-ccopt -lssl \
+			-ccopt $$(poetry -C ../evm-semantics/kevm-pyk run kdist which evm-semantics.plugin)/krypto.a \
+			-ccopt -L../ulm/kllvm \
+			-ccopt -lulmkllvm \
+			-ccopt ../ulm/kllvm/lang/ulm_language_entry.cpp \
+			-ccopt -I../ulm/kllvm \
+			-ccopt -DULM_LANG_ID=rust \
+			-ccopt -shared \
+			-ccopt -fPIC \
+			--llvm-hidden-visibility \
+			--llvm-kompile-type library \
+			--llvm-kompile-output libkrust.so \
+			-o $(ULM_EXECUTION_KOMPILED) \
+			-I ../ulm/kllvm \
 			-I . \
-			--debug
-
-$(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
+			-I ../evm-semantics/kevm-pyk/src/kevm_pyk/kproj/plugin \
+			-v
 
 $(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
@@ -220,6 +225,17 @@ $(ULM_TESTING_TIMESTAMP): $(ULM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) deps/bl
 			-I kllvm \
 			--debug
 
+.build/emit-contract-bytes: $(ULM_EXECUTION_TIMESTAMP)
+	clang++-16 ../ulm/kllvm/emit_contract_bytes.cpp \
+			-I $$(dirname $$(which kompile))/../include/kllvm \
+			-I $$(dirname $$(which kompile))/../include \
+			-std=c++20 \
+			-DULM_LANG_ID=rust \
+			-Wno-return-type-c-linkage \
+			-lulmkllvm -L ../ulm/kllvm/ \
+			-lkrust -L $(ULM_EXECUTION_KOMPILED) \
+			-o .build/emit-contract-bytes
+
 $(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)
 	mkdir -p $(RUST_SYNTAX_OUTPUT_DIR)
 	kast --definition $(RUST_PREPROCESSING_KOMPILED) $< --sort Crate > $@.tmp && mv -f $@.tmp $@

README.md

@@ -13,27 +13,17 @@ traits.
 Setup for ULM
 -------------
 
-The commands below will not work without the encode/decode ULM hooks,
-which are not included by the build commands below.
+You must have `ulm` and `evm-semantics` checked out as sibling directories
+(i.e. `../ulm` and `../evm-semantics`).
 
-"Compiling" the erc-20 contract to bytes:
-
-```sh
-make .build/ulm-preprocessing-kompiled/timestamp
-compilation/prepare-erc20.sh
+Build the semantics:
+```
+make build-ulm -j3
 ```
 
-The above will produce a configuration whose `<k>` cell contains
-`ulmEncodedPreprocessedCell(contract-bytes:Bytes)`
-
-Running the contract requires a different semantics (there main difference from
-the above is the setup of the `<k>` cell; there are other small differences, but
-they matter less):
-
-```sh
-make .build/ulm-execution-kompiled/timestamp
+Preprocess and convert a contract to bytes:
+```
+compilation/prepare-contract.sh \
+    tests/ulm-contracts/erc_20_token.rs \
+    .build/compilation/erc_20_token.preprocessed.kore
 ```
-When running the above (say, with `krun`), and calling the constructor
-(`$CREATE` is `true`), it expects `CallData()` to contain the initial quantity
-to mint and assign to the caller (`u256`). At the end, it will leave the
-contract's bytes in the `<k>` cell in a similar way to the `SIMPLE-ulm` example.

compilation/prepare-contract.sh

@@ -4,19 +4,24 @@
 # It expects two args: the contract path and the arguments for the init function.
 
 set -e
+set -x
 
 ULM_CONTRACTS_TESTING_INPUT_DIR=tests/ulm-contracts
-ULM_PREPROCESSING_KOMPILED=.build/ulm-preprocessing-kompiled
-TEMP_DIR=tmp
+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
+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 \
+  --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.kore > $2

compilation/prepare-erc20.sh

@@ -4,4 +4,6 @@
 
 set -e
 
-compilation/prepare-contract.sh tests/ulm-contracts/erc_20_token.rs "1000000000000000000_u256,"
+compilation/prepare-contract.sh \
+    tests/ulm-contracts/erc_20_token.rs \
+    .build/compilation/erc_20_token.preprocessed.kore

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/main/encoding.md

@@ -1,13 +1,11 @@
 ```k
 
 requires "encoding/encoder.md"
-requires "encoding/impl.md"
 requires "encoding/syntax.md"
 requires "encoding/encoder.md"
 
 module ULM-ENCODING
     imports private ULM-CALLDATA-ENCODER
-    imports private ULM-ENCODING-IMPL
 endmodule
 
 ```

ulm-semantics/main/encoding/syntax.md

@@ -5,9 +5,6 @@ module ULM-ENCODING-SYNTAX
     imports LIST
     imports RUST-REPRESENTATION
 
-    syntax ULMInstruction ::= "ulmEncodePreprocessedCell"
-                            | ulmEncodedPreprocessedCell(Bytes)
-
     // TODO: Make these functions total and returning BytesOrError
     syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list
                    | encodeConstructorData (List, List) [function] // argument types, argument list

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
@@ -22,12 +25,15 @@ module ULM-TARGET-CONFIGURATION
     imports RUST-EXECUTION-CONFIGURATION
     imports ULM-CONFIGURATION
     imports ULM-FULL-PREPROCESSED-CONFIGURATION
+    imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION
 
     configuration
+        <ulm-preprocessing-ephemeral/>
         <ulm-full-preprocessed/>
         <ulm/>
         <execution/>
         <k/>
+
 endmodule
 
 ```

ulm-semantics/targets/execution/ulm-target.md

@@ -1,18 +1,26 @@
 ```k
 
 requires "../../main/decoding.md"
+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