diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..662c1e1 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "deps/ulm"] + path = deps/ulm + url = git@github.com:Pi-Squared-Inc/ulm diff --git a/Dockerfile b/Dockerfile index 418d523..20b4ca2 100644 --- a/Dockerfile +++ b/Dockerfile @@ -12,7 +12,8 @@ COPY --from=Z3 /usr/bin/z3 /usr/bin/z3 RUN apt-get update \ && apt-get upgrade --yes \ && apt-get install --yes \ - curl + curl \ + libcrypto++-dev # cmake \ # pandoc \ # python3 \ diff --git a/Makefile b/Makefile index 26e8e57..4744c99 100644 --- a/Makefile +++ b/Makefile @@ -87,6 +87,23 @@ UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-with-contract/output UKM_WITH_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/*.run) UKM_WITH_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_WITH_CONTRACT_TESTING_INPUTS)) +UKM_FLAGS ::= -I deps/ulm/kllvm \ + -ccopt -Ldeps/ulm/kllvm \ + -ccopt -lulmkllvm + +# TODO: Use a plugin directory that is accessible from the current project +CRYPTO_FLAGS ::= -I ../evm-semantics/kevm-pyk/src/kevm_pyk/kproj/plugin \ + -ccopt -lssl \ + -ccopt -lcrypto \ + -ccopt -lsecp256k1 \ + -ccopt $KRYPTO_DIR/evm-semantics/plugin/krypto.a \ + +# PLUGIN_FLAGS ::= --hook-namespaces 'ULM KRYPTO' +PLUGIN_FLAGS ::= --hook-namespaces 'ULM' \ + -ccopt -std=c++17 \ + ${UKM_FLAGS} \ + # ${CRYPTO_FLAGS} + .PHONY: clean build build-legacy test test-legacy syntax-test preprocessing-test execution-test mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test ukm-no-contracts-test all: build test @@ -134,6 +151,10 @@ ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS) ukm-with-contracts-test: $(UKM_WITH_CONTRACT_TESTING_OUTPUTS) +ulm-plugin: + make -C deps/ulm/kllvm/ libulmkllvm.so +.PHONY: ulm-plugin + $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(RUST_PREPROCESSING_KOMPILED) @@ -197,10 +218,11 @@ $(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) -I . \ --debug -$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) +$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) ulm-plugin # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(UKM_TESTING_KOMPILED) $$(which kompile) ukm-semantics/targets/testing/ukm-target.md \ + ${PLUGIN_FLAGS} \ --emit-json -o $(UKM_TESTING_KOMPILED) \ -I . \ --debug diff --git a/deps/ulm b/deps/ulm new file mode 160000 index 0000000..6e9f77b --- /dev/null +++ b/deps/ulm @@ -0,0 +1 @@ +Subproject commit 6e9f77b14af106d0b97b05bdc1aff47b059988c9 diff --git a/ukm-semantics/main/decoding.md b/ukm-semantics/main/decoding.md index 3561da2..8d41757 100644 --- a/ukm-semantics/main/decoding.md +++ b/ukm-semantics/main/decoding.md @@ -1,8 +1,10 @@ ```k +requires "decoding/impl.md" requires "decoding/syntax.md" module UKM-DECODING + imports private UKM-DECODING-IMPL endmodule ``` diff --git a/ukm-semantics/main/decoding/impl.md b/ukm-semantics/main/decoding/impl.md new file mode 100644 index 0000000..631bbe6 --- /dev/null +++ b/ukm-semantics/main/decoding/impl.md @@ -0,0 +1,16 @@ +```k + +module UKM-DECODING-IMPL + imports private COMMON-K-CELL + imports private UKM-DECODING-SYNTAX + imports private UKM-FULL-PREPROCESSED-CONFIGURATION + + syntax UkmFullPreprocessedCell ::= decodeUkmFullPreprocessedCell(Bytes) + [function, hook(ULM.decode)] + + rule + ukmDecodePreprocessedCell(B:Bytes) => .K ... + (_:UkmFullPreprocessedCell => decodeUkmFullPreprocessedCell(B)) +endmodule + +``` diff --git a/ukm-semantics/main/encoding.md b/ukm-semantics/main/encoding.md index 9f08445..eeb1cdf 100644 --- a/ukm-semantics/main/encoding.md +++ b/ukm-semantics/main/encoding.md @@ -1,8 +1,10 @@ ```k +requires "encoding/impl.md" requires "encoding/syntax.md" module UKM-ENCODING + imports private UKM-ENCODING-IMPL endmodule ``` diff --git a/ukm-semantics/main/encoding/impl.md b/ukm-semantics/main/encoding/impl.md new file mode 100644 index 0000000..d0f10b0 --- /dev/null +++ b/ukm-semantics/main/encoding/impl.md @@ -0,0 +1,22 @@ +```k + +module UKM-ENCODING-IMPL + imports private COMMON-K-CELL + imports private BYTES-SYNTAX + imports private UKM-ENCODING-SYNTAX + imports private UKM-FULL-PREPROCESSED-CONFIGURATION + + syntax Bytes ::= encodeUkmFullPreprocessedCell(UkmFullPreprocessedCell) + [function, hook(ULM.encode)] + + rule + + ukmEncodePreprocessedCell + => ukmEncodedPreprocessedCell(encodeUkmFullPreprocessedCell(Cell)) + ... + + Cell:UkmFullPreprocessedCell + +endmodule + +``` diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index d303075..bd0dab4 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -4,6 +4,7 @@ module UKM-ENCODING-SYNTAX imports BYTES-SYNTAX syntax UKMInstruction ::= "ukmEncodePreprocessedCell" + | ukmEncodedPreprocessedCell(Bytes) endmodule diff --git a/ukm-semantics/targets/testing/configuration.md b/ukm-semantics/targets/testing/configuration.md index 7d3a7c8..cc4bb5c 100644 --- a/ukm-semantics/targets/testing/configuration.md +++ b/ukm-semantics/targets/testing/configuration.md @@ -9,12 +9,16 @@ requires "rust-semantics/test/configuration.md" module COMMON-K-CELL imports private RUST-EXECUTION-TEST-PARSING-SYNTAX imports private RUST-PREPROCESSING-SYNTAX + imports private UKM-ENCODING-SYNTAX imports private UKM-PREPROCESSING-SYNTAX + imports private UKM-TEST-SYNTAX configuration cratesParser($PGM:WrappedCrateList) ~> ukmPreprocessCrates + ~> ukmEncodePreprocessedCell + ~> ukmDecodePreprocessedCell ~> $TEST:ExecutionTest endmodule diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index 1321ddc..bfd9566 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ukm-semantics/targets/testing/ukm-target.md @@ -1,5 +1,7 @@ ```k +requires "../../main/decoding.md" +requires "../../main/encoding.md" requires "../../main/execution.md" requires "../../main/preprocessing.md" requires "../../test/execution.md" @@ -18,6 +20,8 @@ module UKM-TARGET imports private RUST-COMMON imports private RUST-FULL-PREPROCESSING imports private RUST-EXECUTION-TEST + imports private UKM-DECODING + imports private UKM-ENCODING imports private UKM-EXECUTION imports private UKM-PREPROCESSING imports private UKM-TARGET-CONFIGURATION diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index fef9839..b86ed3a 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -5,6 +5,8 @@ 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 @@ -19,6 +21,8 @@ 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 @@ -27,6 +31,10 @@ 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