From fab3b4cb37007775b6be71b419435b7775688fcf Mon Sep 17 00:00:00 2001 From: Virgil Date: Mon, 18 Nov 2024 19:59:24 +0200 Subject: [PATCH 1/7] Preprocess contracts for ULM --- README.md | 3 +- compilation/prepare-contract.sh | 12 +++++- compilation/prepare-erc20.sh | 4 +- .../src/rust_lite/extract_preprocessed.py | 43 +++++++++++++++++++ ulm-semantics/main/encoding.md | 2 - ulm-semantics/main/encoding/impl.md | 22 ---------- ulm-semantics/main/encoding/syntax.md | 3 -- .../targets/preprocessing/configuration.md | 9 ++-- 8 files changed, 60 insertions(+), 38 deletions(-) create mode 100644 rust-lite/src/rust_lite/extract_preprocessed.py delete mode 100644 ulm-semantics/main/encoding/impl.md diff --git a/README.md b/README.md index a6921bd4..979f9455 100644 --- a/README.md +++ b/README.md @@ -23,8 +23,7 @@ make .build/ulm-preprocessing-kompiled/timestamp compilation/prepare-erc20.sh ``` -The above will produce a configuration whose `` cell contains -`ulmEncodedPreprocessedCell(contract-bytes:Bytes)` +The above will produce a cell containing the full preprocessed contract. Running the contract requires a different semantics (there main difference from the above is the setup of the `` cell; there are other small differences, but diff --git a/compilation/prepare-contract.sh b/compilation/prepare-contract.sh index 4c8a3e5a..b995e675 100755 --- a/compilation/prepare-contract.sh +++ b/compilation/prepare-contract.sh @@ -4,14 +4,16 @@ # 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 +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 \ $TEMP_DIR/input.tmp \ @@ -20,3 +22,9 @@ krun \ --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 \ + $COMPILATION_DIR/$2 diff --git a/compilation/prepare-erc20.sh b/compilation/prepare-erc20.sh index 16e4a9a5..8ed0f563 100755 --- a/compilation/prepare-erc20.sh +++ b/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 \ + erc_20_token.preprocessed.kore diff --git a/rust-lite/src/rust_lite/extract_preprocessed.py b/rust-lite/src/rust_lite/extract_preprocessed.py new file mode 100644 index 00000000..f4e3cfe8 --- /dev/null +++ b/rust-lite/src/rust_lite/extract_preprocessed.py @@ -0,0 +1,43 @@ +from __future__ import annotations + +import sys +from pathlib import Path +from typing import TYPE_CHECKING + +from pyk.kore.parser import App, KoreParser + +if TYPE_CHECKING: + from pyk.kore.syntax import Pattern + + +def descend(patt: Pattern, path: list[str]) -> Pattern: + for s in path: + if not isinstance(patt, App): + raise ValueError(type(patt)) + new_patt: Pattern | None = None + for p in patt.args: + if isinstance(p, App): + print(p.symbol, s) + if p.symbol == s: + new_patt = p + break + if new_patt is None: + raise ValueError(patt.symbol) + patt = new_patt + return patt + + +def main(args: list[str]) -> None: + if len(args) != 2: + raise ValueError(args) + input_kore = Path(args[0]).read_text() + config = KoreParser(input_kore).pattern() + config = descend( + config, + ["Lbl'-LT-'ulm-full-preprocessed'-GT-'"], + ) + Path(args[1]).write_text(config.text) + + +if __name__ == '__main__': + main(sys.argv[1:]) diff --git a/ulm-semantics/main/encoding.md b/ulm-semantics/main/encoding.md index 6bd33ac2..fc901f64 100644 --- a/ulm-semantics/main/encoding.md +++ b/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 ``` diff --git a/ulm-semantics/main/encoding/impl.md b/ulm-semantics/main/encoding/impl.md deleted file mode 100644 index 5e10d96e..00000000 --- a/ulm-semantics/main/encoding/impl.md +++ /dev/null @@ -1,22 +0,0 @@ -```k - -module ULM-ENCODING-IMPL - imports private COMMON-K-CELL - imports private BYTES-SYNTAX - imports private ULM-ENCODING-SYNTAX - imports private ULM-FULL-PREPROCESSED-CONFIGURATION - - syntax Bytes ::= encodeUlmFullPreprocessedCell(UlmFullPreprocessedCell) - [function, hook(ULM.encode)] - - rule - - ulmEncodePreprocessedCell - => ulmEncodedPreprocessedCell(encodeUlmFullPreprocessedCell(Cell)) - ... - - Cell:UlmFullPreprocessedCell - -endmodule - -``` diff --git a/ulm-semantics/main/encoding/syntax.md b/ulm-semantics/main/encoding/syntax.md index d7688cb9..2e65f554 100644 --- a/ulm-semantics/main/encoding/syntax.md +++ b/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 diff --git a/ulm-semantics/targets/preprocessing/configuration.md b/ulm-semantics/targets/preprocessing/configuration.md index e14d30b6..ccf73101 100644 --- a/ulm-semantics/targets/preprocessing/configuration.md +++ b/ulm-semantics/targets/preprocessing/configuration.md @@ -15,7 +15,6 @@ module COMMON-K-CELL cratesParser($PGM:WrappedCrateList) ~> ulmPreprocessCrates - ~> ulmEncodePreprocessedCell endmodule @@ -25,11 +24,9 @@ module ULM-TARGET-CONFIGURATION imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION configuration - - - - - + + + endmodule ``` From af7980ee5a4d4bb8e84e76ec4e0bd2c164eb6dfa Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 19 Nov 2024 19:07:24 +0200 Subject: [PATCH 2/7] Compile the execution target for ulm execution --- Makefile | 36 ++++++++++++++++++++++++++++-------- 1 file changed, 28 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index 26df69aa..b70bd4fc 100644 --- a/Makefile +++ b/Makefile @@ -96,10 +96,12 @@ clean: build: $(RUST_PREPROCESSING_TIMESTAMP) \ $(RUST_EXECUTION_TIMESTAMP) \ - $(ULM_EXECUTION_TIMESTAMP) \ $(ULM_PREPROCESSING_TIMESTAMP) \ $(ULM_TESTING_TIMESTAMP) +build-ulm: $(ULM_EXECUTION_TIMESTAMP) \ + $(ULM_PREPROCESSING_TIMESTAMP) \ + build-legacy: \ $(MX_TESTING_TIMESTAMP) \ $(MX_RUST_TIMESTAMP) \ @@ -184,17 +186,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 + -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 From 1187a8118847550080a03432c6d0e99401815bb7 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 19 Nov 2024 19:34:37 +0200 Subject: [PATCH 3/7] Attempt to generate contract binary --- Makefile | 12 ++++++++++++ compilation/prepare-contract.sh | 7 ++++++- compilation/prepare-erc20.sh | 2 +- 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index b70bd4fc..5f60cfa6 100644 --- a/Makefile +++ b/Makefile @@ -101,6 +101,7 @@ build: $(RUST_PREPROCESSING_TIMESTAMP) \ build-ulm: $(ULM_EXECUTION_TIMESTAMP) \ $(ULM_PREPROCESSING_TIMESTAMP) \ + .build/emit-contract-bytes build-legacy: \ $(MX_TESTING_TIMESTAMP) \ @@ -240,6 +241,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 $@ diff --git a/compilation/prepare-contract.sh b/compilation/prepare-contract.sh index b995e675..2fd696b4 100755 --- a/compilation/prepare-contract.sh +++ b/compilation/prepare-contract.sh @@ -27,4 +27,9 @@ poetry -C rust-lite install poetry -C rust-lite run python \ -m rust_lite.extract_preprocessed \ $TEMP_DIR/output.kore \ - $COMPILATION_DIR/$2 + $TEMP_DIR/output.preprocessed.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 diff --git a/compilation/prepare-erc20.sh b/compilation/prepare-erc20.sh index 8ed0f563..f9bed9d3 100755 --- a/compilation/prepare-erc20.sh +++ b/compilation/prepare-erc20.sh @@ -6,4 +6,4 @@ set -e compilation/prepare-contract.sh \ tests/ulm-contracts/erc_20_token.rs \ - erc_20_token.preprocessed.kore + .build/compilation/erc_20_token.preprocessed.kore From b635721c91f8e8d9a18e174525000eb40027a4d8 Mon Sep 17 00:00:00 2001 From: Virgil Date: Tue, 19 Nov 2024 19:59:02 +0200 Subject: [PATCH 4/7] Prevent weird emit-contract-bytes crash --- ulm-semantics/targets/execution/configuration.md | 3 +++ ulm-semantics/targets/execution/ulm-target.md | 6 ++++++ 2 files changed, 9 insertions(+) diff --git a/ulm-semantics/targets/execution/configuration.md b/ulm-semantics/targets/execution/configuration.md index b14867e2..47862f25 100644 --- a/ulm-semantics/targets/execution/configuration.md +++ b/ulm-semantics/targets/execution/configuration.md @@ -22,12 +22,15 @@ module ULM-TARGET-CONFIGURATION imports RUST-EXECUTION-CONFIGURATION imports ULM-CONFIGURATION imports ULM-FULL-PREPROCESSED-CONFIGURATION + imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION configuration + + endmodule ``` diff --git a/ulm-semantics/targets/execution/ulm-target.md b/ulm-semantics/targets/execution/ulm-target.md index 5e931ea0..7e433e89 100644 --- a/ulm-semantics/targets/execution/ulm-target.md +++ b/ulm-semantics/targets/execution/ulm-target.md @@ -1,20 +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/rust-common.md" requires "rust-semantics/rust-common-syntax.md" + module ULM-TARGET-SYNTAX endmodule module ULM-TARGET imports private RUST-COMMON 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 ``` From d20806004b9d48dc47404e3cd178e0808151ba44 Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 20 Nov 2024 15:44:47 +0200 Subject: [PATCH 5/7] Update the documentation --- README.md | 29 ++++++++++------------------- 1 file changed, 10 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index 979f9455..828e9740 100644 --- a/README.md +++ b/README.md @@ -13,26 +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 cell containing the full preprocessed contract. - -Running the contract requires a different semantics (there main difference from -the above is the setup of the `` 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 `` cell in a similar way to the `SIMPLE-ulm` example. From c62c47270307c81d87d57a3f2d9af95971bcc871 Mon Sep 17 00:00:00 2001 From: Virgil Date: Fri, 22 Nov 2024 18:39:48 +0200 Subject: [PATCH 6/7] Remove the preprocessing target --- Makefile | 16 ---------- compilation/prepare-contract.sh | 20 ++++-------- ulm-semantics/main/decoding.md | 2 -- ulm-semantics/main/decoding/impl.md | 16 ---------- ulm-semantics/main/decoding/syntax.md | 4 ++- .../targets/execution/configuration.md | 5 ++- ulm-semantics/targets/execution/ulm-target.md | 4 ++- .../targets/preprocessing/configuration.md | 32 ------------------- .../targets/preprocessing/ulm-target.md | 17 ---------- 9 files changed, 16 insertions(+), 100 deletions(-) delete mode 100644 ulm-semantics/main/decoding/impl.md delete mode 100644 ulm-semantics/targets/preprocessing/configuration.md delete mode 100644 ulm-semantics/targets/preprocessing/ulm-target.md 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 - ulmDecodePreprocessedCell(B:Bytes) => .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 - ulmDecodePreprocessedCell($PGM:Bytes) + cratesParser(ulmDecodeRustCrates($PGM:Bytes)) + ~> ulmPreprocessCrates ~> ulmExecute($CREATE:Bool, $PGM:Bytes, $ACCTCODE:Int, $GAS:Int) 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 - - cratesParser($PGM:WrappedCrateList) - ~> ulmPreprocessCrates - -endmodule - -module ULM-TARGET-CONFIGURATION - imports COMMON-K-CELL - imports ULM-FULL-PREPROCESSED-CONFIGURATION - imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION - - configuration - - - -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 - -``` From bb40e1e3f6fdce043304713c14346e4caafab16d Mon Sep 17 00:00:00 2001 From: Virgil Date: Mon, 25 Nov 2024 22:51:48 +0200 Subject: [PATCH 7/7] Remove unneeded file --- .../src/rust_lite/extract_preprocessed.py | 43 ------------------- 1 file changed, 43 deletions(-) delete mode 100644 rust-lite/src/rust_lite/extract_preprocessed.py diff --git a/rust-lite/src/rust_lite/extract_preprocessed.py b/rust-lite/src/rust_lite/extract_preprocessed.py deleted file mode 100644 index f4e3cfe8..00000000 --- a/rust-lite/src/rust_lite/extract_preprocessed.py +++ /dev/null @@ -1,43 +0,0 @@ -from __future__ import annotations - -import sys -from pathlib import Path -from typing import TYPE_CHECKING - -from pyk.kore.parser import App, KoreParser - -if TYPE_CHECKING: - from pyk.kore.syntax import Pattern - - -def descend(patt: Pattern, path: list[str]) -> Pattern: - for s in path: - if not isinstance(patt, App): - raise ValueError(type(patt)) - new_patt: Pattern | None = None - for p in patt.args: - if isinstance(p, App): - print(p.symbol, s) - if p.symbol == s: - new_patt = p - break - if new_patt is None: - raise ValueError(patt.symbol) - patt = new_patt - return patt - - -def main(args: list[str]) -> None: - if len(args) != 2: - raise ValueError(args) - input_kore = Path(args[0]).read_text() - config = KoreParser(input_kore).pattern() - config = descend( - config, - ["Lbl'-LT-'ulm-full-preprocessed'-GT-'"], - ) - Path(args[1]).write_text(config.text) - - -if __name__ == '__main__': - main(sys.argv[1:])