From 66b66ea2ab62f4a04394b97cb28b5a02e78b5675 Mon Sep 17 00:00:00 2001 From: Virgil Date: Thu, 24 Oct 2024 00:14:07 +0300 Subject: [PATCH 1/2] Call data encoding and decoding --- .gitignore | 1 + .gitmodules | 3 + Dockerfile | 5 +- Makefile | 25 ++- tests/ukm-contracts/bytes_hooks.rs | 3 +- .../test_bytes_hooks.append32.run | 4 +- .../test_bytes_hooks.append64.run | 4 +- tests/ukm-with-contract/endpoints.1.run | 32 ++-- tests/ukm-with-contract/endpoints.2.run | 9 + tests/ukm-with-contract/erc_20_token.1.run | 176 ++++++++---------- tests/ukm-with-contract/events.1.run | 19 +- tests/ukm-with-contract/require.false.run | 12 +- tests/ukm-with-contract/require.true.run | 12 +- tests/ukm-with-contract/storage.key.run | 33 ++-- tests/ukm-with-contract/storage.simple.run | 19 +- ukm-semantics/main/decoding/syntax.md | 2 +- ukm-semantics/main/encoding.md | 2 + ukm-semantics/main/encoding/encoder.md | 88 +++++++++ ukm-semantics/main/encoding/syntax.md | 18 ++ ukm-semantics/main/hooks/bytes.md | 97 ++++++---- ukm-semantics/main/hooks/ukm.md | 4 +- ukm-semantics/main/preprocessing/endpoints.md | 33 ++-- ukm-semantics/main/preprocessing/storage.md | 1 + ukm-semantics/main/preprocessing/syntax.md | 3 +- ukm-semantics/main/representation.md | 12 +- ukm-semantics/targets/testing/ukm-target.md | 3 + ukm-semantics/test/execution.md | 67 ++++++- 27 files changed, 453 insertions(+), 234 deletions(-) create mode 100644 tests/ukm-with-contract/endpoints.2.run create mode 100644 ukm-semantics/main/encoding/encoder.md diff --git a/.gitignore b/.gitignore index 0b667e7..f4bbed0 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ .build .DS_store +blockchain-k-plugin tmp tmp.* diff --git a/.gitmodules b/.gitmodules index e69de29..3558764 100644 --- a/.gitmodules +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "blockchain-k-plugin"] + path = deps/blockchain-k-plugin + url = https://github.com/runtimeverification/blockchain-k-plugin diff --git a/Dockerfile b/Dockerfile index 305329a..6224020 100644 --- a/Dockerfile +++ b/Dockerfile @@ -8,7 +8,10 @@ FROM runtimeverificationinc/kframework-k:ubuntu-noble-${K_COMMIT} RUN apt-get update \ && apt-get upgrade --yes \ && apt-get install --yes \ - curl + curl \ + libcrypto++-dev \ + libsecp256k1-dev \ + libssl-dev ARG USER_ID=1001 ARG GROUP_ID=1001 diff --git a/Makefile b/Makefile index ac83c27..25bb6c9 100644 --- a/Makefile +++ b/Makefile @@ -134,6 +134,9 @@ ukm-no-contracts-test: $(UKM_NO_CONTRACT_TESTING_OUTPUTS) ukm-with-contracts-test: $(UKM_WITH_CONTRACT_TESTING_OUTPUTS) +deps/blockchain-k-plugin/build/krypto/lib/krypto.a: + make -C deps/blockchain-k-plugin build + $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES) # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(RUST_PREPROCESSING_KOMPILED) @@ -181,30 +184,38 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTI -I . \ --debug -$(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) +$(UKM_EXECUTION_TIMESTAMP): $(UKM_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 \ + $$(which kompile) ukm-semantics/targets/execution/ukm-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) \ -I kllvm \ + -I deps/blockchain-k-plugin \ -I . \ --debug -$(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) +$(UKM_PREPROCESSING_TIMESTAMP): $(UKM_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 \ + $$(which kompile) ukm-semantics/targets/preprocessing/ukm-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) \ -I . \ + -I deps/blockchain-k-plugin \ --debug -$(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) +$(UKM_TESTING_TIMESTAMP): $(UKM_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 \ - ${PLUGIN_FLAGS} \ + $$(which kompile) ukm-semantics/targets/testing/ukm-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_TESTING_KOMPILED) \ -I . \ + -I deps/blockchain-k-plugin \ -I kllvm \ --debug diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs index 5620de9..c14b5ba 100644 --- a/tests/ukm-contracts/bytes_hooks.rs +++ b/tests/ukm-contracts/bytes_hooks.rs @@ -1,6 +1,7 @@ extern "C" { fn empty() -> u64; fn length(bytes_id: u64) -> u32; + fn equals(bytes_id_1: u64, bytes_id_2: u64) -> bool; fn append_u256(bytes_id: u64, value: u256) -> u64; fn append_u160(bytes_id: u64, value: u160) -> u64; @@ -19,7 +20,7 @@ extern "C" { fn decode_u32(bytes_id: u64) -> (u64, u32); fn decode_u16(bytes_id: u64) -> (u64, u16); fn decode_u8(bytes_id: u64) -> (u64, u8); - fn decode_str(bytes_id: u64) -> (u64, str); + fn decode_signature(bytes_id: u64) -> (u64, u64); fn hash(bytes_id: u64) -> u64; } diff --git a/tests/ukm-no-contract/test_bytes_hooks.append32.run b/tests/ukm-no-contract/test_bytes_hooks.append32.run index 124d4c5..d7c4dfa 100644 --- a/tests/ukm-no-contract/test_bytes_hooks.append32.run +++ b/tests/ukm-no-contract/test_bytes_hooks.append32.run @@ -3,11 +3,11 @@ call :: test_bytes_hooks :: append_u32; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 3_u32; +check_eq 32_u32; push 1000_u32; call :: test_bytes_hooks :: append_u32; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 4_u32 +check_eq 32_u32 diff --git a/tests/ukm-no-contract/test_bytes_hooks.append64.run b/tests/ukm-no-contract/test_bytes_hooks.append64.run index b02a99a..4dd72f1 100644 --- a/tests/ukm-no-contract/test_bytes_hooks.append64.run +++ b/tests/ukm-no-contract/test_bytes_hooks.append64.run @@ -3,11 +3,11 @@ call :: test_bytes_hooks :: append_u64; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 3_u32; +check_eq 32_u32; push 1000_u64; call :: test_bytes_hooks :: append_u64; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 4_u32 +check_eq 32_u32 diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run index 4264f65..46df244 100644 --- a/tests/ukm-with-contract/endpoints.1.run +++ b/tests/ukm-with-contract/endpoints.1.run @@ -1,23 +1,19 @@ -call :: bytes_hooks :: empty; -return_value_to_arg; -push "myEndpoint(Uint64)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; -push 123_u64; -call :: bytes_hooks :: append_u64; -return_value; -mock CallData; +push "myEndpoint"; +hold_string_from_test_stack; +push "uint64"; +hold_list_values_from_test_stack; +push 123_u64; +hold_list_values_from_test_stack; +encode_call_data; + +return_value; +mock CallData; call_contract 12345; return_value; check_eq (); -push_status; -check_eq 2; - -output_to_arg; -call :: test_helpers :: decode_single_u64; -return_value; - -check_eq 126_u64 - +push_status; +check_eq 2; +output_to_arg; call :: test_helpers :: decode_single_u64; return_value; +check_eq 126_u64 \ No newline at end of file diff --git a/tests/ukm-with-contract/endpoints.2.run b/tests/ukm-with-contract/endpoints.2.run new file mode 100644 index 0000000..c0d4d50 --- /dev/null +++ b/tests/ukm-with-contract/endpoints.2.run @@ -0,0 +1,9 @@ +push "myEndpoint"; +hold_string_from_test_stack; +push "uint64"; +hold_list_values_from_test_stack; +push 1_u64; +hold_list_values_from_test_stack; +mock EncodeCallDataToString; +return_value; +check_eq "\x00\x81\x00\x92\x00(\x00T\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ukm-with-contract/erc_20_token.1.run index 21b01e3..53d83f0 100644 --- a/tests/ukm-with-contract/erc_20_token.1.run +++ b/tests/ukm-with-contract/erc_20_token.1.run @@ -1,33 +1,34 @@ list_mock GetAccountStorageHook ( 7809087261546347641 ) ukmIntResult(0, u256); list_mock SetAccountStorageHook ( 7809087261546347641 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(0, u256); -list_mock SetAccountStorageHook ( 7162266444907899391 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); -list_mock SetAccountStorageHook ( 7162266444907899391 , 9900 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(0, u256); -list_mock SetAccountStorageHook ( 7162266444908917614 , 100 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(100, u256); -list_mock SetAccountStorageHook ( 8028228613167873919 , 200 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 8028228613167873919 ) ukmIntResult(200, u256); -list_mock SetAccountStorageHook ( 8028228613167873919 , 0 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); -list_mock SetAccountStorageHook ( 7162266444907899391 , 9700 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(100, u256); -list_mock SetAccountStorageHook ( 7162266444908917614 , 300 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9700, u256); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(300, u256); - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "#init(Uint256)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +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); + +push "#init"; +hold_string_from_test_stack; +push "uint256"; +hold_list_values_from_test_stack; push 10000_u256; -call :: bytes_hooks :: append_u256; +hold_list_values_from_test_stack; +encode_call_data; + return_value; mock CallData; @@ -49,14 +50,13 @@ check_eq 0_u32; - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "balanceOf(Uint160)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "balanceOf"; +hold_string_from_test_stack; +push "uint160"; +hold_list_values_from_test_stack; push 1010101_u160; -call :: bytes_hooks :: append_u160; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -74,17 +74,15 @@ return_value; check_eq 10000_u256; - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "transfer(Uint160,Uint256)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "transfer"; +hold_string_from_test_stack; +push "uint160"; +push "uint256"; +hold_list_values_from_test_stack; push 2020202_u160; -call :: bytes_hooks :: append_u160; -return_value_to_arg; push 100_u256; -call :: bytes_hooks :: append_u256; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -105,14 +103,13 @@ return_value; check_eq 1_u64; - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "balanceOf(Uint160)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "balanceOf"; +hold_string_from_test_stack; +push "uint160"; +hold_list_values_from_test_stack; push 1010101_u160; -call :: bytes_hooks :: append_u160; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -130,15 +127,13 @@ return_value; check_eq 9900_u256; - - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "balanceOf(Uint160)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "balanceOf"; +hold_string_from_test_stack; +push "uint160"; +hold_list_values_from_test_stack; push 2020202_u160; -call :: bytes_hooks :: append_u160; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -156,20 +151,15 @@ return_value; check_eq 100_u256; - - - - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "approve(Uint160,Uint256)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "approve"; +hold_string_from_test_stack; +push "uint160"; +push "uint256"; +hold_list_values_from_test_stack; push 3030303_u160; -call :: bytes_hooks :: append_u160; -return_value_to_arg; push 200_u256; -call :: bytes_hooks :: append_u256; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -190,20 +180,17 @@ return_value; check_eq 1_u64; - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "transferFrom(Uint160,Uint160,Uint256)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "transferFrom"; +hold_string_from_test_stack; +push "uint160"; +push "uint160"; +push "uint256"; +hold_list_values_from_test_stack; push 1010101_u160; -call :: bytes_hooks :: append_u160; -return_value_to_arg; push 2020202_u160; -call :: bytes_hooks :: append_u160; -return_value_to_arg; push 200_u256; -call :: bytes_hooks :: append_u256; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -225,15 +212,13 @@ check_eq 1_u64; - - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "balanceOf(Uint160)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "balanceOf"; +hold_string_from_test_stack; +push "uint160"; +hold_list_values_from_test_stack; push 1010101_u160; -call :: bytes_hooks :: append_u160; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -252,14 +237,13 @@ check_eq 9700_u256; - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "balanceOf(Uint160)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "balanceOf"; +hold_string_from_test_stack; +push "uint160"; +hold_list_values_from_test_stack; push 2020202_u160; -call :: bytes_hooks :: append_u160; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; diff --git a/tests/ukm-with-contract/events.1.run b/tests/ukm-with-contract/events.1.run index 8c0c04b..34f870c 100644 --- a/tests/ukm-with-contract/events.1.run +++ b/tests/ukm-with-contract/events.1.run @@ -1,14 +1,13 @@ -call :: bytes_hooks :: empty; -return_value_to_arg; -push "logEvent(Uint64,Uint64)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "logEvent"; +hold_string_from_test_stack; +push "uint64"; +push "uint64"; +hold_list_values_from_test_stack; push 123_u64; -call :: bytes_hooks :: append_u64; -return_value_to_arg; -push 555_u64; -call :: bytes_hooks :: append_u64; -return_value; +push 555_u64; +hold_list_values_from_test_stack; +encode_call_data; +return_value; mock CallData; call_contract 12345; diff --git a/tests/ukm-with-contract/require.false.run b/tests/ukm-with-contract/require.false.run index c8ee374..a151319 100644 --- a/tests/ukm-with-contract/require.false.run +++ b/tests/ukm-with-contract/require.false.run @@ -1,10 +1,10 @@ -call :: bytes_hooks :: empty; -return_value_to_arg; -push "myEndpoint(Uint64)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "myEndpoint"; +hold_string_from_test_stack; +push "uint64"; +hold_list_values_from_test_stack; push 0_u64; -call :: bytes_hooks :: append_u64; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; diff --git a/tests/ukm-with-contract/require.true.run b/tests/ukm-with-contract/require.true.run index 4264f65..4e0ec98 100644 --- a/tests/ukm-with-contract/require.true.run +++ b/tests/ukm-with-contract/require.true.run @@ -1,10 +1,10 @@ -call :: bytes_hooks :: empty; -return_value_to_arg; -push "myEndpoint(Uint64)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "myEndpoint"; +hold_string_from_test_stack; +push "uint64"; +hold_list_values_from_test_stack; push 123_u64; -call :: bytes_hooks :: append_u64; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; diff --git a/tests/ukm-with-contract/storage.key.run b/tests/ukm-with-contract/storage.key.run index a2e618d..8d54dcf 100644 --- a/tests/ukm-with-contract/storage.key.run +++ b/tests/ukm-with-contract/storage.key.run @@ -1,16 +1,15 @@ -mock SetAccountStorageHook ( 7010817630605304703 , 123 ) ukmNoResult(); -mock GetAccountStorageHook ( 7010817630605304703 ) ukmIntResult(123, u64); - -call :: bytes_hooks :: empty; -return_value_to_arg; -push "setMyDataKey(Uint64,Uint64)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +mock SetAccountStorageHook ( 8738216329482039167 , 123 ) ukmNoResult(); +mock GetAccountStorageHook ( 8738216329482039167 ) ukmIntResult(123, u64); + +push "setMyDataKey"; +hold_string_from_test_stack; +push "uint64"; +push "uint64"; +hold_list_values_from_test_stack; push 555_u64; -call :: bytes_hooks :: append_u64; -return_value_to_arg; push 123_u64; -call :: bytes_hooks :: append_u64; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -22,13 +21,13 @@ push_status; check_eq 2; -call :: bytes_hooks :: empty; -return_value_to_arg; -push "getMyDataKey(Uint64)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "getMyDataKey"; +hold_string_from_test_stack; +push "uint64"; +hold_list_values_from_test_stack; push 555_u64; -call :: bytes_hooks :: append_u64; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; diff --git a/tests/ukm-with-contract/storage.simple.run b/tests/ukm-with-contract/storage.simple.run index 4648776..2b2b4ba 100644 --- a/tests/ukm-with-contract/storage.simple.run +++ b/tests/ukm-with-contract/storage.simple.run @@ -1,13 +1,13 @@ mock SetAccountStorageHook ( 1809217465971809 , 123 ) ukmNoResult(); mock GetAccountStorageHook ( 1809217465971809 ) ukmIntResult(123, u64); -call :: bytes_hooks :: empty; -return_value_to_arg; -push "setMyData(Uint64)"; -call :: bytes_hooks :: append_str; -return_value_to_arg; +push "setMyData"; +hold_string_from_test_stack; +push "uint64"; +hold_list_values_from_test_stack; push 123_u64; -call :: bytes_hooks :: append_u64; +hold_list_values_from_test_stack; +encode_call_data; return_value; mock CallData; @@ -19,10 +19,9 @@ push_status; check_eq 2; -call :: bytes_hooks :: empty; -return_value_to_arg; -push "getMyData()"; -call :: bytes_hooks :: append_str; +push "getMyData"; +hold_string_from_test_stack; +encode_call_data; return_value; mock CallData; diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md index 7fa88fc..35843be 100644 --- a/ukm-semantics/main/decoding/syntax.md +++ b/ukm-semantics/main/decoding/syntax.md @@ -7,4 +7,4 @@ module UKM-DECODING-SYNTAX endmodule -``` +``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding.md b/ukm-semantics/main/encoding.md index 9f08445..60ba0de 100644 --- a/ukm-semantics/main/encoding.md +++ b/ukm-semantics/main/encoding.md @@ -1,8 +1,10 @@ ```k requires "encoding/syntax.md" +requires "encoding/encoder.md" module UKM-ENCODING + imports UKM-CALLDATA-ENCODER endmodule ``` diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md new file mode 100644 index 0000000..493f962 --- /dev/null +++ b/ukm-semantics/main/encoding/encoder.md @@ -0,0 +1,88 @@ +```k +requires "plugin/krypto.md" + +module UKM-CALLDATA-ENCODER + imports private BYTES + imports private INT-SYNTAX + imports private KRYPTO + imports private STRING + imports private UKM-ENCODING-SYNTAX + + rule encodeFunctionSignatureAsBytes(FS) + => encodeHexBytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) + rule encodeFunctionSignatureAsBytes(E:SemanticsError) => E + + // TODO: Error for argument of length 1 or string not hex + rule encodeHexBytes(_:String) => .Bytes + [owise] + rule encodeHexBytes(S:String) + => Int2Bytes(2, String2Base(substrString(S, 0, 2), 16), BE) + +Bytes encodeHexBytes(substrString(S, 2, lengthString(S))) + requires 2 <=Int lengthString(S) andBool isHex(substrString(S, 0, 2), 0) + + syntax Bool ::= isHex(String, idx:Int) [function, total] + rule isHex(S:String, I:Int) => true + requires I isHexDigit(substrString(S, I, I +Int 1)) andBool isHex(S, I +Int 1) + requires 0 <=Int I andBool I ("0" <=String S andBool S <=String "9") + orBool ("a" <=String S andBool S <=String "f") + orBool ("A" <=String S andBool S <=String "F") + +endmodule + +module UKM-CALLDATA-ENCODER-TEST + imports private BYTES + imports private INT-SYNTAX + imports private KRYPTO + imports private STRING + imports private UKM-ENCODING-SYNTAX + imports private UKM-ENCODING-TESTING-SYNTAX + + rule encodeCallData(FN:String, FAT:List, FAL:List) => + encodeFunctionSignature(FN, FAT, "") +Bytes encodeFunctionParams(FAL, FAT, b"") + + // Function signature encoding + rule encodeFunctionSignature(FuncName:String, RL:List, "") => + encodeFunctionSignature("", RL:List, FuncName +String "(") [priority(40)] + + rule encodeFunctionSignature("", ListItem(FuncParam:String) RL:List, FS) => + encodeFunctionSignature("", RL, FS +String FuncParam +String ",") [owise] + + // The last param does not have a follow up comma + rule encodeFunctionSignature("", ListItem(FuncParam:String) .List, FS) => + encodeFunctionSignature("", .List, FS +String FuncParam ) + + rule encodeFunctionSignature("", .List, FS) => encodeHexBytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) + + // Function parameters encoding + rule encodeFunctionParams(ListItem(V:Value) ARGS:List, ListItem(T:String) PTYPES:List, B:Bytes) => + encodeFunctionParams(ARGS:List, PTYPES:List, B:Bytes +Bytes convertToKBytes(V, T)) + + rule encodeFunctionParams(.List, .List, B:Bytes) => B + + + // Encoding of individual types + + rule convertToKBytes(i8(V) , "int8") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i16(V), "int16") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u16(V), "uint16") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i32(V), "int32") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u32(V), "uint32") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i64(V), "int64") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint64") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u128(V), "uint128") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(true, "bool") => Int2Bytes(32, 1, BE:Endianness) + rule convertToKBytes(false, "bool") => Int2Bytes(32, 0, BE:Endianness) + rule convertToKBytes(u256(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + +endmodule + +``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index d303075..461d987 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -2,9 +2,27 @@ module UKM-ENCODING-SYNTAX imports BYTES-SYNTAX + imports LIST + imports RUST-REPRESENTATION + imports UKM-REPRESENTATION syntax UKMInstruction ::= "ukmEncodePreprocessedCell" + syntax BytesOrError ::= encodeFunctionSignatureAsBytes(StringOrError) [function, total] + syntax Bytes ::= encodeHexBytes(String) [function, total] + +endmodule + +module UKM-ENCODING-TESTING-SYNTAX + imports BYTES-SYNTAX + imports LIST + imports RUST-REPRESENTATION + + syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list + | encodeFunctionSignature (String, List, String) [function] + | encodeFunctionParams (List, List, Bytes) [function] + | convertToKBytes ( Value , String ) [function] + endmodule ``` diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md index e024361..78ee3c3 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ukm-semantics/main/hooks/bytes.md @@ -15,24 +15,21 @@ module UKM-HOOKS-BYTES-CONFIGURATION endmodule -module UKM-HOOKS-BYTES-SYNTAX - imports BYTES-SYNTAX - syntax Expression ::= ukmBytesNew(Bytes) -endmodule - module UKM-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-HOOKS-BYTES-SYNTAX imports private UKM-REPRESENTATION syntax Identifier ::= "bytes_hooks" [token] | "empty" [token] | "length" [token] + | "equals" [token] + | "append_bool" [token] | "append_u256" [token] | "append_u160" [token] | "append_u128" [token] @@ -40,7 +37,6 @@ module UKM-HOOKS-BYTES | "append_u32" [token] | "append_u16" [token] | "append_u8" [token] - | "append_bool" [token] | "append_str" [token] | "decode_u256" [token] | "decode_u160" [token] @@ -51,6 +47,7 @@ module UKM-HOOKS-BYTES | "decode_u8" [token] | "decode_str" [token] | "hash" [token] + | "decode_signature" [token] rule @@ -76,6 +73,13 @@ module UKM-HOOKS-BYTES ) => ukmBytesLength(BufferIdId) + rule + normalizedFunctionCall + ( :: bytes_hooks :: equals :: .PathExprSegments + , BufferIdId1:Ptr, BufferIdId2:Ptr, .PtrList + ) + => ukmBytesEquals(BufferIdId1, BufferIdId2) + rule normalizedFunctionCall ( :: bytes_hooks :: append_u256 :: .PathExprSegments @@ -195,13 +199,19 @@ module UKM-HOOKS-BYTES ) => ukmBytesDecode(BufferIdId, str) - rule + rule normalizedFunctionCall ( :: bytes_hooks :: hash :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) => ukmBytesHash(BufferIdId) + rule + normalizedFunctionCall + ( :: bytes_hooks :: decode_signature :: .PathExprSegments + , BufferIdId:Ptr, .PtrList + ) + => ukmBytesDecodeBytes(BufferIdId, 8) // --------------------------------------- rule @@ -216,16 +226,21 @@ module UKM-HOOKS-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(Bytes, Bytes) + | 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)] @@ -249,6 +264,11 @@ module UKM-HOOKS-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)) + => 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))) @@ -265,54 +285,61 @@ module UKM-HOOKS-BYTES => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) rule ukmBytesAppendInt(ukmBytesValue(B:Bytes), Value:Int) - => ukmBytesAppendLenAndBytes(B, Int2Bytes(Value, BE, Unsigned)) + => 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))) + // TODO: This can create key ambiguity for storage rule ukmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String)) - => ukmBytesAppendBytes(ukmBytesId(BytesId), String2Bytes(Value)) + => ukmBytesAppendLenAndBytes(ukmBytesId(BytesId), String2Bytes(Value)) rule ukmBytesAppendBytes(ukmBytesValue(B:Bytes), Value:Bytes) - => ukmBytesAppendLenAndBytes(B, Value) + => ukmBytesNew(B +Bytes Value) - rule ukmBytesAppendLenAndBytes(First:Bytes, Second:Bytes) + rule ukmBytesAppendLenAndBytes(ukmBytesValue(First:Bytes), Second:Bytes) => ukmBytesNew(First +Bytes Int2Bytes(2, lengthBytes(Second), BE) +Bytes Second) requires lengthBytes(Second) ukmBytesDecodeBytes(ukmBytesId(BytesId), L:Int) + rule ukmBytesDecodeBytes(ukmBytesValue(B:Bytes), L:Int) + => tupleExpression + ( ukmBytesNew(substrBytes(B, L, lengthBytes(B))) + , ukmBytesNew(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 - ( Bytes2Int(substrBytes(B, 0, 2), BE, Unsigned) - , substrBytes(B, 2, lengthBytes(B)) - , T:Type - ) - requires 2 <=Int lengthBytes(B) - rule ukmBytesDecode(Len:Int, B:Bytes, T:Type) - => ukmBytesDecodeInt - ( Bytes2Int(substrBytes(B, 0, Len), BE, Unsigned) - , substrBytes(B, Len, lengthBytes(B)) - , T:Type - ) - requires Len <=Int lengthBytes(B) andBool isUnsignedInt(T) - rule ukmBytesDecode(Len:Int, B:Bytes, T:Type) - => ukmBytesDecodeInt - ( Bytes2Int(substrBytes(B, 0, Len), BE, Signed) - , substrBytes(B, Len, lengthBytes(B)) - , T:Type + ( integerToValue(Bytes2Int(substrBytes(B, 0, 32), BE, Unsigned), T) + , substrBytes(B, 32, lengthBytes(B)) ) - requires Len <=Int lengthBytes(B) andBool isSignedInt(T) - rule ukmBytesDecode(Len:Int, B:Bytes, str) + requires isUnsignedInt(T) andBool 32 <=Int lengthBytes(B) + rule ukmBytesDecode(ukmBytesValue(B:Bytes), T:Type) => ukmBytesDecode - ( Bytes2String(substrBytes(B, 0, Len)) - , substrBytes(B, Len, lengthBytes(B)) + ( 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 + ( Bytes2Int(substrBytes(B, 0, 2), BE, Signed) + , substrBytes(B, 2, lengthBytes(B)) ) - requires Len <=Int 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))) + requires 0 <=Int Len andBool Len <=Int lengthBytes(B) + rule ukmBytesDecode(Value:Value, B:Bytes) => tupleExpression(ukmBytesNew(B) , ptrValue(null, Value) , .TupleElementsNoEndComma) diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md index 5246aba..1129d38 100644 --- a/ukm-semantics/main/hooks/ukm.md +++ b/ukm-semantics/main/hooks/ukm.md @@ -18,9 +18,9 @@ endmodule module UKM-HOOKS-UKM imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX - imports private UKM-HOOKS-BYTES-SYNTAX imports private UKM-HOOKS-SIGNATURE imports private UKM-HOOKS-UKM-SYNTAX + imports private UKM-REPRESENTATION syntax Identifier ::= "ukm" [token] | "CallData" [token] @@ -67,9 +67,9 @@ endmodule // for the ULM hooks. module UKM-HOOKS-TO-ULM-FUNCTIONS imports private RUST-REPRESENTATION - imports private UKM-HOOKS-BYTES-SYNTAX imports private UKM-HOOKS-UKM-SYNTAX imports private ULM-HOOKS + imports private UKM-REPRESENTATION rule CallDataHook() => ukmBytesNew(CallData()) rule CallerHook() => ukmIntResult(Caller(), u160) diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index f567980..98f416b 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -7,8 +7,10 @@ module UKM-PREPROCESSING-ENDPOINTS 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-REPRESENTATION rule @@ -90,7 +92,7 @@ module UKM-PREPROCESSING-ENDPOINTS rule - ukmAddEndpointSignature(Signature:String, Method:Identifier) => .K + ukmAddEndpointSignature(Signature:Bytes, Method:Identifier) => .K ... @@ -163,18 +165,20 @@ module UKM-PREPROCESSING-ENDPOINTS | "decode_u160" [token] | "decode_u256" [token] | "decode_str" [token] + | "decode_signature" [token] | "empty" [token] + | "equals" [token] | "ukm" [token] | "CallData" [token] | "EVMC_BAD_JUMP_DESTINATION" [token] | "EVMC_SUCCESS" [token] - syntax StringOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total] - | signatureTypes(NormalizedFunctionParameterList) [function, total] + syntax BytesOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total] + syntax StringOrError ::= signatureTypes(NormalizedFunctionParameterList) [function, total] | signatureType(Type) [function, total] rule methodSignature(S:String, Ps:NormalizedFunctionParameterList) - => concat(concat(S +String "(", signatureTypes(Ps)), ")") + => encodeFunctionSignatureAsBytes(concat(concat(S +String "(", signatureTypes(Ps)), ")")) rule signatureTypes(.NormalizedFunctionParameterList) => "" rule signatureTypes(_ : T:Type , .NormalizedFunctionParameterList) @@ -186,13 +190,13 @@ module UKM-PREPROCESSING-ENDPOINTS ) => concat(signatureType(T), concat(",", signatureTypes(Ps))) - rule signatureType(u8) => "Uint8" - rule signatureType(u16) => "Uint16" - rule signatureType(u32) => "Uint32" - rule signatureType(u64) => "Uint64" - rule signatureType(u128) => "Uint128" - rule signatureType(u160) => "Uint160" - rule signatureType(u256) => "Uint256" + rule signatureType(u8) => "uint8" + rule signatureType(u16) => "uint16" + rule signatureType(u32) => "uint32" + rule signatureType(u64) => "uint64" + rule signatureType(u128) => "uint128" + rule signatureType(u160) => "uint160" + rule signatureType(u256) => "uint256" rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T)) [owise] @@ -215,12 +219,13 @@ module UKM-PREPROCESSING-ENDPOINTS rule signatureToCall (... signature: Signature:Identifier - , signatures: ListItem(CurrentSignature:String) Signatures:List + , signatures: ListItem(CurrentSignature:Bytes) Signatures:List , signatureToMethod: (CurrentSignature |-> Method:Identifier _:Map) #as SignatureToMethod:Map , bufferId: BufferId:Identifier , gas: Gas:Identifier ) - => if signature == CurrentSignature { + => if :: bytes_hooks :: equals + ( Signature , ukmBytesNew(CurrentSignature) , .CallParamsList ) { .InnerAttributes self . Method ( BufferId , Gas , .CallParamsList ); .NonEmptyStatements @@ -231,7 +236,7 @@ module UKM-PREPROCESSING-ENDPOINTS }; syntax Expression ::= decodeSignature(Identifier) [function, total] - rule decodeSignature(BufferId) => :: bytes_hooks :: decode_str ( BufferId , .CallParamsList ) + rule decodeSignature(BufferId) => :: bytes_hooks :: decode_signature ( BufferId , .CallParamsList ) syntax ExpressionOrError ::= appendValue(bufferId: Identifier, value: Identifier, Type) [function, total] rule appendValue(BufferId:Identifier, Value:Identifier, u8) diff --git a/ukm-semantics/main/preprocessing/storage.md b/ukm-semantics/main/preprocessing/storage.md index a6b108a..2475292 100644 --- a/ukm-semantics/main/preprocessing/storage.md +++ b/ukm-semantics/main/preprocessing/storage.md @@ -1,6 +1,7 @@ ```k module UKM-PREPROCESSING-STORAGE + imports private BYTES imports private COMMON-K-CELL imports private RUST-ERROR-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md index c186d6d..ec39c7e 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ukm-semantics/main/preprocessing/syntax.md @@ -10,6 +10,7 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE imports LIST imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX + imports UKM-REPRESENTATION syntax UKMInstruction ::= ukmPreprocessTraits(List) | ukmPreprocessTrait(TypePath) @@ -34,7 +35,7 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE , appendReturn: ExpressionOrError , decodeStatements: NonEmptyStatementsOrError ) - | ukmAddEndpointSignature(signature: StringOrError, method: Identifier) + | ukmAddEndpointSignature(signature: BytesOrError, method: Identifier) | ukmAddDispatcher(TypePath) | ukmPreprocessStorage ( fullMethodPath: PathInExpression diff --git a/ukm-semantics/main/representation.md b/ukm-semantics/main/representation.md index 50af36f..412bdaf 100644 --- a/ukm-semantics/main/representation.md +++ b/ukm-semantics/main/representation.md @@ -1,10 +1,10 @@ ```k module UKM-REPRESENTATION - imports private BYTES-SYNTAX - imports private INT-SYNTAX - imports private MINT - imports private RUST-VALUE-SYNTAX + imports BYTES-SYNTAX + imports INT-SYNTAX + imports MINT + imports RUST-VALUE-SYNTAX syntax UkmValue ::= ukmBytesValue(Bytes) | ukmIntValue(Int) @@ -14,8 +14,12 @@ module UKM-REPRESENTATION 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/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index 1321ddc..6656b75 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ukm-semantics/targets/testing/ukm-target.md @@ -1,5 +1,6 @@ ```k +requires "../../main/encoding.md" requires "../../main/execution.md" requires "../../main/preprocessing.md" requires "../../test/execution.md" @@ -18,7 +19,9 @@ module UKM-TARGET imports private RUST-COMMON imports private RUST-FULL-PREPROCESSING imports private RUST-EXECUTION-TEST + imports private UKM-CALLDATA-ENCODER-TEST imports private UKM-EXECUTION + imports private UKM-ENCODING imports private UKM-PREPROCESSING imports private UKM-TARGET-CONFIGURATION imports private UKM-TEST-EXECUTION diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index 77956e4..5b99fc1 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -1,18 +1,32 @@ ```k module UKM-TEST-SYNTAX + imports BYTES-SYNTAX imports INT-SYNTAX + imports STRING-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX imports UKM-HOOKS-UKM-SYNTAX + syntax UKMTestTypeHolder ::= "ptr_holder" KItem [strict] + | "value_holder" KItem + | "list_ptrs_holder" List + | "list_values_holder" List + + syntax UKMTestTypeHolderList ::= List{UKMTestTypeHolder, ","} + syntax ExecutionItem ::= "mock" "CallData" | "mock" "Caller" | "mock" UkmHook UkmHookResult | "list_mock" UkmHook UkmHookResult + | "encode_call_data" + | "mock" "EncodeCallDataToString" | "call_contract" Int + | "hold" KItem | "output_to_arg" | "push_status" | "check_eq" Int + | "hold_string_from_test_stack" + | "hold_list_values_from_test_stack" | "expect_cancel" syntax Identifier ::= "u8" [token] @@ -25,18 +39,69 @@ module UKM-TEST-SYNTAX endmodule module UKM-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-ENCODING-TESTING-SYNTAX imports private UKM-EXECUTION-SYNTAX imports private UKM-HOOKS-BYTES-CONFIGURATION - imports private UKM-HOOKS-BYTES-SYNTAX 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 syntax Mockable ::= UkmHook + // 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 hold_string_from_test_stack => ptr_holder P ... + ListItem(P) L:List => L + rule ptr_holder ptrValue(_, V) => value_holder V ... + + rule hold_list_values_from_test_stack => list_ptrs_holder L ~> list_values_holder .List ... + L:List => .List + rule list_ptrs_holder ListItem(I) LPH ~> list_values_holder LLH + => I ~> list_ptrs_holder LPH ~> list_values_holder LLH ... + rule ptrValue(_, V) ~> list_ptrs_holder LPH ~> list_values_holder LLH + => list_ptrs_holder LPH ~> list_values_holder ListItem(V) LLH ... + rule list_ptrs_holder .List => .K ... + + rule hold I => value_holder I ... + + rule mock EncodeCallDataToString + ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList + => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) + ... + + + rule mock EncodeCallDataToString + ~> value_holder FNAME + => Bytes2String(encodeCallData(FNAME, .List, .List)) + ... + [owise] + + rule encode_call_data + ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList + => ukmBytesNew(encodeCallData(FNAME, PTYPES, ARGS)) + ... + + + rule encode_call_data + ~> value_holder FNAME + => ukmBytesNew(encodeCallData(FNAME, .List, .List)) + ... + [owise] + rule mock CallData => mock(CallDataHook(), V) ... From 29162dc607859759c9cf9a698fe9c4120b424f99 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Thu, 24 Oct 2024 14:38:31 -0300 Subject: [PATCH 2/2] Making spliting the encoding to helpers and main module. Adding TODOs. --- ukm-semantics/main/encoding/encoder.md | 75 +++++++++++---------- ukm-semantics/main/encoding/syntax.md | 16 +++-- ukm-semantics/targets/testing/ukm-target.md | 2 +- ukm-semantics/test/execution.md | 1 - 4 files changed, 50 insertions(+), 44 deletions(-) diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index 493f962..a560feb 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -1,16 +1,12 @@ ```k requires "plugin/krypto.md" -module UKM-CALLDATA-ENCODER +module UKM-ENCODING-HELPER imports private BYTES imports private INT-SYNTAX imports private KRYPTO imports private STRING - imports private UKM-ENCODING-SYNTAX - - rule encodeFunctionSignatureAsBytes(FS) - => encodeHexBytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) - rule encodeFunctionSignatureAsBytes(E:SemanticsError) => E + imports private UKM-ENCODING-HELPER-SYNTAX // TODO: Error for argument of length 1 or string not hex rule encodeHexBytes(_:String) => .Bytes @@ -33,56 +29,63 @@ module UKM-CALLDATA-ENCODER orBool ("a" <=String S andBool S <=String "f") orBool ("A" <=String S andBool S <=String "F") + // Encoding of individual types + + rule convertToKBytes(i8(V) , "int8") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i16(V), "int16") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u16(V), "uint16") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i32(V), "int32") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u32(V), "uint32") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i64(V), "int64") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint64") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u128(V), "uint128") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(true, "bool") => Int2Bytes(32, 1, BE:Endianness) + rule convertToKBytes(false, "bool") => Int2Bytes(32, 0, BE:Endianness) + rule convertToKBytes(u256(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + endmodule -module UKM-CALLDATA-ENCODER-TEST +module UKM-CALLDATA-ENCODER imports private BYTES imports private INT-SYNTAX imports private KRYPTO imports private STRING imports private UKM-ENCODING-SYNTAX - imports private UKM-ENCODING-TESTING-SYNTAX + imports private UKM-ENCODING-HELPER-SYNTAX + imports private UKM-ENCODING-HELPER + rule encodeFunctionSignatureAsBytes(FS) + => encodeHexBytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) + rule encodeFunctionSignatureAsBytes(E:SemanticsError) => E + + // TODO: it may be worth extracting the substrString(Keccak256(String2Bytes(FS)), 0, 8) + // thing to a function that takes a String and produces a String or Bytes (as opposed to + // taking a StringOrError as below) (perhaps with an encodeAsBytes(...) on top of it) and + // then use it here and in the rules below. rule encodeCallData(FN:String, FAT:List, FAL:List) => - encodeFunctionSignature(FN, FAT, "") +Bytes encodeFunctionParams(FAL, FAT, b"") + encodeFunctionSignature(FN, FAT) +Bytes encodeFunctionParams(FAL, FAT, b"") // Function signature encoding - rule encodeFunctionSignature(FuncName:String, RL:List, "") => - encodeFunctionSignature("", RL:List, FuncName +String "(") [priority(40)] + rule encodeFunctionSignature(FuncName:String, RL:List) => + encodeFunctionSignatureHelper(RL:List, FuncName +String "(") [priority(40)] - rule encodeFunctionSignature("", ListItem(FuncParam:String) RL:List, FS) => - encodeFunctionSignature("", RL, FS +String FuncParam +String ",") [owise] + rule encodeFunctionSignatureHelper(ListItem(FuncParam:String) RL:List, FS) => + encodeFunctionSignatureHelper(RL, FS +String FuncParam +String ",") [owise] // The last param does not have a follow up comma - rule encodeFunctionSignature("", ListItem(FuncParam:String) .List, FS) => - encodeFunctionSignature("", .List, FS +String FuncParam ) - - rule encodeFunctionSignature("", .List, FS) => encodeHexBytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) + rule encodeFunctionSignatureHelper(ListItem(FuncParam:String) .List, FS) => + encodeFunctionSignatureHelper(.List, FS +String FuncParam ) + + rule encodeFunctionSignatureHelper(.List, FS) => encodeHexBytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) // Function parameters encoding rule encodeFunctionParams(ListItem(V:Value) ARGS:List, ListItem(T:String) PTYPES:List, B:Bytes) => encodeFunctionParams(ARGS:List, PTYPES:List, B:Bytes +Bytes convertToKBytes(V, T)) rule encodeFunctionParams(.List, .List, B:Bytes) => B - - - // Encoding of individual types - - rule convertToKBytes(i8(V) , "int8") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i16(V), "int16") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u16(V), "uint16") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i32(V), "int32") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u32(V), "uint32") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i64(V), "int64") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u64(V), "uint64") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u128(V), "uint128") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(true, "bool") => Int2Bytes(32, 1, BE:Endianness) - rule convertToKBytes(false, "bool") => Int2Bytes(32, 0, BE:Endianness) - rule convertToKBytes(u256(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u160(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u160(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - endmodule ``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index 19ce51a..0f6af3f 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -4,24 +4,28 @@ module UKM-ENCODING-SYNTAX imports BYTES-SYNTAX imports LIST imports RUST-REPRESENTATION - imports UKM-REPRESENTATION syntax UKMInstruction ::= "ukmEncodePreprocessedCell" | ukmEncodedPreprocessedCell(Bytes) + // TODO: Make these functions total and returning BytesOrError + syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list + | encodeFunctionSignature (String, List) [function] + | encodeFunctionSignatureHelper (List, String) [function] + | encodeFunctionParams (List, List, Bytes) [function] + syntax BytesOrError ::= encodeFunctionSignatureAsBytes(StringOrError) [function, total] - syntax Bytes ::= encodeHexBytes(String) [function, total] endmodule -module UKM-ENCODING-TESTING-SYNTAX +module UKM-ENCODING-HELPER-SYNTAX imports BYTES-SYNTAX imports LIST imports RUST-REPRESENTATION + imports UKM-REPRESENTATION - syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list - | encodeFunctionSignature (String, List, String) [function] - | encodeFunctionParams (List, List, Bytes) [function] + // TODO: Make convertToKBytes total + syntax Bytes ::= encodeHexBytes(String) [function, total] | convertToKBytes ( Value , String ) [function] endmodule diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index 6656b75..b0e2281 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ukm-semantics/targets/testing/ukm-target.md @@ -19,7 +19,7 @@ module UKM-TARGET imports private RUST-COMMON imports private RUST-FULL-PREPROCESSING imports private RUST-EXECUTION-TEST - imports private UKM-CALLDATA-ENCODER-TEST + imports private UKM-CALLDATA-ENCODER imports private UKM-EXECUTION imports private UKM-ENCODING imports private UKM-PREPROCESSING diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index e003961..b0f0d3b 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -49,7 +49,6 @@ module UKM-TEST-EXECUTION imports private RUST-EXECUTION-TEST-CONFIGURATION imports private RUST-SHARED-SYNTAX imports private UKM-ENCODING-SYNTAX - imports private UKM-ENCODING-TESTING-SYNTAX imports private UKM-EXECUTION-SYNTAX imports private UKM-HOOKS-BYTES-CONFIGURATION imports private UKM-HOOKS-HELPERS-SYNTAX