Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Call data encoding and decoding #171

Merged
merged 3 commits into from
Oct 24, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions tests/ukm-contracts/bytes_hooks.rs
Original file line number Diff line number Diff line change
@@ -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;
}
4 changes: 2 additions & 2 deletions tests/ukm-no-contract/test_bytes_hooks.append32.run
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions tests/ukm-no-contract/test_bytes_hooks.append64.run
Original file line number Diff line number Diff line change
@@ -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
2 changes: 1 addition & 1 deletion tests/ukm-with-contract/endpoints.2.run
Original file line number Diff line number Diff line change
@@ -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"
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"
40 changes: 20 additions & 20 deletions tests/ukm-with-contract/erc_20_token.1.run
Original file line number Diff line number Diff line change
@@ -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;
4 changes: 2 additions & 2 deletions tests/ukm-with-contract/storage.key.run
Original file line number Diff line number Diff line change
@@ -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;
1 change: 1 addition & 0 deletions ukm-semantics/main/encoding.md
Original file line number Diff line number Diff line change
@@ -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
100 changes: 61 additions & 39 deletions ukm-semantics/main/encoding/encoder.md
Original file line number Diff line number Diff line change
@@ -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 <Int 0 orBool lengthString(S) <=Int I
rule isHex(S:String, I:Int)
=> isHexDigit(substrString(S, I, I +Int 1)) andBool isHex(S, I +Int 1)
requires 0 <=Int I andBool I <Int lengthString(S)
syntax Bool ::= isHexDigit(String) [function, total]
rule isHexDigit(S)
=> ("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
```
18 changes: 15 additions & 3 deletions ukm-semantics/main/encoding/syntax.md
Original file line number Diff line number Diff line change
@@ -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
```
```
112 changes: 59 additions & 53 deletions ukm-semantics/main/hooks/bytes.md
Original file line number Diff line number Diff line change
@@ -15,32 +15,28 @@ module UKM-HOOKS-BYTES-CONFIGURATION
</ukm-bytes>
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]
| "append_u64" [token]
| "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) <Int (1 <<Int 16)
rule ukmBytesDecodeWithLength(ptrValue(_, u64(BytesId)), T:Type, L:Int)
=> 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)
4 changes: 2 additions & 2 deletions ukm-semantics/main/hooks/ukm.md
Original file line number Diff line number Diff line change
@@ -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)
16 changes: 10 additions & 6 deletions ukm-semantics/main/preprocessing/endpoints.md
Original file line number Diff line number Diff line change
@@ -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
<k>
@@ -91,7 +93,7 @@ module UKM-PREPROCESSING-ENDPOINTS
rule
<k>
ukmAddEndpointSignature(Signature:String, Method:Identifier) => .K
ukmAddEndpointSignature(Signature:Bytes, Method:Identifier) => .K
...
</k>
<ukm-endpoint-signatures>
@@ -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
1 change: 1 addition & 0 deletions ukm-semantics/main/preprocessing/storage.md
Original file line number Diff line number Diff line change
@@ -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
3 changes: 2 additions & 1 deletion ukm-semantics/main/preprocessing/syntax.md
Original file line number Diff line number Diff line change
@@ -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
12 changes: 8 additions & 4 deletions ukm-semantics/main/representation.md
Original file line number Diff line number Diff line change
@@ -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
```
1 change: 1 addition & 0 deletions ukm-semantics/targets/testing/ukm-target.md
Original file line number Diff line number Diff line change
@@ -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
5 changes: 4 additions & 1 deletion ukm-semantics/test/execution.md
Original file line number Diff line number Diff line change
@@ -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