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..1e5b67f 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,39 @@ $(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 \ + $$(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' \ ${PLUGIN_FLAGS} \ --emit-json -o $(UKM_TESTING_KOMPILED) \ -I . \ + -I deps/blockchain-k-plugin \ -I kllvm \ --debug diff --git a/deps/blockchain-k-plugin b/deps/blockchain-k-plugin new file mode 160000 index 0000000..e6994c2 --- /dev/null +++ b/deps/blockchain-k-plugin @@ -0,0 +1 @@ +Subproject commit e6994c21c59dd2d15ddb97d5169d78aa6645a8fb diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs index 5620de9..6bc9ec5 100644 --- a/tests/ukm-contracts/bytes_hooks.rs +++ b/tests/ukm-contracts/bytes_hooks.rs @@ -21,5 +21,6 @@ extern "C" { fn decode_u8(bytes_id: u64) -> (u64, u8); fn decode_str(bytes_id: u64) -> (u64, str); + fn decode_signature(bytes_id: u64) -> (u64, str); fn hash(bytes_id: u64) -> u64; } 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..66bd396 --- /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; +encode_call_data_to_string; +return_value; +check_eq "81922854\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" \ No newline at end of file diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ukm-with-contract/erc_20_token.1.run index 21b01e3..6bb77ac 100644 --- a/tests/ukm-with-contract/erc_20_token.1.run +++ b/tests/ukm-with-contract/erc_20_token.1.run @@ -21,13 +21,15 @@ 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; +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 +51,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 +75,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 +104,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 +128,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 +152,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 +181,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 +213,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 +238,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..8eb6705 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; +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..8f88731 --- /dev/null +++ b/ukm-semantics/main/encoding/encoder.md @@ -0,0 +1,69 @@ +```k +requires "plugin/krypto.md" + +module UKM-CALLDATA-ENCODER + imports private COMMON-K-CELL + imports private UKM-ENCODING-SYNTAX + imports private UKM-PREPROCESSING-ENDPOINTS + imports STRING + imports BYTES + imports INT + imports KRYPTO + + // TODO: Properly encode the call data. Currently, we are returning the + // representation of the encoded function signature from a string using + // two characters to represent a byte in hexadecimal. We need to return the + // correct four bytes representation of signature. + // 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"") + + // Function signature encoding + rule encodeFunctionSignature(FuncName:String, RL:List) => + encodeFunctionSignatureHelper(RL:List, FuncName +String "(") [priority(40)] + + 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 encodeFunctionSignatureHelper(ListItem(FuncParam:String) .List, FS) => + encodeFunctionSignatureHelper(.List, FS +String FuncParam ) + + rule encodeFunctionSignatureHelper(.List, FS) => String2Bytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) + + // TODO: Implement helper functions and break down encodeFunctionSignatureAsString + // into smaller productions. Trigger errors for each of the + // possible functions which can be failure causes. + rule encodeFunctionSignatureAsString(FS) => substrString(Keccak256(String2Bytes(FS)), 0, 8) + rule encodeFunctionSignatureAsString(FS) => error("Failed to apply the Keccak256 of function signature.", FS) [owise] + + // 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..2fb33bb 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -2,9 +2,19 @@ module UKM-ENCODING-SYNTAX imports BYTES-SYNTAX + imports LIST + imports RUST-REPRESENTATION syntax UKMInstruction ::= "ukmEncodePreprocessedCell" + 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] + | convertToKBytes ( Value , String ) [function] + + syntax StringOrError ::= encodeFunctionSignatureAsString(StringOrError) [function, total] + endmodule ``` diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md index e024361..3ce1ae9 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ukm-semantics/main/hooks/bytes.md @@ -51,6 +51,7 @@ module UKM-HOOKS-BYTES | "decode_u8" [token] | "decode_str" [token] | "hash" [token] + | "decode_signature" [token] rule @@ -144,49 +145,49 @@ module UKM-HOOKS-BYTES ( :: bytes_hooks :: decode_u256 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u256) + => ukmBytesDecodeWithLength(BufferIdId, u256, 32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u160 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u160) + => ukmBytesDecodeWithLength(BufferIdId, u160, 32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u128 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u128) + => ukmBytesDecodeWithLength(BufferIdId, u128, 32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u64 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u64) + => ukmBytesDecodeWithLength(BufferIdId, u64, 32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u32 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u32) + => ukmBytesDecodeWithLength(BufferIdId, u32, 32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u16 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u16) + => ukmBytesDecodeWithLength(BufferIdId, u16, 32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u8 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u8) + => ukmBytesDecodeWithLength(BufferIdId, u8, 32) rule normalizedFunctionCall @@ -195,13 +196,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 + ) + => ukmBytesDecodeWithLength(BufferIdId, str, 8) // --------------------------------------- rule @@ -224,6 +231,8 @@ module UKM-HOOKS-BYTES | ukmBytesAppendLenAndBytes(Bytes, Bytes) | ukmBytesDecode(Expression, Type) [strict(1)] | ukmBytesDecode(UkmExpression, Type) [strict(1)] + | ukmBytesDecodeWithLength(Expression, Type, Int) [strict(1)] + | ukmBytesDecodeWithLength(UkmExpression, Type, Int) [strict(1)] | ukmBytesDecode(Int, Bytes, Type) | ukmBytesDecodeInt(Int, Bytes, Type) | ukmBytesDecode(ValueOrError, Bytes) @@ -282,6 +291,18 @@ module UKM-HOOKS-BYTES => ukmBytesNew(First +Bytes Int2Bytes(2, lengthBytes(Second), BE) +Bytes Second) requires lengthBytes(Second) ukmBytesDecodeWithLength(ukmBytesId(BytesId), T:Type, L:Int) + rule ukmBytesDecodeWithLength(ukmBytesValue(B:Bytes), T:Type, L:Int) + => ukmBytesDecode + ( L + , B + , T:Type + ) + requires L <=Int lengthBytes(B) + rule ukmBytesDecodeWithLength(ukmBytesValue(B:Bytes), T:Type, _:Int) + => ukmBytesDecode(ukmBytesValue(B), T) [owise] + rule ukmBytesDecode(ptrValue(_, u64(BytesId)), T:Type) => ukmBytesDecode(ukmBytesId(BytesId), T:Type) rule ukmBytesDecode(ukmBytesValue(B:Bytes), T:Type) diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index f567980..034a0b6 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -9,6 +9,7 @@ module UKM-PREPROCESSING-ENDPOINTS imports private UKM-COMMON-TOOLS-SYNTAX imports private UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + imports private UKM-ENCODING-SYNTAX rule @@ -163,6 +164,7 @@ module UKM-PREPROCESSING-ENDPOINTS | "decode_u160" [token] | "decode_u256" [token] | "decode_str" [token] + | "decode_signature" [token] | "empty" [token] | "ukm" [token] | "CallData" [token] @@ -174,7 +176,7 @@ module UKM-PREPROCESSING-ENDPOINTS | signatureType(Type) [function, total] rule methodSignature(S:String, Ps:NormalizedFunctionParameterList) - => concat(concat(S +String "(", signatureTypes(Ps)), ")") + => encodeFunctionSignatureAsString(concat(concat(S +String "(", signatureTypes(Ps)), ")")) rule signatureTypes(.NormalizedFunctionParameterList) => "" rule signatureTypes(_ : T:Type , .NormalizedFunctionParameterList) @@ -186,13 +188,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] @@ -231,7 +233,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/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index 1321ddc..b2f1f70 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" @@ -19,6 +20,7 @@ module UKM-TARGET imports private RUST-FULL-PREPROCESSING imports private RUST-EXECUTION-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..b6e4f1a 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -2,17 +2,35 @@ module UKM-TEST-SYNTAX imports INT-SYNTAX + imports STRING-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX imports UKM-HOOKS-UKM-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] + | "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" + | "encode_call_data_to_string" | "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] @@ -27,6 +45,7 @@ endmodule module UKM-TEST-EXECUTION imports private COMMON-K-CELL imports private RUST-EXECUTION-TEST-CONFIGURATION + imports private UKM-ENCODING-SYNTAX imports private UKM-EXECUTION-SYNTAX imports private UKM-HOOKS-BYTES-CONFIGURATION imports private UKM-HOOKS-BYTES-SYNTAX @@ -34,9 +53,61 @@ module UKM-TEST-EXECUTION imports private UKM-HOOKS-STATE-CONFIGURATION imports private UKM-HOOKS-UKM-SYNTAX imports private UKM-TEST-SYNTAX + imports RUST-SHARED-SYNTAX + imports private BYTES 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 ... + + + // TODO: Rework the implementation of the productions related to list value holding + // Ref - https://github.com/Pi-Squared-Inc/rust-demo-semantics/pull/167#discussion_r1813386536 + 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 encode_call_data_to_string + ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList + => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) + ... + + + rule encode_call_data_to_string + ~> 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) ...