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.

Sign up for GitHub

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

Implement logging #183

Merged
merged 2 commits into from
Nov 8, 2024
+356 −78
Merged

Implement logging #183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7e0483f
Implement logging
virgil-serbanuta Nov 6, 2024
4c36d60
Add TODOs
virgil-serbanuta Nov 8, 2024
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
1 change: 1 addition & 0 deletions rust-semantics/expression/literals.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,7 @@ module RUST-EXPRESSION-INTEGER-LITERALS
andBool isHexadecimal(substrString(S, 1, lengthString(S)))
[owise]

rule integerToValue(E:SemanticsError, _) => E
rule integerToValue(I:Int, i8) => i8(Int2MInt(I))
requires sminMInt(8) <=Int I andBool I <=Int smaxMInt(8)
rule integerToValue(I:Int, u8) => u8(Int2MInt(I))
Expand Down
23 changes: 23 additions & 0 deletions rust-semantics/helpers.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,5 +50,28 @@ module RUST-HELPERS
rule concatNonEmptyStatements(.NonEmptyStatements, S:NonEmptyStatements) => S
rule concatNonEmptyStatements(S:Statement Ss1:NonEmptyStatements, Ss2:NonEmptyStatements)
=> S concatNonEmptyStatements(Ss1, Ss2)

rule length(.NormalizedFunctionParameterList) => 0
rule length(_:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList)
=> 1 +Int length(Ps)

rule last(P:NormalizedFunctionParameter, .NormalizedFunctionParameterList) => P
rule last
( _:NormalizedFunctionParameter
, (P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList)
)
=> last(P, Ps)

rule allButLast(_:NormalizedFunctionParameter, .NormalizedFunctionParameterList)
=> .NormalizedFunctionParameterList
rule allButLast
( Q:NormalizedFunctionParameter
, (P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList)
)
=> Q , allButLast(P, Ps)

rule concatCallParamsList(.CallParamsList, S:CallParamsList) => S
rule concatCallParamsList(S:Expression , Ss1:CallParamsList, Ss2:CallParamsList)
=> S , concatCallParamsList(Ss1, Ss2)
endmodule
```
8 changes: 7 additions & 1 deletion rust-semantics/representation.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ module RUST-REPRESENTATION

syntax IntOrError ::= Int | SemanticsError
syntax IntOrError ::= valueToInteger(Value) [function, total]
syntax ValueOrError ::= integerToValue(Int, Type) [function, total]
syntax ValueOrError ::= integerToValue(IntOrError, Type) [function, total]

syntax StringOrError ::= String | SemanticsError

Expand Down Expand Up @@ -196,6 +196,12 @@ module RUST-REPRESENTATION
syntax NonEmptyStatementsOrError ::= NonEmptyStatements | SemanticsError
syntax NonEmptyStatements ::= concatNonEmptyStatements(NonEmptyStatements, NonEmptyStatements) [function, total]

syntax CallParamsList ::= concatCallParamsList(CallParamsList, CallParamsList) [function, total]

syntax Int ::= length(NormalizedFunctionParameterList) [function, total]
syntax NormalizedFunctionParameter ::= last(NormalizedFunctionParameter, NormalizedFunctionParameterList) [function, total]
syntax NormalizedFunctionParameterList ::= allButLast(NormalizedFunctionParameter, NormalizedFunctionParameterList) [function, total]

endmodule

```
34 changes: 17 additions & 17 deletions tests/ulm-contracts/ulm.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
#![no_std]

// TODO: Support structs and figure out the content of MessageResult
struct MessageResult { gas: u64 }
struct MessageResult { gas: u256 }

pub const EVMC_REJECTED: u64 = 0_u64;
pub const EVMC_INTERNAL_ERROR: u64 = 1_u64;
Expand All @@ -22,19 +22,19 @@ pub const EVMC_NONCE_EXCEEDED: u64 = 15_u64;

extern {
// block parameters
fn sample_method(&self) -> u64;
fn sample_method(&self) -> u256;
fn GasLimit(&self) -> u256;
fn BaseFee(&self) -> u256;
fn Coinbase(&self) -> u64;
fn BlockTimestamp(&self) -> u64;
fn BlockNumber(&self) -> u64;
fn BlockDifficulty(&self) -> u64;
fn PrevRandao(&self) -> u64;
fn BlockHash(&self, index: u64) -> u64;
fn Coinbase(&self) -> u256;
fn BlockTimestamp(&self) -> u256;
fn BlockNumber(&self) -> u256;
fn BlockDifficulty(&self) -> u256;
fn PrevRandao(&self) -> u256;
fn BlockHash(&self, index: u256) -> u256;

// transaction parameters
fn GasPrice(&self) -> u64;
fn Origin(&self) -> u64;
fn GasPrice(&self) -> u256;
fn Origin(&self) -> u256;

// message parameters
fn Address(&self) -> u160;
Expand All @@ -43,7 +43,7 @@ extern {
fn CallData(&self) -> Bytes;

// chain parameters
fn ChainId(&self) -> u64;
fn ChainId(&self) -> u256;

// account getters
fn GetAccountBalance(&self, acct: u160) -> u256;
Expand All @@ -58,17 +58,17 @@ extern {
fn AccessedAccount(&self, acct: u256) -> bool;

fn Transfer(&self, to: u160, value: u256) -> bool;
fn SelfDestruct(&self, to: u64);
fn SelfDestruct(&self, to: u256);
fn SetAccountStorage(&self, key: u256, value: u256);
fn SetAccountTransientStorage(&self, key: u256, value: u256);

fn Log0(data: Bytes);
fn Log1(topic0: u64, data: Bytes);
fn Log2(topic0: u64, topic1: u64, data: Bytes);
fn Log3(topic0: u64, topic1: u64, topic2: u64, data: Bytes);
fn Log4(topic0: u64, topic1: u64, topic2: u64, topic3: u64, data: Bytes);
fn Log1(topic0: u256, data: Bytes);
fn Log2(topic0: u256, topic1: u256, data: Bytes);
fn Log3(topic0: u256, topic1: u256, topic2: u256, data: Bytes);
fn Log4(topic0: u256, topic1: u256, topic2: u256, topic3: u256, data: Bytes);

fn MessageResult(gas: u256, data: Bytes, status: u64, target: u64) -> MessageResult;
fn MessageResult(gas: u256, data: Bytes, status: u256, target: u256) -> MessageResult;
fn Create(value: u256, data: Bytes, gas: u256) -> MessageResult;
fn Create2(value: u256, data: Bytes, salt: Bytes, gas: u256) -> MessageResult;
fn Call(gas: u256, to: u160, value: u256, data: Bytes) -> MessageResult;
Expand Down
21 changes: 12 additions & 9 deletions tests/ulm-with-contract/erc_20_token.1.run
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,16 +8,19 @@ list_mock GetAccountStorageHook ( 1154948450467236006739439905978168116697077396
list_mock SetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 , 9900 ) ulmNoResult();
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(0, u256);
list_mock SetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 , 100 ) ulmNoResult();
list_mock Log3Hook ( 100389287136786176327247604509743168900146139575972864366142685224231313322991 , 1010101 , 2020202 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00d" ) ulmNoResult();
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this the expected topic0, topic1, topic2, and bytes corresponding to an event in erc20? If so, which one, and how can I generally figure out which one?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, these are the topics, in order, and the bytes. These mocks (storage + logs) were developed in a hurry, when we already not fully confident that we can finish until the demo, so we cut corners. They should be implemented in a similar way to the call mocks (see examples in the same file, below), and call mocks themselves could be implemented better (e.g. we could put the entire function signature in a single string instead of building it piece by piece).

If there is interest in the Rust semantics after the demo, this is one of the things that should be fixed.

list_mock GetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 ) ulmIntResult(9900, u256);
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(100, u256);
list_mock SetAccountStorageHook ( 97321503972240892886219376522881926110074550168465622121824657360422868161783 , 200 ) ulmNoResult();
list_mock Log3Hook ( 63486140976153616755203102783360879283472101686154884697241723088393386309925 , 1010101 , 3030303 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" ) ulmNoResult();
list_mock GetAccountStorageHook ( 97321503972240892886219376522881926110074550168465622121824657360422868161783 ) ulmIntResult(200, u256);
list_mock SetAccountStorageHook ( 97321503972240892886219376522881926110074550168465622121824657360422868161783 , 0 ) ulmNoResult();
list_mock GetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 ) ulmIntResult(9900, u256);
list_mock GetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 ) ulmIntResult(9900, u256);
list_mock SetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 , 9700 ) ulmNoResult();
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(100, u256);
list_mock SetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 , 300 ) ulmNoResult();
list_mock Log3Hook ( 100389287136786176327247604509743168900146139575972864366142685224231313322991 , 1010101 , 2020202 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" ) ulmNoResult();
list_mock GetAccountStorageHook ( 115494845046723600673943990597816811669707739681772931244236289759170204726560 ) ulmIntResult(9700, u256);
list_mock GetAccountStorageHook ( 17171626450567201640701347902808840427582371480602455275836469707331258301780 ) ulmIntResult(300, u256);

Expand Down Expand Up @@ -50,7 +53,7 @@ check_eq 0_u32;

push "balanceOf";
hold_string_from_test_stack;
push "uint160";
push "address";
hold_list_values_from_test_stack;
push 1010101_u160;
hold_list_values_from_test_stack;
Expand All @@ -74,7 +77,7 @@ check_eq 10000_u256;

push "transfer";
hold_string_from_test_stack;
push "uint160";
push "address";
push "uint256";
hold_list_values_from_test_stack;
push 2020202_u160;
Expand Down Expand Up @@ -103,7 +106,7 @@ check_eq 1_u64;

push "balanceOf";
hold_string_from_test_stack;
push "uint160";
push "address";
hold_list_values_from_test_stack;
push 1010101_u160;
hold_list_values_from_test_stack;
Expand All @@ -127,7 +130,7 @@ check_eq 9900_u256;

push "balanceOf";
hold_string_from_test_stack;
push "uint160";
push "address";
hold_list_values_from_test_stack;
push 2020202_u160;
hold_list_values_from_test_stack;
Expand All @@ -151,7 +154,7 @@ check_eq 100_u256;

push "approve";
hold_string_from_test_stack;
push "uint160";
push "address";
push "uint256";
hold_list_values_from_test_stack;
push 3030303_u160;
Expand Down Expand Up @@ -180,8 +183,8 @@ check_eq 1_u64;

push "transferFrom";
hold_string_from_test_stack;
push "uint160";
push "uint160";
push "address";
push "address";
push "uint256";
hold_list_values_from_test_stack;
push 1010101_u160;
Expand Down Expand Up @@ -212,7 +215,7 @@ check_eq 1_u64;

push "balanceOf";
hold_string_from_test_stack;
push "uint160";
push "address";
hold_list_values_from_test_stack;
push 1010101_u160;
hold_list_values_from_test_stack;
Expand All @@ -237,7 +240,7 @@ check_eq 9700_u256;

push "balanceOf";
hold_string_from_test_stack;
push "uint160";
push "address";
hold_list_values_from_test_stack;
push 2020202_u160;
hold_list_values_from_test_stack;
Expand Down
2 changes: 2 additions & 0 deletions tests/ulm-with-contract/events.1.run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
list_mock Log2Hook ( 74657075023537209477280918141328480329188930599530356189395812678724488965561 , 123 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02+" ) ulmNoResult();

push "logEvent";
hold_string_from_test_stack;
push "uint64";
Expand Down
72 changes: 72 additions & 0 deletions ulm-semantics/main/encoding/encoder.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,15 +52,31 @@ module ULM-CALLDATA-ENCODER
imports private BYTES
imports private INT-SYNTAX
imports private KRYPTO
imports private RUST-ERROR-SYNTAX
imports private STRING
imports private ULM-ENCODING-SYNTAX
imports private ULM-ENCODING-HELPER-SYNTAX
imports private ULM-ENCODING-HELPER

syntax Identifier ::= "bytes_hooks" [token]
| "append_u8" [token]
| "append_u16" [token]
| "append_u32" [token]
| "append_u64" [token]
| "append_u128" [token]
| "append_u160" [token]
| "append_u256" [token]
| "append_bool" [token]


rule encodeFunctionSignatureAsBytes(FS)
=> encodeHexBytes(substrString(Keccak256(String2Bytes(FS)), 0, 8))
rule encodeFunctionSignatureAsBytes(E:SemanticsError) => E

rule encodeEventSignatureAsInt(FS)
=> Bytes2Int(Keccak256raw(String2Bytes(FS)), BE, Unsigned)
rule encodeEventSignatureAsInt(E:SemanticsError) => E

// TODO: it may be worth extracting the substrString(Keccak256(String2Bytes(FS)), 0, 8)
// thing to a function that takes a String and produces a String or Bytes (as opposed to
// taking a StringOrError as below) (perhaps with an encodeAsBytes(...) on top of it) and
Expand Down Expand Up @@ -88,6 +104,62 @@ module ULM-CALLDATA-ENCODER
encodeFunctionParams(ARGS:List, PTYPES:List, B:Bytes +Bytes convertToKBytes(V, T))

rule encodeFunctionParams(.List, .List, B:Bytes) => B

rule appendValue(BufferId:Identifier, Value:Identifier, u8)
=> v(:: bytes_hooks :: append_u8 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, u16)
=> v(:: bytes_hooks :: append_u16 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, u32)
=> v(:: bytes_hooks :: append_u32 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, u64)
=> v(:: bytes_hooks :: append_u64 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, u128)
=> v(:: bytes_hooks :: append_u128 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, u160)
=> v(:: bytes_hooks :: append_u160 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, u256)
=> v(:: bytes_hooks :: append_u256 ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, Value:Identifier, bool)
=> v(:: bytes_hooks :: append_bool ( BufferId , Value , .CallParamsList ))
rule appendValue(BufferId:Identifier, _Value:Identifier, ()) => v(BufferId)
rule appendValue(BufferId:Identifier, Value:Identifier, T:Type)
=> e(error("appendValue: unrecognized type", ListItem(BufferId) ListItem(Value) ListItem(T)))
[owise]

rule methodSignature(S:String, Ps:NormalizedFunctionParameterList)
=> encodeFunctionSignatureAsBytes(concat(concat(S +String "(", signatureTypes(Ps)), ")"))

rule eventSignature(S, Ps)
=> integerToValue
( encodeEventSignatureAsInt
(concat(concat(S +String "(", signatureTypes(Ps)), ")"))
, u256
)

syntax StringOrError ::= signatureTypes(NormalizedFunctionParameterList) [function, total]
| signatureType(Type) [function, total]

rule signatureTypes(.NormalizedFunctionParameterList) => ""
rule signatureTypes(_ : T:Type , .NormalizedFunctionParameterList)
=> signatureType(T)
rule signatureTypes
( _ : T:Type
, ((_:NormalizedFunctionParameter , _:NormalizedFunctionParameterList)
#as Ps:NormalizedFunctionParameterList)
)
=> concat(signatureType(T), concat(",", signatureTypes(Ps)))

rule signatureType(u8) => "uint8"
rule signatureType(u16) => "uint16"
rule signatureType(u32) => "uint32"
rule signatureType(u64) => "uint64"
rule signatureType(u128) => "uint128"
// TODO: This is the wrong signature type. We should separate addresses from u160.
rule signatureType(u160) => "address"
rule signatureType(u256) => "uint256"
rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T))
[owise]

endmodule

```
6 changes: 6 additions & 0 deletions ulm-semantics/main/encoding/syntax.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,12 @@ module ULM-ENCODING-SYNTAX
| encodeFunctionParams (List, List, Bytes) [function]

syntax BytesOrError ::= encodeFunctionSignatureAsBytes(StringOrError) [function, total]
syntax IntOrError ::= encodeEventSignatureAsInt(StringOrError) [function, total]

syntax BytesOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total]
syntax ValueOrError ::= eventSignature(String, NormalizedFunctionParameterList) [function, total]

syntax ExpressionOrError ::= appendValue(bufferId: Identifier, value: Identifier, Type) [function, total]

endmodule

Expand Down
Loading
Loading