Implement logging (#183)

* Implement logging * Add TODOs
Pi-Squared-Inc · Nov 8, 2024 · ff3d6ef · ff3d6ef
1 parent fe12c11
commit ff3d6ef
Show file tree

Hide file tree

Showing 11 changed files with 356 additions and 78 deletions.
diff --git a/rust-semantics/expression/literals.md b/rust-semantics/expression/literals.md
@@ -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))

diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md
@@ -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
 ```
diff --git a/rust-semantics/representation.md b/rust-semantics/representation.md
@@ -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
 
@@ -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
 
 ```
diff --git a/tests/ulm-contracts/ulm.rs b/tests/ulm-contracts/ulm.rs
@@ -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;
@@ -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;
@@ -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;
@@ -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;

diff --git a/tests/ulm-with-contract/erc_20_token.1.run b/tests/ulm-with-contract/erc_20_token.1.run
@@ -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();
 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);
 
@@ -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; 
@@ -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;
@@ -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; 
@@ -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;
@@ -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;
@@ -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;
@@ -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;
@@ -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;

diff --git a/tests/ulm-with-contract/events.1.run b/tests/ulm-with-contract/events.1.run
@@ -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";

diff --git a/ulm-semantics/main/encoding/encoder.md b/ulm-semantics/main/encoding/encoder.md
@@ -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 
@@ -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
 
 ```
diff --git a/ulm-semantics/main/encoding/syntax.md b/ulm-semantics/main/encoding/syntax.md
@@ -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