From fe926fa28e2cddbd3db79452c4659424dcd851c2 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Wed, 16 Oct 2024 23:34:34 -0300 Subject: [PATCH 01/17] Adding encoding capabilities --- .gitignore | 1 + .gitmodules | 3 ++ Makefile | 12 +++-- blockchain-k-plugin | 1 + tests/ukm-with-contract/endpoints.2.run | 9 ++++ ukm-semantics/main/encoding.md | 2 + ukm-semantics/main/encoding/encoder.md | 57 +++++++++++++++++++++ ukm-semantics/main/encoding/syntax.md | 10 ++++ ukm-semantics/targets/testing/ukm-target.md | 2 + ukm-semantics/test/execution.md | 47 ++++++++++++++++- 10 files changed, 139 insertions(+), 5 deletions(-) create mode 100644 .gitmodules create mode 160000 blockchain-k-plugin 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 new file mode 100644 index 0000000..067a670 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "blockchain-k-plugin"] + path = blockchain-k-plugin + url = https://github.com/runtimeverification/blockchain-k-plugin diff --git a/Makefile b/Makefile index 28e672a..709910f 100644 --- a/Makefile +++ b/Makefile @@ -184,7 +184,9 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTI $(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) # 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 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ --emit-json -o $(UKM_EXECUTION_KOMPILED) \ -I . \ --debug @@ -192,7 +194,9 @@ $(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) # 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 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ --emit-json -o $(UKM_PREPROCESSING_KOMPILED) \ -I . \ --debug @@ -200,7 +204,9 @@ $(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) # 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 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ --emit-json -o $(UKM_TESTING_KOMPILED) \ -I . \ --debug diff --git a/blockchain-k-plugin b/blockchain-k-plugin new file mode 160000 index 0000000..e6994c2 --- /dev/null +++ b/blockchain-k-plugin @@ -0,0 +1 @@ +Subproject commit e6994c21c59dd2d15ddb97d5169d78aa6645a8fb diff --git a/tests/ukm-with-contract/endpoints.2.run b/tests/ukm-with-contract/endpoints.2.run new file mode 100644 index 0000000..441167e --- /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 Encode; +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\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\x00\x01" \ 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..2fb92b4 --- /dev/null +++ b/ukm-semantics/main/encoding/encoder.md @@ -0,0 +1,57 @@ +```k +requires "blockchain-k-plugin/plugin/krypto.md" + +module UKM-CALLDATA-ENCODER + imports private COMMON-K-CELL + imports private UKM-ENCODING-SYNTAX + imports STRING + imports BYTES + imports INT + imports KRYPTO + + // EncodeCallData must map to something that receives two bytes (and has seqstrict). It evaluates the + // params and, once evaluated, concatenate the two. + 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 "(") + + 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) => String2Bytes(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(8, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(8, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i16(V), "int16") => Int2Bytes(16, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u16(V), "uint16") => Int2Bytes(16, 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(64, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint64") => Int2Bytes(64, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u128(V), "uint128") => Int2Bytes(128, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(true, "bool") => Int2Bytes(8, 1, BE:Endianness) + rule convertToKBytes(false, "bool") => Int2Bytes(8, 0, BE:Endianness) + // TODO: as we currently do not support u160 (addresses) or u256, we're converting them to u64 for now + rule convertToKBytes(u64(V), "uint256") => Int2Bytes(256, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint160") => Int2Bytes(160, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u64(V), "address") => Int2Bytes(160, 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..3959972 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-VALUE-SYNTAX syntax UKMInstruction ::= "ukmEncodePreprocessedCell" + // syntax Bytes ::= (CodingOperations, CodingOperations) [function, seqstrict] + + syntax KItem ::= "CodingOperations" + 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/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 de0d56c..a3a35c1 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -2,28 +2,71 @@ module UKM-TEST-SYNTAX imports INT-SYNTAX + imports STRING-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX - syntax ExecutionItem ::= "mock" "CallData" - | "mock" "Caller" + syntax UKMTestTypeHolder ::= "ptr_holder" KItem [strict] + | "value_holder" Value + | "list_ptrs_holder" List + | "list_values_holder" List + + syntax UKMTestTypeHolderList ::= List{UKMTestTypeHolder, ","} + + syntax UKMMockOperations ::= "Caller" + | "CallData" + | "Encode" + + syntax ExecutionItem ::= "mock" UKMMockOperations | "call_contract" Int | "output_to_arg" | "push_status" | "check_eq" Int + | "hold_string_from_test_stack" + | "hold_list_values_from_test_stack" 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 imports private UKM-HOOKS-STATE-CONFIGURATION imports private UKM-HOOKS-UKM-SYNTAX imports private UKM-TEST-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 ... + + 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 mock Encode + ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList + => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) + ... + + rule mock CallData => mock(CallDataHook(), V) ... From c1cb9a34d3bd82a89147a3851af113c307f6f853 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Fri, 18 Oct 2024 02:02:59 -0300 Subject: [PATCH 02/17] Enabling encoding of endpoints at preprocessing stage --- tests/ukm-with-contract/endpoints.1.run | 2 +- ukm-semantics/main/decoding.md | 2 ++ ukm-semantics/main/decoding/decoder.md | 23 +++++++++++++++++++ ukm-semantics/main/decoding/syntax.md | 5 ++++ ukm-semantics/main/encoding/encoder.md | 22 ++++++++++++++++-- ukm-semantics/main/encoding/syntax.md | 8 ++++--- .../main/preprocessing/configuration.md | 3 +++ ukm-semantics/main/preprocessing/endpoints.md | 8 +++---- ukm-semantics/main/preprocessing/methods.md | 17 +++++++++++++- ukm-semantics/main/preprocessing/syntax.md | 3 +++ ukm-semantics/targets/testing/ukm-target.md | 2 ++ ukm-semantics/test/execution.md | 17 +++++++++----- 12 files changed, 95 insertions(+), 17 deletions(-) create mode 100644 ukm-semantics/main/decoding/decoder.md diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run index 4264f65..b218224 100644 --- a/tests/ukm-with-contract/endpoints.1.run +++ b/tests/ukm-with-contract/endpoints.1.run @@ -1,6 +1,6 @@ call :: bytes_hooks :: empty; return_value_to_arg; -push "myEndpoint(Uint64)"; +push "myEndpoint(uint64)"; call :: bytes_hooks :: append_str; return_value_to_arg; push 123_u64; diff --git a/ukm-semantics/main/decoding.md b/ukm-semantics/main/decoding.md index 3561da2..bc60913 100644 --- a/ukm-semantics/main/decoding.md +++ b/ukm-semantics/main/decoding.md @@ -1,8 +1,10 @@ ```k requires "decoding/syntax.md" +requires "decoding/decoder.md" module UKM-DECODING + imports UKM-CALLDATA-DECODER endmodule ``` diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md new file mode 100644 index 0000000..d9e6373 --- /dev/null +++ b/ukm-semantics/main/decoding/decoder.md @@ -0,0 +1,23 @@ +```k + +module UKM-CALLDATA-DECODER + imports RUST-VALUE-SYNTAX + imports UKM-DECODING-SYNTAX + imports BYTES-HOOKED + imports BYTES-SYNTAX + imports INT + + // Convert the bytes to integer and do a bit shifting operation to get the values + rule decodeCallData(D:Bytes) => + substrBytes(D, 0, 8) + + // Int2Bytes(64:Int, + // (Bytes2Int(D:Bytes, BE:Endianness, Unsigned:Signedness) >>Int (lengthBytes(D) -Int 4)):Int, + // BE:Endianness) + // (Bytes2Int(D:Bytes, BE:Endianness, Unsigned:Signedness) + // ( Int2Bytes(D[0]) +Bytes Int2Bytes(D[1]) +Bytes Int2Bytes(D[2]) +Bytes Int2Bytes(D[3]), decodeCallDataArguments(D:Bytes)) + + + +endmodule +``` \ No newline at end of file diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md index 7fa88fc..9b23ca8 100644 --- a/ukm-semantics/main/decoding/syntax.md +++ b/ukm-semantics/main/decoding/syntax.md @@ -2,9 +2,14 @@ module UKM-DECODING-SYNTAX imports BYTES-SYNTAX + imports LIST + imports RUST-VALUE-SYNTAX syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes) + syntax KItem ::= decodeCallData(Bytes) [function] + | decodeCallDataArguments(Bytes) [function] + endmodule ``` diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index 2fb92b4..1e7c1a4 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -4,13 +4,31 @@ requires "blockchain-k-plugin/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 - // EncodeCallData must map to something that receives two bytes (and has seqstrict). It evaluates the - // params and, once evaluated, concatenate the two. + syntax String ::= Identifier2String(Identifier) [function, total, hook(STRING.token2string)] + | Type2String(Type) [function, total, hook(STRING.token2string)] + + rule encodeFunctionSignature (P:PathInExpression, N:NormalizedFunctionParameterList) => + encodeFunctionSignature(convertPathInExprToString(P), convertFuncParamListToStrList(N, .List), "") + + rule convertPathInExprToString(( :: I:Identifier :: R:PathExprSegments):PathInExpression ) => + convertPathInExprToString(R) [priority(80)] + rule convertPathInExprToString(( I:Identifier :: R:PathExprSegments):PathInExpression ) => + convertPathInExprToString(R) [priority(80)] + rule convertPathInExprToString(( I:Identifier :: .PathExprSegments):PathInExpression ) => + Identifier2String(I) [priority(70)] + + rule convertFuncParamListToStrList(((self : _), N:NormalizedFunctionParameterList), .List) => + convertFuncParamListToStrList( N, .List) [priority(60)] + rule convertFuncParamListToStrList(((_ : T:Type), N:NormalizedFunctionParameterList), L:List) => + convertFuncParamListToStrList(N, L ListItem(signatureType(T))) [priority(70)] + rule convertFuncParamListToStrList(.NormalizedFunctionParameterList, L:List) => L + rule encodeCallData(FN:String, FAT:List, FAL:List) => encodeFunctionSignature(FN, FAT, "") +Bytes encodeFunctionParams(FAL, FAT, b"") diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index 3959972..ef8a278 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -3,13 +3,15 @@ module UKM-ENCODING-SYNTAX imports BYTES-SYNTAX imports LIST - imports RUST-VALUE-SYNTAX + imports RUST-REPRESENTATION syntax UKMInstruction ::= "ukmEncodePreprocessedCell" + + syntax Bytes ::= encodeFunctionSignature (PathInExpression, NormalizedFunctionParameterList) [function] - // syntax Bytes ::= (CodingOperations, CodingOperations) [function, seqstrict] + syntax String ::= convertPathInExprToString(PathInExpression) [function] + syntax List ::= convertFuncParamListToStrList(NormalizedFunctionParameterList, List) [function] - syntax KItem ::= "CodingOperations" syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list | encodeFunctionSignature (String, List, String) [function] | encodeFunctionParams (List, List, Bytes) [function] diff --git a/ukm-semantics/main/preprocessing/configuration.md b/ukm-semantics/main/preprocessing/configuration.md index 9302083..ecdf7ac 100644 --- a/ukm-semantics/main/preprocessing/configuration.md +++ b/ukm-semantics/main/preprocessing/configuration.md @@ -8,6 +8,9 @@ module UKM-PREPROCESSING-CONFIGURATION (#token("not#initialized", "Identifier"):Identifier):TypePath + + .Map + endmodule diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index 33accc4..b69e1d9 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -180,10 +180,10 @@ 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(u8) => "uint8" + rule signatureType(u16) => "uint16" + rule signatureType(u32) => "uint32" + rule signatureType(u64) => "uint64" rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T)) [owise] diff --git a/ukm-semantics/main/preprocessing/methods.md b/ukm-semantics/main/preprocessing/methods.md index 4a27f90..1972940 100644 --- a/ukm-semantics/main/preprocessing/methods.md +++ b/ukm-semantics/main/preprocessing/methods.md @@ -5,7 +5,22 @@ module UKM-PREPROCESSING-METHODS imports private K-EQUAL-SYNTAX imports private RUST-CONVERSIONS-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION + imports private UKM-PREPROCESSING-CONFIGURATION imports private UKM-PREPROCESSING-SYNTAX-PRIVATE + imports private UKM-ENCODING-SYNTAX + + rule + ukmPreprocessMethodSignature(Method) => ukmPreprocessingStoreMethodSignature(encodeFunctionSignature(Method, L), Method) + ... + + Method + L:NormalizedFunctionParameterList + + rule ukmPreprocessingStoreMethodSignature(B:Bytes, P:PathInExpression) => .K ... + + STATE => STATE [ B <- P ] + + rule ukmPreprocessMethods(_:TypePath, .List) => .K rule ukmPreprocessMethods(Trait:TypePath, ListItem(Name:Identifier) Methods:List) @@ -20,7 +35,7 @@ module UKM-PREPROCESSING-METHODS , method: MethodIdentifier , fullMethodPath: Method , endpointName: getEndpointName(Atts, MethodIdentifier) - ) + ) ~> ukmPreprocessMethodSignature(Method) ... Method diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md index eeb8a62..4ca5e50 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ukm-semantics/main/preprocessing/syntax.md @@ -10,11 +10,14 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE imports LIST imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX + imports private BYTES-SYNTAX syntax UKMInstruction ::= ukmPreprocessTraits(List) | ukmPreprocessTrait(TypePath) | ukmPreprocessMethods(trait: TypePath, List) | ukmPreprocessMethod(trait: TypePath, methodId: Identifier, fullMethodPath: PathInExpression) + | ukmPreprocessMethodSignature(PathInExpression) + | ukmPreprocessingStoreMethodSignature(Bytes, PathInExpression) | ukmPreprocessEndpoint ( trait: TypePath , method: Identifier diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index b2f1f70..e21bc7f 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ukm-semantics/targets/testing/ukm-target.md @@ -1,6 +1,7 @@ ```k requires "../../main/encoding.md" +requires "../../main/decoding.md" requires "../../main/execution.md" requires "../../main/preprocessing.md" requires "../../test/execution.md" @@ -21,6 +22,7 @@ module UKM-TARGET imports private RUST-EXECUTION-TEST imports private UKM-EXECUTION imports private UKM-ENCODING + imports private UKM-DECODING 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 a3a35c1..6bcca59 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -12,11 +12,10 @@ module UKM-TEST-SYNTAX syntax UKMTestTypeHolderList ::= List{UKMTestTypeHolder, ","} - syntax UKMMockOperations ::= "Caller" - | "CallData" - | "Encode" - - syntax ExecutionItem ::= "mock" UKMMockOperations + syntax ExecutionItem ::= "mock" "Caller" + | "mock" "CallData" + | "mock" "EncodeOp" + | "mock" "DecodeOp" | "call_contract" Int | "output_to_arg" | "push_status" @@ -29,6 +28,7 @@ module UKM-TEST-EXECUTION imports private COMMON-K-CELL imports private RUST-EXECUTION-TEST-CONFIGURATION imports private UKM-ENCODING-SYNTAX + imports private UKM-DECODING-SYNTAX imports private UKM-EXECUTION-SYNTAX imports private UKM-HOOKS-BYTES-CONFIGURATION imports private UKM-HOOKS-BYTES-SYNTAX @@ -61,12 +61,17 @@ module UKM-TEST-EXECUTION rule list_ptrs_holder .List => .K ... - rule mock Encode + rule mock EncodeOp ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) ... + rule mock DecodeOp ~> value_holder CALLDATASTRING => + decodeCallData(String2Bytes(CALLDATASTRING)) + ... + + rule mock CallData => mock(CallDataHook(), V) ... From 0be89749cffc07eb0e32ef59a8d0a9262ce8288a Mon Sep 17 00:00:00 2001 From: acassimiro Date: Sat, 19 Oct 2024 16:56:39 -0300 Subject: [PATCH 03/17] Enabling call data arguments decoding --- tests/ukm-with-contract/endpoints.2.run | 2 +- tests/ukm-with-contract/endpoints.3.run | 3 ++ ukm-semantics/main/decoding/decoder.md | 45 +++++++++++++++---- ukm-semantics/main/decoding/syntax.md | 17 ++++++- .../main/preprocessing/configuration.md | 4 +- ukm-semantics/main/preprocessing/methods.md | 4 +- ukm-semantics/test/execution.md | 11 ++--- 7 files changed, 66 insertions(+), 20 deletions(-) create mode 100644 tests/ukm-with-contract/endpoints.3.run diff --git a/tests/ukm-with-contract/endpoints.2.run b/tests/ukm-with-contract/endpoints.2.run index 441167e..5a29b84 100644 --- a/tests/ukm-with-contract/endpoints.2.run +++ b/tests/ukm-with-contract/endpoints.2.run @@ -4,6 +4,6 @@ push "uint64"; hold_list_values_from_test_stack; push 1_u64; hold_list_values_from_test_stack; -mock Encode; +mock EncodeOp; 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\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\x00\x01" \ No newline at end of file diff --git a/tests/ukm-with-contract/endpoints.3.run b/tests/ukm-with-contract/endpoints.3.run new file mode 100644 index 0000000..1f25c27 --- /dev/null +++ b/tests/ukm-with-contract/endpoints.3.run @@ -0,0 +1,3 @@ +hold b"c6b6e179\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\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\x00\x01"; +mock DecodeOp; +return_value \ No newline at end of file diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md index d9e6373..d2f1b83 100644 --- a/ukm-semantics/main/decoding/decoder.md +++ b/ukm-semantics/main/decoding/decoder.md @@ -5,19 +5,48 @@ module UKM-CALLDATA-DECODER imports UKM-DECODING-SYNTAX imports BYTES-HOOKED imports BYTES-SYNTAX + imports private COMMON-K-CELL + imports private RUST-PREPROCESSING-CONFIGURATION + imports private UKM-PREPROCESSING-CONFIGURATION + imports private RUST-REPRESENTATION imports INT - // Convert the bytes to integer and do a bit shifting operation to get the values - rule decodeCallData(D:Bytes) => - substrBytes(D, 0, 8) + rule decodeCallData(D:Bytes) => + // ( + // decodeFunctionSignature(substrBytes(D, 0, 8)) , + decodeArguments(loadArgumentsFromHash(substrBytes(D, 0, 8)), substrBytes(D, 8, lengthBytes(D)), .List) + // ): TupleExpression + + rule [[ decodeFunctionSignature(FuncSigHash:Bytes) => P ]] + + ... FuncSigHash |-> P:PathInExpression ... + + + rule [[ loadArgumentsFromHash(FuncSigHash:Bytes) => loadArgumentsFromHash(P) ]] + + ... FuncSigHash |-> P:PathInExpression ... + + + rule [[ loadArgumentsFromHash(Method:PathInExpression) => L ]] + Method + (self : $selftype), L:NormalizedFunctionParameterList - // Int2Bytes(64:Int, - // (Bytes2Int(D:Bytes, BE:Endianness, Unsigned:Signedness) >>Int (lengthBytes(D) -Int 4)):Int, - // BE:Endianness) - // (Bytes2Int(D:Bytes, BE:Endianness, Unsigned:Signedness) - // ( Int2Bytes(D[0]) +Bytes Int2Bytes(D[1]) +Bytes Int2Bytes(D[2]) +Bytes Int2Bytes(D[3]), decodeCallDataArguments(D:Bytes)) + rule decodeArguments(((_ : T:Type), R):NormalizedFunctionParameterList, D:Bytes, L:List) => + decodeArguments(R, substrBytes(D, 0, sizeOfType(T)), + convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, sizeOfType(T)), BE, Unsigned ) ) , L ) + rule decodeArguments(.NormalizedFunctionParameterList, _, L:List) => L + rule convertKBytesToPtrValue(u32, I:Int) => ptrValue(null, u32(Int2MInt(I))) + rule convertKBytesToPtrValue(i32, I:Int) => ptrValue(null, i32(Int2MInt(I))) + rule convertKBytesToPtrValue(i64, I:Int) => ptrValue(null, i64(Int2MInt(I))) + rule convertKBytesToPtrValue(u64, I:Int) => ptrValue(null, u64(Int2MInt(I))) + rule convertKBytesToPtrValue(u128, I:Int) => ptrValue(null, u128(Int2MInt(I))) + rule sizeOfType(i32) => 32 + rule sizeOfType(u32) => 32 + rule sizeOfType(u64) => 64 + rule sizeOfType(i64) => 64 + rule sizeOfType(u128) => 128 endmodule ``` \ No newline at end of file diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md index 9b23ca8..e9c1cd8 100644 --- a/ukm-semantics/main/decoding/syntax.md +++ b/ukm-semantics/main/decoding/syntax.md @@ -2,13 +2,26 @@ module UKM-DECODING-SYNTAX imports BYTES-SYNTAX + imports INT-SYNTAX imports LIST imports RUST-VALUE-SYNTAX + imports private RUST-REPRESENTATION syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes) + //c6b6e1790000000000000000000000000000000000000000000000000000000000000001 + syntax NormalizedFunctionParameterList ::= loadArgumentsFromHash(Bytes) [function] + | loadArgumentsFromHash(PathInExpression) [function] + + syntax KItem ::= decodeCallDataArguments(Bytes) [function] + | decodeCallData(Bytes) [function] + | decodeArguments(NormalizedFunctionParameterList, Bytes, List) [function] + + syntax PathInExpression ::= decodeFunctionSignature(Bytes) [function] + + syntax PtrValue ::= convertKBytesToPtrValue(Type, Int) [function] + + syntax Int ::= sizeOfType(Type) [function] - syntax KItem ::= decodeCallData(Bytes) [function] - | decodeCallDataArguments(Bytes) [function] endmodule diff --git a/ukm-semantics/main/preprocessing/configuration.md b/ukm-semantics/main/preprocessing/configuration.md index ecdf7ac..9484412 100644 --- a/ukm-semantics/main/preprocessing/configuration.md +++ b/ukm-semantics/main/preprocessing/configuration.md @@ -8,9 +8,9 @@ module UKM-PREPROCESSING-CONFIGURATION (#token("not#initialized", "Identifier"):Identifier):TypePath - + .Map - + endmodule diff --git a/ukm-semantics/main/preprocessing/methods.md b/ukm-semantics/main/preprocessing/methods.md index 1972940..0515a5e 100644 --- a/ukm-semantics/main/preprocessing/methods.md +++ b/ukm-semantics/main/preprocessing/methods.md @@ -17,9 +17,9 @@ module UKM-PREPROCESSING-METHODS L:NormalizedFunctionParameterList rule ukmPreprocessingStoreMethodSignature(B:Bytes, P:PathInExpression) => .K ... - + STATE => STATE [ B <- P ] - + rule ukmPreprocessMethods(_:TypePath, .List) => .K diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index 6bcca59..25913dc 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -4,9 +4,10 @@ module UKM-TEST-SYNTAX imports INT-SYNTAX imports STRING-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX + imports BYTES-SYNTAX syntax UKMTestTypeHolder ::= "ptr_holder" KItem [strict] - | "value_holder" Value + | "value_holder" KItem | "list_ptrs_holder" List | "list_values_holder" List @@ -17,6 +18,7 @@ module UKM-TEST-SYNTAX | "mock" "EncodeOp" | "mock" "DecodeOp" | "call_contract" Int + | "hold" KItem | "output_to_arg" | "push_status" | "check_eq" Int @@ -35,6 +37,7 @@ 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 @@ -60,6 +63,7 @@ module UKM-TEST-EXECUTION => list_ptrs_holder LPH ~> list_values_holder ListItem(V) LLH ... rule list_ptrs_holder .List => .K ... + rule hold I => value_holder I ... rule mock EncodeOp ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList @@ -67,10 +71,7 @@ module UKM-TEST-EXECUTION ... - rule mock DecodeOp ~> value_holder CALLDATASTRING => - decodeCallData(String2Bytes(CALLDATASTRING)) - ... - + rule mock DecodeOp ~> value_holder B:Bytes => decodeCallData(B) ... rule mock CallData => mock(CallDataHook(), V) ... From f1b24dcd9e4e3480224fb86dd37a30c0aa30889c Mon Sep 17 00:00:00 2001 From: acassimiro Date: Sat, 19 Oct 2024 23:38:38 -0300 Subject: [PATCH 04/17] Fixing minor issue with decoding arguments --- ukm-semantics/main/decoding/decoder.md | 2 +- ukm-semantics/main/decoding/syntax.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md index d2f1b83..1093bd8 100644 --- a/ukm-semantics/main/decoding/decoder.md +++ b/ukm-semantics/main/decoding/decoder.md @@ -33,7 +33,7 @@ module UKM-CALLDATA-DECODER rule decodeArguments(((_ : T:Type), R):NormalizedFunctionParameterList, D:Bytes, L:List) => decodeArguments(R, substrBytes(D, 0, sizeOfType(T)), - convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, sizeOfType(T)), BE, Unsigned ) ) , L ) + ListItem(convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, sizeOfType(T)), BE, Unsigned ) ) ) L ) rule decodeArguments(.NormalizedFunctionParameterList, _, L:List) => L diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md index e9c1cd8..0e00a21 100644 --- a/ukm-semantics/main/decoding/syntax.md +++ b/ukm-semantics/main/decoding/syntax.md @@ -8,7 +8,7 @@ module UKM-DECODING-SYNTAX imports private RUST-REPRESENTATION syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes) - //c6b6e1790000000000000000000000000000000000000000000000000000000000000001 + syntax NormalizedFunctionParameterList ::= loadArgumentsFromHash(Bytes) [function] | loadArgumentsFromHash(PathInExpression) [function] @@ -25,4 +25,4 @@ module UKM-DECODING-SYNTAX endmodule -``` +``` \ No newline at end of file From 580676d0e1a5e32b003bab96f3670babf890c508 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Sun, 20 Oct 2024 12:49:10 -0300 Subject: [PATCH 05/17] Properly returning an object representing the decoded call data --- ukm-semantics/main/decoding/decoder.md | 7 ++----- ukm-semantics/main/decoding/syntax.md | 8 ++++++-- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md index 1093bd8..6ab682e 100644 --- a/ukm-semantics/main/decoding/decoder.md +++ b/ukm-semantics/main/decoding/decoder.md @@ -12,11 +12,8 @@ module UKM-CALLDATA-DECODER imports INT rule decodeCallData(D:Bytes) => - // ( - // decodeFunctionSignature(substrBytes(D, 0, 8)) , - decodeArguments(loadArgumentsFromHash(substrBytes(D, 0, 8)), substrBytes(D, 8, lengthBytes(D)), .List) - // ): TupleExpression - + UKMDecodedCallArgs(decodeFunctionSignature(substrBytes(D, 0, 8)), decodeArguments(loadArgumentsFromHash(substrBytes(D, 0, 8)), substrBytes(D, 8, lengthBytes(D)), .List) ) + rule [[ decodeFunctionSignature(FuncSigHash:Bytes) => P ]] ... FuncSigHash |-> P:PathInExpression ... diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md index 0e00a21..44f47ff 100644 --- a/ukm-semantics/main/decoding/syntax.md +++ b/ukm-semantics/main/decoding/syntax.md @@ -7,15 +7,19 @@ module UKM-DECODING-SYNTAX imports RUST-VALUE-SYNTAX imports private RUST-REPRESENTATION + syntax UKMDecodedCallArguments ::= UKMDecodedCallArgs( PathInExpression , List ) //List + | decodeCallData(Bytes) [function] + syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes) syntax NormalizedFunctionParameterList ::= loadArgumentsFromHash(Bytes) [function] | loadArgumentsFromHash(PathInExpression) [function] - syntax KItem ::= decodeCallDataArguments(Bytes) [function] - | decodeCallData(Bytes) [function] + syntax List ::= decodeCallDataArguments(Bytes) [function] | decodeArguments(NormalizedFunctionParameterList, Bytes, List) [function] + + syntax PathInExpression ::= decodeFunctionSignature(Bytes) [function] syntax PtrValue ::= convertKBytesToPtrValue(Type, Int) [function] From 4175b9d5188ba1e0b533d3c138466414d90016af Mon Sep 17 00:00:00 2001 From: acassimiro Date: Sun, 20 Oct 2024 19:57:48 -0300 Subject: [PATCH 06/17] Enabling function calls from decoded call data --- tests/ukm-with-contract/endpoints.3.run | 4 +++- ukm-semantics/main/decoding/decoder.md | 30 +++++++++++++++++++++++-- ukm-semantics/main/decoding/syntax.md | 6 +++-- ukm-semantics/test/execution.md | 1 + 4 files changed, 36 insertions(+), 5 deletions(-) diff --git a/tests/ukm-with-contract/endpoints.3.run b/tests/ukm-with-contract/endpoints.3.run index 1f25c27..18493ed 100644 --- a/tests/ukm-with-contract/endpoints.3.run +++ b/tests/ukm-with-contract/endpoints.3.run @@ -1,3 +1,5 @@ hold b"c6b6e179\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\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\x00\x01"; mock DecodeOp; -return_value \ No newline at end of file +return_value; + +check_eq 3_u64 \ No newline at end of file diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md index 6ab682e..f01aa91 100644 --- a/ukm-semantics/main/decoding/decoder.md +++ b/ukm-semantics/main/decoding/decoder.md @@ -8,11 +8,37 @@ module UKM-CALLDATA-DECODER imports private COMMON-K-CELL imports private RUST-PREPROCESSING-CONFIGURATION imports private UKM-PREPROCESSING-CONFIGURATION + imports private RUST-EXECUTION-CONFIGURATION imports private RUST-REPRESENTATION + imports private RUST-CONVERSIONS-SYNTAX imports INT rule decodeCallData(D:Bytes) => - UKMDecodedCallArgs(decodeFunctionSignature(substrBytes(D, 0, 8)), decodeArguments(loadArgumentsFromHash(substrBytes(D, 0, 8)), substrBytes(D, 8, lengthBytes(D)), .List) ) + UKMDecodedCallData1(decodeFunctionSignature(substrBytes(D, 0, 8)), decodeArguments(loadArgumentsFromHash(substrBytes(D, 0, 8)), substrBytes(D, 8, lengthBytes(D)), .List) ) + + // TODO: Self is being assigned to an integer 0. This should be fixed in case we need + // to make references to self within rust contracts + rule UKMDecodedCallData1(P:PathInExpression, L:List) + => UKMDecodedCallData1(P, L) + ~> UKMDecodedCallData2(P, ListItem(NextId)) + ... + NextId:Int => NextId +Int 1 + Values:Map => Values[NextId <- u64(Int2MInt(0))] [priority(80)] + + + rule UKMDecodedCallData1(P:PathInExpression, L:List ListItem(ptrValue(_, V))) + ~> UKMDecodedCallData2(P:PathInExpression, PL:List) + => UKMDecodedCallData1(P, L) + ~> UKMDecodedCallData2(P, ListItem(NextId) PL) + ... + NextId:Int => NextId +Int 1 + Values:Map => Values[NextId <- V] [priority(70)] + + rule UKMDecodedCallData1(P:PathInExpression, .List) + => .K ... + + rule UKMDecodedCallData2(P:PathInExpression, L:List) + => UKMDecodedCallData(P:PathInExpression, listToPtrList(L)) ... rule [[ decodeFunctionSignature(FuncSigHash:Bytes) => P ]] @@ -30,7 +56,7 @@ module UKM-CALLDATA-DECODER rule decodeArguments(((_ : T:Type), R):NormalizedFunctionParameterList, D:Bytes, L:List) => decodeArguments(R, substrBytes(D, 0, sizeOfType(T)), - ListItem(convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, sizeOfType(T)), BE, Unsigned ) ) ) L ) + ListItem( convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, sizeOfType(T)), BE, Unsigned ) ) ) L ) rule decodeArguments(.NormalizedFunctionParameterList, _, L:List) => L diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md index 44f47ff..feb2f14 100644 --- a/ukm-semantics/main/decoding/syntax.md +++ b/ukm-semantics/main/decoding/syntax.md @@ -7,8 +7,10 @@ module UKM-DECODING-SYNTAX imports RUST-VALUE-SYNTAX imports private RUST-REPRESENTATION - syntax UKMDecodedCallArguments ::= UKMDecodedCallArgs( PathInExpression , List ) //List - | decodeCallData(Bytes) [function] + syntax UKMDecodedCallDataWrapper ::= UKMDecodedCallData1( PathInExpression , List ) + | UKMDecodedCallData2( PathInExpression , List ) + | UKMDecodedCallData ( PathInExpression , PtrListOrError) + | decodeCallData(Bytes) [function] syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes) diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index 25913dc..c1bf9d5 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -72,6 +72,7 @@ module UKM-TEST-EXECUTION rule mock DecodeOp ~> value_holder B:Bytes => decodeCallData(B) ... + rule UKMDecodedCallData(P:PathInExpression , L:PtrList) => normalizedFunctionCall(P, L) ... rule mock CallData => mock(CallDataHook(), V) ... From f3b27b133ef2d44b47b730a69bb578c903045f0a Mon Sep 17 00:00:00 2001 From: acassimiro Date: Tue, 22 Oct 2024 19:05:07 -0300 Subject: [PATCH 07/17] Modifying the decoding approach to comply with Ethereum's --- tests/ukm-contracts/bytes_hooks.rs | 2 + tests/ukm-with-contract/endpoints.1.run | 34 ++++++++--------- tests/ukm-with-contract/endpoints.2.run | 4 +- tests/ukm-with-contract/endpoints.3.run | 5 --- ukm-semantics/main/decoding/decoder.md | 12 ++---- ukm-semantics/main/encoding/encoder.md | 31 +++++++++------- ukm-semantics/main/encoding/syntax.md | 3 ++ ukm-semantics/main/hooks/bytes.md | 37 ++++++++++++++++--- ukm-semantics/main/preprocessing/endpoints.md | 20 +++++++++- ukm-semantics/main/preprocessing/methods.md | 16 +------- ukm-semantics/main/preprocessing/syntax.md | 4 +- ukm-semantics/test/execution.md | 15 +++++--- 12 files changed, 104 insertions(+), 79 deletions(-) delete mode 100644 tests/ukm-with-contract/endpoints.3.run diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs index ae8e34a..c21e098 100644 --- a/tests/ukm-contracts/bytes_hooks.rs +++ b/tests/ukm-contracts/bytes_hooks.rs @@ -16,4 +16,6 @@ extern "C" { 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, str); } diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run index b218224..f1d3a48 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; +mock EncodeCallData; + +return_value; +mock CallData; call_contract 12345; -return_value; +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 index 5a29b84..16a9489 100644 --- a/tests/ukm-with-contract/endpoints.2.run +++ b/tests/ukm-with-contract/endpoints.2.run @@ -4,6 +4,6 @@ push "uint64"; hold_list_values_from_test_stack; push 1_u64; hold_list_values_from_test_stack; -mock EncodeOp; +mock EncodeCallDataToString; 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\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\x00\x01" \ No newline at end of file +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/endpoints.3.run b/tests/ukm-with-contract/endpoints.3.run deleted file mode 100644 index 18493ed..0000000 --- a/tests/ukm-with-contract/endpoints.3.run +++ /dev/null @@ -1,5 +0,0 @@ -hold b"c6b6e179\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\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\x00\x01"; -mock DecodeOp; -return_value; - -check_eq 3_u64 \ No newline at end of file diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md index f01aa91..c756490 100644 --- a/ukm-semantics/main/decoding/decoder.md +++ b/ukm-semantics/main/decoding/decoder.md @@ -34,7 +34,7 @@ module UKM-CALLDATA-DECODER NextId:Int => NextId +Int 1 Values:Map => Values[NextId <- V] [priority(70)] - rule UKMDecodedCallData1(P:PathInExpression, .List) + rule UKMDecodedCallData1(_:PathInExpression, .List) => .K ... rule UKMDecodedCallData2(P:PathInExpression, L:List) @@ -55,8 +55,8 @@ module UKM-CALLDATA-DECODER (self : $selftype), L:NormalizedFunctionParameterList rule decodeArguments(((_ : T:Type), R):NormalizedFunctionParameterList, D:Bytes, L:List) => - decodeArguments(R, substrBytes(D, 0, sizeOfType(T)), - ListItem( convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, sizeOfType(T)), BE, Unsigned ) ) ) L ) + decodeArguments(R, substrBytes(D, 0, 32), + ListItem( convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, 32), BE, Unsigned ) ) ) L ) rule decodeArguments(.NormalizedFunctionParameterList, _, L:List) => L @@ -65,11 +65,5 @@ module UKM-CALLDATA-DECODER rule convertKBytesToPtrValue(i64, I:Int) => ptrValue(null, i64(Int2MInt(I))) rule convertKBytesToPtrValue(u64, I:Int) => ptrValue(null, u64(Int2MInt(I))) rule convertKBytesToPtrValue(u128, I:Int) => ptrValue(null, u128(Int2MInt(I))) - - rule sizeOfType(i32) => 32 - rule sizeOfType(u32) => 32 - rule sizeOfType(u64) => 64 - rule sizeOfType(i64) => 64 - rule sizeOfType(u128) => 128 endmodule ``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index 1e7c1a4..39c6de1 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -41,9 +41,12 @@ module UKM-CALLDATA-ENCODER // The last param does not have a follow up comma rule encodeFunctionSignature("", ListItem(FuncParam:String) .List, FS) => - encodeFunctionSignature("", .List, FS +String FuncParam ) + encodeFunctionSignature("", .List, FS +String FuncParam +String ")" ) - rule encodeFunctionSignature("", .List, FS) => String2Bytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) + rule encodeFunctionSignature("", .List, FS) => String2Bytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) + + rule encodeFunctionSignatureAsString(FS) => substrString(Keccak256(String2Bytes(FS)), 0, 8) + rule encodeFunctionSignature(FS:String:StringOrError) => String2Bytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) // Function parameters encoding rule encodeFunctionParams(ListItem(V:Value) ARGS:List, ListItem(T:String) PTYPES:List, B:Bytes) => @@ -54,21 +57,21 @@ module UKM-CALLDATA-ENCODER // Encoding of individual types - rule convertToKBytes(i8(V) , "int8") => Int2Bytes(8, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(8, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i16(V), "int16") => Int2Bytes(16, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u16(V), "uint16") => Int2Bytes(16, MInt2Unsigned(V), BE:Endianness) + 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(64, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u64(V), "uint64") => Int2Bytes(64, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u128(V), "uint128") => Int2Bytes(128, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(true, "bool") => Int2Bytes(8, 1, BE:Endianness) - rule convertToKBytes(false, "bool") => Int2Bytes(8, 0, 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) // TODO: as we currently do not support u160 (addresses) or u256, we're converting them to u64 for now - rule convertToKBytes(u64(V), "uint256") => Int2Bytes(256, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u64(V), "uint160") => Int2Bytes(160, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u64(V), "address") => Int2Bytes(160, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u64(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) endmodule diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index ef8a278..fcd3d46 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -14,9 +14,12 @@ module UKM-ENCODING-SYNTAX syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list | encodeFunctionSignature (String, List, String) [function] + | encodeFunctionSignature (StringOrError) [function] | encodeFunctionParams (List, List, Bytes) [function] | convertToKBytes ( Value , String ) [function] + syntax String ::= encodeFunctionSignatureAsString(StringOrError) [function] + endmodule ``` diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md index 9b25d37..fefb3a3 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ukm-semantics/main/hooks/bytes.md @@ -46,6 +46,7 @@ module UKM-HOOKS-BYTES | "decode_u16" [token] | "decode_u8" [token] | "decode_str" [token] + | "decode_signature" [token] rule @@ -125,35 +126,40 @@ module UKM-HOOKS-BYTES ( :: bytes_hooks :: decode_u128 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u32) + => ukmBytesDecodeWithLength(BufferIdId, u32, 32) + // => ukmBytesDecode(BufferIdId, u32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u64 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u64) + => ukmBytesDecodeWithLength(BufferIdId, u64, 32) + // => ukmBytesDecode(BufferIdId, u64) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u32 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u32) + => ukmBytesDecodeWithLength(BufferIdId, u32, 32) + // => ukmBytesDecode(BufferIdId, u32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u16 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u16) + => ukmBytesDecodeWithLength(BufferIdId, u16, 32) + // => ukmBytesDecode(BufferIdId, u16) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u8 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecode(BufferIdId, u8) + => ukmBytesDecodeWithLength(BufferIdId, u8, 32) + // => ukmBytesDecode(BufferIdId, u8) rule normalizedFunctionCall @@ -162,6 +168,13 @@ module UKM-HOOKS-BYTES ) => ukmBytesDecode(BufferIdId, str) + rule + normalizedFunctionCall + ( :: bytes_hooks :: decode_signature :: .PathExprSegments + , BufferIdId:Ptr, .PtrList + ) + => ukmBytesDecodeWithLength(BufferIdId, str, 8) + // --------------------------------------- rule @@ -184,6 +197,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) @@ -236,6 +251,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 b69e1d9..d8c3230 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -9,6 +9,21 @@ 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-PREPROCESSING-CONFIGURATION + imports private UKM-ENCODING-SYNTAX + + rule + ukmPreprocessSignatureHash(Method, EndpointMethod) => ukmPreprocessingStoreSignatureHash(encodeFunctionSignature(Method, L), EndpointMethod) + ... + + Method + L:NormalizedFunctionParameterList + + rule ukmPreprocessingStoreSignatureHash(B:Bytes, P:PathInExpression) => .K ... + + STATE => STATE [ B <- P ] + + rule @@ -157,6 +172,7 @@ module UKM-PREPROCESSING-ENDPOINTS | "decode_u32" [token] | "decode_u64" [token] | "decode_str" [token] + | "decode_signature" [token] | "empty" [token] | "ukm" [token] | "CallData" [token] @@ -168,7 +184,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) @@ -222,7 +238,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/methods.md b/ukm-semantics/main/preprocessing/methods.md index 0515a5e..9d50c6a 100644 --- a/ukm-semantics/main/preprocessing/methods.md +++ b/ukm-semantics/main/preprocessing/methods.md @@ -7,20 +7,6 @@ module UKM-PREPROCESSING-METHODS imports private RUST-PREPROCESSING-CONFIGURATION imports private UKM-PREPROCESSING-CONFIGURATION imports private UKM-PREPROCESSING-SYNTAX-PRIVATE - imports private UKM-ENCODING-SYNTAX - - rule - ukmPreprocessMethodSignature(Method) => ukmPreprocessingStoreMethodSignature(encodeFunctionSignature(Method, L), Method) - ... - - Method - L:NormalizedFunctionParameterList - - rule ukmPreprocessingStoreMethodSignature(B:Bytes, P:PathInExpression) => .K ... - - STATE => STATE [ B <- P ] - - rule ukmPreprocessMethods(_:TypePath, .List) => .K rule ukmPreprocessMethods(Trait:TypePath, ListItem(Name:Identifier) Methods:List) @@ -35,7 +21,7 @@ module UKM-PREPROCESSING-METHODS , method: MethodIdentifier , fullMethodPath: Method , endpointName: getEndpointName(Atts, MethodIdentifier) - ) ~> ukmPreprocessMethodSignature(Method) + ) ... Method diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md index 4ca5e50..6f676fc 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ukm-semantics/main/preprocessing/syntax.md @@ -16,8 +16,8 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE | ukmPreprocessTrait(TypePath) | ukmPreprocessMethods(trait: TypePath, List) | ukmPreprocessMethod(trait: TypePath, methodId: Identifier, fullMethodPath: PathInExpression) - | ukmPreprocessMethodSignature(PathInExpression) - | ukmPreprocessingStoreMethodSignature(Bytes, PathInExpression) + | ukmPreprocessSignatureHash(PathInExpression, PathInExpression) + | ukmPreprocessingStoreSignatureHash(Bytes, PathInExpression) | ukmPreprocessEndpoint ( trait: TypePath , method: Identifier diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index c1bf9d5..51ba812 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -15,8 +15,8 @@ module UKM-TEST-SYNTAX syntax ExecutionItem ::= "mock" "Caller" | "mock" "CallData" - | "mock" "EncodeOp" - | "mock" "DecodeOp" + | "mock" "EncodeCallData" + | "mock" "EncodeCallDataToString" | "call_contract" Int | "hold" KItem | "output_to_arg" @@ -65,14 +65,17 @@ module UKM-TEST-EXECUTION rule hold I => value_holder I ... - rule mock EncodeOp + rule mock EncodeCallDataToString ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) ... - - rule mock DecodeOp ~> value_holder B:Bytes => decodeCallData(B) ... - rule UKMDecodedCallData(P:PathInExpression , L:PtrList) => normalizedFunctionCall(P, L) ... + + rule mock EncodeCallData + ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList + => ukmBytesNew(encodeCallData(FNAME, PTYPES, ARGS)) + ... + rule mock CallData => mock(CallDataHook(), V) ... From f34486007ffceec01624a033367ed017f09550f3 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Tue, 22 Oct 2024 21:18:47 -0300 Subject: [PATCH 08/17] Fixing minor issue from merge and adding the blockchain plugin folder to search path --- Makefile | 5 ++++- ukm-semantics/main/encoding/encoder.md | 2 +- ukm-semantics/test/execution.md | 2 ++ 3 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 0c26fac..bb9fa9d 100644 --- a/Makefile +++ b/Makefile @@ -189,6 +189,7 @@ $(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ --emit-json -o $(UKM_EXECUTION_KOMPILED) \ -I kllvm \ + -I blockchain-k-plugin \ -I . \ --debug @@ -200,17 +201,19 @@ $(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ --emit-json -o $(UKM_PREPROCESSING_KOMPILED) \ -I . \ + -I blockchain-k-plugin \ --debug $(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) # 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} --hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \ -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ + ${PLUGIN_FLAGS} \ --emit-json -o $(UKM_TESTING_KOMPILED) \ -I . \ + -I blockchain-k-plugin \ -I kllvm \ --debug diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index 39c6de1..d4757e7 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -1,5 +1,5 @@ ```k -requires "blockchain-k-plugin/plugin/krypto.md" +requires "plugin/krypto.md" module UKM-CALLDATA-ENCODER imports private COMMON-K-CELL diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index fdd7104..ec28bd0 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -12,6 +12,8 @@ module UKM-TEST-SYNTAX | "list_ptrs_holder" List | "list_values_holder" List + syntax UKMTestTypeHolderList ::= List{UKMTestTypeHolder, ","} + syntax ExecutionItem ::= "mock" "CallData" | "mock" "Caller" | "mock" UkmHook UkmHookResult From ffbb0cf14fbda147f014eda0a9d5e23d24dd9820 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Tue, 22 Oct 2024 21:32:12 -0300 Subject: [PATCH 09/17] Use lowercase type names in function signature --- ukm-semantics/main/preprocessing/endpoints.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index 5e087d5..8b45d02 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -202,10 +202,10 @@ 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(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" From 6d075efcd1e6a5cf297034de63a09e350539b56a Mon Sep 17 00:00:00 2001 From: acassimiro Date: Wed, 23 Oct 2024 01:06:22 -0300 Subject: [PATCH 10/17] Adapting tests to properly encode call data --- tests/ukm-with-contract/erc_20_token.1.run | 135 +++++++++------------ 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 | 27 ++--- tests/ukm-with-contract/storage.simple.run | 19 ++- ukm-semantics/main/encoding/encoder.md | 13 +- ukm-semantics/test/execution.md | 12 ++ 8 files changed, 121 insertions(+), 128 deletions(-) diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ukm-with-contract/erc_20_token.1.run index 21b01e3..af6ed52 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; +mock EncodeCallData; + + 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; +mock EncodeCallData; 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; +mock EncodeCallData; 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; +mock EncodeCallData; 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; +mock EncodeCallData; 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; +mock EncodeCallData; 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; +mock EncodeCallData; 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; +mock EncodeCallData; 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; +mock EncodeCallData; return_value; mock CallData; diff --git a/tests/ukm-with-contract/events.1.run b/tests/ukm-with-contract/events.1.run index 8c0c04b..17b925f 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; +mock EncodeCallData; +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..2122a5a 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; +mock EncodeCallData; return_value; mock CallData; diff --git a/tests/ukm-with-contract/require.true.run b/tests/ukm-with-contract/require.true.run index 4264f65..10c46e1 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; +mock EncodeCallData; return_value; mock CallData; diff --git a/tests/ukm-with-contract/storage.key.run b/tests/ukm-with-contract/storage.key.run index a2e618d..8859022 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; +mock EncodeCallData; 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; +mock EncodeCallData; return_value; mock CallData; diff --git a/tests/ukm-with-contract/storage.simple.run b/tests/ukm-with-contract/storage.simple.run index 4648776..5e30718 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; +mock EncodeCallData; 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; +mock EncodeCallData; return_value; mock CallData; diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index d4757e7..c0889b1 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -34,16 +34,16 @@ module UKM-CALLDATA-ENCODER // Function signature encoding rule encodeFunctionSignature(FuncName:String, RL:List, "") => - encodeFunctionSignature("", RL:List, FuncName +String "(") + 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 +String ")" ) + encodeFunctionSignature("", .List, FS +String FuncParam ) - rule encodeFunctionSignature("", .List, FS) => String2Bytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) + rule encodeFunctionSignature("", .List, FS) => String2Bytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) rule encodeFunctionSignatureAsString(FS) => substrString(Keccak256(String2Bytes(FS)), 0, 8) rule encodeFunctionSignature(FS:String:StringOrError) => String2Bytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) @@ -68,10 +68,9 @@ module UKM-CALLDATA-ENCODER 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) - // TODO: as we currently do not support u160 (addresses) or u256, we're converting them to u64 for now - rule convertToKBytes(u64(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u64(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u64(V), "address") => Int2Bytes(32, MInt2Unsigned(V), 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 diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index ec28bd0..c941c50 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -84,12 +84,24 @@ module UKM-TEST-EXECUTION ... + rule mock EncodeCallDataToString + ~> value_holder FNAME + => Bytes2String(encodeCallData(FNAME, .List, .List)) + ... + [owise] + rule mock EncodeCallData ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList => ukmBytesNew(encodeCallData(FNAME, PTYPES, ARGS)) ... + rule mock EncodeCallData + ~> value_holder FNAME + => ukmBytesNew(encodeCallData(FNAME, .List, .List)) + ... + [owise] + rule mock CallData => mock(CallDataHook(), V) ... From 6a140b212d64c9f12fcfcfaf9e4d15939023febe Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 23 Oct 2024 17:28:39 +0300 Subject: [PATCH 11/17] Fix build --- .gitmodules | 2 +- Makefile | 21 +++++++++++-------- .../blockchain-k-plugin | 0 ukm-semantics/main/encoding/encoder.md | 4 ++-- 4 files changed, 15 insertions(+), 12 deletions(-) rename blockchain-k-plugin => deps/blockchain-k-plugin (100%) diff --git a/.gitmodules b/.gitmodules index 067a670..3558764 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,3 @@ [submodule "blockchain-k-plugin"] - path = blockchain-k-plugin + path = deps/blockchain-k-plugin url = https://github.com/runtimeverification/blockchain-k-plugin diff --git a/Makefile b/Makefile index bb9fa9d..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,39 +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 \ --hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \ - -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ + -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'deps/blockchain-k-plugin/build/krypto/lib/krypto.a' \ --emit-json -o $(UKM_EXECUTION_KOMPILED) \ -I kllvm \ - -I blockchain-k-plugin \ + -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 \ --hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \ - -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ + -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'deps/blockchain-k-plugin/build/krypto/lib/krypto.a' \ --emit-json -o $(UKM_PREPROCESSING_KOMPILED) \ -I . \ - -I blockchain-k-plugin \ + -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 \ --hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \ - -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \ + -ccopt -lsecp256k1 -ccopt -lssl -ccopt 'deps/blockchain-k-plugin/build/krypto/lib/krypto.a' \ ${PLUGIN_FLAGS} \ --emit-json -o $(UKM_TESTING_KOMPILED) \ -I . \ - -I blockchain-k-plugin \ + -I deps/blockchain-k-plugin \ -I kllvm \ --debug diff --git a/blockchain-k-plugin b/deps/blockchain-k-plugin similarity index 100% rename from blockchain-k-plugin rename to deps/blockchain-k-plugin diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index c0889b1..9c219f3 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -16,9 +16,9 @@ module UKM-CALLDATA-ENCODER rule encodeFunctionSignature (P:PathInExpression, N:NormalizedFunctionParameterList) => encodeFunctionSignature(convertPathInExprToString(P), convertFuncParamListToStrList(N, .List), "") - rule convertPathInExprToString(( :: I:Identifier :: R:PathExprSegments):PathInExpression ) => + rule convertPathInExprToString(( :: _I:Identifier :: R:PathExprSegments):PathInExpression ) => convertPathInExprToString(R) [priority(80)] - rule convertPathInExprToString(( I:Identifier :: R:PathExprSegments):PathInExpression ) => + rule convertPathInExprToString(( _I:Identifier :: R:PathExprSegments):PathInExpression ) => convertPathInExprToString(R) [priority(80)] rule convertPathInExprToString(( I:Identifier :: .PathExprSegments):PathInExpression ) => Identifier2String(I) [priority(70)] From f1caec99fc1c8e6de83fb8ba1c67c7ec0583466f Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 23 Oct 2024 17:42:31 +0300 Subject: [PATCH 12/17] Add random dependencies --- Dockerfile | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 305329a..64f9d60 100644 --- a/Dockerfile +++ b/Dockerfile @@ -8,7 +8,11 @@ FROM runtimeverificationinc/kframework-k:ubuntu-noble-${K_COMMIT} RUN apt-get update \ && apt-get upgrade --yes \ && apt-get install --yes \ - curl + curl \ + libcrypto++-dev \ + libprocps-dev \ + libsecp256k1-dev \ + libssl-dev \ ARG USER_ID=1001 ARG GROUP_ID=1001 From 4f39b2f9d5db5e271b87e302a04e10aee84877be Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 23 Oct 2024 17:46:19 +0300 Subject: [PATCH 13/17] Fix dependencies --- Dockerfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index 64f9d60..bc01c7c 100644 --- a/Dockerfile +++ b/Dockerfile @@ -12,7 +12,7 @@ RUN apt-get update \ libcrypto++-dev \ libprocps-dev \ libsecp256k1-dev \ - libssl-dev \ + libssl-dev ARG USER_ID=1001 ARG GROUP_ID=1001 From 73d9494b2f9b3d27a142bd6dbbd286e77455003f Mon Sep 17 00:00:00 2001 From: Virgil Date: Wed, 23 Oct 2024 18:04:22 +0300 Subject: [PATCH 14/17] Fix dependencies --- Dockerfile | 1 - 1 file changed, 1 deletion(-) diff --git a/Dockerfile b/Dockerfile index bc01c7c..6224020 100644 --- a/Dockerfile +++ b/Dockerfile @@ -10,7 +10,6 @@ RUN apt-get update \ && apt-get install --yes \ curl \ libcrypto++-dev \ - libprocps-dev \ libsecp256k1-dev \ libssl-dev From 60a540aacade164c2524b4d05cfc82c30ff0b3f7 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Wed, 23 Oct 2024 14:16:39 -0300 Subject: [PATCH 15/17] Code cleanup --- tests/ukm-with-contract/endpoints.1.run | 2 +- ukm-semantics/main/decoding/decoder.md | 63 ------------------- ukm-semantics/main/decoding/syntax.md | 24 ------- ukm-semantics/main/encoding/encoder.md | 19 ------ ukm-semantics/main/encoding/syntax.md | 5 -- ukm-semantics/main/hooks/bytes.md | 7 --- ukm-semantics/main/preprocessing/endpoints.md | 13 ---- 7 files changed, 1 insertion(+), 132 deletions(-) diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run index f1d3a48..60f2cca 100644 --- a/tests/ukm-with-contract/endpoints.1.run +++ b/tests/ukm-with-contract/endpoints.1.run @@ -10,7 +10,7 @@ return_value; mock CallData; call_contract 12345; -return_value; +return_value; check_eq (); push_status; diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md index c756490..d40b6f3 100644 --- a/ukm-semantics/main/decoding/decoder.md +++ b/ukm-semantics/main/decoding/decoder.md @@ -1,69 +1,6 @@ ```k module UKM-CALLDATA-DECODER - imports RUST-VALUE-SYNTAX - imports UKM-DECODING-SYNTAX - imports BYTES-HOOKED - imports BYTES-SYNTAX - imports private COMMON-K-CELL - imports private RUST-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-CONFIGURATION - imports private RUST-EXECUTION-CONFIGURATION - imports private RUST-REPRESENTATION - imports private RUST-CONVERSIONS-SYNTAX - imports INT - rule decodeCallData(D:Bytes) => - UKMDecodedCallData1(decodeFunctionSignature(substrBytes(D, 0, 8)), decodeArguments(loadArgumentsFromHash(substrBytes(D, 0, 8)), substrBytes(D, 8, lengthBytes(D)), .List) ) - - // TODO: Self is being assigned to an integer 0. This should be fixed in case we need - // to make references to self within rust contracts - rule UKMDecodedCallData1(P:PathInExpression, L:List) - => UKMDecodedCallData1(P, L) - ~> UKMDecodedCallData2(P, ListItem(NextId)) - ... - NextId:Int => NextId +Int 1 - Values:Map => Values[NextId <- u64(Int2MInt(0))] [priority(80)] - - - rule UKMDecodedCallData1(P:PathInExpression, L:List ListItem(ptrValue(_, V))) - ~> UKMDecodedCallData2(P:PathInExpression, PL:List) - => UKMDecodedCallData1(P, L) - ~> UKMDecodedCallData2(P, ListItem(NextId) PL) - ... - NextId:Int => NextId +Int 1 - Values:Map => Values[NextId <- V] [priority(70)] - - rule UKMDecodedCallData1(_:PathInExpression, .List) - => .K ... - - rule UKMDecodedCallData2(P:PathInExpression, L:List) - => UKMDecodedCallData(P:PathInExpression, listToPtrList(L)) ... - - rule [[ decodeFunctionSignature(FuncSigHash:Bytes) => P ]] - - ... FuncSigHash |-> P:PathInExpression ... - - - rule [[ loadArgumentsFromHash(FuncSigHash:Bytes) => loadArgumentsFromHash(P) ]] - - ... FuncSigHash |-> P:PathInExpression ... - - - rule [[ loadArgumentsFromHash(Method:PathInExpression) => L ]] - Method - (self : $selftype), L:NormalizedFunctionParameterList - - rule decodeArguments(((_ : T:Type), R):NormalizedFunctionParameterList, D:Bytes, L:List) => - decodeArguments(R, substrBytes(D, 0, 32), - ListItem( convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, 32), BE, Unsigned ) ) ) L ) - - rule decodeArguments(.NormalizedFunctionParameterList, _, L:List) => L - - rule convertKBytesToPtrValue(u32, I:Int) => ptrValue(null, u32(Int2MInt(I))) - rule convertKBytesToPtrValue(i32, I:Int) => ptrValue(null, i32(Int2MInt(I))) - rule convertKBytesToPtrValue(i64, I:Int) => ptrValue(null, i64(Int2MInt(I))) - rule convertKBytesToPtrValue(u64, I:Int) => ptrValue(null, u64(Int2MInt(I))) - rule convertKBytesToPtrValue(u128, I:Int) => ptrValue(null, u128(Int2MInt(I))) endmodule ``` \ No newline at end of file diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md index feb2f14..35843be 100644 --- a/ukm-semantics/main/decoding/syntax.md +++ b/ukm-semantics/main/decoding/syntax.md @@ -2,33 +2,9 @@ module UKM-DECODING-SYNTAX imports BYTES-SYNTAX - imports INT-SYNTAX - imports LIST - imports RUST-VALUE-SYNTAX - imports private RUST-REPRESENTATION - - syntax UKMDecodedCallDataWrapper ::= UKMDecodedCallData1( PathInExpression , List ) - | UKMDecodedCallData2( PathInExpression , List ) - | UKMDecodedCallData ( PathInExpression , PtrListOrError) - | decodeCallData(Bytes) [function] syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes) - syntax NormalizedFunctionParameterList ::= loadArgumentsFromHash(Bytes) [function] - | loadArgumentsFromHash(PathInExpression) [function] - - syntax List ::= decodeCallDataArguments(Bytes) [function] - | decodeArguments(NormalizedFunctionParameterList, Bytes, List) [function] - - - - syntax PathInExpression ::= decodeFunctionSignature(Bytes) [function] - - syntax PtrValue ::= convertKBytesToPtrValue(Type, Int) [function] - - syntax Int ::= sizeOfType(Type) [function] - - endmodule ``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index 9c219f3..096d573 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -10,25 +10,6 @@ module UKM-CALLDATA-ENCODER imports INT imports KRYPTO - syntax String ::= Identifier2String(Identifier) [function, total, hook(STRING.token2string)] - | Type2String(Type) [function, total, hook(STRING.token2string)] - - rule encodeFunctionSignature (P:PathInExpression, N:NormalizedFunctionParameterList) => - encodeFunctionSignature(convertPathInExprToString(P), convertFuncParamListToStrList(N, .List), "") - - rule convertPathInExprToString(( :: _I:Identifier :: R:PathExprSegments):PathInExpression ) => - convertPathInExprToString(R) [priority(80)] - rule convertPathInExprToString(( _I:Identifier :: R:PathExprSegments):PathInExpression ) => - convertPathInExprToString(R) [priority(80)] - rule convertPathInExprToString(( I:Identifier :: .PathExprSegments):PathInExpression ) => - Identifier2String(I) [priority(70)] - - rule convertFuncParamListToStrList(((self : _), N:NormalizedFunctionParameterList), .List) => - convertFuncParamListToStrList( N, .List) [priority(60)] - rule convertFuncParamListToStrList(((_ : T:Type), N:NormalizedFunctionParameterList), L:List) => - convertFuncParamListToStrList(N, L ListItem(signatureType(T))) [priority(70)] - rule convertFuncParamListToStrList(.NormalizedFunctionParameterList, L:List) => L - rule encodeCallData(FN:String, FAT:List, FAL:List) => encodeFunctionSignature(FN, FAT, "") +Bytes encodeFunctionParams(FAL, FAT, b"") diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index fcd3d46..f617db0 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -6,11 +6,6 @@ module UKM-ENCODING-SYNTAX imports RUST-REPRESENTATION syntax UKMInstruction ::= "ukmEncodePreprocessedCell" - - syntax Bytes ::= encodeFunctionSignature (PathInExpression, NormalizedFunctionParameterList) [function] - - syntax String ::= convertPathInExprToString(PathInExpression) [function] - syntax List ::= convertFuncParamListToStrList(NormalizedFunctionParameterList, List) [function] syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list | encodeFunctionSignature (String, List, String) [function] diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md index 2fc5f79..3ce1ae9 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ukm-semantics/main/hooks/bytes.md @@ -146,7 +146,6 @@ module UKM-HOOKS-BYTES , BufferIdId:Ptr, .PtrList ) => ukmBytesDecodeWithLength(BufferIdId, u256, 32) - // ukmBytesDecode(BufferIdId, u256) rule normalizedFunctionCall @@ -154,7 +153,6 @@ module UKM-HOOKS-BYTES , BufferIdId:Ptr, .PtrList ) => ukmBytesDecodeWithLength(BufferIdId, u160, 32) - // ukmBytesDecode(BufferIdId, u160) rule normalizedFunctionCall @@ -162,7 +160,6 @@ module UKM-HOOKS-BYTES , BufferIdId:Ptr, .PtrList ) => ukmBytesDecodeWithLength(BufferIdId, u128, 32) - // => ukmBytesDecode(BufferIdId, u32) rule normalizedFunctionCall @@ -170,7 +167,6 @@ module UKM-HOOKS-BYTES , BufferIdId:Ptr, .PtrList ) => ukmBytesDecodeWithLength(BufferIdId, u64, 32) - // => ukmBytesDecode(BufferIdId, u64) rule normalizedFunctionCall @@ -178,7 +174,6 @@ module UKM-HOOKS-BYTES , BufferIdId:Ptr, .PtrList ) => ukmBytesDecodeWithLength(BufferIdId, u32, 32) - // => ukmBytesDecode(BufferIdId, u32) rule normalizedFunctionCall @@ -186,7 +181,6 @@ module UKM-HOOKS-BYTES , BufferIdId:Ptr, .PtrList ) => ukmBytesDecodeWithLength(BufferIdId, u16, 32) - // => ukmBytesDecode(BufferIdId, u16) rule normalizedFunctionCall @@ -194,7 +188,6 @@ module UKM-HOOKS-BYTES , BufferIdId:Ptr, .PtrList ) => ukmBytesDecodeWithLength(BufferIdId, u8, 32) - // => ukmBytesDecode(BufferIdId, u8) rule normalizedFunctionCall diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index 8b45d02..ee9b66d 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -12,19 +12,6 @@ module UKM-PREPROCESSING-ENDPOINTS imports private UKM-PREPROCESSING-CONFIGURATION imports private UKM-ENCODING-SYNTAX - rule - ukmPreprocessSignatureHash(Method, EndpointMethod) => ukmPreprocessingStoreSignatureHash(encodeFunctionSignature(Method, L), EndpointMethod) - ... - - Method - L:NormalizedFunctionParameterList - - rule ukmPreprocessingStoreSignatureHash(B:Bytes, P:PathInExpression) => .K ... - - STATE => STATE [ B <- P ] - - - rule ukmPreprocessEndpoint From b8ca60910dce28eebb7740a58d42751d1e845bbe Mon Sep 17 00:00:00 2001 From: acassimiro Date: Wed, 23 Oct 2024 14:29:37 -0300 Subject: [PATCH 16/17] Code cleanup --- ukm-semantics/main/decoding.md | 2 -- ukm-semantics/main/preprocessing/configuration.md | 3 --- ukm-semantics/main/preprocessing/endpoints.md | 1 - ukm-semantics/main/preprocessing/methods.md | 1 - ukm-semantics/main/preprocessing/syntax.md | 3 --- ukm-semantics/targets/testing/ukm-target.md | 2 -- ukm-semantics/test/execution.md | 1 - 7 files changed, 13 deletions(-) diff --git a/ukm-semantics/main/decoding.md b/ukm-semantics/main/decoding.md index bc60913..3561da2 100644 --- a/ukm-semantics/main/decoding.md +++ b/ukm-semantics/main/decoding.md @@ -1,10 +1,8 @@ ```k requires "decoding/syntax.md" -requires "decoding/decoder.md" module UKM-DECODING - imports UKM-CALLDATA-DECODER endmodule ``` diff --git a/ukm-semantics/main/preprocessing/configuration.md b/ukm-semantics/main/preprocessing/configuration.md index 9484412..9302083 100644 --- a/ukm-semantics/main/preprocessing/configuration.md +++ b/ukm-semantics/main/preprocessing/configuration.md @@ -8,9 +8,6 @@ module UKM-PREPROCESSING-CONFIGURATION (#token("not#initialized", "Identifier"):Identifier):TypePath - - .Map - endmodule diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index ee9b66d..034a0b6 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -9,7 +9,6 @@ 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-PREPROCESSING-CONFIGURATION imports private UKM-ENCODING-SYNTAX rule diff --git a/ukm-semantics/main/preprocessing/methods.md b/ukm-semantics/main/preprocessing/methods.md index 5c09100..e820f4a 100644 --- a/ukm-semantics/main/preprocessing/methods.md +++ b/ukm-semantics/main/preprocessing/methods.md @@ -5,7 +5,6 @@ module UKM-PREPROCESSING-METHODS imports private K-EQUAL-SYNTAX imports private RUST-CONVERSIONS-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION - imports private UKM-PREPROCESSING-CONFIGURATION imports private UKM-PREPROCESSING-SYNTAX-PRIVATE rule ukmPreprocessMethods(_:TypePath, .List) => .K diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md index a7f90bb..c186d6d 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ukm-semantics/main/preprocessing/syntax.md @@ -10,14 +10,11 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE imports LIST imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX - imports private BYTES-SYNTAX syntax UKMInstruction ::= ukmPreprocessTraits(List) | ukmPreprocessTrait(TypePath) | ukmPreprocessMethods(trait: TypePath, List) | ukmPreprocessMethod(trait: TypePath, methodId: Identifier, fullMethodPath: PathInExpression) - | ukmPreprocessSignatureHash(PathInExpression, PathInExpression) - | ukmPreprocessingStoreSignatureHash(Bytes, PathInExpression) | ukmPreprocessEndpoint ( trait: TypePath , method: Identifier diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index e21bc7f..b2f1f70 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ukm-semantics/targets/testing/ukm-target.md @@ -1,7 +1,6 @@ ```k requires "../../main/encoding.md" -requires "../../main/decoding.md" requires "../../main/execution.md" requires "../../main/preprocessing.md" requires "../../test/execution.md" @@ -22,7 +21,6 @@ module UKM-TARGET imports private RUST-EXECUTION-TEST imports private UKM-EXECUTION imports private UKM-ENCODING - imports private UKM-DECODING 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 c941c50..ea5bb66 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -42,7 +42,6 @@ module UKM-TEST-EXECUTION imports private COMMON-K-CELL imports private RUST-EXECUTION-TEST-CONFIGURATION imports private UKM-ENCODING-SYNTAX - imports private UKM-DECODING-SYNTAX imports private UKM-EXECUTION-SYNTAX imports private UKM-HOOKS-BYTES-CONFIGURATION imports private UKM-HOOKS-BYTES-SYNTAX From 1bdbb7dc06bfc3f82e68024b54b463ffc11844e9 Mon Sep 17 00:00:00 2001 From: acassimiro Date: Wed, 23 Oct 2024 20:22:53 -0300 Subject: [PATCH 17/17] Addressing review --- tests/ukm-with-contract/endpoints.1.run | 2 +- tests/ukm-with-contract/endpoints.2.run | 2 +- tests/ukm-with-contract/erc_20_token.1.run | 18 +++++++------- tests/ukm-with-contract/events.1.run | 2 +- tests/ukm-with-contract/require.false.run | 2 +- tests/ukm-with-contract/require.true.run | 2 +- tests/ukm-with-contract/storage.key.run | 4 +-- tests/ukm-with-contract/storage.simple.run | 4 +-- ukm-semantics/main/decoding/decoder.md | 6 ----- ukm-semantics/main/encoding/encoder.md | 29 +++++++++++++++------- ukm-semantics/main/encoding/syntax.md | 6 ++--- ukm-semantics/test/execution.md | 21 ++++++++++------ 12 files changed, 55 insertions(+), 43 deletions(-) delete mode 100644 ukm-semantics/main/decoding/decoder.md diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run index 60f2cca..46df244 100644 --- a/tests/ukm-with-contract/endpoints.1.run +++ b/tests/ukm-with-contract/endpoints.1.run @@ -4,7 +4,7 @@ push "uint64"; hold_list_values_from_test_stack; push 123_u64; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; diff --git a/tests/ukm-with-contract/endpoints.2.run b/tests/ukm-with-contract/endpoints.2.run index 16a9489..66bd396 100644 --- a/tests/ukm-with-contract/endpoints.2.run +++ b/tests/ukm-with-contract/endpoints.2.run @@ -4,6 +4,6 @@ push "uint64"; hold_list_values_from_test_stack; push 1_u64; hold_list_values_from_test_stack; -mock EncodeCallDataToString; +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 af6ed52..6bb77ac 100644 --- a/tests/ukm-with-contract/erc_20_token.1.run +++ b/tests/ukm-with-contract/erc_20_token.1.run @@ -27,7 +27,7 @@ push "uint256"; hold_list_values_from_test_stack; push 10000_u256; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; @@ -57,7 +57,7 @@ push "uint160"; hold_list_values_from_test_stack; push 1010101_u160; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -83,7 +83,7 @@ hold_list_values_from_test_stack; push 2020202_u160; push 100_u256; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -110,7 +110,7 @@ push "uint160"; hold_list_values_from_test_stack; push 1010101_u160; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -134,7 +134,7 @@ push "uint160"; hold_list_values_from_test_stack; push 2020202_u160; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -160,7 +160,7 @@ hold_list_values_from_test_stack; push 3030303_u160; push 200_u256; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -191,7 +191,7 @@ push 1010101_u160; push 2020202_u160; push 200_u256; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -219,7 +219,7 @@ push "uint160"; hold_list_values_from_test_stack; push 1010101_u160; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -244,7 +244,7 @@ push "uint160"; hold_list_values_from_test_stack; push 2020202_u160; hold_list_values_from_test_stack; -mock EncodeCallData; +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 17b925f..34f870c 100644 --- a/tests/ukm-with-contract/events.1.run +++ b/tests/ukm-with-contract/events.1.run @@ -6,7 +6,7 @@ hold_list_values_from_test_stack; push 123_u64; push 555_u64; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; diff --git a/tests/ukm-with-contract/require.false.run b/tests/ukm-with-contract/require.false.run index 2122a5a..a151319 100644 --- a/tests/ukm-with-contract/require.false.run +++ b/tests/ukm-with-contract/require.false.run @@ -4,7 +4,7 @@ push "uint64"; hold_list_values_from_test_stack; push 0_u64; hold_list_values_from_test_stack; -mock EncodeCallData; +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 10c46e1..4e0ec98 100644 --- a/tests/ukm-with-contract/require.true.run +++ b/tests/ukm-with-contract/require.true.run @@ -4,7 +4,7 @@ push "uint64"; hold_list_values_from_test_stack; push 123_u64; hold_list_values_from_test_stack; -mock EncodeCallData; +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 8859022..8eb6705 100644 --- a/tests/ukm-with-contract/storage.key.run +++ b/tests/ukm-with-contract/storage.key.run @@ -9,7 +9,7 @@ hold_list_values_from_test_stack; push 555_u64; push 123_u64; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -27,7 +27,7 @@ push "uint64"; hold_list_values_from_test_stack; push 555_u64; hold_list_values_from_test_stack; -mock EncodeCallData; +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 5e30718..2b2b4ba 100644 --- a/tests/ukm-with-contract/storage.simple.run +++ b/tests/ukm-with-contract/storage.simple.run @@ -7,7 +7,7 @@ push "uint64"; hold_list_values_from_test_stack; push 123_u64; hold_list_values_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; @@ -21,7 +21,7 @@ check_eq 2; push "getMyData"; hold_string_from_test_stack; -mock EncodeCallData; +encode_call_data; return_value; mock CallData; diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md deleted file mode 100644 index d40b6f3..0000000 --- a/ukm-semantics/main/decoding/decoder.md +++ /dev/null @@ -1,6 +0,0 @@ -```k - -module UKM-CALLDATA-DECODER - -endmodule -``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index 096d573..8f88731 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -10,24 +10,35 @@ module UKM-CALLDATA-ENCODER 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"") + 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 encodeFunctionSignatureHelper(ListItem(FuncParam:String) .List, FS) => + encodeFunctionSignatureHelper(.List, FS +String FuncParam ) - rule encodeFunctionSignature("", .List, FS) => String2Bytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) + 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 encodeFunctionSignature(FS:String:StringOrError) => String2Bytes(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) => diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index f617db0..2fb33bb 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -8,12 +8,12 @@ module UKM-ENCODING-SYNTAX syntax UKMInstruction ::= "ukmEncodePreprocessedCell" syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list - | encodeFunctionSignature (String, List, String) [function] - | encodeFunctionSignature (StringOrError) [function] + | encodeFunctionSignature (String, List) [function] + | encodeFunctionSignatureHelper (List, String) [function] | encodeFunctionParams (List, List, Bytes) [function] | convertToKBytes ( Value , String ) [function] - syntax String ::= encodeFunctionSignatureAsString(StringOrError) [function] + syntax StringOrError ::= encodeFunctionSignatureAsString(StringOrError) [function, total] endmodule diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index ea5bb66..b6e4f1a 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -7,6 +7,10 @@ module UKM-TEST-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 @@ -18,8 +22,8 @@ module UKM-TEST-SYNTAX | "mock" "Caller" | "mock" UkmHook UkmHookResult | "list_mock" UkmHook UkmHookResult - | "mock" "EncodeCallData" - | "mock" "EncodeCallDataToString" + | "encode_call_data" + | "encode_call_data_to_string" | "call_contract" Int | "hold" KItem | "output_to_arg" @@ -66,7 +70,10 @@ module UKM-TEST-EXECUTION 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 @@ -77,25 +84,25 @@ module UKM-TEST-EXECUTION rule hold I => value_holder I ... - rule mock EncodeCallDataToString + rule encode_call_data_to_string ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) ... - rule mock EncodeCallDataToString + rule encode_call_data_to_string ~> value_holder FNAME => Bytes2String(encodeCallData(FNAME, .List, .List)) ... [owise] - rule mock EncodeCallData + rule encode_call_data ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .UKMTestTypeHolderList => ukmBytesNew(encodeCallData(FNAME, PTYPES, ARGS)) ... - rule mock EncodeCallData + rule encode_call_data ~> value_holder FNAME => ukmBytesNew(encodeCallData(FNAME, .List, .List)) ...