diff --git a/.gitignore b/.gitignore index f4bbed0..0b667e7 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,4 @@ .build .DS_store -blockchain-k-plugin tmp tmp.* diff --git a/.gitmodules b/.gitmodules index 3558764..aeb6745 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "blockchain-k-plugin"] path = deps/blockchain-k-plugin - url = https://github.com/runtimeverification/blockchain-k-plugin + url = https://github.com/runtimeverification/blockchain-k-plugin \ No newline at end of file diff --git a/Makefile b/Makefile index 1e5b67f..3f8fd45 100644 --- a/Makefile +++ b/Makefile @@ -64,30 +64,30 @@ DEMOS_TESTING_OUTPUT_DIR ::= .build/demos/output DEMOS_TESTING_INPUTS ::= $(wildcard $(DEMOS_TESTING_INPUT_DIR)/*.run) DEMOS_TESTING_OUTPUTS ::= $(patsubst $(DEMOS_TESTING_INPUT_DIR)/%,$(DEMOS_TESTING_OUTPUT_DIR)/%.executed.kore,$(DEMOS_TESTING_INPUTS)) -UKM_SEMANTICS_FILES ::= $(shell find ukm-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')') +ULM_SEMANTICS_FILES ::= $(shell find ulm-semantics/ -type f -a '(' -name '*.md' -or -name '*.k' ')') -UKM_EXECUTION_KOMPILED ::= .build/ukm-execution-kompiled -UKM_EXECUTION_TIMESTAMP ::= $(UKM_EXECUTION_KOMPILED)/timestamp +ULM_EXECUTION_KOMPILED ::= .build/ulm-execution-kompiled +ULM_EXECUTION_TIMESTAMP ::= $(ULM_EXECUTION_KOMPILED)/timestamp -UKM_PREPROCESSING_KOMPILED ::= .build/ukm-preprocessing-kompiled -UKM_PREPROCESSING_TIMESTAMP ::= $(UKM_PREPROCESSING_KOMPILED)/timestamp +ULM_PREPROCESSING_KOMPILED ::= .build/ulm-preprocessing-kompiled +ULM_PREPROCESSING_TIMESTAMP ::= $(ULM_PREPROCESSING_KOMPILED)/timestamp -UKM_TESTING_KOMPILED ::= .build/ukm-testing-kompiled -UKM_TESTING_TIMESTAMP ::= $(UKM_TESTING_KOMPILED)/timestamp +ULM_TESTING_KOMPILED ::= .build/ulm-testing-kompiled +ULM_TESTING_TIMESTAMP ::= $(ULM_TESTING_KOMPILED)/timestamp -UKM_CONTRACTS_TESTING_INPUT_DIR ::= tests/ukm-contracts +ULM_CONTRACTS_TESTING_INPUT_DIR ::= tests/ulm-contracts -UKM_NO_CONTRACT_TESTING_INPUT_DIR ::= tests/ukm-no-contract -UKM_NO_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ukm-no-contract/output -UKM_NO_CONTRACT_TESTING_INPUTS ::= $(wildcard $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/*.run) -UKM_NO_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/%,$(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(UKM_NO_CONTRACT_TESTING_INPUTS)) +ULM_NO_CONTRACT_TESTING_INPUT_DIR ::= tests/ulm-no-contract +ULM_NO_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ulm-no-contract/output +ULM_NO_CONTRACT_TESTING_INPUTS ::= $(wildcard $(ULM_NO_CONTRACT_TESTING_INPUT_DIR)/*.run) +ULM_NO_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(ULM_NO_CONTRACT_TESTING_INPUT_DIR)/%,$(ULM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(ULM_NO_CONTRACT_TESTING_INPUTS)) -UKM_WITH_CONTRACT_TESTING_INPUT_DIR ::= tests/ukm-with-contract -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)) +ULM_WITH_CONTRACT_TESTING_INPUT_DIR ::= tests/ulm-with-contract +ULM_WITH_CONTRACT_TESTING_OUTPUT_DIR ::= .build/ulm-with-contract/output +ULM_WITH_CONTRACT_TESTING_INPUTS ::= $(wildcard $(ULM_WITH_CONTRACT_TESTING_INPUT_DIR)/*.run) +ULM_WITH_CONTRACT_TESTING_OUTPUTS ::= $(patsubst $(ULM_WITH_CONTRACT_TESTING_INPUT_DIR)/%,$(ULM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.executed.kore,$(ULM_WITH_CONTRACT_TESTING_INPUTS)) -.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 +.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 ulm-no-contracts-test all: build test @@ -96,9 +96,9 @@ clean: build: $(RUST_PREPROCESSING_TIMESTAMP) \ $(RUST_EXECUTION_TIMESTAMP) \ - $(UKM_EXECUTION_TIMESTAMP) \ - $(UKM_PREPROCESSING_TIMESTAMP) \ - $(UKM_TESTING_TIMESTAMP) + $(ULM_EXECUTION_TIMESTAMP) \ + $(ULM_PREPROCESSING_TIMESTAMP) \ + $(ULM_TESTING_TIMESTAMP) build-legacy: \ $(MX_TESTING_TIMESTAMP) \ @@ -108,7 +108,7 @@ build-legacy: \ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP) -test: build syntax-test preprocessing-test execution-test crates-test ukm-no-contracts-test ukm-with-contracts-test +test: build syntax-test preprocessing-test execution-test crates-test ulm-no-contracts-test ulm-with-contracts-test test-legacy: mx-test mx-rust-test mx-rust-contract-test mx-rust-two-contracts-test demos-test @@ -130,9 +130,9 @@ mx-rust-two-contracts-test: $(MX_RUST_TWO_CONTRACTS_TESTING_OUTPUTS) demos-test: $(DEMOS_TESTING_OUTPUTS) -ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS) +ulm-no-contracts-test: $(ULM_NO_CONTRACT_TESTING_OUTPUTS) -ukm-with-contracts-test: $(UKM_WITH_CONTRACT_TESTING_OUTPUTS) +ulm-with-contracts-test: $(ULM_WITH_CONTRACT_TESTING_OUTPUTS) deps/blockchain-k-plugin/build/krypto/lib/krypto.a: make -C deps/blockchain-k-plugin build @@ -184,37 +184,37 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTI -I . \ --debug -$(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) deps/blockchain-k-plugin/build/krypto/lib/krypto.a +$(ULM_EXECUTION_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 $(UKM_EXECUTION_KOMPILED) - $$(which kompile) ukm-semantics/targets/execution/ukm-target.md \ + -rm -r $(ULM_EXECUTION_KOMPILED) + $$(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 $(UKM_EXECUTION_KOMPILED) \ + --emit-json -o $(ULM_EXECUTION_KOMPILED) \ -I kllvm \ -I deps/blockchain-k-plugin \ -I . \ --debug -$(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) deps/blockchain-k-plugin/build/krypto/lib/krypto.a +$(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 $(UKM_PREPROCESSING_KOMPILED) - $$(which kompile) ukm-semantics/targets/preprocessing/ukm-target.md \ + -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 $(UKM_PREPROCESSING_KOMPILED) \ + --emit-json -o $(ULM_PREPROCESSING_KOMPILED) \ -I . \ -I deps/blockchain-k-plugin \ --debug -$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) deps/blockchain-k-plugin/build/krypto/lib/krypto.a +$(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 $(UKM_TESTING_KOMPILED) - $$(which kompile) ukm-semantics/targets/testing/ukm-target.md \ + -rm -r $(ULM_TESTING_KOMPILED) + $$(which kompile) ulm-semantics/targets/testing/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' \ ${PLUGIN_FLAGS} \ - --emit-json -o $(UKM_TESTING_KOMPILED) \ + --emit-json -o $(ULM_TESTING_KOMPILED) \ -I . \ -I deps/blockchain-k-plugin \ -I kllvm \ @@ -408,26 +408,26 @@ $(CRATES_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ # TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs # as a dependency -$(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ - $(UKM_NO_CONTRACT_TESTING_INPUT_DIR)/%.run \ - $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs \ - $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs \ - $(UKM_TESTING_TIMESTAMP) \ +$(ULM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ + $(ULM_NO_CONTRACT_TESTING_INPUT_DIR)/%.run \ + $(ULM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs \ + $(ULM_CONTRACTS_TESTING_INPUT_DIR)/ulm.rs \ + $(ULM_TESTING_TIMESTAMP) \ $(wildcard parsers/inc-*.sh) \ - parsers/crates-ukm-testing-execution.sh \ - parsers/test-ukm-testing-execution.sh - mkdir -p $(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR) + parsers/crates-ulm-testing-execution.sh \ + parsers/test-ulm-testing-execution.sh + mkdir -p $(ULM_NO_CONTRACT_TESTING_OUTPUT_DIR) echo "<(<" > $@.in.tmp echo "::bytes_hooks" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp # echo "<(<" > $@.in.tmp - # echo "::ukm" >> $@.in.tmp + # echo "::ulm" >> $@.in.tmp # echo "<|>" >> $@.in.tmp - # cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs >> $@.in.tmp + # cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/ulm.rs >> $@.in.tmp # echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp @@ -438,68 +438,68 @@ $(UKM_NO_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ krun \ $@.in.tmp \ - --parser $(CURDIR)/parsers/crates-ukm-testing-execution.sh \ - --definition $(UKM_TESTING_KOMPILED) \ + --parser $(CURDIR)/parsers/crates-ulm-testing-execution.sh \ + --definition $(ULM_TESTING_KOMPILED) \ --output kore \ --output-file $@.tmp \ -cTEST='$(shell cat $<)' \ - -pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh + -pTEST=$(CURDIR)/parsers/test-ulm-testing-execution.sh cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" mv -f $@.tmp $@ # TODO: Add $(shell echo "$<" | sed 's/\.[^.]*.run$$//').rs # as a dependency -$(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ - $(UKM_WITH_CONTRACT_TESTING_INPUT_DIR)/%.run \ - $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs \ - $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs \ - $(UKM_TESTING_TIMESTAMP) \ +$(ULM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ + $(ULM_WITH_CONTRACT_TESTING_INPUT_DIR)/%.run \ + $(ULM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs \ + $(ULM_CONTRACTS_TESTING_INPUT_DIR)/ulm.rs \ + $(ULM_TESTING_TIMESTAMP) \ $(wildcard parsers/inc-*.sh) \ - parsers/crates-ukm-testing-execution.sh \ - parsers/test-ukm-testing-execution.sh - mkdir -p $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR) + parsers/crates-ulm-testing-execution.sh \ + parsers/test-ulm-testing-execution.sh + mkdir -p $(ULM_WITH_CONTRACT_TESTING_OUTPUT_DIR) echo "<(<" > $@.in.tmp echo "::address" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/address.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/address.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp echo "::bytes_hooks" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp echo "::test_helpers" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/test_helpers.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/test_helpers.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp echo "::helpers" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/helpers.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/helpers.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp echo "::state_hooks" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/state_hooks.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/state_hooks.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp echo "::single_value_mapper" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/single_value_mapper.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/single_value_mapper.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp - echo "::ukm" >> $@.in.tmp + echo "::ulm" >> $@.in.tmp echo "<|>" >> $@.in.tmp - cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/ukm.rs >> $@.in.tmp + cat $(ULM_CONTRACTS_TESTING_INPUT_DIR)/ulm.rs >> $@.in.tmp echo ">)>" >> $@.in.tmp echo "<(<" >> $@.in.tmp @@ -510,11 +510,11 @@ $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ krun \ $@.in.tmp \ - --parser $(CURDIR)/parsers/crates-ukm-testing-execution.sh \ - --definition $(UKM_TESTING_KOMPILED) \ + --parser $(CURDIR)/parsers/crates-ulm-testing-execution.sh \ + --definition $(ULM_TESTING_KOMPILED) \ --output kore \ --output-file $@.tmp \ -cTEST='$(shell cat $<)' \ - -pTEST=$(CURDIR)/parsers/test-ukm-testing-execution.sh + -pTEST=$(CURDIR)/parsers/test-ulm-testing-execution.sh cat $@.tmp | grep -q "Lbl'-LT-'k'-GT-'{}(dotk{}())" mv -f $@.tmp $@ diff --git a/compilation/prepare-contract.sh b/compilation/prepare-contract.sh index 9bf5555..8155457 100755 --- a/compilation/prepare-contract.sh +++ b/compilation/prepare-contract.sh @@ -5,8 +5,8 @@ set -e -UKM_CONTRACTS_TESTING_INPUT_DIR=tests/ukm-contracts -UKM_PREPROCESSING_KOMPILED=.build/ukm-preprocessing-kompiled +ULM_CONTRACTS_TESTING_INPUT_DIR=tests/ulm-contracts +ULM_PREPROCESSING_KOMPILED=.build/ulm-preprocessing-kompiled TEMP_DIR=tmp mkdir -p $TEMP_DIR @@ -14,43 +14,43 @@ mkdir -p $TEMP_DIR echo "<(<" > $TEMP_DIR/input.tmp echo "::address" >> $TEMP_DIR/input.tmp echo "<|>" >> $TEMP_DIR/input.tmp -cat $UKM_CONTRACTS_TESTING_INPUT_DIR/address.rs >> $TEMP_DIR/input.tmp +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/address.rs >> $TEMP_DIR/input.tmp echo ">)>" >> $TEMP_DIR/input.tmp echo "<(<" >> $TEMP_DIR/input.tmp echo "::bytes_hooks" >> $TEMP_DIR/input.tmp echo "<|>" >> $TEMP_DIR/input.tmp -cat $UKM_CONTRACTS_TESTING_INPUT_DIR/bytes_hooks.rs >> $TEMP_DIR/input.tmp +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/bytes_hooks.rs >> $TEMP_DIR/input.tmp echo ">)>" >> $TEMP_DIR/input.tmp echo "<(<" >> $TEMP_DIR/input.tmp echo "::test_helpers" >> $TEMP_DIR/input.tmp echo "<|>" >> $TEMP_DIR/input.tmp -cat $UKM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $TEMP_DIR/input.tmp +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $TEMP_DIR/input.tmp echo ">)>" >> $TEMP_DIR/input.tmp echo "<(<" >> $TEMP_DIR/input.tmp echo "::helpers" >> $TEMP_DIR/input.tmp echo "<|>" >> $TEMP_DIR/input.tmp -cat $UKM_CONTRACTS_TESTING_INPUT_DIR/helpers.rs >> $TEMP_DIR/input.tmp +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/helpers.rs >> $TEMP_DIR/input.tmp echo ">)>" >> $TEMP_DIR/input.tmp echo "<(<" >> $TEMP_DIR/input.tmp echo "::state_hooks" >> $TEMP_DIR/input.tmp echo "<|>" >> $TEMP_DIR/input.tmp -cat $UKM_CONTRACTS_TESTING_INPUT_DIR/state_hooks.rs >> $TEMP_DIR/input.tmp +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/state_hooks.rs >> $TEMP_DIR/input.tmp echo ">)>" >> $TEMP_DIR/input.tmp echo "<(<" >> $TEMP_DIR/input.tmp echo "::single_value_mapper" >> $TEMP_DIR/input.tmp echo "<|>" >> $TEMP_DIR/input.tmp -cat $UKM_CONTRACTS_TESTING_INPUT_DIR/single_value_mapper.rs >> $TEMP_DIR/input.tmp +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/single_value_mapper.rs >> $TEMP_DIR/input.tmp echo ">)>" >> $TEMP_DIR/input.tmp echo "<(<" >> $TEMP_DIR/input.tmp -echo "::ukm" >> $TEMP_DIR/input.tmp +echo "::ulm" >> $TEMP_DIR/input.tmp echo "<|>" >> $TEMP_DIR/input.tmp -cat $UKM_CONTRACTS_TESTING_INPUT_DIR/ukm.rs >> $TEMP_DIR/input.tmp +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/ulm.rs >> $TEMP_DIR/input.tmp echo ">)>" >> $TEMP_DIR/input.tmp echo "<(<" >> $TEMP_DIR/input.tmp @@ -61,8 +61,8 @@ echo ">)>" >> $TEMP_DIR/input.tmp krun \ $TEMP_DIR/input.tmp \ - --parser $(pwd)/parsers/crates-ukm-preprocessing-execution.sh \ - --definition $UKM_PREPROCESSING_KOMPILED \ + --parser $(pwd)/parsers/crates-ulm-preprocessing-execution.sh \ + --definition $ULM_PREPROCESSING_KOMPILED \ --output kore \ --output-file $TEMP_DIR/output.kore \ diff --git a/compilation/prepare-erc20.sh b/compilation/prepare-erc20.sh index 3fc541d..16e4a9a 100755 --- a/compilation/prepare-erc20.sh +++ b/compilation/prepare-erc20.sh @@ -4,4 +4,4 @@ set -e -compilation/prepare-contract.sh tests/ukm-contracts/erc_20_token.rs "1000000000000000000_u256," +compilation/prepare-contract.sh tests/ulm-contracts/erc_20_token.rs "1000000000000000000_u256," diff --git a/deps/blockchain-k-plugin b/deps/blockchain-k-plugin index e6994c2..a6b4c7d 160000 --- a/deps/blockchain-k-plugin +++ b/deps/blockchain-k-plugin @@ -1 +1 @@ -Subproject commit e6994c21c59dd2d15ddb97d5169d78aa6645a8fb +Subproject commit a6b4c7d851afd9e2729901b515c6e699464611d7 diff --git a/parsers/args-ukm-preprocessing-execution.sh b/parsers/args-ulm-preprocessing-execution.sh similarity index 79% rename from parsers/args-ukm-preprocessing-execution.sh rename to parsers/args-ulm-preprocessing-execution.sh index 9de7193..9a81689 100755 --- a/parsers/args-ukm-preprocessing-execution.sh +++ b/parsers/args-ulm-preprocessing-execution.sh @@ -9,5 +9,5 @@ function parse_args() { $2 } -parse_args .build/ukm-preprocessing-kompiled $1 +parse_args .build/ulm-preprocessing-kompiled $1 diff --git a/parsers/crates-ukm-preprocessing-execution.sh b/parsers/crates-ulm-preprocessing-execution.sh similarity index 51% rename from parsers/crates-ukm-preprocessing-execution.sh rename to parsers/crates-ulm-preprocessing-execution.sh index 03545b7..2347469 100755 --- a/parsers/crates-ukm-preprocessing-execution.sh +++ b/parsers/crates-ulm-preprocessing-execution.sh @@ -2,4 +2,4 @@ source ${BASH_SOURCE%/*}/inc-crates.sh -parse_crates .build/ukm-preprocessing-kompiled $1 +parse_crates .build/ulm-preprocessing-kompiled $1 diff --git a/parsers/crates-ukm-testing-execution.sh b/parsers/crates-ulm-testing-execution.sh similarity index 55% rename from parsers/crates-ukm-testing-execution.sh rename to parsers/crates-ulm-testing-execution.sh index 5c0d00e..d10577a 100755 --- a/parsers/crates-ukm-testing-execution.sh +++ b/parsers/crates-ulm-testing-execution.sh @@ -2,4 +2,4 @@ source ${BASH_SOURCE%/*}/inc-crates.sh -parse_crates .build/ukm-testing-kompiled $1 +parse_crates .build/ulm-testing-kompiled $1 diff --git a/parsers/test-ukm-testing-execution.sh b/parsers/test-ukm-testing-execution.sh deleted file mode 100755 index 4107757..0000000 --- a/parsers/test-ukm-testing-execution.sh +++ /dev/null @@ -1,8 +0,0 @@ -#! /bin/bash - -kast \ - --output kore \ - --definition .build/ukm-testing-kompiled \ - --module UKM-TARGET-SYNTAX \ - --sort ExecutionTest \ - $1 diff --git a/parsers/test-ulm-testing-execution.sh b/parsers/test-ulm-testing-execution.sh new file mode 100755 index 0000000..594ab64 --- /dev/null +++ b/parsers/test-ulm-testing-execution.sh @@ -0,0 +1,8 @@ +#! /bin/bash + +kast \ + --output kore \ + --definition .build/ulm-testing-kompiled \ + --module ULM-TARGET-SYNTAX \ + --sort ExecutionTest \ + $1 diff --git a/tests/ukm-contracts/address.rs b/tests/ulm-contracts/address.rs similarity index 100% rename from tests/ukm-contracts/address.rs rename to tests/ulm-contracts/address.rs diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ulm-contracts/bytes_hooks.rs similarity index 100% rename from tests/ukm-contracts/bytes_hooks.rs rename to tests/ulm-contracts/bytes_hooks.rs diff --git a/tests/ukm-contracts/erc_20_token.rs b/tests/ulm-contracts/erc_20_token.rs similarity index 95% rename from tests/ukm-contracts/erc_20_token.rs rename to tests/ulm-contracts/erc_20_token.rs index f88b02a..6709262 100644 --- a/tests/ukm-contracts/erc_20_token.rs +++ b/tests/ulm-contracts/erc_20_token.rs @@ -11,7 +11,7 @@ #![no_std] #[allow(unused_imports)] -use ukm::*; +use ulm::*; /* ---------------------------------------------------------------------------- @@ -20,15 +20,15 @@ TODOs: - Reuse the implementation of ManagedBuffer for strings, and the annotations for the contract trait identification, as well as views, storage mappers, update, and inits; - - Support some sort of struct for implementing MessageResult within the UKM module. + - Support some sort of struct for implementing MessageResult within the ULM module. We also have to figure out the contents of MessageResult. Observations: - - ManagedAddress was replaced by an integer to fit the behaviors of UKM; + - ManagedAddress was replaced by an integer to fit the behaviors of ULM; ---------------------------------------------------------------------------- */ -#[ukm::contract] +#[ulm::contract] pub trait Erc20Token { // #[view(totalSupply)] #[storage_mapper("total_supply")] @@ -61,7 +61,7 @@ pub trait Erc20Token { fn init(&self, /*name: &ManagedBuffer, symbol: &ManagedBuffer, */init_supply: u256) { // self.s_name().set_if_empty(name); // self.s_symbol().set_if_empty(symbol); - self._mint(::ukm::Caller(), init_supply); + self._mint(::ulm::Caller(), init_supply); } #[upgrade] @@ -94,7 +94,7 @@ pub trait Erc20Token { #[endpoint(transfer)] fn transfer(&self, to: u160, value: u256) -> bool { - let owner = ::ukm::Caller(); + let owner = ::ulm::Caller(); self._transfer(&owner, to, &value); true } @@ -106,14 +106,14 @@ pub trait Erc20Token { #[endpoint(approve)] fn approve(&self, spender: u160, value: u256) -> bool { - let owner = ::ukm::Caller(); + let owner = ::ulm::Caller(); self._approve(&owner, spender, value, true); true } #[endpoint(transferFrom)] fn transfer_from(&self, from: u160, to: u160, value: u256) -> bool { - let spender = ::ukm::Caller(); + let spender = ::ulm::Caller(); self._spend_allowance(from, &spender, value); self._transfer(from, to, value); true diff --git a/tests/ukm-contracts/helpers.rs b/tests/ulm-contracts/helpers.rs similarity index 84% rename from tests/ukm-contracts/helpers.rs rename to tests/ulm-contracts/helpers.rs index 52b87aa..5acff16 100644 --- a/tests/ukm-contracts/helpers.rs +++ b/tests/ulm-contracts/helpers.rs @@ -1,6 +1,6 @@ fn require(condition: bool, message: str) { if !condition { - :: helpers :: fail(:: ukm :: EVMC_REVERT); + :: helpers :: fail(:: ulm :: EVMC_REVERT); } } diff --git a/tests/ukm-contracts/single_value_mapper.rs b/tests/ulm-contracts/single_value_mapper.rs similarity index 100% rename from tests/ukm-contracts/single_value_mapper.rs rename to tests/ulm-contracts/single_value_mapper.rs diff --git a/tests/ukm-contracts/state_hooks.rs b/tests/ulm-contracts/state_hooks.rs similarity index 100% rename from tests/ukm-contracts/state_hooks.rs rename to tests/ulm-contracts/state_hooks.rs diff --git a/tests/ukm-contracts/test_helpers.rs b/tests/ulm-contracts/test_helpers.rs similarity index 100% rename from tests/ukm-contracts/test_helpers.rs rename to tests/ulm-contracts/test_helpers.rs diff --git a/tests/ukm-contracts/ukm.rs b/tests/ulm-contracts/ulm.rs similarity index 100% rename from tests/ukm-contracts/ukm.rs rename to tests/ulm-contracts/ulm.rs diff --git a/tests/ukm-no-contract/test_bytes_hooks.append32.run b/tests/ulm-no-contract/test_bytes_hooks.append32.run similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.append32.run rename to tests/ulm-no-contract/test_bytes_hooks.append32.run diff --git a/tests/ukm-no-contract/test_bytes_hooks.append64.run b/tests/ulm-no-contract/test_bytes_hooks.append64.run similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.append64.run rename to tests/ulm-no-contract/test_bytes_hooks.append64.run diff --git a/tests/ukm-no-contract/test_bytes_hooks.appenddecode32.run b/tests/ulm-no-contract/test_bytes_hooks.appenddecode32.run similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.appenddecode32.run rename to tests/ulm-no-contract/test_bytes_hooks.appenddecode32.run diff --git a/tests/ukm-no-contract/test_bytes_hooks.appenddecode64.run b/tests/ulm-no-contract/test_bytes_hooks.appenddecode64.run similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.appenddecode64.run rename to tests/ulm-no-contract/test_bytes_hooks.appenddecode64.run diff --git a/tests/ukm-no-contract/test_bytes_hooks.appenddecodestr.run b/tests/ulm-no-contract/test_bytes_hooks.appenddecodestr.run similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.appenddecodestr.run rename to tests/ulm-no-contract/test_bytes_hooks.appenddecodestr.run diff --git a/tests/ukm-no-contract/test_bytes_hooks.appendstr.run b/tests/ulm-no-contract/test_bytes_hooks.appendstr.run similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.appendstr.run rename to tests/ulm-no-contract/test_bytes_hooks.appendstr.run diff --git a/tests/ukm-no-contract/test_bytes_hooks.empty.run b/tests/ulm-no-contract/test_bytes_hooks.empty.run similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.empty.run rename to tests/ulm-no-contract/test_bytes_hooks.empty.run diff --git a/tests/ukm-no-contract/test_bytes_hooks.rs b/tests/ulm-no-contract/test_bytes_hooks.rs similarity index 100% rename from tests/ukm-no-contract/test_bytes_hooks.rs rename to tests/ulm-no-contract/test_bytes_hooks.rs diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ulm-with-contract/endpoints.1.run similarity index 100% rename from tests/ukm-with-contract/endpoints.1.run rename to tests/ulm-with-contract/endpoints.1.run diff --git a/tests/ukm-with-contract/endpoints.2.run b/tests/ulm-with-contract/endpoints.2.run similarity index 100% rename from tests/ukm-with-contract/endpoints.2.run rename to tests/ulm-with-contract/endpoints.2.run diff --git a/tests/ukm-with-contract/endpoints.rs b/tests/ulm-with-contract/endpoints.rs similarity index 87% rename from tests/ukm-with-contract/endpoints.rs rename to tests/ulm-with-contract/endpoints.rs index 2fd7f61..aa970fd 100644 --- a/tests/ukm-with-contract/endpoints.rs +++ b/tests/ulm-with-contract/endpoints.rs @@ -1,9 +1,9 @@ #![no_std] #[allow(unused_imports)] -use ukm::*; +use ulm::*; -#[ukm::contract] +#[ulm::contract] pub trait Endpoints { #[init] fn init(&self) {} diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ulm-with-contract/erc_20_token.1.run similarity index 77% rename from tests/ukm-with-contract/erc_20_token.1.run rename to tests/ulm-with-contract/erc_20_token.1.run index a6cc960..1fa507f 100644 --- a/tests/ukm-with-contract/erc_20_token.1.run +++ b/tests/ulm-with-contract/erc_20_token.1.run @@ -1,25 +1,25 @@ -list_mock GetAccountStorageHook ( 7809087261546347641 ) ukmIntResult(0, u256); -list_mock SetAccountStorageHook ( 7809087261546347641 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(0, u256); -list_mock SetAccountStorageHook ( 7089066454178295295 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(10000, u256); -list_mock SetAccountStorageHook ( 7089066454178295295 , 9900 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(0, u256); -list_mock SetAccountStorageHook ( 7089066454179379067 , 100 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(100, u256); -list_mock SetAccountStorageHook ( 7089066454178299391 , 200 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454178299391 ) ukmIntResult(200, u256); -list_mock SetAccountStorageHook ( 7089066454178299391 , 0 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9900, u256); -list_mock SetAccountStorageHook ( 7089066454178295295 , 9700 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(100, u256); -list_mock SetAccountStorageHook ( 7089066454179379067 , 300 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9700, u256); -list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(300, u256); +list_mock GetAccountStorageHook ( 7809087261546347641 ) ulmIntResult(0, u256); +list_mock SetAccountStorageHook ( 7809087261546347641 , 10000 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(0, u256); +list_mock SetAccountStorageHook ( 7089066454178295295 , 10000 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(10000, u256); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(10000, u256); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(10000, u256); +list_mock SetAccountStorageHook ( 7089066454178295295 , 9900 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ulmIntResult(0, u256); +list_mock SetAccountStorageHook ( 7089066454179379067 , 100 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(9900, u256); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ulmIntResult(100, u256); +list_mock SetAccountStorageHook ( 7089066454178299391 , 200 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178299391 ) ulmIntResult(200, u256); +list_mock SetAccountStorageHook ( 7089066454178299391 , 0 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(9900, u256); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(9900, u256); +list_mock SetAccountStorageHook ( 7089066454178295295 , 9700 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ulmIntResult(100, u256); +list_mock SetAccountStorageHook ( 7089066454179379067 , 300 ) ulmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ulmIntResult(9700, u256); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ulmIntResult(300, u256); push "uint256"; hold_list_values_from_test_stack; diff --git a/tests/ukm-with-contract/erc_20_token.rs b/tests/ulm-with-contract/erc_20_token.rs similarity index 95% rename from tests/ukm-with-contract/erc_20_token.rs rename to tests/ulm-with-contract/erc_20_token.rs index f88b02a..6709262 100644 --- a/tests/ukm-with-contract/erc_20_token.rs +++ b/tests/ulm-with-contract/erc_20_token.rs @@ -11,7 +11,7 @@ #![no_std] #[allow(unused_imports)] -use ukm::*; +use ulm::*; /* ---------------------------------------------------------------------------- @@ -20,15 +20,15 @@ TODOs: - Reuse the implementation of ManagedBuffer for strings, and the annotations for the contract trait identification, as well as views, storage mappers, update, and inits; - - Support some sort of struct for implementing MessageResult within the UKM module. + - Support some sort of struct for implementing MessageResult within the ULM module. We also have to figure out the contents of MessageResult. Observations: - - ManagedAddress was replaced by an integer to fit the behaviors of UKM; + - ManagedAddress was replaced by an integer to fit the behaviors of ULM; ---------------------------------------------------------------------------- */ -#[ukm::contract] +#[ulm::contract] pub trait Erc20Token { // #[view(totalSupply)] #[storage_mapper("total_supply")] @@ -61,7 +61,7 @@ pub trait Erc20Token { fn init(&self, /*name: &ManagedBuffer, symbol: &ManagedBuffer, */init_supply: u256) { // self.s_name().set_if_empty(name); // self.s_symbol().set_if_empty(symbol); - self._mint(::ukm::Caller(), init_supply); + self._mint(::ulm::Caller(), init_supply); } #[upgrade] @@ -94,7 +94,7 @@ pub trait Erc20Token { #[endpoint(transfer)] fn transfer(&self, to: u160, value: u256) -> bool { - let owner = ::ukm::Caller(); + let owner = ::ulm::Caller(); self._transfer(&owner, to, &value); true } @@ -106,14 +106,14 @@ pub trait Erc20Token { #[endpoint(approve)] fn approve(&self, spender: u160, value: u256) -> bool { - let owner = ::ukm::Caller(); + let owner = ::ulm::Caller(); self._approve(&owner, spender, value, true); true } #[endpoint(transferFrom)] fn transfer_from(&self, from: u160, to: u160, value: u256) -> bool { - let spender = ::ukm::Caller(); + let spender = ::ulm::Caller(); self._spend_allowance(from, &spender, value); self._transfer(from, to, value); true diff --git a/tests/ukm-with-contract/events.1.run b/tests/ulm-with-contract/events.1.run similarity index 100% rename from tests/ukm-with-contract/events.1.run rename to tests/ulm-with-contract/events.1.run diff --git a/tests/ukm-with-contract/events.rs b/tests/ulm-with-contract/events.rs similarity index 90% rename from tests/ukm-with-contract/events.rs rename to tests/ulm-with-contract/events.rs index 44d2b7a..7507111 100644 --- a/tests/ukm-with-contract/events.rs +++ b/tests/ulm-with-contract/events.rs @@ -1,9 +1,9 @@ #![no_std] #[allow(unused_imports)] -use ukm::*; +use ulm::*; -#[ukm::contract] +#[ulm::contract] pub trait Events { #[event("MyEvent")] fn my_event(&self, #[indexed] from: u64, value: u64); diff --git a/tests/ukm-with-contract/require.false.run b/tests/ulm-with-contract/require.false.run similarity index 100% rename from tests/ukm-with-contract/require.false.run rename to tests/ulm-with-contract/require.false.run diff --git a/tests/ukm-with-contract/require.rs b/tests/ulm-with-contract/require.rs similarity index 89% rename from tests/ukm-with-contract/require.rs rename to tests/ulm-with-contract/require.rs index ea172f0..dd01faf 100644 --- a/tests/ukm-with-contract/require.rs +++ b/tests/ulm-with-contract/require.rs @@ -1,9 +1,9 @@ #![no_std] #[allow(unused_imports)] -use ukm::*; +use ulm::*; -#[ukm::contract] +#[ulm::contract] pub trait Endpoints { #[init] fn init(&self) {} diff --git a/tests/ukm-with-contract/require.true.run b/tests/ulm-with-contract/require.true.run similarity index 100% rename from tests/ukm-with-contract/require.true.run rename to tests/ulm-with-contract/require.true.run diff --git a/tests/ukm-with-contract/storage.key.run b/tests/ulm-with-contract/storage.key.run similarity index 84% rename from tests/ukm-with-contract/storage.key.run rename to tests/ulm-with-contract/storage.key.run index 8d54dcf..8bf4ff2 100644 --- a/tests/ukm-with-contract/storage.key.run +++ b/tests/ulm-with-contract/storage.key.run @@ -1,5 +1,5 @@ -mock SetAccountStorageHook ( 8738216329482039167 , 123 ) ukmNoResult(); -mock GetAccountStorageHook ( 8738216329482039167 ) ukmIntResult(123, u64); +mock SetAccountStorageHook ( 8738216329482039167 , 123 ) ulmNoResult(); +mock GetAccountStorageHook ( 8738216329482039167 ) ulmIntResult(123, u64); push "setMyDataKey"; hold_string_from_test_stack; diff --git a/tests/ukm-with-contract/storage.rs b/tests/ulm-with-contract/storage.rs similarity index 96% rename from tests/ukm-with-contract/storage.rs rename to tests/ulm-with-contract/storage.rs index 6667714..ed877ed 100644 --- a/tests/ukm-with-contract/storage.rs +++ b/tests/ulm-with-contract/storage.rs @@ -1,9 +1,9 @@ #![no_std] #[allow(unused_imports)] -use ukm::*; +use ulm::*; -#[ukm::contract] +#[ulm::contract] pub trait Storage { #[storage_mapper("myData")] fn my_data(&self) -> ::single_value_mapper::SingleValueMapper; diff --git a/tests/ukm-with-contract/storage.simple.run b/tests/ulm-with-contract/storage.simple.run similarity index 81% rename from tests/ukm-with-contract/storage.simple.run rename to tests/ulm-with-contract/storage.simple.run index 2b2b4ba..0dedb8d 100644 --- a/tests/ukm-with-contract/storage.simple.run +++ b/tests/ulm-with-contract/storage.simple.run @@ -1,5 +1,5 @@ -mock SetAccountStorageHook ( 1809217465971809 , 123 ) ukmNoResult(); -mock GetAccountStorageHook ( 1809217465971809 ) ukmIntResult(123, u64); +mock SetAccountStorageHook ( 1809217465971809 , 123 ) ulmNoResult(); +mock GetAccountStorageHook ( 1809217465971809 ) ulmIntResult(123, u64); push "setMyData"; hold_string_from_test_stack; diff --git a/ukm-semantics/main/common-tools.md b/ukm-semantics/main/common-tools.md deleted file mode 100644 index 35cf524..0000000 --- a/ukm-semantics/main/common-tools.md +++ /dev/null @@ -1,13 +0,0 @@ -```k - -module UKM-COMMON-TOOLS-SYNTAX - syntax Identifier ::= "dispatcherMethodIdentifier" [function, total] -endmodule - -module UKM-COMMON-TOOLS - imports private UKM-COMMON-TOOLS-SYNTAX - - rule dispatcherMethodIdentifier => #token("ukm#dispatch#method", "Identifier") -endmodule - -``` \ No newline at end of file diff --git a/ukm-semantics/main/configuration.md b/ukm-semantics/main/configuration.md deleted file mode 100644 index a065f34..0000000 --- a/ukm-semantics/main/configuration.md +++ /dev/null @@ -1,16 +0,0 @@ -```k - -requires "hooks/bytes.md" -requires "hooks/state.md" - -module UKM-CONFIGURATION - imports UKM-HOOKS-BYTES-CONFIGURATION - imports UKM-HOOKS-STATE-CONFIGURATION - configuration - - - - -endmodule - -``` \ No newline at end of file diff --git a/ukm-semantics/main/decoding/impl.md b/ukm-semantics/main/decoding/impl.md deleted file mode 100644 index 631bbe6..0000000 --- a/ukm-semantics/main/decoding/impl.md +++ /dev/null @@ -1,16 +0,0 @@ -```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/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md deleted file mode 100644 index 35843be..0000000 --- a/ukm-semantics/main/decoding/syntax.md +++ /dev/null @@ -1,10 +0,0 @@ -```k - -module UKM-DECODING-SYNTAX - imports BYTES-SYNTAX - - syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes) - -endmodule - -``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding/impl.md b/ukm-semantics/main/encoding/impl.md deleted file mode 100644 index d0f10b0..0000000 --- a/ukm-semantics/main/encoding/impl.md +++ /dev/null @@ -1,22 +0,0 @@ -```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/execution.md b/ukm-semantics/main/execution.md deleted file mode 100644 index eb608d0..0000000 --- a/ukm-semantics/main/execution.md +++ /dev/null @@ -1,20 +0,0 @@ -```k - -requires "common-tools.md" -requires "execution/casts.md" -requires "execution/dispatch.md" -requires "execution/storage.md" -requires "execution/syntax.md" -requires "hooks.md" -requires "representation.md" - -module UKM-EXECUTION - imports private UKM-COMMON-TOOLS - imports private UKM-EXECUTION-CASTS - imports private UKM-EXECUTION-DISPATCH - imports private UKM-EXECUTION-STORAGE - imports private UKM-HOOKS - imports private UKM-REPRESENTATION -endmodule - -``` diff --git a/ukm-semantics/main/execution/casts.md b/ukm-semantics/main/execution/casts.md deleted file mode 100644 index e4ac3d0..0000000 --- a/ukm-semantics/main/execution/casts.md +++ /dev/null @@ -1,16 +0,0 @@ -```k - -module UKM-EXECUTION-CASTS - imports private RUST-REPRESENTATION - imports private RUST-VALUE-SYNTAX - imports private UKM-REPRESENTATION - - syntax Expression ::= ukmCastResult(ValueOrError) - - rule ukmCast(ptrValue(_, V), ptrValue(_, rustType(T))) => ukmCastResult(implicitCast(V, T)) - rule ukmCastResult(V:Value) => ptrValue(null, V) - - -endmodule - -``` diff --git a/ukm-semantics/main/hooks.md b/ukm-semantics/main/hooks.md deleted file mode 100644 index 1e930b3..0000000 --- a/ukm-semantics/main/hooks.md +++ /dev/null @@ -1,16 +0,0 @@ -```k - -requires "hooks/bytes.md" -requires "hooks/helpers.md" -requires "hooks/state.md" -requires "hooks/ukm.md" -requires "ulm.k" - -module UKM-HOOKS - imports private UKM-HOOKS-BYTES - imports private UKM-HOOKS-HELPERS - imports private UKM-HOOKS-STATE - imports private UKM-HOOKS-UKM -endmodule - -``` diff --git a/ukm-semantics/main/hooks/state.md b/ukm-semantics/main/hooks/state.md deleted file mode 100644 index ef50a11..0000000 --- a/ukm-semantics/main/hooks/state.md +++ /dev/null @@ -1,74 +0,0 @@ -```k - -module UKM-HOOKS-STATE-CONFIGURATION - imports BYTES-SYNTAX - imports INT-SYNTAX - - configuration - - 0 - b"" - 0 - -endmodule - -module UKM-HOOKS-STATE - imports private COMMON-K-CELL - imports private RUST-REPRESENTATION - imports private RUST-SHARED-SYNTAX - imports private UKM-HOOKS-STATE-CONFIGURATION - imports private UKM-REPRESENTATION - - syntax UKMInstruction ::= ukmSetStatus(Expression) [strict(1)] - | ukmSetGasLeft(Expression) [strict(1)] - | ukmSetOutput(Expression) [strict(1)] - | ukmSetOutput(UkmExpression) [strict(1)] - - syntax Identifier ::= "state_hooks" [token] - | "setStatus" [token] - | "setGasLeft" [token] - | "setOutput" [token] - - rule normalizedFunctionCall - ( :: state_hooks :: setStatus :: .PathExprSegments - , StatusId:Ptr , .PtrList - ) - => ukmSetStatus(StatusId) - - rule normalizedFunctionCall - ( :: state_hooks :: setGasLeft :: .PathExprSegments - , GasId:Ptr , .PtrList - ) - => ukmSetGasLeft(GasId) - - rule normalizedFunctionCall - ( :: state_hooks :: setOutput :: .PathExprSegments - , OutputId:Ptr , .PtrList - ) - => ukmSetOutput(OutputId) - - rule - - ukmSetStatus(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList)) - ... - - _ => MInt2Unsigned(Value) - - rule - - ukmSetGasLeft(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList)) - ... - - _ => MInt2Unsigned(Value) - - rule ukmSetOutput(ptrValue(_, u64(BytesId))) => ukmSetOutput(ukmBytesId(BytesId)) - rule - - ukmSetOutput(ukmBytesValue(Value:Bytes)) => ptrValue(null, tuple(.ValueList)) - ... - - _ => Value - -endmodule - -``` diff --git a/ukm-semantics/main/preprocessed-configuration.md b/ukm-semantics/main/preprocessed-configuration.md deleted file mode 100644 index a9e2d93..0000000 --- a/ukm-semantics/main/preprocessed-configuration.md +++ /dev/null @@ -1,16 +0,0 @@ -```k - -requires "preprocessing/configuration.md" - -module UKM-FULL-PREPROCESSED-CONFIGURATION - imports RUST-PREPROCESSING-CONFIGURATION - imports UKM-PREPROCESSING-CONFIGURATION - - configuration - - - - -endmodule - -``` diff --git a/ukm-semantics/main/preprocessing.md b/ukm-semantics/main/preprocessing.md deleted file mode 100644 index ce5ee3c..0000000 --- a/ukm-semantics/main/preprocessing.md +++ /dev/null @@ -1,23 +0,0 @@ -```k - -requires "preprocessing/crates.md" -requires "preprocessing/endpoints.md" -requires "preprocessing/events.md" -requires "preprocessing/methods.md" -requires "preprocessing/storage.md" -requires "preprocessing/syntax.md" -requires "preprocessing/traits.md" -requires "common-tools.md" -requires "representation.md" - -module UKM-PREPROCESSING - imports private UKM-COMMON-TOOLS - imports private UKM-PREPROCESSING-CRATES - imports private UKM-PREPROCESSING-ENDPOINTS - imports private UKM-PREPROCESSING-EVENTS - imports private UKM-PREPROCESSING-METHODS - imports private UKM-PREPROCESSING-STORAGE - imports private UKM-PREPROCESSING-TRAITS -endmodule - -``` diff --git a/ukm-semantics/main/preprocessing/configuration.md b/ukm-semantics/main/preprocessing/configuration.md deleted file mode 100644 index 9302083..0000000 --- a/ukm-semantics/main/preprocessing/configuration.md +++ /dev/null @@ -1,21 +0,0 @@ -```k - -module UKM-PREPROCESSING-CONFIGURATION - imports RUST-SHARED-SYNTAX - - configuration - - - (#token("not#initialized", "Identifier"):Identifier):TypePath - - -endmodule - -module UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION - configuration - - .Map - -endmodule - -``` diff --git a/ukm-semantics/main/preprocessing/crates.md b/ukm-semantics/main/preprocessing/crates.md deleted file mode 100644 index 1f8e44d..0000000 --- a/ukm-semantics/main/preprocessing/crates.md +++ /dev/null @@ -1,14 +0,0 @@ -```k - -module UKM-PREPROCESSING-CRATES - imports private COMMON-K-CELL - imports private RUST-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-SYNTAX - imports private UKM-PREPROCESSING-SYNTAX-PRIVATE - - rule - ukmPreprocessCrates => ukmPreprocessTraits(Traits) ... - Traits:List -endmodule - -``` diff --git a/ukm-semantics/main/representation.md b/ukm-semantics/main/representation.md deleted file mode 100644 index 412bdaf..0000000 --- a/ukm-semantics/main/representation.md +++ /dev/null @@ -1,25 +0,0 @@ -```k - -module UKM-REPRESENTATION - imports BYTES-SYNTAX - imports INT-SYNTAX - imports MINT - imports RUST-VALUE-SYNTAX - - syntax UkmValue ::= ukmBytesValue(Bytes) - | ukmIntValue(Int) - syntax UkmExpression ::= ukmBytesId(MInt{64}) - | ukmInt(MInt{64}) - | UkmValue - syntax KResult ::= UkmValue - - syntax Expression ::= ukmCast(Expression, Expression) [seqstrict] - syntax Expression ::= ukmBytesNew(Bytes) - - syntax Value ::= rustType(Type) - - syntax BytesOrError ::= Bytes | SemanticsError - -endmodule - -``` diff --git a/ukm-semantics/test/configuration.md b/ukm-semantics/test/configuration.md deleted file mode 100644 index 30632b6..0000000 --- a/ukm-semantics/test/configuration.md +++ /dev/null @@ -1,8 +0,0 @@ -```k - -module UKM-TEST-CONFIGURATION - configuration - .K -endmodule - -``` diff --git a/ulm-semantics/main/common-tools.md b/ulm-semantics/main/common-tools.md new file mode 100644 index 0000000..56189bf --- /dev/null +++ b/ulm-semantics/main/common-tools.md @@ -0,0 +1,13 @@ +```k + +module ULM-COMMON-TOOLS-SYNTAX + syntax Identifier ::= "dispatcherMethodIdentifier" [function, total] +endmodule + +module ULM-COMMON-TOOLS + imports private ULM-COMMON-TOOLS-SYNTAX + + rule dispatcherMethodIdentifier => #token("ulm#dispatch#method", "Identifier") +endmodule + +``` \ No newline at end of file diff --git a/ulm-semantics/main/configuration.md b/ulm-semantics/main/configuration.md new file mode 100644 index 0000000..b457738 --- /dev/null +++ b/ulm-semantics/main/configuration.md @@ -0,0 +1,16 @@ +```k + +requires "hooks/bytes.md" +requires "hooks/state.md" + +module ULM-CONFIGURATION + imports ULM-SEMANTICS-HOOKS-BYTES-CONFIGURATION + imports ULM-SEMANTICS-HOOKS-STATE-CONFIGURATION + configuration + + + + +endmodule + +``` \ No newline at end of file diff --git a/ukm-semantics/main/decoding.md b/ulm-semantics/main/decoding.md similarity index 57% rename from ukm-semantics/main/decoding.md rename to ulm-semantics/main/decoding.md index 8d41757..f8fc130 100644 --- a/ukm-semantics/main/decoding.md +++ b/ulm-semantics/main/decoding.md @@ -3,8 +3,8 @@ requires "decoding/impl.md" requires "decoding/syntax.md" -module UKM-DECODING - imports private UKM-DECODING-IMPL +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 new file mode 100644 index 0000000..149c980 --- /dev/null +++ b/ulm-semantics/main/decoding/impl.md @@ -0,0 +1,16 @@ +```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 new file mode 100644 index 0000000..44717c4 --- /dev/null +++ b/ulm-semantics/main/decoding/syntax.md @@ -0,0 +1,10 @@ +```k + +module ULM-DECODING-SYNTAX + imports BYTES-SYNTAX + + syntax ULMInstruction ::= ulmDecodePreprocessedCell(Bytes) + +endmodule + +``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding.md b/ulm-semantics/main/encoding.md similarity index 58% rename from ukm-semantics/main/encoding.md rename to ulm-semantics/main/encoding.md index 98e10fd..6bd33ac 100644 --- a/ukm-semantics/main/encoding.md +++ b/ulm-semantics/main/encoding.md @@ -5,9 +5,9 @@ requires "encoding/impl.md" requires "encoding/syntax.md" requires "encoding/encoder.md" -module UKM-ENCODING - imports private UKM-CALLDATA-ENCODER - imports private UKM-ENCODING-IMPL +module ULM-ENCODING + imports private ULM-CALLDATA-ENCODER + imports private ULM-ENCODING-IMPL endmodule ``` diff --git a/ukm-semantics/main/encoding/encoder.md b/ulm-semantics/main/encoding/encoder.md similarity index 94% rename from ukm-semantics/main/encoding/encoder.md rename to ulm-semantics/main/encoding/encoder.md index 432662a..e889c66 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ulm-semantics/main/encoding/encoder.md @@ -1,12 +1,12 @@ ```k requires "plugin/krypto.md" -module UKM-ENCODING-HELPER +module ULM-ENCODING-HELPER imports private BYTES imports private INT-SYNTAX imports private KRYPTO imports private STRING - imports private UKM-ENCODING-HELPER-SYNTAX + imports private ULM-ENCODING-HELPER-SYNTAX // TODO: Error for argument of length 1 or string not hex rule encodeHexBytes(_:String) => .Bytes @@ -48,14 +48,14 @@ module UKM-ENCODING-HELPER endmodule -module UKM-CALLDATA-ENCODER +module ULM-CALLDATA-ENCODER imports private BYTES imports private INT-SYNTAX imports private KRYPTO imports private STRING - imports private UKM-ENCODING-SYNTAX - imports private UKM-ENCODING-HELPER-SYNTAX - imports private UKM-ENCODING-HELPER + imports private ULM-ENCODING-SYNTAX + imports private ULM-ENCODING-HELPER-SYNTAX + imports private ULM-ENCODING-HELPER rule encodeFunctionSignatureAsBytes(FS) => encodeHexBytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) diff --git a/ulm-semantics/main/encoding/impl.md b/ulm-semantics/main/encoding/impl.md new file mode 100644 index 0000000..5e10d96 --- /dev/null +++ b/ulm-semantics/main/encoding/impl.md @@ -0,0 +1,22 @@ +```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/ukm-semantics/main/encoding/syntax.md b/ulm-semantics/main/encoding/syntax.md similarity index 81% rename from ukm-semantics/main/encoding/syntax.md rename to ulm-semantics/main/encoding/syntax.md index 469e1eb..8f89ca4 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ulm-semantics/main/encoding/syntax.md @@ -1,12 +1,12 @@ ```k -module UKM-ENCODING-SYNTAX +module ULM-ENCODING-SYNTAX imports BYTES-SYNTAX imports LIST imports RUST-REPRESENTATION - syntax UKMInstruction ::= "ukmEncodePreprocessedCell" - | ukmEncodedPreprocessedCell(Bytes) + 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 @@ -19,11 +19,11 @@ module UKM-ENCODING-SYNTAX endmodule -module UKM-ENCODING-HELPER-SYNTAX +module ULM-ENCODING-HELPER-SYNTAX imports BYTES-SYNTAX imports LIST imports RUST-REPRESENTATION - imports UKM-REPRESENTATION + imports ULM-REPRESENTATION // TODO: Make convertToKBytes total syntax Bytes ::= encodeHexBytes(String) [function, total] diff --git a/ulm-semantics/main/execution.md b/ulm-semantics/main/execution.md new file mode 100644 index 0000000..e4b5952 --- /dev/null +++ b/ulm-semantics/main/execution.md @@ -0,0 +1,20 @@ +```k + +requires "common-tools.md" +requires "execution/casts.md" +requires "execution/dispatch.md" +requires "execution/storage.md" +requires "execution/syntax.md" +requires "hooks.md" +requires "representation.md" + +module ULM-EXECUTION + imports private ULM-COMMON-TOOLS + imports private ULM-EXECUTION-CASTS + imports private ULM-EXECUTION-DISPATCH + imports private ULM-EXECUTION-STORAGE + imports private ULM-SEMANTICS-HOOKS + imports private ULM-REPRESENTATION +endmodule + +``` diff --git a/ulm-semantics/main/execution/casts.md b/ulm-semantics/main/execution/casts.md new file mode 100644 index 0000000..8c1ddf0 --- /dev/null +++ b/ulm-semantics/main/execution/casts.md @@ -0,0 +1,16 @@ +```k + +module ULM-EXECUTION-CASTS + imports private RUST-REPRESENTATION + imports private RUST-VALUE-SYNTAX + imports private ULM-REPRESENTATION + + syntax Expression ::= ulmCastResult(ValueOrError) + + rule ulmCast(ptrValue(_, V), ptrValue(_, rustType(T))) => ulmCastResult(implicitCast(V, T)) + rule ulmCastResult(V:Value) => ptrValue(null, V) + + +endmodule + +``` diff --git a/ukm-semantics/main/execution/dispatch.md b/ulm-semantics/main/execution/dispatch.md similarity index 67% rename from ukm-semantics/main/execution/dispatch.md rename to ulm-semantics/main/execution/dispatch.md index 16dacd9..ad34c88 100644 --- a/ukm-semantics/main/execution/dispatch.md +++ b/ulm-semantics/main/execution/dispatch.md @@ -1,33 +1,33 @@ ```k -module UKM-EXECUTION-DISPATCH +module ULM-EXECUTION-DISPATCH imports private BYTES-SYNTAX imports private COMMON-K-CELL imports private K-EQUAL-SYNTAX imports private RUST-REPRESENTATION imports private RUST-VALUE-SYNTAX imports private RUST-EXECUTION-CONFIGURATION - imports private UKM-COMMON-TOOLS-SYNTAX - imports private UKM-EXECUTION-SYNTAX - imports private UKM-PREPROCESSING-CONFIGURATION + imports private ULM-COMMON-TOOLS-SYNTAX + imports private ULM-EXECUTION-SYNTAX + imports private ULM-PREPROCESSING-CONFIGURATION - syntax UkmInstruction ::= ukmExecute(create: Bool, contract:Value, gas: ValueOrError) + syntax UlmInstruction ::= ulmExecute(create: Bool, contract:Value, gas: ValueOrError) rule // TODO: For some reason, kompile rejects 'Create' as a variabler name below. // Figure out why. - ukmExecute(Createy:Bool, Pgm:Bytes, _AccountId:Int, Gas:Int) - => ukmExecute(Createy, struct(ContractTrait, .Map), integerToValue(Gas, u64)) + ulmExecute(Createy:Bool, Pgm:Bytes, _AccountId:Int, Gas:Int) + => ulmExecute(Createy, struct(ContractTrait, .Map), integerToValue(Gas, u64)) ~> #if Createy #then Pgm #else .K #fi ... - + ContractTrait:TypePath - + rule - ukmExecute(... create: Createy:Bool, contract: Contract:Value, gas: Gas:Value) + ulmExecute(... create: Createy:Bool, contract: Contract:Value, gas: Gas:Value) => ptr(NVI) . dispatcherMethodIdentifier ( ptrValue(null, Createy) , ptrValue(null, Gas) diff --git a/ukm-semantics/main/execution/storage.md b/ulm-semantics/main/execution/storage.md similarity index 76% rename from ukm-semantics/main/execution/storage.md rename to ulm-semantics/main/execution/storage.md index 94a168f..b26ba9c 100644 --- a/ukm-semantics/main/execution/storage.md +++ b/ulm-semantics/main/execution/storage.md @@ -1,9 +1,9 @@ ```k -module UKM-EXECUTION-STORAGE +module ULM-EXECUTION-STORAGE imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX - imports private UKM-REPRESENTATION + imports private ULM-REPRESENTATION syntax Identifier ::= "get" [token] | "GetAccountStorage" [token] @@ -12,15 +12,15 @@ module UKM-EXECUTION-STORAGE | "SetAccountStorage" [token] | "single_value_mapper" [token] | "SingleValueMapper" [token] - | "ukm" [token] + | "ulm" [token] rule normalizedFunctionCall ( :: single_value_mapper :: SingleValueMapper :: set :: .PathExprSegments , (SelfPtr:Ptr , ValuePtr:Ptr , .PtrList) ) - => :: ukm :: SetAccountStorage :: .PathExprSegments + => :: ulm :: SetAccountStorage :: .PathExprSegments ( SelfPtr . key - , ukmCast(ValuePtr, ptrValue(null, rustType(u64))) + , ulmCast(ValuePtr, ptrValue(null, rustType(u64))) , .CallParamsList ) @@ -28,7 +28,7 @@ module UKM-EXECUTION-STORAGE ( :: single_value_mapper :: SingleValueMapper :: get :: .PathExprSegments , (SelfPtr:Ptr , .PtrList) ) - => :: ukm :: GetAccountStorage :: .PathExprSegments + => :: ulm :: GetAccountStorage :: .PathExprSegments ( SelfPtr . key , .CallParamsList ) diff --git a/ukm-semantics/main/execution/syntax.md b/ulm-semantics/main/execution/syntax.md similarity index 57% rename from ukm-semantics/main/execution/syntax.md rename to ulm-semantics/main/execution/syntax.md index 2ee0238..4a87c50 100644 --- a/ukm-semantics/main/execution/syntax.md +++ b/ulm-semantics/main/execution/syntax.md @@ -1,11 +1,11 @@ ```k -module UKM-EXECUTION-SYNTAX +module ULM-EXECUTION-SYNTAX imports BOOL-SYNTAX imports BYTES-SYNTAX imports INT-SYNTAX - syntax UKMInstruction ::= ukmExecute(create: Bool, pgm:Bytes, accountId: Int, gas: Int) + syntax ULMInstruction ::= ulmExecute(create: Bool, pgm:Bytes, accountId: Int, gas: Int) endmodule diff --git a/ulm-semantics/main/hooks.md b/ulm-semantics/main/hooks.md new file mode 100644 index 0000000..ad7f659 --- /dev/null +++ b/ulm-semantics/main/hooks.md @@ -0,0 +1,16 @@ +```k + +requires "hooks/bytes.md" +requires "hooks/helpers.md" +requires "hooks/state.md" +requires "hooks/ulm.md" +requires "ulm.k" + +module ULM-SEMANTICS-HOOKS + imports private ULM-SEMANTICS-HOOKS-BYTES + imports private ULM-SEMANTICS-HOOKS-HELPERS + imports private ULM-SEMANTICS-HOOKS-STATE + imports private ULM-SEMANTICS-HOOKS-ULM +endmodule + +``` diff --git a/ukm-semantics/main/hooks/bytes.md b/ulm-semantics/main/hooks/bytes.md similarity index 53% rename from ukm-semantics/main/hooks/bytes.md rename to ulm-semantics/main/hooks/bytes.md index 78ee3c3..7501f3d 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ulm-semantics/main/hooks/bytes.md @@ -1,28 +1,28 @@ ```k -module UKM-HOOKS-BYTES-CONFIGURATION +module ULM-SEMANTICS-HOOKS-BYTES-CONFIGURATION imports INT-SYNTAX imports MAP configuration - - + + .Map // Int to Bytes - - + + 0 - - + + endmodule -module UKM-HOOKS-BYTES +module ULM-SEMANTICS-HOOKS-BYTES imports private BYTES imports private COMMON-K-CELL imports private K-EQUAL-SYNTAX imports private RUST-HELPERS imports private RUST-REPRESENTATION - imports private UKM-HOOKS-BYTES-CONFIGURATION - imports private UKM-REPRESENTATION + imports private ULM-SEMANTICS-HOOKS-BYTES-CONFIGURATION + imports private ULM-REPRESENTATION syntax Identifier ::= "bytes_hooks" [token] @@ -58,12 +58,12 @@ module UKM-HOOKS-BYTES => ptrValue(null, u64(Int2MInt(NextId))) ... - + M => M[NextId <- b""] - - + + NextId:Int => NextId +Int 1 - + requires notBool uoverflowMInt(64, NextId) rule @@ -71,290 +71,290 @@ module UKM-HOOKS-BYTES ( :: bytes_hooks :: length :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesLength(BufferIdId) + => ulmBytesLength(BufferIdId) rule normalizedFunctionCall ( :: bytes_hooks :: equals :: .PathExprSegments , BufferIdId1:Ptr, BufferIdId2:Ptr, .PtrList ) - => ukmBytesEquals(BufferIdId1, BufferIdId2) + => ulmBytesEquals(BufferIdId1, BufferIdId2) rule normalizedFunctionCall ( :: bytes_hooks :: append_u256 :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendInt(BufferIdId, IntId) + => ulmBytesAppendInt(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_u160 :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendInt(BufferIdId, IntId) + => ulmBytesAppendInt(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_u128 :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendInt(BufferIdId, IntId) + => ulmBytesAppendInt(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_u64 :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendInt(BufferIdId, IntId) + => ulmBytesAppendInt(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_u32 :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendInt(BufferIdId, IntId) + => ulmBytesAppendInt(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_u16 :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendInt(BufferIdId, IntId) + => ulmBytesAppendInt(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_u8 :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendInt(BufferIdId, IntId) + => ulmBytesAppendInt(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_bool :: .PathExprSegments , BufferIdId:Ptr, IntId:Ptr, .PtrList ) - => ukmBytesAppendBool(BufferIdId, IntId) + => ulmBytesAppendBool(BufferIdId, IntId) rule normalizedFunctionCall ( :: bytes_hooks :: append_str :: .PathExprSegments , BufferIdId:Ptr, StrId:Ptr, .PtrList ) - => ukmBytesAppendStr(BufferIdId, StrId) + => ulmBytesAppendStr(BufferIdId, StrId) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u256 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u256) + => ulmBytesDecode(BufferIdId, u256) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u160 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u160) + => ulmBytesDecode(BufferIdId, u160) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u128 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u128) + => ulmBytesDecode(BufferIdId, u128) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u64 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u64) + => ulmBytesDecode(BufferIdId, u64) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u32 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u32) + => ulmBytesDecode(BufferIdId, u32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u16 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u16) + => ulmBytesDecode(BufferIdId, u16) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u8 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u8) + => ulmBytesDecode(BufferIdId, u8) rule normalizedFunctionCall ( :: bytes_hooks :: decode_str :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, str) + => ulmBytesDecode(BufferIdId, str) rule normalizedFunctionCall ( :: bytes_hooks :: hash :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesHash(BufferIdId) + => ulmBytesHash(BufferIdId) rule normalizedFunctionCall ( :: bytes_hooks :: decode_signature :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeBytes(BufferIdId, 8) + => ulmBytesDecodeBytes(BufferIdId, 8) // --------------------------------------- rule - ukmBytesId(BytesId) => ukmBytesValue(Value) + ulmBytesId(BytesId) => ulmBytesValue(Value) ... - + MInt2Unsigned(BytesId) |-> Value:Bytes ... - - - syntax UKMInstruction ::= ukmBytesLength(Expression) [strict(1)] - | ukmBytesLength(UkmExpression) [strict(1)] - | ukmBytesEquals(Expression, Expression) [seqstrict] - | ukmBytesEquals(UkmExpression, UkmExpression) [seqstrict] - | ukmBytesAppendInt(Expression, Expression) [seqstrict] - | ukmBytesAppendInt(UkmExpression, Int) [strict(1)] - | ukmBytesAppendBool(Expression, Expression) [seqstrict] - | ukmBytesAppendStr(Expression, Expression) [seqstrict] - | ukmBytesAppendBytes(UkmExpression, Bytes) [strict(1)] - | ukmBytesAppendLenAndBytes(UkmExpression, Bytes) [strict(1)] - | ukmBytesDecode(Expression, Type) [strict(1)] - | ukmBytesDecode(UkmExpression, Type) [strict(1)] - | ukmBytesDecodeBytes(Expression, Int) [strict(1)] - | ukmBytesDecodeBytes(UkmExpression, Int) [strict(1)] - | ukmBytesDecode(Int, Bytes, Type) - | ukmBytesDecodeInt(Int, Bytes, Type) - | ukmBytesDecodeStr(Int, Bytes) - | ukmBytesDecode(ValueOrError, Bytes) - | ukmBytesHash(Expression) [strict(1)] - | ukmBytesHash(UkmExpression) [strict(1)] + + + syntax ULMInstruction ::= ulmBytesLength(Expression) [strict(1)] + | ulmBytesLength(UlmExpression) [strict(1)] + | ulmBytesEquals(Expression, Expression) [seqstrict] + | ulmBytesEquals(UlmExpression, UlmExpression) [seqstrict] + | ulmBytesAppendInt(Expression, Expression) [seqstrict] + | ulmBytesAppendInt(UlmExpression, Int) [strict(1)] + | ulmBytesAppendBool(Expression, Expression) [seqstrict] + | ulmBytesAppendStr(Expression, Expression) [seqstrict] + | ulmBytesAppendBytes(UlmExpression, Bytes) [strict(1)] + | ulmBytesAppendLenAndBytes(UlmExpression, Bytes) [strict(1)] + | ulmBytesDecode(Expression, Type) [strict(1)] + | ulmBytesDecode(UlmExpression, Type) [strict(1)] + | ulmBytesDecodeBytes(Expression, Int) [strict(1)] + | ulmBytesDecodeBytes(UlmExpression, Int) [strict(1)] + | ulmBytesDecode(Int, Bytes, Type) + | ulmBytesDecodeInt(Int, Bytes, Type) + | ulmBytesDecodeStr(Int, Bytes) + | ulmBytesDecode(ValueOrError, Bytes) + | ulmBytesHash(Expression) [strict(1)] + | ulmBytesHash(UlmExpression) [strict(1)] rule - ukmBytesNew(B:Bytes) + ulmBytesNew(B:Bytes) => ptrValue(null, u64(Int2MInt(NextId))) ... - + M => M[NextId <- B] - - + + NextId:Int => NextId +Int 1 - + requires notBool uoverflowMInt(64, NextId) - rule ukmBytesLength(ptrValue(_, u64(BytesId))) => ukmBytesLength(ukmBytesId(BytesId)) - rule ukmBytesLength(ukmBytesValue(Value:Bytes)) + rule ulmBytesLength(ptrValue(_, u64(BytesId))) => ulmBytesLength(ulmBytesId(BytesId)) + rule ulmBytesLength(ulmBytesValue(Value:Bytes)) => ptrValue(null, u32(Int2MInt(lengthBytes(Value)))) requires notBool uoverflowMInt(32, lengthBytes(Value)) - rule ukmBytesEquals(ptrValue(_, u64(BytesId1)), ptrValue(_, u64(BytesId2))) - => ukmBytesEquals(ukmBytesId(BytesId1), ukmBytesId(BytesId2)) - rule ukmBytesEquals(ukmBytesValue(Value1:Bytes), ukmBytesValue(Value2:Bytes)) + rule ulmBytesEquals(ptrValue(_, u64(BytesId1)), ptrValue(_, u64(BytesId2))) + => ulmBytesEquals(ulmBytesId(BytesId1), ulmBytesId(BytesId2)) + rule ulmBytesEquals(ulmBytesValue(Value1:Bytes), ulmBytesValue(Value2:Bytes)) => ptrValue(null, Value1 ==K Value2) - rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u256(Value))) - => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) - rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u160(Value))) - => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) - rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u128(Value))) - => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) - rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u64(Value))) - => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) - rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u32(Value))) - => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) - rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u16(Value))) - => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) - rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u8(Value))) - => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) - - rule ukmBytesAppendInt(ukmBytesValue(B:Bytes), Value:Int) - => ukmBytesNew(B +Bytes Int2Bytes(32, Value, BE)) - - rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, false)) - => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(0p8))) - rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true)) - => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8))) + rule ulmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u256(Value))) + => ulmBytesAppendInt(ulmBytesId(BytesId), MInt2Unsigned(Value)) + rule ulmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u160(Value))) + => ulmBytesAppendInt(ulmBytesId(BytesId), MInt2Unsigned(Value)) + rule ulmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u128(Value))) + => ulmBytesAppendInt(ulmBytesId(BytesId), MInt2Unsigned(Value)) + rule ulmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u64(Value))) + => ulmBytesAppendInt(ulmBytesId(BytesId), MInt2Unsigned(Value)) + rule ulmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u32(Value))) + => ulmBytesAppendInt(ulmBytesId(BytesId), MInt2Unsigned(Value)) + rule ulmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u16(Value))) + => ulmBytesAppendInt(ulmBytesId(BytesId), MInt2Unsigned(Value)) + rule ulmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u8(Value))) + => ulmBytesAppendInt(ulmBytesId(BytesId), MInt2Unsigned(Value)) + + rule ulmBytesAppendInt(ulmBytesValue(B:Bytes), Value:Int) + => ulmBytesNew(B +Bytes Int2Bytes(32, Value, BE)) + + rule ulmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, false)) + => ulmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(0p8))) + rule ulmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true)) + => ulmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8))) // TODO: This can create key ambiguity for storage - rule ukmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String)) - => ukmBytesAppendLenAndBytes(ukmBytesId(BytesId), String2Bytes(Value)) + rule ulmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String)) + => ulmBytesAppendLenAndBytes(ulmBytesId(BytesId), String2Bytes(Value)) - rule ukmBytesAppendBytes(ukmBytesValue(B:Bytes), Value:Bytes) - => ukmBytesNew(B +Bytes Value) + rule ulmBytesAppendBytes(ulmBytesValue(B:Bytes), Value:Bytes) + => ulmBytesNew(B +Bytes Value) - rule ukmBytesAppendLenAndBytes(ukmBytesValue(First:Bytes), Second:Bytes) - => ukmBytesNew(First +Bytes Int2Bytes(2, lengthBytes(Second), BE) +Bytes Second) + rule ulmBytesAppendLenAndBytes(ulmBytesValue(First:Bytes), Second:Bytes) + => ulmBytesNew(First +Bytes Int2Bytes(2, lengthBytes(Second), BE) +Bytes Second) requires lengthBytes(Second) ukmBytesDecodeBytes(ukmBytesId(BytesId), L:Int) - rule ukmBytesDecodeBytes(ukmBytesValue(B:Bytes), L:Int) + rule ulmBytesDecodeBytes(ptrValue(_, u64(BytesId)), L:Int) + => ulmBytesDecodeBytes(ulmBytesId(BytesId), L:Int) + rule ulmBytesDecodeBytes(ulmBytesValue(B:Bytes), L:Int) => tupleExpression - ( ukmBytesNew(substrBytes(B, L, lengthBytes(B))) - , ukmBytesNew(substrBytes(B, 0, L)) + ( ulmBytesNew(substrBytes(B, L, lengthBytes(B))) + , ulmBytesNew(substrBytes(B, 0, L)) , .TupleElementsNoEndComma ) requires L <=Int lengthBytes(B) - rule ukmBytesDecode(ptrValue(_, u64(BytesId)), T:Type) - => ukmBytesDecode(ukmBytesId(BytesId), T:Type) - rule ukmBytesDecode(ukmBytesValue(B:Bytes), T:Type) - => ukmBytesDecode + rule ulmBytesDecode(ptrValue(_, u64(BytesId)), T:Type) + => ulmBytesDecode(ulmBytesId(BytesId), T:Type) + rule ulmBytesDecode(ulmBytesValue(B:Bytes), T:Type) + => ulmBytesDecode ( integerToValue(Bytes2Int(substrBytes(B, 0, 32), BE, Unsigned), T) , substrBytes(B, 32, lengthBytes(B)) ) requires isUnsignedInt(T) andBool 32 <=Int lengthBytes(B) - rule ukmBytesDecode(ukmBytesValue(B:Bytes), T:Type) - => ukmBytesDecode + rule ulmBytesDecode(ulmBytesValue(B:Bytes), T:Type) + => ulmBytesDecode ( integerToValue(Bytes2Int(substrBytes(B, 0, 32), BE, Signed), T) , substrBytes(B, 32, lengthBytes(B)) ) requires isSignedInt(T) andBool 32 <=Int lengthBytes(B) - rule ukmBytesDecode(ukmBytesValue(B:Bytes), str) - => ukmBytesDecodeStr + rule ulmBytesDecode(ulmBytesValue(B:Bytes), str) + => ulmBytesDecodeStr ( Bytes2Int(substrBytes(B, 0, 2), BE, Signed) , substrBytes(B, 2, lengthBytes(B)) ) requires 2 <=Int lengthBytes(B) - rule ukmBytesDecodeInt(Value:Int, B:Bytes, T:Type) - => ukmBytesDecode(integerToValue(Value, T), B) - rule ukmBytesDecodeStr(Len:Int, B:Bytes) - => ukmBytesDecode(Bytes2String(substrBytes(B, 0, Len)), substrBytes(B, Len, lengthBytes(B))) + rule ulmBytesDecodeInt(Value:Int, B:Bytes, T:Type) + => ulmBytesDecode(integerToValue(Value, T), B) + rule ulmBytesDecodeStr(Len:Int, B:Bytes) + => ulmBytesDecode(Bytes2String(substrBytes(B, 0, Len)), substrBytes(B, Len, lengthBytes(B))) requires 0 <=Int Len andBool Len <=Int lengthBytes(B) - rule ukmBytesDecode(Value:Value, B:Bytes) - => tupleExpression(ukmBytesNew(B) , ptrValue(null, Value) , .TupleElementsNoEndComma) + rule ulmBytesDecode(Value:Value, B:Bytes) + => tupleExpression(ulmBytesNew(B) , ptrValue(null, Value) , .TupleElementsNoEndComma) - rule ukmBytesHash(ptrValue(_, u64(BytesId))) - => ukmBytesHash(ukmBytesId(BytesId)) - rule ukmBytesHash(ukmBytesValue(B:Bytes)) - => ptrValue(null, u64(Int2MInt(#ukmBytesHash(Bytes2Int(B, BE, Unsigned))))) + rule ulmBytesHash(ptrValue(_, u64(BytesId))) + => ulmBytesHash(ulmBytesId(BytesId)) + rule ulmBytesHash(ulmBytesValue(B:Bytes)) + => ptrValue(null, u64(Int2MInt(#ulmBytesHash(Bytes2Int(B, BE, Unsigned))))) - syntax Int ::= #ukmBytesHash(Int) [function, total] - rule #ukmBytesHash(I:Int) => #ukmBytesHash(0 -Int I) requires I I requires 0 <=Int I andBool I #ukmBytesHash + syntax Int ::= #ulmBytesHash(Int) [function, total] + rule #ulmBytesHash(I:Int) => #ulmBytesHash(0 -Int I) requires I I requires 0 <=Int I andBool I #ulmBytesHash ( (I &Int ((1 <>Int 64) + |Int #ulmBytesHash(I >>Int 64) ) endmodule diff --git a/ukm-semantics/main/hooks/helpers.md b/ulm-semantics/main/hooks/helpers.md similarity index 60% rename from ukm-semantics/main/hooks/helpers.md rename to ulm-semantics/main/hooks/helpers.md index 0d0cc79..f9f31ac 100644 --- a/ukm-semantics/main/hooks/helpers.md +++ b/ulm-semantics/main/hooks/helpers.md @@ -1,13 +1,13 @@ ```k -module UKM-HOOKS-HELPERS-SYNTAX - syntax UkmInstruction ::= "ukmCancel" +module ULM-SEMANTICS-HOOKS-HELPERS-SYNTAX + syntax UlmInstruction ::= "ulmCancel" endmodule -module UKM-HOOKS-HELPERS +module ULM-SEMANTICS-HOOKS-HELPERS imports private COMMON-K-CELL imports private RUST-REPRESENTATION - imports private UKM-HOOKS-HELPERS-SYNTAX + imports private ULM-SEMANTICS-HOOKS-HELPERS-SYNTAX syntax Identifier ::= "cancel_request" [token] | "helpers" [token] @@ -17,9 +17,9 @@ module UKM-HOOKS-HELPERS ( :: helpers :: cancel_request :: .PathExprSegments , .PtrList ) - => ukmCancel + => ulmCancel - rule (ukmCancel ~> _:KItem) => ukmCancel + rule (ulmCancel ~> _:KItem) => ulmCancel [owise] endmodule diff --git a/ulm-semantics/main/hooks/state.md b/ulm-semantics/main/hooks/state.md new file mode 100644 index 0000000..61e0669 --- /dev/null +++ b/ulm-semantics/main/hooks/state.md @@ -0,0 +1,74 @@ +```k + +module ULM-SEMANTICS-HOOKS-STATE-CONFIGURATION + imports BYTES-SYNTAX + imports INT-SYNTAX + + configuration + + 0 + b"" + 0 + +endmodule + +module ULM-SEMANTICS-HOOKS-STATE + imports private COMMON-K-CELL + imports private RUST-REPRESENTATION + imports private RUST-SHARED-SYNTAX + imports private ULM-SEMANTICS-HOOKS-STATE-CONFIGURATION + imports private ULM-REPRESENTATION + + syntax ULMInstruction ::= ulmSetStatus(Expression) [strict(1)] + | ulmSetGasLeft(Expression) [strict(1)] + | ulmSetOutput(Expression) [strict(1)] + | ulmSetOutput(UlmExpression) [strict(1)] + + syntax Identifier ::= "state_hooks" [token] + | "setStatus" [token] + | "setGasLeft" [token] + | "setOutput" [token] + + rule normalizedFunctionCall + ( :: state_hooks :: setStatus :: .PathExprSegments + , StatusId:Ptr , .PtrList + ) + => ulmSetStatus(StatusId) + + rule normalizedFunctionCall + ( :: state_hooks :: setGasLeft :: .PathExprSegments + , GasId:Ptr , .PtrList + ) + => ulmSetGasLeft(GasId) + + rule normalizedFunctionCall + ( :: state_hooks :: setOutput :: .PathExprSegments + , OutputId:Ptr , .PtrList + ) + => ulmSetOutput(OutputId) + + rule + + ulmSetStatus(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList)) + ... + + _ => MInt2Unsigned(Value) + + rule + + ulmSetGasLeft(ptrValue(_, u64(Value))) => ptrValue(null, tuple(.ValueList)) + ... + + _ => MInt2Unsigned(Value) + + rule ulmSetOutput(ptrValue(_, u64(BytesId))) => ulmSetOutput(ulmBytesId(BytesId)) + rule + + ulmSetOutput(ulmBytesValue(Value:Bytes)) => ptrValue(null, tuple(.ValueList)) + ... + + _ => Value + +endmodule + +``` diff --git a/ukm-semantics/main/hooks/ukm.md b/ulm-semantics/main/hooks/ulm.md similarity index 50% rename from ukm-semantics/main/hooks/ukm.md rename to ulm-semantics/main/hooks/ulm.md index 1129d38..c1d2fcf 100644 --- a/ukm-semantics/main/hooks/ukm.md +++ b/ulm-semantics/main/hooks/ulm.md @@ -1,96 +1,96 @@ ```k -module UKM-HOOKS-UKM-SYNTAX +module ULM-SEMANTICS-HOOKS-ULM-SYNTAX imports INT-SYNTAX - syntax UkmHook ::= CallDataHook() + syntax UlmHook ::= CallDataHook() | CallerHook() | SetAccountStorageHook(Int, Int) | GetAccountStorageHook(Int) syntax K syntax Type - syntax UkmHookResult ::= ukmNoResult() - | ukmIntResult(Int, Type) + syntax UlmHookResult ::= ulmNoResult() + | ulmIntResult(Int, Type) endmodule -module UKM-HOOKS-UKM +module ULM-SEMANTICS-HOOKS-ULM imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX - imports private UKM-HOOKS-SIGNATURE - imports private UKM-HOOKS-UKM-SYNTAX - imports private UKM-REPRESENTATION + imports private ULM-SEMANTICS-HOOKS-SIGNATURE + imports private ULM-SEMANTICS-HOOKS-ULM-SYNTAX + imports private ULM-REPRESENTATION - syntax Identifier ::= "ukm" [token] + syntax Identifier ::= "ulm" [token] | "CallData" [token] | "Caller" [token] | "SetAccountStorage" [token] | "GetAccountStorage" [token] - rule normalizedFunctionCall ( :: ukm :: CallData :: .PathExprSegments , .PtrList ) + rule normalizedFunctionCall ( :: ulm :: CallData :: .PathExprSegments , .PtrList ) => CallDataHook() - rule normalizedFunctionCall ( :: ukm :: Caller :: .PathExprSegments , .PtrList ) + rule normalizedFunctionCall ( :: ulm :: Caller :: .PathExprSegments , .PtrList ) => CallerHook() rule normalizedFunctionCall - ( :: ukm :: SetAccountStorage :: .PathExprSegments + ( :: ulm :: SetAccountStorage :: .PathExprSegments , (KeyPtr:Ptr , ValuePtr:Ptr , .PtrList) ) => #SetAccountStorageHook(KeyPtr, ValuePtr) - syntax UkmHook ::= #SetAccountStorageHook(Expression, Expression) [seqstrict] + syntax UlmHook ::= #SetAccountStorageHook(Expression, Expression) [seqstrict] rule #SetAccountStorageHook(ptrValue(_, u64(Key)), ptrValue(_, u64(Value))) => SetAccountStorageHook(MInt2Unsigned(Key), MInt2Unsigned(Value)) rule normalizedFunctionCall - ( :: ukm :: GetAccountStorage :: .PathExprSegments + ( :: ulm :: GetAccountStorage :: .PathExprSegments , (KeyPtr:Ptr , .PtrList) ) => #GetAccountStorageHook(KeyPtr) - syntax UkmHook ::= #GetAccountStorageHook(Expression) [strict] + syntax UlmHook ::= #GetAccountStorageHook(Expression) [strict] rule #GetAccountStorageHook(ptrValue(_, u64(Key))) => GetAccountStorageHook(MInt2Unsigned(Key)) - rule ukmNoResult() => ptrValue(null, tuple(.ValueList)) - rule ukmIntResult(Value:Int, T:Type) => ukmValueResult(integerToValue(Value, T)) + rule ulmNoResult() => ptrValue(null, tuple(.ValueList)) + rule ulmIntResult(Value:Int, T:Type) => ulmValueResult(integerToValue(Value, T)) - syntax UkmHook ::= ukmValueResult(ValueOrError) - rule ukmValueResult(V:Value) => ptrValue(null, V) + syntax UlmHook ::= ulmValueResult(ValueOrError) + rule ulmValueResult(V:Value) => ptrValue(null, V) endmodule // This module should be used only in kompilation targets which have implementations // for the ULM hooks. -module UKM-HOOKS-TO-ULM-FUNCTIONS +module ULM-SEMANTICS-HOOKS-TO-ULM-FUNCTIONS imports private RUST-REPRESENTATION - imports private UKM-HOOKS-UKM-SYNTAX + imports private ULM-SEMANTICS-HOOKS-ULM-SYNTAX imports private ULM-HOOKS - imports private UKM-REPRESENTATION + imports private ULM-REPRESENTATION - rule CallDataHook() => ukmBytesNew(CallData()) - rule CallerHook() => ukmIntResult(Caller(), u160) - rule SetAccountStorageHook(Key:Int, Value:Int) => SetAccountStorage(Key, Value) ~> ukmNoResult() - rule GetAccountStorageHook(Key:Int) => ukmIntResult(GetAccountStorage(Key), u256) + rule CallDataHook() => ulmBytesNew(CallData()) + rule CallerHook() => ulmIntResult(Caller(), u160) + rule SetAccountStorageHook(Key:Int, Value:Int) => SetAccountStorage(Key, Value) ~> ulmNoResult() + rule GetAccountStorageHook(Key:Int) => ulmIntResult(GetAccountStorage(Key), u256) endmodule -module UKM-HOOKS-SIGNATURE +module ULM-SEMANTICS-HOOKS-SIGNATURE imports private ULM-SIGNATURE - imports private UKM-HOOKS-STATE-CONFIGURATION - imports private UKM-TARGET-CONFIGURATION + imports private ULM-SEMANTICS-HOOKS-STATE-CONFIGURATION + imports private ULM-TARGET-CONFIGURATION rule getOutput ( - - - Value:Bytes + + + Value:Bytes ... - + ... - + ... ) @@ -98,13 +98,13 @@ module UKM-HOOKS-SIGNATURE rule getStatus ( - - - Value:Int + + + Value:Int ... - + ... - + ... ) @@ -112,13 +112,13 @@ module UKM-HOOKS-SIGNATURE rule getGasLeft ( - - - Value:Int + + + Value:Int ... - + ... - + ... ) diff --git a/ulm-semantics/main/preprocessed-configuration.md b/ulm-semantics/main/preprocessed-configuration.md new file mode 100644 index 0000000..3674503 --- /dev/null +++ b/ulm-semantics/main/preprocessed-configuration.md @@ -0,0 +1,16 @@ +```k + +requires "preprocessing/configuration.md" + +module ULM-FULL-PREPROCESSED-CONFIGURATION + imports RUST-PREPROCESSING-CONFIGURATION + imports ULM-PREPROCESSING-CONFIGURATION + + configuration + + + + +endmodule + +``` diff --git a/ulm-semantics/main/preprocessing.md b/ulm-semantics/main/preprocessing.md new file mode 100644 index 0000000..607d4b1 --- /dev/null +++ b/ulm-semantics/main/preprocessing.md @@ -0,0 +1,23 @@ +```k + +requires "preprocessing/crates.md" +requires "preprocessing/endpoints.md" +requires "preprocessing/events.md" +requires "preprocessing/methods.md" +requires "preprocessing/storage.md" +requires "preprocessing/syntax.md" +requires "preprocessing/traits.md" +requires "common-tools.md" +requires "representation.md" + +module ULM-PREPROCESSING + imports private ULM-COMMON-TOOLS + imports private ULM-PREPROCESSING-CRATES + imports private ULM-PREPROCESSING-ENDPOINTS + imports private ULM-PREPROCESSING-EVENTS + imports private ULM-PREPROCESSING-METHODS + imports private ULM-PREPROCESSING-STORAGE + imports private ULM-PREPROCESSING-TRAITS +endmodule + +``` diff --git a/ulm-semantics/main/preprocessing/configuration.md b/ulm-semantics/main/preprocessing/configuration.md new file mode 100644 index 0000000..55a0e34 --- /dev/null +++ b/ulm-semantics/main/preprocessing/configuration.md @@ -0,0 +1,21 @@ +```k + +module ULM-PREPROCESSING-CONFIGURATION + imports RUST-SHARED-SYNTAX + + configuration + + + (#token("not#initialized", "Identifier"):Identifier):TypePath + + +endmodule + +module ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION + configuration + + .Map + +endmodule + +``` diff --git a/ulm-semantics/main/preprocessing/crates.md b/ulm-semantics/main/preprocessing/crates.md new file mode 100644 index 0000000..0fb0045 --- /dev/null +++ b/ulm-semantics/main/preprocessing/crates.md @@ -0,0 +1,14 @@ +```k + +module ULM-PREPROCESSING-CRATES + imports private COMMON-K-CELL + imports private RUST-PREPROCESSING-CONFIGURATION + imports private ULM-PREPROCESSING-SYNTAX + imports private ULM-PREPROCESSING-SYNTAX-PRIVATE + + rule + ulmPreprocessCrates => ulmPreprocessTraits(Traits) ... + Traits:List +endmodule + +``` diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ulm-semantics/main/preprocessing/endpoints.md similarity index 91% rename from ukm-semantics/main/preprocessing/endpoints.md rename to ulm-semantics/main/preprocessing/endpoints.md index 76bd220..23f53b5 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ulm-semantics/main/preprocessing/endpoints.md @@ -1,35 +1,35 @@ ```k -module UKM-PREPROCESSING-ENDPOINTS +module ULM-PREPROCESSING-ENDPOINTS imports private COMMON-K-CELL imports private RUST-CONVERSIONS-SYNTAX imports private RUST-ERROR-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION imports private RUST-SHARED-SYNTAX - imports private UKM-COMMON-TOOLS-SYNTAX - imports private UKM-ENCODING-SYNTAX - imports private UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION - imports private UKM-PREPROCESSING-SYNTAX-PRIVATE - imports private UKM-ENCODING-SYNTAX - imports private UKM-REPRESENTATION + imports private ULM-COMMON-TOOLS-SYNTAX + imports private ULM-ENCODING-SYNTAX + imports private ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION + imports private ULM-PREPROCESSING-SYNTAX-PRIVATE + imports private ULM-ENCODING-SYNTAX + imports private ULM-REPRESENTATION rule - ukmPreprocessEndpoint + ulmPreprocessEndpoint ( Trait:TypePath , Method:Identifier , FullMethodPath:PathInExpression , Name:String ) - => ukmAddEndpointWrapper - ( typePathToPathInExpression(append(Trait, StringToIdentifier("ukmWrap#" +String Name))) + => ulmAddEndpointWrapper + ( typePathToPathInExpression(append(Trait, StringToIdentifier("ulmWrap#" +String Name))) , Params , ReturnType , Method ) - ~> ukmAddEndpointSignature + ~> ulmAddEndpointSignature ( methodSignature(Name, Params) - , StringToIdentifier("ukmWrap#" +String Name) + , StringToIdentifier("ulmWrap#" +String Name) ) ... @@ -38,13 +38,13 @@ module UKM-PREPROCESSING-ENDPOINTS ReturnType:Type - rule ukmAddEndpointWrapper + rule ulmAddEndpointWrapper (... wrapperMethod: WrapperMethod:PathInExpression , params: Params:NormalizedFunctionParameterList , returnType: ReturnType:Type , method: ImplementationMethod:Identifier ) - => #ukmAddEndpointWrapper + => #ulmAddEndpointWrapper (... wrapperMethod: WrapperMethod , params: Params , method: ImplementationMethod @@ -54,7 +54,7 @@ module UKM-PREPROCESSING-ENDPOINTS rule - #ukmAddEndpointWrapper + #ulmAddEndpointWrapper (... wrapperMethod: WrapperMethod:PathInExpression , params: Params:NormalizedFunctionParameterList , method: ImplementationMethod:Identifier @@ -81,7 +81,7 @@ module UKM-PREPROCESSING-ENDPOINTS let buffer_id = :: bytes_hooks :: empty(.CallParamsList); let buffer_id = Append; :: state_hooks :: setOutput(buffer_id , .CallParamsList); - :: state_hooks :: setStatus(:: ukm :: EVMC_SUCCESS , .CallParamsList); + :: state_hooks :: setStatus(:: ulm :: EVMC_SUCCESS , .CallParamsList); ) }) @@ -93,23 +93,23 @@ module UKM-PREPROCESSING-ENDPOINTS rule - ukmAddEndpointSignature(Signature:Bytes, Method:Identifier) => .K + ulmAddEndpointSignature(Signature:Bytes, Method:Identifier) => .K ... - + Signatures:Map => Signatures[Signature <- Method] - + requires notBool (Signature in_keys(Signatures)) rule - ukmAddDispatcher(TypePath) => .K + ulmAddDispatcher(TypePath) => .K ... - + Signatures:Map - + (.Bag => @@ -123,10 +123,10 @@ module UKM-PREPROCESSING-ENDPOINTS block({ .InnerAttributes - let buffer_id = :: ukm :: CallData(); + let buffer_id = :: ulm :: CallData(); if create { .InnerAttributes - self . ukmWrap##init ( buffer_id , gas , .CallParamsList ); + self . ulmWrap##init ( buffer_id , gas , .CallParamsList ); .NonEmptyStatements } else { .InnerAttributes @@ -175,8 +175,8 @@ module UKM-PREPROCESSING-ENDPOINTS | "decode_signature" [token] | "empty" [token] | "equals" [token] - | "ukm" [token] - | "ukmWrap##init" [token] + | "ulm" [token] + | "ulmWrap##init" [token] | "CallData" [token] | "EVMC_BAD_JUMP_DESTINATION" [token] | "EVMC_SUCCESS" [token] @@ -223,7 +223,7 @@ module UKM-PREPROCESSING-ENDPOINTS , gas: _:Identifier ) // TODO: Is this the right kind of error? - => :: state_hooks :: setStatus(:: ukm :: EVMC_BAD_JUMP_DESTINATION , .CallParamsList); + => :: state_hooks :: setStatus(:: ulm :: EVMC_BAD_JUMP_DESTINATION , .CallParamsList); rule signatureToCall (... signature: Signature:Identifier @@ -233,7 +233,7 @@ module UKM-PREPROCESSING-ENDPOINTS , gas: Gas:Identifier ) => if :: bytes_hooks :: equals - ( Signature , ukmBytesNew(CurrentSignature) , .CallParamsList ) { + ( Signature , ulmBytesNew(CurrentSignature) , .CallParamsList ) { .InnerAttributes self . Method ( BufferId , Gas , .CallParamsList ); .NonEmptyStatements diff --git a/ukm-semantics/main/preprocessing/events.md b/ulm-semantics/main/preprocessing/events.md similarity index 82% rename from ukm-semantics/main/preprocessing/events.md rename to ulm-semantics/main/preprocessing/events.md index e8f9f29..3f8c1b3 100644 --- a/ukm-semantics/main/preprocessing/events.md +++ b/ulm-semantics/main/preprocessing/events.md @@ -1,13 +1,13 @@ ```k -module UKM-PREPROCESSING-EVENTS +module ULM-PREPROCESSING-EVENTS imports private COMMON-K-CELL imports private RUST-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + imports private ULM-PREPROCESSING-SYNTAX-PRIVATE rule - ukmPreprocessEvent + ulmPreprocessEvent (... fullMethodPath: Method:PathInExpression , eventName: _EventName:String ) diff --git a/ukm-semantics/main/preprocessing/methods.md b/ulm-semantics/main/preprocessing/methods.md similarity index 86% rename from ukm-semantics/main/preprocessing/methods.md rename to ulm-semantics/main/preprocessing/methods.md index e820f4a..0e567b7 100644 --- a/ukm-semantics/main/preprocessing/methods.md +++ b/ulm-semantics/main/preprocessing/methods.md @@ -1,21 +1,21 @@ ```k -module UKM-PREPROCESSING-METHODS +module ULM-PREPROCESSING-METHODS imports private COMMON-K-CELL imports private K-EQUAL-SYNTAX imports private RUST-CONVERSIONS-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + imports private ULM-PREPROCESSING-SYNTAX-PRIVATE - rule ukmPreprocessMethods(_:TypePath, .List) => .K - rule ukmPreprocessMethods(Trait:TypePath, ListItem(Name:Identifier) Methods:List) - => ukmPreprocessMethod(Trait, Name, typePathToPathInExpression(append(Trait, Name))) - ~> ukmPreprocessMethods(Trait, Methods:List) + rule ulmPreprocessMethods(_:TypePath, .List) => .K + rule ulmPreprocessMethods(Trait:TypePath, ListItem(Name:Identifier) Methods:List) + => ulmPreprocessMethod(Trait, Name, typePathToPathInExpression(append(Trait, Name))) + ~> ulmPreprocessMethods(Trait, Methods:List) rule - ukmPreprocessMethod(Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) - => ukmPreprocessEndpoint + ulmPreprocessMethod(Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) + => ulmPreprocessEndpoint (... trait: Trait , method: MethodIdentifier , fullMethodPath: Method @@ -30,8 +30,8 @@ module UKM-PREPROCESSING-METHODS andBool getEventName(Atts) ==K "" rule - ukmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) - => ukmPreprocessStorage + ulmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) + => ulmPreprocessStorage (... fullMethodPath: Method , storageName: getStorageName(Atts) ) @@ -44,8 +44,8 @@ module UKM-PREPROCESSING-METHODS andBool getEventName(Atts) ==K "" rule - ukmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) - => ukmPreprocessEvent + ulmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression) + => ulmPreprocessEvent (... fullMethodPath: Method , eventName: getEventName(Atts) ) @@ -56,7 +56,7 @@ module UKM-PREPROCESSING-METHODS requires getEventName(Atts) =/=K "" andBool getEndpointName(Atts, MethodIdentifier) ==K "" andBool getStorageName(Atts) ==K "" - rule ukmPreprocessMethod(_:TypePath, _:Identifier, _:PathInExpression) => .K + rule ulmPreprocessMethod(_:TypePath, _:Identifier, _:PathInExpression) => .K [owise] // This is identical to the function in the mx-rust semantics. diff --git a/ukm-semantics/main/preprocessing/storage.md b/ulm-semantics/main/preprocessing/storage.md similarity index 95% rename from ukm-semantics/main/preprocessing/storage.md rename to ulm-semantics/main/preprocessing/storage.md index 2475292..f3875a8 100644 --- a/ukm-semantics/main/preprocessing/storage.md +++ b/ulm-semantics/main/preprocessing/storage.md @@ -1,20 +1,20 @@ ```k -module UKM-PREPROCESSING-STORAGE +module ULM-PREPROCESSING-STORAGE imports private BYTES imports private COMMON-K-CELL imports private RUST-ERROR-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-SYNTAX-PRIVATE - imports private UKM-REPRESENTATION + imports private ULM-PREPROCESSING-SYNTAX-PRIVATE + imports private ULM-REPRESENTATION rule - ukmPreprocessStorage + ulmPreprocessStorage (... fullMethodPath: Method:PathInExpression , storageName: StorageName:String ) - => ukmAddStorageMethodBody + => ulmAddStorageMethodBody (... methodName: Method , storageName: StorageName , mapperValueType: MapperValue @@ -32,7 +32,7 @@ module UKM-PREPROCESSING-STORAGE rule - ukmAddStorageMethodBody + ulmAddStorageMethodBody (... methodName: Method:PathInExpression , storageName: StorageName:String , mapperValueType: MapperValueType:Type diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ulm-semantics/main/preprocessing/syntax.md similarity index 67% rename from ukm-semantics/main/preprocessing/syntax.md rename to ulm-semantics/main/preprocessing/syntax.md index ec39c7e..0a34d8a 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ulm-semantics/main/preprocessing/syntax.md @@ -1,53 +1,53 @@ ```k -module UKM-PREPROCESSING-SYNTAX +module ULM-PREPROCESSING-SYNTAX imports INT-SYNTAX - syntax UKMInstruction ::= "ukmPreprocessCrates" + syntax ULMInstruction ::= "ulmPreprocessCrates" endmodule -module UKM-PREPROCESSING-SYNTAX-PRIVATE +module ULM-PREPROCESSING-SYNTAX-PRIVATE imports LIST imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX - imports UKM-REPRESENTATION + imports ULM-REPRESENTATION - syntax UKMInstruction ::= ukmPreprocessTraits(List) - | ukmPreprocessTrait(TypePath) - | ukmPreprocessMethods(trait: TypePath, List) - | ukmPreprocessMethod(trait: TypePath, methodId: Identifier, fullMethodPath: PathInExpression) - | ukmPreprocessEndpoint + syntax ULMInstruction ::= ulmPreprocessTraits(List) + | ulmPreprocessTrait(TypePath) + | ulmPreprocessMethods(trait: TypePath, List) + | ulmPreprocessMethod(trait: TypePath, methodId: Identifier, fullMethodPath: PathInExpression) + | ulmPreprocessEndpoint ( trait: TypePath , method: Identifier , fullMethodPath: PathInExpression , endpointName: String ) - | ukmAddEndpointWrapper + | ulmAddEndpointWrapper ( wrapperMethod: PathInExpression , params: NormalizedFunctionParameterList , returnType: Type , method: Identifier ) - | #ukmAddEndpointWrapper + | #ulmAddEndpointWrapper ( wrapperMethod: PathInExpression , params: NormalizedFunctionParameterList , method: Identifier , appendReturn: ExpressionOrError , decodeStatements: NonEmptyStatementsOrError ) - | ukmAddEndpointSignature(signature: BytesOrError, method: Identifier) - | ukmAddDispatcher(TypePath) - | ukmPreprocessStorage + | ulmAddEndpointSignature(signature: BytesOrError, method: Identifier) + | ulmAddDispatcher(TypePath) + | ulmPreprocessStorage ( fullMethodPath: PathInExpression , storageName: String ) - | ukmAddStorageMethodBody + | ulmAddStorageMethodBody ( methodName: PathInExpression , storageName: String , mapperValueType: Type , appendParamsInstructions: NonEmptyStatementsOrError ) - | ukmPreprocessEvent + | ulmPreprocessEvent ( fullMethodPath: PathInExpression , eventName: String ) diff --git a/ukm-semantics/main/preprocessing/traits.md b/ulm-semantics/main/preprocessing/traits.md similarity index 50% rename from ukm-semantics/main/preprocessing/traits.md rename to ulm-semantics/main/preprocessing/traits.md index 2f1bcd0..ecfbf82 100644 --- a/ukm-semantics/main/preprocessing/traits.md +++ b/ulm-semantics/main/preprocessing/traits.md @@ -1,33 +1,33 @@ ```k -module UKM-PREPROCESSING-TRAITS +module ULM-PREPROCESSING-TRAITS imports private COMMON-K-CELL imports private RUST-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + imports private ULM-PREPROCESSING-CONFIGURATION + imports private ULM-PREPROCESSING-SYNTAX-PRIVATE - rule ukmPreprocessTraits(.List) => .K - rule ukmPreprocessTraits(ListItem(T:TypePath) Traits:List) - => ukmPreprocessTrait(T) ~> ukmPreprocessTraits(Traits) + rule ulmPreprocessTraits(.List) => .K + rule ulmPreprocessTraits(ListItem(T:TypePath) Traits:List) + => ulmPreprocessTrait(T) ~> ulmPreprocessTraits(Traits) rule - ukmPreprocessTrait(Trait:TypePath) - => ukmPreprocessMethods(Trait, Methods) ~> ukmAddDispatcher(Trait) + ulmPreprocessTrait(Trait:TypePath) + => ulmPreprocessMethods(Trait, Methods) ~> ulmAddDispatcher(Trait) ... Trait - #[ #token("ukm", "Identifier") + #[ #token("ulm", "Identifier") :: #token("contract", "Identifier") :: .SimplePathList ] .NonEmptyOuterAttributes Methods:List - _ => Trait + _ => Trait - // There should be an owise rule rewriting ukmPreprocessTrait(_) to .K + // There should be an owise rule rewriting ulmPreprocessTrait(_) to .K // For now, it is probably more useful to stop execution when encountering // an unknown trait than skipping it. endmodule diff --git a/ulm-semantics/main/representation.md b/ulm-semantics/main/representation.md new file mode 100644 index 0000000..e7c56bc --- /dev/null +++ b/ulm-semantics/main/representation.md @@ -0,0 +1,25 @@ +```k + +module ULM-REPRESENTATION + imports BYTES-SYNTAX + imports INT-SYNTAX + imports MINT + imports RUST-VALUE-SYNTAX + + syntax UlmValue ::= ulmBytesValue(Bytes) + | ulmIntValue(Int) + syntax UlmExpression ::= ulmBytesId(MInt{64}) + | ulmInt(MInt{64}) + | UlmValue + syntax KResult ::= UlmValue + + syntax Expression ::= ulmCast(Expression, Expression) [seqstrict] + syntax Expression ::= ulmBytesNew(Bytes) + + syntax Value ::= rustType(Type) + + syntax BytesOrError ::= Bytes | SemanticsError + +endmodule + +``` diff --git a/ukm-semantics/targets/execution/configuration.md b/ulm-semantics/targets/execution/configuration.md similarity index 54% rename from ukm-semantics/targets/execution/configuration.md rename to ulm-semantics/targets/execution/configuration.md index efbae4d..b14867e 100644 --- a/ukm-semantics/targets/execution/configuration.md +++ b/ulm-semantics/targets/execution/configuration.md @@ -7,25 +7,25 @@ requires "rust-semantics/config.md" module COMMON-K-CELL imports private BYTES-SYNTAX imports private INT-SYNTAX - imports private UKM-DECODING-SYNTAX - imports private UKM-EXECUTION-SYNTAX + imports private ULM-DECODING-SYNTAX + imports private ULM-EXECUTION-SYNTAX configuration - ukmDecodePreprocessedCell($PGM:Bytes) - ~> ukmExecute($CREATE:Bool, $PGM:Bytes, $ACCTCODE:Int, $GAS:Int) + ulmDecodePreprocessedCell($PGM:Bytes) + ~> ulmExecute($CREATE:Bool, $PGM:Bytes, $ACCTCODE:Int, $GAS:Int) endmodule -module UKM-TARGET-CONFIGURATION +module ULM-TARGET-CONFIGURATION imports COMMON-K-CELL imports RUST-EXECUTION-CONFIGURATION - imports UKM-CONFIGURATION - imports UKM-FULL-PREPROCESSED-CONFIGURATION + imports ULM-CONFIGURATION + imports ULM-FULL-PREPROCESSED-CONFIGURATION configuration - - + + endmodule diff --git a/ukm-semantics/targets/execution/ukm-target.md b/ulm-semantics/targets/execution/ulm-target.md similarity index 54% rename from ukm-semantics/targets/execution/ukm-target.md rename to ulm-semantics/targets/execution/ulm-target.md index e0ad3d4..5e931ea 100644 --- a/ukm-semantics/targets/execution/ukm-target.md +++ b/ulm-semantics/targets/execution/ulm-target.md @@ -6,15 +6,15 @@ requires "configuration.md" requires "rust-semantics/rust-common.md" requires "rust-semantics/rust-common-syntax.md" -module UKM-TARGET-SYNTAX +module ULM-TARGET-SYNTAX endmodule -module UKM-TARGET +module ULM-TARGET imports private RUST-COMMON - imports private UKM-DECODING - imports private UKM-EXECUTION - imports private UKM-HOOKS-TO-ULM-FUNCTIONS - imports private UKM-TARGET-CONFIGURATION + imports private ULM-DECODING + imports private ULM-EXECUTION + imports private ULM-SEMANTICS-HOOKS-TO-ULM-FUNCTIONS + imports private ULM-TARGET-CONFIGURATION endmodule ``` diff --git a/ukm-semantics/targets/preprocessing/configuration.md b/ulm-semantics/targets/preprocessing/configuration.md similarity index 53% rename from ukm-semantics/targets/preprocessing/configuration.md rename to ulm-semantics/targets/preprocessing/configuration.md index 117bd71..e14d30b 100644 --- a/ukm-semantics/targets/preprocessing/configuration.md +++ b/ulm-semantics/targets/preprocessing/configuration.md @@ -8,28 +8,28 @@ requires "rust-semantics/rust-common-syntax.md" module COMMON-K-CELL imports private RUST-PREPROCESSING-SYNTAX - imports private UKM-ENCODING-SYNTAX - imports private UKM-PREPROCESSING-SYNTAX + imports private ULM-ENCODING-SYNTAX + imports private ULM-PREPROCESSING-SYNTAX configuration cratesParser($PGM:WrappedCrateList) - ~> ukmPreprocessCrates - ~> ukmEncodePreprocessedCell + ~> ulmPreprocessCrates + ~> ulmEncodePreprocessedCell endmodule -module UKM-TARGET-CONFIGURATION +module ULM-TARGET-CONFIGURATION imports COMMON-K-CELL - imports UKM-FULL-PREPROCESSED-CONFIGURATION - imports UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION + imports ULM-FULL-PREPROCESSED-CONFIGURATION + imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION configuration - - - + + + - + endmodule ``` diff --git a/ukm-semantics/targets/preprocessing/ukm-target.md b/ulm-semantics/targets/preprocessing/ulm-target.md similarity index 52% rename from ukm-semantics/targets/preprocessing/ukm-target.md rename to ulm-semantics/targets/preprocessing/ulm-target.md index 0cee6c0..a62d1fb 100644 --- a/ukm-semantics/targets/preprocessing/ukm-target.md +++ b/ulm-semantics/targets/preprocessing/ulm-target.md @@ -4,14 +4,14 @@ requires "../../main/encoding.md" requires "../../main/preprocessing.md" requires "configuration.md" -module UKM-TARGET-SYNTAX +module ULM-TARGET-SYNTAX endmodule -module UKM-TARGET +module ULM-TARGET imports private RUST-FULL-PREPROCESSING - imports private UKM-ENCODING - imports private UKM-PREPROCESSING - imports private UKM-TARGET-CONFIGURATION + imports private ULM-ENCODING + imports private ULM-PREPROCESSING + imports private ULM-TARGET-CONFIGURATION endmodule ``` diff --git a/ukm-semantics/targets/testing/configuration.md b/ulm-semantics/targets/testing/configuration.md similarity index 63% rename from ukm-semantics/targets/testing/configuration.md rename to ulm-semantics/targets/testing/configuration.md index 37cc2ab..e8627a9 100644 --- a/ukm-semantics/targets/testing/configuration.md +++ b/ulm-semantics/targets/testing/configuration.md @@ -9,30 +9,30 @@ 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-PREPROCESSING-SYNTAX + imports private ULM-PREPROCESSING-SYNTAX configuration cratesParser($PGM:WrappedCrateList) - ~> ukmPreprocessCrates + ~> ulmPreprocessCrates ~> $TEST:ExecutionTest endmodule -module UKM-TARGET-CONFIGURATION +module ULM-TARGET-CONFIGURATION imports COMMON-K-CELL imports RUST-EXECUTION-CONFIGURATION imports RUST-EXECUTION-TEST-CONFIGURATION - imports UKM-CONFIGURATION - imports UKM-FULL-PREPROCESSED-CONFIGURATION - imports UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION - imports UKM-TEST-CONFIGURATION + imports ULM-CONFIGURATION + imports ULM-FULL-PREPROCESSED-CONFIGURATION + imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION + imports ULM-TEST-CONFIGURATION configuration - - - - + + + + diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ulm-semantics/targets/testing/ulm-target.md similarity index 63% rename from ukm-semantics/targets/testing/ukm-target.md rename to ulm-semantics/targets/testing/ulm-target.md index b0e2281..36b874d 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ulm-semantics/targets/testing/ulm-target.md @@ -10,21 +10,21 @@ requires "rust-semantics/rust-common-syntax.md" requires "rust-semantics/full-preprocessing.md" requires "rust-semantics/test/execution.md" -module UKM-TARGET-SYNTAX +module ULM-TARGET-SYNTAX imports RUST-COMMON-SYNTAX - imports UKM-TEST-SYNTAX + imports ULM-TEST-SYNTAX endmodule -module UKM-TARGET +module ULM-TARGET imports private RUST-COMMON imports private RUST-FULL-PREPROCESSING imports private RUST-EXECUTION-TEST - imports private UKM-CALLDATA-ENCODER - imports private UKM-EXECUTION - imports private UKM-ENCODING - imports private UKM-PREPROCESSING - imports private UKM-TARGET-CONFIGURATION - imports private UKM-TEST-EXECUTION + imports private ULM-CALLDATA-ENCODER + imports private ULM-EXECUTION + imports private ULM-ENCODING + imports private ULM-PREPROCESSING + imports private ULM-TARGET-CONFIGURATION + imports private ULM-TEST-EXECUTION endmodule ``` diff --git a/ulm-semantics/test/configuration.md b/ulm-semantics/test/configuration.md new file mode 100644 index 0000000..40502b2 --- /dev/null +++ b/ulm-semantics/test/configuration.md @@ -0,0 +1,8 @@ +```k + +module ULM-TEST-CONFIGURATION + configuration + .K +endmodule + +``` diff --git a/ukm-semantics/test/execution.md b/ulm-semantics/test/execution.md similarity index 70% rename from ukm-semantics/test/execution.md rename to ulm-semantics/test/execution.md index bd03373..15be28d 100644 --- a/ukm-semantics/test/execution.md +++ b/ulm-semantics/test/execution.md @@ -1,28 +1,28 @@ ```k -module UKM-TEST-SYNTAX +module ULM-TEST-SYNTAX imports BYTES-SYNTAX imports INT-SYNTAX imports STRING-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX - imports UKM-HOOKS-UKM-SYNTAX + imports ULM-SEMANTICS-HOOKS-ULM-SYNTAX imports BYTES-SYNTAX // TODO: Do not use KItem for ptr_holder and value_holder. This is // too generic and can lead to problems. // TODO: Replace the list_ptrs_holder and list_values_holder with // PtrList and ValueList. - syntax UKMTestTypeHolder ::= "ptr_holder" KItem [strict] + syntax ULMTestTypeHolder ::= "ptr_holder" KItem [strict] | "value_holder" KItem | "list_ptrs_holder" List | "list_values_holder" List - syntax UKMTestTypeHolderList ::= List{UKMTestTypeHolder, ","} + syntax ULMTestTypeHolderList ::= List{ULMTestTypeHolder, ","} syntax ExecutionItem ::= "mock" "CallData" | "mock" "Caller" - | "mock" UkmHook UkmHookResult - | "list_mock" UkmHook UkmHookResult + | "mock" UlmHook UlmHookResult + | "list_mock" UlmHook UlmHookResult | "encode_call_data" | "encode_call_data_to_string" | "encode_constructor_data" @@ -46,32 +46,32 @@ module UKM-TEST-SYNTAX | "u256" [token] endmodule -module UKM-TEST-EXECUTION +module ULM-TEST-EXECUTION imports private BYTES imports private COMMON-K-CELL imports private RUST-EXECUTION-TEST-CONFIGURATION imports private RUST-SHARED-SYNTAX - imports private UKM-ENCODING-SYNTAX - imports private UKM-EXECUTION-SYNTAX - imports private UKM-HOOKS-BYTES-CONFIGURATION - imports private UKM-HOOKS-HELPERS-SYNTAX - imports private UKM-HOOKS-STATE-CONFIGURATION - imports private UKM-HOOKS-UKM-SYNTAX - imports private UKM-REPRESENTATION - imports private UKM-TEST-SYNTAX + imports private ULM-ENCODING-SYNTAX + imports private ULM-EXECUTION-SYNTAX + imports private ULM-SEMANTICS-HOOKS-BYTES-CONFIGURATION + imports private ULM-SEMANTICS-HOOKS-HELPERS-SYNTAX + imports private ULM-SEMANTICS-HOOKS-STATE-CONFIGURATION + imports private ULM-SEMANTICS-HOOKS-ULM-SYNTAX + imports private ULM-REPRESENTATION + imports private ULM-TEST-SYNTAX imports private RUST-SHARED-SYNTAX imports private BYTES - syntax Mockable ::= UkmHook + syntax Mockable ::= UlmHook // The following constructions allows us to build more complex data structures // for mocking tests - rule UTH:UKMTestTypeHolder ~> EI:ExecutionItem => EI ~> UTH ... - rule UTHL:UKMTestTypeHolderList ~> EI:ExecutionItem => EI ~> UTHL ... - rule UTH1:UKMTestTypeHolder ~> UTH2:UKMTestTypeHolder - => (UTH1, UTH2):UKMTestTypeHolderList ... - rule UTH:UKMTestTypeHolder ~> UTHL:UKMTestTypeHolderList - => (UTH, UTHL):UKMTestTypeHolderList ... + rule UTH:ULMTestTypeHolder ~> EI:ExecutionItem => EI ~> UTH ... + rule UTHL:ULMTestTypeHolderList ~> EI:ExecutionItem => EI ~> UTHL ... + rule UTH1:ULMTestTypeHolder ~> UTH2:ULMTestTypeHolder + => (UTH1, UTH2):ULMTestTypeHolderList ... + rule UTH:ULMTestTypeHolder ~> UTHL:ULMTestTypeHolderList + => (UTH, UTHL):ULMTestTypeHolderList ... rule hold_string_from_test_stack => ptr_holder P ... ListItem(P) L:List => L @@ -91,7 +91,7 @@ module UKM-TEST-EXECUTION rule hold I => value_holder I ... rule encode_call_data_to_string - ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList + ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .ULMTestTypeHolderList => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) ... @@ -103,25 +103,25 @@ module UKM-TEST-EXECUTION [owise] rule encode_call_data - ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList - => ukmBytesNew(encodeCallData(FNAME, PTYPES, ARGS)) + ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .ULMTestTypeHolderList + => ulmBytesNew(encodeCallData(FNAME, PTYPES, ARGS)) ... rule encode_call_data ~> value_holder FNAME - => ukmBytesNew(encodeCallData(FNAME, .List, .List)) + => ulmBytesNew(encodeCallData(FNAME, .List, .List)) ... [owise] rule encode_constructor_data - ~> list_values_holder ARGS , list_values_holder PTYPES , .UKMTestTypeHolderList - => ukmBytesNew(encodeConstructorData(PTYPES, ARGS)) + ~> list_values_holder ARGS , list_values_holder PTYPES , .ULMTestTypeHolderList + => ulmBytesNew(encodeConstructorData(PTYPES, ARGS)) ... rule encode_constructor_data - => ukmBytesNew(encodeConstructorData(.List, .List)) + => ulmBytesNew(encodeConstructorData(.List, .List)) ... [owise] @@ -139,32 +139,32 @@ module UKM-TEST-EXECUTION ... - rule mock Hook:UkmHook Result:UkmHookResult => mock(Hook, Result) - rule list_mock Hook:UkmHook Result:UkmHookResult => listMock(Hook, Result) + rule mock Hook:UlmHook Result:UlmHookResult => mock(Hook, Result) + rule list_mock Hook:UlmHook Result:UlmHookResult => listMock(Hook, Result) - rule call_contract Account => ukmExecute(false, .Bytes, Account, 100) + rule call_contract Account => ulmExecute(false, .Bytes, Account, 100) - rule init_contract Account => ukmExecute(true, b"init", Account, 100) + rule init_contract Account => ulmExecute(true, b"init", Account, 100) rule (V:PtrValue ~> b"init" ~> clear_pgm) => V rule - output_to_arg => ukmBytesNew(Output) ~> return_value_to_arg + output_to_arg => ulmBytesNew(Output) ~> return_value_to_arg ... - + Output:Bytes - + rule push_status => .K ... - + Status:Int - + .List => ListItem(Status) ... @@ -174,7 +174,7 @@ module UKM-TEST-EXECUTION check_eq I:Int => .K ... ListItem(I) => .List ... - rule (ukmCancel ~> expect_cancel) => .K + rule (ulmCancel ~> expect_cancel) => .K endmodule