From 115fd631cc859ff001b7fc8b5cda37d8f963dd73 Mon Sep 17 00:00:00 2001 From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com> Date: Thu, 24 Oct 2024 20:52:50 +0300 Subject: [PATCH] Call data encoding and decoding (#171) * Call data encoding and decoding * Making spliting the encoding to helpers and main module. Adding TODOs. --------- Co-authored-by: ACassimiro --- tests/ukm-contracts/bytes_hooks.rs | 4 +- .../test_bytes_hooks.append32.run | 4 +- .../test_bytes_hooks.append64.run | 4 +- tests/ukm-with-contract/endpoints.2.run | 2 +- tests/ukm-with-contract/erc_20_token.1.run | 40 +++---- tests/ukm-with-contract/storage.key.run | 4 +- ukm-semantics/main/encoding.md | 1 + ukm-semantics/main/encoding/encoder.md | 100 ++++++++++------ ukm-semantics/main/encoding/syntax.md | 18 ++- ukm-semantics/main/hooks/bytes.md | 112 +++++++++--------- ukm-semantics/main/hooks/ukm.md | 4 +- ukm-semantics/main/preprocessing/endpoints.md | 16 ++- ukm-semantics/main/preprocessing/storage.md | 1 + ukm-semantics/main/preprocessing/syntax.md | 3 +- ukm-semantics/main/representation.md | 12 +- ukm-semantics/targets/testing/ukm-target.md | 1 + ukm-semantics/test/execution.md | 5 +- 17 files changed, 193 insertions(+), 138 deletions(-) diff --git a/tests/ukm-contracts/bytes_hooks.rs b/tests/ukm-contracts/bytes_hooks.rs index 6bc9ec5..c14b5ba 100644 --- a/tests/ukm-contracts/bytes_hooks.rs +++ b/tests/ukm-contracts/bytes_hooks.rs @@ -1,6 +1,7 @@ extern "C" { fn empty() -> u64; fn length(bytes_id: u64) -> u32; + fn equals(bytes_id_1: u64, bytes_id_2: u64) -> bool; fn append_u256(bytes_id: u64, value: u256) -> u64; fn append_u160(bytes_id: u64, value: u160) -> u64; @@ -19,8 +20,7 @@ extern "C" { fn decode_u32(bytes_id: u64) -> (u64, u32); fn decode_u16(bytes_id: u64) -> (u64, u16); fn decode_u8(bytes_id: u64) -> (u64, u8); - fn decode_str(bytes_id: u64) -> (u64, str); - fn decode_signature(bytes_id: u64) -> (u64, str); + fn decode_signature(bytes_id: u64) -> (u64, u64); fn hash(bytes_id: u64) -> u64; } diff --git a/tests/ukm-no-contract/test_bytes_hooks.append32.run b/tests/ukm-no-contract/test_bytes_hooks.append32.run index 124d4c5..d7c4dfa 100644 --- a/tests/ukm-no-contract/test_bytes_hooks.append32.run +++ b/tests/ukm-no-contract/test_bytes_hooks.append32.run @@ -3,11 +3,11 @@ call :: test_bytes_hooks :: append_u32; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 3_u32; +check_eq 32_u32; push 1000_u32; call :: test_bytes_hooks :: append_u32; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 4_u32 +check_eq 32_u32 diff --git a/tests/ukm-no-contract/test_bytes_hooks.append64.run b/tests/ukm-no-contract/test_bytes_hooks.append64.run index b02a99a..4dd72f1 100644 --- a/tests/ukm-no-contract/test_bytes_hooks.append64.run +++ b/tests/ukm-no-contract/test_bytes_hooks.append64.run @@ -3,11 +3,11 @@ call :: test_bytes_hooks :: append_u64; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 3_u32; +check_eq 32_u32; push 1000_u64; call :: test_bytes_hooks :: append_u64; return_value_to_arg; call :: bytes_hooks :: length; return_value; -check_eq 4_u32 +check_eq 32_u32 diff --git a/tests/ukm-with-contract/endpoints.2.run b/tests/ukm-with-contract/endpoints.2.run index 66bd396..054c2c5 100644 --- a/tests/ukm-with-contract/endpoints.2.run +++ b/tests/ukm-with-contract/endpoints.2.run @@ -6,4 +6,4 @@ push 1_u64; hold_list_values_from_test_stack; encode_call_data_to_string; return_value; -check_eq "81922854\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" \ No newline at end of file +check_eq "\x00\x81\x00\x92\x00(\x00T\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" \ 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 6bb77ac..3aedc1c 100644 --- a/tests/ukm-with-contract/erc_20_token.1.run +++ b/tests/ukm-with-contract/erc_20_token.1.run @@ -1,25 +1,25 @@ list_mock GetAccountStorageHook ( 7809087261546347641 ) ukmIntResult(0, u256); list_mock SetAccountStorageHook ( 7809087261546347641 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(0, u256); -list_mock SetAccountStorageHook ( 7162266444907899391 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); -list_mock SetAccountStorageHook ( 7162266444907899391 , 9900 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(0, u256); -list_mock SetAccountStorageHook ( 7162266444908917614 , 100 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(100, u256); -list_mock SetAccountStorageHook ( 8028228613167873919 , 200 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 8028228613167873919 ) ukmIntResult(200, u256); -list_mock SetAccountStorageHook ( 8028228613167873919 , 0 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); -list_mock SetAccountStorageHook ( 7162266444907899391 , 9700 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(100, u256); -list_mock SetAccountStorageHook ( 7162266444908917614 , 300 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9700, u256); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(300, u256); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(0, u256); +list_mock SetAccountStorageHook ( 7089066454178295295 , 10000 ) ukmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(10000, u256); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(10000, u256); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(10000, u256); +list_mock SetAccountStorageHook ( 7089066454178295295 , 9900 ) ukmNoResult(); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(0, u256); +list_mock SetAccountStorageHook ( 7089066454179379067 , 100 ) ukmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9900, u256); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(100, u256); +list_mock SetAccountStorageHook ( 7089066454178299391 , 200 ) ukmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178299391 ) ukmIntResult(200, u256); +list_mock SetAccountStorageHook ( 7089066454178299391 , 0 ) ukmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9900, u256); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9900, u256); +list_mock SetAccountStorageHook ( 7089066454178295295 , 9700 ) ukmNoResult(); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(100, u256); +list_mock SetAccountStorageHook ( 7089066454179379067 , 300 ) ukmNoResult(); +list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9700, u256); +list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(300, u256); push "#init"; hold_string_from_test_stack; diff --git a/tests/ukm-with-contract/storage.key.run b/tests/ukm-with-contract/storage.key.run index 8eb6705..8d54dcf 100644 --- a/tests/ukm-with-contract/storage.key.run +++ b/tests/ukm-with-contract/storage.key.run @@ -1,5 +1,5 @@ -mock SetAccountStorageHook ( 7010817630605304703 , 123 ) ukmNoResult(); -mock GetAccountStorageHook ( 7010817630605304703 ) ukmIntResult(123, u64); +mock SetAccountStorageHook ( 8738216329482039167 , 123 ) ukmNoResult(); +mock GetAccountStorageHook ( 8738216329482039167 ) ukmIntResult(123, u64); push "setMyDataKey"; hold_string_from_test_stack; diff --git a/ukm-semantics/main/encoding.md b/ukm-semantics/main/encoding.md index a802f75..98e10fd 100644 --- a/ukm-semantics/main/encoding.md +++ b/ukm-semantics/main/encoding.md @@ -3,6 +3,7 @@ requires "encoding/encoder.md" requires "encoding/impl.md" requires "encoding/syntax.md" +requires "encoding/encoder.md" module UKM-ENCODING imports private UKM-CALLDATA-ENCODER diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md index 8f88731..a560feb 100644 --- a/ukm-semantics/main/encoding/encoder.md +++ b/ukm-semantics/main/encoding/encoder.md @@ -1,69 +1,91 @@ ```k requires "plugin/krypto.md" +module UKM-ENCODING-HELPER + imports private BYTES + imports private INT-SYNTAX + imports private KRYPTO + imports private STRING + imports private UKM-ENCODING-HELPER-SYNTAX + + // TODO: Error for argument of length 1 or string not hex + rule encodeHexBytes(_:String) => .Bytes + [owise] + rule encodeHexBytes(S:String) + => Int2Bytes(2, String2Base(substrString(S, 0, 2), 16), BE) + +Bytes encodeHexBytes(substrString(S, 2, lengthString(S))) + requires 2 <=Int lengthString(S) andBool isHex(substrString(S, 0, 2), 0) + + syntax Bool ::= isHex(String, idx:Int) [function, total] + rule isHex(S:String, I:Int) => true + requires I isHexDigit(substrString(S, I, I +Int 1)) andBool isHex(S, I +Int 1) + requires 0 <=Int I andBool I ("0" <=String S andBool S <=String "9") + orBool ("a" <=String S andBool S <=String "f") + orBool ("A" <=String S andBool S <=String "F") + + // Encoding of individual types + + rule convertToKBytes(i8(V) , "int8") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i16(V), "int16") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u16(V), "uint16") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i32(V), "int32") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u32(V), "uint32") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i64(V), "int64") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint64") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u128(V), "uint128") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(true, "bool") => Int2Bytes(32, 1, BE:Endianness) + rule convertToKBytes(false, "bool") => Int2Bytes(32, 0, BE:Endianness) + rule convertToKBytes(u256(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + +endmodule + module UKM-CALLDATA-ENCODER - imports private COMMON-K-CELL + imports private BYTES + imports private INT-SYNTAX + imports private KRYPTO + imports private STRING imports private UKM-ENCODING-SYNTAX - imports private UKM-PREPROCESSING-ENDPOINTS - imports STRING - imports BYTES - imports INT - imports KRYPTO + imports private UKM-ENCODING-HELPER-SYNTAX + imports private UKM-ENCODING-HELPER + + rule encodeFunctionSignatureAsBytes(FS) + => encodeHexBytes(substrString(Keccak256(String2Bytes(FS)), 0, 8)) + rule encodeFunctionSignatureAsBytes(E:SemanticsError) => E - // TODO: 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) => encodeFunctionSignatureHelper(RL:List, FuncName +String "(") [priority(40)] rule encodeFunctionSignatureHelper(ListItem(FuncParam:String) RL:List, FS) => - encodeFunctionSignatureHelper(RL, FS +String FuncParam +String ",") [owise] + encodeFunctionSignatureHelper(RL, FS +String FuncParam +String ",") [owise] // The last param does not have a follow up comma rule encodeFunctionSignatureHelper(ListItem(FuncParam:String) .List, FS) => - encodeFunctionSignatureHelper(.List, FS +String FuncParam ) - - rule encodeFunctionSignatureHelper(.List, FS) => String2Bytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) + encodeFunctionSignatureHelper(.List, FS +String FuncParam ) - // TODO: Implement helper functions and break down encodeFunctionSignatureAsString - // into smaller productions. Trigger errors for each of the - // possible functions which can be failure causes. - rule encodeFunctionSignatureAsString(FS) => substrString(Keccak256(String2Bytes(FS)), 0, 8) - rule encodeFunctionSignatureAsString(FS) => error("Failed to apply the Keccak256 of function signature.", FS) [owise] + rule encodeFunctionSignatureHelper(.List, FS) => encodeHexBytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) // Function parameters encoding rule encodeFunctionParams(ListItem(V:Value) ARGS:List, ListItem(T:String) PTYPES:List, B:Bytes) => encodeFunctionParams(ARGS:List, PTYPES:List, B:Bytes +Bytes convertToKBytes(V, T)) rule encodeFunctionParams(.List, .List, B:Bytes) => B - - - // Encoding of individual types - - rule convertToKBytes(i8(V) , "int8") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i16(V), "int16") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u16(V), "uint16") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i32(V), "int32") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u32(V), "uint32") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i64(V), "int64") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u64(V), "uint64") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u128(V), "uint128") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(true, "bool") => Int2Bytes(32, 1, BE:Endianness) - rule convertToKBytes(false, "bool") => Int2Bytes(32, 0, BE:Endianness) - rule convertToKBytes(u256(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u160(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u160(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - endmodule ``` \ No newline at end of file diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md index 6be1457..0f6af3f 100644 --- a/ukm-semantics/main/encoding/syntax.md +++ b/ukm-semantics/main/encoding/syntax.md @@ -8,14 +8,26 @@ module UKM-ENCODING-SYNTAX syntax UKMInstruction ::= "ukmEncodePreprocessedCell" | ukmEncodedPreprocessedCell(Bytes) + // TODO: Make these functions total and returning BytesOrError syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list | encodeFunctionSignature (String, List) [function] | encodeFunctionSignatureHelper (List, String) [function] | encodeFunctionParams (List, List, Bytes) [function] - | convertToKBytes ( Value , String ) [function] - syntax StringOrError ::= encodeFunctionSignatureAsString(StringOrError) [function, total] + syntax BytesOrError ::= encodeFunctionSignatureAsBytes(StringOrError) [function, total] + +endmodule + +module UKM-ENCODING-HELPER-SYNTAX + imports BYTES-SYNTAX + imports LIST + imports RUST-REPRESENTATION + imports UKM-REPRESENTATION + + // TODO: Make convertToKBytes total + syntax Bytes ::= encodeHexBytes(String) [function, total] + | convertToKBytes ( Value , String ) [function] endmodule -``` +``` \ No newline at end of file diff --git a/ukm-semantics/main/hooks/bytes.md b/ukm-semantics/main/hooks/bytes.md index 3ce1ae9..78ee3c3 100644 --- a/ukm-semantics/main/hooks/bytes.md +++ b/ukm-semantics/main/hooks/bytes.md @@ -15,24 +15,21 @@ module UKM-HOOKS-BYTES-CONFIGURATION endmodule -module UKM-HOOKS-BYTES-SYNTAX - imports BYTES-SYNTAX - syntax Expression ::= ukmBytesNew(Bytes) -endmodule - module UKM-HOOKS-BYTES imports private BYTES imports private COMMON-K-CELL + imports private K-EQUAL-SYNTAX imports private RUST-HELPERS imports private RUST-REPRESENTATION imports private UKM-HOOKS-BYTES-CONFIGURATION - imports private UKM-HOOKS-BYTES-SYNTAX imports private UKM-REPRESENTATION syntax Identifier ::= "bytes_hooks" [token] | "empty" [token] | "length" [token] + | "equals" [token] + | "append_bool" [token] | "append_u256" [token] | "append_u160" [token] | "append_u128" [token] @@ -40,7 +37,6 @@ module UKM-HOOKS-BYTES | "append_u32" [token] | "append_u16" [token] | "append_u8" [token] - | "append_bool" [token] | "append_str" [token] | "decode_u256" [token] | "decode_u160" [token] @@ -77,6 +73,13 @@ module UKM-HOOKS-BYTES ) => ukmBytesLength(BufferIdId) + rule + normalizedFunctionCall + ( :: bytes_hooks :: equals :: .PathExprSegments + , BufferIdId1:Ptr, BufferIdId2:Ptr, .PtrList + ) + => ukmBytesEquals(BufferIdId1, BufferIdId2) + rule normalizedFunctionCall ( :: bytes_hooks :: append_u256 :: .PathExprSegments @@ -145,49 +148,49 @@ module UKM-HOOKS-BYTES ( :: bytes_hooks :: decode_u256 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, u256, 32) + => ukmBytesDecode(BufferIdId, u256) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u160 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, u160, 32) + => ukmBytesDecode(BufferIdId, u160) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u128 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, u128, 32) + => ukmBytesDecode(BufferIdId, u128) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u64 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, u64, 32) + => ukmBytesDecode(BufferIdId, u64) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u32 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, u32, 32) + => ukmBytesDecode(BufferIdId, u32) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u16 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, u16, 32) + => ukmBytesDecode(BufferIdId, u16) rule normalizedFunctionCall ( :: bytes_hooks :: decode_u8 :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, u8, 32) + => ukmBytesDecode(BufferIdId, u8) rule normalizedFunctionCall @@ -208,7 +211,7 @@ module UKM-HOOKS-BYTES ( :: bytes_hooks :: decode_signature :: .PathExprSegments , BufferIdId:Ptr, .PtrList ) - => ukmBytesDecodeWithLength(BufferIdId, str, 8) + => ukmBytesDecodeBytes(BufferIdId, 8) // --------------------------------------- rule @@ -223,18 +226,21 @@ module UKM-HOOKS-BYTES syntax UKMInstruction ::= ukmBytesLength(Expression) [strict(1)] | ukmBytesLength(UkmExpression) [strict(1)] + | ukmBytesEquals(Expression, Expression) [seqstrict] + | ukmBytesEquals(UkmExpression, UkmExpression) [seqstrict] | ukmBytesAppendInt(Expression, Expression) [seqstrict] | ukmBytesAppendInt(UkmExpression, Int) [strict(1)] | ukmBytesAppendBool(Expression, Expression) [seqstrict] | ukmBytesAppendStr(Expression, Expression) [seqstrict] | ukmBytesAppendBytes(UkmExpression, Bytes) [strict(1)] - | ukmBytesAppendLenAndBytes(Bytes, Bytes) + | ukmBytesAppendLenAndBytes(UkmExpression, Bytes) [strict(1)] | ukmBytesDecode(Expression, Type) [strict(1)] | ukmBytesDecode(UkmExpression, Type) [strict(1)] - | ukmBytesDecodeWithLength(Expression, Type, Int) [strict(1)] - | ukmBytesDecodeWithLength(UkmExpression, Type, Int) [strict(1)] + | ukmBytesDecodeBytes(Expression, Int) [strict(1)] + | ukmBytesDecodeBytes(UkmExpression, Int) [strict(1)] | ukmBytesDecode(Int, Bytes, Type) | ukmBytesDecodeInt(Int, Bytes, Type) + | ukmBytesDecodeStr(Int, Bytes) | ukmBytesDecode(ValueOrError, Bytes) | ukmBytesHash(Expression) [strict(1)] | ukmBytesHash(UkmExpression) [strict(1)] @@ -258,6 +264,11 @@ module UKM-HOOKS-BYTES => ptrValue(null, u32(Int2MInt(lengthBytes(Value)))) requires notBool uoverflowMInt(32, lengthBytes(Value)) + rule ukmBytesEquals(ptrValue(_, u64(BytesId1)), ptrValue(_, u64(BytesId2))) + => ukmBytesEquals(ukmBytesId(BytesId1), ukmBytesId(BytesId2)) + rule ukmBytesEquals(ukmBytesValue(Value1:Bytes), ukmBytesValue(Value2:Bytes)) + => ptrValue(null, Value1 ==K Value2) + rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u256(Value))) => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) rule ukmBytesAppendInt(ptrValue(_, u64(BytesId)), ptrValue(_, u160(Value))) @@ -274,66 +285,61 @@ module UKM-HOOKS-BYTES => ukmBytesAppendInt(ukmBytesId(BytesId), MInt2Unsigned(Value)) rule ukmBytesAppendInt(ukmBytesValue(B:Bytes), Value:Int) - => ukmBytesAppendLenAndBytes(B, Int2Bytes(Value, BE, Unsigned)) + => ukmBytesNew(B +Bytes Int2Bytes(32, Value, BE)) rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, false)) => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(0p8))) rule ukmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true)) => ukmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8))) + // TODO: This can create key ambiguity for storage rule ukmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String)) - => ukmBytesAppendBytes(ukmBytesId(BytesId), String2Bytes(Value)) + => ukmBytesAppendLenAndBytes(ukmBytesId(BytesId), String2Bytes(Value)) rule ukmBytesAppendBytes(ukmBytesValue(B:Bytes), Value:Bytes) - => ukmBytesAppendLenAndBytes(B, Value) + => ukmBytesNew(B +Bytes Value) - rule ukmBytesAppendLenAndBytes(First:Bytes, Second:Bytes) + rule ukmBytesAppendLenAndBytes(ukmBytesValue(First:Bytes), Second:Bytes) => ukmBytesNew(First +Bytes Int2Bytes(2, lengthBytes(Second), BE) +Bytes Second) requires lengthBytes(Second) ukmBytesDecodeWithLength(ukmBytesId(BytesId), T:Type, L:Int) - rule ukmBytesDecodeWithLength(ukmBytesValue(B:Bytes), T:Type, L:Int) - => ukmBytesDecode - ( L - , B - , T:Type + rule ukmBytesDecodeBytes(ptrValue(_, u64(BytesId)), L:Int) + => ukmBytesDecodeBytes(ukmBytesId(BytesId), L:Int) + rule ukmBytesDecodeBytes(ukmBytesValue(B:Bytes), L:Int) + => tupleExpression + ( ukmBytesNew(substrBytes(B, L, lengthBytes(B))) + , ukmBytesNew(substrBytes(B, 0, L)) + , .TupleElementsNoEndComma ) requires L <=Int lengthBytes(B) - rule 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) => ukmBytesDecode - ( Bytes2Int(substrBytes(B, 0, 2), BE, Unsigned) - , substrBytes(B, 2, lengthBytes(B)) - , T:Type - ) - requires 2 <=Int lengthBytes(B) - rule ukmBytesDecode(Len:Int, B:Bytes, T:Type) - => ukmBytesDecodeInt - ( Bytes2Int(substrBytes(B, 0, Len), BE, Unsigned) - , substrBytes(B, Len, lengthBytes(B)) - , T:Type + ( integerToValue(Bytes2Int(substrBytes(B, 0, 32), BE, Unsigned), T) + , substrBytes(B, 32, lengthBytes(B)) ) - requires Len <=Int lengthBytes(B) andBool isUnsignedInt(T) - rule ukmBytesDecode(Len:Int, B:Bytes, T:Type) - => ukmBytesDecodeInt - ( Bytes2Int(substrBytes(B, 0, Len), BE, Signed) - , substrBytes(B, Len, lengthBytes(B)) - , T:Type - ) - requires Len <=Int lengthBytes(B) andBool isSignedInt(T) - rule ukmBytesDecode(Len:Int, B:Bytes, str) + requires isUnsignedInt(T) andBool 32 <=Int lengthBytes(B) + rule ukmBytesDecode(ukmBytesValue(B:Bytes), T:Type) => ukmBytesDecode - ( Bytes2String(substrBytes(B, 0, Len)) - , substrBytes(B, Len, lengthBytes(B)) + ( integerToValue(Bytes2Int(substrBytes(B, 0, 32), BE, Signed), T) + , substrBytes(B, 32, lengthBytes(B)) ) - requires Len <=Int lengthBytes(B) + requires isSignedInt(T) andBool 32 <=Int lengthBytes(B) + rule ukmBytesDecode(ukmBytesValue(B:Bytes), str) + => ukmBytesDecodeStr + ( Bytes2Int(substrBytes(B, 0, 2), BE, Signed) + , substrBytes(B, 2, lengthBytes(B)) + ) + requires 2 <=Int lengthBytes(B) + rule ukmBytesDecodeInt(Value:Int, B:Bytes, T:Type) => ukmBytesDecode(integerToValue(Value, T), B) + rule ukmBytesDecodeStr(Len:Int, B:Bytes) + => ukmBytesDecode(Bytes2String(substrBytes(B, 0, Len)), substrBytes(B, Len, lengthBytes(B))) + requires 0 <=Int Len andBool Len <=Int lengthBytes(B) + rule ukmBytesDecode(Value:Value, B:Bytes) => tupleExpression(ukmBytesNew(B) , ptrValue(null, Value) , .TupleElementsNoEndComma) diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md index 5246aba..1129d38 100644 --- a/ukm-semantics/main/hooks/ukm.md +++ b/ukm-semantics/main/hooks/ukm.md @@ -18,9 +18,9 @@ endmodule module UKM-HOOKS-UKM imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX - imports private UKM-HOOKS-BYTES-SYNTAX imports private UKM-HOOKS-SIGNATURE imports private UKM-HOOKS-UKM-SYNTAX + imports private UKM-REPRESENTATION syntax Identifier ::= "ukm" [token] | "CallData" [token] @@ -67,9 +67,9 @@ endmodule // for the ULM hooks. module UKM-HOOKS-TO-ULM-FUNCTIONS imports private RUST-REPRESENTATION - imports private UKM-HOOKS-BYTES-SYNTAX imports private UKM-HOOKS-UKM-SYNTAX imports private ULM-HOOKS + imports private UKM-REPRESENTATION rule CallDataHook() => ukmBytesNew(CallData()) rule CallerHook() => ukmIntResult(Caller(), u160) diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md index 034a0b6..5128220 100644 --- a/ukm-semantics/main/preprocessing/endpoints.md +++ b/ukm-semantics/main/preprocessing/endpoints.md @@ -7,9 +7,11 @@ module UKM-PREPROCESSING-ENDPOINTS imports private RUST-PREPROCESSING-CONFIGURATION imports private RUST-SHARED-SYNTAX imports private UKM-COMMON-TOOLS-SYNTAX + imports private UKM-ENCODING-SYNTAX imports private UKM-PREPROCESSING-EPHEMERAL-CONFIGURATION imports private UKM-PREPROCESSING-SYNTAX-PRIVATE imports private UKM-ENCODING-SYNTAX + imports private UKM-REPRESENTATION rule @@ -91,7 +93,7 @@ module UKM-PREPROCESSING-ENDPOINTS rule - ukmAddEndpointSignature(Signature:String, Method:Identifier) => .K + ukmAddEndpointSignature(Signature:Bytes, Method:Identifier) => .K ... @@ -166,17 +168,18 @@ module UKM-PREPROCESSING-ENDPOINTS | "decode_str" [token] | "decode_signature" [token] | "empty" [token] + | "equals" [token] | "ukm" [token] | "CallData" [token] | "EVMC_BAD_JUMP_DESTINATION" [token] | "EVMC_SUCCESS" [token] - syntax StringOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total] - | signatureTypes(NormalizedFunctionParameterList) [function, total] + syntax BytesOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total] + syntax StringOrError ::= signatureTypes(NormalizedFunctionParameterList) [function, total] | signatureType(Type) [function, total] rule methodSignature(S:String, Ps:NormalizedFunctionParameterList) - => encodeFunctionSignatureAsString(concat(concat(S +String "(", signatureTypes(Ps)), ")")) + => encodeFunctionSignatureAsBytes(concat(concat(S +String "(", signatureTypes(Ps)), ")")) rule signatureTypes(.NormalizedFunctionParameterList) => "" rule signatureTypes(_ : T:Type , .NormalizedFunctionParameterList) @@ -217,12 +220,13 @@ module UKM-PREPROCESSING-ENDPOINTS rule signatureToCall (... signature: Signature:Identifier - , signatures: ListItem(CurrentSignature:String) Signatures:List + , signatures: ListItem(CurrentSignature:Bytes) Signatures:List , signatureToMethod: (CurrentSignature |-> Method:Identifier _:Map) #as SignatureToMethod:Map , bufferId: BufferId:Identifier , gas: Gas:Identifier ) - => if signature == CurrentSignature { + => if :: bytes_hooks :: equals + ( Signature , ukmBytesNew(CurrentSignature) , .CallParamsList ) { .InnerAttributes self . Method ( BufferId , Gas , .CallParamsList ); .NonEmptyStatements diff --git a/ukm-semantics/main/preprocessing/storage.md b/ukm-semantics/main/preprocessing/storage.md index a6b108a..2475292 100644 --- a/ukm-semantics/main/preprocessing/storage.md +++ b/ukm-semantics/main/preprocessing/storage.md @@ -1,6 +1,7 @@ ```k module UKM-PREPROCESSING-STORAGE + imports private BYTES imports private COMMON-K-CELL imports private RUST-ERROR-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md index c186d6d..ec39c7e 100644 --- a/ukm-semantics/main/preprocessing/syntax.md +++ b/ukm-semantics/main/preprocessing/syntax.md @@ -10,6 +10,7 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE imports LIST imports RUST-REPRESENTATION imports RUST-SHARED-SYNTAX + imports UKM-REPRESENTATION syntax UKMInstruction ::= ukmPreprocessTraits(List) | ukmPreprocessTrait(TypePath) @@ -34,7 +35,7 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE , appendReturn: ExpressionOrError , decodeStatements: NonEmptyStatementsOrError ) - | ukmAddEndpointSignature(signature: StringOrError, method: Identifier) + | ukmAddEndpointSignature(signature: BytesOrError, method: Identifier) | ukmAddDispatcher(TypePath) | ukmPreprocessStorage ( fullMethodPath: PathInExpression diff --git a/ukm-semantics/main/representation.md b/ukm-semantics/main/representation.md index 50af36f..412bdaf 100644 --- a/ukm-semantics/main/representation.md +++ b/ukm-semantics/main/representation.md @@ -1,10 +1,10 @@ ```k module UKM-REPRESENTATION - imports private BYTES-SYNTAX - imports private INT-SYNTAX - imports private MINT - imports private RUST-VALUE-SYNTAX + imports BYTES-SYNTAX + imports INT-SYNTAX + imports MINT + imports RUST-VALUE-SYNTAX syntax UkmValue ::= ukmBytesValue(Bytes) | ukmIntValue(Int) @@ -14,8 +14,12 @@ module UKM-REPRESENTATION syntax KResult ::= UkmValue syntax Expression ::= ukmCast(Expression, Expression) [seqstrict] + syntax Expression ::= ukmBytesNew(Bytes) + syntax Value ::= rustType(Type) + syntax BytesOrError ::= Bytes | SemanticsError + endmodule ``` diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md index b2f1f70..b0e2281 100644 --- a/ukm-semantics/targets/testing/ukm-target.md +++ b/ukm-semantics/targets/testing/ukm-target.md @@ -19,6 +19,7 @@ module UKM-TARGET imports private RUST-COMMON imports private RUST-FULL-PREPROCESSING imports private RUST-EXECUTION-TEST + imports private UKM-CALLDATA-ENCODER imports private UKM-EXECUTION imports private UKM-ENCODING imports private UKM-PREPROCESSING diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index b6e4f1a..b0f0d3b 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -1,6 +1,7 @@ ```k module UKM-TEST-SYNTAX + imports BYTES-SYNTAX imports INT-SYNTAX imports STRING-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX @@ -43,15 +44,17 @@ module UKM-TEST-SYNTAX endmodule module UKM-TEST-EXECUTION + imports private BYTES imports private COMMON-K-CELL imports private RUST-EXECUTION-TEST-CONFIGURATION + imports private RUST-SHARED-SYNTAX imports private UKM-ENCODING-SYNTAX imports private UKM-EXECUTION-SYNTAX imports private UKM-HOOKS-BYTES-CONFIGURATION - imports private UKM-HOOKS-BYTES-SYNTAX imports private UKM-HOOKS-HELPERS-SYNTAX imports private UKM-HOOKS-STATE-CONFIGURATION imports private UKM-HOOKS-UKM-SYNTAX + imports private UKM-REPRESENTATION imports private UKM-TEST-SYNTAX imports RUST-SHARED-SYNTAX imports private BYTES